Safe Haskell	Safe-Inferred
Language	Haskell98

Language.Fixpoint.Types.Spans

Contents

Concrete Location Type
Located Values
Constructing spans
Destructing spans
Orphan instances

Synopsis

data SourcePos = SourcePos {
- sourceName :: FilePath
- sourceLine :: !Pos
- sourceColumn :: !Pos
}
type SourceName = FilePath
data SrcSpan = SS {
- sp_start :: !SourcePos
- sp_stop :: !SourcePos
}
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
- srcSpan :: a -> SrcSpan
data Located a = Loc {
- loc :: !SourcePos
- locE :: !SourcePos
- val :: !a
}
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

data SourcePos #

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.

Constructors

SourcePos
Fields sourceName :: FilePath Name of source file sourceLine :: !Pos Line number sourceColumn :: !Pos Column number

Instances

Instances details

Data SourcePos
Instance details Defined in Text.Megaparsec.Pos Methods 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
Instance details Defined in Text.Megaparsec.Pos Associated Types type Rep SourcePos :: Type -> Type # Methods from :: SourcePos -> Rep SourcePos x # to :: Rep SourcePos x -> SourcePos #
Read SourcePos
Instance details Defined in Text.Megaparsec.Pos Methods readsPrec :: Int -> ReadS SourcePos # readList :: ReadS [SourcePos] # readPrec :: ReadPrec SourcePos # readListPrec :: ReadPrec [SourcePos] #
Show SourcePos
Instance details Defined in Text.Megaparsec.Pos Methods showsPrec :: Int -> SourcePos -> ShowS # show :: SourcePos -> String # showList :: [SourcePos] -> ShowS #
Binary SourcePos Source #
Instance details Defined in Language.Fixpoint.Types.Spans Methods put :: SourcePos -> Put # get :: Get SourcePos # putList :: [SourcePos] -> Put #
Serialize SourcePos Source #
Instance details Defined in Language.Fixpoint.Types.Spans Methods put :: Putter SourcePos # get :: Get SourcePos #
NFData SourcePos
Instance details Defined in Text.Megaparsec.Pos Methods rnf :: SourcePos -> () #
Eq SourcePos
Instance details Defined in Text.Megaparsec.Pos Methods (==) :: SourcePos -> SourcePos -> Bool # (/=) :: SourcePos -> SourcePos -> Bool #
Ord SourcePos
Instance details Defined in Text.Megaparsec.Pos Methods compare :: SourcePos -> SourcePos -> Ordering # (<) :: SourcePos -> SourcePos -> Bool # (<=) :: SourcePos -> SourcePos -> Bool # (>) :: SourcePos -> SourcePos -> Bool # (>=) :: SourcePos -> SourcePos -> Bool # max :: SourcePos -> SourcePos -> SourcePos # min :: SourcePos -> SourcePos -> SourcePos #
Hashable SourcePos Source #
Instance details Defined in Language.Fixpoint.Types.Spans Methods hashWithSalt :: Int -> SourcePos -> Int # hash :: SourcePos -> Int #
Fixpoint SourcePos Source #
Instance details Defined in Language.Fixpoint.Types.Spans Methods toFix :: SourcePos -> Doc Source # simplify :: SourcePos -> SourcePos Source #
PPrint SourcePos Source #
Instance details Defined in Language.Fixpoint.Types.Spans Methods pprintTidy :: Tidy -> SourcePos -> Doc Source # pprintPrec :: Int -> Tidy -> SourcePos -> Doc Source #
Loc SourcePos Source #
Instance details Defined in Language.Fixpoint.Types.Spans Methods srcSpan :: SourcePos -> SrcSpan Source #
Store SourcePos Source #	Retrofitting instances to SourcePos ------------------------------
Instance details Defined in Language.Fixpoint.Types.Spans Methods size :: Size SourcePos # poke :: SourcePos -> Poke () # peek :: Peek SourcePos #
type Rep SourcePos
Instance details Defined in Text.Megaparsec.Pos type Rep SourcePos = D1 ('MetaData "SourcePos" "Text.Megaparsec.Pos" "megaparsec-9.5.0-nV6NFlDOdsDHucVPlnquI" '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.

data SrcSpan Source #

A Reusable SrcSpan Type ------------------------------------------

Constructors

SS
Fields sp_start :: !SourcePos sp_stop :: !SourcePos

Instances

Instances details

Data SrcSpan Source #
Instance details Defined in Language.Fixpoint.Types.Spans Methods 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 #
Instance details Defined in Language.Fixpoint.Types.Spans Associated Types type Rep SrcSpan :: Type -> Type # Methods from :: SrcSpan -> Rep SrcSpan x # to :: Rep SrcSpan x -> SrcSpan #
Show SrcSpan Source #
Instance details Defined in Language.Fixpoint.Types.Spans Methods showsPrec :: Int -> SrcSpan -> ShowS # show :: SrcSpan -> String # showList :: [SrcSpan] -> ShowS #
Binary SrcSpan Source #
Instance details Defined in Language.Fixpoint.Types.Spans Methods put :: SrcSpan -> Put # get :: Get SrcSpan # putList :: [SrcSpan] -> Put #
Serialize SrcSpan Source #
Instance details Defined in Language.Fixpoint.Types.Spans Methods put :: Putter SrcSpan # get :: Get SrcSpan #
NFData SrcSpan Source #
Instance details Defined in Language.Fixpoint.Types.Spans Methods rnf :: SrcSpan -> () #
Eq SrcSpan Source #
Instance details Defined in Language.Fixpoint.Types.Spans Methods (==) :: SrcSpan -> SrcSpan -> Bool # (/=) :: SrcSpan -> SrcSpan -> Bool #
Ord SrcSpan Source #
Instance details Defined in Language.Fixpoint.Types.Spans Methods compare :: SrcSpan -> SrcSpan -> Ordering # (<) :: SrcSpan -> SrcSpan -> Bool # (<=) :: SrcSpan -> SrcSpan -> Bool # (>) :: SrcSpan -> SrcSpan -> Bool # (>=) :: SrcSpan -> SrcSpan -> Bool # max :: SrcSpan -> SrcSpan -> SrcSpan # min :: SrcSpan -> SrcSpan -> SrcSpan #
Hashable SrcSpan Source #
Instance details Defined in Language.Fixpoint.Types.Spans Methods hashWithSalt :: Int -> SrcSpan -> Int # hash :: SrcSpan -> Int #
PPrint SrcSpan Source #
Instance details Defined in Language.Fixpoint.Types.Spans Methods pprintTidy :: Tidy -> SrcSpan -> Doc Source # pprintPrec :: Int -> Tidy -> SrcSpan -> Doc Source #
Loc SrcSpan Source #
Instance details Defined in Language.Fixpoint.Types.Spans Methods srcSpan :: SrcSpan -> SrcSpan Source #
Store SrcSpan Source #
Instance details Defined in Language.Fixpoint.Types.Spans Methods size :: Size SrcSpan # poke :: SrcSpan -> Poke () # peek :: Peek SrcSpan #
type Rep SrcSpan Source #
Instance details Defined in Language.Fixpoint.Types.Spans type Rep SrcSpan = D1 ('MetaData "SrcSpan" "Language.Fixpoint.Types.Spans" "liquid-fixpoint-0.9.2.5-8VOJ4a5jXPy7nyhLFTxkOW" '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)))

data Pos #

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 Poses together.

Since: megaparsec-5.0.0

Instances

Instances details

Data Pos
Instance details Defined in Text.Megaparsec.Pos Methods 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 # toConstr :: Pos -> Constr # 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
Instance details Defined in Text.Megaparsec.Pos Methods (<>) :: Pos -> Pos -> Pos # sconcat :: NonEmpty Pos -> Pos # stimes :: Integral b => b -> Pos -> Pos #
Generic Pos
Instance details Defined in Text.Megaparsec.Pos Associated Types type Rep Pos :: Type -> Type # Methods from :: Pos -> Rep Pos x # to :: Rep Pos x -> Pos #
Read Pos
Instance details Defined in Text.Megaparsec.Pos Methods readsPrec :: Int -> ReadS Pos # readList :: ReadS [Pos] # readPrec :: ReadPrec Pos # readListPrec :: ReadPrec [Pos] #
Show Pos
Instance details Defined in Text.Megaparsec.Pos Methods showsPrec :: Int -> Pos -> ShowS # show :: Pos -> String # showList :: [Pos] -> ShowS #
PrintfArg Pos Source #
Instance details Defined in Language.Fixpoint.Types.Spans Methods formatArg :: Pos -> FieldFormatter # parseFormat :: Pos -> ModifierParser #
Binary Pos Source #	We need the Binary instances for LH's spec serialization
Instance details Defined in Language.Fixpoint.Types.Spans Methods put :: Pos -> Put # get :: Get Pos # putList :: [Pos] -> Put #
Serialize Pos Source #
Instance details Defined in Language.Fixpoint.Types.Spans Methods put :: Putter Pos # get :: Get Pos #
NFData Pos
Instance details Defined in Text.Megaparsec.Pos Methods rnf :: Pos -> () #
Eq Pos
Instance details Defined in Text.Megaparsec.Pos Methods (==) :: Pos -> Pos -> Bool # (/=) :: Pos -> Pos -> Bool #
Ord Pos
Instance details Defined in Text.Megaparsec.Pos Methods compare :: Pos -> Pos -> Ordering # (<) :: Pos -> Pos -> Bool # (<=) :: Pos -> Pos -> Bool # (>) :: Pos -> Pos -> Bool # (>=) :: Pos -> Pos -> Bool # max :: Pos -> Pos -> Pos # min :: Pos -> Pos -> Pos #
Hashable Pos Source #
Instance details Defined in Language.Fixpoint.Types.Spans Methods hashWithSalt :: Int -> Pos -> Int # hash :: Pos -> Int #
Store Pos Source #
Instance details Defined in Language.Fixpoint.Types.Spans Methods size :: Size Pos # poke :: Pos -> Poke () # peek :: Peek Pos #
type Rep Pos
Instance details Defined in Text.Megaparsec.Pos type Rep Pos = D1 ('MetaData "Pos" "Text.Megaparsec.Pos" "megaparsec-9.5.0-nV6NFlDOdsDHucVPlnquI" 'True) (C1 ('MetaCons "Pos" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int)))

predPos :: Pos -> Pos Source #

Computes, safely, the predecessor of a Pos value, stopping at 1.

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.

succPos :: Pos -> Pos Source #

Computes the successor of a Pos value.

unPos :: Pos -> Int #

Extract Int from Pos.

Since: megaparsec-6.0.0

mkPos :: Int -> Pos #

Construction of Pos from Int. The function throws InvalidPosException when given a non-positive argument.

Since: megaparsec-6.0.0

Located Values

class Loc a where Source #

Located Values ---------------------------------------------------

Methods

srcSpan :: a -> SrcSpan Source #

Instances

Instances details

Loc Tag Source #
Instance details Defined in Language.Fixpoint.Horn.Types Methods srcSpan :: Tag -> SrcSpan Source #
Loc Qualifier Source #
Instance details Defined in Language.Fixpoint.Types.Constraints Methods srcSpan :: Qualifier -> SrcSpan Source #
Loc EQual Source #
Instance details Defined in Language.Fixpoint.Types.Solutions Methods srcSpan :: EQual -> SrcSpan Source #
Loc DataDecl Source #
Instance details Defined in Language.Fixpoint.Types.Sorts Methods srcSpan :: DataDecl -> SrcSpan Source #
Loc FTycon Source #
Instance details Defined in Language.Fixpoint.Types.Sorts Methods srcSpan :: FTycon -> SrcSpan Source #
Loc SrcSpan Source #
Instance details Defined in Language.Fixpoint.Types.Spans Methods srcSpan :: SrcSpan -> SrcSpan Source #
Loc SourcePos Source #
Instance details Defined in Language.Fixpoint.Types.Spans Methods srcSpan :: SourcePos -> SrcSpan Source #
Loc () Source #
Instance details Defined in Language.Fixpoint.Types.Spans Methods srcSpan :: () -> SrcSpan Source #
Loc a => Loc (SimpC a) Source #
Instance details Defined in Language.Fixpoint.Types.Constraints Methods srcSpan :: SimpC a -> SrcSpan Source #
Loc (Located a) Source #
Instance details Defined in Language.Fixpoint.Types.Spans Methods srcSpan :: Located a -> SrcSpan Source #

data Located a Source #

Constructors

Loc
Fields loc :: !SourcePos Start Position locE :: !SourcePos End Position val :: !a

Instances

Instances details

Foldable Located Source #
Instance details Defined in Language.Fixpoint.Types.Spans Methods 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 # toList :: Located a -> [a] # null :: Located a -> Bool # length :: Located a -> Int # elem :: Eq a => a -> Located a -> Bool # maximum :: Ord a => Located a -> a # minimum :: Ord a => Located a -> a # sum :: Num a => Located a -> a # product :: Num a => Located a -> a #
Traversable Located Source #
Instance details Defined in Language.Fixpoint.Types.Spans Methods traverse :: Applicative f => (a -> f b) -> Located a -> f (Located b) # sequenceA :: Applicative f => Located (f a) -> f (Located a) # mapM :: Monad m => (a -> m b) -> Located a -> m (Located b) # sequence :: Monad m => Located (m a) -> m (Located a) #
Functor Located Source #
Instance details Defined in Language.Fixpoint.Types.Spans Methods fmap :: (a -> b) -> Located a -> Located b # (<$) :: a -> Located b -> Located a #
SMTLIB2 LocSymbol Source #
Instance details Defined in Language.Fixpoint.Smt.Serialize Methods smt2 :: SymEnv -> LocSymbol -> Builder Source #
Data a => Data (Located a) Source #
Instance details Defined in Language.Fixpoint.Types.Spans Methods 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 #
Instance details Defined in Language.Fixpoint.Types.Spans Methods fromString :: String -> Located a #
Generic (Located a) Source #
Instance details Defined in Language.Fixpoint.Types.Spans Associated Types type Rep (Located a) :: Type -> Type # Methods from :: Located a -> Rep (Located a) x # to :: Rep (Located a) x -> Located a #
Show a => Show (Located a) Source #
Instance details Defined in Language.Fixpoint.Types.Spans Methods showsPrec :: Int -> Located a -> ShowS # show :: Located a -> String # showList :: [Located a] -> ShowS #
Binary a => Binary (Located a) Source #
Instance details Defined in Language.Fixpoint.Types.Spans Methods put :: Located a -> Put # get :: Get (Located a) # putList :: [Located a] -> Put #
NFData a => NFData (Located a) Source #
Instance details Defined in Language.Fixpoint.Types.Spans Methods rnf :: Located a -> () #
Eq a => Eq (Located a) Source #
Instance details Defined in Language.Fixpoint.Types.Spans Methods (==) :: Located a -> Located a -> Bool # (/=) :: Located a -> Located a -> Bool #
Ord a => Ord (Located a) Source #
Instance details Defined in Language.Fixpoint.Types.Spans Methods compare :: Located a -> Located a -> Ordering # (<) :: Located a -> Located a -> Bool # (<=) :: Located a -> Located a -> Bool # (>) :: Located a -> Located a -> Bool # (>=) :: Located a -> Located a -> Bool # max :: Located a -> Located a -> Located a # min :: Located a -> Located a -> Located a #
Hashable a => Hashable (Located a) Source #
Instance details Defined in Language.Fixpoint.Types.Spans Methods hashWithSalt :: Int -> Located a -> Int # hash :: Located a -> Int #
Symbolic a => Symbolic (Located a) Source #
Instance details Defined in Language.Fixpoint.Types.Names Methods symbol :: Located a -> Symbol Source #
Fixpoint a => Fixpoint (Located a) Source #
Instance details Defined in Language.Fixpoint.Types.Spans Methods toFix :: Located a -> Doc Source # simplify :: Located a -> Located a Source #
PPrint a => PPrint (Located a) Source #
Instance details Defined in Language.Fixpoint.Types.Spans Methods pprintTidy :: Tidy -> Located a -> Doc Source # pprintPrec :: Int -> Tidy -> Located a -> Doc Source #
Expression a => Expression (Located a) Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods expr :: Located a -> Expr Source #
Subable a => Subable (Located a) Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods syms :: Located a -> [Symbol] Source # substa :: (Symbol -> Symbol) -> Located a -> Located a Source # substf :: (Symbol -> Expr) -> Located a -> Located a Source # subst :: Subst -> Located a -> Located a Source # subst1 :: Located a -> (Symbol, Expr) -> Located a Source #
Loc (Located a) Source #
Instance details Defined in Language.Fixpoint.Types.Spans Methods srcSpan :: Located a -> SrcSpan Source #
Store a => Store (Located a) Source #
Instance details Defined in Language.Fixpoint.Types.Spans Methods size :: Size (Located a) # poke :: Located a -> Poke () # peek :: Peek (Located a) #
type Rep (Located a) Source #
Instance details Defined in Language.Fixpoint.Types.Spans type Rep (Located a) = D1 ('MetaData "Located" "Language.Fixpoint.Types.Spans" "liquid-fixpoint-0.9.2.5-8VOJ4a5jXPy7nyhLFTxkOW" '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

dummySpan :: SrcSpan Source #

panicSpan :: String -> SrcSpan Source #

locAt :: String -> a -> Located a Source #

dummyLoc :: a -> Located a Source #

dummyPos :: FilePath -> SourcePos Source #

atLoc :: Loc l => l -> b -> Located b Source #

toSourcePos :: (SourceName, Line, Column) -> SourcePos Source #

ofSourcePos :: SourcePos -> (SourceName, Line, Column) Source #

Destructing spans

sourcePosElts :: SourcePos -> (SourceName, Line, Column) Source #

srcLine :: Loc a => a -> Pos Source #

Orphan instances

PrintfArg Pos Source #
Instance details Methods formatArg :: Pos -> FieldFormatter # parseFormat :: Pos -> ModifierParser #
Binary Pos Source #	We need the Binary instances for LH's spec serialization
Instance details Methods put :: Pos -> Put # get :: Get Pos # putList :: [Pos] -> Put #
Binary SourcePos Source #
Instance details Methods put :: SourcePos -> Put # get :: Get SourcePos # putList :: [SourcePos] -> Put #
Serialize Pos Source #
Instance details Methods put :: Putter Pos # get :: Get Pos #
Serialize SourcePos Source #
Instance details Methods put :: Putter SourcePos # get :: Get SourcePos #
Hashable Pos Source #
Instance details Methods hashWithSalt :: Int -> Pos -> Int # hash :: Pos -> Int #
Hashable SourcePos Source #
Instance details Methods hashWithSalt :: Int -> SourcePos -> Int # hash :: SourcePos -> Int #
Fixpoint SourcePos Source #
Instance details Methods toFix :: SourcePos -> Doc Source # simplify :: SourcePos -> SourcePos Source #
PPrint SourcePos Source #
Instance details Methods pprintTidy :: Tidy -> SourcePos -> Doc Source # pprintPrec :: Int -> Tidy -> SourcePos -> Doc Source #
Store Pos Source #
Instance details Methods size :: Size Pos # poke :: Pos -> Poke () # peek :: Peek Pos #
Store SourcePos Source #	Retrofitting instances to SourcePos ------------------------------
Instance details Methods size :: Size SourcePos # poke :: SourcePos -> Poke () # peek :: Peek SourcePos #