source: src/joint/linearise.ma @ 2182

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

updated linearisation pass

File size: 25.2 KB
Line 
1include "joint/TranslateUtils_paolo.ma".
2
3definition graph_to_lin_statement :
4  ∀p : unserialized_params.∀globals.
5  joint_statement (mk_graph_params p) globals → joint_statement (mk_lin_params p) globals ≝
6  λp,globals,stmt.match stmt return λ_.joint_statement (mk_lin_params ?) ? with
7  [ sequential c _ ⇒ sequential … c it
8  | final c ⇒ final … c
9  ].
10
11lemma graph_to_lin_labels :
12  ∀p : unserialized_params.∀globals,s.
13  stmt_labels … (graph_to_lin_statement p globals s) =
14  stmt_explicit_labels … s.
15#p#globals * [//] * //
16qed.
17
18definition hide_prf : ∀P : Prop.P → P ≝ λP,prf.prf.
19definition hide_Prop : Prop → Prop ≝ λP.P.
20
21interpretation "hide proof" 'hide p = (hide_prf ? p).
22interpretation "hide Prop" 'hide p = (hide_Prop p).
23
24(* discard all elements passing test, return first element failing it *)
25(* and the rest of the list, if any. *)
26let rec chop A (test : A → bool) (l : list A) on l : option (A × (list A)) ≝
27  match l with
28  [ nil ⇒ None ?
29  | cons x l' ⇒ if test x then chop A test l' else return 〈x, l'〉
30  ].
31
32lemma chop_ok : ∀A,f,l.
33  match chop A f l with
34  [ Some pr ⇒
35    let x ≝ \fst pr in
36    let post ≝ \snd pr in
37    ∃pre.All ? (λx.bool_to_Prop (f x)) pre ∧
38    l = pre @ x :: post ∧ ¬bool_to_Prop (f x)
39  | None ⇒ All A (λx.bool_to_Prop (f x)) l
40  ].
41#A #f #l elim l
42[ %
43| #hd #tl #IH whd in match (chop ???);
44  elim (true_or_false_Prop (f hd)) #H >H normalize nodelta
45  [ lapply IH elim (chop ???) normalize nodelta
46    [ #G %{H G}
47    | #pr * #pre ** #H1 #H2 #H3 %{(hd :: pre)} %{H3} %
48      [ %{H H1}
49      | >H2 %
50      ]
51    ]
52  | %{[ ]} %{H} %%
53  ]
54]
55qed.
56 
57unification hint 0 ≔ p, globals;
58lp ≟ lin_params_to_params p,
59sp ≟ stmt_pars lp,
60js ≟ joint_statement sp globals,
61lo ≟ labelled_obj LabelTag js
62(*----------------------------*)⊢
63list lo ≡ codeT lp globals.
64
65
66definition graph_visit_ret_type ≝ λp,globals.λg : codeT (mk_graph_params p) globals.
67  λentry : label.
68  (Σ〈visited'   : identifier_map LabelTag ℕ,
69   required'  : identifier_set LabelTag,
70   generated' : codeT (mk_lin_params p) globals〉.'hide (
71      And (And (And (And
72        (lookup ?? visited' entry = Some ? 0)
73        (required' ⊆ visited'))
74        (∃last.stmt_at … generated' 0 = Some ? (final … last)))
75        (code_forall_labels … (λl.bool_to_Prop (l∈required')) (rev … generated')))
76        (∀l,n.lookup ?? visited' l = Some ? n →
77          And (bool_to_Prop (code_has_label … (rev ? generated') l))
78            (∃s.And (And
79              (lookup … g l = Some ? s)
80              (nth_opt … n (rev … generated') = Some ? 〈Some ? l, graph_to_lin_statement … s〉))
81              (opt_All ?
82                (λnext.Or (lookup … visited' next = Some ? (S n))
83                  (nth_opt … (S n) (rev … generated') = Some ? 〈None ?, GOTO … next〉))
84                (stmt_implicit_label … s)))))).
85               
86unification hint 0 ≔ tag ⊢ identifier_set tag ≡ identifier_map tag unit.
87
88include alias "common/Identifiers.ma".
89
90lemma lookup_safe_elim : ∀tag,A.∀P : A → Prop.∀m,i,prf.
91  (∀x.lookup tag A m i = Some ? x → P x) → P (lookup_safe tag A m i prf).
92#tag #A #P #m #i #prf #H @H @lookup_eq_safe qed.
93
94let rec graph_visit
95  (p : unserialized_params)
96  (globals: list ident)
97  (g : codeT (mk_graph_params p) globals)
98  (* = graph (joint_statement (mk_graph_params p) globals *)
99  (required: identifier_set LabelTag)
100  (visited: identifier_map LabelTag ℕ) (* the reversed index of labels in the new code *)
101  (generated: codeT (mk_lin_params p) globals)
102  (* ≝ list ((option label)×(joint_statement (mk_lin_params p) globals)) *)
103  (visiting: list label)
104  (gen_length : ℕ)
105  (n: nat)
106  (entry : label)
107  (g_prf : code_closed … g)
108  (required_prf1 : ∀i.i∈required → Or (In ? visiting i) (bool_to_Prop (i∈visited)))
109  (required_prf2 : code_forall_labels … (λl.bool_to_Prop (l ∈ required)) (rev … generated))
110  (generated_prf1 : ∀l,n.lookup … visited l = Some ? n → hide_Prop (
111    And (bool_to_Prop (code_has_label … (rev ? generated) l))
112    (∃s.And (And
113      (lookup … g l = Some ? s)
114      (nth_opt ? n (rev … generated) = Some ? 〈Some ? l, graph_to_lin_statement … s〉))
115      (opt_All ? (λnext.match lookup … visited next with
116                     [ Some n' ⇒ Or (n' = S n) (nth_opt ? (S n) (rev ? generated) = Some ? 〈None ?, GOTO … next〉)
117                     | None ⇒ And (nth_opt ? 0 visiting = Some ? next) (S n = gen_length) ]) (stmt_implicit_label … s)))))
118  (generated_prf2 : ∀l.lookup … visited l = None ? → does_not_occur … l (rev ? generated))
119  (generated_prf3 : (∃last.stmt_at … generated 0 = Some ? (final … last)) ∨
120     (¬All ? (λx.bool_to_Prop (x∈visited)) visiting))
121  (visiting_prf : All … (λl.bool_to_Prop (l∈g)) visiting)
122  (gen_length_prf : gen_length = length ? generated)
123  (entry_prf : Or (And (And (visiting = [entry]) (gen_length = 0)) (Not (bool_to_Prop (entry∈visited))))
124                  (lookup … visited entry = Some ? 0))
125  (n_prf : le (id_map_size … g) (plus n (id_map_size … visited)))
126  on n
127  : graph_visit_ret_type … g entry ≝
128  match chop ? (λx.x∈visited) visiting
129  return λx.? → graph_visit_ret_type … g entry with
130  [ None ⇒ λH.
131    «〈visited, required, generated〉, ?»
132  | Some pr ⇒ λH.
133    let vis_hd ≝ \fst pr in
134    let vis_tl ≝ \snd pr in
135    match n return λx.? → graph_visit_ret_type … g entry with
136    [ O ⇒ λn_prf'.⊥
137    | S n' ⇒ λn_prf'.
138      (* add the label to the visited ones *)
139      let visited' ≝ add … visited vis_hd gen_length in
140      (* take l's statement *)
141      let hd_vis_in_g ≝ (hide_prf ? ?) in
142      let statement ≝ lookup_safe ?? g vis_hd hd_vis_in_g in 
143      (* translate it to its linear version *)
144      let translated_statement ≝ graph_to_lin_statement p globals statement in
145      (* add the translated statement to the code (which will be reversed later) *)
146      let generated' ≝ 〈Some … vis_hd, translated_statement〉 :: generated in
147      let required' ≝ union_set ??? (set_from_list … (stmt_explicit_labels … statement)) required in
148      (* put successors in the visiting worklist *)
149      let visiting' ≝ stmt_labels … statement @ vis_tl in
150      (* finally, check the implicit successor *)
151      (* if it has been already visited, we need to add a GOTO *)
152      let add_req_gen ≝
153        match stmt_implicit_label … statement
154        with
155        [ Some next ⇒
156          if next ∈ visited' then
157            〈1, {(next)}, [〈None label, (GOTO … next : joint_statement ??)〉]〉
158          else 〈0, ∅, [ ]〉
159        | None ⇒ 〈0, ∅, [ ]〉
160        ] in
161      (* prepare a common utility to deal with add_req_gen *)
162      let add_req_gen_prf :
163        ∀P : (ℕ × (identifier_set LabelTag) × (codeT (mk_lin_params p) globals)) → Prop.
164        (opt_All ? (λnext.¬bool_to_Prop (next ∈ visited')) (stmt_implicit_label … statement) →
165         P 〈0,∅,[ ]〉) →
166        (∀next.stmt_implicit_label … statement = Some ? next →
167          next ∈ visited' →
168          P 〈1, {(next)}, [〈None ?, GOTO (mk_lin_params p) next〉]〉) →
169        P add_req_gen ≝ hide_prf ?? in
170      graph_visit ???
171        (union_set ??? (\snd (\fst add_req_gen)) required')
172        visited'
173        (\snd add_req_gen @ generated')
174        visiting'
175        (plus (\fst (\fst add_req_gen)) (S gen_length))
176        n' entry g_prf ?????????
177    ] n_prf
178  ] (chop_ok ? (λx.x∈visited) visiting).
179whd
180[ (* base case, visiting is all visited *)
181  %[%[%[%]]]
182  [ elim entry_prf
183    [ ** #eq_visiting #gen_length_O #entry_vis >eq_visiting in H; * >entry_vis *
184    | //
185    ]
186  | #l #l_req
187    elim (required_prf1 … l_req) #G
188    [ @(All_In … H G)
189    | assumption
190    ]
191  | cases generated_prf3 [//]
192    * #ABS @⊥ @ABS assumption
193  | assumption
194  | #l #n #H elim (generated_prf1 … H)
195    #H1 * #s ** #H2 #H3 #H4
196    % [assumption] %{s} %
197    [% assumption
198    | @(opt_All_mp … H4) -l #l
199      lapply (in_map_domain … visited l)
200      elim (true_or_false_Prop (l∈visited)) #l_vis >l_vis
201      normalize nodelta [ * #n' ] #EQlookup >EQlookup
202      normalize nodelta *
203      [ #EQn' % >EQn' %
204      | #H %2{H}
205      | #H' lapply (All_nth … H … H') >l_vis *
206      ]
207    ]
208  ]
209(* first, close goals where add_gen_req plays no role *)
210|13: (* vis_hd is in g *)
211  elim H #pre ** #_ #H2 #_
212  @(All_split … visiting_prf … H2)
213|2: (* n = 0 absrud *)
214  elim H #pre ** #_ #H2 #H3
215  @(absurd … n_prf')
216  @lt_to_not_le
217  lapply (add_size … visited vis_hd 0 (* dummy value *))
218  >H3 normalize nodelta
219  whd in match (lt ? ?);
220  whd in match (1 + ?);
221  #EQ <EQ @subset_card @add_subset
222  [ @(All_split ? (λx.bool_to_Prop (x∈g)) ????? H2) @(All_mp … visiting_prf)
223    #a elim g #gm whd in ⊢ (?→?%); #H >(lookup_eq_safe … H) %
224  | #l #H
225    elim (generated_prf1 … (lookup_eq_safe … H)) #_ * #s ** #s_in_g #_ #_
226    whd in ⊢ (?%); >s_in_g %
227  ]
228|8:
229  elim H #pre ** #_ #H2 #_
230  @All_append
231  [ elim(g_prf … vis_hd statement ?) [2:@lookup_eq_safe] #G1 #G2
232    @(All_append … G1)
233    whd in G2; lapply G2 elim statement normalize nodelta #s [2: #_ %]
234    #l #G' %{G'} %
235  | >H2 in visiting_prf;
236    #H' lapply (All_append_r … H') -H' * #_ //
237  ]
238|10:
239  elim H #pre ** #_ #H2 #H3 -add_req_gen_prf
240  %2 elim entry_prf
241  [ ** >H2 cases pre
242    [2: #x' #pre' #ABS normalize in ABS; destruct(ABS)
243      cases pre' in e0; [2: #x'' #pre''] #ABS' normalize in ABS'; destruct(ABS')
244    |1: #EQ normalize in EQ; destruct(EQ)
245      #eq_gen_length #_
246      >lookup_add_hit >eq_gen_length %
247    ]
248  | #lookup_entry cut (entry ≠ vis_hd)
249    [ % whd in match vis_hd; #entry_vis_hd <entry_vis_hd in H3;
250      whd in ⊢ (?(?%)→?); >lookup_entry * #ABS @ABS % ]
251    #entry_not_vis_hd >(lookup_add_miss ?????? entry_not_vis_hd) assumption
252  ]
253|11:
254  elim H #pre ** #_ #_ #H3
255  >commutative_plus
256  >add_size >H3 normalize nodelta
257  whd in match (1 + ?);
258  >commutative_plus
259  assumption
260|12: (* add_req_gen utility *)
261  #P whd in match add_req_gen;
262  elim (stmt_implicit_label ???)
263  [ #H #_ @H % ]
264  #next normalize nodelta elim (true_or_false_Prop (next ∈ visited')) #next_vis
265  >next_vis normalize nodelta
266  [ #_ #H @H [% | assumption]
267  | #H #_ @H whd >next_vis % *
268  ]
269| elim H #pre ** #H1 #H2 #_
270  #i >mem_set_union
271  #H elim (orb_Prop_true … H) -H
272  [ @add_req_gen_prf [ #_ >mem_set_empty * ]
273    #next #_ #next_vis #H >(mem_set_singl_to_eq … H) %2 assumption
274  | >mem_set_union
275    #H elim (orb_Prop_true … H) -H
276    [ #i_expl %1 @Exists_append_l @Exists_append_r
277      @mem_list_as_set
278      @i_expl
279    | (* i was already required *)
280      #i_req
281      elim (required_prf1 … i_req)
282      [ >H2 #H elim (Exists_append … H) -H
283        [ (* i in preamble → i∈visited *)
284          #i_pre %2 >mem_set_add @orb_Prop_r
285          lapply (All_In … H1 i_pre) #H @H
286        | *
287          [ (* i is vis_hd *)
288            #eq_i >eq_i %2 @mem_set_add_id
289          | (* i in vis_tl → i∈visiting' *)
290            #i_post % @Exists_append_r assumption
291          ]
292        ]
293      | (* i in visited *)
294        #i_vis %2 >mem_set_add @orb_Prop_r assumption
295      ]
296    ]
297  ]
298|4,5,6: change with reverse in match rev;
299  >reverse_append whd in match (reverse ??); >rev_append_def
300  >associative_append
301  [ #pt #s
302    @(leb_elim (S pt) (|generated|)) #cmp
303    whd in match (stmt_at ????);
304    [ >nth_opt_append_l [2: >length_reverse assumption ]
305      change with (stmt_at ???? = ? → ?)
306      #EQ lapply(required_prf2 … EQ) @All_mp
307      #l #l_req >mem_set_union @orb_Prop_r
308      >mem_set_union @orb_Prop_r @l_req
309    | >nth_opt_append_r [2: >length_reverse @not_lt_to_le assumption ]
310      cases (pt - ?)
311      [ whd in match (nth_opt ???); whd in ⊢ (??%?→?);
312        #EQ destruct(EQ) whd
313        >graph_to_lin_labels in ⊢ (???%);
314        whd in match required';
315        generalize in match (stmt_explicit_labels … statement);
316        #l @list_as_set_All
317        #i >mem_set_union >mem_set_union
318        #i_l @orb_Prop_r @orb_Prop_l @i_l
319      | @add_req_gen_prf
320        [ #_ | #next #_ #next_vis *
321          [ whd in ⊢ (??%?→?);
322            #EQ' destruct(EQ') whd %{I} >mem_set_union
323            @orb_Prop_l @mem_set_add_id ]]
324        #n whd in ⊢ (??%?→?); #ABS destruct(ABS)
325      ]
326    ]
327  | elim H #pre ** #H1 #H2 #H3
328    #i whd in match visited';
329    @(eq_identifier_elim … i vis_hd)
330    [ #EQi >EQi -i #pos
331      >lookup_add_hit #EQpos (* too slow: destruct(EQpos) *)
332      cut (gen_length = pos)
333      [1,3,5: (* BUG: -graph_visit *) -visited destruct(EQpos) %]
334      -EQpos #EQpos <EQpos -pos
335      %
336      [ >lin_code_has_label
337        @add_req_gen_prf
338        [ #_
339        | #next #_ #next_vis
340          change with (? @ ([?] @ [?])) in match (? @ [? ; ?]);
341          <associative_append >occurs_exactly_once_None
342        ]
343        >occurs_exactly_once_Some_eq >eq_identifier_refl
344        normalize nodelta
345        @generated_prf2
346        lapply (in_map_domain … visited vis_hd)
347        >H3 normalize nodelta //
348      | %{statement}
349        % [ % ]
350        [ @lookup_eq_safe
351        | <associative_append @nth_opt_append_hit_l
352          >nth_opt_append_r
353          >rev_length
354          <gen_length_prf
355          [<minus_n_n] %
356        | @add_req_gen_prf
357          [ lapply (refl … (stmt_implicit_label ?? statement))
358            cases (stmt_implicit_label ???) in ⊢ (???%→%);
359            [#_ #_ %]
360            #next #K change with (¬bool_to_Prop (?∈?)→?) #next_vis
361          | #next #K >K #next_vis
362          ] whd
363          >mem_set_add in next_vis;
364          @eq_identifier_elim
365          [1,3: #EQnext >EQnext * [#ABS elim(ABS I)]
366            >lookup_add_hit
367          |*: #NEQ >(lookup_add_miss … visited … NEQ)
368            change with (?∈?) in match (false∨?);
369            #next_vis lapply(in_map_domain … visited next) >next_vis
370            whd in ⊢ (% → ?); [2: * #s ]
371            #EQlookup >EQlookup
372          ] whd
373          [1,2: %2 <associative_append
374            >nth_opt_append_r >append_length >rev_length >commutative_plus
375            <gen_length_prf
376            [1,3: <minus_n_n ] %
377          | % [2: %] @nth_opt_append_hit_l whd in match (stmt_labels … statement);
378            >K %
379          ]
380        ]
381      ]
382    | #NEQ #n_i >(lookup_add_miss … visited … NEQ)
383      #Hlookup elim (generated_prf1 … Hlookup)
384      #G1 * #s ** #G2 #G3 #G4
385      %
386      [ >lin_code_has_label <associative_append
387        >occurs_exactly_once_append
388        @orb_Prop_l @andb_Prop
389        [ >occurs_exactly_once_Some_eq
390          >eq_identifier_false [2: % #ABS >ABS in NEQ; * #ABS' @ABS' % ]
391          normalize nodelta >lin_code_has_label in G1; #K @K
392        | @add_req_gen_prf
393          [ #_ % | #next #_ #_ % ]
394        ]
395      | %{s}
396        % [ % ]
397        [ assumption
398        | @nth_opt_append_hit_l assumption
399        | @(opt_All_mp … G4)
400          #x
401          @(eq_identifier_elim … x vis_hd) #Heq
402          [ >Heq
403            lapply (in_map_domain … visited vis_hd)
404            >H3 normalize nodelta in ⊢ (%→?);
405            #EQlookup >EQlookup * #nth_opt_visiting #gen_length_eq
406            >lookup_add_hit %1 >gen_length_eq %
407          | >(lookup_add_miss ?????? Heq)
408            lapply (in_map_domain … visited x)
409            elim (true_or_false_Prop (x∈visited)) #x_vis >x_vis
410            normalize nodelta in ⊢ (%→?); [ * #n' ]
411            #EQlookupx >EQlookupx whd in ⊢ (%→%); *
412            [ #G %1{G}
413            | #G %2 @nth_opt_append_hit_l
414              assumption
415            | #G elim(absurd ?? Heq)
416              (* BUG (but useless): -required -g -generated *)
417              >H2 in G; lapply H1 cases pre
418              [ #_
419              | #hd #tl * #hd_vis #_
420              ] normalize #EQ' destruct(EQ')
421              [ %
422              | >x_vis in hd_vis; *
423              ]
424            ]
425          ]
426        ]
427      ]
428    ]
429  | #i whd in match visited';
430    @(eq_identifier_elim … i vis_hd) #Heq
431    [ >Heq >lookup_add_hit #ABS destruct(ABS) ]
432    >(lookup_add_miss ?????? Heq)
433    #i_n_vis
434    >does_not_occur_append @andb_Prop
435    [ @generated_prf2 assumption
436    | change with (bool_to_Prop (¬eq_identifier ??? ∧ ?))
437      >eq_identifier_false [2: % #ABS <ABS in Heq; * #ABS' @ABS' % ]
438      @add_req_gen_prf [ #_ | #next #_ #_ ] %
439    ]
440  ]
441| @add_req_gen_prf
442  [ #K | #next #K #next_vis %1 %{(GOTO … next)} % ]
443  whd in match generated'; whd in match translated_statement;
444  lapply K whd in match visiting';
445  whd in match (stmt_labels ???); cases statement #last
446  [2: #_ %1 %{last} % ] #next whd in ⊢ (%→?); #next_vis
447  %2 % * >next_vis *
448| whd in match generated';
449  @add_req_gen_prf [ #_ | #next #_ #_ ] normalize >gen_length_prf %
450]
451qed.
452
453(* CSC: The branch compression (aka tunneling) optimization is not implemented
454   in Matita *)
455definition branch_compress
456  ≝ λp: graph_params.λglobals.λg:codeT p globals.
457    λentry : Σl.bool_to_Prop (code_has_label … g l).g.
458 
459lemma branch_compress_closed : ∀p,globals,g,l.code_closed ?? g →
460  code_closed … (branch_compress p globals g l).
461#p#globals#g#l#H @H qed.
462
463lemma branch_compress_has_entry : ∀p,globals,g,l.
464  code_has_label … (branch_compress p globals g l) l.
465#p#globals#g*#l#l_prf @l_prf qed.
466
467definition filter_labels ≝ λtag,A.λtest : identifier tag → bool.λc : list (labelled_obj tag A).
468  map ??
469    (λs. let 〈l_opt,x〉 ≝ s in
470      〈! l ← l_opt ; if test l then return l else None ?, x〉) c.
471     
472lemma does_not_occur_filter_labels :
473  ∀tag,A,test,id,c.
474    does_not_occur ?? id (filter_labels tag A test c) =
475      (does_not_occur ?? id c ∨ ¬ test id).
476#tag #A #test #id #c elim c
477[ //
478| ** [2: #lbl] #s #tl #IH
479  whd in match (filter_labels ????); normalize nodelta
480  whd in match (does_not_occur ????) in ⊢ (??%%);
481  [2: @IH]
482  normalize in match (! l ← ? ; ?); >IH
483  @(eq_identifier_elim ?? lbl id) #Heq [<Heq]
484  elim (test lbl) normalize nodelta
485  change with (eq_identifier ???) in match (instruction_matches_identifier ????);
486  [1,2: >eq_identifier_refl [2: >commutative_orb] normalize %
487  |*: >(eq_identifier_false ??? Heq) normalize nodelta %
488  ]
489]
490qed.
491
492lemma occurs_exactly_once_filter_labels :
493  ∀tag,A,test,id,c.
494    occurs_exactly_once ?? id (filter_labels tag A test c) =
495      (occurs_exactly_once ?? id c ∧ test id).
496#tag #A #test #id #c elim c
497[ //
498| ** [2: #lbl] #s #tl #IH
499  whd in match (filter_labels ????); normalize nodelta
500  whd in match (occurs_exactly_once ????) in ⊢ (??%%);
501  [2: @IH]
502  normalize in match (! l ← ? ; ?); >IH
503  >does_not_occur_filter_labels
504  @(eq_identifier_elim ?? lbl id) #Heq [<Heq]
505  elim (test lbl) normalize nodelta
506  change with (eq_identifier ???) in match (instruction_matches_identifier ????);
507  [1,2: >eq_identifier_refl >commutative_andb [ >(commutative_andb ? true) >commutative_orb | >(commutative_andb ? false)] normalize %
508  |*: >(eq_identifier_false ??? Heq) normalize nodelta %
509  ]
510]
511qed.
512
513lemma nth_opt_filter_labels : ∀tag,A,test,instrs,n.
514  nth_opt ? n (filter_labels tag A test instrs) =
515  ! 〈lopt, s〉 ← nth_opt ? n instrs ;
516  return 〈 ! lbl ← lopt; if test lbl then return lbl else None ?, s〉.
517#tag #A #test #instrs elim instrs
518[ * [2: #n'] %
519| * #lopt #s #tl #IH * [2: #n']
520  whd in match (filter_labels ????); normalize nodelta
521  whd in match (nth_opt ???) in ⊢ (??%%); [>IH] %
522]
523qed.
524
525lemma stmt_at_filter_labels : ∀p : lin_params.∀globals,test.∀c : codeT p globals.
526∀i.stmt_at p globals (filter_labels ?? test c) i = stmt_at p globals c i.
527#p#globals#test #c#i
528whd in ⊢ (??%%); >nth_opt_filter_labels
529elim (nth_opt ???); //
530qed.
531
532lemma option_bind_inverse : ∀A,B.∀m : option A.∀f : A → option B.∀r.
533  ! x ← m ; f x = return r →
534  ∃x.m = return x ∧ f x = return r.
535#A #B * normalize [2:#x] #f #r #EQ destruct
536%{x} %{EQ} %
537qed.
538
539lemma nth_opt_reverse_hit :
540  ∀A,l,n.n < |l| → nth_opt A n (reverse ? l) = nth_opt A (|l| - (S n)) l.
541#A #l elim l
542[ #n #ABS normalize in ABS; @⊥ -A /2 by absurd/
543| #hd #tl #IH #n #lim whd in match (reverse ??); >rev_append_def
544  @(leb_elim (S n) (|tl|)) #H
545  [ >nth_opt_append_l [2: >length_reverse @H ]
546    >(IH … H) >(minus_Sn_m … H) %
547  | >(le_to_le_to_eq … (le_S_S_to_le … lim) (not_lt_to_le … H))
548    >nth_opt_append_r >length_reverse [2: % ]
549    <minus_n_n <minus_n_n %
550  ]
551]
552qed.
553
554lemma nth_opt_reverse_hit_inv :
555  ∀A,l,n.n < |l| → nth_opt A (|l| - (S n)) (reverse ? l) = nth_opt A n l.
556#A #l #n #H <(reverse_reverse ? l) in ⊢ (???%); @sym_eq
557<length_reverse @nth_opt_reverse_hit >length_reverse @H
558qed.
559
560definition linearise_code:
561 ∀p : unserialized_params.∀globals.
562  ∀g : codeT (mk_graph_params p) globals.code_closed … g →
563  ∀entry : (Σl.bool_to_Prop (code_has_label … g l)).
564    (Σc : codeT (mk_lin_params p) globals.
565      code_closed … c ∧
566      ∃ sigma : identifier_map LabelTag ℕ.
567      lookup … sigma entry = Some ? 0 ∧
568      ∀l,n.lookup … sigma l = Some ? n →
569        ∃s. lookup … g l = Some ? s ∧
570          opt_Exists ?
571            (λls.let 〈lopt, ts〉 ≝ ls in
572              opt_All ? (eq ? l) lopt ∧
573              ts = graph_to_lin_statement … s ∧
574              opt_All ?
575                (λnext.Or (lookup … sigma next = Some ? (S n))
576                (nth_opt … (S n) c = Some ? 〈None ?, GOTO … next〉))
577                (stmt_implicit_label … s)) (nth_opt … n c))
578
579 λp,globals,g,g_prf,entry_sig.
580    let g ≝ branch_compress (mk_graph_params p) ? g entry_sig in
581    let g_prf ≝ branch_compress_closed … g entry_sig g_prf in
582    match graph_visit p globals g ∅ (empty_map …) [ ] [entry_sig] 0 (|g|)
583      (entry_sig) g_prf ?????????
584    with
585    [ mk_Sig triple H ⇒
586      let sigma ≝ \fst (\fst triple) in
587      let required ≝ \snd (\fst triple) in
588      let crev ≝ \snd triple in
589      let lbld_code ≝ rev ? crev in
590      mk_Sig ?? (filter_labels … (λl.l∈required) lbld_code) ? ].
591[ (* done later *)
592| #i >mem_set_empty *
593|3,4: #a #b whd in ⊢ (??%?→?); #ABS destruct(ABS)
594| #l #_ %
595| %2 % * >mem_set_empty *
596| % [2: %] @(branch_compress_has_entry … g entry_sig)
597| %
598| % % [% %] cases (pi1 … entry_sig) normalize #_ % //
599| >commutative_plus change with (? ≤ |g|) %
600]
601lapply (refl … triple)
602generalize in match triple in ⊢ (???%→%); **
603#visited #required #generated #EQtriple
604>EQtriple in H ⊢ %; normalize nodelta ****
605#entry_O #req_vis #last_fin #labels_in_req #sigma_prop
606% >EQtriple
607[ #i #s
608  >stmt_at_filter_labels #EQ
609  %
610  [ @stmt_forall_labels_explicit
611    @(All_mp … (labels_in_req … EQ))
612    #l #l_req >lin_code_has_label
613    >occurs_exactly_once_filter_labels >l_req
614    >commutative_andb whd in ⊢ (?%);
615    elim (sigma_prop ?? (lookup_eq_safe … (req_vis … l_req)))
616    >lin_code_has_label #H #_ @H
617  | lapply EQ cases s #s' [2: #_ % ]
618    * -EQ #EQ change with (bool_to_Prop (code_has_point ????))
619    whd in match (point_of_succ ???);
620    >lin_code_has_point @leb_elim [ #_ % ] >length_map >length_reverse
621    #INEQ
622    cut (|generated| = S i)
623    [ @(le_to_le_to_eq … (not_lt_to_le … INEQ) )
624      elim (option_bind_inverse ????? EQ) #x * #EQ1 #EQ2
625      <length_reverse
626      @(nth_opt_hit_length … EQ1)
627    ] #EQ_length
628    elim last_fin #fin #EQ'
629    lapply EQ whd in match (stmt_at ????);
630    >nth_opt_reverse_hit >EQ_length [2: % ] <minus_n_n
631    change with (stmt_at ???? = ? → ?)
632    >EQ' #ABS destruct(ABS)
633  ]
634]
635%{visited} % [assumption]
636#lbl #n #eq_lookup elim (sigma_prop ?? eq_lookup)
637#lbl_in_gen * #stmt ** #stmt_in_g #nth_opt_is_stmt #succ_is_in
638% [2: % [ assumption ] |]
639>nth_opt_filter_labels in ⊢ (???%);
640>nth_opt_is_stmt >m_return_bind whd >m_return_bind
641% [ % ]
642[ elim (lbl ∈ required) %
643| %
644| lapply succ_is_in
645  lapply (refl … (stmt_implicit_label … stmt))
646  cases (stmt_implicit_label … stmt) in ⊢ (???%→%); [#_ #_ %]
647  #next #EQ_next *
648  [ #H %1{H} ]
649  #H %2
650  >nth_opt_filter_labels >H %
651]
652qed.
653
654(* Paolo: for now I'm leaving the closed graph stuff out, waiting for it to
655   be done on all passes *)
656definition linearise_int_fun :
657  ∀p : unserialized_params.
658  ∀globals.
659    joint_internal_function globals (mk_graph_params p) →
660    joint_internal_function globals (mk_lin_params p)
661     (* ∃sigma : identifier_map LabelTag ℕ.
662        let g ≝ joint_if_code ?? (pi1 … fin) in
663        let c ≝ joint_if_code ?? (pi1 … fout) in
664        let entry ≝ joint_if_entry ?? (pi1 … fin) in
665         lookup … sigma entry = Some ? 0 ∧
666          ∀l,n.lookup … sigma l = Some ? n →
667            ∃s. lookup … g l = Some ? s ∧
668              opt_Exists ?
669                (λls.let 〈lopt, ts〉 ≝ ls in
670                  opt_All ? (eq ? l) lopt ∧
671                  ts = graph_to_lin_statement … s ∧
672                  opt_All ?
673                    (λnext.Or (lookup … sigma next = Some ? (S n))
674                    (nth_opt … (S n) c = Some ? 〈None ?, GOTO … next〉))
675                    (stmt_implicit_label … s)) (nth_opt … n c)*) ≝
676  λp,globals,f_in.
677  mk_joint_internal_function globals (mk_lin_params p)
678   (joint_if_luniverse ?? f_in) (joint_if_runiverse ?? f_in)
679   (joint_if_result ?? f_in) (joint_if_params ?? f_in) (joint_if_locals ?? f_in)
680   (joint_if_stacksize ?? f_in)
681   (linearise_code p globals (joint_if_code … f_in)
682   (match daemon in False with [ ])
683   (joint_if_entry … f_in))
684   0 0 (* exit is dummy! *).
685elim (linearise_code ?????) #c * #code_closed
686@hide_prf
687* #sigma * #O_in #sigma_prop
688>lin_code_has_point
689elim (sigma_prop … O_in) #s * #_
690cases c
691[1,3: *
692|*: #hd #tl #_ %
693]
694qed.
Note: See TracBrowser for help on using the repository browser.