source: src/joint/TranslateUtils_paolo.ma @ 1651

Last change on this file since 1651 was 1643, checked in by tranquil, 8 years ago
  • some changes in everything
  • separated extensions in sequential and final, to accomodate tailcalls
  • finished RTL's semantics
File size: 9.1 KB
Line 
1include "joint/Joint_paolo.ma".
2include "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 ) *)
7definition freshT ≝ λg.λpars : params.λX,T : Type[0].
8   T → state_monad (joint_internal_function … g pars) X.
9
10definition 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
17let 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
27lemma 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 // ]
36qed.
37
38definition 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. //
42qed.
43
44definition 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 *)
51let 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
71definition 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 *)
88definition 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
123definition 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 *)
147definition 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 
178definition 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(*
201let 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
216definition 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  *)
Note: See TracBrowser for help on using the repository browser.