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

Safe HaskellNone

HERMIT.Dictionary.Navigation

Contents

Synopsis

Navigation

externals :: [External]Source

Externals involving navigating to named entities.

occurrenceOfT :: (AddBindings c, ExtendPath c Crumb, ReadPath c Crumb, MonadCatch m) => (Var -> Bool) -> Translate c m CoreTC LocalPathHSource

Find the path to the first occurrence occurrence of a variable.

bindingOfT :: (AddBindings c, ExtendPath c Crumb, ReadPath c Crumb, MonadCatch m) => (Var -> Bool) -> Translate c m CoreTC LocalPathHSource

Find the path to the binding of a variable.

bindingGroupOfT :: (AddBindings c, ExtendPath c Crumb, ReadPath c Crumb, MonadCatch m) => (Var -> Bool) -> Translate c m CoreTC LocalPathHSource

Find the path to the binding group of a variable.

rhsOfT :: (AddBindings c, ExtendPath c Crumb, ReadPath c Crumb, MonadCatch m) => (Var -> Bool) -> Translate c m Core LocalPathHSource

Find the path to the RHS of a binding.

parentOfT :: MonadCatch m => Translate c m g LocalPathH -> Translate c m g LocalPathHSource

Discard the last crumb of a non-empty LocalPathH.

rhsOfTargetsT :: (ExtendPath c Crumb, AddBindings c, MonadCatch m) => Translate c m CoreTC VarSetSource

Find all possible targets of rhsOfT.

data Considerable Source

Language constructs that can be zoomed to.

considerables :: [(String, Considerable)]Source

Lookup table for constructs that can be considered; the keys are the arguments the user can give to the "consider" command.

considerConstructT :: (AddBindings c, ExtendPath c Crumb, ReadPath c Crumb, MonadCatch m) => Considerable -> Translate c m Core LocalPathHSource

Find the path to the first matching construct.

nthArgPath :: Monad m => Int -> Translate c m CoreExpr LocalPathHSource

Construct a path to the (n-1)th argument in a nested sequence of Apps.