Safe Haskell | None |
---|---|
Language | Haskell98 |
Synopsis
- data SourcePos = SourcePos {
- sourceName :: FilePath
- sourceLine :: !Pos
- sourceColumn :: !Pos
- type SourceName = FilePath
- data SrcSpan = SS {}
- data Pos
- predPos :: Pos -> Pos
- safePos :: Int -> Pos
- safeSourcePos :: FilePath -> Int -> Int -> SourcePos
- succPos :: Pos -> Pos
- unPos :: Pos -> Int
- mkPos :: Int -> Pos
- class Loc a where
- data Located a = Loc {}
- dummySpan :: SrcSpan
- panicSpan :: String -> SrcSpan
- locAt :: String -> a -> Located a
- dummyLoc :: a -> Located a
- dummyPos :: FilePath -> SourcePos
- atLoc :: Loc l => l -> b -> Located b
- toSourcePos :: (SourceName, Line, Column) -> SourcePos
- ofSourcePos :: SourcePos -> (SourceName, Line, Column)
- sourcePosElts :: SourcePos -> (SourceName, Line, Column)
- srcLine :: Loc a => a -> Pos
Concrete Location Type
The data type SourcePos
represents source positions. It contains the
name of the source file, a line number, and a column number. Source line
and column positions change intensively during parsing, so we need to
make them strict to avoid memory leaks.
SourcePos | |
|
Instances
Eq SourcePos | |
Data SourcePos | |
Defined in Text.Megaparsec.Pos gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SourcePos -> c SourcePos # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SourcePos # toConstr :: SourcePos -> Constr # dataTypeOf :: SourcePos -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c SourcePos) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SourcePos) # gmapT :: (forall b. Data b => b -> b) -> SourcePos -> SourcePos # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SourcePos -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SourcePos -> r # gmapQ :: (forall d. Data d => d -> u) -> SourcePos -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> SourcePos -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> SourcePos -> m SourcePos # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SourcePos -> m SourcePos # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SourcePos -> m SourcePos # | |
Ord SourcePos | |
Defined in Text.Megaparsec.Pos | |
Read SourcePos | |
Show SourcePos | |
Generic SourcePos | |
Hashable SourcePos Source # | |
Defined in Language.Fixpoint.Types.Spans | |
Binary SourcePos Source # | |
Serialize SourcePos Source # | |
NFData SourcePos | |
Defined in Text.Megaparsec.Pos | |
Store SourcePos Source # | Retrofitting instances to SourcePos ------------------------------ |
PPrint SourcePos Source # | |
Defined in Language.Fixpoint.Types.Spans | |
Fixpoint SourcePos Source # | |
Loc SourcePos Source # | |
type Rep SourcePos | |
Defined in Text.Megaparsec.Pos type Rep SourcePos = D1 ('MetaData "SourcePos" "Text.Megaparsec.Pos" "megaparsec-8.0.0-9f64OxcyweJEsdVHakiLZx" 'False) (C1 ('MetaCons "SourcePos" 'PrefixI 'True) (S1 ('MetaSel ('Just "sourceName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FilePath) :*: (S1 ('MetaSel ('Just "sourceLine") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Pos) :*: S1 ('MetaSel ('Just "sourceColumn") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Pos)))) |
type SourceName = FilePath Source #
This is a compatibility type synonym for megaparsec vs. parsec.
A Reusable SrcSpan Type ------------------------------------------
Instances
Eq SrcSpan Source # | |
Data SrcSpan Source # | |
Defined in Language.Fixpoint.Types.Spans gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SrcSpan -> c SrcSpan # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SrcSpan # toConstr :: SrcSpan -> Constr # dataTypeOf :: SrcSpan -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c SrcSpan) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SrcSpan) # gmapT :: (forall b. Data b => b -> b) -> SrcSpan -> SrcSpan # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SrcSpan -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SrcSpan -> r # gmapQ :: (forall d. Data d => d -> u) -> SrcSpan -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> SrcSpan -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> SrcSpan -> m SrcSpan # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SrcSpan -> m SrcSpan # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SrcSpan -> m SrcSpan # | |
Ord SrcSpan Source # | |
Defined in Language.Fixpoint.Types.Spans | |
Show SrcSpan Source # | |
Generic SrcSpan Source # | |
Hashable SrcSpan Source # | |
Defined in Language.Fixpoint.Types.Spans | |
Binary SrcSpan Source # | |
Serialize SrcSpan Source # | |
NFData SrcSpan Source # | |
Defined in Language.Fixpoint.Types.Refinements | |
Store SrcSpan Source # | |
PPrint SrcSpan Source # | |
Defined in Language.Fixpoint.Types.Spans | |
Loc SrcSpan Source # | |
type Rep SrcSpan Source # | |
Defined in Language.Fixpoint.Types.Spans type Rep SrcSpan = D1 ('MetaData "SrcSpan" "Language.Fixpoint.Types.Spans" "liquid-fixpoint-0.8.10.7-Dsb9ZI1V79FKe50LlwO7R" 'False) (C1 ('MetaCons "SS" 'PrefixI 'True) (S1 ('MetaSel ('Just "sp_start") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 SourcePos) :*: S1 ('MetaSel ('Just "sp_stop") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 SourcePos))) |
Pos
is the type for positive integers. This is used to represent line
number, column number, and similar things like indentation level.
Semigroup
instance can be used to safely and efficiently add Pos
es
together.
Since: megaparsec-5.0.0
Instances
Eq Pos | |
Data Pos | |
Defined in Text.Megaparsec.Pos gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Pos -> c Pos # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Pos # dataTypeOf :: Pos -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Pos) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Pos) # gmapT :: (forall b. Data b => b -> b) -> Pos -> Pos # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Pos -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Pos -> r # gmapQ :: (forall d. Data d => d -> u) -> Pos -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Pos -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Pos -> m Pos # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Pos -> m Pos # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Pos -> m Pos # | |
Ord Pos | |
Read Pos | |
Show Pos | |
Semigroup Pos | |
Hashable Pos Source # | |
Defined in Language.Fixpoint.Types.Spans | |
PrintfArg Pos Source # | |
Defined in Language.Fixpoint.Types.Spans formatArg :: Pos -> FieldFormatter # parseFormat :: Pos -> ModifierParser # | |
Binary Pos Source # | We need the Binary instances for LH's spec serialization |
Serialize Pos Source # | |
NFData Pos | |
Defined in Text.Megaparsec.Pos | |
Store Pos Source # | |
safePos :: Int -> Pos Source #
Create, safely, as position. If a non-positive number is given, we use 1.
safeSourcePos :: FilePath -> Int -> Int -> SourcePos Source #
Create a source position from integers, using 1 in case of non-positive numbers.
Construction of Pos
from Int
. The function throws
InvalidPosException
when given a non-positive argument.
Since: megaparsec-6.0.0
Located Values
Located Values ---------------------------------------------------
Instances
Functor Located Source # | |
Foldable Located Source # | |
Defined in Language.Fixpoint.Types.Spans fold :: Monoid m => Located m -> m # foldMap :: Monoid m => (a -> m) -> Located a -> m # foldMap' :: Monoid m => (a -> m) -> Located a -> m # foldr :: (a -> b -> b) -> b -> Located a -> b # foldr' :: (a -> b -> b) -> b -> Located a -> b # foldl :: (b -> a -> b) -> b -> Located a -> b # foldl' :: (b -> a -> b) -> b -> Located a -> b # foldr1 :: (a -> a -> a) -> Located a -> a # foldl1 :: (a -> a -> a) -> Located a -> a # elem :: Eq a => a -> Located a -> Bool # maximum :: Ord a => Located a -> a # minimum :: Ord a => Located a -> a # | |
Traversable Located Source # | |
SMTLIB2 LocSymbol Source # | |
Eq a => Eq (Located a) Source # | |
Data a => Data (Located a) Source # | |
Defined in Language.Fixpoint.Types.Spans gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Located a -> c (Located a) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Located a) # toConstr :: Located a -> Constr # dataTypeOf :: Located a -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Located a)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Located a)) # gmapT :: (forall b. Data b => b -> b) -> Located a -> Located a # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Located a -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Located a -> r # gmapQ :: (forall d. Data d => d -> u) -> Located a -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Located a -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Located a -> m (Located a) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Located a -> m (Located a) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Located a -> m (Located a) # | |
Ord a => Ord (Located a) Source # | |
Defined in Language.Fixpoint.Types.Spans | |
Show a => Show (Located a) Source # | |
IsString a => IsString (Located a) Source # | |
Defined in Language.Fixpoint.Types.Spans fromString :: String -> Located a # | |
Generic (Located a) Source # | |
Hashable a => Hashable (Located a) Source # | |
Defined in Language.Fixpoint.Types.Spans | |
Binary a => Binary (Located a) Source # | |
NFData a => NFData (Located a) Source # | |
Defined in Language.Fixpoint.Types.Spans | |
Store a => Store (Located a) Source # | |
PPrint a => PPrint (Located a) Source # | |
Defined in Language.Fixpoint.Types.Spans | |
Fixpoint a => Fixpoint (Located a) Source # | |
Loc (Located a) Source # | |
Symbolic a => Symbolic (Located a) Source # | |
Subable a => Subable (Located a) Source # | |
Defined in Language.Fixpoint.Types.Refinements | |
Expression a => Expression (Located a) Source # | |
type Rep (Located a) Source # | |
Defined in Language.Fixpoint.Types.Spans type Rep (Located a) = D1 ('MetaData "Located" "Language.Fixpoint.Types.Spans" "liquid-fixpoint-0.8.10.7-Dsb9ZI1V79FKe50LlwO7R" 'False) (C1 ('MetaCons "Loc" 'PrefixI 'True) (S1 ('MetaSel ('Just "loc") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 SourcePos) :*: (S1 ('MetaSel ('Just "locE") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 SourcePos) :*: S1 ('MetaSel ('Just "val") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 a)))) |
Constructing spans
toSourcePos :: (SourceName, Line, Column) -> SourcePos Source #
ofSourcePos :: SourcePos -> (SourceName, Line, Column) Source #
Destructing spans
sourcePosElts :: SourcePos -> (SourceName, Line, Column) Source #
Orphan instances
Hashable Pos Source # | |
Hashable SourcePos Source # | |
PrintfArg Pos Source # | |
formatArg :: Pos -> FieldFormatter # parseFormat :: Pos -> ModifierParser # | |
Binary Pos Source # | We need the Binary instances for LH's spec serialization |
Binary SourcePos Source # | |
Serialize Pos Source # | |
Serialize SourcePos Source # | |
Store Pos Source # | |
Store SourcePos Source # | Retrofitting instances to SourcePos ------------------------------ |
PPrint SourcePos Source # | |
Fixpoint SourcePos Source # | |