Safe Haskell | None |
---|---|
Language | Haskell2010 |
- externals :: [External]
- type EqualityProof c m = (Rewrite c m CoreExpr, Rewrite c m CoreExpr)
- eqLhsIntroR :: Clause -> Rewrite c HermitM Core
- eqRhsIntroR :: Clause -> Rewrite c HermitM Core
- birewrite :: (AddBindings c, ExtendPath c Crumb, HasEmptyContext c, ReadBindings c, ReadPath c Crumb, MonadCatch m, MonadUnique m) => Clause -> BiRewrite c m CoreExpr
- extensionalityR :: (AddBindings c, ExtendPath c Crumb, ReadPath c Crumb) => Maybe String -> Rewrite c HermitM Clause
- getLemmasT :: (LemmaContext c, HasLemmas m, Monad m) => Transform c m x Lemmas
- getLemmaByNameT :: (LemmaContext c, HasLemmas m, Monad m) => LemmaName -> Transform c m x Lemma
- 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, LemmaContext 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, LemmaContext c, ReadBindings c, ReadPath c Crumb, HasLemmas m, MonadCatch m, MonadUnique m) => Used -> LemmaName -> Rewrite c m Clause
- markLemmaUsedT :: (LemmaContext c, HasLemmas m, MonadCatch m) => LemmaName -> Used -> Transform c m a ()
- markLemmaProvenT :: (LemmaContext c, HasLemmas m, MonadCatch m) => LemmaName -> Proven -> Transform c m a ()
- modifyLemmaT :: (LemmaContext c, HasLemmas m, Monad m) => LemmaName -> (LemmaName -> LemmaName) -> Rewrite c m Clause -> (Proven -> Proven) -> (Used -> Used) -> Transform c m a ()
- showLemmaT :: LemmaName -> PrettyPrinter -> PrettyH a
- showLemmasT :: Maybe LemmaName -> PrettyPrinter -> PrettyH a
- ppLemmaT :: PrettyPrinter -> LemmaName -> PrettyH Lemma
- ppClauseT :: PrettyPrinter -> PrettyH Clause
- ppLCoreTCT :: PrettyPrinter -> PrettyH LCoreTC
- 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
- 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
- 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)
- lhsR :: (AddBindings c, HasEmptyContext c, LemmaContext c, ReadPath c Crumb, ExtendPath c Crumb, MonadCatch m) => Rewrite c m LCore -> Rewrite c m Clause
- rhsR :: (AddBindings c, HasEmptyContext c, LemmaContext c, ReadPath c Crumb, ExtendPath c Crumb, MonadCatch m) => Rewrite c m LCore -> Rewrite c m Clause
- bothR :: (AddBindings c, HasEmptyContext c, LemmaContext c, ReadPath c Crumb, ExtendPath c Crumb, MonadCatch m) => Rewrite c m LCore -> Rewrite c m Clause
- verifyClauseT :: (AddBindings c, ReadPath c Crumb, ExtendPath c Crumb, MonadCatch m) => Transform c m Clause ()
- lemmaR :: (LemmaContext c, HasLemmas m, MonadCatch m) => Used -> LemmaName -> Rewrite c m Clause
- quantIdentitiesR :: MonadCatch m => Rewrite c m Clause
- 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 ()
- 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 ()
- reflexivityR :: Monad m => Rewrite c m Clause
- simplifyClauseR :: (AddBindings c, ExtendPath c Crumb, HasEmptyContext c, LemmaContext c, ReadPath c Crumb, MonadCatch m) => Rewrite c m LCore
- retractionBR :: forall c. Maybe (Rewrite c HermitM CoreExpr) -> CoreExpr -> CoreExpr -> BiRewrite c HermitM CoreExpr
- unshadowClauseR :: MonadUnique m => Rewrite c m Clause
- instantiateDictsR :: RewriteH Clause
- instantiateClauseVarR :: (Var -> Bool) -> CoreString -> RewriteH Clause
- 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
- ($$) :: (ToCoreExpr a, ToCoreExpr b, MonadCatch m) => a -> b -> m CoreExpr
- ($$$) :: (ToCoreExpr a, ToCoreExpr b, MonadCatch m) => a -> [b] -> m CoreExpr
- (==>) :: (LemmaName, Clause) -> Clause -> Clause
- (-->) :: Type -> Type -> Type
- (===) :: (ToCoreExpr a, ToCoreExpr b) => a -> b -> Clause
- (/\) :: Clause -> Clause -> Clause
- (\/) :: Clause -> Clause -> Clause
- class ToCoreExpr a where
- newLemma :: LemmaName -> Clause -> Map LemmaName Lemma
Equational Reasoning
birewrite :: (AddBindings c, ExtendPath c Crumb, HasEmptyContext c, ReadBindings c, ReadPath c Crumb, MonadCatch m, MonadUnique m) => Clause -> BiRewrite c m CoreExpr Source
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
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
showLemmaT :: LemmaName -> PrettyPrinter -> PrettyH a Source
showLemmasT :: Maybe LemmaName -> PrettyPrinter -> PrettyH a 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
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
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
lhsR :: (AddBindings c, HasEmptyContext c, LemmaContext c, ReadPath c Crumb, ExtendPath c Crumb, MonadCatch m) => Rewrite c m LCore -> Rewrite c m Clause Source
rhsR :: (AddBindings c, HasEmptyContext c, LemmaContext c, ReadPath c Crumb, ExtendPath c Crumb, MonadCatch m) => Rewrite c m LCore -> Rewrite c m Clause Source
bothR :: (AddBindings c, HasEmptyContext c, LemmaContext c, ReadPath c Crumb, ExtendPath c Crumb, MonadCatch m) => Rewrite c m LCore -> Rewrite c m Clause Source
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
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
(===) :: (ToCoreExpr a, ToCoreExpr b) => a -> b -> Clause infix 8 Source
class ToCoreExpr a where Source