| ;; |
| ;; Auxiliary definitions used for describing execution notation |
| ;; |
| |
| ;; Reduction |
| |
| relation NotationReduct: ~> instr* hint(tabular) |
| |
| rule NotationReduct/2: |
| ~> (CONST F64 q_1) (CONST F64 q_4) (CONST F64 q_3) (BINOP F64 ADD) (BINOP F64 MUL) |
| |
| rule NotationReduct/3: |
| ~> (CONST F64 q_1) (CONST F64 q_5) (BINOP F64 MUL) |
| |
| rule NotationReduct/4: |
| ~> (CONST F64 q_6) |
| |
| |
| ;; Frames and Labels |
| |
| def $instrdots : instr* hint(show `...) |
| |
| syntax label hint(desc "label") = LABEL_ n `{instr*} hint(show LABEL_%#%) |
| syntax callframe hint(desc "call frame") = FRAME_ n `{frame} hint(show FRAME_%#%) |
| |
| var L : label |
| |
| |
| ;; Allocation |
| |
| def $allocX(syntax X, syntax Y, store, X, Y) : (store, addr) hint(macro none) |
| def $allocXs(syntax X, syntax Y, store, X*, Y*) : (store, addr*) hint(show $allocX*#((%3, %4, %5))) hint(macro none) |
| def $allocXs(syntax X, syntax Y, s, eps, eps) = (s, eps) |
| def $allocXs(syntax X, syntax Y, s, X X'*, Y Y'*) = (s_2, a a'*) |
| -- if (s_1, a) = $allocX(syntax X, syntax Y, s, X, Y) |
| -- if (s_2, a'*) = $allocXs(syntax X, syntax Y, s_1, X'*, Y'*) |
