source: src/joint/TranslateUtils_paolo.ma @ 1635

Last change on this file since 1635 was 1635, checked in by tranquil, 8 years ago
  • lists with binders and monads
  • Joint.ma and other temprarily forked, awaiting feedback from Claudio
  • translation of RTLabs → RTL refactored with new tools
File size: 6.5 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  (* 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 *)
117definition 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(*
142let 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
157definition 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  *)
Note: See TracBrowser for help on using the repository browser.