Ignore:
Timestamp:
Mar 11, 2013, 1:02:02 PM (7 years ago)
Author:
piccolo
Message:

1) Fixed a litte bug in Joint.ma
2) ERTL to ERTLptr correctness proof in place

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/TranslateUtils.ma

    r2823 r2843  
    606606definition added_registers :
    607607  ∀p : graph_params.∀g.
    608   joint_internal_function p g → (label → option (list register)) → list register ≝
     608  joint_internal_function p g → (label → list register) → list register ≝
    609609  λp,g,def,f_regs.
    610   let f ≝ λlbl : label.λ_.λacc.
    611     match f_regs lbl with [ None ⇒ acc | Some regs ⇒ regs@acc ] in
     610  let f ≝ λlbl : label.λ_.λacc.(f_regs lbl)@acc in
    612611  foldi … f (joint_if_code p g def) [ ].
    613612
     
    615614  ∀p,g,def,f_regs.
    616615  ∀l,s.stmt_at … (joint_if_code … def) l = Some ? s →
    617   opt_All … (All … (λlbl.bool_to_Prop (lbl ∈ added_registers p g def f_regs))) (f_regs l).
     616  (All … (λlbl.bool_to_Prop (lbl ∈ added_registers p g def f_regs)) (f_regs l)).
    618617
    619618(*(* translation without register allocation (more or less an alias) *)
Note: See TracChangeset for help on using the changeset viewer.