Changeset 1170


Ignore:
Timestamp:
Sep 2, 2011, 12:28:26 PM (8 years ago)
Author:
mulligan
Message:

changes to ertl > ltl pass

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTLToLTL.ma

    r1168 r1170  
    7272      〈joint_st_sequential ? ltl_params globals (joint_instr_int ? globals RegisterA off) l, graph, luniv〉.
    7373
    74 definition set_stack ≝
    75   λint_fun.
    76   λglobals.
     74definition set_stack:
     75  ∀globals. ertl_internal_function globals → ltl_statement_graph globals → Byte
     76    → Register → label → ((ltl_statement globals) × (ltl_statement_graph globals) × (universe LabelTag)) ≝
     77  λglobals: list ident.
     78  λint_fun.
    7779  λgraph: graph (ltl_statement (globals)).
    7880  λoff.
    7981  λr.
    8082  λl.
    81   let off ≝ adjust_off int_fun off in
    82   let luniv ≝ ertl_if_luniverse int_fun in
    83   let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_store globals) l) in
    84   let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_to_acc globals r) l) in
    85   let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPH) l) in
    86   let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_op2 globals Addc RegisterSPH) l) in
    87   let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_int globals RegisterA (zero ?)) l) in
    88   let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPL) l) in
    89   let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_op2 globals Add RegisterSPL) l) in
    90     〈joint_st_sequential ? globals (joint_instr_int globals RegisterA off) l, 〈graph, luniv〉〉.
    91 
    92 definition write ≝
    93   λint_fun.
    94   λglobals.
    95   λgraph: graph (ltl_statement (globals)).
    96   λr: register.
    97   λl: label.
     83  let off ≝ adjust_off globals int_fun off in
     84  let luniv ≝ ertl_if_luniverse globals int_fun in
     85  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? ? globals (joint_instr_store ltl_params … globals it it it) l) in
     86  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc r)) l) in
     87  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPH)) l) in
     88  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Addc it RegisterSPH) l) in
     89  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_int … globals RegisterA (zero ?)) l) in
     90  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPL)) l) in
     91  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Add it RegisterSPL) l) in
     92    〈joint_st_sequential ? ltl_params globals (joint_instr_int ? globals RegisterA off) l, graph, luniv〉.
     93
     94definition write:
     95  ∀globals: list ident. ertl_internal_function globals → ltl_statement_graph globals → register → label →
     96    ? ≝
     97  λglobals: list ident.
     98  λint_fun.
     99  λgraph.
     100  λr.
     101  λl.
    98102  match lookup r with
    99103  [ decision_spill off ⇒
    100     let 〈stmt, graph, luniv〉 ≝ set_stack int_fun globals graph off RegisterSST l in
     104    let 〈stmt, graph, luniv〉 ≝ set_stack globals int_fun graph off RegisterSST l in
    101105    let 〈l, graph, int_fun〉 ≝ generate globals luniv graph stmt in
    102       〈RegisterSST, 〈l, 〈graph, luniv〉〉
     106      〈RegisterSST, l, graph, luniv
    103107  | decision_colour hwr ⇒
    104     let luniv ≝ ertl_if_luniverse int_fun in
    105       〈hwr, 〈l, 〈graph, luniv〉〉
     108    let luniv ≝ ertl_if_luniverse globals int_fun in
     109      〈hwr, l, graph, luniv
    106110  ].
    107111
    108 definition read ≝
    109   λint_fun.
    110   λglobals.
    111   λgraph: graph (ltl_statement (globals)).
    112   λr: register.
    113   λstmt: Register → ltl_statement globals.
     112definition read:
     113  ∀globals: list ident. ertl_internal_function globals → ltl_statement_graph globals → register
     114    → (Register → ltl_statement globals) → ? ≝
     115  λglobals.
     116  λint_fun.
     117  λgraph.
     118  λr.
     119  λstmt.
    114120  match lookup r with
    115   [ decision_colour hwr ⇒ generate globals graph (stmt hwr)
     121  [ decision_colour hwr ⇒ generate globals (ertl_if_luniverse globals int_fun) graph (stmt hwr)
    116122  | decision_spill off ⇒
    117123    let temphwr ≝ RegisterSST in
    118     let 〈l, graph〉 ≝ generate globals graph (stmt temphwr) in
    119     let 〈stmt, graph〉 ≝ get_stack int_fun globals graph temphwr off l in
    120       generate globals graph stmt
     124    let 〈l, graph, luniv〉 ≝ generate globals (ertl_if_luniverse globals int_fun) graph (stmt temphwr) in
     125    let 〈stmt, graph, luniv〉 ≝ get_stack globals int_fun graph temphwr off l in
     126      generate globals luniv graph stmt
    121127  ].
    122128
    123129definition move ≝
    124   λint_fun.
    125   λglobals: list ident.
     130  λglobals: list ident.
     131  λint_fun.
    126132  λgraph: graph (ltl_statement globals).
    127133  λdest: decision.
     
    132138    match src with
    133139    [ decision_colour src_hwr ⇒
     140      let luniv ≝ ertl_if_luniverse globals int_fun in
    134141      if eq_Register dest_hwr src_hwr then
    135         〈joint_st_goto ? globals l, graph
     142        〈joint_st_goto … globals l, graph, luniv
    136143      else
    137         let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals dest_hwr) l) in
    138           〈joint_st_sequential ? globals (joint_instr_to_acc globals src_hwr) l, graph
    139     | decision_spill src_off ⇒ get_stack int_fun globals graph dest_hwr src_off l
     144        let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc dest_hwr)) l) in
     145          〈joint_st_sequential ? ? globals (joint_instr_move … ltl_params globals (to_acc src_hwr)) l, graph, luniv
     146    | decision_spill src_off ⇒ get_stack globals int_fun graph dest_hwr src_off l
    140147    ]
    141148  | decision_spill dest_off ⇒
    142149    match src with
    143     [ decision_colour src_hwr ⇒ set_stack int_fun globals graph dest_off src_hwr l
     150    [ decision_colour src_hwr ⇒ set_stack globals int_fun graph dest_off src_hwr l
    144151    | decision_spill src_off ⇒
     152      let luniv ≝ ertl_if_luniverse globals int_fun in
    145153      if eq_bv ? dest_off src_off then
    146         〈joint_st_goto ? globals l, graph
     154        〈joint_st_goto … globals l, graph, luniv
    147155      else
    148156        let temp_hwr ≝ RegisterSST in
    149         let 〈stmt, graph〉 ≝ set_stack int_fun globals graph dest_off temp_hwr l in
    150         let 〈l, graph〉 ≝ generate globals graph stmt in
    151           get_stack int_fun globals graph temp_hwr src_off l
     157        let 〈stmt, graph, luniv〉 ≝ set_stack globals int_fun graph dest_off temp_hwr l in
     158        let 〈l, graph, luniv〉 ≝ generate globals luniv graph stmt in
     159          get_stack globals int_fun graph temp_hwr src_off l
    152160    ]
    153161  ].
    154162
    155163definition newframe ≝
    156   λint_fun.
    157   λglobals.
    158   λgraph: graph (ltl_statement globals).
    159   λl.
    160   if eq_nat (stacksize int_fun) 0 then
     164  λglobals.
     165  λint_fun.
     166  λgraph: ltl_statement_graph globals.
     167  λl.
     168  if eq_nat (stacksize globals int_fun) 0 then
    161169    〈joint_st_goto ? globals l, graph〉
    162170  else
    163     let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterSPH) l) in
    164     let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_op2 globals Sub RegisterDPH) l) in
    165     let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_int globals RegisterDPH (zero ?)) l) in
    166     let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterSPH) l) in
    167     let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterSPL) l) in
    168     let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_op2 globals Sub RegisterDPL) l) in
    169     let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_clear_carry globals) l) in
    170     let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_int globals RegisterDPL (bitvector_of_nat ? (stacksize int_fun))) l) in
    171       〈joint_st_sequential ? globals (joint_instr_to_acc globals RegisterSPL) l, graph〉.
     171    let luniv ≝ ertl_if_luniverse globals int_fun in
     172    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterSPH) l) in
     173    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_op2 globals Sub RegisterDPH) l) in
     174    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_int globals RegisterDPH (zero ?)) l) in
     175    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterSPH) l) in
     176    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterSPL) l) in
     177    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_op2 globals Sub RegisterDPL) l) in
     178    let 〈l, graph, lunive〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_clear_carry globals) l) in
     179    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_int globals RegisterDPL (bitvector_of_nat ? (stacksize int_fun))) l) in
     180      〈joint_st_sequential ? globals (joint_instr_to_acc globals RegisterSPL) l, graph, luniv〉.
    172181
    173182definition delframe ≝
Note: See TracChangeset for help on using the changeset viewer.