HERMIT.Dictionary.Reasoning

Equational Reasoning

externals :: [External]

data CoreExprEquality

An equality is represented as a set of universally quantified binders, and then the LHS and RHS of the equality.

Constructors

CoreExprEquality [CoreBndr] CoreExpr CoreExpr

Instances

Extern (RewriteH CoreExprEquality)

Extern (TransformH CoreExprEquality String)

type Box (RewriteH CoreExprEquality) = RewriteCoreExprEqualityBox

type Box (TransformH CoreExprEquality String) = TransformCoreExprEqualityStringBox

data RewriteCoreExprEqualityBox

Constructors

RewriteCoreExprEqualityBox (RewriteH CoreExprEquality)

Instances

Typeable * RewriteCoreExprEqualityBox

data TransformCoreExprEqualityStringBox

Constructors

TransformCoreExprEqualityStringBox (TransformH CoreExprEquality String)

Instances

Typeable * TransformCoreExprEqualityStringBox

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

flipCoreExprEquality :: CoreExprEquality -> CoreExprEquality

Flip the LHS and RHS of a CoreExprEquality.

eqLhsIntroR :: CoreExprEquality -> Rewrite c HermitM Core

e ==> let v = lhs in e

eqRhsIntroR :: CoreExprEquality -> Rewrite c HermitM Core

e ==> let v = rhs in e

birewrite :: (AddBindings c, ReadBindings c, ExtendPath c Crumb, ReadPath c Crumb, HasEmptyContext c) => CoreExprEquality -> BiRewrite c HermitM CoreExpr

Create a BiRewrite from a CoreExprEquality.

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 CoreExprEquality

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

Lifting transformations over CoreExprEquality

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

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

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

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

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

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

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

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

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

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

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

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

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

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

ppCoreExprEqualityT :: PrettyPrinter -> TransformH CoreExprEquality DocH

proveCoreExprEqualityT :: forall c m. (AddBindings c, Monad m, ReadPath c Crumb) => CoreExprEqualityProof c m -> Transform c m CoreExprEquality ()

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

verifyCoreExprEqualityT :: Monad m => Transform c m CoreExprEquality ()

Verify that the left- and right-hand sides of a CoreExprEquality 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 -> CoreExprEqualityProof 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 CoreExprEquality

unshadowEqualityR :: RewriteH CoreExprEquality

instantiateDictsR :: RewriteH CoreExprEquality

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

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

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

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

discardUniVars :: CoreExprEquality -> CoreExprEquality