Safe Haskell	None
Language	Haskell98

Language.Fixpoint.Types.Spans

Contents

Concrete Location Type
Located Values
Constructing spans
Destructing spans
Orphan instances

Synopsis

data SourcePos
data SrcSpan = SS {
- sp_start :: !SourcePos
- sp_stop :: !SourcePos
}
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 :: String -> SourcePos
atLoc :: Loc l => l -> b -> Located b
toSourcePos :: (SourceName, Line, Column) -> SourcePos
sourcePosElts :: SourcePos -> (SourceName, Line, Column)
srcLine :: Loc a => a -> Int

Concrete Location Type

data SourcePos #

The abstract data type SourcePos represents source positions. It contains the name of the source (i.e. file name), a line number and a column number. SourcePos is an instance of the Show, Eq and Ord class.

Instances

Instances details

Eq SourcePos
Instance details Defined in Text.Parsec.Pos Methods (==) :: SourcePos -> SourcePos -> Bool # (/=) :: SourcePos -> SourcePos -> Bool #
Data SourcePos
Instance details Defined in Text.Parsec.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 #
Ord SourcePos
Instance details Defined in Text.Parsec.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 #
Show SourcePos
Instance details Defined in Text.Parsec.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 #
NFData SourcePos Source #	Retrofitting instances to SourcePos ------------------------------
Instance details Defined in Language.Fixpoint.Types.Spans Methods rnf :: SourcePos -> () #
Hashable SourcePos
Instance details Defined in Language.Fixpoint.Types.Spans Methods hashWithSalt :: Int -> SourcePos -> Int hash :: SourcePos -> Int
Serialize SourcePos
Instance details Defined in Language.Fixpoint.Types.Spans Methods put :: Putter SourcePos get :: Get SourcePos
PPrint SourcePos Source #
Instance details Defined in Language.Fixpoint.Types.Spans Methods pprintTidy :: Tidy -> SourcePos -> Doc Source # pprintPrec :: Int -> Tidy -> SourcePos -> Doc Source #
Fixpoint SourcePos Source #
Instance details Defined in Language.Fixpoint.Types.Spans Methods toFix :: SourcePos -> Doc Source # simplify :: SourcePos -> SourcePos Source #
Loc SourcePos Source #
Instance details Defined in Language.Fixpoint.Types.Spans Methods srcSpan :: SourcePos -> SrcSpan Source #

data SrcSpan Source #

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

Constructors

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

Instances

Instances details

Eq SrcSpan Source #
Instance details Defined in Language.Fixpoint.Types.Spans Methods (==) :: SrcSpan -> SrcSpan -> Bool # (/=) :: SrcSpan -> SrcSpan -> Bool #
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 #
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 #
Show SrcSpan Source #
Instance details Defined in Language.Fixpoint.Types.Spans Methods showsPrec :: Int -> SrcSpan -> ShowS # show :: SrcSpan -> String # showList :: [SrcSpan] -> ShowS #
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 #
Binary SrcSpan Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods put :: SrcSpan -> Put # get :: Get SrcSpan # putList :: [SrcSpan] -> Put #
NFData SrcSpan Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods rnf :: SrcSpan -> () #
Hashable SrcSpan Source #
Instance details Defined in Language.Fixpoint.Types.Spans Methods hashWithSalt :: Int -> SrcSpan -> Int hash :: SrcSpan -> Int
Serialize SrcSpan Source #
Instance details Defined in Language.Fixpoint.Types.Spans Methods put :: Putter SrcSpan get :: Get SrcSpan
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 #
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.8.10.2-inplace" '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)))

Located Values

class Loc a where Source #

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

Methods

srcSpan :: a -> SrcSpan Source #

Instances

Instances details

Loc () Source #
Instance details Defined in Language.Fixpoint.Types.Spans Methods srcSpan :: () -> SrcSpan Source #
Loc SourcePos Source #
Instance details Defined in Language.Fixpoint.Types.Spans Methods srcSpan :: SourcePos -> SrcSpan Source #
Loc SrcSpan Source #
Instance details Defined in Language.Fixpoint.Types.Spans Methods srcSpan :: SrcSpan -> 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 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 (Located a) Source #
Instance details Defined in Language.Fixpoint.Types.Spans Methods srcSpan :: Located a -> SrcSpan Source #
Loc a => Loc (SimpC a) Source #
Instance details Defined in Language.Fixpoint.Types.Constraints Methods srcSpan :: SimpC a -> SrcSpan Source #

data Located a Source #

Constructors

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

Instances

Instances details

Functor Located Source #
Instance details Defined in Language.Fixpoint.Types.Spans Methods fmap :: (a -> b) -> Located a -> Located b # (<$) :: a -> Located b -> Located a #
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) #
SMTLIB2 LocSymbol Source #
Instance details Defined in Language.Fixpoint.Smt.Serialize Methods smt2 :: SymEnv -> LocSymbol -> Builder Source #
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 #
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) #
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 #
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 #
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 #
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 -> () #
Hashable a => Hashable (Located a) Source #
Instance details Defined in Language.Fixpoint.Types.Spans Methods hashWithSalt :: Int -> Located a -> Int hash :: Located a -> Int
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 #
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 #
Loc (Located a) Source #
Instance details Defined in Language.Fixpoint.Types.Spans Methods srcSpan :: Located a -> SrcSpan Source #
Symbolic a => Symbolic (Located a) Source #
Instance details Defined in Language.Fixpoint.Types.Names Methods symbol :: Located a -> Symbol 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 #
Expression a => Expression (Located a) Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods expr :: Located a -> Expr Source #
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.8.10.2-inplace" '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 :: String -> SourcePos Source #

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

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

Destructing spans

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

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

Orphan instances

Binary SourcePos Source #
Instance details Methods put :: SourcePos -> Put # get :: Get SourcePos # putList :: [SourcePos] -> Put #
NFData SourcePos Source #	Retrofitting instances to SourcePos ------------------------------
Instance details Methods rnf :: SourcePos -> () #
Hashable SourcePos Source #
Instance details Methods hashWithSalt :: Int -> SourcePos -> Int hash :: SourcePos -> Int
Serialize SourcePos Source #
Instance details Methods put :: Putter SourcePos get :: Get SourcePos
PPrint SourcePos Source #
Instance details Methods pprintTidy :: Tidy -> SourcePos -> Doc Source # pprintPrec :: Int -> Tidy -> SourcePos -> Doc Source #
Fixpoint SourcePos Source #
Instance details Methods toFix :: SourcePos -> Doc Source # simplify :: SourcePos -> SourcePos Source #