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

Safe HaskellNone

HERMIT.Dictionary.FixPoint

Contents

Synopsis

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]Source

Externals for manipulating fixed points.

Rewrites and BiRewrites on Fixed Points

fixIntroR :: RewriteH CoreDefSource

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

fixComputationRuleBR :: BiRewriteH CoreExprSource

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

fixRollingRuleBR :: BiRewriteH CoreExprSource

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 CoreExprSource

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

Utilities

isFixExprT :: TranslateH CoreExpr (Type, CoreExpr)Source

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