# HG changeset patch
# User desharna
# Date 1413904990 -7200
# Node ID 43a3ef574065f5d7dccb9d76bc335dde46a4fa21
# Parent  b3fd0628f84968fcb28c0d08d268c0961ac64abb
warn for not fully mutually (co)recursive types

diff -r b3fd0628f849 -r 43a3ef574065 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Oct 21 17:00:42 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Oct 21 17:23:10 2014 +0200
@@ -1959,6 +1959,36 @@
     val ctrXs_Tsss = map (map (map freeze_fp)) fake_ctr_Tsss;
     val ctrXs_repTs = map mk_sumprodT_balanced ctrXs_Tsss;
 
+    val _ =
+      let
+        fun mk_edges Xs ctrXs_Tsss =
+          let
+            fun add_edges i =
+              fold (fn T => fold_index (fn (j, X) =>
+                exists_subtype (curry (op =) X) T ? cons (i, j)) Xs);
+          in
+            fold_index (uncurry (fold o add_edges)) ctrXs_Tsss []
+          end;
+
+        fun mk_graph nn edges =
+          Int_Graph.empty
+          |> fold (fn kk => Int_Graph.new_node (kk, ())) (0 upto nn - 1)
+          |> fold Int_Graph.add_edge edges;
+
+        val str_of_scc = curry (op ^) (co_prefix fp ^ "datatype ") o
+          space_implode " and " o map (suffix " = \<dots>" o Long_Name.base_name);
+
+        fun warn [_] = ()
+          | warn sccs =
+            warning ("Defined types not fully mutually " ^ co_prefix fp ^ "recursive\n\
+              \Alternative specification:\n" ^
+              cat_lines (map (prefix "  " o str_of_scc o map (nth fp_b_names)) sccs));
+
+        val edges = mk_edges Xs ctrXs_Tsss;
+        val G = mk_graph nn edges;
+        val sccs = rev (map (sort int_ord) (Int_Graph.strong_conn G));
+      in warn sccs end;
+
     val fp_eqs = map dest_TFree Xs ~~ map (Term.typ_subst_atomic (As ~~ unsorted_As)) ctrXs_repTs;
 
     val killed_As =