Changeset 638 for Deliverables/D3.1


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

Switch to more conservative definitions in preparation for review.
(Efficient mul/div via Z, sort out some disambiguation problems that have
appeared.)

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

Legend:

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

    r583 r638  
    344344#s1 cases s1; #s2 cases s2; /2/; %2 ; % #H destruct; qed.
    345345
    346 let rec type_eq_dec (t1,t2:type) : (t1 = t2) + (t1 ≠ t2) ≝
     346let rec type_eq_dec (t1,t2:type) : Sum (t1 = t2) (t1 ≠ t2) ≝
    347347match t1 return λt'. (t' = t2) + (t' ≠ t2) with
    348348[ Tvoid ⇒ match t2 return λt'. (Tvoid = t') + (Tvoid ≠ t') with [ Tvoid ⇒ inl ?? (refl ??) | _ ⇒ inr ?? (nmk ? (λH.?)) ]
     
    421421λt1,t2. match type_eq_dec t1 t2 with [ inl p ⇒ OK ? p | inr _ ⇒ Error ? ].
    422422
    423 let rec is_is_call_cont (k:cont) : (is_call_cont k) + (¬is_call_cont k) ≝
     423let rec is_is_call_cont (k:cont) : Sum (is_call_cont k) (Not (is_call_cont k)) ≝
    424424match k return λk'.(is_call_cont k') + (¬is_call_cont k') with
    425425[ Kstop ⇒ ?
  • Deliverables/D3.1/C-semantics/Csem.ma

    r583 r638  
    201201      match v1 with
    202202      [ Vint n1 ⇒ match v2 with
    203         [ Vint n2 ⇒ option_map … Vint (division_u ? n1 n2)
     203        [ Vint n2 ⇒ if eq n2 zero then None ? else Some ? (Vint (divu n1 n2))
     204(*        [ Vint n2 ⇒ option_map … Vint (division_u ? n1 n2)*)
    204205        | _ ⇒ None ? ]
    205206      | _ ⇒ None ? ]
     
    207208      match v1 with
    208209       [ Vint n1 ⇒ match v2 with
    209          [ Vint n2 ⇒ option_map … Vint (division_s ? n1 n2)
     210         [ Vint n2 ⇒ if eq n2 zero then None ? else Some ? (Vint(divs n1 n2))
     211(*         [ Vint n2 ⇒ option_map … Vint (division_s ? n1 n2)*)
    210212         | _ ⇒ None ? ]
    211213      | _ ⇒ None ? ]
     
    225227      match v1 with
    226228      [ Vint n1 ⇒ match v2 with
    227         [ Vint n2 ⇒ option_map … Vint (modulus_u ? n1 n2)
     229        [ Vint n2 ⇒ if eq n2 zero then None ? else Some ? (Vint (modu n1 n2))
     230(*        [ Vint n2 ⇒ option_map … Vint (modulus_u ? n1 n2)*)
    228231        | _ ⇒ None ? ]
    229232      | _ ⇒ None ? ]
     
    231234      match v1 with
    232235      [ Vint n1 ⇒ match v2 with
    233         [ Vint n2 ⇒ option_map … Vint (modulus_s ? n1 n2)
     236        [ Vint n2 ⇒ if eq n2 zero then None ? else Some ? (Vint (mods n1 n2))
     237(*        [ Vint n2 ⇒ option_map … Vint (modulus_s ? n1 n2)*)
    234238        | _ ⇒ None ? ]
    235239      | _ ⇒ None ? ]
  • Deliverables/D3.1/C-semantics/Integers.ma

    r582 r638  
    145145definition add ≝ addition_n wordsize.
    146146definition sub ≝ subtraction wordsize.
    147 definition mul ≝ λx,y. \fst (split ? wordsize wordsize (multiplication wordsize x y)).
     147(*definition mul ≝ λx,y. \fst (split ? wordsize wordsize (multiplication wordsize x y)).*)
     148definition mul ≝ λx,y. repr ((unsigned x) * (unsigned y)).
    148149definition Zdiv_round : Z → Z → Z ≝ λx,y: Z.
    149150  if Zltb x 0 then
Note: See TracChangeset for help on using the changeset viewer.