Operational semantics in K

[ayberkt]

Our primary goal is to implement the operational semantics in K. The following rules from the Eisenberg spec need to be implemented.

• [x] S_Var
• [x] S_App
• [x] S_Beta
• [x] S_Push
  • Deferred for now.
• [x] S_TPush
  • Deferred for now.
• [x] S_CPush
  • Deferred for now.
• [x] S_Trans
  • Deferred for now.
• [x] S_Cast
  • Deferred for now.
• [x] S_Tick
  • Deferred for now.
• [x] S_Case
  • Consider how this plays with S_LetRecCase.
• [x] S_MatchData
• [x] S_MatchLit
• [x] S_MatchDefault
• [x] S_CasePush
  • Deferred for now.
• [x] S_LetNonRec
• [x] S_LetRec
  • We should decide how to implement the modification of Σ.
• [x] S_LetRecApp
• [x] S_LetRecCast
  • Deferred for now.
• [ ] S_LetRecCase
  • We might need to discuss this further.
• [ ] S_LetRecFlat
  • We might need to discuss this further.
• [x] S_LetRecReturn

[ayberkt]

To implement S_Var, I and @lucaspena considered the following rule:

// S_Var
rule
  <k> tmVar(_, name(R)) => E ... </k>
  <store> ... L |-> thunk(E, _) ... </store>
  <env> ... R |-> val(L) ... </env>

Does this seem correct to you @bmmoore ? Do we need to do something else for data constructors or closures? How would you implement this S_Var rule from the Eisenberg document?

[bmmoore]

You need to use the saved environment while evaluating the thunk, and include something to update the store with the result. For values that have already been forced, I think just evaluating to val(L) is correct. Indirection in the store may need to be handled.