Changeset 746 for src/ERTL


Ignore:
Timestamp:
Apr 8, 2011, 11:51:38 AM (9 years ago)
Author:
mulligan
Message:

Changes to bitvectortrieset: equality on sets. Added new file for translation of variable set functor. other small changes.

Location:
src/ERTL
Files:
1 added
2 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/Liveness.ma

    r745 r746  
    3232  | ERTL_St_Call_Id id v l ⇒ set_singleton l
    3333  | ERTL_St_CondAcc _ l1 l2 ⇒ set_union ? (set_singleton l1) (set_singleton l2)
    34   ].
     34  ]. 
    3535
    3636definition set_of_list ≝
     
    3838  λl: list (BitVector n).
    3939    foldr ? ? (set_insert ?) (set_empty ?) l.
     40   
     41definition dptr ≝
     42  set_insert ? (word_of_register RegisterDPL) (set_singleton ? (word_of_register RegisterDPH)).
  • src/ERTL/Uses.ma

    r745 r746  
    99    let l ≝ increment ? (lookup ? ? register uses (zero 16)) in
    1010      insert ? 16 register l uses.
    11      
    12 definition word_of_register: Register → Word ≝
    13   λregister.
    14     bitvector_of_nat ? (nat_of_register register).
    1511     
    1612definition examine_statement ≝
Note: See TracChangeset for help on using the changeset viewer.