src/HOL/Tools/Old_Datatype/old_datatype_aux.ML
author wenzelm
Sat Jul 25 23:41:53 2015 +0200 (2015-07-25)
changeset 60781 2da59cdf531c
parent 60757 c09598a97436
child 67334 51a7c90fbf19
permissions -rw-r--r--
updated to infer_instantiate;
tuned;
blanchet@58112
     1
(*  Title:      HOL/Tools/Old_Datatype/old_datatype_aux.ML
wenzelm@11539
     2
    Author:     Stefan Berghofer, TU Muenchen
berghofe@5177
     3
haftmann@33968
     4
Datatype package: auxiliary data structures and functions.
berghofe@5177
     5
*)
berghofe@5177
     6
blanchet@58112
     7
signature OLD_DATATYPE_COMMON =
haftmann@31737
     8
sig
wenzelm@32964
     9
  type config = {strict : bool, quiet : bool}
haftmann@31737
    10
  val default_config : config
haftmann@31737
    11
  datatype dtyp =
wenzelm@45822
    12
      DtTFree of string * sort
wenzelm@32964
    13
    | DtType of string * dtyp list
wenzelm@32964
    14
    | DtRec of int
wenzelm@32964
    15
  type descr = (int * (string * dtyp list * (string * dtyp list) list)) list
wenzelm@32964
    16
  type info =
wenzelm@32964
    17
   {index : int,
wenzelm@32964
    18
    descr : descr,
wenzelm@32964
    19
    inject : thm list,
wenzelm@32964
    20
    distinct : thm list,
wenzelm@32964
    21
    induct : thm,
wenzelm@32964
    22
    inducts : thm list,
wenzelm@32964
    23
    exhaust : thm,
wenzelm@32964
    24
    nchotomy : thm,
wenzelm@32964
    25
    rec_names : string list,
wenzelm@32964
    26
    rec_rewrites : thm list,
wenzelm@32964
    27
    case_name : string,
wenzelm@32964
    28
    case_rewrites : thm list,
wenzelm@32964
    29
    case_cong : thm,
blanchet@57983
    30
    case_cong_weak : thm,
wenzelm@32964
    31
    split : thm,
wenzelm@32964
    32
    split_asm: thm}
blanchet@58114
    33
  type spec = (binding * (string * sort) list * mixfix) * (binding * typ list * mixfix) list
haftmann@31737
    34
end
haftmann@31737
    35
blanchet@58112
    36
signature OLD_DATATYPE_AUX =
berghofe@5177
    37
sig
blanchet@58112
    38
  include OLD_DATATYPE_COMMON
haftmann@31737
    39
haftmann@31737
    40
  val message : config -> string -> unit
wenzelm@45700
    41
wenzelm@18728
    42
  val store_thmss_atts : string -> string list -> attribute list list -> thm list list
berghofe@18349
    43
    -> theory -> thm list list * theory
haftmann@18314
    44
  val store_thmss : string -> string list -> thm list list -> theory -> thm list list * theory
wenzelm@18728
    45
  val store_thms_atts : string -> string list -> attribute list list -> thm list
haftmann@18314
    46
    -> theory -> thm list * theory
haftmann@18314
    47
  val store_thms : string -> string list -> thm list -> theory -> thm list * theory
berghofe@5177
    48
berghofe@5177
    49
  val split_conj_thm : thm -> thm list
berghofe@5177
    50
  val mk_conj : term list -> term
berghofe@5177
    51
  val mk_disj : term list -> term
berghofe@5177
    52
berghofe@13641
    53
  val app_bnds : term -> int -> term
berghofe@13641
    54
wenzelm@60328
    55
  val ind_tac : Proof.context -> thm -> string list -> int -> tactic
wenzelm@58956
    56
  val exh_tac : Proof.context -> (string -> thm) -> int -> tactic
berghofe@5177
    57
berghofe@7015
    58
  exception Datatype
berghofe@14887
    59
  exception Datatype_Empty of string
berghofe@9740
    60
  val name_of_typ : typ -> string
wenzelm@45839
    61
  val dtyp_of_typ : (string * (string * sort) list) list -> typ -> dtyp
berghofe@5177
    62
  val mk_Free : string -> typ -> int -> term
berghofe@5177
    63
  val is_rec_type : dtyp -> bool
wenzelm@45822
    64
  val typ_of_dtyp : descr -> dtyp -> typ
wenzelm@45822
    65
  val dest_DtTFree : dtyp -> string * sort
berghofe@5177
    66
  val dest_DtRec : dtyp -> int
berghofe@13641
    67
  val strip_dtyp : dtyp -> dtyp list * dtyp
berghofe@13641
    68
  val body_index : dtyp -> int
berghofe@13641
    69
  val mk_fun_dtyp : dtyp list -> dtyp -> dtyp
wenzelm@45822
    70
  val get_nonrec_types : descr -> typ list
wenzelm@45822
    71
  val get_branching_types : descr -> typ list
berghofe@13641
    72
  val get_arities : descr -> int list
wenzelm@45822
    73
  val get_rec_types : descr -> typ list
wenzelm@45822
    74
  val interpret_construction : descr -> (string * sort) list ->
wenzelm@45822
    75
    {atyp: typ -> 'a, dtyp: typ list -> int * bool -> string * typ list -> 'a} ->
wenzelm@45822
    76
    ((string * typ list) * (string * 'a list) list) list
berghofe@13641
    77
  val check_nonempty : descr list -> unit
wenzelm@45822
    78
  val unfold_datatypes : Proof.context -> descr -> info Symtab.table ->
wenzelm@45822
    79
    descr -> int -> descr list * int
haftmann@33968
    80
  val find_shortest_path : descr -> int -> (string * int) option
berghofe@5177
    81
end;
berghofe@5177
    82
blanchet@58112
    83
structure Old_Datatype_Aux : OLD_DATATYPE_AUX =
berghofe@5177
    84
struct
berghofe@5177
    85
haftmann@31668
    86
(* datatype option flags *)
haftmann@31668
    87
wenzelm@32964
    88
type config = {strict : bool, quiet : bool};
wenzelm@32964
    89
val default_config : config = {strict = true, quiet = false};
wenzelm@32964
    90
wenzelm@32964
    91
fun message ({quiet = true, ...} : config) s = writeln s
wenzelm@32964
    92
  | message _ _ = ();
berghofe@5661
    93
wenzelm@8435
    94
berghofe@5177
    95
(* store theorems in theory *)
berghofe@5177
    96
wenzelm@45901
    97
fun store_thmss_atts name tnames attss thmss =
haftmann@18377
    98
  fold_map (fn ((tname, atts), thms) =>
wenzelm@45901
    99
    Global_Theory.note_thmss ""
wenzelm@45901
   100
      [((Binding.qualify true tname (Binding.name name), atts), [(thms, [])])]
wenzelm@52788
   101
    #-> (fn [(_, res)] => pair res)) (tnames ~~ attss ~~ thmss);
berghofe@5177
   102
wenzelm@45901
   103
fun store_thmss name tnames = store_thmss_atts name tnames (replicate (length tnames) []);
berghofe@18101
   104
wenzelm@45901
   105
fun store_thms_atts name tnames attss thms =
wenzelm@45901
   106
  fold_map (fn ((tname, atts), thm) =>
wenzelm@45901
   107
    Global_Theory.note_thmss ""
wenzelm@45901
   108
      [((Binding.qualify true tname (Binding.name name), atts), [([thm], [])])]
wenzelm@52788
   109
    #-> (fn [(_, [res])] => pair res)) (tnames ~~ attss ~~ thms);
wenzelm@8435
   110
wenzelm@45901
   111
fun store_thms name tnames = store_thms_atts name tnames (replicate (length tnames) []);
wenzelm@8435
   112
berghofe@5177
   113
berghofe@5177
   114
(* split theorem thm_1 & ... & thm_n into n theorems *)
berghofe@5177
   115
berghofe@5177
   116
fun split_conj_thm th =
wenzelm@45901
   117
  ((th RS conjunct1) :: split_conj_thm (th RS conjunct2)) handle THM _ => [th];
berghofe@5177
   118
haftmann@38795
   119
val mk_conj = foldr1 (HOLogic.mk_binop @{const_name HOL.conj});
haftmann@38795
   120
val mk_disj = foldr1 (HOLogic.mk_binop @{const_name HOL.disj});
berghofe@5177
   121
berghofe@13641
   122
fun app_bnds t i = list_comb (t, map Bound (i - 1 downto 0));
berghofe@13641
   123
berghofe@13641
   124
berghofe@5177
   125
(* instantiate induction rule *)
berghofe@5177
   126
wenzelm@60328
   127
fun ind_tac ctxt indrule indnames = CSUBGOAL (fn (cgoal, i) =>
berghofe@5177
   128
  let
wenzelm@59582
   129
    val goal = Thm.term_of cgoal;
wenzelm@59582
   130
    val ts = HOLogic.dest_conj (HOLogic.dest_Trueprop (Thm.concl_of indrule));
wenzelm@42368
   131
    val ts' = HOLogic.dest_conj (HOLogic.dest_Trueprop (Logic.strip_imp_concl goal));
wenzelm@42368
   132
    val getP =
wenzelm@42368
   133
      if can HOLogic.dest_imp (hd ts)
wenzelm@42368
   134
      then apfst SOME o HOLogic.dest_imp
wenzelm@42368
   135
      else pair NONE;
wenzelm@42368
   136
    val flt =
wenzelm@42368
   137
      if null indnames then I
wenzelm@45738
   138
      else filter (member (op =) indnames o fst);
wenzelm@42368
   139
    fun abstr (t1, t2) =
wenzelm@42368
   140
      (case t1 of
wenzelm@42368
   141
        NONE =>
wenzelm@45738
   142
          (case flt (Term.add_frees t2 []) of
wenzelm@45738
   143
            [(s, T)] => SOME (absfree (s, T) t2)
berghofe@25676
   144
          | _ => NONE)
wenzelm@45700
   145
      | SOME (_ $ t') => SOME (Abs ("x", fastype_of t', abstract_over (t', t2))));
wenzelm@45700
   146
    val insts =
wenzelm@60328
   147
      (ts ~~ ts') |> map_filter (fn (t, u) =>
wenzelm@45700
   148
        (case abstr (getP u) of
wenzelm@45700
   149
          NONE => NONE
wenzelm@60781
   150
        | SOME u' => SOME (t |> getP |> snd |> head_of |> dest_Var |> #1, Thm.cterm_of ctxt u')));
wenzelm@60781
   151
    val indrule' = infer_instantiate ctxt insts indrule;
wenzelm@60757
   152
  in resolve_tac ctxt [indrule'] i end);
wenzelm@42368
   153
berghofe@5177
   154
berghofe@5177
   155
(* perform exhaustive case analysis on last parameter of subgoal i *)
berghofe@5177
   156
wenzelm@58956
   157
fun exh_tac ctxt exh_thm_of = CSUBGOAL (fn (cgoal, i) =>
berghofe@5177
   158
  let
wenzelm@59582
   159
    val goal = Thm.term_of cgoal;
wenzelm@42368
   160
    val params = Logic.strip_params goal;
berghofe@5177
   161
    val (_, Type (tname, _)) = hd (rev params);
wenzelm@42368
   162
    val exhaustion = Thm.lift_rule cgoal (exh_thm_of tname);
wenzelm@59582
   163
    val prem' = hd (Thm.prems_of exhaustion);
berghofe@5177
   164
    val _ $ (_ $ lhs $ _) = hd (rev (Logic.strip_assums_hyp prem'));
wenzelm@42368
   165
    val exhaustion' =
wenzelm@60781
   166
      infer_instantiate ctxt
wenzelm@60781
   167
        [(#1 (dest_Var (head_of lhs)),
wenzelm@60781
   168
          Thm.cterm_of ctxt (fold_rev (fn (_, T) => fn t => Abs ("z", T, t)) params (Bound 0)))]
wenzelm@59582
   169
        exhaustion;
wenzelm@59582
   170
  in compose_tac ctxt (false, exhaustion', Thm.nprems_of exhaustion) i end);
berghofe@5177
   171
berghofe@7015
   172
berghofe@5177
   173
(********************** Internal description of datatypes *********************)
berghofe@5177
   174
berghofe@5177
   175
datatype dtyp =
wenzelm@45822
   176
    DtTFree of string * sort
wenzelm@45821
   177
  | DtType of string * dtyp list
berghofe@5177
   178
  | DtRec of int;
berghofe@5177
   179
berghofe@5177
   180
(* information about datatypes *)
berghofe@5177
   181
berghofe@16901
   182
(* index, datatype name, type arguments, constructor name, types of constructor's arguments *)
wenzelm@8404
   183
type descr = (int * (string * dtyp list * (string * dtyp list) list)) list;
wenzelm@8404
   184
haftmann@31737
   185
type info =
berghofe@5177
   186
  {index : int,
wenzelm@8404
   187
   descr : descr,
haftmann@32718
   188
   inject : thm list,
haftmann@32900
   189
   distinct : thm list,
haftmann@32727
   190
   induct : thm,
haftmann@32727
   191
   inducts : thm list,
haftmann@32718
   192
   exhaust : thm,
haftmann@32718
   193
   nchotomy : thm,
berghofe@5177
   194
   rec_names : string list,
berghofe@5177
   195
   rec_rewrites : thm list,
berghofe@5177
   196
   case_name : string,
berghofe@5177
   197
   case_rewrites : thm list,
wenzelm@10120
   198
   case_cong : thm,
blanchet@57983
   199
   case_cong_weak : thm,
haftmann@32727
   200
   split : thm,
haftmann@32727
   201
   split_asm: thm};
berghofe@5177
   202
blanchet@58114
   203
type spec = (binding * (string * sort) list * mixfix) * (binding * typ list * mixfix) list;
blanchet@58114
   204
wenzelm@45700
   205
fun mk_Free s T i = Free (s ^ string_of_int i, T);
berghofe@5177
   206
wenzelm@45822
   207
fun subst_DtTFree _ substs (T as DtTFree a) = the_default T (AList.lookup (op =) substs a)
wenzelm@45700
   208
  | subst_DtTFree i substs (DtType (name, ts)) = DtType (name, map (subst_DtTFree i substs) ts)
berghofe@5177
   209
  | subst_DtTFree i _ (DtRec j) = DtRec (i + j);
berghofe@5177
   210
berghofe@7015
   211
exception Datatype;
berghofe@14887
   212
exception Datatype_Empty of string;
berghofe@7015
   213
berghofe@7015
   214
fun dest_DtTFree (DtTFree a) = a
berghofe@7015
   215
  | dest_DtTFree _ = raise Datatype;
berghofe@7015
   216
berghofe@7015
   217
fun dest_DtRec (DtRec i) = i
berghofe@7015
   218
  | dest_DtRec _ = raise Datatype;
berghofe@5177
   219
berghofe@5177
   220
fun is_rec_type (DtType (_, dts)) = exists is_rec_type dts
berghofe@5177
   221
  | is_rec_type (DtRec _) = true
berghofe@5177
   222
  | is_rec_type _ = false;
berghofe@5177
   223
berghofe@13641
   224
fun strip_dtyp (DtType ("fun", [T, U])) = apfst (cons T) (strip_dtyp U)
berghofe@13641
   225
  | strip_dtyp T = ([], T);
berghofe@13641
   226
berghofe@13641
   227
val body_index = dest_DtRec o snd o strip_dtyp;
berghofe@13641
   228
berghofe@13641
   229
fun mk_fun_dtyp [] U = U
berghofe@13641
   230
  | mk_fun_dtyp (T :: Ts) U = DtType ("fun", [T, mk_fun_dtyp Ts U]);
berghofe@13641
   231
berghofe@13707
   232
fun name_of_typ (Type (s, Ts)) =
wenzelm@45700
   233
      let val s' = Long_Name.base_name s in
wenzelm@45700
   234
        space_implode "_"
wenzelm@45700
   235
          (filter_out (equal "") (map name_of_typ Ts) @
wenzelm@50239
   236
            [if Symbol_Pos.is_identifier s' then s' else "x"])
berghofe@13707
   237
      end
berghofe@9740
   238
  | name_of_typ _ = "";
berghofe@9740
   239
wenzelm@45822
   240
fun dtyp_of_typ _ (TFree a) = DtTFree a
berghofe@5177
   241
  | dtyp_of_typ _ (TVar _) = error "Illegal schematic type variable(s)"
berghofe@5177
   242
  | dtyp_of_typ new_dts (Type (tname, Ts)) =
haftmann@17485
   243
      (case AList.lookup (op =) new_dts tname of
wenzelm@45700
   244
        NONE => DtType (tname, map (dtyp_of_typ new_dts) Ts)
wenzelm@45700
   245
      | SOME vs =>
wenzelm@45839
   246
          if map (try dest_TFree) Ts = map SOME vs then
wenzelm@45700
   247
            DtRec (find_index (curry op = tname o fst) new_dts)
wenzelm@45822
   248
          else error ("Illegal occurrence of recursive type " ^ quote tname));
berghofe@5177
   249
wenzelm@45822
   250
fun typ_of_dtyp descr (DtTFree a) = TFree a
wenzelm@45822
   251
  | typ_of_dtyp descr (DtRec i) =
wenzelm@45700
   252
      let val (s, ds, _) = the (AList.lookup (op =) descr i)
wenzelm@45822
   253
      in Type (s, map (typ_of_dtyp descr) ds) end
wenzelm@45822
   254
  | typ_of_dtyp descr (DtType (s, ds)) = Type (s, map (typ_of_dtyp descr) ds);
berghofe@5177
   255
berghofe@5177
   256
(* find all non-recursive types in datatype description *)
berghofe@5177
   257
wenzelm@45822
   258
fun get_nonrec_types descr =
wenzelm@45822
   259
  map (typ_of_dtyp descr) (fold (fn (_, (_, _, constrs)) =>
wenzelm@33244
   260
    fold (fn (_, cargs) => union (op =) (filter_out is_rec_type cargs)) constrs) descr []);
berghofe@5177
   261
berghofe@5177
   262
(* get all recursive types in datatype description *)
berghofe@5177
   263
wenzelm@45822
   264
fun get_rec_types descr = map (fn (_ , (s, ds, _)) =>
wenzelm@45822
   265
  Type (s, map (typ_of_dtyp descr) ds)) descr;
berghofe@5177
   266
berghofe@7015
   267
(* get all branching types *)
berghofe@7015
   268
wenzelm@45822
   269
fun get_branching_types descr =
wenzelm@45822
   270
  map (typ_of_dtyp descr)
wenzelm@45700
   271
    (fold
wenzelm@45700
   272
      (fn (_, (_, _, constrs)) =>
wenzelm@45700
   273
        fold (fn (_, cargs) => fold (strip_dtyp #> fst #> fold (insert op =)) cargs) constrs)
wenzelm@45700
   274
      descr []);
berghofe@13641
   275
wenzelm@45700
   276
fun get_arities descr =
wenzelm@45700
   277
  fold
wenzelm@45700
   278
    (fn (_, (_, _, constrs)) =>
wenzelm@45700
   279
      fold (fn (_, cargs) =>
wenzelm@45700
   280
        fold (insert op =) (map (length o fst o strip_dtyp) (filter is_rec_type cargs))) constrs)
wenzelm@45700
   281
    descr [];
berghofe@7015
   282
haftmann@31605
   283
(* interpret construction of datatype *)
haftmann@31605
   284
wenzelm@45700
   285
fun interpret_construction descr vs {atyp, dtyp} =
haftmann@31605
   286
  let
wenzelm@45822
   287
    val typ_of =
wenzelm@45822
   288
      typ_of_dtyp descr #>
wenzelm@45822
   289
      map_atyps (fn TFree (a, _) => TFree (a, the (AList.lookup (op =) vs a)) | T => T);
wenzelm@45700
   290
    fun interpT dT =
wenzelm@45700
   291
      (case strip_dtyp dT of
wenzelm@45700
   292
        (dTs, DtRec l) =>
haftmann@31605
   293
          let
wenzelm@45700
   294
            val (tyco, dTs', _) = the (AList.lookup (op =) descr l);
wenzelm@45822
   295
            val Ts = map typ_of dTs;
wenzelm@45822
   296
            val Ts' = map typ_of dTs';
haftmann@31605
   297
            val is_proper = forall (can dest_TFree) Ts';
haftmann@31605
   298
          in dtyp Ts (l, is_proper) (tyco, Ts') end
wenzelm@45822
   299
      | _ => atyp (typ_of dT));
haftmann@31605
   300
    fun interpC (c, dTs) = (c, map interpT dTs);
wenzelm@45822
   301
    fun interpD (_, (tyco, dTs, cs)) = ((tyco, map typ_of dTs), map interpC cs);
haftmann@31605
   302
  in map interpD descr end;
haftmann@31605
   303
berghofe@5177
   304
(* nonemptiness check for datatypes *)
berghofe@5177
   305
berghofe@5177
   306
fun check_nonempty descr =
berghofe@5177
   307
  let
wenzelm@32952
   308
    val descr' = flat descr;
berghofe@5177
   309
    fun is_nonempty_dt is i =
berghofe@5177
   310
      let
wenzelm@45700
   311
        val (_, _, constrs) = the (AList.lookup (op =) descr' i);
wenzelm@45700
   312
        fun arg_nonempty (_, DtRec i) =
wenzelm@45700
   313
              if member (op =) is i then false
wenzelm@45700
   314
              else is_nonempty_dt (i :: is) i
berghofe@5177
   315
          | arg_nonempty _ = true;
wenzelm@45700
   316
      in exists (forall (arg_nonempty o strip_dtyp) o snd) constrs end
wenzelm@57884
   317
    val _ = hd descr |> forall (fn (i, (s, _, _)) =>
wenzelm@57884
   318
      is_nonempty_dt [i] i orelse raise Datatype_Empty s)
wenzelm@57884
   319
  in () end;
berghofe@5177
   320
berghofe@5177
   321
(* unfold a list of mutually recursive datatype specifications *)
berghofe@5177
   322
(* all types of the form DtType (dt_name, [..., DtRec _, ...]) *)
berghofe@5177
   323
(* need to be unfolded                                         *)
berghofe@5177
   324
wenzelm@45822
   325
fun unfold_datatypes ctxt orig_descr (dt_info : info Symtab.table) descr i =
berghofe@5177
   326
  let
wenzelm@45700
   327
    fun typ_error T msg =
wenzelm@45700
   328
      error ("Non-admissible type expression\n" ^
wenzelm@45822
   329
        Syntax.string_of_typ ctxt (typ_of_dtyp (orig_descr @ descr) T) ^ "\n" ^ msg);
berghofe@7015
   330
berghofe@7015
   331
    fun get_dt_descr T i tname dts =
wenzelm@17412
   332
      (case Symtab.lookup dt_info tname of
wenzelm@45700
   333
        NONE =>
blanchet@58211
   334
          typ_error T (quote tname ^ " is not registered as an old-style datatype and hence cannot \
blanchet@58211
   335
            \be used in nested recursion")
wenzelm@45700
   336
      | SOME {index, descr, ...} =>
wenzelm@45700
   337
          let
wenzelm@45700
   338
            val (_, vars, _) = the (AList.lookup (op =) descr index);
wenzelm@45743
   339
            val subst = map dest_DtTFree vars ~~ dts
wenzelm@45700
   340
              handle ListPair.UnequalLengths =>
wenzelm@45822
   341
                typ_error T ("Type constructor " ^ quote tname ^
wenzelm@45822
   342
                  " used with wrong number of arguments");
wenzelm@45700
   343
          in
wenzelm@45700
   344
            (i + index,
wenzelm@45700
   345
              map (fn (j, (tn, args, cs)) =>
wenzelm@45700
   346
                (i + j, (tn, map (subst_DtTFree i subst) args,
wenzelm@45700
   347
                  map (apsnd (map (subst_DtTFree i subst))) cs))) descr)
wenzelm@45700
   348
          end);
berghofe@5177
   349
berghofe@5177
   350
    (* unfold a single constructor argument *)
berghofe@5177
   351
wenzelm@33244
   352
    fun unfold_arg T (i, Ts, descrs) =
berghofe@13641
   353
      if is_rec_type T then
wenzelm@45700
   354
        let val (Us, U) = strip_dtyp T in
wenzelm@45700
   355
          if exists is_rec_type Us then
berghofe@13641
   356
            typ_error T "Non-strictly positive recursive occurrence of type"
wenzelm@45700
   357
          else
wenzelm@45700
   358
            (case U of
wenzelm@45700
   359
              DtType (tname, dts) =>
berghofe@13641
   360
                let
berghofe@13641
   361
                  val (index, descr) = get_dt_descr T i tname dts;
wenzelm@45700
   362
                  val (descr', i') =
wenzelm@45822
   363
                    unfold_datatypes ctxt orig_descr dt_info descr (i + length descr);
berghofe@13641
   364
                in (i', Ts @ [mk_fun_dtyp Us (DtRec index)], descrs @ descr') end
berghofe@13641
   365
            | _ => (i, Ts @ [T], descrs))
berghofe@13641
   366
        end
berghofe@13641
   367
      else (i, Ts @ [T], descrs);
berghofe@5177
   368
berghofe@5177
   369
    (* unfold a constructor *)
berghofe@5177
   370
wenzelm@33244
   371
    fun unfold_constr (cname, cargs) (i, constrs, descrs) =
wenzelm@33244
   372
      let val (i', cargs', descrs') = fold unfold_arg cargs (i, [], descrs)
berghofe@5177
   373
      in (i', constrs @ [(cname, cargs')], descrs') end;
berghofe@5177
   374
berghofe@5177
   375
    (* unfold a single datatype *)
berghofe@5177
   376
wenzelm@33244
   377
    fun unfold_datatype (j, (tname, tvars, constrs)) (i, dtypes, descrs) =
wenzelm@33244
   378
      let val (i', constrs', descrs') = fold unfold_constr constrs (i, [], descrs)
wenzelm@33244
   379
      in (i', dtypes @ [(j, (tname, tvars, constrs'))], descrs') end;
berghofe@5177
   380
wenzelm@33244
   381
    val (i', descr', descrs) = fold unfold_datatype descr (i, [], []);
berghofe@5177
   382
berghofe@5177
   383
  in (descr' :: descrs, i') end;
berghofe@5177
   384
haftmann@33968
   385
(* find shortest path to constructor with no recursive arguments *)
haftmann@33968
   386
haftmann@33968
   387
fun find_nonempty descr is i =
haftmann@33968
   388
  let
wenzelm@45700
   389
    fun arg_nonempty (_, DtRec i) =
wenzelm@45700
   390
          if member (op =) is i
haftmann@33968
   391
          then NONE
wenzelm@45700
   392
          else Option.map (Integer.add 1 o snd) (find_nonempty descr (i :: is) i)
haftmann@33968
   393
      | arg_nonempty _ = SOME 0;
haftmann@33971
   394
    fun max_inf (SOME i) (SOME j) = SOME (Integer.max i j)
haftmann@33970
   395
      | max_inf _ _ = NONE;
haftmann@33970
   396
    fun max xs = fold max_inf xs (SOME 0);
haftmann@33970
   397
    val (_, _, constrs) = the (AList.lookup (op =) descr i);
wenzelm@45700
   398
    val xs =
wenzelm@59058
   399
      sort (int_ord o apply2 snd)
wenzelm@45700
   400
        (map_filter (fn (s, dts) => Option.map (pair s)
wenzelm@45700
   401
          (max (map (arg_nonempty o strip_dtyp) dts))) constrs)
haftmann@33970
   402
  in if null xs then NONE else SOME (hd xs) end;
haftmann@33968
   403
haftmann@33968
   404
fun find_shortest_path descr i = find_nonempty descr [i] i;
haftmann@33968
   405
berghofe@5177
   406
end;