Ignore:
Timestamp:
Feb 22, 2013, 11:39:03 AM (9 years ago)
Author:
sacerdot
Message:
  1. Stuff moved to correct places.
  2. ERTLptr pass added
File:
1 moved

Legend:

Unmodified
Added
Removed
  • src/ERTLptr/ERTLptrToLTL.ma

    r2690 r2693  
    1 
    21include "LTL/LTL.ma".
    3 include "ERTL/Interference.ma".
     2include "ERTLptr/Interference.ma".
    43include "ASM/Arithmetic.ma".
    54include "joint/TranslateUtils.ma".
     
    300299  ∀globals.∀after : valuation register_lattice.
    301300  coloured_graph after →
    302   ℕ → label → joint_step ERTL globals → bind_step_block LTL globals ≝
     301  ℕ → label → joint_step ERTLptr globals → bind_step_block LTL globals ≝
    303302  λglobals,after,grph,stack_sz,lbl,s.
    304303  bret … (
     
    362361    | extension_seq ext ⇒
    363362      match ext with
    364       [ ertl_new_frame ⇒ newframe ? stack_sz
    365       | ertl_del_frame ⇒ delframe ? stack_sz
    366       | ertl_frame_size r ⇒
    367         move (lookup r) (arg_decision_imm (byte_of_nat stack_sz))
    368       ]
     363        [ ertlptr_ertl ext' ⇒
     364          match ext' with
     365          [ ertl_new_frame ⇒ newframe ? stack_sz
     366          | ertl_del_frame ⇒ delframe ? stack_sz
     367          | ertl_frame_size r ⇒
     368            move (lookup r) (arg_decision_imm (byte_of_nat stack_sz))
     369          ]
     370        | LOW_ADDRESS r1 l ⇒
     371           translate_low_address ? carry_lives_after (lookup_arg r1) l
     372        | HIGH_ADDRESS r1 l ⇒
     373           translate_high_address ? carry_lives_after (lookup_arg r1) l       
     374        ]
    369375    ]
    370376  | COST_LABEL cost_lbl ⇒ 〈[ ], λ_.COST_LABEL … cost_lbl, [ ]〉
     
    383389
    384390definition translate_fin_step:
    385   ∀globals.label → joint_fin_step ERTL → bind_fin_block LTL globals ≝
     391  ∀globals.label → joint_fin_step ERTLptr → bind_fin_block LTL globals ≝
    386392  λglobals,lbl,s.
    387393  bret … (〈[ ],
     
    393399
    394400definition translate_data : ∀globals.
    395   joint_closed_internal_function ERTL globals →
    396   bind_new register (b_graph_translate_data ERTL LTL globals) ≝
     401  joint_closed_internal_function ERTLptr globals →
     402  bind_new register (b_graph_translate_data ERTLptr LTL globals) ≝
    397403λglobals,int_fun.
    398404(* colour registers *)
     
    402408let stack_sz ≝ spilled_no … coloured_graph + joint_if_stacksize … int_fun in
    403409bret …
    404   (mk_b_graph_translate_data ERTL LTL globals
     410  (mk_b_graph_translate_data ERTLptr LTL globals
    405411    (* init_ret ≝ *) it
    406412    (* init_params ≝ *) it
Note: See TracChangeset for help on using the changeset viewer.