HERMIT.Dictionary.FixPoint

Operations on the Fixed Point Operator (fix)

Note that many of these operations require fix to be explicitly imported, if it is not used in the source file.

externals :: [External]

Externals for manipulating fixed points.

Rewrites and BiRewrites on Fixed Points

fixIntroR :: RewriteH CoreDef

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

fixComputationRuleBR :: BiRewriteH CoreExpr

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

fixRollingRuleBR :: BiRewriteH CoreExpr

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

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

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

Utilities

mkFixT :: (BoundVars c, MonadCatch m, HasModGuts m, HasDynFlags m, HasHscEnv m, MonadIO m, MonadThings m) => CoreExpr -> Transform c m z CoreExpr

f ==> fix f

isFixExprT :: TransformH CoreExpr (Type, CoreExpr)

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