# HG changeset patch # User wenzelm # Date 1630759592 -7200 # Node ID 76ac4dbb0a2203e0c7728e16f74139e80ddc211b # Parent c22e5bdb207d5f84d03d9ad74bcdf453a44b2c0a more scalable operations; diff -r c22e5bdb207d -r 76ac4dbb0a22 src/Pure/Tools/rule_insts.ML --- a/src/Pure/Tools/rule_insts.ML Sat Sep 04 14:18:44 2021 +0200 +++ b/src/Pure/Tools/rule_insts.ML Sat Sep 04 14:46:32 2021 +0200 @@ -52,13 +52,13 @@ fun error_var msg (xi, pos) = error (msg ^ quote (Term.string_of_vname xi) ^ Position.here pos); -fun the_sort tvars (xi, pos) : sort = - (case AList.lookup (op =) tvars xi of +fun the_sort tvars (ai, pos) : sort = + (case Term_Subst.TVars.get_first (fn ((bi, S), ()) => if ai = bi then SOME S else NONE) tvars of SOME S => S - | NONE => error_var "No such type variable in theorem: " (xi, pos)); + | NONE => error_var "No such type variable in theorem: " (ai, pos)); fun the_type vars (xi, pos) : typ = - (case AList.lookup (op =) vars xi of + (case Vartab.lookup vars xi of SOME T => T | NONE => error_var "No such variable in theorem: " (xi, pos)); @@ -71,17 +71,23 @@ else error_var "Bad sort for instantiation of type variable: " (xi, pos) end; -fun make_instT f v = +fun make_instT f (tvars: Term_Subst.TVars.set) = let - val T = TVar v; - val T' = f T; - in if T = T' then NONE else SOME (v, T') end; + fun add v = + let + val T = TVar v; + val T' = f T; + in if T = T' then I else cons (v, T') end; + in Term_Subst.TVars.fold (add o #1) tvars [] end; -fun make_inst f v = +fun make_inst f vars = let - val t = Var v; - val t' = f t; - in if t aconv t' then NONE else SOME (v, t') end; + fun add v = + let + val t = Var v; + val t' = f t; + in if t aconv t' then I else cons (v, t') end; + in fold add vars [] end; fun read_terms ss Ts ctxt = let @@ -109,19 +115,21 @@ val (type_insts, term_insts) = List.partition (fn (((x, _), _), _) => String.isPrefix "'" x) raw_insts; - val tvars = Thm.fold_terms Term.add_tvars thm []; - val vars = Thm.fold_terms Term.add_vars thm []; + val tvars = Thm.fold_terms Term_Subst.add_tvars thm Term_Subst.TVars.empty; + val vars = Thm.fold_terms Term_Subst.add_vars thm Term_Subst.Vars.empty; (*eigen-context*) val (_, ctxt1) = ctxt - |> fold (Variable.declare_internal o Logic.mk_type o TVar) tvars - |> fold (Variable.declare_internal o Var) vars + |> Term_Subst.TVars.fold (Variable.declare_internal o Logic.mk_type o TVar o #1) tvars + |> Term_Subst.Vars.fold (Variable.declare_internal o Var o #1) vars |> Proof_Context.add_fixes_cmd raw_fixes; (*explicit type instantiations*) val instT1 = Term_Subst.instantiateT (Term_Subst.TVars.table (map (read_type ctxt1 tvars) type_insts)); - val vars1 = map (apsnd instT1) vars; + val vars1 = + Term_Subst.Vars.fold (fn ((v, T), ()) => Vartab.insert (K true) (v, instT1 T)) + vars Vartab.empty; (*term instantiations*) val (xs, ss) = split_list term_insts; @@ -130,15 +138,15 @@ (*implicit type instantiations*) val instT2 = Term_Subst.instantiateT (Term_Subst.TVars.table inferred); - val vars2 = map (apsnd instT2) vars1; + val vars2 = Vartab.fold (fn (v, T) => cons (v, instT2 T)) vars1 []; val inst2 = Term_Subst.instantiate (Term_Subst.TVars.empty, fold2 (fn (xi, _) => fn t => Term_Subst.Vars.add ((xi, Term.fastype_of t), t)) xs ts Term_Subst.Vars.empty) #> Envir.beta_norm; - val inst_tvars = map_filter (make_instT (instT2 o instT1)) tvars; - val inst_vars = map_filter (make_inst inst2) vars2; + val inst_tvars = make_instT (instT2 o instT1) tvars; + val inst_vars = make_inst inst2 vars2; in ((inst_tvars, inst_vars), ctxt2) end; end;