Changeset 1388


Ignore:
Timestamp:
Oct 17, 2011, 10:54:50 AM (8 years ago)
Author:
sacerdot
Message:

fetch_result implemented for ERTL. This required a different istantiation of
resultT that is not in line with the OCaml's code. Look at CHANGES for details.
RTLToERTL has been ported in an hopefully correct manner.

Location:
src
Files:
4 edited

Legend:

Unmodified
Added
Removed
  • src/CHANGES

    r1198 r1388  
    8282  it only needs to do a simple pattern match per recursion and copes with deeper
    8383  arithmetic expressions such as (char)((int)x + (int)y + (int)z).
     84
     8517/10/2011: (CSC)
     86  In OCaml, RTL's and ERTL's St_return statement holds the return register list,
     87  to be used in is_final. In Matita, they don't. For RTL the information was
     88  duplicated in the internal function record. I have done the same for ERTL too.
     89  To be double checked with the OCaml semantics.
  • src/ERTL/ERTL.ma

    r1280 r1388  
    1414  register nat unit ertl_statement_extension.
    1515definition ertl_params_: params_ ≝ graph_params_ ertl_params__.
    16 definition ertl_params0: params0 ≝ mk_params0 ertl_params__ unit nat.
     16definition ertl_params0: params0 ≝ mk_params0 ertl_params__ (list register) nat.
    1717definition ertl_params1: params1 ≝ rtl_ertl_params1 ertl_params0.
    1818definition ertl_params: ∀globals. params globals ≝ rtl_ertl_params ertl_params0.
  • src/ERTL/semantics.ma

    r1386 r1388  
    6060    (set_regs ertl_sem_params 〈empty_map …,\snd (regs … st)〉 st)).
    6161
    62 (*CSC: XXXXX, for is_final only *)
    63 axiom ertl_fetch_result:
    64  ∀globals. genv … (ertl_params globals) → state ertl_sem_params → res (list beval).
     62definition ertl_fetch_result:
     63 ∀globals. genv … (ertl_params globals) → state ertl_sem_params → res (list beval) ≝
     64 λglobals,ge,st.
     65  do fn ← graph_fetch_function … globals ge st ;
     66  let ret_val_regs ≝ joint_if_result … fn in
     67   mmap … (λreg.greg_retrieve ertl_sem_params st reg) ret_val_regs.
    6568
    6669(*CSC: XXXX, for external functions only*)
  • src/RTL/RTLToERTL.ma

    r1352 r1388  
    354354  let def' ≝
    355355    mk_joint_internal_function globals (ertl_params globals)
    356       (joint_if_luniverse … def) (joint_if_runiverse … def) it
     356      (joint_if_luniverse … def) (joint_if_runiverse … def) (joint_if_result … def) (*CSC: different from OCaml code where joint_if_result is unit*)
    357357      nb_params new_locals ((joint_if_stacksize … def) + added_stacksize)
    358358      graph' ? ? in
Note: See TracChangeset for help on using the changeset viewer.