Changeset 961 for src/Cminor/semantics.ma

Timestamp:

Jun 15, 2011, 4:15:52 PM (10 years ago)

Author:

campbell

Message:

Use precise bitvector sizes throughout the front end, rather than 32bits
everywhere.

File:

• src/Cminor/semantics.ma (modified) (3 diffs)

src/Cminor/semantics.ma

@@ -91 +91 @@
 ].
 
-let rec find_case (A:Type[0]) (i:int) (cs:list (int × A)) (default:A) on cs : A ≝
+let rec find_case (A:Type[0]) (sz:intsize) (i:bvint sz) (cs:list (bvint sz × A)) (default:A) on cs : A ≝
 match cs with
 [ nil ⇒ default
 | cons h t ⇒
     let 〈hi,a〉 ≝ h in
-    if eq i hi then a else find_case A i t default
+    if eq_bv ? i hi then a else find_case A sz i t default
 ].
 
@@ -199 +199 @@
         ! k' ← k_exit n k;
         ret ? 〈E0, State f St_skip en m sp k'〉
-    | St_switch _ _ e cs default ⇒
+    | St_switch sz _ e cs default ⇒
         ! 〈tr,v〉 ← eval_expr ge ? e en sp m;
         match v with
-        [ Vint i ⇒
-            ! k' ← k_exit (find_case ? i cs default) k;
-            ret ? 〈tr, State f St_skip en m sp k'〉
+        [ Vint sz' i ⇒ intsize_eq_elim ? sz' sz ? i (λi.
+            ! k' ← k_exit (find_case ?? i cs default) k;
+            ret ? 〈tr, State f St_skip en m sp k'〉)
+            (Wrong ??? (msg BadSwitchValue))
         | _ ⇒ Wrong ??? (msg BadSwitchValue)
         ]
@@ -257 +258 @@
         | Some v ⇒
             match v with
-            [ Vint i ⇒ Some ? i
+            [ Vint sz i ⇒ intsize_eq_elim ? sz I32 ? i (λi. Some ? i) (None ?)
             | _ ⇒ None ?
             ]