Changeset 15 for C-semantics/Mem.ma


Ignore:
Timestamp:
Jul 22, 2010, 4:50:06 PM (10 years ago)
Author:
campbell
Message:

Make some definitions more normalization friendly by a little 'nlet rec'
abuse.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/Mem.ma

    r14 r15  
    381381      ##|#Hl2;nwhd in ⊢ (??%?);nrewrite > (? : eqZb q p = false)
    382382         ##[nwhd in ⊢ (??%?);napply IH
    383             ##[//
     383            ##[napply Hl2
    384384            ##|(* Hr *) napply daemon ##]
    385385         ##|(*Hl2*)napply daemon ##]
     
    571571  at the given offset in the given block respects the bounds of the block. *)
    572572
    573 ndefinition in_bounds :
    574   ∀m:mem. ∀chunk:memory_chunk. ∀b:block. ∀ofs:Z.
    575     valid_access m chunk b ofs + (¬ valid_access m chunk b ofs).
    576 #m;#chunk;#b;#ofs;
     573(* XXX: Using + and ¬ instead of Sum and Not causes trouble *)
     574nlet rec in_bounds
     575  (m:mem) (chunk:memory_chunk) (b:block) (ofs:Z) on b : 
     576    Sum (valid_access m chunk b ofs) (Not (valid_access m chunk b ofs)) ≝ ?.
    577577napply (Zltb_elim_Type0 b (nextblock m)); #Hnext;
    578578##[ napply (Zleb_elim_Type0 (low_bound m b) ofs); #Hlo;
     
    637637  as a single value [addr], which must be a pointer value. *)
    638638
    639 ndefinition loadv : memory_chunk → mem → val → option val ≝
    640 λchunk,m,addr.
     639nlet rec loadv (chunk:memory_chunk) (m:mem) (addr:val) on addr : option val ≝
    641640  match addr with
    642641  [ Vptr b ofs ⇒ load chunk m b (signed ofs)
     
    16741673ncut (load chunk0 m1 b1 ofs0 = Some ? v1);
    16751674##[ nrewrite < Hload; napply sym_eq; napply (load_store_other … Hstore);
    1676     @1;@1; napply nmk; #eq; nrewrite > eq in Hmi0; nrewrite > Hmi; (* XXX: fails to terminate in reasonable time  ndestruct;*) napply grumpydestruct;
     1675    @1;@1; napply nmk; #eq; nrewrite > eq in Hmi0; nrewrite > Hmi; #H; ndestruct;
    16771676##| #Hload'; napply (Hinj … Hmi0 Hload');
    16781677##] nqed.
     
    17471746        ##[ #e;#e0;#e1;#H; (* similar *)
    17481747            nrewrite > e in Hb1; #Hb1;
    1749             nrewrite > CP in Hb1; #Hb1; (* XXX too long ndestruct;*)
     1748            nrewrite > CP in Hb1; #Hb1; (* XXX ndestruct expands proof state too much;*)
    17501749            nelim (grumpydestruct2 ?????? Hb1);
    17511750            #e2;#e3; nrewrite < e0; nrewrite > e2; nrewrite > e3;
    17521751            @ (load_result chunk' v2);@;
    17531752            ##[ napply (load_store_similar … STORE2); //
    1754             ##| nrewrite > LOAD1 in H; #H; nwhd in H:(??%%);
    1755                 nrewrite > (grumpydestruct1 … H); napply Hvalinj;
    1756                 napply sym_eq; //
     1753            ##| nrewrite > LOAD1 in H; #H; nwhd in H:(??%%); ndestruct;
     1754                napply Hvalinj; //;
    17571755            ##]
    17581756         ##| #Hdis; #H; (* disjoint *)
     
    17631761             nrewrite < LOAD2; napply (load_store_other … STORE2);
    17641762             nelim (decidable_eq_Z b1 b1'); #eb1;
    1765              ##[ nrewrite < eb1 in CP; #CP; nrewrite > CP in Hb1; #eb2d; 
     1763             ##[ nrewrite < eb1 in CP; #CP; nrewrite > CP in Hb1; #eb2d;
    17661764                 nelim (grumpydestruct2 ?????? eb2d); #eb2; #ed;
    17671765                 nelim Hdis; ##[ #Hdis; nelim Hdis;
     
    18911889##| *;*;#A;#B;#C;
    18921890  nrewrite > A in Hbinj' LOAD; #Hbinj'; #LOAD;
    1893   nrewrite > Hbinj in Hbinj'; #bad; (* XXX ndestruct doesn't complete *) nelim (grumpydestruct ?? bad);
     1891  nrewrite > Hbinj in Hbinj'; #bad; ndestruct;
    18941892##] nqed.
    18951893
     
    19141912##| *;*;#A;#B;*;#C;#D;
    19151913    nrewrite > A in Hbinj' LOAD; #Hbinj'; #LOAD; nrewrite > Hbinj in Hbinj';
    1916     #Hbinj'; (* XXX surprised ndestruct can't copy here *) nelim (grumpydestruct2 ?????? Hbinj'); #eb2; #edelta;
     1914    #Hbinj'; (* XXX ndestruct normalizes too much here *) nelim (grumpydestruct2 ?????? Hbinj'); #eb2; #edelta;
    19171915    nrewrite < eb2; nrewrite < edelta;
    19181916    ncut (v1 = Vundef); ##[ napply (load_alloc_same … ALLOC … LOAD) ##]
     
    20172015  ∀m: mem. extends m m.
    20182016#m;@;//;
    2019 nwhd; #chunk;#b1;#ofs;#v1;#b2;#delta;nnormalize in ⊢ (%→?);#H;
    2020 (* XXX: *really* suprised ndestruct didn't complete *) nelim (grumpydestruct2 ?????? H); #eb1;#edelta;#LOAD;
     2017nwhd; #chunk;#b1;#ofs;#v1;#b2;#delta;nnormalize in ⊢ (%→?);#H; 
     2018(* XXX: ndestruct makes the goal unreadable *) nelim (grumpydestruct2 ?????? H); #eb1;#edelta;#LOAD;
    20212019@ v1; @;
    20222020##[ nrewrite < edelta; nrewrite > (Zplus_z_OZ ofs); //;
     
    20552053##| napply (free_parallel_inj … Hinj);
    20562054  ##[ ##2: //;
    2057   ##| ##3: nnormalize; #b';#delta;#ee;
    2058            nelim (grumpydestruct2 ?????? ee); //
     2055  ##| ##3: nnormalize; #b';#delta;#ee; ndestruct; //
    20592056  ##]
    20602057##] nqed.
     
    21052102    #b';#delta;#einj;nnormalize in einj; ndestruct;
    21062103    nelim Houtside;
    2107     ##[ #lo;@ 2; nrewrite > (Zplus_z_OZ ?); //
    2108     ##| #hi;@ 1;  nrewrite > (Zplus_z_OZ ?); //
     2104    ##[ #lo;@ 2; nrewrite > (Zplus_z_OZ ?); /2/
     2105    ##| #hi;@ 1;  nrewrite > (Zplus_z_OZ ?); /2/
    21092106    ##]
    21102107##] nqed.
     
    21622159    ##| #b';#off; napply load_lessdef; //
    21632160    ##]
    2164 ##| #v;#e;nrewrite > e in LOAD; #LOAD; nwhd in LOAD:(??%?); napply False_ind (* XXX otherwise ndestruct takes 30s *); ndestruct
     2161##| #v;#e;nrewrite > e in LOAD; #LOAD; nwhd in LOAD:(??%?); ndestruct;
    21652162##] nqed.
    21662163
     
    21972194##[ #v; #e1;#e2; nrewrite > e1 in STORE; ncases v;
    21982195    ##[ nwhd in ⊢ ((??%?)→?); #H'; napply False_ind; ndestruct;
    2199     ##| ##2,3: #v'; nwhd in ⊢ ((??%?)→?); #H'; napply False_ind; ndestruct;
     2196    ##| ##2,3: #v'; nwhd in ⊢ ((??%?)→?); #H'; ndestruct;
    22002197    ##| #b';#off; napply store_lessdef; //
    22012198    ##]
    2202 ##| #v;#e;nrewrite > e in STORE; #STORE; nwhd in STORE:(??%?); napply False_ind (* XXX otherwise ndestruct fails *); ndestruct
     2199##| #v;#e;nrewrite > e in STORE; #STORE; nwhd in STORE:(??%?); ndestruct
    22032200##] nqed.
    22042201
     
    25152512(* FIXME: the next two cases are very similar *)
    25162513##| #chunk'';#i;#i';*;#echunk;nrewrite > echunk;#Hz;#_;#_;#_;
    2517     nelim chunk'; nwhd in ⊢ ((??%%)→?); #Hsize;
    2518     ##[ ##3,4,5,6,7,10,11,12,13,14: napply False_ind; ndestruct;
    2519     ##| ##2,9: nwhd in ⊢ (??%%); nrewrite > Hz; @
    2520     ##| ##1,8: nwhd in ⊢ (??%%);
    2521         (* XXX: applying the rewrite directly fails with a unification error,
    2522            but establishing the equality then using napplyS works! *)
    2523         nlapply (sign_ext_equal_if_zero_equal … Hz);
    2524         ##[ ##1,3: @; ##[ ##1,3: napply I; ##| ##2,4: napply leb_true_to_le; @; ##]
    2525         ##| ##2,4: #H; napplyS val_inject_int;
    2526         ##]
    2527         (* original version:
    2528         nrewrite > (sign_ext_equal_if_zero_equal … Hz); @; nnormalize;
    2529         ##[ ##1,3: napply I ##| ##2,4: napply leb_true_to_le; @; ##]
    2530         *)
     2514    nelim chunk'; nwhd in ⊢ ((??%%)→?); #Hsize; ndestruct;
     2515    ##[ ##2,4: nwhd in ⊢ (??%%); nrewrite > Hz; @
     2516    ##| ##1,3: nwhd in ⊢ (??%%); nrewrite > (sign_ext_equal_if_zero_equal … Hz);
     2517        @; ##[ ##1,3: napply I; ##| ##2,4: napply leb_true_to_le; @; ##]
    25312518    ##]
    2532 
    25332519##| #chunk'';#i;#i';*;#echunk;nrewrite > echunk;#Hz;#_;#_;#_;
    2534     nelim chunk'; nwhd in ⊢ ((??%%)→?); #Hsize;
    2535     ##[ ##1,2,5,6,7,8,9,12,13,14: napply False_ind; ndestruct;
    2536     ##| ##4,11: nwhd in ⊢ (??%%); nrewrite > Hz; @
    2537     ##| ##3,10: nwhd in ⊢ (??%%);
    2538         (* XXX: actually, napplyS doesn't complete in a reasonable time here;
    2539                 but rewriting on one goal at a time giving the exact position
    2540                 does! *)
    2541         ##[ nrewrite > (sign_ext_equal_if_zero_equal … Hz) in ⊢ (??(?%)?); @;
    2542           ##[ ##1,3: napply I; ##| ##2,4: napply leb_true_to_le; @; ##]
    2543         ##|  nrewrite > (sign_ext_equal_if_zero_equal … Hz) in ⊢ (??(?%)?); @;
    2544           ##[ ##1,3: napply I; ##| ##2,4: napply leb_true_to_le; @; ##]
    2545         ##]
     2520    nelim chunk'; nwhd in ⊢ ((??%%)→?); #Hsize; ndestruct;
     2521    ##[ ##2,4: nwhd in ⊢ (??%%); nrewrite > Hz; @
     2522    ##| ##1,3: nwhd in ⊢ (??%%); nrewrite > (sign_ext_equal_if_zero_equal … Hz);
     2523        @; ##[ ##1,3: napply I; ##| ##2,4: napply leb_true_to_le; @; ##]
    25462524    ##]
    25472525
     
    28112789    nwhd in ⊢ ((??%?)→?→?); napply eqZb_elim; #e; nwhd in ⊢ ((??%?)→?→?);
    28122790    #Hextend;#LOAD;
    2813     ##[ napply False_ind; (* XXX *) napply grumpydestruct; //;
     2791    ##[ ndestruct;
    28142792    ##| nlapply (mi_inj … Hextend LOAD); *; #v2; *; #LOAD2; #VINJ;
    28152793    @ v2; @; //;
     
    29072885    ##| nelim (decidable_eq_Z b1' b2'); #e';
    29082886        ##[ nrewrite < e' in INJb2 ⊢ %; nrewrite < eb1'; nrewrite < eofs1; #INJb2; nlapply (boundmapped … INJb2);
    2909             *; #H; @2; /2/;
     2887            *; #H; @2; ##[ @2 ##| @1 ##] napply H;
    29102888        ##| @1;@1;@1; napply e'
    29112889        ##]
    29122890    ##| nelim (decidable_eq_Z b1' b2'); #e';
    29132891        ##[ nrewrite < e' in INJb2 ⊢ %; #INJb2; nelim (grumpydestruct2 ?????? INJb2); #eb'; #eofs; nrewrite < eb' in INJb1; nrewrite < eofs; #INJb1; nlapply (boundmapped … INJb1);
    2914             *; #H; @2; /2/;
     2892            *; #H; @2; ##[ @1; /2/ ##| @2; napply H; ##]
    29152893        ##| @1;@1;@1; napply e'
    29162894        ##]
     
    30343012  alloc_init_data m id = 〈m', b〉 →
    30353013  mem_inject_neutral m'.
    3036 #m;#id;#m';#b;#Hneutral;#INIT; nwhd in INIT:(??%?); (* XXX: ndestruct too long*)
     3014#m;#id;#m';#b;#Hneutral;#INIT; nwhd in INIT:(??%?); (* XXX: ndestruct makes a bit of a mess *)
    30373015napply (pairdisc_elim … INIT);
    30383016nwhd in ⊢ (??%% → ?);#B;nrewrite < B in ⊢ (??%% → ?);
     
    34493427    napply eqZb_elim; #eb0; nrewrite > eb;
    34503428    ##[ nrewrite > eb0; #ed; nrewrite < (grumpydestruct1 ??? ed);
    3451         nrewrite > (eqZb_z_z ?); /2/;
     3429        nrewrite > (eqZb_z_z ?); /3/;
    34523430    ##| #edelta0; nrewrite > (eqZb_false … eb0);
    34533431        napply ms_range_2; nwhd in edelta0:(??%?); //;
     
    35093487##[ ##1,3,4: //;
    35103488##| #i; nwhd in ⊢ (??(??%)(??%));
    3511      (* XXX: need to specify which side of the equality to rewrite on to avoid
    3512              a unification assertion. *)
    3513     nrewrite > (sign_ext_zero_ext ?? i) in ⊢ (???%); ##[ napply refl; (* XXX: // ? *)
     3489    nrewrite > (sign_ext_zero_ext ?? i); ##[ napply refl; (* XXX: // ? *)
    35143490    ##| (* arith *) napply daemon;
    35153491    ##]
Note: See TracChangeset for help on using the changeset viewer.