Changeset 2391


Ignore:
Timestamp:
Oct 9, 2012, 3:10:07 PM (7 years ago)
Author:
campbell
Message:

Revert "Put the post-loop cost label into the Clight while statement ..."
Rely on the Cminor to RTLabs stage ignoring Cminor skips instead.
This reverts commit 2353.

Location:
src/Clight
Files:
12 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/Cexec.ma

    r2353 r2391  
    390390          | _ ⇒ Wrong ??? (msg NonsenseState)
    391391          ]
    392       | Kwhile a s' cl k' ⇒ ret ? 〈E0, State f (Swhile a s' cl) k' e m〉
     392      | Kwhile a s' k' ⇒ ret ? 〈E0, State f (Swhile a s') k' e m〉
    393393      | Kdowhile a s' k' ⇒
    394394          ! 〈v,tr〉 ← exec_expr ge e m a : IO ???;
     
    406406      match k with
    407407      [ Kseq s' k' ⇒ ret ? 〈E0, State f Scontinue k' e m〉
    408       | Kwhile a s' cl k' ⇒ ret ? 〈E0, State f (Swhile a s' cl) k' e m〉
     408      | Kwhile a s' k' ⇒ ret ? 〈E0, State f (Swhile a s') k' e m〉
    409409      | Kdowhile a s' k' ⇒
    410410          ! 〈v,tr〉 ← exec_expr ge e m a : IO ???;
     
    421421      match k with
    422422      [ Kseq s' k' ⇒ ret ? 〈E0, State f Sbreak k' e m〉
    423       | Kwhile a s' cl k' ⇒ ret ? 〈E0, State f (optional_cost cl Sskip) k' e m〉
     423      | Kwhile a s' k' ⇒ ret ? 〈E0, State f Sskip k' e m〉
    424424      | Kdowhile a s' k' ⇒ ret ? 〈E0, State f Sskip k' e m〉
    425425      | Kfor2 a2 a3 s' k' ⇒ ret ? 〈E0, State f Sskip k' e m〉
     
    431431      ! b ← err_to_io … (exec_bool_of_val v (typeof a));
    432432      ret ? 〈tr, State f (if b then s1 else s2) k e m〉
    433   | Swhile a s' cl
     433  | Swhile a s'
    434434      ! 〈v,tr〉 ← exec_expr ge e m a : IO ???;
    435435      ! b ← err_to_io … (exec_bool_of_val v (typeof a));
    436       ret ? 〈tr, if b then State f s' (Kwhile a s' cl k) e m
    437                       else State f (optional_cost cl Sskip) k e m〉
     436      ret ? 〈tr, if b then State f s' (Kwhile a s' k) e m
     437                      else State f Sskip k e m〉
    438438  | Sdowhile a s' ⇒ ret ? 〈E0, State f s' (Kdowhile a s' k) e m〉
    439439  | Sfor a1 a2 a3 s' ⇒
  • src/Clight/CexecComplete.ma

    r2353 r2391  
    383383    >(yields_eq ??? (bool_of_false ?? H2))
    384384    @refl
    385 | #f #e #s #cl #k #env #m #v #tr #H1 #H2 whd in ⊢ (??%?);
    386     >(yields_eq ??? (expr_complete … H1)) whd in ⊢ (??%?);
    387     >(yields_eq ??? (bool_of_false ?? H2))
    388     @refl
    389 | #f #e #s #cl #k #env #m #v #tr #H1 #H2 whd in ⊢ (??%?);
    390     >(yields_eq ??? (expr_complete … H1)) whd in ⊢ (??%?);
    391     >(yields_eq ??? (bool_of_true ?? H2))
    392     @refl
    393 | #f #s1 #e #s2 #cl #k #env #m #H cases H; #es1 >es1 @refl
    394 | 13,14: #f #e #s [#cl] #k #env #m @refl
     385| #f #e #s #k #env #m #v #tr #H1 #H2 whd in ⊢ (??%?);
     386    >(yields_eq ??? (expr_complete … H1)) whd in ⊢ (??%?);
     387    >(yields_eq ??? (bool_of_false ?? H2))
     388    @refl
     389| #f #e #s #k #env #m #v #tr #H1 #H2 whd in ⊢ (??%?);
     390    >(yields_eq ??? (expr_complete … H1)) whd in ⊢ (??%?);
     391    >(yields_eq ??? (bool_of_true ?? H2))
     392    @refl
     393| #f #s1 #e #s2 #k #env #m #H cases H; #es1 >es1 @refl
     394| 13,14: #f #e #s #k #env #m @refl
    395395| #f #s1 #e #s2 #k #env #m #v #tr *; #es1 >es1 #H1 #H2 whd in ⊢ (??%?);
    396396    >(yields_eq ??? (expr_complete … H1)) whd in ⊢ (??%?);
     
    424424    [ #H1 #H2 whd in ⊢ (??%?); >H2 @refl
    425425    | #s' #k' whd in ⊢ (% → ?); *;
    426     | 3,4: #e' #s' [#cl] #k' whd in ⊢ (% → ?); *;
     426    | 3,4: #e' #s' #k' whd in ⊢ (% → ?); *;
    427427    | 5,6: #e' #s1' #s2' #k' whd in ⊢ (% → ?); *;
    428428    | #k' whd in ⊢ (% → ?); *;
  • src/Clight/CexecEquiv.ma

    r2353 r2391  
    514514#ge #s cases s;
    515515[ #f #st #kk #e #m cases st;
    516   [ 11,14: #a | 2,4,7,12,13,15: #a #b | 3,5,6: #a #b #c | 8: #a #b #c #d ]
    517   [ 4,5,7,8: @I ]
     516  [ 11,14: #a | 2,4,6,7,12,13,15: #a #b | 3,5: #a #b #c | 8: #a #b #c #d ]
     517  [ 4,6,8,9: @I ]
    518518  whd in ⊢ (???%);
    519519  [ cases a; [ cases (fn_return f); //; | #e whd nodelta in ⊢ (???%);
     
    521521  | cases (find_label a (fn_body f) (call_cont kk)); [ @I | #z cases z #x #y @I ]
    522522  | @err2_does_not_interact #x1 #x2 @err2_does_not_interact #x3 #x4 @opt_does_not_interact #x5 @I
     523  | 4,7: @err2_does_not_interact #x1 #x2 @err_does_not_interact #x3 @I
    523524  | @err2_does_not_interact #x1 #x2 cases x1; //;
    524525  | @err2_does_not_interact #x1 #x2 @err2_does_not_interact #x3 #x4 @opt_does_not_interact #x5  @err_does_not_interact #x6 cases a;
    525526      [ @I | #x7 @err2_does_not_interact #x8 #x9 @I ]
    526   | 6,7: @err2_does_not_interact #x1 #x2 @err_does_not_interact #x3 @I
    527527  | cases (is_Sskip a); #H [ @err2_does_not_interact #x1 #x2 @err_does_not_interact #x3 @I
    528528      | @I ]
  • src/Clight/CexecSound.ma

    r2353 r2391  
    337337        @step_skip_call //;
    338338    | #s' #k' whd; //
    339     | #ex #s' #cl #k' @step_skip_or_continue_while % //;
     339    | #ex #s' #k' @step_skip_or_continue_while % //;
    340340    | #ex #s' #k'
    341341        @res_bindIO2_OK #v #tr #Hv
     
    385385    | @(step_ifthenelse_false … (exec_expr_sound' … Hv)) @(bool_of … Hb)
    386386    ]
    387   | #ex #s' #cl
     387  | #ex #s'
    388388    @res_bindIO2_OK #v #tr #Hv
    389389    letin bexpr ≝ (exec_bool_of_val v (typeof ex));
     
    407407  | whd in ⊢ (?????%); cases k; // #k' @step_skip_break_switch %2 //
    408408  | whd in ⊢ (?????%); cases k; //;
    409     [ #ex #s' #cl #k' whd; @step_skip_or_continue_while %2 ; //;
     409    [ #ex #s' #k' whd; @step_skip_or_continue_while %2 ; //;
    410410    | #ex #s' #k' whd;
    411411      @res_bindIO2_OK #v #tr #Hv
  • src/Clight/Csem.ma

    r2353 r2391  
    910910  | Kseq: statement -> cont -> cont
    911911       (**r [Kseq s2 k] = after [s1] in [s1;s2] *)
    912   | Kwhile: expr -> statement → option costlabel -> cont -> cont
     912  | Kwhile: expr -> statement -> cont -> cont
    913913       (**r [Kwhile e s k] = after [s] in [while (e) s] *)
    914914  | Kdowhile: expr -> statement -> cont -> cont
     
    930930  match k with
    931931  [ Kseq s k => call_cont k
    932   | Kwhile e s l k => call_cont k
     932  | Kwhile e s k => call_cont k
    933933  | Kdowhile e s k => call_cont k
    934934  | Kfor2 e2 e3 s k => call_cont k
     
    983983      | None => find_label lbl s2 k
    984984      ]
    985   | Swhile a s1 l =>
    986       find_label lbl s1 (Kwhile a s1 l k)
     985  | Swhile a s1 =>
     986      find_label lbl s1 (Kwhile a s1 k)
    987987  | Sdowhile a s1 =>
    988988      find_label lbl s1 (Kdowhile a s1 k)
     
    10351035].
    10361036
    1037 definition optional_cost : option costlabel → statement → statement ≝
    1038 λo,s. match o with [ Some cl ⇒ Scost cl s | None ⇒ s ].
    1039 
    10401037(* XXX: note that cost labels in exprs expose a particular eval order. *)
    10411038
     
    10901087           tr (State f s2 k e m)
    10911088
    1092   | step_while_false: ∀f,a,s,cl,k,e,m,v,tr.
     1089  | step_while_false: ∀f,a,s,k,e,m,v,tr.
    10931090      eval_expr ge e m a v tr →
    10941091      is_false v (typeof a) →
    1095       step ge (State f (Swhile a s cl) k e m)
    1096            tr (State f (optional_cost cl Sskip) k e m)
    1097   | step_while_true: ∀f,a,s,cl,k,e,m,v,tr.
     1092      step ge (State f (Swhile a s) k e m)
     1093           tr (State f Sskip k e m)
     1094  | step_while_true: ∀f,a,s,k,e,m,v,tr.
    10981095      eval_expr ge e m a v tr →
    10991096      is_true v (typeof a) →
    1100       step ge (State f (Swhile a s cl) k e m)
    1101            tr (State f s (Kwhile a s cl k) e m)
    1102   | step_skip_or_continue_while: ∀f,x,a,s,cl,k,e,m.
     1097      step ge (State f (Swhile a s) k e m)
     1098           tr (State f s (Kwhile a s k) e m)
     1099  | step_skip_or_continue_while: ∀f,x,a,s,k,e,m.
    11031100      x = Sskip ∨ x = Scontinue →
    1104       step ge (State f x (Kwhile a s cl k) e m)
    1105            E0 (State f (Swhile a s cl) k e m)
    1106   | step_break_while: ∀f,a,s,cl,k,e,m.
    1107       step ge (State f Sbreak (Kwhile a s cl k) e m)
    1108            E0 (State f (optional_cost cl Sskip) k e m)
     1101      step ge (State f x (Kwhile a s k) e m)
     1102           E0 (State f (Swhile a s) k e m)
     1103  | step_break_while: ∀f,a,s,k,e,m.
     1104      step ge (State f Sbreak (Kwhile a s k) e m)
     1105           E0 (State f Sskip k e m)
    11091106
    11101107  | step_dowhile: ∀f,a,s,k,e,m.
  • src/Clight/Csyntax.ma

    r2353 r2391  
    194194  | Ssequence : statement → statement → statement  (**r sequence *)
    195195  | Sifthenelse : expr  → statement → statement → statement (**r conditional *)
    196   | Swhile : expr → statement → option costlabel → statement   (**r [while] loop *)
     196  | Swhile : expr → statement → statement   (**r [while] loop *)
    197197  | Sdowhile : expr → statement → statement (**r [do] loop *)
    198198  | Sfor: statement → expr → statement → statement → statement (**r [for] loop *)
     
    226226  (Ssq:∀s1,s2. P s1 → P s2 → P (Ssequence s1 s2))
    227227  (Sif:∀e,s1,s2. P s1 → P s2 → P (Sifthenelse e s1 s2))
    228   (Swh:∀e,s,l. P s → P (Swhile e s l))
     228  (Swh:∀e,s. P s → P (Swhile e s))
    229229  (Sdo:∀e,s. P s → P (Sdowhile e s))
    230230  (Sfo:∀s1,e,s2,s3. P s1 → P s2 → P s3 → P (Sfor s1 e s2 s3))
     
    249249    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s1)
    250250    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s2)
    251 | Swhile e s cl ⇒ Swh e s cl
     251| Swhile e s ⇒ Swh e s
    252252    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s)
    253253| Sdowhile e s ⇒ Sdo e s
     
    275275  (Ssq:∀s1,s2. P s1 → P s2 → P (Ssequence s1 s2))
    276276  (Sif:∀e,s1,s2. P s1 → P s2 → P (Sifthenelse e s1 s2))
    277   (Swh:∀e,s,l. P s → P (Swhile e s l))
     277  (Swh:∀e,s. P s → P (Swhile e s))
    278278  (Sdo:∀e,s. P s → P (Sdowhile e s))
    279279  (Sfo:∀s1,e,s2,s3. P s1 → P s2 → P s3 → P (Sfor s1 e s2 s3))
  • src/Clight/SimplifyCasts.ma

    r2353 r2391  
    19821982| Ssequence s1 s2 ⇒ Ssequence (simplify_statement s1) (simplify_statement s2)
    19831983| Sifthenelse e s1 s2 ⇒ Sifthenelse (simplify_e e) (simplify_statement s1) (simplify_statement s2) (* TODO: try to reduce size of e *)
    1984 | Swhile e s1 cl ⇒ Swhile (simplify_e e) (simplify_statement s1) cl (* TODO: try to reduce size of e *)
     1984| Swhile e s1 ⇒ Swhile (simplify_e e) (simplify_statement s1) (* TODO: try to reduce size of e *)
    19851985| Sdowhile e s1 ⇒ Sdowhile (simplify_e e) (simplify_statement s1) (* TODO: try to reduce size of e *)
    19861986| Sfor s1 e s2 s3 ⇒ Sfor (simplify_statement s1) (simplify_e e) (simplify_statement s2) (simplify_statement s3) (* TODO: reduce size of e *)
     
    20152015| cc_stop : cont_cast Kstop Kstop
    20162016| cc_seq : ∀s,k,k'. cont_cast k k' → cont_cast (Kseq s k) (Kseq (simplify_statement s) k')
    2017 | cc_while : ∀e,s,cl,k,k'.
     2017| cc_while : ∀e,s,k,k'.
    20182018    cont_cast k k' →
    2019     cont_cast (Kwhile e s cl k) (Kwhile (simplify_e e) (simplify_statement s) cl k')
     2019    cont_cast (Kwhile e s k) (Kwhile (simplify_e e) (simplify_statement s) k')
    20202020| cc_dowhile : ∀e,s,k,k'.
    20212021    cont_cast k k' →
     
    24242424          | 1: * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 normalize nodelta //
    24252425     ] ]
    2426 | 6: #e #s #cl #Hind_s #k #k' #Hcont_cast
     2426| 6: #e #s #Hind_s #k #k' #Hcont_cast
    24272427     whd in match (find_label ???);
    24282428     whd in match (find_label ? (simplify_statement ?) ?);
    2429      elim (elim_IH_aux lab s (Kwhile e s cl k) (Kwhile (simplify_e e) (simplify_statement s) cl k') ? Hind_s)
     2429     elim (elim_IH_aux lab s (Kwhile e s k) (Kwhile (simplify_e e) (simplify_statement s) k') ? Hind_s)
    24302430     [ 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast'
    24312431          normalize nodelta %{kst'} /2/
     
    26162616               [ 1: // | 2: %1 // ]               
    26172617          | 3: (* Kwhile *)
    2618                #cond #body #cl #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_ normalize nodelta #Eq
     2618               #cond #body #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_ normalize nodelta #Eq
    26192619               whd in match (ret ??) in Eq; destruct (Eq)               
    2620                %{(State (simplify_function f) (Swhile (simplify_e cond) (simplify_statement body) cl) k0' en m)} @conj
     2620               %{(State (simplify_function f) (Swhile (simplify_e cond) (simplify_statement body)) k0' en m)} @conj
    26212621               [ 1: // | 2: %1 // ]
    26222622          | 4: (* Kdowhile *)
     
    27832783                             [ 1: // | 2: <e0 %1 // ]
    27842784                        ] ] ] ]
    2785     | 6: #cl #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome;
     2785    | 6: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome;
    27862786         whd in match (simplify_statement ?) in Heq ⊢ %; #Heq
    27872787         whd in match (exec_step ??) in Heq ⊢ %;
     
    27982798                   | 1: * whd in match (bindIO ??????) in ⊢ (% → %); #Heq normalize nodelta in Heq ⊢ %;
    27992799                        [ 1: destruct skip (condtrace)
    2800                              %{(State (simplify_function f) (simplify_statement body) (Kwhile (simplify_e cond) (simplify_statement body) cl k') en m)}
     2800                             %{(State (simplify_function f) (simplify_statement body) (Kwhile (simplify_e cond) (simplify_statement body) k') en m)}
    28012801                             @conj
    28022802                             [ 1: // | 2: <e0 %1 @cc_while // ]
    28032803                        | 2: destruct skip (condtrace)
    2804                              %{(State (simplify_function f) (optional_cost cl Sskip) k' en m)} @conj
    2805                              [ 1: // | 2: <e0 cases cl [2:#cl'] %1 // ]
     2804                             %{(State (simplify_function f) Sskip k' en m)} @conj
     2805                             [ 1: // | 2: <e0 %1 // ]
    28062806                        ] ] ] ]
    28072807    | 7: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome;
     
    28502850         [ 1: #Hk #Hk' #_
    28512851         | 2: #stm' #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_
    2852          | 3: #cond #body #cl #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_
     2852         | 3: #cond #body #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_
    28532853         | 4: #cond #body #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_
    28542854         | 5,6,7: #cond #step #body #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_
     
    28582858         destruct (H)
    28592859         [ 1,4: %{(State (simplify_function f) Sbreak k0' en m)} @conj [ 1,3: // | 2,4: %1 // ]
    2860          | %{(State (simplify_function f) (optional_cost cl Sskip) k0' en m)} @conj try // cases cl [2:#cl'] %1 //
    2861          | 3,5,6: %{(State (simplify_function f) Sskip k0' en m)} @conj try // %1 // ]
     2860         | 2,3,5,6: %{(State (simplify_function f) Sskip k0' en m)} @conj try // %1 // ]
    28622861    | 10: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome;
    28632862         whd in match (simplify_statement ?) in Heq ⊢ %; #Heq
     
    28662865         [ 1: #Hk #Hk' #_
    28672866         | 2: #stm' #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_
    2868          | 3: #cond #body #cl #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_
     2867         | 3: #cond #body #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_
    28692868         | 4: #cond #body #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_
    28702869         | 5,6,7: #cond #step #body #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_
     
    28742873         destruct (H)
    28752874         [ 1,4,6: %{(State (simplify_function f) Scontinue k0' en m)} @conj try // %1 //
    2876          | 2: %{(State (simplify_function f) (Swhile (simplify_e cond) (simplify_statement body) cl) k0' en m)}
     2875         | 2: %{(State (simplify_function f) (Swhile (simplify_e cond) (simplify_statement body)) k0' en m)}
    28772876              @conj try // %1 //
    28782877         | 3: elim (Hsim_related cond) #Hsim_cond #Htype_cond_eq elim Hsim_cond in H;
     
    30083007     [ 1: #Hk #Hk' #_
    30093008     | 2: #stm' #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_
    3010      | 3: #cond #body #cl #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_
     3009     | 3: #cond #body #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_
    30113010     | 4: #cond #body #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_
    30123011     | 5,6,7: #cond #step #body #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_
  • src/Clight/label.ma

    r2353 r2391  
    2727| Ssequence s1 s2 ⇒ statement_label_free s1 ∧ statement_label_free s2
    2828| Sifthenelse e1 s1 s2 ⇒ expr_label_free e1 ∧ statement_label_free s1 ∧ statement_label_free s2
    29 | Swhile e1 s1 cl ⇒ expr_label_free e1 ∧ statement_label_free s1 ∧ match cl with [ None ⇒ true | _ ⇒ false ]
     29| Swhile e1 s1 ⇒ expr_label_free e1 ∧ statement_label_free s1
    3030| Sdowhile e1 s1 ⇒ expr_label_free e1 ∧ statement_label_free s1
    3131| Sfor s1 e1 s2 s3 ⇒ statement_label_free s1 ∧ expr_label_free e1 ∧ statement_label_free s2 ∧ statement_label_free s3
     
    145145| Some e ⇒ let 〈e,costgen〉 ≝ label_expr e costgen in 〈Some ? e,costgen〉
    146146].
    147 
    148 definition ensure_label : option costlabel → universe CostTag → costlabel × (universe CostTag) ≝
    149 λo,u.
    150   match o with
    151   [ Some cl ⇒ 〈cl,u〉
    152   | None ⇒ fresh … u
    153   ].
    154147
    155148
     
    178171    let 〈s2,costgen〉 ≝ add_cost_before s2 costgen in
    179172    〈Sifthenelse e s1 s2, costgen〉
    180 | Swhile e s' cl
     173| Swhile e s'
    181174    let 〈e,costgen〉 ≝ label_expr e costgen in
    182175    let 〈s',costgen〉 ≝ label_statement s' costgen in
    183176    let 〈s',costgen〉 ≝ add_cost_before s' costgen in
    184     let 〈after,costgen〉 ≝ ensure_label cl costgen in
    185     〈Swhile e s' (Some ? after), costgen〉
     177    let 〈s,costgen〉 ≝ add_cost_after (Swhile e s') costgen in
     178    〈s,costgen〉
    186179| Sdowhile e s' ⇒
    187180    let 〈e,costgen〉 ≝ label_expr e costgen in
  • src/Clight/labelSimulation.ma

    r2353 r2391  
    264264| cwl_stop : cont_with_labels Kstop Kstop
    265265| cwl_seq : ∀u,s,k,k'. cont_with_labels k k' → cont_with_labels (Kseq s k) (Kseq (\fst (label_statement s u)) k')
    266 | cwl_while : ∀ue,e,us,s,cl,cs,cpost,k,k'.
     266| cwl_while : ∀ue,e,us,s,cs,cpost,k,k'.
    267267    cont_with_labels k k' →
    268     (cl = None ? ∨ cl = Some ? cpost) →
    269     cont_with_labels (Kwhile e s cl k) (Kwhile (\fst (label_expr e ue)) (Scost cs (\fst (label_statement s us))) (Some ? cpost) k')
     268    cont_with_labels (Kwhile e s k) (Kwhile (\fst (label_expr e ue)) (Scost cs (\fst (label_statement s us))) (Kseq (Scost cpost Sskip) k'))
    270269| cwl_dowhile : ∀ue,e,us,s,cs,cpost,k,k'.
    271270    cont_with_labels k k' →
     
    292291(* Extra matching states that we can reach that don't quite correspond to the
    293292   labelling function *)
    294 | swl_whilestate : ∀g,f,ua,a,us,s,cl,cs,cpost,k,k',e,m. cont_with_labels k k' →
    295     (cl = None ? ∨ cl = Some ? cpost) →
    296     state_with_labels_partial (State f (Swhile a s cl) k e m) (State (\fst (label_function g f)) (Swhile (\fst (label_expr a ua)) (Scost cs (\fst (label_statement s us))) (Some ? cpost)) k' e m)
     293| swl_whilestate : ∀g,f,ua,a,us,s,cs,cpost,k,k',e,m. cont_with_labels k k' →
     294    state_with_labels_partial (State f (Swhile a s) k e m) (State (\fst (label_function g f)) (Swhile (\fst (label_expr a ua)) (Scost cs (\fst (label_statement s us)))) (Kseq (Scost cpost Sskip) k') e m)
    297295| swl_dowhilestate : ∀g,f,ua,a,us,s,cs,cpost,k,k',e,m. cont_with_labels k k' →
    298296    state_with_labels_partial (State f (Sdowhile a s) k e m) (State (\fst (label_function g f)) (Sdowhile (\fst (label_expr a ua)) (Scost cs (\fst (label_statement s us)))) (Kseq (Scost cpost Sskip) k') e m)
     
    434432| Ssequence s1 s2 ⇒ ∀u1,u2. P (Ssequence (\fst (label_statement s1 u1)) (\fst (label_statement s2 u2)))
    435433| Sifthenelse e s1 s2 ⇒ ∀u1,u2,u3,c2,c3. P (Sifthenelse (\fst (label_expr e u1)) (Scost c2 (\fst (label_statement s1 u2))) (Scost c3 (\fst (label_statement s2 u3))))
    436 | Swhile e s1 cl ⇒ ∀u1,u2,cs,cpost. cl = None ? ∨ cl = Some ? cpost → P (Swhile (\fst (label_expr e u1)) (Scost cs (\fst (label_statement s1 u2))) (Some ? cpost))
     434| Swhile e s1 ⇒ ∀u1,u2,cs,cpost. P (Ssequence (Swhile (\fst (label_expr e u1)) (Scost cs (\fst (label_statement s1 u2)))) (Scost cpost Sskip))
    437435| Sdowhile e s1 ⇒ ∀u1,u2,cs,cpost. P (Ssequence (Sdowhile (\fst (label_expr e u1)) (Scost cs (\fst (label_statement s1 u2)))) (Scost cpost Sskip))
    438436| Sfor s1 e s2 s3 ⇒ ∀u1,u2,u3,u4,c3,c4. P (Ssequence (Sfor (\fst (label_statement s1 u1)) (\fst (label_expr e u2)) (\fst (label_statement s2 u3)) (Scost c3 (\fst (label_statement s3 u4)))) (Scost c4 Sskip))
     
    449447@label_gen_elim #u2 //
    450448[ 6: >shift_fst //
    451 | 3: @label_gen_elim #u3 >shift_fst >shift_fst
    452      cases C in E ⊢ %; /3/
    453449| *: @label_gen_elim #u3 //
    454450     @label_gen_elim #u4
    455451     [ @label_gen_elim #u5 >shift_fst >shift_fst //
    456      | >shift_fst >shift_fst //
     452     | 2,3: >shift_fst >shift_fst //
    457453     | @label_gen_elim #u5 >shift_fst >shift_fst >shift_fst //
    458454     ]
     
    533529      @refl | // ] |skip ]| skip ]| skip ]
    534530  ]
    535 | #e #s0 #cl #IH #k #k' #u #K @blindly_label #u1 #u2 #cs #cpost #CL
     531| #e #s0 #IH #k #k' #u #K @blindly_label #u1 #u2 #cs #cpost
    536532  whd in match (find_label ?? k); normalize in match (find_label ?? k');
    537533  @(lfl_IH s0 … IH) [ /2/ ]
     
    675671    | #u #s0 #k0 #k0' #K #_ #E1 #E2 #E3 destruct %{0} whd
    676672      whd in EX:(??%%); destruct /4/
    677     | #ue #e0 #us0 #s0 #cl #cs #cpost #k0 #k0' #K #CL #_ #E1 #E2 #E3 destruct %{0}
     673    | #ue #e0 #us0 #s0 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct %{0}
    678674      whd in EX:(??%%); destruct whd /4/
    679675    | #ue #e0 #us0 #s0 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct
     
    765761    whd in ⊢ (??%?); >label_expr_type >EX2
    766762    whd in ⊢ (??%?); % [1,3: <(E0_right tr) ] /4/
    767   | #a #st #cl #EX
     763  | #a #st #EX
    768764    cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
    769765    cases (bindIO_inversion ??????? EX) -EX * * #EX2 #EX
    770766    normalize in EX; destruct
    771     @blindly_label #u1 #u2 #cs #cpost * #CL destruct
    772     cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 u1) #tr1' * #EX1' #T1
    773     [ 1,2,3: %{1} | %{0} ] whd
     767    whd in match (label_statement ??); @label_gen_elim #u1
     768    @label_gen_elim #u2
     769    whd in match (add_cost_before ??); cases (fresh ??) #c6 #u6
     770    >shift_fst whd in match (add_cost_after ??); cases (fresh ??) #c7 #u7
     771    >shift_fst
     772    cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 us) #tr1' * #EX1' #T1
     773    [ %{2} | %{3} ] whd
    774774    whd in ⊢ (??%?); >EX1'
    775775    whd in ⊢ (??%?); >label_expr_type >EX2
    776     whd in ⊢ (??%?); whd % [ 1,3,5,7: <(E0_right tr) ] /5 by twel_new, swl_partial, swl_state, cwl_while, twel_app, or_introl, or_intror/
     776    whd in ⊢ (??%?); % [ 1,3: <(E0_right tr) ] /5/
    777777  | #a #st #EX
    778778    normalize in EX; destruct
     
    805805    [ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
    806806    |#u #s0 #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
    807     | #ue #e0 #us0 #s0 #cl #cs #cpost #k0 #k0' #K' * #CL #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
     807    | #ue #e0 #us0 #s0 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
    808808    | #ue #e0 #us0 #s0 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
    809809    | #ue #e0 #us1 #s1 #us2 #st2 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
     
    815815    ]
    816816    whd in match (label_statement ??);
    817     [ 1,3,7,8: %{0} % /3/
    818     | 2,5: %{1} whd % /3/
    819     | 4,6: %{2} whd % /3/
     817    [ 1,6,7: %{0} % /3/
     818    | 2,3,5: %{2} % /3/
     819    | %{1} % /3/
    820820    ]
    821821  | #EX inversion KL
    822822    [ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
    823823    |#u #s0 #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
    824     | #ue #e0 #us0 #s0 #cl #cs #cpost #k0 #k0' #K' * #CL #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
     824    | #ue #e0 #us0 #s0 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
    825825    | #ue #e0 #us0 #s0 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
    826826    | #ue #e0 #us1 #s1 #us2 #st2 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
     
    832832    ]
    833833    whd in match (label_statement ??);
    834     [ 1,2,3,6,7,8: %{0} % /4/
    835     | 5: %{1} % /4/
     834    [ 1,2,5,6,7: %{0} % /4/
     835    | 4: %{1} % /4/
    836836    | cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
    837837      cases (bindIO_inversion ??????? EX) -EX * * #EX2 #EX
     
    897897    %{0} % /3/
    898898  ]
    899 | #u0 #f #ua #a #us #s #cl #cs #cpost #k #k' #e #m #K * #CL #EX
     899| #u0 #f #ua #a #us #s #cs #cpost #k #k' #e #m #K #EX
    900900  cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
    901901  cases (bindIO_inversion ??????? EX) -EX * * #EX2 #EX
    902902  whd in EX:(??%%); destruct
    903903  cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 ua) #tr1' * #EX1' #T1
    904   [ 4: %{0} | 1,2,3: %{1} ] whd
     904  [ %{1} | %{2} ] whd
    905905  whd in ⊢ (??%?); >EX1'
    906906  whd in ⊢ (??%?); >label_expr_type >EX2
    907   whd % [ 1,3,5,7: <(E0_right tr) ] /5/
     907  % [ 1,3: <(E0_right tr) ] /4/
    908908| #u0 #f #ua #a #us #s #cs #cpost #k #k' #e #m #K #EX
    909909  whd in EX:(??%%); destruct
     
    991991#ge #s cases s
    992992[ #f #st #kk #e #m #o #k #EX @⊥ cases st in EX ⊢ %;
    993   [ 11,14: #a | 2,4,7,12,13,15: #a #b | 3,5,6: #a #b #c | 8: #a #b #c #d ]
     993  [ 11,14: #a | 2,4,6,7,12,13,15: #a #b | 3,5: #a #b #c | 8: #a #b #c #d ]
    994994  whd in ⊢ (??%? → ?);
    995   [ 4,5,7,8: #EX destruct ]
     995  [ 4,6,8,9: #EX destruct ]
    996996  [ cases a
    997997    [ whd in ⊢ (??%? → ?); cases (fn_return f) normalize #A try #B try #C try #D destruct
     
    10011001  | cases (find_label a (fn_body f) (call_cont kk)) [ 2: * #x #y ] #EX whd in EX:(??%?); destruct
    10021002  | @bindIO_res_interact #l #El @bindIO_res_interact #vt #Evt @bindIO_opt_interact #m' #Em #EX whd in EX:(??%?); destruct
     1003  | 4,7: @bindIO_res_interact #x1 #x2 @bindIO_res_interact #x3 #x4 #EX whd in EX:(??%?); destruct
    10031004  | @bindIO_res_interact * * normalize #A #B #C try #D try #E destruct
    10041005  | @bindIO_res_interact #x1 #x2 @bindIO_res_interact #x3 #x4 @bindIO_opt_interact #x5 #x6 @bindIO_res_interact #x7 #x8 cases a
    10051006      [ 2: #x9 @bindIO_res_interact #x10 #x11 ] #EX whd in EX:(??%?); destruct
    1006   | 6,7: @bindIO_res_interact #x1 #x2 @bindIO_res_interact #x3 #x4 #EX whd in EX:(??%?); destruct
    10071007  | cases (is_Sskip a) #H [ @bindIO_res_interact #vt #Evt @bindIO_res_interact #v #Ev ] #EX whd in EX:(??%?); destruct
    10081008  | cases kk [ 1,8: cases (fn_return f) normalize #A try #B try #C try #D try #E try #F try #G try #H destruct
     
    10381038[ #s #s' #S' #E1 #E2 #E3 destruct inversion S'
    10391039  [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 destruct
    1040   | #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 destruct
     1040  | #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 destruct
    10411041  | #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 destruct
    10421042  | #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 #H59 #H60 #H61 destruct
  • src/Clight/switchRemoval.ma

    r2387 r2391  
    7878| Ssequence s1 s2 ⇒ switch_free s1 ∧ switch_free s2
    7979| Sifthenelse e s1 s2 ⇒ switch_free s1 ∧ switch_free s2
    80 | Swhile e body _ ⇒ switch_free body
     80| Swhile e body ⇒ switch_free body
    8181| Sdowhile e body ⇒ switch_free body
    8282| Sfor s1 _ s2 s3 ⇒ switch_free s1 ∧ switch_free s2 ∧ switch_free s3
     
    249249  do 〈s2', acc2, fvs'', u''〉 ← switch_removal s2 fvs' u';
    250250  ret 〈Sifthenelse e s1' s2', acc1 @ acc2, fvs'', u''〉
    251 | Swhile e body cl
     251| Swhile e body
    252252  do 〈body', acc, fvs', u'〉 ← switch_removal body fvs u;
    253   ret 〈Swhile e body' cl, acc, fvs', u'〉
     253  ret 〈Swhile e body', acc, fvs', u'〉
    254254| Sdowhile e body ⇒
    255255  do 〈body', acc, fvs', u'〉 ← switch_removal body fvs u;
     
    318318  let 〈fvs', u''〉 ≝ mk_fresh_variables s2 u' in
    319319  〈fvs @ fvs', u''〉
    320 | Swhile e body cl
     320| Swhile e body
    321321  mk_fresh_variables body u
    322322| Sdowhile e body ⇒
     
    367367  (Ssq:∀s1,s2. P s1 → P s2 → P (Ssequence s1 s2))
    368368  (Sif:∀e,s1,s2. P s1 → P s2 → P (Sifthenelse e s1 s2))
    369   (Swh:∀e,s,cl. P s → P (Swhile e s cl))
     369  (Swh:∀e,s. P s → P (Swhile e s))
    370370  (Sdo:∀e,s. P s → P (Sdowhile e s))
    371371  (Sfo:∀s1,e,s2,s3. P s1 → P s2 → P s3 → P (Sfor s1 e s2 s3))
     
    390390    (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s1)
    391391    (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s2)
    392 | Swhile e s cl ⇒ Swh e s cl
     392| Swhile e s ⇒ Swh e s
    393393    (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s)
    394394| Sdowhile e s ⇒ Sdo e s
     
    416416  (Ssq:∀s1,s2. P s1 → P s2 → P (Ssequence s1 s2))
    417417  (Sif:∀e,s1,s2. P s1 → P s2 → P (Sifthenelse e s1 s2))
    418   (Swh:∀e,s,cl. P s → P (Swhile e s cl))
     418  (Swh:∀e,s. P s → P (Swhile e s))
    419419  (Sdo:∀e,s. P s → P (Sdowhile e s))
    420420  (Sfo:∀s1,e,s2,s3. P s1 → P s2 → P s3 → P (Sfor s1 e s2 s3))
     
    472472         (ret_acc statement s1'@ret_acc statement s2') (ret_fvs statement s2')
    473473         (ret_u statement s2')))} % try //
    474 | 6: #e #s #cl #H #u0 #u1 #post normalize
     474| 6: #e #s #H #u0 #u1 #post normalize
    475475     elim (H u0 u1 post) #s1' * normalize
    476476     cases (mk_fresh_variables s u0) #fvs #u'
    477477     #Heq1 #Heq1_fvs >Heq1 normalize nodelta
    478      %{(mk_swret statement (Swhile e (ret_st statement s1') cl) (ret_acc statement s1')
     478     %{(mk_swret statement (Swhile e (ret_st statement s1')) (ret_acc statement s1')
    479479        (ret_fvs statement s1') (ret_u statement s1'))} % try //
    480480| 7: #e #s #H #u0 #u1 #post normalize
     
    628628| Sifthenelse e s1 s2 ⇒
    629629  max_id (max_of_expr e) (max_id (max_of_statement s1) (max_of_statement s2))
    630 | Swhile e body _
     630| Swhile e body
    631631  max_id (max_of_expr e) (max_of_statement body)
    632632| Sdowhile e body ⇒
     
    712712| Ssequence sub1 sub2 ⇒ P sub1 ∧ P sub2
    713713| Sifthenelse e sub1 sub2 ⇒ P sub1 ∧ P sub2
    714 | Swhile e sub _ ⇒ Q e ∧ P sub
     714| Swhile e sub ⇒ Q e ∧ P sub
    715715| Sdowhile e sub ⇒ Q e ∧ P sub
    716716| Sfor sub1 cond sub2 sub3 ⇒ P sub1 ∧ Q cond ∧ P sub2 ∧ P sub3
     
    21942194    switch_removal s fvs u = Some ? result →
    21952195    switch_cont_sim fvs (Kseq s k) (Kseq (ret_st ? result) k')
    2196 | swc_while : ∀fvs,e,s,optlab,k,k',u,result.
    2197     fresh_for_statement (Swhile e s optlab) u →
     2196| swc_while : ∀fvs,e,s,k,k',u,result.
     2197    fresh_for_statement (Swhile e s) u →
    21982198    switch_cont_sim fvs k k' →
    21992199    switch_removal s fvs u = Some ? result →
    2200     switch_cont_sim fvs (Kwhile e s optlab k) (Kwhile e (ret_st ? result) optlab k')
     2200    switch_cont_sim fvs (Kwhile e s k) (Kwhile e (ret_st ? result) k')
    22012201| swc_dowhile : ∀fvs,e,s,k,k',u,result.
    22022202    fresh_for_statement (Sdowhile e s) u →
     
    28012801qed. *)
    28022802
    2803 lemma while_fresh_lift : ∀e,s,cl,u.
    2804    fresh_for_expression e u → fresh_for_statement s u → fresh_for_statement (Swhile e s cl) u.
    2805 #e #s #cl * #u whd in ⊢ (% → % → %); whd in match (max_of_statement (Swhile ???));
     2803lemma while_fresh_lift : ∀e,s,u.
     2804   fresh_for_expression e u → fresh_for_statement s u → fresh_for_statement (Swhile e s) u.
     2805#e #s * #u whd in ⊢ (% → % → %); whd in match (max_of_statement (Swhile ??));
    28062806cases (max_of_expr e) #e cases (max_of_statement s) #s normalize
    28072807cases (leb e s) try /2/
  • src/Clight/test/controlflow.c.ma

    r2388 r2391  
    2828               (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed  ))
    2929               (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
    30                (Tint I32 Signed  ))))
    31          (None ?))
     30               (Tint I32 Signed  )))))
    3231         (Ssequence
    3332         (Sassign (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed  ))
     
    133132                 (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed  ))
    134133                 (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
    135                  (Tint I32 Signed  )))))
    136              (None ?)))
     134                 (Tint I32 Signed  )))))))
    137135         )
    138136         (Sreturn (Some expr (Expr (Evar (ident_of_nat 3))
  • src/Clight/toCminor.ma

    r2389 r2391  
    5151                         gather_mem_vars_stmt s1 ∪
    5252                         gather_mem_vars_stmt s2
    53 | Swhile e1 s1 _ ⇒ gather_mem_vars_expr e1 ∪
    54                    gather_mem_vars_stmt s1
     53| Swhile e1 s1 ⇒ gather_mem_vars_expr e1 ∪
     54                 gather_mem_vars_stmt s1
    5555| Sdowhile e1 s1 ⇒ gather_mem_vars_expr e1 ∪
    5656                   gather_mem_vars_stmt s1
     
    926926[ Ssequence s1 s2 ⇒ labels_defined s1 @ labels_defined s2
    927927| Sifthenelse _ s1 s2 ⇒ labels_defined s1 @ labels_defined s2
    928 | Swhile _ s _ ⇒ labels_defined s
     928| Swhile _ s ⇒ labels_defined s
    929929| Sdowhile _ s ⇒ labels_defined s
    930930| Sfor s1 _ s2 s3 ⇒ labels_defined s1 @ labels_defined s2 @ labels_defined s3
     
    11241124axiom ReturnMismatch : String.
    11251125
    1126 definition optional_cost : option costlabel → stmt → stmt ≝
    1127 λo,s. match o with [ Some l ⇒ St_cost l s | None ⇒ s ].
    1128 
    11291126let rec translate_statement (vars:var_types) (uv:tmpgen vars) (ul:labgen) (lbls:lenv) (flag:convert_flag) (rettyp:option typ) (s:statement) on s
    11301127  : res (Σsu:(tmpgen vars)×labgen×stmt.trans_inv vars lbls s uv flag rettyp su) ≝
     
    11731170   but the behaviour of the next stage means that we can put in Cminor skips and
    11741171   goto labels before the cost label. *)
    1175 | Swhile e1 s1 cl
     1172| Swhile e1 s1
    11761173    do e1' ← translate_expr vars e1;
    11771174    match typ_of_type (typeof e1) return λx.(Σe:CMexpr x.expr_vars ? e ?) → ? with
     
    11831180        let converted_loop ≝
    11841181          St_label entry
    1185             (St_ifthenelse ?? e1' (St_seq s1' (St_goto entry)) (St_label exit (optional_cost cl St_skip)))
     1182          (St_seq
     1183            (St_ifthenelse ?? e1' (St_seq s1' (St_goto entry)) St_skip)
     1184            (St_label exit St_skip))
    11861185        in         
    11871186          OK ? «〈fgens2, converted_loop〉, ?»
     
    13541353                | 3,6: #H %2 assumption ] ]
    13551354try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @I try assumption
    1356 [ 1,10,22: whd elim e1' #e #Hvars @(expr_vars_mp … Hvars) #i #t #Hlocal @(tmp_preserved … Hlocal)
    1357 | cases cl normalize /3/
    1358 | (*2,8: @(stmt_P_mp … Hstmt_inv1) #s0 #Hstmt_vars @(stmt_vars_mp … Hstmt_vars) //
    1359 |*) 3,11: whd #l #H normalize in H;
    1360          elim (Hlabels_tr1 … H) #label #Hlabel @(ex_intro … label)
    1361          @conj
    1362          [ 1,3: @(proj1 … Hlabel)
    1363          | 2,4: whd @or_intror normalize in ⊢ (???%);
    1364                 [ @Exists_append_l @Exists_append_l | %2 @Exists_append_l @Exists_append_l @Exists_append_l ]
    1365                 @(proj2 … Hlabel) ]
    1366 | cases cl normalize /3/
    1367 | 5,13,16: whd %1 %1 normalize /2/
    1368 | 6,15: @(stmt_P_mp … Hind) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)
     1355[ 1,7,19: whd elim e1' #e #Hvars @(expr_vars_mp … Hvars) #i #t #Hlocal @(tmp_preserved … Hlocal)
     1356| 2,8: whd #l #H normalize in H;
     1357       elim (Hlabels_tr1 … H) #label #Hlabel @(ex_intro … label)
     1358       @conj
     1359       [ 1,3: @(proj1 … Hlabel)
     1360       | 2,4: whd @or_intror normalize in ⊢ (???%);
     1361              [ @Exists_append_l @Exists_append_l @Exists_append_l | %2 @Exists_append_l @Exists_append_l @Exists_append_l ]
     1362              @(proj2 … Hlabel) ]
     1363| whd %1 %1 normalize /2/
     1364| 4,12: @(stmt_P_mp … Hind) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)
    13691365   #l * try * [ 1,5: #H %1 %1 normalize %2 [ 2: %2 ] @Exists_append_l @Exists_append_l try @Exists_append_l @H
    13701366              | 2,6: #H %1 %2 assumption
     
    13741370                                               | 2,4: * ]
    13751371              ]
    1376 | 7: normalize %1 %1 %1 //
    1377 | 8,14: normalize %1 %1 %2 [ @Exists_append_r normalize /2/ | %1 % ]
    1378 | cases cl normalize /3/
     1372| normalize %1 %1 %1 //
     1373| 6,11: normalize %1 %1 %2 [ @Exists_append_r normalize /2/ | %1 % ]
    13791374| whd %1 %1 normalize %2 %1 %
     1375| 10,13: normalize %1 %1 %1 %
    13801376| normalize %1 %1 %2 %2 /2/
    13811377| whd #label * [ 1: #Eq @(ex_intro … l') @conj [ 1: destruct // | whd /2/ ]
Note: See TracChangeset for help on using the changeset viewer.