author blanchet Wed, 11 Jul 2012 21:43:19 +0200 changeset 48247 8f37d2ddabc8 parent 48246 fb11c09d7729 child 48248 b6eb45a52c28
optimized type intersection, hoping this will reduce the number of sudden Interrupts in the "incr_tvar" code
```--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Wed Jul 11 21:43:19 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Wed Jul 11 21:43:19 2012 +0200
@@ -419,7 +419,7 @@
fun atp_schematic_consts_of t = add_schematic_consts_of t Symtab.empty

val tvar_a_str = "'a"
-val tvar_a_z = ((tvar_a_str, 0), HOLogic.typeS)
+val tvar_a_z = ((tvar_a_str, 100 (* arbitrary *)), HOLogic.typeS)
val tvar_a = TVar tvar_a_z
val tvar_a_name = tvar_name tvar_a_z
val itself_name = `make_fixed_type_const @{type_name itself}```
```--- a/src/HOL/Tools/ATP/atp_util.ML	Wed Jul 11 21:43:19 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_util.ML	Wed Jul 11 21:43:19 2012 +0200
@@ -130,9 +130,20 @@

fun type_instance thy T T' = Sign.typ_instance thy (T, T')
fun type_generalization thy T T' = Sign.typ_instance thy (T', T)
-fun type_intersect thy T T' =
-  can (Sign.typ_unify thy (Logic.incr_tvar (maxidx_of_typ T' + 1) T, T'))
-      (Vartab.empty, 0)
+
+fun type_intersect _ (TVar _) _ = true
+  | type_intersect _ _ (TVar _) = true
+  | type_intersect thy T T' =
+    let
+      val tvars = Term.add_tvar_namesT T []
+      val tvars' = Term.add_tvar_namesT T' []
+      val T =
+        if exists (member (op =) tvars') tvars then
+          T |> Logic.incr_tvar (maxidx_of_typ T' + 1)
+        else
+          T
+    in can (Sign.typ_unify thy (T, T')) (Vartab.empty, 0) end
+
val type_equiv = Sign.typ_equiv

fun varify_type ctxt T =```