source: src/joint/TranslateUtils_paolo.ma @ 2155

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

updates to blocks and RTLabs to RTL translation (which sidesteps pointer arithmetics issues for now)

Joint semantics and traces momentarily broken, concentrating on syntax now

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