Ignore:
Timestamp:
Oct 19, 2011, 11:54:13 AM (8 years ago)
Author:
campbell
Message:

Remove a few old workarounds.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/CexecSound.ma

    r1350 r1410  
    11include "Clight/Cexec.ma".
    22
    3 (*include "Plogic/connectives.ma".*)
    4 
    5 (* Is rather careful about using destruct because it currently uses excessive
    6    normalization. *)
    73lemma exec_bool_of_val_sound: ∀v,ty,r.
    84 exec_bool_of_val v ty = OK ? r → bool_of_val v ty (of_bool r).
     
    1511  | *; whd @eq_bv_elim
    1612    [ #E1 #E2 destruct @bool_of_val_false @is_false_int
    17     | #E1 #E2 >(?:r=¬false) [ @bool_of_val_true @is_true_int_int @E1 | destruct @refl ]
     13    | #E1 #E2 destruct @bool_of_val_true @is_true_int_int @E1
    1814    ]
    1915  ]
    2016| 8: #H cases (eq_dec f Fzero)
    2117  [ #e >e in H ⊢ % >Feq_zero_true #E destruct @bool_of_val_false @is_false_float
    22   | #ne >Feq_zero_false in H // #E >(?:r=¬false) [ @bool_of_val_true @is_true_float @ne | destruct @refl ]
    23   ]
    24 | 14: #H >(?:r=false) [ @bool_of_val_false @is_false_pointer | destruct @refl ]
    25 | 15: #H >(?:r=true) [ @bool_of_val_true @is_true_pointer_pointer | destruct @refl ]
     18  | #ne >Feq_zero_false in H // #E destruct @bool_of_val_true @is_true_float @ne
     19  ]
     20| 14: #H destruct @bool_of_val_false @is_false_pointer
     21| 15: #H destruct @bool_of_val_true @is_true_pointer_pointer
    2622| *: #H destruct
    2723] qed.
    2824
    2925lemma bool_val_distinct: Vtrue ≠ Vfalse.
    30 % #H whd in H:(??%%); (*Wilmer: XXX*) cases daemon (*destruct; @(absurd ? e0 one_not_zero)*)
     26% normalize #H destruct
    3127qed.
    3228
     
    5046qed.
    5147
    52 axiom 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 (*Wilmer: XXXX #m #v #ty #ty' #v'
     48lemma 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'.
     49#m #v #ty #ty' #v'
    5450cases v;
    5551[ #H whd in H:(??%?); destruct;
     
    122118        ]
    123119    ]
    124 ] qed.*)
     120] qed.
    125121
    126122let rec expr_lvalue_ind
     
    194190(P_res ? (λx.eval_expr ge en m e (\fst x) (\snd x)) (exec_expr ge en m e)).
    195191#ge #en #m #e @(expr_lvalue_ind ? (λe',ty.P_res ? (λr.eval_lvalue ge en m (Expr e' ty) (\fst (\fst r)) (\snd (\fst r)) (\snd r)) (exec_lvalue' ge en m e' ty)) … e)
    196 (* XXX // fails [ 1,2: #ty #c whd //  *)
    197192[ #sz #ty #c whd in ⊢ (???%) cases ty try #sz' try #sg try #x try @I whd in ⊢ (???%)
    198193  @eq_intsize_elim #E try @I <E whd %
    199 | #ty #c whd %2
     194| #ty #c whd //
    200195(* expressions that are lvalues *)
    201196| #e' #ty cases e'; //; [ #i #He' | #e #He' | #e #i #He' ] whd in He' ⊢ %;
     
    263258        [ @(bool_of … Hb1) | @(exec_bool_of_val_sound … eb2) ]
    264259    ]
    265 | #ty #ty' cases ty try #sz try #sg try #x try @I whd; (* XXX //*) @eval_Esizeof
     260| #ty #ty' cases ty try #sz try #sg try #x //
    266261| #ty #e' #ty' #i cases ty'; //;
    267262    [ #id #fs #He' @bind2_OK #x cases x; #sp #l #ofs #H
     
    337332lemma exec_exprlist_sound: ∀ge,e,m,l. P_res ? (λvltr:list val×trace. eval_exprlist ge e m l (\fst vltr) (\snd vltr)) (exec_exprlist ge e m l).
    338333#ge #e #m #l elim l;
    339  whd; (* XXX //; *)
     334 whd
    340335[ %
    341336| #e1 #es #IH
     
    402397        //; #H whd;
    403398        @step_skip_call //;
    404     | #s' #k' whd; (* XXX //; *) @step_skip_seq
     399    | #s' #k' whd; //
    405400    | #ex #s' #k' @step_skip_or_continue_while % //;
    406401    | #ex #s' #k'
     
    442437        whd; @(step_call_some … (exec_lvalue_sound' … Hlocofs) Hvf Hvargs efd ety)
    443438    ]
    444   | #s1 #s2 whd; (* XXX //; *) @step_seq
     439  | #s1 #s2 //
    445440  | #ex #s1 #s2
    446441    @res_bindIO2_OK #v #tr #Hv
     
    459454    | @(step_while_false … (exec_expr_sound' … Hv)) @(bool_of … Hb)
    460455    ]
    461   | #ex #s' whd; (* XXX //; *) @step_dowhile
     456  | #ex #s' //
    462457  | #s1 #ex #s2 #s3 whd in ⊢ (?????%); elim (is_Sskip s1); #Hs1 whd in ⊢ (?????%);
    463458    [ >Hs1
     
    495490  | #ex #ls @res_bindIO2_OK * // #sz #n #tr #Hv
    496491    @step_switch @(exec_expr_sound' … Hv)
    497   | #l #s' whd; @step_label (* XXX //; *)
     492  | #l #s' //
    498493  | #l whd in ⊢ (?????%); lapply (refl ? (find_label l (fn_body f) (call_cont k)));
    499494      cases (find_label l (fn_body f) (call_cont k)) in ⊢ (???% → %); //;
    500495      #sk cases sk; #s' #k' #H
    501496      @(step_goto … H)
    502   | #l #s' whd; (* XXX //; *) @step_cost
     497  | #l #s' //
    503498  ]
    504499| #f0 #vargs #k #m whd in ⊢ (?????%); cases f0;
Note: See TracChangeset for help on using the changeset viewer.