diff --git a/src/posts/secd.md b/src/posts/secd.md index 490aded..36017c1 100644 --- a/src/posts/secd.md +++ b/src/posts/secd.md @@ -76,43 +76,21 @@ data Inst All stacks grow from right to left, that is, the left most element is at the top of the stack. -{% katexmm %} - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
BeforeAfter
ControlEnvStackControlEnvStack
Const i : cescei : s
Global i : cesceGlobals[i] : s
Local i : cesc ee[i] : s
Closure n a : $c_1$ ... $c_n$ : cesceClosure a {e} [$c_1$ ... $c_n$] : s
App : ceClosure {e'} [c'] : v : sc'v : e'Closure$^0$ {e} [c] : s
App : ceClosure$^n$ {e'} [c'] : v : sceClosure$^{n - 1}$ {v : e'} [c'] : s
Ret : c ev : Closure$^0$ \{e'\} [c'] : s c'e' v : s
Dup : cev : scev : v : s
Add : c ev : scev + v : s
-{% endkatexmm %} + +| Before | | | After | | | +| ----------------------------------- | --- | -------------------------------- | ------- | ------ | --------------------------------------- | +| Control | Env | Stack | Control | Env | Stack | +| Const i : c | e | s | c | e | i : s | +| Global i : c | e | s | c | e | Globals\[i\] : s | +| Local i : c | e | s | c | e | e\[i\] : s | +| Closure n a : $c\_1$ ... $c\_n$ : c | e | s | c | e | Closure a {e} \[$c\_1$ ... $c\_n$\] : s | +| App : c | e | Closure {e'} \[c'\] : v : s | c' | v : e' | Closure⁰ {e} \[c\] : s | +| App : c | e | Closureⁿ {e'} \[c'\] : v : s | c | e | Closureⁿ⁻¹ {v : e'} \[c'\] : s | +| Ret : c | e | v : Closure⁰ {e'} \[c'\] : s | c' | e' | v : s | +| Dup : c | e | v : s | c | e | v : v : s | +| Add : c | e | v : s | c | e | v + v : s | ### An example