source: src/joint/TranslateUtils_paolo.ma @ 2125

Last change on this file since 2125 was 1882, checked in by tranquil, 8 years ago

big update, alas incomplete:
joint changed a bit, and all BE languages need to be updated
started development of blocks to aid preservation results, but still incomplete
if it breaks too many things, feel free to roll back

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