Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Evaluation Context

Before writing a single evaluation rule, we need somewhere to store what the interpreter knows at runtime: which type names exist, which callables have been loaded, and which variables are currently in scope along with their runtime values. That storage is the evaluation context, defined in 8.00-eval-context.watsup.

If you have read Section 3.1, the structure here will look familiar. The evaluation context mirrors the three-layer design of the typing context, but maps names to values rather than types.

The Three Layers

syntax evalContext =
  { GLOBAL globalEvalLayer,
    BLOCK  blockEvalLayer,
    LOCAL  localEvalLayer }

Global layer holds information visible everywhere: the type definition environment, the callable definitions loaded by the loading phase, a global frame, the loaded parser declaration, and the loaded control declaration.

syntax globalEvalLayer =
  { TYPE     typeDefEnv,
    CALLABLE callableDefEnv,
    FRAME    frame,
    PARSER   parserDeclarationIR,
    CONTROL  controlDeclarationIR }

The PARSER and CONTROL fields are new compared to the typing context. At runtime the interpreter needs the full bodies of the top-level parser and control, not merely their type signatures, so the evaluation context carries the complete IR forms.

Block layer holds runtime values for the parameters and block-level declarations of the current parser or control block.

syntax blockEvalLayer =
  { FRAME frame }

Local layer holds variables declared inside a block body, as a stack of frames.

syntax localEvalLayer =
  { FRAMES frame* }

A frame is a map from nameIR to value:

syntax frame = map<nameIR, value>

Unlike the typing context, which stores a (direction, type) pair per name, a frame here stores the actual runtime value. Direction is irrelevant at evaluation time; what matters is the current contents of each variable.

Constructing the Initial Context

$make_evalContext builds the evaluation context from the typing context and load context produced by the loading phase:

def $make_evalContext(TC, LC) = EC
  -- if parserDeclarationIR = LC.PARSER
  -- if controlDeclarationIR = LC.CONTROL
  -- if globalEvalLayer
      = { TYPE TC.GLOBAL.TYPE,
          CALLABLE LC.CALLABLE,
          FRAME $empty_frame,
          PARSER parserDeclarationIR,
          CONTROL controlDeclarationIR }
  -- if blockEvalLayer = { FRAME $empty_frame }
  -- if localEvalLayer = { FRAMES ([ $empty_frame ]) }
  -- if EC
      = { GLOBAL globalEvalLayer,
          BLOCK  blockEvalLayer,
          LOCAL  localEvalLayer }

The type definitions come from the typing context (TC.GLOBAL.TYPE), while the callable definitions and loaded declarations come from the load context (LC). All three frames start empty; the interpreter fills them as it evaluates variable declarations and calls.

Context Inheritance

When the interpreter enters a new callable, it does not start with a blank slate. The global layer should still be accessible, but the block and local layers must be reset so that the new callable’s parameters and locals do not collide with the caller’s. $inherit_e handles this reset:

def $inherit_e(GLOBAL, EC)
  = EC[ .BLOCK = blockEvalLayer ][ .LOCAL = localEvalLayer ]
  -- if blockEvalLayer  = { FRAME $empty_frame }
  -- if localEvalLayer  = { FRAMES ([ $empty_frame ]) }

def $inherit_e(BLOCK, EC)
  = EC[ .LOCAL = localEvalLayer ]
  -- if localEvalLayer  = { FRAMES ([ $empty_frame ]) }

def $inherit_e(LOCAL, EC) = EC

The three clauses form a staircase: inheriting at GLOBAL scope resets both the block frame and the local stack; inheriting at BLOCK scope resets only the local stack; inheriting at LOCAL scope leaves everything untouched.

There is no counterpart to $inherit_e in the static semantics. Type checking walks each top-level declaration under the outer context and never invokes a callable body from an arbitrary caller, so it never needs to reset the block and local layers the way the interpreter does at a call site.

Helper Functions

The rest of 8.00-eval-context.watsup defines helper functions that closely mirror those in 5.00-typing-context.watsup from Section 3.1, so they are not covered in full here. Briefly:

  • Finders ($find_var_e, $find_callableDef_e, $find_typeDef_e): look up a name by walking the same local-then-block-then-global scope chain as the typing context finders.
  • Adders ($add_var_e): insert a new binding into the appropriate layer, refusing to overwrite an existing name.
  • Frame entry and exit ($enter_e, $exit_e): push and pop a fresh frame on the local stack when entering and leaving a block statement, the runtime counterpart to $enter_t / $exit_t.

One helper with no direct analog in the typing context is the updater ($update_var_e). The type checker never changes a variable’s type after declaration, but the interpreter must overwrite values on every assignment. The local updater walks the frame stack recursively until it finds the frame that owns the name:

def $update_var_e(LOCAL, EC, nameIR, value)
  = EC_pop'[ .LOCAL.FRAMES = frame_h :: EC_pop'.LOCAL.FRAMES ]
  -- if frame_h :: frame_t* = EC.LOCAL.FRAMES
  -- if ~$in_set<nameIR>($dom_map<nameIR, value>(frame_h), nameIR)
  -- if EC_pop  = EC[ .LOCAL.FRAMES = frame_t* ]
  -- if EC_pop' = $update_var_e(LOCAL, EC_pop, nameIR, value)

This clause fires when the name is not in the head frame: it pops the head, recurses on the tail, then pushes the head back on top of the updated context. Without it, assigning to a variable declared in an outer scope from inside a nested block would fail.

The EC Meta-variable

var EC : evalContext

EC is the typed meta-variable for the evaluation context, analogous to TC in the static semantics. Any identifier beginning with EC (EC', EC_0, EC_pop, etc.) is recognized by the elaborator as a value of type evalContext. You will see it threaded through almost every evaluation relation in the chapters that follow.

Exercise

Branch: exercise/5.1

Check out the exercise branch in the spec submodule:

git -C nano-p4/spec checkout exercise/5.1

Run the following test to observe the failure:

./nano-p4spectec eval nano-p4/spec -i nano-p4/include -p nano-p4/testdata/exercise/5.1.p4 -stf nano-p4/testdata/exercise/5.1.stf

The test should succeed, but the interpreter gets stuck. If you get stuck, Chapter 6 covers the debugging techniques that apply here. In 8.00-eval-context.watsup, the LOCAL updater clause that handles the case where a name is not in the head frame has been removed. Without it, assigning to a variable declared in an outer scope from inside a nested block fails silently.

Add the missing clause back to $update_var_e(LOCAL, ...) in 8.00-eval-context.watsup.

When you are done, restore the original branch:

git -C nano-p4/spec checkout main