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

Safe HaskellNone
LanguageHaskell2010

HERMIT.Dictionary.Reasoning

Contents

Synopsis

Equational Reasoning

externals :: [External] Source

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

eqLhsIntroR :: Clause -> Rewrite c HermitM Core Source

e ==> let v = lhs in e

eqRhsIntroR :: Clause -> Rewrite c HermitM Core Source

e ==> let v = rhs in e

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

Create a BiRewrite from a Clause.

extensionalityR :: (AddBindings c, ExtendPath c Crumb, ReadPath c Crumb) => Maybe String -> Rewrite c HermitM Clause Source

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

getLemmasT :: (LemmaContext c, HasLemmas m, Monad m) => Transform c m x Lemmas Source

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

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

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

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

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

markLemmaUsedT :: (LemmaContext c, HasLemmas m, MonadCatch m) => LemmaName -> Used -> Transform c m a () Source

markLemmaProvenT :: (LemmaContext c, HasLemmas m, MonadCatch m) => LemmaName -> Proven -> Transform c m a () Source

modifyLemmaT Source

Arguments

:: (LemmaContext c, HasLemmas m, Monad m) 
=> LemmaName 
-> (LemmaName -> LemmaName)

modify lemma name

-> Rewrite c m Clause

rewrite the quantified clause

-> (Proven -> Proven)

modify proven status

-> (Used -> Used)

modify used status

-> Transform c m a () 

showLemmaT :: LemmaName -> PrettyPrinter -> PrettyH a Source

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

ppLemmaT :: PrettyPrinter -> LemmaName -> PrettyH Lemma Source

ppClauseT :: PrettyPrinter -> PrettyH Clause Source

ppLCoreTCT :: PrettyPrinter -> PrettyH LCoreTC Source

Lifting transformations over Clause

lhsT :: (AddBindings c, HasEmptyContext c, LemmaContext c, ReadPath c Crumb, ExtendPath c Crumb, MonadCatch m) => Transform c m LCore a -> Transform c m Clause a Source

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

rhsT :: (AddBindings c, HasEmptyContext c, LemmaContext c, ReadPath c Crumb, ExtendPath c Crumb, MonadCatch m) => Transform c m LCore a -> Transform c m Clause a Source

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

bothT :: (AddBindings c, HasEmptyContext c, LemmaContext c, ReadPath c Crumb, ExtendPath c Crumb, MonadCatch m) => Transform c m LCore a -> Transform c m Clause (a, a) Source

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

lhsR :: (AddBindings c, HasEmptyContext c, LemmaContext c, ReadPath c Crumb, ExtendPath c Crumb, MonadCatch m) => Rewrite c m LCore -> Rewrite c m Clause Source

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

rhsR :: (AddBindings c, HasEmptyContext c, LemmaContext c, ReadPath c Crumb, ExtendPath c Crumb, MonadCatch m) => Rewrite c m LCore -> Rewrite c m Clause Source

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

bothR :: (AddBindings c, HasEmptyContext c, LemmaContext c, ReadPath c Crumb, ExtendPath c Crumb, MonadCatch m) => Rewrite c m LCore -> Rewrite c m Clause Source

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

verifyClauseT :: (AddBindings c, ReadPath c Crumb, ExtendPath c Crumb, MonadCatch m) => Transform c m Clause () Source

lemmaR :: (LemmaContext c, HasLemmas m, MonadCatch m) => Used -> LemmaName -> Rewrite c m Clause Source

quantIdentitiesR :: MonadCatch m => Rewrite c m Clause Source

verifyOrCreateT :: (AddBindings c, ExtendPath c Crumb, HasCoreRules c, LemmaContext c, ReadBindings c, ReadPath c Crumb, HasHermitMEnv m, HasLemmas m, LiftCoreM m, MonadCatch m) => Used -> LemmaName -> Clause -> Transform c m a () Source

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

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 () Source

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

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

reflexivityR :: Monad m => Rewrite c m Clause Source

simplifyClauseR :: (AddBindings c, ExtendPath c Crumb, HasEmptyContext c, LemmaContext c, ReadPath c Crumb, MonadCatch m) => Rewrite c m LCore Source

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

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

unshadowClauseR :: MonadUnique m => Rewrite c m Clause Source

instantiateDictsR :: RewriteH Clause Source

instantiateClauseVarR :: (Var -> Bool) -> CoreString -> RewriteH Clause Source

abstractClauseR :: forall c m. (AddBindings c, BoundVars c, ExtendPath c Crumb, HasEmptyContext c, ReadBindings c, ReadPath c Crumb, LemmaContext c, HasHermitMEnv m, HasLemmas m, LiftCoreM m, MonadCatch m, MonadUnique m) => String -> Transform c m Clause CoreExpr -> Rewrite c m Clause Source

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

Constructing Composite Lemmas

($$) :: (ToCoreExpr a, ToCoreExpr b, MonadCatch m) => a -> b -> m CoreExpr infixl 9 Source

($$$) :: (ToCoreExpr a, ToCoreExpr b, MonadCatch m) => a -> [b] -> m CoreExpr Source

(==>) :: (LemmaName, Clause) -> Clause -> Clause infixr 3 Source

(-->) :: Type -> Type -> Type infixr 5 Source

(===) :: (ToCoreExpr a, ToCoreExpr b) => a -> b -> Clause infix 8 Source

(/\) :: Clause -> Clause -> Clause infixr 5 Source

(\/) :: Clause -> Clause -> Clause infixr 4 Source

class ToCoreExpr a where Source

Methods

toCE :: a -> CoreExpr Source

Instances

newLemma :: LemmaName -> Clause -> Map LemmaName Lemma Source