| Safe Haskell | None |
|---|---|
| Language | Haskell98 |
Language.Fixpoint.Types.Refinements
Contents
Description
This module has the types for representing terms in the refinement logic.
Synopsis
- data SymConst = SL !Text
- data Constant
- data Bop
- data Brel
- 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 {}
- 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 {}
- newtype Subst = Su (HashMap Symbol Expr)
- data KVSub = KVS {}
- newtype Reft = Reft (Symbol, Expr)
- data SortedReft = RR {}
- 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
- class Predicate a where
- class Subable a where
- class (Monoid r, Subable r) => Reftable r where
- 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
- srcGradInfo :: SourcePos -> GradInfo
Representing Terms
Expressions ---------------------------------------------------------------
Uninterpreted constants that are embedded as "constant symbol : Str"
Instances
| Eq SymConst Source # | |
| Data SymConst Source # | |
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 :: (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 # | |
Defined in Language.Fixpoint.Types.Refinements | |
| Show SymConst Source # | |
| Generic SymConst Source # | |
| Binary SymConst Source # | |
| NFData SymConst Source # | |
Defined in Language.Fixpoint.Types.Refinements | |
| Hashable SymConst Source # | |
Defined in Language.Fixpoint.Types.Refinements | |
| PPrint SymConst Source # | |
Defined in Language.Fixpoint.Types.Refinements | |
| Fixpoint SymConst Source # | |
| Symbolic SymConst Source # | String Constants ---------------------------------------------------------- Replace all symbol-representations-of-string-literals with string-literal Used to transform parsed output from fixpoint back into fq. |
| SMTLIB2 SymConst Source # | |
| type Rep SymConst Source # | |
Defined in Language.Fixpoint.Types.Refinements | |
Instances
Instances
| Eq Bop Source # | |
| Data Bop Source # | |
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 # dataTypeOf :: Bop -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Bop) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Bop) # gmapT :: (forall b. Data b => b -> b) -> Bop -> Bop # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Bop -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Bop -> r # gmapQ :: (forall d. Data d => d -> u) -> Bop -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Bop -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Bop -> m Bop # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Bop -> m Bop # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Bop -> m Bop # | |
| Ord Bop Source # | |
| Show Bop Source # | |
| Generic Bop Source # | |
| Binary Bop Source # | |
| NFData Bop Source # | |
Defined in Language.Fixpoint.Types.Refinements | |
| Hashable Bop Source # | |
Defined in Language.Fixpoint.Types.Refinements | |
| PPrint Bop Source # | |
Defined in Language.Fixpoint.Types.Refinements | |
| Fixpoint Bop Source # | |
| SMTLIB2 Bop Source # | |
| type Rep Bop Source # | |
Defined in Language.Fixpoint.Types.Refinements type Rep Bop = D1 (MetaData "Bop" "Language.Fixpoint.Types.Refinements" "liquid-fixpoint-0.8.10.2-Ld6PWXA9XrKe3HZnOCc57" 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)))) | |
Instances
| Eq Brel Source # | |
| Data Brel Source # | |
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 # dataTypeOf :: Brel -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Brel) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Brel) # gmapT :: (forall b. Data b => b -> b) -> Brel -> Brel # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Brel -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Brel -> r # gmapQ :: (forall d. Data d => d -> u) -> Brel -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Brel -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Brel -> m Brel # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Brel -> m Brel # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Brel -> m Brel # | |
| Ord Brel Source # | |
| Show Brel Source # | |
| Generic Brel Source # | |
| Binary Brel Source # | |
| NFData Brel Source # | |
Defined in Language.Fixpoint.Types.Refinements | |
| Hashable Brel Source # | |
Defined in Language.Fixpoint.Types.Refinements | |
| PPrint Brel Source # | |
Defined in Language.Fixpoint.Types.Refinements | |
| Fixpoint Brel Source # | |
| SMTLIB2 Brel Source # | |
| type Rep Brel Source # | |
Defined in Language.Fixpoint.Types.Refinements type Rep Brel = D1 (MetaData "Brel" "Language.Fixpoint.Types.Refinements" "liquid-fixpoint-0.8.10.2-Ld6PWXA9XrKe3HZnOCc57" 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)))) | |
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
| Eq GradInfo Source # | |
| Data GradInfo Source # | |
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 :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> GradInfo -> r # gmapQ :: (forall d. Data d => d -> u) -> GradInfo -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> GradInfo -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> GradInfo -> m GradInfo # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> GradInfo -> m GradInfo # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> GradInfo -> m GradInfo # | |
| Show GradInfo Source # | |
| Generic GradInfo Source # | |
| Binary GradInfo Source # | |
| NFData GradInfo Source # | |
Defined in Language.Fixpoint.Types.Refinements | |
| Hashable GradInfo Source # | |
Defined in Language.Fixpoint.Types.Refinements | |
| type Rep GradInfo Source # | |
Defined in Language.Fixpoint.Types.Refinements type Rep GradInfo = D1 (MetaData "GradInfo" "Language.Fixpoint.Types.Refinements" "liquid-fixpoint-0.8.10.2-Ld6PWXA9XrKe3HZnOCc57" 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)))) | |
Kvars ---------------------------------------------------------------------
Instances
| Eq KVar Source # | |
| Data KVar Source # | |
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 # dataTypeOf :: KVar -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c KVar) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c KVar) # gmapT :: (forall b. Data b => b -> b) -> KVar -> KVar # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> KVar -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> KVar -> r # gmapQ :: (forall d. Data d => d -> u) -> KVar -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> KVar -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> KVar -> m KVar # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> KVar -> m KVar # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> KVar -> m KVar # | |
| Ord KVar Source # | |
| Show KVar Source # | |
| IsString KVar Source # | |
Defined in Language.Fixpoint.Types.Refinements Methods fromString :: String -> KVar # | |
| Generic KVar Source # | |
| Binary KVar Source # | |
| NFData KVar Source # | |
Defined in Language.Fixpoint.Types.Refinements | |
| Hashable KVar Source # | |
Defined in Language.Fixpoint.Types.Refinements | |
| PPrint KVar Source # | |
Defined in Language.Fixpoint.Types.Refinements | |
| Fixpoint KVar Source # | |
| Inputable (FixResult Integer, FixSolution) Source # | |
| type Rep KVar Source # | |
Defined in Language.Fixpoint.Types.Refinements | |
Substitutions -------------------------------------------------------------
Instances
| Eq Subst Source # | |
| Data Subst Source # | |
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 # dataTypeOf :: Subst -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Subst) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Subst) # gmapT :: (forall b. Data b => b -> b) -> Subst -> Subst # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Subst -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Subst -> r # gmapQ :: (forall d. Data d => d -> u) -> Subst -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Subst -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Subst -> m Subst # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Subst -> m Subst # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Subst -> m Subst # | |
| Show Subst Source # | |
| Generic Subst Source # | |
| Semigroup Subst Source # | |
| Monoid Subst Source # | |
| Binary Subst Source # | |
| NFData Subst Source # | |
Defined in Language.Fixpoint.Types.Refinements | |
| Hashable Subst Source # | |
Defined in Language.Fixpoint.Types.Refinements | |
| PPrint Subst Source # | |
Defined in Language.Fixpoint.Types.Refinements | |
| Fixpoint Subst Source # | |
| type Rep Subst Source # | |
Defined in Language.Fixpoint.Types.Refinements | |
Instances
| Eq KVSub Source # | |
| Data KVSub Source # | |
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 # dataTypeOf :: KVSub -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c KVSub) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c KVSub) # gmapT :: (forall b. Data b => b -> b) -> KVSub -> KVSub # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> KVSub -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> KVSub -> r # gmapQ :: (forall d. Data d => d -> u) -> KVSub -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> KVSub -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> KVSub -> m KVSub # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> KVSub -> m KVSub # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> KVSub -> m KVSub # | |
| Show KVSub Source # | |
| Generic KVSub Source # | |
| PPrint KVSub Source # | |
Defined in Language.Fixpoint.Types.Refinements | |
| type Rep KVSub Source # | |
Defined in Language.Fixpoint.Types.Refinements type Rep KVSub = D1 (MetaData "KVSub" "Language.Fixpoint.Types.Refinements" "liquid-fixpoint-0.8.10.2-Ld6PWXA9XrKe3HZnOCc57" 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)))) | |
Parsed refinement of Symbol as Expr
e.g. in '{v: _ | e }' v is the Symbol and e the Expr
Instances
data SortedReft Source #
Instances
Constructing Terms
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
Instances
| Expression Int Source # | |
| Expression Integer Source # | |
| Expression Text Source # | |
| Expression Symbol Source # | The symbol may be an encoding of a SymConst. |
| Expression SortedReft Source # | |
Defined in Language.Fixpoint.Types.Refinements Methods expr :: SortedReft -> Expr Source # | |
| Expression Reft Source # | |
| Expression Expr Source # | |
| Expression Bv Source # | Construct an |
| Expression a => Expression (Located a) Source # | |
| Expression (Symbol, SortedReft) Source # | |
Defined in Language.Fixpoint.Types.Substitutions | |
class Predicate a where Source #
Values that can be viewed as Predicates
class Subable a where Source #
Class Predicates for Valid Refinements -----------------------------
Methods
Arguments
| :: a | |
| -> [Symbol] | free symbols of a |
substa :: (Symbol -> Symbol) -> a -> a Source #
substf :: (Symbol -> Expr) -> a -> a Source #
Instances
| Subable () Source # | |
| Subable Symbol Source # | |
| Subable SortedReft Source # | |
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 # | |
| Subable Expr Source # | |
| Subable Equation Source # | |
Defined in Language.Fixpoint.Types.Constraints | |
| Subable Qualifier Source # | |
Defined in Language.Fixpoint.Types.Constraints | |
| Subable Bind Source # | |
| Subable Pred Source # | |
| Subable a => Subable [a] Source # | |
| Subable a => Subable (Maybe a) Source # | |
Defined in Language.Fixpoint.Types.Substitutions | |
| Subable a => Subable (Located a) Source # | |
Defined in Language.Fixpoint.Types.Refinements | |
| (Subable a, Subable b) => Subable (a, b) Source # | |
| Subable a => Subable (HashMap k a) Source # | |
Defined in Language.Fixpoint.Types.Substitutions | |
class (Monoid r, Subable r) => Reftable r where Source #
Instances
| Reftable () Source # | |
| Reftable SortedReft Source # | |
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 # | |
Defined in Language.Fixpoint.Types.Substitutions | |
Constructors
trueSortedReft :: Sort -> SortedReft 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 #
Predicates
isFunctionSortedReft :: SortedReft -> Bool Source #
Refinements ----------------------------------------------
isNonTrivial :: Reftable r => r -> Bool Source #
isContraPred :: Expr -> Bool Source #
isTautoPred :: Expr -> Bool Source #
isSingletonReft :: Reft -> Maybe Expr Source #
Predicates ----------------------------------------------------------------
Destructing
flattenRefas :: [Expr] -> [Expr] Source #
reftConjuncts :: Reft -> [Reft] Source #
Transforming
debruijnIndex :: Expr -> Int Source #
Gradual Type Manipulation
class HasGradual a where Source #
Minimal complete definition
Instances
| HasGradual SortedReft Source # | |
Defined in Language.Fixpoint.Types.Refinements Methods isGradual :: SortedReft -> Bool Source # gVars :: SortedReft -> [KVar] Source # ungrad :: SortedReft -> SortedReft Source # | |
| HasGradual Reft Source # | |
| HasGradual Expr Source # | |
| HasGradual (WfC a) Source # | |
| HasGradual (GInfo c a) Source # | |
srcGradInfo :: SourcePos -> GradInfo Source #