simplified names of common datatype types
authorhaftmann
Sun Jun 21 08:38:58 2009 +0200 (2009-06-21)
changeset 31737b3f63611784e
parent 31736 926ebca5a145
child 31738 7b9b9ba532ca
simplified names of common datatype types
src/HOL/Nominal/nominal.ML
src/HOL/Nominal/nominal_atoms.ML
src/HOL/Tools/datatype_package/datatype_abs_proofs.ML
src/HOL/Tools/datatype_package/datatype_aux.ML
src/HOL/Tools/datatype_package/datatype_case.ML
src/HOL/Tools/datatype_package/datatype_codegen.ML
src/HOL/Tools/datatype_package/datatype_realizer.ML
src/HOL/Tools/datatype_package/datatype_rep_proofs.ML
src/HOL/Tools/function_package/size.ML
src/HOL/Tools/old_primrec.ML
src/HOL/Tools/primrec.ML
src/HOL/Tools/quickcheck_generators.ML
src/HOL/Tools/refute.ML
     1.1 --- a/src/HOL/Nominal/nominal.ML	Sun Jun 21 08:38:57 2009 +0200
     1.2 +++ b/src/HOL/Nominal/nominal.ML	Sun Jun 21 08:38:58 2009 +0200
     1.3 @@ -6,7 +6,7 @@
     1.4  
     1.5  signature NOMINAL =
     1.6  sig
     1.7 -  val add_nominal_datatype : DatatypeAux.datatype_config -> string list ->
     1.8 +  val add_nominal_datatype : Datatype.config -> string list ->
     1.9      (string list * bstring * mixfix *
    1.10        (bstring * string list * mixfix) list) list -> theory -> theory
    1.11    type descr
    1.12 @@ -2084,7 +2084,7 @@
    1.13      val names = map (fn ((((NONE, _), t), _), _) => t | ((((SOME t, _), _), _), _) => t) args;
    1.14      val specs = map (fn ((((_, vs), t), mx), cons) =>
    1.15        (vs, t, mx, map (fn ((x, y), z) => (x, y, z)) cons)) args;
    1.16 -  in add_nominal_datatype DatatypeAux.default_datatype_config names specs end;
    1.17 +  in add_nominal_datatype Datatype.default_config names specs end;
    1.18  
    1.19  val _ =
    1.20    OuterSyntax.command "nominal_datatype" "define inductive datatypes" K.thy_decl
     2.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Sun Jun 21 08:38:57 2009 +0200
     2.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Sun Jun 21 08:38:58 2009 +0200
     2.3 @@ -102,7 +102,7 @@
     2.4      fold_map (fn ak => fn thy => 
     2.5            let val dt = ([], Binding.name ak, NoSyn, [(Binding.name ak, [@{typ nat}], NoSyn)])
     2.6                val ({inject,case_thms,...},thy1) = Datatype.add_datatype
     2.7 -                DatatypeAux.default_datatype_config [ak] [dt] thy
     2.8 +                Datatype.default_config [ak] [dt] thy
     2.9                val inject_flat = flat inject
    2.10                val ak_type = Type (Sign.intern_type thy1 ak,[])
    2.11                val ak_sign = Sign.intern_const thy1 ak 
     3.1 --- a/src/HOL/Tools/datatype_package/datatype_abs_proofs.ML	Sun Jun 21 08:38:57 2009 +0200
     3.2 +++ b/src/HOL/Tools/datatype_package/datatype_abs_proofs.ML	Sun Jun 21 08:38:58 2009 +0200
     3.3 @@ -14,24 +14,22 @@
     3.4  
     3.5  signature DATATYPE_ABS_PROOFS =
     3.6  sig
     3.7 -  type datatype_config = DatatypeAux.datatype_config
     3.8 -  type descr = DatatypeAux.descr
     3.9 -  type datatype_info = DatatypeAux.datatype_info
    3.10 -  val prove_casedist_thms : datatype_config -> string list ->
    3.11 +  include DATATYPE_COMMON
    3.12 +  val prove_casedist_thms : config -> string list ->
    3.13      descr list -> (string * sort) list -> thm ->
    3.14      attribute list -> theory -> thm list * theory
    3.15 -  val prove_primrec_thms : datatype_config -> string list ->
    3.16 +  val prove_primrec_thms : config -> string list ->
    3.17      descr list -> (string * sort) list ->
    3.18 -      datatype_info Symtab.table -> thm list list -> thm list list ->
    3.19 +      info Symtab.table -> thm list list -> thm list list ->
    3.20          simpset -> thm -> theory -> (string list * thm list) * theory
    3.21 -  val prove_case_thms : datatype_config -> string list ->
    3.22 +  val prove_case_thms : config -> string list ->
    3.23      descr list -> (string * sort) list ->
    3.24        string list -> thm list -> theory -> (thm list list * string list) * theory
    3.25 -  val prove_split_thms : datatype_config -> string list ->
    3.26 +  val prove_split_thms : config -> string list ->
    3.27      descr list -> (string * sort) list ->
    3.28        thm list list -> thm list list -> thm list -> thm list list -> theory ->
    3.29          (thm * thm) list * theory
    3.30 -  val prove_nchotomys : datatype_config -> string list -> descr list ->
    3.31 +  val prove_nchotomys : config -> string list -> descr list ->
    3.32      (string * sort) list -> thm list -> theory -> thm list * theory
    3.33    val prove_weak_case_congs : string list -> descr list ->
    3.34      (string * sort) list -> theory -> thm list * theory
    3.35 @@ -47,7 +45,7 @@
    3.36  
    3.37  (************************ case distinction theorems ***************************)
    3.38  
    3.39 -fun prove_casedist_thms (config : datatype_config) new_type_names descr sorts induct case_names_exhausts thy =
    3.40 +fun prove_casedist_thms (config : config) new_type_names descr sorts induct case_names_exhausts thy =
    3.41    let
    3.42      val _ = message config "Proving case distinction theorems ...";
    3.43  
    3.44 @@ -89,8 +87,8 @@
    3.45  
    3.46  (*************************** primrec combinators ******************************)
    3.47  
    3.48 -fun prove_primrec_thms (config : datatype_config) new_type_names descr sorts
    3.49 -    (dt_info : datatype_info Symtab.table) constr_inject dist_rewrites dist_ss induct thy =
    3.50 +fun prove_primrec_thms (config : config) new_type_names descr sorts
    3.51 +    (dt_info : info Symtab.table) constr_inject dist_rewrites dist_ss induct thy =
    3.52    let
    3.53      val _ = message config "Constructing primrec combinators ...";
    3.54  
    3.55 @@ -275,7 +273,7 @@
    3.56  
    3.57  (***************************** case combinators *******************************)
    3.58  
    3.59 -fun prove_case_thms (config : datatype_config) new_type_names descr sorts reccomb_names primrec_thms thy =
    3.60 +fun prove_case_thms (config : config) new_type_names descr sorts reccomb_names primrec_thms thy =
    3.61    let
    3.62      val _ = message config "Proving characteristic theorems for case combinators ...";
    3.63  
    3.64 @@ -349,7 +347,7 @@
    3.65  
    3.66  (******************************* case splitting *******************************)
    3.67  
    3.68 -fun prove_split_thms (config : datatype_config) new_type_names descr sorts constr_inject dist_rewrites
    3.69 +fun prove_split_thms (config : config) new_type_names descr sorts constr_inject dist_rewrites
    3.70      casedist_thms case_thms thy =
    3.71    let
    3.72      val _ = message config "Proving equations for case splitting ...";
    3.73 @@ -398,7 +396,7 @@
    3.74  
    3.75  (************************* additional theorems for TFL ************************)
    3.76  
    3.77 -fun prove_nchotomys (config : datatype_config) new_type_names descr sorts casedist_thms thy =
    3.78 +fun prove_nchotomys (config : config) new_type_names descr sorts casedist_thms thy =
    3.79    let
    3.80      val _ = message config "Proving additional theorems for TFL ...";
    3.81  
     4.1 --- a/src/HOL/Tools/datatype_package/datatype_aux.ML	Sun Jun 21 08:38:57 2009 +0200
     4.2 +++ b/src/HOL/Tools/datatype_package/datatype_aux.ML	Sun Jun 21 08:38:58 2009 +0200
     4.3 @@ -4,11 +4,23 @@
     4.4  Auxiliary functions for defining datatypes.
     4.5  *)
     4.6  
     4.7 +signature DATATYPE_COMMON =
     4.8 +sig
     4.9 +  type config
    4.10 +  val default_config : config
    4.11 +  datatype dtyp =
    4.12 +      DtTFree of string
    4.13 +    | DtType of string * (dtyp list)
    4.14 +    | DtRec of int;
    4.15 +  type descr
    4.16 +  type info
    4.17 +end
    4.18 +
    4.19  signature DATATYPE_AUX =
    4.20  sig
    4.21 -  type datatype_config
    4.22 -  val default_datatype_config : datatype_config
    4.23 -  val message : datatype_config -> string -> unit
    4.24 +  include DATATYPE_COMMON
    4.25 +
    4.26 +  val message : config -> string -> unit
    4.27    
    4.28    val add_path : bool -> string -> theory -> theory
    4.29    val parent_path : bool -> theory -> theory
    4.30 @@ -33,12 +45,6 @@
    4.31    datatype simproc_dist = FewConstrs of thm list
    4.32                          | ManyConstrs of thm * simpset;
    4.33  
    4.34 -  datatype dtyp =
    4.35 -      DtTFree of string
    4.36 -    | DtType of string * (dtyp list)
    4.37 -    | DtRec of int;
    4.38 -  type descr
    4.39 -  type datatype_info
    4.40  
    4.41    exception Datatype
    4.42    exception Datatype_Empty of string
    4.43 @@ -61,7 +67,7 @@
    4.44      -> ((string * Term.typ list) * (string * 'a list) list) list
    4.45    val check_nonempty : descr list -> unit
    4.46    val unfold_datatypes : 
    4.47 -    theory -> descr -> (string * sort) list -> datatype_info Symtab.table ->
    4.48 +    theory -> descr -> (string * sort) list -> info Symtab.table ->
    4.49        descr -> int -> descr list * int
    4.50  end;
    4.51  
    4.52 @@ -70,10 +76,10 @@
    4.53  
    4.54  (* datatype option flags *)
    4.55  
    4.56 -type datatype_config = { strict: bool, flat_names: bool, quiet: bool };
    4.57 -val default_datatype_config : datatype_config =
    4.58 +type config = { strict: bool, flat_names: bool, quiet: bool };
    4.59 +val default_config : config =
    4.60    { strict = true, flat_names = false, quiet = false };
    4.61 -fun message ({ quiet, ...} : datatype_config) s =
    4.62 +fun message ({ quiet, ...} : config) s =
    4.63    if quiet then () else writeln s;
    4.64  
    4.65  fun add_path flat_names s = if flat_names then I else Sign.add_path s;
    4.66 @@ -186,7 +192,7 @@
    4.67  (* index, datatype name, type arguments, constructor name, types of constructor's arguments *)
    4.68  type descr = (int * (string * dtyp list * (string * dtyp list) list)) list;
    4.69  
    4.70 -type datatype_info =
    4.71 +type info =
    4.72    {index : int,
    4.73     alt_names : string list option,
    4.74     descr : descr,
    4.75 @@ -317,7 +323,7 @@
    4.76  (* all types of the form DtType (dt_name, [..., DtRec _, ...]) *)
    4.77  (* need to be unfolded                                         *)
    4.78  
    4.79 -fun unfold_datatypes sign orig_descr sorts (dt_info : datatype_info Symtab.table) descr i =
    4.80 +fun unfold_datatypes sign orig_descr sorts (dt_info : info Symtab.table) descr i =
    4.81    let
    4.82      fun typ_error T msg = error ("Non-admissible type expression\n" ^
    4.83        Syntax.string_of_typ_global sign (typ_of_dtyp (orig_descr @ descr) sorts T) ^ "\n" ^ msg);
     5.1 --- a/src/HOL/Tools/datatype_package/datatype_case.ML	Sun Jun 21 08:38:57 2009 +0200
     5.2 +++ b/src/HOL/Tools/datatype_package/datatype_case.ML	Sun Jun 21 08:38:58 2009 +0200
     5.3 @@ -7,16 +7,16 @@
     5.4  
     5.5  signature DATATYPE_CASE =
     5.6  sig
     5.7 -  val make_case: (string -> DatatypeAux.datatype_info option) ->
     5.8 +  val make_case: (string -> DatatypeAux.info option) ->
     5.9      Proof.context -> bool -> string list -> term -> (term * term) list ->
    5.10      term * (term * (int * bool)) list
    5.11 -  val dest_case: (string -> DatatypeAux.datatype_info option) -> bool ->
    5.12 +  val dest_case: (string -> DatatypeAux.info option) -> bool ->
    5.13      string list -> term -> (term * (term * term) list) option
    5.14 -  val strip_case: (string -> DatatypeAux.datatype_info option) -> bool ->
    5.15 +  val strip_case: (string -> DatatypeAux.info option) -> bool ->
    5.16      term -> (term * (term * term) list) option
    5.17 -  val case_tr: bool -> (theory -> string -> DatatypeAux.datatype_info option)
    5.18 +  val case_tr: bool -> (theory -> string -> DatatypeAux.info option)
    5.19      -> Proof.context -> term list -> term
    5.20 -  val case_tr': (theory -> string -> DatatypeAux.datatype_info option) ->
    5.21 +  val case_tr': (theory -> string -> DatatypeAux.info option) ->
    5.22      string -> Proof.context -> term list -> term
    5.23  end;
    5.24  
    5.25 @@ -31,7 +31,7 @@
    5.26   * Get information about datatypes
    5.27   *---------------------------------------------------------------------------*)
    5.28  
    5.29 -fun ty_info (tab : string -> DatatypeAux.datatype_info option) s =
    5.30 +fun ty_info (tab : string -> DatatypeAux.info option) s =
    5.31    case tab s of
    5.32      SOME {descr, case_name, index, sorts, ...} =>
    5.33        let
     6.1 --- a/src/HOL/Tools/datatype_package/datatype_codegen.ML	Sun Jun 21 08:38:57 2009 +0200
     6.2 +++ b/src/HOL/Tools/datatype_package/datatype_codegen.ML	Sun Jun 21 08:38:58 2009 +0200
     6.3 @@ -6,7 +6,7 @@
     6.4  
     6.5  signature DATATYPE_CODEGEN =
     6.6  sig
     6.7 -  val find_shortest_path: DatatypeAux.descr -> int -> (string * int) option
     6.8 +  val find_shortest_path: Datatype.descr -> int -> (string * int) option
     6.9    val mk_eq_eqns: theory -> string -> (thm * bool) list
    6.10    val mk_case_cert: theory -> string -> thm
    6.11    val setup: theory -> theory
    6.12 @@ -17,7 +17,7 @@
    6.13  
    6.14  (** find shortest path to constructor with no recursive arguments **)
    6.15  
    6.16 -fun find_nonempty (descr: DatatypeAux.descr) is i =
    6.17 +fun find_nonempty (descr: Datatype.descr) is i =
    6.18    let
    6.19      val (_, _, constrs) = the (AList.lookup (op =) descr i);
    6.20      fun arg_nonempty (_, DatatypeAux.DtRec i) = if member (op =) is i
    6.21 @@ -42,7 +42,7 @@
    6.22  
    6.23  (* datatype definition *)
    6.24  
    6.25 -fun add_dt_defs thy defs dep module (descr: DatatypeAux.descr) sorts gr =
    6.26 +fun add_dt_defs thy defs dep module (descr: Datatype.descr) sorts gr =
    6.27    let
    6.28      val descr' = List.filter (can (map DatatypeAux.dest_DtTFree o #2 o snd)) descr;
    6.29      val rtnames = map (#1 o snd) (List.filter (fn (_, (_, _, cs)) =>
     7.1 --- a/src/HOL/Tools/datatype_package/datatype_realizer.ML	Sun Jun 21 08:38:57 2009 +0200
     7.2 +++ b/src/HOL/Tools/datatype_package/datatype_realizer.ML	Sun Jun 21 08:38:58 2009 +0200
     7.3 @@ -7,7 +7,7 @@
     7.4  
     7.5  signature DATATYPE_REALIZER =
     7.6  sig
     7.7 -  val add_dt_realizers: DatatypeAux.datatype_config -> string list -> theory -> theory
     7.8 +  val add_dt_realizers: Datatype.config -> string list -> theory -> theory
     7.9    val setup: theory -> theory
    7.10  end;
    7.11  
    7.12 @@ -38,7 +38,7 @@
    7.13  
    7.14  fun mk_realizes T = Const ("realizes", T --> HOLogic.boolT --> HOLogic.boolT);
    7.15  
    7.16 -fun make_ind sorts ({descr, rec_names, rec_rewrites, induction, ...} : datatype_info) is thy =
    7.17 +fun make_ind sorts ({descr, rec_names, rec_rewrites, induction, ...} : info) is thy =
    7.18    let
    7.19      val recTs = get_rec_types descr sorts;
    7.20      val pnames = if length descr = 1 then ["P"]
    7.21 @@ -157,7 +157,7 @@
    7.22    in Extraction.add_realizers_i [(ind_name, (vs, r', prf))] thy' end;
    7.23  
    7.24  
    7.25 -fun make_casedists sorts ({index, descr, case_name, case_rewrites, exhaustion, ...} : datatype_info) thy =
    7.26 +fun make_casedists sorts ({index, descr, case_name, case_rewrites, exhaustion, ...} : info) thy =
    7.27    let
    7.28      val cert = cterm_of thy;
    7.29      val rT = TFree ("'P", HOLogic.typeS);
     8.1 --- a/src/HOL/Tools/datatype_package/datatype_rep_proofs.ML	Sun Jun 21 08:38:57 2009 +0200
     8.2 +++ b/src/HOL/Tools/datatype_package/datatype_rep_proofs.ML	Sun Jun 21 08:38:58 2009 +0200
     8.3 @@ -11,12 +11,10 @@
     8.4  
     8.5  signature DATATYPE_REP_PROOFS =
     8.6  sig
     8.7 -  type datatype_config = DatatypeAux.datatype_config
     8.8 -  type descr = DatatypeAux.descr
     8.9 -  type datatype_info = DatatypeAux.datatype_info
    8.10 +  include DATATYPE_COMMON
    8.11    val distinctness_limit : int Config.T
    8.12    val distinctness_limit_setup : theory -> theory
    8.13 -  val representation_proofs : datatype_config -> datatype_info Symtab.table ->
    8.14 +  val representation_proofs : config -> info Symtab.table ->
    8.15      string list -> descr list -> (string * sort) list ->
    8.16        (binding * mixfix) list -> (binding * mixfix) list list -> attribute
    8.17          -> theory -> (thm list list * thm list list * thm list list *
    8.18 @@ -43,12 +41,12 @@
    8.19  val myinv_f_f = thm "myinv_f_f";
    8.20  
    8.21  
    8.22 -fun exh_thm_of (dt_info : datatype_info Symtab.table) tname =
    8.23 +fun exh_thm_of (dt_info : info Symtab.table) tname =
    8.24    #exhaustion (the (Symtab.lookup dt_info tname));
    8.25  
    8.26  (******************************************************************************)
    8.27  
    8.28 -fun representation_proofs (config : datatype_config) (dt_info : datatype_info Symtab.table)
    8.29 +fun representation_proofs (config : config) (dt_info : info Symtab.table)
    8.30        new_type_names descr sorts types_syntax constr_syntax case_names_induct thy =
    8.31    let
    8.32      val Datatype_thy = ThyInfo.the_theory "Datatype" thy;
     9.1 --- a/src/HOL/Tools/function_package/size.ML	Sun Jun 21 08:38:57 2009 +0200
     9.2 +++ b/src/HOL/Tools/function_package/size.ML	Sun Jun 21 08:38:58 2009 +0200
     9.3 @@ -57,7 +57,7 @@
     9.4  
     9.5  val app = curry (list_comb o swap);
     9.6  
     9.7 -fun prove_size_thms (info : datatype_info) new_type_names thy =
     9.8 +fun prove_size_thms (info : info) new_type_names thy =
     9.9    let
    9.10      val {descr, alt_names, sorts, rec_names, rec_rewrites, induction, ...} = info;
    9.11      val l = length new_type_names;
    10.1 --- a/src/HOL/Tools/old_primrec.ML	Sun Jun 21 08:38:57 2009 +0200
    10.2 +++ b/src/HOL/Tools/old_primrec.ML	Sun Jun 21 08:38:58 2009 +0200
    10.3 @@ -221,7 +221,7 @@
    10.4  
    10.5  (* find datatypes which contain all datatypes in tnames' *)
    10.6  
    10.7 -fun find_dts (dt_info : datatype_info Symtab.table) _ [] = []
    10.8 +fun find_dts (dt_info : info Symtab.table) _ [] = []
    10.9    | find_dts dt_info tnames' (tname::tnames) =
   10.10        (case Symtab.lookup dt_info tname of
   10.11            NONE => primrec_err (quote tname ^ " is not a datatype")
   10.12 @@ -230,7 +230,7 @@
   10.13                (tname, dt)::(find_dts dt_info tnames' tnames)
   10.14              else find_dts dt_info tnames' tnames);
   10.15  
   10.16 -fun prepare_induct ({descr, induction, ...}: datatype_info) rec_eqns =
   10.17 +fun prepare_induct ({descr, induction, ...}: info) rec_eqns =
   10.18    let
   10.19      fun constrs_of (_, (_, _, cs)) =
   10.20        map (fn (cname:string, (_, cargs, _, _, _)) => (cname, map fst cargs)) cs;
    11.1 --- a/src/HOL/Tools/primrec.ML	Sun Jun 21 08:38:57 2009 +0200
    11.2 +++ b/src/HOL/Tools/primrec.ML	Sun Jun 21 08:38:58 2009 +0200
    11.3 @@ -203,7 +203,7 @@
    11.4  
    11.5  (* find datatypes which contain all datatypes in tnames' *)
    11.6  
    11.7 -fun find_dts (dt_info : datatype_info Symtab.table) _ [] = []
    11.8 +fun find_dts (dt_info : info Symtab.table) _ [] = []
    11.9    | find_dts dt_info tnames' (tname::tnames) =
   11.10        (case Symtab.lookup dt_info tname of
   11.11            NONE => primrec_error (quote tname ^ " is not a datatype")
    12.1 --- a/src/HOL/Tools/quickcheck_generators.ML	Sun Jun 21 08:38:57 2009 +0200
    12.2 +++ b/src/HOL/Tools/quickcheck_generators.ML	Sun Jun 21 08:38:58 2009 +0200
    12.3 @@ -12,10 +12,10 @@
    12.4      -> seed -> (('a -> 'b) * (unit -> Term.term)) * seed
    12.5    val ensure_random_typecopy: string -> theory -> theory
    12.6    val random_aux_specification: string -> term list -> local_theory -> local_theory
    12.7 -  val mk_random_aux_eqs: theory -> DatatypeAux.descr -> (string * sort) list
    12.8 +  val mk_random_aux_eqs: theory -> Datatype.descr -> (string * sort) list
    12.9      -> string list -> string list * string list -> typ list * typ list
   12.10      -> string * (term list * (term * term) list)
   12.11 -  val ensure_random_datatype: DatatypeAux.datatype_config -> string list -> theory -> theory
   12.12 +  val ensure_random_datatype: Datatype.config -> string list -> theory -> theory
   12.13    val eval_ref: (unit -> int -> seed -> term list option * seed) option ref
   12.14    val setup: theory -> theory
   12.15  end;
    13.1 --- a/src/HOL/Tools/refute.ML	Sun Jun 21 08:38:57 2009 +0200
    13.2 +++ b/src/HOL/Tools/refute.ML	Sun Jun 21 08:38:58 2009 +0200
    13.3 @@ -73,7 +73,7 @@
    13.4    val specialize_type : theory -> (string * Term.typ) -> Term.term -> Term.term
    13.5    val string_of_typ : Term.typ -> string
    13.6    val typ_of_dtyp :
    13.7 -    DatatypeAux.descr -> (DatatypeAux.dtyp * Term.typ) list -> DatatypeAux.dtyp
    13.8 +    Datatype.descr -> (Datatype.dtyp * Term.typ) list -> Datatype.dtyp
    13.9      -> Term.typ
   13.10  end;  (* signature REFUTE *)
   13.11  
   13.12 @@ -411,15 +411,6 @@
   13.13  (* TRANSLATION HOL -> PROPOSITIONAL LOGIC, BOOLEAN ASSIGNMENT -> MODEL       *)
   13.14  (* ------------------------------------------------------------------------- *)
   13.15  
   13.16 -(* ------------------------------------------------------------------------- *)
   13.17 -(* typ_of_dtyp: converts a data type ('DatatypeAux.dtyp') into a type        *)
   13.18 -(*              ('Term.typ'), given type parameters for the data type's type *)
   13.19 -(*              arguments                                                    *)
   13.20 -(* ------------------------------------------------------------------------- *)
   13.21 -
   13.22 -  (* DatatypeAux.descr -> (DatatypeAux.dtyp * Term.typ) list ->
   13.23 -    DatatypeAux.dtyp -> Term.typ *)
   13.24 -
   13.25    fun typ_of_dtyp descr typ_assoc (DatatypeAux.DtTFree a) =
   13.26      (* replace a 'DtTFree' variable by the associated type *)
   13.27      the (AList.lookup (op =) typ_assoc (DatatypeAux.DtTFree a))
   13.28 @@ -1660,10 +1651,6 @@
   13.29  (*               their arguments) of the size of the argument types          *)
   13.30  (* ------------------------------------------------------------------------- *)
   13.31  
   13.32 -  (* theory -> (Term.typ * int) list -> DatatypeAux.descr ->
   13.33 -    (DatatypeAux.dtyp * Term.typ) list ->
   13.34 -    (string * DatatypeAux.dtyp list) list -> int *)
   13.35 -
   13.36    fun size_of_dtyp thy typ_sizes descr typ_assoc constructors =
   13.37      sum (map (fn (_, dtyps) =>
   13.38        product (map (size_of_type thy (typ_sizes, []) o
   13.39 @@ -2144,7 +2131,6 @@
   13.40                (* decrement depth for the IDT 'T' *)
   13.41                val typs' = (case AList.lookup (op =) typs T of NONE => typs
   13.42                  | SOME n => AList.update (op =) (T, n-1) typs)
   13.43 -              (* Term.term list -> DatatypeAux.dtyp list -> Term.term list *)
   13.44                fun constructor_terms terms [] = terms
   13.45                  | constructor_terms terms (d::ds) =
   13.46                  let
   13.47 @@ -2241,7 +2227,6 @@
   13.48                      else ()
   13.49                    (* returns an interpretation where everything is mapped to *)
   13.50                    (* an "undefined" element of the datatype                  *)
   13.51 -                  (* DatatypeAux.dtyp list -> interpretation *)
   13.52                    fun make_undef [] =
   13.53                      Leaf (replicate total False)
   13.54                      | make_undef (d::ds) =
   13.55 @@ -2253,7 +2238,6 @@
   13.56                        Node (replicate size (make_undef ds))
   13.57                      end
   13.58                    (* returns the interpretation for a constructor *)
   13.59 -                  (* int * DatatypeAux.dtyp list -> int * interpretation *)
   13.60                    fun make_constr (offset, []) =
   13.61                      if offset<total then
   13.62                        (offset+1, Leaf ((replicate offset False) @ True ::
   13.63 @@ -2421,9 +2405,6 @@
   13.64                    (* mutually recursive types must have the same type   *)
   13.65                    (* parameters, unless the mutual recursion comes from *)
   13.66                    (* indirect recursion                                 *)
   13.67 -                  (* (DatatypeAux.dtyp * Term.typ) list ->
   13.68 -                    (DatatypeAux.dtyp * Term.typ) list ->
   13.69 -                    (DatatypeAux.dtyp * Term.typ) list *)
   13.70                    fun rec_typ_assoc acc [] =
   13.71                      acc
   13.72                      | rec_typ_assoc acc ((d, T)::xs) =
   13.73 @@ -2458,7 +2439,6 @@
   13.74                        else
   13.75                          raise REFUTE ("IDT_recursion_interpreter",
   13.76                            "different type associations for the same dtyp"))
   13.77 -                  (* (DatatypeAux.dtyp * Term.typ) list *)
   13.78                    val typ_assoc = filter
   13.79                      (fn (DatatypeAux.DtTFree _, _) => true | (_, _) => false)
   13.80                      (rec_typ_assoc []
   13.81 @@ -2613,7 +2593,6 @@
   13.82                          val rec_dtyps_args  = List.filter
   13.83                            (DatatypeAux.is_rec_type o fst) (dtyps ~~ args)
   13.84                          (* map those indices to interpretations *)
   13.85 -                        (* (DatatypeAux.dtyp * interpretation) list *)
   13.86                          val rec_dtyps_intrs = map (fn (dtyp, arg) =>
   13.87                            let
   13.88                              val dT     = typ_of_dtyp descr typ_assoc dtyp
   13.89 @@ -2625,8 +2604,6 @@
   13.90                          (* takes the dtyp and interpretation of an element, *)
   13.91                          (* and computes the interpretation for the          *)
   13.92                          (* corresponding recursive argument                 *)
   13.93 -                        (* DatatypeAux.dtyp -> interpretation ->
   13.94 -                          interpretation *)
   13.95                          fun rec_intr (DatatypeAux.DtRec i) (Leaf xs) =
   13.96                            (* recursive argument is "rec_i params elem" *)
   13.97                            compute_array_entry i (find_index_eq True xs)
   13.98 @@ -3252,8 +3229,6 @@
   13.99              (* constructor generates the datatype's element that is given by *)
  13.100              (* 'element', returns the constructor (as a term) as well as the *)
  13.101              (* indices of the arguments                                      *)
  13.102 -            (* string * DatatypeAux.dtyp list ->
  13.103 -              (Term.term * int list) option *)
  13.104              fun get_constr_args (cname, cargs) =
  13.105                let
  13.106                  val cTerm      = Const (cname,
  13.107 @@ -3281,7 +3256,6 @@
  13.108                in
  13.109                  Option.map (fn args => (cTerm, cargs, args)) (get_args iC)
  13.110                end
  13.111 -            (* Term.term * DatatypeAux.dtyp list * int list *)
  13.112              val (cTerm, cargs, args) =
  13.113                (* we could speed things up by computing the correct          *)
  13.114                (* constructor directly (rather than testing all              *)