Safe Haskell | None |
---|
Type and instance definitions for Rewrite modules
- data CoreContext
- data RewriteState = RewriteState {
- _transformCounter :: Int
- _bindings :: HashMap TmName (Type, Term)
- _uniqSupply :: Supply
- _typeTranslator :: Type -> Maybe (Either String HWType)
- uniqSupply :: Lens' RewriteState Supply
- typeTranslator :: Lens' RewriteState (Type -> Maybe (Either String HWType))
- transformCounter :: Lens' RewriteState Int
- bindings :: Lens' RewriteState (HashMap TmName (Type, Term))
- data DebugLevel
- = DebugNone
- | DebugFinal
- | DebugApplied
- | DebugAll
- newtype RewriteEnv = RE {}
- dbgLevel :: Iso' RewriteEnv DebugLevel
- type RewriteSession m = ReaderT RewriteEnv (StateT RewriteState (FreshMT m))
- type RewriteMonad m = WriterT Any (RewriteSession m)
- newtype R m a = R {
- runR :: RewriteMonad m a
- type Transform m = [CoreContext] -> Term -> m Term
- type Rewrite m = Transform (R m)
Documentation
data CoreContext Source
Context in which a term appears
AppFun | Function position of an application |
AppArg | Argument position of an application |
TyAppC | Function position of a type application |
LetBinding [Id] | RHS of a Let-binder with the sibling LHS' |
LetBody [Id] | Body of a Let-binding with the bound LHS' |
LamBody Id | Body of a lambda-term with the abstracted variable |
TyLamBody TyVar | Body of a TyLambda-term with the abstracted type-variable |
CaseAlt [Id] | RHS of a case-alternative with the variables bound by the pattern on the LHS |
CaseScrut | Subject of a case-decomposition |
data RewriteState Source
State of a rewriting session
RewriteState | |
|
Monad m => MonadState RewriteState (R m) | |
Monad m => MonadUnique (RewriteMonad m) |
typeTranslator :: Lens' RewriteState (Type -> Maybe (Either String HWType))Source
data DebugLevel Source
Debug Message Verbosity
DebugNone | Don't show debug messages |
DebugFinal | Show completely normalized expressions |
DebugApplied | Show sub-expressions after a successful rewrite |
DebugAll | Show all sub-expressions on which a rewrite is attempted |
newtype RewriteEnv Source
Read-only environment of a rewriting session
Monad m => MonadReader RewriteEnv (R m) | |
Monad m => MonadUnique (RewriteMonad m) |
type RewriteSession m = ReaderT RewriteEnv (StateT RewriteState (FreshMT m))Source
Monad that keeps track how many transformations have been applied and can generate fresh variables and unique identifiers
type RewriteMonad m = WriterT Any (RewriteSession m)Source
Monad that can do the same as RewriteSession
and in addition keeps track
if a transformation/rewrite has been successfully applied.
MTL convenience wrapper around RewriteMonad
R | |
|
type Transform m = [CoreContext] -> Term -> m TermSource
Monadic action that transforms a term given a certain context