liquid-fixpoint-0.8.10.1: Predicate Abstraction-based Horn-Clause/Implication Constraint Solver

Safe HaskellNone
LanguageHaskell98

Language.Fixpoint.Types.Spans

Contents

Synopsis

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

Defined in Text.Parsec.Pos

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

Show SourcePos 
Instance details

Defined in Text.Parsec.Pos

Binary SourcePos Source # 
Instance details

Defined in Language.Fixpoint.Types.Spans

Serialize SourcePos Source # 
Instance details

Defined in Language.Fixpoint.Types.Spans

NFData SourcePos Source #

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

Instance details

Defined in Language.Fixpoint.Types.Spans

Methods

rnf :: SourcePos -> () #

Hashable SourcePos Source # 
Instance details

Defined in Language.Fixpoint.Types.Spans

PPrint SourcePos Source # 
Instance details

Defined in Language.Fixpoint.Types.Spans

Fixpoint SourcePos Source # 
Instance details

Defined in Language.Fixpoint.Types.Spans

Loc SourcePos Source # 
Instance details

Defined in Language.Fixpoint.Types.Spans

data SrcSpan Source #

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

Constructors

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

Show SrcSpan Source # 
Instance details

Defined in Language.Fixpoint.Types.Spans

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 #

Serialize SrcSpan Source # 
Instance details

Defined in Language.Fixpoint.Types.Spans

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 #

PPrint SrcSpan Source # 
Instance details

Defined in Language.Fixpoint.Types.Spans

Loc SrcSpan Source # 
Instance details

Defined in Language.Fixpoint.Types.Spans

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.1-GurPN6vmwrs4cBOYBbkvBH" 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
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

Loc SrcSpan Source # 
Instance details

Defined in Language.Fixpoint.Types.Spans

Loc DataDecl Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Loc FTycon Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Loc Qualifier Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Loc EQual Source # 
Instance details

Defined in Language.Fixpoint.Types.Solutions

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

Instances
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 #

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

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

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

Defined in Language.Fixpoint.Types.Spans

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

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.1-GurPN6vmwrs4cBOYBbkvBH" 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

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

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

Destructing spans

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

Orphan instances

Binary SourcePos Source # 
Instance details

Serialize SourcePos Source # 
Instance details

NFData SourcePos Source #

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

Instance details

Methods

rnf :: SourcePos -> () #

Hashable SourcePos Source # 
Instance details

PPrint SourcePos Source # 
Instance details

Fixpoint SourcePos Source # 
Instance details