Changeset 2286 for src/ERTL/ERTL.ma
 Timestamp:
 Aug 2, 2012, 3:18:11 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ERTL/ERTL.ma
r1388 r2286 1 1 include "joint/Joint.ma". 2 2 3 inductive move_registers: Type[0] ≝ 4  pseudo: register → move_registers 5  hardware: Register → move_registers. 6 7 inductive ertl_statement_extension: Type[0] ≝ 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. 3 inductive move_dst: Type[0] ≝ 4  PSD: register → move_dst 5  HDW: Register → move_dst. 11 6 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__ (list register) nat. 17 definition ertl_params1: params1 ≝ rtl_ertl_params1 ertl_params0. 18 definition ertl_params: ∀globals. params globals ≝ rtl_ertl_params ertl_params0. 7 definition move_src ≝ argument move_dst. 19 8 20 definition ertl_statement ≝ joint_statement ertl_params_. 9 definition move_src_from_dst : move_dst → move_src ≝ Reg move_dst. 10 coercion move_dst_to_src : ∀r : move_dst.move_src ≝ move_src_from_dst on _r : move_dst to move_src. 21 11 22 definition ertl_internal_function ≝ 23 λglobals.joint_internal_function … (ertl_params globals). 12 definition psd_argument_move_src : psd_argument → move_src ≝ 13 λarg.match arg with 14 [ Imm b ⇒ Imm ? b 15  Reg r ⇒ Reg ? (PSD r) 16 ]. 17 coercion psd_argument_to_move_src : ∀a:psd_argument.move_src ≝ 18 psd_argument_move_src on _a : psd_argument to move_src. 24 19 25 definition ertl_program ≝ joint_program ertl_params. 20 inductive ertl_seq : Type[0] ≝ 21  ertl_new_frame: ertl_seq 22  ertl_del_frame: ertl_seq 23  ertl_frame_size: register → ertl_seq. 24 25 definition ERTL_uns ≝ mk_unserialized_params 26 (* acc_a_reg ≝ *) register 27 (* acc_b_reg ≝ *) register 28 (* acc_a_arg ≝ *) psd_argument 29 (* acc_b_arg ≝ *) psd_argument 30 (* dpl_reg ≝ *) register 31 (* dph_reg ≝ *) register 32 (* dpl_arg ≝ *) psd_argument 33 (* dph_arg ≝ *) psd_argument 34 (* snd_arg ≝ *) psd_argument 35 (* pair_move ≝ *) (move_dst × move_src) 36 (* call_args ≝ *) ℕ 37 (* call_dest ≝ *) unit 38 (* ext_seq ≝ *) ertl_seq 39 (* ext_call ≝ *) void 40 (* ext_tailcall ≝ *) void 41 (* paramsT ≝ *) ℕ 42 (* localsT ≝ *) register. 43 44 definition ERTL ≝ mk_graph_params ERTL_uns. 45 definition ertl_program ≝ joint_program ERTL. 46 47 interpretation "move" 'mov r a = (MOVE ?? (mk_Prod move_dst move_src r a)). 48 49 (* aid unification *) 50 unification hint 0 ≔ 51 (**) ⊢ 52 pair_move ERTL ≡ move_dst × move_src. 53 unification hint 0 ≔ 54 (**) ⊢ 55 acc_a_reg ERTL ≡ register. 56 unification hint 0 ≔ 57 (**) ⊢ 58 acc_b_reg ERTL ≡ register. 59 unification hint 0 ≔ 60 (**) ⊢ 61 acc_a_arg ERTL ≡ psd_argument. 62 unification hint 0 ≔ 63 (**) ⊢ 64 acc_b_arg ERTL ≡ psd_argument. 65 unification hint 0 ≔ 66 (**) ⊢ 67 dpl_reg ERTL ≡ register. 68 unification hint 0 ≔ 69 (**) ⊢ 70 dph_reg ERTL ≡ register. 71 unification hint 0 ≔ 72 (**) ⊢ 73 dpl_arg ERTL ≡ psd_argument. 74 unification hint 0 ≔ 75 (**) ⊢ 76 dph_arg ERTL ≡ psd_argument. 77 unification hint 0 ≔ 78 (**) ⊢ 79 snd_arg ERTL ≡ psd_argument. 80 unification hint 0 ≔ 81 (**) ⊢ 82 call_args ERTL ≡ ℕ. 83 unification hint 0 ≔ 84 (**) ⊢ 85 call_dest ERTL ≡ unit. 86 87 unification hint 0 ≔ 88 (**) ⊢ 89 ext_seq ERTL ≡ ertl_seq. 90 unification hint 0 ≔ 91 (**) ⊢ 92 ext_call ERTL ≡ void. 93 unification hint 0 ≔ 94 (**) ⊢ 95 ext_tailcall ERTL ≡ void. 96 97 coercion reg_to_ertl_snd_argument : ∀r : register.snd_arg ERTL ≝ 98 psd_argument_from_reg 99 on _r : register to snd_arg ERTL. 100 coercion byte_to_ertl_snd_argument : ∀b : Byte.snd_arg ERTL ≝ 101 psd_argument_from_byte 102 on _b : Byte to snd_arg ERTL. 103 104 definition ertl_seq_joint ≝ extension_seq ERTL. 105 coercion ertl_seq_to_joint_seq : ∀globals.∀s : ertl_seq.joint_seq ERTL globals ≝ ertl_seq_joint 106 on _s : ertl_seq to joint_seq ERTL.
Note: See TracChangeset
for help on using the changeset viewer.