Changeset 487 for Deliverables/D3.1/Csemantics/Values.ma
 Timestamp:
 Feb 9, 2011, 11:49:17 AM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D3.1/Csemantics/Values.ma
r484 r487 22 22 include "Floats.ma". 23 23 24 include " Plogic/connectives.ma".25 26 ndefinition block ≝ Z.27 (* ndefinition eq_block ≝ zeq.*)24 include "basics/logic.ma". 25 26 definition block ≝ Z. 27 (*definition eq_block ≝ zeq.*) 28 28 29 29 (* * A value is either: … … 38 38 *) 39 39 40 ninductive val: Type[0] ≝40 inductive val: Type[0] ≝ 41 41  Vundef: val 42 42  Vint: int → val … … 45 45  Vptr: region → block → int → val. 46 46 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.47 definition Vzero: val ≝ Vint zero. 48 definition Vone: val ≝ Vint one. 49 definition Vmone: val ≝ Vint mone. 50 51 definition Vtrue: val ≝ Vint one. 52 definition Vfalse: val ≝ Vint zero. 53 53 54 54 (* … … 59 59 Module Val. 60 60 *) 61 ndefinition of_bool : bool → val ≝ λb. if b then Vtrue else Vfalse.61 definition of_bool : bool → val ≝ λb. if b then Vtrue else Vfalse. 62 62 (* 63 ndefinition has_type ≝ λv: val. λt: typ.63 definition has_type ≝ λv: val. λt: typ. 64 64 match v with 65 65 [ Vundef ⇒ True … … 70 70 ]. 71 71 72 nlet rec has_type_list (vl: list val) (tl: list typ) on vl : Prop ≝72 let rec has_type_list (vl: list val) (tl: list typ) on vl : Prop ≝ 73 73 match vl with 74 74 [ nil ⇒ match tl with [ nil ⇒ True  _ ⇒ False ] … … 81 81 [Vundef] and floats are neither true nor false. *) 82 82 83 ndefinition is_true : val → Prop ≝ λv.83 definition is_true : val → Prop ≝ λv. 84 84 match v with 85 85 [ Vint n ⇒ n ≠ zero … … 88 88 ]. 89 89 90 ndefinition is_false : val → Prop ≝ λv.90 definition is_false : val → Prop ≝ λv. 91 91 match v with 92 92 [ Vint n ⇒ n = zero … … 95 95 ]. 96 96 97 ninductive bool_of_val: val → bool → Prop ≝97 inductive bool_of_val: val → bool → Prop ≝ 98 98  bool_of_val_int_true: 99 99 ∀n. n ≠ zero → bool_of_val (Vint n) true … … 105 105 ∀r. bool_of_val (Vnull r) true. 106 106 107 ndefinition neg : val → val ≝ λv.107 definition neg : val → val ≝ λv. 108 108 match v with 109 109 [ Vint n ⇒ Vint (neg n) … … 111 111 ]. 112 112 113 ndefinition negf : val → val ≝ λv.113 definition negf : val → val ≝ λv. 114 114 match v with 115 115 [ Vfloat f ⇒ Vfloat (Fneg f) … … 117 117 ]. 118 118 119 ndefinition absf : val → val ≝ λv.119 definition absf : val → val ≝ λv. 120 120 match v with 121 121 [ Vfloat f ⇒ Vfloat (Fabs f) … … 123 123 ]. 124 124 125 ndefinition intoffloat : val → val ≝ λv.125 definition intoffloat : val → val ≝ λv. 126 126 match v with 127 127 [ Vfloat f ⇒ Vint (intoffloat f) … … 129 129 ]. 130 130 131 ndefinition intuoffloat : val → val ≝ λv.131 definition intuoffloat : val → val ≝ λv. 132 132 match v with 133 133 [ Vfloat f ⇒ Vint (intuoffloat f) … … 135 135 ]. 136 136 137 ndefinition floatofint : val → val ≝ λv.137 definition floatofint : val → val ≝ λv. 138 138 match v with 139 139 [ Vint n ⇒ Vfloat (floatofint n) … … 141 141 ]. 142 142 143 ndefinition floatofintu : val → val ≝ λv.143 definition floatofintu : val → val ≝ λv. 144 144 match v with 145 145 [ Vint n ⇒ Vfloat (floatofintu n) … … 147 147 ]. 148 148 149 ndefinition notint : val → val ≝ λv.149 definition notint : val → val ≝ λv. 150 150 match v with 151 151 [ Vint n ⇒ Vint (xor n mone) … … 154 154 155 155 (* FIXME: switch to alias, or rename, or … *) 156 ndefinition int_eq : int → int → bool ≝ eq.157 ndefinition notbool : val → val ≝ λv.156 definition int_eq : int → int → bool ≝ eq. 157 definition notbool : val → val ≝ λv. 158 158 match v with 159 159 [ Vint n ⇒ of_bool (int_eq n zero) … … 163 163 ]. 164 164 165 ndefinition zero_ext ≝ λnbits: Z. λv: val.165 definition zero_ext ≝ λnbits: Z. λv: val. 166 166 match v with 167 167 [ Vint n ⇒ Vint (zero_ext nbits n) … … 169 169 ]. 170 170 171 ndefinition sign_ext ≝ λnbits:Z. λv:val.171 definition sign_ext ≝ λnbits:Z. λv:val. 172 172 match v with 173 173 [ Vint i ⇒ Vint (sign_ext nbits i) … … 175 175 ]. 176 176 177 ndefinition singleoffloat : val → val ≝ λv.177 definition singleoffloat : val → val ≝ λv. 178 178 match v with 179 179 [ Vfloat f ⇒ Vfloat (singleoffloat f) … … 182 182 183 183 (* TODO: add zero to null? *) 184 ndefinition add ≝ λv1,v2: val.184 definition add ≝ λv1,v2: val. 185 185 match v1 with 186 186 [ Vint n1 ⇒ match v2 with … … 193 193  _ ⇒ Vundef ]. 194 194 195 ndefinition sub ≝ λv1,v2: val.195 definition sub ≝ λv1,v2: val. 196 196 match v1 with 197 197 [ Vint n1 ⇒ match v2 with … … 206 206  _ ⇒ Vundef ]. 207 207 208 ndefinition mul ≝ λv1, v2: val.208 definition mul ≝ λv1, v2: val. 209 209 match v1 with 210 210 [ Vint n1 ⇒ match v2 with … … 213 213  _ ⇒ Vundef ]. 214 214 (* 215 ndefinition divs ≝ λv1, v2: val.215 definition divs ≝ λv1, v2: val. 216 216 match v1 with 217 217 [ Vint n1 ⇒ match v2 with … … 241 241 end. 242 242 *) 243 ndefinition v_and ≝ λv1, v2: val.243 definition v_and ≝ λv1, v2: val. 244 244 match v1 with 245 245 [ Vint n1 ⇒ match v2 with … … 248 248  _ ⇒ Vundef ]. 249 249 250 ndefinition or ≝ λv1, v2: val.250 definition or ≝ λv1, v2: val. 251 251 match v1 with 252 252 [ Vint n1 ⇒ match v2 with … … 255 255  _ ⇒ Vundef ]. 256 256 257 ndefinition xor ≝ λv1, v2: val.257 definition xor ≝ λv1, v2: val. 258 258 match v1 with 259 259 [ Vint n1 ⇒ match v2 with … … 322 322 end. 323 323 *) 324 ndefinition addf ≝ λv1,v2: val.324 definition addf ≝ λv1,v2: val. 325 325 match v1 with 326 326 [ Vfloat f1 ⇒ match v2 with … … 329 329  _ ⇒ Vundef ]. 330 330 331 ndefinition subf ≝ λv1,v2: val.331 definition subf ≝ λv1,v2: val. 332 332 match v1 with 333 333 [ Vfloat f1 ⇒ match v2 with … … 336 336  _ ⇒ Vundef ]. 337 337 338 ndefinition mulf ≝ λv1,v2: val.338 definition mulf ≝ λv1,v2: val. 339 339 match v1 with 340 340 [ Vfloat f1 ⇒ match v2 with … … 343 343  _ ⇒ Vundef ]. 344 344 345 ndefinition divf ≝ λv1,v2: val.345 definition divf ≝ λv1,v2: val. 346 346 match v1 with 347 347 [ Vfloat f1 ⇒ match v2 with … … 350 350  _ ⇒ Vundef ]. 351 351 352 ndefinition cmp_match : comparison → val ≝ λc.352 definition cmp_match : comparison → val ≝ λc. 353 353 match c with 354 354 [ Ceq ⇒ Vtrue … … 357 357 ]. 358 358 359 ndefinition cmp_mismatch : comparison → val ≝ λc.359 definition cmp_mismatch : comparison → val ≝ λc. 360 360 match c with 361 361 [ Ceq ⇒ Vfalse … … 365 365 366 366 (* TODO: consider whether to check pointer representations *) 367 ndefinition cmp ≝ λc: comparison. λv1,v2: val.367 definition cmp ≝ λc: comparison. λv1,v2: val. 368 368 match v1 with 369 369 [ Vint n1 ⇒ match v2 with … … 384 384  _ ⇒ Vundef ]. 385 385 386 ndefinition cmpu ≝ λc: comparison. λv1,v2: val.386 definition cmpu ≝ λc: comparison. λv1,v2: val. 387 387 match v1 with 388 388 [ Vint n1 ⇒ match v2 with … … 403 403  _ ⇒ Vundef ]. 404 404 405 ndefinition cmpf ≝ λc: comparison. λv1,v2: val.405 definition cmpf ≝ λc: comparison. λv1,v2: val. 406 406 match v1 with 407 407 [ Vfloat f1 ⇒ match v2 with … … 419 419 (e.g. reading back a float as a [Mint32]) read back as [Vundef]. *) 420 420 421 nlet rec load_result (chunk: memory_chunk) (v: val) ≝421 let rec load_result (chunk: memory_chunk) (v: val) ≝ 422 422 match v with 423 423 [ Vint n ⇒ … … 1000 1000 less defined than any value. *) 1001 1001 1002 ninductive Val_lessdef: val → val → Prop ≝1002 inductive Val_lessdef: val → val → Prop ≝ 1003 1003  lessdef_refl: ∀v. Val_lessdef v v 1004 1004  lessdef_undef: ∀v. Val_lessdef Vundef v. 1005 1005 1006 ninductive lessdef_list: list val → list val → Prop ≝1006 inductive lessdef_list: list val → list val → Prop ≝ 1007 1007  lessdef_list_nil: 1008 1008 lessdef_list (nil ?) (nil ?) … … 1013 1013 1014 1014 (*Hint Resolve lessdef_refl lessdef_undef lessdef_list_nil lessdef_list_cons.*) 1015 1016 nlemma lessdef_list_inv:1015 (* 1016 lemma lessdef_list_inv: 1017 1017 ∀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; ndestruct1020 ## #h;#t;#IH;#vl2;#H; 1021 ninversion H;1022 ##[ #H'; ndestruct1023 ## #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 *) 1032 lemma load_result_lessdef: 1033 1033 ∀chunk,v1,v2. 1034 1034 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 ⊢ (?%?); //; 1037 qed. 1038 1038 1039 1039 (* … … 1044 1044 Qed. 1045 1045 *) 1046 nlemma sign_ext_lessdef:1046 lemma sign_ext_lessdef: 1047 1047 ∀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 //; 1049 qed. 1050 1050 (* 1051 1051 Lemma singleoffloat_lessdef:
Note: See TracChangeset
for help on using the changeset viewer.