Changeset 746 for src

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:

• ASM/I8051.ma (modified) (1 diff)
• ASM/Util.ma (modified) (1 diff)
• ERTL/Liveness.ma (modified) (2 diffs)
• ERTL/Uses.ma (modified) (1 diff)
• ERTL/VariableSet.ma (added)
• common/Graphs.ma (modified) (1 diff)
• utilities/BitVectorTrieSet.ma (modified) (3 diffs)

src/ASM/I8051.ma

@@ -105 +105 @@
   | RegisterDPH ⇒ 35
   ].
+  
+definition physical_register_count ≝ 36.
+
+definition word_of_register: Register → Word ≝
+  λregister.
+    bitvector_of_nat ? (nat_of_register register).
 
 definition compare_register: Register → Register → Compare ≝

src/ASM/Util.ma

@@ -115 +115 @@
   λm, n: nat.
     leb n m.
+    
+(* dpm: unless I'm being stupid, this isn't defined in the stdlib? *)
+let rec eq_nat (n: nat) (m: nat) on n: bool ≝
+  match n with
+  [ O ⇒ match m with [ O ⇒ true | _ ⇒ false ]
+  | S n' ⇒ match m with [ S m' ⇒ eq_nat n' m' | _ ⇒ false ]
+  ].
 
 (* dpm: conflicts with library definitions

src/ERTL/Liveness.ma

@@ -32 +32 @@
   | ERTL_St_Call_Id id v l ⇒ set_singleton l
   | ERTL_St_CondAcc _ l1 l2 ⇒ set_union ? (set_singleton l1) (set_singleton l2)
-  ].
+  ]. 
 
 definition set_of_list ≝
@@ -38 +38 @@
   λl: list (BitVector n).
     foldr ? ? (set_insert ?) (set_empty ?) l.
+    
+definition dptr ≝
+  set_insert ? (word_of_register RegisterDPL) (set_singleton ? (word_of_register RegisterDPH)).

src/ERTL/Uses.ma

@@ -9 +9 @@
     let l ≝ increment ? (lookup ? ? register uses (zero 16)) in
       insert ? 16 register l uses.
-      
-definition word_of_register: Register → Word ≝
-  λregister.
-    bitvector_of_nat ? (nat_of_register register).
       
 definition examine_statement ≝

src/common/Graphs.ma

@@ -10 +10 @@
 definition label_eq : ∀x,y:label. (x=y) + (x≠y) ≝ identifier_eq ?.
 
-
 definition graph : Type[0] → Type[0] ≝ identifier_map LabelTag.

src/utilities/BitVectorTrieSet.ma

@@ -1 +1 @@
 include "ASM/BitVectorTrie.ma".
+include "ASM/Util.ma".
 
 definition BitVectorTrieSet ≝ BitVectorTrie unit.
@@ -50 +51 @@
 qed.
 
+let rec set_eq (n: nat) (b: BitVectorTrieSet n) (c: BitVectorTrieSet n) on b: bool ≝
+  match b return λh. λ_. n = h → bool with
+  [ Stub s ⇒
+    match c with
+    [ Stub s' ⇒ λ_. eq_nat s s'
+    | _ ⇒ λ_. false
+    ]
+  | Leaf l ⇒
+    match c with
+    [ Leaf l' ⇒ λ_. true (* dpm: l and l' both unit *)
+    | _ ⇒ λ_. false
+    ]
+  | Node h l r ⇒
+    match c with
+    [ Node h' l' r' ⇒ λprf. andb (set_eq h l ?) (set_eq h r ?)
+    | _ ⇒ λ_. false
+    ]
+  ] (refl ? n).
+  [ 1: @ r
+  | 2: lapply (injective_S … prf)
+       # H
+       < H
+       @ r'
+  ]
+qed.
+
+(*
+let rec set_diff (n: nat) (b: BitVectorTrieSet n) (c: BitVectorTrieSet n) on b: BitVectorTrieSet n ≝
+  match b with
+  [ Stub ⇒ 
+*)
+
 definition set_insert ≝
   λn: nat.
@@ -57 +90 @@
 
 definition set_empty ≝ λn. Stub unit n.
+
+definition set_singleton ≝
+  λn: nat.
+  λb: BitVector n.
+    insert unit n b it (set_empty ?).