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

Safe HaskellNone
LanguageHaskell98

Language.Fixpoint.Types.Refinements

Contents

Description

This module has the types for representing terms in the refinement logic.

Synopsis

Representing Terms

data SymConst Source #

Expressions ---------------------------------------------------------------

Uninterpreted constants that are embedded as "constant symbol : Str"

Constructors

SL !Text 

Instances

Eq SymConst Source # 
Data SymConst Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SymConst -> c SymConst #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SymConst #

toConstr :: SymConst -> Constr #

dataTypeOf :: SymConst -> DataType #

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c SymConst) #

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SymConst) #

gmapT :: (forall b. Data b => b -> b) -> SymConst -> SymConst #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SymConst -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SymConst -> r #

gmapQ :: (forall d. Data d => d -> u) -> SymConst -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> SymConst -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> SymConst -> m SymConst #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SymConst -> m SymConst #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SymConst -> m SymConst #

Ord SymConst Source # 
Show SymConst Source # 
Generic SymConst Source # 

Associated Types

type Rep SymConst :: * -> * #

Methods

from :: SymConst -> Rep SymConst x #

to :: Rep SymConst x -> SymConst #

Binary SymConst Source # 

Methods

put :: SymConst -> Put #

get :: Get SymConst #

putList :: [SymConst] -> Put #

NFData SymConst Source # 

Methods

rnf :: SymConst -> () #

Hashable SymConst Source # 

Methods

hashWithSalt :: Int -> SymConst -> Int #

hash :: SymConst -> Int #

PPrint SymConst Source # 
Fixpoint SymConst Source # 
Symbolic SymConst Source #

String Constants ----------------------------------------------------------

Replace all symbol-representations-of-string-literals with string-literal Used to transform parsed output from fixpoint back into fq.

type Rep SymConst Source # 
type Rep SymConst = D1 (MetaData "SymConst" "Language.Fixpoint.Types.Refinements" "liquid-fixpoint-0.7.0.2-3repHVQ2bkqGganvJ6cFNP" False) (C1 (MetaCons "SL" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Text)))

data Constant Source #

Constructors

I !Integer 
R !Double 
L !Text !Sort 

Instances

Eq Constant Source # 
Data Constant Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Constant -> c Constant #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Constant #

toConstr :: Constant -> Constr #

dataTypeOf :: Constant -> DataType #

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c Constant) #

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Constant) #

gmapT :: (forall b. Data b => b -> b) -> Constant -> Constant #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Constant -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Constant -> r #

gmapQ :: (forall d. Data d => d -> u) -> Constant -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Constant -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Constant -> m Constant #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Constant -> m Constant #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Constant -> m Constant #

Ord Constant Source # 
Show Constant Source # 
Generic Constant Source # 

Associated Types

type Rep Constant :: * -> * #

Methods

from :: Constant -> Rep Constant x #

to :: Rep Constant x -> Constant #

Binary Constant Source # 

Methods

put :: Constant -> Put #

get :: Get Constant #

putList :: [Constant] -> Put #

NFData Constant Source # 

Methods

rnf :: Constant -> () #

Hashable Constant Source # 

Methods

hashWithSalt :: Int -> Constant -> Int #

hash :: Constant -> Int #

PPrint Constant Source # 
Fixpoint Constant Source # 
Inputable Constant Source # 
type Rep Constant Source # 

data Bop Source #

Constructors

Plus 
Minus 
Times 
Div 
Mod 
RTimes 
RDiv 

Instances

Eq Bop Source # 

Methods

(==) :: Bop -> Bop -> Bool #

(/=) :: Bop -> Bop -> Bool #

Data Bop Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Bop -> c Bop #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Bop #

toConstr :: Bop -> Constr #

dataTypeOf :: Bop -> DataType #

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c Bop) #

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Bop) #

gmapT :: (forall b. Data b => b -> b) -> Bop -> Bop #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Bop -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Bop -> r #

gmapQ :: (forall d. Data d => d -> u) -> Bop -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Bop -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Bop -> m Bop #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Bop -> m Bop #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Bop -> m Bop #

Ord Bop Source # 

Methods

compare :: Bop -> Bop -> Ordering #

(<) :: Bop -> Bop -> Bool #

(<=) :: Bop -> Bop -> Bool #

(>) :: Bop -> Bop -> Bool #

(>=) :: Bop -> Bop -> Bool #

max :: Bop -> Bop -> Bop #

min :: Bop -> Bop -> Bop #

Show Bop Source # 

Methods

showsPrec :: Int -> Bop -> ShowS #

show :: Bop -> String #

showList :: [Bop] -> ShowS #

Generic Bop Source # 

Associated Types

type Rep Bop :: * -> * #

Methods

from :: Bop -> Rep Bop x #

to :: Rep Bop x -> Bop #

Binary Bop Source # 

Methods

put :: Bop -> Put #

get :: Get Bop #

putList :: [Bop] -> Put #

NFData Bop Source # 

Methods

rnf :: Bop -> () #

Hashable Bop Source # 

Methods

hashWithSalt :: Int -> Bop -> Int #

hash :: Bop -> Int #

PPrint Bop Source # 

Methods

pprintTidy :: Tidy -> Bop -> Doc Source #

pprintPrec :: Int -> Tidy -> Bop -> Doc Source #

Fixpoint Bop Source # 

Methods

toFix :: Bop -> Doc Source #

simplify :: Bop -> Bop Source #

type Rep Bop Source # 
type Rep Bop = D1 (MetaData "Bop" "Language.Fixpoint.Types.Refinements" "liquid-fixpoint-0.7.0.2-3repHVQ2bkqGganvJ6cFNP" False) ((:+:) ((:+:) (C1 (MetaCons "Plus" PrefixI False) U1) ((:+:) (C1 (MetaCons "Minus" PrefixI False) U1) (C1 (MetaCons "Times" PrefixI False) U1))) ((:+:) ((:+:) (C1 (MetaCons "Div" PrefixI False) U1) (C1 (MetaCons "Mod" PrefixI False) U1)) ((:+:) (C1 (MetaCons "RTimes" PrefixI False) U1) (C1 (MetaCons "RDiv" PrefixI False) U1))))

data Brel Source #

Constructors

Eq 
Ne 
Gt 
Ge 
Lt 
Le 
Ueq 
Une 

Instances

Eq Brel Source # 

Methods

(==) :: Brel -> Brel -> Bool #

(/=) :: Brel -> Brel -> Bool #

Data Brel Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Brel -> c Brel #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Brel #

toConstr :: Brel -> Constr #

dataTypeOf :: Brel -> DataType #

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c Brel) #

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Brel) #

gmapT :: (forall b. Data b => b -> b) -> Brel -> Brel #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Brel -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Brel -> r #

gmapQ :: (forall d. Data d => d -> u) -> Brel -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Brel -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Brel -> m Brel #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Brel -> m Brel #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Brel -> m Brel #

Ord Brel Source # 

Methods

compare :: Brel -> Brel -> Ordering #

(<) :: Brel -> Brel -> Bool #

(<=) :: Brel -> Brel -> Bool #

(>) :: Brel -> Brel -> Bool #

(>=) :: Brel -> Brel -> Bool #

max :: Brel -> Brel -> Brel #

min :: Brel -> Brel -> Brel #

Show Brel Source # 

Methods

showsPrec :: Int -> Brel -> ShowS #

show :: Brel -> String #

showList :: [Brel] -> ShowS #

Generic Brel Source # 

Associated Types

type Rep Brel :: * -> * #

Methods

from :: Brel -> Rep Brel x #

to :: Rep Brel x -> Brel #

Binary Brel Source # 

Methods

put :: Brel -> Put #

get :: Get Brel #

putList :: [Brel] -> Put #

NFData Brel Source # 

Methods

rnf :: Brel -> () #

Hashable Brel Source # 

Methods

hashWithSalt :: Int -> Brel -> Int #

hash :: Brel -> Int #

PPrint Brel Source # 
Fixpoint Brel Source # 
type Rep Brel Source # 
type Rep Brel = D1 (MetaData "Brel" "Language.Fixpoint.Types.Refinements" "liquid-fixpoint-0.7.0.2-3repHVQ2bkqGganvJ6cFNP" False) ((:+:) ((:+:) ((:+:) (C1 (MetaCons "Eq" PrefixI False) U1) (C1 (MetaCons "Ne" PrefixI False) U1)) ((:+:) (C1 (MetaCons "Gt" PrefixI False) U1) (C1 (MetaCons "Ge" PrefixI False) U1))) ((:+:) ((:+:) (C1 (MetaCons "Lt" PrefixI False) U1) (C1 (MetaCons "Le" PrefixI False) U1)) ((:+:) (C1 (MetaCons "Ueq" PrefixI False) U1) (C1 (MetaCons "Une" PrefixI False) U1))))

data Expr Source #

Instances

Eq Expr Source # 

Methods

(==) :: Expr -> Expr -> Bool #

(/=) :: Expr -> Expr -> Bool #

Data Expr Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Expr -> c Expr #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Expr #

toConstr :: Expr -> Constr #

dataTypeOf :: Expr -> DataType #

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c Expr) #

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Expr) #

gmapT :: (forall b. Data b => b -> b) -> Expr -> Expr #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Expr -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Expr -> r #

gmapQ :: (forall d. Data d => d -> u) -> Expr -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Expr -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Expr -> m Expr #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Expr -> m Expr #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Expr -> m Expr #

Show Expr Source # 

Methods

showsPrec :: Int -> Expr -> ShowS #

show :: Expr -> String #

showList :: [Expr] -> ShowS #

Show GFixSolution # 
Generic Expr Source # 

Associated Types

type Rep Expr :: * -> * #

Methods

from :: Expr -> Rep Expr x #

to :: Rep Expr x -> Expr #

Binary Expr Source # 

Methods

put :: Expr -> Put #

get :: Get Expr #

putList :: [Expr] -> Put #

Binary GFixSolution # 
NFData Expr Source # 

Methods

rnf :: Expr -> () #

NFData GFixSolution # 

Methods

rnf :: GFixSolution -> () #

PPrint Expr Source # 
PPrint GFixSolution Source # 
Fixpoint Expr Source # 
Predicate Expr Source # 

Methods

prop :: Expr -> Expr Source #

Expression Expr Source # 

Methods

expr :: Expr -> Expr Source #

HasGradual Expr Source # 
Inputable Expr Source # 

Methods

rr :: String -> Expr Source #

rr' :: String -> String -> Expr Source #

SymConsts Expr Source # 

Methods

symConsts :: Expr -> [SymConst] Source #

Visitable Expr Source # 

Methods

visit :: Monoid a => Visitor a c -> c -> Expr -> VisitM a Expr Source #

Elaborate Expr Source # 

Methods

elaborate :: String -> SymEnv -> Expr -> Expr Source #

Gradual Expr Source # 

Methods

gsubst :: GSol -> Expr -> Expr Source #

Defunc Expr Source # 

Methods

defunc :: Expr -> DF Expr Source #

Inputable (FixResult Integer, FixSolution) Source # 
type Rep Expr Source # 
type Rep Expr = D1 (MetaData "Expr" "Language.Fixpoint.Types.Refinements" "liquid-fixpoint-0.7.0.2-3repHVQ2bkqGganvJ6cFNP" False) ((:+:) ((:+:) ((:+:) ((:+:) (C1 (MetaCons "ESym" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 SymConst))) (C1 (MetaCons "ECon" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Constant)))) ((:+:) (C1 (MetaCons "EVar" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Symbol))) ((:+:) (C1 (MetaCons "EApp" PrefixI False) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Expr)) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Expr)))) (C1 (MetaCons "ENeg" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Expr)))))) ((:+:) ((:+:) (C1 (MetaCons "EBin" PrefixI False) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Bop)) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Expr)) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Expr))))) (C1 (MetaCons "EIte" PrefixI False) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Expr)) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Expr)) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Expr)))))) ((:+:) (C1 (MetaCons "ECst" PrefixI False) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Expr)) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Sort)))) ((:+:) (C1 (MetaCons "ELam" PrefixI False) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 (Symbol, Sort))) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Expr)))) (C1 (MetaCons "ETApp" PrefixI False) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Expr)) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Sort)))))))) ((:+:) ((:+:) ((:+:) (C1 (MetaCons "ETAbs" PrefixI False) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Expr)) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Symbol)))) (C1 (MetaCons "PAnd" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 [Expr])))) ((:+:) (C1 (MetaCons "POr" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 [Expr]))) ((:+:) (C1 (MetaCons "PNot" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Expr))) (C1 (MetaCons "PImp" PrefixI False) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Expr)) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Expr))))))) ((:+:) ((:+:) (C1 (MetaCons "PIff" PrefixI False) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Expr)) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Expr)))) ((:+:) (C1 (MetaCons "PAtom" PrefixI False) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Brel)) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Expr)) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Expr))))) (C1 (MetaCons "PKVar" PrefixI False) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 KVar)) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Subst)))))) ((:+:) (C1 (MetaCons "PAll" PrefixI False) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 [(Symbol, Sort)])) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Expr)))) ((:+:) (C1 (MetaCons "PExist" PrefixI False) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 [(Symbol, Sort)])) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Expr)))) (C1 (MetaCons "PGrad" PrefixI False) ((:*:) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 KVar)) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Subst))) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 GradInfo)) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Expr))))))))))

type Pred = Expr Source #

data GradInfo Source #

Constructors

GradInfo 

Fields

Instances

Eq GradInfo Source # 
Data GradInfo Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> GradInfo -> c GradInfo #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c GradInfo #

toConstr :: GradInfo -> Constr #

dataTypeOf :: GradInfo -> DataType #

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c GradInfo) #

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c GradInfo) #

gmapT :: (forall b. Data b => b -> b) -> GradInfo -> GradInfo #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> GradInfo -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> GradInfo -> r #

gmapQ :: (forall d. Data d => d -> u) -> GradInfo -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> GradInfo -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> GradInfo -> m GradInfo #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> GradInfo -> m GradInfo #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> GradInfo -> m GradInfo #

Show GradInfo Source # 
Generic GradInfo Source # 

Associated Types

type Rep GradInfo :: * -> * #

Methods

from :: GradInfo -> Rep GradInfo x #

to :: Rep GradInfo x -> GradInfo #

Binary GradInfo Source # 

Methods

put :: GradInfo -> Put #

get :: Get GradInfo #

putList :: [GradInfo] -> Put #

NFData GradInfo Source # 

Methods

rnf :: GradInfo -> () #

type Rep GradInfo Source # 
type Rep GradInfo = D1 (MetaData "GradInfo" "Language.Fixpoint.Types.Refinements" "liquid-fixpoint-0.7.0.2-3repHVQ2bkqGganvJ6cFNP" False) (C1 (MetaCons "GradInfo" PrefixI True) ((:*:) (S1 (MetaSel (Just Symbol "gsrc") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 SrcSpan)) (S1 (MetaSel (Just Symbol "gused") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe SrcSpan)))))

pattern PTrue :: Expr Source #

pattern PTop :: Expr Source #

pattern PFalse :: Expr Source #

pattern EBot :: Expr Source #

pattern ETimes :: Expr -> Expr -> Expr Source #

pattern ERTimes :: Expr -> Expr -> Expr Source #

pattern EDiv :: Expr -> Expr -> Expr Source #

pattern ERDiv :: Expr -> Expr -> Expr Source #

pattern EEq :: Expr -> Expr -> Expr Source #

newtype KVar Source #

Kvars ---------------------------------------------------------------------

Constructors

KV 

Fields

Instances

Eq KVar Source # 

Methods

(==) :: KVar -> KVar -> Bool #

(/=) :: KVar -> KVar -> Bool #

Data KVar Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> KVar -> c KVar #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c KVar #

toConstr :: KVar -> Constr #

dataTypeOf :: KVar -> DataType #

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c KVar) #

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c KVar) #

gmapT :: (forall b. Data b => b -> b) -> KVar -> KVar #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> KVar -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> KVar -> r #

gmapQ :: (forall d. Data d => d -> u) -> KVar -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> KVar -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> KVar -> m KVar #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> KVar -> m KVar #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> KVar -> m KVar #

Ord KVar Source # 

Methods

compare :: KVar -> KVar -> Ordering #

(<) :: KVar -> KVar -> Bool #

(<=) :: KVar -> KVar -> Bool #

(>) :: KVar -> KVar -> Bool #

(>=) :: KVar -> KVar -> Bool #

max :: KVar -> KVar -> KVar #

min :: KVar -> KVar -> KVar #

Show KVar Source # 

Methods

showsPrec :: Int -> KVar -> ShowS #

show :: KVar -> String #

showList :: [KVar] -> ShowS #

IsString KVar Source # 

Methods

fromString :: String -> KVar #

Generic KVar Source # 

Associated Types

type Rep KVar :: * -> * #

Methods

from :: KVar -> Rep KVar x #

to :: Rep KVar x -> KVar #

Binary KVar Source # 

Methods

put :: KVar -> Put #

get :: Get KVar #

putList :: [KVar] -> Put #

NFData KVar Source # 

Methods

rnf :: KVar -> () #

Hashable KVar Source # 

Methods

hashWithSalt :: Int -> KVar -> Int #

hash :: KVar -> Int #

PPrint KVar Source # 
Fixpoint KVar Source # 
Inputable (FixResult Integer, FixSolution) Source # 
type Rep KVar Source # 
type Rep KVar = D1 (MetaData "KVar" "Language.Fixpoint.Types.Refinements" "liquid-fixpoint-0.7.0.2-3repHVQ2bkqGganvJ6cFNP" True) (C1 (MetaCons "KV" PrefixI True) (S1 (MetaSel (Just Symbol "kv") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Symbol)))

newtype Subst Source #

Substitutions -------------------------------------------------------------

Constructors

Su (HashMap Symbol Expr) 

Instances

Eq Subst Source # 

Methods

(==) :: Subst -> Subst -> Bool #

(/=) :: Subst -> Subst -> Bool #

Data Subst Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Subst -> c Subst #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Subst #

toConstr :: Subst -> Constr #

dataTypeOf :: Subst -> DataType #

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c Subst) #

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Subst) #

gmapT :: (forall b. Data b => b -> b) -> Subst -> Subst #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Subst -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Subst -> r #

gmapQ :: (forall d. Data d => d -> u) -> Subst -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Subst -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Subst -> m Subst #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Subst -> m Subst #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Subst -> m Subst #

Show Subst Source # 

Methods

showsPrec :: Int -> Subst -> ShowS #

show :: Subst -> String #

showList :: [Subst] -> ShowS #

Generic Subst Source # 

Associated Types

type Rep Subst :: * -> * #

Methods

from :: Subst -> Rep Subst x #

to :: Rep Subst x -> Subst #

Binary Subst Source # 

Methods

put :: Subst -> Put #

get :: Get Subst #

putList :: [Subst] -> Put #

NFData Subst Source # 

Methods

rnf :: Subst -> () #

PPrint Subst Source # 
Fixpoint Subst Source # 
type Rep Subst Source # 
type Rep Subst = D1 (MetaData "Subst" "Language.Fixpoint.Types.Refinements" "liquid-fixpoint-0.7.0.2-3repHVQ2bkqGganvJ6cFNP" True) (C1 (MetaCons "Su" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (HashMap Symbol Expr))))

data KVSub Source #

Constructors

KVS 

Instances

Eq KVSub Source # 

Methods

(==) :: KVSub -> KVSub -> Bool #

(/=) :: KVSub -> KVSub -> Bool #

Data KVSub Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> KVSub -> c KVSub #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c KVSub #

toConstr :: KVSub -> Constr #

dataTypeOf :: KVSub -> DataType #

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c KVSub) #

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c KVSub) #

gmapT :: (forall b. Data b => b -> b) -> KVSub -> KVSub #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> KVSub -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> KVSub -> r #

gmapQ :: (forall d. Data d => d -> u) -> KVSub -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> KVSub -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> KVSub -> m KVSub #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> KVSub -> m KVSub #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> KVSub -> m KVSub #

Show KVSub Source # 

Methods

showsPrec :: Int -> KVSub -> ShowS #

show :: KVSub -> String #

showList :: [KVSub] -> ShowS #

Generic KVSub Source # 

Associated Types

type Rep KVSub :: * -> * #

Methods

from :: KVSub -> Rep KVSub x #

to :: Rep KVSub x -> KVSub #

PPrint KVSub Source # 
type Rep KVSub Source # 

newtype Reft Source #

Parsed refinement of Symbol as Expr e.g. in '{v: _ | e }' v is the Symbol and e the Expr

Constructors

Reft (Symbol, Expr) 

Instances

Eq Reft Source # 

Methods

(==) :: Reft -> Reft -> Bool #

(/=) :: Reft -> Reft -> Bool #

Data Reft Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Reft -> c Reft #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Reft #

toConstr :: Reft -> Constr #

dataTypeOf :: Reft -> DataType #

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c Reft) #

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Reft) #

gmapT :: (forall b. Data b => b -> b) -> Reft -> Reft #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Reft -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Reft -> r #

gmapQ :: (forall d. Data d => d -> u) -> Reft -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Reft -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Reft -> m Reft #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Reft -> m Reft #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Reft -> m Reft #

Generic Reft Source # 

Associated Types

type Rep Reft :: * -> * #

Methods

from :: Reft -> Rep Reft x #

to :: Rep Reft x -> Reft #

Binary Reft Source # 

Methods

put :: Reft -> Put #

get :: Get Reft #

putList :: [Reft] -> Put #

NFData Reft Source # 

Methods

rnf :: Reft -> () #

Expression Reft Source # 

Methods

expr :: Reft -> Expr Source #

HasGradual Reft Source # 
SymConsts Reft Source # 

Methods

symConsts :: Reft -> [SymConst] Source #

Visitable Reft Source # 

Methods

visit :: Monoid a => Visitor a c -> c -> Reft -> VisitM a Reft Source #

Gradual Reft Source # 

Methods

gsubst :: GSol -> Reft -> Reft Source #

Defunc Reft Source # 

Methods

defunc :: Reft -> DF Reft Source #

type Rep Reft Source # 
type Rep Reft = D1 (MetaData "Reft" "Language.Fixpoint.Types.Refinements" "liquid-fixpoint-0.7.0.2-3repHVQ2bkqGganvJ6cFNP" True) (C1 (MetaCons "Reft" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Symbol, Expr))))

data SortedReft Source #

Constructors

RR 

Fields

Instances

Eq SortedReft Source # 
Data SortedReft Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SortedReft -> c SortedReft #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SortedReft #

toConstr :: SortedReft -> Constr #

dataTypeOf :: SortedReft -> DataType #

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c SortedReft) #

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SortedReft) #

gmapT :: (forall b. Data b => b -> b) -> SortedReft -> SortedReft #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SortedReft -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SortedReft -> r #

gmapQ :: (forall d. Data d => d -> u) -> SortedReft -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> SortedReft -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> SortedReft -> m SortedReft #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SortedReft -> m SortedReft #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SortedReft -> m SortedReft #

Generic SortedReft Source # 

Associated Types

type Rep SortedReft :: * -> * #

Monoid BindEnv # 
Binary SortedReft Source # 
Binary BindEnv # 

Methods

put :: BindEnv -> Put #

get :: Get BindEnv #

putList :: [BindEnv] -> Put #

NFData SortedReft Source # 

Methods

rnf :: SortedReft -> () #

NFData BindEnv # 

Methods

rnf :: BindEnv -> () #

Fixpoint BindEnv Source # 
Expression SortedReft Source # 

Methods

expr :: SortedReft -> Expr Source #

HasGradual SortedReft Source # 
SymConsts SortedReft Source # 
SymConsts BindEnv Source # 
Visitable SortedReft Source # 

Methods

visit :: Monoid a => Visitor a c -> c -> SortedReft -> VisitM a SortedReft Source #

Visitable BindEnv Source # 

Methods

visit :: Monoid a => Visitor a c -> c -> BindEnv -> VisitM a BindEnv Source #

Elaborate SortedReft Source # 
Elaborate BindEnv Source # 
Gradual SortedReft Source # 
Gradual BindEnv Source # 

Methods

gsubst :: GSol -> BindEnv -> BindEnv Source #

Defunc SortedReft Source # 
Defunc BindEnv Source # 

Methods

defunc :: BindEnv -> DF BindEnv Source #

Visitable (Symbol, SortedReft) Source # 

Methods

visit :: Monoid a => Visitor a c -> c -> (Symbol, SortedReft) -> VisitM a (Symbol, SortedReft) Source #

Defunc (Symbol, SortedReft) Source # 
type Rep SortedReft Source # 
type Rep SortedReft = D1 (MetaData "SortedReft" "Language.Fixpoint.Types.Refinements" "liquid-fixpoint-0.7.0.2-3repHVQ2bkqGganvJ6cFNP" False) (C1 (MetaCons "RR" PrefixI True) ((:*:) (S1 (MetaSel (Just Symbol "sr_sort") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Sort)) (S1 (MetaSel (Just Symbol "sr_reft") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Reft))))

Constructing Terms

eVar :: Symbolic a => a -> Expr Source #

eProp :: Symbolic a => a -> Expr Source #

pIte :: Pred -> Expr -> Expr -> Expr Source #

Generalizing Embedding with Typeclasses

class Expression a where Source #

Generalizing Symbol, Expression, Predicate into Classes -----------

Values that can be viewed as Constants

Values that can be viewed as Expressions

Minimal complete definition

expr

Methods

expr :: a -> Expr Source #

Instances

Expression Int Source # 

Methods

expr :: Int -> Expr Source #

Expression Integer Source # 

Methods

expr :: Integer -> Expr Source #

Expression Text Source # 

Methods

expr :: Text -> Expr Source #

Expression Symbol Source #

The symbol may be an encoding of a SymConst.

Methods

expr :: Symbol -> Expr Source #

Expression SortedReft Source # 

Methods

expr :: SortedReft -> Expr Source #

Expression Reft Source # 

Methods

expr :: Reft -> Expr Source #

Expression Expr Source # 

Methods

expr :: Expr -> Expr Source #

Expression Bv Source #

Construct an Expr using a raw string, e.g. (Bv S32 "#x02000000")

Methods

expr :: Bv -> Expr Source #

Expression a => Expression (Located a) Source # 

Methods

expr :: Located a -> Expr Source #

class Predicate a where Source #

Values that can be viewed as Predicates

Minimal complete definition

prop

Methods

prop :: a -> Expr Source #

class Subable a where Source #

Class Predicates for Valid Refinements -----------------------------

Minimal complete definition

syms, substa, substf, subst

Methods

syms :: a -> [Symbol] Source #

substa :: (Symbol -> Symbol) -> a -> a Source #

substf :: (Symbol -> Expr) -> a -> a Source #

subst :: Subst -> a -> a Source #

subst1 :: a -> (Symbol, Expr) -> a Source #

Instances

class (Monoid r, Subable r) => Reftable r where Source #

Minimal complete definition

isTauto, ppTy, bot, toReft, ofReft, params

Methods

isTauto :: r -> Bool Source #

ppTy :: r -> Doc -> Doc Source #

top :: r -> r Source #

bot :: r -> r Source #

meet :: r -> r -> r Source #

toReft :: r -> Reft Source #

ofReft :: Reft -> r Source #

params :: r -> [Symbol] Source #

Constructors

symbolReft :: Symbolic a => a -> Reft Source #

Generally Useful Refinements --------------------------

Predicates

isFunctionSortedReft :: SortedReft -> Bool Source #

Refinements ----------------------------------------------

isSingletonReft :: Reft -> Maybe Expr Source #

Predicates ----------------------------------------------------------------

isFalse :: Falseable a => a -> Bool Source #

Destructing

eApps :: Expr -> [Expr] -> Expr Source #

Transforming

Gradual Type Manipulation

pGAnds :: [Expr] -> Expr Source #

Gradual Type Manipulation ----------------------------

Orphan instances

Binary SrcSpan Source # 

Methods

put :: SrcSpan -> Put #

get :: Get SrcSpan #

putList :: [SrcSpan] -> Put #

NFData SrcSpan Source # 

Methods

rnf :: SrcSpan -> () #

PPrint Sort Source # 
(Hashable k, Eq k, Binary k, Binary v) => Binary (HashMap k v) Source # 

Methods

put :: HashMap k v -> Put #

get :: Get (HashMap k v) #

putList :: [HashMap k v] -> Put #