-- Hoogle documentation, generated by Haddock -- See Hoogle, http://www.haskell.org/hoogle/ -- | Haskell Equational Reasoning Model-to-Implementation Tunnel -- -- HERMIT uses Haskell to express semi-formal models, efficient -- implementations, and provide a bridging DSL to describe via stepwise -- refinement the connection between these models and implementations. -- The key transformation in the bridging DSL is the worker/wrapper -- transformation. -- -- This is an alpha `please give feedback' release. Shortcomings/gotchas -- include: -- -- -- -- Examples can be found in the examples sub-directory. -- -- 
--   $ cd examples/reverse
--
-- -- Example of running a script. -- -- 
--   $ hermit Reverse.hs Reverse.hss resume
--   [starting HERMIT v0.3.0.0 on Reverse.hs]
--   % ghc Reverse.hs -fforce-recomp -O2 -dcore-lint -fexpose-all-unfoldings -fsimple-list-literals -fplugin=HERMIT -fplugin-opt=HERMIT:Main:Reverse.hss -fplugin-opt=HERMIT:Main:resume
--   [1 of 2] Compiling HList            ( HList.hs, HList.o )
--   Loading package ghc-prim ... linking ... done.
--   ...
--   Loading package hermit-0.3.0.0 ... linking ... done.
--   [2 of 2] Compiling Main             ( Reverse.hs, Reverse.o )
--   Linking Reverse ...
--   $ ./Reverse
--   ....
--
-- -- Example of interactive use. -- -- 
--   $ hermit Reverse.hs
--   [starting HERMIT v0.3.0.0 on Reverse.hs]
--   % ghc Reverse.hs -fforce-recomp -O2 -dcore-lint -fexpose-all-unfoldings -fsimple-list-literals -fplugin=HERMIT -fplugin-opt=HERMIT:Main:
--   [1 of 2] Compiling HList            ( HList.hs, HList.o )
--   Loading package ghc-prim ... linking ... done.
--   ...
--   Loading package hermit-0.3.0.0 ... linking ... done.
--   [2 of 2] Compiling Main             ( Reverse.hs, Reverse.o )
--   ===================== Welcome to HERMIT =====================
--   HERMIT is a toolkit for the interactive transformation of GHC
--   core language programs. Documentation on HERMIT can be found
--   on the HERMIT web page at:
--   http://www.ittc.ku.edu/csdl/fpg/software/hermit.html
--   
--   You have just loaded the interactive shell. To exit, type
--   "abort" or "resume" to abort or resume GHC compilation.
--   
--   Type "help" for instructions on how to list or search the
--   available HERMIT commands.
--   
--   To get started, you could try the following:
--     - type "consider 'foo", where "foo" is a function
--       defined in the module;
--     - type "set-pp-type Show" to switch on typing information;
--     - use natural numbers such as "0" and "1" to descend into
--       the definition, and "up" to ascend;
--     - type "info" for more information about the current node;
--     - type "log" to display an activity log.
--   =============================================================
--   module main:Main where
--     rev ∷ ∀ a . [a] -> [a]
--     unwrap ∷ ∀ a . ([a] -> [a]) -> [a] -> H a
--     wrap ∷ ∀ a . ([a] -> H a) -> [a] -> [a]
--     main ∷ IO ()
--     main ∷ IO ()
--   hermit<0>
--   ...
--
-- -- To resume compilation, use resume. -- -- 
--   ...
--   hermit<0> resume
--   hermit<0> Linking Reverse ...
--   $
--
@package hermit @version 0.3.0.0 module HERMIT.Parser type Script = [ExprH] parseScript :: String -> Either String Script unparseScript :: Script -> String unparseExprH :: ExprH -> String -- | A simple expression language AST, for things parsed from String -- or JSON structures. data ExprH -- | Variable names (refers to source code). SrcName :: String -> ExprH -- | Commands (to be looked up in Dictionary). CmdName :: String -> ExprH -- | Application. AppH :: ExprH -> ExprH -> ExprH -- | Core Fragment CoreH :: String -> ExprH -- | List of expressions ListH :: [ExprH] -> ExprH instance Eq ExprH instance Show ExprH instance Eq Token instance Show Token module HERMIT.Driver hermit_version :: String ghcFlags :: [String] module HERMIT.GHC -- | Pretty-print an identifier. ppIdInfo :: Id -> IdInfo -> SDoc -- | Erase all OccInfo in a variable if it is is an Id, or do -- nothing if it's a TyVar or CoVar (which have no -- OccInfo). zapVarOccInfo :: Var -> Var -- | Convert a variable to a neat string for printing (unqualfied name). var2String :: Var -> String thRdrNameGuesses :: Name -> [RdrName] -- | Converts a GHC Name to a Template Haskell Name, going -- via a String. name2THName :: Name -> Name -- | Converts an Var to a Template Haskell Name, going via a -- String. var2THName :: Var -> Name -- | Compare a Name to a Name for equality. See -- cmpString2Name. cmpTHName2Name :: Name -> Name -> Bool -- | Compare a String to a Name for equality. Strings -- containing a period are assumed to be fully qualified names. cmpString2Name :: String -> Name -> Bool -- | Compare a Name to a Var for equality. See -- cmpString2Name. cmpTHName2Var :: Name -> Var -> Bool -- | Compare a String to a Var for equality. See -- cmpString2Name. cmpString2Var :: String -> Var -> Bool -- | Get the fully qualified name from a Name. fqName :: Name -> String -- | Get the unqualified name from a NamedThing. uqName :: NamedThing nm => nm -> String -- | Find Names matching a given fully qualified or unqualified -- name. If given name is fully qualified, will only return first result, -- which is assumed unique. findNamesFromString :: GlobalRdrEnv -> String -> [Name] -- | Find Names matching a Name. See -- findNamesFromString. findNamesFromTH :: GlobalRdrEnv -> Name -> [Name] alphaTyVars :: [TyVar] -- | The key representation of types within the compiler data Type :: * -- | Vanilla type or kind variable (*never* a coercion variable) TyVarTy :: Var -> Type -- | Type application to something other than a TyCon. Parameters: -- -- 1) Function: must not be a TyConApp, must be another -- AppTy, or TyVarTy -- -- 2) Argument type AppTy :: Type -> Type -> Type -- | Application of a TyCon, including newtypes and synonyms. -- Invariant: saturated appliations of FunTyCon must use -- FunTy and saturated synonyms must use their own constructors. -- However, unsaturated FunTyCons do appear as -- TyConApps. Parameters: -- -- 1) Type constructor being applied to. -- -- 2) Type arguments. Might not have enough type arguments here to -- saturate the constructor. Even type synonyms are not necessarily -- saturated; for example unsaturated type synonyms can appear as the -- right hand side of a type synonym. TyConApp :: TyCon -> [KindOrType] -> Type -- | Special case of TyConApp: TyConApp FunTyCon [t1, t2] -- See Note [Equality-constrained types] FunTy :: Type -> Type -> Type -- | A polymorphic type ForAllTy :: Var -> Type -> Type -- | Type literals are simillar to type constructors. LitTy :: TyLit -> Type data TyLit :: * NumTyLit :: Integer -> TyLit StrTyLit :: FastString -> TyLit -- | GHC's own exception type error messages all take the form: -- -- 
--   location: error
--
-- -- If the location is on the command line, or in GHC itself, then -- location=ghc. All of the error types below correspond to -- a location of ghc, except for ProgramError (where the -- string is assumed to contain a location already, so we don't print -- one). data GhcException :: * -- | An error in the user's code, probably. ProgramError :: String -> GhcException throwGhcException :: GhcException -> a -- | An approximate, fast, version of exprEtaExpandArity exprArity :: CoreExpr -> Arity occurAnalyseExpr :: CoreExpr -> CoreExpr -- | Is this a kind (i.e. a type-of-types)? isKind :: Kind -> Bool isLiftedTypeKindCon :: TyCon -> Bool -- | Determine if a Var is not an element of a VarSet. notElemVarSet :: Var -> VarSet -> Bool -- | Convert a VarSet to a list of user-readable strings. varSetToStrings :: VarSet -> [String] -- | Show a human-readable version of a VarSet. showVarSet :: VarSet -> String data Pair a :: * -> * Pair :: a -> a -> Pair a pFst :: Pair a -> a pSnd :: Pair a -> a -- | Lift a computation from the IO monad. liftIO :: MonadIO m => forall a. IO a -> m a instance MonadIO CoreM instance Monoid VarSet module HERMIT.Core -- | A program is a telescope of nested binding groups. That is, each -- binding scopes over the remainder of the program. In GHC Core, -- programs are encoded as [CoreBind]. This data type is -- isomorphic. data CoreProg -- | An empty program. ProgNil :: CoreProg -- | A binding group and the program it scopes over. ProgCons :: CoreBind -> CoreProg -> CoreProg -- | A (potentially recursive) definition is an identifier and an -- expression. In GHC Core, recursive definitions are encoded as -- (Id, CoreExpr) pairs. This data type is isomorphic. data CoreDef Def :: Id -> CoreExpr -> CoreDef -- | Unlike everything else, there is no synonym for Tickish -- Id provided by GHC, so we define one. type CoreTickish = Tickish Id -- | Syntactic Equality of programs. progSyntaxEq :: CoreProg -> CoreProg -> Bool -- | Syntactic Equality of binding groups. bindSyntaxEq :: CoreBind -> CoreBind -> Bool -- | Syntactic Equality of recursive definitions. defSyntaxEq :: CoreDef -> CoreDef -> Bool -- | Syntactic Equality of expressions. exprSyntaxEq :: CoreExpr -> CoreExpr -> Bool -- | Syntactic Equality of case alternatives. altSyntaxEq :: CoreAlt -> CoreAlt -> Bool -- | Syntactic Equality of Types. typeSyntaxEq :: Type -> Type -> Bool -- | Syntactic Equality of Coercions. coercionSyntaxEq :: Coercion -> Coercion -> Bool -- | Alpha equality of programs. progAlphaEq :: CoreProg -> CoreProg -> Bool -- | Alpha equality of binding groups. bindAlphaEq :: CoreBind -> CoreBind -> Bool -- | Alpha equality of recursive definitions. defAlphaEq :: CoreDef -> CoreDef -> Bool -- | Alpha equality of expressions. exprAlphaEq :: CoreExpr -> CoreExpr -> Bool -- | Alpha equality of case alternatives. altAlphaEq :: CoreAlt -> CoreAlt -> Bool -- | Alpha equality of types. typeAlphaEq :: Type -> Type -> Bool -- | Alpha equality of coercions. coercionAlphaEq :: Coercion -> Coercion -> Bool -- | Convert a list of recursive definitions into an (isomorphic) recursive -- binding group. defsToRecBind :: [CoreDef] -> CoreBind -- | Convert a definition to an identifier/expression pair. defToIdExpr :: CoreDef -> (Id, CoreExpr) -- | Get the list of bindings in a program. progToBinds :: CoreProg -> [CoreBind] -- | Build a program from a list of bindings. Note that bindings earlier in -- the list are considered scope over bindings later in the list. bindsToProg :: [CoreBind] -> CoreProg -- | Extract the list of identifier/expression pairs from a binding group. bindToVarExprs :: CoreBind -> [(Var, CoreExpr)] -- | List all identifiers bound at the top-level in a program. progIds :: CoreProg -> [Id] -- | List all variables bound in a binding group. bindVars :: CoreBind -> [Var] -- | Return the identifier bound by a recursive definition. defId :: CoreDef -> Id -- | List the variables bound by a case alternative. altVars :: CoreAlt -> [Var] -- | Find all free variables in a program. freeVarsProg :: CoreProg -> VarSet -- | Find all free identifiers in a binding group, which excludes any -- variables bound in the group. freeVarsBind :: CoreBind -> VarSet -- | Find all free variables is a recursive definition, which excludes the -- bound variable. freeVarsDef :: CoreDef -> VarSet -- | Find all free variables in an expression. freeVarsExpr :: CoreExpr -> VarSet -- | Find all free variables in a case alternative, which excludes any -- variables bound in the alternative. freeVarsAlt :: CoreAlt -> VarSet -- | Find all free variables in a type. freeVarsType :: Type -> TyVarSet -- | Find all free variables in a coercion. freeVarsCoercion :: Coercion -> VarSet -- | Find all locally defined free variables in an expression. localFreeVarsExpr :: CoreExpr -> VarSet -- | Find all free identifiers in an expression. freeIdsExpr :: CoreExpr -> IdSet -- | Find all locally defined free identifiers in an expression. localFreeIdsExpr :: CoreExpr -> VarSet -- | Returns True iff the expression is a Coercion -- expression at its top level. isCoArg :: CoreExpr -> Bool -- | GHC's exprType function throws an error if applied to a -- Type. This function returns the Kind of a Type, -- but otherwise behaves as exprType. exprKindOrType :: CoreExpr -> KindOrType -- | GHC's exprType function throws an error if applied to a -- Type. This function catches that case as failure in an -- arbitrary monad. exprTypeM :: Monad m => CoreExpr -> m Type -- | Return the domain/codomain type of an endofunction expression. endoFunType :: Monad m => CoreExpr -> m Type -- | Return the domain and codomain types of a function type, if it is a -- function type. splitFunTypeM :: Monad m => Type -> m (Type, Type) -- | Return the domain and codomain types of a function expression. funArgResTypes :: Monad m => CoreExpr -> m (Type, Type) -- | Check two expressions have types a -> b and b -> -- a, returning (a,b). funsWithInverseTypes :: MonadCatch m => CoreExpr -> CoreExpr -> m (Type, Type) -- | Count the number of nested applications. appCount :: CoreExpr -> Int -- | Map a function over the RHS of each case alternative. mapAlts :: (CoreExpr -> CoreExpr) -> [CoreAlt] -> [CoreAlt] -- | Crumbs record a path through the tree, using descriptive constructor -- names. data Crumb ModGuts_Prog :: Crumb ProgCons_Head :: Crumb ProgCons_Tail :: Crumb NonRec_RHS :: Crumb NonRec_Var :: Crumb Rec_Def :: Int -> Crumb Def_Id :: Crumb Def_RHS :: Crumb Var_Id :: Crumb Lit_Lit :: Crumb App_Fun :: Crumb App_Arg :: Crumb Lam_Var :: Crumb Lam_Body :: Crumb Let_Bind :: Crumb Let_Body :: Crumb Case_Scrutinee :: Crumb Case_Binder :: Crumb Case_Type :: Crumb Case_Alt :: Int -> Crumb Cast_Expr :: Crumb Cast_Co :: Crumb Tick_Tick :: Crumb Tick_Expr :: Crumb Type_Type :: Crumb Co_Co :: Crumb Alt_Con :: Crumb Alt_Var :: Int -> Crumb Alt_RHS :: Crumb TyVarTy_TyVar :: Crumb LitTy_TyLit :: Crumb AppTy_Fun :: Crumb AppTy_Arg :: Crumb TyConApp_TyCon :: Crumb TyConApp_Arg :: Int -> Crumb FunTy_Dom :: Crumb FunTy_CoDom :: Crumb ForAllTy_Var :: Crumb ForAllTy_Body :: Crumb Refl_Type :: Crumb TyConAppCo_TyCon :: Crumb TyConAppCo_Arg :: Int -> Crumb AppCo_Fun :: Crumb AppCo_Arg :: Crumb ForAllCo_TyVar :: Crumb ForAllCo_Body :: Crumb CoVarCo_CoVar :: Crumb AxiomInstCo_Axiom :: Crumb AxiomInstCo_Index :: Crumb AxiomInstCo_Arg :: Int -> Crumb UnsafeCo_Left :: Crumb UnsafeCo_Right :: Crumb SymCo_Co :: Crumb TransCo_Left :: Crumb TransCo_Right :: Crumb NthCo_Int :: Crumb NthCo_Co :: Crumb InstCo_Co :: Crumb InstCo_Type :: Crumb LRCo_LR :: Crumb LRCo_Co :: Crumb showCrumbs :: [Crumb] -> String -- | Converts a Crumb into the Crumb pointing to its -- left-sibling, if a such a Crumb exists. This is for backwards -- compatibility purposes with the old Int representation. deprecatedLeftSibling :: Crumb -> Maybe Crumb -- | Converts a Crumb into the Crumb pointing to its -- right-sibling, if a such a Crumb exists. This is for backwards -- compatibility purposes with the old Int representation. deprecatedRightSibling :: Crumb -> Maybe Crumb instance Eq Crumb instance Read Crumb instance Show Crumb module HERMIT.Context type AbsolutePathH = AbsolutePath Crumb type LocalPathH = LocalPath Crumb -- | The HERMIT context, containing all bindings in scope and the current -- location in the AST. The bindings here are lazy by choice, so that we -- can avoid the cost of building the context if we never use it. data HermitC -- | Create the initial HERMIT HermitC by providing a -- ModGuts. initHermitC :: ModGuts -> HermitC -- | HERMIT's representation of variable bindings. Bound expressions cannot -- be inlined without checking for shadowing issues (using the depth -- information). data HermitBindingSite -- | A lambda-bound variable. LAM :: HermitBindingSite -- | A non-recursive binding of an expression. NONREC :: CoreExpr -> HermitBindingSite -- | A (potentially) recursive binding of an expression. REC :: CoreExpr -> HermitBindingSite -- | A (potentially) recursive binding of a superexpression of the current -- node. SELFREC :: HermitBindingSite -- | A variable bound in a case alternative. CASEALT :: HermitBindingSite -- | A case wildcard binder. We store both the scrutinised expression, and -- the case alternative AltCon and variables. CASEWILD :: CoreExpr -> (AltCon, [Var]) -> HermitBindingSite -- | A universally quantified type variable. FORALL :: HermitBindingSite -- | The depth of a binding. Used, for example, to detect shadowing when -- inlining. type BindingDepth = Int type HermitBinding = (BindingDepth, HermitBindingSite) -- | Retrieve the expression in a HermitBindingSite, if there is -- one. hermitBindingSiteExpr :: HermitBindingSite -> KureM CoreExpr -- | Retrieve the expression in a HermitBinding, if there is one. hermitBindingExpr :: HermitBinding -> KureM CoreExpr -- | A class of contexts that can have HERMIT bindings added to them. class AddBindings c addHermitBindings :: AddBindings c => [(Var, HermitBindingSite)] -> c -> c -- | Add all bindings in a binding group to a context. addBindingGroup :: AddBindings c => CoreBind -> c -> c -- | Add the binding for a recursive definition currently under -- examination. Note that because the expression may later be modified, -- the context only records the identifier, not the expression. addDefBinding :: AddBindings c => Id -> c -> c -- | Add a list of recursive bindings to the context, except the nth -- binding in the list. The idea is to exclude the definition being -- descended into. addDefBindingsExcept :: AddBindings c => Int -> [(Id, CoreExpr)] -> c -> c -- | Add a lambda bound variable to a context. All that is known is the -- variable, which may shadow something. If so, we don't worry about that -- here, it is instead checked during inlining. addLambdaBinding :: AddBindings c => Var -> c -> c -- | Add the variables bound by a DataCon in a case. They are all -- bound at the same depth. addAltBindings :: AddBindings c => [Var] -> c -> c -- | Add a wildcard binding for a specific case alternative. addCaseWildBinding :: AddBindings c => (Id, CoreExpr, CoreAlt) -> c -> c -- | Add a universally quantified type variable to a context. addForallBinding :: AddBindings c => TyVar -> c -> c -- | A class of contexts that stores the set of variables in scope that -- have been bound during the traversal. class BoundVars c boundVars :: BoundVars c => c -> VarSet -- | Determine if a variable is bound in a context. boundIn :: ReadBindings c => Var -> c -> Bool -- | List all variables bound in the context that match the given name. findBoundVars :: BoundVars c => Name -> c -> VarSet -- | A class of contexts from which HERMIT bindings can be retrieved. class BoundVars c => ReadBindings c hermitDepth :: ReadBindings c => c -> BindingDepth hermitBindings :: ReadBindings c => c -> Map Var HermitBinding -- | Lookup the binding for a variable in a context. lookupHermitBinding :: (ReadBindings c, Monad m) => Var -> c -> m HermitBinding -- | Lookup the depth of a variable's binding in a context. lookupHermitBindingDepth :: (ReadBindings c, Monad m) => Var -> c -> m BindingDepth -- | Lookup the binding for a variable in a context, ensuring it was bound -- at the specified depth. lookupHermitBindingSite :: (ReadBindings c, Monad m) => Var -> BindingDepth -> c -> m HermitBindingSite -- | A class of contexts that store the Global Reader Environment. class HasGlobalRdrEnv c hermitGlobalRdrEnv :: HasGlobalRdrEnv c => c -> GlobalRdrEnv -- | A class of contexts that store GHC rewrite rules. class HasCoreRules c hermitCoreRules :: HasCoreRules c => c -> [CoreRule] instance HasGlobalRdrEnv HermitC instance HasCoreRules HermitC instance ReadBindings HermitC instance BoundVars HermitC instance AddBindings HermitC instance ExtendPath HermitC Crumb instance ReadPath HermitC Crumb instance HasGlobalRdrEnv GlobalRdrEnv instance HasCoreRules [CoreRule] instance BoundVars VarSet instance (AddBindings c, AddBindings e) => AddBindings (ExtendContext c e) instance AddBindings (SnocPath crumb) module HERMIT.Kure.SumTypes -- | Core is a sum type for use by KURE. Core = ModGuts + CoreProg + -- CoreBind + CoreDef + CoreExpr + CoreAlt data Core -- | The module. GutsCore :: ModGuts -> Core -- | A program (a telescope of top-level binding groups). ProgCore :: CoreProg -> Core -- | A binding group. BindCore :: CoreBind -> Core -- | A recursive definition. DefCore :: CoreDef -> Core -- | An expression. ExprCore :: CoreExpr -> Core -- | A case alternative. AltCore :: CoreAlt -> Core -- | TyCo is a sum type for use by KURE. TyCo = Type + Coercion data TyCo -- | A type. TypeCore :: Type -> TyCo -- | A coercion. CoercionCore :: Coercion -> TyCo -- | CoreTC is a sum type for use by KURE. CoreTC = Core + TyCo data CoreTC Core :: Core -> CoreTC TyCo :: TyCo -> CoreTC -- | Syntactic equality of Core fragments. coreSyntaxEq :: Core -> Core -> Bool -- | Syntactic equality of TyCo fragments. tyCoSyntaxEq :: TyCo -> TyCo -> Bool -- | Syntactic equality of CoreTC fragments. coreTCSyntaxEq :: CoreTC -> CoreTC -> Bool -- | Alpha equality of Core fragments. coreAlphaEq :: Core -> Core -> Bool -- | Alpha equality of TyCo fragments. tyCoAlphaEq :: TyCo -> TyCo -> Bool -- | Alpha equality of CoreTC fragments. coreTCAlphaEq :: CoreTC -> CoreTC -> Bool -- | Find all free variables in a Core node. freeVarsCore :: Core -> VarSet -- | Find all free variables in a TyCo node. freeVarsTyCo :: TyCo -> VarSet -- | Find all free variables in a CoreTC node. freeVarsCoreTC :: CoreTC -> VarSet -- | Promote a translate on ModGuts. promoteModGutsT :: (Monad m, Injection ModGuts g) => Translate c m ModGuts b -> Translate c m g b -- | Promote a translate on CoreProg. promoteProgT :: (Monad m, Injection CoreProg g) => Translate c m CoreProg b -> Translate c m g b -- | Promote a translate on CoreBind. promoteBindT :: (Monad m, Injection CoreBind g) => Translate c m CoreBind b -> Translate c m g b -- | Promote a translate on CoreDef. promoteDefT :: (Monad m, Injection CoreDef g) => Translate c m CoreDef b -> Translate c m g b -- | Promote a translate on CoreExpr. promoteExprT :: (Monad m, Injection CoreExpr g) => Translate c m CoreExpr b -> Translate c m g b -- | Promote a translate on CoreAlt. promoteAltT :: (Monad m, Injection CoreAlt g) => Translate c m CoreAlt b -> Translate c m g b -- | Promote a translate on Type. promoteTypeT :: (Monad m, Injection Type g) => Translate c m Type b -> Translate c m g b -- | Promote a translate on Coercion. promoteCoercionT :: (Monad m, Injection Coercion g) => Translate c m Coercion b -> Translate c m g b -- | Promote a rewrite on ModGuts. promoteModGutsR :: (Monad m, Injection ModGuts g) => Rewrite c m ModGuts -> Rewrite c m g -- | Promote a rewrite on CoreProg. promoteProgR :: (Monad m, Injection CoreProg g) => Rewrite c m CoreProg -> Rewrite c m g -- | Promote a rewrite on CoreBind. promoteBindR :: (Monad m, Injection CoreBind g) => Rewrite c m CoreBind -> Rewrite c m g -- | Promote a rewrite on CoreDef. promoteDefR :: (Monad m, Injection CoreDef g) => Rewrite c m CoreDef -> Rewrite c m g -- | Promote a rewrite on CoreExpr. promoteExprR :: (Monad m, Injection CoreExpr g) => Rewrite c m CoreExpr -> Rewrite c m g -- | Promote a rewrite on CoreAlt. promoteAltR :: (Monad m, Injection CoreAlt g) => Rewrite c m CoreAlt -> Rewrite c m g -- | Promote a rewrite on Type. promoteTypeR :: (Monad m, Injection Type g) => Rewrite c m Type -> Rewrite c m g -- | Promote a rewrite on Coercion. promoteCoercionR :: (Monad m, Injection Coercion g) => Rewrite c m Coercion -> Rewrite c m g -- | Promote a bidirectional rewrite on CoreExpr. promoteExprBiR :: (Monad m, Injection CoreExpr g) => BiRewrite c m CoreExpr -> BiRewrite c m g instance Injection Coercion CoreTC instance Injection Type CoreTC instance Injection CoreExpr CoreTC instance Injection CoreAlt CoreTC instance Injection CoreDef CoreTC instance Injection CoreBind CoreTC instance Injection CoreProg CoreTC instance Injection ModGuts CoreTC instance Injection TyCo CoreTC instance Injection Core CoreTC instance Injection Coercion TyCo instance Injection Type TyCo instance Injection CoreExpr Core instance Injection CoreAlt Core instance Injection CoreDef Core instance Injection CoreBind Core instance Injection CoreProg Core instance Injection ModGuts Core module HERMIT.Monad -- | The HERMIT monad is kept abstract. data HermitM a -- | Eliminator for HermitM. runHM :: HermitMEnv -> DefStash -> (DefStash -> a -> CoreM b) -> (String -> CoreM b) -> HermitM a -> CoreM b -- | CoreM can be lifted to HermitM. liftCoreM :: CoreM a -> HermitM a -- | Make a unique global identifier for a specified type, using a provided -- name. newGlobalIdH :: String -> Type -> HermitM Id -- | Make a unique identifier for a specified type, using a provided name. newIdH :: String -> Type -> HermitM Id -- | Make a unique type variable for a specified kind, using a provided -- name. newTyVarH :: String -> Kind -> HermitM TyVar -- | Make a unique coercion variable for a specified type, using a provided -- name. newCoVarH :: String -> Type -> HermitM TyVar -- | Make a new variable of the same type, with a modified textual name. cloneVarH :: (String -> String) -> Var -> HermitM Var -- | A label for individual definitions. type Label = String -- | A store of saved definitions. type DefStash = Map Label CoreDef -- | Save a definition for future use. saveDef :: Label -> CoreDef -> HermitM () -- | Lookup a previously saved definition. lookupDef :: Label -> HermitM CoreDef -- | Get the stash of saved definitions. getStash :: HermitM DefStash -- | A way of sending messages to top level newtype HermitMEnv HermitMEnv :: (DebugMessage -> HermitM ()) -> HermitMEnv hs_debugChan :: HermitMEnv -> DebugMessage -> HermitM () -- | A message packet. data DebugMessage DebugTick :: String -> DebugMessage DebugCore :: String -> HermitC -> CoreTC -> DebugMessage mkHermitMEnv :: (DebugMessage -> HermitM ()) -> HermitMEnv sendDebugMessage :: DebugMessage -> HermitM () instance HasDynFlags HermitM instance MonadThings HermitM instance MonadUnique HermitM instance MonadIO HermitM instance MonadCatch HermitM instance Monad HermitM instance Applicative HermitM instance Functor HermitM module HERMIT.Kure type TranslateH a b = Translate HermitC HermitM a b type RewriteH a = Rewrite HermitC HermitM a type BiRewriteH a = BiRewrite HermitC HermitM a type LensH a b = Lens HermitC HermitM a b type PathH = Path Crumb -- | Translate a module. Slightly different to the other congruence -- combinators: it passes in all of the original to the -- reconstruction function. modGutsT :: (ExtendPath c Crumb, Monad m) => Translate c m CoreProg a -> (ModGuts -> a -> b) -> Translate c m ModGuts b -- | Rewrite the CoreProg child of a module. modGutsR :: (ExtendPath c Crumb, Monad m) => Rewrite c m CoreProg -> Rewrite c m ModGuts -- | Translate an empty list. progNilT :: Monad m => b -> Translate c m CoreProg b -- | Translate a program of the form: (CoreBind : -- CoreProg) progConsT :: (ExtendPath c Crumb, AddBindings c, Monad m) => Translate c m CoreBind a1 -> Translate c m CoreProg a2 -> (a1 -> a2 -> b) -> Translate c m CoreProg b -- | Rewrite all children of a program of the form: (CoreBind -- : CoreProg) progConsAllR :: (ExtendPath c Crumb, AddBindings c, Monad m) => Rewrite c m CoreBind -> Rewrite c m CoreProg -> Rewrite c m CoreProg -- | Rewrite any children of a program of the form: (CoreBind -- : CoreProg) progConsAnyR :: (ExtendPath c Crumb, AddBindings c, MonadCatch m) => Rewrite c m CoreBind -> Rewrite c m CoreProg -> Rewrite c m CoreProg -- | Rewrite one child of a program of the form: (CoreBind -- : CoreProg) progConsOneR :: (ExtendPath c Crumb, AddBindings c, MonadCatch m) => Rewrite c m CoreBind -> Rewrite c m CoreProg -> Rewrite c m CoreProg -- | Translate a binding group of the form: NonRec Var -- CoreExpr nonRecT :: (ExtendPath c Crumb, Monad m) => Translate c m Var a1 -> Translate c m CoreExpr a2 -> (a1 -> a2 -> b) -> Translate c m CoreBind b -- | Rewrite all children of a binding group of the form: NonRec -- Var CoreExpr nonRecAllR :: (ExtendPath c Crumb, Monad m) => Rewrite c m Var -> Rewrite c m CoreExpr -> Rewrite c m CoreBind -- | Rewrite any children of a binding group of the form: NonRec -- Var CoreExpr nonRecAnyR :: (ExtendPath c Crumb, MonadCatch m) => Rewrite c m Var -> Rewrite c m CoreExpr -> Rewrite c m CoreBind -- | Rewrite one child of a binding group of the form: NonRec -- Var CoreExpr nonRecOneR :: (ExtendPath c Crumb, MonadCatch m) => Rewrite c m Var -> Rewrite c m CoreExpr -> Rewrite c m CoreBind -- | Translate a binding group of the form: Rec [CoreDef] recT :: (ExtendPath c Crumb, AddBindings c, Monad m) => (Int -> Translate c m CoreDef a) -> ([a] -> b) -> Translate c m CoreBind b -- | Rewrite all children of a binding group of the form: Rec -- [CoreDef] recAllR :: (ExtendPath c Crumb, AddBindings c, Monad m) => (Int -> Rewrite c m CoreDef) -> Rewrite c m CoreBind -- | Rewrite any children of a binding group of the form: Rec -- [CoreDef] recAnyR :: (ExtendPath c Crumb, AddBindings c, MonadCatch m) => (Int -> Rewrite c m CoreDef) -> Rewrite c m CoreBind -- | Rewrite one child of a binding group of the form: Rec -- [CoreDef] recOneR :: (ExtendPath c Crumb, AddBindings c, MonadCatch m) => (Int -> Rewrite c m CoreDef) -> Rewrite c m CoreBind -- | Translate a recursive definition of the form: Def Id -- CoreExpr defT :: (ExtendPath c Crumb, AddBindings c, Monad m) => Translate c m Id a1 -> Translate c m CoreExpr a2 -> (a1 -> a2 -> b) -> Translate c m CoreDef b -- | Rewrite all children of a recursive definition of the form: -- Def Id CoreExpr defAllR :: (ExtendPath c Crumb, AddBindings c, Monad m) => Rewrite c m Id -> Rewrite c m CoreExpr -> Rewrite c m CoreDef -- | Rewrite any children of a recursive definition of the form: -- Def Id CoreExpr defAnyR :: (ExtendPath c Crumb, AddBindings c, MonadCatch m) => Rewrite c m Id -> Rewrite c m CoreExpr -> Rewrite c m CoreDef -- | Rewrite one child of a recursive definition of the form: Def -- Id CoreExpr defOneR :: (ExtendPath c Crumb, AddBindings c, MonadCatch m) => Rewrite c m Id -> Rewrite c m CoreExpr -> Rewrite c m CoreDef -- | Translate a case alternative of the form: (AltCon, -- [Var], CoreExpr) altT :: (ExtendPath c Crumb, AddBindings c, Monad m) => Translate c m AltCon a1 -> (Int -> Translate c m Var a2) -> Translate c m CoreExpr a3 -> (a1 -> [a2] -> a3 -> b) -> Translate c m CoreAlt b -- | Rewrite all children of a case alternative of the form: -- (AltCon, Id, CoreExpr) altAllR :: (ExtendPath c Crumb, AddBindings c, Monad m) => Rewrite c m AltCon -> (Int -> Rewrite c m Var) -> Rewrite c m CoreExpr -> Rewrite c m CoreAlt -- | Rewrite any children of a case alternative of the form: -- (AltCon, Id, CoreExpr) altAnyR :: (ExtendPath c Crumb, AddBindings c, MonadCatch m) => Rewrite c m AltCon -> (Int -> Rewrite c m Var) -> Rewrite c m CoreExpr -> Rewrite c m CoreAlt -- | Rewrite one child of a case alternative of the form: (AltCon, -- Id, CoreExpr) altOneR :: (ExtendPath c Crumb, AddBindings c, MonadCatch m) => Rewrite c m AltCon -> (Int -> Rewrite c m Var) -> Rewrite c m CoreExpr -> Rewrite c m CoreAlt -- | Translate an expression of the form: Var Id varT :: (ExtendPath c Crumb, Monad m) => Translate c m Id b -> Translate c m CoreExpr b -- | Rewrite the Id child in an expression of the form: Var -- Id varR :: (ExtendPath c Crumb, Monad m) => Rewrite c m Id -> Rewrite c m CoreExpr -- | Translate an expression of the form: Lit Literal litT :: (ExtendPath c Crumb, Monad m) => Translate c m Literal b -> Translate c m CoreExpr b -- | Rewrite the Literal child in an expression of the form: -- Lit Literal litR :: (ExtendPath c Crumb, Monad m) => Rewrite c m Literal -> Rewrite c m CoreExpr -- | Translate an expression of the form: App CoreExpr -- CoreExpr appT :: (ExtendPath c Crumb, Monad m) => Translate c m CoreExpr a1 -> Translate c m CoreExpr a2 -> (a1 -> a2 -> b) -> Translate c m CoreExpr b -- | Rewrite all children of an expression of the form: App -- CoreExpr CoreExpr appAllR :: (ExtendPath c Crumb, Monad m) => Rewrite c m CoreExpr -> Rewrite c m CoreExpr -> Rewrite c m CoreExpr -- | Rewrite any children of an expression of the form: App -- CoreExpr CoreExpr appAnyR :: (ExtendPath c Crumb, MonadCatch m) => Rewrite c m CoreExpr -> Rewrite c m CoreExpr -> Rewrite c m CoreExpr -- | Rewrite one child of an expression of the form: App -- CoreExpr CoreExpr appOneR :: (ExtendPath c Crumb, MonadCatch m) => Rewrite c m CoreExpr -> Rewrite c m CoreExpr -> Rewrite c m CoreExpr -- | Translate an expression of the form: Lam Var -- CoreExpr lamT :: (ExtendPath c Crumb, AddBindings c, Monad m) => Translate c m Var a1 -> Translate c m CoreExpr a2 -> (a1 -> a2 -> b) -> Translate c m CoreExpr b -- | Rewrite all children of an expression of the form: Lam -- Var CoreExpr lamAllR :: (ExtendPath c Crumb, AddBindings c, Monad m) => Rewrite c m Var -> Rewrite c m CoreExpr -> Rewrite c m CoreExpr -- | Rewrite any children of an expression of the form: Lam -- Var CoreExpr lamAnyR :: (ExtendPath c Crumb, AddBindings c, MonadCatch m) => Rewrite c m Var -> Rewrite c m CoreExpr -> Rewrite c m CoreExpr -- | Rewrite one child of an expression of the form: Lam -- Var CoreExpr lamOneR :: (ExtendPath c Crumb, AddBindings c, MonadCatch m) => Rewrite c m Var -> Rewrite c m CoreExpr -> Rewrite c m CoreExpr -- | Translate an expression of the form: Let CoreBind -- CoreExpr letT :: (ExtendPath c Crumb, AddBindings c, Monad m) => Translate c m CoreBind a1 -> Translate c m CoreExpr a2 -> (a1 -> a2 -> b) -> Translate c m CoreExpr b -- | Rewrite all children of an expression of the form: Let -- CoreBind CoreExpr letAllR :: (ExtendPath c Crumb, AddBindings c, Monad m) => Rewrite c m CoreBind -> Rewrite c m CoreExpr -> Rewrite c m CoreExpr -- | Rewrite any children of an expression of the form: Let -- CoreBind CoreExpr letAnyR :: (ExtendPath c Crumb, AddBindings c, MonadCatch m) => Rewrite c m CoreBind -> Rewrite c m CoreExpr -> Rewrite c m CoreExpr -- | Rewrite one child of an expression of the form: Let -- CoreBind CoreExpr letOneR :: (ExtendPath c Crumb, AddBindings c, MonadCatch m) => Rewrite c m CoreBind -> Rewrite c m CoreExpr -> Rewrite c m CoreExpr -- | Translate an expression of the form: Case CoreExpr -- Id Type [CoreAlt] caseT :: (ExtendPath c Crumb, AddBindings c, Monad m) => Translate c m CoreExpr e -> Translate c m Id w -> Translate c m Type ty -> (Int -> Translate c m CoreAlt alt) -> (e -> w -> ty -> [alt] -> b) -> Translate c m CoreExpr b -- | Rewrite all children of an expression of the form: Case -- CoreExpr Id Type [CoreAlt] caseAllR :: (ExtendPath c Crumb, AddBindings c, Monad m) => Rewrite c m CoreExpr -> Rewrite c m Id -> Rewrite c m Type -> (Int -> Rewrite c m CoreAlt) -> Rewrite c m CoreExpr -- | Rewrite any children of an expression of the form: Case -- CoreExpr Id Type [CoreAlt] caseAnyR :: (ExtendPath c Crumb, AddBindings c, MonadCatch m) => Rewrite c m CoreExpr -> Rewrite c m Id -> Rewrite c m Type -> (Int -> Rewrite c m CoreAlt) -> Rewrite c m CoreExpr -- | Rewrite one child of an expression of the form: Case -- CoreExpr Id Type [CoreAlt] caseOneR :: (ExtendPath c Crumb, AddBindings c, MonadCatch m) => Rewrite c m CoreExpr -> Rewrite c m Id -> Rewrite c m Type -> (Int -> Rewrite c m CoreAlt) -> Rewrite c m CoreExpr -- | Translate an expression of the form: Cast CoreExpr -- Coercion castT :: (ExtendPath c Crumb, Monad m) => Translate c m CoreExpr a1 -> Translate c m Coercion a2 -> (a1 -> a2 -> b) -> Translate c m CoreExpr b -- | Rewrite all children of an expression of the form: Cast -- CoreExpr Coercion castAllR :: (ExtendPath c Crumb, Monad m) => Rewrite c m CoreExpr -> Rewrite c m Coercion -> Rewrite c m CoreExpr -- | Rewrite any children of an expression of the form: Cast -- CoreExpr Coercion castAnyR :: (ExtendPath c Crumb, MonadCatch m) => Rewrite c m CoreExpr -> Rewrite c m Coercion -> Rewrite c m CoreExpr -- | Rewrite one child of an expression of the form: Cast -- CoreExpr Coercion castOneR :: (ExtendPath c Crumb, MonadCatch m) => Rewrite c m CoreExpr -> Rewrite c m Coercion -> Rewrite c m CoreExpr -- | Translate an expression of the form: Tick CoreTickish -- CoreExpr tickT :: (ExtendPath c Crumb, Monad m) => Translate c m CoreTickish a1 -> Translate c m CoreExpr a2 -> (a1 -> a2 -> b) -> Translate c m CoreExpr b -- | Rewrite all children of an expression of the form: Tick -- CoreTickish CoreExpr tickAllR :: (ExtendPath c Crumb, Monad m) => Rewrite c m CoreTickish -> Rewrite c m CoreExpr -> Rewrite c m CoreExpr -- | Rewrite any children of an expression of the form: Tick -- CoreTickish CoreExpr tickAnyR :: (ExtendPath c Crumb, MonadCatch m) => Rewrite c m CoreTickish -> Rewrite c m CoreExpr -> Rewrite c m CoreExpr -- | Rewrite any children of an expression of the form: Tick -- CoreTickish CoreExpr tickOneR :: (ExtendPath c Crumb, MonadCatch m) => Rewrite c m CoreTickish -> Rewrite c m CoreExpr -> Rewrite c m CoreExpr -- | Translate an expression of the form: Type Type typeT :: (ExtendPath c Crumb, Monad m) => Translate c m Type b -> Translate c m CoreExpr b -- | Rewrite the Type child in an expression of the form: -- Type Type typeR :: (ExtendPath c Crumb, Monad m) => Rewrite c m Type -> Rewrite c m CoreExpr -- | Translate an expression of the form: Coercion Coercion coercionT :: (ExtendPath c Crumb, Monad m) => Translate c m Coercion b -> Translate c m CoreExpr b -- | Rewrite the Coercion child in an expression of the form: -- Coercion Coercion coercionR :: (ExtendPath c Crumb, Monad m) => Rewrite c m Coercion -> Rewrite c m CoreExpr -- | Translate a definition of the form NonRec Var -- CoreExpr or Def Id CoreExpr defOrNonRecT :: (Injection CoreBind g, Injection CoreDef g, ExtendPath c Crumb, AddBindings c, MonadCatch m) => Translate c m Var a1 -> Translate c m CoreExpr a2 -> (a1 -> a2 -> b) -> Translate c m g b -- | Rewrite all children of a definition of the form NonRec Var -- CoreExpr or Def Id CoreExpr defOrNonRecAllR :: (Injection CoreBind g, Injection CoreDef g, ExtendPath c Crumb, AddBindings c, MonadCatch m) => Rewrite c m Var -> Rewrite c m CoreExpr -> Rewrite c m g -- | Rewrite any children of a definition of the form NonRec Var -- CoreExpr or Def Id CoreExpr defOrNonRecAnyR :: (Injection CoreBind g, Injection CoreDef g, ExtendPath c Crumb, AddBindings c, MonadCatch m) => Rewrite c m Var -> Rewrite c m CoreExpr -> Rewrite c m g -- | Rewrite one child of a definition of the form NonRec Var -- CoreExpr or Def Id CoreExpr defOrNonRecOneR :: (Injection CoreBind g, Injection CoreDef g, ExtendPath c Crumb, AddBindings c, MonadCatch m) => Rewrite c m Var -> Rewrite c m CoreExpr -> Rewrite c m g -- | Translate a binding group of the form: Rec [(Id, -- CoreExpr)] recDefT :: (ExtendPath c Crumb, AddBindings c, Monad m) => (Int -> (Translate c m Id a1, Translate c m CoreExpr a2)) -> ([(a1, a2)] -> b) -> Translate c m CoreBind b -- | Rewrite all children of a binding group of the form: Rec -- [(Id, CoreExpr)] recDefAllR :: (ExtendPath c Crumb, AddBindings c, Monad m) => (Int -> (Rewrite c m Id, Rewrite c m CoreExpr)) -> Rewrite c m CoreBind -- | Rewrite any children of a binding group of the form: Rec -- [(Id, CoreExpr)] recDefAnyR :: (ExtendPath c Crumb, AddBindings c, MonadCatch m) => (Int -> (Rewrite c m Id, Rewrite c m CoreExpr)) -> Rewrite c m CoreBind -- | Rewrite one child of a binding group of the form: Rec -- [(Id, CoreExpr)] recDefOneR :: (ExtendPath c Crumb, AddBindings c, MonadCatch m) => (Int -> (Rewrite c m Id, Rewrite c m CoreExpr)) -> Rewrite c m CoreBind -- | Translate an expression of the form: Let (NonRec -- Var CoreExpr) CoreExpr letNonRecT :: (ExtendPath c Crumb, AddBindings c, Monad m) => Translate c m Var a1 -> Translate c m CoreExpr a2 -> Translate c m CoreExpr a3 -> (a1 -> a2 -> a3 -> b) -> Translate c m CoreExpr b -- | Rewrite all children of an expression of the form: Let -- (NonRec Var CoreExpr) CoreExpr letNonRecAllR :: (ExtendPath c Crumb, AddBindings c, Monad m) => Rewrite c m Var -> Rewrite c m CoreExpr -> Rewrite c m CoreExpr -> Rewrite c m CoreExpr -- | Rewrite any children of an expression of the form: Let -- (NonRec Var CoreExpr) CoreExpr letNonRecAnyR :: (ExtendPath c Crumb, AddBindings c, MonadCatch m) => Rewrite c m Var -> Rewrite c m CoreExpr -> Rewrite c m CoreExpr -> Rewrite c m CoreExpr -- | Rewrite one child of an expression of the form: Let -- (NonRec Var CoreExpr) CoreExpr letNonRecOneR :: (ExtendPath c Crumb, AddBindings c, MonadCatch m) => Rewrite c m Var -> Rewrite c m CoreExpr -> Rewrite c m CoreExpr -> Rewrite c m CoreExpr -- | Translate an expression of the form: Let (Rec -- [CoreDef]) CoreExpr letRecT :: (ExtendPath c Crumb, AddBindings c, Monad m) => (Int -> Translate c m CoreDef a1) -> Translate c m CoreExpr a2 -> ([a1] -> a2 -> b) -> Translate c m CoreExpr b -- | Rewrite all children of an expression of the form: Let -- (Rec [CoreDef]) CoreExpr letRecAllR :: (ExtendPath c Crumb, AddBindings c, Monad m) => (Int -> Rewrite c m CoreDef) -> Rewrite c m CoreExpr -> Rewrite c m CoreExpr -- | Rewrite any children of an expression of the form: Let -- (Rec [CoreDef]) CoreExpr letRecAnyR :: (ExtendPath c Crumb, AddBindings c, MonadCatch m) => (Int -> Rewrite c m CoreDef) -> Rewrite c m CoreExpr -> Rewrite c m CoreExpr -- | Rewrite one child of an expression of the form: Let -- (Rec [CoreDef]) CoreExpr letRecOneR :: (ExtendPath c Crumb, AddBindings c, MonadCatch m) => (Int -> Rewrite c m CoreDef) -> Rewrite c m CoreExpr -> Rewrite c m CoreExpr -- | Translate an expression of the form: Let (Rec -- [(Id, CoreExpr)]) CoreExpr letRecDefT :: (ExtendPath c Crumb, AddBindings c, Monad m) => (Int -> (Translate c m Id a1, Translate c m CoreExpr a2)) -> Translate c m CoreExpr a3 -> ([(a1, a2)] -> a3 -> b) -> Translate c m CoreExpr b -- | Rewrite all children of an expression of the form: Let -- (Rec [(Id, CoreExpr)]) CoreExpr letRecDefAllR :: (ExtendPath c Crumb, AddBindings c, Monad m) => (Int -> (Rewrite c m Id, Rewrite c m CoreExpr)) -> Rewrite c m CoreExpr -> Rewrite c m CoreExpr -- | Rewrite any children of an expression of the form: Let -- (Rec [(Id, CoreExpr)]) CoreExpr letRecDefAnyR :: (ExtendPath c Crumb, AddBindings c, MonadCatch m) => (Int -> (Rewrite c m Id, Rewrite c m CoreExpr)) -> Rewrite c m CoreExpr -> Rewrite c m CoreExpr -- | Rewrite one child of an expression of the form: Let -- (Rec [(Id, CoreExpr)]) CoreExpr letRecDefOneR :: (ExtendPath c Crumb, AddBindings c, MonadCatch m) => (Int -> (Rewrite c m Id, Rewrite c m CoreExpr)) -> Rewrite c m CoreExpr -> Rewrite c m CoreExpr -- | Translate a program of the form: (NonRec Var -- CoreExpr) : CoreProg consNonRecT :: (ExtendPath c Crumb, AddBindings c, Monad m) => Translate c m Var a1 -> Translate c m CoreExpr a2 -> Translate c m CoreProg a3 -> (a1 -> a2 -> a3 -> b) -> Translate c m CoreProg b -- | Rewrite all children of an expression of the form: (NonRec -- Var CoreExpr) : CoreProg consNonRecAllR :: (ExtendPath c Crumb, AddBindings c, Monad m) => Rewrite c m Var -> Rewrite c m CoreExpr -> Rewrite c m CoreProg -> Rewrite c m CoreProg -- | Rewrite any children of an expression of the form: (NonRec -- Var CoreExpr) : CoreProg consNonRecAnyR :: (ExtendPath c Crumb, AddBindings c, MonadCatch m) => Rewrite c m Var -> Rewrite c m CoreExpr -> Rewrite c m CoreProg -> Rewrite c m CoreProg -- | Rewrite one child of an expression of the form: (NonRec -- Var CoreExpr) : CoreProg consNonRecOneR :: (ExtendPath c Crumb, AddBindings c, MonadCatch m) => Rewrite c m Var -> Rewrite c m CoreExpr -> Rewrite c m CoreProg -> Rewrite c m CoreProg -- | Translate an expression of the form: (Rec [CoreDef]) -- : CoreProg consRecT :: (ExtendPath c Crumb, AddBindings c, Monad m) => (Int -> Translate c m CoreDef a1) -> Translate c m CoreProg a2 -> ([a1] -> a2 -> b) -> Translate c m CoreProg b -- | Rewrite all children of an expression of the form: (Rec -- [CoreDef]) : CoreProg consRecAllR :: (ExtendPath c Crumb, AddBindings c, Monad m) => (Int -> Rewrite c m CoreDef) -> Rewrite c m CoreProg -> Rewrite c m CoreProg -- | Rewrite any children of an expression of the form: (Rec -- [CoreDef]) : CoreProg consRecAnyR :: (ExtendPath c Crumb, AddBindings c, MonadCatch m) => (Int -> Rewrite c m CoreDef) -> Rewrite c m CoreProg -> Rewrite c m CoreProg -- | Rewrite one child of an expression of the form: (Rec -- [CoreDef]) : CoreProg consRecOneR :: (ExtendPath c Crumb, AddBindings c, MonadCatch m) => (Int -> Rewrite c m CoreDef) -> Rewrite c m CoreProg -> Rewrite c m CoreProg -- | Translate an expression of the form: (Rec [(Id, -- CoreExpr)]) : CoreProg consRecDefT :: (ExtendPath c Crumb, AddBindings c, Monad m) => (Int -> (Translate c m Id a1, Translate c m CoreExpr a2)) -> Translate c m CoreProg a3 -> ([(a1, a2)] -> a3 -> b) -> Translate c m CoreProg b -- | Rewrite all children of an expression of the form: (Rec -- [(Id, CoreExpr)]) : CoreProg consRecDefAllR :: (ExtendPath c Crumb, AddBindings c, Monad m) => (Int -> (Rewrite c m Id, Rewrite c m CoreExpr)) -> Rewrite c m CoreProg -> Rewrite c m CoreProg -- | Rewrite any children of an expression of the form: (Rec -- [(Id, CoreExpr)]) : CoreProg consRecDefAnyR :: (ExtendPath c Crumb, AddBindings c, MonadCatch m) => (Int -> (Rewrite c m Id, Rewrite c m CoreExpr)) -> Rewrite c m CoreProg -> Rewrite c m CoreProg -- | Rewrite one child of an expression of the form: (Rec -- [(Id, CoreExpr)]) : CoreProg consRecDefOneR :: (ExtendPath c Crumb, AddBindings c, MonadCatch m) => (Int -> (Rewrite c m Id, Rewrite c m CoreExpr)) -> Rewrite c m CoreProg -> Rewrite c m CoreProg -- | Translate an expression of the form: Case CoreExpr -- Id Type [(AltCon, [Var], CoreExpr)] caseAltT :: (ExtendPath c Crumb, AddBindings c, Monad m) => Translate c m CoreExpr sc -> Translate c m Id w -> Translate c m Type ty -> (Int -> (Translate c m AltCon con, Int -> Translate c m Var v, Translate c m CoreExpr rhs)) -> (sc -> w -> ty -> [(con, [v], rhs)] -> b) -> Translate c m CoreExpr b -- | Rewrite all children of an expression of the form: Case -- CoreExpr Id Type [(AltCon, [Var], -- CoreExpr)] caseAltAllR :: (ExtendPath c Crumb, AddBindings c, Monad m) => Rewrite c m CoreExpr -> Rewrite c m Id -> Rewrite c m Type -> (Int -> (Rewrite c m AltCon, Int -> Rewrite c m Var, Rewrite c m CoreExpr)) -> Rewrite c m CoreExpr -- | Rewrite any children of an expression of the form: Case -- CoreExpr Id Type [(AltCon, [Var], -- CoreExpr)] caseAltAnyR :: (ExtendPath c Crumb, AddBindings c, MonadCatch m) => Rewrite c m CoreExpr -> Rewrite c m Id -> Rewrite c m Type -> (Int -> (Rewrite c m AltCon, Int -> Rewrite c m Var, Rewrite c m CoreExpr)) -> Rewrite c m CoreExpr -- | Rewrite one child of an expression of the form: Case -- CoreExpr Id Type [(AltCon, [Var], -- CoreExpr)] caseAltOneR :: (ExtendPath c Crumb, AddBindings c, MonadCatch m) => Rewrite c m CoreExpr -> Rewrite c m Id -> Rewrite c m Type -> (Int -> (Rewrite c m AltCon, Int -> Rewrite c m Var, Rewrite c m CoreExpr)) -> Rewrite c m CoreExpr -- | Translate a type of the form: TyVarTy TyVar tyVarT :: (ExtendPath c Crumb, Monad m) => Translate c m TyVar b -> Translate c m Type b -- | Rewrite the TyVar child of a type of the form: TyVarTy -- TyVar tyVarR :: (ExtendPath c Crumb, Monad m) => Rewrite c m TyVar -> Rewrite c m Type -- | Translate a type of the form: LitTy TyLit litTyT :: (ExtendPath c Crumb, Monad m) => Translate c m TyLit b -> Translate c m Type b -- | Rewrite the TyLit child of a type of the form: LitTy -- TyLit litTyR :: (ExtendPath c Crumb, Monad m) => Rewrite c m TyLit -> Rewrite c m Type -- | Translate a type of the form: AppTy Type Type appTyT :: (ExtendPath c Crumb, Monad m) => Translate c m Type a1 -> Translate c m Type a2 -> (a1 -> a2 -> b) -> Translate c m Type b -- | Rewrite all children of a type of the form: AppTy Type -- Type appTyAllR :: (ExtendPath c Crumb, Monad m) => Rewrite c m Type -> Rewrite c m Type -> Rewrite c m Type -- | Rewrite any children of a type of the form: AppTy Type -- Type appTyAnyR :: (ExtendPath c Crumb, MonadCatch m) => Rewrite c m Type -> Rewrite c m Type -> Rewrite c m Type -- | Rewrite one child of a type of the form: AppTy Type -- Type appTyOneR :: (ExtendPath c Crumb, MonadCatch m) => Rewrite c m Type -> Rewrite c m Type -> Rewrite c m Type -- | Translate a type of the form: FunTy Type Type funTyT :: (ExtendPath c Crumb, Monad m) => Translate c m Type a1 -> Translate c m Type a2 -> (a1 -> a2 -> b) -> Translate c m Type b -- | Rewrite all children of a type of the form: FunTy Type -- Type funTyAllR :: (ExtendPath c Crumb, Monad m) => Rewrite c m Type -> Rewrite c m Type -> Rewrite c m Type -- | Rewrite any children of a type of the form: FunTy Type -- Type funTyAnyR :: (ExtendPath c Crumb, MonadCatch m) => Rewrite c m Type -> Rewrite c m Type -> Rewrite c m Type -- | Rewrite one child of a type of the form: FunTy Type -- Type funTyOneR :: (ExtendPath c Crumb, MonadCatch m) => Rewrite c m Type -> Rewrite c m Type -> Rewrite c m Type -- | Translate a type of the form: ForAllTy Var Type forAllTyT :: (ExtendPath c Crumb, AddBindings c, Monad m) => Translate c m Var a1 -> Translate c m Type a2 -> (a1 -> a2 -> b) -> Translate c m Type b -- | Rewrite all children of a type of the form: ForAllTy -- Var Type forAllTyAllR :: (ExtendPath c Crumb, AddBindings c, Monad m) => Rewrite c m Var -> Rewrite c m Type -> Rewrite c m Type -- | Rewrite any children of a type of the form: ForAllTy -- Var Type forAllTyAnyR :: (ExtendPath c Crumb, AddBindings c, MonadCatch m) => Rewrite c m Var -> Rewrite c m Type -> Rewrite c m Type -- | Rewrite one child of a type of the form: ForAllTy Var -- Type forAllTyOneR :: (ExtendPath c Crumb, AddBindings c, MonadCatch m) => Rewrite c m Var -> Rewrite c m Type -> Rewrite c m Type -- | Translate a type of the form: TyConApp TyCon -- [KindOrType] tyConAppT :: (ExtendPath c Crumb, Monad m) => Translate c m TyCon a1 -> (Int -> Translate c m KindOrType a2) -> (a1 -> [a2] -> b) -> Translate c m Type b -- | Rewrite all children of a type of the form: TyConApp -- TyCon [KindOrType] tyConAppAllR :: (ExtendPath c Crumb, Monad m) => Rewrite c m TyCon -> (Int -> Rewrite c m KindOrType) -> Rewrite c m Type -- | Rewrite any children of a type of the form: TyConApp -- TyCon [KindOrType] tyConAppAnyR :: (ExtendPath c Crumb, MonadCatch m) => Rewrite c m TyCon -> (Int -> Rewrite c m KindOrType) -> Rewrite c m Type -- | Rewrite one child of a type of the form: TyConApp -- TyCon [KindOrType] tyConAppOneR :: (ExtendPath c Crumb, MonadCatch m) => Rewrite c m TyCon -> (Int -> Rewrite c m KindOrType) -> Rewrite c m Type -- | Translate a coercion of the form: Refl Type reflT :: (ExtendPath c Crumb, Monad m) => Translate c m Type b -> Translate c m Coercion b -- | Rewrite the Type child of a coercion of the form: Refl -- Type reflR :: (ExtendPath c Crumb, Monad m) => Rewrite c m Type -> Rewrite c m Coercion -- | Translate a coercion of the form: TyConAppCo TyCon -- [Coercion] tyConAppCoT :: (ExtendPath c Crumb, Monad m) => Translate c m TyCon a1 -> (Int -> Translate c m Coercion a2) -> (a1 -> [a2] -> b) -> Translate c m Coercion b -- | Rewrite all children of a coercion of the form: TyConAppCo -- TyCon [Coercion] tyConAppCoAllR :: (ExtendPath c Crumb, Monad m) => Rewrite c m TyCon -> (Int -> Rewrite c m Coercion) -> Rewrite c m Coercion -- | Rewrite any children of a coercion of the form: TyConAppCo -- TyCon [Coercion] tyConAppCoAnyR :: (ExtendPath c Crumb, MonadCatch m) => Rewrite c m TyCon -> (Int -> Rewrite c m Coercion) -> Rewrite c m Coercion -- | Rewrite one child of a coercion of the form: TyConAppCo -- TyCon [Coercion] tyConAppCoOneR :: (ExtendPath c Crumb, MonadCatch m) => Rewrite c m TyCon -> (Int -> Rewrite c m Coercion) -> Rewrite c m Coercion -- | Translate a coercion of the form: AppCo Coercion -- Coercion appCoT :: (ExtendPath c Crumb, Monad m) => Translate c m Coercion a1 -> Translate c m Coercion a2 -> (a1 -> a2 -> b) -> Translate c m Coercion b -- | Rewrite all children of a coercion of the form: AppCo -- Coercion Coercion appCoAllR :: (ExtendPath c Crumb, Monad m) => Rewrite c m Coercion -> Rewrite c m Coercion -> Rewrite c m Coercion -- | Rewrite any children of a coercion of the form: AppCo -- Coercion Coercion appCoAnyR :: (ExtendPath c Crumb, MonadCatch m) => Rewrite c m Coercion -> Rewrite c m Coercion -> Rewrite c m Coercion -- | Rewrite one child of a coercion of the form: AppCo -- Coercion Coercion appCoOneR :: (ExtendPath c Crumb, MonadCatch m) => Rewrite c m Coercion -> Rewrite c m Coercion -> Rewrite c m Coercion -- | Translate a coercion of the form: ForAllCo TyVar -- Coercion forAllCoT :: (ExtendPath c Crumb, AddBindings c, Monad m) => Translate c m TyVar a1 -> Translate c m Coercion a2 -> (a1 -> a2 -> b) -> Translate c m Coercion b -- | Rewrite all children of a coercion of the form: ForAllCo -- TyVar Coercion forAllCoAllR :: (ExtendPath c Crumb, AddBindings c, Monad m) => Rewrite c m TyVar -> Rewrite c m Coercion -> Rewrite c m Coercion -- | Rewrite any children of a coercion of the form: ForAllCo -- TyVar Coercion forAllCoAnyR :: (ExtendPath c Crumb, AddBindings c, MonadCatch m) => Rewrite c m TyVar -> Rewrite c m Coercion -> Rewrite c m Coercion -- | Rewrite one child of a coercion of the form: ForAllCo -- TyVar Coercion forAllCoOneR :: (ExtendPath c Crumb, AddBindings c, MonadCatch m) => Rewrite c m TyVar -> Rewrite c m Coercion -> Rewrite c m Coercion -- | Translate a coercion of the form: CoVarCo CoVar coVarCoT :: (ExtendPath c Crumb, Monad m) => Translate c m CoVar b -> Translate c m Coercion b -- | Rewrite the CoVar child of a coercion of the form: -- CoVarCo CoVar coVarCoR :: (ExtendPath c Crumb, Monad m) => Rewrite c m CoVar -> Rewrite c m Coercion -- | Translate a coercion of the form: AxiomInstCo CoAxiom -- [Coercion] axiomInstCoT :: (ExtendPath c Crumb, Monad m) => Translate c m CoAxiom a1 -> (Int -> Translate c m Coercion a2) -> (a1 -> [a2] -> b) -> Translate c m Coercion b -- | Rewrite all children of a coercion of the form: AxiomInstCo -- CoAxiom [Coercion] axiomInstCoAllR :: (ExtendPath c Crumb, Monad m) => Rewrite c m CoAxiom -> (Int -> Rewrite c m Coercion) -> Rewrite c m Coercion -- | Rewrite any children of a coercion of the form: AxiomInstCo -- CoAxiom [Coercion] axiomInstCoAnyR :: (ExtendPath c Crumb, MonadCatch m) => Rewrite c m CoAxiom -> (Int -> Rewrite c m Coercion) -> Rewrite c m Coercion -- | Rewrite one child of a coercion of the form: AxiomInstCo -- CoAxiom [Coercion] axiomInstCoOneR :: (ExtendPath c Crumb, MonadCatch m) => Rewrite c m CoAxiom -> (Int -> Rewrite c m Coercion) -> Rewrite c m Coercion -- | Translate a coercion of the form: UnsafeCo Type -- Type unsafeCoT :: (ExtendPath c Crumb, Monad m) => Translate c m Type a1 -> Translate c m Type a2 -> (a1 -> a2 -> b) -> Translate c m Coercion b -- | Rewrite all children of a coercion of the form: UnsafeCo -- Type Type unsafeCoAllR :: (ExtendPath c Crumb, Monad m) => Rewrite c m Type -> Rewrite c m Type -> Rewrite c m Coercion -- | Rewrite any children of a coercion of the form: UnsafeCo -- Type Type unsafeCoAnyR :: (ExtendPath c Crumb, MonadCatch m) => Rewrite c m Type -> Rewrite c m Type -> Rewrite c m Coercion -- | Rewrite one child of a coercion of the form: UnsafeCo -- Type Type unsafeCoOneR :: (ExtendPath c Crumb, MonadCatch m) => Rewrite c m Type -> Rewrite c m Type -> Rewrite c m Coercion -- | Translate a coercion of the form: SymCo Coercion symCoT :: (ExtendPath c Crumb, Monad m) => Translate c m Coercion b -> Translate c m Coercion b -- | Rewrite the Coercion child of a coercion of the form: -- SymCo Coercion symCoR :: (ExtendPath c Crumb, Monad m) => Rewrite c m Coercion -> Rewrite c m Coercion -- | Translate a coercion of the form: TransCo Coercion -- Coercion transCoT :: (ExtendPath c Crumb, Monad m) => Translate c m Coercion a1 -> Translate c m Coercion a2 -> (a1 -> a2 -> b) -> Translate c m Coercion b -- | Rewrite all children of a coercion of the form: TransCo -- Coercion Coercion transCoAllR :: (ExtendPath c Crumb, Monad m) => Rewrite c m Coercion -> Rewrite c m Coercion -> Rewrite c m Coercion -- | Rewrite any children of a coercion of the form: TransCo -- Coercion Coercion transCoAnyR :: (ExtendPath c Crumb, MonadCatch m) => Rewrite c m Coercion -> Rewrite c m Coercion -> Rewrite c m Coercion -- | Rewrite one child of a coercion of the form: TransCo -- Coercion Coercion transCoOneR :: (ExtendPath c Crumb, MonadCatch m) => Rewrite c m Coercion -> Rewrite c m Coercion -> Rewrite c m Coercion -- | Translate a coercion of the form: NthCo Int -- Coercion nthCoT :: (ExtendPath c Crumb, Monad m) => Translate c m Int a1 -> Translate c m Coercion a2 -> (a1 -> a2 -> b) -> Translate c m Coercion b -- | Rewrite all children of a coercion of the form: NthCo -- Int Coercion nthCoAllR :: (ExtendPath c Crumb, Monad m) => Rewrite c m Int -> Rewrite c m Coercion -> Rewrite c m Coercion -- | Rewrite any children of a coercion of the form: NthCo -- Int Coercion nthCoAnyR :: (ExtendPath c Crumb, MonadCatch m) => Rewrite c m Int -> Rewrite c m Coercion -> Rewrite c m Coercion -- | Rewrite one child of a coercion of the form: NthCo Int -- Coercion nthCoOneR :: (ExtendPath c Crumb, MonadCatch m) => Rewrite c m Int -> Rewrite c m Coercion -> Rewrite c m Coercion -- | Translate a coercion of the form: InstCo Coercion -- Type instCoT :: (ExtendPath c Crumb, Monad m) => Translate c m Coercion a1 -> Translate c m Type a2 -> (a1 -> a2 -> b) -> Translate c m Coercion b -- | Rewrite all children of a coercion of the form: InstCo -- Coercion Type instCoAllR :: (ExtendPath c Crumb, Monad m) => Rewrite c m Coercion -> Rewrite c m Type -> Rewrite c m Coercion -- | Rewrite any children of a coercion of the form: InstCo -- Coercion Type instCoAnyR :: (ExtendPath c Crumb, MonadCatch m) => Rewrite c m Coercion -> Rewrite c m Type -> Rewrite c m Coercion -- | Rewrite one child of a coercion of the form: InstCo -- Coercion Type instCoOneR :: (ExtendPath c Crumb, MonadCatch m) => Rewrite c m Coercion -> Rewrite c m Type -> Rewrite c m Coercion -- | Earlier versions of HERMIT used Int as the crumb type. This -- translation maps an Int to the corresponding Crumb, for -- backwards compatibility purposes. deprecatedIntToCrumbT :: Monad m => Int -> Translate c m Core Crumb -- | Builds a path to the first child, based on the old numbering system. deprecatedIntToPathT :: Monad m => Int -> Translate c m Core LocalPathH instance (ExtendPath c Crumb, AddBindings c) => Walker c CoreTC instance (ExtendPath c Crumb, AddBindings c) => Walker c TyCo instance (ExtendPath c Crumb, AddBindings c) => Walker c Coercion instance (ExtendPath c Crumb, AddBindings c) => Walker c Type instance (ExtendPath c Crumb, AddBindings c) => Walker c Core -- | Note: this module should NOT export externals. It is for common -- transformations needed by the other primitive modules. module HERMIT.Dictionary.Common -- | Apply a transformation to a value in the current context. applyInContextT :: Translate c m a b -> a -> Translate c m x b -- | Lift GHC's collectArgs callT :: Monad m => Translate c m CoreExpr (CoreExpr, [CoreExpr]) callPredT :: Monad m => (Id -> [CoreExpr] -> Bool) -> Translate c m CoreExpr (CoreExpr, [CoreExpr]) -- | Succeeds if we are looking at an application of given function -- returning zero or more arguments to which it is applied. callNameT :: MonadCatch m => Name -> Translate c m CoreExpr (CoreExpr, [CoreExpr]) -- | Succeeds if we are looking at a fully saturated function call. callSaturatedT :: Monad m => Translate c m CoreExpr (CoreExpr, [CoreExpr]) -- | Succeeds if we are looking at an application of given function callNameG :: MonadCatch m => Name -> Translate c m CoreExpr () -- | Succeeds if we are looking at an application of a data constructor. callDataConT :: MonadCatch m => Translate c m CoreExpr (DataCon, [Type], [CoreExpr]) -- | Succeeds if we are looking at an application of a named data -- constructor. callDataConNameT :: MonadCatch m => Name -> Translate c m CoreExpr (DataCon, [Type], [CoreExpr]) -- | Apply a rewrite to all applications of a given function in a top-down -- manner, pruning on success. callsR :: (ExtendPath c Crumb, AddBindings c, MonadCatch m) => Name -> Rewrite c m CoreExpr -> Rewrite c m Core -- | Apply a translate to all applications of a given function in a -- top-down manner, pruning on success, collecting the results. callsT :: (ExtendPath c Crumb, AddBindings c, MonadCatch m) => Name -> Translate c m CoreExpr b -> Translate c m Core [b] -- | List the identifiers bound by the top-level binding group at the head -- of the program. progConsIdsT :: (ExtendPath c Crumb, AddBindings c, MonadCatch m) => Translate c m CoreProg [Id] -- | List the identifiers bound by a recursive top-level binding group at -- the head of the program. progConsRecIdsT :: (ExtendPath c Crumb, AddBindings c, Monad m) => Translate c m CoreProg [Id] -- | Return the identifier bound by a non-recursive top-level binding at -- the head of the program. progConsNonRecIdT :: (ExtendPath c Crumb, AddBindings c, Monad m) => Translate c m CoreProg Id -- | Return the variable bound by a non-recursive let expression. nonRecVarT :: (ExtendPath c Crumb, Monad m) => Translate c m CoreBind Var -- | List all identifiers bound in a recursive binding group. recIdsT :: (ExtendPath c Crumb, AddBindings c, Monad m) => Translate c m CoreBind [Id] -- | Return the variable bound by a lambda expression. lamVarT :: (ExtendPath c Crumb, AddBindings c, Monad m) => Translate c m CoreExpr Var -- | List the variables bound by a let expression. letVarsT :: (ExtendPath c Crumb, AddBindings c, MonadCatch m) => Translate c m CoreExpr [Var] -- | List the identifiers bound by a recursive let expression. letRecIdsT :: (ExtendPath c Crumb, AddBindings c, Monad m) => Translate c m CoreExpr [Id] -- | Return the variable bound by a non-recursive let expression. letNonRecVarT :: (ExtendPath c Crumb, AddBindings c, Monad m) => Translate c m CoreExpr Var -- | List all variables bound by a case expression (in the alternatives and -- the wildcard binder). caseVarsT :: (ExtendPath c Crumb, AddBindings c, Monad m) => Translate c m CoreExpr [Var] -- | Return the case wildcard binder. caseWildIdT :: (ExtendPath c Crumb, AddBindings c, Monad m) => Translate c m CoreExpr Id -- | List the variables bound by all alternatives in a case expression. caseAltVarsT :: (ExtendPath c Crumb, AddBindings c, Monad m) => Translate c m CoreExpr [[Var]] -- | Lifted version of boundVars. boundVarsT :: (BoundVars c, Monad m) => Translate c m a VarSet -- | Find the unique variable bound in the context that matches the given -- name, failing if it is not unique. findBoundVarT :: (BoundVars c, MonadCatch m) => Name -> Translate c m a Var -- | Lookup the name in the context first, then, failing that, in GHC's -- global reader environment. findIdT :: (BoundVars c, HasGlobalRdrEnv c, HasDynFlags m, MonadThings m, MonadCatch m) => Name -> Translate c m a Id findId :: (BoundVars c, HasGlobalRdrEnv c, HasDynFlags m, MonadThings m) => Name -> c -> m Id -- | Find the depth of a variable's binding. varBindingDepthT :: (ReadBindings c, Monad m) => Var -> Translate c m g BindingDepth -- | Determine if the current variable matches the given variable, and is -- bound at the specified depth (helpful to detect shadowing). varIsOccurrenceOfT :: (ExtendPath c Crumb, ReadBindings c, Monad m) => Var -> BindingDepth -> Translate c m Var Bool -- | Determine if the current expression is an occurrence of the given -- variable, bound at the specified depth (helpful to detect shadowing). exprIsOccurrenceOfT :: (ExtendPath c Crumb, ReadBindings c, Monad m) => Var -> BindingDepth -> Translate c m CoreExpr Bool -- | Constructs a common error message. Argument String should be -- the desired form of the expression. wrongExprForm :: String -> String module HERMIT.External -- | An External is a Dynamic value with some associated -- meta-data (name, help string and tags). data External -- | External names are just strings. type ExternalName = String -- | Help information for Externals is stored as a list of strings, -- designed for multi-line displaying. type ExternalHelp = [String] -- | Get the name of an External. externName :: External -> ExternalName -- | Get the Dynamic value stored in an External. externDyn :: External -> Dynamic -- | Get the list of help Strings for an External. externHelp :: External -> ExternalHelp -- | A Dictionary is a collection of Dynamics. Looking up a -- Dynamic (via an ExternalName key) returns a list, as -- there can be multiple Dynamics with the same name. type Dictionary = Map ExternalName [Dynamic] -- | Build a Map from names to Dynamic values. toDictionary :: [External] -> Dictionary -- | Build a Map from names to help information. toHelp :: [External] -> Map ExternalName ExternalHelp -- | The primitive way to build an External. external :: Extern a => ExternalName -> a -> ExternalHelp -> External -- | The class of things that can be made into Externals. To be an -- Extern there must exist an isomorphic Box type that is -- an instance of Typeable. class Typeable (Box a) => Extern a where type family Box a box :: Extern a => a -> Box a unbox :: Extern a => Box a -> a -- | Get all the Externals which match a given tag predicate and box -- a Translate of the appropriate type. matchingExternals :: (Extern tr, Tag t) => t -> [External] -> [(External, tr)] -- | Requirement: commands cannot have the same name as any CmdTag -- (or the help function will not find it). These should be user -- facing, because they give the user a way of sub-dividing our -- confusing array of commands. data CmdTag -- | Shell-specific command. Shell :: CmdTag -- | The arrow of evaluation (reduces a term). Eval :: CmdTag -- | KURE command. KURE :: CmdTag -- | Command may operate multiple times. Loop :: CmdTag -- | Command may make a deep change, can be O(n). Deep :: CmdTag -- | Command operates on local nodes only, O(1). Shallow :: CmdTag -- | Uses Path or Lens to focus onto something. Navigation :: CmdTag -- | A question we ask. Query :: CmdTag -- | Something that passes or fails. Predicate :: CmdTag -- | Introduce something, like a new name. Introduce :: CmdTag -- | Commute is when you swap nested terms. Commute :: CmdTag -- | Operation has a (perhaps undocumented) precondition. PreCondition :: CmdTag -- | Commands specifically to help debugging. Debug :: CmdTag -- | Version control for Core syntax. VersionControl :: CmdTag -- | A command that uses its context, such as inlining. Context :: CmdTag -- | Commands that are not type safe (may cause Core Lint to fail), or may -- otherwise change the semantics of the program. Unsafe :: CmdTag -- | An incomplete or potentially buggy command. TODO :: CmdTag -- | Things we are trying out. Experiment :: CmdTag -- | A command that will be removed in a future release; it has probably -- been renamed or subsumed by another command. Deprecated :: CmdTag -- | A data type of logical operations on tags. data TagE :: * -- | Tags are meta-data that we add to Externals to make them -- sortable and searchable. class Tag a (.+) :: Tag a => External -> a -> External remTag :: Tag a => a -> External -> External tagMatch :: Tag a => a -> External -> Bool -- | An "and" on Tags. (.&) :: (Tag a, Tag b) => a -> b -> TagE -- | An "or" on Tags. (.||) :: (Tag a, Tag b) => a -> b -> TagE -- | A "not" on Tags. notT :: Tag a => a -> TagE -- | List all the CmdTags associated with an External externTags :: External -> [CmdTag] -- | Lists all the tags paired with a short description of what they're -- about. dictionaryOfTags :: [(CmdTag, String)] data TagBox TagBox :: TagE -> TagBox data IntBox IntBox :: Int -> IntBox data RewriteCoreBox RewriteCoreBox :: (RewriteH Core) -> RewriteCoreBox data RewriteCoreTCBox RewriteCoreTCBox :: (RewriteH CoreTC) -> RewriteCoreTCBox data BiRewriteCoreBox BiRewriteCoreBox :: (BiRewriteH Core) -> BiRewriteCoreBox data TranslateCoreStringBox TranslateCoreStringBox :: (TranslateH Core String) -> TranslateCoreStringBox data TranslateCoreTCStringBox TranslateCoreTCStringBox :: (TranslateH CoreTC String) -> TranslateCoreTCStringBox data TranslateCoreCheckBox TranslateCoreCheckBox :: (TranslateH Core ()) -> TranslateCoreCheckBox data TranslateCoreTCCheckBox TranslateCoreTCCheckBox :: (TranslateH CoreTC ()) -> TranslateCoreTCCheckBox data TranslateCorePathBox TranslateCorePathBox :: (TranslateH Core LocalPathH) -> TranslateCorePathBox data TranslateCoreTCPathBox TranslateCoreTCPathBox :: (TranslateH CoreTC LocalPathH) -> TranslateCoreTCPathBox data NameBox NameBox :: (Name) -> NameBox newtype CoreString CoreString :: String -> CoreString unCoreString :: CoreString -> String data CoreBox CoreBox :: CoreString -> CoreBox data CrumbBox CrumbBox :: Crumb -> CrumbBox data PathBox PathBox :: LocalPathH -> PathBox data StringBox StringBox :: String -> StringBox data NameListBox NameListBox :: [Name] -> NameListBox data StringListBox StringListBox :: [String] -> StringListBox data IntListBox IntListBox :: [Int] -> IntListBox data RewriteCoreListBox RewriteCoreListBox :: [RewriteH Core] -> RewriteCoreListBox instance Typeable TagBox instance Typeable IntBox instance Typeable RewriteCoreBox instance Typeable RewriteCoreTCBox instance Typeable BiRewriteCoreBox instance Typeable TranslateCoreTCStringBox instance Typeable TranslateCoreStringBox instance Typeable TranslateCoreTCCheckBox instance Typeable TranslateCoreCheckBox instance Typeable NameBox instance Typeable CrumbBox instance Typeable PathBox instance Typeable TranslateCorePathBox instance Typeable TranslateCoreTCPathBox instance Typeable CoreBox instance Typeable StringBox instance Typeable NameListBox instance Typeable StringListBox instance Typeable IntListBox instance Typeable RewriteCoreListBox instance Eq CmdTag instance Show CmdTag instance Read CmdTag instance Bounded CmdTag instance Enum CmdTag instance Extern [RewriteH Core] instance Extern [Int] instance Extern [String] instance Extern [Name] instance Extern String instance Extern CoreString instance Extern (TranslateH CoreTC LocalPathH) instance Extern (TranslateH Core LocalPathH) instance Extern LocalPathH instance Extern Crumb instance Extern Name instance Extern (TranslateH Core ()) instance Extern (TranslateH CoreTC ()) instance Extern (TranslateH Core String) instance Extern (TranslateH CoreTC String) instance Extern (BiRewriteH Core) instance Extern (RewriteH CoreTC) instance Extern (RewriteH Core) instance Extern Int instance Extern TagE instance (Extern a, Extern b) => Extern (a -> b) instance Tag CmdTag instance Tag TagE module HERMIT.Dictionary.Debug -- | Exposed debugging Externals. externals :: [External] -- | Show before and after a rewrite. bracketR :: Injection a CoreTC => String -> RewriteH a -> RewriteH a -- | Print out the Core, with a message. observeR :: Injection a CoreTC => String -> RewriteH a -- | If the Rewrite fails, print out the Core, with a -- message. observeFailureR :: Injection a CoreTC => String -> RewriteH a -> RewriteH a -- | Just say something, every time the rewrite is done. traceR :: String -> RewriteH a module HERMIT.Dictionary.Function externals :: [External] -- | Traditional Static Argument Transformation staticArgR :: (ExtendPath c Crumb, AddBindings c) => Rewrite c HermitM CoreDef -- | Static Argument Transformations which requires that arguments in the -- given position are static. staticArgPosR :: (ExtendPath c Crumb, AddBindings c) => [Int] -> Rewrite c HermitM CoreDef -- | Generalized Static Argument Transformation, which allows static -- arguments to be filtered. staticArgPredR :: (ExtendPath c Crumb, AddBindings c) => ([(Int, Var)] -> HermitM [Int]) -> Rewrite c HermitM CoreDef -- | Static Argument Transformation that only considers type arguments to -- be static. staticArgTypesR :: (ExtendPath c Crumb, AddBindings c) => Rewrite c HermitM CoreDef module HERMIT.Dictionary.GHC -- | Externals that reflect GHC functions, or are derived from GHC -- functions. externals :: [External] -- | Top-down traversal tuned to matching function calls. anyCallR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, MonadCatch m) => Rewrite c m Core -> Rewrite c m Core -- | Substitute all occurrences of a variable with an expression, in either -- a program or an expression. substR :: (ExtendPath c Crumb, AddBindings c, MonadCatch m) => Var -> CoreExpr -> Rewrite c m Core -- | Substitute all occurrences of a variable with an expression, in an -- expression. substExprR :: Monad m => Var -> CoreExpr -> Rewrite c m CoreExpr -- | Determine whether an identifier is in scope. inScope :: ReadBindings c => c -> Id -> Bool -- | Lookup a rule and attempt to construct a corresponding rewrite. rule :: (ReadBindings c, HasCoreRules c) => String -> Rewrite c HermitM CoreExpr rules :: (ReadBindings c, HasCoreRules c) => [String] -> Rewrite c HermitM CoreExpr -- | Lifted version of getDynFlags. dynFlagsT :: HasDynFlags m => Translate c m a DynFlags -- | Try to figure out the arity of an identifier. arityOf :: ReadBindings c => c -> Id -> Int -- | Note: this can miss several things that a whole-module core lint will -- find. For instance, running this on the RHS of a binding, the type of -- the RHS will not be checked against the type of the binding. Running -- on the whole let expression will catch that however. lintExprT :: (BoundVars c, Monad m, HasDynFlags m) => Translate c m CoreExpr String -- | Run the Core Lint typechecker. Fails on errors, with error messages. -- Succeeds returning warnings. lintModuleT :: TranslateH ModGuts String specConstrR :: RewriteH ModGuts -- | Apply occurAnalyseExprR to all sub-expressions. occurAnalyseR :: (AddBindings c, ExtendPath c Crumb, MonadCatch m) => Rewrite c m Core -- | Occurrence analyse all sub-expressions, failing if the result is -- syntactically equal to the initial expression. occurAnalyseChangedR :: (AddBindings c, ExtendPath c Crumb, MonadCatch m) => Rewrite c m Core -- | Occurrence analyse an expression, failing if the result is -- syntactically equal to the initial expression. occurAnalyseExprChangedR :: MonadCatch m => Rewrite c m CoreExpr -- | Run GHC's occurrence analyser, and also eliminate any zombies. occurAnalyseAndDezombifyR :: (AddBindings c, ExtendPath c Crumb, MonadCatch m) => Rewrite c m Core -- | Zap the OccInfo in a zombie identifier. dezombifyR :: (ExtendPath c Crumb, Monad m) => Rewrite c m CoreExpr module HERMIT.Dictionary.AlphaConversion -- | Externals for alpha-renaming. externals :: [External] -- | Alpha rename any bindings at this node. Note: does not rename case -- alternatives unless invoked on the alternative. alphaR :: (ExtendPath c Crumb, AddBindings c, BoundVars c) => Rewrite c HermitM Core -- | Alpha rename a lambda binder. Optionally takes a suggested new name. alphaLamR :: (ExtendPath c Crumb, AddBindings c, BoundVars c) => Maybe Name -> Rewrite c HermitM CoreExpr -- | Alpha rename a case binder. Optionally takes a suggested new name. alphaCaseBinderR :: (ExtendPath c Crumb, AddBindings c, BoundVars c) => Maybe Name -> Rewrite c HermitM CoreExpr -- | Rename the variables bound in a case alternative with the given list -- of suggested names. alphaAltWithR :: (ExtendPath c Crumb, AddBindings c, BoundVars c) => [Name] -> Rewrite c HermitM CoreAlt -- | Rename the specified variables in a case alternative. alphaAltVarsR :: (ExtendPath c Crumb, AddBindings c, BoundVars c) => [Var] -> Rewrite c HermitM CoreAlt -- | Rename all identifiers bound in a case alternative. alphaAltR :: (ExtendPath c Crumb, AddBindings c, BoundVars c) => Rewrite c HermitM CoreAlt -- | Rename all identifiers bound in a case expression. alphaCaseR :: (ExtendPath c Crumb, AddBindings c, BoundVars c) => Rewrite c HermitM CoreExpr -- | Rename the identifiers bound in a Let with the given list of suggested -- names. alphaLetWithR :: (ExtendPath c Crumb, AddBindings c, BoundVars c) => [Name] -> Rewrite c HermitM CoreExpr -- | Rename the specified variables bound in a let. alphaLetVarsR :: (ExtendPath c Crumb, AddBindings c, BoundVars c) => [Var] -> Rewrite c HermitM CoreExpr -- | Rename all identifiers bound in a Let. alphaLetR :: (ExtendPath c Crumb, AddBindings c, BoundVars c) => Rewrite c HermitM CoreExpr -- | Rename the identifiers bound in the top-level binding at the head of -- the program with the given list of suggested names. alphaProgConsWithR :: (ExtendPath c Crumb, AddBindings c) => [Name] -> Rewrite c HermitM CoreProg -- | Rename local variables with manifestly unique names (x, x0, x1, ...). -- Does not rename top-level definitions. unshadowR :: (ExtendPath c Crumb, AddBindings c, BoundVars c) => Rewrite c HermitM Core -- | List all visible identifiers (in the expression or the context). visibleVarsT :: (BoundVars c, Monad m) => Translate c m CoreExpr VarSet -- | If a name is provided replace the string with that, otherwise modify -- the string making sure to not clash with any visible variables. freshNameGenT :: (BoundVars c, Monad m) => Maybe Name -> Translate c m CoreExpr (String -> String) -- | Use the optional argument if given, otherwise generate a new name -- avoiding clashes with the list of variables. freshNameGenAvoiding :: Maybe Name -> VarSet -> (String -> String) -- | Replace all occurrences of a specified variable. Arguments are the -- variable to replace and the replacement variable, respectively. replaceVarR :: (ExtendPath c Crumb, AddBindings c, Injection a Core, MonadCatch m) => Var -> Var -> Rewrite c m a module HERMIT.Dictionary.Inline -- | Externals for inlining variables. externals :: [External] data InlineConfig CaseBinderOnly :: CaseBinderInlineOption -> InlineConfig AllBinders :: InlineConfig data CaseBinderInlineOption Scrutinee :: CaseBinderInlineOption Alternative :: CaseBinderInlineOption -- | Return the unfolding of an identifier, and a predicate over the -- binding depths of all variables within that unfolding to determine if -- they have been captured in their new location. getUnfoldingT :: ReadBindings c => InlineConfig -> Translate c HermitM Id (CoreExpr, BindingDepth -> Bool) -- | Inline the current variable. inlineR :: (ExtendPath c Crumb, AddBindings c, ReadBindings c) => Rewrite c HermitM CoreExpr -- | If the current variable matches the given name, then inline it. inlineNameR :: (ExtendPath c Crumb, AddBindings c, ReadBindings c) => Name -> Rewrite c HermitM CoreExpr -- | If the current variable matches any of the given names, then inline -- it. inlineNamesR :: (ExtendPath c Crumb, AddBindings c, ReadBindings c) => [Name] -> Rewrite c HermitM CoreExpr -- | Inline the current identifier if it is a case binder, using the -- scrutinee rather than the case-alternative pattern. inlineCaseScrutineeR :: (ExtendPath c Crumb, AddBindings c, ReadBindings c) => Rewrite c HermitM CoreExpr -- | Inline the current identifier if is a case binder, using the -- case-alternative pattern rather than the scrutinee. inlineCaseAlternativeR :: (ExtendPath c Crumb, AddBindings c, ReadBindings c) => Rewrite c HermitM CoreExpr -- | The implementation of inline, an important transformation. This *only* -- works if the current expression has the form Var v (it does -- not traverse the expression). It can trivially be prompted to more -- general cases using traversal strategies. configurableInlineR :: (ExtendPath c Crumb, AddBindings c, ReadBindings c) => InlineConfig -> (Translate c HermitM Id Bool) -> Rewrite c HermitM CoreExpr -- | Get list of possible inline targets. Used by shell for completion. inlineTargetsT :: (ExtendPath c Crumb, AddBindings c, ReadBindings c) => Translate c HermitM Core [String] instance Eq CaseBinderInlineOption instance Show CaseBinderInlineOption instance Eq InlineConfig instance Show InlineConfig module HERMIT.Dictionary.Fold externals :: [External] foldR :: ReadBindings c => Name -> Rewrite c HermitM CoreExpr foldVarR :: ReadBindings c => Var -> Maybe BindingDepth -> Rewrite c HermitM CoreExpr stashFoldR :: ReadBindings c => Label -> Rewrite c HermitM CoreExpr stashFoldAnyR :: ReadBindings c => Rewrite c HermitM CoreExpr module HERMIT.Dictionary.Query -- | Externals that reflect GHC functions, or are derived from GHC -- functions. externals :: [External] infoT :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, ReadBindings c, BoundVars c, HasDynFlags m, MonadCatch m) => Translate c m CoreTC String -- | Compare the core fragments at the end of the specified -- LocalPathHs. compareCoreAtT :: (ExtendPath c Crumb, AddBindings c, ReadBindings c, ReadPath c Crumb, MonadCatch m) => Translate c m Core LocalPathH -> Translate c m Core LocalPathH -> Translate c m Core () -- | Compare the definitions of two identifiers for alpha-equality. compareBoundIdsT :: (ExtendPath c Crumb, AddBindings c, ReadBindings c) => Id -> Id -> Translate c HermitM x () module HERMIT.Dictionary.Navigation.Crumbs -- | Externals for individual Crumbs. crumbExternals :: [External] module HERMIT.Dictionary.Navigation -- | Externals involving navigating to named entities. externals :: [External] -- | Find the path to the first occurrence occurrence of a variable. occurrenceOfT :: (AddBindings c, ExtendPath c Crumb, ReadPath c Crumb, MonadCatch m) => (Var -> Bool) -> Translate c m CoreTC LocalPathH -- | Find the path to the binding of a variable. bindingOfT :: (AddBindings c, ExtendPath c Crumb, ReadPath c Crumb, MonadCatch m) => (Var -> Bool) -> Translate c m CoreTC LocalPathH -- | Find the path to the binding group of a variable. bindingGroupOfT :: (AddBindings c, ExtendPath c Crumb, ReadPath c Crumb, MonadCatch m) => (Var -> Bool) -> Translate c m CoreTC LocalPathH -- | Find the path to the RHS of a binding. rhsOfT :: (AddBindings c, ExtendPath c Crumb, ReadPath c Crumb, MonadCatch m) => (Var -> Bool) -> Translate c m Core LocalPathH -- | Discard the last crumb of a non-empty LocalPathH. parentOfT :: MonadCatch m => Translate c m g LocalPathH -> Translate c m g LocalPathH -- | Find all possible targets of occurrenceOfT. occurrenceOfTargetsT :: (ExtendPath c Crumb, AddBindings c, MonadCatch m) => Translate c m CoreTC VarSet -- | Find all possible targets of bindingOfT. bindingOfTargetsT :: (ExtendPath c Crumb, AddBindings c, MonadCatch m) => Translate c m CoreTC VarSet -- | Find all possible targets of bindingGroupOfT. bindingGroupOfTargetsT :: (ExtendPath c Crumb, AddBindings c, MonadCatch m) => Translate c m CoreTC VarSet -- | Find all possible targets of rhsOfT. rhsOfTargetsT :: (ExtendPath c Crumb, AddBindings c, MonadCatch m) => Translate c m CoreTC VarSet -- | Language constructs that can be zoomed to. data Considerable Binding :: Considerable Definition :: Considerable CaseAlt :: Considerable Variable :: Considerable Literal :: Considerable Application :: Considerable Lambda :: Considerable LetExpr :: Considerable CaseOf :: Considerable Casty :: Considerable Ticky :: Considerable TypeExpr :: Considerable CoercionExpr :: Considerable -- | Lookup table for constructs that can be considered; the keys are the -- arguments the user can give to the "consider" command. considerables :: [(String, Considerable)] -- | Find the path to the first matching construct. considerConstructT :: (AddBindings c, ExtendPath c Crumb, ReadPath c Crumb, MonadCatch m) => Considerable -> Translate c m Core LocalPathH -- | Construct a path to the (n-1)th argument in a nested sequence of -- Apps. nthArgPath :: Monad m => Int -> Translate c m CoreExpr LocalPathH module HERMIT.Dictionary.Kure -- | externals :: [External] module HERMIT.ParserCore parseCore :: CoreString -> HermitC -> HermitM CoreExpr -- | Parse a CoreString to a CoreExpr, using the current -- context. parseCoreExprT :: CoreString -> TranslateH a CoreExpr parse2beforeBiR :: (CoreExpr -> CoreExpr -> BiRewriteH a) -> CoreString -> CoreString -> BiRewriteH a parse3beforeBiR :: (CoreExpr -> CoreExpr -> CoreExpr -> BiRewriteH a) -> CoreString -> CoreString -> CoreString -> BiRewriteH a instance Eq Token instance Show Token module HERMIT.Dictionary.New externals :: [External] -- | Test if the current expression is an identifier matching the given -- name. isVar :: (ExtendPath c Crumb, AddBindings c, MonadCatch m) => Name -> Translate c m CoreExpr () -- | prog ==> ProgCons (v = e) prog progNonRecIntroR :: String -> CoreString -> RewriteH CoreProg -- | body ==> let v = e in body letNonRecIntroR :: String -> CoreString -> RewriteH CoreExpr module HERMIT.Dictionary.Reasoning externals :: [External] -- | Given two expressions, and a rewrite from the former to the latter, -- verify that rewrite. verifyEqualityLeftToRightT :: MonadCatch m => CoreExpr -> CoreExpr -> Rewrite c m CoreExpr -> Translate c m a () -- | Given two expressions, and a rewrite from the former to the latter, -- verify that rewrite. verifyEqualityCommonTargetT :: MonadCatch m => CoreExpr -> CoreExpr -> Rewrite c m CoreExpr -> Rewrite c m CoreExpr -> Translate c m a () -- | Given f :: X -> Y and g :: Y -> X, verify that f (g y) ==> y -- and g (f x) ==> x. verifyIsomorphismT :: CoreExpr -> CoreExpr -> Rewrite c HermitM CoreExpr -> Rewrite c HermitM CoreExpr -> Translate c HermitM a () -- | Given f :: X -> Y and g :: Y -> X, verify that f (g y) ==> y. verifyRetractionT :: CoreExpr -> CoreExpr -> Rewrite c HermitM CoreExpr -> Translate c HermitM a () -- | Given f :: X -> Y and g :: Y -> X, and a proof that f (g y) -- ==> y, then f (g y) == y. retractionBR :: Maybe (Rewrite c HermitM CoreExpr) -> CoreExpr -> CoreExpr -> BiRewrite c HermitM CoreExpr module HERMIT.Dictionary.Undefined externals :: [External] -- | Verify that the given rewrite is a proof that the given expression is -- a strict function. verifyStrictT :: (BoundVars c, HasGlobalRdrEnv c, MonadCatch m, HasDynFlags m, MonadThings m) => CoreExpr -> Rewrite c m CoreExpr -> Translate c m a () -- | Make an undefined value of the given type. mkUndefinedValT :: (BoundVars c, HasGlobalRdrEnv c, MonadCatch m, HasDynFlags m, MonadThings m) => Type -> Translate c m a CoreExpr -- | Check if the current expression is an undefined value. isUndefinedValT :: (BoundVars c, HasGlobalRdrEnv c, MonadCatch m, HasDynFlags m, MonadThings m) => Translate c m CoreExpr () -- | Set the current expression to undefined. replaceWithUndefinedR :: (BoundVars c, HasGlobalRdrEnv c, MonadCatch m, HasDynFlags m, MonadThings m) => Rewrite c m CoreExpr -- | error ty string ==> undefined ty errorToUndefinedR :: (BoundVars c, HasGlobalRdrEnv c, MonadCatch m, HasDynFlags m, MonadThings m) => Rewrite c m CoreExpr -- | undefinedExprR = undefinedAppR <+ undefinedLamR <+ undefinedLetR -- <+ undefinedCastR <+ undefinedTickR <+ undefinedCaseR undefinedExprR :: (AddBindings c, BoundVars c, ExtendPath c Crumb, HasGlobalRdrEnv c, MonadCatch m, HasDynFlags m, MonadThings m) => Rewrite c m CoreExpr -- | (undefined ty1) e ==> undefined ty2 undefinedAppR :: (BoundVars c, ExtendPath c Crumb, HasGlobalRdrEnv c, MonadCatch m, HasDynFlags m, MonadThings m) => Rewrite c m CoreExpr -- | ( v -> undefined ty1) ==> undefined ty2 (where -- v is not a TyVar) undefinedLamR :: (AddBindings c, BoundVars c, ExtendPath c Crumb, HasGlobalRdrEnv c, MonadCatch m, HasDynFlags m, MonadThings m) => Rewrite c m CoreExpr -- | let bds in (undefined ty) ==> undefined ty undefinedLetR :: (AddBindings c, BoundVars c, ExtendPath c Crumb, HasGlobalRdrEnv c, MonadCatch m, HasDynFlags m, MonadThings m) => Rewrite c m CoreExpr -- | case (undefined ty) of alts ==> undefined ty undefinedCaseScrutineeR :: (AddBindings c, BoundVars c, ExtendPath c Crumb, HasGlobalRdrEnv c, MonadCatch m, HasDynFlags m, MonadThings m) => Rewrite c m CoreExpr -- | case e of {pat_1 -> undefined ty ; pat_2 -> undefined ty ; ... ; -- pat_n -> undefined ty} ==> undefined ty undefinedCaseAltsR :: (AddBindings c, BoundVars c, ExtendPath c Crumb, HasGlobalRdrEnv c, MonadCatch m, HasDynFlags m, MonadThings m) => Rewrite c m CoreExpr -- | undefinedCaseR = undefinedCaseScrutineeR <+ undefinedCaseAltsR undefinedCaseR :: (AddBindings c, BoundVars c, ExtendPath c Crumb, HasGlobalRdrEnv c, MonadCatch m, HasDynFlags m, MonadThings m) => Rewrite c m CoreExpr -- | Cast (undefined ty1) co ==> undefined ty2 undefinedCastR :: (BoundVars c, ExtendPath c Crumb, HasGlobalRdrEnv c, MonadCatch m, HasDynFlags m, MonadThings m) => Rewrite c m CoreExpr -- | Tick tick (undefined ty1) ==> undefined ty1 undefinedTickR :: (BoundVars c, ExtendPath c Crumb, HasGlobalRdrEnv c, MonadCatch m, HasDynFlags m, MonadThings m) => Rewrite c m CoreExpr module HERMIT.Dictionary.FixPoint -- | Externals for manipulating fixed points. externals :: [External] -- | f = e ==> f = fix (\ f -> e) fixIntroR :: RewriteH CoreDef -- | fix ty f <==> f (fix ty f) fixComputationRuleBR :: BiRewriteH CoreExpr -- | fix tyA (\ a -> f (g a)) <==> f (fix tyB (\ b -- -> g (f b)) fixRollingRuleBR :: BiRewriteH CoreExpr -- | If f is strict, then (f (g a) == h (f a)) -- ==> (f (fix g) == fix h) fixFusionRuleBR :: Maybe (RewriteH CoreExpr, RewriteH CoreExpr) -> Maybe (RewriteH CoreExpr) -> CoreExpr -> CoreExpr -> CoreExpr -> BiRewriteH CoreExpr -- | f ==> fix f mkFixT :: (BoundVars c, HasGlobalRdrEnv c, MonadCatch m, HasDynFlags m, MonadThings m) => CoreExpr -> Translate c m z CoreExpr -- | Check that the expression has the form fix t (f :: t -> t), -- returning t and f. isFixExprT :: TranslateH CoreExpr (Type, CoreExpr) module HERMIT.Dictionary.Unsafe externals :: [External] unsafeReplaceR :: CoreString -> RewriteH CoreExpr unsafeReplaceStashR :: String -> RewriteH CoreExpr module HERMIT.Dictionary.Local.Bind -- | Externals for manipulating binding groups. externals :: [External] -- | NonRec v e ==> Rec [(v,e)] nonrecToRecR :: MonadCatch m => Rewrite c m CoreBind -- | Rec [(v,e)] ==> NonRec v e recToNonrecR :: MonadCatch m => Rewrite c m CoreBind module HERMIT.Dictionary.Local.Case -- | Externals relating to Case expressions. externals :: [External] -- | (case s of alt1 -> e1; alt2 -> e2) v ==> case s of alt1 -> -- e1 v; alt2 -> e2 v caseFloatAppR :: (ExtendPath c Crumb, AddBindings c, ReadBindings c) => Rewrite c HermitM CoreExpr -- | f (case s of alt1 -> e1; alt2 -> e2) ==> case s -- of alt1 -> f e1; alt2 -> f e2 Only safe if f is -- strict. caseFloatArgR :: (ExtendPath c Crumb, AddBindings c, BoundVars c, HasGlobalRdrEnv c) => Maybe (CoreExpr, Maybe (Rewrite c HermitM CoreExpr)) -> Rewrite c HermitM CoreExpr -- | case (case s1 of alt11 -> e11; alt12 -> e12) of alt21 -> e21; -- alt22 -> e22 ==> case s1 of alt11 -> case e11 of alt21 -> -- e21; alt22 -> e22 alt12 -> case e12 of alt21 -> e21; alt22 -- -> e22 caseFloatCaseR :: (ExtendPath c Crumb, AddBindings c, ReadBindings c) => Rewrite c HermitM CoreExpr -- | cast (case s of p -> e) co ==> case s of p -> cast e co caseFloatCastR :: MonadCatch m => Rewrite c m CoreExpr -- | let v = case s of alt1 -> e1 in e ==> case s of alt1 -> let v -- = e1 in e caseFloatLetR :: (ExtendPath c Crumb, AddBindings c, ReadBindings c) => Rewrite c HermitM CoreExpr -- | caseFloatR = caseFloatAppR <+ caseFloatCaseR <+ caseFloatLetR -- <+ caseFloatCastR Note: does NOT include caseFloatArg caseFloatR :: (ExtendPath c Crumb, AddBindings c, ReadBindings c) => Rewrite c HermitM CoreExpr -- | Unfloat a Case whatever the context. caseUnfloatR :: (ExtendPath c Crumb, AddBindings c, MonadCatch m) => Rewrite c m CoreExpr -- | Unimplemented! caseUnfloatAppR :: Monad m => Rewrite c m CoreExpr caseUnfloatArgsR :: (ExtendPath c Crumb, AddBindings c, MonadCatch m) => Rewrite c m CoreExpr -- | Case of Known Constructor. Eliminate a case if the scrutinee is a data -- constructor or a literal. caseReduceR :: (ExtendPath c Crumb, AddBindings c, ReadBindings c) => Rewrite c HermitM CoreExpr -- | Case of Known Constructor. Eliminate a case if the scrutinee is a data -- constructor. caseReduceDataconR :: (ExtendPath c Crumb, AddBindings c, ReadBindings c) => Rewrite c HermitM CoreExpr -- | Case of Known Constructor. Eliminate a case if the scrutinee is a -- literal. NB: LitAlt cases don't do evaluation caseReduceLiteralR :: MonadCatch m => Rewrite c m CoreExpr -- | Inline the case scrutinee (if it is an identifier), and then perform -- case reduction. caseReduceIdR :: (ExtendPath c Crumb, AddBindings c, ReadBindings c) => Rewrite c HermitM CoreExpr -- | Case split a free identifier in an expression: -- -- E.g. Assume expression e which mentions i :: [a] -- -- e ==> case i of i [] -> e (a:as) -> e caseSplitR :: Name -> Rewrite c HermitM CoreExpr -- | Like caseSplit, but additionally inlines the constructor applications -- for each occurance of the named variable. -- -- 
--   caseSplitInline nm = caseSplit nm >>> anybuR (inlineName nm)
--
caseSplitInlineR :: (ExtendPath c Crumb, AddBindings c, ReadBindings c) => Name -> Rewrite c HermitM Core -- | Inline the case wildcard binder as the case scrutinee everywhere in -- the case alternatives. caseInlineScrutineeR :: (ExtendPath c Crumb, AddBindings c, ReadBindings c) => Rewrite c HermitM CoreExpr -- | Inline the case wildcard binder as the case-alternative pattern -- everywhere in the case alternatives. caseInlineAlternativeR :: (ExtendPath c Crumb, AddBindings c, ReadBindings c) => Rewrite c HermitM CoreExpr -- | Merge all case alternatives into a single default case. The RHS of -- each alternative must be the same. case s of {pat1 -> e ; pat2 -- -> e ; ... ; patn -> e} ==> case s of {_ -> -- e} caseMergeAltsR :: MonadCatch m => Rewrite c m CoreExpr -- | A cleverer version of mergeCaseAlts that first attempts to -- abstract out any occurrences of the alternative pattern using the -- wildcard binder. caseMergeAltsWithWildR :: (ExtendPath c Crumb, AddBindings c, ReadBindings c) => Rewrite c HermitM CoreExpr -- | case s of w; C vs -> e ==> e if w and vs are not free in e caseElimR :: Rewrite c HermitM CoreExpr -- | Eliminate a case, inlining any occurrences of the case binder as the -- scrutinee. caseElimInlineScrutineeR :: (ExtendPath c Crumb, AddBindings c, ReadBindings c) => Rewrite c HermitM CoreExpr -- | Eliminate a case, merging the case alternatives into a single default -- alternative and inlining the case binder as the scrutinee (if -- possible). caseElimMergeAltsR :: (ExtendPath c Crumb, AddBindings c, ReadBindings c) => Rewrite c HermitM CoreExpr -- | Force evaluation of an identifier by introducing a case. This is -- equivalent to adding (seq v) in the source code. -- -- e -> case v of v _ -> e caseIntroSeqR :: Name -> Rewrite c HermitM CoreExpr -- | Eliminate a case that corresponds to a pointless seq. caseElimSeqR :: (ExtendPath c Crumb, AddBindings c, ReadBindings c) => Rewrite c HermitM CoreExpr module HERMIT.Dictionary.Local.Cast -- | Externals relating to Case expressions. externals :: [External] castElimReflR :: MonadCatch m => Rewrite c m CoreExpr castElimSymR :: MonadCatch m => Rewrite c m CoreExpr castFloatAppR :: MonadCatch m => Rewrite c m CoreExpr castElimSymPlusR :: (ExtendPath c Crumb, AddBindings c, Monad m) => Rewrite c m CoreExpr module HERMIT.Dictionary.Local.Let -- | Externals relating to Let expressions. externals :: [External] -- | Let (NonRec v e) body ==> body[e/v] letNonRecSubstR :: MonadCatch m => Rewrite c m CoreExpr -- | Currently we always substitute types and coercions, and use a -- heuristic to decide whether to substitute expressions. This may need -- revisiting. letNonRecSubstSafeR :: (AddBindings c, ExtendPath c Crumb, ReadBindings c, MonadCatch m) => Rewrite c m CoreExpr -- | (let x = e1 in e2) ==> (e2[e1/x]), (x must not be free in e1) letSubstR :: (AddBindings c, ExtendPath c Crumb, MonadCatch m) => Rewrite c m CoreExpr -- | As letNonRecSubstSafeR, but attempting to convert a singleton -- recursive binding to a non-recursive binding first. letSubstSafeR :: (AddBindings c, ExtendPath c Crumb, ReadBindings c, MonadCatch m) => Rewrite c m CoreExpr letElimR :: (ExtendPath c Crumb, AddBindings c, MonadCatch m) => Rewrite c m CoreExpr -- | Remove an unused non-recursive let binding. let v = E1 in E2 -- ==> E2, if v is not free in E2 letNonRecElimR :: MonadCatch m => Rewrite c m CoreExpr -- | Remove all unused recursive let bindings in the current group. letRecElimR :: MonadCatch m => Rewrite c m CoreExpr -- | e ==> (let v = e in v), name of v is provided letIntroR :: String -> Rewrite c HermitM CoreExpr -- | (let v = ev in e) x ==> let v = ev in e x letFloatAppR :: (ExtendPath c Crumb, AddBindings c, BoundVars c) => Rewrite c HermitM CoreExpr -- | f (let v = ev in e) ==> let v = ev in f e letFloatArgR :: (ExtendPath c Crumb, AddBindings c, BoundVars c) => Rewrite c HermitM CoreExpr -- | let v = (let bds in e1) in e2 ==> let bds in let v = -- e1 in e2 letFloatLetR :: (ExtendPath c Crumb, AddBindings c, BoundVars c) => Rewrite c HermitM CoreExpr -- | ( v -> let binds in e2) ==> let binds in ( v1 -> -- e2) Fails if v occurs in the RHS of binds. If -- v is shadowed in binds, then v will be -- alpha-renamed. letFloatLamR :: (ExtendPath c Crumb, AddBindings c, BoundVars c) => Rewrite c HermitM CoreExpr -- | case (let bnds in e) of wild alts ==> let bnds in -- (case e of wild alts) Fails if any variables bound in -- bnds occurs in alts. letFloatCaseR :: (ExtendPath c Crumb, AddBindings c, BoundVars c) => Rewrite c HermitM CoreExpr -- | cast (let bnds in e) co ==> let bnds in cast e co letFloatCastR :: MonadCatch m => Rewrite c m CoreExpr -- | Float a Let through an expression, whatever the context. letFloatExprR :: (ExtendPath c Crumb, AddBindings c, BoundVars c) => Rewrite c HermitM CoreExpr -- | ProgCons (NonRec v (Let bds e)) p ==> -- ProgCons bds (ProgCons (NonRec v e) p) letFloatTopR :: (ExtendPath c Crumb, AddBindings c, BoundVars c) => Rewrite c HermitM CoreProg -- | Unfloat a Let if possible. letUnfloatR :: (ExtendPath c Crumb, AddBindings c, MonadCatch m) => Rewrite c m CoreExpr -- | let v = ev in f a ==> (let v = ev in f) (let v = ev in -- a) letUnfloatAppR :: MonadCatch m => Rewrite c m CoreExpr -- | let v = ev in case s of p -> e ==> case (let v = ev -- in s) of p -> let v = ev in e, if v does not shadow a -- pattern binder in p letUnfloatCaseR :: MonadCatch m => Rewrite c m CoreExpr -- | let v = ev in x -> e ==> x -> let v = ev in -- e if v does not shadow x letUnfloatLamR :: (ExtendPath c Crumb, AddBindings c, MonadCatch m) => Rewrite c m CoreExpr -- | Re-order a sequence of nested non-recursive let bindings. The argument -- list should contain the let-bound variables, in the desired order. reorderNonRecLetsR :: MonadCatch m => [Name] -> Rewrite c m CoreExpr -- | Combine nested non-recursive lets into case of a tuple. E.g. let {v1 = -- e1 ; v2 = e2 ; v3 = e3} in body ==> case (e1,e2,e3) of {(v1,v2,v3) -- -> body} letTupleR :: String -> Rewrite c HermitM CoreExpr -- | let v = ev in e ==> case ev of v -> e letToCaseR :: (ExtendPath c Crumb, AddBindings c, ReadBindings c) => Rewrite c HermitM CoreExpr module HERMIT.Dictionary.Local -- | Externals for local structural manipulations. (Many taken from Chapter -- 3 of Andre Santos' dissertation.) externals :: [External] -- | Abstract over a variable using a lambda. e ==> ( x. e) x abstractR :: (ReadBindings c, MonadCatch m) => Name -> Rewrite c m CoreExpr -- | Push a function through a Case or Let expression. Unsafe if the -- function is not strict. pushR :: (ExtendPath c Crumb, AddBindings c, ReadBindings c, HasGlobalRdrEnv c) => Maybe (Rewrite c HermitM CoreExpr) -> (Id -> Bool) -> Rewrite c HermitM CoreExpr -- | ((\ 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). betaReduceR :: MonadCatch m => Rewrite c m CoreExpr -- | Perform one or more beta-reductions. betaReducePlusR :: MonadCatch m => Rewrite c m CoreExpr -- | (let v = e1 in e2) ==> (\ v -> e2) e1 betaExpandR :: MonadCatch m => Rewrite c m CoreExpr -- | (\ v -> f v) ==> f etaReduceR :: MonadCatch m => Rewrite c m CoreExpr -- | e1 ==> (\ v -> e1 v) etaExpandR :: String -> Rewrite c HermitM CoreExpr -- | Perform multiple eta-expansions. multiEtaExpandR :: (ExtendPath c Crumb, AddBindings c) => [String] -> Rewrite c HermitM CoreExpr -- | Flatten all the top-level binding groups in the module to a single -- recursive binding group. flattenModuleR :: (ExtendPath c Crumb, Monad m) => Rewrite c m ModGuts -- | Flatten all the top-level binding groups in a program to a program -- containing a single recursive binding group. flattenProgramR :: Monad m => Rewrite c m CoreProg -- | Flatten all the top-level binding groups in a program to a single -- recursive binding group. flattenProgramT :: Monad m => Translate c m CoreProg CoreBind module HERMIT.PrettyPrinter.Common type DocH = MDoc HermitMark data Attr PathAttr :: AbsolutePathH -> Attr Color :: SyntaxForColor -> Attr SpecialFont :: Attr attrP :: AbsolutePathH -> DocH -> DocH newtype HTML HTML :: String -> HTML coercionColor :: DocH -> DocH idColor :: DocH -> DocH keywordColor :: DocH -> DocH markColor :: SyntaxForColor -> DocH -> DocH typeColor :: DocH -> DocH data ShowOption Show :: ShowOption Abstract :: ShowOption Omit :: ShowOption Kind :: ShowOption specialFont :: DocH -> DocH data SpecialSymbol LambdaSymbol :: SpecialSymbol TypeOfSymbol :: SpecialSymbol RightArrowSymbol :: SpecialSymbol CastSymbol :: SpecialSymbol CoercionSymbol :: SpecialSymbol CoercionBindSymbol :: SpecialSymbol TypeSymbol :: SpecialSymbol TypeBindSymbol :: SpecialSymbol ForallSymbol :: SpecialSymbol data SyntaxForColor KeywordColor :: SyntaxForColor SyntaxColor :: SyntaxForColor IdColor :: SyntaxForColor CoercionColor :: SyntaxForColor TypeColor :: SyntaxForColor LitColor :: SyntaxForColor WarningColor :: SyntaxForColor coreRenders :: [(String, PrettyOptions -> DocH -> String)] renderCode :: RenderCode a => PrettyOptions -> DocH -> a class (RenderSpecial a, Monoid a) => RenderCode a where rStart = mempty rEnd = mempty rStart :: RenderCode a => a rEnd :: RenderCode a => a rDoHighlight :: RenderCode a => Maybe Attr -> [Attr] -> a rPutStr :: RenderCode a => String -> a class RenderSpecial a renderSpecial :: RenderSpecial a => SpecialSymbol -> a newtype Unicode Unicode :: Char -> Unicode type PrettyH a = Translate PrettyC HermitM a DocH liftPrettyH :: (ReadBindings c, ReadPath c Crumb) => PrettyOptions -> PrettyH a -> Translate c HermitM a DocH -- | Context for PrettyH translations. data PrettyC PrettyC :: AbsolutePath Crumb -> VarSet -> PrettyOptions -> PrettyC prettyC_path :: PrettyC -> AbsolutePath Crumb prettyC_vars :: PrettyC -> VarSet prettyC_options :: PrettyC -> PrettyOptions initPrettyC :: PrettyOptions -> PrettyC liftPrettyC :: (ReadBindings c, ReadPath c Crumb) => PrettyOptions -> c -> PrettyC newtype TranslateDocH a TranslateDocH :: (PrettyC -> PrettyH a -> TranslateH a DocH) -> TranslateDocH a unTranslateDocH :: TranslateDocH a -> PrettyC -> PrettyH a -> TranslateH a DocH data TranslateCoreTCDocHBox TranslateCoreTCDocHBox :: (TranslateDocH CoreTC) -> TranslateCoreTCDocHBox data PrettyOptions PrettyOptions :: Bool -> ShowOption -> ShowOption -> ShowOption -> Maybe PathH -> Maybe Int -> Bool -> Float -> Int -> PrettyOptions -- | Do you show fully qualified names? po_fullyQualified :: PrettyOptions -> Bool -- | Do you hide types, and type arguments, as ? po_exprTypes :: PrettyOptions -> ShowOption -- | Do you hide coercions? po_coercions :: PrettyOptions -> ShowOption -- | Do you give the types for all bindings? po_typesForBinders :: PrettyOptions -> ShowOption -- | This region should be highlighted (is the current focus) po_focus :: PrettyOptions -> Maybe PathH -- | below this depth are ..., Nothing => infinite po_depth :: PrettyOptions -> Maybe Int -- | notes might be added to output po_notes :: PrettyOptions -> Bool po_ribbon :: PrettyOptions -> Float po_width :: PrettyOptions -> Int updateCoShowOption :: ShowOption -> PrettyOptions -> PrettyOptions updateTypeShowOption :: ShowOption -> PrettyOptions -> PrettyOptions updateWidthOption :: Int -> PrettyOptions -> PrettyOptions -- | like vcat and hcat, only make the list syntax explicit hlist :: [MDoc a] -> MDoc a -- | like vcat and hcat, only make the list syntax explicit vlist :: [MDoc a] -> MDoc a instance Typeable TranslateCoreTCDocHBox instance Eq SyntaxForColor instance Show SyntaxForColor instance Eq Attr instance Show Attr instance Show HermitMark instance Eq ShowOption instance Ord ShowOption instance Show ShowOption instance Read ShowOption instance Show PrettyOptions instance Show SpecialSymbol instance Eq SpecialSymbol instance Ord SpecialSymbol instance Bounded SpecialSymbol instance Enum SpecialSymbol instance RenderCode DebugPretty instance Monoid DebugPretty instance RenderSpecial DebugPretty instance RenderCode ASCII instance RenderCode HTML instance RenderCode LaTeX instance RenderSpecial HTML instance Monoid HTML instance RenderSpecial LaTeX instance Monoid LaTeX instance RenderSpecial Unicode instance RenderSpecial ASCII instance Monoid ASCII instance RenderSpecial Char instance Default PrettyOptions instance BoundVars PrettyC instance AddBindings PrettyC instance ExtendPath PrettyC Crumb instance ReadPath PrettyC Crumb instance Extern (TranslateDocH CoreTC) module HERMIT.Dictionary.Unfold externals :: [External] -- | cleanupUnfoldR cleans a unfold operation (for example, an inline or -- rule application) It is used at the level of the top-redex. Invariant: -- will not introduce let bindings cleanupUnfoldR :: (AddBindings c, ExtendPath c Crumb, MonadCatch m) => Rewrite c m CoreExpr -- | Stash a binding with a name for later use. Allows us to look at past -- definitions. rememberR :: Label -> Rewrite c HermitM Core showStashT :: Injection CoreDef a => PrettyC -> PrettyH a -> Translate c HermitM a DocH -- | A more powerful inline. Matches two cases: Var ==> inlines -- App ==> inlines the head of the function call for the app tree unfoldR :: (ExtendPath c Crumb, AddBindings c, ReadBindings c) => Rewrite c HermitM CoreExpr unfoldPredR :: (ExtendPath c Crumb, AddBindings c, ReadBindings c) => (Id -> [CoreExpr] -> Bool) -> Rewrite c HermitM CoreExpr unfoldNameR :: (ExtendPath c Crumb, AddBindings c, ReadBindings c) => Name -> Rewrite c HermitM CoreExpr unfoldNamesR :: (ExtendPath c Crumb, AddBindings c, ReadBindings c) => [Name] -> Rewrite c HermitM CoreExpr unfoldSaturatedR :: (ExtendPath c Crumb, AddBindings c, ReadBindings c) => Rewrite c HermitM CoreExpr -- | Stash a binding with a name for later use. Allows us to look at past -- definitions. rememberR :: String -> Translate c m Core () rememberR -- label = contextfreeT $ core -> case core of DefCore def -> -- saveDef label def BindCore (NonRec i e) -> saveDef label (Def i e) -- _ -> fail remember: not a binding -- -- Apply a stashed definition (like inline, but looks in stash instead of -- context). unfoldStashR :: ReadBindings c => String -> Rewrite c HermitM CoreExpr specializeR :: (ExtendPath c Crumb, AddBindings c, ReadBindings c) => Rewrite c HermitM CoreExpr module HERMIT.Dictionary.Composite externals :: [External] -- | Unfold the current expression if it is one of the basic combinators: -- ($), (.), id, flip, const, -- fst or snd. This is intended to be used as a component -- of simplification traversals such as simplifyR or bashR. unfoldBasicCombinatorR :: (ExtendPath c Crumb, AddBindings c, ReadBindings c) => Rewrite c HermitM CoreExpr simplifyR :: (ExtendPath c Crumb, AddBindings c, ReadBindings c) => Rewrite c HermitM Core bashUsingR :: (ExtendPath c Crumb, AddBindings c, MonadCatch m) => [Rewrite c m Core] -> Rewrite c m Core bashR :: (ExtendPath c Crumb, AddBindings c, ReadBindings c) => Rewrite c HermitM Core bashExtendedWithR :: (ExtendPath c Crumb, AddBindings c, ReadBindings c) => [Rewrite c HermitM Core] -> Rewrite c HermitM Core bashDebugR :: RewriteH Core module HERMIT.Dictionary.WorkerWrapper.Common data WWAssumptionTag A :: WWAssumptionTag B :: WWAssumptionTag C :: WWAssumptionTag data WWAssumption WWAssumption :: WWAssumptionTag -> (RewriteH CoreExpr) -> WWAssumption workLabel :: Label instance Eq WWAssumptionTag instance Ord WWAssumptionTag instance Show WWAssumptionTag instance Read WWAssumptionTag module HERMIT.Dictionary.WorkerWrapper.Fix -- | Externals for manipulating fixed points, and for the worker/wrapper -- transformation. externals :: [External] -- | For any f :: A -> A, and given wrap :: B -> A -- and unwrap :: A -> B as arguments, then fix A f -- <==> wrap (fix B (\ b -> unwrap (f (wrap b)))) wwFacBR :: Maybe WWAssumption -> CoreExpr -> CoreExpr -> BiRewriteH CoreExpr -- | \ wrap unwrap -> (prog = expr ==> prog = let f = \ -- prog -> expr in let work = unwrap (f (wrap work)) in wrap -- work) wwSplitR :: Maybe WWAssumption -> CoreExpr -> CoreExpr -> RewriteH CoreDef -- | As wwSplit but performs the static-argument transformation for -- n static arguments first, and optionally provides some of -- those arguments (specified by index) to all calls of wrap and unwrap. -- This is useful if, for example, the expression, and wrap and unwrap, -- all have a forall type. wwSplitStaticArg :: Int -> [Int] -> Maybe WWAssumption -> CoreString -> CoreString -> RewriteH CoreDef -- | Save the recursive definition of work in the stash, so that we can -- later verify uses of wwFusionBR. Must be applied to a -- definition of the form: work = unwrap (f (wrap work)) Note -- that this is performed automatically as part of wwSplitR. wwGenerateFusionR :: Maybe WWAssumption -> RewriteH Core -- | Given wrap :: B -> A, unwrap :: A -> B and -- work :: B as arguments, then unwrap (wrap work) -- <==> work wwFusionBR :: BiRewriteH CoreExpr -- | wrap (unwrap a) <==> a wwAssA :: Maybe (RewriteH CoreExpr) -> CoreExpr -> CoreExpr -> BiRewriteH CoreExpr -- | wrap (unwrap (f a)) <==> f a wwAssB :: Maybe (RewriteH CoreExpr) -> CoreExpr -> CoreExpr -> CoreExpr -> BiRewriteH CoreExpr -- | fix A ( a -> wrap (unwrap (f a))) <==> fix A -- f wwAssC :: Maybe (RewriteH CoreExpr) -> CoreExpr -> CoreExpr -> CoreExpr -> BiRewriteH CoreExpr module HERMIT.Dictionary.WorkerWrapper.FixResult -- | Externals for manipulating fixed points, and for the worker/wrapper -- transformation. externals :: [External] -- | For any f :: (X -> A) -> (X -> A), and given abs -- :: B -> A and rep :: A -> B as arguments, then -- fix A f <==> \ x1 -> abs (fix (X->B) (\ h x2 -- -> rep (f (\ x3 -> abs (h x3)) x2)) x1) wwResultFacBR :: Maybe WWAssumption -> CoreExpr -> CoreExpr -> BiRewriteH CoreExpr -- | \ abs rep -> (prog = expr ==> prog = let f = \ prog -- -> expr in let work = \ x1 -> rep (f (\ x2 -> abs (work x2)) -- x1) in \ x0 -> abs (work x0)) wwResultSplitR :: Maybe WWAssumption -> CoreExpr -> CoreExpr -> RewriteH CoreDef -- | As wwSplit but performs the static-argument transformation for -- n static arguments first, and optionally provides some of -- those arguments (specified by index) to all calls of abs and rep. This -- is useful if, for example, the expression, and abs and rep, all have a -- forall type. wwResultSplitStaticArg :: Int -> [Int] -> Maybe WWAssumption -> CoreString -> CoreString -> RewriteH CoreDef -- | Save the recursive definition of work in the stash, so that we can -- later verify uses of wwResultFusionBR. Must be applied to a -- definition of the form: work = \ x1 -> rep (f (\ x2 -> abs -- (work x2)) x1) Note that this is performed automatically as part -- of wwResultSplitR. wwResultGenerateFusionR :: Maybe WWAssumption -> RewriteH Core -- | Given abs :: B -> A, rep :: A -> B and -- work :: X -> B as arguments, then rep (abs (work -- x)) <==> work x wwResultFusionBR :: BiRewriteH CoreExpr -- | abs (rep a) <==> a wwResultAssA :: Maybe (RewriteH CoreExpr) -> CoreExpr -> CoreExpr -> BiRewriteH CoreExpr -- | abs (rep (f h x)) <==> f h x wwResultAssB :: Maybe (RewriteH CoreExpr) -> CoreExpr -> CoreExpr -> CoreExpr -> BiRewriteH CoreExpr -- | fix (X->A) ( h x -> abs (rep (f h x))) <==> -- fix (X->A) f wwResultAssC :: Maybe (RewriteH CoreExpr) -> CoreExpr -> CoreExpr -> CoreExpr -> BiRewriteH CoreExpr module HERMIT.Dictionary -- | List of all Externals provided by HERMIT. externals :: [External] module HERMIT.Interp -- | An Interp a is a possible means of converting a -- Typeable value to a value of type a. data Interp :: * -> * -- | The primitive way of building an Interp. interp :: Typeable a => (a -> b) -> Interp b -- | Interpret an ExprH by looking up the appropriate -- Dynamic(s) in the provided Dictionary, then interpreting -- the Dynamic(s) with the provided Interps, returning the -- first interpretation to succeed (or an error string if none succeed). interpExprH :: Monad m => Dictionary -> [Interp a] -> ExprH -> m a instance Functor Interp module HERMIT.Kernel -- | A handle for a specific version of the ModGuts. data AST -- | A Kernel is a repository for complete Core syntax trees -- (ModGuts). For now, operations on a Kernel are -- sequential, but later it will be possible to have two applyKs -- running in parallel. data Kernel -- | Start a HERMIT client by providing an IO function that takes the -- initial Kernel and inital AST handle. The -- Modguts to CoreM Modguts' function required by GHC -- Plugins is returned. The callback is only ever called once. hermitKernel :: (Kernel -> AST -> IO ()) -> ModGuts -> CoreM ModGuts -- | Halt the Kernel and return control to GHC, which compiles the -- specified AST. resumeK :: Kernel -> AST -> IO () -- | Halt the Kernel and abort GHC without compiling. abortK :: Kernel -> IO () -- | Apply a Rewrite to the specified AST and return a handle -- to the resulting AST. applyK :: Kernel -> AST -> RewriteH ModGuts -> HermitMEnv -> IO (KureM AST) -- | Apply a TranslateH to the AST and return the resulting -- value. queryK :: Kernel -> forall a. AST -> TranslateH ModGuts a -> HermitMEnv -> IO (KureM a) -- | Delete the internal record of the specified AST. deleteK :: Kernel -> AST -> IO () -- | List all the ASTs tracked by the Kernel. listK :: Kernel -> IO [AST] instance Eq AST instance Ord AST instance Show AST module HERMIT.Kernel.Scoped -- | A primitive means of denoting navigation of a tree (within a local -- scope). data Direction -- | Left L :: Direction -- | Right R :: Direction -- | Up U :: Direction -- | Top T :: Direction -- | A SnocPath from a local origin. type LocalPath = SnocPath -- | Movement confined within the local scope. moveLocally :: Direction -> LocalPathH -> LocalPathH -- | An alternative HERMIT kernel, that provides scoping. data ScopedKernel ScopedKernel :: (forall m. (MonadIO m, MonadCatch m) => SAST -> m ()) -> (forall m. MonadIO m => m ()) -> (forall g m. (MonadIO m, MonadCatch m, Injection ModGuts g, Walker HermitC g) => RewriteH g -> HermitMEnv -> SAST -> m SAST) -> (forall g a m. (MonadIO m, MonadCatch m, Injection ModGuts g, Walker HermitC g) => TranslateH g a -> HermitMEnv -> SAST -> m a) -> (forall m. (MonadIO m, MonadCatch m) => SAST -> m ()) -> (forall m. MonadIO m => m [SAST]) -> (forall m. (MonadIO m, MonadCatch m) => SAST -> m [PathH]) -> (forall m. (MonadIO m, MonadCatch m) => (LocalPathH -> LocalPathH) -> HermitMEnv -> SAST -> m SAST) -> (forall m. (MonadIO m, MonadCatch m) => SAST -> m SAST) -> (forall m. (MonadIO m, MonadCatch m) => SAST -> m SAST) -> Kernel -> (forall m. (MonadIO m, MonadCatch m) => SAST -> m AST) -> ScopedKernel resumeS :: ScopedKernel -> forall m. (MonadIO m, MonadCatch m) => SAST -> m () abortS :: ScopedKernel -> forall m. MonadIO m => m () applyS :: ScopedKernel -> forall g m. (MonadIO m, MonadCatch m, Injection ModGuts g, Walker HermitC g) => RewriteH g -> HermitMEnv -> SAST -> m SAST queryS :: ScopedKernel -> forall g a m. (MonadIO m, MonadCatch m, Injection ModGuts g, Walker HermitC g) => TranslateH g a -> HermitMEnv -> SAST -> m a deleteS :: ScopedKernel -> forall m. (MonadIO m, MonadCatch m) => SAST -> m () listS :: ScopedKernel -> forall m. MonadIO m => m [SAST] pathS :: ScopedKernel -> forall m. (MonadIO m, MonadCatch m) => SAST -> m [PathH] modPathS :: ScopedKernel -> forall m. (MonadIO m, MonadCatch m) => (LocalPathH -> LocalPathH) -> HermitMEnv -> SAST -> m SAST beginScopeS :: ScopedKernel -> forall m. (MonadIO m, MonadCatch m) => SAST -> m SAST endScopeS :: ScopedKernel -> forall m. (MonadIO m, MonadCatch m) => SAST -> m SAST kernelS :: ScopedKernel -> Kernel toASTS :: ScopedKernel -> forall m. (MonadIO m, MonadCatch m) => SAST -> m AST -- | A handle for an AST combined with scoping information. newtype SAST SAST :: Int -> SAST -- | Start a HERMIT client by providing an IO function that takes the -- initial ScopedKernel and inital SAST handle. The -- Modguts to CoreM Modguts' function required by GHC -- Plugins is returned. scopedKernel :: (ScopedKernel -> SAST -> IO ()) -> ModGuts -> CoreM ModGuts instance Eq Direction instance Show Direction instance Eq SAST instance Ord SAST instance Show SAST module HERMIT.Plugin -- | Given a list of CommandLineOptions, produce the ModGuts -- to ModGuts function required to build a plugin. type HermitPass = PhaseInfo -> [CommandLineOption] -> ModGuts -> CoreM ModGuts -- | Build a hermit plugin. This mainly handles the per-module options. hermitPlugin :: HermitPass -> Plugin data CorePass FloatInwards :: CorePass LiberateCase :: CorePass PrintCore :: CorePass StaticArgs :: CorePass Strictness :: CorePass WorkerWrapper :: CorePass Specialising :: CorePass SpecConstr :: CorePass CSE :: CorePass Vectorisation :: CorePass Desugar :: CorePass DesugarOpt :: CorePass Tidy :: CorePass Prep :: CorePass Simplify :: CorePass FloatOutwards :: CorePass RuleCheck :: CorePass Passes :: CorePass PluginPass :: String -> CorePass NoOp :: CorePass Unknown :: CorePass getCorePass :: CoreToDo -> CorePass ghcPasses :: [(CorePass, CoreToDo)] data PhaseInfo PhaseInfo :: Int -> [CorePass] -> [CorePass] -> PhaseInfo phaseNum :: PhaseInfo -> Int phasesDone :: PhaseInfo -> [CorePass] phasesLeft :: PhaseInfo -> [CorePass] instance Read CorePass instance Show CorePass instance Eq CorePass instance Read PhaseInfo instance Show PhaseInfo instance Eq PhaseInfo module HERMIT.PrettyPrinter.Clean -- | Pretty print a fragment of GHC Core using HERMIT's "Clean" pretty -- printer. ppCoreTC :: PrettyH CoreTC ppModGuts :: PrettyH ModGuts ppCoreProg :: PrettyH CoreProg ppCoreBind :: PrettyH CoreBind ppCoreExpr :: PrettyH CoreExpr ppCoreAlt :: PrettyH CoreAlt ppKindOrType :: PrettyH KindOrType ppCoercion :: PrettyH Coercion module HERMIT.Shell.Types -- | There are four types of commands. data ShellCommand -- | Command that modifies the state of the (scoped) kernel. KernelEffect :: KernelEffect -> ShellCommand -- | Command that modifies the state of the shell. ShellEffect :: ShellEffect -> ShellCommand -- | Command that queries the AST with a Translate (read only). QueryFun :: QueryFun -> ShellCommand -- | Command that otherwise controls HERMIT (abort, resume, save, etc). MetaCommand :: MetaCommand -> ShellCommand -- | KernelEffects are things that affect the state of the Kernel - Apply a -- rewrite (giving a whole new lower-level AST). - Change the current -- location using a computed path. - Change the currect location using -- directions. - Begin or end a scope. - Delete an AST - Run a -- precondition or other predicate that must not fail. data KernelEffect :: * Apply :: RewriteH g -> KernelEffect Pathfinder :: TranslateH g LocalPathH -> KernelEffect Direction :: Direction -> KernelEffect BeginScope :: KernelEffect EndScope :: KernelEffect Delete :: SAST -> KernelEffect CorrectnessCritera :: TranslateH g () -> KernelEffect data ShellEffect :: * CLSModify :: (CommandLineState -> IO CommandLineState) -> ShellEffect data QueryFun :: * QueryString :: TranslateH g String -> QueryFun QueryDocH :: (PrettyC -> PrettyH CoreTC -> TranslateH CoreTC DocH) -> QueryFun Display :: QueryFun Inquiry :: (CommandLineState -> IO String) -> QueryFun message :: String -> QueryFun type RewriteName = String data MetaCommand Resume :: MetaCommand Abort :: MetaCommand Continue :: MetaCommand Diff :: SAST -> SAST -> MetaCommand Dump :: String -> String -> Int -> MetaCommand LoadFile :: ScriptName -> FilePath -> MetaCommand SaveFile :: FilePath -> MetaCommand ScriptToRewrite :: RewriteName -> ScriptName -> MetaCommand DefineScript :: ScriptName -> String -> MetaCommand RunScript :: ScriptName -> MetaCommand SaveScript :: FilePath -> ScriptName -> MetaCommand SeqMeta :: [MetaCommand] -> MetaCommand -- | A composite meta-command for running a loaded script immediately. The -- script is given the same name as the filepath. loadAndRun :: FilePath -> MetaCommand data VersionCmd Back :: VersionCmd Step :: VersionCmd Goto :: Int -> VersionCmd GotoTag :: String -> VersionCmd AddTag :: String -> VersionCmd data CLException CLAbort :: CLException CLResume :: SAST -> CLException CLContinue :: CommandLineState -> CLException CLError :: String -> CLException newtype CLM m a CLM :: ErrorT CLException (StateT CommandLineState m) a -> CLM m a unCLM :: CLM m a -> ErrorT CLException (StateT CommandLineState m) a abort :: Monad m => CLM m () resume :: Monad m => SAST -> CLM m () continue :: Monad m => CommandLineState -> CLM m () runCLM :: CommandLineState -> CLM m a -> m (Either CLException a, CommandLineState) iokm2clm' :: MonadIO m => String -> (a -> CLM m b) -> IO (KureM a) -> CLM m b iokm2clm :: MonadIO m => String -> IO (KureM a) -> CLM m a iokm2clm'' :: MonadIO m => IO (KureM a) -> CLM m a data VersionStore VersionStore :: [(SAST, ExprH, SAST)] -> [(String, SAST)] -> VersionStore vs_graph :: VersionStore -> [(SAST, ExprH, SAST)] vs_tags :: VersionStore -> [(String, SAST)] newSAST :: ExprH -> SAST -> CommandLineState -> CommandLineState data CommandLineState CommandLineState :: SAST -> PrettyH CoreTC -> PrettyOptions -> (Handle -> PrettyOptions -> Either String DocH -> IO ()) -> Int -> Bool -> Bool -> TVar (Map String Int) -> Bool -> Bool -> PathH -> Dictionary -> [(ScriptName, Script)] -> ScopedKernel -> SAST -> VersionStore -> CommandLineState -- | the current AST cl_cursor :: CommandLineState -> SAST -- | which pretty printer to use cl_pretty :: CommandLineState -> PrettyH CoreTC -- | the options for the pretty printer cl_pretty_opts :: CommandLineState -> PrettyOptions -- | the way of outputing to the screen cl_render :: CommandLineState -> Handle -> PrettyOptions -> Either String DocH -> IO () -- | console height, in lines cl_height :: CommandLineState -> Int -- | keyboard input the nav panel cl_nav :: CommandLineState -> Bool -- | if running a script cl_running_script :: CommandLineState -> Bool -- | the list of ticked messages cl_tick :: CommandLineState -> TVar (Map String Int) -- | if true, run Core Lint on module after each rewrite cl_corelint :: CommandLineState -> Bool -- | if true, abort on *any* failure cl_failhard :: CommandLineState -> Bool -- | path to beginning of window, always a prefix of focus path in kernel -- these four should be in a reader cl_window :: CommandLineState -> PathH cl_dict :: CommandLineState -> Dictionary cl_scripts :: CommandLineState -> [(ScriptName, Script)] cl_kernel :: CommandLineState -> ScopedKernel cl_initSAST :: CommandLineState -> SAST cl_version :: CommandLineState -> VersionStore type ScriptName = String instance Typeable KernelEffect instance Typeable QueryFun instance Typeable ShellEffect instance Typeable MetaCommand instance Show VersionCmd instance MonadIO m => MonadIO (CLM m) instance Monad m => MonadError CLException (CLM m) instance Monad m => MonadState CommandLineState (CLM m) instance Monad m => MonadCatch (CLM m) instance MonadTrans CLM instance Monad m => Monad (CLM m) instance Error CLException instance Extern ShellEffect instance Extern MetaCommand instance Extern QueryFun instance Extern KernelEffect module HERMIT.Shell.ScriptToRewrite -- | Insert a script into the Dictionary. addScriptToDict :: Monad m => ScriptName -> Script -> Dictionary -> m Dictionary module HERMIT.Shell.Renderer showRenderers :: QueryFun changeRenderer :: String -> ShellEffect newtype UnicodeTerminal UnicodeTerminal :: (Handle -> Maybe PathH -> IO ()) -> UnicodeTerminal shellRenderers :: [(String, Handle -> PrettyOptions -> Either String DocH -> IO ())] unicodeConsole :: Handle -> PrettyOptions -> Either String DocH -> IO () doSGR :: [SGR] -> UnicodeTerminal undoSGRWith :: [SGR] -> [Attr] -> UnicodeTerminal setHighlight :: PathH -> Handle -> Maybe PathH -> IO () instance RenderCode UnicodeTerminal instance Monoid UnicodeTerminal instance RenderSpecial UnicodeTerminal -- | Output the raw Expr constructors. Helpful for writing pattern matching -- rewrites. module HERMIT.PrettyPrinter.AST -- | Pretty print a fragment of GHC Core using HERMIT's "AST" pretty -- printer. This displays the tree of constructors using nested -- indentation. ppCoreTC :: PrettyH CoreTC ppModGuts :: PrettyH ModGuts ppCoreProg :: PrettyH CoreProg ppCoreBind :: PrettyH CoreBind ppCoreExpr :: PrettyH CoreExpr ppCoreAlt :: PrettyH CoreAlt ppKindOrType :: PrettyH Type ppCoercion :: PrettyH Coercion -- | Output the raw Expr constructors. Helpful for writing pattern matching -- rewrites. module HERMIT.PrettyPrinter.GHC -- | This pretty printer is just a reflection of GHC's standard pretty -- printer. ppCoreTC :: PrettyH CoreTC ppModGuts :: PrettyH ModGuts ppCoreProg :: PrettyH CoreProg ppCoreBind :: PrettyH CoreBind ppCoreExpr :: PrettyH CoreExpr ppCoreAlt :: PrettyH CoreAlt ppKindOrType :: PrettyH Type ppCoercion :: PrettyH Coercion module HERMIT.Shell.Dictionary -- | Create a dictionary from a list of Externals. mkDict :: [External] -> Dictionary -- | The pretty-printing dictionaries. pp_dictionary :: Map String (PrettyH CoreTC) module HERMIT.Shell.Externals -- | Interpret a boxed thing as one of the four possible shell command -- types. interpShellCommand :: [Interp ShellCommand] shell_externals :: [External] gc :: CommandLineState -> IO CommandLineState setWindow :: CommandLineState -> IO CommandLineState versionCmd :: VersionCmd -> CommandLineState -> IO CommandLineState showDerivationTree :: CommandLineState -> IO String showRefactorTrail :: (Eq a, Show a) => [(a, [String], a)] -> [(a, String)] -> a -> a -> [String] showGraph :: [(SAST, ExprH, SAST)] -> [(String, SAST)] -> SAST -> String displayScripts :: QueryFun showScripts :: [(ScriptName, Script)] -> String module HERMIT.Shell.Command -- | The first argument includes a list of files to load. commandLine :: MonadIO m => [CommandLineOption] -> Behavior -> [External] -> CLM m () unicodeConsole :: Handle -> PrettyOptions -> Either String DocH -> IO () diffDocH :: (MonadCatch m, MonadIO m) => PrettyOptions -> DocH -> DocH -> m String diffR :: Injection a CoreTC => PrettyOptions -> String -> RewriteH a -> RewriteH a performKernelEffect :: MonadIO m => KernelEffect -> ExprH -> CLM m () performQuery :: MonadIO m => QueryFun -> CLM m () performShellEffect :: MonadIO m => ShellEffect -> CLM m () performMetaCommand :: MonadIO m => MetaCommand -> CLM m () cl_kernel_env :: CommandLineState -> HermitMEnv getFocusPath :: MonadIO m => CLM m PathH shellComplete :: MVar CommandLineState -> String -> String -> IO [Completion] evalScript :: MonadIO m => String -> CLM m () instance Show CompletionType module HERMIT.Optimize optimize :: ([CommandLineOption] -> OM ()) -> Plugin query :: (Injection ModGuts g, Walker HermitC g) => TranslateH g a -> OM a run :: RewriteH Core -> OM () interactive :: [External] -> [CommandLineOption] -> OM () display :: OM () setPretty :: PrettyH CoreTC -> OM () setPrettyOptions :: PrettyOptions -> OM () at :: TranslateH Core LocalPathH -> OM a -> OM a phase :: Int -> OM () -> OM () after :: CorePass -> OM () -> OM () before :: CorePass -> OM () -> OM () allPhases :: OM () -> OM () firstPhase :: OM () -> OM () lastPhase :: OM () -> OM () data OM a omToIO :: CommandLineState -> PhaseInfo -> OM a -> IO (Either CLException a, CommandLineState) instance Monad OM instance MonadIO OM module HERMIT plugin :: Plugin