Ignore:
Timestamp:
Sep 28, 2011, 11:08:37 PM (8 years ago)
Author:
sacerdot
Message:

Porting of all transformation to the joint syntax practically completed.
Some functions remain to be ported in RTLAbstoRTL, but it is just repetitive
coding.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/semantics.ma

    r1250 r1281  
    1717  eq_beval (\fst addr1) (\fst addr2) ∧ eq_beval (\snd addr1) (\snd addr2).
    1818
    19 record more_sem_params (p:params_): Type[1] ≝
     19record more_sem_params (p:params1): Type[1] ≝
    2020 { framesT: Type[0]
    21  ; regsT: Type[0] (* regs = pseudo-registers + hw registers *)
     21 ; regsT: Type[0]
    2222
    2323 ; succ_pc: succ p → address → address
     
    5555
    5656definition genv ≝ λglobals.λp:params globals. (genv_t Genv) (joint_function globals p).
    57 
    58 (*
    59 CSC: fetch_statement credo sia implementabile ⇒ globals non e' necessario ⇒ niente
    60 casino e posso back-trackare il cambiamento in SmallstepExec!!! Togliere del
    61 tutto il parametro a exec_extended.
    62 CSC: NO! RTL ha come exec_extended tail_call e (tail_)call_ptr che usa genv
    63 *)
    6457
    6558record more_sem_params2 (globals: list ident) (p: params globals) : Type[1] ≝
Note: See TracChangeset for help on using the changeset viewer.