Changeset 2783 for src/ERTL/ERTL.ma


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/ERTL/ERTL.ma

    r2645 r2783  
    4141    (* paramsT ≝ *) ℕ.
    4242
    43 definition ERTL ≝ mk_graph_params ERTL_uns.
     43definition regs_from_move_dst : move_dst → list register ≝
     44λm. match m with [PSD r ⇒ [r] | HDW _ ⇒ [ ] ].
     45
     46definition regs_from_move_src : move_src → list register ≝
     47λm. match m with [Imm _ ⇒ [ ] | Reg r ⇒ match r with [PSD r1 ⇒ [r1] | HDW _ ⇒ [ ] ] ].
     48
     49definition ertl_ext_seq_regs : ertl_seq → list register ≝
     50λs.match s with [ertl_frame_size r ⇒ [r] | _ ⇒ [ ]].
     51
     52definition ERTL_functs ≝ mk_get_pseudo_reg_functs ERTL_uns
     53(* acc_a_regs *) (λr.[r])
     54(* acc_b_regs *) (λr.[r])
     55(* acc_a_args *) (λarg.match arg with [ Imm _ ⇒ [ ] | Reg r ⇒ [r]])
     56(* acc_b_args *) (λarg.match arg with [ Imm _ ⇒ [ ] | Reg r ⇒ [r]])
     57(* dpl_regs *) (λr.[r])
     58(* dph_regs *) (λr.[r])
     59(* dpl_args *) (λarg.match arg with [ Imm _ ⇒ [ ] | Reg r ⇒ [r]])
     60(* dph_args *) (λarg.match arg with [ Imm _ ⇒ [ ] | Reg r ⇒ [r]])
     61(* snd_args *) (λarg.match arg with [ Imm _ ⇒ [ ] | Reg r ⇒ [r]])
     62(* pair_move_regs *) (λx.(regs_from_move_dst (\fst x)) @ (regs_from_move_src (\snd x)))
     63(* f_call_args *) (λ_.[ ])
     64(* f_call_dest *) (λ_.[ ])
     65(* ext_seq_regs *) ertl_ext_seq_regs
     66(* params_regs *) (λ_.[ ]).
     67
     68definition ERTL ≝ mk_graph_params (mk_uns_params ERTL_uns ERTL_functs).
    4469definition ertl_program ≝ joint_program ERTL.
    4570
Note: See TracChangeset for help on using the changeset viewer.