Changeset 1151


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

Only new_/del_frame and framesize left.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/semantics.ma

    r1150 r1151  
    2121(* CSC: ???????????? *)
    2222axiom smerge: val → val → res val.
    23 (*
    2423(* CSC: ???????????? In OCaml: IntValue.Int32.merge
    2524   Note also that the translation can fail; so it should be a res int! *)
    2625axiom smerge2: list val → int.
    27 *)
    2826(* CSC: I have a byte, I need a value, but it is complex to do so *)
    2927axiom val_of_Byte: Byte → val.
     
    5250definition frame: Type[0] ≝ register_env val.
    5351
     52(* CSC: exit not put in the state, like in OCaml. It is constant througout
     53   execution *)
    5454record state : Type[0] ≝
    5555 { st_frms: list frame
    5656 ; pc: address
    5757 ; sp: address
    58 (* ; exit: address *)
    5958 ; locals: register_env val
    6059 ; carry: val
     
    199198    (λregs,v,reg. hwreg_store reg v regs) (regs st) vs RegisterRets)
    200199  (λregs.OK ? (set_regs regs st)).
     200
     201definition fetch_result: state → nat → res (list val) ≝
     202 λst,registersno.
     203  let retregs ≝ prefix … registersno RegisterRets in
     204  mmap … (λr. hwreg_retrieve (regs st) r) retregs.
    201205
    202206definition eval_statement : genv → state → IO io_out io_in (trace × state) ≝
     
    334338     ret ? 〈E0, goto l st〉
    335339  ].
     340cases daemon. qed.
    336341
    337342axiom WrongReturnValueType: String.
    338343
    339 definition is_final : state → option ((*CSC: why not res*) int) ≝
    340 λs. match s with
    341 [ State _ _ _ ⇒ None ?
    342 | Callstate _ _ _ _ _ ⇒ None ?
    343 | Returnstate v _ fs _ ⇒
    344     match fs with
    345      [ nil ⇒ Some ? (smerge2 v)
    346      | _ ⇒ None ? ]].
    347 
    348 definition RTL_exec : execstep io_out io_in ≝
    349   mk_execstep … ? is_final mem_of_state eval_statement.
     344definition is_final : label → nat → state → option ((*CSC: why not res*) int) ≝
     345λexit,registersno,st.
     346 (* CSC: monadic notation missing here *)
     347 match fetch_statement st with
     348  [ Error _ ⇒ None ?
     349  | OK s ⇒
     350     match s with
     351      [ ertl_st_return ⇒
     352       (* CSC: monadic notation missing here *)
     353        match fetch_ra st with
     354         [ Error _ ⇒ None ?
     355         | OK st_l ⇒ let 〈st,l〉 ≝ st_l in
     356            match label_eq l exit with
     357             [ inl _ ⇒
     358               (* CSC: monadic notation missing here *)
     359                match fetch_result st registersno with
     360                 [ Error _ ⇒ None ?
     361                 | OK vals ⇒ Some ? (smerge2 vals) ]
     362             | inr _ ⇒ None ? ]]
     363      | _ ⇒ None … ]].
     364
     365definition ERTL_exec : label → nat → execstep io_out io_in ≝
     366 λexit,registersno.
     367  mk_execstep … ? (is_final exit registersno) m eval_statement.
    350368
    351369(* CSC: XXX the program type does not fit with the globalenv and init_mem
Note: See TracChangeset for help on using the changeset viewer.