Changeset 1251


Ignore:
Timestamp:
Sep 22, 2011, 2:29:52 PM (8 years ago)
Author:
mulligan
Message:

changes to get things compiling again after yet another CSC rearrangement!

Location:
src/ERTL
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTLToLTL.ma

    r1250 r1251  
    4747  ].
    4848*)
    49 
    50 definition lookup ≝ colouring.
    5149
    5250definition fresh_label ≝
     
    141139  λr.
    142140  λl.
    143   match lookup valuation coloured_graph (inl … r) with
     141  match colouring valuation coloured_graph (inl … r) with
    144142  [ decision_spill off ⇒
    145143    let 〈stmt, graph, luniv〉 ≝ set_stack globals int_fun graph (bitvector_of_nat … off) RegisterSST l in
     
    159157  λr.
    160158  λstmt.
    161   match lookup valuation coloured_graph (inl … r) with
     159  match colouring valuation coloured_graph (inl … r) with
    162160  [ decision_colour hwr ⇒ generate globals (joint_if_luniverse globals (ertl_params globals) int_fun) graph (stmt hwr)
    163161  | decision_spill off ⇒
     
    343341      [ pseudo p1  ⇒
    344342        match regr with
    345         [ pseudo p2  ⇒ move globals int_fun graph (lookup valuation coloured_graph (inl … p1)) (lookup valuation coloured_graph (inl … p2)) l
    346         | hardware h ⇒ move globals int_fun graph (lookup valuation coloured_graph (inl … p1)) (decision_colour h) l
     343        [ pseudo p2  ⇒ move globals int_fun graph (colouring valuation coloured_graph (inl … p1)) (colouring valuation coloured_graph (inl … p2)) l
     344        | hardware h ⇒ move globals int_fun graph (colouring valuation coloured_graph (inl … p1)) (decision_colour h) l
    347345        ]
    348346      | hardware h1 ⇒
    349347        match regr with
    350         [ pseudo p    ⇒ move globals int_fun graph (decision_colour h1) (lookup valuation coloured_graph (inl … p)) l
     348        [ pseudo p    ⇒ move globals int_fun graph (decision_colour h1) (colouring valuation coloured_graph (inl … p)) l
    351349        | hardware h2 ⇒
    352350          let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc h1)) l) in
  • src/ERTL/uses.ma

    r1250 r1251  
    6060  λint_fun: ertl_internal_function globals.
    6161  let graph ≝ recover_graph globals int_fun in
    62   let uses ≝ tbl_fold ?? (examine_statement globals) (joint_if_graph … int_fun) (tbl_empty …) in
     62  let uses ≝ tbl_fold … (examine_statement globals) (joint_if_code … int_fun) (tbl_empty …) in
    6363      lookup uses.
    6464*)
Note: See TracChangeset for help on using the changeset viewer.