Changeset 2217 for src/ERTL


Ignore:
Timestamp:
Jul 19, 2012, 6:13:54 PM (8 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
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTL_paolo.ma

    r2214 r2217  
    2525  | ertl_frame_size: register → ertl_seq.
    2626
    27 definition ertl_uns_params ≝ mk_unserialized_params
    28   (mk_step_params
     27definition ERTL_uns ≝ mk_unserialized_params
    2928    (* acc_a_reg ≝ *) register
    3029    (* acc_b_reg ≝ *) register
     
    4241    (* ext_call ≝ *) void
    4342    (* ext_tailcall ≝ *) void
    44   )
    45   (mk_local_params
    46     (mk_funct_params
    47       (* resultT ≝ *) unit
    48       (* paramsT ≝ *) ℕ)
    49       (* localsT ≝ *) register).
     43    (* paramsT ≝ *) ℕ
     44    (* localsT ≝ *) register.
    5045
    51 definition ERTL ≝ mk_graph_params ertl_uns_params.
     46definition ERTL ≝ mk_graph_params ERTL_uns.
    5247definition ertl_program ≝ joint_program ERTL.
    5348
Note: See TracChangeset for help on using the changeset viewer.