Changeset 1177


Ignore:
Timestamp:
Sep 4, 2011, 9:36:41 PM (8 years ago)
Author:
sacerdot
Message:

Almost finished. Some functions still to be implemented, but I suspect
those must be parameters since they do not have a uniform implementation.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/semantics.ma

    r1176 r1177  
    1515*)
    1616axiom smerge: val → val → res val.
    17 (*
    1817(* CSC: ???????????? In OCaml: IntValue.Int32.merge
    1918   Note also that the translation can fail; so it should be a res int! *)
    2019axiom smerge2: list val → int.
    21 *)
    2220(* CSC: I have a byte, I need a value, but it is complex to do so *)
    2321axiom val_of_Byte: Byte → val.
     
    259257*)
    260258
     259(*CSC: XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX *)
     260axiom fetch_result: ∀p. state p → nat → res (list val).
    261261(*
    262262definition fetch_result: state → nat → res (list val) ≝
     
    407407    ].
    408408
    409 definition is_final: list ident → label → nat → state → option ((*CSC: why not res*) int) ≝
    410   λglobals: list ident.
     409definition is_final: ∀p. list ident → label → nat → state p → option ((*CSC: why not res*) int) ≝
     410  λp.λglobals: list ident.
    411411  λexit.
    412412  λregistersno.
    413413  λst.
    414414 (* CSC: monadic notation missing here *)
    415   match fetch_statement p globals st with
     415  match fetch_statement globals st with
    416416  [ Error _ ⇒ None ?
    417417  | OK s ⇒
    418418    match s with
    419419      [ joint_st_return ⇒
    420         match fetch_ra st with
     420        match fetch_ra st with
    421421         [ Error _ ⇒ None ?
    422422         | OK st_l ⇒
     
    425425           [ inl _ ⇒
    426426             (* CSC: monadic notation missing here *)
    427              match fetch_result st registersno with
     427             match fetch_result st registersno with
    428428             [ Error _ ⇒ None ?
    429429             | OK vals ⇒ Some ? (smerge2 vals)
     
    436436  ].
    437437
    438 definition ERTL_exec: list ident → label → nat → execstep io_out io_in ≝
    439   λglobals.
     438definition joint_exec: ∀globals:list ident. sem_params2 globals → label → nat → execstep io_out io_in ≝
     439  λglobals,p.
    440440  λexit.
    441441  λregistersno.
    442   mk_execstep ? ? ? ? (is_final globals exit registersno) m (eval_statement globals).
     442  mk_execstep ? ? ? ? (is_final p globals exit registersno) (m p) (eval_statement globals p).
    443443
    444444(* CSC: XXX the program type does not fit with the globalenv and init_mem
Note: See TracChangeset for help on using the changeset viewer.