Changeset 1311 for Deliverables/D3.3/id-lookup-branch/ERTL/ERTL.ma
- Timestamp:
- Oct 6, 2011, 6:45:54 PM (10 years ago)
- Location:
- Deliverables/D3.3/id-lookup-branch
- Files:
-
- 2 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D3.3/id-lookup-branch
- Property svn:mergeinfo changed
/src merged: 1198,1206-1233,1236-1260,1262-1264,1266,1268-1271,1274-1276,1278-1290,1292
- Property svn:mergeinfo changed
-
Deliverables/D3.3/id-lookup-branch/ERTL/ERTL.ma
r1197 r1311 1 include "ASM/I8051.ma".2 1 include "joint/Joint.ma". 3 include "utilities/BitVectorTrieSet.ma".4 include "utilities/IdentifierTools.ma".5 include "common/Graphs.ma".6 include "common/CostLabel.ma".7 include "common/Registers.ma".8 9 definition registers ≝ list register.10 2 11 3 inductive move_registers: Type[0] ≝ … … 14 6 15 7 inductive ertl_statement_extension: Type[0] ≝ 16 | ertl_st_ext_new_frame: label →ertl_statement_extension17 | ertl_st_ext_del_frame: label →ertl_statement_extension18 | ertl_st_ext_frame_size: register → label →ertl_statement_extension.8 | ertl_st_ext_new_frame: ertl_statement_extension 9 | ertl_st_ext_del_frame: ertl_statement_extension 10 | ertl_st_ext_frame_size: register → ertl_statement_extension. 19 11 20 definition ertl_params: params ≝ 21 mk_params 22 register register register register 23 (move_registers × move_registers) register 24 ertl_statement_extension unit (list register) nat. 12 definition ertl_params__: params__ ≝ 13 mk_params__ register register register register (move_registers × move_registers) 14 register nat unit ertl_statement_extension. 15 definition ertl_params_: params_ ≝ graph_params_ ertl_params__. 16 definition ertl_params0: params0 ≝ mk_params0 ertl_params__ unit nat. 17 definition ertl_params1: params1 ≝ rtl_ertl_params1 ertl_params0. 18 definition ertl_params: ∀globals. params globals ≝ rtl_ertl_params ertl_params0. 25 19 26 definition ertl_statement ≝ joint_statement ertl_params .20 definition ertl_statement ≝ joint_statement ertl_params_. 27 21 28 definition ertl_statement_graph ≝ λglobals. graph (ertl_statement globals). 22 definition ertl_internal_function ≝ 23 λglobals.joint_internal_function … (ertl_params globals). 29 24 30 record ertl_internal_function (globals: list ident): Type[0] ≝ 31 { 32 ertl_if_luniverse: universe LabelTag; 33 ertl_if_runiverse: universe RegisterTag; 34 ertl_if_params: nat; 35 ertl_if_locals: registers; 36 ertl_if_stacksize: nat; 37 ertl_if_graph: ertl_statement_graph globals; 38 ertl_if_entry: Σl: label. lookup ? ? ertl_if_graph l ≠ None ?; 39 ertl_if_exit: Σl: label. lookup ? ? ertl_if_graph l ≠ None ? 40 }. 41 42 definition set_luniverse ≝ 43 λglobals : list ident. 44 λint_fun : ertl_internal_function globals. 45 λluniverse: universe LabelTag. 46 let runiverse ≝ ertl_if_runiverse globals int_fun in 47 let params ≝ ertl_if_params globals int_fun in 48 let locals ≝ ertl_if_locals globals int_fun in 49 let stacksize ≝ ertl_if_stacksize globals int_fun in 50 let graph ≝ ertl_if_graph globals int_fun in 51 let entry ≝ ertl_if_entry globals int_fun in 52 let exit ≝ ertl_if_exit globals int_fun in 53 mk_ertl_internal_function globals 54 luniverse runiverse params locals 55 stacksize graph entry exit. 56 57 definition ertl_function ≝ λglobals. fundef (ertl_internal_function globals). 58 59 record ertl_program (globals: list ident): Type[0] ≝ 60 { 61 ertl_pr_vars: list (ident × nat); 62 ertl_pr_funcs: list (ident × (ertl_function globals)); 63 ertl_pr_main: option ident 64 }. 65 66 67 (* XXX: changed from O'Caml 68 | ertl_st_addr_h: register → ident → label → ertl_statement 69 | ertl_st_addr_l: register → ident → label → ertl_statement 70 *) 71 72 (* XXX: changed from O'Caml 73 | ertl_st_opaccs_a: OpAccs → register → register → register → label → ertl_statement 74 | ertl_st_opaccs_b: OpAccs → register → register → register → label → ertl_statement 75 *) 25 definition ertl_program ≝ joint_program ertl_params.
Note: See TracChangeset
for help on using the changeset viewer.