Ignore:
Timestamp:
Jun 15, 2011, 4:15:52 PM (8 years ago)
Author:
campbell
Message:

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

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/semantics.ma

    r886 r961  
    9191].
    9292
    93 let rec find_case (A:Type[0]) (i:int) (cs:list (int × A)) (default:A) on cs : A ≝
     93let rec find_case (A:Type[0]) (sz:intsize) (i:bvint sz) (cs:list (bvint sz × A)) (default:A) on cs : A ≝
    9494match cs with
    9595[ nil ⇒ default
    9696| cons h t ⇒
    9797    let 〈hi,a〉 ≝ h in
    98     if eq i hi then a else find_case A i t default
     98    if eq_bv ? i hi then a else find_case A sz i t default
    9999].
    100100
     
    199199        ! k' ← k_exit n k;
    200200        ret ? 〈E0, State f St_skip en m sp k'〉
    201     | St_switch _ _ e cs default ⇒
     201    | St_switch sz _ e cs default ⇒
    202202        ! 〈tr,v〉 ← eval_expr ge ? e en sp m;
    203203        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))
    207208        | _ ⇒ Wrong ??? (msg BadSwitchValue)
    208209        ]
     
    257258        | Some v ⇒
    258259            match v with
    259             [ Vint i ⇒ Some ? i
     260            [ Vint sz i ⇒ intsize_eq_elim ? sz I32 ? i (λi. Some ? i) (None ?)
    260261            | _ ⇒ None ?
    261262            ]
Note: See TracChangeset for help on using the changeset viewer.