source: src/RTL/RTL_paolo.ma @ 1643

Last change on this file since 1643 was 1643, checked in by tranquil, 8 years ago
  • some changes in everything
  • separated extensions in sequential and final, to accomodate tailcalls
  • finished RTL's semantics
File size: 5.2 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
18(*CSC: XXX PROBLEM HERE. Tailcalls are not instructions, but statements since they
19  are not sequential. Thus there is a dummy label at the moment in the code.
20  To be fixed once we understand exactly what to do with tail calls. *)
21inductive rtl_instruction_extension: Type[0] ≝
22  | rtl_st_ext_stack_address: register → register → rtl_instruction_extension
23  | rtl_st_ext_call_ptr: register → register → list rtl_argument → list register → rtl_instruction_extension.
24
25inductive rtl_statement_extension : Type[0] ≝
26  | rtl_st_ext_tailcall_id: ident → list rtl_argument → rtl_statement_extension
27  | rtl_st_ext_tailcall_ptr: register → register → list rtl_argument → rtl_statement_extension.
28
29definition rtl_uns_params ≝ mk_unserialized_params
30  (mk_inst_params
31    (* acc_a_reg ≝ *) register
32    (* acc_b_reg ≝ *) register
33    (* acc_a_arg ≝ *) rtl_argument
34    (* acc_b_arg ≝ *) rtl_argument
35    (* dpl_reg   ≝ *) register
36    (* dph_reg   ≝ *) register
37    (* dpl_arg   ≝ *) rtl_argument
38    (* dph_arg   ≝ *) rtl_argument
39    (* snd_arg   ≝ *) rtl_argument
40    (* pair_move ≝ *) (register × rtl_argument)
41    (* call_args ≝ *) (list rtl_argument)
42    (* call_dest ≝ *) (list register)
43    (* ext_instruction ≝ *) rtl_instruction_extension
44    (* ext_forall_labels ≝ *) (λP.λes.True)
45    (* ext_fin_instruction ≝ *) rtl_statement_extension
46    (* ext_fin_forall_labels ≝ *) (λP.λes.True))
47  (mk_local_params
48    (mk_funct_params
49      (* resultT ≝ *) (list register)
50      (* paramsT ≝ *) (list register))
51      (* localsT ≝ *) (list register)).
52
53definition rtl_params ≝ mk_graph_params rtl_uns_params.
54definition lin_rtl_params ≝ mk_lin_params rtl_uns_params.
55
56interpretation "move" 'mov r a = (MOVE ? ? (mk_Prod ?? r a)).
57
58(* aid unification *)
59include "hints_declaration.ma".
60unification hint 0 ≔
61(*---------------*) ⊢
62acc_a_reg (u_inst_pars (g_u_pars rtl_params)) ≡ register.
63unification hint 0 ≔
64(*---------------*) ⊢
65acc_b_reg (u_inst_pars (g_u_pars rtl_params)) ≡ register.
66unification hint 0 ≔
67(*---------------*) ⊢
68acc_a_arg (u_inst_pars (g_u_pars rtl_params)) ≡ rtl_argument.
69unification hint 0 ≔
70(*---------------*) ⊢
71acc_b_arg (u_inst_pars (g_u_pars rtl_params)) ≡ rtl_argument.
72unification hint 0 ≔
73(*---------------*) ⊢
74dpl_reg (u_inst_pars (g_u_pars rtl_params)) ≡ register.
75unification hint 0 ≔
76(*---------------*) ⊢
77dph_reg (u_inst_pars (g_u_pars rtl_params)) ≡ register.
78unification hint 0 ≔
79(*---------------*) ⊢
80dpl_arg (u_inst_pars (g_u_pars rtl_params)) ≡ rtl_argument.
81unification hint 0 ≔
82(*---------------*) ⊢
83dph_arg (u_inst_pars (g_u_pars rtl_params)) ≡ rtl_argument.
84unification hint 0 ≔
85(*---------------*) ⊢
86snd_arg (u_inst_pars (g_u_pars rtl_params)) ≡ rtl_argument.
87unification hint 0 ≔
88(*---------------*) ⊢
89pair_move (u_inst_pars (g_u_pars rtl_params)) ≡ register × rtl_argument.
90unification hint 0 ≔
91(*---------------*) ⊢
92call_args (u_inst_pars (g_u_pars rtl_params)) ≡ list rtl_argument.
93unification hint 0 ≔
94(*---------------*) ⊢
95call_dest (u_inst_pars (g_u_pars rtl_params)) ≡ list register.
96
97
98definition rtl_instruction ≝ joint_instruction rtl_uns_params.
99
100definition rtl_statement ≝ joint_statement rtl_params.
101
102definition rtl_internal_function ≝
103  λglobals. joint_internal_function globals rtl_params.
104
105definition rtl_program ≝ joint_program rtl_params.
106
107(************ Same without tail calls ****************)
108
109inductive rtlntc_statement_extension: Type[0] ≝
110  | rtlntc_st_ext_stack_address: register → register → rtlntc_statement_extension
111  | rtlntc_st_ext_call_ptr: register → register → list register → list register → rtlntc_statement_extension.
112
113definition rtlntc_params ≝ mk_graph_params (mk_unserialized_params
114  (mk_inst_params
115    (* acc_a_reg ≝ *) register
116    (* acc_b_reg ≝ *) register
117    (* acc_a_arg ≝ *) rtl_argument
118    (* acc_b_arg ≝ *) rtl_argument
119    (* dpl_reg   ≝ *) register
120    (* dph_reg   ≝ *) register
121    (* dpl_arg   ≝ *) rtl_argument
122    (* dph_arg   ≝ *) rtl_argument
123    (* snd_arg   ≝ *) rtl_argument
124    (* pair_move ≝ *) (register × rtl_argument)
125    (* call_args ≝ *) (list rtl_argument)
126    (* call_dest ≝ *) (list register)
127    (* extend_statements ≝ *) rtlntc_statement_extension
128    (* ext_forall_labels ≝ *) (λP.λes.True)
129    void (λP,es.True))
130  (mk_local_params
131    (mk_funct_params
132      (* resultT ≝ *) (list register)
133      (* paramsT ≝ *) (list register))
134      (* localsT ≝ *) (list register))).
135
136definition rtlntc_statement ≝ joint_statement (rtlntc_params : params).
137
138definition rtlntc_internal_function ≝
139  λglobals. joint_internal_function … globals rtlntc_params.
140
141definition rtlntc_program ≝ joint_program rtlntc_params.
Note: See TracBrowser for help on using the repository browser.