# HG changeset patch
# User blanchet
# Date 1386246120 -3600
# Node ID 7a14f831d02d35cde346bd7e36efab09f4c0762b
# Parent  da88a625cce1af2d576c8d01a1f57e959645436c
make sure acyclicity axiom gets generated in the case where the problem involves mutually recursive datatypes

diff -r da88a625cce1 -r 7a14f831d02d NEWS
--- a/NEWS	Thu Dec 05 09:23:59 2013 +0100
+++ b/NEWS	Thu Dec 05 13:22:00 2013 +0100
@@ -520,6 +520,10 @@
     sets ~> set
 IMCOMPATIBILITY.
 
+* Nitpick:
+  - Fixed soundness bug whereby mutually recursive datatypes could take
+    infinite values.
+
 
 *** ML ***
 
diff -r da88a625cce1 -r 7a14f831d02d src/HOL/Tools/Nitpick/nitpick_kodkod.ML
--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Thu Dec 05 09:23:59 2013 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Thu Dec 05 13:22:00 2013 +0100
@@ -1545,16 +1545,16 @@
   |> Typ_Graph.strong_conn
   |> map (fn keys => filter (member (op =) keys o fst) nfa)
 
-fun acyclicity_axiom_for_datatype (kk as {kk_no, kk_intersect, ...}) nfa
-                                  start_T =
-  kk_no (kk_intersect
-             (loop_path_rel_expr kk nfa (pull start_T (map fst nfa)) start_T)
-             KK.Iden)
 (* Cycle breaking in the bounds takes care of singly recursive datatypes, hence
    the first equation. *)
-fun acyclicity_axioms_for_datatypes _ [_] = []
-  | acyclicity_axioms_for_datatypes kk nfas =
-    maps (fn nfa => map (acyclicity_axiom_for_datatype kk nfa o fst) nfa) nfas
+fun acyclicity_axioms_for_datatype _ [_] _ = []
+  | acyclicity_axioms_for_datatype (kk as {kk_no, kk_intersect, ...}) nfa
+                                   start_T =
+    [kk_no (kk_intersect
+                (loop_path_rel_expr kk nfa (pull start_T (map fst nfa)) start_T)
+                KK.Iden)]
+fun acyclicity_axioms_for_datatypes kk =
+  maps (fn nfa => maps (acyclicity_axioms_for_datatype kk nfa o fst) nfa)
 
 fun atom_equation_for_nut ofs kk (u, j) =
   let val dummy_u = RelReg (0, type_of u, rep_of u) in