--- a/src/HOL/Nominal/nominal_package.ML Sat Jan 10 01:06:32 2009 +0100
+++ b/src/HOL/Nominal/nominal_package.ML Sat Jan 10 01:28:31 2009 +0100
@@ -571,7 +571,7 @@
InductivePackage.add_inductive_global (serial_string ())
{quiet_mode = false, verbose = false, kind = Thm.internalK,
alt_name = Binding.name big_rep_name, coind = false, no_elim = true, no_ind = false,
- skip_mono = true}
+ skip_mono = true, fork_mono = false}
(map (fn (s, T) => ((Binding.name s, T --> HOLogic.boolT), NoSyn))
(rep_set_names' ~~ recTs'))
[] (map (fn x => (Attrib.empty_binding, x)) intr_ts) [] thy3;
@@ -1509,7 +1509,7 @@
InductivePackage.add_inductive_global (serial_string ())
{quiet_mode = ! quiet_mode, verbose = false, kind = Thm.internalK,
alt_name = Binding.name big_rec_name, coind = false, no_elim = false, no_ind = false,
- skip_mono = true}
+ skip_mono = true, fork_mono = false}
(map (fn (s, T) => ((Binding.name s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
(map dest_Free rec_fns)
(map (fn x => (Attrib.empty_binding, x)) rec_intr_ts) [] ||>
--- a/src/HOL/Tools/datatype_abs_proofs.ML Sat Jan 10 01:06:32 2009 +0100
+++ b/src/HOL/Tools/datatype_abs_proofs.ML Sat Jan 10 01:28:31 2009 +0100
@@ -155,7 +155,7 @@
InductivePackage.add_inductive_global (serial_string ())
{quiet_mode = ! quiet_mode, verbose = false, kind = Thm.internalK,
alt_name = Binding.name big_rec_name', coind = false, no_elim = false, no_ind = true,
- skip_mono = true}
+ skip_mono = true, fork_mono = false}
(map (fn (s, T) => ((Binding.name s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
(map dest_Free rec_fns)
(map (fn x => (Attrib.empty_binding, x)) rec_intr_ts) [] thy0;
--- a/src/HOL/Tools/datatype_rep_proofs.ML Sat Jan 10 01:06:32 2009 +0100
+++ b/src/HOL/Tools/datatype_rep_proofs.ML Sat Jan 10 01:28:31 2009 +0100
@@ -183,7 +183,7 @@
InductivePackage.add_inductive_global (serial_string ())
{quiet_mode = ! quiet_mode, verbose = false, kind = Thm.internalK,
alt_name = Binding.name big_rec_name, coind = false, no_elim = true, no_ind = false,
- skip_mono = true}
+ skip_mono = true, fork_mono = false}
(map (fn s => ((Binding.name s, UnivT'), NoSyn)) rep_set_names') []
(map (fn x => (Attrib.empty_binding, x)) intr_ts) [] thy1;
--- a/src/HOL/Tools/function_package/inductive_wrap.ML Sat Jan 10 01:06:32 2009 +0100
+++ b/src/HOL/Tools/function_package/inductive_wrap.ML Sat Jan 10 01:28:31 2009 +0100
@@ -48,7 +48,8 @@
coind = false,
no_elim = false,
no_ind = false,
- skip_mono = true}
+ skip_mono = true,
+ fork_mono = false}
[((Binding.name R, T), NoSyn)] (* the relation *)
[] (* no parameters *)
(map (fn t => (Attrib.empty_binding, t)) defs) (* the intros *)
--- a/src/HOL/Tools/inductive_package.ML Sat Jan 10 01:06:32 2009 +0100
+++ b/src/HOL/Tools/inductive_package.ML Sat Jan 10 01:28:31 2009 +0100
@@ -46,7 +46,7 @@
(Binding.T * string option * mixfix) list ->
(Attrib.binding * string) list ->
(Facts.ref * Attrib.src list) list ->
- local_theory -> inductive_result * local_theory
+ bool -> local_theory -> inductive_result * local_theory
val add_inductive_global: string -> inductive_flags ->
((Binding.T * typ) * mixfix) list -> (string * typ) list -> (Attrib.binding * term) list ->
thm list -> theory -> inductive_result * theory
@@ -74,9 +74,9 @@
(Binding.T * string option * mixfix) list ->
(Binding.T * string option * mixfix) list ->
(Attrib.binding * string) list -> (Facts.ref * Attrib.src list) list ->
- local_theory -> inductive_result * local_theory
+ bool -> local_theory -> inductive_result * local_theory
val gen_ind_decl: add_ind_def -> bool ->
- OuterParse.token list -> (local_theory -> local_theory) * OuterParse.token list
+ OuterParse.token list -> (bool -> local_theory -> local_theory) * OuterParse.token list
end;
structure InductivePackage: INDUCTIVE_PACKAGE =
@@ -312,10 +312,11 @@
(* prove monotonicity *)
-fun prove_mono quiet_mode skip_mono predT fp_fun monos ctxt =
- (message (quiet_mode orelse skip_mono andalso !quick_and_dirty)
+fun prove_mono quiet_mode skip_mono fork_mono predT fp_fun monos ctxt =
+ (message (quiet_mode orelse skip_mono andalso !quick_and_dirty orelse fork_mono)
" Proving monotonicity ...";
- (if skip_mono then SkipProof.prove else Goal.prove) ctxt [] []
+ (if skip_mono then SkipProof.prove else if fork_mono then Goal.prove_future else Goal.prove) ctxt
+ [] []
(HOLogic.mk_Trueprop
(Const (@{const_name Orderings.mono}, (predT --> predT) --> HOLogic.boolT) $ fp_fun))
(fn _ => EVERY [rtac @{thm monoI} 1,
@@ -582,7 +583,7 @@
(** specification of (co)inductive predicates **)
-fun mk_ind_def quiet_mode skip_mono alt_name coind cs intr_ts monos params cnames_syn ctxt =
+fun mk_ind_def quiet_mode skip_mono fork_mono alt_name coind cs intr_ts monos params cnames_syn ctxt =
let
val fp_name = if coind then @{const_name Inductive.gfp} else @{const_name Inductive.lfp};
@@ -662,9 +663,11 @@
val (consts_defs, ctxt'') = fold_map (LocalTheory.define Thm.internalK) specs ctxt';
val preds = (case cs of [_] => [rec_const] | _ => map #1 consts_defs);
- val mono = prove_mono quiet_mode skip_mono predT fp_fun monos ctxt''
+ val mono = prove_mono quiet_mode skip_mono fork_mono predT fp_fun monos ctxt'';
+ val ((_, [mono']), ctxt''') =
+ LocalTheory.note Thm.internalK (Attrib.empty_binding, [mono]) ctxt'';
- in (ctxt'', rec_name, mono, fp_def', map (#2 o #2) consts_defs,
+ in (ctxt''', rec_name, mono', fp_def', map (#2 o #2) consts_defs,
list_comb (rec_const, params), preds, argTs, bs, xs)
end;
@@ -718,7 +721,7 @@
type inductive_flags =
{quiet_mode: bool, verbose: bool, kind: string, alt_name: Binding.T,
- coind: bool, no_elim: bool, no_ind: bool, skip_mono: bool}
+ coind: bool, no_elim: bool, no_ind: bool, skip_mono: bool, fork_mono: bool}
type add_ind_def =
inductive_flags ->
@@ -726,7 +729,7 @@
term list -> (Binding.T * mixfix) list ->
local_theory -> inductive_result * local_theory
-fun add_ind_def {quiet_mode, verbose, kind, alt_name, coind, no_elim, no_ind, skip_mono}
+fun add_ind_def {quiet_mode, verbose, kind, alt_name, coind, no_elim, no_ind, skip_mono, fork_mono}
cs intros monos params cnames_syn ctxt =
let
val _ = null cnames_syn andalso error "No inductive predicates given";
@@ -739,7 +742,7 @@
apfst split_list (split_list (map (check_rule ctxt cs params) intros));
val (ctxt1, rec_name, mono, fp_def, rec_preds_defs, rec_const, preds,
- argTs, bs, xs) = mk_ind_def quiet_mode skip_mono alt_name coind cs intr_ts
+ argTs, bs, xs) = mk_ind_def quiet_mode skip_mono fork_mono alt_name coind cs intr_ts
monos params cnames_syn ctxt;
val (intrs, unfold) = prove_intrs quiet_mode coind mono fp_def (length bs + length xs)
@@ -780,7 +783,7 @@
(* external interfaces *)
fun gen_add_inductive_i mk_def
- (flags as {quiet_mode, verbose, kind, alt_name, coind, no_elim, no_ind, skip_mono})
+ (flags as {quiet_mode, verbose, kind, alt_name, coind, no_elim, no_ind, skip_mono, fork_mono})
cnames_syn pnames spec monos lthy =
let
val thy = ProofContext.theory_of lthy;
@@ -836,7 +839,7 @@
||> fold (snd oo LocalTheory.abbrev Syntax.mode_default) abbrevs
end;
-fun gen_add_inductive mk_def verbose coind cnames_syn pnames_syn intro_srcs raw_monos lthy =
+fun gen_add_inductive mk_def verbose coind cnames_syn pnames_syn intro_srcs raw_monos int lthy =
let
val ((vars, specs), _) = lthy |> ProofContext.set_mode ProofContext.mode_abbrev
|> Specification.read_specification
@@ -845,7 +848,8 @@
val intrs = map (apsnd the_single) specs;
val monos = Attrib.eval_thms lthy raw_monos;
val flags = {quiet_mode = false, verbose = verbose, kind = Thm.theoremK,
- alt_name = Binding.empty, coind = coind, no_elim = false, no_ind = false, skip_mono = false};
+ alt_name = Binding.empty, coind = coind, no_elim = false, no_ind = false,
+ skip_mono = false, fork_mono = not int};
in
lthy
|> LocalTheory.set_group (serial_string ())
@@ -956,12 +960,12 @@
Scan.optional (P.$$$ "where" |-- P.!!! SpecParse.specification) [] --
Scan.optional (P.$$$ "monos" |-- P.!!! SpecParse.xthms1) []
>> (fn (((preds, params), specs), monos) =>
- (snd o gen_add_inductive mk_def true coind preds params (flatten_specification specs) monos));
+ (snd oo gen_add_inductive mk_def true coind preds params (flatten_specification specs) monos));
val ind_decl = gen_ind_decl add_ind_def;
-val _ = OuterSyntax.local_theory "inductive" "define inductive predicates" K.thy_decl (ind_decl false);
-val _ = OuterSyntax.local_theory "coinductive" "define coinductive predicates" K.thy_decl (ind_decl true);
+val _ = OuterSyntax.local_theory' "inductive" "define inductive predicates" K.thy_decl (ind_decl false);
+val _ = OuterSyntax.local_theory' "coinductive" "define coinductive predicates" K.thy_decl (ind_decl true);
val _ =
OuterSyntax.local_theory "inductive_cases"
--- a/src/HOL/Tools/inductive_realizer.ML Sat Jan 10 01:06:32 2009 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML Sat Jan 10 01:28:31 2009 +0100
@@ -347,7 +347,7 @@
val (ind_info, thy3') = thy2 |>
InductivePackage.add_inductive_global (serial_string ())
{quiet_mode = false, verbose = false, kind = Thm.theoremK, alt_name = Binding.empty,
- coind = false, no_elim = false, no_ind = false, skip_mono = false}
+ coind = false, no_elim = false, no_ind = false, skip_mono = false, fork_mono = false}
rlzpreds rlzparams (map (fn (rintr, intr) =>
((Binding.name (Sign.base_name (name_of_thm intr)), []),
subst_atomic rlzpreds' (Logic.unvarify rintr)))
--- a/src/HOL/Tools/inductive_set_package.ML Sat Jan 10 01:06:32 2009 +0100
+++ b/src/HOL/Tools/inductive_set_package.ML Sat Jan 10 01:28:31 2009 +0100
@@ -20,7 +20,7 @@
(Binding.T * string option * mixfix) list ->
(Binding.T * string option * mixfix) list ->
(Attrib.binding * string) list -> (Facts.ref * Attrib.src list) list ->
- local_theory -> InductivePackage.inductive_result * local_theory
+ bool -> local_theory -> InductivePackage.inductive_result * local_theory
val codegen_preproc: theory -> thm list -> thm list
val setup: theory -> theory
end;
@@ -403,7 +403,8 @@
(**** definition of inductive sets ****)
-fun add_ind_set_def {quiet_mode, verbose, kind, alt_name, coind, no_elim, no_ind, skip_mono}
+fun add_ind_set_def
+ {quiet_mode, verbose, kind, alt_name, coind, no_elim, no_ind, skip_mono, fork_mono}
cs intros monos params cnames_syn ctxt =
let
val thy = ProofContext.theory_of ctxt;
@@ -468,7 +469,8 @@
val ({preds, intrs, elims, raw_induct, ...}, ctxt1) =
InductivePackage.add_ind_def
{quiet_mode = quiet_mode, verbose = verbose, kind = kind, alt_name = Binding.empty,
- coind = coind, no_elim = no_elim, no_ind = no_ind, skip_mono = skip_mono}
+ coind = coind, no_elim = no_elim, no_ind = no_ind,
+ skip_mono = skip_mono, fork_mono = fork_mono}
cs' intros' monos' params1 cnames_syn' ctxt;
(* define inductive sets using previously defined predicates *)
@@ -550,10 +552,10 @@
val ind_set_decl = InductivePackage.gen_ind_decl add_ind_set_def;
val _ =
- OuterSyntax.local_theory "inductive_set" "define inductive sets" K.thy_decl (ind_set_decl false);
+ OuterSyntax.local_theory' "inductive_set" "define inductive sets" K.thy_decl (ind_set_decl false);
val _ =
- OuterSyntax.local_theory "coinductive_set" "define coinductive sets" K.thy_decl (ind_set_decl true);
+ OuterSyntax.local_theory' "coinductive_set" "define coinductive sets" K.thy_decl (ind_set_decl true);
end;
--- a/src/Pure/General/lazy.ML Sat Jan 10 01:06:32 2009 +0100
+++ b/src/Pure/General/lazy.ML Sat Jan 10 01:28:31 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/General/lazy.ML
- ID: $Id$
Author: Florian Haftmann and Makarius, TU Muenchen
Lazy evaluation with memoing. Concurrency may lead to multiple
@@ -13,6 +12,7 @@
val lazy: (unit -> 'a) -> 'a lazy
val value: 'a -> 'a lazy
val peek: 'a lazy -> 'a Exn.result option
+ val force_result: 'a lazy -> 'a Exn.result
val force: 'a lazy -> 'a
val map_force: ('a -> 'a) -> 'a lazy -> 'a lazy
end
@@ -41,7 +41,7 @@
(* force result *)
-fun force r =
+fun force_result r =
let
(*potentially concurrent evaluation*)
val res =
@@ -53,7 +53,9 @@
(case ! r of
Lazy _ => (r := Result res; res)
| Result res' => res'));
- in Exn.release res' end;
+ in res' end;
+
+fun force r = Exn.release (force_result r);
fun map_force f = value o f o force;
--- a/src/Pure/General/markup.ML Sat Jan 10 01:06:32 2009 +0100
+++ b/src/Pure/General/markup.ML Sat Jan 10 01:28:31 2009 +0100
@@ -85,8 +85,9 @@
val subgoalN: string val subgoal: T
val sendbackN: string val sendback: T
val hiliteN: string val hilite: T
+ val taskN: string
val unprocessedN: string val unprocessed: T
- val runningN: string val running: T
+ val runningN: string val running: string -> T
val failedN: string val failed: T
val finishedN: string val finished: T
val disposedN: string val disposed: T
@@ -259,8 +260,10 @@
(* command status *)
+val taskN = "task";
+
val (unprocessedN, unprocessed) = markup_elem "unprocessed";
-val (runningN, running) = markup_elem "running";
+val (runningN, running) = markup_string "running" taskN;
val (failedN, failed) = markup_elem "failed";
val (finishedN, finished) = markup_elem "finished";
val (disposedN, disposed) = markup_elem "disposed";
--- a/src/Pure/General/markup.scala Sat Jan 10 01:06:32 2009 +0100
+++ b/src/Pure/General/markup.scala Sat Jan 10 01:28:31 2009 +0100
@@ -110,6 +110,8 @@
/* command status */
+ val TASK = "task"
+
val UNPROCESSED = "unprocessed"
val RUNNING = "running"
val FAILED = "failed"
--- a/src/Pure/Isar/isar.ML Sat Jan 10 01:06:32 2009 +0100
+++ b/src/Pure/Isar/isar.ML Sat Jan 10 01:28:31 2009 +0100
@@ -194,7 +194,7 @@
Finished of Toplevel.state;
fun status_markup Unprocessed = Markup.unprocessed
- | status_markup Running = Markup.running
+ | status_markup Running = (Markup.runningN, [])
| status_markup (Failed _) = Markup.failed
| status_markup (Finished _) = Markup.finished;
--- a/src/Pure/Isar/proof.ML Sat Jan 10 01:06:32 2009 +0100
+++ b/src/Pure/Isar/proof.ML Sat Jan 10 01:28:31 2009 +0100
@@ -345,7 +345,8 @@
(case filter_out (fn s => s = "") strs of [] => ""
| strs' => enclose " (" ")" (commas strs'));
- fun prt_goal (SOME (ctxt, (i, {statement = ((_, pos), _, _), messages, using, goal, before_qed, after_qed}))) =
+ fun prt_goal (SOME (ctxt, (i,
+ {statement = ((_, pos), _, _), messages, using, goal, before_qed = _, after_qed = _}))) =
pretty_facts "using " ctxt
(if mode <> Backward orelse null using then NONE else SOME using) @
[Pretty.str ("goal" ^
--- a/src/Pure/Thy/thy_info.ML Sat Jan 10 01:06:32 2009 +0100
+++ b/src/Pure/Thy/thy_info.ML Sat Jan 10 01:28:31 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/Thy/thy_info.ML
- ID: $Id$
Author: Markus Wenzel, TU Muenchen
Main part of theory loader database, including handling of theory and
@@ -24,6 +23,8 @@
val get_parents: string -> string list
val touch_thy: string -> unit
val touch_child_thys: string -> unit
+ val remove_thy: string -> unit
+ val kill_thy: string -> unit
val provide_file: Path.T -> string -> unit
val load_file: bool -> Path.T -> unit
val exec_file: bool -> Path.T -> Context.generic -> Context.generic
@@ -32,8 +33,6 @@
val use_thys: string list -> unit
val use_thy: string -> unit
val time_use_thy: string -> unit
- val remove_thy: string -> unit
- val kill_thy: string -> unit
val thy_ord: theory * theory -> order
val begin_theory: string -> string list -> (Path.T * bool) list -> bool -> theory
val end_theory: theory -> unit
@@ -232,6 +231,27 @@
end;
+(* remove theory *)
+
+fun remove_thy name =
+ if is_finished name then error (loader_msg "cannot remove finished theory" [name])
+ else
+ let val succs = thy_graph Graph.all_succs [name] in
+ priority (loader_msg "removing" succs);
+ CRITICAL (fn () => (List.app (perform Remove) succs; change_thys (Graph.del_nodes succs)))
+ end;
+
+val kill_thy = if_known_thy remove_thy;
+
+fun consolidate_thy name =
+ (case lookup_theory name of
+ NONE => []
+ | SOME thy =>
+ (case PureThy.join_proofs thy of
+ [] => []
+ | exns => (kill_thy name; exns)));
+
+
(* load_file *)
local
@@ -342,7 +362,7 @@
in (x, Symtab.update (name, x) tab) end;
val thy_results = Future.join_results (#1 (fold_map future tasks Symtab.empty));
- val proof_results = PureThy.join_proofs (map_filter (try get_theory o #1) tasks);
+ val proof_results = map Exn.Exn (maps (consolidate_thy o #1) tasks);
in ignore (Exn.release_all (thy_results @ proof_results)) end;
in
@@ -464,19 +484,6 @@
end;
-(* remove theory *)
-
-fun remove_thy name =
- if is_finished name then error (loader_msg "cannot remove finished theory" [name])
- else
- let val succs = thy_graph Graph.all_succs [name] in
- priority (loader_msg "removing" succs);
- CRITICAL (fn () => (List.app (perform Remove) succs; change_thys (Graph.del_nodes succs)))
- end;
-
-val kill_thy = if_known_thy remove_thy;
-
-
(* update_time *)
structure UpdateTime = TheoryDataFun
--- a/src/Pure/Thy/thy_load.ML Sat Jan 10 01:06:32 2009 +0100
+++ b/src/Pure/Thy/thy_load.ML Sat Jan 10 01:28:31 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/Thy/thy_load.ML
- ID: $Id$
Author: Markus Wenzel, TU Muenchen
Theory loader primitives, including load path.
@@ -22,6 +21,7 @@
val ml_exts: string list
val ml_path: string -> Path.T
val thy_path: string -> Path.T
+ val split_thy_path: Path.T -> Path.T * string
val check_file: Path.T -> Path.T -> (Path.T * File.ident) option
val check_ml: Path.T -> Path.T -> (Path.T * File.ident) option
val check_thy: Path.T -> string -> Path.T * File.ident
@@ -62,6 +62,11 @@
val ml_path = Path.ext "ML" o Path.basic;
val thy_path = Path.ext "thy" o Path.basic;
+fun split_thy_path path =
+ (case Path.split_ext path of
+ (path', "thy") => (Path.dir path', Path.implode (Path.base path'))
+ | _ => error ("Bad theory file specification " ^ Path.implode path));
+
(* check files *)
--- a/src/Pure/pure_thy.ML Sat Jan 10 01:06:32 2009 +0100
+++ b/src/Pure/pure_thy.ML Sat Jan 10 01:28:31 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/pure_thy.ML
- ID: $Id$
Author: Markus Wenzel, TU Muenchen
Theorem storage. Pure theory syntax and logical content.
@@ -11,7 +10,7 @@
val intern_fact: theory -> xstring -> string
val defined_fact: theory -> string -> bool
val hide_fact: bool -> string -> theory -> theory
- val join_proofs: theory list -> unit Exn.result list
+ val join_proofs: theory -> exn list
val get_fact: Context.generic -> theory -> Facts.ref -> thm list
val get_thms: theory -> xstring -> thm list
val get_thm: theory -> xstring -> thm
@@ -81,7 +80,8 @@
fun lazy_proof thm = Lazy.lazy (fn () => Thm.join_proof thm);
-val join_proofs = maps (fn thy => map (Exn.capture Lazy.force) (rev (#2 (FactsData.get thy))));
+fun join_proofs thy =
+ map_filter (Exn.get_exn o Lazy.force_result) (rev (#2 (FactsData.get thy)));