Ignore:
Timestamp:
Mar 6, 2013, 12:09:52 PM (7 years ago)
Author:
piccolo
Message:

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

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTLptr/ERTLptr.ma

    r2674 r2783  
    2424    (* has_tailcall ≝ *) false
    2525    (* paramsT ≝ *) ℕ.
     26   
     27definition 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 *) (λ_.[ ]).
    2646
    27 definition ERTLptr ≝ mk_graph_params ERTLptr_uns.
     47definition ERTLptr ≝ mk_graph_params (mk_uns_params ERTLptr_uns ERTLptr_functs).
    2848definition ertlptr_program ≝ joint_program ERTLptr.
    2949 
Note: See TracChangeset for help on using the changeset viewer.