Changeset 636


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.

Location:
Deliverables/D3.1/C-semantics
Files:
4 edited

Legend:

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

    r487 r636  
    436436  ef_sig: signature
    437437}.
    438 (*
    439 inductive fundef (F: Type): Type
     438
     439inductive fundef (F: Type[0]): Type[0]
    440440  | Internal: F → fundef F
    441441  | External: external_function → fundef F.
    442 
     442(*
    443443(* Implicit Arguments External [F]. *)
    444444(*
  • Deliverables/D3.1/C-semantics/Errors.ma

    r487 r636  
    1616include "basics/types.ma".
    1717include "basics/logic.ma".
     18include "basics/list.ma".
    1819
    1920(* * Error reporting and the error monad. *)
     
    107108
    108109(** This is the familiar monadic map iterator. *)
    109 
    110 Fixpoint mmap (A B: Type) (f: A -> res B) (l: list A) {struct l} : res (list B) :=
     110*)
     111
     112let rec mmap (A, B: Type[0]) (f: A → res B) (l: list A) on l : res (list B) ≝
    111113  match l with
    112   | nil => OK nil
    113   | hd :: tl => do hd' <- f hd; do tl' <- mmap f tl; OK (hd' :: tl')
    114   end.
    115 
    116 Remark mmap_inversion:
    117   forall (A B: Type) (f: A -> res B) (l: list A) (l': list B),
    118   mmap f l = OK l' ->
     114  [ nil ⇒ OK ? []
     115  | cons hd tl ⇒ do hd' ← f hd; do tl' ← mmap ?? f tl; OK ? (hd'::tl')
     116  ].
     117
     118(*
     119lemma mmap_inversion:
     120  ∀A, B: Type[0]. ∀f: A -> res B. ∀l: list A. ∀l': list B.
     121  mmap A B f l = OK ? l' →
    119122  list_forall2 (fun x y => f x = OK y) l l'.
    120123Proof.
  • 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(*
  • Deliverables/D3.1/C-semantics/cerco/Vector.ma

    r535 r636  
    201201    ].
    202202
     203let rec fold_right_i (A: Type[0]) (B: nat → Type[0]) (n: nat)
     204                     (f: ∀n. A → B n → B (S n)) (x: B 0) (v: Vector A n) on v ≝
     205  match v with
     206    [ VEmpty ⇒ x
     207    | VCons n hd tl ⇒ f ? hd (fold_right_i A B n f x tl)
     208    ].
     209
    203210let rec fold_right2_i (A: Type[0]) (B: Type[0]) (C: nat → Type[0])
    204211                      (f: ∀N. A → B → C N → C (S N)) (c: C O) (n: nat)
Note: See TracChangeset for help on using the changeset viewer.