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