Changeset 746


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
Files:
1 added
6 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/I8051.ma

    r724 r746  
    105105  | RegisterDPH ⇒ 35
    106106  ].
     107 
     108definition physical_register_count ≝ 36.
     109
     110definition word_of_register: Register → Word ≝
     111  λregister.
     112    bitvector_of_nat ? (nat_of_register register).
    107113
    108114definition compare_register: Register → Register → Compare ≝
  • src/ASM/Util.ma

    r715 r746  
    115115  λm, n: nat.
    116116    leb n m.
     117   
     118(* dpm: unless I'm being stupid, this isn't defined in the stdlib? *)
     119let rec eq_nat (n: nat) (m: nat) on n: bool ≝
     120  match n with
     121  [ O ⇒ match m with [ O ⇒ true | _ ⇒ false ]
     122  | S n' ⇒ match m with [ S m' ⇒ eq_nat n' m' | _ ⇒ false ]
     123  ].
    117124
    118125(* dpm: conflicts with library definitions
  • 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 ≝
  • src/common/Graphs.ma

    r738 r746  
    1010definition label_eq : ∀x,y:label. (x=y) + (x≠y) ≝ identifier_eq ?.
    1111
    12 
    1312definition graph : Type[0] → Type[0] ≝ identifier_map LabelTag.
  • src/utilities/BitVectorTrieSet.ma

    r698 r746  
    11include "ASM/BitVectorTrie.ma".
     2include "ASM/Util.ma".
    23
    34definition BitVectorTrieSet ≝ BitVectorTrie unit.
     
    5051qed.
    5152
     53let rec set_eq (n: nat) (b: BitVectorTrieSet n) (c: BitVectorTrieSet n) on b: bool ≝
     54  match b return λh. λ_. n = h → bool with
     55  [ Stub s ⇒
     56    match c with
     57    [ Stub s' ⇒ λ_. eq_nat s s'
     58    | _ ⇒ λ_. false
     59    ]
     60  | Leaf l ⇒
     61    match c with
     62    [ Leaf l' ⇒ λ_. true (* dpm: l and l' both unit *)
     63    | _ ⇒ λ_. false
     64    ]
     65  | Node h l r ⇒
     66    match c with
     67    [ Node h' l' r' ⇒ λprf. andb (set_eq h l ?) (set_eq h r ?)
     68    | _ ⇒ λ_. false
     69    ]
     70  ] (refl ? n).
     71  [ 1: @ r
     72  | 2: lapply (injective_S … prf)
     73       # H
     74       < H
     75       @ r'
     76  ]
     77qed.
     78
     79(*
     80let rec set_diff (n: nat) (b: BitVectorTrieSet n) (c: BitVectorTrieSet n) on b: BitVectorTrieSet n ≝
     81  match b with
     82  [ Stub ⇒
     83*)
     84
    5285definition set_insert ≝
    5386  λn: nat.
     
    5790
    5891definition set_empty ≝ λn. Stub unit n.
     92
     93definition set_singleton ≝
     94  λn: nat.
     95  λb: BitVector n.
     96    insert unit n b it (set_empty ?).
Note: See TracChangeset for help on using the changeset viewer.