source: src/joint/TranslateUtils.ma @ 2681

Last change on this file since 2681 was 2681, checked in by tranquil, 8 years ago
  • improvements to the graph translation function
  • fixed passes up to LTL
File size: 23.0 KB
Line 
1include "joint/Joint.ma".
2include "joint/blocks.ma".
3include "utilities/hide.ma".
4include "utilities/deqsets.ma".
5
6(*include alias "basics/lists/list.ma".
7let rec repeat_fresh pars globals A (fresh : freshT pars globals A) (n : ℕ)
8  on n :
9  freshT pars globals (Σl : list A. |l| = n) ≝
10  match n  return λx.freshT … (Σl.|l| = x) with
11  [ O ⇒ return «[ ], ?»
12  | S n' ⇒
13    ! regs' ← repeat_fresh … fresh n';
14    ! reg ← fresh ;
15    return «reg::regs',?»
16  ]. [% | @hide_prf cases regs' #l #EQ normalize >EQ % ] qed.*)
17
18definition fresh_label:
19 ∀g_pars,globals.state_monad (joint_internal_function g_pars globals) label ≝
20  λg_pars,globals,def.
21    let 〈r,luniverse〉 ≝ fresh … (joint_if_luniverse … def) in
22     〈set_luniverse … def luniverse, r〉.
23
24definition fresh_register:
25 ∀g_pars,globals.state_monad (joint_internal_function g_pars globals) register ≝
26  λg_pars,globals,def.
27    let 〈r,runiverse〉 ≝ fresh … (joint_if_runiverse … def) in
28     〈set_runiverse … def runiverse, r〉.
29
30definition state_update : ∀S.(S → S) → state_monad S unit ≝
31λS,f,s.〈f s, it〉.
32
33(* insert into a graph a list of instructions *)
34let rec adds_graph_pre
35  X
36  (g_pars: graph_params)
37  (globals: list ident)
38  (* for ERTLptr: the label parameter is filled by the last label *)
39  (pre_process : label → X → joint_seq g_pars globals)
40  (insts: list X)
41  (src : label) on insts :
42  state_monad (joint_internal_function g_pars globals) label ≝
43  match insts with
44  [ nil ⇒ return src
45  | cons i rest ⇒
46    ! mid ← fresh_label … ;
47    ! dst ← adds_graph_pre … pre_process rest mid ;
48    !_ state_update … (add_graph … src (sequential … (pre_process dst i) mid)) ;
49    return dst
50  ].
51
52let rec adds_graph_post
53  (g_pars: graph_params)
54  (globals: list ident)
55  (insts: list (joint_seq g_pars globals))
56  (dst : label) on insts :
57  state_monad (joint_internal_function g_pars globals) label ≝
58  match insts with
59  [ nil ⇒ return dst
60  | cons i rest ⇒
61    ! src ← fresh_label … ;
62    ! mid ← adds_graph_post … rest dst ;
63    !_ state_update … (add_graph … src (sequential … i mid)) ;
64    return src
65  ].
66
67definition adds_graph :
68  ∀g_pars : graph_params.
69  ∀globals: list ident.
70  ∀b : step_block g_pars globals.
71  label → label →
72  joint_internal_function g_pars globals → joint_internal_function g_pars globals ≝
73  λg_pars,globals,insts,src,dst,def.
74  let pref ≝ \fst (\fst insts) in
75  let op ≝ \snd (\fst insts) in
76  let post ≝ \snd insts in
77  let 〈def, mid〉 ≝ adds_graph_pre … (λlbl,inst.inst lbl) pref src def in
78  let 〈def, mid'〉 ≝ adds_graph_post … post dst def in
79  add_graph … mid (sequential … (op mid) mid') def.
80
81definition fin_adds_graph :
82  ∀g_pars : graph_params.
83  ∀globals: list ident.
84  ∀b : fin_block g_pars globals.
85  label →
86  joint_internal_function g_pars globals → joint_internal_function g_pars globals ≝
87  λg_pars,globals,insts,src,def.
88  let pref ≝ \fst insts in
89  let last ≝ \snd insts in
90  let 〈def, mid〉 ≝ adds_graph_pre … (λ_.λi.i) pref src def in
91  add_graph … mid (final … last) def.
92
93(* ignoring register allocation for now *)
94
95(*
96definition luniverse_ok : ∀p : graph_params.∀g.joint_internal_function p g → Prop ≝
97λp,g,def.fresh_map_for_univ … (joint_if_code … def) (joint_if_luniverse … def).
98*)
99(*
100lemma All_fresh_not_memb : ∀tag,u,l,id,u'.
101  All (identifier tag) (λid'.¬fresh_for_univ tag id' u) l →
102  〈id, u'〉 = fresh tag u →
103  ¬id ∈ l.
104#tag #u #l elim l [2: #hd #tl #IH] #id #u' *
105[ #hd_fresh #tl_fresh #EQfresh
106  whd in ⊢ (?(?%));
107  change with (eq_identifier ???) in match (?==?);
108  >eq_identifier_sym
109  >(eq_identifier_false … (fresh_distinct … hd_fresh EQfresh))
110  normalize nodelta @(IH … tl_fresh EQfresh)
111| #_ %
112]
113qed.
114
115
116lemma fresh_was_fresh : ∀tag,id,id',u,u'.
117〈id,u'〉 = fresh tag u →
118fresh_for_univ tag id' u' →
119id' ≠ id →
120fresh_for_univ tag id' u.
121#tag * #id * #id' * #u * #u'
122normalize #EQfresh destruct
123#H #NEQ
124elim (le_to_or_lt_eq … H)
125[ (* not recompiling... /2 by monotonic_pred/ *) /2/ ]
126#H >(succ_injective … H) in NEQ;
127* #G elim (G (refl …))
128qed.
129
130lemma fresh_not_in_univ : ∀tag,id,u,u'.
131〈id, u'〉 = fresh tag u →
132¬fresh_for_univ tag id u.
133#tag * #id * #u * #u' normalize #EQ destruct //
134qed.
135*)
136(*
137lemma adds_graph_list_fresh_preserve :
138  ∀g_pars,globals,b,src,dst,def.
139  let def' ≝ adds_graph_list g_pars globals b src dst def in
140  ∀lbl.fresh_for_univ … lbl (joint_if_luniverse … def) →
141       fresh_for_univ … lbl (joint_if_luniverse … def').
142#g_pars #globals #l elim l -l
143[ #src #dst #def whd #lbl #H @H ]
144#hd1 * [ #_ #src #dst #def whd #lbl #H @H ] #hd2 #tl #IH #src #dst #def whd #lbl #H
145whd in match (adds_graph_list ??????);
146whd in match fresh_label; normalize nodelta
147inversion (fresh ??) #mid #luniv' #EQfresh lapply (sym_eq ??? EQfresh) -EQfresh #EQfresh
148normalize nodelta
149@IH whd in match (joint_if_luniverse ???);
150@(fresh_remains_fresh … EQfresh) @H
151qed.
152
153lemma with_last_not_empty : ∀X,pref,last.not_empty X (pref @ [last]).
154#X * [2: #hd #tl ] #last % qed.
155
156lemma split_on_last_ne_elim : ∀X,l.∀P : ((list X) × X) → Prop.
157(∀pref,last.pi1 ?? l = pref @ [last] → P 〈pref, last〉) →
158P (split_on_last_ne X l).
159#X * @list_elim_left [ * ] #last #pref #_ #prf #P #H
160>split_on_last_ne_def @H % qed.
161
162(* use Russell? *)
163lemma adds_graph_list_ok :
164  ∀g_pars,globals,b,src,dst,def.
165  fresh_for_univ … src (joint_if_luniverse … def) →
166  luniverse_ok ?? def →
167  let def' ≝ adds_graph_list g_pars globals b src dst def in
168  luniverse_ok ?? def' ∧
169  (∀lbl.lbl ≠ src → fresh_for_univ … lbl (joint_if_luniverse … def) →
170                      stmt_at … (joint_if_code … def') lbl =
171                      stmt_at … (joint_if_code … def) lbl) ∧
172  let B ≝ ensure_step_block … b in
173  ∃l.bool_to_Prop (uniqueb … l) ∧
174    All … (λlbl.¬fresh_for_univ … lbl (joint_if_luniverse … def) ∧
175                 fresh_for_univ … lbl (joint_if_luniverse … def')) l ∧
176    src ~❨B,l❩~> dst in joint_if_code … def'.
177#p #g #l elim l -l [2: #hd1 * [ #_ | #hd2 #tl #IH ]]
178#src #dst #def #Hsrc #Hdef
179[1,3: %
180  [1,3: %
181    [1,3: #lbl @(eq_identifier_elim … lbl src) #H destruct [1,3: #_ @Hsrc ]
182      whd in ⊢ (%→?); whd in match (adds_graph_list ??????);
183      >(lookup_add_miss ?????? H) @Hdef
184    |*: #lbl #H #G @lookup_add_miss @H
185    ]
186  |*: %{[]} % [1,3: %% ] %{src} % [1,3:%] %{dst} % [1,3: @lookup_add_hit ] %
187  ]
188]
189whd in match (adds_graph_list ??????);
190whd in match (fresh_label ???);
191inversion (fresh ??) normalize nodelta
192#mid #luniverse' #EQfresh lapply (sym_eq ??? EQfresh) -EQfresh #EQfresh
193letin def' ≝ (add_graph p g src (sequential … hd1 mid) (set_luniverse … def luniverse'))
194lapply (IH mid dst def' ??)
195[ #lbl @(eq_identifier_elim … lbl src) #H destruct
196  [2: whd in ⊢ (%→?); whd in match (adds_graph_list ??????);
197    >(lookup_add_miss ?????? H) ]
198  #Hpres @(fresh_remains_fresh … EQfresh) [ @Hdef ] assumption
199| whd in match def';
200  @(fresh_is_fresh … EQfresh)
201]
202whd in match (joint_if_luniverse ???);
203whd in match (joint_if_code ???);
204** #Hdef'' #stmt_preserved * #l ** #Hl1 #Hl2
205whd in ⊢ (%→?); @split_on_last_ne_elim #pref #last #EQ * #mid' * #Hl3 #Hl4
206%
207[ %{Hdef''} #lbl #NEQ
208  @(eq_identifier_elim ?? lbl mid)
209  [ #EQ destruct #ABS cases (absurd ? ABS ?) @(fresh_not_in_univ … EQfresh)
210  | #NEQ' #H >(stmt_preserved … NEQ')
211    [ whd in match (joint_if_code ???);
212      whd in match (stmt_at ????); >lookup_add_miss [2: @NEQ ] %
213    | @(fresh_remains_fresh … EQfresh) @H
214    ]
215  ]
216]
217%{(mid::l)}
218% [ % ]
219[ whd in ⊢ (?%);
220  cut (Not (bool_to_Prop (mid∈l)))
221  [ % #H elim (All_memb … Hl2 H)
222    whd in match (joint_if_luniverse ???);
223    #G #_ @(absurd ?? G)
224    @ (fresh_is_fresh … EQfresh)
225  | #H >H assumption
226  ]
227| %
228  [ %{(fresh_not_in_univ … EQfresh)}
229    @adds_graph_list_fresh_preserve @(fresh_is_fresh … EQfresh)
230  | @(All_mp … Hl2) #lbl * * #H1 #H2 %{H2} % #H3 @H1
231    @(fresh_remains_fresh … EQfresh) assumption
232  ]
233| whd in match (ensure_step_block ???) in EQ ⊢ %;
234  whd in match (map ??? (hd2 :: ?)); >EQ whd
235  change with ((?::?)@?) in match (?::?@?); >split_on_last_ne_def
236  %{mid'} % [2: @Hl4 ]
237  %{Hl3} %{mid} >stmt_preserved
238  [ % [2: % ] @lookup_add_hit
239  | @(fresh_remains_fresh … EQfresh) assumption
240  | % #ABS destruct @(absurd ? Hsrc) @(fresh_not_in_univ … EQfresh)
241  ]
242]
243qed.
244*)
245(*
246axiom adds_graph_ok :
247  ∀g_pars,globals,B,src,dst,def.
248  fresh_for_univ … src (joint_if_luniverse … def) →
249  luniverse_ok ?? def →
250  let def' ≝ adds_graph g_pars globals B src dst def in
251  luniverse_ok ?? def' ∧
252  (∀lbl.lbl ≠ src → fresh_for_univ … lbl (joint_if_luniverse … def) →
253                      stmt_at … (joint_if_code … def') lbl =
254                      stmt_at … (joint_if_code … def) lbl) ∧
255  ∃l.bool_to_Prop (uniqueb … l) ∧
256    All … (λlbl.¬fresh_for_univ … lbl (joint_if_luniverse … def) ∧
257                 fresh_for_univ … lbl (joint_if_luniverse … def')) l ∧
258    src ~❨B,src::l❩~> dst in joint_if_code … def'.
259 
260axiom fin_adds_graph_ok :
261  ∀g_pars,globals,B,src,def.
262  fresh_for_univ … src (joint_if_luniverse … def) →
263  luniverse_ok ?? def →
264  let def' ≝ fin_adds_graph g_pars globals B src def in
265  luniverse_ok ?? def' ∧
266  (∀lbl.lbl ≠ src → fresh_for_univ … lbl (joint_if_luniverse … def) →
267                      stmt_at … (joint_if_code … def') lbl =
268                      stmt_at … (joint_if_code … def) lbl) ∧
269  ∃l.bool_to_Prop (uniqueb … l) ∧
270    All … (λlbl.¬fresh_for_univ … lbl (joint_if_luniverse … def) ∧
271                 fresh_for_univ … lbl (joint_if_luniverse … def')) l ∧
272    src ~❨B,src::l❩~> it in joint_if_code … def'.
273*)
274
275definition append_seq_list :
276∀p,g.bind_step_block p g → bind_new register (list (joint_seq p g)) →
277  bind_step_block p g ≝
278λp,g,bbl,bl.
279! 〈pref, op, post〉 ← bbl ; ! l ← bl ; return 〈pref, op, post @ l〉.
280
281(*
282definition insert_epilogue ≝
283  λg_pars:graph_params.λglobals.λinsts : list (joint_seq g_pars globals).
284  λdef : joint_internal_function g_pars globals.
285  let exit ≝ joint_if_exit … def in
286  match stmt_at … exit
287  return λx.match x with [None ⇒ false | Some _ ⇒ true] → ?
288  with
289  [ Some s ⇒ λ_.
290    let 〈def', tmp〉 as prf ≝ adds_graph_list ?? insts exit def in
291    let def'' ≝ add_graph … tmp s def' in
292    set_joint_code … def'' (joint_if_code … def'') (joint_if_entry … def'') tmp
293  | None ⇒ Ⓧ
294  ] (pi2 … exit).
295whd in match def''; >graph_code_has_point //
296qed.
297*)
298
299definition b_adds_graph :
300  ∀g_pars: graph_params.
301  ∀globals: list ident.
302  ∀b : bind_step_block g_pars globals.
303  label → label →
304  joint_internal_function g_pars globals→
305  joint_internal_function g_pars globals ≝
306  λg_pars,globals,insts,src,dst,def.
307  let 〈def, stmts〉 ≝ bcompile ??? (fresh_register …) insts def in
308  adds_graph … stmts src dst def.
309
310(*
311axiom b_adds_graph_ok :
312  ∀g_pars,globals,B,src,dst,def.
313  fresh_for_univ … src (joint_if_luniverse … def) →
314  luniverse_ok ?? def →
315  let def' ≝ b_adds_graph g_pars globals B src dst def in
316  luniverse_ok ?? def' ∧
317  (∀lbl.lbl ≠ src → fresh_for_univ … lbl (joint_if_luniverse … def) →
318                      stmt_at … (joint_if_code … def') lbl =
319                      stmt_at … (joint_if_code … def) lbl) ∧
320  ∃l,r.
321    bool_to_Prop (uniqueb … l) ∧
322    bool_to_Prop (uniqueb … r) ∧
323    All … (λlbl.¬fresh_for_univ … lbl (joint_if_luniverse … def) ∧
324                 fresh_for_univ … lbl (joint_if_luniverse … def')) l ∧
325    All … (λreg.¬fresh_for_univ … reg (joint_if_runiverse … def) ∧
326                 fresh_for_univ … reg (joint_if_runiverse … def')) r ∧
327    src ~❨B,src::l,r❩~> dst in joint_if_code … def'.
328*)
329definition b_fin_adds_graph :
330  ∀g_pars: graph_params.
331  ∀globals: list ident.
332  ∀b : bind_fin_block g_pars globals.
333  label →
334  joint_internal_function g_pars globals→
335  joint_internal_function g_pars globals ≝
336  λg_pars,globals,insts,src,def.
337  let 〈def, stmts〉 ≝ bcompile ??? (fresh_register …) insts def in
338  fin_adds_graph … stmts src def.
339
340(*
341axiom b_fin_adds_graph_ok :
342  ∀g_pars,globals,B,src,def.
343  fresh_for_univ … src (joint_if_luniverse … def) →
344  luniverse_ok ?? def →
345  let def' ≝ b_fin_adds_graph g_pars globals B src def in
346  luniverse_ok ?? def' ∧
347  (∀lbl.lbl ≠ src → fresh_for_univ … lbl (joint_if_luniverse … def) →
348                      stmt_at … (joint_if_code … def') lbl =
349                      stmt_at … (joint_if_code … def) lbl) ∧
350  ∃l,r.
351    bool_to_Prop (uniqueb … l) ∧
352    bool_to_Prop (uniqueb … r) ∧
353    All … (λlbl.¬fresh_for_univ … lbl (joint_if_luniverse … def) ∧
354                 fresh_for_univ … lbl (joint_if_luniverse … def')) l ∧
355    All … (λreg.¬fresh_for_univ … reg (joint_if_runiverse … def) ∧
356                 fresh_for_univ … reg (joint_if_runiverse … def')) r ∧
357    src ~❨B,src::l,r❩~> it in joint_if_code … def'.
358*)
359
360definition partial_partition : ∀X.∀Y : DeqSet.(X → option (list Y)) → Prop ≝
361λX,Y,f.
362(∀x.opt_All … (λys.bool_to_Prop (uniqueb … ys)) (f x)) ∧
363(∀x1,x2.
364  opt_All …
365    (λys1.
366      opt_All …
367      (λys2.
368        ∀y.y ∈ ys1 → y ∈ ys2 → x1 = x2)
369      (f x2))
370    (f x1)).
371
372lemma opt_All_intro : ∀X,P,o.
373(∀x.o = Some ? x → P x) → opt_All X P o. #X #P * [//] #x #H @H % qed.
374 
375(*
376definition points_of : ∀p,g.joint_internal_function p g → Type[0] ≝
377λp,g,def.Σl.bool_to_Prop (code_has_point … (joint_if_code … def) l).
378
379unification hint 0 ≔ p, g, def;
380points ≟ code_point p,
381code ≟ joint_if_code p g def,
382P ≟ λl : points.bool_to_Prop (code_has_point p g code l)
383
384points_of p g def ≡ Sig points P.
385
386definition stmt_at_safe : ∀p,g,def.points_of p g def → joint_statement p g ≝
387  λp,g,def,pt.opt_safe ? (stmt_at ?? (joint_if_code ?? def) (pi1 … pt)) ?.
388@hide_prf cases pt -pt #pt whd in ⊢ (?%→?); #H % #G >G in H; * qed.
389*)
390
391record b_graph_translate_data
392  (src, dst : graph_params)
393  (globals : list ident) : Type[0] ≝
394{ init_ret : call_dest dst
395; init_params : paramsT dst
396; init_stack_size : ℕ
397; added_prologue : list (joint_seq dst globals)
398; f_step : label → joint_step src globals → bind_step_block dst globals
399; f_fin : label → joint_fin_step src → bind_fin_block dst globals
400; good_f_step_good :
401  ∀l,s.bind_new_P ??
402    (λblock.let 〈pref, op, post〉 ≝ block in
403       All (label → joint_seq ??)
404         (λs'.∀l.step_forall_labels … (In ? (l :: step_labels … s)) (s' l))
405         pref ∧
406       (∀l.step_forall_labels … (In ? (l :: step_labels … s)) (op l)) ∧
407       All (joint_seq ??) (step_forall_labels … (In ? (step_labels … s))) post)
408    (f_step l s)
409; good_f_fin :
410  ∀l,s.bind_new_P ??
411    (λblock.let 〈pref, op〉 ≝ block in
412       All (joint_seq ??) (step_forall_labels … (In ? (fin_step_labels … s))) pref ∧
413       All … (In ? (fin_step_labels … s)) (fin_step_labels … op))
414    (f_fin l s)
415; f_step_on_cost :
416  ∀l,c.f_step l (COST_LABEL … c) = bret … [ COST_LABEL … c ]
417}.
418
419definition get_first_costlabel : ∀p,g.
420  joint_closed_internal_function p g → costlabel × (succ p) ≝
421  λp,g,def.
422  match stmt_at … (joint_if_code … def) (joint_if_entry … def)
423  return λx.stmt_at ???? = x → ? with
424  [ Some s ⇒
425    match s return λx.stmt_at ???? = Some ? x → ? with
426    [ sequential s' nxt ⇒
427      match s' return λx.stmt_at ???? = Some ? (sequential … x nxt) → ? with
428      [ step_seq s'' ⇒
429        match s'' return λx.stmt_at ???? = Some ? (sequential … (step_seq … x) nxt) → ? with
430        [ COST_LABEL c ⇒ λ_.〈c, nxt〉
431        | _ ⇒ λabs.⊥
432        ]
433      | _ ⇒ λabs.⊥
434      ]
435    | _ ⇒ λabs.⊥
436    ]
437  | _ ⇒ λabs.⊥
438  ] (refl …).
439@hide_prf
440cases def in abs; -def #def #good_def
441cases (entry_costed … good_def) #c * #nxt' #EQ >EQ #ABS destruct
442qed.
443
444record b_graph_translate_props
445  (src_g_pars, dst_g_pars : graph_params)
446  (globals: list ident)
447  (data : b_graph_translate_data src_g_pars dst_g_pars globals)
448  (data_regs : list register)
449  (def_in : joint_closed_internal_function src_g_pars globals)
450  (def_out : joint_closed_internal_function dst_g_pars globals)
451  (f_lbls : label → option (list label))
452  (f_regs : label → option (list register)) : Prop ≝
453{ res_def_out_eq :
454           joint_if_result … def_out = init_ret … data
455; pars_def_out_eq :
456           joint_if_params … def_out = init_params … data
457; ss_def_out_eq :
458           joint_if_stacksize … def_out = init_stack_size … data
459; entry_eq :
460          pi1 … (joint_if_entry … def_out) = pi1 … (joint_if_entry … def_in)
461; partition_lbls : partial_partition … f_lbls
462; partition_regs : partial_partition … f_regs
463; freshness_lbls :
464  (∀l.opt_All … (All …
465    (λlbl.¬fresh_for_univ … lbl (joint_if_luniverse … def_in) ∧
466           fresh_for_univ … lbl (joint_if_luniverse … def_out))) (f_lbls l))
467; freshness_regs :
468  (∀l.opt_All … (All …
469    (λreg.¬fresh_for_univ … reg (joint_if_runiverse … def_in) ∧
470           fresh_for_univ … reg (joint_if_runiverse … def_out))) (f_regs l))
471; freshness_data_regs :
472  All … (λreg.¬fresh_for_univ … reg (joint_if_runiverse … def_in) ∧
473               fresh_for_univ … reg (joint_if_runiverse … def_out)) data_regs
474; data_regs_disjoint : ∀l.opt_All … (λregs.∀r.r ∈ regs → r ∈ data_regs → False) (f_regs l)
475; multi_fetch_ok :
476  ∀l,s.stmt_at … (joint_if_code … def_in) l = Some ? s →
477  ∃lbls,regs.f_lbls l = Some ? lbls ∧ f_regs l = Some ? regs ∧
478  match s with
479  [ sequential s' nxt ⇒
480    let block ≝
481      if eq_identifier … (joint_if_entry … def_in) l then
482        append_seq_list … (f_step … data l s') (added_prologue … data)
483      else
484        f_step … data l s' in
485    l ~❨block, l::lbls, regs❩~> nxt in joint_if_code … def_out
486  | final s' ⇒
487    l ~❨f_fin … data l s', l::lbls, regs❩~> it in joint_if_code … def_out
488  | FCOND abs _ _ _ ⇒ Ⓧabs
489  ]
490}.
491
492lemma if_merge_right : ∀A.∀b.∀x,y : A.x = y → if b then x else y = y.
493#A * #x #y #EQ >EQ % qed.
494
495lemma append_seq_list_nil : ∀p,g,b.append_seq_list p g b [ ] = b.
496#p #g #b elim b -b
497[ ** #a #b #c normalize >append_nil %
498| #f #IH @bnew_proper #r @IH
499]
500qed.
501
502definition pair_swap : ∀A,B.(A × B) → B × A ≝ λA,B,pr.〈\snd pr, \fst pr〉.
503
504(* translation with inline fresh register allocation *)
505definition b_graph_translate :
506  ∀src_g_pars,dst_g_pars : graph_params.
507  ∀globals: list ident.
508  (* initialization info *)
509  ∀data : bind_new register (b_graph_translate_data src_g_pars dst_g_pars globals).
510  (* source function *)
511  ∀def_in : joint_closed_internal_function src_g_pars globals.
512  (* destination function *)
513  Σdef_out : joint_closed_internal_function dst_g_pars globals.
514  ∃data',regs,f_lbls,f_regs.
515    bind_new_instantiates … data' data regs ∧
516    b_graph_translate_props … data' regs def_in def_out f_lbls f_regs
517   ≝
518  λsrc_g_pars,dst_g_pars,globals,data,def.
519  let runiv_data ≝ bcompile … (pair_swap ?? ∘ fresh RegisterTag) data (joint_if_runiverse … def) in
520  let runiv ≝ \fst runiv_data in
521  let data ≝ \snd runiv_data in
522  let entry ≝ joint_if_entry … def in
523  let init ≝
524    mk_joint_internal_function dst_g_pars globals
525    (joint_if_luniverse … def)
526    runiv
527    (init_ret … data) (init_params … data) (init_stack_size … data)
528    (add ?? (empty_map ? (joint_statement ??)) entry (RETURN …))
529    («pi1 … entry, mem_set_add_id …») in
530  let f : label → joint_statement (src_g_pars : params) globals →
531    joint_internal_function dst_g_pars globals → joint_internal_function dst_g_pars globals ≝
532    λlbl,stmt,def.
533    match stmt with
534    [ sequential inst next ⇒
535      b_adds_graph … (f_step … data lbl inst) lbl next def
536    | final inst ⇒
537      b_fin_adds_graph … (f_fin … data lbl inst) lbl def
538    | FCOND abs _ _ _ ⇒ Ⓧabs
539    ] in
540  let def_out ≝ foldi ??? f (joint_if_code … def) init in
541  let init_c_nxt ≝ get_first_costlabel … def in
542  let def_out_nxt ≝ adds_graph_post … (added_prologue … data) (\snd (init_c_nxt)) def_out in
543  ««add_graph … entry (sequential … (COST_LABEL … (\fst init_c_nxt)) (\snd def_out_nxt)) (\fst def_out_nxt), ?», ?».
544@hide_prf
545[ cases daemon
546| cases daemon (* TODO *)
547] qed.
548
549definition b_graph_transform_program :
550  ∀src_g_pars,dst_g_pars : graph_params.
551  (* initialization *)
552  (∀globals.joint_closed_internal_function src_g_pars globals →
553    bind_new register (b_graph_translate_data src_g_pars dst_g_pars globals)) →
554  joint_program src_g_pars →
555  joint_program dst_g_pars ≝
556  λsrc,dst,init,p.
557  transform_program ??? p
558    (λvarnames.transf_fundef ?? (λdef_in.
559      b_graph_translate … (init varnames def_in) def_in)).
560
561definition added_registers :
562  ∀p : graph_params.∀g.
563  joint_internal_function p g → (label → option (list register)) → list register ≝
564  λp,g,def,f_regs.
565  let f ≝ λlbl : label.λ_.λacc.
566    match f_regs lbl with [ None ⇒ acc | Some regs ⇒ regs@acc ] in
567  foldi … f (joint_if_code p g def) [ ].
568
569axiom added_registers_ok :
570  ∀p,g,def,f_regs.
571  ∀l,s.stmt_at … (joint_if_code … def) l = Some ? s →
572  opt_All … (All … (λlbl.bool_to_Prop (lbl ∈ added_registers p g def f_regs))) (f_regs l).
573
574(*(* translation without register allocation (more or less an alias) *)
575definition graph_translate :
576  ∀src_g_pars,dst_g_pars : graph_params.
577  ∀globals: list ident.
578  (* initialization info *)
579  call_dest dst_g_pars → (* joint_if_result *)
580  paramsT dst_g_pars → (* joint_if_params *)
581  ℕ → (* joint_if_stacksize *)
582  (* functions dictating the translation *)
583  (label → joint_step src_g_pars globals → step_block dst_g_pars globals) →
584  (label → joint_fin_step src_g_pars → fin_block dst_g_pars globals) →
585  (* source function *)
586  joint_internal_function src_g_pars globals →
587  (* destination function *)
588  joint_internal_function dst_g_pars globals ≝
589  λsrc_g_pars,dst_g_pars,globals,init1,init2,init3,trans_step,trans_fin_step.
590  b_graph_translate … init1 init2 init3
591    (λl,s.return trans_step l s)
592    (λl,s.return trans_fin_step l s).
593*)
594(*
595let rec add_translates
596  (pars1: params1) (globals: list ident)
597  (translate_list: list ?) (start_lbl: label) (dest_lbl: label)
598  (def: joint_internal_function … (graph_params pars1 globals))
599    on translate_list ≝
600  match translate_list with
601  [ nil ⇒ add_graph … start_lbl (GOTO … dest_lbl) def
602  | cons trans translate_list ⇒
603    match translate_list with
604    [ nil ⇒ trans start_lbl dest_lbl def
605    | _ ⇒
606      let 〈tmp_lbl, def〉 ≝ fresh_label … def in
607      let def ≝ trans start_lbl tmp_lbl def in
608        add_translates pars1 globals translate_list tmp_lbl dest_lbl def]].
609
610definition adds_graph ≝
611 λpars1:params1.λglobals. λstmt_list: list (label → joint_statement (graph_params_ pars1) globals).
612  add_translates … (map ?? (λf,start_lbl,dest_lbl. add_graph pars1 ? start_lbl (f dest_lbl)) stmt_list).
613  *)
Note: See TracBrowser for help on using the repository browser.