Changeset 1347
 Timestamp:
 Oct 10, 2011, 7:22:13 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/common/Values.ma
r1339 r1347 50 50 definition Vfalse: val ≝ Vzero I32. 51 51 52 (* Values split into bytes. Ideally we'd use some kind of sizeof for the53 predicates here, but we don't (currently) have a single sizeof for Vundef.54 We only split in stages of the compiler where all Vint values are byte sized.55 *)56 57 definition ptr_may_be_single : region → bool ≝58 λr.match r with [ Data ⇒ true  IData ⇒ true  _ ⇒ false ].59 60 definition may_be_single : val → Prop ≝61 λv. match v with62 [ Vundef ⇒ True63  Vint _ _ ⇒ True64  Vfloat _ ⇒ False65  Vnull r ⇒ ptr_may_be_single r = true66  Vptr r _ _ _ ⇒ ptr_may_be_single r = true67 ].68 69 definition may_be_split : val → Prop ≝70 λv.match v with71 [ Vint _ _ ⇒ False72  Vnull r ⇒ ptr_may_be_single r = false73  Vptr r _ _ _ ⇒ ptr_may_be_single r = false74  _ ⇒ True75 ].76 77 inductive split_val : Type[0] ≝78  Single : ∀v:val. may_be_single v → split_val79  High : ∀v:val. may_be_split v → split_val80  Low : ∀v:val. may_be_split v → split_val.81 82 notation > "vbox('do' _ ← e; break e')" with precedence 40 for @{'bind ${e} (λ_.${e'})}.83 (*84 let rec assert_nat_eq (m,n:nat) : res (m = n) ≝85 match m return λx.res (x = n) with86 [ O ⇒ match n return λx. res (O = x) with [ O ⇒ OK ? (refl ??)  _ ⇒ Error ? ]87  S m' ⇒ match n return λx.res (S m' = x) with [ O ⇒ Error ?  S n' ⇒88 do E ← assert_nat_eq m' n';89 match E return λx.λ_. res (S m' = S x) with [ refl ⇒ OK ? (refl ??) ] ]90 ].91 92 definition res_eq_nat : ∀m,n:nat. ∀P:nat → Type[0]. P m → res (P n) ≝93 λm,n,P,p.94 do E ← assert_nat_eq m n;95 match E return λx.λ_. res (P x) with [ refl ⇒ OK ? p ].96 97 definition break : ∀n:nat. val → res (Vector split_val n) ≝98 λn,v. match v return λv'. (may_be_single v' → ?) → (may_be_split v' → ?) → ? with99 [ Vundef ⇒ λs.λt. res_eq_nat 1 n ? (s I)100  Vint i ⇒ λs.λt. res_eq_nat 1 n ? (s I)101  Vfloat f ⇒ λs.λt. res_eq_nat 2 n ? (t I)102  Vnull r ⇒103 match ptr_may_be_single r return λx. (x = true → ?) → (x = false → ?) → ? with104 [ true ⇒ λs.λt. res_eq_nat 1 n ? (s (refl ??))105  false ⇒ λs.λt. ?106 ]107  Vptr r b p o ⇒108 match ptr_may_be_single r return λx. (x = true → ?) → (x = false → ?) → ? with109 [ true ⇒ λs.λt. res_eq_nat 1 n ? (s (refl ??))110  false ⇒ λs.λt. ?111 ]112 ] (λp. [[ Single v p ]]) (λp. [[ Low v p; High v p ]]).113 @(res_eq_nat 2 n ? (t (refl ??))) qed. (* XXX: I have no idea why this fails if you do it directly. *)114 115 definition val_eq : val → val → bool ≝116 λx,y.117 match x with118 [ Vundef ⇒ match y with [ Vundef ⇒ true  _ ⇒ false ]119  Vint i ⇒ match y with [ Vint j ⇒ eq i j  _ ⇒ false ]120  Vfloat f ⇒ match y with [ Vfloat f' ⇒ match eq_dec f f' with [ inl _ ⇒ true  _ ⇒ false ]  _ ⇒ false ]121  Vnull r ⇒ match y with [ Vnull r' ⇒ eq_region r r'  _ ⇒ false ]122  Vptr r b p o ⇒ match y with [ Vptr r' b' p' o' ⇒ eq_region r r' ∧ eq_block b b' ∧ eq_offset o o'  _ ⇒ false ]123 ].124 125 definition merge : ∀n:nat. Vector split_val n → res val ≝126 λn,s. match s with127 [ VEmpty ⇒ Error ?128  VCons _ h1 t1 ⇒129 match t1 with130 [ VEmpty ⇒ match h1 with [ Single v _ ⇒ OK ? v  _ ⇒ Error ? ]131  VCons _ h2 t2 ⇒132 match t2 with133 [ VEmpty ⇒ match h1 with [ Low v _ ⇒ match h2 with [ High v' _ ⇒ if val_eq v v' then OK ? v else Error ?  _ ⇒ Error ? ]  _ ⇒ Error ? ]134  VCons _ _ _ ⇒ Error ?135 ]136 ]137 ].138 139 *)140 52 (* 141 53 (** The module [Val] defines a number of arithmetic and logical operations
Note: See TracChangeset
for help on using the changeset viewer.