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 (RewriteH CoreExpr, RewriteH CoreExpr) -> 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, HasGlobalRdrEnv c, MonadCatch m, HasDynFlags m, MonadThings m) => CoreExpr -> Translate c m z CoreExpr

f ==> fix f

isFixExprT :: TranslateH CoreExpr (Type, CoreExpr)

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