# HG changeset patch # User haftmann # Date 1575547775 0 # Node ID acc6cb1a1a670fb6cc47b32228ff63bcaa470db7 # Parent 9612115e06d12afa219c1c2f9ec230ab67e6b879 proper table data structure diff -r 9612115e06d1 -r acc6cb1a1a67 src/Pure/raw_simplifier.ML --- a/src/Pure/raw_simplifier.ML Thu Dec 05 12:09:33 2019 +0000 +++ b/src/Pure/raw_simplifier.ML Thu Dec 05 12:09:35 2019 +0000 @@ -122,6 +122,8 @@ | cong_name (Free (a, _)) = SOME (false, a) | cong_name _ = NONE; +structure Congtab = Table(type key = cong_name val ord = prod_ord bool_ord fast_string_ord); + (* rewrite rules *) @@ -250,7 +252,7 @@ {rules: rrule Net.net, prems: thm list, depth: int * bool Unsynchronized.ref} * - {congs: (cong_name * thm) list * cong_name list, + {congs: thm Congtab.table * cong_name list, procs: proc Net.net, mk_rews: {mk: Proof.context -> thm -> thm list, @@ -285,8 +287,8 @@ |> map (fn Proc {name, lhs, stamp, ...} => ((name, lhs), stamp)) |> partition_eq (eq_snd op =) |> map (fn ps => (fst (fst (hd ps)), map (snd o fst) ps)), - congs = #1 congs, - weak_congs = #2 congs, + congs = congs |> fst |> Congtab.dest, + weak_congs = congs |> snd, loopers = map fst loop_tacs, unsafe_solvers = map solver_name (#1 solvers), safe_solvers = map solver_name (#2 solvers)}; @@ -296,7 +298,7 @@ fun init_ss depth mk_rews term_ord subgoal_tac solvers = make_simpset ((Net.empty, [], depth), - (([], []), Net.empty, mk_rews, term_ord, subgoal_tac, [], solvers)); + ((Congtab.empty, []), Net.empty, mk_rews, term_ord, subgoal_tac, [], solvers)); fun default_mk_sym _ th = SOME (th RS Drule.symmetric_thm); @@ -326,7 +328,7 @@ val rules' = Net.merge eq_rrule (rules1, rules2); val prems' = Thm.merge_thms (prems1, prems2); val depth' = if #1 depth1 < #1 depth2 then depth2 else depth1; - val congs' = AList.merge (op =) (K true) (congs1, congs2); + val congs' = Congtab.merge (K true) (congs1, congs2); val weak' = merge (op =) (weak1, weak2); val procs' = Net.merge eq_proc (procs1, procs2); val loop_tacs' = AList.merge (op =) (K true) (loop_tacs1, loop_tacs2); @@ -678,7 +680,7 @@ val a = the (cong_name (head_of lhs)) handle Option.Option => raise SIMPLIFIER ("Congruence must start with a constant or free variable", [thm]); val (xs, weak) = congs; - val xs' = AList.update (op =) (a, Thm.trim_context thm) xs; + val xs' = Congtab.update (a, Thm.trim_context thm) xs; val weak' = if is_full_cong thm then weak else a :: weak; in ((xs', weak'), procs, mk_rews, term_ord, subgoal_tac, loop_tacs, solvers) end); @@ -691,8 +693,8 @@ val a = the (cong_name (head_of lhs)) handle Option.Option => raise SIMPLIFIER ("Congruence must start with a constant", [thm]); val (xs, _) = congs; - val xs' = filter_out (fn (x : cong_name, _) => x = a) xs; - val weak' = xs' |> map_filter (fn (a, th) => if is_full_cong th then NONE else SOME a); + val xs' = Congtab.delete_safe a xs; + val weak' = Congtab.fold (fn (a, th) => if is_full_cong th then I else insert (op =) a) xs' []; in ((xs', weak'), procs, mk_rews, term_ord, subgoal_tac, loop_tacs, solvers) end); fun add_cong thm ctxt = add_eqcong (mk_cong ctxt thm) ctxt; @@ -1178,7 +1180,7 @@ in (case cong_name h of SOME a => - (case AList.lookup (op =) (fst congs) a of + (case Congtab.lookup (fst congs) a of NONE => appc () | SOME cong => (*post processing: some partial applications h t1 ... tj, j <= length ts,