Changeset 1641 for src/RTL


Ignore:
Timestamp:
Jan 11, 2012, 8:03:53 PM (9 years ago)
Author:
tranquil
Message:
  • semanticsUtils_paolo.ma contains code to generate both graph and linear semantics parameters (partially migrated from LIN/semantics.ma)
  • fetch_function is now common to both graph and linear
  • started porting RTL's semantics
Location:
src/RTL
Files:
1 added
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/RTL_paolo.ma

    r1640 r1641  
    2525  | rtl_st_ext_tailcall_ptr: register → register → list rtl_argument → rtl_statement_extension.
    2626
    27 definition rtl_params ≝ mk_graph_params (mk_unserialized_params
     27definition rtl_uns_params ≝ mk_unserialized_params
    2828  (mk_inst_params
    2929    (* acc_a_reg ≝ *) register
     
    4545      (* resultT ≝ *) (list register)
    4646      (* paramsT ≝ *) (list register))
    47       (* localsT ≝ *) (list register))).
     47      (* localsT ≝ *) (list register)).
     48
     49definition rtl_params ≝ mk_graph_params rtl_uns_params.
     50definition lin_rtl_params ≝ mk_lin_params rtl_uns_params.
    4851
    4952interpretation "move" 'mov r a = (MOVE ? ? (mk_Prod ?? r a)).
     
    8992
    9093
    91 definition rtl_instruction ≝ joint_instruction rtl_params.
    92 (* Paolo: can't understand why coercions do not compose implicitly here *)
    93 definition rtl_statement ≝ joint_statement (rtl_params : params).
     94definition rtl_instruction ≝ joint_instruction rtl_uns_params.
     95
     96definition rtl_statement ≝ joint_statement rtl_params.
    9497
    9598definition rtl_internal_function ≝
Note: See TracChangeset for help on using the changeset viewer.