liquid-fixpoint-0.9.6.3.4: Predicate Abstraction-based Horn-Clause/Implication Constraint Solver
Safe HaskellNone
LanguageHaskell98

Language.Fixpoint.Types.Spans

Synopsis

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

Instances

Instances details
FromJSON SourcePos Source # 
Instance details

Defined in Language.Fixpoint.Types.Spans

Methods

parseJSON :: Value -> Parser SourcePos #

parseJSONList :: Value -> Parser [SourcePos] #

omittedField :: Maybe SourcePos #

ToJSON SourcePos Source # 
Instance details

Defined in Language.Fixpoint.Types.Spans

Methods

toJSON :: SourcePos -> Value #

toEncoding :: SourcePos -> Encoding #

toJSONList :: [SourcePos] -> Value #

toEncodingList :: [SourcePos] -> Encoding #

omitField :: SourcePos -> Bool #

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 
Instance details

Defined in Text.Megaparsec.Pos

type Rep SourcePos = D1 ('MetaData "SourcePos" "Text.Megaparsec.Pos" "megaparsec-9.7.0-5TYMwA2DC6yGQlbpnP5uYQ" '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))))

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.7.0-5TYMwA2DC6yGQlbpnP5uYQ" '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

Instances

Instances details
FromJSON SrcSpan Source # 
Instance details

Defined in Language.Fixpoint.Types.Spans

Methods

parseJSON :: Value -> Parser SrcSpan #

parseJSONList :: Value -> Parser [SrcSpan] #

omittedField :: Maybe SrcSpan #

ToJSON SrcSpan Source # 
Instance details

Defined in Language.Fixpoint.Types.Spans

Methods

toJSON :: SrcSpan -> Value #

toEncoding :: SrcSpan -> Encoding #

toJSONList :: [SrcSpan] -> Value #

toEncodingList :: [SrcSpan] -> Encoding #

omitField :: 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 #

Generic SrcSpan Source # 
Instance details

Defined in Language.Fixpoint.Types.Spans

Associated Types

type Rep SrcSpan 
Instance details

Defined in Language.Fixpoint.Types.Spans

type Rep SrcSpan = D1 ('MetaData "SrcSpan" "Language.Fixpoint.Types.Spans" "liquid-fixpoint-0.9.6.3.4-CmH5CYTDh7gFBJNG3w2uNw" '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)))

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.6.3.4-CmH5CYTDh7gFBJNG3w2uNw" '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
FromJSON Pos Source # 
Instance details

Defined in Language.Fixpoint.Types.Spans

Methods

parseJSON :: Value -> Parser Pos #

parseJSONList :: Value -> Parser [Pos] #

omittedField :: Maybe Pos #

ToJSON Pos Source # 
Instance details

Defined in Language.Fixpoint.Types.Spans

Methods

toJSON :: Pos -> Value #

toEncoding :: Pos -> Encoding #

toJSONList :: [Pos] -> Value #

toEncodingList :: [Pos] -> Encoding #

omitField :: Pos -> Bool #

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 
Instance details

Defined in Text.Megaparsec.Pos

type Rep Pos = D1 ('MetaData "Pos" "Text.Megaparsec.Pos" "megaparsec-9.7.0-5TYMwA2DC6yGQlbpnP5uYQ" 'True) (C1 ('MetaCons "Pos" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int)))

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.7.0-5TYMwA2DC6yGQlbpnP5uYQ" '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

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 :: LocSymbol -> SymM Builder Source #

FromJSON a => FromJSON (Located a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Spans

Methods

parseJSON :: Value -> Parser (Located a) #

parseJSONList :: Value -> Parser [Located a] #

omittedField :: Maybe (Located a) #

ToJSON a => ToJSON (Located a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Spans

Methods

toJSON :: Located a -> Value #

toEncoding :: Located a -> Encoding #

toJSONList :: [Located a] -> Value #

toEncodingList :: [Located a] -> Encoding #

omitField :: 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) #

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) 
Instance details

Defined in Language.Fixpoint.Types.Spans

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

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 #

ToHornSMT a => ToHornSMT (Located a) Source # 
Instance details

Defined in Language.Fixpoint.Types.SMTPrint

Methods

toHornSMT :: Located a -> Doc 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.6.3.4-CmH5CYTDh7gFBJNG3w2uNw" '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

FromJSON Pos Source # 
Instance details

Methods

parseJSON :: Value -> Parser Pos #

parseJSONList :: Value -> Parser [Pos] #

omittedField :: Maybe Pos #

FromJSON SourcePos Source # 
Instance details

Methods

parseJSON :: Value -> Parser SourcePos #

parseJSONList :: Value -> Parser [SourcePos] #

omittedField :: Maybe SourcePos #

ToJSON Pos Source # 
Instance details

Methods

toJSON :: Pos -> Value #

toEncoding :: Pos -> Encoding #

toJSONList :: [Pos] -> Value #

toEncodingList :: [Pos] -> Encoding #

omitField :: Pos -> Bool #

ToJSON SourcePos Source # 
Instance details

Methods

toJSON :: SourcePos -> Value #

toEncoding :: SourcePos -> Encoding #

toJSONList :: [SourcePos] -> Value #

toEncodingList :: [SourcePos] -> Encoding #

omitField :: SourcePos -> Bool #

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 #