Changeset 961 for src/Cminor/semantics.ma
- Timestamp:
- Jun 15, 2011, 4:15:52 PM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/Cminor/semantics.ma
r886 r961 91 91 ]. 92 92 93 let rec find_case (A:Type[0]) ( i:int) (cs:list (int× A)) (default:A) on cs : A ≝93 let rec find_case (A:Type[0]) (sz:intsize) (i:bvint sz) (cs:list (bvint sz × A)) (default:A) on cs : A ≝ 94 94 match cs with 95 95 [ nil ⇒ default 96 96 | cons h t ⇒ 97 97 let 〈hi,a〉 ≝ h in 98 if eq i hi then a else find_case Ai t default98 if eq_bv ? i hi then a else find_case A sz i t default 99 99 ]. 100 100 … … 199 199 ! k' ← k_exit n k; 200 200 ret ? 〈E0, State f St_skip en m sp k'〉 201 | St_switch __ e cs default ⇒201 | St_switch sz _ e cs default ⇒ 202 202 ! 〈tr,v〉 ← eval_expr ge ? e en sp m; 203 203 match v with 204 [ Vint i ⇒ 205 ! k' ← k_exit (find_case ? i cs default) k; 206 ret ? 〈tr, State f St_skip en m sp k'〉 204 [ Vint sz' i ⇒ intsize_eq_elim ? sz' sz ? i (λi. 205 ! k' ← k_exit (find_case ?? i cs default) k; 206 ret ? 〈tr, State f St_skip en m sp k'〉) 207 (Wrong ??? (msg BadSwitchValue)) 207 208 | _ ⇒ Wrong ??? (msg BadSwitchValue) 208 209 ] … … 257 258 | Some v ⇒ 258 259 match v with 259 [ Vint i ⇒ Some ? i260 [ Vint sz i ⇒ intsize_eq_elim ? sz I32 ? i (λi. Some ? i) (None ?) 260 261 | _ ⇒ None ? 261 262 ]
Note: See TracChangeset
for help on using the changeset viewer.