Changeset 1350 for src/Clight


Ignore:
Timestamp:
Oct 11, 2011, 2:27:53 AM (8 years ago)
Author:
sacerdot
Message:

Porting to latest destruct tactic.

Note: the tactics has a few remaining bugs to be ironed out.
Look for "Wilmer: XXX" comments in the .ma files to see where
these are avoided ATM using axioms.

Location:
src/Clight
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/CexecEquiv.ma

    r1344 r1350  
    176176            [ #o2 #k2 #E whd in E:(??%??); destruct (E)
    177177            | #x cases x; #tr2 #s2 whd in ⊢ (??%?? → ?);
    178                 lapply (is_final_elim s2) #IFE whd in IFE:(∀_. ? → ? → ?%)
     178                lapply (is_final_elim s2) #IFE whd in IFE:(∀_. ? → ? → ?%);
     179                change in match (is_final ?????) with (is_final s2)
    179180                @IFE
    180181                [ #r' #FINAL #E whd in E:(??%??);
     
    416417            [ #o2 #k2 #EXECK whd in EXECK:(??%??); destruct
    417418            | #x cases x; #tr2 #s2 whd in ⊢ (??%?? → ?);
    418                 lapply (is_final_elim s2) #IFE whd in IFE:(∀_. ? → ? → ?%)
     419                lapply (is_final_elim s2) #IFE whd in IFE:(∀_. ? → ? → ?%);
     420                change in match (is_final ?????) with (is_final s2)
    419421                @IFE [ #r ] #F #EXECK
    420422                whd in EXECK:(??%??); destruct;
     
    687689    >E2 in H1 #H1 whd in H1:(?%?); >K' in H1
    688690    >(exec_inf_aux_unfold …) whd in ⊢ (?%? → ?);
     691    change in match (is_final ?????) with (is_final s'')
    689692    @is_final_elim
    690693    [ #r #F whd in ⊢ (?%? → ?); #S
     
    879882            cases (exec_step ge s');
    880883            [ #o1 #k1 #EXEC' #H whd in EXEC':(?%?) H;
    881                 cases (se_inv … EXEC'); *; #E1 #E2 #H2 destruct (E1 E2);
     884                cases (se_inv … EXEC'); *; #E1 #E2 #H2 destruct (E1 E2); normalize in H2;
    882885                cases (H i); #tr1 *; #s1 *; #K #E >K in H2
    883886                >(exec_inf_aux_unfold …)
     
    896899            cases (exec_step ge s');
    897900            [ #o1 #k1 #EXEC' #H whd in EXEC':(?%?) H;
    898                 cases (se_inv … EXEC'); *; #E1 #E2 #H2 destruct (E1 E2);
     901                cases (se_inv … EXEC'); *; #E1 #E2 #H2 destruct (E1 E2); normalize in H2;
    899902                cases (H i); #tr1 *; #s1 *; #K #E >K in H2
    900903                >(exec_inf_aux_unfold …)
  • src/Clight/CexecSound.ma

    r1342 r1350  
    2828
    2929lemma bool_val_distinct: Vtrue ≠ Vfalse.
    30 % #H whd in H:(??%%); destruct; @(absurd ? e0 one_not_zero)
     30% #H whd in H:(??%%); (*Wilmer: XXX*) cases daemon (*destruct; @(absurd ? e0 one_not_zero)*)
    3131qed.
    3232
     
    5151
    5252axiom exec_cast_sound : ∀m:mem. ∀v:val. ∀ty:type. ∀ty':type. ∀v':val. exec_cast m v ty ty' = OK ? v' → cast m v ty ty' v'.
    53 (*#m #v #ty #ty' #v'
     53(*Wilmer: XXXX #m #v #ty #ty' #v'
    5454cases v;
    5555[ #H whd in H:(??%?); destruct;
  • src/Clight/TypeComparison.ma

    r1198 r1350  
    8787        | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
    8888        | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ] ]
    89 ]. destruct; //; qed.
     89]. try destruct // (*Wilmer:XXXX*) cases daemon qed.
    9090
    9191definition assert_type_eq : ∀t1,t2:type. res (t1 = t2) ≝
Note: See TracChangeset for help on using the changeset viewer.