source: src/joint/TranslateUtils_paolo.ma @ 2162

Last change on this file since 2162 was 2162, checked in by tranquil, 8 years ago
  • yet another correction to joint
  • added functions adding prologues and epilogues in TranslateUtils?. Adding a prologue will preserve the invariant of having a cost label at the start of the function, without needing transformations later
  • redefined ERTL and rewritten RTLToERTL (with suffix "_paolo")
File size: 32.7 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  (* function dictating the translation *)
169  (label → joint_step src_g_pars globals →
170    list (joint_step dst_g_pars globals)) →
171  (label → ext_fin_stmt src_g_pars →
172    (list (joint_step dst_g_pars globals))
173    ×
174    (joint_statement dst_g_pars globals)) →
175  (* initialized function definition with empty graph *)
176  joint_internal_function … dst_g_pars →
177  (* source function *)
178  joint_internal_function … src_g_pars →
179  (* destination function *)
180  joint_internal_function … dst_g_pars ≝
181  λsrc_g_pars,dst_g_pars,globals,trans,trans',empty,def.
182  let f : label → joint_statement (src_g_pars : params) globals →
183    joint_internal_function … dst_g_pars → joint_internal_function … dst_g_pars ≝
184    λlbl,stmt,def.
185    match stmt with
186    [ sequential inst next ⇒
187      adds_graph dst_g_pars globals (trans lbl inst) lbl next def
188    | GOTO next ⇒ add_graph … lbl (GOTO … next) def
189    | RETURN ⇒ add_graph … lbl (RETURN …) def
190    | extension_fin c ⇒ let 〈l, fin〉 ≝ trans' lbl c in
191      let 〈def, tmp_lbl〉 ≝ fresh_label … def in
192      adds_graph … l lbl tmp_lbl (add_graph … tmp_lbl fin def)
193    ] in
194  foldi ??? f (joint_if_code ?? def) empty.
195*)
196(*
197definition graph_to_lin_statement :
198  ∀p : unserialized_params.∀globals.
199  joint_statement (mk_graph_params p) globals → joint_statement (mk_lin_params p) globals ≝
200  λp,globals,stmt.match stmt with
201  [ sequential c _ ⇒ sequential … c it
202  | final c ⇒
203    final ?? match c return λx.joint_fin_step (mk_lin_params p) globals with
204    [ GOTO l ⇒ GOTO … l
205    | RETURN ⇒ RETURN …
206    | extension_fin c ⇒ extension_fin ?? c
207    ]
208  ].
209
210lemma graph_to_lin_labels :
211  ∀p : unserialized_params.∀globals,s.
212  stmt_labels … (graph_to_lin_statement p globals s) =
213  stmt_explicit_labels … s.
214#p#globals * [//] * //
215qed.
216
217(* in order to make the coercion from lists to sets to work, one needs these hints *)
218unification hint 0 ≔ ;
219X ≟ identifier LabelTag
220
221list label ≡ list X.
222
223unification hint 0 ≔ ;
224X ≟ identifier RegisterTag
225
226list register ≡ list X.
227
228   
229definition hide_prf : ∀P : Prop.P → P ≝ λP,prf.prf.
230definition hide_Prop : Prop → Prop ≝ λP.P.
231
232interpretation "hide proof" 'hide p = (hide_prf ? p).
233interpretation "hide Prop" 'hide p = (hide_Prop p).
234
235(* discard all elements failing test, return first element succeeding it *)
236(* and the rest of the list, if any. *)
237let rec chop A (test : A → bool) (l : list A) on l : option (A × (list A)) ≝
238  match l with
239  [ nil ⇒ None ?
240  | cons x l' ⇒ if test x then return 〈x, l'〉 else chop A test l'
241  ].
242
243lemma chop_hit : ∀A,f,l,pr. chop A f l = Some ? pr →
244  let x ≝ \fst pr in
245  let post ≝ \snd pr in
246  ∃pre.All ? (λx.Not (bool_to_Prop (f x))) pre ∧ l = pre @ x :: post ∧ bool_to_Prop (f x).
247#A#f#l elim l
248[ normalize * #x #post #EQ destruct
249| #y #l' #Hi * #x #post
250  normalize elim (true_or_false_Prop (f y)) #fy >fy normalize
251  #EQ
252  [ destruct >fy %{[ ]} /3 by refl, conj, I/
253  | elim (Hi … EQ) #pre ** #prefalse #chopd #fx
254    %{(y :: pre)} %[%[%{fy prefalse}| >chopd %]|@fx]
255  ]
256]
257qed.
258
259lemma chop_miss : ∀A,f,l. chop A f l = None ? → All A (λx.Not (bool_to_Prop (f x))) l.
260#A#f#l elim l
261[ normalize #_ %
262| #y #l' #Hi normalize
263  elim (true_or_false_Prop (f y)) #fy >fy normalize
264  #EQ
265  [ destruct
266  | /3 by conj, nmk/
267  ]
268]
269qed.
270
271unification hint 0 ≔ p, globals;
272lp ≟ lin_params_to_params p,
273sp ≟ stmt_pars lp,
274js ≟ joint_statement sp globals,
275lo ≟ labelled_obj LabelTag js
276(*----------------------------*)⊢
277list lo ≡ codeT lp globals.
278
279
280definition graph_visit_ret_type ≝ λp,globals.λg : codeT (mk_graph_params p) globals.
281  λentry : label.
282  (Σ〈visited'   : identifier_map LabelTag ℕ,
283   required'  : identifier_set LabelTag,
284   generated' : codeT (mk_lin_params p) globals〉.'hide (
285      And (And (And (lookup ?? visited' entry = Some ? 0) (required' ⊆ visited'))
286        (code_forall_labels … (λl.bool_to_Prop (l∈required')) generated'))
287        (∀l,n.lookup ?? visited' l = Some ? n →
288          And (code_has_label … (rev ? generated') l)
289            (∃s.And (And
290              (lookup … g l = Some ? s)
291              (nth_opt … n (rev … generated') = Some ? 〈Some ? l, graph_to_lin_statement … s〉))
292              (opt_All ?
293                (λnext.Or (lookup … visited' next = Some ? (S n))
294                  (nth_opt … (S n) (rev … generated') = Some ? 〈None ?, GOTO … next〉))
295                (stmt_implicit_label … s)))))).
296               
297unification hint 0 ≔ tag ⊢ identifier_set tag ≡ identifier_map tag unit.
298
299let rec graph_visit
300  (p : unserialized_params)
301  (globals: list ident)
302  (g : codeT (mk_graph_params p) globals)
303  (* = graph (joint_statement (mk_graph_params p) globals *)
304  (required: identifier_set LabelTag)
305  (visited: identifier_map LabelTag ℕ) (* the reversed index of labels in the new code *)
306  (generated: codeT (mk_lin_params p) globals)
307  (* ≝ list ((option label)×(joint_statement (mk_lin_params p) globals)) *)
308  (visiting: list label)
309  (gen_length : ℕ)
310  (n: nat)
311  (entry : label)
312  (g_prf : code_closed … g)
313  (required_prf1 : ∀i.i∈required → Or (In ? visiting i) (bool_to_Prop (i ∈ visited)))
314  (required_prf2 : code_forall_labels … (λl.bool_to_Prop (l ∈ required)) generated)
315  (generated_prf1 : ∀l,n.lookup … visited l = Some ? n → hide_Prop (
316    And (code_has_label … (rev ? generated) l)
317    (∃s.And (And
318      (lookup … g l = Some ? s)
319      (nth_opt ? n (rev … generated) = Some ? 〈Some ? l, graph_to_lin_statement … s〉))
320      (opt_All ? (λnext.match lookup … visited next with
321                     [ Some n' ⇒ Or (n' = S n) (nth_opt ? (S n) (rev ? generated) = Some ? 〈None ?, GOTO … next〉)
322                     | None ⇒ And (nth_opt ? 0 visiting = Some ? next) (S n = gen_length) ]) (stmt_implicit_label … s)))))
323  (generated_prf2 : ∀l.lookup … visited l = None ? → does_not_occur … l (rev ? generated))
324  (visiting_prf : All … (λl.lookup … g l ≠ None ?) visiting)
325  (gen_length_prf : gen_length = length ? generated)
326  (entry_prf : Or (And (And (visiting = [entry]) (gen_length = 0)) (Not (bool_to_Prop (entry∈visited))))
327                  (lookup … visited entry = Some ? 0))
328  (n_prf : le (id_map_size … g) (plus n (id_map_size … visited)))
329  on n
330  : graph_visit_ret_type … g entry ≝
331  match chop ? (λx.¬x∈visited) visiting
332  return λx.chop ? (λx.¬x∈visited) visiting = x → graph_visit_ret_type … g entry with
333  [ None ⇒ λeq_chop.
334    let H ≝ chop_miss … eq_chop in
335    mk_Sig … 〈visited, required, generated〉 ?
336  | Some pr ⇒ λeq_chop.
337    let vis_hd ≝ \fst pr in
338    let vis_tl ≝ \snd pr in
339    let H ≝ chop_hit ???? eq_chop in
340    match n return λx.x = n → graph_visit_ret_type … g entry with
341    [ O ⇒ λeq_n.⊥
342    | S n' ⇒ λeq_n.
343      (* add the label to the visited ones *)
344      let visited' ≝ add … visited vis_hd gen_length in
345      (* take l's statement *)
346      let statement ≝ opt_safe … (lookup ?? g vis_hd) (hide_prf ? ?) in 
347      (* translate it to its linear version *)
348      let translated_statement ≝ graph_to_lin_statement p globals statement in
349      (* add the translated statement to the code (which will be reversed later) *)
350      let generated' ≝ 〈Some … vis_hd, translated_statement〉 :: generated in
351      let required' ≝ stmt_explicit_labels … statement ∪ required in
352      (* put successors in the visiting worklist *)
353      let visiting' ≝ stmt_labels … statement @ vis_tl in
354      (* finally, check the implicit successor *)
355      (* if it has been already visited, we need to add a GOTO *)
356      let add_req_gen ≝ match stmt_implicit_label … statement with
357        [ Some next ⇒
358          if next ∈ visited' then 〈1, {(next)}, [〈None label, GOTO … next〉]〉 else 〈0, ∅, [ ]〉
359        | None ⇒ 〈0, ∅, [ ]〉
360        ] in
361      graph_visit ???
362        (\snd (\fst add_req_gen) ∪ required')
363        visited'
364        (\snd add_req_gen @ generated')
365        visiting'
366        (\fst (\fst add_req_gen) + S(gen_length))
367        n' entry g_prf ????????
368    ] (refl …)
369  ] (refl …).
370whd
371[ (* base case, visiting is all visited *)
372  %[
373    %[
374      %[
375        elim entry_prf
376        [ ** #eq_visiting #gen_length_O #entry_vis >eq_visiting in H; * >entry_vis
377          * #ABS elim (ABS I)
378        | //
379        ]
380      | #l #l_req
381        elim (required_prf1 … l_req) #G
382        [ lapply (All_In … H G) #H >(notb_false ? H) %
383        | assumption
384        ]
385      ]
386    | assumption
387    ]
388   | #l #n #H elim (generated_prf1 … H)
389      #H1 * #s ** #H2 #H3 #H4
390      % [assumption] %{s} %
391      [% assumption
392      | @(opt_All_mp … H4) -l #l
393        lapply (in_map_domain … visited l)
394        elim (true_or_false (l∈visited)) #l_vis >l_vis
395        normalize nodelta [ * #n' ] #EQlookup >EQlookup
396        normalize nodelta *
397        [ #EQn' % >EQn' %
398        | #H %2{H}
399        | #H' lapply (All_nth … H … H') >l_vis * #ABS elim (ABS I)
400        ]
401      ]
402    ]
403|*: (* unpack H in all other cases *) elim H #pre ** #H1 #H2 #H3 ]
404(* first, close goals where add_gen_req plays no role *)
405[10: (* vis_hd is in g *) @(All_split … visiting_prf … H2)
406|1: (* n = 0 absrud *)
407  @(absurd … n_prf)
408  @lt_to_not_le
409  <eq_n
410  lapply (add_size … visited vis_hd 0 (* dummy value *))
411  >(notb_true … H3)
412  whd in match (if ? then ? else ?);
413  whd in match (? + ?);
414  whd in match (lt ? ?);
415  #EQ <EQ @subset_card @add_subset
416  [ @(All_split ? (λx.bool_to_Prop (x∈g)) ????? H2) @(All_mp … visiting_prf)
417    #a elim g #gm whd in ⊢ (?→?%); #H >(opt_to_opt_safe … H) %
418  | #l #H lapply (mem_map_domain … H) -H #H lapply(opt_to_opt_safe … H)
419    generalize in match (opt_safe ???); #n #l_is_n
420    elim (generated_prf1 … l_is_n) #_ * #s ** #s_in_g #_ #_ lapply s_in_g -s_in_g
421    elim g #mg  whd in ⊢ (?→?%); #H >H whd %
422  ]
423|6:
424  @All_append
425  [ @(g_prf … vis_hd) <opt_to_opt_safe %
426  | >H2 in visiting_prf;
427    #H' lapply (All_append_r … H') -H' * #_ //
428  ]
429|8:
430  %2 elim entry_prf
431  [ ** >H2 cases pre
432    [2: #x' #pre' #ABS normalize in ABS; destruct(ABS)
433      cases pre' in e0; [2: #x'' #pre''] #ABS' normalize in ABS'; destruct(ABS')
434    |1: #EQ normalize in EQ; destruct(EQ) #eq_gen_length #_
435      >lookup_add_hit >eq_gen_length %
436    ]
437  | #lookup_entry cut (entry ≠ vis_hd)
438    [ % whd in match vis_hd; #entry_vis_hd <entry_vis_hd in H3; #entry_vis
439      lapply (in_map_domain … visited entry) >(notb_true … entry_vis)
440      normalize nodelta >lookup_entry #ABS destruct(ABS)]
441    #entry_not_vis_hd >(lookup_add_miss ?????? entry_not_vis_hd) assumption
442  ]
443|9:
444  >commutative_plus
445  >add_size >(notb_true … H3) normalize nodelta
446  whd in match (? + ?);
447  >commutative_plus
448  change with (? ≤ S(?) + ?)
449  >eq_n assumption
450|*: (* where add_gen_req does matter, expand the three possible cases *)
451  lapply (refl … add_req_gen)
452  whd in ⊢ (???%→?);
453  lapply (refl … (stmt_implicit_label … statement))
454  (* BUG *)
455  [ generalize in match (stmt_implicit_label … statement) in ⊢ (???%→%);
456  | generalize in match (stmt_implicit_label … statement) in ⊢ (???%→%);
457  | generalize in match (stmt_implicit_label … statement) in ⊢ (???%→%);
458  | generalize in match (stmt_implicit_label … statement) in ⊢ (???%→%);
459  | generalize in match (stmt_implicit_label … statement) in ⊢ (???%→%);
460  ]
461  *[2,4,6,8,10: #next]
462  #EQimpl
463  whd in ⊢ (???%→?);
464  [1,2,3,4,5: elim (true_or_false_Prop … (next∈visited')) #next_vis >next_vis
465    whd in ⊢ (???%→?);]
466  #EQ_req_gen >EQ_req_gen
467  (* these are the cases, reordering them *)
468  [1,2,11: | 3,4,12: | 5,6,13: | 7,8,14: |9,10,15: ]
469  [1,2,3: #i >mem_set_union
470    [ #H elim (orb_Prop_true … H) -H
471      [ #H >(mem_set_singl_to_eq … H) %2{next_vis}]
472    |*: >mem_set_empty whd in match (false ∨ ?);
473    ]
474    >mem_set_union
475    #H elim(orb_Prop_true … H) -H
476    [1,3,5: (* i is an explicit successor *)
477      #i_succ
478      (* if it's visited it's ok *)
479      elim(true_or_false_Prop (i ∈visited')) #i_vis >i_vis
480      [1,3,5: %2 %
481      |*: %
482        @Exists_append_l
483        whd in match (stmt_labels ???);
484        @Exists_append_r
485        @mem_list_as_set
486        @i_succ
487      ]
488    |2,4,6: (* i was already required *)
489      #i_req
490      elim (required_prf1 … i_req)
491      [1,3,5: >H2 #H elim (Exists_append … H) -H
492        [1,3,5: (* i in preamble → i∈visited *)
493          #i_pre %2 >mem_set_add @orb_Prop_r
494          lapply (All_In … H1 i_pre)
495          #H >(notb_false … H) %
496        |*: *
497          [1,3,5: (* i is vis_hd *)
498            #eq_i >eq_i %2 @mem_set_add_id
499          |*: (* i in vis_tl → i∈visiting' *)
500            #i_post % @Exists_append_r assumption
501          ]
502        ]
503      |*: #i_vis %2 >mem_set_add @orb_Prop_r assumption
504      ]
505    ]
506  |4,5,6:
507    [% [ whd % [ >mem_set_union >mem_set_add_id % | %]]]
508    whd in match (? @ ?); %
509    [1,3,5:
510      whd
511      >graph_to_lin_labels
512      change with (All ?? (stmt_explicit_labels ?? statement))
513      whd in match required';
514      generalize in match (stmt_explicit_labels … statement);
515      #l @list_as_set_All
516      #i >mem_set_union >mem_set_union
517      #i_l @orb_Prop_r @orb_Prop_l @i_l
518    |*: @(All_mp … required_prf2)
519      * #l_opt #s @All_mp
520      #l #l_req >mem_set_union @orb_Prop_r
521      >mem_set_union @orb_Prop_r @l_req
522    ]
523  |7,8,9:
524    #i whd in match visited';
525    @(eq_identifier_elim … i vis_hd)
526    [1,3,5: #EQi >EQi #pos
527      >lookup_add_hit #EQpos cut (gen_length = pos)
528        [1,3,5: (* BUG: -graph_visit *) -visited destruct(EQpos) %]
529        -EQpos #EQpos <EQpos -pos
530      %
531      [1,3,5: whd in match (rev ? ?);
532        >rev_append_def
533        whd
534        [ change with (? @ ([?] @ [?])) in match (? @ [? ; ?]);
535          <associative_append >occurs_exactly_once_None]
536        >occurs_exactly_once_Some_eq >eq_identifier_refl
537        normalize nodelta
538        @generated_prf2
539        lapply (in_map_domain … visited vis_hd)
540        >(notb_true … H3) normalize nodelta //
541      |*: %{statement}
542        %
543        [1,3,5: %
544          [1,3,5:
545           change with (? = Some ? (opt_safe ???))
546           @opt_safe_elim #s //
547          |*: whd in match (rev ? ?);
548            >rev_append_def
549            [ change with (? @ ([?] @ [?])) in match (? @ [? ; ?]);
550              <associative_append @nth_opt_append_hit_l ]
551            >nth_opt_append_r
552            >rev_length
553            <gen_length_prf
554            [1,3,5: <minus_n_n] %
555          ]
556        |*: >EQimpl whd [3: %]
557          >mem_set_add in next_vis;
558          @eq_identifier_elim
559          [1,3: #EQnext >EQnext * [2: #ABS elim(ABS I)]
560            >lookup_add_hit
561          |*: #NEQ >(lookup_add_miss … visited … NEQ)
562            whd in match (false ∨ ?);
563            #next_vis lapply(in_map_domain … visited next) >next_vis
564            whd in ⊢ (% → ?); [ * #s ]
565            #EQlookup >EQlookup
566          ] whd
567          [1,2: %2
568            >rev_append >nth_opt_append_r
569            >rev_length whd in match generated';
570            whd in match (|? :: ?|); <gen_length_prf
571            [1,3: <minus_n_n ] %
572          |*: % [2: %] @nth_opt_append_hit_l whd in match (stmt_labels … statement);
573            >EQimpl %
574          ]
575        ]
576      ]
577    |*:
578      #NEQ #n_i >(lookup_add_miss … visited … NEQ)
579      #Hlookup elim (generated_prf1 … Hlookup)
580      #G1 * #s ** #G2 #G3 #G4
581      %
582      [1,3,5: whd in match (rev ??);
583        >rev_append_def whd
584        [ change with (? @ ([?] @ [?])) in match (? @ [? ; ?]);
585          <associative_append >occurs_exactly_once_None]
586        >occurs_exactly_once_Some_eq
587        >eq_identifier_false
588        [2,4,6: % #ABS >ABS in NEQ; * #ABS' @ABS' %]
589        normalize nodelta
590        assumption
591      |*: %{s}
592        %
593        [1,3,5: %
594          [1,3,5: assumption
595          |*: whd in match (rev ??); >rev_append_def
596            [ change with (? @ ([?] @ [?])) in match (? @ [? ; ?]);
597              <associative_append @nth_opt_append_hit_l ]
598            @nth_opt_append_hit_l assumption
599          ]
600        |*: @(opt_All_mp … G4)
601          #x
602          @(eq_identifier_elim … x vis_hd) #Heq
603          [1,3,5: >Heq
604            lapply (in_map_domain … visited vis_hd)
605            >(notb_true … H3)
606           normalize nodelta #EQlookup >EQlookup normalize nodelta
607           * #nth_opt_visiting #gen_length_eq
608           >lookup_add_hit normalize nodelta %
609           >gen_length_eq %
610          |*: >(lookup_add_miss ?????? Heq)
611            lapply (in_map_domain … visited x)
612            elim (true_or_false_Prop (x∈visited)) #x_vis >x_vis normalize nodelta
613            [1,3,5: * #n'] #EQlookupx >EQlookupx normalize nodelta *
614            [1,3,5: #G %{G}
615            |2,4,6: #G %2 whd in match (rev ??); >rev_append_def
616              [ change with (? @ ([?] @ [?])) in match (? @ [? ; ?]);
617              <associative_append @nth_opt_append_hit_l ]
618              @nth_opt_append_hit_l assumption
619            |*: #G elim(absurd ?? Heq)
620              (* BUG (but useless): -required -g -generated *)
621               >H2 in G; #G
622              lapply (refl … (nth_opt ? 0 pre))
623              (* BUG *)
624              [generalize in ⊢ (???%→?);
625              |generalize in ⊢ (???%→?);
626              |generalize in ⊢ (???%→?);
627              ] *
628              [1,3,5: #G' >(nth_opt_append_miss_l … G') in G;
629                change with (Some ? vis_hd = ? → ?)
630                #EQvis_hd' destruct(EQvis_hd') %
631              |*: #lbl'' #G' >(nth_opt_append_hit_l ? pre ??? G') in G;
632                #EQlbl'' destruct(EQlbl'') lapply (All_nth … H1 … G')
633                >x_vis * #ABS elim (ABS I)
634              ]
635            ]
636          ]
637        ]
638      ]
639    ]
640  |10,11,12:
641    #i whd in match visited';
642    lapply (in_map_domain … visited' i)
643    >mem_set_add
644    elim (true_or_false_Prop (eq_identifier … vis_hd i)) #i_vis_hd
645    >eq_identifier_sym >i_vis_hd
646    [2,4,6: elim(true_or_false (i∈visited)) #i_vis >i_vis]
647    [1,3,5,7,8,9: change with ((∃_.?) → ?); * #n #EQlook >EQlook #ABS destruct(ABS)]
648    #_ #EQlookup >lookup_add_miss in EQlookup;
649    [2,4,6: % #ABS >ABS in i_vis_hd; >eq_identifier_refl *]
650    #EQlookup
651    [1,2,3: @EQlookup %]
652    whd in match (rev ??); >rev_append_def
653    [ change with (? @ ([?] @ [?])) in match (? @ [? ; ?]);
654              <associative_append >does_not_occur_None]
655    >(does_not_occur_Some ?????? (i_vis_hd))
656    @generated_prf2 assumption
657  |13,14,15:
658    whd in match generated'; normalize <gen_length_prf %
659  ]
660]
661qed.
662
663(* CSC: The branch compression (aka tunneling) optimization is not implemented
664   in Matita *)
665definition branch_compress
666  ≝ λp: graph_params.λglobals.λg:codeT p globals.
667    λentry : Σl.code_has_label … g l.g.
668 
669lemma branch_compress_closed : ∀p,globals,g,l.code_closed ?? g →
670  code_closed … (branch_compress p globals g l).
671#p#globals#g#l#H @H qed.
672
673lemma branch_compress_has_entry : ∀p,globals,g,l.
674  code_has_label … (branch_compress p globals g l) l.
675#p#globals#g*#l#l_prf @l_prf qed.
676
677definition filter_labels ≝ λtag,A.λtest : identifier tag → bool.λc : list (labelled_obj tag A).
678  map ??
679    (λs. let 〈l_opt,x〉 ≝ s in
680      〈! l ← l_opt ; if test l then return l else None ?, x〉) c.
681     
682lemma does_not_occur_filter_labels :
683  ∀tag,A,test,id,c.
684    does_not_occur ?? id (filter_labels tag A test c) =
685      (does_not_occur ?? id c ∨ ¬ test id).
686#tag #A #test #id #c elim c
687[ //
688| ** [2: #lbl] #s #tl #IH
689  whd in match (filter_labels ????); normalize nodelta
690  whd in match (does_not_occur ????) in ⊢ (??%%);
691  [2: @IH]
692  normalize in match (! l ← ? ; ?); >IH
693  @(eq_identifier_elim ?? lbl id) #Heq [<Heq]
694  elim (test lbl) normalize nodelta
695  change with (eq_identifier ???) in match (instruction_matches_identifier ????);
696  [1,2: >eq_identifier_refl [2: >commutative_orb] normalize %
697  |*: >(eq_identifier_false ??? Heq) normalize nodelta %
698  ]
699]
700qed.
701
702lemma occurs_exactly_once_filter_labels :
703  ∀tag,A,test,id,c.
704    occurs_exactly_once ?? id (filter_labels tag A test c) =
705      (occurs_exactly_once ?? id c ∧ test id).
706#tag #A #test #id #c elim c
707[ //
708| ** [2: #lbl] #s #tl #IH
709  whd in match (filter_labels ????); normalize nodelta
710  whd in match (occurs_exactly_once ????) in ⊢ (??%%);
711  [2: @IH]
712  normalize in match (! l ← ? ; ?); >IH
713  >does_not_occur_filter_labels
714  @(eq_identifier_elim ?? lbl id) #Heq [<Heq]
715  elim (test lbl) normalize nodelta
716  change with (eq_identifier ???) in match (instruction_matches_identifier ????);
717  [1,2: >eq_identifier_refl >commutative_andb [ >(commutative_andb ? true) >commutative_orb | >(commutative_andb ? false)] normalize %
718  |*: >(eq_identifier_false ??? Heq) normalize nodelta %
719  ]
720]
721qed.
722
723lemma nth_opt_filter_labels : ∀tag,A,test,instrs,n.
724  nth_opt ? n (filter_labels tag A test instrs) =
725  ! 〈lopt, s〉 ← nth_opt ? n instrs ;
726  return 〈 ! lbl ← lopt; if test lbl then return lbl else None ?, s〉.
727#tag #A #test #instrs elim instrs
728[ * [2: #n'] %
729| * #lopt #s #tl #IH * [2: #n']
730  whd in match (filter_labels ????); normalize nodelta
731  whd in match (nth_opt ???) in ⊢ (??%%); [>IH] %
732]
733qed.
734
735definition linearize_code:
736 ∀p : unserialized_params.∀globals.
737  ∀g : codeT (mk_graph_params p) globals.code_closed … g →
738  ∀entry : (Σl. code_has_label … g l).
739    (Σc : codeT (mk_lin_params p) globals.
740      code_closed … c ∧
741      ∃ sigma : identifier_map LabelTag ℕ.
742      lookup … sigma entry = Some ? 0 ∧
743      ∀l,n.lookup … sigma l = Some ? n →
744        ∃s. lookup … g l = Some ? s ∧
745          opt_Exists ?
746            (λls.let 〈lopt, ts〉 ≝ ls in
747              opt_All ? (eq ? l) lopt ∧
748              ts = graph_to_lin_statement … s ∧
749              opt_All ?
750                (λnext.Or (lookup … sigma next = Some ? (S n))
751                (nth_opt … (S n) c = Some ? 〈None ?, GOTO … next〉))
752                (stmt_implicit_label … s)) (nth_opt … n c))
753
754 λp,globals,g,g_prf,entry_sig.
755    let g ≝ branch_compress (mk_graph_params p) ? g entry_sig in
756    let g_prf ≝ branch_compress_closed … g entry_sig g_prf in
757    let entry_sig' ≝ mk_Sig ?? entry_sig (branch_compress_has_entry … g entry_sig) in
758    match graph_visit p globals g ∅ (empty_map …) [ ] [entry_sig] 0 (|g|)
759      (entry_sig) g_prf ????????
760    with
761    [ mk_Sig triple H ⇒
762      let sigma ≝ \fst (\fst triple) in
763      let required ≝ \snd (\fst triple) in
764      let crev ≝ \snd triple in
765      let lbld_code ≝ rev ? crev in
766      mk_Sig ?? (filter_labels … (λl.l∈required) lbld_code) ? ].
767[ (* done later *)
768| #i >mem_set_empty *
769| %
770|#l #n normalize in ⊢ (%→?); #ABS destruct(ABS)
771| #l #_ %
772| % [2: %] @(pi2 … entry_sig')
773| %
774| % % [% %] cases (pi1 … entry_sig) normalize #_ % //
775| >commutative_plus change with (? ≤ |g|) %
776]
777lapply (refl … triple)
778generalize in match triple in ⊢ (???%→%); **
779#visited #required #generated #EQtriple
780>EQtriple in H ⊢ %; normalize nodelta ***
781#entry_O #req_vis #labels_in_req #sigma_prop
782% >EQtriple
783[ (* code closed *)
784  @All_map
785  [2: @All_rev
786    @(All_mp … labels_in_req) #ls #H @H
787  |1: (* side-effect close *)
788  |3: * #lopt #s @All_mp
789    #lbl #lbl_req whd in match (code_has_label ????);
790    >occurs_exactly_once_filter_labels
791    @andb_Prop [2: assumption]
792    lapply (in_map_domain … visited lbl)
793    >(req_vis … lbl_req) * #n #eq_lookup
794    elim (sigma_prop ?? eq_lookup) #H #_ @H
795  ]
796]
797%{visited} % [assumption]
798#lbl #n #eq_lookup elim (sigma_prop ?? eq_lookup)
799#lbl_in_gen * #stmt ** #stmt_in_g #nth_opt_is_stmt #succ_is_in
800% [2: % [ assumption ] |]
801>nth_opt_filter_labels in ⊢ (???%);
802>nth_opt_is_stmt
803whd in match (! 〈lopt, s〉 ← Some ??; ?);
804whd
805whd in match (! lbl0 ← Some ??; ?);
806% [ % [ elim (lbl ∈ required) ] % ]
807whd
808lapply (refl … (stmt_implicit_label … stmt))
809generalize in match (stmt_implicit_label … stmt) in ⊢ (???%→%); * [2: #next]
810#eq_impl_lbl normalize nodelta [2: %]
811>eq_impl_lbl in succ_is_in; whd in match (opt_All ???); * #H
812[ %{H}
813| %2 >nth_opt_filter_labels >H
814  whd in match (! 〈lopt, s〉 ← ?; ?);
815  whd in match (! lbl0 ← ?; ?);
816  %
817]
818qed.
819
820definition graph_linearize :
821  ∀p : unserialized_params.
822  ∀globals. ∀fin : joint_closed_internal_function globals (mk_graph_params p).
823    Σfout : joint_closed_internal_function globals (mk_lin_params p).
824      ∃sigma : identifier_map LabelTag ℕ.
825        let g ≝ joint_if_code ?? (pi1 … fin) in
826        let c ≝ joint_if_code ?? (pi1 … fout) in
827        let entry ≝ joint_if_entry ?? (pi1 … fin) in
828         lookup … sigma entry = Some ? 0 ∧
829          ∀l,n.lookup … sigma l = Some ? n →
830            ∃s. lookup … g l = Some ? s ∧
831              opt_Exists ?
832                (λls.let 〈lopt, ts〉 ≝ ls in
833                  opt_All ? (eq ? l) lopt ∧
834                  ts = graph_to_lin_statement … s ∧
835                  opt_All ?
836                    (λnext.Or (lookup … sigma next = Some ? (S n))
837                    (nth_opt … (S n) c = Some ? 〈None ?, GOTO … next〉))
838                    (stmt_implicit_label … s)) (nth_opt … n c) ≝
839  λp,globals,f_sig.
840  mk_Sig ?? (match f_sig with
841  [ mk_Sig f f_prf ⇒ 
842  mk_joint_internal_function globals (mk_lin_params p)
843   (joint_if_luniverse ?? f) (joint_if_runiverse ?? f)
844   (joint_if_result ?? f) (joint_if_params ?? f) (joint_if_locals ?? f)
845   (joint_if_stacksize ?? f)
846   (linearize_code p globals (joint_if_code … f) f_prf (joint_if_entry … f))
847   (mk_Sig ?? it I) (mk_Sig ?? it I)
848  ]) ?.
849elim f_sig
850normalize nodelta #f_in #f_in_prf
851elim (linearize_code ?????)
852#f_out * #f_out_closed #H assumption
853qed.
854*) 
855
856     
857(*
858let rec add_translates
859  (pars1: params1) (globals: list ident)
860  (translate_list: list ?) (start_lbl: label) (dest_lbl: label)
861  (def: joint_internal_function … (graph_params pars1 globals))
862    on translate_list ≝
863  match translate_list with
864  [ nil ⇒ add_graph … start_lbl (GOTO … dest_lbl) def
865  | cons trans translate_list ⇒
866    match translate_list with
867    [ nil ⇒ trans start_lbl dest_lbl def
868    | _ ⇒
869      let 〈tmp_lbl, def〉 ≝ fresh_label … def in
870      let def ≝ trans start_lbl tmp_lbl def in
871        add_translates pars1 globals translate_list tmp_lbl dest_lbl def]].
872
873definition adds_graph ≝
874 λpars1:params1.λglobals. λstmt_list: list (label → joint_statement (graph_params_ pars1) globals).
875  add_translates … (map ?? (λf,start_lbl,dest_lbl. add_graph pars1 ? start_lbl (f dest_lbl)) stmt_list).
876  *)
Note: See TracBrowser for help on using the repository browser.