Safe Haskell	Safe-Inferred
Language	Haskell98

Language.Fixpoint.Types.Refinements

Contents

Representing Terms
Constructing Terms
Generalizing Embedding with Typeclasses
Constructors
Predicates
Destructing
Transforming
Gradual Type Manipulation
Orphan instances

Description

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

Synopsis

newtype SymConst = SL Text
data Constant
- = I !Integer
- | R !Double
- | L !Text !Sort
data Bop
- = Plus
- | Minus
- | Times
- | Div
- | Mod
- | RTimes
- | RDiv
data Brel
- = Eq
- | Ne
- | Gt
- | Ge
- | Lt
- | Le
- | Ueq
- | Une
data Expr
- = ESym !SymConst
- | ECon !Constant
- | EVar !Symbol
- | EApp !Expr !Expr
- | ENeg !Expr
- | EBin !Bop !Expr !Expr
- | EIte !Expr !Expr !Expr
- | ECst !Expr !Sort
- | ELam !(Symbol, Sort) !Expr
- | ETApp !Expr !Sort
- | ETAbs !Expr !Symbol
- | PAnd ![Expr]
- | POr ![Expr]
- | PNot !Expr
- | PImp !Expr !Expr
- | PIff !Expr !Expr
- | PAtom !Brel !Expr !Expr
- | PKVar !KVar !Subst
- | PAll ![(Symbol, Sort)] !Expr
- | PExist ![(Symbol, Sort)] !Expr
- | PGrad !KVar !Subst !GradInfo !Expr
- | ECoerc !Sort !Sort !Expr
type Pred = Expr
data GradInfo = GradInfo {
- gsrc :: SrcSpan
- gused :: Maybe SrcSpan
}
pattern PTrue :: Expr
pattern PTop :: Expr
pattern PFalse :: Expr
pattern EBot :: Expr
pattern ETimes :: Expr -> Expr -> Expr
pattern ERTimes :: Expr -> Expr -> Expr
pattern EDiv :: Expr -> Expr -> Expr
pattern ERDiv :: Expr -> Expr -> Expr
pattern EEq :: Expr -> Expr -> Expr
newtype KVar = KV {
- kv :: Symbol
}
newtype Subst = Su (HashMap Symbol Expr)
data KVSub = KVS {
- ksuVV :: Symbol
- ksuSort :: Sort
- ksuKVar :: KVar
- ksuSubst :: Subst
}
newtype Reft = Reft (Symbol, Expr)
data SortedReft = RR {
- sr_sort :: !Sort
- sr_reft :: !Reft
}
eVar :: Symbolic a => a -> Expr
elit :: Located Symbol -> Sort -> Expr
eProp :: Symbolic a => a -> Expr
conj :: [Pred] -> Pred
pAnd :: ListNE Pred -> Pred
pOr :: ListNE Pred -> Pred
pIte :: Pred -> Expr -> Expr -> Expr
pAndNoDedup :: ListNE Pred -> Pred
(&.&) :: Pred -> Pred -> Pred
(|.|) :: Pred -> Pred -> Pred
pExist :: [(Symbol, Sort)] -> Pred -> Pred
mkEApp :: LocSymbol -> [Expr] -> Expr
mkProp :: Expr -> Pred
intKvar :: Integer -> KVar
vv_ :: Symbol
class Expression a where
- expr :: a -> Expr
class Predicate a where
- prop :: a -> Expr
class Subable a where
- syms :: a -> [Symbol]
- substa :: (Symbol -> Symbol) -> a -> a
- substf :: (Symbol -> Expr) -> a -> a
- subst :: Subst -> a -> a
- subst1 :: a -> (Symbol, Expr) -> a
class (Monoid r, Subable r) => Reftable r where
- isTauto :: r -> Bool
- ppTy :: r -> Doc -> Doc
- top :: r -> r
- bot :: r -> r
- meet :: r -> r -> r
- toReft :: r -> Reft
- ofReft :: Reft -> r
- params :: r -> [Symbol]
reft :: Symbol -> Expr -> Reft
trueSortedReft :: Sort -> SortedReft
trueReft :: Reft
falseReft :: Reft
exprReft :: Expression a => a -> Reft
notExprReft :: Expression a => a -> Reft
uexprReft :: Expression a => a -> Reft
symbolReft :: Symbolic a => a -> Reft
usymbolReft :: Symbolic a => a -> Reft
propReft :: Predicate a => a -> Reft
predReft :: Predicate a => a -> Reft
reftPred :: Reft -> Expr
reftBind :: Reft -> Symbol
isFunctionSortedReft :: SortedReft -> Bool
functionSort :: Sort -> Maybe ([Int], [Sort], Sort)
isNonTrivial :: Reftable r => r -> Bool
isContraPred :: Expr -> Bool
isTautoPred :: Expr -> Bool
isSingletonExpr :: Symbol -> Expr -> Maybe Expr
isSingletonReft :: Reft -> Maybe Expr
isFalse :: Falseable a => a -> Bool
flattenRefas :: [Expr] -> [Expr]
conjuncts :: Expr -> [Expr]
concConjuncts :: Expr -> [Expr]
dropECst :: Expr -> Expr
eApps :: Expr -> [Expr] -> Expr
eAppC :: Sort -> Expr -> Expr -> Expr
eCst :: Expr -> Sort -> Expr
exprKVars :: Expr -> HashMap KVar [Subst]
exprSymbolsSet :: Expr -> HashSet Symbol
splitEApp :: Expr -> (Expr, [Expr])
splitEAppThroughECst :: Expr -> (Expr, [Expr])
splitPAnd :: Expr -> [Expr]
reftConjuncts :: Reft -> [Reft]
sortedReftSymbols :: SortedReft -> HashSet Symbol
substSortInExpr :: (Symbol -> Sort) -> Expr -> Expr
mapPredReft :: (Expr -> Expr) -> Reft -> Reft
onEverySubexpr :: (Expr -> Expr) -> Expr -> Expr
pprintReft :: Tidy -> Reft -> Doc
debruijnIndex :: Expr -> Int
pGAnds :: [Expr] -> Expr
pGAnd :: Expr -> Expr -> Expr
class HasGradual a where
- isGradual :: a -> Bool
- gVars :: a -> [KVar]
- ungrad :: a -> a
srcGradInfo :: SourcePos -> GradInfo

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 Methods showsPrec :: Int -> SymConst -> ShowS # show :: SymConst -> String # showList :: [SymConst] -> ShowS #
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 Methods (==) :: SymConst -> SymConst -> Bool # (/=) :: SymConst -> SymConst -> Bool #
Ord SymConst Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods compare :: SymConst -> SymConst -> Ordering # (<) :: SymConst -> SymConst -> Bool # (<=) :: SymConst -> SymConst -> Bool # (>) :: SymConst -> SymConst -> Bool # (>=) :: SymConst -> SymConst -> Bool # max :: SymConst -> SymConst -> SymConst # min :: SymConst -> SymConst -> SymConst #
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 Methods smt2 :: SymEnv -> SymConst -> Builder 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.
Instance details Defined in Language.Fixpoint.Types.Refinements Methods symbol :: SymConst -> Symbol Source #
Fixpoint SymConst Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods toFix :: SymConst -> Doc Source # simplify :: SymConst -> SymConst Source #
PPrint SymConst Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods pprintTidy :: Tidy -> SymConst -> Doc Source # pprintPrec :: Int -> Tidy -> SymConst -> Doc Source #
Store SymConst Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods size :: Size SymConst # poke :: SymConst -> Poke () # peek :: Peek SymConst #
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 Methods showsPrec :: Int -> Constant -> ShowS # show :: Constant -> String # showList :: [Constant] -> ShowS #
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 Methods (==) :: Constant -> Constant -> Bool # (/=) :: Constant -> Constant -> Bool #
Ord Constant Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods compare :: Constant -> Constant -> Ordering # (<) :: Constant -> Constant -> Bool # (<=) :: Constant -> Constant -> Bool # (>) :: Constant -> Constant -> Bool # (>=) :: Constant -> Constant -> Bool # max :: Constant -> Constant -> Constant # min :: Constant -> Constant -> Constant #
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 Methods rr :: String -> Constant Source # rr' :: String -> String -> Constant Source #
SMTLIB2 Constant Source #
Instance details Defined in Language.Fixpoint.Smt.Serialize Methods smt2 :: SymEnv -> Constant -> Builder Source #
Fixpoint Constant Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods toFix :: Constant -> Doc Source # simplify :: Constant -> Constant Source #
PPrint Constant Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods pprintTidy :: Tidy -> Constant -> Doc Source # pprintPrec :: Int -> Tidy -> Constant -> Doc Source #
Store Constant Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods size :: Size Constant # poke :: Constant -> Poke () # peek :: Peek Constant #
type Rep Constant Source #
Instance details Defined in Language.Fixpoint.Types.Refinements type Rep Constant = D1 ('MetaData "Constant" "Language.Fixpoint.Types.Refinements" "liquid-fixpoint-0.9.2.5-8VOJ4a5jXPy7nyhLFTxkOW" 'False) (C1 ('MetaCons "I" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Integer)) :+: (C1 ('MetaCons "R" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Double)) :+: C1 ('MetaCons "L" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Text) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Sort))))

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 Methods toFix :: Brel -> Doc Source # simplify :: Brel -> Brel Source #
PPrint Brel Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods pprintTidy :: Tidy -> Brel -> Doc Source # pprintPrec :: Int -> Tidy -> Brel -> Doc Source #
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 #

Constructors

ESym !SymConst
ECon !Constant
EVar !Symbol
EApp !Expr !Expr
ENeg !Expr
EBin !Bop !Expr !Expr
EIte !Expr !Expr !Expr
ECst !Expr !Sort
ELam !(Symbol, Sort) !Expr
ETApp !Expr !Sort
ETAbs !Expr !Symbol
PAnd ![Expr]
POr ![Expr]
PNot !Expr
PImp !Expr !Expr
PIff !Expr !Expr
PAtom !Brel !Expr !Expr
PKVar !KVar !Subst
PAll ![(Symbol, Sort)] !Expr
PExist ![(Symbol, Sort)] !Expr
PGrad !KVar !Subst !GradInfo !Expr
ECoerc !Sort !Sort !Expr

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 Methods showsPrec :: Int -> GFixSolution -> ShowS # show :: GFixSolution -> String # showList :: [GFixSolution] -> ShowS #
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 Methods elaborate :: Located String -> SymEnv -> Expr -> Expr Source #
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 Methods toFix :: Expr -> Doc Source # simplify :: Expr -> Expr Source #
PPrint GFixSolution Source #
Instance details Defined in Language.Fixpoint.Types.Constraints Methods pprintTidy :: Tidy -> GFixSolution -> Doc Source # pprintPrec :: Int -> Tidy -> GFixSolution -> Doc Source #
PPrint Expr Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods pprintTidy :: Tidy -> Expr -> Doc Source # pprintPrec :: Int -> Tidy -> Expr -> Doc Source #
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 Methods isGradual :: Expr -> Bool Source # gVars :: Expr -> [KVar] Source # ungrad :: Expr -> Expr Source #
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 Methods syms :: Expr -> [Symbol] Source # substa :: (Symbol -> Symbol) -> Expr -> Expr Source # substf :: (Symbol -> Expr) -> Expr -> Expr Source # subst :: Subst -> Expr -> Expr Source # subst1 :: Expr -> (Symbol, Expr) -> Expr Source #
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 Methods size :: Size GFixSolution # poke :: GFixSolution -> Poke () # peek :: Peek GFixSolution #
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 Methods smt2 :: SymEnv -> Triggered Expr -> Builder Source #
Inputable (FixResult Integer, FixSolution) Source #
Instance details Defined in Language.Fixpoint.Parse Methods rr :: String -> (FixResult Integer, FixSolution) Source # rr' :: String -> String -> (FixResult Integer, FixSolution) Source #
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 gsrc :: SrcSpan gused :: Maybe SrcSpan

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 Methods showsPrec :: Int -> GradInfo -> ShowS # show :: GradInfo -> String # showList :: [GradInfo] -> ShowS #
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 Methods (==) :: GradInfo -> GradInfo -> Bool # (/=) :: GradInfo -> GradInfo -> Bool #
Ord GradInfo Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods compare :: GradInfo -> GradInfo -> Ordering # (<) :: GradInfo -> GradInfo -> Bool # (<=) :: GradInfo -> GradInfo -> Bool # (>) :: GradInfo -> GradInfo -> Bool # (>=) :: GradInfo -> GradInfo -> Bool # max :: GradInfo -> GradInfo -> GradInfo # min :: GradInfo -> GradInfo -> GradInfo #
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 Methods size :: Size GradInfo # poke :: GradInfo -> Poke () # peek :: Peek GradInfo #
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 kv :: Symbol

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 Methods toFix :: KVar -> Doc Source # simplify :: KVar -> KVar Source #
PPrint KVar Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods pprintTidy :: Tidy -> KVar -> Doc Source # pprintPrec :: Int -> Tidy -> KVar -> Doc Source #
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 Methods rr :: String -> (FixResult Integer, FixSolution) Source # rr' :: String -> String -> (FixResult Integer, FixSolution) Source #
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 Methods toFix :: Subst -> Doc Source # simplify :: Subst -> Subst Source #
PPrint Subst Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods pprintTidy :: Tidy -> Subst -> Doc Source # pprintPrec :: Int -> Tidy -> Subst -> Doc Source #
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
Fields ksuVV :: Symbol ksuSort :: Sort ksuKVar :: KVar ksuSubst :: Subst

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 Methods pprintTidy :: Tidy -> KVSub -> Doc Source # pprintPrec :: Int -> Tidy -> KVSub -> Doc Source #
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 Methods toFix :: Reft -> Doc Source # simplify :: Reft -> Reft Source #
PPrint Reft Source #
Instance details Defined in Language.Fixpoint.Types.Substitutions Methods pprintTidy :: Tidy -> Reft -> Doc Source # pprintPrec :: Int -> Tidy -> Reft -> Doc Source #
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 Methods isGradual :: Reft -> Bool Source # gVars :: Reft -> [KVar] Source # ungrad :: Reft -> Reft Source #
Reftable Reft Source #
Instance details Defined in Language.Fixpoint.Types.Substitutions Methods isTauto :: Reft -> Bool Source # ppTy :: Reft -> Doc -> Doc Source # top :: Reft -> Reft Source # bot :: Reft -> Reft Source # meet :: Reft -> Reft -> Reft Source # toReft :: Reft -> Reft Source # ofReft :: Reft -> Reft Source # params :: Reft -> [Symbol] Source #
Subable Reft Source #
Instance details Defined in Language.Fixpoint.Types.Substitutions Methods syms :: Reft -> [Symbol] Source # substa :: (Symbol -> Symbol) -> Reft -> Reft Source # substf :: (Symbol -> Expr) -> Reft -> Reft Source # subst :: Subst -> Reft -> Reft Source # subst1 :: Reft -> (Symbol, Expr) -> Reft Source #
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 sr_sort :: !Sort sr_reft :: !Reft

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 Methods mempty :: SortedReft # mappend :: SortedReft -> SortedReft -> SortedReft # mconcat :: [SortedReft] -> SortedReft #
Semigroup SortedReft Source #
Instance details Defined in Language.Fixpoint.Types.Substitutions Methods (<>) :: SortedReft -> SortedReft -> SortedReft # sconcat :: NonEmpty SortedReft -> SortedReft # stimes :: Integral b => b -> SortedReft -> SortedReft #
Generic SortedReft Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Associated Types type Rep SortedReft :: Type -> Type # Methods from :: SortedReft -> Rep SortedReft x # to :: Rep SortedReft x -> SortedReft #
Show SortedReft Source #
Instance details Defined in Language.Fixpoint.Types.Substitutions Methods showsPrec :: Int -> SortedReft -> ShowS # show :: SortedReft -> String # showList :: [SortedReft] -> ShowS #
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 Methods (==) :: SortedReft -> SortedReft -> Bool # (/=) :: SortedReft -> SortedReft -> Bool #
Ord SortedReft Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods compare :: SortedReft -> SortedReft -> Ordering # (<) :: SortedReft -> SortedReft -> Bool # (<=) :: SortedReft -> SortedReft -> Bool # (>) :: SortedReft -> SortedReft -> Bool # (>=) :: SortedReft -> SortedReft -> Bool # max :: SortedReft -> SortedReft -> SortedReft # min :: SortedReft -> SortedReft -> SortedReft #
Hashable SortedReft Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods hashWithSalt :: Int -> SortedReft -> Int # hash :: SortedReft -> Int #
Defunc SortedReft Source #
Instance details Defined in Language.Fixpoint.Defunctionalize Methods defunc :: SortedReft -> DF SortedReft Source #
Elaborate SortedReft Source #
Instance details Defined in Language.Fixpoint.SortCheck Methods elaborate :: Located String -> SymEnv -> SortedReft -> SortedReft Source #
Gradual SortedReft Source #
Instance details Defined in Language.Fixpoint.Types.Graduals Methods gsubst :: GSol -> SortedReft -> SortedReft Source #
Fixpoint SortedReft Source #
Instance details Defined in Language.Fixpoint.Types.Substitutions Methods toFix :: SortedReft -> Doc Source # simplify :: SortedReft -> SortedReft Source #
PPrint SortedReft Source #
Instance details Defined in Language.Fixpoint.Types.Substitutions Methods pprintTidy :: Tidy -> SortedReft -> Doc Source # pprintPrec :: Int -> Tidy -> SortedReft -> Doc Source #
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 Methods isGradual :: SortedReft -> Bool Source # gVars :: SortedReft -> [KVar] Source # ungrad :: SortedReft -> SortedReft Source #
Reftable SortedReft Source #
Instance details Defined in Language.Fixpoint.Types.Substitutions Methods isTauto :: SortedReft -> Bool Source # ppTy :: SortedReft -> Doc -> Doc Source # top :: SortedReft -> SortedReft Source # bot :: SortedReft -> SortedReft Source # meet :: SortedReft -> SortedReft -> SortedReft Source # toReft :: SortedReft -> Reft Source # ofReft :: Reft -> SortedReft Source # params :: SortedReft -> [Symbol] Source #
Subable SortedReft Source #
Instance details Defined in Language.Fixpoint.Types.Substitutions Methods syms :: SortedReft -> [Symbol] Source # substa :: (Symbol -> Symbol) -> SortedReft -> SortedReft Source # substf :: (Symbol -> Expr) -> SortedReft -> SortedReft Source # subst :: Subst -> SortedReft -> SortedReft Source # subst1 :: SortedReft -> (Symbol, Expr) -> SortedReft Source #
SymConsts SortedReft Source #
Instance details Defined in Language.Fixpoint.Types.Visitor Methods symConsts :: SortedReft -> [SymConst] Source #
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 Methods size :: Size SortedReft # poke :: SortedReft -> Poke () # peek :: Peek SortedReft #
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 Methods elaborate :: Located String -> SymEnv -> BindEnv a -> BindEnv a Source #
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 Methods toFix :: BindEnv a -> Doc Source # simplify :: BindEnv a -> BindEnv a Source #
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 Methods defunc :: (Symbol, SortedReft) -> DF (Symbol, SortedReft) Source #
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 #

elit :: Located Symbol -> Sort -> 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 #

pAndNoDedup :: ListNE Pred -> Pred Source #

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

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

pExist :: [(Symbol, Sort)] -> Pred -> Pred Source #

mkEApp :: LocSymbol -> [Expr] -> Expr Source #

mkProp :: Expr -> Pred Source #

intKvar :: Integer -> KVar Source #

vv_ :: Symbol 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 Methods syms :: Pred -> [Symbol] Source # substa :: (Symbol -> Symbol) -> Pred -> Pred Source # substf :: (Symbol -> Expr) -> Pred -> Pred Source # subst :: Subst -> Pred -> Pred Source # subst1 :: Pred -> (Symbol, Expr) -> Pred Source #
Subable Equation Source #
Instance details Defined in Language.Fixpoint.Types.Constraints Methods syms :: Equation -> [Symbol] Source # substa :: (Symbol -> Symbol) -> Equation -> Equation Source # substf :: (Symbol -> Expr) -> Equation -> Equation Source # subst :: Subst -> Equation -> Equation Source # subst1 :: Equation -> (Symbol, Expr) -> Equation Source #
Subable Qualifier Source #
Instance details Defined in Language.Fixpoint.Types.Constraints Methods syms :: Qualifier -> [Symbol] Source # substa :: (Symbol -> Symbol) -> Qualifier -> Qualifier Source # substf :: (Symbol -> Expr) -> Qualifier -> Qualifier Source # subst :: Subst -> Qualifier -> Qualifier Source # subst1 :: Qualifier -> (Symbol, Expr) -> Qualifier Source #
Subable Symbol Source #
Instance details Defined in Language.Fixpoint.Types.Substitutions Methods syms :: Symbol -> [Symbol] Source # substa :: (Symbol -> Symbol) -> Symbol -> Symbol Source # substf :: (Symbol -> Expr) -> Symbol -> Symbol Source # subst :: Subst -> Symbol -> Symbol Source # subst1 :: Symbol -> (Symbol, Expr) -> Symbol Source #
Subable Expr Source #
Instance details Defined in Language.Fixpoint.Types.Substitutions Methods syms :: Expr -> [Symbol] Source # substa :: (Symbol -> Symbol) -> Expr -> Expr Source # substf :: (Symbol -> Expr) -> Expr -> Expr Source # subst :: Subst -> Expr -> Expr Source # subst1 :: Expr -> (Symbol, Expr) -> Expr Source #
Subable Reft Source #
Instance details Defined in Language.Fixpoint.Types.Substitutions Methods syms :: Reft -> [Symbol] Source # substa :: (Symbol -> Symbol) -> Reft -> Reft Source # substf :: (Symbol -> Expr) -> Reft -> Reft Source # subst :: Subst -> Reft -> Reft Source # subst1 :: Reft -> (Symbol, Expr) -> Reft Source #
Subable SortedReft Source #
Instance details Defined in Language.Fixpoint.Types.Substitutions Methods syms :: SortedReft -> [Symbol] Source # substa :: (Symbol -> Symbol) -> SortedReft -> SortedReft Source # substf :: (Symbol -> Expr) -> SortedReft -> SortedReft Source # subst :: Subst -> SortedReft -> SortedReft Source # subst1 :: SortedReft -> (Symbol, Expr) -> SortedReft Source #
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 Methods syms :: Located a -> [Symbol] Source # substa :: (Symbol -> Symbol) -> Located a -> Located a Source # substf :: (Symbol -> Expr) -> Located a -> Located a Source # subst :: Subst -> Located a -> Located a Source # subst1 :: Located a -> (Symbol, Expr) -> Located a Source #
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

Instances

Instances details

Reftable Reft Source #
Instance details Defined in Language.Fixpoint.Types.Substitutions Methods isTauto :: Reft -> Bool Source # ppTy :: Reft -> Doc -> Doc Source # top :: Reft -> Reft Source # bot :: Reft -> Reft Source # meet :: Reft -> Reft -> Reft Source # toReft :: Reft -> Reft Source # ofReft :: Reft -> Reft Source # params :: Reft -> [Symbol] Source #
Reftable SortedReft Source #
Instance details Defined in Language.Fixpoint.Types.Substitutions Methods isTauto :: SortedReft -> Bool Source # ppTy :: SortedReft -> Doc -> Doc Source # top :: SortedReft -> SortedReft Source # bot :: SortedReft -> SortedReft Source # meet :: SortedReft -> SortedReft -> SortedReft Source # toReft :: SortedReft -> Reft Source # ofReft :: Reft -> SortedReft Source # params :: SortedReft -> [Symbol] Source #
Reftable () Source #
Instance details Defined in Language.Fixpoint.Types.Substitutions Methods isTauto :: () -> Bool Source # ppTy :: () -> Doc -> Doc Source # top :: () -> () Source # bot :: () -> () Source # meet :: () -> () -> () Source # toReft :: () -> Reft Source # ofReft :: Reft -> () Source # params :: () -> [Symbol] Source #

Constructors

reft :: Symbol -> Expr -> Reft Source #

trueSortedReft :: Sort -> SortedReft Source #

trueReft :: Reft Source #

falseReft :: Reft Source #

exprReft :: Expression a => a -> Reft Source #

notExprReft :: Expression a => a -> Reft Source #

uexprReft :: Expression a => a -> Reft Source #

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

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

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

propReft :: Predicate a => a -> Reft Source #

predReft :: Predicate a => a -> Reft Source #

reftPred :: Reft -> Expr Source #

reftBind :: Reft -> Symbol Source #

Predicates

isFunctionSortedReft :: SortedReft -> Bool Source #

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

functionSort :: Sort -> Maybe ([Int], [Sort], Sort) Source #

isNonTrivial :: Reftable r => r -> Bool Source #

isContraPred :: Expr -> Bool Source #

isTautoPred :: Expr -> Bool Source #

isSingletonExpr :: Symbol -> Expr -> Maybe Expr Source #

isSingletonReft :: Reft -> Maybe Expr Source #

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

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

Destructing

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

conjuncts :: Expr -> [Expr] Source #

concConjuncts :: Expr -> [Expr] Source #

dropECst :: Expr -> Expr Source #

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

eAppC :: Sort -> Expr -> Expr -> Expr Source #

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

Eliminates redundant casts

exprKVars :: Expr -> HashMap KVar [Subst] Source #

exprSymbolsSet :: Expr -> HashSet Symbol Source #

splitEApp :: Expr -> (Expr, [Expr]) Source #

splitEAppThroughECst :: Expr -> (Expr, [Expr]) Source #

splitPAnd :: Expr -> [Expr] Source #

reftConjuncts :: Reft -> [Reft] Source #

sortedReftSymbols :: SortedReft -> HashSet Symbol Source #

substSortInExpr :: (Symbol -> Sort) -> Expr -> Expr Source #

Transforming

mapPredReft :: (Expr -> Expr) -> Reft -> Reft Source #

onEverySubexpr :: (Expr -> Expr) -> Expr -> Expr Source #

pprintReft :: Tidy -> Reft -> Doc Source #

debruijnIndex :: Expr -> Int Source #

Gradual Type Manipulation

pGAnds :: [Expr] -> Expr Source #

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

pGAnd :: Expr -> Expr -> Expr Source #

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 Methods isGradual :: Expr -> Bool Source # gVars :: Expr -> [KVar] Source # ungrad :: Expr -> Expr Source #
HasGradual Reft Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods isGradual :: Reft -> Bool Source # gVars :: Reft -> [KVar] Source # ungrad :: Reft -> Reft Source #
HasGradual SortedReft Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods isGradual :: SortedReft -> Bool Source # gVars :: SortedReft -> [KVar] Source # ungrad :: SortedReft -> SortedReft Source #
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 #

srcGradInfo :: SourcePos -> GradInfo 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 #