# HG changeset patch
# User blanchet
# Date 1458629822 -3600
# Node ID 1c4842b32bfb3251cf9957d73bc4c6426bc6811b
# Parent  6e8924f957f6838ce9ae47fbb5bb0f460dd9925e
better warning, with definitions in right order

diff -r 6e8924f957f6 -r 1c4842b32bfb src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Mar 22 07:57:02 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Mar 22 07:57:02 2016 +0100
@@ -2137,19 +2137,18 @@
 
     val _ =
       let
-        fun mk_edges Xs ctrXs_Tsss =
-          let
-            fun add_edges i =
-              fold (fn T => fold_index (fn (j, X) =>
-                Term.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;
+        fun add_deps i =
+          fold (fn T => fold_index (fn (j, X) =>
+            (i <> j andalso Term.exists_subtype (curry (op =) X) T) ? insert (op =) (i, j)) Xs);
+
+        val add_missing_nodes = fold (AList.default (op =) o rpair []) (0 upto nn - 1);
+
+        val deps = fold_index (uncurry (fold o add_deps)) ctrXs_Tsss []
+          |> AList.group (op =)
+          |> add_missing_nodes;
+
+        val G = Int_Graph.make (map (apfst (rpair ())) deps);
+        val sccs = map (sort int_ord) (Int_Graph.strong_conn G);
 
         val str_of_scc = curry (op ^) (co_prefix fp ^ "datatype ") o
           space_implode " and " o map (suffix " = \<dots>" o Long_Name.base_name);
@@ -2159,11 +2158,9 @@
             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;
+      in
+        warn (order_strong_conn (op =) Int_Graph.make Int_Graph.topological_order deps sccs)
+      end;
 
     val fp_eqs = map dest_TFree Xs ~~ map (Term.typ_subst_atomic (As ~~ unsorted_As)) ctrXs_repTs;
 
diff -r 6e8924f957f6 -r 1c4842b32bfb src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML
--- a/src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML	Tue Mar 22 07:57:02 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML	Tue Mar 22 07:57:02 2016 +0100
@@ -34,6 +34,9 @@
   val finds: ('a * 'b -> bool) -> 'a list -> 'b list -> ('a * 'b list) list * 'b list
   val find_indices: ('b * 'a -> bool) -> 'a list -> 'b list -> int list
 
+  val order_strong_conn: ('a * 'a -> bool) -> ((('a * unit) * 'a list) list -> 'b) ->
+    ('b -> 'a list) -> ('a * 'a list) list -> 'a list list -> 'a list list
+
   val mk_common_name: string list -> string
 
   val num_binder_types: typ -> int
@@ -102,9 +105,26 @@
 fun find_indices eq xs ys =
   map_filter I (map_index (fn (i, y) => if member eq xs y then SOME i else NONE) ys);
 
+fun order_strong_conn eq make_graph topological_order deps sccs =
+  let
+    val normals = maps (fn x :: xs => map (fn y => (y, x)) xs) sccs;
+    fun normal s = AList.lookup eq normals s |> the_default s;
+
+    val normal_deps = deps
+      |> map (fn (x, xs) => let val x' = normal x in
+          (x', fold (insert eq o normal) xs [] |> remove eq x')
+        end)
+      |> AList.group eq
+      |> map (apsnd (fn xss => fold (union eq) xss []));
+
+    val normal_G = make_graph (map (apfst (rpair ())) normal_deps);
+    val ordered_normals = rev (topological_order normal_G);
+  in
+    map (fn x => the (find_first (fn (y :: _) => eq (y, x)) sccs)) ordered_normals
+  end;
+
 val mk_common_name = space_implode "_";
 
-(*stolen from ~~/src/HOL/Tools/Nitpick/nitpick_hol.ML*)
 fun num_binder_types (Type (@{type_name fun}, [_, T])) = 1 + num_binder_types T
   | num_binder_types _ = 0;