| Safe Haskell | None |
|---|---|
| Language | Haskell98 |
Language.Fixpoint.Types.Refinements
Contents
Description
This module has the types for representing terms in the refinement logic.
- 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
- 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])
- 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 # | |
| Ord SymConst Source # | |
| Show SymConst Source # | |
| Generic SymConst Source # | |
| Binary SymConst Source # | |
| NFData SymConst Source # | |
| Hashable SymConst Source # | |
| PPrint SymConst Source # | |
| Fixpoint SymConst Source # | |
| Symbolic SymConst Source # | String Constants ---------------------------------------------------------- Replace all symbol-representations-of-string-literals with string-literal Used to transform parsed output from fixpoint back into fq. |
| type Rep SymConst Source # | |
Instances
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
Kvars ---------------------------------------------------------------------
Instances
| Eq KVar Source # | |
| Data KVar Source # | |
| Ord KVar Source # | |
| Show KVar Source # | |
| IsString KVar Source # | |
| Generic KVar Source # | |
| Binary KVar Source # | |
| NFData KVar Source # | |
| Hashable KVar Source # | |
| PPrint KVar Source # | |
| Fixpoint KVar Source # | |
| Inputable (FixResult Integer, FixSolution) Source # | |
| type Rep KVar Source # | |
Substitutions -------------------------------------------------------------
Parsed refinement of Symbol as Expr
e.g. in '{v: _ | e }' v is the Symbol and e the Expr
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
Minimal complete definition
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 # | |
| Expression Reft Source # | |
| Expression Expr Source # | |
| Expression Bv Source # | Construct an |
| Expression a => Expression (Located a) Source # | |
class Subable a where Source #
Class Predicates for Valid Refinements -----------------------------
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 # | |
| HasGradual Reft Source # | |
| HasGradual Expr Source # | |
| HasGradual (WfC a) Source # | |
| HasGradual (GInfo c a) Source # | |
srcGradInfo :: SourcePos -> GradInfo Source #