hermit-0.3.1.0: Haskell Equational Reasoning Model-to-Implementation Tunnel

Safe HaskellNone

HERMIT.Dictionary.Reasoning

Contents

Synopsis

Equational Reasoning

externals :: [External]Source

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

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

verifyEqualityCommonTargetT :: MonadCatch m => CoreExpr -> CoreExpr -> Rewrite c m CoreExpr -> Rewrite c m CoreExpr -> Translate c m a ()Source

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

verifyIsomorphismT :: CoreExpr -> CoreExpr -> Rewrite c HermitM CoreExpr -> Rewrite c HermitM CoreExpr -> Translate c HermitM a ()Source

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 -> Translate c HermitM a ()Source

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 CoreExprSource

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