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 | (* initialized function definition with empty graph *) |
---|
100 | joint_internal_function globals dst_g_pars → |
---|
101 | (* source function *) |
---|
102 | joint_internal_function globals src_g_pars → |
---|
103 | (* destination function *) |
---|
104 | joint_internal_function globals dst_g_pars ≝ |
---|
105 | λsrc_g_pars,dst_g_pars,globals,registerT,fresh_reg,trans,empty,def. |
---|
106 | let f : label → joint_statement src_g_pars globals → |
---|
107 | joint_internal_function globals dst_g_pars → joint_internal_function globals dst_g_pars ≝ |
---|
108 | λlbl,stmt,def. |
---|
109 | match stmt with |
---|
110 | [ sequential inst next ⇒ b_adds_graph … fresh_reg (trans lbl inst) lbl next def |
---|
111 | | GOTO next ⇒ add_graph … lbl (GOTO … next) def |
---|
112 | | RETURN ⇒ add_graph … lbl (RETURN …) def |
---|
113 | ] in |
---|
114 | foldi … f (joint_if_code … def) empty. |
---|
115 | |
---|
116 | (* translation without register allocation *) |
---|
117 | definition graph_translate : |
---|
118 | ∀src_g_pars,dst_g_pars : graph_params. |
---|
119 | ∀globals: list ident. |
---|
120 | (* function dictating the translation *) |
---|
121 | (label → joint_instruction src_g_pars globals → |
---|
122 | list (joint_instruction dst_g_pars globals)) → |
---|
123 | (* initialized function definition with empty graph *) |
---|
124 | joint_internal_function … dst_g_pars → |
---|
125 | (* source function *) |
---|
126 | joint_internal_function … src_g_pars → |
---|
127 | (* destination function *) |
---|
128 | joint_internal_function … dst_g_pars ≝ |
---|
129 | λsrc_g_pars,dst_g_pars,globals,trans,empty,def. |
---|
130 | let f : label → joint_statement src_g_pars globals → |
---|
131 | joint_internal_function … dst_g_pars → joint_internal_function … dst_g_pars ≝ |
---|
132 | λlbl,stmt,def. |
---|
133 | match stmt with |
---|
134 | [ sequential inst next ⇒ |
---|
135 | adds_graph dst_g_pars globals (trans lbl inst) lbl next def |
---|
136 | | GOTO next ⇒ add_graph … lbl (GOTO … next) def |
---|
137 | | RETURN ⇒ add_graph … lbl (RETURN …) def |
---|
138 | ] in |
---|
139 | foldi ??? f (joint_if_code ?? def) empty. |
---|
140 | |
---|
141 | (* |
---|
142 | let rec add_translates |
---|
143 | (pars1: params1) (globals: list ident) |
---|
144 | (translate_list: list ?) (start_lbl: label) (dest_lbl: label) |
---|
145 | (def: joint_internal_function … (graph_params pars1 globals)) |
---|
146 | on translate_list ≝ |
---|
147 | match translate_list with |
---|
148 | [ nil ⇒ add_graph … start_lbl (GOTO … dest_lbl) def |
---|
149 | | cons trans translate_list ⇒ |
---|
150 | match translate_list with |
---|
151 | [ nil ⇒ trans start_lbl dest_lbl def |
---|
152 | | _ ⇒ |
---|
153 | let 〈tmp_lbl, def〉 ≝ fresh_label … def in |
---|
154 | let def ≝ trans start_lbl tmp_lbl def in |
---|
155 | add_translates pars1 globals translate_list tmp_lbl dest_lbl def]]. |
---|
156 | |
---|
157 | definition adds_graph ≝ |
---|
158 | λpars1:params1.λglobals. λstmt_list: list (label → joint_statement (graph_params_ pars1) globals). |
---|
159 | add_translates … (map ?? (λf,start_lbl,dest_lbl. add_graph pars1 ? start_lbl (f dest_lbl)) stmt_list). |
---|
160 | *) |
---|