|
Last change
on this file since 2244 was
2217,
checked in by tranquil, 9 years ago
|
- collapsed step_params, unserialized_params, funct_params and local_params into one (unserialized_params)
- completed update of RTL, LTL and LIN semantics
|
|
File size:
1.3 KB
|
| Line | |
|---|
| 1 | include "joint/Joint_paolo.ma". |
|---|
| 2 | |
|---|
| 3 | inductive registers_move: Type[0] ≝ |
|---|
| 4 | | from_acc: Register → unit → registers_move |
|---|
| 5 | | to_acc: unit → Register → registers_move |
|---|
| 6 | | int_to_reg : Register → beval → registers_move |
|---|
| 7 | | int_to_acc : unit → beval → registers_move. |
|---|
| 8 | (* the last is redudant, but kept for notation's sake *) |
|---|
| 9 | |
|---|
| 10 | inductive ltl_lin_seq : Type[0] ≝ |
|---|
| 11 | | SAVE_CARRY : ltl_lin_seq |
|---|
| 12 | | RESTORE_CARRY : ltl_lin_seq. |
|---|
| 13 | |
|---|
| 14 | definition LTL_LIN : unserialized_params ≝ mk_unserialized_params |
|---|
| 15 | (* acc_a_reg ≝ *) unit |
|---|
| 16 | (* acc_b_reg ≝ *) unit |
|---|
| 17 | (* acc_a_arg ≝ *) unit |
|---|
| 18 | (* acc_b_arg ≝ *) unit |
|---|
| 19 | (* dpl_reg ≝ *) unit |
|---|
| 20 | (* dph_reg ≝ *) unit |
|---|
| 21 | (* dpl_arg ≝ *) unit |
|---|
| 22 | (* dph_arg ≝ *) unit |
|---|
| 23 | (* snd_arg ≝ *) hdw_argument |
|---|
| 24 | (* pair_move ≝ *) registers_move |
|---|
| 25 | (* call_args ≝ *) ℕ |
|---|
| 26 | (* call_dest ≝ *) unit |
|---|
| 27 | (* ext_seq ≝ *) ltl_lin_seq |
|---|
| 28 | (* ext_call ≝ *) void |
|---|
| 29 | (* ext_tailcall ≝ *) void |
|---|
| 30 | (* paramsT ≝ *) unit |
|---|
| 31 | (* localsT ≝ *) void. |
|---|
| 32 | |
|---|
| 33 | interpretation "move from acc" 'mov a b = (MOVE ?? (from_acc a b)). |
|---|
| 34 | interpretation "move to acc" 'mov a b = (MOVE ?? (to_acc a b)). |
|---|
| 35 | interpretation "move int to reg" 'mov a b = (MOVE ?? (int_to_reg a b)). |
|---|
| 36 | interpretation "move int to acc" 'mov a b = (MOVE ?? (int_to_acc a b)). |
|---|
Note: See
TracBrowser
for help on using the repository browser.
