source: src/RTL/RTL_paolo.ma @ 2131

Last change on this file since 2131 was 1882, checked in by tranquil, 9 years ago

big update, alas incomplete:
joint changed a bit, and all BE languages need to be updated
started development of blocks to aid preservation results, but still incomplete
if it breaks too many things, feel free to roll back
File size: 5.5 KB
Line 
1include "joint/Joint_paolo.ma".
2
3inductive rtl_argument : Type[0] ≝
4  | Reg : register → rtl_argument
5  | Imm : Byte → rtl_argument.
6 
7coercion reg_to_rtl_argument : ∀r : register.rtl_argument ≝ Reg
8  on _r : register to rtl_argument.
9
10coercion byte_to_rtl_argument : ∀b : Byte.rtl_argument ≝ Imm
11  on _b : Byte to rtl_argument.
12
13definition imm_nat : nat → rtl_argument ≝ λn.Imm (nat_to_bv ? n).
14 
15coercion nat_to_rtl_argument : ∀n : nat.rtl_argument ≝ imm_nat
16  on _n : nat to rtl_argument.
17
18inductive 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.
21
22inductive rtl_statement_extension : Type[0] ≝
23  | rtl_st_ext_tailcall_id: ident → list rtl_argument → rtl_statement_extension
24  | rtl_st_ext_tailcall_ptr: register → register → list rtl_argument → rtl_statement_extension.
25
26definition rtl_uns_params ≝ mk_unserialized_params
27  (mk_step_params
28    (* acc_a_reg ≝ *) register
29    (* acc_b_reg ≝ *) register
30    (* acc_a_arg ≝ *) rtl_argument
31    (* acc_b_arg ≝ *) rtl_argument
32    (* dpl_reg   ≝ *) register
33    (* dph_reg   ≝ *) register
34    (* dpl_arg   ≝ *) rtl_argument
35    (* dph_arg   ≝ *) rtl_argument
36    (* snd_arg   ≝ *) rtl_argument
37    (* pair_move ≝ *) (register × rtl_argument)
38    (* call_args ≝ *) (list rtl_argument)
39    (* call_dest ≝ *) (list register)
40    (* ext_step ≝ *) rtl_step_extension
41    (* ext_step_labels ≝ *) (λes.[ ])
42    (* ext_fin_stmt ≝ *) rtl_statement_extension
43    (* ext_fin_stmt_labels ≝ *) (λes.[ ]))
44  (mk_local_params
45    (mk_funct_params
46      (* resultT ≝ *) (list register)
47      (* paramsT ≝ *) (list register))
48      (* localsT ≝ *) (list register)).
49
50definition rtl_params ≝ mk_graph_params rtl_uns_params.
51definition lin_rtl_params ≝ mk_lin_params rtl_uns_params.
52definition rtl_internal_function ≝
53  λglobals. joint_internal_function globals rtl_params.
54definition rtl_program ≝ joint_program rtl_params.
55definition rtl_step ≝ joint_step rtl_params.
56definition rtl_statement ≝ joint_statement rtl_params.
57
58
59interpretation "move" 'mov r a = (MOVE ? ? (mk_Prod ? rtl_argument r a)).
60
61(* aid unification *)
62include "hints_declaration.ma".
63unification hint 0 ≔
64(*---------------*) ⊢
65acc_a_reg (u_inst_pars (g_u_pars rtl_params)) ≡ register.
66unification hint 0 ≔
67(*---------------*) ⊢
68acc_b_reg (u_inst_pars (g_u_pars rtl_params)) ≡ register.
69unification hint 0 ≔
70(*---------------*) ⊢
71acc_a_arg (u_inst_pars (g_u_pars rtl_params)) ≡ rtl_argument.
72unification hint 0 ≔
73(*---------------*) ⊢
74acc_b_arg (u_inst_pars (g_u_pars rtl_params)) ≡ rtl_argument.
75unification hint 0 ≔
76(*---------------*) ⊢
77dpl_reg (u_inst_pars (g_u_pars rtl_params)) ≡ register.
78unification hint 0 ≔
79(*---------------*) ⊢
80dph_reg (u_inst_pars (g_u_pars rtl_params)) ≡ register.
81unification hint 0 ≔
82(*---------------*) ⊢
83dpl_arg (u_inst_pars (g_u_pars rtl_params)) ≡ rtl_argument.
84unification hint 0 ≔
85(*---------------*) ⊢
86dph_arg (u_inst_pars (g_u_pars rtl_params)) ≡ rtl_argument.
87unification hint 0 ≔
88(*---------------*) ⊢
89snd_arg (u_inst_pars (g_u_pars rtl_params)) ≡ rtl_argument.
90unification hint 0 ≔
91(*---------------*) ⊢
92pair_move (u_inst_pars (g_u_pars rtl_params)) ≡ register × rtl_argument.
93unification hint 0 ≔
94(*---------------*) ⊢
95call_args (u_inst_pars (g_u_pars rtl_params)) ≡ list rtl_argument.
96unification hint 0 ≔
97(*---------------*) ⊢
98call_dest (u_inst_pars (g_u_pars rtl_params)) ≡ list register.
99
100unification hint 0 ≔
101(*---------------*) ⊢
102ext_step (u_inst_pars (g_u_pars rtl_params)) ≡ rtl_step_extension.
103unification hint 0 ≔ globals
104(*---------------*) ⊢
105joint_step (u_inst_pars (g_u_pars rtl_params)) globals ≡ rtl_step globals.
106
107unification hint 0 ≔
108(*---------------*) ⊢
109ext_fin_stmt (u_inst_pars (g_u_pars rtl_params)) ≡ rtl_statement_extension.
110unification hint 0 ≔ globals
111(*---------------*) ⊢
112joint_statement (stmt_pars (graph_params_to_params rtl_params)) globals ≡ rtl_statement globals.
113
114(************ Same without tail calls ****************)
115
116inductive rtlntc_statement_extension: Type[0] ≝
117  | rtlntc_st_ext_stack_address: register → register → rtlntc_statement_extension
118  | rtlntc_st_ext_call_ptr: register → register → list register → list register → rtlntc_statement_extension.
119
120definition rtlntc_params ≝ mk_graph_params (mk_unserialized_params
121  (mk_step_params
122    (* acc_a_reg ≝ *) register
123    (* acc_b_reg ≝ *) register
124    (* acc_a_arg ≝ *) rtl_argument
125    (* acc_b_arg ≝ *) rtl_argument
126    (* dpl_reg   ≝ *) register
127    (* dph_reg   ≝ *) register
128    (* dpl_arg   ≝ *) rtl_argument
129    (* dph_arg   ≝ *) rtl_argument
130    (* snd_arg   ≝ *) rtl_argument
131    (* pair_move ≝ *) (register × rtl_argument)
132    (* call_args ≝ *) (list rtl_argument)
133    (* call_dest ≝ *) (list register)
134    (* extend_statements ≝ *) rtlntc_statement_extension
135    (* ext_forall_labels ≝ *) (λes.[ ])
136    void (λes.[ ]))
137  (mk_local_params
138    (mk_funct_params
139      (* resultT ≝ *) (list register)
140      (* paramsT ≝ *) (list register))
141      (* localsT ≝ *) (list register))).
142
143definition rtlntc_statement ≝ joint_statement (rtlntc_params : params).
144
145definition rtlntc_internal_function ≝
146  λglobals. joint_internal_function … globals rtlntc_params.
147
148definition rtlntc_program ≝ joint_program rtlntc_params.
Note: See TracBrowser for help on using the repository browser.