# HG changeset patch # User haftmann # Date 1245566338 -7200 # Node ID b3f63611784ee9fc5c4e5ab812b146b6fd9783cc # Parent 926ebca5a145746255544d43cdcb7046662cd725 simplified names of common datatype types diff -r 926ebca5a145 -r b3f63611784e src/HOL/Nominal/nominal.ML --- a/src/HOL/Nominal/nominal.ML Sun Jun 21 08:38:57 2009 +0200 +++ b/src/HOL/Nominal/nominal.ML Sun Jun 21 08:38:58 2009 +0200 @@ -6,7 +6,7 @@ signature NOMINAL = sig - val add_nominal_datatype : DatatypeAux.datatype_config -> string list -> + val add_nominal_datatype : Datatype.config -> string list -> (string list * bstring * mixfix * (bstring * string list * mixfix) list) list -> theory -> theory type descr @@ -2084,7 +2084,7 @@ val names = map (fn ((((NONE, _), t), _), _) => t | ((((SOME t, _), _), _), _) => t) args; val specs = map (fn ((((_, vs), t), mx), cons) => (vs, t, mx, map (fn ((x, y), z) => (x, y, z)) cons)) args; - in add_nominal_datatype DatatypeAux.default_datatype_config names specs end; + in add_nominal_datatype Datatype.default_config names specs end; val _ = OuterSyntax.command "nominal_datatype" "define inductive datatypes" K.thy_decl diff -r 926ebca5a145 -r b3f63611784e src/HOL/Nominal/nominal_atoms.ML --- a/src/HOL/Nominal/nominal_atoms.ML Sun Jun 21 08:38:57 2009 +0200 +++ b/src/HOL/Nominal/nominal_atoms.ML Sun Jun 21 08:38:58 2009 +0200 @@ -102,7 +102,7 @@ fold_map (fn ak => fn thy => let val dt = ([], Binding.name ak, NoSyn, [(Binding.name ak, [@{typ nat}], NoSyn)]) val ({inject,case_thms,...},thy1) = Datatype.add_datatype - DatatypeAux.default_datatype_config [ak] [dt] thy + Datatype.default_config [ak] [dt] thy val inject_flat = flat inject val ak_type = Type (Sign.intern_type thy1 ak,[]) val ak_sign = Sign.intern_const thy1 ak diff -r 926ebca5a145 -r b3f63611784e src/HOL/Tools/datatype_package/datatype_abs_proofs.ML --- a/src/HOL/Tools/datatype_package/datatype_abs_proofs.ML Sun Jun 21 08:38:57 2009 +0200 +++ b/src/HOL/Tools/datatype_package/datatype_abs_proofs.ML Sun Jun 21 08:38:58 2009 +0200 @@ -14,24 +14,22 @@ signature DATATYPE_ABS_PROOFS = sig - type datatype_config = DatatypeAux.datatype_config - type descr = DatatypeAux.descr - type datatype_info = DatatypeAux.datatype_info - val prove_casedist_thms : datatype_config -> string list -> + include DATATYPE_COMMON + val prove_casedist_thms : config -> string list -> descr list -> (string * sort) list -> thm -> attribute list -> theory -> thm list * theory - val prove_primrec_thms : datatype_config -> string list -> + val prove_primrec_thms : config -> string list -> descr list -> (string * sort) list -> - datatype_info Symtab.table -> thm list list -> thm list list -> + info Symtab.table -> thm list list -> thm list list -> simpset -> thm -> theory -> (string list * thm list) * theory - val prove_case_thms : datatype_config -> string list -> + val prove_case_thms : config -> string list -> descr list -> (string * sort) list -> string list -> thm list -> theory -> (thm list list * string list) * theory - val prove_split_thms : datatype_config -> string list -> + val prove_split_thms : config -> string list -> descr list -> (string * sort) list -> thm list list -> thm list list -> thm list -> thm list list -> theory -> (thm * thm) list * theory - val prove_nchotomys : datatype_config -> string list -> descr list -> + val prove_nchotomys : config -> string list -> descr list -> (string * sort) list -> thm list -> theory -> thm list * theory val prove_weak_case_congs : string list -> descr list -> (string * sort) list -> theory -> thm list * theory @@ -47,7 +45,7 @@ (************************ case distinction theorems ***************************) -fun prove_casedist_thms (config : datatype_config) new_type_names descr sorts induct case_names_exhausts thy = +fun prove_casedist_thms (config : config) new_type_names descr sorts induct case_names_exhausts thy = let val _ = message config "Proving case distinction theorems ..."; @@ -89,8 +87,8 @@ (*************************** primrec combinators ******************************) -fun prove_primrec_thms (config : datatype_config) new_type_names descr sorts - (dt_info : datatype_info Symtab.table) constr_inject dist_rewrites dist_ss induct thy = +fun prove_primrec_thms (config : config) new_type_names descr sorts + (dt_info : info Symtab.table) constr_inject dist_rewrites dist_ss induct thy = let val _ = message config "Constructing primrec combinators ..."; @@ -275,7 +273,7 @@ (***************************** case combinators *******************************) -fun prove_case_thms (config : datatype_config) new_type_names descr sorts reccomb_names primrec_thms thy = +fun prove_case_thms (config : config) new_type_names descr sorts reccomb_names primrec_thms thy = let val _ = message config "Proving characteristic theorems for case combinators ..."; @@ -349,7 +347,7 @@ (******************************* case splitting *******************************) -fun prove_split_thms (config : datatype_config) new_type_names descr sorts constr_inject dist_rewrites +fun prove_split_thms (config : config) new_type_names descr sorts constr_inject dist_rewrites casedist_thms case_thms thy = let val _ = message config "Proving equations for case splitting ..."; @@ -398,7 +396,7 @@ (************************* additional theorems for TFL ************************) -fun prove_nchotomys (config : datatype_config) new_type_names descr sorts casedist_thms thy = +fun prove_nchotomys (config : config) new_type_names descr sorts casedist_thms thy = let val _ = message config "Proving additional theorems for TFL ..."; diff -r 926ebca5a145 -r b3f63611784e src/HOL/Tools/datatype_package/datatype_aux.ML --- a/src/HOL/Tools/datatype_package/datatype_aux.ML Sun Jun 21 08:38:57 2009 +0200 +++ b/src/HOL/Tools/datatype_package/datatype_aux.ML Sun Jun 21 08:38:58 2009 +0200 @@ -4,11 +4,23 @@ Auxiliary functions for defining datatypes. *) +signature DATATYPE_COMMON = +sig + type config + val default_config : config + datatype dtyp = + DtTFree of string + | DtType of string * (dtyp list) + | DtRec of int; + type descr + type info +end + signature DATATYPE_AUX = sig - type datatype_config - val default_datatype_config : datatype_config - val message : datatype_config -> string -> unit + include DATATYPE_COMMON + + val message : config -> string -> unit val add_path : bool -> string -> theory -> theory val parent_path : bool -> theory -> theory @@ -33,12 +45,6 @@ datatype simproc_dist = FewConstrs of thm list | ManyConstrs of thm * simpset; - datatype dtyp = - DtTFree of string - | DtType of string * (dtyp list) - | DtRec of int; - type descr - type datatype_info exception Datatype exception Datatype_Empty of string @@ -61,7 +67,7 @@ -> ((string * Term.typ list) * (string * 'a list) list) list val check_nonempty : descr list -> unit val unfold_datatypes : - theory -> descr -> (string * sort) list -> datatype_info Symtab.table -> + theory -> descr -> (string * sort) list -> info Symtab.table -> descr -> int -> descr list * int end; @@ -70,10 +76,10 @@ (* datatype option flags *) -type datatype_config = { strict: bool, flat_names: bool, quiet: bool }; -val default_datatype_config : datatype_config = +type config = { strict: bool, flat_names: bool, quiet: bool }; +val default_config : config = { strict = true, flat_names = false, quiet = false }; -fun message ({ quiet, ...} : datatype_config) s = +fun message ({ quiet, ...} : config) s = if quiet then () else writeln s; fun add_path flat_names s = if flat_names then I else Sign.add_path s; @@ -186,7 +192,7 @@ (* index, datatype name, type arguments, constructor name, types of constructor's arguments *) type descr = (int * (string * dtyp list * (string * dtyp list) list)) list; -type datatype_info = +type info = {index : int, alt_names : string list option, descr : descr, @@ -317,7 +323,7 @@ (* all types of the form DtType (dt_name, [..., DtRec _, ...]) *) (* need to be unfolded *) -fun unfold_datatypes sign orig_descr sorts (dt_info : datatype_info Symtab.table) descr i = +fun unfold_datatypes sign orig_descr sorts (dt_info : info Symtab.table) descr i = let fun typ_error T msg = error ("Non-admissible type expression\n" ^ Syntax.string_of_typ_global sign (typ_of_dtyp (orig_descr @ descr) sorts T) ^ "\n" ^ msg); diff -r 926ebca5a145 -r b3f63611784e src/HOL/Tools/datatype_package/datatype_case.ML --- a/src/HOL/Tools/datatype_package/datatype_case.ML Sun Jun 21 08:38:57 2009 +0200 +++ b/src/HOL/Tools/datatype_package/datatype_case.ML Sun Jun 21 08:38:58 2009 +0200 @@ -7,16 +7,16 @@ signature DATATYPE_CASE = sig - val make_case: (string -> DatatypeAux.datatype_info option) -> + val make_case: (string -> DatatypeAux.info option) -> Proof.context -> bool -> string list -> term -> (term * term) list -> term * (term * (int * bool)) list - val dest_case: (string -> DatatypeAux.datatype_info option) -> bool -> + val dest_case: (string -> DatatypeAux.info option) -> bool -> string list -> term -> (term * (term * term) list) option - val strip_case: (string -> DatatypeAux.datatype_info option) -> bool -> + val strip_case: (string -> DatatypeAux.info option) -> bool -> term -> (term * (term * term) list) option - val case_tr: bool -> (theory -> string -> DatatypeAux.datatype_info option) + val case_tr: bool -> (theory -> string -> DatatypeAux.info option) -> Proof.context -> term list -> term - val case_tr': (theory -> string -> DatatypeAux.datatype_info option) -> + val case_tr': (theory -> string -> DatatypeAux.info option) -> string -> Proof.context -> term list -> term end; @@ -31,7 +31,7 @@ * Get information about datatypes *---------------------------------------------------------------------------*) -fun ty_info (tab : string -> DatatypeAux.datatype_info option) s = +fun ty_info (tab : string -> DatatypeAux.info option) s = case tab s of SOME {descr, case_name, index, sorts, ...} => let diff -r 926ebca5a145 -r b3f63611784e src/HOL/Tools/datatype_package/datatype_codegen.ML --- a/src/HOL/Tools/datatype_package/datatype_codegen.ML Sun Jun 21 08:38:57 2009 +0200 +++ b/src/HOL/Tools/datatype_package/datatype_codegen.ML Sun Jun 21 08:38:58 2009 +0200 @@ -6,7 +6,7 @@ signature DATATYPE_CODEGEN = sig - val find_shortest_path: DatatypeAux.descr -> int -> (string * int) option + val find_shortest_path: Datatype.descr -> int -> (string * int) option val mk_eq_eqns: theory -> string -> (thm * bool) list val mk_case_cert: theory -> string -> thm val setup: theory -> theory @@ -17,7 +17,7 @@ (** find shortest path to constructor with no recursive arguments **) -fun find_nonempty (descr: DatatypeAux.descr) is i = +fun find_nonempty (descr: Datatype.descr) is i = let val (_, _, constrs) = the (AList.lookup (op =) descr i); fun arg_nonempty (_, DatatypeAux.DtRec i) = if member (op =) is i @@ -42,7 +42,7 @@ (* datatype definition *) -fun add_dt_defs thy defs dep module (descr: DatatypeAux.descr) sorts gr = +fun add_dt_defs thy defs dep module (descr: Datatype.descr) sorts gr = let val descr' = List.filter (can (map DatatypeAux.dest_DtTFree o #2 o snd)) descr; val rtnames = map (#1 o snd) (List.filter (fn (_, (_, _, cs)) => diff -r 926ebca5a145 -r b3f63611784e src/HOL/Tools/datatype_package/datatype_realizer.ML --- a/src/HOL/Tools/datatype_package/datatype_realizer.ML Sun Jun 21 08:38:57 2009 +0200 +++ b/src/HOL/Tools/datatype_package/datatype_realizer.ML Sun Jun 21 08:38:58 2009 +0200 @@ -7,7 +7,7 @@ signature DATATYPE_REALIZER = sig - val add_dt_realizers: DatatypeAux.datatype_config -> string list -> theory -> theory + val add_dt_realizers: Datatype.config -> string list -> theory -> theory val setup: theory -> theory end; @@ -38,7 +38,7 @@ fun mk_realizes T = Const ("realizes", T --> HOLogic.boolT --> HOLogic.boolT); -fun make_ind sorts ({descr, rec_names, rec_rewrites, induction, ...} : datatype_info) is thy = +fun make_ind sorts ({descr, rec_names, rec_rewrites, induction, ...} : info) is thy = let val recTs = get_rec_types descr sorts; val pnames = if length descr = 1 then ["P"] @@ -157,7 +157,7 @@ in Extraction.add_realizers_i [(ind_name, (vs, r', prf))] thy' end; -fun make_casedists sorts ({index, descr, case_name, case_rewrites, exhaustion, ...} : datatype_info) thy = +fun make_casedists sorts ({index, descr, case_name, case_rewrites, exhaustion, ...} : info) thy = let val cert = cterm_of thy; val rT = TFree ("'P", HOLogic.typeS); diff -r 926ebca5a145 -r b3f63611784e src/HOL/Tools/datatype_package/datatype_rep_proofs.ML --- a/src/HOL/Tools/datatype_package/datatype_rep_proofs.ML Sun Jun 21 08:38:57 2009 +0200 +++ b/src/HOL/Tools/datatype_package/datatype_rep_proofs.ML Sun Jun 21 08:38:58 2009 +0200 @@ -11,12 +11,10 @@ signature DATATYPE_REP_PROOFS = sig - type datatype_config = DatatypeAux.datatype_config - type descr = DatatypeAux.descr - type datatype_info = DatatypeAux.datatype_info + include DATATYPE_COMMON val distinctness_limit : int Config.T val distinctness_limit_setup : theory -> theory - val representation_proofs : datatype_config -> datatype_info Symtab.table -> + val representation_proofs : config -> info Symtab.table -> string list -> descr list -> (string * sort) list -> (binding * mixfix) list -> (binding * mixfix) list list -> attribute -> theory -> (thm list list * thm list list * thm list list * @@ -43,12 +41,12 @@ val myinv_f_f = thm "myinv_f_f"; -fun exh_thm_of (dt_info : datatype_info Symtab.table) tname = +fun exh_thm_of (dt_info : info Symtab.table) tname = #exhaustion (the (Symtab.lookup dt_info tname)); (******************************************************************************) -fun representation_proofs (config : datatype_config) (dt_info : datatype_info Symtab.table) +fun representation_proofs (config : config) (dt_info : info Symtab.table) new_type_names descr sorts types_syntax constr_syntax case_names_induct thy = let val Datatype_thy = ThyInfo.the_theory "Datatype" thy; diff -r 926ebca5a145 -r b3f63611784e src/HOL/Tools/function_package/size.ML --- a/src/HOL/Tools/function_package/size.ML Sun Jun 21 08:38:57 2009 +0200 +++ b/src/HOL/Tools/function_package/size.ML Sun Jun 21 08:38:58 2009 +0200 @@ -57,7 +57,7 @@ val app = curry (list_comb o swap); -fun prove_size_thms (info : datatype_info) new_type_names thy = +fun prove_size_thms (info : info) new_type_names thy = let val {descr, alt_names, sorts, rec_names, rec_rewrites, induction, ...} = info; val l = length new_type_names; diff -r 926ebca5a145 -r b3f63611784e src/HOL/Tools/old_primrec.ML --- a/src/HOL/Tools/old_primrec.ML Sun Jun 21 08:38:57 2009 +0200 +++ b/src/HOL/Tools/old_primrec.ML Sun Jun 21 08:38:58 2009 +0200 @@ -221,7 +221,7 @@ (* find datatypes which contain all datatypes in tnames' *) -fun find_dts (dt_info : datatype_info Symtab.table) _ [] = [] +fun find_dts (dt_info : info Symtab.table) _ [] = [] | find_dts dt_info tnames' (tname::tnames) = (case Symtab.lookup dt_info tname of NONE => primrec_err (quote tname ^ " is not a datatype") @@ -230,7 +230,7 @@ (tname, dt)::(find_dts dt_info tnames' tnames) else find_dts dt_info tnames' tnames); -fun prepare_induct ({descr, induction, ...}: datatype_info) rec_eqns = +fun prepare_induct ({descr, induction, ...}: info) rec_eqns = let fun constrs_of (_, (_, _, cs)) = map (fn (cname:string, (_, cargs, _, _, _)) => (cname, map fst cargs)) cs; diff -r 926ebca5a145 -r b3f63611784e src/HOL/Tools/primrec.ML --- a/src/HOL/Tools/primrec.ML Sun Jun 21 08:38:57 2009 +0200 +++ b/src/HOL/Tools/primrec.ML Sun Jun 21 08:38:58 2009 +0200 @@ -203,7 +203,7 @@ (* find datatypes which contain all datatypes in tnames' *) -fun find_dts (dt_info : datatype_info Symtab.table) _ [] = [] +fun find_dts (dt_info : info Symtab.table) _ [] = [] | find_dts dt_info tnames' (tname::tnames) = (case Symtab.lookup dt_info tname of NONE => primrec_error (quote tname ^ " is not a datatype") diff -r 926ebca5a145 -r b3f63611784e src/HOL/Tools/quickcheck_generators.ML --- a/src/HOL/Tools/quickcheck_generators.ML Sun Jun 21 08:38:57 2009 +0200 +++ b/src/HOL/Tools/quickcheck_generators.ML Sun Jun 21 08:38:58 2009 +0200 @@ -12,10 +12,10 @@ -> seed -> (('a -> 'b) * (unit -> Term.term)) * seed val ensure_random_typecopy: string -> theory -> theory val random_aux_specification: string -> term list -> local_theory -> local_theory - val mk_random_aux_eqs: theory -> DatatypeAux.descr -> (string * sort) list + val mk_random_aux_eqs: theory -> Datatype.descr -> (string * sort) list -> string list -> string list * string list -> typ list * typ list -> string * (term list * (term * term) list) - val ensure_random_datatype: DatatypeAux.datatype_config -> string list -> theory -> theory + val ensure_random_datatype: Datatype.config -> string list -> theory -> theory val eval_ref: (unit -> int -> seed -> term list option * seed) option ref val setup: theory -> theory end; diff -r 926ebca5a145 -r b3f63611784e src/HOL/Tools/refute.ML --- a/src/HOL/Tools/refute.ML Sun Jun 21 08:38:57 2009 +0200 +++ b/src/HOL/Tools/refute.ML Sun Jun 21 08:38:58 2009 +0200 @@ -73,7 +73,7 @@ val specialize_type : theory -> (string * Term.typ) -> Term.term -> Term.term val string_of_typ : Term.typ -> string val typ_of_dtyp : - DatatypeAux.descr -> (DatatypeAux.dtyp * Term.typ) list -> DatatypeAux.dtyp + Datatype.descr -> (Datatype.dtyp * Term.typ) list -> Datatype.dtyp -> Term.typ end; (* signature REFUTE *) @@ -411,15 +411,6 @@ (* TRANSLATION HOL -> PROPOSITIONAL LOGIC, BOOLEAN ASSIGNMENT -> MODEL *) (* ------------------------------------------------------------------------- *) -(* ------------------------------------------------------------------------- *) -(* typ_of_dtyp: converts a data type ('DatatypeAux.dtyp') into a type *) -(* ('Term.typ'), given type parameters for the data type's type *) -(* arguments *) -(* ------------------------------------------------------------------------- *) - - (* DatatypeAux.descr -> (DatatypeAux.dtyp * Term.typ) list -> - DatatypeAux.dtyp -> Term.typ *) - fun typ_of_dtyp descr typ_assoc (DatatypeAux.DtTFree a) = (* replace a 'DtTFree' variable by the associated type *) the (AList.lookup (op =) typ_assoc (DatatypeAux.DtTFree a)) @@ -1660,10 +1651,6 @@ (* their arguments) of the size of the argument types *) (* ------------------------------------------------------------------------- *) - (* theory -> (Term.typ * int) list -> DatatypeAux.descr -> - (DatatypeAux.dtyp * Term.typ) list -> - (string * DatatypeAux.dtyp list) list -> int *) - fun size_of_dtyp thy typ_sizes descr typ_assoc constructors = sum (map (fn (_, dtyps) => product (map (size_of_type thy (typ_sizes, []) o @@ -2144,7 +2131,6 @@ (* decrement depth for the IDT 'T' *) val typs' = (case AList.lookup (op =) typs T of NONE => typs | SOME n => AList.update (op =) (T, n-1) typs) - (* Term.term list -> DatatypeAux.dtyp list -> Term.term list *) fun constructor_terms terms [] = terms | constructor_terms terms (d::ds) = let @@ -2241,7 +2227,6 @@ else () (* returns an interpretation where everything is mapped to *) (* an "undefined" element of the datatype *) - (* DatatypeAux.dtyp list -> interpretation *) fun make_undef [] = Leaf (replicate total False) | make_undef (d::ds) = @@ -2253,7 +2238,6 @@ Node (replicate size (make_undef ds)) end (* returns the interpretation for a constructor *) - (* int * DatatypeAux.dtyp list -> int * interpretation *) fun make_constr (offset, []) = if offset - (DatatypeAux.dtyp * Term.typ) list -> - (DatatypeAux.dtyp * Term.typ) list *) fun rec_typ_assoc acc [] = acc | rec_typ_assoc acc ((d, T)::xs) = @@ -2458,7 +2439,6 @@ else raise REFUTE ("IDT_recursion_interpreter", "different type associations for the same dtyp")) - (* (DatatypeAux.dtyp * Term.typ) list *) val typ_assoc = filter (fn (DatatypeAux.DtTFree _, _) => true | (_, _) => false) (rec_typ_assoc [] @@ -2613,7 +2593,6 @@ val rec_dtyps_args = List.filter (DatatypeAux.is_rec_type o fst) (dtyps ~~ args) (* map those indices to interpretations *) - (* (DatatypeAux.dtyp * interpretation) list *) val rec_dtyps_intrs = map (fn (dtyp, arg) => let val dT = typ_of_dtyp descr typ_assoc dtyp @@ -2625,8 +2604,6 @@ (* takes the dtyp and interpretation of an element, *) (* and computes the interpretation for the *) (* corresponding recursive argument *) - (* DatatypeAux.dtyp -> interpretation -> - interpretation *) fun rec_intr (DatatypeAux.DtRec i) (Leaf xs) = (* recursive argument is "rec_i params elem" *) compute_array_entry i (find_index_eq True xs) @@ -3252,8 +3229,6 @@ (* constructor generates the datatype's element that is given by *) (* 'element', returns the constructor (as a term) as well as the *) (* indices of the arguments *) - (* string * DatatypeAux.dtyp list -> - (Term.term * int list) option *) fun get_constr_args (cname, cargs) = let val cTerm = Const (cname, @@ -3281,7 +3256,6 @@ in Option.map (fn args => (cTerm, cargs, args)) (get_args iC) end - (* Term.term * DatatypeAux.dtyp list * int list *) val (cTerm, cargs, args) = (* we could speed things up by computing the correct *) (* constructor directly (rather than testing all *)