1(* 2 * Copyright 2018, Data61 3 * Commonwealth Scientific and Industrial Research Organisation (CSIRO) 4 * ABN 41 687 119 230. 5 * 6 * This software may be distributed and modified according to the terms of 7 * the BSD 2-Clause license. Note that NO WARRANTY is provided. 8 * See "LICENSE_BSD2.txt" for details. 9 * 10 * @TAG(DATA61_BSD) 11 *) 12 13theory FastMap_Test 14imports 15 Lib.FastMap 16 Lib.LexordList 17 Lib.NICTATools 18 Lib.Qualify 19begin 20 21section \<open>Basic usage example\<close> 22 23experiment begin 24 local_setup \<open> 25 FastMap.define_map 26 (* The name of the map constant and names of associated theorems. 27 * This function constructs a set of sensible default names, but 28 * you can also choose different names manually. *) 29 (FastMap.name_opts_default "simple_test_map") 30 31 (* List of the actual mappings. These must be sorted by key 32 * and the key type must admit a linear order. *) 33 [(@{term "0 :: nat"}, @{term "0 :: nat"}), 34 (@{term "1 :: nat"}, @{term "1 :: nat"}), 35 (@{term "2 :: nat"}, @{term "1 :: nat"}), 36 (@{term "3 :: nat"}, @{term "2 :: nat"}), 37 (@{term "4 :: nat"}, @{term "3 :: nat"}), 38 (@{term "5 :: nat"}, @{term "5 :: nat"})] 39 40 (* Key transformer. Must be an injective function that maps the 41 * key type to a linorder type. This will usually be id, unless 42 * the key type isn't naturally linorder. See string_map below 43 * for an example of a non-trivial key transform. *) 44 @{term "id :: nat \<Rightarrow> nat"} 45 46 (* Extra simp rules to use when verifying the key ordering. *) 47 @{thms} 48 49 (* Use the default background simpset for solving goals. 50 * Set to true if you want precise control over the simpset. *) 51 false 52 \<close> 53 thm simple_test_map_def 54 55 text \<open>Default theorem names are generated based on the map name\<close> 56 thm simple_test_map_to_lookup_list 57 thm simple_test_map_lookups 58 thm simple_test_map_domain simple_test_map_range simple_test_map_keys_distinct 59 60 61 subsection \<open>Check the generated theorems\<close> 62 lemma "simple_test_map = map_of [(0, 0), (1, 1), (2, 1), (3, 2), (4, 3), (5, 5)]" 63 by (rule simple_test_map_to_lookup_list) 64 65 lemma 66 "simple_test_map 0 = Some 0" 67 "simple_test_map 1 = Some 1" 68 "simple_test_map 2 = Some 1" 69 "simple_test_map 3 = Some 2" 70 "simple_test_map 4 = Some 3" 71 "simple_test_map 5 = Some 5" 72 by (rule simple_test_map_lookups)+ 73 74 lemma 75 "dom simple_test_map = set [0, 1, 2, 3, 4, 5]" 76 by (rule simple_test_map_domain) 77 78 text \<open>Note that the range is not simplified\<close> 79 lemma 80 "ran simple_test_map = set [0, 1, 1, 2, 3, 5]" 81 by (rule simple_test_map_range) 82 83 lemma 84 "distinct ([0, 1, 2, 3, 4, 5] :: nat list)" 85 by (rule simple_test_map_keys_distinct[simplified list.map prod.sel]) 86 87end 88 89 90section \<open>Basic tests for the generated theorems\<close> 91 92ML \<open> 93fun create_int_map name n typ ctxt = 94 FastMap.define_map (FastMap.name_opts_default name) 95 (List.tabulate (n, fn i => (HOLogic.mk_number typ i, 96 HOLogic.mk_string (string_of_int i)))) 97 (Const (@{const_name id}, typ --> typ)) 98 @{thms} 99 false 100 ctxt 101\<close> 102 103experiment begin 104 local_setup \<open> 105 create_int_map "simple_test_map_100" 100 @{typ int} 106 \<close> 107 print_theorems 108 109 text \<open>Direct lookup theorems\<close> 110 lemma "simple_test_map_100 42 = Some ''42''" 111 by (rule simple_test_map_100_lookups) 112 113 text \<open>We try to configure the default simpset for fast lookups\<close> 114 lemma "simple_test_map_100 100 = None" 115 by (time_methods 116 default: 117 \<open>simp add: simple_test_map_100_def\<close> 118 minimal: 119 \<open>simp only: simple_test_map_100_def FastMap.lookup_tree_simps' 120 id_apply rel_simps if_False 121 cong: if_weak_cong\<close> 122 slow_simps: 123 \<open>simp add: simple_test_map_100_def FastMap.lookup_tree.simps 124 del: FastMap.lookup_tree_simps' 125 cong: if_weak_cong cong del: if_cong\<close> 126 slow_simps_l4v: 127 \<open>simp add: simple_test_map_100_def FastMap.lookup_tree.simps 128 del: FastMap.lookup_tree_simps' 129 cong: if_cong cong del: if_weak_cong\<close> 130 (* This simulates using a functional map instead of FastMap *) 131 fun_map: 132 \<open>simp add: simple_test_map_100_to_lookup_list\<close> 133 (* Strangely, this is much faster, even though it uses the same rules 134 (and even has the same simp trace) *) 135 fun_map_minimal: 136 \<open>simp only: simple_test_map_100_to_lookup_list 137 map_of.simps fun_upd_apply prod.sel 138 rel_simps simp_thms if_True if_False 139 cong: if_weak_cong\<close>) 140 141 text \<open>Domain and range theorems\<close> 142 lemma "dom simple_test_map_100 = {0 .. 99}" 143 apply (simp add: atLeastAtMost_upto upto_rec1) 144 by (simp only: simple_test_map_100_domain set_simps) 145 146 lemma 147 "ran simple_test_map_100 = 148 set ([[x] | x \<leftarrow> ''0123456789''] @ [[x, y] | x \<leftarrow> ''123456789'', y \<leftarrow> ''0123456789''])" 149 apply simp 150 by (simp only: simple_test_map_100_range set_simps) 151end 152 153 154 155section \<open>Test with larger mapping\<close> 156 157experiment begin 158 local_setup \<open> 159 create_int_map "simple_test_map_1000" 1000 @{typ int} 160 \<close> 161 162 lemma "simple_test_map_1000 42 = Some ''42''" 163 by (rule simple_test_map_1000_lookups) 164 165 lemma "simple_test_map_1000 1000 = None" 166 by (simp add: simple_test_map_1000_def) 167 168 lemma "dom simple_test_map_1000 = {0 .. 999}" 169 apply (simp add: atLeastAtMost_upto upto_rec1) 170 by (simp only: simple_test_map_1000_domain set_simps) 171 172 lemma 173 "ran simple_test_map_1000 = 174 set ([[x] | x \<leftarrow> ''0123456789''] @ 175 [[x, y] | x \<leftarrow> ''123456789'', y \<leftarrow> ''0123456789''] @ 176 [[x, y, z] | x \<leftarrow> ''123456789'', y \<leftarrow> ''0123456789'', z \<leftarrow> ''0123456789''])" 177 apply simp 178 by (simp only: simple_test_map_1000_range set_simps) 179end 180 181 182 183section \<open>Optimising an existing mapping\<close> 184 185experiment begin 186 local_setup \<open> 187 let 188 val map_def = 189 fold (fn i => fn m => 190 @{term "fun_upd :: (int \<Rightarrow> string option) \<Rightarrow> int \<Rightarrow> string option \<Rightarrow> (int \<Rightarrow> string option)"} $ 191 m $ HOLogic.mk_number @{typ int} i $ 192 (@{term "Some :: string \<Rightarrow> string option"} $ HOLogic.mk_string (string_of_int i))) 193 (0 upto 100 - 1) @{term "Map.empty :: int \<Rightarrow> string option"}; 194 val name = Binding.name "slow_map"; 195 in 196 Local_Theory.define 197 ((name, NoSyn), ((Thm.def_binding name, []), map_def)) 198 #> snd 199 end 200 \<close> 201 thm slow_map_def 202 203 local_setup \<open> 204 create_int_map "fast_map" 100 @{typ int} 205 \<close> 206 207 lemma slow_map_alt_def: 208 "slow_map = fast_map" 209 unfolding slow_map_def 210 unfolding fast_map_to_lookup_list 211 apply (simp only: FastMap.map_of_rev[symmetric] fast_map_keys_distinct) 212 apply (simp only: rev.simps append.simps map_of.simps prod.sel) 213 done 214 215 lemma "slow_map 42 = Some ''42''" 216 by (time_methods 217 fast_map: \<open>simp add: slow_map_alt_def fast_map_def\<close> 218 direct_lookup: \<open>simp add: slow_map_alt_def fast_map_lookups\<close> 219 slow_map: \<open>simp add: slow_map_def\<close>) 220 221 lemma "slow_map 100 = None" 222 by (time_methods 223 fast_map: \<open>simp add: slow_map_alt_def fast_map_def\<close> 224 slow_map: \<open>simp add: slow_map_def\<close>) 225 226 lemma "dom slow_map = {0 .. 99}" 227 supply upto_rec1[simp] 228 apply (simp add: atLeastAtMost_upto) 229 (* Domain for slow_map gets generated in reverse order *) 230 using set_rev[where xs="[0 .. 99] :: int list", simplified] 231 232 by (time_methods 233 fast_map: \<open>simp add: slow_map_alt_def fast_map_domain\<close> 234 slow_map: \<open>simp add: slow_map_def\<close>) 235end 236 237 238 239section \<open>Simpset tests\<close> 240 241definition my_id 242 where 243 "my_id x \<equiv> x" 244 245lemma my_id_loop: 246 "my_id x = my_id (Suc x) - 1" 247 by (simp add: my_id_def) 248 249declare my_id_loop[simp] 250declare my_id_def[simp] 251 252text \<open>With our faulty simpset, the key ordering solver gets into a loop.\<close> 253local_setup \<open> fn ctxt => 254 (Timeout.apply (Time.fromSeconds 5) ( 255 FastMap.define_map (FastMap.name_opts_default "minimal_test_map") 256 (List.tabulate (100, fn i => (HOLogic.mk_number @{typ nat} i, 257 HOLogic.mk_string (string_of_int i)))) 258 @{term "my_id :: nat => nat"} 259 @{thms} 260 false 261 ) ctxt; 262 error "FastMap timeout test: shouldn't get here" 263 ) 264 handle Timeout.TIMEOUT _ => ctxt 265\<close> 266declare my_id_loop[simp del] 267declare my_id_def[simp del] 268 269 270text \<open>The solver for injectivity of the key transformer can also loop.\<close> 271lemma inj_my_id_loop[simp]: 272 fixes x y :: nat 273 shows "(my_id x = my_id y) = (my_id (x + x) = my_id (y + y))" 274 by (auto simp: my_id_def) 275 276lemma my_id_lessI: 277 "(my_id x < my_id y) = (x < y)" 278 by (simp add: my_id_def) 279 280local_setup \<open> fn ctxt => 281 (Timeout.apply (Time.fromSeconds 5) ( 282 FastMap.define_map (FastMap.name_opts_default "minimal_test_map") 283 (List.tabulate (100, fn i => (HOLogic.mk_number @{typ nat} i, 284 HOLogic.mk_string (string_of_int i)))) 285 @{term "my_id :: nat => nat"} 286 @{thms my_id_lessI} 287 false 288 ) ctxt; 289 error "FastMap timeout test: shouldn't get here" 290 ) 291 handle Timeout.TIMEOUT _ => ctxt 292\<close> 293 294 295text \<open>Manual simpset control.\<close> 296lemma my_id_inj: 297 "inj my_id" 298 by (simp add: inj_def my_id_def) 299 300local_setup \<open> 301 FastMap.define_map (FastMap.name_opts_default "minimal_test_map") 302 (List.tabulate (100, fn i => (HOLogic.mk_number @{typ nat} i, 303 HOLogic.mk_string (string_of_int i)))) 304 @{term "my_id :: nat => nat"} 305 @{thms my_id_lessI rel_simps my_id_inj[THEN inj_eq]} 306 true 307\<close> 308 309 310 311section \<open>Test preserving user input\<close> 312 313text \<open> 314 Even when using the background simpset, FastMap should never simplify 315 inside of the supplied keys and values. 316\<close> 317 318local_setup \<open> 319 FastMap.define_map (FastMap.name_opts_default "preserve_input_test_map") 320 (List.tabulate (100, fn i => (@{term "(+) :: nat \<Rightarrow> nat \<Rightarrow> nat"} $ 321 HOLogic.mk_number @{typ nat} i $ 322 @{term "0 :: nat"}, 323 @{term "rev :: string \<Rightarrow> string"} $ 324 HOLogic.mk_string (string_of_int i)))) 325 @{term "id :: nat => nat"} 326 @{thms} 327 false 328\<close> 329 330lemma "preserve_input_test_map (42 + 0) = Some (rev ''42'')" 331 apply (fails \<open>simp; rule preserve_input_test_map_lookups\<close>) 332 by (rule preserve_input_test_map_lookups) 333 334lemma "42 + 0 \<in> dom preserve_input_test_map" 335 apply (fails \<open>solves \<open>simp; unfold preserve_input_test_map_domain; intro list.set_intros\<close>\<close>) 336 by (unfold preserve_input_test_map_domain; intro list.set_intros) 337 338lemma "rev ''42'' \<in> ran preserve_input_test_map" 339 apply (fails \<open>solves \<open>simp; unfold preserve_input_test_map_range; intro list.set_intros\<close>\<close>) 340 by (unfold preserve_input_test_map_range; intro list.set_intros) 341 342 343 344section \<open>Test @{command qualify}\<close> 345 346locale qualified_map_test 347qualify qualified_map_test 348 349local_setup \<open> 350 create_int_map "qualified_map" 100 @{typ nat} 351\<close> 352 353end_qualify 354 355text \<open>Check that unqualified name doesn't exist\<close> 356ML \<open> 357 @{assert} (not (can dest_Const @{term qualified_map})); 358 @{assert} (can dest_Const @{term qualified_map_test.qualified_map}); 359\<close> 360 361 362 363section \<open>Test locales\<close> 364 365context qualified_map_test begin 366 367local_setup \<open> 368 create_int_map "locale_map" 100 @{typ nat} 369\<close> 370thm locale_map_def 371 372end 373 374text \<open>Check that unqualified name doesn't exist\<close> 375ML \<open> 376 @{assert} (not (can dest_Const @{term locale_map})); 377 @{assert} (can dest_Const @{term qualified_map_test.locale_map}); 378\<close> 379 380 381 382section \<open>Test other key types\<close> 383 384subsection \<open>Finite words\<close> 385 386experiment begin 387 local_setup \<open> 388 create_int_map "word_map" 256 @{typ word32} 389 \<close> 390 391 lemma "word_map 42 = Some ''42''" 392 by (rule word_map_lookups) 393 394 lemma "word_map 999 = None" 395 by (simp add: word_map_def) 396end 397 398 399subsection \<open>Strings\<close> 400 401instantiation char :: ord begin 402 definition[simp]: "(c::char) < d \<equiv> (of_char c :: nat) < of_char d" 403 definition[simp]: "(c::char) \<le> d \<equiv> (of_char c :: nat) \<le> of_char d" 404 instance .. 405end 406 407instantiation char :: linorder begin 408 instance 409 by intro_classes 410 (auto simp: preorder_class.less_le_not_le linorder_class.linear) 411end 412 413experiment begin 414 text \<open> 415 Strings are not naturally in the @{class linorder} class. 416 However, we can use a key transformer (@{const lexord_list}) 417 to use strings as @{class linorder} keys. 418 \<close> 419 local_setup \<open> 420 FastMap.define_map (FastMap.name_opts_default "string_map") 421 (List.tabulate (100, fn i => (HOLogic.mk_string (StringCvt.padLeft #"0" 3 (string_of_int i)), 422 HOLogic.mk_number @{typ nat} i))) 423 @{term "lexord_list :: string \<Rightarrow> char lexord_list"} 424 @{thms} 425 false 426 \<close> 427 428 lemma "string_map ''042'' = Some 42" 429 by (rule string_map_lookups) 430 431 lemma "string_map ''0123'' = None" 432 by (simp add: string_map_def) 433 434 text \<open> 435 Notice that the domain and map theorems don't include the key 436 transformer; it is merely an implementation detail. 437 \<close> 438 schematic_goal "(dom string_map = (?x :: string set))" 439 by (rule string_map_domain) 440 schematic_goal "string_map = map_of (?binds :: (string \<times> nat) list)" 441 by (rule string_map_to_lookup_list) 442end 443 444 445 446section \<open>Small inputs\<close> 447experiment begin 448 text \<open> 449 Note that the current interface doesn't support empty mappings, 450 because it would have no input values to derive the correct map 451 type. This tests 1-to-4-element mappings. 452 \<close> 453 454 local_setup \<open> 455 create_int_map "small_test_map_1" 1 @{typ nat} 456 \<close> 457 lemma 458 "small_test_map_1 \<equiv> FastMap.lookup_tree id (FastMap.Node 0 ''0'' FastMap.Leaf FastMap.Leaf)" 459 by (rule small_test_map_1_def) 460 lemma 461 "small_test_map_1 = map_of [(0, ''0'')]" 462 by (rule small_test_map_1_to_lookup_list) 463 lemma 464 "small_test_map_1 0 = Some ''0''" 465 by (rule small_test_map_1_lookups) 466 467 local_setup \<open> 468 create_int_map "small_test_map_2" 2 @{typ nat} 469 #> 470 create_int_map "small_test_map_3" 3 @{typ nat} 471 #> 472 create_int_map "small_test_map_4" 4 @{typ nat} 473 \<close> 474end 475 476end