--- a/src/HOL/Tools/Datatype/datatype_aux.ML Mon Nov 30 11:42:48 2009 +0100
+++ b/src/HOL/Tools/Datatype/datatype_aux.ML Mon Nov 30 11:42:49 2009 +0100
@@ -1,7 +1,7 @@
-(* Title: HOL/Tools/datatype_aux.ML
+(* Title: HOL/Tools/Datatype/datatype_aux.ML
Author: Stefan Berghofer, TU Muenchen
-Auxiliary functions for defining datatypes.
+Datatype package: auxiliary data structures and functions.
*)
signature DATATYPE_COMMON =
@@ -79,9 +79,10 @@
val unfold_datatypes :
theory -> descr -> (string * sort) list -> info Symtab.table ->
descr -> int -> descr list * int
+ val find_shortest_path : descr -> int -> (string * int) option
end;
-structure DatatypeAux : DATATYPE_AUX =
+structure Datatype_Aux : DATATYPE_AUX =
struct
(* datatype option flags *)
@@ -365,4 +366,24 @@
in (descr' :: descrs, i') end;
+(* find shortest path to constructor with no recursive arguments *)
+
+fun find_nonempty descr is i =
+ let
+ val (_, _, constrs) = the (AList.lookup (op =) descr i);
+ fun arg_nonempty (_, DtRec i) = if member (op =) is i
+ then NONE
+ else Option.map (Integer.add 1 o snd) (find_nonempty descr (i::is) i)
+ | arg_nonempty _ = SOME 0;
+ fun max xs = Library.foldl
+ (fn (NONE, _) => NONE
+ | (SOME i, SOME j) => SOME (Int.max (i, j))
+ | (_, NONE) => NONE) (SOME 0, xs);
+ val xs = sort (int_ord o pairself snd)
+ (map_filter (fn (s, dts) => Option.map (pair s)
+ (max (map (arg_nonempty o strip_dtyp) dts))) constrs)
+ in case xs of [] => NONE | x :: _ => SOME x end;
+
+fun find_shortest_path descr i = find_nonempty descr [i] i;
+
end;