1.1 --- a/src/HOL/Nominal/nominal.ML Sun Jun 21 15:47:41 2009 +0200
1.2 +++ b/src/HOL/Nominal/nominal.ML Sun Jun 21 19:09:31 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 15:47:41 2009 +0200
2.2 +++ b/src/HOL/Nominal/nominal_atoms.ML Sun Jun 21 19:09:31 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.ML Sun Jun 21 15:47:41 2009 +0200
3.2 +++ b/src/HOL/Tools/datatype_package/datatype.ML Sun Jun 21 19:09:31 2009 +0200
3.3 @@ -6,26 +6,7 @@
3.4
3.5 signature DATATYPE =
3.6 sig
3.7 - type datatype_config = DatatypeAux.datatype_config
3.8 - type datatype_info = DatatypeAux.datatype_info
3.9 - type descr = DatatypeAux.descr
3.10 - val get_datatypes : theory -> datatype_info Symtab.table
3.11 - val get_datatype : theory -> string -> datatype_info option
3.12 - val the_datatype : theory -> string -> datatype_info
3.13 - val datatype_of_constr : theory -> string -> datatype_info option
3.14 - val datatype_of_case : theory -> string -> datatype_info option
3.15 - val the_datatype_spec : theory -> string -> (string * sort) list * (string * typ list) list
3.16 - val the_datatype_descr : theory -> string list
3.17 - -> descr * (string * sort) list * string list
3.18 - * (string list * string list) * (typ list * typ list)
3.19 - val get_datatype_constrs : theory -> string -> (string * typ) list option
3.20 - val distinct_simproc : simproc
3.21 - val make_case : Proof.context -> bool -> string list -> term ->
3.22 - (term * term) list -> term * (term * (int * bool)) list
3.23 - val strip_case : Proof.context -> bool -> term -> (term * (term * term) list) option
3.24 - val read_typ: theory ->
3.25 - (typ list * (string * sort) list) * string -> typ list * (string * sort) list
3.26 - val interpretation : (datatype_config -> string list -> theory -> theory) -> theory -> theory
3.27 + include DATATYPE_COMMON
3.28 type rules = {distinct : thm list list,
3.29 inject : thm list list,
3.30 exhaustion : thm list,
3.31 @@ -34,15 +15,31 @@
3.32 split_thms : (thm * thm) list,
3.33 induction : thm,
3.34 simps : thm list}
3.35 - val rep_datatype : datatype_config -> (rules -> Proof.context -> Proof.context)
3.36 - -> string list option -> term list -> theory -> Proof.state;
3.37 + val add_datatype : config -> string list -> (string list * binding * mixfix *
3.38 + (binding * typ list * mixfix) list) list -> theory -> rules * theory
3.39 + val datatype_cmd : string list -> (string list * binding * mixfix *
3.40 + (binding * string list * mixfix) list) list -> theory -> theory
3.41 + val rep_datatype : config -> (rules -> Proof.context -> Proof.context)
3.42 + -> string list option -> term list -> theory -> Proof.state
3.43 val rep_datatype_cmd : string list option -> string list -> theory -> Proof.state
3.44 - val add_datatype : datatype_config -> string list -> (string list * binding * mixfix *
3.45 - (binding * typ list * mixfix) list) list -> theory -> rules * theory
3.46 - val add_datatype_cmd : string list -> (string list * binding * mixfix *
3.47 - (binding * string list * mixfix) list) list -> theory -> rules * theory
3.48 + val get_datatypes : theory -> info Symtab.table
3.49 + val get_datatype : theory -> string -> info option
3.50 + val the_datatype : theory -> string -> info
3.51 + val datatype_of_constr : theory -> string -> info option
3.52 + val datatype_of_case : theory -> string -> info option
3.53 + val the_datatype_spec : theory -> string -> (string * sort) list * (string * typ list) list
3.54 + val the_datatype_descr : theory -> string list
3.55 + -> descr * (string * sort) list * string list
3.56 + * (string list * string list) * (typ list * typ list)
3.57 + val get_datatype_constrs : theory -> string -> (string * typ) list option
3.58 + val interpretation : (config -> string list -> theory -> theory) -> theory -> theory
3.59 + val distinct_simproc : simproc
3.60 + val make_case : Proof.context -> bool -> string list -> term ->
3.61 + (term * term) list -> term * (term * (int * bool)) list
3.62 + val strip_case : Proof.context -> bool -> term -> (term * (term * term) list) option
3.63 + val read_typ: theory ->
3.64 + (typ list * (string * sort) list) * string -> typ list * (string * sort) list
3.65 val setup: theory -> theory
3.66 - val print_datatypes : theory -> unit
3.67 end;
3.68
3.69 structure Datatype : DATATYPE =
3.70 @@ -56,9 +53,9 @@
3.71 structure DatatypesData = TheoryDataFun
3.72 (
3.73 type T =
3.74 - {types: datatype_info Symtab.table,
3.75 - constrs: datatype_info Symtab.table,
3.76 - cases: datatype_info Symtab.table};
3.77 + {types: info Symtab.table,
3.78 + constrs: info Symtab.table,
3.79 + cases: info Symtab.table};
3.80
3.81 val empty =
3.82 {types = Symtab.empty, constrs = Symtab.empty, cases = Symtab.empty};
3.83 @@ -75,14 +72,10 @@
3.84 val get_datatypes = #types o DatatypesData.get;
3.85 val map_datatypes = DatatypesData.map;
3.86
3.87 -fun print_datatypes thy =
3.88 - Pretty.writeln (Pretty.strs ("datatypes:" ::
3.89 - map #1 (NameSpace.extern_table (Sign.type_space thy, get_datatypes thy))));
3.90 -
3.91
3.92 (** theory information about datatypes **)
3.93
3.94 -fun put_dt_infos (dt_infos : (string * datatype_info) list) =
3.95 +fun put_dt_infos (dt_infos : (string * info) list) =
3.96 map_datatypes (fn {types, constrs, cases} =>
3.97 {types = fold Symtab.update dt_infos types,
3.98 constrs = fold Symtab.default (*conservative wrt. overloaded constructors*)
3.99 @@ -207,7 +200,7 @@
3.100 let
3.101 val inducts = ProjectRule.projections (ProofContext.init thy) induction;
3.102
3.103 - fun named_rules (name, {index, exhaustion, ...}: datatype_info) =
3.104 + fun named_rules (name, {index, exhaustion, ...}: info) =
3.105 [((Binding.empty, nth inducts index), [Induct.induct_type name]),
3.106 ((Binding.empty, exhaustion), [Induct.cases_type name])];
3.107 fun unnamed_rule i =
3.108 @@ -351,13 +344,13 @@
3.109 simps : thm list}
3.110
3.111 structure DatatypeInterpretation = InterpretationFun
3.112 - (type T = datatype_config * string list val eq: T * T -> bool = eq_snd op =);
3.113 + (type T = config * string list val eq: T * T -> bool = eq_snd op =);
3.114 fun interpretation f = DatatypeInterpretation.interpretation (uncurry f);
3.115
3.116
3.117 (******************* definitional introduction of datatypes *******************)
3.118
3.119 -fun add_datatype_def (config : datatype_config) new_type_names descr sorts types_syntax constr_syntax dt_info
3.120 +fun add_datatype_def (config : config) new_type_names descr sorts types_syntax constr_syntax dt_info
3.121 case_names_induct case_names_exhausts thy =
3.122 let
3.123 val _ = message config ("Proofs for datatype(s) " ^ commas_quote new_type_names);
3.124 @@ -414,7 +407,7 @@
3.125
3.126 (*********************** declare existing type as datatype *********************)
3.127
3.128 -fun prove_rep_datatype (config : datatype_config) alt_names new_type_names descr sorts induct inject half_distinct thy =
3.129 +fun prove_rep_datatype (config : config) alt_names new_type_names descr sorts induct inject half_distinct thy =
3.130 let
3.131 val ((_, [induct']), _) =
3.132 Variable.importT_thms [induct] (Variable.thm_context induct);
3.133 @@ -487,7 +480,7 @@
3.134 simps = simps}, thy11)
3.135 end;
3.136
3.137 -fun gen_rep_datatype prep_term (config : datatype_config) after_qed alt_names raw_ts thy =
3.138 +fun gen_rep_datatype prep_term (config : config) after_qed alt_names raw_ts thy =
3.139 let
3.140 fun constr_of_term (Const (c, T)) = (c, T)
3.141 | constr_of_term t =
3.142 @@ -553,13 +546,13 @@
3.143 end;
3.144
3.145 val rep_datatype = gen_rep_datatype Sign.cert_term;
3.146 -val rep_datatype_cmd = gen_rep_datatype Syntax.read_term_global default_datatype_config (K I);
3.147 +val rep_datatype_cmd = gen_rep_datatype Syntax.read_term_global default_config (K I);
3.148
3.149
3.150
3.151 (******************************** add datatype ********************************)
3.152
3.153 -fun gen_add_datatype prep_typ (config : datatype_config) new_type_names dts thy =
3.154 +fun gen_add_datatype prep_typ (config : config) new_type_names dts thy =
3.155 let
3.156 val _ = Theory.requires thy "Datatype" "datatype definitions";
3.157
3.158 @@ -627,12 +620,12 @@
3.159 val case_names_exhausts = mk_case_names_exhausts descr' (map #1 new_dts);
3.160 in
3.161 add_datatype_def
3.162 - (config : datatype_config) new_type_names descr sorts types_syntax constr_syntax dt_info
3.163 + (config : config) new_type_names descr sorts types_syntax constr_syntax dt_info
3.164 case_names_induct case_names_exhausts thy
3.165 end;
3.166
3.167 val add_datatype = gen_add_datatype cert_typ;
3.168 -val add_datatype_cmd = gen_add_datatype read_typ default_datatype_config;
3.169 +val datatype_cmd = snd ooo gen_add_datatype read_typ default_config;
3.170
3.171
3.172
3.173 @@ -649,23 +642,29 @@
3.174
3.175 (* outer syntax *)
3.176
3.177 -local structure P = OuterParse and K = OuterKeyword in
3.178 +local
3.179
3.180 -val datatype_decl =
3.181 - Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.type_args -- P.binding -- P.opt_infix --
3.182 - (P.$$$ "=" |-- P.enum1 "|" (P.binding -- Scan.repeat P.typ -- P.opt_mixfix));
3.183 +structure P = OuterParse and K = OuterKeyword
3.184
3.185 -fun mk_datatype args =
3.186 +fun prep_datatype_decls args =
3.187 let
3.188 val names = map
3.189 (fn ((((NONE, _), t), _), _) => Binding.name_of t | ((((SOME t, _), _), _), _) => t) args;
3.190 val specs = map (fn ((((_, vs), t), mx), cons) =>
3.191 (vs, t, mx, map (fn ((x, y), z) => (x, y, z)) cons)) args;
3.192 - in snd o add_datatype_cmd names specs end;
3.193 + in (names, specs) end;
3.194 +
3.195 +val parse_datatype_decl =
3.196 + (Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.type_args -- P.binding -- P.opt_infix --
3.197 + (P.$$$ "=" |-- P.enum1 "|" (P.binding -- Scan.repeat P.typ -- P.opt_mixfix)));
3.198 +
3.199 +val parse_datatype_decls = P.and_list1 parse_datatype_decl >> prep_datatype_decls;
3.200 +
3.201 +in
3.202
3.203 val _ =
3.204 OuterSyntax.command "datatype" "define inductive datatypes" K.thy_decl
3.205 - (P.and_list1 datatype_decl >> (Toplevel.theory o mk_datatype));
3.206 + (parse_datatype_decls >> (fn (names, specs) => Toplevel.theory (datatype_cmd names specs)));
3.207
3.208 val _ =
3.209 OuterSyntax.command "rep_datatype" "represent existing types inductively" K.thy_goal
4.1 --- a/src/HOL/Tools/datatype_package/datatype_abs_proofs.ML Sun Jun 21 15:47:41 2009 +0200
4.2 +++ b/src/HOL/Tools/datatype_package/datatype_abs_proofs.ML Sun Jun 21 19:09:31 2009 +0200
4.3 @@ -14,24 +14,22 @@
4.4
4.5 signature DATATYPE_ABS_PROOFS =
4.6 sig
4.7 - type datatype_config = DatatypeAux.datatype_config
4.8 - type descr = DatatypeAux.descr
4.9 - type datatype_info = DatatypeAux.datatype_info
4.10 - val prove_casedist_thms : datatype_config -> string list ->
4.11 + include DATATYPE_COMMON
4.12 + val prove_casedist_thms : config -> string list ->
4.13 descr list -> (string * sort) list -> thm ->
4.14 attribute list -> theory -> thm list * theory
4.15 - val prove_primrec_thms : datatype_config -> string list ->
4.16 + val prove_primrec_thms : config -> string list ->
4.17 descr list -> (string * sort) list ->
4.18 - datatype_info Symtab.table -> thm list list -> thm list list ->
4.19 + info Symtab.table -> thm list list -> thm list list ->
4.20 simpset -> thm -> theory -> (string list * thm list) * theory
4.21 - val prove_case_thms : datatype_config -> string list ->
4.22 + val prove_case_thms : config -> string list ->
4.23 descr list -> (string * sort) list ->
4.24 string list -> thm list -> theory -> (thm list list * string list) * theory
4.25 - val prove_split_thms : datatype_config -> string list ->
4.26 + val prove_split_thms : config -> string list ->
4.27 descr list -> (string * sort) list ->
4.28 thm list list -> thm list list -> thm list -> thm list list -> theory ->
4.29 (thm * thm) list * theory
4.30 - val prove_nchotomys : datatype_config -> string list -> descr list ->
4.31 + val prove_nchotomys : config -> string list -> descr list ->
4.32 (string * sort) list -> thm list -> theory -> thm list * theory
4.33 val prove_weak_case_congs : string list -> descr list ->
4.34 (string * sort) list -> theory -> thm list * theory
4.35 @@ -47,7 +45,7 @@
4.36
4.37 (************************ case distinction theorems ***************************)
4.38
4.39 -fun prove_casedist_thms (config : datatype_config) new_type_names descr sorts induct case_names_exhausts thy =
4.40 +fun prove_casedist_thms (config : config) new_type_names descr sorts induct case_names_exhausts thy =
4.41 let
4.42 val _ = message config "Proving case distinction theorems ...";
4.43
4.44 @@ -89,8 +87,8 @@
4.45
4.46 (*************************** primrec combinators ******************************)
4.47
4.48 -fun prove_primrec_thms (config : datatype_config) new_type_names descr sorts
4.49 - (dt_info : datatype_info Symtab.table) constr_inject dist_rewrites dist_ss induct thy =
4.50 +fun prove_primrec_thms (config : config) new_type_names descr sorts
4.51 + (dt_info : info Symtab.table) constr_inject dist_rewrites dist_ss induct thy =
4.52 let
4.53 val _ = message config "Constructing primrec combinators ...";
4.54
4.55 @@ -275,7 +273,7 @@
4.56
4.57 (***************************** case combinators *******************************)
4.58
4.59 -fun prove_case_thms (config : datatype_config) new_type_names descr sorts reccomb_names primrec_thms thy =
4.60 +fun prove_case_thms (config : config) new_type_names descr sorts reccomb_names primrec_thms thy =
4.61 let
4.62 val _ = message config "Proving characteristic theorems for case combinators ...";
4.63
4.64 @@ -349,7 +347,7 @@
4.65
4.66 (******************************* case splitting *******************************)
4.67
4.68 -fun prove_split_thms (config : datatype_config) new_type_names descr sorts constr_inject dist_rewrites
4.69 +fun prove_split_thms (config : config) new_type_names descr sorts constr_inject dist_rewrites
4.70 casedist_thms case_thms thy =
4.71 let
4.72 val _ = message config "Proving equations for case splitting ...";
4.73 @@ -398,7 +396,7 @@
4.74
4.75 (************************* additional theorems for TFL ************************)
4.76
4.77 -fun prove_nchotomys (config : datatype_config) new_type_names descr sorts casedist_thms thy =
4.78 +fun prove_nchotomys (config : config) new_type_names descr sorts casedist_thms thy =
4.79 let
4.80 val _ = message config "Proving additional theorems for TFL ...";
4.81
5.1 --- a/src/HOL/Tools/datatype_package/datatype_aux.ML Sun Jun 21 15:47:41 2009 +0200
5.2 +++ b/src/HOL/Tools/datatype_package/datatype_aux.ML Sun Jun 21 19:09:31 2009 +0200
5.3 @@ -4,11 +4,23 @@
5.4 Auxiliary functions for defining datatypes.
5.5 *)
5.6
5.7 +signature DATATYPE_COMMON =
5.8 +sig
5.9 + type config
5.10 + val default_config : config
5.11 + datatype dtyp =
5.12 + DtTFree of string
5.13 + | DtType of string * (dtyp list)
5.14 + | DtRec of int;
5.15 + type descr
5.16 + type info
5.17 +end
5.18 +
5.19 signature DATATYPE_AUX =
5.20 sig
5.21 - type datatype_config
5.22 - val default_datatype_config : datatype_config
5.23 - val message : datatype_config -> string -> unit
5.24 + include DATATYPE_COMMON
5.25 +
5.26 + val message : config -> string -> unit
5.27
5.28 val add_path : bool -> string -> theory -> theory
5.29 val parent_path : bool -> theory -> theory
5.30 @@ -33,12 +45,6 @@
5.31 datatype simproc_dist = FewConstrs of thm list
5.32 | ManyConstrs of thm * simpset;
5.33
5.34 - datatype dtyp =
5.35 - DtTFree of string
5.36 - | DtType of string * (dtyp list)
5.37 - | DtRec of int;
5.38 - type descr
5.39 - type datatype_info
5.40
5.41 exception Datatype
5.42 exception Datatype_Empty of string
5.43 @@ -61,7 +67,7 @@
5.44 -> ((string * Term.typ list) * (string * 'a list) list) list
5.45 val check_nonempty : descr list -> unit
5.46 val unfold_datatypes :
5.47 - theory -> descr -> (string * sort) list -> datatype_info Symtab.table ->
5.48 + theory -> descr -> (string * sort) list -> info Symtab.table ->
5.49 descr -> int -> descr list * int
5.50 end;
5.51
5.52 @@ -70,10 +76,10 @@
5.53
5.54 (* datatype option flags *)
5.55
5.56 -type datatype_config = { strict: bool, flat_names: bool, quiet: bool };
5.57 -val default_datatype_config : datatype_config =
5.58 +type config = { strict: bool, flat_names: bool, quiet: bool };
5.59 +val default_config : config =
5.60 { strict = true, flat_names = false, quiet = false };
5.61 -fun message ({ quiet, ...} : datatype_config) s =
5.62 +fun message ({ quiet, ...} : config) s =
5.63 if quiet then () else writeln s;
5.64
5.65 fun add_path flat_names s = if flat_names then I else Sign.add_path s;
5.66 @@ -186,7 +192,7 @@
5.67 (* index, datatype name, type arguments, constructor name, types of constructor's arguments *)
5.68 type descr = (int * (string * dtyp list * (string * dtyp list) list)) list;
5.69
5.70 -type datatype_info =
5.71 +type info =
5.72 {index : int,
5.73 alt_names : string list option,
5.74 descr : descr,
5.75 @@ -317,7 +323,7 @@
5.76 (* all types of the form DtType (dt_name, [..., DtRec _, ...]) *)
5.77 (* need to be unfolded *)
5.78
5.79 -fun unfold_datatypes sign orig_descr sorts (dt_info : datatype_info Symtab.table) descr i =
5.80 +fun unfold_datatypes sign orig_descr sorts (dt_info : info Symtab.table) descr i =
5.81 let
5.82 fun typ_error T msg = error ("Non-admissible type expression\n" ^
5.83 Syntax.string_of_typ_global sign (typ_of_dtyp (orig_descr @ descr) sorts T) ^ "\n" ^ msg);
6.1 --- a/src/HOL/Tools/datatype_package/datatype_case.ML Sun Jun 21 15:47:41 2009 +0200
6.2 +++ b/src/HOL/Tools/datatype_package/datatype_case.ML Sun Jun 21 19:09:31 2009 +0200
6.3 @@ -7,16 +7,16 @@
6.4
6.5 signature DATATYPE_CASE =
6.6 sig
6.7 - val make_case: (string -> DatatypeAux.datatype_info option) ->
6.8 + val make_case: (string -> DatatypeAux.info option) ->
6.9 Proof.context -> bool -> string list -> term -> (term * term) list ->
6.10 term * (term * (int * bool)) list
6.11 - val dest_case: (string -> DatatypeAux.datatype_info option) -> bool ->
6.12 + val dest_case: (string -> DatatypeAux.info option) -> bool ->
6.13 string list -> term -> (term * (term * term) list) option
6.14 - val strip_case: (string -> DatatypeAux.datatype_info option) -> bool ->
6.15 + val strip_case: (string -> DatatypeAux.info option) -> bool ->
6.16 term -> (term * (term * term) list) option
6.17 - val case_tr: bool -> (theory -> string -> DatatypeAux.datatype_info option)
6.18 + val case_tr: bool -> (theory -> string -> DatatypeAux.info option)
6.19 -> Proof.context -> term list -> term
6.20 - val case_tr': (theory -> string -> DatatypeAux.datatype_info option) ->
6.21 + val case_tr': (theory -> string -> DatatypeAux.info option) ->
6.22 string -> Proof.context -> term list -> term
6.23 end;
6.24
6.25 @@ -31,7 +31,7 @@
6.26 * Get information about datatypes
6.27 *---------------------------------------------------------------------------*)
6.28
6.29 -fun ty_info (tab : string -> DatatypeAux.datatype_info option) s =
6.30 +fun ty_info (tab : string -> DatatypeAux.info option) s =
6.31 case tab s of
6.32 SOME {descr, case_name, index, sorts, ...} =>
6.33 let
7.1 --- a/src/HOL/Tools/datatype_package/datatype_codegen.ML Sun Jun 21 15:47:41 2009 +0200
7.2 +++ b/src/HOL/Tools/datatype_package/datatype_codegen.ML Sun Jun 21 19:09:31 2009 +0200
7.3 @@ -6,7 +6,7 @@
7.4
7.5 signature DATATYPE_CODEGEN =
7.6 sig
7.7 - val find_shortest_path: DatatypeAux.descr -> int -> (string * int) option
7.8 + val find_shortest_path: Datatype.descr -> int -> (string * int) option
7.9 val mk_eq_eqns: theory -> string -> (thm * bool) list
7.10 val mk_case_cert: theory -> string -> thm
7.11 val setup: theory -> theory
7.12 @@ -17,7 +17,7 @@
7.13
7.14 (** find shortest path to constructor with no recursive arguments **)
7.15
7.16 -fun find_nonempty (descr: DatatypeAux.descr) is i =
7.17 +fun find_nonempty (descr: Datatype.descr) is i =
7.18 let
7.19 val (_, _, constrs) = the (AList.lookup (op =) descr i);
7.20 fun arg_nonempty (_, DatatypeAux.DtRec i) = if member (op =) is i
7.21 @@ -42,7 +42,7 @@
7.22
7.23 (* datatype definition *)
7.24
7.25 -fun add_dt_defs thy defs dep module (descr: DatatypeAux.descr) sorts gr =
7.26 +fun add_dt_defs thy defs dep module (descr: Datatype.descr) sorts gr =
7.27 let
7.28 val descr' = List.filter (can (map DatatypeAux.dest_DtTFree o #2 o snd)) descr;
7.29 val rtnames = map (#1 o snd) (List.filter (fn (_, (_, _, cs)) =>
8.1 --- a/src/HOL/Tools/datatype_package/datatype_realizer.ML Sun Jun 21 15:47:41 2009 +0200
8.2 +++ b/src/HOL/Tools/datatype_package/datatype_realizer.ML Sun Jun 21 19:09:31 2009 +0200
8.3 @@ -7,7 +7,7 @@
8.4
8.5 signature DATATYPE_REALIZER =
8.6 sig
8.7 - val add_dt_realizers: DatatypeAux.datatype_config -> string list -> theory -> theory
8.8 + val add_dt_realizers: Datatype.config -> string list -> theory -> theory
8.9 val setup: theory -> theory
8.10 end;
8.11
8.12 @@ -38,7 +38,7 @@
8.13
8.14 fun mk_realizes T = Const ("realizes", T --> HOLogic.boolT --> HOLogic.boolT);
8.15
8.16 -fun make_ind sorts ({descr, rec_names, rec_rewrites, induction, ...} : datatype_info) is thy =
8.17 +fun make_ind sorts ({descr, rec_names, rec_rewrites, induction, ...} : info) is thy =
8.18 let
8.19 val recTs = get_rec_types descr sorts;
8.20 val pnames = if length descr = 1 then ["P"]
8.21 @@ -157,7 +157,7 @@
8.22 in Extraction.add_realizers_i [(ind_name, (vs, r', prf))] thy' end;
8.23
8.24
8.25 -fun make_casedists sorts ({index, descr, case_name, case_rewrites, exhaustion, ...} : datatype_info) thy =
8.26 +fun make_casedists sorts ({index, descr, case_name, case_rewrites, exhaustion, ...} : info) thy =
8.27 let
8.28 val cert = cterm_of thy;
8.29 val rT = TFree ("'P", HOLogic.typeS);
9.1 --- a/src/HOL/Tools/datatype_package/datatype_rep_proofs.ML Sun Jun 21 15:47:41 2009 +0200
9.2 +++ b/src/HOL/Tools/datatype_package/datatype_rep_proofs.ML Sun Jun 21 19:09:31 2009 +0200
9.3 @@ -11,12 +11,10 @@
9.4
9.5 signature DATATYPE_REP_PROOFS =
9.6 sig
9.7 - type datatype_config = DatatypeAux.datatype_config
9.8 - type descr = DatatypeAux.descr
9.9 - type datatype_info = DatatypeAux.datatype_info
9.10 + include DATATYPE_COMMON
9.11 val distinctness_limit : int Config.T
9.12 val distinctness_limit_setup : theory -> theory
9.13 - val representation_proofs : datatype_config -> datatype_info Symtab.table ->
9.14 + val representation_proofs : config -> info Symtab.table ->
9.15 string list -> descr list -> (string * sort) list ->
9.16 (binding * mixfix) list -> (binding * mixfix) list list -> attribute
9.17 -> theory -> (thm list list * thm list list * thm list list *
9.18 @@ -43,12 +41,12 @@
9.19 val myinv_f_f = thm "myinv_f_f";
9.20
9.21
9.22 -fun exh_thm_of (dt_info : datatype_info Symtab.table) tname =
9.23 +fun exh_thm_of (dt_info : info Symtab.table) tname =
9.24 #exhaustion (the (Symtab.lookup dt_info tname));
9.25
9.26 (******************************************************************************)
9.27
9.28 -fun representation_proofs (config : datatype_config) (dt_info : datatype_info Symtab.table)
9.29 +fun representation_proofs (config : config) (dt_info : info Symtab.table)
9.30 new_type_names descr sorts types_syntax constr_syntax case_names_induct thy =
9.31 let
9.32 val Datatype_thy = ThyInfo.the_theory "Datatype" thy;
10.1 --- a/src/HOL/Tools/function_package/size.ML Sun Jun 21 15:47:41 2009 +0200
10.2 +++ b/src/HOL/Tools/function_package/size.ML Sun Jun 21 19:09:31 2009 +0200
10.3 @@ -57,7 +57,7 @@
10.4
10.5 val app = curry (list_comb o swap);
10.6
10.7 -fun prove_size_thms (info : datatype_info) new_type_names thy =
10.8 +fun prove_size_thms (info : info) new_type_names thy =
10.9 let
10.10 val {descr, alt_names, sorts, rec_names, rec_rewrites, induction, ...} = info;
10.11 val l = length new_type_names;
11.1 --- a/src/HOL/Tools/hologic.ML Sun Jun 21 15:47:41 2009 +0200
11.2 +++ b/src/HOL/Tools/hologic.ML Sun Jun 21 19:09:31 2009 +0200
11.3 @@ -603,8 +603,11 @@
11.4
11.5 val typerepT = Type ("Typerep.typerep", []);
11.6
11.7 -fun mk_typerep T = Const ("Typerep.typerep_class.typerep",
11.8 - Term.itselfT T --> typerepT) $ Logic.mk_type T;
11.9 +fun mk_typerep (Type (tyco, Ts)) = Const ("Typerep.typerep.Typerep",
11.10 + literalT --> listT typerepT --> typerepT) $ mk_literal tyco
11.11 + $ mk_list typerepT (map mk_typerep Ts)
11.12 + | mk_typerep (T as TFree _) = Const ("Typerep.typerep_class.typerep",
11.13 + Term.itselfT T --> typerepT) $ Logic.mk_type T;
11.14
11.15 val termT = Type ("Code_Eval.term", []);
11.16
12.1 --- a/src/HOL/Tools/old_primrec.ML Sun Jun 21 15:47:41 2009 +0200
12.2 +++ b/src/HOL/Tools/old_primrec.ML Sun Jun 21 19:09:31 2009 +0200
12.3 @@ -221,7 +221,7 @@
12.4
12.5 (* find datatypes which contain all datatypes in tnames' *)
12.6
12.7 -fun find_dts (dt_info : datatype_info Symtab.table) _ [] = []
12.8 +fun find_dts (dt_info : info Symtab.table) _ [] = []
12.9 | find_dts dt_info tnames' (tname::tnames) =
12.10 (case Symtab.lookup dt_info tname of
12.11 NONE => primrec_err (quote tname ^ " is not a datatype")
12.12 @@ -230,7 +230,7 @@
12.13 (tname, dt)::(find_dts dt_info tnames' tnames)
12.14 else find_dts dt_info tnames' tnames);
12.15
12.16 -fun prepare_induct ({descr, induction, ...}: datatype_info) rec_eqns =
12.17 +fun prepare_induct ({descr, induction, ...}: info) rec_eqns =
12.18 let
12.19 fun constrs_of (_, (_, _, cs)) =
12.20 map (fn (cname:string, (_, cargs, _, _, _)) => (cname, map fst cargs)) cs;
13.1 --- a/src/HOL/Tools/primrec.ML Sun Jun 21 15:47:41 2009 +0200
13.2 +++ b/src/HOL/Tools/primrec.ML Sun Jun 21 19:09:31 2009 +0200
13.3 @@ -203,7 +203,7 @@
13.4
13.5 (* find datatypes which contain all datatypes in tnames' *)
13.6
13.7 -fun find_dts (dt_info : datatype_info Symtab.table) _ [] = []
13.8 +fun find_dts (dt_info : info Symtab.table) _ [] = []
13.9 | find_dts dt_info tnames' (tname::tnames) =
13.10 (case Symtab.lookup dt_info tname of
13.11 NONE => primrec_error (quote tname ^ " is not a datatype")
14.1 --- a/src/HOL/Tools/quickcheck_generators.ML Sun Jun 21 15:47:41 2009 +0200
14.2 +++ b/src/HOL/Tools/quickcheck_generators.ML Sun Jun 21 19:09:31 2009 +0200
14.3 @@ -12,10 +12,10 @@
14.4 -> seed -> (('a -> 'b) * (unit -> Term.term)) * seed
14.5 val ensure_random_typecopy: string -> theory -> theory
14.6 val random_aux_specification: string -> term list -> local_theory -> local_theory
14.7 - val mk_random_aux_eqs: theory -> DatatypeAux.descr -> (string * sort) list
14.8 + val mk_random_aux_eqs: theory -> Datatype.descr -> (string * sort) list
14.9 -> string list -> string list * string list -> typ list * typ list
14.10 -> string * (term list * (term * term) list)
14.11 - val ensure_random_datatype: DatatypeAux.datatype_config -> string list -> theory -> theory
14.12 + val ensure_random_datatype: Datatype.config -> string list -> theory -> theory
14.13 val eval_ref: (unit -> int -> seed -> term list option * seed) option ref
14.14 val setup: theory -> theory
14.15 end;
15.1 --- a/src/HOL/Tools/refute.ML Sun Jun 21 15:47:41 2009 +0200
15.2 +++ b/src/HOL/Tools/refute.ML Sun Jun 21 19:09:31 2009 +0200
15.3 @@ -73,7 +73,7 @@
15.4 val specialize_type : theory -> (string * Term.typ) -> Term.term -> Term.term
15.5 val string_of_typ : Term.typ -> string
15.6 val typ_of_dtyp :
15.7 - DatatypeAux.descr -> (DatatypeAux.dtyp * Term.typ) list -> DatatypeAux.dtyp
15.8 + Datatype.descr -> (Datatype.dtyp * Term.typ) list -> Datatype.dtyp
15.9 -> Term.typ
15.10 end; (* signature REFUTE *)
15.11
15.12 @@ -411,15 +411,6 @@
15.13 (* TRANSLATION HOL -> PROPOSITIONAL LOGIC, BOOLEAN ASSIGNMENT -> MODEL *)
15.14 (* ------------------------------------------------------------------------- *)
15.15
15.16 -(* ------------------------------------------------------------------------- *)
15.17 -(* typ_of_dtyp: converts a data type ('DatatypeAux.dtyp') into a type *)
15.18 -(* ('Term.typ'), given type parameters for the data type's type *)
15.19 -(* arguments *)
15.20 -(* ------------------------------------------------------------------------- *)
15.21 -
15.22 - (* DatatypeAux.descr -> (DatatypeAux.dtyp * Term.typ) list ->
15.23 - DatatypeAux.dtyp -> Term.typ *)
15.24 -
15.25 fun typ_of_dtyp descr typ_assoc (DatatypeAux.DtTFree a) =
15.26 (* replace a 'DtTFree' variable by the associated type *)
15.27 the (AList.lookup (op =) typ_assoc (DatatypeAux.DtTFree a))
15.28 @@ -1660,10 +1651,6 @@
15.29 (* their arguments) of the size of the argument types *)
15.30 (* ------------------------------------------------------------------------- *)
15.31
15.32 - (* theory -> (Term.typ * int) list -> DatatypeAux.descr ->
15.33 - (DatatypeAux.dtyp * Term.typ) list ->
15.34 - (string * DatatypeAux.dtyp list) list -> int *)
15.35 -
15.36 fun size_of_dtyp thy typ_sizes descr typ_assoc constructors =
15.37 sum (map (fn (_, dtyps) =>
15.38 product (map (size_of_type thy (typ_sizes, []) o
15.39 @@ -2144,7 +2131,6 @@
15.40 (* decrement depth for the IDT 'T' *)
15.41 val typs' = (case AList.lookup (op =) typs T of NONE => typs
15.42 | SOME n => AList.update (op =) (T, n-1) typs)
15.43 - (* Term.term list -> DatatypeAux.dtyp list -> Term.term list *)
15.44 fun constructor_terms terms [] = terms
15.45 | constructor_terms terms (d::ds) =
15.46 let
15.47 @@ -2241,7 +2227,6 @@
15.48 else ()
15.49 (* returns an interpretation where everything is mapped to *)
15.50 (* an "undefined" element of the datatype *)
15.51 - (* DatatypeAux.dtyp list -> interpretation *)
15.52 fun make_undef [] =
15.53 Leaf (replicate total False)
15.54 | make_undef (d::ds) =
15.55 @@ -2253,7 +2238,6 @@
15.56 Node (replicate size (make_undef ds))
15.57 end
15.58 (* returns the interpretation for a constructor *)
15.59 - (* int * DatatypeAux.dtyp list -> int * interpretation *)
15.60 fun make_constr (offset, []) =
15.61 if offset<total then
15.62 (offset+1, Leaf ((replicate offset False) @ True ::
15.63 @@ -2421,9 +2405,6 @@
15.64 (* mutually recursive types must have the same type *)
15.65 (* parameters, unless the mutual recursion comes from *)
15.66 (* indirect recursion *)
15.67 - (* (DatatypeAux.dtyp * Term.typ) list ->
15.68 - (DatatypeAux.dtyp * Term.typ) list ->
15.69 - (DatatypeAux.dtyp * Term.typ) list *)
15.70 fun rec_typ_assoc acc [] =
15.71 acc
15.72 | rec_typ_assoc acc ((d, T)::xs) =
15.73 @@ -2458,7 +2439,6 @@
15.74 else
15.75 raise REFUTE ("IDT_recursion_interpreter",
15.76 "different type associations for the same dtyp"))
15.77 - (* (DatatypeAux.dtyp * Term.typ) list *)
15.78 val typ_assoc = filter
15.79 (fn (DatatypeAux.DtTFree _, _) => true | (_, _) => false)
15.80 (rec_typ_assoc []
15.81 @@ -2613,7 +2593,6 @@
15.82 val rec_dtyps_args = List.filter
15.83 (DatatypeAux.is_rec_type o fst) (dtyps ~~ args)
15.84 (* map those indices to interpretations *)
15.85 - (* (DatatypeAux.dtyp * interpretation) list *)
15.86 val rec_dtyps_intrs = map (fn (dtyp, arg) =>
15.87 let
15.88 val dT = typ_of_dtyp descr typ_assoc dtyp
15.89 @@ -2625,8 +2604,6 @@
15.90 (* takes the dtyp and interpretation of an element, *)
15.91 (* and computes the interpretation for the *)
15.92 (* corresponding recursive argument *)
15.93 - (* DatatypeAux.dtyp -> interpretation ->
15.94 - interpretation *)
15.95 fun rec_intr (DatatypeAux.DtRec i) (Leaf xs) =
15.96 (* recursive argument is "rec_i params elem" *)
15.97 compute_array_entry i (find_index_eq True xs)
15.98 @@ -3252,8 +3229,6 @@
15.99 (* constructor generates the datatype's element that is given by *)
15.100 (* 'element', returns the constructor (as a term) as well as the *)
15.101 (* indices of the arguments *)
15.102 - (* string * DatatypeAux.dtyp list ->
15.103 - (Term.term * int list) option *)
15.104 fun get_constr_args (cname, cargs) =
15.105 let
15.106 val cTerm = Const (cname,
15.107 @@ -3281,7 +3256,6 @@
15.108 in
15.109 Option.map (fn args => (cTerm, cargs, args)) (get_args iC)
15.110 end
15.111 - (* Term.term * DatatypeAux.dtyp list * int list *)
15.112 val (cTerm, cargs, args) =
15.113 (* we could speed things up by computing the correct *)
15.114 (* constructor directly (rather than testing all *)
16.1 --- a/src/HOL/Tools/typecopy.ML Sun Jun 21 15:47:41 2009 +0200
16.2 +++ b/src/HOL/Tools/typecopy.ML Sun Jun 21 19:09:31 2009 +0200
16.3 @@ -6,21 +6,13 @@
16.4
16.5 signature TYPECOPY =
16.6 sig
16.7 - type info = {
16.8 - vs: (string * sort) list,
16.9 - constr: string,
16.10 - typ: typ,
16.11 - inject: thm,
16.12 - proj: string * typ,
16.13 - proj_def: thm
16.14 - }
16.15 + type info = { vs: (string * sort) list, constr: string, typ: typ,
16.16 + inject: thm, proj: string * typ, proj_def: thm }
16.17 val typecopy: binding * string list -> typ -> (binding * binding) option
16.18 -> theory -> (string * info) * theory
16.19 - val get_typecopies: theory -> string list
16.20 val get_info: theory -> string -> info option
16.21 val interpretation: (string -> theory -> theory) -> theory -> theory
16.22 val add_default_code: string -> theory -> theory
16.23 - val print_typecopies: theory -> unit
16.24 val setup: theory -> theory
16.25 end;
16.26
16.27 @@ -47,22 +39,6 @@
16.28 fun merge _ = Symtab.merge (K true);
16.29 );
16.30
16.31 -fun print_typecopies thy =
16.32 - let
16.33 - val tab = TypecopyData.get thy;
16.34 - fun mk (tyco, { vs, constr, typ, proj = (proj, _), ... } : info) =
16.35 - (Pretty.block o Pretty.breaks) [
16.36 - Syntax.pretty_typ_global thy (Type (tyco, map TFree vs)),
16.37 - Pretty.str "=",
16.38 - (Pretty.str o Sign.extern_const thy) constr,
16.39 - Syntax.pretty_typ_global thy typ,
16.40 - Pretty.block [Pretty.str "(", (Pretty.str o Sign.extern_const thy) proj, Pretty.str ")"]];
16.41 - in
16.42 - (Pretty.writeln o Pretty.block o Pretty.fbreaks)
16.43 - (Pretty.str "type copies:" :: map mk (Symtab.dest tab))
16.44 - end;
16.45 -
16.46 -val get_typecopies = Symtab.keys o TypecopyData.get;
16.47 val get_info = Symtab.lookup o TypecopyData.get;
16.48
16.49
16.50 @@ -72,7 +48,7 @@
16.51 val interpretation = TypecopyInterpretation.interpretation;
16.52
16.53
16.54 -(* declaring typecopies *)
16.55 +(* introducing typecopies *)
16.56
16.57 fun typecopy (raw_tyco, raw_vs) raw_ty constr_proj thy =
16.58 let
17.1 --- a/src/HOL/Tools/typedef.ML Sun Jun 21 15:47:41 2009 +0200
17.2 +++ b/src/HOL/Tools/typedef.ML Sun Jun 21 19:09:31 2009 +0200
17.3 @@ -12,13 +12,13 @@
17.4 type_definition: thm, set_def: thm option, Rep: thm, Rep_inverse: thm,
17.5 Abs_inverse: thm, Rep_inject: thm, Abs_inject: thm, Rep_cases: thm, Abs_cases: thm,
17.6 Rep_induct: thm, Abs_induct: thm}
17.7 - val get_info: theory -> string -> info option
17.8 val add_typedef: bool -> binding option -> binding * string list * mixfix ->
17.9 term -> (binding * binding) option -> tactic -> theory -> (string * info) * theory
17.10 val typedef: (bool * binding) * (binding * string list * mixfix) * term
17.11 * (binding * binding) option -> theory -> Proof.state
17.12 val typedef_cmd: (bool * binding) * (binding * string list * mixfix) * string
17.13 * (binding * binding) option -> theory -> Proof.state
17.14 + val get_info: theory -> string -> info option
17.15 val interpretation: (string -> theory -> theory) -> theory -> theory
17.16 val setup: theory -> theory
17.17 end;
18.1 --- a/src/HOLCF/Fixrec.thy Sun Jun 21 15:47:41 2009 +0200
18.2 +++ b/src/HOLCF/Fixrec.thy Sun Jun 21 19:09:31 2009 +0200
18.3 @@ -6,7 +6,7 @@
18.4
18.5 theory Fixrec
18.6 imports Sprod Ssum Up One Tr Fix
18.7 -uses ("Tools/fixrec_package.ML")
18.8 +uses ("Tools/fixrec.ML")
18.9 begin
18.10
18.11 subsection {* Maybe monad type *}
18.12 @@ -599,12 +599,12 @@
18.13
18.14 subsection {* Initializing the fixrec package *}
18.15
18.16 -use "Tools/fixrec_package.ML"
18.17 +use "Tools/fixrec.ML"
18.18
18.19 -setup {* FixrecPackage.setup *}
18.20 +setup {* Fixrec.setup *}
18.21
18.22 setup {*
18.23 - FixrecPackage.add_matchers
18.24 + Fixrec.add_matchers
18.25 [ (@{const_name up}, @{const_name match_up}),
18.26 (@{const_name sinl}, @{const_name match_sinl}),
18.27 (@{const_name sinr}, @{const_name match_sinr}),
19.1 --- a/src/HOLCF/IOA/meta_theory/Abstraction.thy Sun Jun 21 15:47:41 2009 +0200
19.2 +++ b/src/HOLCF/IOA/meta_theory/Abstraction.thy Sun Jun 21 19:09:31 2009 +0200
19.3 @@ -6,7 +6,7 @@
19.4
19.5 theory Abstraction
19.6 imports LiveIOA
19.7 -uses ("ioa_package.ML")
19.8 +uses ("ioa.ML")
19.9 begin
19.10
19.11 defaultsort type
19.12 @@ -613,6 +613,6 @@
19.13
19.14 method_setup abstraction = {* Scan.succeed (SIMPLE_METHOD' o abstraction_tac) *} ""
19.15
19.16 -use "ioa_package.ML"
19.17 +use "ioa.ML"
19.18
19.19 end
20.1 --- a/src/HOLCF/IOA/meta_theory/ioa_package.ML Sun Jun 21 15:47:41 2009 +0200
20.2 +++ b/src/HOLCF/IOA/meta_theory/ioa_package.ML Sun Jun 21 19:09:31 2009 +0200
20.3 @@ -1,9 +1,8 @@
20.4 -(* Title: HOLCF/IOA/meta_theory/ioa_package.ML
20.5 - ID: $Id$
20.6 +(* Title: HOLCF/IOA/meta_theory/ioa.ML
20.7 Author: Tobias Hamberger, TU Muenchen
20.8 *)
20.9
20.10 -signature IOA_PACKAGE =
20.11 +signature IOA =
20.12 sig
20.13 val add_ioa: string -> string
20.14 -> (string) list -> (string) list -> (string) list
20.15 @@ -16,7 +15,7 @@
20.16 val add_rename : string -> string -> string -> theory -> theory
20.17 end;
20.18
20.19 -structure IoaPackage: IOA_PACKAGE =
20.20 +structure Ioa: IOA =
20.21 struct
20.22
20.23 val string_of_typ = PrintMode.setmp [] o Syntax.string_of_typ_global;
21.1 --- a/src/HOLCF/IsaMakefile Sun Jun 21 15:47:41 2009 +0200
21.2 +++ b/src/HOLCF/IsaMakefile Sun Jun 21 19:09:31 2009 +0200
21.3 @@ -67,8 +67,8 @@
21.4 Tools/domain/domain_library.ML \
21.5 Tools/domain/domain_syntax.ML \
21.6 Tools/domain/domain_theorems.ML \
21.7 - Tools/fixrec_package.ML \
21.8 - Tools/pcpodef_package.ML \
21.9 + Tools/fixrec.ML \
21.10 + Tools/pcpodef.ML \
21.11 holcf_logic.ML \
21.12 document/root.tex
21.13 @$(ISABELLE_TOOL) usedir -b -g true -r $(OUT)/HOL HOLCF
21.14 @@ -127,7 +127,7 @@
21.15 IOA/meta_theory/TL.thy IOA/meta_theory/TLS.thy \
21.16 IOA/meta_theory/LiveIOA.thy IOA/meta_theory/Pred.thy \
21.17 IOA/meta_theory/Abstraction.thy IOA/meta_theory/Simulations.thy \
21.18 - IOA/meta_theory/SimCorrectness.thy IOA/meta_theory/ioa_package.ML
21.19 + IOA/meta_theory/SimCorrectness.thy IOA/meta_theory/ioa.ML
21.20 @cd IOA; $(ISABELLE_TOOL) usedir -b $(OUT)/HOLCF IOA
21.21
21.22
22.1 --- a/src/HOLCF/Pcpodef.thy Sun Jun 21 15:47:41 2009 +0200
22.2 +++ b/src/HOLCF/Pcpodef.thy Sun Jun 21 19:09:31 2009 +0200
22.3 @@ -6,7 +6,7 @@
22.4
22.5 theory Pcpodef
22.6 imports Adm
22.7 -uses ("Tools/pcpodef_package.ML")
22.8 +uses ("Tools/pcpodef.ML")
22.9 begin
22.10
22.11 subsection {* Proving a subtype is a partial order *}
22.12 @@ -303,6 +303,6 @@
22.13
22.14 subsection {* HOLCF type definition package *}
22.15
22.16 -use "Tools/pcpodef_package.ML"
22.17 +use "Tools/pcpodef.ML"
22.18
22.19 end
23.1 --- a/src/HOLCF/Tools/domain/domain_axioms.ML Sun Jun 21 15:47:41 2009 +0200
23.2 +++ b/src/HOLCF/Tools/domain/domain_axioms.ML Sun Jun 21 19:09:31 2009 +0200
23.3 @@ -6,7 +6,7 @@
23.4
23.5 signature DOMAIN_AXIOMS =
23.6 sig
23.7 - val copy_of_dtyp : (int -> term) -> DatatypeAux.dtyp -> term
23.8 + val copy_of_dtyp : (int -> term) -> Datatype.dtyp -> term
23.9
23.10 val calc_axioms :
23.11 string -> Domain_Library.eq list -> int -> Domain_Library.eq ->
23.12 @@ -171,7 +171,7 @@
23.13 val mat_names = map mat_name con_names;
23.14 fun qualify n = Sign.full_name thy (Binding.name n);
23.15 val ms = map qualify con_names ~~ map qualify mat_names;
23.16 - in FixrecPackage.add_matchers ms thy end;
23.17 + in Fixrec.add_matchers ms thy end;
23.18
23.19 fun add_axioms comp_dnam (eqs : eq list) thy' =
23.20 let
24.1 --- a/src/HOLCF/Tools/domain/domain_library.ML Sun Jun 21 15:47:41 2009 +0200
24.2 +++ b/src/HOLCF/Tools/domain/domain_library.ML Sun Jun 21 19:09:31 2009 +0200
24.3 @@ -135,10 +135,10 @@
24.4 eqtype arg;
24.5 type cons = string * arg list;
24.6 type eq = (string * typ list) * cons list;
24.7 - val mk_arg : (bool * DatatypeAux.dtyp) * string option * string -> arg;
24.8 + val mk_arg : (bool * Datatype.dtyp) * string option * string -> arg;
24.9 val is_lazy : arg -> bool;
24.10 val rec_of : arg -> int;
24.11 - val dtyp_of : arg -> DatatypeAux.dtyp;
24.12 + val dtyp_of : arg -> Datatype.dtyp;
24.13 val sel_of : arg -> string option;
24.14 val vname : arg -> string;
24.15 val upd_vname : (string -> string) -> arg -> arg;
24.16 @@ -154,7 +154,7 @@
24.17 val idx_name : 'a list -> string -> int -> string;
24.18 val app_rec_arg : (int -> term) -> arg -> term;
24.19 val con_app : string -> arg list -> term;
24.20 - val dtyp_of_eq : eq -> DatatypeAux.dtyp;
24.21 + val dtyp_of_eq : eq -> Datatype.dtyp;
24.22
24.23
24.24 (* Name mangling *)
24.25 @@ -215,7 +215,7 @@
24.26 (* ----- constructor list handling ----- *)
24.27
24.28 type arg =
24.29 - (bool * DatatypeAux.dtyp) * (* (lazy, recursive element) *)
24.30 + (bool * Datatype.dtyp) * (* (lazy, recursive element) *)
24.31 string option * (* selector name *)
24.32 string; (* argument name *)
24.33
25.1 --- a/src/HOLCF/Tools/fixrec_package.ML Sun Jun 21 15:47:41 2009 +0200
25.2 +++ b/src/HOLCF/Tools/fixrec_package.ML Sun Jun 21 19:09:31 2009 +0200
25.3 @@ -1,10 +1,10 @@
25.4 -(* Title: HOLCF/Tools/fixrec_package.ML
25.5 +(* Title: HOLCF/Tools/fixrec.ML
25.6 Author: Amber Telfer and Brian Huffman
25.7
25.8 Recursive function definition package for HOLCF.
25.9 *)
25.10
25.11 -signature FIXREC_PACKAGE =
25.12 +signature FIXREC =
25.13 sig
25.14 val add_fixrec: bool -> (binding * typ option * mixfix) list
25.15 -> (Attrib.binding * term) list -> local_theory -> local_theory
25.16 @@ -16,7 +16,7 @@
25.17 val setup: theory -> theory
25.18 end;
25.19
25.20 -structure FixrecPackage :> FIXREC_PACKAGE =
25.21 +structure Fixrec :> FIXREC =
25.22 struct
25.23
25.24 val def_cont_fix_eq = @{thm def_cont_fix_eq};
25.25 @@ -327,7 +327,7 @@
25.26 (*************************************************************************)
25.27
25.28 local
25.29 -(* code adapted from HOL/Tools/primrec_package.ML *)
25.30 +(* code adapted from HOL/Tools/primrec.ML *)
25.31
25.32 fun gen_fixrec
25.33 (set_group : bool)
26.1 --- a/src/HOLCF/Tools/pcpodef_package.ML Sun Jun 21 15:47:41 2009 +0200
26.2 +++ b/src/HOLCF/Tools/pcpodef_package.ML Sun Jun 21 19:09:31 2009 +0200
26.3 @@ -1,11 +1,11 @@
26.4 -(* Title: HOLCF/Tools/pcpodef_package.ML
26.5 +(* Title: HOLCF/Tools/pcpodef.ML
26.6 Author: Brian Huffman
26.7
26.8 Primitive domain definitions for HOLCF, similar to Gordon/HOL-style
26.9 -typedef (see also ~~/src/HOL/Tools/typedef_package.ML).
26.10 +typedef (see also ~~/src/HOL/Tools/typedef.ML).
26.11 *)
26.12
26.13 -signature PCPODEF_PACKAGE =
26.14 +signature PCPODEF =
26.15 sig
26.16 val pcpodef_proof: (bool * binding) * (binding * string list * mixfix) * term
26.17 * (binding * binding) option -> theory -> Proof.state
26.18 @@ -17,7 +17,7 @@
26.19 * (binding * binding) option -> theory -> Proof.state
26.20 end;
26.21
26.22 -structure PcpodefPackage :> PCPODEF_PACKAGE =
26.23 +structure Pcpodef :> PCPODEF =
26.24 struct
26.25
26.26 (** type definitions **)