source: src/joint/TranslateUtils_paolo.ma @ 2182

Last change on this file since 2182 was 2182, checked in by tranquil, 9 years ago

updated linearisation pass

File size: 8.3 KB
Line 
1include "joint/Joint_paolo.ma".
2include "joint/blocks.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.state_monad (joint_internal_function … g pars).
8
9definition rtl_ertl_fresh_reg:
10 ∀inst_pars,funct_pars,globals.
11  freshT globals (rtl_ertl_params inst_pars funct_pars) register ≝
12  λinst_pars,var_pars,globals,def.
13    let 〈r, runiverse〉 ≝ fresh … (joint_if_runiverse … def) in
14    〈set_locals ?? (set_runiverse ?? def runiverse)(r::joint_if_locals ?? def), r〉.
15
16include alias "basics/lists/list.ma".
17let rec rtl_ertl_fresh_regs inst_pars funct_pars globals (n : ℕ) on n :
18  freshT globals (rtl_ertl_params inst_pars funct_pars)
19    (Σl : list register. |l| = n) ≝
20  let ret_type ≝ (Σl : list register. |l| = n) in
21  match n  return λx.x = n → freshT … ret_type with
22  [ O ⇒ λeq'.return (mk_Sig … [ ] ?)
23  | S n' ⇒ λeq'.
24    ! regs' ← rtl_ertl_fresh_regs inst_pars funct_pars globals n';
25    ! reg ← rtl_ertl_fresh_reg inst_pars funct_pars globals;
26    return (mk_Sig … (reg :: regs') ?)
27  ](refl …). <eq' normalize [//] elim regs' #l #eql >eql //
28  qed.
29
30definition fresh_label:
31 ∀g_pars,globals.freshT globals g_pars label ≝
32  λg_pars,globals,def.
33    let 〈r,luniverse〉 ≝ fresh … (joint_if_luniverse … def) in
34     〈set_luniverse … def luniverse, r〉.
35
36(* insert into a graph a block of instructions *)
37let rec adds_graph_list
38  (g_pars: graph_params)
39  (globals: list ident)
40  (insts: list (joint_seq g_pars globals))
41  (src : label) on insts : state_monad (joint_internal_function … g_pars) label ≝
42  match insts with
43  [ nil ⇒ return src
44  | cons instr others ⇒
45    ! mid ← fresh_label … ;
46    ! def ← state_get … ;
47    !_ state_set … (add_graph … src (sequential … instr mid) def) ;
48    adds_graph_list g_pars globals others mid
49  ].
50
51definition adds_graph :
52  ∀g_pars : graph_params.
53  ∀globals: list ident.
54  ∀b : seq_block g_pars globals (joint_step g_pars globals) +
55       seq_block g_pars globals (joint_fin_step g_pars).
56  label → if is_inl … b then label else unit →
57  joint_internal_function … g_pars → joint_internal_function … g_pars ≝
58  λg_pars,globals,insts,src.
59  match insts return λx.if is_inl … x then ? else ? → ? → ? with
60  [ inl b ⇒ λdst,def.
61    let 〈def, mid〉 ≝ adds_graph_list … (\fst b) src def in
62    add_graph … mid (sequential … (\snd b) dst) def
63  | inr b ⇒ λdst,def.
64    let 〈def, mid〉 ≝ adds_graph_list … (\fst b) src def in
65    add_graph … mid (final … (\snd b)) def
66  ].
67
68(* preserves first statement if a cost label (should be an invariant) *)
69definition insert_prologue ≝
70  λg_pars:graph_params.λglobals.λinsts : list (joint_seq g_pars globals).
71  λdef : joint_internal_function globals g_pars.
72  let entry ≝ joint_if_entry … def in
73  match stmt_at … entry
74  return λx.match x with [None ⇒ false | Some _ ⇒ true] → ?
75  with
76  [ Some s ⇒ λ_.
77    match s with
78    [ sequential s' next ⇒
79      match s' with
80      [ step_seq s'' ⇒
81        match s'' with
82        [ COST_LABEL _ ⇒
83          adds_graph ?? (inl … (s'' :: insts)) entry next def
84        | _ ⇒
85          let 〈def', tmp〉 ≝ adds_graph_list ?? insts entry def in
86          add_graph … tmp s def'
87        ]
88      | _ ⇒
89        let 〈def', tmp〉 ≝ adds_graph_list ?? insts entry def in
90        add_graph … tmp s def'
91      ]
92    | _ ⇒
93      let 〈def', tmp〉 ≝ adds_graph_list ?? insts entry def in
94      add_graph … tmp s def'
95    ]
96  | None ⇒ Ⓧ
97  ] (pi2 … entry).
98
99definition insert_epilogue ≝
100  λg_pars:graph_params.λglobals.λinsts : list (joint_seq g_pars globals).
101  λdef : joint_internal_function globals g_pars.
102  let exit ≝ joint_if_exit … def in
103  match stmt_at … exit
104  return λx.match x with [None ⇒ false | Some _ ⇒ true] → ?
105  with
106  [ Some s ⇒ λ_.
107    let 〈def', tmp〉 as prf ≝ adds_graph_list ?? insts exit def in
108    let def'' ≝ add_graph … tmp s def' in
109    set_joint_code … def'' (joint_if_code … def'') (joint_if_entry … def'') tmp
110  | None ⇒ Ⓧ
111  ] (pi2 … exit).
112whd in match def''; >graph_code_has_point //
113qed.
114
115definition b_adds_graph :
116  ∀g_pars: graph_params.
117  ∀globals: list ident.
118  (* fresh register creation *)
119  freshT globals g_pars (localsT … g_pars) →
120  ∀b : bind_seq_block g_pars globals (joint_step g_pars globals) +
121       bind_seq_block g_pars globals (joint_fin_step g_pars).
122  label → if is_inl … b then label else unit →
123  joint_internal_function globals g_pars →
124  joint_internal_function globals g_pars ≝
125  λg_pars,globals,fresh_r,insts,src.
126  match insts return λx.if is_inl … x then ? else ? → ? → ? with
127  [ inl b ⇒ λdst,def.
128    let 〈def, stmts〉 ≝ bcompile ??? fresh_r b def in
129    adds_graph … (inl … stmts) src dst def
130  | inr b ⇒ λdst,def.
131    let 〈def, stmts〉 ≝ bcompile ??? fresh_r b def in
132    adds_graph … (inr … stmts) src dst def
133  ].
134
135(* translation with inline fresh register allocation *)
136definition b_graph_translate :
137  ∀src_g_pars,dst_g_pars : graph_params.
138  ∀globals: list ident.
139  (* fresh register creation *)
140  freshT globals dst_g_pars (localsT dst_g_pars) →
141  (* initialized function definition with empty graph *)
142  joint_internal_function globals dst_g_pars →
143  (* functions dictating the translation *)
144  (label → joint_step src_g_pars globals →
145    bind_seq_block dst_g_pars globals (joint_step dst_g_pars globals)) →
146  (label → joint_fin_step src_g_pars →
147    bind_seq_block dst_g_pars globals (joint_fin_step dst_g_pars)) →
148  (* source function *)
149  joint_internal_function globals src_g_pars →
150  (* destination function *)
151  joint_internal_function globals dst_g_pars ≝
152  λsrc_g_pars,dst_g_pars,globals,fresh_reg,empty,trans_step,trans_fin_step,def.
153  let f : label → joint_statement (src_g_pars : params) globals →
154    joint_internal_function globals dst_g_pars → joint_internal_function globals dst_g_pars ≝
155    λlbl,stmt,def.
156    match stmt with
157    [ sequential inst next ⇒
158      b_adds_graph … fresh_reg (inl … (trans_step lbl inst)) lbl next def
159    | final inst ⇒
160      b_adds_graph … fresh_reg (inr … (trans_fin_step lbl inst)) lbl it def
161    ] in
162  foldi … f (joint_if_code … def) empty.
163
164(* translation without register allocation *)
165definition graph_translate :
166  ∀src_g_pars,dst_g_pars : graph_params.
167  ∀globals: list ident.
168  (* initialized function definition with empty graph *)
169  joint_internal_function … dst_g_pars →
170  (* functions dictating the translation *)
171  (label → joint_step src_g_pars globals →
172    seq_block dst_g_pars globals (joint_step dst_g_pars globals)) →
173  (label → joint_fin_step src_g_pars →
174    seq_block dst_g_pars globals (joint_fin_step dst_g_pars)) →
175  (* source function *)
176  joint_internal_function … src_g_pars →
177  (* destination function *)
178  joint_internal_function … dst_g_pars ≝
179  λsrc_g_pars,dst_g_pars,globals,empty,trans_step,trans_fin_step,def.
180  let f : label → joint_statement (src_g_pars : params) globals →
181    joint_internal_function globals dst_g_pars → joint_internal_function globals dst_g_pars ≝
182    λlbl,stmt,def.
183    match stmt with
184    [ sequential inst next ⇒
185      adds_graph … (inl … (trans_step lbl inst)) lbl next def
186    | final inst ⇒
187      adds_graph … (inr … (trans_fin_step lbl inst)) lbl it def
188    ] in
189  foldi … f (joint_if_code … def) empty.
190
191(*
192let rec add_translates
193  (pars1: params1) (globals: list ident)
194  (translate_list: list ?) (start_lbl: label) (dest_lbl: label)
195  (def: joint_internal_function … (graph_params pars1 globals))
196    on translate_list ≝
197  match translate_list with
198  [ nil ⇒ add_graph … start_lbl (GOTO … dest_lbl) def
199  | cons trans translate_list ⇒
200    match translate_list with
201    [ nil ⇒ trans start_lbl dest_lbl def
202    | _ ⇒
203      let 〈tmp_lbl, def〉 ≝ fresh_label … def in
204      let def ≝ trans start_lbl tmp_lbl def in
205        add_translates pars1 globals translate_list tmp_lbl dest_lbl def]].
206
207definition adds_graph ≝
208 λpars1:params1.λglobals. λstmt_list: list (label → joint_statement (graph_params_ pars1) globals).
209  add_translates … (map ?? (λf,start_lbl,dest_lbl. add_graph pars1 ? start_lbl (f dest_lbl)) stmt_list).
210  *)
Note: See TracBrowser for help on using the repository browser.