Language.Fixpoint.Types.Spans

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

Eq SourcePos

Defined in Text.Parsec.Pos

Methods

(==) :: SourcePos -> SourcePos -> Bool

(/=) :: SourcePos -> SourcePos -> Bool

Data SourcePos

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 :: (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.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

Defined in Text.Parsec.Pos

Methods

showsPrec :: Int -> SourcePos -> ShowS

show :: SourcePos -> String

showList :: [SourcePos] -> ShowS

Binary SourcePos

Defined in Language.Fixpoint.Types.Spans

Methods

put :: SourcePos -> Put

get :: Get SourcePos

putList :: [SourcePos] -> Put

Serialize SourcePos

Defined in Language.Fixpoint.Types.Spans

Methods

put :: Putter SourcePos

get :: Get SourcePos

NFData SourcePos

Retrofitting instances to SourcePos ------------------------------

Defined in Language.Fixpoint.Types.Spans

Methods

rnf :: SourcePos -> ()

Hashable SourcePos

Defined in Language.Fixpoint.Types.Spans

Methods

hashWithSalt :: Int -> SourcePos -> Int

hash :: SourcePos -> Int

PPrint SourcePos

Defined in Language.Fixpoint.Types.Spans

Methods

pprintTidy :: Tidy -> SourcePos -> Doc

pprintPrec :: Int -> Tidy -> SourcePos -> Doc

Fixpoint SourcePos

Defined in Language.Fixpoint.Types.Spans

Methods

toFix :: SourcePos -> Doc

simplify :: SourcePos -> SourcePos

Loc SourcePos

Defined in Language.Fixpoint.Types.Spans

Methods

srcSpan :: SourcePos -> SrcSpan

data SrcSpan

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

Constructors

SS

Fields

• sp_start :: !SourcePos
• sp_stop :: !SourcePos

Instances

Eq SrcSpan

Defined in Language.Fixpoint.Types.Spans

Methods

(==) :: SrcSpan -> SrcSpan -> Bool

(/=) :: SrcSpan -> SrcSpan -> Bool

Data SrcSpan

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 :: (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

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

Defined in Language.Fixpoint.Types.Spans

Methods

showsPrec :: Int -> SrcSpan -> ShowS

show :: SrcSpan -> String

showList :: [SrcSpan] -> ShowS

Generic SrcSpan

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

Defined in Language.Fixpoint.Types.Refinements

Methods

put :: SrcSpan -> Put

get :: Get SrcSpan

putList :: [SrcSpan] -> Put

Serialize SrcSpan

Defined in Language.Fixpoint.Types.Spans

Methods

put :: Putter SrcSpan

get :: Get SrcSpan

NFData SrcSpan

Defined in Language.Fixpoint.Types.Refinements

Methods

rnf :: SrcSpan -> ()

Hashable SrcSpan

Defined in Language.Fixpoint.Types.Spans

Methods

hashWithSalt :: Int -> SrcSpan -> Int

hash :: SrcSpan -> Int

PPrint SrcSpan

Defined in Language.Fixpoint.Types.Spans

Methods

pprintTidy :: Tidy -> SrcSpan -> Doc

pprintPrec :: Int -> Tidy -> SrcSpan -> Doc

Loc SrcSpan

Defined in Language.Fixpoint.Types.Spans

Methods

srcSpan :: SrcSpan -> SrcSpan

type Rep SrcSpan

Defined in Language.Fixpoint.Types.Spans

type Rep SrcSpan = D1 (MetaData "SrcSpan" "Language.Fixpoint.Types.Spans" "liquid-fixpoint-0.8.0.2-EGSzGwrlcJrCaUaEYLNzOY" 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

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

Methods

srcSpan :: a -> SrcSpan

Instances

Loc ()

Defined in Language.Fixpoint.Types.Spans

Methods

srcSpan :: () -> SrcSpan

Loc SourcePos

Defined in Language.Fixpoint.Types.Spans

Methods

srcSpan :: SourcePos -> SrcSpan

Loc SrcSpan

Defined in Language.Fixpoint.Types.Spans

Methods

srcSpan :: SrcSpan -> SrcSpan

Loc DataDecl

Defined in Language.Fixpoint.Types.Sorts

Methods

srcSpan :: DataDecl -> SrcSpan

Loc FTycon

Defined in Language.Fixpoint.Types.Sorts

Methods

srcSpan :: FTycon -> SrcSpan

Loc Qualifier

Defined in Language.Fixpoint.Types.Constraints

Methods

srcSpan :: Qualifier -> SrcSpan

Loc EQual

Defined in Language.Fixpoint.Types.Solutions

Methods

srcSpan :: EQual -> SrcSpan

Loc (Located a)

Defined in Language.Fixpoint.Types.Spans

Methods

srcSpan :: Located a -> SrcSpan

Loc a => Loc (SimpC a)

Defined in Language.Fixpoint.Types.Constraints

Methods

srcSpan :: SimpC a -> SrcSpan

data Located a

Constructors

Loc

Fields

• loc :: !SourcePos

  Start Position

• locE :: !SourcePos

  End Position

• val :: !a

Instances

Functor Located

Defined in Language.Fixpoint.Types.Spans

Methods

fmap :: (a -> b) -> Located a -> Located b

(<$) :: a -> Located b -> Located a

Foldable Located

Defined in Language.Fixpoint.Types.Spans

Methods

fold :: Monoid m => Located m -> 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

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

Defined in Language.Fixpoint.Smt.Serialize

Methods

smt2 :: SymEnv -> LocSymbol -> Builder

Eq a => Eq (Located a)

Defined in Language.Fixpoint.Types.Spans

Methods

(==) :: Located a -> Located a -> Bool

(/=) :: Located a -> Located a -> Bool

Data a => Data (Located a)

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 :: (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)

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)

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)

Defined in Language.Fixpoint.Types.Spans

Methods

fromString :: String -> Located a

Generic (Located a)

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)

Defined in Language.Fixpoint.Types.Spans

Methods

put :: Located a -> Put

get :: Get (Located a)

putList :: [Located a] -> Put

NFData a => NFData (Located a)

Defined in Language.Fixpoint.Types.Spans

Methods

rnf :: Located a -> ()

Hashable a => Hashable (Located a)

Defined in Language.Fixpoint.Types.Spans

Methods

hashWithSalt :: Int -> Located a -> Int

hash :: Located a -> Int

PPrint a => PPrint (Located a)

Defined in Language.Fixpoint.Types.Spans

Methods

pprintTidy :: Tidy -> Located a -> Doc

pprintPrec :: Int -> Tidy -> Located a -> Doc

Fixpoint a => Fixpoint (Located a)

Defined in Language.Fixpoint.Types.Spans

Methods

toFix :: Located a -> Doc

simplify :: Located a -> Located a

Loc (Located a)

Defined in Language.Fixpoint.Types.Spans

Methods

srcSpan :: Located a -> SrcSpan

Symbolic a => Symbolic (Located a)

Defined in Language.Fixpoint.Types.Names

Methods

symbol :: Located a -> Symbol

Subable a => Subable (Located a)

Defined in Language.Fixpoint.Types.Refinements

Methods

syms :: Located a -> [Symbol]

substa :: (Symbol -> Symbol) -> Located a -> Located a

substf :: (Symbol -> Expr) -> Located a -> Located a

subst :: Subst -> Located a -> Located a

subst1 :: Located a -> (Symbol, Expr) -> Located a

Expression a => Expression (Located a)

Defined in Language.Fixpoint.Types.Refinements

Methods

expr :: Located a -> Expr

type Rep (Located a)

Defined in Language.Fixpoint.Types.Spans

type Rep (Located a) = D1 (MetaData "Located" "Language.Fixpoint.Types.Spans" "liquid-fixpoint-0.8.0.2-EGSzGwrlcJrCaUaEYLNzOY" 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

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

Destructing spans

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

srcLine :: Loc a => a -> Int

Orphan instances

Binary SourcePos

Methods

put :: SourcePos -> Put

get :: Get SourcePos

putList :: [SourcePos] -> Put

Serialize SourcePos

Methods

put :: Putter SourcePos

get :: Get SourcePos

NFData SourcePos

Retrofitting instances to SourcePos ------------------------------

Methods

rnf :: SourcePos -> ()

Hashable SourcePos

Methods

hashWithSalt :: Int -> SourcePos -> Int

hash :: SourcePos -> Int

PPrint SourcePos

Methods

pprintTidy :: Tidy -> SourcePos -> Doc

pprintPrec :: Int -> Tidy -> SourcePos -> Doc

Fixpoint SourcePos

Methods

toFix :: SourcePos -> Doc

simplify :: SourcePos -> SourcePos