source: src/RTL/RTL.ma @ 2860

Last change on this file since 2860 was 2783, checked in by piccolo, 7 years ago

modified joint_closed_internal_function definition (added condition on pseudo-registers)
added new record for parameters
modified state definition with option for framesT

File size: 3.0 KB
Line 
1include "joint/Joint.ma".
2
3inductive rtl_seq : Type[0] ≝
4  | rtl_stack_address: register → register → rtl_seq.
5 
6definition RTL_uns ≝ 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    (* ext_seq_labels ≝ *) (λ_.[])
21    (* has_tailcalls ≝ *) false
22    (* paramsT ≝ *) (list register).
23
24definition RTL_functs ≝ mk_get_pseudo_reg_functs RTL_uns
25(* acc_a_regs *) (λr.[r])
26(* acc_b_regs *) (λr.[r])
27(* acc_a_args *) (λa. match a with [Reg r ⇒ [r] |Imm _ ⇒ [ ]])
28(* acc_b_args *) (λa. match a with [Reg r ⇒ [r] |Imm _ ⇒ [ ]])
29(* dpl_regs *) (λr.[r])
30(* dph_regs *) (λr.[r])
31(* dpl_args *) (λa. match a with [Reg r ⇒ [r] |Imm _ ⇒ [ ]])
32(* dph_args *) (λa. match a with [Reg r ⇒ [r] |Imm _ ⇒ [ ]])
33(* snd_args *) (λa. match a with [Reg r ⇒ [r] |Imm _ ⇒ [ ]])
34(* pair_move_regs *) (λx.[\fst x] @ (match \snd x with [Reg r ⇒ [r] |Imm _ ⇒ [ ]]))
35(* f_call_args *) (λl.foldl ?? (λl1.λa.l1@(match a with [Reg r ⇒ [r] |Imm _ ⇒ [ ]])) [ ] l)
36(* f_call_dest *) (λx.x)
37(* ext_seq_regs *) (λext.match ext with [rtl_stack_address r1 r2 ⇒ [r1;r2]])
38(* params_regs *) (λx.x).
39
40definition RTL ≝ mk_graph_params (mk_uns_params RTL_uns RTL_functs).
41definition rtl_program ≝ joint_program RTL.
42
43interpretation "move" 'mov r a = (MOVE RTL ? (mk_Prod ? psd_argument r a)).
44
45(* aid unification *)
46include "hints_declaration.ma".
47unification hint 0 ≔
48(*---------------*) ⊢
49acc_a_reg RTL ≡ register.
50unification hint 0 ≔
51(*---------------*) ⊢
52acc_b_reg RTL ≡ register.
53unification hint 0 ≔
54(*---------------*) ⊢
55acc_a_arg RTL ≡ psd_argument.
56unification hint 0 ≔
57(*---------------*) ⊢
58acc_b_arg RTL ≡ psd_argument.
59unification hint 0 ≔
60(*---------------*) ⊢
61dpl_reg RTL ≡ register.
62unification hint 0 ≔
63(*---------------*) ⊢
64dph_reg RTL ≡ register.
65unification hint 0 ≔
66(*---------------*) ⊢
67dpl_arg RTL ≡ psd_argument.
68unification hint 0 ≔
69(*---------------*) ⊢
70dph_arg RTL ≡ psd_argument.
71unification hint 0 ≔
72(*---------------*) ⊢
73snd_arg RTL ≡ psd_argument.
74unification hint 0 ≔
75(*---------------*) ⊢
76pair_move RTL ≡ register × psd_argument.
77unification hint 0 ≔
78(*---------------*) ⊢
79call_args RTL ≡ list psd_argument.
80unification hint 0 ≔
81(*---------------*) ⊢
82call_dest RTL ≡ list register.
83
84unification hint 0 ≔
85(*---------------*) ⊢
86ext_seq RTL ≡ rtl_seq.
87
88coercion reg_to_rtl_snd_argument : ∀r : register.snd_arg RTL ≝ psd_argument_from_reg
89  on _r : register to snd_arg RTL.
90coercion byte_to_rtl_snd_argument : ∀b : Byte.snd_arg RTL ≝ psd_argument_from_byte
91  on _b : Byte to snd_arg RTL.
Note: See TracBrowser for help on using the repository browser.