| 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 | (λs.match s with [ LOW_ADDRESS _ l ⇒ [l] | HIGH_ADDRESS _ l ⇒ [l] | _ ⇒ [ ]]) |
|---|
| 24 | (* has_tailcall ≝ *) false |
|---|
| 25 | (* paramsT ≝ *) ℕ. |
|---|
| 26 | |
|---|
| 27 | definition ERTLptr_functs ≝ mk_get_pseudo_reg_functs ERTLptr_uns |
|---|
| 28 | (* acc_a_regs *) (λr.[r]) |
|---|
| 29 | (* acc_b_regs *) (λr.[r]) |
|---|
| 30 | (* acc_a_args *) (λarg.match arg with [ Imm _ ⇒ [ ] | Reg r ⇒ [r]]) |
|---|
| 31 | (* acc_b_args *) (λarg.match arg with [ Imm _ ⇒ [ ] | Reg r ⇒ [r]]) |
|---|
| 32 | (* dpl_regs *) (λr.[r]) |
|---|
| 33 | (* dph_regs *) (λr.[r]) |
|---|
| 34 | (* dpl_args *) (λarg.match arg with [ Imm _ ⇒ [ ] | Reg r ⇒ [r]]) |
|---|
| 35 | (* dph_args *) (λarg.match arg with [ Imm _ ⇒ [ ] | Reg r ⇒ [r]]) |
|---|
| 36 | (* snd_args *) (λarg.match arg with [ Imm _ ⇒ [ ] | Reg r ⇒ [r]]) |
|---|
| 37 | (* pair_move_regs *) (λx.(regs_from_move_dst (\fst x)) @ (regs_from_move_src (\snd x))) |
|---|
| 38 | (* f_call_args *) (λ_.[ ]) |
|---|
| 39 | (* f_call_dest *) (λ_.[ ]) |
|---|
| 40 | (* ext_seq_regs *) |
|---|
| 41 | (λs.match s with [ LOW_ADDRESS r _ ⇒ [r] |
|---|
| 42 | | HIGH_ADDRESS r _ ⇒ [r] |
|---|
| 43 | | ertlptr_ertl s' ⇒ ertl_ext_seq_regs s' |
|---|
| 44 | ]) |
|---|
| 45 | (* params_regs *) (λ_.[ ]). |
|---|
| 46 | |
|---|
| 47 | definition ERTLptr ≝ mk_graph_params (mk_uns_params ERTLptr_uns ERTLptr_functs). |
|---|
| 48 | definition ertlptr_program ≝ joint_program ERTLptr. |
|---|
| 49 | |
|---|
| 50 | definition ertlptr_seq_joint ≝ extension_seq ERTLptr. |
|---|
| 51 | coercion ertlptr_seq_to_joint_seq : ∀globals.∀s : ertlptr_seq.joint_seq ERTLptr globals ≝ ertlptr_seq_joint |
|---|
| 52 | on _s : ertlptr_seq to joint_seq ERTLptr ?. |
|---|
| 53 | |
|---|
