Changeset 10 for C-semantics/Mem.ma


Ignore:
Timestamp:
Jul 6, 2010, 11:53:23 AM (9 years ago)
Author:
campbell
Message:

Add binary arithmetic libraries, use for integers and identifiers (but
we're not doing modular arithmetic yet.)
Add a dummy "tree" implementation to make environment lookups executable.
Fix if .. then .. else .. precedence.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/Mem.ma

    r9 r10  
    2525*)
    2626
    27 include "arithmetics/Z.ma".
     27include "arithmetics/nat.ma".
     28include "binary/Z.ma".
    2829include "datatypes/sums.ma".
    2930include "datatypes/list.ma".
     
    127128  | Mfloat64 => 7].
    128129
     130alias symbol "plus" (instance 2) = "integer plus".
    129131nlemma size_chunk_pred:
    130132  ∀chunk. size_chunk chunk = 1 + pred_size_chunk chunk.
     
    164166nlemma align_size_chunk_divides:
    165167  ∀chunk. (align_chunk chunk ∣ size_chunk chunk).
    166 #chunk;ncases chunk;nnormalize;@;//;##[ napply 2; ##| // ##]
     168#chunk;ncases chunk;nnormalize;/3/;
    167169nqed.
    168170
     
    176178(* The initial store. *)
    177179
    178 ndefinition oneZ ≝ pos O.
     180ndefinition oneZ ≝ pos one.
    179181
    180182nremark one_pos: OZ < oneZ.
     
    186188
    187189ndefinition empty: mem ≝
    188   mk_mem (λx.empty_block OZ OZ) (pos O) one_pos.
     190  mk_mem (λx.empty_block OZ OZ) (pos one) one_pos.
    189191
    190192ndefinition nullptr: block ≝ OZ.
     
    501503nchange in ⊢ (??(???%)?) with (update ????);
    502504nwhd in ⊢(??%?);nrewrite > (update_s content …);
    503 nwhd in ⊢(??%?);nrewrite > (not_eq_to_eqb_false …);//;napply sym_neq;//;
     505nwhd in ⊢(??%?);nrewrite > (not_eq_to_eqb_false … (sym_neq … H));//;
    504506nqed.
    505507
     
    512514nlapply (eqZb_to_Prop p1 p2); ncases (eqZb p1 p2); #Hp;
    513515##[nrewrite > Hp;
    514    nlapply (eqb_to_Prop n1 n2);ncases (eqb n1 n2); #Hn;
     516   napply (eqb_elim n1 n2); #Hn;
    515517   ##[nrewrite > Hn;@; @; //;
    516518   ##|@2;/2/]
     
    10551057##|nrewrite > (size_chunk_pred …) in H1;nrewrite > (size_chunk_pred …);
    10561058   #H1;napply nmk;#Hfalse;nelim H1;#H4;napply H4;
    1057    napply (eq_f ?? (λx.Z_of_nat (1 + x)) ???);//##]
     1059   napply (eq_f ?? (λx.1 + x) ???);//##]
    10581060nqed.
    10591061
     
    15821584    ##| napply (Zleb_true_to_Zle … H2)
    15831585    ##| nwhd in ⊢ (?(??%)?); (* arith, Zleb_true_to_Zle *) napply daemon
    1584     ##| napply (witness ?? (abs ofs)); nnormalize; nrewrite > (Zplus_z_OZ ?); //
     1586    ##| ncases ofs; /2/;
    15851587    ##]
    15861588##| *; #Hval;#Hlo;#Hhi;#Hal;
     
    16991701##| #ineq; @1; @1; napply ineq;
    17001702##] nqed.
    1701 
     1703(*  XXX: reenable once I've sorted out performance a bit
    17021704ndefinition meminj_no_overlap ≝ λmi: meminj. λm: mem.
    17031705  ∀b1,b1',delta1,b2,b2',delta2.
     
    23652367    ##]
    23662368##] nqed.
    2367 (*  XXX: reenable once I've sorted out Integers.ma a bit
     2369
    23682370nlemma valid_pointer_inject_no_overflow:
    23692371  ∀f,m1,m2,b,ofs,b',x.
Note: See TracChangeset for help on using the changeset viewer.