liquid-fixpoint-0.9.2.5: Predicate Abstraction-based Horn-Clause/Implication Constraint Solver
Safe HaskellSafe-Inferred
LanguageHaskell98

Language.Fixpoint.Types.Refinements

Description

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

Synopsis

Representing Terms

newtype SymConst Source #

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

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

Constructors

SL Text 

Instances

Instances details
Data SymConst Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

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 :: forall r r'. (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 #

Generic SymConst Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Associated Types

type Rep SymConst :: Type -> Type #

Methods

from :: SymConst -> Rep SymConst x #

to :: Rep SymConst x -> SymConst #

Show SymConst Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Binary SymConst Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

put :: SymConst -> Put #

get :: Get SymConst #

putList :: [SymConst] -> Put #

NFData SymConst Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

rnf :: SymConst -> () #

Eq SymConst Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Ord SymConst Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Hashable SymConst Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

hashWithSalt :: Int -> SymConst -> Int #

hash :: SymConst -> Int #

SMTLIB2 SymConst Source # 
Instance details

Defined in Language.Fixpoint.Smt.Serialize

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.

Instance details

Defined in Language.Fixpoint.Types.Refinements

Fixpoint SymConst Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

PPrint SymConst Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Store SymConst Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

type Rep SymConst Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

type Rep SymConst = D1 ('MetaData "SymConst" "Language.Fixpoint.Types.Refinements" "liquid-fixpoint-0.9.2.5-8VOJ4a5jXPy7nyhLFTxkOW" 'True) (C1 ('MetaCons "SL" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Text)))

data Constant Source #

Constructors

I !Integer 
R !Double 
L !Text !Sort 

Instances

Instances details
Data Constant Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

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 :: forall r r'. (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 #

Generic Constant Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Associated Types

type Rep Constant :: Type -> Type #

Methods

from :: Constant -> Rep Constant x #

to :: Rep Constant x -> Constant #

Show Constant Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Binary Constant Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

put :: Constant -> Put #

get :: Get Constant #

putList :: [Constant] -> Put #

NFData Constant Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

rnf :: Constant -> () #

Eq Constant Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Ord Constant Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Hashable Constant Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

hashWithSalt :: Int -> Constant -> Int #

hash :: Constant -> Int #

Inputable Constant Source # 
Instance details

Defined in Language.Fixpoint.Parse

SMTLIB2 Constant Source # 
Instance details

Defined in Language.Fixpoint.Smt.Serialize

Fixpoint Constant Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

PPrint Constant Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Store Constant Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

type Rep Constant Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

data Bop Source #

Constructors

Plus 
Minus 
Times 
Div 
Mod 
RTimes 
RDiv 

Instances

Instances details
Data Bop Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

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 :: forall r r'. (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 #

Generic Bop Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Associated Types

type Rep Bop :: Type -> Type #

Methods

from :: Bop -> Rep Bop x #

to :: Rep Bop x -> Bop #

Show Bop Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

showsPrec :: Int -> Bop -> ShowS #

show :: Bop -> String #

showList :: [Bop] -> ShowS #

Binary Bop Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

put :: Bop -> Put #

get :: Get Bop #

putList :: [Bop] -> Put #

NFData Bop Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

rnf :: Bop -> () #

Eq Bop Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

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

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

Ord Bop Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

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 #

Hashable Bop Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

hashWithSalt :: Int -> Bop -> Int #

hash :: Bop -> Int #

SMTLIB2 Bop Source # 
Instance details

Defined in Language.Fixpoint.Smt.Serialize

Methods

smt2 :: SymEnv -> Bop -> Builder Source #

Fixpoint Bop Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

toFix :: Bop -> Doc Source #

simplify :: Bop -> Bop Source #

PPrint Bop Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

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

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

Store Bop Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

size :: Size Bop #

poke :: Bop -> Poke () #

peek :: Peek Bop #

type Rep Bop Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

type Rep Bop = D1 ('MetaData "Bop" "Language.Fixpoint.Types.Refinements" "liquid-fixpoint-0.9.2.5-8VOJ4a5jXPy7nyhLFTxkOW" 'False) ((C1 ('MetaCons "Plus" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Minus" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Times" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "Div" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Mod" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "RTimes" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "RDiv" 'PrefixI 'False) (U1 :: Type -> Type))))

data Brel Source #

Constructors

Eq 
Ne 
Gt 
Ge 
Lt 
Le 
Ueq 
Une 

Instances

Instances details
Data Brel Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

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 :: forall r r'. (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 #

Generic Brel Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Associated Types

type Rep Brel :: Type -> Type #

Methods

from :: Brel -> Rep Brel x #

to :: Rep Brel x -> Brel #

Show Brel Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

showsPrec :: Int -> Brel -> ShowS #

show :: Brel -> String #

showList :: [Brel] -> ShowS #

Binary Brel Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

put :: Brel -> Put #

get :: Get Brel #

putList :: [Brel] -> Put #

NFData Brel Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

rnf :: Brel -> () #

Eq Brel Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

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

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

Ord Brel Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

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 #

Hashable Brel Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

hashWithSalt :: Int -> Brel -> Int #

hash :: Brel -> Int #

SMTLIB2 Brel Source # 
Instance details

Defined in Language.Fixpoint.Smt.Serialize

Methods

smt2 :: SymEnv -> Brel -> Builder Source #

Fixpoint Brel Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

PPrint Brel Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Store Brel Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

size :: Size Brel #

poke :: Brel -> Poke () #

peek :: Peek Brel #

type Rep Brel Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

type Rep Brel = D1 ('MetaData "Brel" "Language.Fixpoint.Types.Refinements" "liquid-fixpoint-0.9.2.5-8VOJ4a5jXPy7nyhLFTxkOW" 'False) (((C1 ('MetaCons "Eq" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Ne" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "Gt" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Ge" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "Lt" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Le" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "Ueq" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Une" 'PrefixI 'False) (U1 :: Type -> Type))))

data Expr Source #

Instances

Instances details
Data Expr Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

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 :: forall r r'. (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 #

Monoid Expr Source # 
Instance details

Defined in Language.Fixpoint.Types.Substitutions

Methods

mempty :: Expr #

mappend :: Expr -> Expr -> Expr #

mconcat :: [Expr] -> Expr #

Semigroup Expr Source # 
Instance details

Defined in Language.Fixpoint.Types.Substitutions

Methods

(<>) :: Expr -> Expr -> Expr #

sconcat :: NonEmpty Expr -> Expr #

stimes :: Integral b => b -> Expr -> Expr #

Generic Expr Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Associated Types

type Rep Expr :: Type -> Type #

Methods

from :: Expr -> Rep Expr x #

to :: Rep Expr x -> Expr #

Show GFixSolution Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Show Expr Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

showsPrec :: Int -> Expr -> ShowS #

show :: Expr -> String #

showList :: [Expr] -> ShowS #

Binary Expr Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

put :: Expr -> Put #

get :: Get Expr #

putList :: [Expr] -> Put #

NFData GFixSolution Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Methods

rnf :: GFixSolution -> () #

NFData Expr Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

rnf :: Expr -> () #

Eq Expr Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

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

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

Ord Expr Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

compare :: Expr -> Expr -> Ordering #

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

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

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

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

max :: Expr -> Expr -> Expr #

min :: Expr -> Expr -> Expr #

Hashable Expr Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

hashWithSalt :: Int -> Expr -> Int #

hash :: Expr -> Int #

Defunc Expr Source # 
Instance details

Defined in Language.Fixpoint.Defunctionalize

Methods

defunc :: Expr -> DF Expr Source #

Inputable Expr Source # 
Instance details

Defined in Language.Fixpoint.Parse

Methods

rr :: String -> Expr Source #

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

SMTLIB2 Expr Source # 
Instance details

Defined in Language.Fixpoint.Smt.Serialize

Methods

smt2 :: SymEnv -> Expr -> Builder Source #

Simplifiable Expr Source # 
Instance details

Defined in Language.Fixpoint.Solver.Interpreter

Methods

simplify :: Knowledge -> ICtx -> Expr -> Expr Source #

Elaborate Expr Source # 
Instance details

Defined in Language.Fixpoint.SortCheck

Gradual Expr Source # 
Instance details

Defined in Language.Fixpoint.Types.Graduals

Methods

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

Fixpoint Expr Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

PPrint GFixSolution Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

PPrint Expr Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Expression Expr Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

expr :: Expr -> Expr Source #

HasGradual Expr Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Predicate Expr Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

prop :: Expr -> Expr Source #

Subable Expr Source # 
Instance details

Defined in Language.Fixpoint.Types.Substitutions

SymConsts Expr Source # 
Instance details

Defined in Language.Fixpoint.Types.Visitor

Methods

symConsts :: Expr -> [SymConst] Source #

Visitable Expr Source # 
Instance details

Defined in Language.Fixpoint.Types.Visitor

Methods

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

Store GFixSolution Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Store Expr Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

size :: Size Expr #

poke :: Expr -> Poke () #

peek :: Peek Expr #

SMTLIB2 (Triggered Expr) Source # 
Instance details

Defined in Language.Fixpoint.Smt.Serialize

Inputable (FixResult Integer, FixSolution) Source # 
Instance details

Defined in Language.Fixpoint.Parse

type Rep Expr Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

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

type Pred = Expr Source #

data GradInfo Source #

Constructors

GradInfo 

Fields

Instances

Instances details
Data GradInfo Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

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 :: forall r r'. (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 #

Generic GradInfo Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Associated Types

type Rep GradInfo :: Type -> Type #

Methods

from :: GradInfo -> Rep GradInfo x #

to :: Rep GradInfo x -> GradInfo #

Show GradInfo Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Binary GradInfo Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

put :: GradInfo -> Put #

get :: Get GradInfo #

putList :: [GradInfo] -> Put #

NFData GradInfo Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

rnf :: GradInfo -> () #

Eq GradInfo Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Ord GradInfo Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Hashable GradInfo Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

hashWithSalt :: Int -> GradInfo -> Int #

hash :: GradInfo -> Int #

Store GradInfo Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

type Rep GradInfo Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

type Rep GradInfo = D1 ('MetaData "GradInfo" "Language.Fixpoint.Types.Refinements" "liquid-fixpoint-0.9.2.5-8VOJ4a5jXPy7nyhLFTxkOW" 'False) (C1 ('MetaCons "GradInfo" 'PrefixI 'True) (S1 ('MetaSel ('Just "gsrc") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SrcSpan) :*: S1 ('MetaSel ('Just "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

Instances details
Data KVar Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

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 :: forall r r'. (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 #

IsString KVar Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

fromString :: String -> KVar #

Generic KVar Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Associated Types

type Rep KVar :: Type -> Type #

Methods

from :: KVar -> Rep KVar x #

to :: Rep KVar x -> KVar #

Show KVar Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

showsPrec :: Int -> KVar -> ShowS #

show :: KVar -> String #

showList :: [KVar] -> ShowS #

Binary KVar Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

put :: KVar -> Put #

get :: Get KVar #

putList :: [KVar] -> Put #

NFData KVar Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

rnf :: KVar -> () #

Eq KVar Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

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

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

Ord KVar Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

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 #

Hashable KVar Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

hashWithSalt :: Int -> KVar -> Int #

hash :: KVar -> Int #

Fixpoint KVar Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

PPrint KVar Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Store KVar Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

size :: Size KVar #

poke :: KVar -> Poke () #

peek :: Peek KVar #

Inputable (FixResult Integer, FixSolution) Source # 
Instance details

Defined in Language.Fixpoint.Parse

type Rep KVar Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

type Rep KVar = D1 ('MetaData "KVar" "Language.Fixpoint.Types.Refinements" "liquid-fixpoint-0.9.2.5-8VOJ4a5jXPy7nyhLFTxkOW" 'True) (C1 ('MetaCons "KV" 'PrefixI 'True) (S1 ('MetaSel ('Just "kv") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Symbol)))

newtype Subst Source #

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

Constructors

Su (HashMap Symbol Expr) 

Instances

Instances details
Data Subst Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

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 :: forall r r'. (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 #

Monoid Subst Source # 
Instance details

Defined in Language.Fixpoint.Types.Substitutions

Methods

mempty :: Subst #

mappend :: Subst -> Subst -> Subst #

mconcat :: [Subst] -> Subst #

Semigroup Subst Source # 
Instance details

Defined in Language.Fixpoint.Types.Substitutions

Methods

(<>) :: Subst -> Subst -> Subst #

sconcat :: NonEmpty Subst -> Subst #

stimes :: Integral b => b -> Subst -> Subst #

Generic Subst Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Associated Types

type Rep Subst :: Type -> Type #

Methods

from :: Subst -> Rep Subst x #

to :: Rep Subst x -> Subst #

Show Subst Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

showsPrec :: Int -> Subst -> ShowS #

show :: Subst -> String #

showList :: [Subst] -> ShowS #

Binary Subst Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

put :: Subst -> Put #

get :: Get Subst #

putList :: [Subst] -> Put #

NFData Subst Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

rnf :: Subst -> () #

Eq Subst Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

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

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

Ord Subst Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

compare :: Subst -> Subst -> Ordering #

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

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

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

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

max :: Subst -> Subst -> Subst #

min :: Subst -> Subst -> Subst #

Hashable Subst Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

hashWithSalt :: Int -> Subst -> Int #

hash :: Subst -> Int #

Fixpoint Subst Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

PPrint Subst Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Store Subst Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

size :: Size Subst #

poke :: Subst -> Poke () #

peek :: Peek Subst #

type Rep Subst Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

type Rep Subst = D1 ('MetaData "Subst" "Language.Fixpoint.Types.Refinements" "liquid-fixpoint-0.9.2.5-8VOJ4a5jXPy7nyhLFTxkOW" 'True) (C1 ('MetaCons "Su" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashMap Symbol Expr))))

data KVSub Source #

Constructors

KVS 

Instances

Instances details
Data KVSub Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

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 :: forall r r'. (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 #

Generic KVSub Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Associated Types

type Rep KVSub :: Type -> Type #

Methods

from :: KVSub -> Rep KVSub x #

to :: Rep KVSub x -> KVSub #

Show KVSub Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

showsPrec :: Int -> KVSub -> ShowS #

show :: KVSub -> String #

showList :: [KVSub] -> ShowS #

Eq KVSub Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

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

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

PPrint KVSub Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

type Rep KVSub Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

type Rep KVSub = D1 ('MetaData "KVSub" "Language.Fixpoint.Types.Refinements" "liquid-fixpoint-0.9.2.5-8VOJ4a5jXPy7nyhLFTxkOW" 'False) (C1 ('MetaCons "KVS" 'PrefixI 'True) ((S1 ('MetaSel ('Just "ksuVV") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Symbol) :*: S1 ('MetaSel ('Just "ksuSort") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Sort)) :*: (S1 ('MetaSel ('Just "ksuKVar") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KVar) :*: S1 ('MetaSel ('Just "ksuSubst") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Subst))))

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

Instances details
Data Reft Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

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 :: forall r r'. (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 #

Monoid Reft Source # 
Instance details

Defined in Language.Fixpoint.Types.Substitutions

Methods

mempty :: Reft #

mappend :: Reft -> Reft -> Reft #

mconcat :: [Reft] -> Reft #

Semigroup Reft Source # 
Instance details

Defined in Language.Fixpoint.Types.Substitutions

Methods

(<>) :: Reft -> Reft -> Reft #

sconcat :: NonEmpty Reft -> Reft #

stimes :: Integral b => b -> Reft -> Reft #

Generic Reft Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Associated Types

type Rep Reft :: Type -> Type #

Methods

from :: Reft -> Rep Reft x #

to :: Rep Reft x -> Reft #

Show Reft Source # 
Instance details

Defined in Language.Fixpoint.Types.Substitutions

Methods

showsPrec :: Int -> Reft -> ShowS #

show :: Reft -> String #

showList :: [Reft] -> ShowS #

Binary Reft Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

put :: Reft -> Put #

get :: Get Reft #

putList :: [Reft] -> Put #

NFData Reft Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

rnf :: Reft -> () #

Eq Reft Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

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

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

Ord Reft Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

compare :: Reft -> Reft -> Ordering #

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

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

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

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

max :: Reft -> Reft -> Reft #

min :: Reft -> Reft -> Reft #

Hashable Reft Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

hashWithSalt :: Int -> Reft -> Int #

hash :: Reft -> Int #

Defunc Reft Source # 
Instance details

Defined in Language.Fixpoint.Defunctionalize

Methods

defunc :: Reft -> DF Reft Source #

Gradual Reft Source # 
Instance details

Defined in Language.Fixpoint.Types.Graduals

Methods

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

Fixpoint Reft Source # 
Instance details

Defined in Language.Fixpoint.Types.Substitutions

PPrint Reft Source # 
Instance details

Defined in Language.Fixpoint.Types.Substitutions

Expression Reft Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

expr :: Reft -> Expr Source #

HasGradual Reft Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Reftable Reft Source # 
Instance details

Defined in Language.Fixpoint.Types.Substitutions

Subable Reft Source # 
Instance details

Defined in Language.Fixpoint.Types.Substitutions

SymConsts Reft Source # 
Instance details

Defined in Language.Fixpoint.Types.Visitor

Methods

symConsts :: Reft -> [SymConst] Source #

Visitable Reft Source # 
Instance details

Defined in Language.Fixpoint.Types.Visitor

Methods

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

Store Reft Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

size :: Size Reft #

poke :: Reft -> Poke () #

peek :: Peek Reft #

type Rep Reft Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

type Rep Reft = D1 ('MetaData "Reft" "Language.Fixpoint.Types.Refinements" "liquid-fixpoint-0.9.2.5-8VOJ4a5jXPy7nyhLFTxkOW" 'True) (C1 ('MetaCons "Reft" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Symbol, Expr))))

data SortedReft Source #

Constructors

RR 

Fields

Instances

Instances details
Data SortedReft Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

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 :: forall r r'. (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 #

Monoid SortedReft Source # 
Instance details

Defined in Language.Fixpoint.Types.Substitutions

Semigroup SortedReft Source # 
Instance details

Defined in Language.Fixpoint.Types.Substitutions

Generic SortedReft Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Associated Types

type Rep SortedReft :: Type -> Type #

Show SortedReft Source # 
Instance details

Defined in Language.Fixpoint.Types.Substitutions

NFData SortedReft Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

rnf :: SortedReft -> () #

Eq SortedReft Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Ord SortedReft Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Hashable SortedReft Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Defunc SortedReft Source # 
Instance details

Defined in Language.Fixpoint.Defunctionalize

Elaborate SortedReft Source # 
Instance details

Defined in Language.Fixpoint.SortCheck

Gradual SortedReft Source # 
Instance details

Defined in Language.Fixpoint.Types.Graduals

Fixpoint SortedReft Source # 
Instance details

Defined in Language.Fixpoint.Types.Substitutions

PPrint SortedReft Source # 
Instance details

Defined in Language.Fixpoint.Types.Substitutions

Expression SortedReft Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

expr :: SortedReft -> Expr Source #

HasGradual SortedReft Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Reftable SortedReft Source # 
Instance details

Defined in Language.Fixpoint.Types.Substitutions

Subable SortedReft Source # 
Instance details

Defined in Language.Fixpoint.Types.Substitutions

SymConsts SortedReft Source # 
Instance details

Defined in Language.Fixpoint.Types.Visitor

Visitable SortedReft Source # 
Instance details

Defined in Language.Fixpoint.Types.Visitor

Methods

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

Store SortedReft Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Monoid (BindEnv a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Environments

Methods

mempty :: BindEnv a #

mappend :: BindEnv a -> BindEnv a -> BindEnv a #

mconcat :: [BindEnv a] -> BindEnv a #

Semigroup (BindEnv a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Environments

Methods

(<>) :: BindEnv a -> BindEnv a -> BindEnv a #

sconcat :: NonEmpty (BindEnv a) -> BindEnv a #

stimes :: Integral b => b -> BindEnv a -> BindEnv a #

NFData a => NFData (BindEnv a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Environments

Methods

rnf :: BindEnv a -> () #

Defunc (BindEnv a) Source # 
Instance details

Defined in Language.Fixpoint.Defunctionalize

Methods

defunc :: BindEnv a -> DF (BindEnv a) Source #

Loc a => Elaborate (BindEnv a) Source # 
Instance details

Defined in Language.Fixpoint.SortCheck

Gradual (BindEnv a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Graduals

Methods

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

Fixpoint (BindEnv a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Environments

SymConsts (BindEnv a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Visitor

Methods

symConsts :: BindEnv a -> [SymConst] Source #

Visitable (BindEnv a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Visitor

Methods

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

Store a => Store (BindEnv a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Environments

Methods

size :: Size (BindEnv a) #

poke :: BindEnv a -> Poke () #

peek :: Peek (BindEnv a) #

Defunc (Symbol, SortedReft) Source # 
Instance details

Defined in Language.Fixpoint.Defunctionalize

Expression (Symbol, SortedReft) Source # 
Instance details

Defined in Language.Fixpoint.Types.Substitutions

Methods

expr :: (Symbol, SortedReft) -> Expr Source #

Visitable (Symbol, SortedReft, a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Visitor

Methods

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

type Rep SortedReft Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

type Rep SortedReft = D1 ('MetaData "SortedReft" "Language.Fixpoint.Types.Refinements" "liquid-fixpoint-0.9.2.5-8VOJ4a5jXPy7nyhLFTxkOW" 'False) (C1 ('MetaCons "RR" 'PrefixI 'True) (S1 ('MetaSel ('Just "sr_sort") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Sort) :*: S1 ('MetaSel ('Just "sr_reft") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Reft)))

Constructing Terms

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

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

conj :: [Pred] -> Pred Source #

conj is a fast version of pAnd needed for the ebind tests

pAnd :: ListNE Pred -> Pred Source #

NOTE: pAnd-SLOW
pAnd and pOr are super slow as they go inside the predicates; so they SHOULD NOT be used inside the solver loop. Instead, use conj which ensures some basic things but is faster.

pOr :: ListNE Pred -> Pred Source #

NOTE: pAnd-SLOW
pAnd and pOr are super slow as they go inside the predicates; so they SHOULD NOT be used inside the solver loop. Instead, use conj which ensures some basic things but is faster.

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

(&.&) :: Pred -> Pred -> Pred infixl 9 Source #

(|.|) :: Pred -> Pred -> Pred infixl 9 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

Methods

expr :: a -> Expr Source #

Instances

Instances details
Expression Symbol Source #

The symbol may be an encoding of a SymConst.

Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

expr :: Symbol -> Expr Source #

Expression Expr Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

expr :: Expr -> Expr Source #

Expression Reft Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

expr :: Reft -> Expr Source #

Expression SortedReft Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

expr :: SortedReft -> Expr Source #

Expression Text Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

expr :: Text -> Expr Source #

Expression Integer Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

expr :: Integer -> Expr Source #

Expression Int Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

expr :: Int -> Expr Source #

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

Defined in Language.Fixpoint.Types.Refinements

Methods

expr :: Located a -> Expr Source #

Expression (Symbol, SortedReft) Source # 
Instance details

Defined in Language.Fixpoint.Types.Substitutions

Methods

expr :: (Symbol, SortedReft) -> Expr Source #

class Predicate a where Source #

Values that can be viewed as Predicates

Methods

prop :: a -> Expr Source #

Instances

Instances details
Predicate Symbol Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

prop :: Symbol -> Expr Source #

Predicate Expr Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

prop :: Expr -> Expr Source #

Predicate Bool Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

prop :: Bool -> Expr Source #

class Subable a where Source #

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

Minimal complete definition

syms, substa, substf, subst

Methods

syms Source #

Arguments

:: a 
-> [Symbol]

free symbols of a

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

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

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

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

Instances

Instances details
Subable Pred Source # 
Instance details

Defined in Language.Fixpoint.Horn.Types

Subable Equation Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Subable Qualifier Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Subable Symbol Source # 
Instance details

Defined in Language.Fixpoint.Types.Substitutions

Subable Expr Source # 
Instance details

Defined in Language.Fixpoint.Types.Substitutions

Subable Reft Source # 
Instance details

Defined in Language.Fixpoint.Types.Substitutions

Subable SortedReft Source # 
Instance details

Defined in Language.Fixpoint.Types.Substitutions

Subable () Source # 
Instance details

Defined in Language.Fixpoint.Types.Substitutions

Methods

syms :: () -> [Symbol] Source #

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

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

subst :: Subst -> () -> () Source #

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

Subable (Bind a) Source # 
Instance details

Defined in Language.Fixpoint.Horn.Types

Methods

syms :: Bind a -> [Symbol] Source #

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

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

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

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

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

Defined in Language.Fixpoint.Types.Refinements

Subable a => Subable (Maybe a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Substitutions

Methods

syms :: Maybe a -> [Symbol] Source #

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

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

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

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

Subable a => Subable [a] Source # 
Instance details

Defined in Language.Fixpoint.Types.Substitutions

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 #

Subable a => Subable (HashMap k a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Substitutions

Methods

syms :: HashMap k a -> [Symbol] Source #

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

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

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

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

(Subable a, Subable b) => Subable (a, b) Source # 
Instance details

Defined in Language.Fixpoint.Types.Substitutions

Methods

syms :: (a, b) -> [Symbol] Source #

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

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

subst :: Subst -> (a, b) -> (a, b) Source #

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

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

Arguments

:: r 
-> [Symbol]

parameters for Reft, vv + others

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 #

eCst :: Expr -> Sort -> Expr Source #

Eliminates redundant casts

Transforming

Gradual Type Manipulation

pGAnds :: [Expr] -> Expr Source #

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

class HasGradual a where Source #

Minimal complete definition

isGradual

Methods

isGradual :: a -> Bool Source #

gVars :: a -> [KVar] Source #

ungrad :: a -> a Source #

Instances

Instances details
HasGradual Expr Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

HasGradual Reft Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

HasGradual SortedReft Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

HasGradual (WfC a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Methods

isGradual :: WfC a -> Bool Source #

gVars :: WfC a -> [KVar] Source #

ungrad :: WfC a -> WfC a Source #

HasGradual (GInfo c a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Methods

isGradual :: GInfo c a -> Bool Source #

gVars :: GInfo c a -> [KVar] Source #

ungrad :: GInfo c a -> GInfo c a Source #

Orphan instances

Fixpoint Doc Source # 
Instance details

Methods

toFix :: Doc -> Doc Source #

simplify :: Doc -> Doc Source #

(Hashable a, Eq a, Binary a) => Binary (HashSet a) Source # 
Instance details

Methods

put :: HashSet a -> Put #

get :: Get (HashSet a) #

putList :: [HashSet a] -> Put #

(Hashable k, Eq k, Binary k, Binary v) => Binary (HashMap k v) Source # 
Instance details

Methods

put :: HashMap k v -> Put #

get :: Get (HashMap k v) #

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