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

Safe HaskellNone
LanguageHaskell2010

HERMIT.Dictionary.FixPoint

Contents

Synopsis

Operations on the Fixed Point Operator (fix)

externals :: [External] Source

Externals for manipulating fixed points.

Rewrites and BiRewrites on Fixed Points

fixIntroR :: (AddBindings c, BoundVars c, ExtendPath c Crumb, HasEmptyContext c, ReadBindings c, ReadPath c Crumb, HasHermitMEnv m, LiftCoreM m, MonadCatch m, MonadIO m, MonadThings m, MonadUnique m) => Rewrite c m Core Source

fixIntroNonRecR :: (AddBindings c, BoundVars c, ExtendPath c Crumb, HasEmptyContext c, ReadBindings c, ReadPath c Crumb, HasHermitMEnv m, LiftCoreM m, MonadCatch m, MonadIO m, MonadThings m, MonadUnique m) => Rewrite c m CoreBind Source

fixIntroRecR :: (AddBindings c, BoundVars c, ExtendPath c Crumb, HasEmptyContext c, ReadBindings c, ReadPath c Crumb, HasHermitMEnv m, LiftCoreM m, MonadCatch m, MonadIO m, MonadThings m, MonadUnique m) => Rewrite c m CoreDef Source

f = e ==> f = fix (\ f -> e)

fixComputationRuleBR :: BiRewriteH CoreExpr Source

fix ty f <==> f (fix ty f)

fixRollingRuleBR :: BiRewriteH CoreExpr Source

fix tyA (\ a -> f (g a)) <==> f (fix tyB (\ b -> g (f b))

fixFusionRuleBR :: Maybe (EqualityProof HermitC HermitM) -> Maybe (RewriteH CoreExpr) -> CoreExpr -> CoreExpr -> CoreExpr -> BiRewriteH CoreExpr Source

If f is strict, then (f (g a) == h (f a)) ==> (f (fix g) == fix h)

Utilities

isFixExprT :: TransformH CoreExpr (Type, CoreExpr) Source

Check that the expression has the form "fix t (f :: t -> t)", returning "t" and "f".