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