Changeset 1285 for src/utilities
 Timestamp:
 Oct 3, 2011, 3:08:21 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/utilities/adt/table_adt.ma
r1274 r1285 13 13  empty: table dom_type rng_type 14 14  node : nat → dom_type → rng_type → table dom_type rng_type → table dom_type rng_type → table dom_type rng_type. 15 16 definition tbl_empty ≝ empty. 17 18 definition tbl_size ≝ 15 16 definition tbl_height ≝ 19 17 λdom_type : Type[0]. 20 18 λrng_type : Type[0]. … … 25 23 ]. 26 24 25 let rec tbl_size 26 (dom_type : Type[0]) (rng_type : Type[0]) (the_table: table dom_type rng_type) 27 on the_table: nat ≝ 28 match the_table with 29 [ empty ⇒ 0 30  node sz key val l r ⇒ S (tbl_size … l) + (tbl_size … r) 31 ]. 32 33 definition tbl_empty ≝ 34 λdom_type: Type[0]. 35 λrng_type: Type[0]. 36 empty dom_type rng_type. 37 38 definition tbl_is_empty ≝ 39 λdom_type: Type[0]. 40 λrng_type: Type[0]. 41 λthe_table: table dom_type rng_type. 42 match the_table with 43 [ empty ⇒ true 44  _ ⇒ false 45 ]. 46 47 definition tbl_is_empty_p ≝ 48 λdom_type: Type[0]. 49 λrng_type: Type[0]. 50 λthe_table: table dom_type rng_type. 51 match the_table with 52 [ empty ⇒ True 53  _ ⇒ False 54 ]. 55 27 56 let rec tbl_to_list 28 57 (dom_type: Type[0]) (rng_type: Type[0]) (the_table: table dom_type rng_type) … … 32 61  node sz key val l r ⇒ 〈key, val〉 :: tbl_to_list … l @ tbl_to_list … r 33 62 ]. 34 35 axiom tbl_insert : ∀key_type, rng_type. key_type → rng_type → table key_type rng_type → table key_type rng_type. 36 37 axiom tbl_merge: 38 ∀key_type, rng_type. 39 (key_type → key_type → order) → table key_type rng_type → table key_type rng_type → table key_type rng_type. 40 41 axiom tbl_remove : ∀key_type, rng_type. key_type → table key_type rng_type → table key_type rng_type. 63 64 let rec tbl_min_binding 65 (key_type: Type[0]) (rng_type: Type[0]) (the_table: table key_type rng_type) 66 (proof: ¬ (tbl_is_empty_p … the_table)) 67 on the_table: key_type × rng_type ≝ 68 match the_table return λx. ¬ (tbl_is_empty_p … x) → key_type × rng_type with 69 [ empty ⇒ λabsurd. ? 70  node sz key val l r ⇒ λproof. 71 match l return λx. x = l → key_type × rng_type with 72 [ empty ⇒ λproof. 〈key, val〉 73  _ ⇒ λproof. tbl_min_binding key_type rng_type l ? 74 ] (refl … l) 75 ] proof. 76 [1: normalize in absurd; 77 elim absurd; 78 #ABSURD 79 @⊥ @ABSURD @I 80 2: <proof 81 normalize 82 /2/ 83 ] 84 qed. 85 86 definition tbl_create ≝ 87 λkey_type: Type[0]. 88 λrng_type: Type[0]. 89 λleft : table key_type rng_type. 90 λkey : key_type. 91 λval : rng_type. 92 λright : table key_type rng_type. 93 let hl ≝ tbl_height … left in 94 let hr ≝ tbl_height … right in 95 let height ≝ if gtb hl hr then hl + 1 else hr + 1 in 96 node key_type rng_type height key val left right. 97 98 let rec tbl_balance 99 (key_type: Type[0]) (rng_type: Type[0]) (ord: key_type → key_type → order) 100 (left: table key_type rng_type) (key: key_type) (val: rng_type) 101 (right: table key_type rng_type) (left_proof: ¬ (tbl_is_empty_p … left)) 102 (right_proof: ¬ (tbl_is_empty_p … right)) 103 on left: table key_type rng_type ≝ 104 match gtb (tbl_height … left) ((tbl_height … right) + 2) with 105 [ true ⇒ 106 match left return λx. ¬ (tbl_is_empty_p … x) → table key_type rng_type with 107 [ empty ⇒ λabsurd. ? 108  node _ lv ld ll lr ⇒ λnon_empty_proof. 109 if gtb (tbl_height … ll) (tbl_height … lr) then 110 tbl_create … ll lv ld (tbl_create … lr key val right) 111 else 112 match lr return λx. ¬ (tbl_is_empty_p … x) → table key_type rng_type with 113 [ empty ⇒ λabsurd. ? 114  node _ lrv lrd lrl lrr ⇒ λ 115 tbl_create … (tbl_create … ll lv ld lrl) lrv lrd (tbl_create … lrr key val right) 116 ] 117 ] left_proof 118  false ⇒ ? 119 ]. 120 [1: normalize in absurd; 121 elim absurd 122 #ABSURD 123 @⊥ @ABSURD @I 124 *: cases daemon 125 ] 126 qed. 127 128 let rec tbl_remove_min_binding 129 (key_type: Type[0]) (rng_type: Type[0]) (ord: key_type → key_type → order) 130 (the_table: table key_type rng_type) (proof: ¬ (tbl_is_empty_p … the_table)) 131 on the_table: table key_type rng_type ≝ 132 match the_table return λx. ¬ (tbl_is_empty_p … x) → table key_type rng_type with 133 [ empty ⇒ λabsurd. ? 134  node sz key val l r ⇒ λproof. 135 match l return λx. x = l → table key_type rng_type with 136 [ empty ⇒ λproof. r 137  _ ⇒ λproof. tbl_balance … ord (tbl_remove_min_binding … ord l ?) key val r 138 ] (refl … l) 139 ] proof. 140 [1: normalize in absurd; 141 elim absurd; 142 #ABSURD 143 @⊥ @ABSURD @I 144 2: <proof 145 normalize 146 @nmk // 147 ] 148 qed. 149 150 let rec tbl_insert 151 (key_type: Type[0]) (rng_type: Type[0]) (ord: key_type → key_type → order) 152 (key: key_type) (val: rng_type) (the_table: table key_type rng_type) 153 on the_table: table key_type rng_type ≝ 154 match the_table with 155 [ empty ⇒ node … 1 key val (empty …) (empty …) 156  node sz key' val' l r ⇒ 157 match ord key key' with 158 [ order_lt ⇒ tbl_balance … ord (tbl_insert … ord key val l) key' val' r 159  order_eq ⇒ node … sz key val l r 160  order_gt ⇒ tbl_balance … ord l key' val' (tbl_insert … ord key val r) 161 ] 162 ]. 163 164 let rec tbl_merge 165 (dom_type: Type[0]) (rng_type: Type[0]) (ord: dom_type → dom_type → order) 166 (left: table dom_type rng_type) (right: table dom_type rng_type) 167 on left: table dom_type rng_type ≝ 168 match left with 169 [ empty ⇒ right 170  _ ⇒ 171 match right return λx. x = right → table dom_type rng_type with 172 [ empty ⇒ λid_proof. left 173  node sz key val l r ⇒ λid_proof. 174 let 〈x, d〉 ≝ tbl_min_binding dom_type rng_type right ? in 175 tbl_balance … ord left x d (tbl_remove_min_binding … ord right ?) 176 ] (refl … right) 177 ]. 178 <id_proof 179 normalize /2/ 180 qed. 181 182 let rec tbl_remove 183 (key_type: Type[0]) (rng_type: Type[0]) (ord: key_type → key_type → order) 184 (key: key_type) (the_table: table key_type rng_type) 185 on the_table: table key_type rng_type ≝ 186 match the_table with 187 [ empty ⇒ empty … 188  node sz key' val' l r ⇒ 189 match ord key key' with 190 [ order_lt ⇒ tbl_balance … ord (tbl_remove … ord key l) key' val' r 191  order_eq ⇒ tbl_merge … ord l r 192  order_gt ⇒ tbl_balance … ord l key' val' (tbl_remove … ord key r) 193 ] 194 ]. 42 195 43 196 let rec tbl_find … … 87 240  node sz key val l r ⇒ f val ∨ tbl_exists … f l ∨ tbl_exists … f r 88 241 ]. 89 90 axiom tbl_equal : ∀key_type, rng_type. table key_type rng_type 91 → table key_type rng_type → bool. 242 243 axiom tbl_equal: 244 ∀key_type, rng_type. 245 (key_type → key_type → order) → (rng_type → rng_type → order) → 246 table key_type rng_type → table key_type rng_type → bool. 92 247 93 248 let rec tbl_mapi … … 117 272  node sz key val l r ⇒ tbl_fold … f r (f key val (tbl_fold … f l seed)) 118 273 ]. 119 120 definition tbl_is_empty ≝121 λkey_type : Type[0].122 λrng_type : Type[0].123 λtable : table key_type rng_type.124 tbl_size … table = 0.125 274 126 275 definition tbl_singleton ≝ … … 129 278 λkey : key_type. 130 279 λrng : rng_type. 131 tbl_insert … key rng (tbl_empty …).280 node key_type rng_type 1 key rng (empty …) (empty …). 132 281 133 282 definition tbl_from_list ≝ 134 283 λkey_type : Type[0]. 135 284 λrng_type : Type[0]. 285 λord : key_type → key_type → order. 136 286 λthe_list : list (key_type × rng_type). 137 287 foldr … (λkey_rng. 138 288 let 〈key, rng〉 ≝ key_rng in 139 tbl_insert … key rng) (tbl_empty …) the_list.289 tbl_insert … ord key rng) (tbl_empty …) the_list. 140 290 141 291 definition tbl_filter ≝ 142 292 λdom_type : Type[0]. 143 293 λrng_type : Type[0]. 294 λord : dom_type → dom_type → order. 144 295 λf : rng_type → bool. 145 296 λthe_table: table dom_type rng_type. 146 297 let as_list ≝ tbl_to_list … the_table in 147 298 let filtered ≝ filter … (λx. f (\snd x)) as_list in 148 tbl_from_list … filtered.149 299 tbl_from_list … ord filtered. 300
Note: See TracChangeset
for help on using the changeset viewer.