1 | include "joint/Joint_paolo.ma". |
---|
2 | include "utilities/bindLists.ma". |
---|
3 | |
---|
4 | (* general type of functions generating fresh things *) |
---|
5 | (* type T is the syntactic type of the generated things *) |
---|
6 | (* (sig for RTLabs registers, unit in others ) *) |
---|
7 | definition freshT ≝ λg.λpars : params.λX,T : Type[0]. |
---|
8 | T → state_monad (joint_internal_function … g pars) X. |
---|
9 | |
---|
10 | definition rtl_ertl_fresh_reg: |
---|
11 | ∀inst_pars,funct_pars,globals. |
---|
12 | freshT globals (rtl_ertl_params inst_pars funct_pars) register unit ≝ |
---|
13 | λinst_pars,var_pars,globals,it,def. |
---|
14 | let 〈r, runiverse〉 ≝ fresh … (joint_if_runiverse … def) in |
---|
15 | 〈set_locals ?? (set_runiverse ?? def runiverse)(r::joint_if_locals ?? def), r〉. |
---|
16 | |
---|
17 | let rec rtl_ertl_fresh_regs inst_pars funct_pars globals (n : ℕ) on n : |
---|
18 | freshT globals (rtl_ertl_params inst_pars funct_pars) (list register) unit ≝ |
---|
19 | match n with |
---|
20 | [ O ⇒ λ_. return [ ] |
---|
21 | | S n' ⇒ λ_. |
---|
22 | ! regs' ← rtl_ertl_fresh_regs inst_pars funct_pars globals n' it; |
---|
23 | ! reg ← rtl_ertl_fresh_reg inst_pars funct_pars globals it; |
---|
24 | return (reg :: regs') |
---|
25 | ]. |
---|
26 | |
---|
27 | lemma rtl_ertl_fresh_regs_length: |
---|
28 | ∀i_pars,f_pars,globals.∀def: joint_internal_function … globals |
---|
29 | (rtl_ertl_params i_pars f_pars). ∀n: nat. |
---|
30 | |(\snd (rtl_ertl_fresh_regs … n it def))| = n. |
---|
31 | #ipars#fpars #globals #def #n elim n |
---|
32 | [ % |
---|
33 | | #m whd in ⊢ (? → ??(??(???%))?); @pair_elim |
---|
34 | #def' #regs #EQ>EQ |
---|
35 | whd in ⊢ (? → ??(??(???%))?); @pair_elim #def'' #reg #_ normalize // ] |
---|
36 | qed. |
---|
37 | |
---|
38 | definition rtl_ertl_fresh_regs_strong: |
---|
39 | ∀i_pars,f_pars,globals. joint_internal_function … globals (rtl_ertl_params i_pars f_pars) → |
---|
40 | ∀n: nat. Σregs: (joint_internal_function … globals (rtl_ertl_params i_pars f_pars)) × (list register). |\snd regs| = n ≝ |
---|
41 | λi_pars,f_pars,globals,def,n.rtl_ertl_fresh_regs i_pars f_pars globals n it def. // |
---|
42 | qed. |
---|
43 | |
---|
44 | definition fresh_label: |
---|
45 | ∀g_pars,globals.freshT globals g_pars label unit ≝ |
---|
46 | λg_pars,globals,it,def. |
---|
47 | let 〈r,luniverse〉 ≝ fresh … (joint_if_luniverse … def) in |
---|
48 | 〈set_luniverse … def luniverse, r〉. |
---|
49 | |
---|
50 | (* insert into a graph a block of instructions *) |
---|
51 | let rec adds_graph |
---|
52 | (g_pars: graph_params) |
---|
53 | (globals: list ident) |
---|
54 | (insts: list (joint_instruction g_pars globals)) |
---|
55 | (src : label) |
---|
56 | (dest : label) |
---|
57 | (def: joint_internal_function … g_pars) on insts ≝ |
---|
58 | match insts with |
---|
59 | [ nil ⇒ add_graph … src (GOTO … dest) def |
---|
60 | | cons instr others ⇒ |
---|
61 | match others with |
---|
62 | [ nil ⇒ (* only one instruction *) |
---|
63 | add_graph … src (sequential … instr dest) def |
---|
64 | | _ ⇒ (* need to generate label *) |
---|
65 | let 〈def, tmp_lbl〉 ≝ fresh_label … it def in |
---|
66 | adds_graph g_pars globals others tmp_lbl dest |
---|
67 | (add_graph … src (sequential … instr tmp_lbl) def) |
---|
68 | ] |
---|
69 | ]. |
---|
70 | |
---|
71 | definition b_adds_graph : |
---|
72 | ∀g_pars: graph_params. |
---|
73 | ∀globals: list ident. |
---|
74 | (* type of allocatable registers and of their types (unit if not in RTLabs) *) |
---|
75 | ∀R,T : Type[0]. |
---|
76 | (* fresh register creation *) |
---|
77 | freshT globals g_pars R T → |
---|
78 | ∀insts: bind_list R T (joint_instruction g_pars globals). |
---|
79 | ∀src : label. |
---|
80 | ∀dest : label. |
---|
81 | joint_internal_function globals g_pars → |
---|
82 | joint_internal_function globals g_pars ≝ |
---|
83 | λg_pars,globals,T,R,fresh_r,insts,src,dest,def. |
---|
84 | let 〈def', stmts〉 ≝ bcompile … fresh_r insts def in |
---|
85 | adds_graph … stmts src dest def'. |
---|
86 | |
---|
87 | (* translation with inline fresh register allocation *) |
---|
88 | definition b_graph_translate : |
---|
89 | ∀src_g_pars,dst_g_pars : graph_params. |
---|
90 | ∀globals: list ident. |
---|
91 | (* type of allocatable registers (unit if not in RTLabs) *) |
---|
92 | ∀T : Type[0]. |
---|
93 | (* fresh register creation *) |
---|
94 | freshT globals dst_g_pars (localsT dst_g_pars) T → |
---|
95 | (* function dictating the translation *) |
---|
96 | (label → joint_instruction src_g_pars globals → |
---|
97 | bind_list (localsT dst_g_pars) T (joint_instruction dst_g_pars globals) |
---|
98 | (* this can be added to allow redirections: × label *)) → |
---|
99 | (label → ext_fin_instruction src_g_pars → |
---|
100 | (bind_list (localsT dst_g_pars) T (joint_instruction dst_g_pars globals)) |
---|
101 | × |
---|
102 | (joint_statement dst_g_pars globals)) → |
---|
103 | (* initialized function definition with empty graph *) |
---|
104 | joint_internal_function globals dst_g_pars → |
---|
105 | (* source function *) |
---|
106 | joint_internal_function globals src_g_pars → |
---|
107 | (* destination function *) |
---|
108 | joint_internal_function globals dst_g_pars ≝ |
---|
109 | λsrc_g_pars,dst_g_pars,globals,registerT,fresh_reg,trans,trans',empty,def. |
---|
110 | let f : label → joint_statement (src_g_pars : params) globals → |
---|
111 | joint_internal_function globals dst_g_pars → joint_internal_function globals dst_g_pars ≝ |
---|
112 | λlbl,stmt,def. |
---|
113 | match stmt with |
---|
114 | [ sequential inst next ⇒ b_adds_graph … fresh_reg (trans lbl inst) lbl next def |
---|
115 | | GOTO next ⇒ add_graph … lbl (GOTO … next) def |
---|
116 | | RETURN ⇒ add_graph … lbl (RETURN …) def |
---|
117 | | extension_fin c ⇒ let 〈l, fin〉 ≝ trans' lbl c in |
---|
118 | let 〈def, tmp_lbl〉 ≝ fresh_label … it def in |
---|
119 | b_adds_graph … fresh_reg l lbl tmp_lbl (add_graph … tmp_lbl fin def) |
---|
120 | ] in |
---|
121 | foldi … f (joint_if_code … def) empty. |
---|
122 | |
---|
123 | definition b_graph_translate_no_fin : |
---|
124 | ∀src_g_pars : graph_params. |
---|
125 | ext_fin_instruction src_g_pars = void → |
---|
126 | ∀dst_g_pars : graph_params. |
---|
127 | ∀globals: list ident. |
---|
128 | (* type of allocatable registers (unit if not in RTLabs) *) |
---|
129 | ∀T : Type[0]. |
---|
130 | (* fresh register creation *) |
---|
131 | freshT globals dst_g_pars (localsT dst_g_pars) T → |
---|
132 | (* function dictating the translation *) |
---|
133 | (label → joint_instruction src_g_pars globals → |
---|
134 | bind_list (localsT dst_g_pars) T (joint_instruction dst_g_pars globals) |
---|
135 | (* this can be added to allow redirections: × label *)) → |
---|
136 | (* initialized function definition with empty graph *) |
---|
137 | joint_internal_function globals dst_g_pars → |
---|
138 | (* source function *) |
---|
139 | joint_internal_function globals src_g_pars → |
---|
140 | (* destination function *) |
---|
141 | joint_internal_function globals dst_g_pars ≝ |
---|
142 | λsrc_g_pars,src_g_pars_prf,dst_g_pars,globals,registerT,fresh_reg,trans. |
---|
143 | b_graph_translate src_g_pars dst_g_pars globals registerT fresh_reg |
---|
144 | trans (λ_.λc.⊥). >src_g_pars_prf in c; #H elim H qed. |
---|
145 | |
---|
146 | (* translation without register allocation *) |
---|
147 | definition graph_translate : |
---|
148 | ∀src_g_pars,dst_g_pars : graph_params. |
---|
149 | ∀globals: list ident. |
---|
150 | (* function dictating the translation *) |
---|
151 | (label → joint_instruction src_g_pars globals → |
---|
152 | list (joint_instruction dst_g_pars globals)) → |
---|
153 | (label → ext_fin_instruction src_g_pars → |
---|
154 | (list (joint_instruction dst_g_pars globals)) |
---|
155 | × |
---|
156 | (joint_statement dst_g_pars globals)) → |
---|
157 | (* initialized function definition with empty graph *) |
---|
158 | joint_internal_function … dst_g_pars → |
---|
159 | (* source function *) |
---|
160 | joint_internal_function … src_g_pars → |
---|
161 | (* destination function *) |
---|
162 | joint_internal_function … dst_g_pars ≝ |
---|
163 | λsrc_g_pars,dst_g_pars,globals,trans,trans',empty,def. |
---|
164 | let f : label → joint_statement (src_g_pars : params) globals → |
---|
165 | joint_internal_function … dst_g_pars → joint_internal_function … dst_g_pars ≝ |
---|
166 | λlbl,stmt,def. |
---|
167 | match stmt with |
---|
168 | [ sequential inst next ⇒ |
---|
169 | adds_graph dst_g_pars globals (trans lbl inst) lbl next def |
---|
170 | | GOTO next ⇒ add_graph … lbl (GOTO … next) def |
---|
171 | | RETURN ⇒ add_graph … lbl (RETURN …) def |
---|
172 | | extension_fin c ⇒ let 〈l, fin〉 ≝ trans' lbl c in |
---|
173 | let 〈def, tmp_lbl〉 ≝ fresh_label … it def in |
---|
174 | adds_graph … l lbl tmp_lbl (add_graph … tmp_lbl fin def) |
---|
175 | ] in |
---|
176 | foldi ??? f (joint_if_code ?? def) empty. |
---|
177 | |
---|
178 | definition graph_translate_no_fin : |
---|
179 | ∀src_g_pars : graph_params. |
---|
180 | ext_fin_instruction src_g_pars = void → |
---|
181 | ∀dst_g_pars : graph_params. |
---|
182 | ∀globals: list ident. |
---|
183 | (* type of allocatable registers (unit if not in RTLabs) *) |
---|
184 | (* function dictating the translation *) |
---|
185 | (label → joint_instruction src_g_pars globals → |
---|
186 | list (joint_instruction dst_g_pars globals) |
---|
187 | (* this can be added to allow redirections: × label *)) → |
---|
188 | (* initialized function definition with empty graph *) |
---|
189 | joint_internal_function globals dst_g_pars → |
---|
190 | (* source function *) |
---|
191 | joint_internal_function globals src_g_pars → |
---|
192 | (* destination function *) |
---|
193 | joint_internal_function globals dst_g_pars ≝ |
---|
194 | λsrc_g_pars,src_g_pars_prf,dst_g_pars,globals,trans. |
---|
195 | graph_translate src_g_pars dst_g_pars globals |
---|
196 | trans (λ_.λc.⊥). >src_g_pars_prf in c; #H elim H qed. |
---|
197 | |
---|
198 | |
---|
199 | |
---|
200 | (* |
---|
201 | let rec add_translates |
---|
202 | (pars1: params1) (globals: list ident) |
---|
203 | (translate_list: list ?) (start_lbl: label) (dest_lbl: label) |
---|
204 | (def: joint_internal_function … (graph_params pars1 globals)) |
---|
205 | on translate_list ≝ |
---|
206 | match translate_list with |
---|
207 | [ nil ⇒ add_graph … start_lbl (GOTO … dest_lbl) def |
---|
208 | | cons trans translate_list ⇒ |
---|
209 | match translate_list with |
---|
210 | [ nil ⇒ trans start_lbl dest_lbl def |
---|
211 | | _ ⇒ |
---|
212 | let 〈tmp_lbl, def〉 ≝ fresh_label … def in |
---|
213 | let def ≝ trans start_lbl tmp_lbl def in |
---|
214 | add_translates pars1 globals translate_list tmp_lbl dest_lbl def]]. |
---|
215 | |
---|
216 | definition adds_graph ≝ |
---|
217 | λpars1:params1.λglobals. λstmt_list: list (label → joint_statement (graph_params_ pars1) globals). |
---|
218 | add_translates … (map ?? (λf,start_lbl,dest_lbl. add_graph pars1 ? start_lbl (f dest_lbl)) stmt_list). |
---|
219 | *) |
---|