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

Safe HaskellNone

HERMIT.Dictionary.Local

Contents

Synopsis

Local Structural Manipulations

externals :: [External]Source

Externals for local structural manipulations. (Many taken from Chapter 3 of Andre Santos' dissertation.)

Binding Groups

Case Expressions

Cast Expressions

Let Expressions

Miscellaneous

abstractR :: ReadBindings c => Name -> Rewrite c HermitM CoreExprSource

Abstract over a variable using a lambda. e ==> ( x. e) x

pushRSource

Arguments

:: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, ReadBindings c, HasGlobalRdrEnv c) 
=> Maybe (Rewrite c HermitM CoreExpr)

a proof that the function (after being applied to its type arguments) is strict

-> (Id -> Bool)

a predicate to identify the function

-> Rewrite c HermitM CoreExpr 

Push a function through a Case or Let expression. Unsafe if the function is not strict.

betaReduceR :: MonadCatch m => Rewrite c m CoreExprSource

((\ v -> e1) e2) ==> (let v = e2 in e1) This form of beta-reduction is safe if e2 is an arbitrary expression (won't duplicate work).

betaReducePlusR :: MonadCatch m => Rewrite c m CoreExprSource

Perform one or more beta-reductions.

betaExpandR :: MonadCatch m => Rewrite c m CoreExprSource

(let v = e1 in e2) ==> (\ v -> e2) e1

etaReduceR :: MonadCatch m => Rewrite c m CoreExprSource

(\ v -> f v) ==> f

etaExpandR :: String -> Rewrite c HermitM CoreExprSource

e1 ==> (\ v -> e1 v)

multiEtaExpandR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c) => [String] -> Rewrite c HermitM CoreExprSource

Perform multiple eta-expansions.

flattenModuleR :: (ExtendPath c Crumb, Monad m) => Rewrite c m ModGutsSource

Flatten all the top-level binding groups in the module to a single recursive binding group.

flattenProgramR :: Monad m => Rewrite c m CoreProgSource

Flatten all the top-level binding groups in a program to a program containing a single recursive binding group.

flattenProgramT :: Monad m => Translate c m CoreProg CoreBindSource

Flatten all the top-level binding groups in a program to a single recursive binding group.