# HG changeset patch
# User bulwahn
# Date 1269876653 -7200
# Node ID ea7d0df15be00d7d1c19eb23baae482504e7ed49
# Parent  d82682936c529516cb10f68908633905898b7eff
no specialisation for patterns with only tuples in the predicate compiler

diff -r d82682936c52 -r ea7d0df15be0 src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML	Mon Mar 29 17:30:53 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML	Mon Mar 29 17:30:53 2010 +0200
@@ -45,8 +45,23 @@
     (((pred', intros'), args'), ctxt')
   end
 
-
-
+(* patterns only constructed of variables and pairs/tuples are trivial constructor terms*)
+fun is_nontrivial_constrt thy t =
+  let
+    val cnstrs = flat (maps
+      (map (fn (_, (Tname, _, cs)) => map (apsnd (rpair Tname o length)) cs) o #descr o snd)
+      (Symtab.dest (Datatype.get_all thy)));
+    fun check t = (case strip_comb t of
+        (Var _, []) => (true, true)
+      | (Free _, []) => (true, true)
+      | (Const (@{const_name Pair}, _), ts) =>
+        pairself (forall I) (split_list (map check ts))
+      | (Const (s, T), ts) => (case (AList.lookup (op =) cnstrs s, body_type T) of
+            (SOME (i, Tname), Type (Tname', _)) => (false,
+              length ts = i andalso Tname = Tname' andalso forall (snd o check) ts)
+          | _ => (false, false))
+      | _ => (false, false))
+  in check t = (false, true) end;
 
 fun specialise_intros black_list (pred, intros) pats thy =
   let
@@ -101,7 +116,6 @@
 and find_specialisations black_list specs thy =
   let
     val add_vars = fold_aterms (fn Var v => cons v | _ => I);
-    fun is_nontrivial_constrt thy t = not (is_Var t) andalso (is_constrt thy t)
     fun fresh_free T free_names =
       let
         val free_name = Name.variant free_names "x"