--- a/.hgignore Tue Jun 16 22:07:39 2009 -0700
+++ b/.hgignore Wed Jun 17 08:31:13 2009 +0200
@@ -8,6 +8,7 @@
syntax: regexp
+^contrib
^heaps/
^browser_info/
^doc-src/.*\.aux
--- a/src/HOL/Nominal/nominal_atoms.ML Tue Jun 16 22:07:39 2009 -0700
+++ b/src/HOL/Nominal/nominal_atoms.ML Wed Jun 17 08:31:13 2009 +0200
@@ -101,8 +101,9 @@
val (_,thy1) =
fold_map (fn ak => fn thy =>
let val dt = ([], Binding.name ak, NoSyn, [(Binding.name ak, [@{typ nat}], NoSyn)])
- val ({inject,case_thms,...},thy1) = DatatypePackage.add_datatype true false [ak] [dt] thy
- val inject_flat = Library.flat inject
+ val ({inject,case_thms,...},thy1) = DatatypePackage.add_datatype
+ DatatypeAux.default_datatype_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
--- a/src/HOL/Nominal/nominal_package.ML Tue Jun 16 22:07:39 2009 -0700
+++ b/src/HOL/Nominal/nominal_package.ML Wed Jun 17 08:31:13 2009 +0200
@@ -6,8 +6,9 @@
signature NOMINAL_PACKAGE =
sig
- val add_nominal_datatype : bool -> string list -> (string list * bstring * mixfix *
- (bstring * string list * mixfix) list) list -> theory -> theory
+ val add_nominal_datatype : DatatypeAux.datatype_config -> string list ->
+ (string list * bstring * mixfix *
+ (bstring * string list * mixfix) list) list -> theory -> theory
type descr
type nominal_datatype_info
val get_nominal_datatypes : theory -> nominal_datatype_info Symtab.table
@@ -190,7 +191,7 @@
fun fresh_star_const T U =
Const ("Nominal.fresh_star", HOLogic.mk_setT T --> U --> HOLogic.boolT);
-fun gen_add_nominal_datatype prep_typ err flat_names new_type_names dts thy =
+fun gen_add_nominal_datatype prep_typ config new_type_names dts thy =
let
(* this theory is used just for parsing *)
@@ -243,7 +244,7 @@
val full_new_type_names' = map (Sign.full_bname thy) new_type_names';
val ({induction, ...},thy1) =
- DatatypePackage.add_datatype err flat_names new_type_names' dts'' thy;
+ DatatypePackage.add_datatype config new_type_names' dts'' thy;
val SOME {descr, ...} = Symtab.lookup
(DatatypePackage.get_datatypes thy1) (hd full_new_type_names');
@@ -815,7 +816,7 @@
val (thy', defs', eqns') = Library.foldl (make_constr_def tname T T')
((Sign.add_path tname thy, defs, []), constrs ~~ constrs' ~~ constr_syntax)
in
- (parent_path flat_names thy', defs', eqns @ [eqns'], dist_lemmas @ [dist])
+ (parent_path (#flat_names config) thy', defs', eqns @ [eqns'], dist_lemmas @ [dist])
end;
val (thy8, constr_defs, constr_rep_eqns, dist_lemmas) = Library.foldl dt_constr_defs
@@ -1509,7 +1510,7 @@
val ({intrs = rec_intrs, elims = rec_elims, raw_induct = rec_induct, ...}, thy11) =
thy10 |>
InductivePackage.add_inductive_global (serial_string ())
- {quiet_mode = ! quiet_mode, verbose = false, kind = Thm.internalK,
+ {quiet_mode = #quiet config, verbose = false, kind = Thm.internalK,
alt_name = Binding.name big_rec_name, coind = false, no_elim = false, no_ind = false,
skip_mono = true, fork_mono = false}
(map (fn (s, T) => ((Binding.name s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
@@ -2067,7 +2068,7 @@
thy13
end;
-val add_nominal_datatype = gen_add_nominal_datatype DatatypePackage.read_typ true;
+val add_nominal_datatype = gen_add_nominal_datatype DatatypePackage.read_typ;
(* FIXME: The following stuff should be exported by DatatypePackage *)
@@ -2083,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 false names specs end;
+ in add_nominal_datatype DatatypeAux.default_datatype_config names specs end;
val _ =
OuterSyntax.command "nominal_datatype" "define inductive datatypes" K.thy_decl
--- a/src/HOL/Product_Type.thy Tue Jun 16 22:07:39 2009 -0700
+++ b/src/HOL/Product_Type.thy Wed Jun 17 08:31:13 2009 +0200
@@ -1,5 +1,4 @@
(* Title: HOL/Product_Type.thy
- ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
*)
--- a/src/HOL/Rational.thy Tue Jun 16 22:07:39 2009 -0700
+++ b/src/HOL/Rational.thy Wed Jun 17 08:31:13 2009 +0200
@@ -1048,7 +1048,7 @@
val p' = p div g;
val q' = q div g;
val r = (if one_of [true, false] then p' else ~ p',
- if p' = 0 then 0 else q')
+ if p' = 0 then 1 else q')
in
(r, fn () => term_of_rat r)
end;
@@ -1060,8 +1060,7 @@
consts_code
"of_int :: int \<Rightarrow> rat" ("\<module>rat'_of'_int")
attach {*
-fun rat_of_int 0 = (0, 0)
- | rat_of_int i = (i, 1);
+fun = rat_of_int i (i, 1);
*}
end
--- a/src/HOL/RealDef.thy Tue Jun 16 22:07:39 2009 -0700
+++ b/src/HOL/RealDef.thy Wed Jun 17 08:31:13 2009 +0200
@@ -1169,7 +1169,7 @@
val p' = p div g;
val q' = q div g;
val r = (if one_of [true, false] then p' else ~ p',
- if p' = 0 then 0 else q')
+ if p' = 0 then 1 else q')
in
(r, fn () => term_of_real r)
end;
@@ -1181,8 +1181,7 @@
consts_code
"of_int :: int \<Rightarrow> real" ("\<module>real'_of'_int")
attach {*
-fun real_of_int 0 = (0, 0)
- | real_of_int i = (i, 1);
+fun real_of_int i = (i, 1);
*}
end
--- a/src/HOL/Tools/datatype_package/datatype_abs_proofs.ML Tue Jun 16 22:07:39 2009 -0700
+++ b/src/HOL/Tools/datatype_package/datatype_abs_proofs.ML Wed Jun 17 08:31:13 2009 +0200
@@ -14,26 +14,29 @@
signature DATATYPE_ABS_PROOFS =
sig
- val prove_casedist_thms : string list ->
- DatatypeAux.descr list -> (string * sort) list -> thm ->
+ type datatype_config = DatatypeAux.datatype_config
+ type descr = DatatypeAux.descr
+ type datatype_info = DatatypeAux.datatype_info
+ val prove_casedist_thms : datatype_config -> string list ->
+ descr list -> (string * sort) list -> thm ->
attribute list -> theory -> thm list * theory
- val prove_primrec_thms : bool -> string list ->
- DatatypeAux.descr list -> (string * sort) list ->
- DatatypeAux.datatype_info Symtab.table -> thm list list -> thm list list ->
+ val prove_primrec_thms : datatype_config -> string list ->
+ descr list -> (string * sort) list ->
+ datatype_info Symtab.table -> thm list list -> thm list list ->
simpset -> thm -> theory -> (string list * thm list) * theory
- val prove_case_thms : bool -> string list ->
- DatatypeAux.descr list -> (string * sort) list ->
+ val prove_case_thms : datatype_config -> string list ->
+ descr list -> (string * sort) list ->
string list -> thm list -> theory -> (thm list list * string list) * theory
- val prove_split_thms : string list ->
- DatatypeAux.descr list -> (string * sort) list ->
+ val prove_split_thms : datatype_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 : string list -> DatatypeAux.descr list ->
+ val prove_nchotomys : datatype_config -> string list -> descr list ->
(string * sort) list -> thm list -> theory -> thm list * theory
- val prove_weak_case_congs : string list -> DatatypeAux.descr list ->
+ val prove_weak_case_congs : string list -> descr list ->
(string * sort) list -> theory -> thm list * theory
val prove_case_congs : string list ->
- DatatypeAux.descr list -> (string * sort) list ->
+ descr list -> (string * sort) list ->
thm list -> thm list list -> theory -> thm list * theory
end;
@@ -44,9 +47,9 @@
(************************ case distinction theorems ***************************)
-fun prove_casedist_thms new_type_names descr sorts induct case_names_exhausts thy =
+fun prove_casedist_thms (config : datatype_config) new_type_names descr sorts induct case_names_exhausts thy =
let
- val _ = message "Proving case distinction theorems ...";
+ val _ = message config "Proving case distinction theorems ...";
val descr' = List.concat descr;
val recTs = get_rec_types descr' sorts;
@@ -86,13 +89,13 @@
(*************************** primrec combinators ******************************)
-fun prove_primrec_thms flat_names new_type_names descr sorts
+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 =
let
- val _ = message "Constructing primrec combinators ...";
+ val _ = message config "Constructing primrec combinators ...";
val big_name = space_implode "_" new_type_names;
- val thy0 = add_path flat_names big_name thy;
+ val thy0 = add_path (#flat_names config) big_name thy;
val descr' = List.concat descr;
val recTs = get_rec_types descr' sorts;
@@ -153,7 +156,7 @@
val ({intrs = rec_intrs, elims = rec_elims, ...}, thy1) =
InductivePackage.add_inductive_global (serial_string ())
- {quiet_mode = ! quiet_mode, verbose = false, kind = Thm.internalK,
+ {quiet_mode = #quiet config, verbose = false, kind = Thm.internalK,
alt_name = Binding.name big_rec_name', coind = false, no_elim = false, no_ind = true,
skip_mono = true, fork_mono = false}
(map (fn (s, T) => ((Binding.name s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
@@ -162,7 +165,7 @@
(* prove uniqueness and termination of primrec combinators *)
- val _ = message "Proving termination and uniqueness of primrec functions ...";
+ val _ = message config "Proving termination and uniqueness of primrec functions ...";
fun mk_unique_tac ((tac, intrs), ((((i, (tname, _, constrs)), elim), T), T')) =
let
@@ -242,13 +245,13 @@
Const ("The", (T' --> HOLogic.boolT) --> T') $ absfree ("y", T',
set $ Free ("x", T) $ Free ("y", T'))))))
(reccomb_names ~~ reccombs ~~ rec_sets ~~ recTs ~~ rec_result_Ts))
- ||> parent_path flat_names
+ ||> parent_path (#flat_names config)
||> Theory.checkpoint;
(* prove characteristic equations for primrec combinators *)
- val _ = message "Proving characteristic theorems for primrec combinators ..."
+ val _ = message config "Proving characteristic theorems for primrec combinators ..."
val rec_thms = map (fn t => SkipProof.prove_global thy2 [] [] t
(fn _ => EVERY
@@ -272,11 +275,11 @@
(***************************** case combinators *******************************)
-fun prove_case_thms flat_names new_type_names descr sorts reccomb_names primrec_thms thy =
+fun prove_case_thms (config : datatype_config) new_type_names descr sorts reccomb_names primrec_thms thy =
let
- val _ = message "Proving characteristic theorems for case combinators ...";
+ val _ = message config "Proving characteristic theorems for case combinators ...";
- val thy1 = add_path flat_names (space_implode "_" new_type_names) thy;
+ val thy1 = add_path (#flat_names config) (space_implode "_" new_type_names) thy;
val descr' = List.concat descr;
val recTs = get_rec_types descr' sorts;
@@ -338,7 +341,7 @@
thy2
|> Context.the_theory o fold (fold Nitpick_Const_Simp_Thms.add_thm) case_thms
o Context.Theory
- |> parent_path flat_names
+ |> parent_path (#flat_names config)
|> store_thmss "cases" new_type_names case_thms
|-> (fn thmss => pair (thmss, case_names))
end;
@@ -346,12 +349,12 @@
(******************************* case splitting *******************************)
-fun prove_split_thms new_type_names descr sorts constr_inject dist_rewrites
+fun prove_split_thms (config : datatype_config) new_type_names descr sorts constr_inject dist_rewrites
casedist_thms case_thms thy =
let
- val _ = message "Proving equations for case splitting ...";
+ val _ = message config "Proving equations for case splitting ...";
- val descr' = List.concat descr;
+ val descr' = flat descr;
val recTs = get_rec_types descr' sorts;
val newTs = Library.take (length (hd descr), recTs);
@@ -395,9 +398,9 @@
(************************* additional theorems for TFL ************************)
-fun prove_nchotomys new_type_names descr sorts casedist_thms thy =
+fun prove_nchotomys (config : datatype_config) new_type_names descr sorts casedist_thms thy =
let
- val _ = message "Proving additional theorems for TFL ...";
+ val _ = message config "Proving additional theorems for TFL ...";
fun prove_nchotomy (t, exhaustion) =
let
--- a/src/HOL/Tools/datatype_package/datatype_aux.ML Tue Jun 16 22:07:39 2009 -0700
+++ b/src/HOL/Tools/datatype_package/datatype_aux.ML Wed Jun 17 08:31:13 2009 +0200
@@ -6,8 +6,9 @@
signature DATATYPE_AUX =
sig
- val quiet_mode : bool ref
- val message : string -> unit
+ type datatype_config
+ val default_datatype_config : datatype_config
+ val message : datatype_config -> string -> unit
val add_path : bool -> string -> theory -> theory
val parent_path : bool -> theory -> theory
@@ -67,8 +68,13 @@
structure DatatypeAux : DATATYPE_AUX =
struct
-val quiet_mode = ref false;
-fun message s = if !quiet_mode then () else writeln s;
+(* datatype option flags *)
+
+type datatype_config = { strict: bool, flat_names: bool, quiet: bool };
+val default_datatype_config : datatype_config =
+ { strict = true, flat_names = false, quiet = false };
+fun message ({ quiet, ...} : datatype_config) s =
+ if quiet then () else writeln s;
fun add_path flat_names s = if flat_names then I else Sign.add_path s;
fun parent_path flat_names = if flat_names then I else Sign.parent_path;
--- a/src/HOL/Tools/datatype_package/datatype_codegen.ML Tue Jun 16 22:07:39 2009 -0700
+++ b/src/HOL/Tools/datatype_package/datatype_codegen.ML Wed Jun 17 08:31:13 2009 +0200
@@ -426,7 +426,7 @@
(* register a datatype etc. *)
-fun add_all_code dtcos thy =
+fun add_all_code config dtcos thy =
let
val (vs :: _, coss) = (split_list o map (DatatypePackage.the_datatype_spec thy)) dtcos;
val any_css = map2 (mk_constr_consts thy vs) dtcos coss;
@@ -437,7 +437,7 @@
in
if null css then thy
else thy
- |> tap (fn _ => DatatypeAux.message "Registering datatype for code generator ...")
+ |> tap (fn _ => DatatypeAux.message config "Registering datatype for code generator ...")
|> fold Code.add_datatype css
|> fold_rev Code.add_default_eqn case_rewrites
|> fold Code.add_case certs
--- a/src/HOL/Tools/datatype_package/datatype_package.ML Tue Jun 16 22:07:39 2009 -0700
+++ b/src/HOL/Tools/datatype_package/datatype_package.ML Wed Jun 17 08:31:13 2009 +0200
@@ -6,6 +6,7 @@
signature DATATYPE_PACKAGE =
sig
+ type datatype_config = DatatypeAux.datatype_config
type datatype_info = DatatypeAux.datatype_info
type descr = DatatypeAux.descr
val get_datatypes : theory -> datatype_info Symtab.table
@@ -24,39 +25,23 @@
val strip_case : Proof.context -> bool -> term -> (term * (term * term) list) option
val read_typ: theory ->
(typ list * (string * sort) list) * string -> typ list * (string * sort) list
- val interpretation : (string list -> theory -> theory) -> theory -> theory
- val rep_datatype : ({distinct : thm list list,
- inject : thm list list,
- exhaustion : thm list,
- rec_thms : thm list,
- case_thms : thm list list,
- split_thms : (thm * thm) list,
- induction : thm,
- simps : thm list} -> Proof.context -> Proof.context) -> string list option -> term list
- -> theory -> Proof.state;
- val rep_datatype_cmd : string list option -> string list -> theory -> Proof.state;
- val add_datatype : bool -> bool -> string list -> (string list * binding * mixfix *
- (binding * typ list * mixfix) list) list -> theory ->
- {distinct : thm list list,
- inject : thm list list,
- exhaustion : thm list,
- rec_thms : thm list,
- case_thms : thm list list,
- split_thms : (thm * thm) list,
- induction : thm,
- simps : thm list} * theory
- val add_datatype_cmd : bool -> string list -> (string list * binding * mixfix *
- (binding * string list * mixfix) list) list -> theory ->
- {distinct : thm list list,
- inject : thm list list,
- exhaustion : thm list,
- rec_thms : thm list,
- case_thms : thm list list,
- split_thms : (thm * thm) list,
- induction : thm,
- simps : thm list} * theory
+ val interpretation : (datatype_config -> string list -> theory -> theory) -> theory -> theory
+ type rules = {distinct : thm list list,
+ inject : thm list list,
+ exhaustion : thm list,
+ rec_thms : thm list,
+ case_thms : thm list list,
+ split_thms : (thm * thm) list,
+ induction : thm,
+ simps : thm list}
+ val rep_datatype : datatype_config -> (rules -> Proof.context -> Proof.context)
+ -> string list option -> term list -> theory -> Proof.state;
+ val rep_datatype_cmd : string list option -> string list -> theory -> Proof.state
+ val add_datatype : datatype_config -> string list -> (string list * binding * mixfix *
+ (binding * typ list * mixfix) list) list -> theory -> rules * theory
+ val add_datatype_cmd : string list -> (string list * binding * mixfix *
+ (binding * string list * mixfix) list) list -> theory -> rules * theory
val setup: theory -> theory
- val quiet_mode : bool ref
val print_datatypes : theory -> unit
end;
@@ -65,8 +50,6 @@
open DatatypeAux;
-val quiet_mode = quiet_mode;
-
(* theory data *)
@@ -358,31 +341,41 @@
case_cong = case_cong,
weak_case_cong = weak_case_cong});
-structure DatatypeInterpretation = InterpretationFun(type T = string list val eq = op =);
-val interpretation = DatatypeInterpretation.interpretation;
+type rules = {distinct : thm list list,
+ inject : thm list list,
+ exhaustion : thm list,
+ rec_thms : thm list,
+ case_thms : thm list list,
+ split_thms : (thm * thm) list,
+ induction : thm,
+ simps : thm list}
+
+structure DatatypeInterpretation = InterpretationFun
+ (type T = datatype_config * string list val eq = eq_snd op =);
+fun interpretation f = DatatypeInterpretation.interpretation (uncurry f);
(******************* definitional introduction of datatypes *******************)
-fun add_datatype_def flat_names new_type_names descr sorts types_syntax constr_syntax dt_info
+fun add_datatype_def (config : datatype_config) new_type_names descr sorts types_syntax constr_syntax dt_info
case_names_induct case_names_exhausts thy =
let
- val _ = message ("Proofs for datatype(s) " ^ commas_quote new_type_names);
+ val _ = message config ("Proofs for datatype(s) " ^ commas_quote new_type_names);
val ((inject, distinct, dist_rewrites, simproc_dists, induct), thy2) = thy |>
- DatatypeRepProofs.representation_proofs flat_names dt_info new_type_names descr sorts
+ DatatypeRepProofs.representation_proofs config dt_info new_type_names descr sorts
types_syntax constr_syntax case_names_induct;
- val (casedist_thms, thy3) = DatatypeAbsProofs.prove_casedist_thms new_type_names descr
+ val (casedist_thms, thy3) = DatatypeAbsProofs.prove_casedist_thms config new_type_names descr
sorts induct case_names_exhausts thy2;
val ((reccomb_names, rec_thms), thy4) = DatatypeAbsProofs.prove_primrec_thms
- flat_names new_type_names descr sorts dt_info inject dist_rewrites
+ config new_type_names descr sorts dt_info inject dist_rewrites
(Simplifier.theory_context thy3 dist_ss) induct thy3;
val ((case_thms, case_names), thy6) = DatatypeAbsProofs.prove_case_thms
- flat_names new_type_names descr sorts reccomb_names rec_thms thy4;
- val (split_thms, thy7) = DatatypeAbsProofs.prove_split_thms new_type_names
+ config new_type_names descr sorts reccomb_names rec_thms thy4;
+ val (split_thms, thy7) = DatatypeAbsProofs.prove_split_thms config new_type_names
descr sorts inject dist_rewrites casedist_thms case_thms thy6;
- val (nchotomys, thy8) = DatatypeAbsProofs.prove_nchotomys new_type_names
+ val (nchotomys, thy8) = DatatypeAbsProofs.prove_nchotomys config new_type_names
descr sorts casedist_thms thy7;
val (case_congs, thy9) = DatatypeAbsProofs.prove_case_congs new_type_names
descr sorts nchotomys case_thms thy8;
@@ -406,7 +399,7 @@
|> add_cases_induct dt_infos induct
|> Sign.parent_path
|> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms) |> snd
- |> DatatypeInterpretation.data (map fst dt_infos);
+ |> DatatypeInterpretation.data (config, map fst dt_infos);
in
({distinct = distinct,
inject = inject,
@@ -421,7 +414,7 @@
(*********************** declare existing type as datatype *********************)
-fun prove_rep_datatype alt_names new_type_names descr sorts induct inject half_distinct thy =
+fun prove_rep_datatype (config : datatype_config) alt_names new_type_names descr sorts induct inject half_distinct thy =
let
val ((_, [induct']), _) =
Variable.importT_thms [induct] (Variable.thm_context induct);
@@ -440,19 +433,19 @@
val (case_names_induct, case_names_exhausts) =
(mk_case_names_induct descr, mk_case_names_exhausts descr (map #1 dtnames));
- val _ = message ("Proofs for datatype(s) " ^ commas_quote new_type_names);
+ val _ = message config ("Proofs for datatype(s) " ^ commas_quote new_type_names);
val (casedist_thms, thy2) = thy |>
- DatatypeAbsProofs.prove_casedist_thms new_type_names [descr] sorts induct
+ DatatypeAbsProofs.prove_casedist_thms config new_type_names [descr] sorts induct
case_names_exhausts;
val ((reccomb_names, rec_thms), thy3) = DatatypeAbsProofs.prove_primrec_thms
- false new_type_names [descr] sorts dt_info inject distinct
+ config new_type_names [descr] sorts dt_info inject distinct
(Simplifier.theory_context thy2 dist_ss) induct thy2;
- val ((case_thms, case_names), thy4) = DatatypeAbsProofs.prove_case_thms false
- new_type_names [descr] sorts reccomb_names rec_thms thy3;
+ val ((case_thms, case_names), thy4) = DatatypeAbsProofs.prove_case_thms
+ config new_type_names [descr] sorts reccomb_names rec_thms thy3;
val (split_thms, thy5) = DatatypeAbsProofs.prove_split_thms
- new_type_names [descr] sorts inject distinct casedist_thms case_thms thy4;
- val (nchotomys, thy6) = DatatypeAbsProofs.prove_nchotomys new_type_names
+ config new_type_names [descr] sorts inject distinct casedist_thms case_thms thy4;
+ val (nchotomys, thy6) = DatatypeAbsProofs.prove_nchotomys config new_type_names
[descr] sorts casedist_thms thy5;
val (case_congs, thy7) = DatatypeAbsProofs.prove_case_congs new_type_names
[descr] sorts nchotomys case_thms thy6;
@@ -482,7 +475,7 @@
|> Sign.parent_path
|> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)
|> snd
- |> DatatypeInterpretation.data (map fst dt_infos);
+ |> DatatypeInterpretation.data (config, map fst dt_infos);
in
({distinct = distinct,
inject = inject,
@@ -494,7 +487,7 @@
simps = simps}, thy11)
end;
-fun gen_rep_datatype prep_term after_qed alt_names raw_ts thy =
+fun gen_rep_datatype prep_term (config : datatype_config) after_qed alt_names raw_ts thy =
let
fun constr_of_term (Const (c, T)) = (c, T)
| constr_of_term t =
@@ -550,7 +543,7 @@
(*FIXME somehow dubious*)
in
ProofContext.theory_result
- (prove_rep_datatype alt_names new_type_names descr vs induct injs half_distincts)
+ (prove_rep_datatype config alt_names new_type_names descr vs induct injs half_distincts)
#-> after_qed
end;
in
@@ -560,13 +553,13 @@
end;
val rep_datatype = gen_rep_datatype Sign.cert_term;
-val rep_datatype_cmd = gen_rep_datatype Syntax.read_term_global (K I);
+val rep_datatype_cmd = gen_rep_datatype Syntax.read_term_global default_datatype_config (K I);
(******************************** add datatype ********************************)
-fun gen_add_datatype prep_typ err flat_names new_type_names dts thy =
+fun gen_add_datatype prep_typ (config : datatype_config) new_type_names dts thy =
let
val _ = Theory.requires thy "Datatype" "datatype definitions";
@@ -598,7 +591,7 @@
val _ = (case fold (curry OldTerm.add_typ_tfree_names) cargs' [] \\ tvs of
[] => ()
| vs => error ("Extra type variables on rhs: " ^ commas vs))
- in (constrs @ [((if flat_names then Sign.full_name tmp_thy else
+ in (constrs @ [((if #flat_names config then Sign.full_name tmp_thy else
Sign.full_name_path tmp_thy tname')
(Binding.map_name (Syntax.const_name mx') cname),
map (dtyp_of_typ new_dts) cargs')],
@@ -626,7 +619,7 @@
val dt_info = get_datatypes thy;
val (descr, _) = unfold_datatypes tmp_thy dts' sorts dt_info dts' i;
val _ = check_nonempty descr handle (exn as Datatype_Empty s) =>
- if err then error ("Nonemptiness check failed for datatype " ^ s)
+ if #strict config then error ("Nonemptiness check failed for datatype " ^ s)
else raise exn;
val descr' = flat descr;
@@ -634,12 +627,12 @@
val case_names_exhausts = mk_case_names_exhausts descr' (map #1 new_dts);
in
add_datatype_def
- flat_names new_type_names descr sorts types_syntax constr_syntax dt_info
+ (config : datatype_config) new_type_names descr sorts types_syntax constr_syntax dt_info
case_names_induct case_names_exhausts thy
end;
val add_datatype = gen_add_datatype cert_typ;
-val add_datatype_cmd = gen_add_datatype read_typ true;
+val add_datatype_cmd = gen_add_datatype read_typ default_datatype_config;
@@ -668,7 +661,7 @@
(fn ((((NONE, _), t), _), _) => Binding.name_of 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 snd o add_datatype_cmd false names specs end;
+ in snd o add_datatype_cmd names specs end;
val _ =
OuterSyntax.command "datatype" "define inductive datatypes" K.thy_decl
--- a/src/HOL/Tools/datatype_package/datatype_realizer.ML Tue Jun 16 22:07:39 2009 -0700
+++ b/src/HOL/Tools/datatype_package/datatype_realizer.ML Wed Jun 17 08:31:13 2009 +0200
@@ -7,7 +7,7 @@
signature DATATYPE_REALIZER =
sig
- val add_dt_realizers: string list -> theory -> theory
+ val add_dt_realizers: DatatypeAux.datatype_config -> string list -> theory -> theory
val setup: theory -> theory
end;
@@ -213,10 +213,10 @@
(exh_name, ([], Extraction.nullt, prf_of exhaustion))] thy'
end;
-fun add_dt_realizers names thy =
+fun add_dt_realizers config names thy =
if ! Proofterm.proofs < 2 then thy
else let
- val _ = message "Adding realizers for induction and case analysis ..."
+ val _ = message config "Adding realizers for induction and case analysis ..."
val infos = map (DatatypePackage.the_datatype thy) names;
val info :: _ = infos;
in
--- a/src/HOL/Tools/datatype_package/datatype_rep_proofs.ML Tue Jun 16 22:07:39 2009 -0700
+++ b/src/HOL/Tools/datatype_package/datatype_rep_proofs.ML Wed Jun 17 08:31:13 2009 +0200
@@ -11,10 +11,13 @@
signature DATATYPE_REP_PROOFS =
sig
+ type datatype_config = DatatypeAux.datatype_config
+ type descr = DatatypeAux.descr
+ type datatype_info = DatatypeAux.datatype_info
val distinctness_limit : int Config.T
val distinctness_limit_setup : theory -> theory
- val representation_proofs : bool -> DatatypeAux.datatype_info Symtab.table ->
- string list -> DatatypeAux.descr list -> (string * sort) list ->
+ val representation_proofs : datatype_config -> datatype_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 *
DatatypeAux.simproc_dist list * thm) * theory
@@ -45,7 +48,7 @@
(******************************************************************************)
-fun representation_proofs flat_names (dt_info : datatype_info Symtab.table)
+fun representation_proofs (config : datatype_config) (dt_info : datatype_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;
@@ -69,7 +72,7 @@
val descr' = flat descr;
val big_name = space_implode "_" new_type_names;
- val thy1 = add_path flat_names big_name thy;
+ val thy1 = add_path (#flat_names config) big_name thy;
val big_rec_name = big_name ^ "_rep_set";
val rep_set_names' =
(if length descr' = 1 then [big_rec_name] else
@@ -147,7 +150,7 @@
(************** generate introduction rules for representing set **********)
- val _ = message "Constructing representing sets ...";
+ val _ = message config "Constructing representing sets ...";
(* make introduction rule for a single constructor *)
@@ -181,7 +184,7 @@
val ({raw_induct = rep_induct, intrs = rep_intrs, ...}, thy2) =
InductivePackage.add_inductive_global (serial_string ())
- {quiet_mode = ! quiet_mode, verbose = false, kind = Thm.internalK,
+ {quiet_mode = #quiet config, verbose = false, kind = Thm.internalK,
alt_name = Binding.name big_rec_name, coind = false, no_elim = true, no_ind = false,
skip_mono = true, fork_mono = false}
(map (fn s => ((Binding.name s, UnivT'), NoSyn)) rep_set_names') []
@@ -190,7 +193,7 @@
(********************************* typedef ********************************)
val (typedefs, thy3) = thy2 |>
- parent_path flat_names |>
+ parent_path (#flat_names config) |>
fold_map (fn ((((name, mx), tvs), c), name') =>
TypedefPackage.add_typedef false (SOME (Binding.name name')) (name, tvs, mx)
(Collect $ Const (c, UnivT')) NONE
@@ -199,7 +202,7 @@
(resolve_tac rep_intrs 1)))
(types_syntax ~~ tyvars ~~
(Library.take (length newTs, rep_set_names)) ~~ new_type_names) ||>
- add_path flat_names big_name;
+ add_path (#flat_names config) big_name;
(*********************** definition of constructors ***********************)
@@ -257,19 +260,19 @@
val cong' = standard (cterm_instantiate [(cterm_of thy cong_f, rep_const)] arg_cong);
val dist = standard (cterm_instantiate [(cterm_of thy distinct_f, rep_const)] distinct_lemma);
val (thy', defs', eqns', _) = Library.foldl ((make_constr_def tname T) (length constrs))
- ((add_path flat_names tname thy, defs, [], 1), constrs ~~ constr_syntax)
+ ((add_path (#flat_names config) tname thy, defs, [], 1), constrs ~~ constr_syntax)
in
- (parent_path flat_names thy', defs', eqns @ [eqns'],
+ (parent_path (#flat_names config) thy', defs', eqns @ [eqns'],
rep_congs @ [cong'], dist_lemmas @ [dist])
end;
val (thy4, constr_defs, constr_rep_eqns, rep_congs, dist_lemmas) = Library.foldl dt_constr_defs
- ((thy3 |> Sign.add_consts_i iso_decls |> parent_path flat_names, [], [], [], []),
+ ((thy3 |> Sign.add_consts_i iso_decls |> parent_path (#flat_names config), [], [], [], []),
hd descr ~~ new_type_names ~~ newTs ~~ constr_syntax);
(*********** isomorphisms for new types (introduced by typedef) ***********)
- val _ = message "Proving isomorphism properties ...";
+ val _ = message config "Proving isomorphism properties ...";
val newT_iso_axms = map (fn (_, td) =>
(collect_simp (#Abs_inverse td), #Rep_inverse td,
@@ -358,7 +361,7 @@
in (thy', char_thms' @ char_thms) end;
val (thy5, iso_char_thms) = apfst Theory.checkpoint (List.foldr make_iso_defs
- (add_path flat_names big_name thy4, []) (tl descr));
+ (add_path (#flat_names config) big_name thy4, []) (tl descr));
(* prove isomorphism properties *)
@@ -496,7 +499,7 @@
(******************* freeness theorems for constructors *******************)
- val _ = message "Proving freeness of constructors ...";
+ val _ = message config "Proving freeness of constructors ...";
(* prove theorem Rep_i (Constr_j ...) = Inj_j ... *)
@@ -568,13 +571,13 @@
val ((constr_inject', distinct_thms'), thy6) =
thy5
- |> parent_path flat_names
+ |> parent_path (#flat_names config)
|> store_thmss "inject" new_type_names constr_inject
||>> store_thmss "distinct" new_type_names distinct_thms;
(*************************** induction theorem ****************************)
- val _ = message "Proving induction rule for datatypes ...";
+ val _ = message config "Proving induction rule for datatypes ...";
val Rep_inverse_thms = (map (fn (_, iso, _) => iso RS subst) newT_iso_axms) @
(map (fn r => r RS myinv_f_f RS subst) iso_inj_thms_unfolded);
--- a/src/HOL/Tools/function_package/fundef_package.ML Tue Jun 16 22:07:39 2009 -0700
+++ b/src/HOL/Tools/function_package/fundef_package.ML Wed Jun 17 08:31:13 2009 +0200
@@ -191,9 +191,7 @@
|> safe_mk_meta_eq)))
thy
-val case_cong = fold add_case_cong
-
-val setup_case_cong = DatatypePackage.interpretation case_cong
+val setup_case_cong = DatatypePackage.interpretation (K (fold add_case_cong))
(* setup *)
--- a/src/HOL/Tools/function_package/size.ML Tue Jun 16 22:07:39 2009 -0700
+++ b/src/HOL/Tools/function_package/size.ML Wed Jun 17 08:31:13 2009 +0200
@@ -218,7 +218,7 @@
(new_type_names ~~ size_names)) thy''
end;
-fun add_size_thms (new_type_names as name :: _) thy =
+fun add_size_thms config (new_type_names as name :: _) thy =
let
val info as {descr, alt_names, ...} = DatatypePackage.the_datatype thy name;
val prefix = Long_Name.map_base_name (K (space_implode "_"
--- a/src/HOL/Tools/inductive_realizer.ML Tue Jun 16 22:07:39 2009 -0700
+++ b/src/HOL/Tools/inductive_realizer.ML Wed Jun 17 08:31:13 2009 +0200
@@ -307,8 +307,8 @@
val ((dummies, dt_info), thy2) =
thy1
- |> add_dummies
- (DatatypePackage.add_datatype false false (map (Binding.name_of o #2) dts))
+ |> add_dummies (DatatypePackage.add_datatype
+ { strict = false, flat_names = false, quiet = false } (map (Binding.name_of o #2) dts))
(map (pair false) dts) []
||> Extraction.add_typeof_eqns_i ty_eqs
||> Extraction.add_realizes_eqns_i rlz_eqs;
--- a/src/HOL/Tools/quickcheck_generators.ML Tue Jun 16 22:07:39 2009 -0700
+++ b/src/HOL/Tools/quickcheck_generators.ML Wed Jun 17 08:31:13 2009 +0200
@@ -15,7 +15,7 @@
val mk_random_aux_eqs: theory -> DatatypeAux.descr -> (string * sort) list
-> string list -> string list * string list -> typ list * typ list
-> string * (term list * (term * term) list)
- val ensure_random_datatype: string list -> theory -> theory
+ val ensure_random_datatype: DatatypeAux.datatype_config -> string list -> theory -> theory
val eval_ref: (unit -> int -> seed -> term list option * seed) option ref
val setup: theory -> theory
end;
@@ -320,9 +320,9 @@
val prefix = space_implode "_" (random_auxN :: names);
in (prefix, (random_auxs, auxs_lhss ~~ auxs_rhss)) end;
-fun mk_random_datatype descr vs tycos (names, auxnames) (Ts, Us) thy =
+fun mk_random_datatype config descr vs tycos (names, auxnames) (Ts, Us) thy =
let
- val _ = DatatypeAux.message "Creating quickcheck generators ...";
+ val _ = DatatypeAux.message config "Creating quickcheck generators ...";
val i = @{term "i\<Colon>code_numeral"};
val mk_prop_eq = HOLogic.mk_Trueprop o HOLogic.mk_eq;
fun mk_size_arg k = case DatatypeCodegen.find_shortest_path descr k
@@ -356,7 +356,7 @@
in SOME (fn (v, _) => (v, (the o Vartab.lookup vtab) (v, 0)))
end handle CLASS_ERROR => NONE;
-fun ensure_random_datatype raw_tycos thy =
+fun ensure_random_datatype config raw_tycos thy =
let
val pp = Syntax.pp_global thy;
val algebra = Sign.classes_of thy;
@@ -370,7 +370,7 @@
can (Sorts.mg_domain algebra tyco) @{sort random}) tycos;
in if has_inst then thy
else case perhaps_constrain thy (random_insts @ term_of_insts) raw_vs
- of SOME constrain => mk_random_datatype descr
+ of SOME constrain => mk_random_datatype config descr
(map constrain raw_vs) tycos (names, auxnames)
((pairself o map o map_atyps) (fn TFree v => TFree (constrain v)) raw_TUs) thy
| NONE => thy
--- a/src/Tools/code/code_haskell.ML Tue Jun 16 22:07:39 2009 -0700
+++ b/src/Tools/code/code_haskell.ML Wed Jun 17 08:31:13 2009 +0200
@@ -106,11 +106,9 @@
|> pr_bind tyvars thm BR ((NONE, SOME pat), ty)
|>> (fn p => semicolon [p, str "=", pr_term tyvars thm vars NOBR t])
val (ps, vars') = fold_map pr binds vars;
- in
- Pretty.block_enclose (
- str "(let {",
- concat [str "}", str "in", pr_term tyvars thm vars' NOBR body, str ")"]
- ) ps
+ in brackify_block fxy (str "let {")
+ ps
+ (concat [str "}", str "in", pr_term tyvars thm vars' NOBR body])
end
| pr_case tyvars thm vars fxy (((t, ty), clauses as _ :: _), _) =
let
@@ -118,11 +116,10 @@
let
val (p, vars') = pr_bind tyvars thm NOBR ((NONE, SOME pat), ty) vars;
in semicolon [p, str "->", pr_term tyvars thm vars' NOBR body] end;
- in
- Pretty.block_enclose (
- concat [str "(case", pr_term tyvars thm vars NOBR t, str "of", str "{"],
- str "})"
- ) (map pr clauses)
+ in brackify_block fxy
+ (concat [str "case", pr_term tyvars thm vars NOBR t, str "of", str "{"])
+ (map pr clauses)
+ (str "}")
end
| pr_case tyvars thm vars fxy ((_, []), _) =
(brackify fxy o Pretty.breaks o map str) ["error", "\"empty case\""];
--- a/src/Tools/code/code_ml.ML Tue Jun 16 22:07:39 2009 -0700
+++ b/src/Tools/code/code_ml.ML Wed Jun 17 08:31:13 2009 +0200
@@ -151,7 +151,7 @@
concat [str delim, p, str "=>", pr_term is_closure thm vars' NOBR body]
end;
in
- (Pretty.enclose "(" ")" o single o brackify fxy) (
+ brackets (
str "case"
:: pr_term is_closure thm vars NOBR t
:: pr "of" clause
@@ -441,8 +441,10 @@
|>> (fn p => concat
[str "let", p, str "=", pr_term is_closure thm vars NOBR t, str "in"])
val (ps, vars') = fold_map pr binds vars;
- fun mk_brack (p :: ps) = Pretty.block [str "(", p] :: ps;
- in Pretty.chunks (mk_brack ps @| Pretty.block [pr_term is_closure thm vars' NOBR body, str ")"]) end
+ in
+ brackify_block fxy (Pretty.chunks ps) []
+ (pr_term is_closure thm vars' NOBR body)
+ end
| pr_case is_closure thm vars fxy (((t, ty), clause :: clauses), _) =
let
fun pr delim (pat, body) =
@@ -450,7 +452,7 @@
val (p, vars') = pr_bind is_closure thm NOBR ((NONE, SOME pat), ty) vars;
in concat [str delim, p, str "->", pr_term is_closure thm vars' NOBR body] end;
in
- (Pretty.enclose "(" ")" o single o brackify fxy) (
+ brackets (
str "match"
:: pr_term is_closure thm vars NOBR t
:: pr "with" clause
--- a/src/Tools/code/code_printer.ML Tue Jun 16 22:07:39 2009 -0700
+++ b/src/Tools/code/code_printer.ML Wed Jun 17 08:31:13 2009 +0200
@@ -45,6 +45,7 @@
val APP: fixity
val brackify: fixity -> Pretty.T list -> Pretty.T
val brackify_infix: int * lrx -> fixity -> Pretty.T list -> Pretty.T
+ val brackify_block: fixity -> Pretty.T -> Pretty.T list -> Pretty.T -> Pretty.T
type itype = Code_Thingol.itype
type iterm = Code_Thingol.iterm
@@ -175,6 +176,13 @@
fun brackify_infix infx fxy_ctxt =
gen_brackify (fixity (INFX infx) fxy_ctxt) o Pretty.breaks;
+fun brackify_block fxy_ctxt p1 ps p2 =
+ let val p = Pretty.block_enclose (p1, p2) ps
+ in if fixity BR fxy_ctxt
+ then Pretty.enclose "(" ")" [p]
+ else p
+ end;
+
(* generic syntax *)