source: src/joint/TranslateUtils.ma @ 2645

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