Changeset 2217 for src/LIN


Ignore:
Timestamp:
Jul 19, 2012, 6:13:54 PM (7 years ago)
Author:
tranquil
Message:
  • collapsed step_params, unserialized_params, funct_params and local_params into one (unserialized_params)
  • completed update of RTL, LTL and LIN semantics
Location:
src/LIN
Files:
2 added
1 edited

Legend:

Unmodified
Added
Removed
  • src/LIN/joint_LTL_LIN_paolo.ma

    r2214 r2217  
    1313
    1414definition LTL_LIN : unserialized_params ≝ mk_unserialized_params
    15   (mk_step_params
    1615    (* acc_a_reg ≝ *) unit
    1716    (* acc_b_reg ≝ *) unit
     
    2928    (* ext_call ≝ *) void
    3029    (* ext_tailcall ≝ *) void
    31   )
    32   (mk_local_params
    33     (mk_funct_params
    34       (* resultT ≝ *) unit
    35       (* paramsT ≝ *) unit)
    36       (* localsT ≝ *) void).
     30    (* paramsT ≝ *) unit
     31    (* localsT ≝ *) void.
    3732
    3833interpretation "move from acc" 'mov a b = (MOVE ?? (from_acc a b)).
Note: See TracChangeset for help on using the changeset viewer.