Last change
on this file since 2566 was
2566,
checked in by piccolo, 7 years ago
|
ERTL to ERTLptr pass implemented up to a few things to be
left to the infrastructure (marked with PAOLO)
|
File size:
1.1 KB
|
Line | |
---|
1 | include "ERTL/ERTL.ma". |
---|
2 | |
---|
3 | inductive ertlptr_seq : Type[0] ≝ |
---|
4 | | ertlptr_ertl: ertl_seq → ertlptr_seq |
---|
5 | | LOW_ADDRESS : register → label → ertlptr_seq |
---|
6 | | HIGH_ADDRESS : register → label → ertlptr_seq. |
---|
7 | |
---|
8 | definition ERTLptr_uns ≝ mk_unserialized_params |
---|
9 | (* acc_a_reg ≝ *) register |
---|
10 | (* acc_b_reg ≝ *) register |
---|
11 | (* acc_a_arg ≝ *) psd_argument |
---|
12 | (* acc_b_arg ≝ *) psd_argument |
---|
13 | (* dpl_reg ≝ *) register |
---|
14 | (* dph_reg ≝ *) register |
---|
15 | (* dpl_arg ≝ *) psd_argument |
---|
16 | (* dph_arg ≝ *) psd_argument |
---|
17 | (* snd_arg ≝ *) psd_argument |
---|
18 | (* pair_move ≝ *) (move_dst × move_src) |
---|
19 | (* call_args ≝ *) ℕ |
---|
20 | (* call_dest ≝ *) unit |
---|
21 | (* ext_seq ≝ *) ertlptr_seq |
---|
22 | (* ext_seq_labels ≝ *) (λ_.[]) |
---|
23 | (* has_tailcall ≝ *) false |
---|
24 | (* paramsT ≝ *) ℕ |
---|
25 | (* localsT ≝ *) register. |
---|
26 | |
---|
27 | definition ERTLptr ≝ mk_graph_params ERTLptr_uns. |
---|
28 | definition ertlptr_program ≝ joint_program ERTLptr. |
---|
29 | |
---|
30 | definition ertlptr_seq_joint ≝ extension_seq ERTLptr. |
---|
31 | coercion ertlptr_seq_to_joint_seq : ∀globals.∀s : ertlptr_seq.joint_seq ERTLptr globals ≝ ertlptr_seq_joint |
---|
32 | on _s : ertlptr_seq to joint_seq ERTLptr. |
---|
33 | |
---|
Note: See
TracBrowser
for help on using the repository browser.