Changeset 1121


Ignore:
Timestamp:
Aug 26, 2011, 8:00:06 PM (8 years ago)
Author:
sacerdot
Message:

External function calls implemented (but look at the new comment on the
semantics of the return type).

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/semantics.ma

    r1120 r1121  
    1111
    1212include "RTL/RTL.ma". (* CSC: syntax.ma in RTLabs *)
     13
     14(* CSC: external functions never fail (??) and always return something of the
     15   size of one register, both in the frontend and in the backend.
     16   Is this reasonable??? In OCaml it always return a list, but in the frontend
     17   only the head is kept (or Undef if the list is empty) ??? *)
    1318
    1419(* CSC: carries are values and booleans are not values; so we use integers.
     
    217222    ret ? 〈E0, State (mk_frame (func f) (locals f) l (sp f) (retdst f) Vtrue) fs m〉
    218223  ]
    219 | Callstate fd params dst fs m ⇒ ? (* CSC: XXXXXXXXXXXX
     224| Callstate fd params dst fs m ⇒
    220225    match fd with
    221     [ Internal fn ⇒
     226    [ Internal fn ⇒ ? (*
    222227        ! locals ← params_store (f_params fn) params (init_locals (f_locals fn));
    223228        let 〈m', sp〉 ≝ alloc m 0 (f_stacksize fn) Any in
    224         ret ? 〈E0, State (mk_frame fn locals (f_entry fn) sp dst Vundef) fs m'〉
     229        ret ? 〈E0, State (mk_frame fn locals (f_entry fn) sp dst Vundef) fs m'〉 *)
    225230    | External fn ⇒
    226231        ! evargs ← check_eventval_list params (sig_args (ef_sig fn));
    227232        ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
    228         ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), Returnstate (Some ? (mk_val ? evres) (*FIXME should allow None *)) dst fs m〉
    229     ] *)
     233        (* CSC: return type changed from option to list *)
     234        ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), Returnstate [mk_val ? evres] dst fs m〉
     235    ]
    230236| Returnstate v dst fs m ⇒ ? (* CSC: XXXXXXXXXXXXXXXXXX
    231237    match fs with
Note: See TracChangeset for help on using the changeset viewer.