# source:src/joint/linearise.ma@2557

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

going on in proof of linearise
simplified by use of monadic functional relations

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