Load Context

The load context is defined in 7.0-load-context.watsup. It is a single flat layer, unlike the three-layered typing context. This reflects its narrower purpose: it only needs to hold information that the evaluator will look up by name at runtime.

Elaborated Callable Definitions

Before defining the context itself, the spec introduces the intermediate representation (IR) for callables. The IR for each callable kind pairs the callable’s elaborated parameter list with its body:

syntax actionDeclarationIR =
  ACTION nameIR
    `( parameterIR* `) blockStatement

syntax parserDeclarationIR =
  PARSER nameIR
    `( parameterIR* `)
    `{ parserLocalDeclarationList parserStateList `}

syntax controlDeclarationIR =
  CONTROL nameIR
    `( parameterIR* `)
    `{ controlLocalDeclarationList APPLY controlBody `}

syntax callableDef =
  | actionDeclarationIR
  | parserDeclarationIR
  | controlDeclarationIR

The surface syntax uses parameterList, containing raw parameter names and type annotations. The IR replaces this with parameterIR*, a list of direction-annotated internal types produced by elaboration. The loading phase is responsible for attaching the correct parameterIR* from the typingContext to the callable body from the source declaration.

The Load Context

syntax globalLoadLayer =
  { CALLABLE_TYPE callableTypeDefEnv,
    CALLABLE callableDefEnv,
    PARSER parserDeclarationIR?,
    CONTROL controlDeclarationIR? }

syntax loadContext = globalLoadLayer

var LC : loadContext

The four fields serve two purposes:

• CALLABLE_TYPE is copied directly from TC.GLOBAL.CALLABLE at initialization. It gives the loading rules read-only access to the elaborated parameter types from the typing phase, so each callable body can be paired with the correct parameterIR*.
• CALLABLE starts empty and is populated as declarations are processed. By the end of loading it contains the full callableDef for every action, parser, and control in the program.
• PARSER and CONTROL start as eps (absent) and are set when the instantiation declaration is encountered. They identify the specific parser and control that serve as the NanoSwitch entry point.

Initialization

dec $make_loadContext(typingContext) : loadContext
def $make_loadContext(TC) = LC
  -- if LC
      = {
          CALLABLE_TYPE TC.GLOBAL.CALLABLE,
          CALLABLE $empty_callableDefEnv,
          PARSER eps,
          CONTROL eps }

$make_loadContext seeds the context from the typingContext that typing produced. The callable type information is carried over; everything else starts empty and is filled in as declarations are loaded.

Helpers

The spec defines three helper functions for working with the load context.

$find_callableDef_l looks up a callable body by its identifier:

dec $find_callableDef_l(loadContext, callableId) : callableDef
def $find_callableDef_l(LC, callableId) = callableDef
  -- if callableDef
      = $find_map<callableId, callableDef>(LC.CALLABLE, callableId)

$add_callableDef_l inserts a new callable body. It first checks that the identifier is not already present, preventing duplicate definitions:

dec $add_callableDef_l(loadContext, callableId, callableDef)
  : loadContext

def $add_callableDef_l(LC, callableId, callableDef)
  = LC'
  -- if callableDefEnv = LC.CALLABLE
  -- if ~$in_set<callableId>(
        $dom_map<callableId, callableDef>(callableDefEnv),
        callableId
      )
  -- if callableDefEnv'
      = $add_map<callableId, callableDef>(
          callableDefEnv,
          callableId,
          callableDef
        )
  -- if LC' = LC[ .CALLABLE = callableDefEnv' ]

$find_callableTypeDef_l looks up a callable’s elaborated type from the CALLABLE_TYPE field. Loading rules call this to retrieve the parameterIR* that was computed during type checking:

dec $find_callableTypeDef_l(loadContext, callableId) : callableTypeDef
def $find_callableTypeDef_l(LC, callableId) = callableTypeDef
  -- if callableTypeDef
      = $find_map<callableId, callableTypeDef>(LC.CALLABLE_TYPE, callableId)