Changeset 1146


Ignore:
Timestamp:
Aug 30, 2011, 4:07:39 PM (8 years ago)
Author:
sacerdot
Message:

More progress: function call/return almost completed.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/semantics.ma

    r1142 r1146  
    177177(*CSC: to be implemented *)
    178178axiom fetch_external_args: external_function → state → list val.
    179 axiom set_result: list val → state → state.
     179
     180(*CSC: to be implemented; fails if the first list is longer *)
     181axiom fold_left2_first_not_longer:
     182 ∀A,B,C:Type[0]. ∀f:(C → A → B → res C).
     183  ∀acc:C. ∀l1:list A. ∀l2: list B.
     184   res C.
     185
     186(* CSC: the list should be a vector or have an upper bounded length *)
     187definition set_result: list val → state → res state ≝
     188 λvs,st.
     189  (* CSC: monadic notation not used *)
     190  bind ?? (
     191   fold_left2_first_not_longer …
     192    (λregs,v,reg. hwreg_store reg v regs) (regs st) vs RegisterRets)
     193  (λregs.OK ? (set_regs regs st)).
    180194
    181195definition eval_statement : genv → state → IO io_out io_in (trace × state) ≝
     
    288302           components; instead I am making a singleton out of it *)
    289303        let vs ≝ [mk_val ? evres] in
    290         ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres),
    291          goto l (set_result vs st)
     304        ! st ← set_result vs st;
     305        ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), goto l st
    292306      ]
    293307  | ertl_st_return ⇒
Note: See TracChangeset for help on using the changeset viewer.