Operational semantics in K

kframework / haskell-core-semantics

Haskell's Core in K.

Other

20 stars 0 forks source link

Operational semantics in K #4

Open ayberkt opened 7 years ago

ayberkt commented 7 years ago

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 commented 7 years ago

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 commented 7 years ago

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.