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

Safe HaskellNone
LanguageHaskell2010

HERMIT.Dictionary.AlphaConversion

Contents

Synopsis

Alpha-Renaming and Shadowing

externals :: [External] Source

Externals for alpha-renaming.

Alpha-Renaming

alphaR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, BoundVars c) => Rewrite c HermitM Core Source

Alpha rename any bindings at this node. Note: does not rename case alternatives unless invoked on the alternative.

alphaLamR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, BoundVars c) => Maybe String -> Rewrite c HermitM CoreExpr Source

Alpha rename a lambda binder. Optionally takes a suggested new name.

alphaCaseBinderR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, BoundVars c) => Maybe String -> Rewrite c HermitM CoreExpr Source

Alpha rename a case binder. Optionally takes a suggested new name.

alphaAltWithR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, BoundVars c) => [String] -> Rewrite c HermitM CoreAlt Source

Rename the variables bound in a case alternative with the given list of suggested names.

alphaAltVarsR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, BoundVars c) => [Var] -> Rewrite c HermitM CoreAlt Source

Rename the specified variables in a case alternative.

alphaAltR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, BoundVars c) => Rewrite c HermitM CoreAlt Source

Rename all identifiers bound in a case alternative.

alphaCaseR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, BoundVars c) => Rewrite c HermitM CoreExpr Source

Rename all identifiers bound in a case expression.

alphaLetWithR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, BoundVars c) => [String] -> Rewrite c HermitM CoreExpr Source

Rename the identifiers bound in a Let with the given list of suggested names.

alphaLetVarsR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, BoundVars c) => [Var] -> Rewrite c HermitM CoreExpr Source

Rename the specified variables bound in a let.

alphaLetR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, BoundVars c) => Rewrite c HermitM CoreExpr Source

Rename all identifiers bound in a Let.

alphaProgConsWithR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, BoundVars c) => [String] -> Rewrite c HermitM CoreProg Source

Rename the identifiers bound in the top-level binding at the head of the program with the given list of suggested names.

alphaProgConsIdsR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, BoundVars c) => [Id] -> Rewrite c HermitM CoreProg Source

Rename the specified variables bound in the top-level binding at the head of the program.

alphaProgConsR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, BoundVars c) => Rewrite c HermitM CoreProg Source

Rename all identifiers bound in the top-level binding at the head of the program.

alphaProgR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, BoundVars c) => Rewrite c HermitM CoreProg Source

Rename all identifiers bound at the top-level.

Shadow Detection and Unshadowing

unshadowR :: (AddBindings c, BoundVars c, ExtendPath c Crumb, HasEmptyContext c, ReadPath c Crumb) => Rewrite c HermitM Core Source

Rename local variables with manifestly unique names (x, x0, x1, ...). Does not rename top-level definitions.

visibleVarsT :: (BoundVars c, Monad m) => Transform c m CoreTC VarSet Source

Collect all visible variables (in the expression or the context).

cloneVarAvoidingT :: BoundVars c => Var -> Maybe String -> [Var] -> Transform c HermitM CoreTC Var Source

If a name is provided, use that as the name of the new variable. Otherwise modify the variable name making sure to not clash with the given variables or any visible variables.

freshNameGenAvoiding :: Maybe String -> VarSet -> String -> String Source

Use the optional argument if given, otherwise generate a new name avoiding clashes with the set of variables.

detectShadowsM :: Monad m => [Var] -> VarSet -> m VarSet Source

Shadows are any duplicates in the list, or any occurrences of the list elements in the set.

replaceVarR :: (Injection a Core, MonadCatch m) => Var -> Var -> Rewrite c m a Source

Replace all occurrences of a specified variable. Arguments are the variable to replace and the replacement variable, respectively.