Changeset 1424 for src/ERTL


Ignore:
Timestamp:
Oct 19, 2011, 7:17:04 PM (9 years ago)
Author:
sacerdot
Message:
  1. fold function over BitVectorTries? moved from ERTLToLTL to ASM/BitVectorTrie
  2. ERTLToLTL now compiles again after removal of spill.ma
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTLToLTL.ma

    r1423 r1424  
    1 include "ERTL/ERTL.ma".
    21include "LTL/LTL.ma".
     2include "ERTL/Interference.ma".
    33include "ASM/Arithmetic.ma".
    44
     
    105105  [ decision_spill off ⇒
    106106    let luniv ≝ joint_if_luniverse … int_fun in
    107     let 〈graph, luniv〉 ≝ set_stack globals int_fun graph (bitvector_of_nat … off) RegisterSST l original_label in
     107    let 〈graph, luniv〉 ≝ set_stack (spilled_no … coloured_graph) globals int_fun graph (bitvector_of_nat … off) RegisterSST l original_label in
    108108      〈RegisterSST, l, graph, luniv〉
    109109  | decision_colour hwr ⇒
     
    129129    let luniv ≝ joint_if_luniverse … int_fun in
    130130    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (stmt temphwr) in
    131       get_stack globals int_fun graph temphwr (bitvector_of_nat … off) l original_label
     131      get_stack (spilled_no … coloured_graph) globals int_fun graph temphwr (bitvector_of_nat … off) l original_label
    132132  ].
    133133
    134134definition move ≝
     135  λspilled_no.
    135136  λglobals: list ident.
    136137  λint_fun.
     
    150151        let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc dest_hwr)) l) in
    151152          〈add_graph globals original_label (sequential (ltl_params globals) globals (MOVE … globals (to_acc src_hwr)) l) graph, luniv〉
    152     | decision_spill src_off ⇒ get_stack globals int_fun graph dest_hwr (bitvector_of_nat … src_off) l original_label
     153    | decision_spill src_off ⇒ get_stack spilled_no globals int_fun graph dest_hwr (bitvector_of_nat … src_off) l original_label
    153154    ]
    154155  | decision_spill dest_off ⇒
    155156    match src with
    156     [ decision_colour src_hwr ⇒ set_stack globals int_fun graph (bitvector_of_nat … dest_off) src_hwr l original_label
     157    [ decision_colour src_hwr ⇒ set_stack spilled_no globals int_fun graph (bitvector_of_nat … dest_off) src_hwr l original_label
    157158    | decision_spill src_off ⇒
    158159      let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
     
    161162      else
    162163        let temp_hwr ≝ RegisterSST in
    163         let 〈graph, luniv〉 ≝ set_stack globals int_fun graph (bitvector_of_nat … dest_off) temp_hwr l original_label in
    164           get_stack globals int_fun graph temp_hwr (bitvector_of_nat … src_off) l original_label
     164        let 〈graph, luniv〉 ≝ set_stack spilled_no globals int_fun graph (bitvector_of_nat … dest_off) temp_hwr l original_label in
     165          get_stack spilled_no globals int_fun graph temp_hwr (bitvector_of_nat … src_off) l original_label
    165166    ]
    166167  ].
    167168
    168169definition newframe ≝
     170  λspilled_no.
    169171  λglobals: list ident.
    170172  λint_fun: ertl_internal_function globals.
     
    172174  λl: label.
    173175  λoriginal_label: label.
    174   if eq_nat (stacksize globals int_fun) 0 then
     176  if eq_nat (stacksize spilled_no globals int_fun) 0 then
    175177    let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
    176178      〈add_graph globals original_label (GOTO … globals l) graph, luniv〉
     
    184186    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (OP2 … globals Sub it it RegisterDPL) l) in
    185187    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (CLEAR_CARRY … globals) l) in
    186     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (INT … globals RegisterDPL (bitvector_of_nat ? (stacksize globals int_fun))) l) in
     188    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (INT … globals RegisterDPL (bitvector_of_nat ? (stacksize spilled_no globals int_fun))) l) in
    187189      〈add_graph globals original_label (sequential (ltl_params globals) globals (MOVE … globals (to_acc RegisterSPL)) l) graph, luniv〉.
    188190
    189191definition delframe ≝
     192  λspilled_no.
    190193  λglobals.
    191194  λint_fun.
     
    193196  λl.
    194197  λoriginal_label: label.
    195   if eq_nat (stacksize globals int_fun) 0 then
     198  if eq_nat (stacksize spilled_no globals int_fun) 0 then
    196199    let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
    197200      〈add_graph globals original_label (GOTO (ltl_params globals) globals l) graph, luniv〉
     
    203206    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc RegisterSPL)) l) in
    204207    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (OP2 … globals Add it it RegisterSPL) l) in
    205       〈add_graph globals original_label (sequential (ltl_params globals) globals (INT ? globals RegisterA (bitvector_of_nat ? (stacksize globals int_fun))) l) graph, luniv〉.
     208      〈add_graph globals original_label (sequential (ltl_params globals) globals (INT ? globals RegisterA (bitvector_of_nat ? (stacksize spilled_no globals int_fun))) l) graph, luniv〉.
    206209
    207210definition translate_statement:
     
    322325      [ pseudo p1  ⇒
    323326        match regr with
    324         [ pseudo p2  ⇒ move globals int_fun graph (colouring valuation coloured_graph (inl … p1)) (colouring valuation coloured_graph (inl … p2)) l original_label
    325         | hardware h ⇒ move globals int_fun graph (colouring valuation coloured_graph (inl … p1)) (decision_colour h) l original_label
     327        [ pseudo p2  ⇒ move (spilled_no … coloured_graph) globals int_fun graph (colouring valuation coloured_graph (inl … p1)) (colouring valuation coloured_graph (inl … p2)) l original_label
     328        | hardware h ⇒ move (spilled_no … coloured_graph) globals int_fun graph (colouring valuation coloured_graph (inl … p1)) (decision_colour h) l original_label
    326329        ]
    327330      | hardware h1 ⇒
    328331        match regr with
    329         [ pseudo p    ⇒ move globals int_fun graph (decision_colour h1) (colouring valuation coloured_graph (inl … p)) l original_label
     332        [ pseudo p    ⇒ move (spilled_no … coloured_graph) globals int_fun graph (decision_colour h1) (colouring valuation coloured_graph (inl … p)) l original_label
    330333        | hardware h2 ⇒
    331334          let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc h1)) l) in
     
    349352    | extension ext ⇒
    350353      match ext with
    351       [ ertl_st_ext_new_frame ⇒ newframe globals int_fun graph l original_label
    352       | ertl_st_ext_del_frame ⇒ delframe globals int_fun graph l original_label
     354      [ ertl_st_ext_new_frame ⇒ newframe (spilled_no … coloured_graph)globals int_fun graph l original_label
     355      | ertl_st_ext_del_frame ⇒ delframe (spilled_no … coloured_graph) globals int_fun graph l original_label
    353356      | ertl_st_ext_frame_size r ⇒
    354357        let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
    355358        let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    356359        let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph r l fresh_lbl in
    357           〈add_graph globals original_label (sequential ltl_params_ globals (INT … hdw (bitvector_of_nat … (stacksize … int_fun))) l) graph, luniv〉
     360          〈add_graph globals original_label (sequential ltl_params_ globals (INT … hdw (bitvector_of_nat … (stacksize (spilled_no … coloured_graph) … int_fun))) l) graph, luniv〉
    358361      ]
    359362    | OPACCS opaccs dacc_a_reg dacc_b_reg sacc_a_reg sacc_b_reg ⇒
     
    376379  | GOTO l ⇒ 〈add_graph globals original_label (GOTO ltl_params_ globals l) graph, joint_if_luniverse globals (ertl_params globals) int_fun〉
    377380  ].
    378 
    379 lemma Sm_leq_n_m_leq_n:
    380   ∀m, n: nat.
    381     S m ≤ n → m ≤ n.
    382   #m #n /2/
    383 qed.
    384 
    385 let rec fold_aux
    386   (a, b: Type[0]) (f: BitVector 16 → a → b → b) (seed: b) (n: nat)
    387     on n: n ≤ 16 → BitVectorTrie a n → BitVector (16 - n) → b ≝
    388   match n return λn: nat. n ≤ 16 → BitVectorTrie a n → BitVector (16 - n) → b with
    389   [ O    ⇒ λinvariant: 0 ≤ 16. λtrie: BitVectorTrie a 0. λpath: BitVector 16.
    390     match trie return λx: nat. λtrie': BitVectorTrie a x. ∀prf: x = 0. b with
    391     [ Leaf l      ⇒ λproof. f path l seed
    392     | Stub s      ⇒ λproof. seed
    393     | Node n' l r ⇒ λabsrd. ⊥
    394     ] (refl … 0)
    395   | S n' ⇒ λinvariant: S n' ≤ 16. λtrie: BitVectorTrie a (S n'). λpath: BitVector (16 - S n').
    396     match trie return λx: nat. λtrie': BitVectorTrie a x. ∀prf: x = S n'. b with
    397     [ Leaf l      ⇒ λabsrd. ⊥
    398     | Stub s      ⇒ λproof. seed
    399     | Node n'' l r ⇒ λproof.
    400         fold_aux a b f (fold_aux a b f seed n' ? (l⌈BitVectorTrie a n'' ↦ BitVectorTrie a n'⌉) ((false:::path)⌈S (16 - S n') ↦ 16 - n'⌉)) n' ? (r⌈BitVectorTrie a n'' ↦ BitVectorTrie a n'⌉) ((true:::path)⌈S (16 - S n') ↦ 16 - n'⌉)
    401     ] (refl … (S n'))
    402   ].
    403   [ 1, 2: destruct(absrd)
    404   | 3,8: >minus_S_S <minus_Sn_m // @le_S_S_to_le //
    405   | 4,7: destruct(proof) %
    406   | 5,6: @Sm_leq_n_m_leq_n // ]
    407 qed.
    408381
    409382definition bvt_fold ≝
     
    415388      f (an_identifier LabelTag bv) a b
    416389    in
    417       fold_aux a b f' seed 16 ? trie [[]].
     390      bvtfold_aux a b f' seed 16 ? trie [[]].
    418391  //
    419392qed.
Note: See TracChangeset for help on using the changeset viewer.