source: src/RTL/RTL_paolo.ma @ 2211

Last change on this file since 2211 was 2208, checked in by tranquil, 9 years ago
  • moving some code around
  • changed immediates to hold beval in general, not only bytes
  • fixed RTLabsToRTL after redefinitions in front end
File size: 4.7 KB
Line 
1include "joint/Joint_paolo.ma".
2
3inductive rtl_seq : Type[0] ≝
4  | rtl_stack_address: register → register → rtl_seq.
5 
6inductive rtl_call : Type[0] ≝
7  | rtl_call_ptr: register → register → list psd_argument → list register → rtl_call.
8
9inductive rtl_tailcall : Type[0] ≝
10  | rtl_tailcall_id: ident → list psd_argument → rtl_tailcall
11  | rtl_tailcall_ptr: register → register → list psd_argument → rtl_tailcall.
12
13definition rtl_uns_params ≝ mk_unserialized_params
14  (mk_step_params
15    (* acc_a_reg ≝ *) register
16    (* acc_b_reg ≝ *) register
17    (* acc_a_arg ≝ *) psd_argument
18    (* acc_b_arg ≝ *) psd_argument
19    (* dpl_reg   ≝ *) register
20    (* dph_reg   ≝ *) register
21    (* dpl_arg   ≝ *) psd_argument
22    (* dph_arg   ≝ *) psd_argument
23    (* snd_arg   ≝ *) psd_argument
24    (* pair_move ≝ *) (register × psd_argument)
25    (* call_args ≝ *) (list psd_argument)
26    (* call_dest ≝ *) (list register)
27    (* ext_seq ≝ *) rtl_seq
28    (* ext_call ≝ *) rtl_call
29    (* ext_tailcall ≝ *) rtl_tailcall
30  )
31  (mk_local_params
32    (mk_funct_params
33      (* resultT ≝ *) (list register)
34      (* paramsT ≝ *) (list register))
35      (* localsT ≝ *) register).
36
37definition rtl_params ≝ mk_graph_params rtl_uns_params.
38definition lin_rtl_params ≝ mk_lin_params rtl_uns_params.
39definition rtl_internal_function ≝
40  λglobals. joint_internal_function globals rtl_params.
41definition rtl_program ≝ joint_program rtl_params.
42definition rtl_step ≝ joint_step rtl_params.
43definition rtl_seq ≝ joint_seq rtl_params.
44definition rtl_statement ≝ joint_statement rtl_params.
45
46interpretation "move" 'mov r a = (MOVE rtl_params ? (mk_Prod ? psd_argument r a)).
47
48(* aid unification *)
49include "hints_declaration.ma".
50unification hint 0 ≔
51(*---------------*) ⊢
52acc_a_reg rtl_params ≡ register.
53unification hint 0 ≔
54(*---------------*) ⊢
55acc_b_reg rtl_params ≡ register.
56unification hint 0 ≔
57(*---------------*) ⊢
58acc_a_arg rtl_params ≡ psd_argument.
59unification hint 0 ≔
60(*---------------*) ⊢
61acc_b_arg rtl_params ≡ psd_argument.
62unification hint 0 ≔
63(*---------------*) ⊢
64dpl_reg rtl_params ≡ register.
65unification hint 0 ≔
66(*---------------*) ⊢
67dph_reg rtl_params ≡ register.
68unification hint 0 ≔
69(*---------------*) ⊢
70dpl_arg rtl_params ≡ psd_argument.
71unification hint 0 ≔
72(*---------------*) ⊢
73dph_arg rtl_params ≡ psd_argument.
74unification hint 0 ≔
75(*---------------*) ⊢
76snd_arg rtl_params ≡ psd_argument.
77unification hint 0 ≔
78(*---------------*) ⊢
79pair_move rtl_params ≡ register × psd_argument.
80unification hint 0 ≔
81(*---------------*) ⊢
82call_args rtl_params ≡ list psd_argument.
83unification hint 0 ≔
84(*---------------*) ⊢
85call_dest rtl_params ≡ list register.
86
87unification hint 0 ≔
88(*---------------*) ⊢
89ext_seq rtl_params ≡ rtl_seq.
90unification hint 0 ≔
91(*---------------*) ⊢
92ext_call rtl_params ≡ rtl_call.
93unification hint 0 ≔
94(*---------------*) ⊢
95ext_tailcall rtl_params ≡ rtl_tailcall.
96unification hint 0 ≔ globals
97(*---------------*) ⊢
98joint_step rtl_params globals ≡ rtl_step globals.
99
100unification hint 0 ≔ globals
101(*---------------*) ⊢
102joint_seq rtl_params globals ≡ rtl_seq globals.
103unification hint 0 ≔ globals
104(*---------------*) ⊢
105joint_statement (stmt_pars (graph_params_to_params rtl_params)) globals ≡ rtl_statement globals.
106
107coercion reg_to_rtl_snd_argument : ∀r : register.snd_arg rtl_params ≝ psd_argument_from_reg
108  on _r : register to snd_arg rtl_params.
109coercion byte_to_rtl_snd_argument : ∀b : Byte.snd_arg rtl_params ≝ psd_argument_from_byte
110  on _b : Byte to snd_arg rtl_params.
111
112
113(************ Same without tail calls ****************)
114
115definition rtlntc_params ≝ mk_graph_params (mk_unserialized_params
116  (mk_step_params
117    (* acc_a_reg ≝ *) register
118    (* acc_b_reg ≝ *) register
119    (* acc_a_arg ≝ *) psd_argument
120    (* acc_b_arg ≝ *) psd_argument
121    (* dpl_reg   ≝ *) register
122    (* dph_reg   ≝ *) register
123    (* dpl_arg   ≝ *) psd_argument
124    (* dph_arg   ≝ *) psd_argument
125    (* snd_arg   ≝ *) psd_argument
126    (* pair_move ≝ *) (register × psd_argument)
127    (* call_args ≝ *) (list psd_argument)
128    (* call_dest ≝ *) (list register)
129    (* ext_seq ≝ *) rtl_seq
130    (* ext_call ≝ *) rtl_call
131    (* ext_tailcall ≝ *) void
132  )
133  (mk_local_params
134    (mk_funct_params
135      (* resultT ≝ *) (list register)
136      (* paramsT ≝ *) (list register))
137      (* localsT ≝ *) register)).
138
139definition rtlntc_statement ≝ joint_statement (rtlntc_params : params).
140
141definition rtlntc_internal_function ≝
142  λglobals. joint_internal_function … globals rtlntc_params.
143
144definition rtlntc_program ≝ joint_program rtlntc_params.
Note: See TracBrowser for help on using the repository browser.