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

Safe HaskellNone

Language.HERMIT.Kernel.Scoped

Synopsis

Documentation

data Direction Source

A primitive means of denoting navigation of a tree (within a local scope).

Constructors

L

Left

R

Right

U

Up

D

Down

T

Top

data LocalPath Source

The path within the current local scope.

moveLocally :: Direction -> LocalPath -> LocalPathSource

Movement confined within the local scope.

data ScopedKernel Source

An alternative HERMIT kernel, that provides scoping.

Constructors

ScopedKernel 

Fields

resumeS :: SAST -> IO ()
 
abortS :: IO ()
 
applyS :: SAST -> RewriteH Core -> HermitMEnv -> IO (KureMonad SAST)
 
queryS :: forall a. SAST -> TranslateH Core a -> HermitMEnv -> IO (KureMonad a)
 
deleteS :: SAST -> IO ()
 
listS :: IO [SAST]
 
pathS :: SAST -> IO [Path]
 
modPathS :: SAST -> (LocalPath -> LocalPath) -> HermitMEnv -> IO (KureMonad SAST)
 
beginScopeS :: SAST -> IO SAST
 
endScopeS :: SAST -> IO SAST
 

newtype SAST Source

A handle for an AST combined with scoping information.

Constructors

SAST Int 

Instances

scopedKernel :: (ScopedKernel -> SAST -> IO ()) -> ModGuts -> CoreM ModGutsSource

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.