author wenzelm Sat, 04 Sep 2021 14:46:32 +0200 changeset 74566 76ac4dbb0a22 parent 74565 c22e5bdb207d child 74567 d637611b41bd
more scalable operations;
```--- 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;
+      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;
+      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

(*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;```