source: src/LIN/joint_LTL_LIN.ma @ 3096

Last change on this file since 3096 was 3014, checked in by tranquil, 8 years ago

ERTL to ERTLptr pass suppressed (it introduced a bug in the later ERTLptr to LTL), and integrated in a single ERTToLTL pass like before

File size: 2.0 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(* store low/high parts of label address in the accumulator *)
14| LOW_ADDRESS : label → ltl_lin_seq
15| HIGH_ADDRESS : label → ltl_lin_seq.
16
17definition ltl_lin_seq_labels ≝ λs.match s with
18[ LOW_ADDRESS lbl ⇒ [ lbl ]
19| HIGH_ADDRESS lbl ⇒ [ lbl ]
20| _ ⇒ [ ]
21].
22
23definition LTL_LIN_uns : unserialized_params ≝ mk_unserialized_params
24    (* acc_a_reg ≝ *) unit
25    (* acc_b_reg ≝ *) unit
26    (* acc_a_arg ≝ *) unit
27    (* acc_b_arg ≝ *) unit
28    (* dpl_reg   ≝ *) unit
29    (* dph_reg   ≝ *) unit
30    (* dpl_arg   ≝ *) unit
31    (* dph_arg   ≝ *) unit
32    (* snd_arg   ≝ *) hdw_argument
33    (* pair_move ≝ *) registers_move
34    (* call_args ≝ *) ℕ
35    (* call_dest ≝ *) unit
36    (* ext_seq ≝ *) ltl_lin_seq
37    (* ext_seq_labels ≝ *) ltl_lin_seq_labels
38    (* has_tailcalls ≝ *) false
39    (* paramsT ≝ *) unit.
40
41definition LTL_LIN_functs : get_pseudo_reg_functs LTL_LIN_uns ≝
42mk_get_pseudo_reg_functs ?
43(* acc_a_regs *) (λ_.[ ])
44(* acc_b_regs *) (λ_.[ ])
45(* acc_a_args *) (λ_.[ ])
46(* acc_b_args *) (λ_.[ ])
47(* dpl_regs *) (λ_.[ ])
48(* dph_regs *) (λ_.[ ])
49(* dpl_args *) (λ_.[ ])
50(* dph_args *) (λ_.[ ])
51(* snd_args *) (λ_.[ ])
52(* pair_move_regs *) (λ_.[ ])
53(* f_call_args *) (λ_.[ ])
54(* f_call_dest *) (λ_.[ ])
55(* ext_seq_regs *) (λ_.[ ])
56(* params_regs *) (λ_.[ ]).
57
58definition LTL_LIN ≝  mk_uns_params LTL_LIN_uns LTL_LIN_functs.
59
60interpretation "move from acc" 'mov a b = (MOVE ?? (from_acc a b)).
61interpretation "move to acc" 'mov a b = (MOVE ?? (to_acc a b)).
62interpretation "move int to reg" 'mov a b = (MOVE ?? (int_to_reg a b)).
63interpretation "move int to acc" 'mov a b = (MOVE ?? (int_to_acc a b)).
Note: See TracBrowser for help on using the repository browser.