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