src/HOL/Tools/Datatype/datatype_aux.ML
changeset 33968 f94fb13ecbb3
parent 33338 de76079f973a
child 33970 74db95c74f89
     1.1 --- a/src/HOL/Tools/Datatype/datatype_aux.ML	Mon Nov 30 11:42:48 2009 +0100
     1.2 +++ b/src/HOL/Tools/Datatype/datatype_aux.ML	Mon Nov 30 11:42:49 2009 +0100
     1.3 @@ -1,7 +1,7 @@
     1.4 -(*  Title:      HOL/Tools/datatype_aux.ML
     1.5 +(*  Title:      HOL/Tools/Datatype/datatype_aux.ML
     1.6      Author:     Stefan Berghofer, TU Muenchen
     1.7  
     1.8 -Auxiliary functions for defining datatypes.
     1.9 +Datatype package: auxiliary data structures and functions.
    1.10  *)
    1.11  
    1.12  signature DATATYPE_COMMON =
    1.13 @@ -79,9 +79,10 @@
    1.14    val unfold_datatypes : 
    1.15      theory -> descr -> (string * sort) list -> info Symtab.table ->
    1.16        descr -> int -> descr list * int
    1.17 +  val find_shortest_path : descr -> int -> (string * int) option
    1.18  end;
    1.19  
    1.20 -structure DatatypeAux : DATATYPE_AUX =
    1.21 +structure Datatype_Aux : DATATYPE_AUX =
    1.22  struct
    1.23  
    1.24  (* datatype option flags *)
    1.25 @@ -365,4 +366,24 @@
    1.26  
    1.27    in (descr' :: descrs, i') end;
    1.28  
    1.29 +(* find shortest path to constructor with no recursive arguments *)
    1.30 +
    1.31 +fun find_nonempty descr is i =
    1.32 +  let
    1.33 +    val (_, _, constrs) = the (AList.lookup (op =) descr i);
    1.34 +    fun arg_nonempty (_, DtRec i) = if member (op =) is i
    1.35 +          then NONE
    1.36 +          else Option.map (Integer.add 1 o snd) (find_nonempty descr (i::is) i)
    1.37 +      | arg_nonempty _ = SOME 0;
    1.38 +    fun max xs = Library.foldl
    1.39 +      (fn (NONE, _) => NONE
    1.40 +        | (SOME i, SOME j) => SOME (Int.max (i, j))
    1.41 +        | (_, NONE) => NONE) (SOME 0, xs);
    1.42 +    val xs = sort (int_ord o pairself snd)
    1.43 +      (map_filter (fn (s, dts) => Option.map (pair s)
    1.44 +        (max (map (arg_nonempty o strip_dtyp) dts))) constrs)
    1.45 +  in case xs of [] => NONE | x :: _ => SOME x end;
    1.46 +
    1.47 +fun find_shortest_path descr i = find_nonempty descr [i] i;
    1.48 +
    1.49  end;