source: src/LIN/joint_LTL_LIN_paolo.ma @ 2208

Last change on this file since 2208 was 2208, checked in by tranquil, 8 years ago
  • moving some code around
  • changed immediates to hold beval in general, not only bytes
  • fixed RTLabsToRTL after redefinitions in front end
File size: 1.4 KB
Line 
1include "joint/Joint_paolo.ma".
2
3inductive 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
10inductive ltl_lin_seq : Type[0] ≝
11| SAVE_CARRY : ltl_lin_seq
12| RESTORE_CARRY : ltl_lin_seq.
13
14definition ltl_lin_params : unserialized_params ≝ mk_unserialized_params
15  (mk_step_params
16    (* acc_a_reg ≝ *) unit
17    (* acc_b_reg ≝ *) unit
18    (* acc_a_arg ≝ *) unit
19    (* acc_b_arg ≝ *) unit
20    (* dpl_reg   ≝ *) unit
21    (* dph_reg   ≝ *) unit
22    (* dpl_arg   ≝ *) unit
23    (* dph_arg   ≝ *) unit
24    (* snd_arg   ≝ *) hdw_argument
25    (* pair_move ≝ *) registers_move
26    (* call_args ≝ *) ℕ
27    (* call_dest ≝ *) unit
28    (* ext_seq ≝ *) ltl_lin_seq
29    (* ext_call ≝ *) void
30    (* ext_tailcall ≝ *) void
31  )
32  (mk_local_params
33    (mk_funct_params
34      (* resultT ≝ *) unit
35      (* paramsT ≝ *) unit)
36      (* localsT ≝ *) void).
37
38interpretation "move from acc" 'mov a b = (MOVE ?? (from_acc a b)).
39interpretation "move to acc" 'mov a b = (MOVE ?? (to_acc a b)).
40interpretation "move int to reg" 'mov a b = (MOVE ?? (int_to_reg a b)).
41interpretation "move int to acc" 'mov a b = (MOVE ?? (int_to_acc a b)).
Note: See TracBrowser for help on using the repository browser.