source: src/RTL/RTL_paolo.ma @ 1636

Last change on this file since 1636 was 1636, checked in by tranquil, 9 years ago
  • added coercions to arguments (in RTL) and notation for ops (for the momenti in RTLabsToRTL)
  • changed slightly notations for bindLists
File size: 5.8 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_statement_extension: Type[0] ≝
22  | rtl_st_ext_stack_address: register → register → rtl_statement_extension
23  | rtl_st_ext_call_ptr: register → register → list rtl_argument → list register → rtl_statement_extension
24  | rtl_st_ext_tailcall_id: ident → list rtl_argument → rtl_statement_extension
25  | rtl_st_ext_tailcall_ptr: register → register → list rtl_argument → rtl_statement_extension.
26
27 
28inductive rtl_move : Type[0] ≝
29  | CARRY : bool → rtl_move
30  | REG : register → rtl_argument → rtl_move.
31 
32(* avoid expansion *)
33definition rtl_params : graph_params ≝ mk_graph_params
34  (mk_inst_params
35    (* acc_a_reg ≝ *) register
36    (* acc_b_reg ≝ *) register
37    (* acc_a_arg ≝ *) rtl_argument
38    (* acc_b_arg ≝ *) rtl_argument
39    (* dpl_reg   ≝ *) register
40    (* dph_reg   ≝ *) register
41    (* dpl_arg   ≝ *) rtl_argument
42    (* dph_arg   ≝ *) rtl_argument
43    (* snd_arg   ≝ *) rtl_argument
44    (* operator1 ≝ *) Op1
45    (* operator2 ≝ *) Op2
46    (* pair_move ≝ *) rtl_move
47    (* call_args ≝ *) (list rtl_argument)
48    (* call_dest ≝ *) (list register)
49    (* extend_statements ≝ *) rtl_statement_extension
50    (* ext_forall_labels ≝ *) (λP.λes.True))
51  (mk_local_params
52    (mk_funct_params
53      (* resultT ≝ *) (list register)
54      (* paramsT ≝ *) (list register))
55      (* localsT ≝ *) (list register)).
56
57(* aid unification *)
58include "hints_declaration.ma".
59unification hint 0 ≔
60(*---------------*) ⊢
61acc_a_reg (g_inst_pars rtl_params) ≡ register.
62unification hint 0 ≔
63(*---------------*) ⊢
64acc_b_reg (g_inst_pars rtl_params) ≡ register.
65unification hint 0 ≔
66(*---------------*) ⊢
67acc_a_arg (g_inst_pars rtl_params) ≡ rtl_argument.
68unification hint 0 ≔
69(*---------------*) ⊢
70acc_b_arg (g_inst_pars rtl_params) ≡ rtl_argument.
71unification hint 0 ≔
72(*---------------*) ⊢
73dpl_reg (g_inst_pars rtl_params) ≡ register.
74unification hint 0 ≔
75(*---------------*) ⊢
76dph_reg (g_inst_pars rtl_params) ≡ register.
77unification hint 0 ≔
78(*---------------*) ⊢
79dpl_arg (g_inst_pars rtl_params) ≡ rtl_argument.
80unification hint 0 ≔
81(*---------------*) ⊢
82dph_arg (g_inst_pars rtl_params) ≡ rtl_argument.
83unification hint 0 ≔
84(*---------------*) ⊢
85snd_arg (g_inst_pars rtl_params) ≡ rtl_argument.
86unification hint 0 ≔
87(*---------------*) ⊢
88operator1 (g_inst_pars rtl_params) ≡ Op1.
89unification hint 0 ≔
90(*---------------*) ⊢
91operator2 (g_inst_pars rtl_params) ≡ Op2.
92unification hint 0 ≔
93(*---------------*) ⊢
94pair_move (g_inst_pars rtl_params) ≡ rtl_move.
95unification hint 0 ≔
96(*---------------*) ⊢
97call_args (g_inst_pars rtl_params) ≡ list rtl_argument.
98unification hint 0 ≔
99(*---------------*) ⊢
100call_dest (g_inst_pars rtl_params) ≡ list register.
101
102check (λglobals,r.OP2 rtl_params globals Or r r r)
103
104definition rtl_instruction ≝ joint_instruction rtl_params.
105definition rtl_statement ≝ joint_statement rtl_params.
106
107
108definition reg_from_nat : ∀globals.register → ℕ → rtl_instruction globals ≝
109  λglobals,r,k.
110  MOVE rtl_params globals (REG r (imm_nat k)).
111
112definition reg_from_byte : ∀globals.register → Byte → rtl_instruction globals ≝
113  λglobals,r,k.
114  MOVE rtl_params globals (REG r (Imm k)).
115
116definition reg_from_reg : ∀globals.register → register → rtl_instruction globals ≝
117  λglobals,r,k.
118  MOVE … (REG r (Reg k)).
119
120definition set_carry : ∀globals.rtl_instruction globals ≝
121  λglobals.MOVE … (CARRY true).
122
123definition clear_carry : ∀globals.rtl_instruction globals ≝
124  λglobals.MOVE … (CARRY false).
125 
126
127definition rtl_internal_function ≝
128  λglobals. joint_internal_function globals rtl_params.
129
130definition rtl_program ≝ joint_program rtl_params.
131
132(************ Same without tail calls ****************)
133
134inductive rtlntc_statement_extension: Type[0] ≝
135  | rtlntc_st_ext_stack_address: register → register → rtlntc_statement_extension
136  | rtlntc_st_ext_call_ptr: register → register → list register → list register → rtlntc_statement_extension.
137
138definition rtlntc_params : graph_params ≝ mk_graph_params
139  (mk_inst_params
140    (* acc_a_reg ≝ *) register
141    (* acc_b_reg ≝ *) register
142    (* acc_a_arg ≝ *) rtl_argument
143    (* acc_b_arg ≝ *) rtl_argument
144    (* dpl_reg   ≝ *) register
145    (* dph_reg   ≝ *) register
146    (* dpl_arg   ≝ *) rtl_argument
147    (* dph_arg   ≝ *) rtl_argument
148    (* snd_arg   ≝ *) rtl_argument
149    (* operator1 ≝ *) Op1
150    (* operator2 ≝ *) Op2
151    (* pair_move ≝ *) rtl_move
152    (* call_args ≝ *) (list rtl_argument)
153    (* call_dest ≝ *) (list register)
154    (* extend_statements ≝ *) rtlntc_statement_extension
155    (* ext_forall_labels ≝ *) (λP.λes.True))
156  (mk_local_params
157    (mk_funct_params
158      (* resultT ≝ *) (list register)
159      (* paramsT ≝ *) (list register))
160      (* localsT ≝ *) (list register)).
161
162definition rtlntc_statement ≝ joint_statement rtlntc_params.
163
164definition rtlntc_internal_function ≝
165  λglobals. joint_internal_function … globals rtlntc_params.
166
167definition rtlntc_program ≝ joint_program rtlntc_params.
Note: See TracBrowser for help on using the repository browser.