1 | |
---|
2 | include "joint/Joint_paolo.ma". |
---|
3 | include "RTL/RTL_paolo.ma". |
---|
4 | |
---|
5 | inductive move_dst: Type[0] ≝ |
---|
6 | | PSD: register → move_dst |
---|
7 | | HDW: Register → move_dst. |
---|
8 | |
---|
9 | definition move_src ≝ argument move_dst. |
---|
10 | |
---|
11 | definition move_src_from_dst : move_dst → move_src ≝ Reg move_dst. |
---|
12 | coercion move_dst_to_src : ∀r : move_dst.move_src ≝ move_src_from_dst on _r : move_dst to move_src. |
---|
13 | |
---|
14 | definition psd_argument_move_src : psd_argument → move_src ≝ |
---|
15 | λarg.match arg with |
---|
16 | [ Imm b ⇒ Imm ? b |
---|
17 | | Reg r ⇒ Reg ? (PSD r) |
---|
18 | ]. |
---|
19 | coercion psd_argument_to_move_src : ∀a:psd_argument.move_src ≝ |
---|
20 | psd_argument_move_src on _a : psd_argument to move_src. |
---|
21 | |
---|
22 | inductive ertl_seq : Type[0] ≝ |
---|
23 | | ertl_new_frame: ertl_seq |
---|
24 | | ertl_del_frame: ertl_seq |
---|
25 | | ertl_frame_size: register → ertl_seq. |
---|
26 | |
---|
27 | definition ertl_uns_params ≝ mk_unserialized_params |
---|
28 | (mk_step_params |
---|
29 | (* acc_a_reg ≝ *) register |
---|
30 | (* acc_b_reg ≝ *) register |
---|
31 | (* acc_a_arg ≝ *) psd_argument |
---|
32 | (* acc_b_arg ≝ *) psd_argument |
---|
33 | (* dpl_reg ≝ *) register |
---|
34 | (* dph_reg ≝ *) register |
---|
35 | (* dpl_arg ≝ *) psd_argument |
---|
36 | (* dph_arg ≝ *) psd_argument |
---|
37 | (* snd_arg ≝ *) psd_argument |
---|
38 | (* pair_move ≝ *) (move_dst × move_src) |
---|
39 | (* call_args ≝ *) ℕ |
---|
40 | (* call_dest ≝ *) unit |
---|
41 | (* ext_seq ≝ *) ertl_seq |
---|
42 | (* ext_call ≝ *) void |
---|
43 | (* ext_tailcall ≝ *) void |
---|
44 | ) |
---|
45 | (mk_local_params |
---|
46 | (mk_funct_params |
---|
47 | (* resultT ≝ *) unit |
---|
48 | (* paramsT ≝ *) ℕ) |
---|
49 | (* localsT ≝ *) register). |
---|
50 | |
---|
51 | definition ERTL ≝ mk_graph_params ertl_uns_params. |
---|
52 | definition ertl_program ≝ joint_program ERTL. |
---|
53 | |
---|
54 | interpretation "move" 'mov r a = (MOVE ?? (mk_Prod move_dst move_src r a)). |
---|
55 | |
---|
56 | (* aid unification *) |
---|
57 | unification hint 0 ≔ |
---|
58 | (*---------------*) ⊢ |
---|
59 | pair_move ERTL ≡ move_dst × move_src. |
---|
60 | unification hint 0 ≔ |
---|
61 | (*---------------*) ⊢ |
---|
62 | acc_a_reg ERTL ≡ register. |
---|
63 | unification hint 0 ≔ |
---|
64 | (*---------------*) ⊢ |
---|
65 | acc_b_reg ERTL ≡ register. |
---|
66 | unification hint 0 ≔ |
---|
67 | (*---------------*) ⊢ |
---|
68 | acc_a_arg ERTL ≡ psd_argument. |
---|
69 | unification hint 0 ≔ |
---|
70 | (*---------------*) ⊢ |
---|
71 | acc_b_arg ERTL ≡ psd_argument. |
---|
72 | unification hint 0 ≔ |
---|
73 | (*---------------*) ⊢ |
---|
74 | dpl_reg ERTL ≡ register. |
---|
75 | unification hint 0 ≔ |
---|
76 | (*---------------*) ⊢ |
---|
77 | dph_reg ERTL ≡ register. |
---|
78 | unification hint 0 ≔ |
---|
79 | (*---------------*) ⊢ |
---|
80 | dpl_arg ERTL ≡ psd_argument. |
---|
81 | unification hint 0 ≔ |
---|
82 | (*---------------*) ⊢ |
---|
83 | dph_arg ERTL ≡ psd_argument. |
---|
84 | unification hint 0 ≔ |
---|
85 | (*---------------*) ⊢ |
---|
86 | snd_arg ERTL ≡ psd_argument. |
---|
87 | unification hint 0 ≔ |
---|
88 | (*---------------*) ⊢ |
---|
89 | call_args ERTL ≡ ℕ. |
---|
90 | unification hint 0 ≔ |
---|
91 | (*---------------*) ⊢ |
---|
92 | call_dest ERTL ≡ unit. |
---|
93 | |
---|
94 | unification hint 0 ≔ |
---|
95 | (*---------------*) ⊢ |
---|
96 | ext_seq ERTL ≡ ertl_seq. |
---|
97 | unification hint 0 ≔ |
---|
98 | (*---------------*) ⊢ |
---|
99 | ext_call ERTL ≡ void. |
---|
100 | unification hint 0 ≔ |
---|
101 | (*---------------*) ⊢ |
---|
102 | ext_tailcall ERTL ≡ void. |
---|
103 | |
---|
104 | coercion reg_to_ertl_snd_argument : ∀r : register.snd_arg ERTL ≝ |
---|
105 | psd_argument_from_reg |
---|
106 | on _r : register to snd_arg ERTL. |
---|
107 | coercion byte_to_ertl_snd_argument : ∀b : Byte.snd_arg ERTL ≝ |
---|
108 | psd_argument_from_byte |
---|
109 | on _b : Byte to snd_arg ERTL. |
---|
110 | |
---|
111 | definition ertl_seq_joint ≝ extension_seq ERTL. |
---|
112 | coercion ertl_seq_to_joint_seq : ∀globals.∀s : ertl_seq.joint_seq ERTL globals ≝ ertl_seq_joint |
---|
113 | on _s : ertl_seq to joint_seq ERTL. |
---|