source: src/RTL/RTL.ma @ 2541

Last change on this file since 2541 was 2490, checked in by tranquil, 8 years ago

switched back to Byte immediate (instead of beval ones)
propagated pending changes to all passes

File size: 2.4 KB
Line 
1include "joint/Joint.ma".
2
3inductive rtl_seq : Type[0] ≝
4  | rtl_stack_address: register → register → rtl_seq.
5 
6definition RTL_uns ≝ λhas_tailcalls.mk_unserialized_params
7    (* acc_a_reg ≝ *) register
8    (* acc_b_reg ≝ *) register
9    (* acc_a_arg ≝ *) psd_argument
10    (* acc_b_arg ≝ *) psd_argument
11    (* dpl_reg   ≝ *) register
12    (* dph_reg   ≝ *) register
13    (* dpl_arg   ≝ *) psd_argument
14    (* dph_arg   ≝ *) psd_argument
15    (* snd_arg   ≝ *) psd_argument
16    (* pair_move ≝ *) (register × psd_argument)
17    (* call_args ≝ *) (list psd_argument)
18    (* call_dest ≝ *) (list register)
19    (* ext_seq ≝ *) rtl_seq
20    (* has_tailcalls ≝ *) has_tailcalls
21    (* paramsT ≝ *) (list register)
22    (* localsT ≝ *) register.
23
24definition RTL ≝ mk_graph_params (RTL_uns true).
25definition rtl_program ≝ joint_program RTL.
26
27interpretation "move" 'mov r a = (MOVE RTL ? (mk_Prod ? psd_argument r a)).
28
29(* aid unification *)
30include "hints_declaration.ma".
31unification hint 0 ≔
32(*---------------*) ⊢
33acc_a_reg RTL ≡ register.
34unification hint 0 ≔
35(*---------------*) ⊢
36acc_b_reg RTL ≡ register.
37unification hint 0 ≔
38(*---------------*) ⊢
39acc_a_arg RTL ≡ psd_argument.
40unification hint 0 ≔
41(*---------------*) ⊢
42acc_b_arg RTL ≡ psd_argument.
43unification hint 0 ≔
44(*---------------*) ⊢
45dpl_reg RTL ≡ register.
46unification hint 0 ≔
47(*---------------*) ⊢
48dph_reg RTL ≡ register.
49unification hint 0 ≔
50(*---------------*) ⊢
51dpl_arg RTL ≡ psd_argument.
52unification hint 0 ≔
53(*---------------*) ⊢
54dph_arg RTL ≡ psd_argument.
55unification hint 0 ≔
56(*---------------*) ⊢
57snd_arg RTL ≡ psd_argument.
58unification hint 0 ≔
59(*---------------*) ⊢
60pair_move RTL ≡ register × psd_argument.
61unification hint 0 ≔
62(*---------------*) ⊢
63call_args RTL ≡ list psd_argument.
64unification hint 0 ≔
65(*---------------*) ⊢
66call_dest RTL ≡ list register.
67
68unification hint 0 ≔
69(*---------------*) ⊢
70ext_seq RTL ≡ rtl_seq.
71
72coercion reg_to_rtl_snd_argument : ∀r : register.snd_arg RTL ≝ psd_argument_from_reg
73  on _r : register to snd_arg RTL.
74coercion byte_to_rtl_snd_argument : ∀b : Byte.snd_arg RTL ≝ psd_argument_from_byte
75  on _b : Byte to snd_arg RTL.
76
77
78(************ Same without tail calls ****************)
79
80definition RTL_ntc ≝ mk_graph_params (RTL_uns false).
81definition rtl_ntc_program ≝ joint_program RTL_ntc.
Note: See TracBrowser for help on using the repository browser.