Safe Haskell  SafeInferred 

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
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 #  
Generic SourcePos  
Read SourcePos  
Show SourcePos  
Binary SourcePos Source #  
Serialize SourcePos Source #  
NFData SourcePos  
Defined in Text.Megaparsec.Pos  
Eq SourcePos  
Ord SourcePos  
Defined in Text.Megaparsec.Pos  
Hashable SourcePos Source #  
Defined in Language.Fixpoint.Types.Spans  
Fixpoint SourcePos Source #  
PPrint SourcePos Source #  
Defined in Language.Fixpoint.Types.Spans  
Loc SourcePos Source #  
Store SourcePos Source #  Retrofitting instances to SourcePos  
type Rep SourcePos  
Defined in Text.Megaparsec.Pos type Rep SourcePos = D1 ('MetaData "SourcePos" "Text.Megaparsec.Pos" "megaparsec9.5.0nV6NFlDOdsDHucVPlnquI" '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
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 #  
Generic SrcSpan Source #  
Show SrcSpan Source #  
Binary SrcSpan Source #  
Serialize SrcSpan Source #  
NFData SrcSpan Source #  
Defined in Language.Fixpoint.Types.Spans  
Eq SrcSpan Source #  
Ord SrcSpan Source #  
Defined in Language.Fixpoint.Types.Spans  
Hashable SrcSpan Source #  
Defined in Language.Fixpoint.Types.Spans  
PPrint SrcSpan Source #  
Defined in Language.Fixpoint.Types.Spans  
Loc SrcSpan Source #  
Store SrcSpan Source #  
type Rep SrcSpan Source #  
Defined in Language.Fixpoint.Types.Spans type Rep SrcSpan = D1 ('MetaData "SrcSpan" "Language.Fixpoint.Types.Spans" "liquidfixpoint0.9.2.58VOJ4a5jXPy7nyhLFTxkOW" '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: megaparsec5.0.0
Instances
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 #  
Semigroup Pos  
Generic Pos  
Read Pos  
Show Pos  
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  
Eq Pos  
Ord Pos  
Hashable Pos Source #  
Defined in Language.Fixpoint.Types.Spans  
Store Pos Source #  
type Rep Pos  
Defined in Text.Megaparsec.Pos 
safePos :: Int > Pos Source #
Create, safely, as position. If a nonpositive number is given, we use 1.
safeSourcePos :: FilePath > Int > Int > SourcePos Source #
Create a source position from integers, using 1 in case of nonpositive numbers.
Construction of Pos
from Int
. The function throws
InvalidPosException
when given a nonpositive argument.
Since: megaparsec6.0.0
Located Values
Located Values 
Instances
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 #  
Functor Located Source #  
SMTLIB2 LocSymbol 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) #  
IsString a => IsString (Located a) Source #  
Defined in Language.Fixpoint.Types.Spans fromString :: String > Located a #  
Generic (Located a) Source #  
Show a => Show (Located a) Source #  
Binary a => Binary (Located a) Source #  
NFData a => NFData (Located a) Source #  
Defined in Language.Fixpoint.Types.Spans  
Eq a => Eq (Located a) Source #  
Ord a => Ord (Located a) Source #  
Defined in Language.Fixpoint.Types.Spans  
Hashable a => Hashable (Located a) Source #  
Defined in Language.Fixpoint.Types.Spans  
Symbolic a => Symbolic (Located a) Source #  
Fixpoint a => Fixpoint (Located a) Source #  
PPrint a => PPrint (Located a) Source #  
Defined in Language.Fixpoint.Types.Spans  
Expression a => Expression (Located a) Source #  
Subable a => Subable (Located a) Source #  
Defined in Language.Fixpoint.Types.Refinements  
Loc (Located a) Source #  
Store a => Store (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" "liquidfixpoint0.9.2.58VOJ4a5jXPy7nyhLFTxkOW" '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
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 #  
Hashable Pos Source #  
Hashable SourcePos Source #  
Fixpoint SourcePos Source #  
PPrint SourcePos Source #  
Store Pos Source #  
Store SourcePos Source #  Retrofitting instances to SourcePos  