Changeset 1122


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

Internal function call implemented too.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/semantics.ma

    r1121 r1122  
    7070definition build_state ≝ λf.λfs.λm.λn. State (adv n f) fs m.
    7171
    72 definition init_locals : list (register × typ) → register_env val ≝
    73 foldr ?? (λidt,en. let 〈id,ty〉 ≝ idt in add RegisterTag val en id Vundef) (empty_map ??).
     72(* CSC: modified to take in input a list of registers (untyped) *)
     73definition init_locals : list register → register_env val ≝
     74foldr ?? (λid,en. add RegisterTag val en id Vundef) (empty_map ??).
    7475
    7576definition reg_store ≝
     
    7980axiom WrongNumberOfParameters : String.
    8081
    81 let rec params_store (rs:list (register × typ)) (vs:list val) (locals : register_env val) : res (register_env val) ≝
     82(* CSC: modified to take in input a list of registers (untyped) *)
     83let rec params_store (rs:list register) (vs:list val) (locals : register_env val) : res (register_env val) ≝
    8284match rs with
    8385[ nil ⇒ match vs with [ nil ⇒ OK ? locals | _ ⇒ Error ? (msg WrongNumberOfParameters)]
    84 | cons rt rst ⇒ match vs with [ nil ⇒ Error ? (msg WrongNumberOfParameters) | cons v vst ⇒
    85   let 〈r,ty〉 ≝ rt in
     86| cons r rst ⇒ match vs with [ nil ⇒ Error ? (msg WrongNumberOfParameters) | cons v vst ⇒
    8687  let locals' ≝ add RegisterTag val locals r v in
    8788  params_store rst vst locals'
     
    224225| Callstate fd params dst fs m ⇒
    225226    match fd with
    226     [ Internal fn ⇒ ? (*
    227         ! locals ← params_store (f_params fn) params (init_locals (f_locals fn));
    228         let 〈m', sp〉 ≝ alloc m 0 (f_stacksize fn) Any in
    229         ret ? 〈E0, State (mk_frame fn locals (f_entry fn) sp dst Vundef) fs m'〉 *)
     227    [ Internal fn ⇒
     228        ! locals ← params_store (rtl_if_params fn) params (init_locals (rtl_if_locals fn));
     229        let 〈m', sp〉 ≝ alloc m 0 (rtl_if_stacksize fn) Any in
     230        (* CSC: added carry *)
     231        ret ? 〈E0, State (mk_frame fn locals (rtl_if_entry fn) sp dst Vundef) fs m'〉
    230232    | External fn ⇒
    231233        ! evargs ← check_eventval_list params (sig_args (ef_sig fn));
Note: See TracChangeset for help on using the changeset viewer.