Changeset 1999 for src/RTL/semantics.ma


Ignore:
Timestamp:
May 25, 2012, 10:45:15 AM (9 years ago)
Author:
campbell
Message:

Make back-end use the main global envs.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/semantics.ma

    r1451 r1999  
    117117  block → call_args rtl_sem_params → IO io_out io_in (trace×(state rtl_sem_params)) ≝
    118118 λglobals,ge,st,b,args.
    119   ! fd ← opt_to_res … [MSG BadPointer] (find_funct_ptr ?? ge b);
     119  ! fd ← opt_to_res … [MSG BadPointer] (find_funct_ptr ge b);
    120120    match fd with
    121121    [ Internal fn ⇒
     
    125125      let l' ≝ joint_if_entry … fn in
    126126      ! st ← next … (rtl_sem_params1 …) l' (set_regs rtl_sem_params regs st) ;
    127        ret ? 〈 E0, st〉
     127       return 〈 E0, st〉
    128128    | External fn ⇒ ?(*
    129129      ! params ← fetch_external_args … fn st;
     
    154154      ! st ← greg_store rtl_sem_params dreg2 dph st ;
    155155      ! st ← next … (rtl_sem_params1 globals) l st ;
    156        ret ? 〈E0, st〉
     156       return 〈E0, st〉
    157157   | rtl_st_ext_call_ptr r1 r2 args dest ⇒
    158       ! b ← block_of_register_pair r1 r2 st ;
    159       ! ra ← succ_pc … (rtl_more_sem_params1 globals) l (pc … st) ;
     158      ! b ← block_of_register_pair r1 r2 st : IO ??? ;
     159      ! ra ← succ_pc … (rtl_more_sem_params1 globals) l (pc … st) : IO ??? ;
    160160      eval_call_block … (mk_sem_params1 … (rtl_more_sem_params1 globals))
    161161       ge st b args dest ra
    162162   | rtl_st_ext_tailcall_id id args ⇒
    163       ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
     163      ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol … ge id) : IO ???;
    164164      eval_tail_call_block … ge st b args
    165165   | rtl_st_ext_tailcall_ptr r1 r2 args ⇒
    166       ! b ← block_of_register_pair r1 r2 st ;
     166      ! b ← block_of_register_pair r1 r2 st : IO ???;
    167167      eval_tail_call_block … ge st b args
    168168   ].
Note: See TracChangeset for help on using the changeset viewer.