Safe Haskell | None |
---|---|
Language | Haskell98 |
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"
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 |
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 |
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
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