Loading Declarations

The loading rules are defined in 7.1-load-declaration.watsup. The central relation is Decl_load, which processes a single declaration and returns an updated loadContext.

relation Decl_load:
  loadContext |- declaration -| loadContext
  hint(input %0 %1)

Most declaration kinds either pass through unchanged or build a callableDef and register it. The interesting cases also retrieve elaborated parameter types from CALLABLE_TYPE.

Passthrough Rules

Type declarations, extern declarations, and match-kind declarations do not contribute anything to the load context. Each was fully handled during type checking. Their loading rules are one-liners that pass the context through unchanged:

rule Decl_load/typeDeclaration:
  LC |- typeDeclaration -| LC

rule Decl_load/externDeclaration:
  LC |- externDeclaration -| LC

rule Decl_load/matchKindDeclaration:
  LC |- MATCH_KIND `{ nameList `} -| LC

Action, Parser, and Control Declarations

All three rules follow the same pattern: extract the callable’s name from the source declaration, look up the elaborated parameterIR* that type checking stored in CALLABLE_TYPE, pair it with the body to form the IR, and register the result.

Here is the action rule:

rule Decl_load/actionDeclaration:
  LC_0 |- actionDeclaration -| LC_1
  -- if ACTION name_action `( _ `) blockStatement = actionDeclaration
  -- if callableId = $id(name_action)
  -- if ACTION parameterIR* = $find_callableTypeDef_l(LC_0, callableId)
  -- if actionDeclarationIR
      = ACTION callableId `( parameterIR* `) blockStatement
  -- if LC_1 = $add_callableDef_l(LC_0, callableId, actionDeclarationIR)

The parameter list in the source declaration is matched with _, discarding the raw surface parameters. The elaborated parameterIR* is fetched from CALLABLE_TYPE instead. This is why CALLABLE_TYPE exists in the load context: it gives loading rules read access to what type checking already computed, without re-running elaboration.

The parser and control rules are identical in structure, substituting PARSER and CONTROL for ACTION and including the body fields specific to each:

rule Decl_load/parserDeclaration:
  LC_0 |- parserDeclaration -| LC_1
  -- if PARSER name
    `( parameterList `)
    `{ parserLocalDeclarationList parserStateList `} = parserDeclaration
  -- if callableId = $id(name)
  -- if PARSER parameterIR* = $find_callableTypeDef_l(LC_0, callableId)
  -- if parserDeclarationIR
      = PARSER callableId
          `( parameterIR* `)
          `{ parserLocalDeclarationList parserStateList `}
  -- if LC_1 = $add_callableDef_l(LC_0, callableId, parserDeclarationIR)

rule Decl_load/controlDeclaration:
  LC_0 |- controlDeclaration -| LC_1
  -- if CONTROL name
    `( parameterList `)
    `{ controlLocalDeclarationList APPLY controlBody `} = controlDeclaration
  -- if callableId = $id(name)
  -- if CONTROL parameterIR* = $find_callableTypeDef_l(LC_0, callableId)
  -- if controlDeclarationIR
      = CONTROL callableId
          `( parameterIR* `)
          `{ controlLocalDeclarationList APPLY controlBody `}
  -- if LC_1 = $add_callableDef_l(LC_0, callableId, controlDeclarationIR)

Instantiation

The instantiation rule is different from the others. Its job is not to build a callableDef but to record which parser and control serve as the NanoSwitch entry point.

rule Decl_load/instantiation:
  LC_0 |- (_TID typeId_target) `( argumentList `) name ';' -| LC_1
  -- if argument* = $flatten_argumentList(argumentList)
  -- if (_TID callableId_parser) `( _ `) = argument*[0]
  -- if parserDeclarationIR
      = $find_callableDef_l(LC_0, callableId_parser)
  -- if (_TID callableId_control) `( _ `) = argument*[1]
  -- if controlDeclarationIR
      = $find_callableDef_l(LC_0, callableId_control)
  -- if LC_1
      = LC_0[ .PARSER = parserDeclarationIR ][ .CONTROL = controlDeclarationIR ]

The NanoSwitch(Parser(), Filter()) main; instantiation declaration passes the parser and control as its first two arguments. The rule extracts their names from argument*[0] and argument*[1], looks up each callableDef from the CALLABLE map, and writes the results into LC.PARSER and LC.CONTROL. The parser and control declarations must already be in CALLABLE when this rule fires, so declaration order matters.

Sequencing and Entry Point

Decls_load sequences declarations using the same nil/cons threading pattern seen throughout the spec:

rule Decls_load/nil:
  LC_0 |- eps -| LC_0

rule Decls_load/cons:
  LC_0 |- declaration_h :: declaration_t* -| LC_2
  -- Decl_load: LC_0 |- declaration_h -| LC_1
  -- Decls_load: LC_1 |- declaration_t* -| LC_2

Program_load is the top-level entry point. It initializes a fresh loadContext from the typingContext produced by type checking, then threads all declarations through Decls_load:

relation Program_load:
  typingContext |- program -| loadContext
  hint(input %0 %1)

rule Program_load:
  TC |- program -| LC'
  -- if declaration* = $flatten_program(program)
  -- if LC = $make_loadContext(TC)
  -- Decls_load: LC |- declaration* -| LC'

The resulting LC' is passed to $make_evalContext, which combines it with TC to build the evalContext used throughout execution.