Safe Haskell | None |
---|---|
Language | Haskell2010 |
- externals :: [External]
- type EqualityProof c m = (Rewrite c m CoreExpr, Rewrite c m CoreExpr)
- eqLhsIntroR :: Quantified -> Rewrite c HermitM Core
- eqRhsIntroR :: Quantified -> Rewrite c HermitM Core
- birewrite :: (AddBindings c, ExtendPath c Crumb, HasEmptyContext c, ReadBindings c, ReadPath c Crumb, MonadCatch m, MonadUnique m) => Quantified -> BiRewrite c m CoreExpr
- extensionalityR :: Maybe String -> Rewrite c HermitM Quantified
- 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 :: (HasLemmas m, Monad m) => LemmaName -> (LemmaName -> LemmaName) -> Rewrite c m Quantified -> (Proven -> Proven) -> (Used -> Used) -> 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
- lhsT :: (AddBindings c, ReadPath c Crumb, ExtendPath c Crumb, Monad m) => Transform c m LCore a -> Transform c m Quantified a
- rhsT :: (AddBindings c, ReadPath c Crumb, ExtendPath c Crumb, Monad m) => Transform c m LCore a -> Transform c m Quantified a
- bothT :: (AddBindings c, ReadPath c Crumb, ExtendPath c Crumb, Monad m) => Transform c m LCore a -> Transform c m Quantified (a, a)
- lhsR :: (AddBindings c, Monad m, ReadPath c Crumb, ExtendPath c Crumb) => Rewrite c m LCore -> Rewrite c m Quantified
- rhsR :: (AddBindings c, Monad m, ReadPath c Crumb, ExtendPath c Crumb) => Rewrite c m LCore -> Rewrite c m Quantified
- bothR :: (AddBindings c, MonadCatch m, ReadPath c Crumb, ExtendPath c Crumb) => Rewrite c m LCore -> Rewrite c m 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 ()
- verifyEqualityCommonTargetT :: MonadCatch m => CoreExpr -> CoreExpr -> EqualityProof c m -> Transform c m a ()
- verifyIsomorphismT :: CoreExpr -> CoreExpr -> Rewrite c HermitM CoreExpr -> Rewrite c HermitM CoreExpr -> Transform c HermitM a ()
- verifyRetractionT :: CoreExpr -> CoreExpr -> Rewrite c HermitM CoreExpr -> Transform c HermitM a ()
- retractionBR :: forall c. Maybe (Rewrite c HermitM CoreExpr) -> CoreExpr -> CoreExpr -> BiRewrite c HermitM CoreExpr
- 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
- discardUniVars :: Quantified -> Quantified
Equational Reasoning
eqLhsIntroR :: Quantified -> Rewrite c HermitM Core Source
e
==> let v = lhs in e
eqRhsIntroR :: Quantified -> 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) => Quantified -> BiRewrite c m CoreExpr Source
Create a BiRewrite
from a Quantified
.
extensionalityR :: Maybe String -> Rewrite c HermitM Quantified Source
f == g ==> forall x. f x == g x
getLemmasT :: HasLemmas m => Transform c m x Lemmas Source
getObligationNotProvenT :: (HasLemmas m, Monad m) => Transform c m x [NamedLemma] Source
insertLemmasT :: (HasLemmas m, Monad m) => [NamedLemma] -> Transform c m a () Source
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 Source
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 Source
showLemmaT :: LemmaName -> PrettyPrinter -> PrettyH a Source
showLemmasT :: Maybe LemmaName -> PrettyPrinter -> PrettyH a Source
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 Source
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 Source
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) Source
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 Source
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 Source
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 Source
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 () Source
verifyEquivalentT :: (HasLemmas m, MonadCatch m) => Used -> LemmaName -> Transform c m Quantified () Source
verifyOrCreateT :: (HasLemmas m, MonadCatch m) => Used -> LemmaName -> Lemma -> 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.
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.
unshadowQuantifiedR :: MonadUnique m => Rewrite c m Quantified Source
instantiateQuantifiedVarR :: (Var -> Bool) -> CoreString -> RewriteH Quantified Source
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 Source
Replace all occurrences of the given expression with a new quantified variable.