Safe Haskell	None
Language	Haskell2010

HERMIT.Lemma

Contents

Clause
Lemmas

Synopsis

Clause

data Clause Source

Constructors

Forall [CoreBndr] Clause
Conj Clause Clause
Disj Clause Clause
Impl LemmaName Clause Clause	name for the antecedent when it is in scope
Equiv CoreExpr CoreExpr
CTrue

Instances

Injection Clause LCoreTC
Injection Clause LCore

mkClause :: [CoreBndr] -> CoreExpr -> CoreExpr -> Clause Source

Build a Clause 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. mkClause [] (x. foo x) bar === forall x. foo x = bar x mkClause [] (baz y z) (x. foo x x) === forall x. baz y z x = foo x x mkClause [] (x. foo x) (y. bar y) === forall x. foo x = bar x

mkForall :: [CoreBndr] -> Clause -> Clause Source

forallQs :: Clause -> [CoreBndr] Source

instClause :: MonadCatch m => VarSet -> (Var -> Bool) -> CoreExpr -> Clause -> m Clause Source

Instantiate one of the universally quantified variables in a Clause. 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.

instsClause :: MonadCatch m => VarSet -> [(Var, CoreExpr)] -> Clause -> m Clause Source

Instantiate a set of universally quantified variables in a Clause. It is important that all type variables appear before any value-level variables in the first argument.

discardUniVars :: Clause -> Clause Source

freeVarsClause :: Clause -> VarSet Source

clauseSyntaxEq :: Clause -> Clause -> Bool Source

Syntactic Equality of clauses.

substClause :: Var -> CoreArg -> Clause -> Clause Source

Assumes Var is free in Clause. If not, no substitution will happen, though uniques might be freshened.

substClauses :: [(Var, CoreArg)] -> Clause -> Clause Source

dropBinders :: Clause -> Clause Source

redundantDicts :: Clause -> Clause 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 lemmaC :: Clause lemmaP :: Proven lemmaU :: Used

data Proven Source

Constructors

Proven
Assumed	Assumed by user
BuiltIn	Assumed by library/HERMIT
NotProven

Instances

Enum Proven
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

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.