|
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.
