source: src/joint/linearise.ma @ 2481

Last change on this file since 2481 was 2481, checked in by piccolo, 7 years ago

corrected some inconsistencies
fixed some of lineariseProof

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