Changeset 1191 for src/ERTL/ERTLToLTL.ma


Ignore:
Timestamp:
Sep 6, 2011, 10:38:48 AM (8 years ago)
Author:
mulligan
Message:

ertl to ertl pass back where it was before the changes to joint

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTLToLTL.ma

    r1179 r1191  
    294294      let 〈l, graph, luniv〉 ≝ read globals int_fun graph acc_b_reg (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
    295295        〈joint_st_goto ltl_params globals l, graph, luniv〉
    296     | _ ⇒ ?
     296    | joint_instr_move pair_regs ⇒
     297      let regl ≝ \fst pair_regs in
     298      let regr ≝ \snd pair_regs in
     299      match regl with
     300      [ pseudo p1  ⇒
     301        match regr with
     302        [ pseudo p2  ⇒ move globals int_fun graph (lookup p1) (lookup p2) l
     303        | hardware h ⇒ move globals int_fun graph (lookup p1) (decision_colour h) l
     304        ]
     305      | hardware h1 ⇒
     306        match regr with
     307        [ pseudo p    ⇒ move globals int_fun graph (decision_colour h1) (lookup p) l
     308        | hardware h2 ⇒
     309          let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc h1)) l) in
     310            〈joint_st_sequential ltl_params globals (joint_instr_move ltl_params globals (to_acc h2)) l, graph, luniv〉
     311        ]
     312      ]
     313    | joint_instr_address lbl prf dpl dph ⇒
     314      let 〈hdw1, l, graph, luniv〉 ≝ write globals int_fun graph dph l in
     315      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw1)) l) in
     316      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterDPH)) l) in
     317      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_address … globals lbl prf it it) l) in
     318      let int_fun ≝ set_luniverse globals int_fun luniv in
     319      let 〈hdw2, l, graph, luniv〉 ≝ write globals int_fun graph dpl l in
     320      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw2)) l) in
     321      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterDPL)) l) in
     322        〈joint_st_sequential ltl_params globals (joint_instr_address … globals lbl prf it it) l, graph, luniv〉
    297323    ]
    298324  | joint_st_return ⇒ 〈joint_st_return … globals, graph, ertl_if_luniverse globals int_fun〉
     
    307333    ]
    308334  ].
    309  
    310   match stmt with
    311   | ertl_st_get_hdw destr sourcehwr l ⇒ move int_fun globals graph (lookup destr) (decision_colour sourcehwr) l
    312   | ertl_st_set_hdw desthwr srcr l ⇒ move int_fun globals graph (decision_colour desthwr) (lookup srcr) l
    313   | ertl_st_hdw_to_hdw r1 r2 l ⇒
    314     let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals r1) l) in
    315       〈joint_st_sequential ? globals (joint_instr_to_acc globals r2) l, graph〉
    316   | ertl_st_addr rl rh x l ⇒
    317     let 〈hdw1, l〉 ≝ write int_fun globals graph rh l in
    318     let 〈l, graph〉 ≝ l in
    319     let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals hdw1) l) in
    320     let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterDPH) l) in
    321     let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_address globals x ?) l) in
    322     let 〈hdw2, l〉 ≝ write int_fun globals graph rl l in
    323     let 〈l, graph〉 ≝ l in
    324     let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals hdw2) l) in
    325     let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterDPL) l) in
    326       〈joint_st_sequential ? globals (joint_instr_address globals x ?) l, graph〉
    327 (*  | ertl_st_addr_h r x l ⇒
    328     let 〈hdw, l〉 ≝ write int_fun globals graph r l in
    329     let 〈l, graph〉 ≝ generate globals graph (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l)) in
    330     let 〈l, graph〉 ≝ generate globals graph (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterDPH) l)) in
    331       ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_address globals x ?) l)
    332   | ertl_st_addr_l r x l ⇒
    333     let 〈hdw, l〉 ≝ write int_fun globals graph r l in
    334     let 〈l, graph〉 ≝ generate globals graph (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l)) in
    335     let 〈l, graph〉 ≝ generate globals graph (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterDPL) l)) in
    336       ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_address globals x ?) l)
    337 *)
    338   | ertl_st_move r1 r2 l ⇒ move int_fun globals graph (lookup r1) (lookup r2) l
    339 (*
    340   | ertl_st_opaccs_a opaccs destr srcr1 srcr2 l ⇒
    341     let 〈hdw, l〉 ≝ write int_fun globals graph destr l in
    342     let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
    343     let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_opaccs globals opaccs) l) in
    344     let 〈l, graph〉 ≝ read int_fun globals graph srcr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
    345     let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterB) l) in
    346     let 〈l, graph〉 ≝ read int_fun globals graph srcr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
    347       joint_st_goto ? globals l
    348   | ertl_st_opaccs_b opaccs destr srcr1 srcr2 l ⇒
    349     let 〈hdw, l〉 ≝ write int_fun globals graph destr l in
    350     let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
    351     let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterB) l) in
    352     let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_opaccs globals opaccs) l) in
    353     let 〈l, graph〉 ≝ read int_fun globals graph srcr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
    354     let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterB) l) in
    355     let 〈l, graph〉 ≝ read int_fun globals graph srcr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
    356       joint_st_goto ? globals l
    357 *)
    358   ].
    359   cases daemon (* XXX: todo -- proofs regarding gvars *)
    360 qed.
    361 
    362 (* **** *)
    363335
    364336definition translate_internal ≝
Note: See TracChangeset for help on using the changeset viewer.