Safe Haskell | None |
---|---|
Language | Haskell2010 |
- data Quantified = Quantified [CoreBndr] Clause
- mkQuantified :: [CoreBndr] -> CoreExpr -> CoreExpr -> Quantified
- data Clause
- instQuantified :: MonadCatch m => VarSet -> (Var -> Bool) -> CoreExpr -> Quantified -> m Quantified
- instsQuantified :: MonadCatch m => VarSet -> [(Var, CoreExpr)] -> Quantified -> m Quantified
- discardUniVars :: Quantified -> Quantified
- freeVarsQuantified :: Quantified -> VarSet
- clauseSyntaxEq :: Clause -> Clause -> Bool
- quantifiedSyntaxEq :: Quantified -> Quantified -> Bool
- substQuantified :: Var -> CoreArg -> Quantified -> Quantified
- substQuantifieds :: [(Var, CoreArg)] -> Quantified -> Quantified
- dropBinders :: Quantified -> Quantified
- redundantDicts :: Quantified -> Quantified
- newtype LemmaName = LemmaName String
- data Lemma = Lemma {}
- data Proven
- andP :: Proven -> Proven -> Proven
- orP :: Proven -> Proven -> Proven
- data Used
- type Lemmas = Map LemmaName Lemma
- type NamedLemma = (LemmaName, Lemma)
Quantified
data Quantified Source
mkQuantified :: [CoreBndr] -> CoreExpr -> CoreExpr -> Quantified Source
Build a Quantified from a list of universally quantified binders and two expressions. If the head of either expression is a lambda expression, it's binder will become a universally quantified binder over both sides. It is assumed the two expressions have the same type.
Ex. mkQuantified [] (x. foo x) bar === forall x. foo x = bar x mkQuantified [] (baz y z) (x. foo x x) === forall x. baz y z x = foo x x mkQuantified [] (x. foo x) (y. bar y) === forall x. foo x = bar x
instQuantified :: MonadCatch m => VarSet -> (Var -> Bool) -> CoreExpr -> Quantified -> m Quantified Source
Instantiate one of the universally quantified variables in a Quantified
.
Note: assumes implicit ordering of variables, such that substitution happens to the right
as it does in case alternatives. Only first variable that matches predicate is
instantiated.
instsQuantified :: MonadCatch m => VarSet -> [(Var, CoreExpr)] -> Quantified -> m Quantified Source
Instantiate a set of universally quantified variables in a Quantified
.
It is important that all type variables appear before any value-level variables in the first argument.
clauseSyntaxEq :: Clause -> Clause -> Bool Source
Syntactic Equality of clauses.
quantifiedSyntaxEq :: Quantified -> Quantified -> Bool Source
Syntactic Equality of quantifiers.
substQuantified :: Var -> CoreArg -> Quantified -> Quantified Source
Assumes Var is free in Quantified. If not, no substitution will happen, though uniques might be freshened.
substQuantifieds :: [(Var, CoreArg)] -> Quantified -> Quantified Source
Lemmas
A name for lemmas. Use a newtype so we can tab-complete in shell.
An equality with a proven/used status.
Obligation | this MUST be proven immediately |
UnsafeUsed | used, but can be proven later (only introduced in unsafe shell) |
NotUsed | not used |
type NamedLemma = (LemmaName, Lemma) Source
A LemmaName, Lemma pair.