- Timestamp:
- Apr 8, 2011, 11:51:38 AM (10 years ago)
- Location:
- src
- Files:
-
- 1 added
- 6 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/I8051.ma
r724 r746 105 105 | RegisterDPH ⇒ 35 106 106 ]. 107 108 definition physical_register_count ≝ 36. 109 110 definition word_of_register: Register → Word ≝ 111 λregister. 112 bitvector_of_nat ? (nat_of_register register). 107 113 108 114 definition compare_register: Register → Register → Compare ≝ -
src/ASM/Util.ma
r715 r746 115 115 λm, n: nat. 116 116 leb n m. 117 118 (* dpm: unless I'm being stupid, this isn't defined in the stdlib? *) 119 let 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 ]. 117 124 118 125 (* dpm: conflicts with library definitions -
src/ERTL/Liveness.ma
r745 r746 32 32 | ERTL_St_Call_Id id v l ⇒ set_singleton l 33 33 | ERTL_St_CondAcc _ l1 l2 ⇒ set_union ? (set_singleton l1) (set_singleton l2) 34 ]. 34 ]. 35 35 36 36 definition set_of_list ≝ … … 38 38 λl: list (BitVector n). 39 39 foldr ? ? (set_insert ?) (set_empty ?) l. 40 41 definition dptr ≝ 42 set_insert ? (word_of_register RegisterDPL) (set_singleton ? (word_of_register RegisterDPH)). -
src/ERTL/Uses.ma
r745 r746 9 9 let l ≝ increment ? (lookup ? ? register uses (zero 16)) in 10 10 insert ? 16 register l uses. 11 12 definition word_of_register: Register → Word ≝13 λregister.14 bitvector_of_nat ? (nat_of_register register).15 11 16 12 definition examine_statement ≝ -
src/common/Graphs.ma
r738 r746 10 10 definition label_eq : ∀x,y:label. (x=y) + (x≠y) ≝ identifier_eq ?. 11 11 12 13 12 definition graph : Type[0] → Type[0] ≝ identifier_map LabelTag. -
src/utilities/BitVectorTrieSet.ma
r698 r746 1 1 include "ASM/BitVectorTrie.ma". 2 include "ASM/Util.ma". 2 3 3 4 definition BitVectorTrieSet ≝ BitVectorTrie unit. … … 50 51 qed. 51 52 53 let 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 ] 77 qed. 78 79 (* 80 let rec set_diff (n: nat) (b: BitVectorTrieSet n) (c: BitVectorTrieSet n) on b: BitVectorTrieSet n ≝ 81 match b with 82 [ Stub ⇒ 83 *) 84 52 85 definition set_insert ≝ 53 86 λn: nat. … … 57 90 58 91 definition set_empty ≝ λn. Stub unit n. 92 93 definition 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.