source: src/LIN/joint_LTL_LIN.ma @ 2537

Last change on this file since 2537 was 2537, checked in by tranquil, 7 years ago

rolled back changes on calls in joint. Now the save_frame parameter
has a switch that tells whether the call is an ident one or a pointer one.
The idea is that in the latter case, from LTL onwards, the caller address is not saved (as it is done by explicit instructions

File size: 1.5 KB
Line 
1include "joint/Joint.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 → Byte → registers_move
7 | int_to_acc : unit → Byte → 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| LOW_ADDRESS : Register → label → ltl_lin_seq
14| HIGH_ADDRESS : Register → label → ltl_lin_seq.
15
16definition ltl_lin_seq_labels ≝ λs.match s with
17[ LOW_ADDRESS _ lbl ⇒ [ lbl ]
18| HIGH_ADDRESS _ lbl ⇒ [ lbl ]
19| _ ⇒ [ ]
20].
21
22definition LTL_LIN : unserialized_params ≝ mk_unserialized_params
23    (* acc_a_reg ≝ *) unit
24    (* acc_b_reg ≝ *) unit
25    (* acc_a_arg ≝ *) unit
26    (* acc_b_arg ≝ *) unit
27    (* dpl_reg   ≝ *) unit
28    (* dph_reg   ≝ *) unit
29    (* dpl_arg   ≝ *) unit
30    (* dph_arg   ≝ *) unit
31    (* snd_arg   ≝ *) hdw_argument
32    (* pair_move ≝ *) registers_move
33    (* call_args ≝ *) ℕ
34    (* call_dest ≝ *) unit
35    (* ext_seq ≝ *) ltl_lin_seq
36    (* ext_seq_labels ≝ *) ltl_lin_seq_labels
37    (* has_tailcalls ≝ *) false
38    (* paramsT ≝ *) unit
39    (* localsT ≝ *) void.
40
41interpretation "move from acc" 'mov a b = (MOVE ?? (from_acc a b)).
42interpretation "move to acc" 'mov a b = (MOVE ?? (to_acc a b)).
43interpretation "move int to reg" 'mov a b = (MOVE ?? (int_to_reg a b)).
44interpretation "move int to acc" 'mov a b = (MOVE ?? (int_to_acc a b)).
Note: See TracBrowser for help on using the repository browser.