Changeset 1242 for src/ERTL/ERTL.ma
- Timestamp:
- Sep 21, 2011, 5:35:54 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ERTL/ERTL.ma
r1241 r1242 1 1 include "joint/Joint.ma". 2 include "common/Graphs.ma".3 4 definition registers ≝ list register.5 2 6 3 inductive move_registers: Type[0] ≝ … … 13 10 | ertl_st_ext_frame_size: register → label → ertl_statement_extension. 14 11 15 definition ertl_params_: params_ ≝ 16 mk_params_ register register register register 12 definition ertl_params: params ≝ 13 mk_params 14 (mk_params_ register register register register 17 15 (move_registers × move_registers) register 18 ertl_statement_extension unit (list register) nat. 19 20 definition ertl_params: params ≝ 21 mk_params ertl_params_ label. 16 ertl_statement_extension unit (list register) nat) label. 22 17 23 18 definition ertl_statement ≝ joint_statement ertl_params. 24 19 25 (* 26 definition ertl_sem_params_ : ∀globals. sem_params_ ertl_params globals ≝ 27 λglobals. 28 mk_sem_params_ ertl_params globals (graph (ertl_statement globals)) (lookup …). 29 *) 30 31 definition ertl_internal_function ≝ 32 joint_internal_function ertl_params. 20 definition ertl_internal_function ≝ joint_internal_function ertl_params. 33 21 34 22 definition ertl_program ≝ joint_program ertl_params.
Note: See TracChangeset
for help on using the changeset viewer.