# HG changeset patch
# User blanchet
# Date 1381305198 -7200
# Node ID 957115f3dae4927880945de475c1adac86d95c9c
# Parent  819cd1046922171514ccfbf03223c909548fbd9d
use plain types instead of dedicated type pattern

diff -r 819cd1046922 -r 957115f3dae4 src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Wed Oct 09 09:51:24 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Wed Oct 09 09:53:18 2013 +0200
@@ -43,23 +43,23 @@
 
 (* An abstraction of Isabelle types and first-order terms *)
 datatype pattern = PVar | PApp of string * pattern list
-datatype patternT = PVarT | PAppT of string * patternT list
-datatype ptype = PType of int * patternT list
+datatype ptype = PType of int * typ list
 
 fun string_of_pattern PVar = "_"
   | string_of_pattern (PApp (s, ps)) =
     if null ps then s else s ^ string_of_patterns ps
 and string_of_patterns ps = "(" ^ commas (map string_of_pattern ps) ^ ")"
 
-fun string_of_patternT PVarT = "_"
-  | string_of_patternT (PAppT (s, ps)) =
+fun string_of_patternT (TVar _) = "_"
+  | string_of_patternT (Type (s, ps)) =
     if null ps then s else s ^ string_of_patternsT ps
+  | string_of_patternT (TFree (s, _)) = s
 and string_of_patternsT ps = "(" ^ commas (map string_of_patternT ps) ^ ")"
 fun string_of_ptype (PType (_, ps)) = string_of_patternsT ps
 
 (*Is the second type an instance of the first one?*)
 fun match_pattern (PVar, _) = true
-  | match_pattern (PApp _, PVar) = false
+  | match_pattern (_, PVar) = false
   | match_pattern (PApp (s, ps), PApp (t, qs)) =
     s = t andalso match_patterns (ps, qs)
 and match_patterns (_, []) = true
@@ -68,10 +68,11 @@
     match_pattern (p, q) andalso match_patterns (ps, qs)
 
 (*Is the second type an instance of the first one?*)
-fun match_patternT (PVarT, _) = true
-  | match_patternT (PAppT _, PVarT) = false
-  | match_patternT (PAppT (s, ps), PAppT (t, qs)) =
+fun match_patternT (TVar _, _) = true
+  | match_patternT (Type (s, ps), Type (t, qs)) =
     s = t andalso match_patternsT (ps, qs)
+  | match_patternT (TFree (s, _), TFree (t, _)) = s = t
+  | match_patternT (_, _) = false
 and match_patternsT (_, []) = true
   | match_patternsT ([], _) = false
   | match_patternsT (p :: ps, q :: qs) =
@@ -85,14 +86,9 @@
 fun pconst_hyper_mem f const_tab (s, ps) =
   exists (curry (match_ptype o f) ps) (these (Symtab.lookup const_tab s))
 
-fun patternT_of_type (Type (s, Ts)) = PAppT (s, map patternT_of_type Ts)
-  | patternT_of_type (TFree (s, _)) = PAppT (s, [])
-  | patternT_of_type (TVar _) = PVarT
-
 (* Pairs a constant with the list of its type instantiations. *)
 fun ptype thy const x =
-  (if const then map patternT_of_type (these (try (Sign.const_typargs thy) x))
-   else [])
+  (if const then these (try (Sign.const_typargs thy) x) else [])
 fun rich_ptype thy const (s, T) =
   PType (order_of_type T, ptype thy const (s, T))
 fun rich_pconst thy const (s, T) = (s, rich_ptype thy const (s, T))
@@ -100,9 +96,19 @@
 fun string_of_hyper_pconst (s, ps) =
   s ^ "{" ^ commas (map string_of_ptype ps) ^ "}"
 
-(* Add a pconstant to the table, but a [] entry means a standard
-   connective, which we ignore.*)
-fun add_pconst_to_table (s, p) = Symtab.map_default (s, [p]) (insert (op =) p)
+fun patternT_eq (TVar _, TVar _) = true
+  | patternT_eq (Type (s, Ts), Type (t, Us)) = s = t andalso patternsT_eq (Ts, Us)
+  | patternT_eq (TFree (s, _), TFree (t, _)) = (s = t)
+  | patternT_eq _ = false
+and patternsT_eq ([], []) = true
+  | patternsT_eq ([], _) = false
+  | patternsT_eq (_, []) = false
+  | patternsT_eq (T :: Ts, U :: Us) = patternT_eq (T, U) andalso patternsT_eq (Ts, Us)
+fun ptype_eq (PType (m, Ts), PType (n, Us)) = m = n andalso patternsT_eq (Ts, Us)
+
+ (* Add a pconstant to the table, but a [] entry means a standard connective,
+    which we ignore. *)
+fun add_pconst_to_table (s, p) = Symtab.map_default (s, [p]) (insert ptype_eq p)
 
 (* Set constants tend to pull in too many irrelevant facts. We limit the damage
    by treating them more or less as if they were built-in but add their
@@ -195,11 +201,16 @@
 
 fun patternT_ord p =
   case p of
-    (PVarT, PVarT) => EQUAL
-  | (PVarT, PAppT _) => LESS
-  | (PAppT _, PVarT) => GREATER
-  | (PAppT q1, PAppT q2) =>
+    (TVar _, TVar _) => EQUAL
+  | (TVar _, Type _) => LESS
+  | (TVar _, TFree _) => LESS
+  | (Type _, TVar _) => GREATER
+  | (TFree _, TVar _) => GREATER
+  | (Type q1, Type q2) =>
     prod_ord fast_string_ord (dict_ord patternT_ord) (q1, q2)
+  | (Type _, TFree _) => LESS
+  | (TFree _, Type _) => GREATER
+  | (TFree (s, _), TFree (t, _)) => fast_string_ord (s, t)
 fun ptype_ord (PType p, PType q) =
   prod_ord (dict_ord patternT_ord) int_ord (swap p, swap q)
 
@@ -376,6 +387,8 @@
    facts are included. *)
 val special_fact_index = 45 (* FUDGE *)
 
+fun eq_prod eqx eqy ((x1, y1), (x2, y2)) = eqx (x1, x2) andalso eqy (y1, y2)
+
 val really_hopeless_get_kicked_out_iter = 5 (* FUDGE *)
 
 fun relevance_filter ctxt thres0 decay max_facts is_built_in_const
@@ -437,7 +450,8 @@
               trace_msg ctxt (fn () => "New or updated constants: " ^
                   commas (rel_const_tab'
                           |> Symtab.dest
-                          |> subtract (op =) (rel_const_tab |> Symtab.dest)
+                          |> subtract (eq_prod (op =) (eq_list ptype_eq))
+                                      (rel_const_tab |> Symtab.dest)
                           |> map string_of_hyper_pconst));
               map (fst o fst) accepts @
               (if remaining_max = 0 then