Safe Haskell	None
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

data 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
pAnd :: ListNE Pred -> Pred
pOr :: ListNE Pred -> Pred
pIte :: Pred -> Expr -> Expr -> Expr
(&.&) :: 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]
eApps :: Expr -> [Expr] -> Expr
eAppC :: Sort -> Expr -> Expr -> Expr
splitEApp :: Expr -> (Expr, [Expr])
splitPAnd :: Expr -> [Expr]
reftConjuncts :: Reft -> [Reft]
mapPredReft :: (Expr -> Expr) -> Reft -> Reft
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

data SymConst Source #

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

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

Constructors

SL !Text

Instances

Instances details

Eq SymConst Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods (==) :: SymConst -> SymConst -> Bool # (/=) :: SymConst -> SymConst -> Bool #
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 #
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 #
Show SymConst Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods showsPrec :: Int -> SymConst -> ShowS # show :: SymConst -> String # showList :: [SymConst] -> ShowS #
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 #
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 -> () #
Hashable SymConst Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods hashWithSalt :: Int -> SymConst -> Int hash :: SymConst -> Int
PPrint SymConst Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods pprintTidy :: Tidy -> SymConst -> Doc Source # pprintPrec :: Int -> Tidy -> SymConst -> Doc Source #
Fixpoint SymConst Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods toFix :: SymConst -> Doc Source # simplify :: SymConst -> SymConst Source #
Symbolic SymConst Source #	String Constants ---------------------------------------------------------- Replace all symbol-representations-of-string-literals with string-literal Used to transform parsed output from fixpoint back into fq.
Instance details Defined in Language.Fixpoint.Types.Refinements Methods symbol :: SymConst -> Symbol Source #
SMTLIB2 SymConst Source #
Instance details Defined in Language.Fixpoint.Smt.Serialize Methods smt2 :: SymEnv -> SymConst -> Builder Source #
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.8.10.2-inplace" 'False) (C1 ('MetaCons "SL" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Text)))

data Constant Source #

Constructors

I !Integer
R !Double
L !Text !Sort

Instances

Instances details

Eq Constant Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods (==) :: Constant -> Constant -> Bool # (/=) :: Constant -> Constant -> Bool #
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 #
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 #
Show Constant Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods showsPrec :: Int -> Constant -> ShowS # show :: Constant -> String # showList :: [Constant] -> ShowS #
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 #
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 -> () #
Hashable Constant Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods hashWithSalt :: Int -> Constant -> Int hash :: Constant -> Int
PPrint Constant Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods pprintTidy :: Tidy -> Constant -> Doc Source # pprintPrec :: Int -> Tidy -> Constant -> Doc Source #
Fixpoint Constant Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods toFix :: Constant -> Doc Source # simplify :: Constant -> Constant Source #
SMTLIB2 Constant Source #
Instance details Defined in Language.Fixpoint.Smt.Serialize Methods smt2 :: SymEnv -> Constant -> Builder Source #
Inputable Constant Source #
Instance details Defined in Language.Fixpoint.Parse Methods rr :: String -> Constant Source # rr' :: String -> String -> Constant Source #
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.8.10.2-inplace" '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

Eq Bop Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods (==) :: Bop -> Bop -> Bool # (/=) :: Bop -> Bop -> Bool #
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 #
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 #
Show Bop Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods showsPrec :: Int -> Bop -> ShowS # show :: Bop -> String # showList :: [Bop] -> ShowS #
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 #
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 -> () #
Hashable Bop Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods hashWithSalt :: Int -> Bop -> Int hash :: Bop -> Int
PPrint Bop Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods pprintTidy :: Tidy -> Bop -> Doc Source # pprintPrec :: Int -> Tidy -> Bop -> Doc Source #
Fixpoint Bop Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods toFix :: Bop -> Doc Source # simplify :: Bop -> Bop Source #
SMTLIB2 Bop Source #
Instance details Defined in Language.Fixpoint.Smt.Serialize Methods smt2 :: SymEnv -> Bop -> Builder Source #
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.8.10.2-inplace" '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

Eq Brel Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods (==) :: Brel -> Brel -> Bool # (/=) :: Brel -> Brel -> Bool #
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 #
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 #
Show Brel Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods showsPrec :: Int -> Brel -> ShowS # show :: Brel -> String # showList :: [Brel] -> ShowS #
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 #
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 -> () #
Hashable Brel Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods hashWithSalt :: Int -> Brel -> Int hash :: Brel -> Int
PPrint Brel Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods pprintTidy :: Tidy -> Brel -> Doc Source # pprintPrec :: Int -> Tidy -> Brel -> Doc Source #
Fixpoint Brel Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods toFix :: Brel -> Doc Source # simplify :: Brel -> Brel Source #
SMTLIB2 Brel Source #
Instance details Defined in Language.Fixpoint.Smt.Serialize Methods smt2 :: SymEnv -> Brel -> Builder Source #
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.8.10.2-inplace" '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

Eq Expr Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods (==) :: Expr -> Expr -> Bool # (/=) :: Expr -> Expr -> Bool #
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 #
Show Expr Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods showsPrec :: Int -> Expr -> ShowS # show :: Expr -> String # showList :: [Expr] -> ShowS #
Show GFixSolution Source #
Instance details Defined in Language.Fixpoint.Types.Constraints Methods showsPrec :: Int -> GFixSolution -> ShowS # show :: GFixSolution -> String # showList :: [GFixSolution] -> ShowS #
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 #
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 #
Monoid Expr Source #
Instance details Defined in Language.Fixpoint.Types.Substitutions Methods mempty :: Expr # mappend :: Expr -> Expr -> Expr # mconcat :: [Expr] -> Expr #
Binary Expr Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods put :: Expr -> Put # get :: Get Expr # putList :: [Expr] -> Put #
Binary GFixSolution Source #
Instance details Defined in Language.Fixpoint.Types.Constraints Methods put :: GFixSolution -> Put # get :: Get GFixSolution # putList :: [GFixSolution] -> Put #
NFData Expr Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods rnf :: Expr -> () #
NFData GFixSolution Source #
Instance details Defined in Language.Fixpoint.Types.Constraints Methods rnf :: GFixSolution -> () #
Hashable Expr Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods hashWithSalt :: Int -> Expr -> Int hash :: Expr -> Int
PPrint Expr Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods pprintTidy :: Tidy -> Expr -> Doc Source # pprintPrec :: Int -> Tidy -> Expr -> Doc Source #
PPrint GFixSolution Source #
Instance details Defined in Language.Fixpoint.Types.Constraints Methods pprintTidy :: Tidy -> GFixSolution -> Doc Source # pprintPrec :: Int -> Tidy -> GFixSolution -> Doc Source #
Fixpoint Expr Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods toFix :: Expr -> Doc Source # simplify :: 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 #
Predicate Expr Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods prop :: Expr -> Expr 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 #
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 #
SMTLIB2 Expr Source #
Instance details Defined in Language.Fixpoint.Smt.Serialize Methods smt2 :: SymEnv -> Expr -> Builder Source #
Elaborate Expr Source #
Instance details Defined in Language.Fixpoint.SortCheck Methods elaborate :: Located String -> SymEnv -> Expr -> Expr Source #
Inputable Expr Source #
Instance details Defined in Language.Fixpoint.Parse Methods rr :: String -> Expr Source # rr' :: String -> String -> Expr Source #
Gradual Expr Source #
Instance details Defined in Language.Fixpoint.Types.Graduals Methods gsubst :: GSol -> Expr -> Expr Source #
Defunc Expr Source #
Instance details Defined in Language.Fixpoint.Defunctionalize Methods defunc :: Expr -> DF Expr Source #
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.8.10.2-inplace" '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

Eq GradInfo Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods (==) :: GradInfo -> GradInfo -> Bool # (/=) :: GradInfo -> GradInfo -> Bool #
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 #
Show GradInfo Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods showsPrec :: Int -> GradInfo -> ShowS # show :: GradInfo -> String # showList :: [GradInfo] -> ShowS #
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 #
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 -> () #
Hashable GradInfo Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods hashWithSalt :: Int -> GradInfo -> Int hash :: GradInfo -> Int
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.8.10.2-inplace" '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

Eq KVar Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods (==) :: KVar -> KVar -> Bool # (/=) :: KVar -> KVar -> Bool #
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 #
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 #
Show KVar Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods showsPrec :: Int -> KVar -> ShowS # show :: KVar -> String # showList :: [KVar] -> ShowS #
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 #
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 -> () #
Hashable KVar Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods hashWithSalt :: Int -> KVar -> Int hash :: KVar -> Int
PPrint KVar Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods pprintTidy :: Tidy -> KVar -> Doc Source # pprintPrec :: Int -> Tidy -> KVar -> Doc Source #
Fixpoint KVar Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods toFix :: KVar -> Doc Source # simplify :: KVar -> KVar 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 KVar Source #
Instance details Defined in Language.Fixpoint.Types.Refinements type Rep KVar = D1 ('MetaData "KVar" "Language.Fixpoint.Types.Refinements" "liquid-fixpoint-0.8.10.2-inplace" '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

Eq Subst Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods (==) :: Subst -> Subst -> Bool # (/=) :: Subst -> Subst -> Bool #
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 #
Show Subst Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods showsPrec :: Int -> Subst -> ShowS # show :: Subst -> String # showList :: [Subst] -> ShowS #
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 #
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 #
Monoid Subst Source #
Instance details Defined in Language.Fixpoint.Types.Substitutions Methods mempty :: Subst # mappend :: Subst -> Subst -> Subst # mconcat :: [Subst] -> Subst #
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 -> () #
Hashable Subst Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods hashWithSalt :: Int -> Subst -> Int hash :: Subst -> Int
PPrint Subst Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods pprintTidy :: Tidy -> Subst -> Doc Source # pprintPrec :: Int -> Tidy -> Subst -> Doc Source #
Fixpoint Subst Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods toFix :: Subst -> Doc Source # simplify :: Subst -> Subst Source #
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.8.10.2-inplace" '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

Eq KVSub Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods (==) :: KVSub -> KVSub -> Bool # (/=) :: KVSub -> KVSub -> Bool #
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 #
Show KVSub Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods showsPrec :: Int -> KVSub -> ShowS # show :: KVSub -> String # showList :: [KVSub] -> ShowS #
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 #
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.8.10.2-inplace" '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

Eq Reft Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods (==) :: Reft -> Reft -> Bool # (/=) :: Reft -> Reft -> Bool #
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 #
Show Reft Source #
Instance details Defined in Language.Fixpoint.Types.Substitutions Methods showsPrec :: Int -> Reft -> ShowS # show :: Reft -> String # showList :: [Reft] -> ShowS #
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 #
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 #
Monoid Reft Source #
Instance details Defined in Language.Fixpoint.Types.Substitutions Methods mempty :: Reft # mappend :: Reft -> Reft -> Reft # mconcat :: [Reft] -> Reft #
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 -> () #
Hashable Reft Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods hashWithSalt :: Int -> Reft -> Int hash :: Reft -> Int
PPrint Reft Source #
Instance details Defined in Language.Fixpoint.Types.Substitutions Methods pprintTidy :: Tidy -> Reft -> Doc Source # pprintPrec :: Int -> Tidy -> Reft -> Doc Source #
Fixpoint Reft Source #
Instance details Defined in Language.Fixpoint.Types.Substitutions Methods toFix :: Reft -> Doc Source # simplify :: 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 #
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 #
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 #
Gradual Reft Source #
Instance details Defined in Language.Fixpoint.Types.Graduals Methods gsubst :: GSol -> Reft -> Reft Source #
Defunc Reft Source #
Instance details Defined in Language.Fixpoint.Defunctionalize Methods defunc :: Reft -> DF Reft Source #
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.8.10.2-inplace" '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

Eq SortedReft Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods (==) :: SortedReft -> SortedReft -> Bool # (/=) :: SortedReft -> SortedReft -> Bool #
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 #
Show SortedReft Source #
Instance details Defined in Language.Fixpoint.Types.Substitutions Methods showsPrec :: Int -> SortedReft -> ShowS # show :: SortedReft -> String # showList :: [SortedReft] -> ShowS #
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 #
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 #
Semigroup BindEnv Source #
Instance details Defined in Language.Fixpoint.Types.Environments Methods (<>) :: BindEnv -> BindEnv -> BindEnv # sconcat :: NonEmpty BindEnv -> BindEnv # stimes :: Integral b => b -> BindEnv -> BindEnv #
Monoid SortedReft Source #
Instance details Defined in Language.Fixpoint.Types.Substitutions Methods mempty :: SortedReft # mappend :: SortedReft -> SortedReft -> SortedReft # mconcat :: [SortedReft] -> SortedReft #
Monoid BindEnv Source #
Instance details Defined in Language.Fixpoint.Types.Environments Methods mempty :: BindEnv # mappend :: BindEnv -> BindEnv -> BindEnv # mconcat :: [BindEnv] -> BindEnv #
Binary SortedReft Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods put :: SortedReft -> Put # get :: Get SortedReft # putList :: [SortedReft] -> Put #
Binary BindEnv Source #
Instance details Defined in Language.Fixpoint.Types.Environments Methods put :: BindEnv -> Put # get :: Get BindEnv # putList :: [BindEnv] -> Put #
NFData SortedReft Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods rnf :: SortedReft -> () #
NFData BindEnv Source #
Instance details Defined in Language.Fixpoint.Types.Environments Methods rnf :: BindEnv -> () #
Hashable SortedReft
Instance details Defined in Language.Fixpoint.Types.Constraints Methods hashWithSalt :: Int -> SortedReft -> Int hash :: SortedReft -> Int
PPrint SortedReft Source #
Instance details Defined in Language.Fixpoint.Types.Substitutions Methods pprintTidy :: Tidy -> SortedReft -> Doc Source # pprintPrec :: Int -> Tidy -> SortedReft -> Doc Source #
Fixpoint SortedReft Source #
Instance details Defined in Language.Fixpoint.Types.Substitutions Methods toFix :: SortedReft -> Doc Source # simplify :: SortedReft -> SortedReft Source #
Fixpoint BindEnv Source #
Instance details Defined in Language.Fixpoint.Types.Environments Methods toFix :: BindEnv -> Doc Source # simplify :: BindEnv -> BindEnv 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 #
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 #
SymConsts SortedReft Source #
Instance details Defined in Language.Fixpoint.Types.Visitor Methods symConsts :: SortedReft -> [SymConst] Source #
SymConsts BindEnv Source #
Instance details Defined in Language.Fixpoint.Types.Visitor Methods symConsts :: BindEnv -> [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 #
Visitable BindEnv Source #
Instance details Defined in Language.Fixpoint.Types.Visitor Methods visit :: Monoid a => Visitor a c -> c -> BindEnv -> VisitM a BindEnv Source #
Elaborate SortedReft Source #
Instance details Defined in Language.Fixpoint.SortCheck Methods elaborate :: Located String -> SymEnv -> SortedReft -> SortedReft Source #
Elaborate BindEnv Source #
Instance details Defined in Language.Fixpoint.SortCheck Methods elaborate :: Located String -> SymEnv -> BindEnv -> BindEnv Source #
Gradual SortedReft Source #
Instance details Defined in Language.Fixpoint.Types.Graduals Methods gsubst :: GSol -> SortedReft -> SortedReft Source #
Gradual BindEnv Source #
Instance details Defined in Language.Fixpoint.Types.Graduals Methods gsubst :: GSol -> BindEnv -> BindEnv Source #
Defunc SortedReft Source #
Instance details Defined in Language.Fixpoint.Defunctionalize Methods defunc :: SortedReft -> DF SortedReft Source #
Defunc BindEnv Source #
Instance details Defined in Language.Fixpoint.Defunctionalize Methods defunc :: BindEnv -> DF BindEnv Source #
Expression (Symbol, SortedReft) Source #
Instance details Defined in Language.Fixpoint.Types.Substitutions Methods expr :: (Symbol, SortedReft) -> Expr Source #
Visitable (Symbol, SortedReft) Source #
Instance details Defined in Language.Fixpoint.Types.Visitor Methods visit :: Monoid a => Visitor a c -> c -> (Symbol, SortedReft) -> VisitM a (Symbol, SortedReft) Source #
Defunc (Symbol, SortedReft) Source #
Instance details Defined in Language.Fixpoint.Defunctionalize Methods defunc :: (Symbol, SortedReft) -> DF (Symbol, SortedReft) 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.8.10.2-inplace" '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 #

pAnd :: ListNE Pred -> Pred Source #

pOr :: ListNE Pred -> Pred Source #

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

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

(|.|) :: Pred -> Pred -> Pred 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 Int Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods expr :: Int -> Expr Source #
Expression Integer Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods expr :: Integer -> Expr Source #
Expression Text Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods expr :: Text -> Expr Source #
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 SortedReft Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods expr :: SortedReft -> Expr Source #
Expression Reft Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods expr :: Reft -> Expr Source #
Expression Expr Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods expr :: Expr -> Expr Source #
Expression Bv Source #	Construct an `Expr` using a raw string, e.g. (Bv S32 "#x02000000")
Instance details Defined in Language.Fixpoint.Smt.Bitvector Methods expr :: Bv -> 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 Bool Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods prop :: Bool -> Expr Source #
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 #

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 () 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 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 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 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 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 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 Bind Source #
Instance details Defined in Language.Fixpoint.Horn.Types Methods syms :: Bind -> [Symbol] Source # substa :: (Symbol -> Symbol) -> Bind -> Bind Source # substf :: (Symbol -> Expr) -> Bind -> Bind Source # subst :: Subst -> Bind -> Bind Source # subst1 :: Bind -> (Symbol, Expr) -> Bind Source #
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 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 (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 (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 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 #
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 #

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 () 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 #
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 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 #

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 #

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

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

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

splitPAnd :: Expr -> [Expr] Source #

reftConjuncts :: Reft -> [Reft] Source #

Transforming

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

Binary SrcSpan Source #
Instance details Methods put :: SrcSpan -> Put # get :: Get SrcSpan # putList :: [SrcSpan] -> Put #
NFData SrcSpan Source #
Instance details Methods rnf :: SrcSpan -> () #
PPrint Sort Source #
Instance details Methods pprintTidy :: Tidy -> Sort -> Doc Source # pprintPrec :: Int -> Tidy -> Sort -> Doc Source #
(Eq a, Hashable a, Binary a) => Binary (TCEmb a) Source #
Instance details Methods put :: TCEmb a -> Put # get :: Get (TCEmb a) # putList :: [TCEmb a] -> Put #
PPrint a => PPrint (TCEmb a) Source #
Instance details Methods pprintTidy :: Tidy -> TCEmb a -> Doc Source # pprintPrec :: Int -> Tidy -> TCEmb a -> Doc Source #
(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 #