source: src/joint/TranslateUtils.ma @ 2674

Last change on this file since 2674 was 2674, checked in by tranquil, 8 years ago
  • another change in block definition
  • RTLabs -> RTL and ERTL -> ERTLptr passes fixed, others stil broken
File size: 20.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
95definition luniverse_ok : ∀p : graph_params.∀g.joint_internal_function p g → Prop ≝
96λp,g,def.fresh_map_for_univ … (joint_if_code … def) (joint_if_luniverse … def).
97
98(*
99lemma All_fresh_not_memb : ∀tag,u,l,id,u'.
100  All (identifier tag) (λid'.¬fresh_for_univ tag id' u) l →
101  〈id, u'〉 = fresh tag u →
102  ¬id ∈ l.
103#tag #u #l elim l [2: #hd #tl #IH] #id #u' *
104[ #hd_fresh #tl_fresh #EQfresh
105  whd in ⊢ (?(?%));
106  change with (eq_identifier ???) in match (?==?);
107  >eq_identifier_sym
108  >(eq_identifier_false … (fresh_distinct … hd_fresh EQfresh))
109  normalize nodelta @(IH … tl_fresh EQfresh)
110| #_ %
111]
112qed.
113*)
114
115lemma fresh_was_fresh : ∀tag,id,id',u,u'.
116〈id,u'〉 = fresh tag u →
117fresh_for_univ tag id' u' →
118id' ≠ id →
119fresh_for_univ tag id' u.
120#tag * #id * #id' * #u * #u'
121normalize #EQfresh destruct
122#H #NEQ
123elim (le_to_or_lt_eq … H)
124[ (* not recompiling... /2 by monotonic_pred/ *) /2/ ]
125#H >(succ_injective … H) in NEQ;
126* #G elim (G (refl …))
127qed.
128
129lemma fresh_not_in_univ : ∀tag,id,u,u'.
130〈id, u'〉 = fresh tag u →
131¬fresh_for_univ tag id u.
132#tag * #id * #u * #u' normalize #EQ destruct //
133qed.
134
135(*
136lemma adds_graph_list_fresh_preserve :
137  ∀g_pars,globals,b,src,dst,def.
138  let def' ≝ adds_graph_list g_pars globals b src dst def in
139  ∀lbl.fresh_for_univ … lbl (joint_if_luniverse … def) →
140       fresh_for_univ … lbl (joint_if_luniverse … def').
141#g_pars #globals #l elim l -l
142[ #src #dst #def whd #lbl #H @H ]
143#hd1 * [ #_ #src #dst #def whd #lbl #H @H ] #hd2 #tl #IH #src #dst #def whd #lbl #H
144whd in match (adds_graph_list ??????);
145whd in match fresh_label; normalize nodelta
146inversion (fresh ??) #mid #luniv' #EQfresh lapply (sym_eq ??? EQfresh) -EQfresh #EQfresh
147normalize nodelta
148@IH whd in match (joint_if_luniverse ???);
149@(fresh_remains_fresh … EQfresh) @H
150qed.
151
152lemma with_last_not_empty : ∀X,pref,last.not_empty X (pref @ [last]).
153#X * [2: #hd #tl ] #last % qed.
154
155lemma split_on_last_ne_elim : ∀X,l.∀P : ((list X) × X) → Prop.
156(∀pref,last.pi1 ?? l = pref @ [last] → P 〈pref, last〉) →
157P (split_on_last_ne X l).
158#X * @list_elim_left [ * ] #last #pref #_ #prf #P #H
159>split_on_last_ne_def @H % qed.
160
161(* use Russell? *)
162lemma adds_graph_list_ok :
163  ∀g_pars,globals,b,src,dst,def.
164  fresh_for_univ … src (joint_if_luniverse … def) →
165  luniverse_ok ?? def →
166  let def' ≝ adds_graph_list g_pars globals b src dst def in
167  luniverse_ok ?? def' ∧
168  (∀lbl.lbl ≠ src → fresh_for_univ … lbl (joint_if_luniverse … def) →
169                      stmt_at … (joint_if_code … def') lbl =
170                      stmt_at … (joint_if_code … def) lbl) ∧
171  let B ≝ ensure_step_block … b in
172  ∃l.bool_to_Prop (uniqueb … l) ∧
173    All … (λlbl.¬fresh_for_univ … lbl (joint_if_luniverse … def) ∧
174                 fresh_for_univ … lbl (joint_if_luniverse … def')) l ∧
175    src ~❨B,l❩~> dst in joint_if_code … def'.
176#p #g #l elim l -l [2: #hd1 * [ #_ | #hd2 #tl #IH ]]
177#src #dst #def #Hsrc #Hdef
178[1,3: %
179  [1,3: %
180    [1,3: #lbl @(eq_identifier_elim … lbl src) #H destruct [1,3: #_ @Hsrc ]
181      whd in ⊢ (%→?); whd in match (adds_graph_list ??????);
182      >(lookup_add_miss ?????? H) @Hdef
183    |*: #lbl #H #G @lookup_add_miss @H
184    ]
185  |*: %{[]} % [1,3: %% ] %{src} % [1,3:%] %{dst} % [1,3: @lookup_add_hit ] %
186  ]
187]
188whd in match (adds_graph_list ??????);
189whd in match (fresh_label ???);
190inversion (fresh ??) normalize nodelta
191#mid #luniverse' #EQfresh lapply (sym_eq ??? EQfresh) -EQfresh #EQfresh
192letin def' ≝ (add_graph p g src (sequential … hd1 mid) (set_luniverse … def luniverse'))
193lapply (IH mid dst def' ??)
194[ #lbl @(eq_identifier_elim … lbl src) #H destruct
195  [2: whd in ⊢ (%→?); whd in match (adds_graph_list ??????);
196    >(lookup_add_miss ?????? H) ]
197  #Hpres @(fresh_remains_fresh … EQfresh) [ @Hdef ] assumption
198| whd in match def';
199  @(fresh_is_fresh … EQfresh)
200]
201whd in match (joint_if_luniverse ???);
202whd in match (joint_if_code ???);
203** #Hdef'' #stmt_preserved * #l ** #Hl1 #Hl2
204whd in ⊢ (%→?); @split_on_last_ne_elim #pref #last #EQ * #mid' * #Hl3 #Hl4
205%
206[ %{Hdef''} #lbl #NEQ
207  @(eq_identifier_elim ?? lbl mid)
208  [ #EQ destruct #ABS cases (absurd ? ABS ?) @(fresh_not_in_univ … EQfresh)
209  | #NEQ' #H >(stmt_preserved … NEQ')
210    [ whd in match (joint_if_code ???);
211      whd in match (stmt_at ????); >lookup_add_miss [2: @NEQ ] %
212    | @(fresh_remains_fresh … EQfresh) @H
213    ]
214  ]
215]
216%{(mid::l)}
217% [ % ]
218[ whd in ⊢ (?%);
219  cut (Not (bool_to_Prop (mid∈l)))
220  [ % #H elim (All_memb … Hl2 H)
221    whd in match (joint_if_luniverse ???);
222    #G #_ @(absurd ?? G)
223    @ (fresh_is_fresh … EQfresh)
224  | #H >H assumption
225  ]
226| %
227  [ %{(fresh_not_in_univ … EQfresh)}
228    @adds_graph_list_fresh_preserve @(fresh_is_fresh … EQfresh)
229  | @(All_mp … Hl2) #lbl * * #H1 #H2 %{H2} % #H3 @H1
230    @(fresh_remains_fresh … EQfresh) assumption
231  ]
232| whd in match (ensure_step_block ???) in EQ ⊢ %;
233  whd in match (map ??? (hd2 :: ?)); >EQ whd
234  change with ((?::?)@?) in match (?::?@?); >split_on_last_ne_def
235  %{mid'} % [2: @Hl4 ]
236  %{Hl3} %{mid} >stmt_preserved
237  [ % [2: % ] @lookup_add_hit
238  | @(fresh_remains_fresh … EQfresh) assumption
239  | % #ABS destruct @(absurd ? Hsrc) @(fresh_not_in_univ … EQfresh)
240  ]
241]
242qed.
243*)
244
245axiom adds_graph_ok :
246  ∀g_pars,globals,B,src,dst,def.
247  fresh_for_univ … src (joint_if_luniverse … def) →
248  luniverse_ok ?? def →
249  let def' ≝ adds_graph g_pars globals B src dst def in
250  luniverse_ok ?? def' ∧
251  (∀lbl.lbl ≠ src → fresh_for_univ … lbl (joint_if_luniverse … def) →
252                      stmt_at … (joint_if_code … def') lbl =
253                      stmt_at … (joint_if_code … def) lbl) ∧
254  ∃l.bool_to_Prop (uniqueb … l) ∧
255    All … (λlbl.¬fresh_for_univ … lbl (joint_if_luniverse … def) ∧
256                 fresh_for_univ … lbl (joint_if_luniverse … def')) l ∧
257    src ~❨B,l❩~> dst in joint_if_code … def'.
258 
259axiom fin_adds_graph_ok :
260  ∀g_pars,globals,B,src,def.
261  fresh_for_univ … src (joint_if_luniverse … def) →
262  luniverse_ok ?? def →
263  let def' ≝ fin_adds_graph g_pars globals B src def in
264  luniverse_ok ?? def' ∧
265  (∀lbl.lbl ≠ src → fresh_for_univ … lbl (joint_if_luniverse … def) →
266                      stmt_at … (joint_if_code … def') lbl =
267                      stmt_at … (joint_if_code … def) lbl) ∧
268  ∃l.bool_to_Prop (uniqueb … l) ∧
269    All … (λlbl.¬fresh_for_univ … lbl (joint_if_luniverse … def) ∧
270                 fresh_for_univ … lbl (joint_if_luniverse … def')) l ∧
271    src ~❨B,l❩~> it in joint_if_code … def'.
272
273(* preserves first statement if a cost label (should be an invariant) *)
274definition insert_prologue ≝
275  λg_pars:graph_params.λglobals.λinsts : list (joint_seq g_pars globals).
276  λdef : joint_internal_function g_pars globals.
277  let entry ≝ joint_if_entry … def in
278  match stmt_at … entry
279  return λx.match x with [None ⇒ false | Some _ ⇒ true] → ?
280  with
281  [ Some s ⇒ λ_.
282    let default_add ≝ λ_ : unit.
283      let 〈def', lbl〉 ≝ fresh_label … def in
284      let def'' ≝ add_graph … lbl s def' in
285      adds_graph … insts entry lbl def'' in
286    match s with
287    [ sequential s' next ⇒
288      match s' with
289      [ step_seq s'' ⇒
290        match s'' with
291        [ COST_LABEL _ ⇒
292          adds_graph ?? (s'' :: insts) entry next def
293        | _ ⇒
294          default_add it
295        ]
296      | _ ⇒
297        default_add it
298      ]
299    | _ ⇒
300      default_add it
301    ]
302  | None ⇒ Ⓧ
303  ] (pi2 … entry).
304
305(*
306definition insert_epilogue ≝
307  λg_pars:graph_params.λglobals.λinsts : list (joint_seq g_pars globals).
308  λdef : joint_internal_function g_pars globals.
309  let exit ≝ joint_if_exit … def in
310  match stmt_at … exit
311  return λx.match x with [None ⇒ false | Some _ ⇒ true] → ?
312  with
313  [ Some s ⇒ λ_.
314    let 〈def', tmp〉 as prf ≝ adds_graph_list ?? insts exit def in
315    let def'' ≝ add_graph … tmp s def' in
316    set_joint_code … def'' (joint_if_code … def'') (joint_if_entry … def'') tmp
317  | None ⇒ Ⓧ
318  ] (pi2 … exit).
319whd in match def''; >graph_code_has_point //
320qed.
321*)
322
323definition b_adds_graph :
324  ∀g_pars: graph_params.
325  ∀globals: list ident.
326  ∀b : bind_step_block g_pars globals.
327  label → label →
328  joint_internal_function g_pars globals→
329  joint_internal_function g_pars globals ≝
330  λg_pars,globals,insts,src,dst,def.
331  let 〈def, stmts〉 ≝ bcompile ??? (fresh_register …) insts def in
332  adds_graph … stmts src dst def.
333
334axiom b_adds_graph_ok :
335  ∀g_pars,globals,B,src,dst,def.
336  fresh_for_univ … src (joint_if_luniverse … def) →
337  luniverse_ok ?? def →
338  let def' ≝ b_adds_graph g_pars globals B src dst def in
339  luniverse_ok ?? def' ∧
340  (∀lbl.lbl ≠ src → fresh_for_univ … lbl (joint_if_luniverse … def) →
341                      stmt_at … (joint_if_code … def') lbl =
342                      stmt_at … (joint_if_code … def) lbl) ∧
343  ∃l,r.
344    bool_to_Prop (uniqueb … l) ∧
345    bool_to_Prop (uniqueb … r) ∧
346    All … (λlbl.¬fresh_for_univ … lbl (joint_if_luniverse … def) ∧
347                 fresh_for_univ … lbl (joint_if_luniverse … def')) l ∧
348    All … (λreg.¬fresh_for_univ … reg (joint_if_runiverse … def) ∧
349                 fresh_for_univ … reg (joint_if_runiverse … def')) r ∧
350    src ~❨B,l,r❩~> dst in joint_if_code … def'.
351 
352definition b_fin_adds_graph :
353  ∀g_pars: graph_params.
354  ∀globals: list ident.
355  ∀b : bind_fin_block g_pars globals.
356  label →
357  joint_internal_function g_pars globals→
358  joint_internal_function g_pars globals ≝
359  λg_pars,globals,insts,src,def.
360  let 〈def, stmts〉 ≝ bcompile ??? (fresh_register …) insts def in
361  fin_adds_graph … stmts src def.
362
363axiom b_fin_adds_graph_ok :
364  ∀g_pars,globals,B,src,def.
365  fresh_for_univ … src (joint_if_luniverse … def) →
366  luniverse_ok ?? def →
367  let def' ≝ b_fin_adds_graph g_pars globals B src def in
368  luniverse_ok ?? def' ∧
369  (∀lbl.lbl ≠ src → fresh_for_univ … lbl (joint_if_luniverse … def) →
370                      stmt_at … (joint_if_code … def') lbl =
371                      stmt_at … (joint_if_code … def) lbl) ∧
372  ∃l,r.
373    bool_to_Prop (uniqueb … l) ∧
374    bool_to_Prop (uniqueb … r) ∧
375    All … (λlbl.¬fresh_for_univ … lbl (joint_if_luniverse … def) ∧
376                 fresh_for_univ … lbl (joint_if_luniverse … def')) l ∧
377    All … (λreg.¬fresh_for_univ … reg (joint_if_runiverse … def) ∧
378                 fresh_for_univ … reg (joint_if_runiverse … def')) r ∧
379    src ~❨B,l,r❩~> it in joint_if_code … def'.
380
381(* translation with inline fresh register allocation *)
382definition b_graph_translate :
383  ∀src_g_pars,dst_g_pars : graph_params.
384  ∀globals: list ident.
385  (* initialization info *)
386  call_dest dst_g_pars → (* joint_if_result *)
387  paramsT dst_g_pars → (* joint_if_params *)
388  ℕ → (* joint_if_stacksize *)
389  (* functions dictating the translation *)
390  (label → joint_step src_g_pars globals → bind_step_block dst_g_pars globals) →
391  (label → joint_fin_step src_g_pars → bind_fin_block dst_g_pars globals) →
392  (* source function *)
393  joint_internal_function src_g_pars globals →
394  (* destination function *)
395  joint_internal_function dst_g_pars globals ≝
396  λsrc_g_pars,dst_g_pars,globals,
397   init_ret,init_params,init_stack_size,trans_step,trans_fin_step,def.
398  let init ≝
399    mk_joint_internal_function dst_g_pars globals
400    (joint_if_luniverse … def)
401    (joint_if_runiverse … def)
402    init_ret init_params init_stack_size
403    (add ?? (empty_map ? (joint_statement ??)) (joint_if_entry … def) (RETURN …))
404    (pi1 … (joint_if_entry … def)) in
405  let f : label → joint_statement (src_g_pars : params) globals →
406    joint_internal_function dst_g_pars globals → joint_internal_function dst_g_pars globals ≝
407    λlbl,stmt,def.
408    match stmt with
409    [ sequential inst next ⇒
410      b_adds_graph … (trans_step lbl inst) lbl next def
411    | final inst ⇒
412      b_fin_adds_graph … (trans_fin_step lbl inst) lbl def
413    | FCOND abs _ _ _ ⇒ Ⓧabs
414    ] in
415  foldi … f (joint_if_code … def) init.
416@hide_prf >graph_code_has_point @mem_set_add_id qed.
417
418definition partial_partition : ∀X.∀Y : DeqSet.(X → option (list Y)) → Prop ≝
419λX,Y,f.
420(∀x.opt_All … (λys.bool_to_Prop (uniqueb … ys)) (f x)) ∧
421(∀x1,x2.
422  opt_All …
423    (λys1.
424      opt_All …
425      (λys2.
426        ∀y.y ∈ ys1 → y ∈ ys2 → x1 = x2)
427      (f x2))
428    (f x1)).
429
430lemma opt_All_intro : ∀X,P,o.
431(∀x.o = Some ? x → P x) → opt_All X P o. #X #P * [//] #x #H @H % qed.
432 
433(*
434definition points_of : ∀p,g.joint_internal_function p g → Type[0] ≝
435λp,g,def.Σl.bool_to_Prop (code_has_point … (joint_if_code … def) l).
436
437unification hint 0 ≔ p, g, def;
438points ≟ code_point p,
439code ≟ joint_if_code p g def,
440P ≟ λl : points.bool_to_Prop (code_has_point p g code l)
441
442points_of p g def ≡ Sig points P.
443
444definition stmt_at_safe : ∀p,g,def.points_of p g def → joint_statement p g ≝
445  λp,g,def,pt.opt_safe ? (stmt_at ?? (joint_if_code ?? def) (pi1 … pt)) ?.
446@hide_prf cases pt -pt #pt whd in ⊢ (?%→?); #H % #G >G in H; * qed.
447*)
448
449
450axiom b_graph_translate_ok :
451  ∀src_g_pars,dst_g_pars : graph_params.
452  ∀globals: list ident.
453  ∀init_ret,init_params,init_stack_size.
454  ∀f_step,f_fin,def_in.
455  luniverse_ok ?? def_in →
456  code_closed … (joint_if_code … def_in) →
457  let def_out ≝
458    b_graph_translate src_g_pars dst_g_pars globals
459      init_ret init_params init_stack_size f_step f_fin def_in in
460  luniverse_ok … def_out ∧
461  code_closed … (joint_if_code … def_out) ∧
462  joint_if_result … def_out = init_ret ∧
463  joint_if_params … def_out = init_params ∧
464  joint_if_stacksize … def_out = init_stack_size ∧
465  pi1 … (joint_if_entry … def_out) = pi1 … (joint_if_entry … def_in) ∧
466  ∃f_lbls : label → option (list label).
467  ∃f_regs : label → option (list register).
468  partial_partition … f_lbls ∧
469  partial_partition … f_regs ∧
470  (∀l.opt_All … (All …
471    (λlbl.¬fresh_for_univ … lbl (joint_if_luniverse … def_in) ∧
472           fresh_for_univ … lbl (joint_if_luniverse … def_out))) (f_lbls l)) ∧
473  (∀l.opt_All … (All …
474    (λreg.¬fresh_for_univ … reg (joint_if_runiverse … def_in) ∧
475           fresh_for_univ … reg (joint_if_runiverse … def_out))) (f_regs l)) ∧
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    l ~❨f_step l s', lbls, regs❩~> nxt in joint_if_code … def_out
481  | final s' ⇒
482    l ~❨f_fin l s', lbls, regs❩~> it in joint_if_code … def_out
483  | FCOND abs _ _ _ ⇒ Ⓧabs
484  ].
485
486definition added_registers :
487  ∀p : graph_params.∀g.
488  joint_internal_function p g → (label → option (list register)) → list register ≝
489  λp,g,def,f_regs.
490  let f ≝ λlbl : label.λ_.λacc.
491    match f_regs lbl with [ None ⇒ acc | Some regs ⇒ regs@acc ] in
492  foldi … f (joint_if_code p g def) [ ].
493
494axiom added_registers_ok :
495  ∀p,g,def,f_regs.
496  ∀l,s.stmt_at … (joint_if_code … def) l = Some ? s →
497  opt_All … (All … (λlbl.bool_to_Prop (lbl ∈ added_registers p g def f_regs))) (f_regs l).
498
499(* translation without register allocation (more or less an alias) *)
500definition graph_translate :
501  ∀src_g_pars,dst_g_pars : graph_params.
502  ∀globals: list ident.
503  (* initialization info *)
504  call_dest dst_g_pars → (* joint_if_result *)
505  paramsT dst_g_pars → (* joint_if_params *)
506  ℕ → (* joint_if_stacksize *)
507  (* functions dictating the translation *)
508  (label → joint_step src_g_pars globals → step_block dst_g_pars globals) →
509  (label → joint_fin_step src_g_pars → fin_block dst_g_pars globals) →
510  (* source function *)
511  joint_internal_function src_g_pars globals →
512  (* destination function *)
513  joint_internal_function dst_g_pars globals ≝
514  λsrc_g_pars,dst_g_pars,globals,init1,init2,init3,trans_step,trans_fin_step.
515  b_graph_translate … init1 init2 init3
516    (λl,s.return trans_step l s)
517    (λl,s.return trans_fin_step l s).
518
519(*
520let rec add_translates
521  (pars1: params1) (globals: list ident)
522  (translate_list: list ?) (start_lbl: label) (dest_lbl: label)
523  (def: joint_internal_function … (graph_params pars1 globals))
524    on translate_list ≝
525  match translate_list with
526  [ nil ⇒ add_graph … start_lbl (GOTO … dest_lbl) def
527  | cons trans translate_list ⇒
528    match translate_list with
529    [ nil ⇒ trans start_lbl dest_lbl def
530    | _ ⇒
531      let 〈tmp_lbl, def〉 ≝ fresh_label … def in
532      let def ≝ trans start_lbl tmp_lbl def in
533        add_translates pars1 globals translate_list tmp_lbl dest_lbl def]].
534
535definition adds_graph ≝
536 λpars1:params1.λglobals. λstmt_list: list (label → joint_statement (graph_params_ pars1) globals).
537  add_translates … (map ?? (λf,start_lbl,dest_lbl. add_graph pars1 ? start_lbl (f dest_lbl)) stmt_list).
538  *)
Note: See TracBrowser for help on using the repository browser.