1 | include "joint/Joint_paolo.ma". |
---|
2 | |
---|
3 | inductive rtl_argument : Type[0] ≝ |
---|
4 | | Reg : register → rtl_argument |
---|
5 | | Imm : Byte → rtl_argument. |
---|
6 | |
---|
7 | coercion reg_to_rtl_argument : ∀r : register.rtl_argument ≝ Reg |
---|
8 | on _r : register to rtl_argument. |
---|
9 | |
---|
10 | coercion byte_to_rtl_argument : ∀b : Byte.rtl_argument ≝ Imm |
---|
11 | on _b : Byte to rtl_argument. |
---|
12 | |
---|
13 | definition imm_nat : nat → rtl_argument ≝ λn.Imm (nat_to_bv ? n). |
---|
14 | |
---|
15 | coercion nat_to_rtl_argument : ∀n : nat.rtl_argument ≝ imm_nat |
---|
16 | on _n : nat to rtl_argument. |
---|
17 | |
---|
18 | (*CSC: XXX PROBLEM HERE. Tailcalls are not instructions, but statements since they |
---|
19 | are not sequential. Thus there is a dummy label at the moment in the code. |
---|
20 | To be fixed once we understand exactly what to do with tail calls. *) |
---|
21 | inductive rtl_statement_extension: Type[0] ≝ |
---|
22 | | rtl_st_ext_stack_address: register → register → rtl_statement_extension |
---|
23 | | rtl_st_ext_call_ptr: register → register → list rtl_argument → list register → rtl_statement_extension |
---|
24 | | rtl_st_ext_tailcall_id: ident → list rtl_argument → rtl_statement_extension |
---|
25 | | rtl_st_ext_tailcall_ptr: register → register → list rtl_argument → rtl_statement_extension. |
---|
26 | |
---|
27 | |
---|
28 | inductive rtl_move : Type[0] ≝ |
---|
29 | | CARRY : bool → rtl_move |
---|
30 | | REG : register → rtl_argument → rtl_move. |
---|
31 | |
---|
32 | (* avoid expansion *) |
---|
33 | definition rtl_params : graph_params ≝ mk_graph_params |
---|
34 | (mk_inst_params |
---|
35 | (* acc_a_reg ≝ *) register |
---|
36 | (* acc_b_reg ≝ *) register |
---|
37 | (* acc_a_arg ≝ *) rtl_argument |
---|
38 | (* acc_b_arg ≝ *) rtl_argument |
---|
39 | (* dpl_reg ≝ *) register |
---|
40 | (* dph_reg ≝ *) register |
---|
41 | (* dpl_arg ≝ *) rtl_argument |
---|
42 | (* dph_arg ≝ *) rtl_argument |
---|
43 | (* snd_arg ≝ *) rtl_argument |
---|
44 | (* operator1 ≝ *) Op1 |
---|
45 | (* operator2 ≝ *) Op2 |
---|
46 | (* pair_move ≝ *) rtl_move |
---|
47 | (* call_args ≝ *) (list rtl_argument) |
---|
48 | (* call_dest ≝ *) (list register) |
---|
49 | (* extend_statements ≝ *) rtl_statement_extension |
---|
50 | (* ext_forall_labels ≝ *) (λP.λes.True)) |
---|
51 | (mk_local_params |
---|
52 | (mk_funct_params |
---|
53 | (* resultT ≝ *) (list register) |
---|
54 | (* paramsT ≝ *) (list register)) |
---|
55 | (* localsT ≝ *) (list register)). |
---|
56 | |
---|
57 | (* aid unification *) |
---|
58 | include "hints_declaration.ma". |
---|
59 | unification hint 0 ≔ |
---|
60 | (*---------------*) ⊢ |
---|
61 | acc_a_reg (g_inst_pars rtl_params) ≡ register. |
---|
62 | unification hint 0 ≔ |
---|
63 | (*---------------*) ⊢ |
---|
64 | acc_b_reg (g_inst_pars rtl_params) ≡ register. |
---|
65 | unification hint 0 ≔ |
---|
66 | (*---------------*) ⊢ |
---|
67 | acc_a_arg (g_inst_pars rtl_params) ≡ rtl_argument. |
---|
68 | unification hint 0 ≔ |
---|
69 | (*---------------*) ⊢ |
---|
70 | acc_b_arg (g_inst_pars rtl_params) ≡ rtl_argument. |
---|
71 | unification hint 0 ≔ |
---|
72 | (*---------------*) ⊢ |
---|
73 | dpl_reg (g_inst_pars rtl_params) ≡ register. |
---|
74 | unification hint 0 ≔ |
---|
75 | (*---------------*) ⊢ |
---|
76 | dph_reg (g_inst_pars rtl_params) ≡ register. |
---|
77 | unification hint 0 ≔ |
---|
78 | (*---------------*) ⊢ |
---|
79 | dpl_arg (g_inst_pars rtl_params) ≡ rtl_argument. |
---|
80 | unification hint 0 ≔ |
---|
81 | (*---------------*) ⊢ |
---|
82 | dph_arg (g_inst_pars rtl_params) ≡ rtl_argument. |
---|
83 | unification hint 0 ≔ |
---|
84 | (*---------------*) ⊢ |
---|
85 | snd_arg (g_inst_pars rtl_params) ≡ rtl_argument. |
---|
86 | unification hint 0 ≔ |
---|
87 | (*---------------*) ⊢ |
---|
88 | operator1 (g_inst_pars rtl_params) ≡ Op1. |
---|
89 | unification hint 0 ≔ |
---|
90 | (*---------------*) ⊢ |
---|
91 | operator2 (g_inst_pars rtl_params) ≡ Op2. |
---|
92 | unification hint 0 ≔ |
---|
93 | (*---------------*) ⊢ |
---|
94 | pair_move (g_inst_pars rtl_params) ≡ rtl_move. |
---|
95 | unification hint 0 ≔ |
---|
96 | (*---------------*) ⊢ |
---|
97 | call_args (g_inst_pars rtl_params) ≡ list rtl_argument. |
---|
98 | unification hint 0 ≔ |
---|
99 | (*---------------*) ⊢ |
---|
100 | call_dest (g_inst_pars rtl_params) ≡ list register. |
---|
101 | |
---|
102 | check (λglobals,r.OP2 rtl_params globals Or r r r) |
---|
103 | |
---|
104 | definition rtl_instruction ≝ joint_instruction rtl_params. |
---|
105 | definition rtl_statement ≝ joint_statement rtl_params. |
---|
106 | |
---|
107 | |
---|
108 | definition reg_from_nat : ∀globals.register → ℕ → rtl_instruction globals ≝ |
---|
109 | λglobals,r,k. |
---|
110 | MOVE rtl_params globals (REG r (imm_nat k)). |
---|
111 | |
---|
112 | definition reg_from_byte : ∀globals.register → Byte → rtl_instruction globals ≝ |
---|
113 | λglobals,r,k. |
---|
114 | MOVE rtl_params globals (REG r (Imm k)). |
---|
115 | |
---|
116 | definition reg_from_reg : ∀globals.register → register → rtl_instruction globals ≝ |
---|
117 | λglobals,r,k. |
---|
118 | MOVE … (REG r (Reg k)). |
---|
119 | |
---|
120 | definition set_carry : ∀globals.rtl_instruction globals ≝ |
---|
121 | λglobals.MOVE … (CARRY true). |
---|
122 | |
---|
123 | definition clear_carry : ∀globals.rtl_instruction globals ≝ |
---|
124 | λglobals.MOVE … (CARRY false). |
---|
125 | |
---|
126 | |
---|
127 | definition rtl_internal_function ≝ |
---|
128 | λglobals. joint_internal_function globals rtl_params. |
---|
129 | |
---|
130 | definition rtl_program ≝ joint_program rtl_params. |
---|
131 | |
---|
132 | (************ Same without tail calls ****************) |
---|
133 | |
---|
134 | inductive rtlntc_statement_extension: Type[0] ≝ |
---|
135 | | rtlntc_st_ext_stack_address: register → register → rtlntc_statement_extension |
---|
136 | | rtlntc_st_ext_call_ptr: register → register → list register → list register → rtlntc_statement_extension. |
---|
137 | |
---|
138 | definition rtlntc_params : graph_params ≝ mk_graph_params |
---|
139 | (mk_inst_params |
---|
140 | (* acc_a_reg ≝ *) register |
---|
141 | (* acc_b_reg ≝ *) register |
---|
142 | (* acc_a_arg ≝ *) rtl_argument |
---|
143 | (* acc_b_arg ≝ *) rtl_argument |
---|
144 | (* dpl_reg ≝ *) register |
---|
145 | (* dph_reg ≝ *) register |
---|
146 | (* dpl_arg ≝ *) rtl_argument |
---|
147 | (* dph_arg ≝ *) rtl_argument |
---|
148 | (* snd_arg ≝ *) rtl_argument |
---|
149 | (* operator1 ≝ *) Op1 |
---|
150 | (* operator2 ≝ *) Op2 |
---|
151 | (* pair_move ≝ *) rtl_move |
---|
152 | (* call_args ≝ *) (list rtl_argument) |
---|
153 | (* call_dest ≝ *) (list register) |
---|
154 | (* extend_statements ≝ *) rtlntc_statement_extension |
---|
155 | (* ext_forall_labels ≝ *) (λP.λes.True)) |
---|
156 | (mk_local_params |
---|
157 | (mk_funct_params |
---|
158 | (* resultT ≝ *) (list register) |
---|
159 | (* paramsT ≝ *) (list register)) |
---|
160 | (* localsT ≝ *) (list register)). |
---|
161 | |
---|
162 | definition rtlntc_statement ≝ joint_statement rtlntc_params. |
---|
163 | |
---|
164 | definition rtlntc_internal_function ≝ |
---|
165 | λglobals. joint_internal_function … globals rtlntc_params. |
---|
166 | |
---|
167 | definition rtlntc_program ≝ joint_program rtlntc_params. |
---|