Ignore:
Timestamp:
Apr 6, 2012, 8:02:10 PM (8 years ago)
Author:
tranquil
Message:

big update, alas incomplete:
joint changed a bit, and all BE languages need to be updated
started development of blocks to aid preservation results, but still incomplete
if it breaks too many things, feel free to roll back

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/semantics.ma

    r1880 r1882  
    124124      ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
    125125      ! fd ← opt_to_res … [MSG BadFunction; CTX ? id] (find_funct_ptr ?? ge b);
    126       ! vs ← m_mmap … (reg_retrieve (locals f)) args;
     126      ! vs ← m_list_map … (reg_retrieve (locals f)) args;
    127127      return 〈E0, Callstate fd vs dst (adv l f ?::fs) m〉
    128128  | St_call_ptr frs args dst l ⇒ λH.
    129129      ! fv ← reg_retrieve (locals f) frs;
    130130      ! fd ← opt_to_res … (msg BadFunction) (find_funct ?? ge fv);
    131       ! vs ← m_mmap … (reg_retrieve (locals f)) args;
     131      ! vs ← m_list_map … (reg_retrieve (locals f)) args;
    132132      return 〈E0, Callstate fd vs dst (adv l f ?::fs) m〉
    133133(*
     
    135135      ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
    136136      ! fd ← opt_to_res … [MSG BadFunction; CTX ? id] (find_funct_ptr ?? ge b);
    137       ! vs ← m_mmap … (reg_retrieve (locals f)) args;
     137      ! vs ← m_list_map … (reg_retrieve (locals f)) args;
    138138      return 〈E0, Callstate fd vs (retdst f) fs (free m (sp f))〉
    139139  | St_tailcall_ptr frs args ⇒ λH.
    140140      ! fv ← reg_retrieve (locals f) frs;
    141141      ! fd ← opt_to_res … (msg BadFunction) (find_funct ?? ge fv);
    142       ! vs ← m_mmap … (reg_retrieve (locals f)) args;
     142      ! vs ← m_list_map … (reg_retrieve (locals f)) args;
    143143      return 〈E0, Callstate fd vs (retdst f) fs (free m (sp f))〉
    144144*)
Note: See TracChangeset for help on using the changeset viewer.