source: src/joint/TranslateUtils.ma @ 2536

Last change on this file since 2536 was 2532, checked in by tranquil, 8 years ago

added FCOND in LIN, and rewritten linearise so that it never adds a GOTO after a COND (writes in FCOND instead)
LIN to ASM is broken atm

File size: 12.1 KB
Line 
1include "joint/Joint.ma".
2include "joint/blocks.ma".
3include "utilities/hide.ma".
4include "utilities/deqsets.ma".
5
6(* general type of functions generating fresh things *)
7definition freshT ≝ λpars : params.λg.state_monad (joint_internal_function pars g).
8
9include alias "basics/lists/list.ma".
10let rec repeat_fresh pars globals A (fresh : freshT pars globals A) (n : ℕ)
11  on n :
12  freshT pars globals (Σl : list A. |l| = n) ≝
13  match n  return λx.freshT … (Σl.|l| = x) with
14  [ O ⇒ return «[ ], ?»
15  | S n' ⇒
16    ! regs' ← repeat_fresh … fresh n';
17    ! reg ← fresh ;
18    return «reg::regs',?»
19  ]. [% | @hide_prf cases regs' #l #EQ normalize >EQ % ] qed.
20
21definition fresh_label:
22 ∀g_pars,globals.freshT globals g_pars label ≝
23  λg_pars,globals,def.
24    let 〈r,luniverse〉 ≝ fresh … (joint_if_luniverse … def) in
25     〈set_luniverse … def luniverse, r〉.
26
27(* insert into a graph a block of instructions *)
28let rec adds_graph_list
29  (g_pars: graph_params)
30  (globals: list ident)
31  (insts: list (joint_seq g_pars globals))
32  (src : label) on insts : state_monad (joint_internal_function g_pars globals) label ≝
33  match insts with
34  [ nil ⇒ return src
35  | cons instr others ⇒
36    ! mid ← fresh_label … ;
37    ! def ← state_get … ;
38    !_ state_set … (add_graph … src (sequential … instr mid) def) ;
39    adds_graph_list g_pars globals others mid
40  ].
41
42definition is_inr : ∀A,B.A + B → bool ≝ λA,B,x.match x with
43  [ inl _ ⇒ true
44  | inr _ ⇒ false
45  ].
46definition is_inl : ∀A,B.A + B → bool ≝ λA,B,x.match x with
47  [ inl _ ⇒ true
48  | inr _ ⇒ false
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 globals → joint_internal_function g_pars globals ≝
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(* ignoring register allocation for now *)
69
70definition luniverse_ok : ∀p : graph_params.∀g.joint_internal_function p g → Prop ≝
71λp,g,def.fresh_map_for_univ … (joint_if_code … def) (joint_if_luniverse … def).
72
73lemma present_to_memb : ∀tag,A,l,m.present tag A m l → bool_to_Prop (l∈m).
74#tag #A * #l * #m whd in ⊢ (%→?%);
75elim (lookup tag ???)
76[ * #ABS elim (ABS ?) %
77| #a #_ %
78] qed.
79
80lemma memb_to_present : ∀tag,A,l,m.l∈m → present tag A m l.
81#tag #A * #l * #m whd in ⊢ (?%→%);
82elim (lookup tag ???)
83[ * | #a * % #ABS destruct(ABS) ] qed.
84
85(*
86lemma All_fresh_not_memb : ∀tag,u,l,id,u'.
87  All (identifier tag) (λid'.¬fresh_for_univ tag id' u) l →
88  〈id, u'〉 = fresh tag u →
89  ¬id ∈ l.
90#tag #u #l elim l [2: #hd #tl #IH] #id #u' *
91[ #hd_fresh #tl_fresh #EQfresh
92  whd in ⊢ (?(?%));
93  change with (eq_identifier ???) in match (?==?);
94  >eq_identifier_sym
95  >(eq_identifier_false … (fresh_distinct … hd_fresh EQfresh))
96  normalize nodelta @(IH … tl_fresh EQfresh)
97| #_ %
98]
99qed.
100*)
101
102lemma fresh_was_fresh : ∀tag,id,id',u,u'.
103〈id,u'〉 = fresh tag u →
104fresh_for_univ tag id' u' →
105id' ≠ id →
106fresh_for_univ tag id' u.
107#tag * #id * #id' * #u * #u'
108normalize #EQfresh destruct
109#H #NEQ
110elim (le_to_or_lt_eq … H)
111[ (* not recompiling... /2 by monotonic_pred/ *) /2/ ]
112#H >(succ_injective … H) in NEQ;
113* #G elim (G (refl …))
114qed.
115
116
117(* use Russell? *)
118axiom adds_graph_list_ok :
119  ∀g_pars,globals,b,src,def.
120  fresh_for_univ … src (joint_if_luniverse … def) →
121  luniverse_ok ?? def →
122  let 〈def', dst〉 ≝ adds_graph_list g_pars globals b src def in
123  luniverse_ok ?? def' ∧
124  ∃l.bool_to_Prop (uniqueb … l) ∧
125     All … (λlbl.¬fresh_for_univ … lbl (joint_if_luniverse … def) ∧
126                  fresh_for_univ … lbl (joint_if_luniverse … def')) l ∧
127     src ~❨b,l❩~> dst in joint_if_code … def'.
128(* #p #g #l elim l
129[ #src #def #_ #Hdef whd
130  %{Hdef} %{[ ]} %%%
131| #hd #tl #IH #src #def #src_fresh #Hdef
132  whd in match (adds_graph_list ?????);
133  whd in match (fresh_label ???);
134  @(pair_elim … (fresh ??)) normalize nodelta
135  #mid #luniverse' #EQfresh
136  whd in ⊢ (match % with [ _ ⇒ ?]);
137  letin def' ≝ (add_graph p g src (sequential … hd mid) (set_luniverse … def luniverse'))
138  cut (joint_if_code p g (set_luniverse p g def luniverse') = joint_if_code … def)
139  [ cases def // ] #EQ_aux
140  lapply (IH mid def' ??)
141  [ #l whd in match def'; #Hpres
142    lapply (present_to_memb … Hpres) -Hpres
143    >mem_set_add @eq_identifier_elim
144    [ #EQ destruct(EQ) *
145    | #NEQ change with (? ∈ joint_if_code p ??) in ⊢ (?%→?); >EQ_aux
146      #l_in
147    ]
148    @(fresh_remains_fresh … (sym_eq … EQfresh))
149    [2: @Hdef @memb_to_present ] assumption
150  | whd in match def';
151    cases def #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9
152    whd in match (set_luniverse ????);
153    @(fresh_is_fresh … (sym_eq … EQfresh))
154  ]
155  elim (adds_graph_list ?????) #def'' #mid' normalize nodelta
156  * #Hdef'' * #l ** #Hl1 #Hl2 #Hl3 %{Hdef''} %{(mid::l)}
157  % [ % ]
158  [ whd in ⊢ (?%);
159    elim (true_or_false_Prop (mid∈l)) #H >H normalize nodelta
160    [ elim (All_memb … Hl2 H)
161      cases def #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 normalize in ⊢ (%→?);
162      #H #_ @(absurd ?? H)
163      @(fresh_remains_fresh … (eqEQfresh)
164      normalize #H10 #H11
165     
166    >(All_fresh_not_memb … (sym_eq … EQfresh))
167    [ assumption ]
168    @(All_mp … Hl2) #lbl *
169    cases def in EQfresh; #H11 #H12 #H13 #H14 #H15 #H16 #H17 #H18 #H19
170    normalize #EQfresh #H #lbl_not_mid
171    lapply(fresh_remains_fresh … H (sym_eq … EQfresh))
172   
173    elim (true_or_false_Prop (mid∈l)) #mid_l >mid_l
174    [ normalize
175*)
176
177(* preserves first statement if a cost label (should be an invariant) *)
178definition insert_prologue ≝
179  λg_pars:graph_params.λglobals.λinsts : list (joint_seq g_pars globals).
180  λdef : joint_internal_function g_pars globals.
181  let entry ≝ joint_if_entry … def in
182  match stmt_at … entry
183  return λx.match x with [None ⇒ false | Some _ ⇒ true] → ?
184  with
185  [ Some s ⇒ λ_.
186    match s with
187    [ sequential s' next ⇒
188      match s' with
189      [ step_seq s'' ⇒
190        match s'' with
191        [ COST_LABEL _ ⇒
192          adds_graph ?? (inl … (s'' :: insts)) entry next def
193        | _ ⇒
194          let 〈def', tmp〉 ≝ adds_graph_list ?? insts entry def in
195          add_graph … tmp s def'
196        ]
197      | _ ⇒
198        let 〈def', tmp〉 ≝ adds_graph_list ?? insts entry def in
199        add_graph … tmp s def'
200      ]
201    | _ ⇒
202      let 〈def', tmp〉 ≝ adds_graph_list ?? insts entry def in
203      add_graph … tmp s def'
204    ]
205  | None ⇒ Ⓧ
206  ] (pi2 … entry).
207
208definition insert_epilogue ≝
209  λg_pars:graph_params.λglobals.λinsts : list (joint_seq g_pars globals).
210  λdef : joint_internal_function g_pars globals.
211  let exit ≝ joint_if_exit … def in
212  match stmt_at … exit
213  return λx.match x with [None ⇒ false | Some _ ⇒ true] → ?
214  with
215  [ Some s ⇒ λ_.
216    let 〈def', tmp〉 as prf ≝ adds_graph_list ?? insts exit def in
217    let def'' ≝ add_graph … tmp s def' in
218    set_joint_code … def'' (joint_if_code … def'') (joint_if_entry … def'') tmp
219  | None ⇒ Ⓧ
220  ] (pi2 … exit).
221whd in match def''; >graph_code_has_point //
222qed.
223
224definition b_adds_graph :
225  ∀g_pars: graph_params.
226  ∀globals: list ident.
227  (* fresh register creation *)
228  freshT g_pars globals (localsT … g_pars) →
229  ∀b : bind_seq_block g_pars globals (joint_step g_pars globals) +
230       bind_seq_block g_pars globals (joint_fin_step g_pars).
231  label → if is_inl … b then label else unit →
232  joint_internal_function g_pars globals→
233  joint_internal_function g_pars globals ≝
234  λg_pars,globals,fresh_r,insts,src.
235  match insts return λx.if is_inl … x then ? else ? → ? → ? with
236  [ inl b ⇒ λdst,def.
237    let 〈def, stmts〉 ≝ bcompile ??? fresh_r b def in
238    adds_graph … (inl … stmts) src dst def
239  | inr b ⇒ λdst,def.
240    let 〈def, stmts〉 ≝ bcompile ??? fresh_r b def in
241    adds_graph … (inr … stmts) src dst def
242  ].
243
244 
245
246(* translation with inline fresh register allocation *)
247definition b_graph_translate :
248  ∀src_g_pars,dst_g_pars : graph_params.
249  ∀globals: list ident.
250  (* fresh register creation *)
251  freshT dst_g_pars globals (localsT dst_g_pars) →
252  (* initialized function definition with empty graph *)
253  joint_internal_function dst_g_pars globals →
254  (* functions dictating the translation *)
255  (label → joint_step src_g_pars globals →
256    bind_seq_block dst_g_pars globals (joint_step dst_g_pars globals)) →
257  (label → joint_fin_step src_g_pars →
258    bind_seq_block dst_g_pars globals (joint_fin_step dst_g_pars)) →
259  (* source function *)
260  joint_internal_function src_g_pars globals →
261  (* destination function *)
262  joint_internal_function dst_g_pars globals ≝
263  λsrc_g_pars,dst_g_pars,globals,fresh_reg,empty,trans_step,trans_fin_step,def.
264  let f : label → joint_statement (src_g_pars : params) globals →
265    joint_internal_function dst_g_pars globals → joint_internal_function dst_g_pars globals ≝
266    λlbl,stmt,def.
267    match stmt with
268    [ sequential inst next ⇒
269      b_adds_graph … fresh_reg (inl … (trans_step lbl inst)) lbl next def
270    | final inst ⇒
271      b_adds_graph … fresh_reg (inr … (trans_fin_step lbl inst)) lbl it def
272    | FCOND abs _ _ _ ⇒ Ⓧabs
273    ] in
274  foldi … f (joint_if_code … def) empty.
275
276(* translation without register allocation *)
277definition graph_translate :
278  ∀src_g_pars,dst_g_pars : graph_params.
279  ∀globals: list ident.
280  (* initialized function definition with empty graph *)
281  joint_internal_function dst_g_pars globals →
282  (* functions dictating the translation *)
283  (label → joint_step src_g_pars globals →
284    seq_block dst_g_pars globals (joint_step dst_g_pars globals)) →
285  (label → joint_fin_step src_g_pars →
286    seq_block dst_g_pars globals (joint_fin_step dst_g_pars)) →
287  (* source function *)
288  joint_internal_function src_g_pars globals →
289  (* destination function *)
290  joint_internal_function dst_g_pars globals ≝
291  λsrc_g_pars,dst_g_pars,globals,empty,trans_step,trans_fin_step,def.
292  let f : label → joint_statement (src_g_pars : params) globals →
293    joint_internal_function dst_g_pars globals → joint_internal_function dst_g_pars globals ≝
294    λlbl,stmt,def.
295    match stmt with
296    [ sequential inst next ⇒
297      adds_graph … (inl … (trans_step lbl inst)) lbl next def
298    | final inst ⇒
299      adds_graph … (inr … (trans_fin_step lbl inst)) lbl it def
300    | FCOND abs _ _ _ ⇒ Ⓧabs
301    ] in
302  foldi … f (joint_if_code … def) empty.
303
304definition init_graph_if ≝
305  λg_pars : graph_params.λglobals.
306  λluniverse,runiverse,ret,params,locals,stack_size,entry,exit.
307  let graph ≝ add ? ? (empty_map ? (joint_statement ??)) entry (GOTO … exit) in
308  let graph ≝ add ? ? graph exit (RETURN …) in
309  mk_joint_internal_function g_pars globals
310    luniverse runiverse ret params locals stack_size
311    graph entry exit.
312>graph_code_has_point @map_mem_prop
313[@graph_add_lookup] @graph_add
314qed.
315
316
317(*
318let rec add_translates
319  (pars1: params1) (globals: list ident)
320  (translate_list: list ?) (start_lbl: label) (dest_lbl: label)
321  (def: joint_internal_function … (graph_params pars1 globals))
322    on translate_list ≝
323  match translate_list with
324  [ nil ⇒ add_graph … start_lbl (GOTO … dest_lbl) def
325  | cons trans translate_list ⇒
326    match translate_list with
327    [ nil ⇒ trans start_lbl dest_lbl def
328    | _ ⇒
329      let 〈tmp_lbl, def〉 ≝ fresh_label … def in
330      let def ≝ trans start_lbl tmp_lbl def in
331        add_translates pars1 globals translate_list tmp_lbl dest_lbl def]].
332
333definition adds_graph ≝
334 λpars1:params1.λglobals. λstmt_list: list (label → joint_statement (graph_params_ pars1) globals).
335  add_translates … (map ?? (λf,start_lbl,dest_lbl. add_graph pars1 ? start_lbl (f dest_lbl)) stmt_list).
336  *)
Note: See TracBrowser for help on using the repository browser.