Ignore:
Timestamp:
Oct 5, 2011, 3:19:40 PM (9 years ago)
Author:
sacerdot
Message:

RTL semantics: porting to joint semantics started.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/semantics.ma

    r1289 r1294  
    3434 ; dph_store_: dph_reg p → beval → regsT → res regsT
    3535 ; dph_retrieve_: regsT → dph_reg p → res beval
    36  ; pair_reg_move_: regsT → pair_reg p → regsT
     36 ; pair_reg_move_: regsT → pair_reg p → res regsT
    3737 
    3838 ; pointer_of_label: label → Σp:pointer. ptype p = Code
     
    6161 
    6262 ; fetch_statement: state (mk_sem_params … more_sparams) → res (joint_statement (mk_sem_params … more_sparams) globals)
     63 ; fetch_result: state (mk_sem_params … more_sparams) → nat → res val
     64
    6365 ; fetch_external_args: external_function → state (mk_sem_params … more_sparams) → res (list val)
    6466 ; set_result: list val → state (mk_sem_params … more_sparams) → res (state (mk_sem_params … more_sparams))
    65  ; fetch_result: state (mk_sem_params … more_sparams) → nat → res val
    6667
    6768 ; exec_extended: genv globals p → extend_statements (mk_sem_params … more_sparams) → state (mk_sem_params … more_sparams) → IO io_out io_in (trace × (state (mk_sem_params … more_sparams)))
     
    155156 λp,st,dst.dph_retrieve_ … (regs … st) dst.
    156157
    157 definition pair_reg_move: ∀p:sem_params. state p → pair_reg p → state p ≝
    158  λp,st,rs.set_regs … (pair_reg_move_ … (regs … st) rs) st.
     158definition pair_reg_move: ∀p:sem_params. state p → pair_reg p → res (state p) ≝
     159 λp,st,rs.
     160  do regs ← pair_reg_move_ … (regs … st) rs;
     161  OK … (set_regs … regs st).
    159162
    160163definition save_frame: ∀p:sem_params. state p → state p ≝
     
    276279          ret ? 〈E0, next … l st〉
    277280      | MOVE dst_src ⇒
    278           ret ? 〈E0, next … l (pair_reg_move … st dst_src)〉
     281        ! st ← pair_reg_move … st dst_src ;
     282          ret ? 〈E0, next … l st〉
    279283      (*CSC: XXX bug here dest unused *)
    280284      | CALL_ID id argsno dest ⇒
Note: See TracChangeset for help on using the changeset viewer.