| Safe Haskell | None |
|---|---|
| Language | Haskell98 |
Language.Fixpoint.Types.Refinements
Contents
Description
This module contains the data types for representing terms in the
refinement logic; currently split into Expr and Pred but which
will be unified.
- 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
- type Pred = Expr
- pattern PTrue :: Expr
- pattern PTop :: Expr
- pattern PFalse :: Expr
- pattern EBot :: Expr
- newtype KVar = KV {}
- newtype Subst = Su (HashMap Symbol Expr)
- 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 Expr -> Expr
- pOr :: ListNE Expr -> Expr
- pIte :: Expr -> Expr -> Expr -> Expr
- mkEApp :: LocSymbol -> [Expr] -> Expr
- 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
- isTautoPred :: Expr -> Bool
- isSingletonReft :: Reft -> Maybe Expr
- isEVar :: Expr -> Bool
- isFalse :: Falseable a => a -> Bool
- flattenRefas :: [Expr] -> [Expr]
- conjuncts :: Expr -> [Expr]
- eApps :: Expr -> [Expr] -> Expr
- splitEApp :: Expr -> (Expr, [Expr])
- reftConjuncts :: Reft -> [Reft]
- mapPredReft :: (Expr -> Expr) -> Reft -> Reft
- pprintReft :: Tidy -> Reft -> Doc
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 |
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 |
Instances
Kvars ---------------------------------------------------------------------
Substitutions -------------------------------------------------------------
data SortedReft Source
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 Expr Source | |
| Expression Bv Source | Construct an |
| Expression a => Expression (Located a) 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
isTautoPred :: Expr -> Bool Source
isSingletonReft :: Reft -> Maybe Expr Source
Predicates ----------------------------------------------------------------
Destructing
flattenRefas :: [Expr] -> [Expr] Source
reftConjuncts :: Reft -> [Reft] Source
Transforming
pprintReft :: Tidy -> Reft -> Doc Source