source: src/RTL/RTL_paolo.ma @ 2214

Last change on this file since 2214 was 2214, checked in by tranquil, 8 years ago
  • changed order of parameters of joint_internal_function and genv in semantics
  • in semantics, unified more_sem_unserialized_params and more_sem_genv_params
  • renamed all <language>_params to <LANGUAGE>
File size: 3.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 ≝ 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 ≝ mk_graph_params RTL_uns.
38definition rtl_program ≝ joint_program RTL.
39
40interpretation "move" 'mov r a = (MOVE RTL ? (mk_Prod ? psd_argument r a)).
41
42(* aid unification *)
43include "hints_declaration.ma".
44unification hint 0 ≔
45(*---------------*) ⊢
46acc_a_reg RTL ≡ register.
47unification hint 0 ≔
48(*---------------*) ⊢
49acc_b_reg RTL ≡ register.
50unification hint 0 ≔
51(*---------------*) ⊢
52acc_a_arg RTL ≡ psd_argument.
53unification hint 0 ≔
54(*---------------*) ⊢
55acc_b_arg RTL ≡ psd_argument.
56unification hint 0 ≔
57(*---------------*) ⊢
58dpl_reg RTL ≡ register.
59unification hint 0 ≔
60(*---------------*) ⊢
61dph_reg RTL ≡ register.
62unification hint 0 ≔
63(*---------------*) ⊢
64dpl_arg RTL ≡ psd_argument.
65unification hint 0 ≔
66(*---------------*) ⊢
67dph_arg RTL ≡ psd_argument.
68unification hint 0 ≔
69(*---------------*) ⊢
70snd_arg RTL ≡ psd_argument.
71unification hint 0 ≔
72(*---------------*) ⊢
73pair_move RTL ≡ register × psd_argument.
74unification hint 0 ≔
75(*---------------*) ⊢
76call_args RTL ≡ list psd_argument.
77unification hint 0 ≔
78(*---------------*) ⊢
79call_dest RTL ≡ list register.
80
81unification hint 0 ≔
82(*---------------*) ⊢
83ext_seq RTL ≡ rtl_seq.
84unification hint 0 ≔
85(*---------------*) ⊢
86ext_call RTL ≡ rtl_call.
87unification hint 0 ≔
88(*---------------*) ⊢
89ext_tailcall RTL ≡ rtl_tailcall.
90
91coercion reg_to_rtl_snd_argument : ∀r : register.snd_arg RTL ≝ psd_argument_from_reg
92  on _r : register to snd_arg RTL.
93coercion byte_to_rtl_snd_argument : ∀b : Byte.snd_arg RTL ≝ psd_argument_from_byte
94  on _b : Byte to snd_arg RTL.
95
96
97(************ Same without tail calls ****************)
98
99definition RTL_ntc ≝ mk_graph_params (mk_unserialized_params
100  (mk_step_params
101    (* acc_a_reg ≝ *) register
102    (* acc_b_reg ≝ *) register
103    (* acc_a_arg ≝ *) psd_argument
104    (* acc_b_arg ≝ *) psd_argument
105    (* dpl_reg   ≝ *) register
106    (* dph_reg   ≝ *) register
107    (* dpl_arg   ≝ *) psd_argument
108    (* dph_arg   ≝ *) psd_argument
109    (* snd_arg   ≝ *) psd_argument
110    (* pair_move ≝ *) (register × psd_argument)
111    (* call_args ≝ *) (list psd_argument)
112    (* call_dest ≝ *) (list register)
113    (* ext_seq ≝ *) rtl_seq
114    (* ext_call ≝ *) rtl_call
115    (* ext_tailcall ≝ *) void
116  )
117  (mk_local_params
118    (mk_funct_params
119      (* resultT ≝ *) (list register)
120      (* paramsT ≝ *) (list register))
121      (* localsT ≝ *) register)).
122
123definition rtl_ntc_program ≝ joint_program RTL_ntc.
Note: See TracBrowser for help on using the repository browser.