Ignore:
Timestamp:
Apr 4, 2011, 5:13:08 PM (9 years ago)
Author:
campbell
Message:

Extra type safety for identifiers.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLabs-sem.ma

    r731 r736  
    5151λrs,v,locals. match rs with [ dp n regs ⇒
    5252  do vs ← break n v;
    53   OK ? (fold_right2_i ??? (λ_. register_update split_val) locals n regs vs)
     53  OK ? (fold_right2_i ??? (λ_.λr,v,lcls. add RegisterTag ? lcls r v) locals n regs vs)
    5454].
    5555
     
    6464definition reg_retrieve : register_env ? → registers → res val ≝
    6565λlocals,rs. match rs with [ dp n regs ⇒
    66   do vs ← fold_right_i ??? (λm,r,vs. do vs' ← vs; do v ← opt_to_res … (register_lookup ? locals r); OK ? (v:::vs')) (OK ? [[ ]]) regs;
     66  do vs ← fold_right_i ??? (λm,r,vs. do vs' ← vs; do v ← opt_to_res … (lookup ?? locals r); OK ? (v:::vs')) (OK ? [[ ]]) regs;
    6767  merge n vs
    6868].
     
    111111match st with
    112112[ State f fs m ⇒
    113   ! s ← graph_lookup ? (f_graph (func f)) (next f);
     113  ! s ← lookup ?? (f_graph (func f)) (next f);
    114114  match s with
    115115  [ St_skip l ⇒ ret ? 〈E0, build_state f fs m l〉
     
    194194    match fd with
    195195    [ Internal fn ⇒
    196         ! locals ← params_store (f_params fn) params (register_empty ?);
     196        ! locals ← params_store (f_params fn) params (empty_map RegisterTag ?);
    197197        let 〈m', sp〉 ≝ alloc m 0 (f_stacksize fn) Any in
    198198        ret ? 〈E0, State (mk_frame fn locals (f_entry fn) sp dst) fs m'〉
Note: See TracChangeset for help on using the changeset viewer.