Changeset 3014 for src/ERTL/ERTLToLTL.ma


Ignore:
Timestamp:
Mar 28, 2013, 4:58:26 PM (7 years ago)
Author:
tranquil
Message:

ERTL to ERTLptr pass suppressed (it introduced a bug in the later ERTLptr to LTL), and integrated in a single ERTToLTL pass like before

File:
1 moved

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTLToLTL.ma

    r3012 r3014  
    11include "LTL/LTL.ma".
    2 include "ERTLptr/Interference.ma".
     2include "ERTL/Interference.ma".
    33include "ASM/Arithmetic.ma".
    44include "joint/TranslateUtils.ma".
     
    299299     move ? localss false addr2 RegisterDPH).
    300300
    301 definition translate_low_address :
    302   ∀globals.nat → bool → decision → label →
    303   list (joint_seq LTL globals) ≝
    304   λglobals,localss,carry_lives_after,dst,lbl.
    305   match dst return λ_.list (joint_seq LTL globals) with
    306   [ decision_colour r ⇒ [LOW_ADDRESS r lbl]
    307   | _ ⇒
    308     LOW_ADDRESS RegisterA lbl :: move ? localss carry_lives_after dst RegisterA
    309   ].
    310 
    311 definition translate_high_address :
    312   ∀globals.nat → bool → decision → label →
    313   list (joint_seq LTL globals) ≝
    314   λglobals,localss,carry_lives_after,dst,lbl.
    315   match dst return λ_.list (joint_seq LTL globals) with
    316   [ decision_colour r ⇒ [HIGH_ADDRESS r lbl]
    317   | _ ⇒
    318     HIGH_ADDRESS RegisterA lbl :: move ? localss carry_lives_after dst RegisterA
    319   ].
    320 
    321301definition translate_step:
    322302  ∀globals,fn.nat → ∀after : valuation register_lattice.
    323303  coloured_graph (livebefore globals fn after) →
    324   ℕ → label → joint_step ERTLptr globals → bind_step_block LTL globals ≝
     304  ℕ → label → joint_step ERTL globals → bind_step_block LTL globals ≝
    325305  λglobals,fn,localss,after,grph,stack_sz,lbl,s.
    326306  bret … (
     
    385365    | extension_seq ext ⇒
    386366      match ext with
    387         [ ertlptr_ertl ext' ⇒
    388           match ext' with
    389           [ ertl_new_frame ⇒ newframe ? stack_sz
    390           | ertl_del_frame ⇒ delframe ? stack_sz
    391           | ertl_frame_size r ⇒
    392             move (lookup r) (arg_decision_imm (byte_of_nat stack_sz))
    393           ]
    394         | LOW_ADDRESS r1 l ⇒
    395            translate_low_address ? localss carry_lives_after (lookup r1) l
    396         | HIGH_ADDRESS r1 l ⇒
    397            translate_high_address ? localss carry_lives_after (lookup r1) l       
    398         ]
     367      [ ertl_new_frame ⇒ newframe ? stack_sz
     368      | ertl_del_frame ⇒ delframe ? stack_sz
     369      | ertl_frame_size r ⇒
     370        move (lookup r) (arg_decision_imm (byte_of_nat stack_sz))
     371      ]
    399372    ]
    400373  | COST_LABEL cost_lbl ⇒ 〈[ ], λ_.COST_LABEL … cost_lbl, [ ]〉
     
    407380      | inr dp ⇒
    408381        let 〈dpl, dph〉 ≝ dp in
    409         〈add_dummy_variance … (move_to_dp ? localss (lookup_arg dpl) (lookup_arg dph)),
     382        〈add_dummy_variance … (move_to_dp ? localss (lookup_arg dpl) (lookup_arg dph)) @
     383         [λl.(LOW_ADDRESS l : joint_seq ??);
     384          λ_.PUSH LTL ? it;
     385          λl.HIGH_ADDRESS l;
     386          λ_.PUSH LTL ? it],
    410387         λ_.CALL LTL ? (inr … 〈it, it〉) n_args it, [ ]〉
    411388      ]
     
    413390
    414391definition translate_fin_step:
    415   ∀globals.label → joint_fin_step ERTLptr → bind_fin_block LTL globals ≝
     392  ∀globals.label → joint_fin_step ERTL → bind_fin_block LTL globals ≝
    416393  λglobals,lbl,s.
    417394  bret … (〈[ ],
     
    425402 fixpoint_computer → coloured_graph_computer →
    426403 ∀globals.
    427   joint_closed_internal_function ERTLptr globals →
    428   bind_new register (b_graph_translate_data ERTLptr LTL globals) ≝
     404  joint_closed_internal_function ERTL globals →
     405  bind_new register (b_graph_translate_data ERTL LTL globals) ≝
    429406λthe_fixpoint,build,globals,int_fun.
    430407(* colour registers *)
     
    434411let stack_sz ≝ spilled_no … coloured_graph + joint_if_stacksize … int_fun in
    435412bret …
    436   (mk_b_graph_translate_data ERTLptr LTL globals
     413  (mk_b_graph_translate_data ERTL LTL globals
    437414    (* init_ret ≝ *) it
    438415    (* init_params ≝ *) it
     
    452429   when it is an info easily available from any program in the back end?
    453430   Also, is it really 2^16 - |globals|, or should there also be a -1? *)
    454 definition ertlptr_to_ltl:
    455  fixpoint_computer → coloured_graph_computer → ertlptr_program →
     431definition ertl_to_ltl:
     432 fixpoint_computer → coloured_graph_computer → ertl_program →
    456433  ltl_program × stack_cost_model × nat ≝
    457434  λthe_fixpoint,build,pr.
Note: See TracChangeset for help on using the changeset viewer.