Safe Haskell	None
Language	Haskell2010

HERMIT.Lemma

Contents

Quantified
Lemmas

Synopsis

Quantified

data Quantified Source

Constructors

Quantified [CoreBndr] Clause

Instances

Injection Quantified LCoreTC
Injection Quantified LCore

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

data Clause Source

Constructors

Conj Quantified Quantified
Disj Quantified Quantified
Impl Quantified Quantified
Equiv CoreExpr CoreExpr

Instances

Injection Clause LCoreTC
Injection Clause LCore

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.

discardUniVars :: Quantified -> Quantified Source

freeVarsQuantified :: Quantified -> VarSet Source

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

dropBinders :: Quantified -> Quantified Source

redundantDicts :: Quantified -> Quantified Source

Lemmas

newtype LemmaName Source

A name for lemmas. Use a newtype so we can tab-complete in shell.

Constructors

LemmaName String

Instances

Eq LemmaName
Ord LemmaName
Show LemmaName
IsString LemmaName
Monoid LemmaName
Extern LemmaName
Typeable * LemmaName
type Box LemmaName = LemmaName

data Lemma Source

An equality with a proven/used status.

Constructors

Lemma
Fields lemmaQ :: Quantified lemmaP :: Proven lemmaU :: Used lemmaT :: Bool

data Proven Source

Constructors

Proven
Assumed Bool	True = assumed by user, False = assumed by library/HERMIT for good reason
NotProven

Instances

Eq Proven
Ord Proven
Show Proven
Typeable * Proven

andP :: Proven -> Proven -> Proven Source

orP :: Proven -> Proven -> Proven Source

data Used Source

Constructors

Obligation	this MUST be proven immediately
UnsafeUsed	used, but can be proven later (only introduced in unsafe shell)
NotUsed	not used

Instances

Eq Used
Show Used
Typeable * Used

type Lemmas = Map LemmaName Lemma Source

A collection of named lemmas.

type NamedLemma = (LemmaName, Lemma) Source

A LemmaName, Lemma pair.