- Timestamp:
- Jan 11, 2012, 5:41:45 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/RTL/RTL_paolo.ma
r1636 r1640 25 25 | rtl_st_ext_tailcall_ptr: register → register → list rtl_argument → rtl_statement_extension. 26 26 27 28 inductive rtl_move : Type[0] ≝ 29 | CARRY : bool → rtl_move 30 | REG : register → rtl_argument → rtl_move. 31 32 (* avoid expansion *) 33 definition rtl_params : graph_params ≝ mk_graph_params 27 definition rtl_params ≝ mk_graph_params (mk_unserialized_params 34 28 (mk_inst_params 35 29 (* acc_a_reg ≝ *) register … … 42 36 (* dph_arg ≝ *) rtl_argument 43 37 (* snd_arg ≝ *) rtl_argument 44 (* operator1 ≝ *) Op1 45 (* operator2 ≝ *) Op2 46 (* pair_move ≝ *) rtl_move 38 (* pair_move ≝ *) (register × rtl_argument) 47 39 (* call_args ≝ *) (list rtl_argument) 48 40 (* call_dest ≝ *) (list register) … … 53 45 (* resultT ≝ *) (list register) 54 46 (* paramsT ≝ *) (list register)) 55 (* localsT ≝ *) (list register)). 47 (* localsT ≝ *) (list register))). 48 49 interpretation "move" 'mov r a = (MOVE ? ? (mk_Prod ?? r a)). 56 50 57 51 (* aid unification *) … … 59 53 unification hint 0 ≔ 60 54 (*---------------*) ⊢ 61 acc_a_reg ( g_inst_pars rtl_params) ≡ register.55 acc_a_reg (u_inst_pars (g_u_pars rtl_params)) ≡ register. 62 56 unification hint 0 ≔ 63 57 (*---------------*) ⊢ 64 acc_b_reg ( g_inst_pars rtl_params) ≡ register.58 acc_b_reg (u_inst_pars (g_u_pars rtl_params)) ≡ register. 65 59 unification hint 0 ≔ 66 60 (*---------------*) ⊢ 67 acc_a_arg ( g_inst_pars rtl_params) ≡ rtl_argument.61 acc_a_arg (u_inst_pars (g_u_pars rtl_params)) ≡ rtl_argument. 68 62 unification hint 0 ≔ 69 63 (*---------------*) ⊢ 70 acc_b_arg ( g_inst_pars rtl_params) ≡ rtl_argument.64 acc_b_arg (u_inst_pars (g_u_pars rtl_params)) ≡ rtl_argument. 71 65 unification hint 0 ≔ 72 66 (*---------------*) ⊢ 73 dpl_reg ( g_inst_pars rtl_params) ≡ register.67 dpl_reg (u_inst_pars (g_u_pars rtl_params)) ≡ register. 74 68 unification hint 0 ≔ 75 69 (*---------------*) ⊢ 76 dph_reg ( g_inst_pars rtl_params) ≡ register.70 dph_reg (u_inst_pars (g_u_pars rtl_params)) ≡ register. 77 71 unification hint 0 ≔ 78 72 (*---------------*) ⊢ 79 dpl_arg ( g_inst_pars rtl_params) ≡ rtl_argument.73 dpl_arg (u_inst_pars (g_u_pars rtl_params)) ≡ rtl_argument. 80 74 unification hint 0 ≔ 81 75 (*---------------*) ⊢ 82 dph_arg ( g_inst_pars rtl_params) ≡ rtl_argument.76 dph_arg (u_inst_pars (g_u_pars rtl_params)) ≡ rtl_argument. 83 77 unification hint 0 ≔ 84 78 (*---------------*) ⊢ 85 snd_arg ( g_inst_pars rtl_params) ≡ rtl_argument.79 snd_arg (u_inst_pars (g_u_pars rtl_params)) ≡ rtl_argument. 86 80 unification hint 0 ≔ 87 81 (*---------------*) ⊢ 88 operator1 (g_inst_pars rtl_params) ≡ Op1.82 pair_move (u_inst_pars (g_u_pars rtl_params)) ≡ register × rtl_argument. 89 83 unification hint 0 ≔ 90 84 (*---------------*) ⊢ 91 operator2 (g_inst_pars rtl_params) ≡ Op2.85 call_args (u_inst_pars (g_u_pars rtl_params)) ≡ list rtl_argument. 92 86 unification hint 0 ≔ 93 87 (*---------------*) ⊢ 94 pair_move (g_inst_pars rtl_params) ≡ rtl_move. 95 unification hint 0 ≔ 96 (*---------------*) ⊢ 97 call_args (g_inst_pars rtl_params) ≡ list rtl_argument. 98 unification hint 0 ≔ 99 (*---------------*) ⊢ 100 call_dest (g_inst_pars rtl_params) ≡ list register. 88 call_dest (u_inst_pars (g_u_pars rtl_params)) ≡ list register. 101 89 102 check (λglobals,r.OP2 rtl_params globals Or r r r)103 90 104 91 definition rtl_instruction ≝ joint_instruction rtl_params. 105 definition rtl_statement ≝ joint_statement rtl_params. 106 107 108 definition reg_from_nat : ∀globals.register → ℕ → rtl_instruction globals ≝ 109 λglobals,r,k. 110 MOVE rtl_params globals (REG r (imm_nat k)). 111 112 definition reg_from_byte : ∀globals.register → Byte → rtl_instruction globals ≝ 113 λglobals,r,k. 114 MOVE rtl_params globals (REG r (Imm k)). 115 116 definition reg_from_reg : ∀globals.register → register → rtl_instruction globals ≝ 117 λglobals,r,k. 118 MOVE … (REG r (Reg k)). 119 120 definition set_carry : ∀globals.rtl_instruction globals ≝ 121 λglobals.MOVE … (CARRY true). 122 123 definition clear_carry : ∀globals.rtl_instruction globals ≝ 124 λglobals.MOVE … (CARRY false). 125 92 (* Paolo: can't understand why coercions do not compose implicitly here *) 93 definition rtl_statement ≝ joint_statement (rtl_params : params). 126 94 127 95 definition rtl_internal_function ≝ … … 136 104 | rtlntc_st_ext_call_ptr: register → register → list register → list register → rtlntc_statement_extension. 137 105 138 definition rtlntc_params : graph_params ≝ mk_graph_params106 definition rtlntc_params ≝ mk_graph_params (mk_unserialized_params 139 107 (mk_inst_params 140 108 (* acc_a_reg ≝ *) register … … 147 115 (* dph_arg ≝ *) rtl_argument 148 116 (* snd_arg ≝ *) rtl_argument 149 (* operator1 ≝ *) Op1 150 (* operator2 ≝ *) Op2 151 (* pair_move ≝ *) rtl_move 117 (* pair_move ≝ *) (register × rtl_argument) 152 118 (* call_args ≝ *) (list rtl_argument) 153 119 (* call_dest ≝ *) (list register) … … 158 124 (* resultT ≝ *) (list register) 159 125 (* paramsT ≝ *) (list register)) 160 (* localsT ≝ *) (list register)) .126 (* localsT ≝ *) (list register))). 161 127 162 definition rtlntc_statement ≝ joint_statement rtlntc_params.128 definition rtlntc_statement ≝ joint_statement (rtlntc_params : params). 163 129 164 130 definition rtlntc_internal_function ≝
Note: See TracChangeset
for help on using the changeset viewer.