Changeset 1347


Ignore:
Timestamp:
Oct 10, 2011, 7:22:13 PM (8 years ago)
Author:
campbell
Message:

Remove obsolete definitions.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Values.ma

    r1339 r1347  
    5050definition Vfalse: val ≝ Vzero I32.
    5151
    52 (* Values split into bytes.  Ideally we'd use some kind of sizeof for the
    53    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 with
    62 [ Vundef ⇒ True
    63 | Vint _ _ ⇒ True
    64 | Vfloat _ ⇒ False
    65 | Vnull r ⇒ ptr_may_be_single r = true
    66 | Vptr r _ _ _ ⇒ ptr_may_be_single r = true
    67 ].
    68 
    69 definition may_be_split : val → Prop ≝
    70 λv.match v with
    71 [ Vint _ _ ⇒ False
    72 | Vnull r ⇒ ptr_may_be_single r = false
    73 | Vptr r _ _ _ ⇒ ptr_may_be_single r = false
    74 | _ ⇒ True
    75 ].
    76 
    77 inductive split_val : Type[0] ≝
    78 | Single : ∀v:val. may_be_single v → split_val
    79 | High   : ∀v:val. may_be_split v → split_val
    80 | 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) with
    86 [ 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' → ?) → ? with
    99 [ 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 → ?) → ? with
    104     [ 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 → ?) → ? with
    109     [ 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 with
    118 [ 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 with
    127 [ VEmpty ⇒ Error ?
    128 | VCons _ h1 t1 ⇒
    129   match t1 with
    130   [ VEmpty ⇒ match h1 with [ Single v _ ⇒ OK ? v | _ ⇒ Error ? ]
    131   | VCons _ h2 t2 ⇒
    132     match t2 with
    133     [ 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 *)
    14052(*
    14153(** The module [Val] defines a number of arithmetic and logical operations
Note: See TracChangeset for help on using the changeset viewer.