Ignore:
Timestamp:
Dec 10, 2012, 8:11:35 PM (8 years ago)
Author:
piccolo
Message:

completed isFinal and fetchStatementSigmaCommute. Fixed exit definition and sigma_pc in semantics.ma

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/semantics.ma

    r2537 r2551  
    619619    [ RETURN ⇒
    620620      do st' ← pop_frame … ge id fn st;
    621       ! nxt ← next_of_pc … ge (pc … st') ;
    622       let pc' ≝ succ_pc … (pc … st') nxt in
    623       if eq_program_counter pc' exit then
    624        do vals ← read_result … ge (joint_if_result … fn) st ;
    625        Word_of_list_beval vals
     621      if eq_program_counter (pc … st') exit then
     622      do vals ← read_result … ge (joint_if_result … fn) st ;
     623        Word_of_list_beval vals
    626624      else
    627        Error ? [ ]
     625        Error ? [ ]
    628626   | _ ⇒ Error ? [ ]
    629627   ]
Note: See TracChangeset for help on using the changeset viewer.