# HG changeset patch # User wenzelm # Date 1630756166 -7200 # Node ID fdcc7e8f95ea34152854c8ceb9aa808a1b882337 # Parent bf595bfbdc98f38961adb12f6696ef7b26090340 more scalable operations; diff -r bf595bfbdc98 -r fdcc7e8f95ea src/Pure/General/table.ML --- a/src/Pure/General/table.ML Fri Sep 03 19:56:03 2021 +0200 +++ b/src/Pure/General/table.ML Sat Sep 04 13:49:26 2021 +0200 @@ -24,13 +24,14 @@ val map: (key -> 'a -> 'b) -> 'a table -> 'b table val fold: (key * 'b -> 'a -> 'a) -> 'b table -> 'a -> 'a val fold_rev: (key * 'b -> 'a -> 'a) -> 'b table -> 'a -> 'a + val size: 'a table -> int val dest: 'a table -> (key * 'a) list val keys: 'a table -> key list val min: 'a table -> (key * 'a) option val max: 'a table -> (key * 'a) option - val get_first: (key * 'a -> 'b option) -> 'a table -> 'b option val exists: (key * 'a -> bool) -> 'a table -> bool val forall: (key * 'a -> bool) -> 'a table -> bool + val get_first: (key * 'a -> 'b option) -> 'a table -> 'b option val lookup_key: 'a table -> key -> (key * 'a) option val lookup: 'a table -> key -> 'a option val defined: 'a table -> key -> bool @@ -60,6 +61,8 @@ val insert_set: key -> set -> set val remove_set: key -> set -> set val make_set: key list -> set + val subset: set * set -> bool + val eq_set: set * set -> bool end; functor Table(Key: KEY): TABLE = @@ -118,6 +121,7 @@ fold left (f p1 (fold mid (f p2 (fold right x)))); in fold end; +fun size tab = fold_table (fn _ => fn n => n + 1) tab 0; fun dest tab = fold_rev_table cons tab []; fun keys tab = fold_rev_table (cons o #1) tab []; @@ -137,6 +141,20 @@ | max (Branch3 (_, _, _, _, right)) = max right; +(* exists and forall *) + +fun exists pred = + let + fun ex Empty = false + | ex (Branch2 (left, (k, x), right)) = + ex left orelse pred (k, x) orelse ex right + | ex (Branch3 (left, (k1, x1), mid, (k2, x2), right)) = + ex left orelse pred (k1, x1) orelse ex mid orelse pred (k2, x2) orelse ex right; + in ex end; + +fun forall pred = not o exists (not o pred); + + (* get_first *) fun get_first f = @@ -164,9 +182,6 @@ | some => some); in get end; -fun exists pred = is_some o get_first (fn entry => if pred entry then SOME () else NONE); -fun forall pred = not o exists (not o pred); - (* lookup *) @@ -424,7 +439,7 @@ fun merge_list eq = join (fn _ => Library.merge eq); -(* unit tables *) +(* set operations *) type set = unit table; @@ -432,6 +447,9 @@ fun remove_set x : set -> set = delete_safe x; fun make_set entries = fold insert_set entries empty; +fun subset (A: set, B: set) = forall (defined B o #1) A; +fun eq_set (A: set, B: set) = size A = size B andalso subset (A, B); + (* ML pretty-printing *) diff -r bf595bfbdc98 -r fdcc7e8f95ea src/Pure/raw_simplifier.ML --- a/src/Pure/raw_simplifier.ML Fri Sep 03 19:56:03 2021 +0200 +++ b/src/Pure/raw_simplifier.ML Sat Sep 04 13:49:26 2021 +0200 @@ -161,13 +161,13 @@ fun rewrite_rule_extra_vars prems elhs erhs = let val elhss = elhs :: prems; - val tvars = fold Term.add_tvars elhss []; - val vars = fold Term.add_vars elhss []; + val tvars = fold Term_Subst.add_tvars elhss Term_Subst.TVars.empty; + val vars = fold Term_Subst.add_vars elhss Term_Subst.Vars.empty; in erhs |> Term.exists_type (Term.exists_subtype - (fn TVar v => not (member (op =) tvars v) | _ => false)) orelse + (fn TVar v => not (Term_Subst.TVars.defined tvars v) | _ => false)) orelse erhs |> Term.exists_subterm - (fn Var v => not (member (op =) vars v) | _ => false) + (fn Var v => not (Term_Subst.Vars.defined vars v) | _ => false) end; fun rrule_extra_vars elhs thm = @@ -474,6 +474,8 @@ (cond_warning ctxt (fn () => print_thm ctxt "Ignoring duplicate rewrite rule:" ("", thm)); ctxt)); +fun vars_set t = Term_Subst.add_vars t Term_Subst.Vars.empty; + local fun vperm (Var _, Var _) = true @@ -481,8 +483,7 @@ | vperm (t1 $ t2, u1 $ u2) = vperm (t1, u1) andalso vperm (t2, u2) | vperm (t, u) = (t = u); -fun var_perm (t, u) = - vperm (t, u) andalso eq_set (op =) (Term.add_vars t [], Term.add_vars u []); +fun var_perm (t, u) = vperm (t, u) andalso Term_Subst.Vars.eq_set (apply2 vars_set (t, u)); in @@ -945,7 +946,7 @@ while the premises are solved.*) fun cond_skel (args as (_, (lhs, rhs))) = - if subset (op =) (Term.add_vars rhs [], Term.add_vars lhs []) then uncond_skel args + if Term_Subst.Vars.subset (vars_set rhs, vars_set lhs) then uncond_skel args else skel0; (* diff -r bf595bfbdc98 -r fdcc7e8f95ea src/Pure/term_subst.ML --- a/src/Pure/term_subst.ML Fri Sep 03 19:56:03 2021 +0200 +++ b/src/Pure/term_subst.ML Sat Sep 04 13:49:26 2021 +0200 @@ -29,6 +29,15 @@ structure TVars: INST_TABLE structure Frees: INST_TABLE structure Vars: INST_TABLE + val add_tfreesT: typ -> TFrees.set -> TFrees.set + val add_tfrees: term -> TFrees.set -> TFrees.set + val add_tvarsT: typ -> TVars.set -> TVars.set + val add_tvars: term -> TVars.set -> TVars.set + val add_frees: term -> Frees.set -> Frees.set + val add_vars: term -> Vars.set -> Vars.set + val add_tfree_namesT: typ -> Symtab.set -> Symtab.set + val add_tfree_names: term -> Symtab.set -> Symtab.set + val add_free_names: term -> Symtab.set -> Symtab.set val map_atypsT_same: typ Same.operation -> typ Same.operation val map_types_same: typ Same.operation -> term Same.operation val map_aterms_same: term Same.operation -> term Same.operation @@ -77,6 +86,16 @@ val ord = pointer_eq_ord (prod_ord Term_Ord.fast_indexname_ord Term_Ord.typ_ord) ); +val add_tfreesT = fold_atyps (fn TFree v => TFrees.add (v, ()) | _ => I); +val add_tfrees = fold_types add_tfreesT; +val add_tvarsT = fold_atyps (fn TVar v => TVars.add (v, ()) | _ => I); +val add_tvars = fold_types add_tvarsT; +val add_frees = fold_aterms (fn Free v => Frees.add (v, ()) | _ => I); +val add_vars = fold_aterms (fn Var v => Vars.add (v, ()) | _ => I); +val add_tfree_namesT = fold_atyps (fn TFree (a, _) => Symtab.insert_set a | _ => I); +val add_tfree_names = fold_types add_tfree_namesT; +val add_free_names = fold_aterms (fn Free (x, _) => Symtab.insert_set x | _ => I); + (* generic mapping *)