1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6 7theory RangeMap_Test 8imports 9 Lib.RangeMap 10 Main 11begin 12 13section \<open>Examples for RangeMap\<close> 14 15experiment begin 16 17subsection \<open>Basic usage\<close> 18 19local_setup \<open> 20RangeMap.define_map 21 (* Specification of names to generate. "name_opts_default" generates qualified names 22 starting with the given string i.e. "test_map.foo". *) 23 (RangeMap.name_opts_default "test_map") 24 25 (* List of ((start key, end key), value). 26 Key ranges include the start but not the end points. *) 27 [((@{cterm "1::nat"}, @{cterm "2::nat"}), @{cterm "True"}), 28 ((@{cterm "2::nat"}, @{cterm "3::nat"}), @{cterm "False"}), 29 ((@{cterm "5::nat"}, @{cterm "8::nat"}), @{cterm "True \<and> False"}), 30 (* Key ranges are allowed to be empty, such as this one *) 31 ((@{cterm "8::nat"}, @{cterm "8::nat"}), @{cterm "True \<or> False"}), 32 (* Test for input preservation; see below *) 33 ((@{cterm "if True then 8::nat else undefined"}, @{cterm "6 + 7 :: nat"}), 34 @{cterm "False \<longrightarrow> True"}) 35 ] 36 37 (* Key and value types. *) 38 @{typ nat} @{typ bool} 39 (* Key comparison solver. This should be a conversion that converts 40 key comparisons to True or False. *) 41 (Simplifier.rewrite @{context}) 42\<close> 43print_theorems 44 45text \<open> 46 Generated definitions for lookup tree and list: 47\<close> 48thm test_map.tree_def test_map.list_def 49 50text \<open> 51 Lookup theorems: 52\<close> 53thm test_map.lookups 54 55text \<open> 56 We also get lookup theorems for the start of each range (if nonempty). 57 These can be useful simplifier equations in some scenarios. 58\<close> 59thm test_map.start_lookups 60 61text \<open> 62 Test that user-provided key terms are preserved verbatim. 63\<close> 64ML \<open> 65@{assert} 66 (Thm.prop_of @{thm test_map.lookups(5)[where x=x]} 67 = @{term "Trueprop (((if True then 8 else undefined) \<le> x \<and> x < 6 + 7) 68 = (RangeMap.lookup_range_tree test_map.tree x 69 = Some ((if True then 8 else undefined, 6 + 7), False \<longrightarrow> True)))"}); 70\<close> 71 72text \<open> 73 The domain is just the union of all key ranges. 74 In practice, maps tend to have many contiguous ranges. RangeMap also 75 generates a "compact" domain theorem that merges adjacent ranges. 76\<close> 77thm test_map.domain test_map.domain_compact 78 79 80subsection \<open>Test that empty maps are supported\<close> 81 82local_setup \<open> 83RangeMap.define_map 84 (RangeMap.name_opts_default "empty_test") 85 [] 86 @{typ int} @{typ int} 87 Thm.reflexive (* unused *) 88\<close> 89print_theorems 90 91 92subsection \<open>Stress testing\<close> 93ML \<open> 94fun range_map_test_legendre n = 95 let fun P q x = if q*q > x then true else x mod q <> 0 andalso P (q+1) x; 96 in (1 upto n) 97 |> map (fn k => ((k*k, (k+1)*(k+1)), hd (filter (P 2) (k*k+1 upto (k+1)*(k+1))))) end; 98 99fun range_map_test_legendre_ct T n = 100 let fun cterm_of_num T n = Thm.cterm_of @{context} (HOLogic.mk_number T n); 101 in range_map_test_legendre n 102 |> map (fn ((ks, ke), v) => ((cterm_of_num T ks, cterm_of_num T ke), cterm_of_num T v)) end; 103\<close> 104 105local_setup \<open> 106RangeMap.define_map 107 (RangeMap.name_opts_default "legendre_10") 108 (range_map_test_legendre_ct @{typ nat} 10) 109 @{typ nat} @{typ nat} 110 (FP_Eval.eval_conv @{context} (FP_Eval.make_rules @{thms rel_simps} [])) 111\<close> 112 113local_setup \<open> 114RangeMap.define_map 115 (RangeMap.name_opts_default "legendre_100") 116 (range_map_test_legendre_ct @{typ nat} 100) 117 @{typ nat} @{typ nat} 118 (FP_Eval.eval_conv @{context} (FP_Eval.make_rules @{thms rel_simps} [])) 119\<close> 120 121local_setup \<open> 122RangeMap.define_map 123 (RangeMap.name_opts_default "legendre_1000") 124 (range_map_test_legendre_ct @{typ nat} 1000) 125 @{typ nat} @{typ nat} 126 (FP_Eval.eval_conv @{context} (FP_Eval.make_rules @{thms rel_simps} [])) 127\<close> 128 129(* Example of proof using range map *) 130lemma legendre_100_values: 131 "RangeMap.lookup_range_tree legendre_100.tree k = Some ((start, end), v) 132 \<Longrightarrow> start < v \<and> v < end" 133 (* Convert to list and expand *) 134 apply (subst (asm) legendre_100.tree_list_lookup_eq) 135 apply (drule RangeMap.range_map_of_Some) 136 apply (clarsimp simp: legendre_100.list_def) 137 apply linarith 138 done 139 140end 141 142end 143