Changeset 1128


Ignore:
Timestamp:
Aug 29, 2011, 4:27:30 PM (8 years ago)
Author:
mulligan
Message:

fixed ERTLtoLTLI so it type checks again

Location:
src/ERTL
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTLToLTL.ma

    r1124 r1128  
    22include "ERTL/ERTLToLTLI.ma".
    33include "LTL/LTL.ma".
     4include "ERTL/spill.ma".
    45
    56definition translate_internal ≝
  • src/ERTL/ERTLToLTLI.ma

    r1108 r1128  
    2828  λl.
    2929    let off ≝ adjust_off off in
    30     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals r) l) in
    31     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_load globals) l) in
    32     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPH) l) in
    33     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_op2 globals Addc RegisterSPH) l) in
    34     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_int globals RegisterA (zero ?)) l) in
    35     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPL) l) in
    36     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_op2 globals Add RegisterSPL) l) in
    37       joint_st_sequential ? globals (joint_instr_int globals RegisterA off) l.
     30    let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_from_acc globals r) l)) in
     31    let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_load globals) l)) in
     32    let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPH) l)) in
     33    let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_op2 globals Addc RegisterSPH) l)) in
     34    let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_int globals RegisterA (zero ?)) l)) in
     35    let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPL) l)) in
     36    let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_op2 globals Add RegisterSPL) l)) in
     37      (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_int globals RegisterA off) l)).
    3838
    3939definition set_stack ≝
     
    4343  λl.
    4444  let off ≝ adjust_off off in
    45   let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_store globals) l) in
    46   let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_to_acc globals r) l) in
    47   let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPH) l) in
    48   let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_op2 globals Addc RegisterSPH) l) in
    49   let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_int globals RegisterA (zero ?)) l) in
    50   let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPL) l) in
    51   let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_op2 globals Add RegisterSPL) l) in
    52     joint_st_sequential ? globals (joint_instr_int globals RegisterA off) l.
     45  let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_store globals) l)) in
     46  let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_to_acc globals r) l)) in
     47  let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPH) l)) in
     48  let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_op2 globals Addc RegisterSPH) l)) in
     49  let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_int globals RegisterA (zero ?)) l)) in
     50  let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPL) l)) in
     51  let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_op2 globals Add RegisterSPL) l)) in
     52    (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_int globals RegisterA off) l)).
    5353
    5454definition write ≝
     
    8383    [ decision_colour src_hwr ⇒
    8484      if eq_Register dest_hwr src_hwr then
    85         joint_st_sequential ? globals (joint_instr_skip globals) l
     85        ltl_st_skip globals l
    8686      else
    87         let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals dest_hwr) l) in
    88           joint_st_sequential ? globals (joint_instr_to_acc globals src_hwr) l
     87        let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_from_acc globals dest_hwr) l)) in
     88          (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_to_acc globals src_hwr) l))
    8989    | decision_spill src_off ⇒ get_stack globals dest_hwr src_off l
    9090    ]
     
    9494    | decision_spill src_off ⇒
    9595      if eq_bv ? dest_off src_off then
    96         joint_st_sequential ? globals (joint_instr_skip globals) l
     96        ltl_st_skip globals l
    9797      else
    9898        let temp_hwr ≝ RegisterSST in
     
    106106  λl.
    107107  if eq_nat stacksize 0 then
    108     joint_st_sequential ? globals (joint_instr_skip globals) l
     108    ltl_st_skip globals l
    109109  else
    110     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterSPH) l) in
    111     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_op2 globals Sub RegisterDPH) l) in
    112     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_int globals RegisterDPH (zero ?)) l) in
    113     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterSPH) l) in
    114     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterSPL) l) in
    115     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_op2 globals Sub RegisterDPL) l) in
    116     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_clear_carry globals) l) in
    117     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_int globals RegisterDPL (bitvector_of_nat ? stacksize)) l) in
    118       joint_st_sequential ? globals (joint_instr_to_acc globals RegisterSPL) l.
     110    let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterSPH) l)) in
     111    let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_op2 globals Sub RegisterDPH) l)) in
     112    let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_int globals RegisterDPH (zero ?)) l)) in
     113    let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterSPH) l)) in
     114    let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterSPL) l)) in
     115    let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_op2 globals Sub RegisterDPL) l)) in
     116    let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_clear_carry globals) l)) in
     117    let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_int globals RegisterDPL (bitvector_of_nat ? stacksize)) l)) in
     118      (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterSPL) l)).
    119119
    120120definition delframe ≝
     
    122122  λl.
    123123  if eq_nat stacksize 0 then
    124     joint_st_sequential ? globals (joint_instr_skip globals) l
     124    ltl_st_skip globals l
    125125  else
    126     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterSPH) l) in
    127     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_op2 globals Addc RegisterSPH) l) in
    128     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_int globals RegisterA (zero ?)) l) in
    129     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterSPL) l) in
    130     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_op2 globals Add RegisterSPL) l) in
    131       joint_st_sequential ? globals (joint_instr_int globals RegisterA (bitvector_of_nat ? stacksize)) l.
     126    let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterSPH) l)) in
     127    let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_op2 globals Addc RegisterSPH) l)) in
     128    let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_int globals RegisterA (zero ?)) l)) in
     129    let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterSPL) l)) in
     130    let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_op2 globals Add RegisterSPL) l)) in
     131      (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_int globals RegisterA (bitvector_of_nat ? stacksize)) l)).
    132132
    133133definition translate_statement ≝
     
    135135  λstmt: ertl_statement.
    136136  match stmt with
    137   [ ertl_st_skip l ⇒ joint_st_sequential ? globals (joint_instr_skip globals) l
    138   | ertl_st_comment s l ⇒ joint_st_sequential ? globals (joint_instr_comment globals s) l
    139   | ertl_st_cost cost_lbl l ⇒ joint_st_sequential ? globals (joint_instr_cost_label globals cost_lbl) l
     137  [ ertl_st_skip l ⇒ ltl_st_skip globals l
     138  | ertl_st_comment s l ⇒ ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_comment globals s) l)
     139  | ertl_st_cost cost_lbl l ⇒ ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_cost_label globals cost_lbl) l)
    140140  | ertl_st_get_hdw destr sourcehwr l ⇒ move globals (lookup destr) (decision_colour sourcehwr) l
    141141  | ertl_st_set_hdw desthwr srcr l ⇒ move globals (decision_colour desthwr) (lookup srcr) l
    142142  | ertl_st_hdw_to_hdw r1 r2 l ⇒
    143     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals r1) l) in
    144       joint_st_sequential ? globals (joint_instr_to_acc globals r2) l
     143    let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_from_acc globals r1) l)) in
     144      ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_to_acc globals r2) l)
    145145  | ertl_st_new_frame l ⇒ newframe globals l
    146146  | ertl_st_del_frame l ⇒ delframe globals l
    147147  | ertl_st_frame_size r l ⇒
    148148    let 〈hdw, l〉 ≝ write globals r l in
    149       joint_st_sequential ? globals (joint_instr_int globals hdw (bitvector_of_nat ? stacksize)) l
     149      ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_int globals hdw (bitvector_of_nat ? stacksize)) l)
    150150  | ertl_st_pop r l ⇒
    151151    let 〈hdw, l〉 ≝ write globals r l in
    152     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
    153       joint_st_sequential ? globals (joint_instr_pop globals) l
     152    let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l)) in
     153      ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_pop globals) l)
    154154  | ertl_st_push r l ⇒
    155     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_push globals) l) in
    156     let l ≝ read globals r (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
    157       joint_st_sequential ? globals (joint_instr_skip globals) l
     155    let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_push globals) l)) in
     156    let l ≝ read globals r (λhdw. ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l)) in
     157      ltl_st_skip globals l
    158158  | ertl_st_addr_h r x l ⇒
    159159    let 〈hdw, l〉 ≝ write globals r l in
    160     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
    161     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterDPH) l) in
    162       joint_st_sequential ? globals (joint_instr_address globals x ?) l
     160    let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l)) in
     161    let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterDPH) l)) in
     162      ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_address globals x ?) l)
    163163  | ertl_st_addr_l r x l ⇒
    164164    let 〈hdw, l〉 ≝ write globals r l in
    165     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
    166     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterDPL) l) in
    167       joint_st_sequential ? globals (joint_instr_address globals x ?) l
     165    let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l)) in
     166    let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterDPL) l)) in
     167      ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_address globals x ?) l)
    168168  | ertl_st_int r i l ⇒
    169169    let 〈hdw, l〉 ≝ write globals r l in
    170       joint_st_sequential ? globals (joint_instr_int globals hdw i) l
     170      ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_int globals hdw i) l)
    171171  | ertl_st_move r1 r2 l ⇒ move globals (lookup r1) (lookup r2) l
    172172  | ertl_st_opaccs_a opaccs destr srcr1 srcr2 l ⇒
    173173    let 〈hdw, l〉 ≝ write globals destr l in
    174     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
    175     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_opaccs globals opaccs) l) in
    176     let l ≝ read globals srcr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
    177     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterB) l) in
    178     let l ≝ read globals srcr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
    179       joint_st_sequential ? globals (joint_instr_skip globals) l
     174    let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l)) in
     175    let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_opaccs globals opaccs) l)) in
     176    let l ≝ read globals srcr1 (λhdw. ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l)) in
     177    let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterB) l)) in
     178    let l ≝ read globals srcr2 (λhdw. ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l)) in
     179      ltl_st_skip globals l
    180180  | ertl_st_opaccs_b opaccs destr srcr1 srcr2 l ⇒
    181181    let 〈hdw, l〉 ≝ write globals destr l in
    182     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
    183     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterB) l) in
    184     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_opaccs globals opaccs) l) in
    185     let l ≝ read globals srcr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
    186     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterB) l) in
    187     let l ≝ read globals srcr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
    188       joint_st_sequential ? globals (joint_instr_skip globals) l
     182    let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l)) in
     183    let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterB) l)) in
     184    let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_opaccs globals opaccs) l)) in
     185    let l ≝ read globals srcr1 (λhdw. ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l)) in
     186    let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterB) l)) in
     187    let l ≝ read globals srcr2 (λhdw. ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l)) in
     188      ltl_st_skip globals l
    189189  | ertl_st_op1 op1 destr srcr l ⇒
    190190    let 〈hdw, l〉 ≝ write globals destr l in
    191     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
    192     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_op1 globals op1) l) in
    193     let l ≝ read globals srcr (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
    194       joint_st_sequential ? globals (joint_instr_skip globals) l
     191    let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l)) in
     192    let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_op1 globals op1) l)) in
     193    let l ≝ read globals srcr (λhdw. ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l)) in
     194      ltl_st_skip globals l
    195195  | ertl_st_op2 op2 destr srcr1 srcr2 l ⇒
    196196    let 〈hdw, l〉 ≝ write globals destr l in
    197     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
    198     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_op2 globals op2 RegisterB) l) in
    199     let l ≝ read globals srcr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
    200     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterB) l) in
    201     let l ≝ read globals srcr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
    202       joint_st_sequential ? globals (joint_instr_skip globals) l
    203   | ertl_st_clear_carry l ⇒ joint_st_sequential ? globals (joint_instr_clear_carry globals) l
    204   | ertl_st_set_carry l ⇒ joint_st_sequential ? globals (joint_instr_set_carry globals) l
     197    let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l)) in
     198    let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_op2 globals op2 RegisterB) l)) in
     199    let l ≝ read globals srcr1 (λhdw. ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l)) in
     200    let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterB) l)) in
     201    let l ≝ read globals srcr2 (λhdw. ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l)) in
     202      ltl_st_skip globals l
     203  | ertl_st_clear_carry l ⇒ ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_clear_carry globals) l)
     204  | ertl_st_set_carry l ⇒ ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_set_carry globals) l)
    205205  | ertl_st_load destr addr1 addr2 l ⇒
    206206    let 〈hdw, l〉 ≝ write globals destr l in
    207     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
    208     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_load globals) l) in
    209     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPH) l) in
    210     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterST0) l) in
    211     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPL) l) in
    212     let l ≝ read globals addr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
    213     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterST0) l) in
    214     let l ≝ read globals addr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
    215       joint_st_sequential ? globals (joint_instr_skip globals) l
     207    let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l)) in
     208    let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_load globals) l)) in
     209    let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPH) l)) in
     210    let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterST0) l)) in
     211    let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPL) l)) in
     212    let l ≝ read globals addr1 (λhdw. ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l)) in
     213    let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterST0) l)) in
     214    let l ≝ read globals addr2 (λhdw. ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l)) in
     215      ltl_st_skip globals l
    216216  | ertl_st_store addr1 addr2 srcr l ⇒
    217     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_store globals) l) in
    218     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterST1) l) in
    219     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPH) l) in
    220     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterST0) l) in
    221     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPL) l) in
    222     let l ≝ read globals addr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
    223     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterST0) l) in
    224     let l ≝ read globals addr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
    225     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterST1) l) in
    226     let l ≝ read globals srcr (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
    227       joint_st_sequential ? globals (joint_instr_skip globals) l
    228   | ertl_st_call_id f ignore l ⇒  joint_st_sequential ? globals (joint_instr_call_id globals f) l
     217    let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_store globals) l)) in
     218    let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterST1) l)) in
     219    let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPH) l)) in
     220    let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterST0) l)) in
     221    let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPL) l)) in
     222    let l ≝ read globals addr1 (λhdw. ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l)) in
     223    let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterST0) l)) in
     224    let l ≝ read globals addr2 (λhdw. ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l)) in
     225    let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterST1) l)) in
     226    let l ≝ read globals srcr (λhdw. ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l)) in
     227      ltl_st_skip globals l
     228  | ertl_st_call_id f ignore l ⇒  ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_call_id globals f) l)
    229229  | ertl_st_cond srcr lbl_true lbl_false ⇒
    230     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_cond_acc globals lbl_true) lbl_false) in
    231     let l ≝ read globals srcr (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
    232       joint_st_sequential ? globals (joint_instr_skip globals) l
    233   | ertl_st_return ⇒ joint_st_return ? globals
     230    let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_cond_acc globals lbl_true) lbl_false)) in
     231    let l ≝ read globals srcr (λhdw. ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l)) in
     232      ltl_st_skip globals l
     233  | ertl_st_return ⇒ ltl_st_lift globals (joint_st_return ? globals)
    234234  ].
    235235  cases daemon (* XXX: todo -- proofs regarding gvars *)
  • src/ERTL/spill.ma

    r1127 r1128  
    11include "common/AST.ma".
     2include "utilities/Interference.ma".
    23
    34definition decision ≝ Immediate.
    45
    5 definition colouring ≝
     6(* XXX: should be a map! *)
     7definition colouring ≝ list (vertex × decision).
     8
     9axiom colour_colouring: colouring.
     10axiom colour_locals: nat.
Note: See TracChangeset for help on using the changeset viewer.