From 1dfb962ad2134e11e04a65c76b7df1dd8bb4ec35 Mon Sep 17 00:00:00 2001 From: Japheth Lim Date: Thu, 11 Oct 2018 21:35:50 +1100 Subject: [PATCH] lib: add FastMap tool Many issues remain (see TODO list), but it's now mature enough to be used for proof automation and has a comprehensive test suite. --- lib/FastMap.thy | 603 +++++++++++++++++++++++++++++++++++++++++++ lib/FastMap_Test.thy | 437 +++++++++++++++++++++++++++++++ lib/ROOT | 2 + 3 files changed, 1042 insertions(+) create mode 100644 lib/FastMap.thy create mode 100644 lib/FastMap_Test.thy diff --git a/lib/FastMap.thy b/lib/FastMap.thy new file mode 100644 index 000000000..bff224942 --- /dev/null +++ b/lib/FastMap.thy @@ -0,0 +1,603 @@ +(* + * Copyright 2018, Data61 + * Commonwealth Scientific and Industrial Research Organisation (CSIRO) + * ABN 41 687 119 230. + * + * This software may be distributed and modified according to the terms of + * the BSD 2-Clause license. Note that NO WARRANTY is provided. + * See "LICENSE_BSD2.txt" for details. + * + * @TAG(DATA61_BSD) + *) + +theory FastMap +imports + LemmaBucket + Qualify +begin + +text \ + Efficient rules and tactics for working with large lookup tables (maps). + + Features: + \<^item> Define a binary lookup tree for any lookup table (requires linorder keys) + \<^item> Conversion from lookup tree to lookup lists + \<^item> Pre-computation of lookup results and domain/range sets + + See FastMap_Test for examples. +\ + +(* + * TODO: + * + * • Storing the (large) auxilliary theorems with Local_Theory.notes + * seems to take quadratic time. Investigate this, or work around + * it by hiding the map data behind additional constants. + * + * • Still a bit slower than the StaticFun package. Streamline the + * rulesets and proofs. + * + * • We use a lot of manual convs for performance and to avoid + * relying on the dynamic simpset. However, we should clean up the + * convs and move as much as possible to (simp only:) invocations. + * + * Note that running simp on deeply nested terms (e.g. lists) + * always takes quadratic time and we can't use it there. This is + * because rewritec unconditionally calls eta_conversion (urgh). + * + * • The injectivity prover currently hardcodes inj_def into the + * simpset. This should be changed at some point, probably by + * asking the user to prove it beforehand. + * + * • Using the simplifier to evaluate tree lookups is still quite + * slow because it looks at the entire tree term (even though + * most of it is irrelevant for any given lookup). We should + * provide a tactic or simproc to do this. + * + * We already generate lookup theorems for keys in the map, so + * this tactic should be optimised for missing keys. + * + * • The linorder requirement can be cumbersome. It arises because + * we express the map_of conversion as a general theorem using + * lookup_tree_valid. An alternative approach is to extend what + * StaticFun does, and cleverly extract the set of all relevant + * bindings from the tree on a case-by-case basis. + * + * We would still need to evaluate the key ordering function on + * the input keys, but any arbitrary relation would be allowed. + * This one probably calls for a wizard. + *) + +locale FastMap +qualify FastMap + +text \ + Binary lookup tree. This is largely an implementation detail, so we + choose the structure to make automation easier (e.g. separate fields + for the key and value). +\ +datatype ('k, 'v) Tree = Leaf | Node 'k 'v "('k, 'v) Tree" "('k, 'v) Tree" + +primrec + lookup_tree :: "('k, 'v) Tree \ ('k \ 'ok :: linorder) \ 'k \ 'v option" +where + "lookup_tree Leaf fn x = None" +| "lookup_tree (Node k v l r) fn x = + (if fn x = fn k then Some v + else if fn x < fn k then lookup_tree l fn x + else lookup_tree r fn x)" + +text \ + Predicate for well-formed lookup trees. + This states that the keys are distinct and appear in ascending order. + It also returns the lowest and highest keys in the tree (or None for empty trees). +\ +primrec lookup_tree_valid where + "lookup_tree_valid (key :: ('k \ 'ok :: linorder)) Leaf = (True, None)" +| "lookup_tree_valid key (Node k v lt rt) = + (let (lt_valid, lt_range) = lookup_tree_valid key lt; + (rt_valid, rt_range) = lookup_tree_valid key rt; + lt_low = (case lt_range of None \ k | Some (low, high) \ low); + rt_high = (case rt_range of None \ k | Some (low, high) \ high) + in (lt_valid \ rt_valid \ + (case lt_range of None \ True | Some (low, high) \ key high < key k) \ + (case rt_range of None \ True | Some (low, high) \ key k < key low), + Some (lt_low, rt_high)))" + +lemma lookup_tree_valid_simps': + "lookup_tree_valid key Leaf = (True, None)" + "lookup_tree_valid key (Node k v Leaf Leaf) = (True, Some (k, k))" + "\ lookup_tree_valid key (Node lk lv llt lrt) = (True, Some (llow, lhigh)); + key lhigh < key k + \ \ lookup_tree_valid key (Node k v (Node lk lv llt lrt) Leaf) = + (True, Some (llow, k))" + "\ lookup_tree_valid key (Node rk rv rlt rrt) = (True, Some (rlow, rhigh)); + key k < key rlow + \ \ lookup_tree_valid key (Node k v Leaf (Node rk rv rlt rrt)) = + (True, Some (k, rhigh))" + "\ lookup_tree_valid key (Node lk lv llt lrt) = (True, Some (llow, lhigh)); + lookup_tree_valid key (Node rk rv rlt rrt) = (True, Some (rlow, rhigh)); + key lhigh < key k; + key k < key rlow + \ \ lookup_tree_valid key (Node k v (Node lk lv llt lrt) (Node rk rv rlt rrt)) = + (True, Some (llow, rhigh))" + by auto + +lemma lookup_tree_valid_empty: + "lookup_tree_valid key tree = (True, None) \ tree = Leaf" + apply (induct tree) + apply simp + apply (fastforce split: prod.splits option.splits if_splits) + done + +lemma lookup_tree_valid_range: + "lookup_tree_valid key tree = (True, Some (low, high)) \ key low \ key high" + apply (induct tree arbitrary: low high) + apply simp + apply (fastforce split: prod.splits option.splits if_splits) + done + +lemma lookup_tree_valid_in_range: + "lookup_tree_valid key tree = (True, Some (low, high)) \ + lookup_tree tree key k = Some v \ + key k \ {key low .. key high}" + apply (induct tree arbitrary: k v low high) + apply simp + apply (fastforce split: prod.splits option.splits if_split_asm + dest: lookup_tree_valid_empty lookup_tree_valid_range) + done + +lemma lookup_tree_valid_in_range_None: + "lookup_tree_valid key tree = (True, Some (low, high)) \ + key k \ {key low .. key high} \ + lookup_tree tree key k = None" + using lookup_tree_valid_in_range by fastforce + +text \ + Flatten a lookup tree into an assoc-list. + As long as the tree is well-formed, both forms are equivalent. +\ +primrec lookup_tree_to_map where + "lookup_tree_to_map Leaf = []" +| "lookup_tree_to_map (Node k v lt rt) = lookup_tree_to_map lt @ [(k, v)] @ lookup_tree_to_map rt" + +lemma lookup_tree_to_map_range: + "lookup_tree_valid key tree = (True, Some (low, high)) \ + (k, v) \ set (lookup_tree_to_map tree) \ + key k \ {key low .. key high}" + apply (induct tree arbitrary: k v low high) + apply simp + apply (fastforce split: prod.splits option.splits if_split_asm + dest: lookup_tree_valid_empty lookup_tree_valid_range) + done + +lemma lookup_tree_dom_distinct_sorted_: + "fst (lookup_tree_valid key tree) \ + distinct (lookup_tree_to_map tree) \ sorted (map (key o fst) (lookup_tree_to_map tree))" + apply (induct tree) + apply simp + apply (fastforce simp: sorted_append + split: prod.splits option.splits if_splits + dest: lookup_tree_valid_empty lookup_tree_valid_range + lookup_tree_valid_in_range lookup_tree_to_map_range + elim: lookup_tree_valid_in_range_None) + done + +lemmas lookup_tree_dom_distinct = lookup_tree_dom_distinct_sorted_[THEN conjunct1] +lemmas lookup_tree_dom_sorted = lookup_tree_dom_distinct_sorted_[THEN conjunct2] + +(* The goal is eta-expanded and flipped, which seems to help the proof *) +lemma lookup_tree_to_map_of_: + "fst (lookup_tree_valid key tree) \ + map_of (map (apfst key) (lookup_tree_to_map tree)) (key k) = lookup_tree tree key k" + apply (induct tree arbitrary: k) + apply simp + (* this big blob just does case distinctions of both subtrees and + all possible lookup results within each, then solves *) + (* slow 10s *) + apply (fastforce simp: apfst_def map_prod_def map_add_def + split: prod.splits option.splits if_splits + dest: lookup_tree_valid_empty lookup_tree_valid_range lookup_tree_valid_in_range + elim: lookup_tree_valid_in_range_None) + done + +(* Standard form of above *) +lemma lookup_tree_to_map_of: + "fst (lookup_tree_valid key tree) \ + lookup_tree tree key = map_of (map (apfst key) (lookup_tree_to_map tree)) o key" + apply (rule ext) + apply (simp add: lookup_tree_to_map_of_) + done + +lemma map_of_key: + "inj key \ map_of (map (apfst key) binds) o key = map_of binds" + apply (rule ext) + apply (induct binds) + apply simp + apply (clarsimp simp: inj_def dom_def) + done + +lemma lookup_tree_to_map_of_distinct: + "\ fst (lookup_tree_valid key tree); + lookup_tree_to_map tree = binds; + lookup_tree tree key = map_of (map (apfst key) binds) o key + \ \ distinct (map (key o fst) binds)" + apply (drule sym[where t = binds]) + apply clarsimp + apply (thin_tac "binds = _") + apply (induct tree) + apply simp + apply (fastforce simp: map_add_def lookup_tree_to_map_of + split: prod.splits option.splits if_splits + dest: lookup_tree_valid_empty lookup_tree_valid_range + lookup_tree_valid_in_range lookup_tree_to_map_range + elim: lookup_tree_valid_in_range_None) + done + +lemma distinct_inj: + "inj f \ distinct xs = distinct (map f xs)" + apply (induct xs) + apply simp + apply (simp add: inj_image_mem_iff) + done + +(* Top-level rule for converting to lookup list. + We add a distinctness assertion for inferring the range of values. *) +lemma lookup_tree_to_map_of_gen: + "\ inj key; + fst (lookup_tree_valid key tree); + lookup_tree_to_map tree = binds + \ \ lookup_tree tree key = map_of binds \ distinct (map fst binds)" + using lookup_tree_to_map_of + apply (fastforce intro: lookup_tree_to_map_of_distinct + simp: map_of_key distinct_inj) + done + +text \ + Domain and range of a @{const map_of}. + Like @{thm dom_map_of_conv_image_fst} but leaving out the set bloat. +\ +lemma dom_map_of_conv_list: + "dom (map_of xs) = set (map fst xs)" + by (simp add: dom_map_of_conv_image_fst) + +lemma ran_map_of_conv_list: + "distinct (map fst xs) \ ran (map_of xs) = set (map snd xs)" + by (erule distinct_map_via_ran) + +text \ + Read lookup rules from a @{const map_of}. +\ + +lemma map_of_lookups: + "m = map_of binds \ distinct (map fst binds) \ + list_all (\(k, v). m k = Some v) binds" + apply (induct binds) + apply simp + apply (force simp: list_all_iff) + done + +(* Helper for converting from maps defined as @{const fun_upd} chains, + * which are applied in reverse order *) +lemma map_of_rev: + "distinct (map fst binds) \ + map_of (rev binds) = map_of binds" + apply (subgoal_tac "distinct (map fst (rev binds))") + apply (rule ext) + apply (induct binds) + apply simp + apply (force simp: map_add_def split: option.splits) + apply (metis distinct_rev rev_map) + done + +lemma list_all_dest: + "list_all P [(x, y)] \ P (x, y)" + "list_all P ((x, y) # z # xs) \ (P (x, y) \ list_all P (z # xs))" + by auto + +(* Tail-recursive list conversion. + * FIXME: unused; we currently use the default simp rules with manual convs *) +experiment begin +primrec lookup_tree_to_map_append where + "lookup_tree_to_map_append Leaf xs = xs" +| "lookup_tree_to_map_append (Node k v lt rt) xs = + lookup_tree_to_map_append lt ((k, v) # lookup_tree_to_map_append rt xs)" + +lemma lookup_tree_to_map_append: + "lookup_tree_to_map tree @ xs = lookup_tree_to_map_append tree xs" + apply (induct tree arbitrary: xs; fastforce) + done + +lemma lookup_tree_to_map_eval: + "lookup_tree_to_map tree = lookup_tree_to_map_append tree []" + by (simp add: lookup_tree_to_map_append[symmetric]) +end + +(* Install lookup rules that don't depend on if_cong/if_weak_cong setup *) +lemma lookup_tree_simps'[simp]: + "lookup_tree Leaf fn x = None" + "fn x = fn y \ lookup_tree (Node y v l r) fn x = Some v" + "fn x < fn y \ lookup_tree (Node y v l r) fn x = lookup_tree l fn x" + "fn x > fn y \ lookup_tree (Node y v l r) fn x = lookup_tree r fn x" + by auto +declare lookup_tree.simps[simp del] + +ML \ +structure FastMap = struct + +(* utils *) +fun mk_optionT typ = Type ("Option.option", [typ]) +fun dest_optionT (Type ("Option.option", [typ])) = typ + | dest_optionT t = raise TYPE ("dest_optionT", [t], []) + +val lhs_conv = Conv.fun_conv o Conv.arg_conv +val rhs_conv = Conv.arg_conv +(* first order rewr_conv *) +fun fo_rewr_conv rule ct = let + val (pure_eq, eqn) = + ((true, Thm.instantiate (Thm.first_order_match (Thm.lhs_of rule, ct)) rule) + handle TERM _ => + (false, Thm.instantiate (Thm.first_order_match (fst (Thm.dest_binop (Thm.dest_arg (Thm.cprop_of rule))), ct)) rule)) + handle Pattern.MATCH => raise CTERM ("fo_rewr_conv", [Thm.cprop_of rule, ct]); + in if pure_eq then eqn else eqn RS @{thm eq_reflection} end; +fun fo_rewrs_conv rules = Conv.first_conv (map fo_rewr_conv rules); + +(* Tree builder code, copied from StaticFun *) + +(* Actually build the tree -- theta (n lg(n)) *) +fun build_tree' _ mk_leaf [] = mk_leaf + | build_tree' mk_node mk_leaf xs = let + val len = length xs + val (ys, zs) = chop (len div 2) xs + in case zs of [] => error "build_tree': impossible" + | ((a, b) :: zs) => mk_node a b (build_tree' mk_node mk_leaf ys) + (build_tree' mk_node mk_leaf zs) + end + +fun build_tree ord xs = case xs of [] => error "build_tree : empty" + | (idx, v) :: _ => let + val idxT = fastype_of idx + val vT = fastype_of v + val treeT = Type (@{type_name Tree}, [idxT, vT]) + val mk_leaf = Const (@{const_name Leaf}, treeT) + val node = Const (@{const_name Node}, + idxT --> vT --> treeT --> treeT --> treeT) + fun mk_node a b l r = node $ a $ b $ l $ r + val lookup = Const (@{const_name lookup_tree}, + treeT --> fastype_of ord --> idxT + --> Type (@{type_name option}, [vT])) + in + lookup $ (build_tree' mk_node mk_leaf xs) $ ord + end + +fun define_partial_map_tree name mappings ord ctxt = let + val tree = build_tree ord mappings + in Local_Theory.define + ((name, NoSyn), ((Thm.def_binding name, []), tree)) ctxt + |> apfst (apsnd snd) + end + +(* Prove key ordering theorems. This lets us issue precise error messages + when the user gives us keys whose ordering cannot be verified. + We will also need these thms to prove the lookup_tree_valid property. *) +fun prove_key_ord_thms tree_name keyT mappings get_key simp_ctxt ctxt = + let + val solver = simp_tac (simp_ctxt ctxt [] []) 1; + in + fst (split_last mappings) ~~ tl mappings + |> map_index (fn (i, ((k1, _), (k2, _))) => let + val prop = Const (@{const_name less}, keyT --> keyT --> HOLogic.boolT) $ + (get_key $ k1) $ (get_key $ k2) + |> HOLogic.mk_Trueprop; + val thm = case try (Goal.prove ctxt [] [] prop) (K solver) of + SOME x => x + | _ => raise TERM (tree_name ^ ": failed to prove less-than ordering for keys #" ^ + string_of_int i ^ ", #" ^ string_of_int (i + 1), + [prop]); + in thm end) + end; + +(* Prove lookup_tree_valid *) +fun prove_tree_valid tree_name mappings kT keyT tree_term get_key simp_ctxt ctxt = let + val key_ord_thms = prove_key_ord_thms tree_name keyT mappings get_key simp_ctxt ctxt; + val treeT = fastype_of tree_term + val valid_resultT = HOLogic.mk_prodT (HOLogic.boolT, mk_optionT (HOLogic.mk_prodT (kT, kT))) + val tree_valid_prop = + HOLogic.mk_Trueprop ( + Const (@{const_name fst}, valid_resultT --> HOLogic.boolT) $ + (Const (@{const_name lookup_tree_valid}, (kT --> keyT) --> treeT --> valid_resultT) $ + get_key $ tree_term)) + val solver = simp_tac (put_simpset HOL_basic_ss ctxt + addsimps (@{thms prod.sel lookup_tree_valid_simps'} @ key_ord_thms)) 1 + in Goal.prove ctxt [] [] tree_valid_prop (K solver) end + +fun solve_simp_tac name ctxt = SUBGOAL (fn (t, i) => + (simp_tac ctxt THEN_ALL_NEW SUBGOAL (fn (t', _) => + raise TERM (name ^ ": unsolved", [t, t']))) i) + +fun convert_tree_to_map kT valT mappings lookup_const tree_def tree_valid_thm simp_ctxt ctxt = let + val lookupT = fastype_of lookup_const + (* map_eq = " = map_of " *) + val bindT = HOLogic.mk_prodT (kT, valT) + val mapping_list = HOLogic.mk_list bindT (map HOLogic.mk_prod mappings) + val map_eq = HOLogic.mk_eq (lookup_const, Const (@{const_name map_of}, HOLogic.listT bindT --> lookupT) $ mapping_list) + (* distinct_pred = "distinct (map fst )" *) + val distinct_pred = + Const (@{const_name distinct}, HOLogic.listT kT --> HOLogic.boolT) $ + (Const (@{const_name map}, (bindT --> kT) --> HOLogic.listT bindT --> HOLogic.listT kT) $ + Const (@{const_name fst}, bindT --> kT) $ + mapping_list) + val convert_prop = HOLogic.mk_Trueprop ( + HOLogic.mk_conj (map_eq, distinct_pred) + ) + fun TIMED desc tac = fn st => Seq.make (K (Timing.timeap_msg ("tactic timing for " ^ desc) (fn () => Seq.pull (tac st)) ())) + + val lookup_tree_to_map_eval = let + (* allow recursive conv in cv2, deferred by function application *) + infix 1 then_conv' + fun (cv1 then_conv' cv2) ct = + let + val eq1 = cv1 ct; + val eq2 = cv2 () (Thm.rhs_of eq1); + in + if Thm.is_reflexive eq1 then eq2 + else if Thm.is_reflexive eq2 then eq1 + else Thm.transitive eq1 eq2 + end; + + fun append_conv () = + fo_rewr_conv @{thm append.simps(1)} else_conv + (fo_rewr_conv @{thm append.simps(2)} then_conv' + (fn () => rhs_conv (append_conv ()))) + fun to_map_conv () = + fo_rewr_conv @{thm lookup_tree_to_map.simps(1)} else_conv + (fo_rewr_conv @{thm lookup_tree_to_map.simps(2)[simplified append.simps]} then_conv' + (fn () => lhs_conv (to_map_conv ())) then_conv' + (fn () => rhs_conv (rhs_conv (to_map_conv ()))) then_conv + append_conv ()) + in to_map_conv () end + + val solver = + TIMED "unfold" (Conv.gconv_rule (Conv.arg_conv (lhs_conv (lhs_conv (K tree_def)))) 1 #> Seq.succeed) THEN + TIMED "main rule" (resolve_tac ctxt @{thms lookup_tree_to_map_of_gen} 1) THEN + TIMED "solve inj" (solve_simp_tac "convert_tree_to_map" (simp_ctxt ctxt @{thms simp_thms} @{thms inj_def}) 1) THEN + TIMED "resolve valid" (resolve_tac ctxt [tree_valid_thm] 1) THEN + TIMED "convert tree" (Conv.gconv_rule (Conv.arg_conv (lhs_conv lookup_tree_to_map_eval)) 1 #> Seq.succeed) THEN + resolve_tac ctxt @{thms refl} 1 + val convert_thm = Goal.prove ctxt [] [] convert_prop (K solver) + in convert_thm end + +(* Obtain domain and range from lookup list *) +fun domain_range_common dom_ran_const xT xs lookup_const tree_map_eqn intro_conv_tac ctxt = let + val lookupT = fastype_of lookup_const + val prop = HOLogic.mk_Trueprop ( + HOLogic.mk_eq ( + Const (dom_ran_const, lookupT --> HOLogic.mk_setT xT) $ lookup_const, + Const (@{const_name set}, HOLogic.listT xT --> HOLogic.mk_setT xT) $ + (HOLogic.mk_list xT xs) + )) + val tree_map_eqn' = tree_map_eqn RS @{thm eq_reflection} + val map_eqns = @{thms list.map prod.sel} + val solver = + (Conv.gconv_rule (Conv.arg_conv (lhs_conv (Conv.arg_conv (K tree_map_eqn')))) 1 #> Seq.succeed) THEN + intro_conv_tac THEN + (Conv.gconv_rule (Conv.arg_conv (lhs_conv ( + Conv.top_conv (K (Conv.try_conv (fo_rewrs_conv map_eqns))) ctxt + ))) 1 #> Seq.succeed) THEN + resolve_tac ctxt @{thms refl} 1 + in Goal.prove ctxt [] [] prop (K solver) end; + +fun tree_domain kT mappings lookup_const tree_map_eqn ctxt = + domain_range_common + @{const_name dom} kT (map fst mappings) lookup_const tree_map_eqn + (* like (subst dom_map_of_conv_list) but faster *) + (resolve_tac ctxt @{thms dom_map_of_conv_list[THEN trans]} 1) + ctxt; + +fun tree_range valT mappings lookup_const tree_map_eqn map_distinct_thm ctxt = + domain_range_common + @{const_name ran} valT (map snd mappings) lookup_const tree_map_eqn + (* like (subst ran_map_of_conv_list) but faster *) + (resolve_tac ctxt @{thms ran_map_of_conv_list[THEN trans]} 1 THEN + resolve_tac ctxt [map_distinct_thm] 1) + ctxt; + +(* Choosing names for the const and its theorems. The constant will be named with + map_name; Local_Theory.define may also add extra names (e.g. _def) *) +type name_opts = { + map_name: string, + tree_valid_thm: string, + tree_map_eqn: string, + keys_distinct_thm: string, + lookup_thms: string, + domain_thm: string, + range_thm: string +}; + +fun name_opts_default (map_name: string): name_opts = { + map_name = map_name, + tree_valid_thm = map_name ^ "_tree_valid", + tree_map_eqn = map_name ^ "_tree_to_map", + keys_distinct_thm = map_name ^ "_keys_distinct", + lookup_thms = map_name ^ "_lookups", + domain_thm = map_name ^ "_domain", + range_thm = map_name ^ "_range" +}; + +(* Top level interface *) +fun define_map + (name_opts: name_opts) + (mappings: (term * term) list) + (get_key: term) (* function to get linorder key, must be injective *) + (extra_simps: thm list) + (minimal_simp: bool) (* true: start with minimal simpset; extra_simps must be adequate *) + ctxt = let + fun simp_ctxt ctxt basic_simps more_simps = if minimal_simp + then put_simpset HOL_basic_ss ctxt addsimps (basic_simps @ extra_simps @ more_simps) + else ctxt addsimps (extra_simps @ more_simps) + + val _ = tracing (#map_name name_opts ^ ": defining tree") + val start = Timing.start () + val ((lookup_const, tree_def), ctxt) = + define_partial_map_tree (Binding.name (#map_name name_opts)) mappings get_key ctxt + val (tree_const, _ $ tree_term $ _) = Logic.dest_equals (Thm.prop_of tree_def) + val (kT, keyT) = dest_funT (fastype_of get_key) + val valT = dest_optionT (snd (dest_funT (fastype_of tree_const))) + val _ = tracing (" done: " ^ Timing.message (Timing.result start)) + + val _ = tracing (#map_name name_opts ^ ": proving tree is well-formed") + val start = Timing.start () + val tree_valid_thm = prove_tree_valid (#map_name name_opts) mappings kT keyT tree_term get_key simp_ctxt ctxt + val (_, ctxt) = ctxt |> Local_Theory.notes + [((Binding.name (#tree_valid_thm name_opts), []), [([tree_valid_thm], [])])] + val _ = tracing (" done: " ^ Timing.message (Timing.result start)) + + val _ = tracing (#map_name name_opts ^ ": converting tree to map") + val start = Timing.start () + val convert_thm = + convert_tree_to_map kT valT mappings lookup_const tree_def tree_valid_thm simp_ctxt ctxt + val [tree_map_eqn, map_distinct_thm] = HOLogic.conj_elims ctxt convert_thm + val _ = tracing (" done: " ^ Timing.message (Timing.result start)) + val _ = tracing (#map_name name_opts ^ ": storing map and distinctness theorems") + val start = Timing.start () + val (_, ctxt) = ctxt |> Local_Theory.notes + [((Binding.name (#tree_map_eqn name_opts), []), [([tree_map_eqn], [])]), + ((Binding.name (#keys_distinct_thm name_opts), []), [([map_distinct_thm], [])])] + val _ = tracing (" done: " ^ Timing.message (Timing.result start)) + + val _ = tracing (#map_name name_opts ^ ": obtaining lookup rules") + val start = Timing.start () + val combined_lookup_thm = + (convert_thm RS @{thm map_of_lookups}) + |> Conv.fconv_rule (Conv.top_conv (K (Conv.try_conv (fo_rewrs_conv @{thms list_all_dest}))) ctxt) + val _ = tracing (" splitting... " ^ Timing.message (Timing.result start)) + val lookup_thms = HOLogic.conj_elims ctxt combined_lookup_thm + |> map (Conv.fconv_rule (Conv.arg_conv (Conv.rewr_conv @{thm prod.case[THEN eq_reflection]}))) + + val _ = if length lookup_thms = length mappings then () else + raise THM ("wrong number of lookup thms: " ^ string_of_int (length lookup_thms) ^ + " instead of " ^ string_of_int (length mappings), 0, + lookup_thms) + val (_, ctxt) = ctxt |> Local_Theory.notes + [((Binding.name (#lookup_thms name_opts), []), [(lookup_thms, [])])] + val _ = tracing (" done: " ^ Timing.message (Timing.result start)) + + (* domain and range *) + val _ = tracing (#map_name name_opts ^ ": getting domain and range") + val start = Timing.start () + val domain_thm = timeap_msg " calculate domain" + (tree_domain kT mappings lookup_const tree_map_eqn) ctxt + val range_thm = timeap_msg " calculate range" + (tree_range valT mappings lookup_const tree_map_eqn map_distinct_thm) ctxt + val (_, ctxt) = ctxt |> Local_Theory.notes + [((Binding.name (#domain_thm name_opts), []), [([domain_thm], [])]), + ((Binding.name (#range_thm name_opts), []), [([range_thm], [])])] + val _ = tracing (" done: " ^ Timing.message (Timing.result start)) + in ctxt end + +end +\ + +end_qualify + +end \ No newline at end of file diff --git a/lib/FastMap_Test.thy b/lib/FastMap_Test.thy new file mode 100644 index 000000000..209b1cf66 --- /dev/null +++ b/lib/FastMap_Test.thy @@ -0,0 +1,437 @@ +(* + * Copyright 2018, Data61 + * Commonwealth Scientific and Industrial Research Organisation (CSIRO) + * ABN 41 687 119 230. + * + * This software may be distributed and modified according to the terms of + * the BSD 2-Clause license. Note that NO WARRANTY is provided. + * See "LICENSE_BSD2.txt" for details. + * + * @TAG(DATA61_BSD) + *) + +theory FastMap_Test +imports + Lib.FastMap + Lib.LexordList + Lib.NICTATools + Lib.Qualify +begin + +section \Basic usage example\ + +experiment begin + local_setup \ + FastMap.define_map + (* The name of the map constant and names of associated theorems. + * This function constructs a set of sensible default names, but + * you can also choose different names manually. *) + (FastMap.name_opts_default "simple_test_map") + + (* List of the actual mappings. These must be sorted by key + * and the key type must admit a linear order. *) + [(@{term "0 :: nat"}, @{term "0 :: nat"}), + (@{term "1 :: nat"}, @{term "1 :: nat"}), + (@{term "2 :: nat"}, @{term "1 :: nat"}), + (@{term "3 :: nat"}, @{term "2 :: nat"}), + (@{term "4 :: nat"}, @{term "3 :: nat"}), + (@{term "5 :: nat"}, @{term "5 :: nat"})] + + (* Key transformer. Must be an injective function that maps the + * key type to a linorder type. This will usually be id, unless + * the key type isn't naturally linorder. See string_map below + * for an example of a non-trivial key transform. *) + @{term "id :: nat \ nat"} + + (* Extra simp rules to use when verifying the key ordering. *) + @{thms} + + (* Use the default background simpset for solving goals. + * Set to true if you want precise control over the simpset. *) + false + \ + thm simple_test_map_def + + text \Default theorem names are generated based on the map name\ + thm simple_test_map_tree_to_map + thm simple_test_map_lookups + thm simple_test_map_domain simple_test_map_range simple_test_map_keys_distinct + + + subsection \Check the generated theorems\ + lemma "simple_test_map = map_of [(0, 0), (1, 1), (2, 1), (3, 2), (4, 3), (5, 5)]" + by (rule simple_test_map_tree_to_map) + + lemma + "simple_test_map 0 = Some 0" + "simple_test_map 1 = Some 1" + "simple_test_map 2 = Some 1" + "simple_test_map 3 = Some 2" + "simple_test_map 4 = Some 3" + "simple_test_map 5 = Some 5" + by (rule simple_test_map_lookups)+ + + lemma + "dom simple_test_map = set [0, 1, 2, 3, 4, 5]" + by (rule simple_test_map_domain) + + text \Note that the range is not simplified\ + lemma + "ran simple_test_map = set [0, 1, 1, 2, 3, 5]" + by (rule simple_test_map_range) + + lemma + "distinct ([0, 1, 2, 3, 4, 5] :: nat list)" + by (rule simple_test_map_keys_distinct[simplified list.map prod.sel]) + +end + + +section \Basic tests for the generated theorems\ + +ML \ +fun create_int_map name n typ ctxt = + FastMap.define_map (FastMap.name_opts_default name) + (List.tabulate (n, fn i => (HOLogic.mk_number typ i, + HOLogic.mk_string (string_of_int i)))) + (Const (@{const_name id}, typ --> typ)) + @{thms} + false + ctxt +\ + +experiment begin + local_setup \ + create_int_map "simple_test_map_100" 100 @{typ int} + \ + print_theorems + + text \Direct lookup theorems\ + lemma "simple_test_map_100 42 = Some ''42''" + by (rule simple_test_map_100_lookups) + + text \We try to configure the default simpset for fast lookups\ + lemma "simple_test_map_100 100 = None" + by (time_methods + default: + \simp add: simple_test_map_100_def\ + minimal: + \simp only: simple_test_map_100_def FastMap.lookup_tree_simps' + id_apply rel_simps if_False + cong: if_weak_cong\ + slow_simps: + \simp add: simple_test_map_100_def FastMap.lookup_tree.simps + del: FastMap.lookup_tree_simps' + cong: if_weak_cong cong del: if_cong\ + slow_simps_l4v: + \simp add: simple_test_map_100_def FastMap.lookup_tree.simps + del: FastMap.lookup_tree_simps' + cong: if_cong cong del: if_weak_cong\ + (* This simulates using a functional map instead of FastMap *) + fun_map: + \simp add: simple_test_map_100_tree_to_map\) + + text \Domain and range theorems\ + lemma "dom simple_test_map_100 = {0 .. 99}" + apply (simp add: atLeastAtMost_upto upto_rec1) + by (simp only: simple_test_map_100_domain set_simps) + + lemma + "ran simple_test_map_100 = + set ([[x] | x \ ''0123456789''] @ [[x, y] | x \ ''123456789'', y \ ''0123456789''])" + apply simp + by (simp only: simple_test_map_100_range set_simps) +end + + + +section \Test with larger mapping\ + +experiment begin + local_setup \ + create_int_map "simple_test_map_1000" 1000 @{typ int} + \ + + lemma "simple_test_map_1000 42 = Some ''42''" + by (rule simple_test_map_1000_lookups) + + lemma "simple_test_map_1000 1000 = None" + by (simp add: simple_test_map_1000_def) + + lemma "dom simple_test_map_1000 = {0 .. 999}" + apply (simp add: atLeastAtMost_upto upto_rec1) + by (simp only: simple_test_map_1000_domain set_simps) + + lemma + "ran simple_test_map_1000 = + set ([[x] | x \ ''0123456789''] @ + [[x, y] | x \ ''123456789'', y \ ''0123456789''] @ + [[x, y, z] | x \ ''123456789'', y \ ''0123456789'', z \ ''0123456789''])" + apply simp + by (simp only: simple_test_map_1000_range set_simps) +end + + + +section \Optimising an existing mapping\ + +experiment begin + local_setup \ + let + val map_def = + fold (fn i => fn m => + @{term "fun_upd :: (int \ string option) \ int \ string option \ (int \ string option)"} $ + m $ HOLogic.mk_number @{typ int} i $ + (@{term "Some :: string \ string option"} $ HOLogic.mk_string (string_of_int i))) + (0 upto 100 - 1) @{term "Map.empty :: int \ string option"}; + val name = Binding.name "slow_map"; + in + Local_Theory.define + ((name, NoSyn), ((Thm.def_binding name, []), map_def)) + #> snd + end + \ + thm slow_map_def + + local_setup \ + create_int_map "fast_map" 100 @{typ int} + \ + + lemma slow_map_alt_def: + "slow_map = fast_map" + unfolding slow_map_def + unfolding fast_map_tree_to_map + apply (simp only: FastMap.map_of_rev[symmetric] fast_map_keys_distinct) + apply (simp only: rev.simps append.simps map_of.simps prod.sel) + done + + lemma "slow_map 42 = Some ''42''" + by (time_methods + fast_map: \simp add: slow_map_alt_def fast_map_def\ + direct_lookup: \simp add: slow_map_alt_def fast_map_lookups\ + slow_map: \simp add: slow_map_def\) + + lemma "slow_map 100 = None" + by (time_methods + fast_map: \simp add: slow_map_alt_def fast_map_def\ + slow_map: \simp add: slow_map_def\) + + lemma "dom slow_map = {0 .. 99}" + supply upto_rec1[simp] + apply (simp add: atLeastAtMost_upto) + (* Domain for slow_map gets generated in reverse order *) + using set_rev[where xs="[0 .. 99] :: int list", simplified] + + by (time_methods + fast_map: \simp add: slow_map_alt_def fast_map_domain\ + slow_map: \simp add: slow_map_def\) +end + + + +section \Simpset tests\ + +definition my_id + where + "my_id x \ x" + +lemma my_id_loop: + "my_id x = my_id (Suc x) - 1" + by (simp add: my_id_def) + +declare my_id_loop[simp] +declare my_id_def[simp] + +text \With our faulty simpset, the key ordering solver gets into a loop.\ +local_setup \ fn ctxt => + (Timeout.apply (Time.fromSeconds 5) ( + FastMap.define_map (FastMap.name_opts_default "minimal_test_map") + (List.tabulate (100, fn i => (HOLogic.mk_number @{typ nat} i, + HOLogic.mk_string (string_of_int i)))) + @{term "my_id :: nat => nat"} + @{thms} + false + ) ctxt; + error "FastMap timeout test: shouldn't get here" + ) + handle Timeout.TIMEOUT _ => ctxt +\ +declare my_id_loop[simp del] +declare my_id_def[simp del] + + +text \The solver for injectivity of the key transformer can also loop.\ +lemma inj_my_id_loop[simp]: + fixes x y :: nat + shows "(my_id x = my_id y) = (my_id (x + x) = my_id (y + y))" + by (auto simp: my_id_def) + +lemma my_id_lessI: + "(my_id x < my_id y) = (x < y)" + by (simp add: my_id_def) + +local_setup \ fn ctxt => + (Timeout.apply (Time.fromSeconds 5) ( + FastMap.define_map (FastMap.name_opts_default "minimal_test_map") + (List.tabulate (100, fn i => (HOLogic.mk_number @{typ nat} i, + HOLogic.mk_string (string_of_int i)))) + @{term "my_id :: nat => nat"} + @{thms my_id_lessI} + false + ) ctxt; + error "FastMap timeout test: shouldn't get here" + ) + handle Timeout.TIMEOUT _ => ctxt +\ + + +text \Manual simpset control.\ +lemma my_id_inj: + "inj my_id" + by (simp add: inj_def my_id_def) + +local_setup \ + FastMap.define_map (FastMap.name_opts_default "minimal_test_map") + (List.tabulate (100, fn i => (HOLogic.mk_number @{typ nat} i, + HOLogic.mk_string (string_of_int i)))) + @{term "my_id :: nat => nat"} + @{thms my_id_lessI rel_simps my_id_inj[THEN inj_eq]} + true +\ + + + +section \Test preserving user input\ + +text \ + Even when using the background simpset, FastMap should never simplify + inside of the supplied keys and values. +\ + +local_setup \ + FastMap.define_map (FastMap.name_opts_default "preserve_input_test_map") + (List.tabulate (100, fn i => (@{term "(+) :: nat \ nat \ nat"} $ + HOLogic.mk_number @{typ nat} i $ + @{term "0 :: nat"}, + @{term "rev :: string \ string"} $ + HOLogic.mk_string (string_of_int i)))) + @{term "id :: nat => nat"} + @{thms} + false +\ + +lemma "preserve_input_test_map (42 + 0) = Some (rev ''42'')" + apply (fails \simp; rule preserve_input_test_map_lookups\) + by (rule preserve_input_test_map_lookups) + +lemma "42 + 0 \ dom preserve_input_test_map" + apply (fails \solves \simp; unfold preserve_input_test_map_domain; intro list.set_intros\\) + by (unfold preserve_input_test_map_domain; intro list.set_intros) + +lemma "rev ''42'' \ ran preserve_input_test_map" + apply (fails \solves \simp; unfold preserve_input_test_map_range; intro list.set_intros\\) + by (unfold preserve_input_test_map_range; intro list.set_intros) + + + +section \Test @{command qualify}\ + +locale qualified_map_test +qualify qualified_map_test + +local_setup \ + create_int_map "qualified_map" 100 @{typ nat} +\ + +end_qualify + +text \Check that unqualified name doesn't exist\ +ML \ + @{assert} (not (can dest_Const @{term qualified_map})); + @{assert} (can dest_Const @{term qualified_map_test.qualified_map}); +\ + + + +section \Test locales\ + +context qualified_map_test begin + +local_setup \ + create_int_map "locale_map" 100 @{typ nat} +\ +thm locale_map_def + +end + +text \Check that unqualified name doesn't exist\ +ML \ + @{assert} (not (can dest_Const @{term locale_map})); + @{assert} (can dest_Const @{term qualified_map_test.locale_map}); +\ + + + +section \Test other key types\ + +subsection \Finite words\ + +experiment begin + local_setup \ + create_int_map "word_map" 256 @{typ word32} + \ + + lemma "word_map 42 = Some ''42''" + by (rule word_map_lookups) + + lemma "word_map 999 = None" + by (simp add: word_map_def) +end + + +subsection \Strings\ + +instantiation char :: ord begin + definition[simp]: "(c::char) < d \ (of_char c :: nat) < of_char d" + definition[simp]: "(c::char) \ d \ (of_char c :: nat) \ of_char d" + instance .. +end + +instantiation char :: linorder begin + instance + by intro_classes + (auto simp: preorder_class.less_le_not_le linorder_class.linear) +end + +experiment begin + text \ + Strings are not naturally in the @{class linorder} class. + However, we can use a key transformer (@{const lexord_list}) + to use strings as @{class linorder} keys. + \ + local_setup \ + FastMap.define_map (FastMap.name_opts_default "string_map") + (List.tabulate (100, fn i => (HOLogic.mk_string (StringCvt.padLeft #"0" 3 (string_of_int i)), + HOLogic.mk_number @{typ nat} i))) + @{term "lexord_list :: string \ char lexord_list"} + @{thms} + false + \ + + lemma "string_map ''042'' = Some 42" + by (rule string_map_lookups) + + lemma "string_map ''0123'' = None" + by (simp add: string_map_def) + + text \ + Notice that the domain and map theorems don't include the key + transformer; it is merely an implementation detail. + \ + schematic_goal "(dom string_map = (?x :: string set))" + by (rule string_map_domain) + schematic_goal "string_map = map_of (?binds :: (string \ nat) list)" + by (rule string_map_tree_to_map) +end + +end \ No newline at end of file diff --git a/lib/ROOT b/lib/ROOT index c930c306c..2c411a6a6 100644 --- a/lib/ROOT +++ b/lib/ROOT @@ -69,6 +69,7 @@ session Lib (lib) = Word_Lib + EquivValid SplitRule DataMap + FastMap Corres_Method Conjuncts DetWPLib @@ -144,6 +145,7 @@ session LibTest (lib) = Refine + Insulin_Test ShowTypes_Test Time_Methods_Cmd_Test + FastMap_Test Trace_Schematic_Insts_Test Local_Method_Tests Qualify_Test