HERMIT.Dictionary.Reasoning

Equational Reasoning

externals :: [External]

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

eqLhsIntroR :: Quantified -> Rewrite c HermitM Core

e ==> let v = lhs in e

eqRhsIntroR :: Quantified -> 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) => Quantified -> BiRewrite c m CoreExpr

Create a BiRewrite from a Quantified.

extensionalityR :: Maybe String -> Rewrite c HermitM Quantified

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

getObligationNotProvenT :: (HasLemmas m, Monad m) => Transform c m x [NamedLemma]

insertLemmaT :: (HasLemmas m, Monad m) => LemmaName -> Lemma -> Transform c m a ()

insertLemmasT :: (HasLemmas m, Monad m) => [NamedLemma] -> Transform c m a ()

lemmaBiR :: (AddBindings c, ExtendPath c Crumb, HasEmptyContext c, ReadBindings c, ReadPath c Crumb, HasLemmas m, MonadCatch m, MonadUnique m) => Used -> LemmaName -> BiRewrite c m CoreExpr

lemmaConsequentR :: forall c m. (AddBindings c, ExtendPath c Crumb, HasEmptyContext c, ReadBindings c, ReadPath c Crumb, HasLemmas m, MonadCatch m, MonadUnique m) => Used -> LemmaName -> Rewrite c m Quantified

markLemmaUsedT :: (HasLemmas m, Monad m) => LemmaName -> Used -> Transform c m a ()

markLemmaProvenT :: (HasLemmas m, Monad m) => LemmaName -> Proven -> Transform c m a ()

modifyLemmaT

Arguments

:: (HasLemmas m, Monad m)

=> LemmaName

-> (LemmaName -> LemmaName)

modify lemma name

-> Rewrite c m Quantified

rewrite the quantified clause

-> (Proven -> Proven)

modify proven status

-> (Used -> Used)

modify used status

-> Transform c m a ()

showLemmaT :: LemmaName -> PrettyPrinter -> PrettyH a

showLemmasT :: Maybe LemmaName -> PrettyPrinter -> PrettyH a

ppLemmaT :: PrettyPrinter -> LemmaName -> PrettyH Lemma

ppQuantifiedT :: PrettyPrinter -> PrettyH Quantified

ppLCoreTCT :: PrettyPrinter -> PrettyH LCoreTC

Lifting transformations over Quantified

lhsT :: (AddBindings c, ReadPath c Crumb, ExtendPath c Crumb, Monad m) => Transform c m LCore a -> Transform c m Quantified a

Lift a transformation over LCoreTC into a transformation over the left-hand side of a Quantified.

rhsT :: (AddBindings c, ReadPath c Crumb, ExtendPath c Crumb, Monad m) => Transform c m LCore a -> Transform c m Quantified a

Lift a transformation over LCoreTC into a transformation over the right-hand side of a Quantified.

bothT :: (AddBindings c, ReadPath c Crumb, ExtendPath c Crumb, Monad m) => Transform c m LCore a -> Transform c m Quantified (a, a)

Lift a transformation over LCoreTC into a transformation over both sides of a Quantified.

lhsR :: (AddBindings c, Monad m, ReadPath c Crumb, ExtendPath c Crumb) => Rewrite c m LCore -> Rewrite c m Quantified

Lift a rewrite over LCoreTC into a rewrite over the left-hand side of a Quantified.

rhsR :: (AddBindings c, Monad m, ReadPath c Crumb, ExtendPath c Crumb) => Rewrite c m LCore -> Rewrite c m Quantified

Lift a rewrite over LCoreTC into a rewrite over the right-hand side of a Quantified.

bothR :: (AddBindings c, MonadCatch m, ReadPath c Crumb, ExtendPath c Crumb) => Rewrite c m LCore -> Rewrite c m Quantified

Lift a rewrite over LCoreTC into a rewrite over both sides of a Quantified.

verifyQuantifiedT :: (AddBindings c, ReadPath c Crumb, ExtendPath c Crumb, MonadCatch m) => Transform c m Quantified ()

verifyEquivalentT :: (HasLemmas m, MonadCatch m) => Used -> LemmaName -> Transform c m Quantified ()

verifyOrCreateT :: (HasLemmas m, MonadCatch m) => Used -> LemmaName -> Lemma -> Transform c m a ()

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.

unshadowQuantifiedR :: MonadUnique m => Rewrite c m Quantified

instantiateDictsR :: RewriteH Quantified

instantiateQuantifiedVarR :: (Var -> Bool) -> CoreString -> RewriteH Quantified

abstractQuantifiedR :: forall c m. (AddBindings c, BoundVars c, ExtendPath c Crumb, HasEmptyContext c, ReadBindings c, ReadPath c Crumb, HasDebugChan m, HasHermitMEnv m, HasLemmas m, LiftCoreM m, MonadCatch m, MonadUnique m) => String -> Transform c m Quantified CoreExpr -> Rewrite c m Quantified

Replace all occurrences of the given expression with a new quantified variable.

discardUniVars :: Quantified -> Quantified