better warning, with definitions in right order
authorblanchet
Tue Mar 22 07:57:02 2016 +0100 (2016-03-22)
changeset 626871c4842b32bfb
parent 62686 6e8924f957f6
child 62688 a3cccaef566a
better warning, with definitions in right order
src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML
     1.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Mar 22 07:57:02 2016 +0100
     1.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Mar 22 07:57:02 2016 +0100
     1.3 @@ -2137,19 +2137,18 @@
     1.4  
     1.5      val _ =
     1.6        let
     1.7 -        fun mk_edges Xs ctrXs_Tsss =
     1.8 -          let
     1.9 -            fun add_edges i =
    1.10 -              fold (fn T => fold_index (fn (j, X) =>
    1.11 -                Term.exists_subtype (curry (op =) X) T ? cons (i, j)) Xs);
    1.12 -          in
    1.13 -            fold_index (uncurry (fold o add_edges)) ctrXs_Tsss []
    1.14 -          end;
    1.15 -
    1.16 -        fun mk_graph nn edges =
    1.17 -          Int_Graph.empty
    1.18 -          |> fold (fn kk => Int_Graph.new_node (kk, ())) (0 upto nn - 1)
    1.19 -          |> fold Int_Graph.add_edge edges;
    1.20 +        fun add_deps i =
    1.21 +          fold (fn T => fold_index (fn (j, X) =>
    1.22 +            (i <> j andalso Term.exists_subtype (curry (op =) X) T) ? insert (op =) (i, j)) Xs);
    1.23 +
    1.24 +        val add_missing_nodes = fold (AList.default (op =) o rpair []) (0 upto nn - 1);
    1.25 +
    1.26 +        val deps = fold_index (uncurry (fold o add_deps)) ctrXs_Tsss []
    1.27 +          |> AList.group (op =)
    1.28 +          |> add_missing_nodes;
    1.29 +
    1.30 +        val G = Int_Graph.make (map (apfst (rpair ())) deps);
    1.31 +        val sccs = map (sort int_ord) (Int_Graph.strong_conn G);
    1.32  
    1.33          val str_of_scc = curry (op ^) (co_prefix fp ^ "datatype ") o
    1.34            space_implode " and " o map (suffix " = \<dots>" o Long_Name.base_name);
    1.35 @@ -2159,11 +2158,9 @@
    1.36              warning ("Defined types not fully mutually " ^ co_prefix fp ^ "recursive\n\
    1.37                \Alternative specification:\n" ^
    1.38                cat_lines (map (prefix "  " o str_of_scc o map (nth fp_b_names)) sccs));
    1.39 -
    1.40 -        val edges = mk_edges Xs ctrXs_Tsss;
    1.41 -        val G = mk_graph nn edges;
    1.42 -        val sccs = rev (map (sort int_ord) (Int_Graph.strong_conn G));
    1.43 -      in warn sccs end;
    1.44 +      in
    1.45 +        warn (order_strong_conn (op =) Int_Graph.make Int_Graph.topological_order deps sccs)
    1.46 +      end;
    1.47  
    1.48      val fp_eqs = map dest_TFree Xs ~~ map (Term.typ_subst_atomic (As ~~ unsorted_As)) ctrXs_repTs;
    1.49  
     2.1 --- a/src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML	Tue Mar 22 07:57:02 2016 +0100
     2.2 +++ b/src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML	Tue Mar 22 07:57:02 2016 +0100
     2.3 @@ -34,6 +34,9 @@
     2.4    val finds: ('a * 'b -> bool) -> 'a list -> 'b list -> ('a * 'b list) list * 'b list
     2.5    val find_indices: ('b * 'a -> bool) -> 'a list -> 'b list -> int list
     2.6  
     2.7 +  val order_strong_conn: ('a * 'a -> bool) -> ((('a * unit) * 'a list) list -> 'b) ->
     2.8 +    ('b -> 'a list) -> ('a * 'a list) list -> 'a list list -> 'a list list
     2.9 +
    2.10    val mk_common_name: string list -> string
    2.11  
    2.12    val num_binder_types: typ -> int
    2.13 @@ -102,9 +105,26 @@
    2.14  fun find_indices eq xs ys =
    2.15    map_filter I (map_index (fn (i, y) => if member eq xs y then SOME i else NONE) ys);
    2.16  
    2.17 +fun order_strong_conn eq make_graph topological_order deps sccs =
    2.18 +  let
    2.19 +    val normals = maps (fn x :: xs => map (fn y => (y, x)) xs) sccs;
    2.20 +    fun normal s = AList.lookup eq normals s |> the_default s;
    2.21 +
    2.22 +    val normal_deps = deps
    2.23 +      |> map (fn (x, xs) => let val x' = normal x in
    2.24 +          (x', fold (insert eq o normal) xs [] |> remove eq x')
    2.25 +        end)
    2.26 +      |> AList.group eq
    2.27 +      |> map (apsnd (fn xss => fold (union eq) xss []));
    2.28 +
    2.29 +    val normal_G = make_graph (map (apfst (rpair ())) normal_deps);
    2.30 +    val ordered_normals = rev (topological_order normal_G);
    2.31 +  in
    2.32 +    map (fn x => the (find_first (fn (y :: _) => eq (y, x)) sccs)) ordered_normals
    2.33 +  end;
    2.34 +
    2.35  val mk_common_name = space_implode "_";
    2.36  
    2.37 -(*stolen from ~~/src/HOL/Tools/Nitpick/nitpick_hol.ML*)
    2.38  fun num_binder_types (Type (@{type_name fun}, [_, T])) = 1 + num_binder_types T
    2.39    | num_binder_types _ = 0;
    2.40