Safe Haskell | None |
---|

Utilities for rewriting: e.g. inlining, specialisation, etc.

- liftR :: Monad m => m a -> RewriteMonad m a
- liftRS :: Monad m => m a -> RewriteSession m a
- apply :: (Monad m, Functor m) => String -> Rewrite m -> Rewrite m
- runRewrite :: (Monad m, Functor m) => String -> Rewrite m -> Term -> RewriteSession m Term
- runRewriteSession :: Monad m => DebugLevel -> RewriteState -> RewriteSession m a -> m a
- setChanged :: Monad m => RewriteMonad m ()
- changed :: Monad m => a -> RewriteMonad m a
- contextEnv :: [CoreContext] -> (Gamma, Delta)
- mkEnv :: (Functor m, Monad m) => [CoreContext] -> RewriteMonad m (Gamma, Delta)
- mkTmBinderFor :: (Functor m, Fresh m, MonadUnique m) => String -> Term -> m (Id, Term)
- mkBinderFor :: (Functor m, Monad m, MonadUnique m, Fresh m) => String -> Either Term Type -> m (Either (Id, Term) (TyVar, Type))
- mkInternalVar :: (Functor m, Monad m, MonadUnique m) => String -> KindOrType -> m (Id, Term)
- inlineBinders :: Monad m => (LetBinding -> RewriteMonad m Bool) -> Rewrite m
- substituteBinders :: [LetBinding] -> [LetBinding] -> Term -> ([LetBinding], Term)
- localFreeVars :: (Functor m, Monad m, Collection c) => Term -> RewriteMonad m (c TyName, c TmName)
- liftBinders :: (Functor m, Monad m) => (LetBinding -> RewriteMonad m Bool) -> Rewrite m
- liftBinding :: (Functor m, Monad m) => Gamma -> Delta -> LetBinding -> RewriteMonad m LetBinding
- mkFunction :: (Functor m, Monad m) => TmName -> Term -> RewriteMonad m (TmName, Type)
- addGlobalBind :: (Functor m, Monad m) => TmName -> Type -> Term -> RewriteMonad m ()
- cloneVar :: (Functor m, Monad m) => TmName -> RewriteMonad m TmName
- isLocalVar :: (Functor m, Monad m) => Term -> RewriteMonad m Bool
- isUntranslatable :: (Functor m, Monad m) => Term -> RewriteMonad m Bool
- isLambdaBodyCtx :: CoreContext -> Bool
- mkWildValBinder :: (Functor m, Monad m, MonadUnique m) => Type -> m Id
- mkSelectorCase :: (Functor m, Monad m, MonadUnique m, Fresh m) => String -> [CoreContext] -> Term -> Int -> Int -> m Term
- specialise :: (Functor m, MonadState s m) => Lens' s (Map (TmName, Int, Either Term Type) (TmName, Type)) -> Rewrite m
- specialise' :: (Functor m, MonadState s m) => Lens' s (Map (TmName, Int, Either Term Type) (TmName, Type)) -> [CoreContext] -> Term -> (Term, [Either Term Type]) -> Either Term Type -> R m Term
- specArgBndrsAndVars :: (Functor m, Monad m) => [CoreContext] -> Either Term Type -> RewriteMonad m ([Either Id TyVar], [Either Term Type])

# Documentation

liftR :: Monad m => m a -> RewriteMonad m aSource

Lift an action working in the inner monad to the `RewriteMonad`

liftRS :: Monad m => m a -> RewriteSession m aSource

Lift an action working in the inner monad to the `RewriteSession`

:: (Monad m, Functor m) | |

=> String | Name of the transformation |

-> Rewrite m | Transformation to be applied |

-> Rewrite m |

Record if a transformation is succesfully applied

:: (Monad m, Functor m) | |

=> String | Name of the transformation |

-> Rewrite m | Transformation to perform |

-> Term | Term to transform |

-> RewriteSession m Term |

Perform a transformation on a Term

runRewriteSession :: Monad m => DebugLevel -> RewriteState -> RewriteSession m a -> m aSource

Evaluate a RewriteSession to its inner monad

setChanged :: Monad m => RewriteMonad m ()Source

Notify that a transformation has changed the expression

changed :: Monad m => a -> RewriteMonad m aSource

Identity function that additionally notifies that a transformation has changed the expression

contextEnv :: [CoreContext] -> (Gamma, Delta)Source

Create a type and kind context out of a transformation context

mkEnv :: (Functor m, Monad m) => [CoreContext] -> RewriteMonad m (Gamma, Delta)Source

Create a complete type and kind context out of the global binders and the transformation context

:: (Functor m, Fresh m, MonadUnique m) | |

=> String | Name of the new binder |

-> Term | Term to bind |

-> m (Id, Term) |

Make a new binder and variable reference for a term

:: (Functor m, Monad m, MonadUnique m, Fresh m) | |

=> String | Name of the new binder |

-> Either Term Type | Type or Term to bind |

-> m (Either (Id, Term) (TyVar, Type)) |

Make a new binder and variable reference for either a term or a type

:: (Functor m, Monad m, MonadUnique m) | |

=> String | Name of the identifier |

-> KindOrType | |

-> m (Id, Term) |

Make a new, unique, identifier and corresponding variable reference

:: Monad m | |

=> (LetBinding -> RewriteMonad m Bool) | Property test |

-> Rewrite m |

Inline the binders in a let-binding that have a certain property

:: [LetBinding] | Let-binders to substitute |

-> [LetBinding] | Let-binders where substitution takes place |

-> Term | Expression where substitution takes place |

-> ([LetBinding], Term) |

Substitute the RHS of the first set of Let-binders for references to the first set of Let-binders in: the second set of Let-binders and the additional term

localFreeVars :: (Functor m, Monad m, Collection c) => Term -> RewriteMonad m (c TyName, c TmName)Source

Calculate the *local* free variable of an expression: the free variables
that are not bound in the global environment.

:: (Functor m, Monad m) | |

=> (LetBinding -> RewriteMonad m Bool) | Property test |

-> Rewrite m |

Lift the binders in a let-binding to a global function that have a certain property

liftBinding :: (Functor m, Monad m) => Gamma -> Delta -> LetBinding -> RewriteMonad m LetBindingSource

Create a global function for a Let-binding and return a Let-binding where the RHS is a reference to the new global function applied to the free variables of the original RHS

:: (Functor m, Monad m) | |

=> TmName | Name of the function |

-> Term | Term bound to the function |

-> RewriteMonad m (TmName, Type) | Name with a proper unique and the type of the function |

Make a global function for a name-term tuple

addGlobalBind :: (Functor m, Monad m) => TmName -> Type -> Term -> RewriteMonad m ()Source

Add a function to the set of global binders

cloneVar :: (Functor m, Monad m) => TmName -> RewriteMonad m TmNameSource

Create a new name out of the given name, but with another unique

isLocalVar :: (Functor m, Monad m) => Term -> RewriteMonad m BoolSource

Test whether a term is a variable reference to a local binder

isUntranslatable :: (Functor m, Monad m) => Term -> RewriteMonad m BoolSource

Determine if a term cannot be represented in hardware

isLambdaBodyCtx :: CoreContext -> BoolSource

Is the Context a Lambda/Term-abstraction context?

mkWildValBinder :: (Functor m, Monad m, MonadUnique m) => Type -> m IdSource

Make a binder that should not be referenced

:: (Functor m, Monad m, MonadUnique m, Fresh m) | |

=> String | Name of the caller of this function |

-> [CoreContext] | Transformation Context in which this function is called |

-> Term | Subject of the case-composition |

-> Int | |

-> Int | |

-> m Term |

Make a case-decomposition that extracts a field out of a (Sum-of-)Product type

specialise :: (Functor m, MonadState s m) => Lens' s (Map (TmName, Int, Either Term Type) (TmName, Type)) -> Rewrite mSource

Specialise an application on its argument

:: (Functor m, MonadState s m) | |

=> Lens' s (Map (TmName, Int, Either Term Type) (TmName, Type)) | Lens into previous specialisations |

-> [CoreContext] | |

-> Term | Original term |

-> (Term, [Either Term Type]) | Function part of the term, split into root and applied arguments |

-> Either Term Type | Argument to specialize on |

-> R m Term |

Specialise an application on its argument

specArgBndrsAndVars :: (Functor m, Monad m) => [CoreContext] -> Either Term Type -> RewriteMonad m ([Either Id TyVar], [Either Term Type])Source

Create binders and variable references for free variables in `specArg`