Ignore:
Timestamp:
Feb 9, 2011, 11:49:17 AM (10 years ago)
Author:
campbell
Message:

Port Clight semantics to the new-new matita syntax.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.1/C-semantics/Values.ma

    r484 r487  
    2222include "Floats.ma".
    2323
    24 include "Plogic/connectives.ma".
    25 
    26 ndefinition block ≝ Z.
    27 (*ndefinition eq_block ≝ zeq.*)
     24include "basics/logic.ma".
     25
     26definition block ≝ Z.
     27(*definition eq_block ≝ zeq.*)
    2828
    2929(* * A value is either:
     
    3838*)
    3939
    40 ninductive val: Type[0] ≝
     40inductive val: Type[0] ≝
    4141  | Vundef: val
    4242  | Vint: int → val
     
    4545  | Vptr: region → block → int → val.
    4646
    47 ndefinition Vzero: val ≝ Vint zero.
    48 ndefinition Vone: val ≝ Vint one.
    49 ndefinition Vmone: val ≝ Vint mone.
    50 
    51 ndefinition Vtrue: val ≝ Vint one.
    52 ndefinition Vfalse: val ≝ Vint zero.
     47definition Vzero: val ≝ Vint zero.
     48definition Vone: val ≝ Vint one.
     49definition Vmone: val ≝ Vint mone.
     50
     51definition Vtrue: val ≝ Vint one.
     52definition Vfalse: val ≝ Vint zero.
    5353
    5454(*
     
    5959Module Val.
    6060*)
    61 ndefinition of_bool : bool → val ≝ λb. if b then Vtrue else Vfalse.
     61definition of_bool : bool → val ≝ λb. if b then Vtrue else Vfalse.
    6262(*
    63 ndefinition has_type ≝ λv: val. λt: typ.
     63definition has_type ≝ λv: val. λt: typ.
    6464  match v with
    6565  [ Vundef ⇒ True
     
    7070  ].
    7171
    72 nlet rec has_type_list (vl: list val) (tl: list typ) on vl : Prop ≝
     72let rec has_type_list (vl: list val) (tl: list typ) on vl : Prop ≝
    7373  match vl with
    7474  [ nil ⇒ match tl with [ nil ⇒ True | _ ⇒ False ]
     
    8181  [Vundef] and floats are neither true nor false. *)
    8282
    83 ndefinition is_true : val → Prop ≝ λv.
     83definition is_true : val → Prop ≝ λv.
    8484  match v with
    8585  [ Vint n ⇒ n ≠ zero
     
    8888  ].
    8989
    90 ndefinition is_false : val → Prop ≝ λv.
     90definition is_false : val → Prop ≝ λv.
    9191  match v with
    9292  [ Vint n ⇒ n = zero
     
    9595  ].
    9696
    97 ninductive bool_of_val: val → bool → Prop ≝
     97inductive bool_of_val: val → bool → Prop ≝
    9898  | bool_of_val_int_true:
    9999      ∀n. n ≠ zero → bool_of_val (Vint n) true
     
    105105      ∀r. bool_of_val (Vnull r) true.
    106106
    107 ndefinition neg : val → val ≝ λv.
     107definition neg : val → val ≝ λv.
    108108  match v with
    109109  [ Vint n ⇒ Vint (neg n)
     
    111111  ].
    112112
    113 ndefinition negf : val → val ≝ λv.
     113definition negf : val → val ≝ λv.
    114114  match v with
    115115  [ Vfloat f ⇒ Vfloat (Fneg f)
     
    117117  ].
    118118
    119 ndefinition absf : val → val ≝ λv.
     119definition absf : val → val ≝ λv.
    120120  match v with
    121121  [ Vfloat f ⇒ Vfloat (Fabs f)
     
    123123  ].
    124124
    125 ndefinition intoffloat : val → val ≝ λv.
     125definition intoffloat : val → val ≝ λv.
    126126  match v with
    127127  [ Vfloat f ⇒ Vint (intoffloat f)
     
    129129  ].
    130130
    131 ndefinition intuoffloat : val → val ≝ λv.
     131definition intuoffloat : val → val ≝ λv.
    132132  match v with
    133133  [ Vfloat f ⇒ Vint (intuoffloat f)
     
    135135  ].
    136136
    137 ndefinition floatofint : val → val ≝ λv.
     137definition floatofint : val → val ≝ λv.
    138138  match v with
    139139  [ Vint n ⇒ Vfloat (floatofint n)
     
    141141  ].
    142142
    143 ndefinition floatofintu : val → val ≝ λv.
     143definition floatofintu : val → val ≝ λv.
    144144  match v with
    145145  [ Vint n ⇒ Vfloat (floatofintu n)
     
    147147  ].
    148148
    149 ndefinition notint : val → val ≝ λv.
     149definition notint : val → val ≝ λv.
    150150  match v with
    151151  [ Vint n ⇒ Vint (xor n mone)
     
    154154 
    155155(* FIXME: switch to alias, or rename, or … *)
    156 ndefinition int_eq : int → int → bool ≝ eq.
    157 ndefinition notbool : val → val ≝ λv.
     156definition int_eq : int → int → bool ≝ eq.
     157definition notbool : val → val ≝ λv.
    158158  match v with
    159159  [ Vint n ⇒ of_bool (int_eq n zero)
     
    163163  ].
    164164
    165 ndefinition zero_ext ≝ λnbits: Z. λv: val.
     165definition zero_ext ≝ λnbits: Z. λv: val.
    166166  match v with
    167167  [ Vint n ⇒ Vint (zero_ext nbits n)
     
    169169  ].
    170170
    171 ndefinition sign_ext ≝ λnbits:Z. λv:val.
     171definition sign_ext ≝ λnbits:Z. λv:val.
    172172  match v with
    173173  [ Vint i ⇒ Vint (sign_ext nbits i)
     
    175175  ].
    176176
    177 ndefinition singleoffloat : val → val ≝ λv.
     177definition singleoffloat : val → val ≝ λv.
    178178  match v with
    179179  [ Vfloat f ⇒ Vfloat (singleoffloat f)
     
    182182
    183183(* TODO: add zero to null? *)
    184 ndefinition add ≝ λv1,v2: val.
     184definition add ≝ λv1,v2: val.
    185185  match v1 with
    186186  [ Vint n1 ⇒ match v2 with
     
    193193  | _ ⇒ Vundef ].
    194194
    195 ndefinition sub ≝ λv1,v2: val.
     195definition sub ≝ λv1,v2: val.
    196196  match v1 with
    197197  [ Vint n1 ⇒ match v2 with
     
    206206  | _ ⇒ Vundef ].
    207207
    208 ndefinition mul ≝ λv1, v2: val.
     208definition mul ≝ λv1, v2: val.
    209209  match v1 with
    210210  [ Vint n1 ⇒ match v2 with
     
    213213  | _ ⇒ Vundef ].
    214214(*
    215 ndefinition divs ≝ λv1, v2: val.
     215definition divs ≝ λv1, v2: val.
    216216  match v1 with
    217217  [ Vint n1 ⇒ match v2 with
     
    241241  end.
    242242*)
    243 ndefinition v_and ≝ λv1, v2: val.
     243definition v_and ≝ λv1, v2: val.
    244244  match v1 with
    245245  [ Vint n1 ⇒ match v2 with
     
    248248  | _ ⇒ Vundef ].
    249249
    250 ndefinition or ≝ λv1, v2: val.
     250definition or ≝ λv1, v2: val.
    251251  match v1 with
    252252  [ Vint n1 ⇒ match v2 with
     
    255255  | _ ⇒ Vundef ].
    256256
    257 ndefinition xor ≝ λv1, v2: val.
     257definition xor ≝ λv1, v2: val.
    258258  match v1 with
    259259  [ Vint n1 ⇒ match v2 with
     
    322322  end.
    323323*)
    324 ndefinition addf ≝ λv1,v2: val.
     324definition addf ≝ λv1,v2: val.
    325325  match v1 with
    326326  [ Vfloat f1 ⇒ match v2 with
     
    329329  | _ ⇒ Vundef ].
    330330
    331 ndefinition subf ≝ λv1,v2: val.
     331definition subf ≝ λv1,v2: val.
    332332  match v1 with
    333333  [ Vfloat f1 ⇒ match v2 with
     
    336336  | _ ⇒ Vundef ].
    337337
    338 ndefinition mulf ≝ λv1,v2: val.
     338definition mulf ≝ λv1,v2: val.
    339339  match v1 with
    340340  [ Vfloat f1 ⇒ match v2 with
     
    343343  | _ ⇒ Vundef ].
    344344
    345 ndefinition divf ≝ λv1,v2: val.
     345definition divf ≝ λv1,v2: val.
    346346  match v1 with
    347347  [ Vfloat f1 ⇒ match v2 with
     
    350350  | _ ⇒ Vundef ].
    351351
    352 ndefinition cmp_match : comparison → val ≝ λc.
     352definition cmp_match : comparison → val ≝ λc.
    353353  match c with
    354354  [ Ceq ⇒ Vtrue
     
    357357  ].
    358358
    359 ndefinition cmp_mismatch : comparison → val ≝ λc.
     359definition cmp_mismatch : comparison → val ≝ λc.
    360360  match c with
    361361  [ Ceq ⇒ Vfalse
     
    365365
    366366(* TODO: consider whether to check pointer representations *)
    367 ndefinition cmp ≝ λc: comparison. λv1,v2: val.
     367definition cmp ≝ λc: comparison. λv1,v2: val.
    368368  match v1 with
    369369  [ Vint n1 ⇒ match v2 with
     
    384384  | _ ⇒ Vundef ].
    385385
    386 ndefinition cmpu ≝ λc: comparison. λv1,v2: val.
     386definition cmpu ≝ λc: comparison. λv1,v2: val.
    387387  match v1 with
    388388  [ Vint n1 ⇒ match v2 with
     
    403403  | _ ⇒ Vundef ].
    404404
    405 ndefinition cmpf ≝ λc: comparison. λv1,v2: val.
     405definition cmpf ≝ λc: comparison. λv1,v2: val.
    406406  match v1 with
    407407  [ Vfloat f1 ⇒ match v2 with
     
    419419  (e.g. reading back a float as a [Mint32]) read back as [Vundef]. *)
    420420
    421 nlet rec load_result (chunk: memory_chunk) (v: val) ≝
     421let rec load_result (chunk: memory_chunk) (v: val) ≝
    422422  match v with
    423423  [ Vint n ⇒
     
    10001000    less defined than any value. *)
    10011001
    1002 ninductive Val_lessdef: val → val → Prop ≝
     1002inductive Val_lessdef: val → val → Prop ≝
    10031003  | lessdef_refl: ∀v. Val_lessdef v v
    10041004  | lessdef_undef: ∀v. Val_lessdef Vundef v.
    10051005
    1006 ninductive lessdef_list: list val → list val → Prop ≝
     1006inductive lessdef_list: list val → list val → Prop ≝
    10071007  | lessdef_list_nil:
    10081008      lessdef_list (nil ?) (nil ?)
     
    10131013
    10141014(*Hint Resolve lessdef_refl lessdef_undef lessdef_list_nil lessdef_list_cons.*)
    1015 
    1016 nlemma lessdef_list_inv:
     1015(*
     1016lemma lessdef_list_inv:
    10171017  ∀vl1,vl2. lessdef_list vl1 vl2 → vl1 = vl2 ∨ in_list ? Vundef vl1.
    1018 #vl1; nelim vl1;
    1019 ##[ #vl2; #H; ninversion H; /2/; #h1;#h2;#t1;#t2;#H1;#H2;#H3;#Hbad; ndestruct
    1020 ##| #h;#t;#IH;#vl2;#H;
    1021     ninversion H;
    1022     ##[ #H'; ndestruct
    1023     ##| #h1;#h2;#t1;#t2;#H1;#H2;#H3;#e1;#e2; ndestruct;
    1024         nelim H1;
    1025         ##[ nelim (IH t2 H2);
    1026             ##[ #e; ndestruct; /2/;
    1027             ##| /3/ ##]
    1028         ##| /3/ ##]
    1029     ##]
    1030 ##] nqed.
    1031 
    1032 nlemma load_result_lessdef:
     1018#vl1 elim vl1;
     1019[ #vl2 #H inversion H; /2/; #h1 #h2 #t1 #t2 #H1 #H2 #H3 #Hbad destruct
     1020| #h #t #IH #vl2 #H
     1021    inversion H;
     1022    [ #H' destruct
     1023    | #h1 #h2 #t1 #t2 #H1 #H2 #H3 #e1 #e2 destruct;
     1024        elim H1;
     1025        [ elim (IH t2 H2);
     1026            [ #e destruct; /2/;
     1027            | /3/ ]
     1028        | /3/ ]
     1029    ]
     1030] qed.
     1031*)
     1032lemma load_result_lessdef:
    10331033  ∀chunk,v1,v2.
    10341034  Val_lessdef v1 v2 → Val_lessdef (load_result chunk v1) (load_result chunk v2).
    1035 #chunk;#v1;#v2;#H; ninversion H; //; #v e1 e2; ncases chunk;
    1036 ##[ ##8: #r ##] nwhd in ⊢ (?%?); //;
    1037 nqed.
     1035#chunk #v1 #v2 #H inversion H; //; #v #e1 #e2 cases chunk
     1036[ 8: #r ] whd in ⊢ (?%?); //;
     1037qed.
    10381038
    10391039(*
     
    10441044Qed.
    10451045*)
    1046 nlemma sign_ext_lessdef:
     1046lemma sign_ext_lessdef:
    10471047  ∀n,v1,v2. Val_lessdef v1 v2 → Val_lessdef (sign_ext n v1) (sign_ext n v2).
    1048 #n;#v1;#v2;#H;ninversion H;//;#v;#e1;#e2;nrewrite < e1 in H; nrewrite > e2; //;
    1049 nqed.
     1048#n #v1 #v2 #H inversion H;//;#v #e1 #e2 <e1 in H >e2 //;
     1049qed.
    10501050(*
    10511051Lemma singleoffloat_lessdef:
Note: See TracChangeset for help on using the changeset viewer.