- Timestamp:
- Jul 6, 2012, 11:25:43 AM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/RTL/RTL_paolo.ma
r1882 r2155 16 16 on _n : nat to rtl_argument. 17 17 18 inductive rtl_step_extension: Type[0] ≝ 19 | rtl_st_ext_stack_address: register → register → rtl_step_extension 20 | rtl_st_ext_call_ptr: register → register → list rtl_argument → list register → rtl_step_extension. 18 inductive rtl_seq : Type[0] ≝ 19 | rtl_stack_address: register → register → rtl_seq. 20 21 inductive rtl_call : Type[0] ≝ 22 | rtl_call_ptr: register → register → list rtl_argument → list register → rtl_call. 21 23 22 inductive rtl_ statement_extension: Type[0] ≝23 | rtl_ st_ext_tailcall_id: ident → list rtl_argument → rtl_statement_extension24 | rtl_ st_ext_tailcall_ptr: register → register → list rtl_argument → rtl_statement_extension.24 inductive rtl_tailcall : Type[0] ≝ 25 | rtl_tailcall_id: ident → list rtl_argument → rtl_tailcall 26 | rtl_tailcall_ptr: register → register → list rtl_argument → rtl_tailcall. 25 27 26 28 definition rtl_uns_params ≝ mk_unserialized_params … … 38 40 (* call_args ≝ *) (list rtl_argument) 39 41 (* call_dest ≝ *) (list register) 40 (* ext_s tep ≝ *) rtl_step_extension41 (* ext_ step_labels ≝ *) (λes.[ ])42 (* ext_ fin_stmt ≝ *) rtl_statement_extension43 (* ext_fin_stmt_labels ≝ *) (λes.[ ]))42 (* ext_seq ≝ *) rtl_seq 43 (* ext_call ≝ *) rtl_call 44 (* ext_tailcall ≝ *) rtl_tailcall 45 ) 44 46 (mk_local_params 45 47 (mk_funct_params 46 48 (* resultT ≝ *) (list register) 47 49 (* paramsT ≝ *) (list register)) 48 (* localsT ≝ *) (list register)).50 (* localsT ≝ *) register). 49 51 50 52 definition rtl_params ≝ mk_graph_params rtl_uns_params. … … 54 56 definition rtl_program ≝ joint_program rtl_params. 55 57 definition rtl_step ≝ joint_step rtl_params. 58 definition rtl_seq ≝ joint_seq rtl_params. 56 59 definition rtl_statement ≝ joint_statement rtl_params. 57 58 60 59 61 interpretation "move" 'mov r a = (MOVE ? ? (mk_Prod ? rtl_argument r a)). … … 63 65 unification hint 0 ≔ 64 66 (*---------------*) ⊢ 65 acc_a_reg (u_inst_pars (g_u_pars rtl_params))≡ register.67 acc_a_reg rtl_params ≡ register. 66 68 unification hint 0 ≔ 67 69 (*---------------*) ⊢ 68 acc_b_reg (u_inst_pars (g_u_pars rtl_params))≡ register.70 acc_b_reg rtl_params ≡ register. 69 71 unification hint 0 ≔ 70 72 (*---------------*) ⊢ 71 acc_a_arg (u_inst_pars (g_u_pars rtl_params))≡ rtl_argument.73 acc_a_arg rtl_params ≡ rtl_argument. 72 74 unification hint 0 ≔ 73 75 (*---------------*) ⊢ 74 acc_b_arg (u_inst_pars (g_u_pars rtl_params))≡ rtl_argument.76 acc_b_arg rtl_params ≡ rtl_argument. 75 77 unification hint 0 ≔ 76 78 (*---------------*) ⊢ 77 dpl_reg (u_inst_pars (g_u_pars rtl_params))≡ register.79 dpl_reg rtl_params ≡ register. 78 80 unification hint 0 ≔ 79 81 (*---------------*) ⊢ 80 dph_reg (u_inst_pars (g_u_pars rtl_params))≡ register.82 dph_reg rtl_params ≡ register. 81 83 unification hint 0 ≔ 82 84 (*---------------*) ⊢ 83 dpl_arg (u_inst_pars (g_u_pars rtl_params))≡ rtl_argument.85 dpl_arg rtl_params ≡ rtl_argument. 84 86 unification hint 0 ≔ 85 87 (*---------------*) ⊢ 86 dph_arg (u_inst_pars (g_u_pars rtl_params))≡ rtl_argument.88 dph_arg rtl_params ≡ rtl_argument. 87 89 unification hint 0 ≔ 88 90 (*---------------*) ⊢ 89 snd_arg (u_inst_pars (g_u_pars rtl_params))≡ rtl_argument.91 snd_arg rtl_params ≡ rtl_argument. 90 92 unification hint 0 ≔ 91 93 (*---------------*) ⊢ 92 pair_move (u_inst_pars (g_u_pars rtl_params))≡ register × rtl_argument.94 pair_move rtl_params ≡ register × rtl_argument. 93 95 unification hint 0 ≔ 94 96 (*---------------*) ⊢ 95 call_args (u_inst_pars (g_u_pars rtl_params))≡ list rtl_argument.97 call_args rtl_params ≡ list rtl_argument. 96 98 unification hint 0 ≔ 97 99 (*---------------*) ⊢ 98 call_dest (u_inst_pars (g_u_pars rtl_params))≡ list register.100 call_dest rtl_params ≡ list register. 99 101 100 102 unification hint 0 ≔ 101 103 (*---------------*) ⊢ 102 ext_step (u_inst_pars (g_u_pars rtl_params)) ≡ rtl_step_extension. 104 ext_seq rtl_params ≡ rtl_seq. 105 unification hint 0 ≔ 106 (*---------------*) ⊢ 107 ext_call rtl_params ≡ rtl_call. 108 unification hint 0 ≔ 109 (*---------------*) ⊢ 110 ext_tailcall rtl_params ≡ rtl_tailcall. 103 111 unification hint 0 ≔ globals 104 112 (*---------------*) ⊢ 105 joint_step (u_inst_pars (g_u_pars rtl_params))globals ≡ rtl_step globals.113 joint_step rtl_params globals ≡ rtl_step globals. 106 114 107 unification hint 0 ≔ 115 unification hint 0 ≔ globals 108 116 (*---------------*) ⊢ 109 ext_fin_stmt (u_inst_pars (g_u_pars rtl_params)) ≡ rtl_statement_extension.117 joint_seq rtl_params globals ≡ rtl_seq globals. 110 118 unification hint 0 ≔ globals 111 119 (*---------------*) ⊢ 112 120 joint_statement (stmt_pars (graph_params_to_params rtl_params)) globals ≡ rtl_statement globals. 113 121 122 coercion reg_to_rtl_snd_argument : ∀r : register.snd_arg rtl_params ≝ Reg 123 on _r : register to snd_arg rtl_params. 124 coercion byte_to_rtl_snd_argument : ∀b : Byte.snd_arg rtl_params ≝ Imm 125 on _b : Byte to snd_arg rtl_params. 126 127 114 128 (************ Same without tail calls ****************) 115 116 inductive rtlntc_statement_extension: Type[0] ≝117 | rtlntc_st_ext_stack_address: register → register → rtlntc_statement_extension118 | rtlntc_st_ext_call_ptr: register → register → list register → list register → rtlntc_statement_extension.119 129 120 130 definition rtlntc_params ≝ mk_graph_params (mk_unserialized_params … … 132 142 (* call_args ≝ *) (list rtl_argument) 133 143 (* call_dest ≝ *) (list register) 134 (* extend_statements ≝ *) rtlntc_statement_extension 135 (* ext_forall_labels ≝ *) (λes.[ ]) 136 void (λes.[ ])) 144 (* ext_seq ≝ *) rtl_seq 145 (* ext_call ≝ *) rtl_call 146 (* ext_tailcall ≝ *) void 147 ) 137 148 (mk_local_params 138 149 (mk_funct_params 139 150 (* resultT ≝ *) (list register) 140 151 (* paramsT ≝ *) (list register)) 141 (* localsT ≝ *) (list register))).152 (* localsT ≝ *) register)). 142 153 143 154 definition rtlntc_statement ≝ joint_statement (rtlntc_params : params).
Note: See TracChangeset
for help on using the changeset viewer.