Ignore:
Timestamp:
Mar 4, 2011, 6:20:26 PM (9 years ago)
Author:
campbell
Message:

A few definitions that will be useful for some preliminary rtlabs semantics.

File:
1 edited

Legend:

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

    r635 r636  
    2121include "Integers.ma".
    2222include "Floats.ma".
     23include "Errors.ma".
     24
     25include "cerco/Vector.ma".
    2326
    2427include "basics/logic.ma".
     
    118121definition Vtrue: val ≝ Vint one.
    119122definition Vfalse: val ≝ Vint zero.
     123
     124(* Values split into bytes.  Ideally we'd use some kind of sizeof for the
     125   predicates here, but we don't (currently) have a single sizeof for Vundef.
     126   We only split in stages of the compiler where all Vint values are byte sized.
     127 *)
     128
     129definition ptr_may_be_single : region → bool ≝
     130λr.match r with [ Data ⇒ true | IData ⇒ true | _ ⇒ false ].
     131
     132definition may_be_single : val → Prop ≝
     133λv. match v with
     134[ Vundef ⇒ True
     135| Vint _ ⇒ True
     136| Vfloat _ ⇒ False
     137| Vnull r ⇒ ptr_may_be_single r = true
     138| Vptr r _ _ _ ⇒ ptr_may_be_single r = true
     139].
     140
     141definition may_be_split : val → Prop ≝
     142λv.match v with
     143[ Vint _ ⇒ False
     144| Vnull r ⇒ ptr_may_be_single r = false
     145| Vptr r _ _ _ ⇒ ptr_may_be_single r = false
     146| _ ⇒ True
     147].
     148
     149inductive split_val : Type[0] ≝
     150| Single : ∀v:val. may_be_single v → split_val
     151| High   : ∀v:val. may_be_split v → split_val
     152| Low    : ∀v:val. may_be_split v → split_val.
     153
     154notation > "vbox('do' _ ← e; break e')" with precedence 40 for @{'bind ${e} (λ_.${e'})}.
     155
     156let rec assert_nat_eq (m,n:nat) : res (m = n) ≝
     157match m return λx.res (x = n) with
     158[ O ⇒ match n return λx. res (O = x) with [ O ⇒ OK ? (refl ??) | _ ⇒ Error ? ]
     159| S m' ⇒ match n return λx.res (S m' = x) with [ O ⇒ Error ? | S n' ⇒
     160  do E ← assert_nat_eq m' n';
     161  match E return λx.λ_. res (S m' = S x) with [ refl ⇒ OK ? (refl ??) ] ]
     162].
     163
     164definition res_eq_nat : ∀m,n:nat. ∀P:nat → Type[0]. P m → res (P n) ≝
     165λm,n,P,p.
     166  do E ← assert_nat_eq m n;
     167  match E return λx.λ_. res (P x) with [ refl ⇒ OK ? p ].
     168
     169definition break : ∀n:nat. val → res (Vector split_val n) ≝
     170λn,v. match v return λv'. (may_be_single v' → ?) → (may_be_split v' → ?) → ? with
     171[ Vundef ⇒ λs.λt. res_eq_nat 1 n ? (s I)
     172| Vint i ⇒ λs.λt. res_eq_nat 1 n ? (s I)
     173| Vfloat f ⇒ λs.λt. res_eq_nat 2 n ? (t I)
     174| Vnull r ⇒
     175    match ptr_may_be_single r return λx. (x = true → ?) → (x = false → ?) → ? with
     176    [ true ⇒ λs.λt. res_eq_nat 1 n ? (s (refl ??))
     177    | false ⇒ λs.λt. ?
     178    ]
     179| Vptr r b p o ⇒
     180    match ptr_may_be_single r return λx. (x = true → ?) → (x = false → ?) → ? with
     181    [ true ⇒ λs.λt. res_eq_nat 1 n ? (s (refl ??))
     182    | false ⇒ λs.λt. ?
     183    ]
     184] (λp. [[ Single v p ]]) (λp. [[ Low v p; High v p ]]).
     185@(res_eq_nat 2 n ? (t (refl ??))) qed. (* XXX: I have no idea why this fails if you do it directly. *)
     186
     187definition val_eq : val → val → bool ≝
     188λx,y.
     189match x with
     190[ Vundef ⇒ match y with [ Vundef ⇒ true | _ ⇒ false ]
     191| Vint i ⇒ match y with [ Vint j ⇒ eq i j | _ ⇒ false ]
     192| Vfloat f ⇒ match y with [ Vfloat f' ⇒ match eq_dec f f' with [ inl _ ⇒ true | _ ⇒ false ] | _ ⇒ false ]
     193| Vnull r ⇒ match y with [ Vnull r' ⇒ eq_region r r' | _ ⇒ false ]
     194| 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 ]
     195].
     196
     197definition merge : ∀n:nat. Vector split_val n → res val ≝
     198λn,s. match s with
     199[ VEmpty ⇒ Error ?
     200| VCons _ h1 t1 ⇒
     201  match t1 with
     202  [ VEmpty ⇒ match h1 with [ Single v _ ⇒ OK ? v | _ ⇒ Error ? ]
     203  | VCons _ h2 t2 ⇒
     204    match t2 with
     205    [ VEmpty ⇒ match h1 with [ Low v _ ⇒ match h2 with [ High v' _ ⇒ if val_eq v v' then OK ? v else Error ? | _ ⇒ Error ? ] | _ ⇒ Error ? ]
     206    | VCons _ _ _ ⇒ Error ?
     207    ]
     208  ]
     209].
     210   
    120211
    121212(*
Note: See TracChangeset for help on using the changeset viewer.