HERMIT.Dictionary.Reasoning

Equational Reasoning

externals :: [External]

type EqualityProof c m = (Rewrite c m CoreExpr, Rewrite c m CoreExpr)

flipEquality :: Equality -> Equality

Flip the LHS and RHS of a Equality.

eqLhsIntroR :: Equality -> Rewrite c HermitM Core

e ==> let v = lhs in e

eqRhsIntroR :: Equality -> Rewrite c HermitM Core

e ==> let v = rhs in e

birewrite :: (AddBindings c, ExtendPath c Crumb, HasEmptyContext c, ReadBindings c, ReadPath c Crumb, MonadCatch m, MonadUnique m) => Equality -> BiRewrite c m CoreExpr

Create a BiRewrite from a Equality.

The high level idea: create a temporary function with two definitions. Fold one of the defintions, then immediately unfold the other.

extensionalityR :: Maybe String -> Rewrite c HermitM Equality

f == g ==> forall x. f x == g x

getLemmasT :: HasLemmas m => Transform c m x Lemmas

getLemmaByNameT :: (HasLemmas m, Monad m) => LemmaName -> Transform c m x Lemma

insertLemmaR :: (HasLemmas m, Monad m) => LemmaName -> Lemma -> Rewrite c m a

lemmaR :: LemmaName -> BiRewriteH CoreExpr

markLemmaUsedR :: (HasLemmas m, Monad m) => LemmaName -> Rewrite c m a

modifyLemmaR

Arguments

:: (HasLemmas m, Monad m)

=> LemmaName

-> (LemmaName -> LemmaName)

modify lemma name

-> Rewrite c m Equality

rewrite the equality

-> (Bool -> Bool)

modify proven status

-> (Bool -> Bool)

modify used status

-> Rewrite c m a

Lifting transformations over Equality

lhsT :: (AddBindings c, Monad m, ReadPath c Crumb) => Transform c m CoreExpr b -> Transform c m Equality b

Lift a transformation over CoreExpr into a transformation over the left-hand side of a Equality.

rhsT :: (AddBindings c, Monad m, ReadPath c Crumb) => Transform c m CoreExpr b -> Transform c m Equality b

Lift a transformation over CoreExpr into a transformation over the right-hand side of a Equality.

bothT :: (AddBindings c, Monad m, ReadPath c Crumb) => Transform c m CoreExpr b -> Transform c m Equality (b, b)

Lift a transformation over CoreExpr into a transformation over both sides of a Equality.

forallVarsT :: Monad m => Transform c m [Var] b -> Transform c m Equality b

Lift a transformation over '[Var]' into a transformation over the universally quantified variables of a Equality.

lhsR :: (AddBindings c, Monad m, ReadPath c Crumb) => Rewrite c m CoreExpr -> Rewrite c m Equality

Lift a rewrite over CoreExpr into a rewrite over the left-hand side of a Equality.

rhsR :: (AddBindings c, Monad m, ReadPath c Crumb) => Rewrite c m CoreExpr -> Rewrite c m Equality

Lift a rewrite over CoreExpr into a rewrite over the right-hand side of a Equality.

bothR :: (AddBindings c, MonadCatch m, ReadPath c Crumb) => Rewrite c m CoreExpr -> Rewrite c m Equality

Lift a rewrite over CoreExpr into a rewrite over both sides of a Equality.

ppEqualityT :: PrettyPrinter -> TransformH Equality DocH

proveEqualityT :: forall c m. (AddBindings c, Monad m, ReadPath c Crumb) => EqualityProof c m -> Transform c m Equality ()

Verify that a Equality holds, by applying a rewrite to each side, and checking that the results are equal.

verifyEqualityT :: Monad m => Transform c m Equality ()

Verify that the left- and right-hand sides of a Equality are alpha equivalent.

verifyEqualityLeftToRightT :: MonadCatch m => CoreExpr -> CoreExpr -> Rewrite c m CoreExpr -> Transform c m a ()

Given two expressions, and a rewrite from the former to the latter, verify that rewrite.

verifyEqualityCommonTargetT :: MonadCatch m => CoreExpr -> CoreExpr -> EqualityProof c m -> Transform c m a ()

Given two expressions, and a rewrite to apply to each, verify that the resulting expressions are equal.

verifyIsomorphismT :: CoreExpr -> CoreExpr -> Rewrite c HermitM CoreExpr -> Rewrite c HermitM CoreExpr -> Transform c HermitM a ()

Given f :: X -> Y and g :: Y -> X, verify that f (g y) ==> y and g (f x) ==> x.

verifyRetractionT :: CoreExpr -> CoreExpr -> Rewrite c HermitM CoreExpr -> Transform c HermitM a ()

Given f :: X -> Y and g :: Y -> X, verify that f (g y) ==> y.

retractionBR :: forall c. Maybe (Rewrite c HermitM CoreExpr) -> CoreExpr -> CoreExpr -> BiRewrite c HermitM CoreExpr

Given f :: X -> Y and g :: Y -> X, and a proof that f (g y) ==> y, then f (g y) == y.

alphaEqualityR :: (Var -> Bool) -> (String -> String) -> RewriteH Equality

unshadowEqualityR :: RewriteH Equality

instantiateDictsR :: RewriteH Equality

instantiateEquality :: MonadIO m => [(Var, CoreExpr, [Var])] -> Equality -> m Equality

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

instantiateEqualityVar :: MonadIO m => (Var -> Bool) -> CoreExpr -> [Var] -> Equality -> m Equality

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

instantiateEqualityVarR :: (Var -> Bool) -> CoreString -> RewriteH Equality

discardUniVars :: Equality -> Equality