# HG changeset patch
# User blanchet
# Date 1256812897 -3600
# Node ID 5fad8e36dfb1aa42450528b5112f1669bdc074c2
# Parent  75ce0f60617a0f4be248bc1f58c73a4a52ac7c87
fixed error in Nitpick's display of uncurried constants, which resulted in an exception

diff -r 75ce0f60617a -r 5fad8e36dfb1 src/HOL/Tools/Nitpick/HISTORY
--- a/src/HOL/Tools/Nitpick/HISTORY	Thu Oct 29 11:41:11 2009 +0100
+++ b/src/HOL/Tools/Nitpick/HISTORY	Thu Oct 29 11:41:37 2009 +0100
@@ -10,6 +10,7 @@
   * Optimized Kodkod encoding of datatypes whose constructors don't appear in
     the formula to falsify
   * Fixed monotonicity check
+  * Fixed error in display of uncurried constants
 
 Version 1.2.2 (16 Oct 2009)
 
diff -r 75ce0f60617a -r 5fad8e36dfb1 src/HOL/Tools/Nitpick/nitpick_model.ML
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Thu Oct 29 11:41:11 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Thu Oct 29 11:41:37 2009 +0100
@@ -133,12 +133,14 @@
       | aux t = raise TERM ("Nitpick_Model.dest_plain_fun", [t])
   in apsnd (pairself rev) o aux end
 
-(* typ -> term -> term list * term *)
-fun break_in_two (Type ("*", [T1, T2]))
-                 (Const (@{const_name Pair}, _) $ t1 $ t2) =
-    break_in_two T2 t2 |>> cons t1
-  | break_in_two _ (Const (@{const_name Pair}, _) $ t1 $ t2) = ([t1], t2)
-  | break_in_two _ t = raise TERM ("Nitpick_Model.break_in_two", [t])
+(* typ -> typ -> typ -> term -> term * term *)
+fun break_in_two T T1 T2 t =
+  let
+    val ps = HOLogic.flat_tupleT_paths T
+    val cut = length (HOLogic.strip_tupleT T1)
+    val (ps1, ps2) = pairself HOLogic.flat_tupleT_paths (T1, T2)
+    val (ts1, ts2) = t |> HOLogic.strip_ptuple ps |> chop cut
+  in (HOLogic.mk_ptuple ps1 T1 ts1, HOLogic.mk_ptuple ps2 T2 ts2) end
 (* typ -> term -> term -> term *)
 fun pair_up (Type ("*", [T1', T2']))
             (t1 as Const (@{const_name Pair},
@@ -153,12 +155,12 @@
 (* typ -> typ -> typ -> term -> term *)
 fun typecast_fun (Type ("fun", [T1', T2'])) T1 T2 t =
     let
-      (* typ -> typ -> typ -> term -> term *)
-      fun do_curry T1a T1b T2 t =
+      (* typ -> typ -> typ -> typ -> term -> term *)
+      fun do_curry T1 T1a T1b T2 t =
         let
           val (maybe_opt, ps) = dest_plain_fun t
           val ps =
-            ps |>> map (break_in_two T1a #>> mk_flat_tuple T1a)
+            ps |>> map (break_in_two T1 T1a T1b)
                |> uncurry (map2 (fn (t1a, t1b) => fn t2 => (t1a, (t1b, t2))))
                |> AList.coalesce (op =)
                |> map (apsnd (make_plain_fun maybe_opt T1b T2))
@@ -185,7 +187,7 @@
         case factor_out_types T1' T1 of
           ((_, NONE), (_, NONE)) => t |> do_arrow T1' T2' T1 T2
         | ((_, NONE), (T1a, SOME T1b)) =>
-          t |> do_curry T1a T1b T2 |> do_arrow T1' T2' T1a (T1b --> T2)
+          t |> do_curry T1 T1a T1b T2 |> do_arrow T1' T2' T1a (T1b --> T2)
         | ((T1a', SOME T1b'), (_, NONE)) =>
           t |> do_arrow T1a' (T1b' --> T2') T1 T2 |> do_uncurry T1' T2'
         | _ => raise TYPE ("Nitpick_Model.typecast_fun.do_fun", [T1, T1'], [])