merged.
--- a/CONTRIBUTORS Thu Jan 08 12:25:22 2009 -0800
+++ b/CONTRIBUTORS Thu Jan 08 21:13:40 2009 -0800
@@ -7,12 +7,19 @@
Contributions to this Isabelle version
--------------------------------------
+* December 2008: Clemens Ballarin, TUM
+ New locale implementation.
+
* December 2008: Armin Heller, TUM and Alexander Krauss, TUM
Method "sizechange" for advanced termination proofs.
* November 2008: Timothy Bourke, NICTA
Performance improvement (factor 50) for find_theorems.
+* 2008: Florian Haftmann, TUM
+ Various extensions and restructurings in HOL, improvements
+ in evaluation mechanisms, new module binding.ML for name bindings.
+
* October 2008: Fabian Immler, TUM
ATP manager for Sledgehammer, based on ML threads instead of Posix
processes. Additional ATP wrappers, including remote SystemOnTPTP
--- a/NEWS Thu Jan 08 12:25:22 2009 -0800
+++ b/NEWS Thu Jan 08 21:13:40 2009 -0800
@@ -236,6 +236,13 @@
src/HOL/Real/rat_arith.ML ~> src/HOL/Tools
src/HOL/Real/real_arith.ML ~> src/HOL/Tools
+ src/HOL/Library/Array.thy ~> src/HOL/Imperative_HOL
+ src/HOL/Library/Heap_Monad.thy ~> src/HOL/Imperative_HOL
+ src/HOL/Library/Heap.thy ~> src/HOL/Imperative_HOL
+ src/HOL/Library/Imperative_HOL.thy ~> src/HOL/Imperative_HOL
+ src/HOL/Library/Ref.thy ~> src/HOL/Imperative_HOL
+ src/HOL/Library/Relational.thy ~> src/HOL/Imperative_HOL
+
* If methods "eval" and "evaluation" encounter a structured proof state
with !!/==>, only the conclusion is evaluated to True (if possible),
avoiding strange error messages.
--- a/doc-src/more_antiquote.ML Thu Jan 08 12:25:22 2009 -0800
+++ b/doc-src/more_antiquote.ML Thu Jan 08 21:13:40 2009 -0800
@@ -50,7 +50,7 @@
end
-(* class antiquotation *)
+(* class and type constructor antiquotation *)
local
@@ -74,6 +74,38 @@
end;
+(* code theorem antiquotation *)
+
+local
+
+fun pretty_term ctxt t = Syntax.pretty_term (Variable.auto_fixes t ctxt) t;
+
+fun pretty_thm ctxt = pretty_term ctxt o Thm.full_prop_of;
+
+fun no_vars ctxt thm =
+ let
+ val ctxt' = Variable.set_body false ctxt;
+ val ((_, [thm]), _) = Variable.import_thms true [thm] ctxt';
+ in thm end;
+
+fun pretty_code_thm src ctxt raw_const =
+ let
+ val thy = ProofContext.theory_of ctxt;
+ val const = Code_Unit.check_const thy raw_const;
+ val (_, funcgr) = Code_Funcgr.make thy [const];
+ val thms = Code_Funcgr.eqns funcgr const
+ |> map_filter (fn (thm, linear) => if linear then SOME thm else NONE)
+ |> map (no_vars ctxt o AxClass.overload thy);
+ in ThyOutput.output_list pretty_thm src ctxt thms end;
+
+in
+
+val _ = O.add_commands
+ [("code_thms", ThyOutput.args Args.term pretty_code_thm)];
+
+end;
+
+
(* code antiquotation *)
local
--- a/src/HOL/Statespace/state_space.ML Thu Jan 08 12:25:22 2009 -0800
+++ b/src/HOL/Statespace/state_space.ML Thu Jan 08 21:13:40 2009 -0800
@@ -160,7 +160,7 @@
fun add_locale_cmd name expr elems thy =
thy
- |> Expression.add_locale_cmd name name expr elems
+ |> Expression.add_locale_cmd name "" expr elems
|> snd
|> LocalTheory.exit;
--- a/src/HOL/Tools/function_package/fundef_datatype.ML Thu Jan 08 12:25:22 2009 -0800
+++ b/src/HOL/Tools/function_package/fundef_datatype.ML Thu Jan 08 21:13:40 2009 -0800
@@ -199,14 +199,14 @@
fun pat_completeness ctxt = Method.SIMPLE_METHOD' (pat_complete_tac ctxt)
val by_pat_completeness_simp =
- Proof.future_terminal_proof
+ Proof.global_future_terminal_proof
(Method.Basic (pat_completeness, Position.none),
SOME (Method.Source_i (Args.src (("HOL.auto", []), Position.none))))
-fun termination_by method =
+fun termination_by method int =
FundefPackage.setup_termination_proof NONE
- #> Proof.future_terminal_proof
- (Method.Basic (method, Position.none), NONE)
+ #> Proof.global_future_terminal_proof
+ (Method.Basic (method, Position.none), NONE) int
fun mk_catchall fixes arities =
let
@@ -304,19 +304,19 @@
local structure P = OuterParse and K = OuterKeyword in
-fun fun_cmd config fixes statements flags lthy =
+fun fun_cmd config fixes statements flags int lthy =
let val group = serial_string () in
lthy
|> LocalTheory.set_group group
|> FundefPackage.add_fundef fixes statements config flags
- |> by_pat_completeness_simp
+ |> by_pat_completeness_simp int
|> LocalTheory.restore
|> LocalTheory.set_group group
- |> termination_by (FundefCommon.get_termination_prover (Context.Proof lthy))
+ |> termination_by (FundefCommon.get_termination_prover (Context.Proof lthy)) int
end;
val _ =
- OuterSyntax.local_theory "fun" "define general recursive functions (short version)" K.thy_decl
+ OuterSyntax.local_theory' "fun" "define general recursive functions (short version)" K.thy_decl
(fundef_parser fun_config
>> (fn ((config, fixes), (flags, statements)) => fun_cmd config fixes statements flags));
--- a/src/HOL/Tools/res_axioms.ML Thu Jan 08 12:25:22 2009 -0800
+++ b/src/HOL/Tools/res_axioms.ML Thu Jan 08 21:13:40 2009 -0800
@@ -456,7 +456,7 @@
|> fold (mark_seen o #1) new_facts
|> fold_map skolem_def (sort_distinct (Thm.thm_ord o pairself snd) new_thms)
|>> map_filter I;
- val cache_entries = ParList.map skolem_cnfs defs;
+ val cache_entries = Par_List.map skolem_cnfs defs;
in SOME (fold update_cache cache_entries thy') end
end;
--- a/src/HOL/ex/ROOT.ML Thu Jan 08 12:25:22 2009 -0800
+++ b/src/HOL/ex/ROOT.ML Thu Jan 08 21:13:40 2009 -0800
@@ -11,12 +11,14 @@
"Word",
"Eval_Examples",
"Quickcheck",
- "Term_Of_Syntax"
+ "Term_Of_Syntax",
+ "Codegenerator",
+ "Codegenerator_Pretty",
+ "NormalForm",
+ "../NumberTheory/Factorization",
+ "../Library/BigO"
];
-no_document use_thy "Codegenerator";
-no_document use_thy "Codegenerator_Pretty";
-
use_thys [
"Numeral",
"ImperativeQuicksort",
@@ -57,56 +59,43 @@
"Meson_Test",
"Code_Antiq",
"Termination",
- "Coherent"
+ "Coherent",
+ "Dense_Linear_Order_Ex",
+ "PresburgerEx",
+ "Reflected_Presburger",
+ "Reflection",
+ "ReflectionEx",
+ "BinEx",
+ "Sqrt",
+ "Sqrt_Script",
+ "BigO_Complex",
+ "Arithmetic_Series_Complex",
+ "HarmonicSeries",
+ "MIR",
+ "ReflectedFerrack",
+ "Refute_Examples",
+ "Quickcheck_Examples"
];
-setmp Proofterm.proofs 2 time_use_thy "Hilbert_Classical";
+setmp Proofterm.proofs 2 use_thy "Hilbert_Classical";
-time_use_thy "Dense_Linear_Order_Ex";
-time_use_thy "PresburgerEx";
-time_use_thy "Reflected_Presburger";
-use_thys ["Reflection", "ReflectionEx"];
+use_thy "SVC_Oracle";
-time_use_thy "SVC_Oracle";
-
-(*check if user has SVC installed*)
fun svc_enabled () = getenv "SVC_HOME" <> "";
fun if_svc_enabled f x = if svc_enabled () then f x else ();
-if_svc_enabled time_use_thy "svc_test";
+if_svc_enabled use_thy "svc_test";
+
(* requires a proof-generating SAT solver (zChaff or MiniSAT) to be *)
(* installed: *)
-try time_use_thy "SAT_Examples";
+try use_thy "SAT_Examples";
(* requires zChaff (or some other reasonably fast SAT solver) to be *)
(* installed: *)
if getenv "ZCHAFF_HOME" <> "" then
- time_use_thy "Sudoku"
+ use_thy "Sudoku"
else ();
-time_use_thy "Refute_Examples";
-time_use_thy "Quickcheck_Examples";
-no_document time_use_thy "NormalForm";
-
HTML.with_charset "utf-8" (no_document use_thys) ["Hebrew", "Chinese"];
-
-no_document use_thys [
- "../NumberTheory/Factorization",
- "../Library/BigO"
-];
-
-use_thys [
- "BinEx",
- "Sqrt",
- "Sqrt_Script",
- "BigO_Complex",
-
- "Arithmetic_Series_Complex",
- "HarmonicSeries",
-
- "MIR",
- "ReflectedFerrack"
-];
-
--- a/src/Pure/Concurrent/future.ML Thu Jan 08 12:25:22 2009 -0800
+++ b/src/Pure/Concurrent/future.ML Thu Jan 08 21:13:40 2009 -0800
@@ -137,15 +137,17 @@
change workers (AList.update Thread.equal (Thread.self (), active));
-(* execute *)
+(* execute jobs *)
fun do_cancel group = (*requires SYNCHRONIZED*)
change canceled (insert Task_Queue.eq_group group);
-fun execute name (task, group, run) =
+fun execute name (task, group, jobs) =
let
val _ = trace_active ();
- val ok = setmp_thread_data (name, task) run ();
+ val valid = Task_Queue.is_valid group;
+ val ok = setmp_thread_data (name, task) (fn () =>
+ fold (fn job => fn ok => job valid andalso ok) jobs true) ();
val _ = SYNCHRONIZED "execute" (fn () =>
(change queue (Task_Queue.finish task);
if ok then ()
@@ -225,16 +227,15 @@
else ());
-(* future values: fork independent computation *)
+
+(** futures **)
-fun future opt_group deps pri (e: unit -> 'a) =
+(* future job: fill result *)
+
+fun future_job group (e: unit -> 'a) =
let
- val _ = scheduler_check "future check";
-
- val group = (case opt_group of SOME group => group | NONE => Task_Queue.new_group ());
-
val result = ref (NONE: 'a Exn.result option);
- val run = Multithreading.with_attributes (Thread.getAttributes ())
+ val job = Multithreading.with_attributes (Thread.getAttributes ())
(fn _ => fn ok =>
let
val res = if ok then Exn.capture e () else Exn.Exn Exn.Interrupt;
@@ -245,63 +246,91 @@
| Exn.Exn Exn.Interrupt => (Task_Queue.invalidate_group group; true)
| _ => false);
in res_ok end);
+ in (result, job) end;
+
+(* fork *)
+
+fun fork_future opt_group deps pri e =
+ let
+ val _ = scheduler_check "future check";
+
+ val group = (case opt_group of SOME group => group | NONE => Task_Queue.new_group ());
+ val (result, job) = future_job group e;
val task = SYNCHRONIZED "future" (fn () =>
- change_result queue (Task_Queue.enqueue group deps pri run) before notify_all ());
+ change_result queue (Task_Queue.enqueue group deps pri job) before notify_all ());
in Future {task = task, group = group, result = result} end;
-fun fork e = future NONE [] 0 e;
-fun fork_group group e = future (SOME group) [] 0 e;
-fun fork_deps deps e = future NONE (map task_of deps) 0 e;
-fun fork_pri pri e = future NONE [] pri e;
+fun fork e = fork_future NONE [] 0 e;
+fun fork_group group e = fork_future (SOME group) [] 0 e;
+fun fork_deps deps e = fork_future NONE (map task_of deps) 0 e;
+fun fork_pri pri e = fork_future NONE [] pri e;
-(* join: retrieve results *)
+(* join *)
+
+fun get_result x = the_default (Exn.Exn (SYS_ERROR "unfinished future")) (peek x);
-fun join_results [] = []
- | join_results xs = uninterruptible (fn _ => fn () =>
- let
- val _ = scheduler_check "join check";
- val _ = Multithreading.self_critical () andalso
- exists (not o is_finished) xs andalso
- error "Cannot join future values within critical section";
+fun join_results xs =
+ if forall is_finished xs then map get_result xs
+ else uninterruptible (fn _ => fn () =>
+ let
+ val _ = scheduler_check "join check";
+ val _ = Multithreading.self_critical () andalso
+ error "Cannot join future values within critical section";
- fun join_loop _ [] = ()
- | join_loop name tasks =
- (case SYNCHRONIZED name (fn () =>
- change_result queue (Task_Queue.dequeue_towards tasks)) of
- NONE => ()
- | SOME (work, tasks') => (execute name work; join_loop name tasks'));
- val _ =
- (case thread_data () of
- NONE =>
- (*alien thread -- refrain from contending for resources*)
- while exists (not o is_finished) xs
- do SYNCHRONIZED "join_thread" (fn () => wait ())
- | SOME (name, task) =>
- (*proper task -- actively work towards results*)
- let
- val unfinished = xs |> map_filter
- (fn Future {task, result = ref NONE, ...} => SOME task | _ => NONE);
- val _ = SYNCHRONIZED "join" (fn () =>
- (change queue (Task_Queue.depend unfinished task); notify_all ()));
- val _ = join_loop ("join_loop: " ^ name) unfinished;
- val _ =
- while exists (not o is_finished) xs
- do SYNCHRONIZED "join_task" (fn () => worker_wait ());
- in () end);
+ fun join_loop _ [] = ()
+ | join_loop name deps =
+ (case SYNCHRONIZED name (fn () =>
+ change_result queue (Task_Queue.dequeue_towards deps)) of
+ NONE => ()
+ | SOME (work, deps') => (execute name work; join_loop name deps'));
+ val _ =
+ (case thread_data () of
+ NONE =>
+ (*alien thread -- refrain from contending for resources*)
+ while not (forall is_finished xs)
+ do SYNCHRONIZED "join_thread" (fn () => wait ())
+ | SOME (name, task) =>
+ (*proper task -- actively work towards results*)
+ let
+ val pending = filter_out is_finished xs;
+ val deps = map task_of pending;
+ val _ = SYNCHRONIZED "join" (fn () =>
+ (change queue (Task_Queue.depend deps task); notify_all ()));
+ val _ = join_loop ("join_loop: " ^ name) deps;
+ val _ =
+ while not (forall is_finished pending)
+ do SYNCHRONIZED "join_task" (fn () => worker_wait ());
+ in () end);
- in xs |> map (fn Future {result = ref (SOME res), ...} => res) end) ();
+ in map get_result xs end) ();
fun join_result x = singleton join_results x;
fun join x = Exn.release (join_result x);
-fun map f x =
- let val task = task_of x
- in future NONE [task] (Task_Queue.pri_of_task task) (fn () => f (join x)) end;
+
+(* map *)
+
+fun map_future f x =
+ let
+ val _ = scheduler_check "map_future check";
+
+ val task = task_of x;
+ val group = Task_Queue.new_group ();
+ val (result, job) = future_job group (fn () => f (join x));
+
+ val extended = SYNCHRONIZED "map_future" (fn () =>
+ (case Task_Queue.extend task job (! queue) of
+ SOME queue' => (queue := queue'; true)
+ | NONE => false));
+ in
+ if extended then Future {task = task, group = group, result = result}
+ else fork_future NONE [task] (Task_Queue.pri_of_task task) (fn () => f (join x))
+ end;
-(* misc operations *)
+(* cancel *)
(*interrupt: permissive signal, may get ignored*)
fun interrupt_task id = SYNCHRONIZED "interrupt"
@@ -313,7 +342,9 @@
SYNCHRONIZED "cancel" (fn () => (do_cancel (group_of x); notify_all ())));
-(*global join and shutdown*)
+
+(** global join and shutdown **)
+
fun shutdown () =
if Multithreading.available then
(scheduler_check "shutdown check";
@@ -327,6 +358,10 @@
OS.Process.sleep (Time.fromMilliseconds 300))))
else ();
+
+(*final declarations of this structure!*)
+val map = map_future;
+
end;
type 'a future = 'a Future.future;
--- a/src/Pure/Concurrent/par_list.ML Thu Jan 08 12:25:22 2009 -0800
+++ b/src/Pure/Concurrent/par_list.ML Thu Jan 08 21:13:40 2009 -0800
@@ -1,5 +1,4 @@
(* Title: Pure/Concurrent/par_list.ML
- ID: $Id$
Author: Makarius
Parallel list combinators.
@@ -24,7 +23,7 @@
val forall: ('a -> bool) -> 'a list -> bool
end;
-structure ParList: PAR_LIST =
+structure Par_List: PAR_LIST =
struct
fun raw_map f xs =
--- a/src/Pure/Concurrent/par_list_dummy.ML Thu Jan 08 12:25:22 2009 -0800
+++ b/src/Pure/Concurrent/par_list_dummy.ML Thu Jan 08 21:13:40 2009 -0800
@@ -1,11 +1,10 @@
(* Title: Pure/Concurrent/par_list_dummy.ML
- ID: $Id$
Author: Makarius
Dummy version of parallel list combinators -- plain sequential evaluation.
*)
-structure ParList: PAR_LIST =
+structure Par_List: PAR_LIST =
struct
val map = map;
--- a/src/Pure/Concurrent/task_queue.ML Thu Jan 08 12:25:22 2009 -0800
+++ b/src/Pure/Concurrent/task_queue.ML Thu Jan 08 21:13:40 2009 -0800
@@ -13,16 +13,18 @@
type group
val eq_group: group * group -> bool
val new_group: unit -> group
+ val is_valid: group -> bool
val invalidate_group: group -> unit
val str_of_group: group -> string
type queue
val empty: queue
val is_empty: queue -> bool
val enqueue: group -> task list -> int -> (bool -> bool) -> queue -> task * queue
+ val extend: task -> (bool -> bool) -> queue -> queue option
val depend: task list -> task -> queue -> queue
- val dequeue: queue -> (task * group * (unit -> bool)) option * queue
+ val dequeue: queue -> (task * group * (bool -> bool) list) option * queue
val dequeue_towards: task list -> queue ->
- (((task * group * (unit -> bool)) * task list) option * queue)
+ (((task * group * (bool -> bool) list) * task list) option * queue)
val interrupt: queue -> task -> unit
val interrupt_external: queue -> string -> unit
val cancel: queue -> group -> bool
@@ -52,6 +54,7 @@
fun new_group () = Group (serial (), ref true);
+fun is_valid (Group (_, ref ok)) = ok;
fun invalidate_group (Group (_, ok)) = ok := false;
fun str_of_group (Group (i, ref ok)) =
@@ -61,14 +64,14 @@
(* jobs *)
datatype job =
- Job of bool -> bool |
+ Job of (bool -> bool) list |
Running of Thread.thread;
type jobs = (group * job) Task_Graph.T;
fun get_group (jobs: jobs) task = #1 (Task_Graph.get_node jobs task);
fun get_job (jobs: jobs) task = #2 (Task_Graph.get_node jobs task);
-fun map_job task f (jobs: jobs) = Task_Graph.map_node task (apsnd f) jobs;
+fun set_job task job (jobs: jobs) = Task_Graph.map_node task (fn (group, _) => (group, job)) jobs;
fun add_job task dep (jobs: jobs) =
Task_Graph.add_edge (dep, task) jobs handle Task_Graph.UNDEF _ => jobs;
@@ -96,9 +99,14 @@
val task = new_task pri;
val groups' = Inttab.cons_list (gid, task) groups;
val jobs' = jobs
- |> Task_Graph.new_node (task, (group, Job job)) |> fold (add_job task) deps;
+ |> Task_Graph.new_node (task, (group, Job [job])) |> fold (add_job task) deps;
in (task, make_queue groups' jobs') end;
+fun extend task job (Queue {groups, jobs}) =
+ (case try (get_job jobs) task of
+ SOME (Job list) => SOME (make_queue groups (set_job task (Job (job :: list)) jobs))
+ | _ => NONE);
+
fun depend deps task (Queue {groups, jobs}) =
make_queue groups (fold (add_job_acyclic task) deps jobs);
@@ -109,14 +117,13 @@
fun dequeue_result NONE queue = (NONE, queue)
| dequeue_result (SOME (result as (task, _, _))) (Queue {groups, jobs}) =
- (SOME result, make_queue groups (map_job task (K (Running (Thread.self ()))) jobs));
+ (SOME result, make_queue groups (set_job task (Running (Thread.self ())) jobs));
in
fun dequeue (queue as Queue {jobs, ...}) =
let
- fun ready (task, ((group as Group (_, ref ok), Job job), ([], _))) =
- SOME (task, group, (fn () => job ok))
+ fun ready (task, ((group, Job list), ([], _))) = SOME (task, group, rev list)
| ready _ = NONE;
in dequeue_result (Task_Graph.get_first ready jobs) queue end;
@@ -126,8 +133,8 @@
fun ready task =
(case Task_Graph.get_node jobs task of
- (group as Group (_, ref ok), Job job) =>
- if null (Task_Graph.imm_preds jobs task) then SOME (task, group, (fn () => job ok))
+ (group, Job list) =>
+ if null (Task_Graph.imm_preds jobs task) then SOME (task, group, rev list)
else NONE
| _ => NONE);
in
--- a/src/Pure/Isar/class.ML Thu Jan 08 12:25:22 2009 -0800
+++ b/src/Pure/Isar/class.ML Thu Jan 08 21:13:40 2009 -0800
@@ -11,9 +11,9 @@
ML is artificial*)
val class: bstring -> class list -> Element.context_i list
- -> theory -> string * Proof.context
+ -> theory -> string * local_theory
val class_cmd: bstring -> xstring list -> Element.context list
- -> theory -> string * Proof.context
+ -> theory -> string * local_theory
val prove_subclass: tactic -> class -> local_theory -> local_theory
val subclass: class -> local_theory -> Proof.state
val subclass_cmd: xstring -> local_theory -> Proof.state
@@ -208,7 +208,7 @@
register class sups params base_sort inst
morphism axiom assm_intro of_class
#> fold (note_assm_intro class) (the_list assm_intro))))))
- |> init class
+ |> TheoryTarget.init (SOME class)
|> pair class
end;
--- a/src/Pure/Isar/expression.ML Thu Jan 08 12:25:22 2009 -0800
+++ b/src/Pure/Isar/expression.ML Thu Jan 08 21:13:40 2009 -0800
@@ -18,9 +18,9 @@
Proof.context -> (term * term list) list list * Proof.context;
(* Declaring locales *)
- val add_locale: string -> bstring -> expression_i -> Element.context_i list ->
+ val add_locale: bstring -> bstring -> expression_i -> Element.context_i list ->
theory -> string * local_theory;
- val add_locale_cmd: string -> bstring -> expression -> Element.context list ->
+ val add_locale_cmd: bstring -> bstring -> expression -> Element.context list ->
theory -> string * local_theory;
(* Interpretation *)
@@ -698,18 +698,20 @@
| defines_to_notes _ e = e;
fun gen_add_locale prep_decl
- bname predicate_name raw_imprt raw_body thy =
+ bname raw_predicate_bname raw_imprt raw_body thy =
let
val name = Sign.full_bname thy bname;
- val _ = Locale.test_locale thy name andalso
+ val _ = Locale.defined thy name andalso
error ("Duplicate definition of locale " ^ quote name);
val ((fixed, deps, body_elems), (parms, ctxt')) =
prep_decl raw_imprt raw_body (ProofContext.init thy);
val text as (((_, exts'), _), defs) = eval ctxt' deps body_elems;
+ val predicate_bname = if raw_predicate_bname = "" then bname
+ else raw_predicate_bname;
val ((a_statement, a_intro, a_axioms), (b_statement, b_intro, b_axioms), thy') =
- define_preds predicate_name parms text thy;
+ define_preds predicate_bname parms text thy;
val extraTs = fold Term.add_tfrees exts' [] \\ fold Term.add_tfreesT (map snd parms) [];
val _ = if null extraTs then ()
@@ -787,7 +789,7 @@
fold store_dep (deps ~~ prep_result propss results) #>
(* propagate registrations *)
(fn thy => fold_rev (fn reg => Locale.activate_global_facts reg)
- (Locale.get_global_registrations thy) thy));
+ (Locale.get_registrations thy) thy));
in
goal_ctxt |>
Proof.theorem_i NONE after_qed (prep_propp propss) |>
@@ -824,7 +826,7 @@
let
val thms' = map (Element.morph_witness export') thms;
val morph' = morph $> Element.satisfy_morphism thms';
- val add = Locale.add_global_registration (name, (morph', export));
+ val add = Locale.add_registration (name, (morph', export));
in ((name, morph') :: regs, add thy) end
| store (Eqns [], []) (regs, thy) =
let val add = fold_rev (fn (name, morph) =>
@@ -842,7 +844,7 @@
val attns' = map ((apsnd o map) (Attrib.attribute_i thy)) attns;
val add =
fold_rev (fn (name, morph) =>
- Locale.amend_global_registration eq_morph (name, morph) #>
+ Locale.amend_registration eq_morph (name, morph) #>
Locale.activate_global_facts (name, morph $> eq_morph $> export)) regs #>
PureThy.note_thmss Thm.lemmaK (attns' ~~ map (fn th => [([th], [])]) thms') #>
snd
@@ -887,7 +889,7 @@
end;
fun after_qed results =
- Proof.map_context (fold store_reg (regs ~~ prep_result propss results)) #> Seq.single;
+ Proof.map_context (fold store_reg (regs ~~ prep_result propss results));
in
state |> Proof.map_context (K goal_ctxt) |>
Proof.local_goal (ProofDisplay.print_results int) (K I) ProofContext.bind_propp_i
--- a/src/Pure/Isar/isar.ML Thu Jan 08 12:25:22 2009 -0800
+++ b/src/Pure/Isar/isar.ML Thu Jan 08 21:13:40 2009 -0800
@@ -133,11 +133,12 @@
(case Source.get_single (Source.set_prompt Source.default_prompt src) of
NONE => if secure then quit () else ()
| SOME (tr, src') => if op >> tr orelse check_secure () then raw_loop secure src' else ())
- handle exn => (Output.error_msg (Toplevel.exn_message exn)
- handle crash =>
- (CRITICAL (fn () => change crashes (cons crash));
- warning "Recovering after Isar toplevel crash -- see also Isar.crashes");
- raw_loop secure src)
+ handle exn =>
+ (Output.error_msg (Toplevel.exn_message exn)
+ handle crash =>
+ (CRITICAL (fn () => change crashes (cons crash));
+ warning "Recovering from Isar toplevel crash -- see also Isar.crashes");
+ raw_loop secure src)
end;
in
--- a/src/Pure/Isar/isar_cmd.ML Thu Jan 08 12:25:22 2009 -0800
+++ b/src/Pure/Isar/isar_cmd.ML Thu Jan 08 21:13:40 2009 -0800
@@ -1,5 +1,4 @@
(* Title: Pure/Isar/isar_cmd.ML
- ID: $Id$
Author: Markus Wenzel, TU Muenchen
Derived Isar commands.
@@ -219,7 +218,7 @@
(* goals *)
fun goal opt_chain goal stmt int =
- opt_chain #> goal NONE (K Seq.single) stmt int;
+ opt_chain #> goal NONE (K I) stmt int;
val have = goal I Proof.have;
val hence = goal Proof.chain Proof.have;
@@ -229,12 +228,12 @@
(* local endings *)
-fun local_qed m = Toplevel.proofs (Proof.local_qed (m, true));
-val local_terminal_proof = Toplevel.proofs o Proof.local_terminal_proof;
-val local_default_proof = Toplevel.proofs Proof.local_default_proof;
-val local_immediate_proof = Toplevel.proofs Proof.local_immediate_proof;
-val local_done_proof = Toplevel.proofs Proof.local_done_proof;
-val local_skip_proof = Toplevel.proofs' Proof.local_skip_proof;
+fun local_qed m = Toplevel.proof (Proof.local_qed (m, true));
+val local_terminal_proof = Toplevel.proof o Proof.local_terminal_proof;
+val local_default_proof = Toplevel.proof Proof.local_default_proof;
+val local_immediate_proof = Toplevel.proof Proof.local_immediate_proof;
+val local_done_proof = Toplevel.proof Proof.local_done_proof;
+val local_skip_proof = Toplevel.proof' Proof.local_skip_proof;
val skip_local_qed = Toplevel.skip_proof (fn i => if i > 1 then i - 1 else raise Toplevel.UNDEF);
--- a/src/Pure/Isar/isar_syn.ML Thu Jan 08 12:25:22 2009 -0800
+++ b/src/Pure/Isar/isar_syn.ML Thu Jan 08 21:13:40 2009 -0800
@@ -393,7 +393,7 @@
(P.name -- Scan.optional (P.$$$ "=" |-- P.!!! locale_val) (([], []), []) -- P.opt_begin
>> (fn ((name, (expr, elems)), begin) =>
(begin ? Toplevel.print) o Toplevel.begin_local_theory begin
- (Expression.add_locale_cmd name name expr elems #> snd)));
+ (Expression.add_locale_cmd name "" expr elems #> snd)));
val _ =
OuterSyntax.command "sublocale"
@@ -470,7 +470,7 @@
(P.name -- (P.$$$ "=" |-- class_val) -- P.opt_begin
>> (fn ((name, (supclasses, elems)), begin) =>
(begin ? Toplevel.print) o Toplevel.begin_local_theory begin
- (Class.class_cmd name supclasses elems #-> TheoryTarget.begin)));
+ (Class.class_cmd name supclasses elems #> snd)));
val _ =
OuterSyntax.local_theory_to_proof "subclass" "prove a subclass relation" K.thy_goal
--- a/src/Pure/Isar/locale.ML Thu Jan 08 12:25:22 2009 -0800
+++ b/src/Pure/Isar/locale.ML Thu Jan 08 21:13:40 2009 -0800
@@ -31,7 +31,6 @@
sig
type locale
- val test_locale: theory -> string -> bool
val register_locale: bstring ->
(string * sort) list * (Binding.T * typ option * mixfix) list ->
term option * term list ->
@@ -44,6 +43,7 @@
val extern: theory -> string -> xstring
(* Specification *)
+ val defined: theory -> string -> bool
val params_of: theory -> string -> (Binding.T * typ option * mixfix) list
val instance_of: theory -> string -> Morphism.morphism -> term list
val specification_of: theory -> string -> term option * term list
@@ -71,11 +71,11 @@
val intro_locales_tac: bool -> Proof.context -> thm list -> tactic
(* Registrations *)
- val add_global_registration: (string * (Morphism.morphism * Morphism.morphism)) ->
+ val add_registration: (string * (Morphism.morphism * Morphism.morphism)) ->
theory -> theory
- val amend_global_registration: Morphism.morphism -> (string * Morphism.morphism) ->
+ val amend_registration: Morphism.morphism -> (string * Morphism.morphism) ->
theory -> theory
- val get_global_registrations: theory -> (string * Morphism.morphism) list
+ val get_registrations: theory -> (string * Morphism.morphism) list
(* Diagnostic *)
val print_locales: theory -> unit
@@ -109,107 +109,79 @@
datatype ctxt = datatype Element.ctxt;
-(*** Basics ***)
+
+(*** Theory data ***)
datatype locale = Loc of {
- (* extensible lists are in reverse order: decls, notes, dependencies *)
+ (** static part **)
parameters: (string * sort) list * (Binding.T * typ option * mixfix) list,
(* type and term parameters *)
spec: term option * term list,
(* assumptions (as a single predicate expression) and defines *)
+ (** dynamic part **)
decls: (declaration * stamp) list * (declaration * stamp) list,
(* type and term syntax declarations *)
notes: ((string * (Attrib.binding * (thm list * Attrib.src list) list) list) * stamp) list,
(* theorem declarations *)
dependencies: ((string * Morphism.morphism) * stamp) list
(* locale dependencies (sublocale relation) *)
-}
+};
-
-(*** Theory data ***)
+fun mk_locale ((parameters, spec), ((decls, notes), dependencies)) =
+ Loc {parameters = parameters, spec = spec, decls = decls,
+ notes = notes, dependencies = dependencies};
+fun map_locale f (Loc {parameters, spec, decls, notes, dependencies}) =
+ mk_locale (f ((parameters, spec), ((decls, notes), dependencies)));
+fun merge_locale (Loc {parameters, spec, decls = (decls1, decls2), notes, dependencies},
+ Loc {decls = (decls1', decls2'), notes = notes', dependencies = dependencies', ...}) =
+ mk_locale ((parameters, spec),
+ (((merge (eq_snd op =) (decls1, decls1'), merge (eq_snd op =) (decls2, decls2')),
+ merge (eq_snd op =) (notes, notes')),
+ merge (eq_snd op =) (dependencies, dependencies')));
structure LocalesData = TheoryDataFun
(
- type T = NameSpace.T * locale Symtab.table;
- (* locale namespace and locales of the theory *)
-
+ type T = locale NameSpace.table;
val empty = NameSpace.empty_table;
val copy = I;
val extend = I;
-
- fun join_locales _
- (Loc {parameters, spec, decls = (decls1, decls2), notes, dependencies},
- Loc {decls = (decls1', decls2'), notes = notes', dependencies = dependencies', ...}) =
- Loc {
- parameters = parameters,
- spec = spec,
- decls =
- (merge (eq_snd op =) (decls1, decls1'),
- merge (eq_snd op =) (decls2, decls2')),
- notes = merge (eq_snd op =) (notes, notes'),
- dependencies = merge (eq_snd op =) (dependencies, dependencies')};
-
- fun merge _ = NameSpace.join_tables join_locales;
+ fun merge _ = NameSpace.join_tables (K merge_locale);
);
val intern = NameSpace.intern o #1 o LocalesData.get;
val extern = NameSpace.extern o #1 o LocalesData.get;
-fun get_locale thy name = Symtab.lookup (#2 (LocalesData.get thy)) name;
+fun get_locale thy = Symtab.lookup (#2 (LocalesData.get thy));
+
+fun defined thy = is_some o get_locale thy;
fun the_locale thy name = case get_locale thy name
- of SOME loc => loc
+ of SOME (Loc loc) => loc
| NONE => error ("Unknown locale " ^ quote name);
-fun test_locale thy name = case get_locale thy name
- of SOME _ => true | NONE => false;
-
fun register_locale bname parameters spec decls notes dependencies thy =
thy |> LocalesData.map (NameSpace.bind (Sign.naming_of thy) (Binding.name bname,
- Loc {parameters = parameters, spec = spec, decls = decls, notes = notes,
- dependencies = dependencies}) #> snd);
+ mk_locale ((parameters, spec), ((decls, notes), dependencies))) #> snd);
-fun change_locale name f thy =
- let
- val Loc {parameters, spec, decls, notes, dependencies} =
- the_locale thy name;
- val (parameters', spec', decls', notes', dependencies') =
- f (parameters, spec, decls, notes, dependencies);
- in
- thy
- |> (LocalesData.map o apsnd) (Symtab.update (name, Loc {parameters = parameters',
- spec = spec', decls = decls', notes = notes', dependencies = dependencies'}))
- end;
+fun change_locale name =
+ LocalesData.map o apsnd o Symtab.map_entry name o map_locale o apsnd;
fun print_locales thy =
- let val (space, locs) = LocalesData.get thy in
- Pretty.strs ("locales:" :: map #1 (NameSpace.extern_table (space, locs)))
- |> Pretty.writeln
- end;
+ Pretty.strs ("locales:" :: map #1 (NameSpace.extern_table (LocalesData.get thy)))
+ |> Pretty.writeln;
(*** Primitive operations ***)
-fun params_of thy name =
- let
- val Loc {parameters = (_, params), ...} = the_locale thy name
- in params end;
+fun params_of thy = snd o #parameters o the_locale thy;
-fun instance_of thy name morph =
- params_of thy name |>
- map ((fn (b, T, _) => Free (Binding.base_name b, the T)) #> Morphism.term morph);
+fun instance_of thy name morph = params_of thy name |>
+ map ((fn (b, T, _) => Free (Binding.base_name b, the T)) #> Morphism.term morph);
-fun specification_of thy name =
- let
- val Loc {spec, ...} = the_locale thy name
- in spec end;
+fun specification_of thy = #spec o the_locale thy;
-fun declarations_of thy name =
- let
- val Loc {decls, ...} = the_locale thy name
- in
- decls |> apfst (map fst) |> apsnd (map fst)
- end;
+fun declarations_of thy name = the_locale thy name |>
+ #decls |> apfst (map fst) |> apsnd (map fst);
(*** Activate context elements of locale ***)
@@ -267,7 +239,7 @@
then error "Roundup bound exceeded (sublocale relation probably not terminating)."
else
let
- val Loc {parameters = (_, params), dependencies, ...} = the_locale thy name;
+ val {parameters = (_, params), dependencies, ...} = the_locale thy name;
val instance = instance_of thy name morph;
in
if member (ident_eq thy) marked (name, instance)
@@ -304,7 +276,7 @@
fun activate_decls thy (name, morph) ctxt =
let
- val Loc {decls = (typ_decls, term_decls), ...} = the_locale thy name;
+ val {decls = (typ_decls, term_decls), ...} = the_locale thy name;
in
ctxt |> fold_rev (fn (decl, _) => Context.proof_map (decl morph)) typ_decls |>
fold_rev (fn (decl, _) => Context.proof_map (decl morph)) term_decls
@@ -312,7 +284,7 @@
fun activate_notes activ_elem transfer thy (name, morph) input =
let
- val Loc {notes, ...} = the_locale thy name;
+ val {notes, ...} = the_locale thy name;
fun activate ((kind, facts), _) input =
let
val facts' = facts |> Element.facts_map (Element.morph_ctxt (transfer input $> morph))
@@ -323,7 +295,7 @@
fun activate_all name thy activ_elem transfer (marked, input) =
let
- val Loc {parameters = (_, params), spec = (asm, defs), ...} =
+ val {parameters = (_, params), spec = (asm, defs), ...} =
the_locale thy name;
in
input |>
@@ -342,9 +314,9 @@
local
fun init_global_elem (Notes (kind, facts)) thy =
- let
- val facts' = Attrib.map_facts (Attrib.attribute_i thy) facts
- in Old_Locale.global_note_qualified kind facts' thy |> snd end
+ let
+ val facts' = Attrib.map_facts (Attrib.attribute_i thy) facts
+ in Old_Locale.global_note_qualified kind facts' thy |> snd end
fun init_local_elem (Fixes fixes) ctxt = ctxt |>
ProofContext.add_fixes_i fixes |> snd
@@ -408,42 +380,40 @@
(*** Registrations: interpretations in theories ***)
-(* FIXME only global variant needed *)
-structure RegistrationsData = GenericDataFun
+structure RegistrationsData = TheoryDataFun
(
type T = ((string * (Morphism.morphism * Morphism.morphism)) * stamp) list;
-(* FIXME mixins need to be stamped *)
+ (* FIXME mixins need to be stamped *)
(* registrations, in reverse order of declaration *)
val empty = [];
val extend = I;
+ val copy = I;
fun merge _ data : T = Library.merge (eq_snd op =) data;
(* FIXME consolidate with dependencies, consider one data slot only *)
);
-val get_global_registrations =
- Context.Theory #> RegistrationsData.get #> map fst #> map (apsnd op $>);
+val get_registrations =
+ RegistrationsData.get #> map fst #> map (apsnd op $>);
-fun add_global reg =
- (Context.theory_map o RegistrationsData.map) (cons (reg, stamp ()));
-
-fun add_global_registration (name, (base_morph, export)) thy =
- roundup thy (fn _ => fn (name', morph') => fn thy => add_global (name', (morph', export)) thy)
+fun add_registration (name, (base_morph, export)) thy =
+ roundup thy (fn _ => fn (name', morph') =>
+ (RegistrationsData.map o cons) ((name', (morph', export)), stamp ()))
(name, base_morph) (get_global_idents thy, thy) |>
snd (* FIXME ?? uncurry put_global_idents *);
-fun amend_global_registration morph (name, base_morph) thy =
+fun amend_registration morph (name, base_morph) thy =
let
- val regs = (Context.Theory #> RegistrationsData.get #> map fst) thy;
+ val regs = (RegistrationsData.get #> map fst) thy;
val base = instance_of thy name base_morph;
fun match (name', (morph', _)) =
name = name' andalso eq_list (op aconv) (base, instance_of thy name' morph');
val i = find_index match (rev regs);
- val _ = if i = ~1 then error ("No interpretation of locale " ^
+ val _ = if i = ~1 then error ("No registration of locale " ^
quote (extern thy name) ^ " and parameter instantiation " ^
space_implode " " (map (quote o Syntax.string_of_term_global thy) base) ^ " available.")
else ();
in
- (Context.theory_map o RegistrationsData.map) (nth_map (length regs - 1 - i)
+ RegistrationsData.map (nth_map (length regs - 1 - i)
(fn ((name, (base, export)), stamp) => ((name, (base $> morph, export)), stamp))) thy
end;
@@ -456,16 +426,15 @@
let
val ([Notes args'], ctxt') = Element.activate_i [Notes (kind, args)] ctxt;
val ctxt'' = ctxt' |> ProofContext.theory (
- change_locale loc
- (fn (parameters, spec, decls, notes, dependencies) =>
- (parameters, spec, decls, (args', stamp ()) :: notes, dependencies)) #>
+ (change_locale loc o apfst o apsnd) (cons (args', stamp ()))
+ #>
(* Registrations *)
(fn thy => fold_rev (fn (name, morph) =>
let
val args'' = snd args' |> Element.facts_map (Element.morph_ctxt morph) |>
Attrib.map_facts (Attrib.attribute_i thy)
in Old_Locale.global_note_qualified kind args'' #> snd end)
- (get_global_registrations thy |> filter (fn (name, _) => name = loc)) thy))
+ (get_registrations thy |> filter (fn (name, _) => name = loc)) thy))
in ctxt'' end;
@@ -476,9 +445,8 @@
fun decl_attrib decl phi = Thm.declaration_attribute (K (decl phi));
fun add_decls add loc decl =
- ProofContext.theory (change_locale loc
- (fn (parameters, spec, decls, notes, dependencies) =>
- (parameters, spec, add (decl, stamp ()) decls, notes, dependencies))) #>
+ ProofContext.theory ((change_locale loc o apfst o apfst) (add (decl, stamp ())))
+ #>
add_thmss loc Thm.internalK
[((Binding.empty, [Attrib.internal (decl_attrib decl)]), [([Drule.dummy_thm], [])])];
@@ -492,10 +460,7 @@
(* Dependencies *)
-fun add_dependency loc dep =
- change_locale loc
- (fn (parameters, spec, decls, notes, dependencies) =>
- (parameters, spec, decls, notes, (dep, stamp ()) :: dependencies));
+fun add_dependency loc dep = (change_locale loc o apsnd) (cons (dep, stamp ()));
(*** Reasoning about locales ***)
--- a/src/Pure/Isar/obtain.ML Thu Jan 08 12:25:22 2009 -0800
+++ b/src/Pure/Isar/obtain.ML Thu Jan 08 21:13:40 2009 -0800
@@ -1,5 +1,4 @@
(* Title: Pure/Isar/obtain.ML
- ID: $Id$
Author: Markus Wenzel, TU Muenchen
The 'obtain' and 'guess' language elements -- generalized existence at
@@ -150,13 +149,13 @@
fun after_qed _ =
Proof.local_qed (NONE, false)
- #> Seq.map (`Proof.the_fact #-> (fn rule =>
+ #> `Proof.the_fact #-> (fn rule =>
Proof.fix_i vars
- #> Proof.assm_i (obtain_export fix_ctxt rule (map (cert o Free) parms)) asms));
+ #> Proof.assm_i (obtain_export fix_ctxt rule (map (cert o Free) parms)) asms);
in
state
|> Proof.enter_forward
- |> Proof.have_i NONE (K Seq.single) [((Binding.empty, []), [(obtain_prop, [])])] int
+ |> Proof.have_i NONE (K I) [((Binding.empty, []), [(obtain_prop, [])])] int
|> Proof.proof (SOME Method.succeed_text) |> Seq.hd
|> Proof.fix_i [(Binding.name thesisN, NONE, NoSyn)]
|> Proof.assume_i
@@ -306,7 +305,7 @@
val before_qed = SOME (Method.primitive_text (Goal.conclude #> MetaSimplifier.norm_hhf #>
(fn th => Goal.protect (Conjunction.intr (Drule.mk_term (Thm.cprop_of th)) th))));
fun after_qed [[_, res]] =
- Proof.end_block #> guess_context (check_result ctxt thesis res) #> Seq.single;
+ Proof.end_block #> guess_context (check_result ctxt thesis res);
in
state
|> Proof.enter_forward
--- a/src/Pure/Isar/old_locale.ML Thu Jan 08 12:25:22 2009 -0800
+++ b/src/Pure/Isar/old_locale.ML Thu Jan 08 21:13:40 2009 -0800
@@ -116,7 +116,7 @@
theory -> Proof.state
val interpretation_in_locale: (Proof.context -> Proof.context) ->
xstring * expr -> theory -> Proof.state
- val interpret: (Proof.state -> Proof.state Seq.seq) ->
+ val interpret: (Proof.state -> Proof.state) ->
(Binding.T -> Binding.T) -> expr ->
term option list * (Attrib.binding * term) list ->
bool -> Proof.state ->
@@ -2478,7 +2478,7 @@
val interpret = gen_interpret prep_local_registration;
fun interpret_cmd interp_prfx = snd oooo gen_interpret prep_local_registration_cmd
- Seq.single (standard_name_morph interp_prfx);
+ I (standard_name_morph interp_prfx);
end;
--- a/src/Pure/Isar/outer_syntax.ML Thu Jan 08 12:25:22 2009 -0800
+++ b/src/Pure/Isar/outer_syntax.ML Thu Jan 08 21:13:40 2009 -0800
@@ -17,6 +17,8 @@
val improper_command: string -> string -> OuterKeyword.T ->
(Toplevel.transition -> Toplevel.transition) parser -> unit
val internal_command: string -> (Toplevel.transition -> Toplevel.transition) parser -> unit
+ val local_theory': string -> string -> OuterKeyword.T ->
+ (bool -> local_theory -> local_theory) parser -> unit
val local_theory: string -> string -> OuterKeyword.T ->
(local_theory -> local_theory) parser -> unit
val local_theory_to_proof': string -> string -> OuterKeyword.T ->
@@ -138,6 +140,7 @@
command name comment kind (P.opt_target -- parse
>> (fn (loc, f) => (if do_print then Toplevel.print else I) o trans loc f));
+val local_theory' = local_theory_command false Toplevel.local_theory';
val local_theory = local_theory_command false Toplevel.local_theory;
val local_theory_to_proof' = local_theory_command true Toplevel.local_theory_to_proof';
val local_theory_to_proof = local_theory_command true Toplevel.local_theory_to_proof;
--- a/src/Pure/Isar/proof.ML Thu Jan 08 12:25:22 2009 -0800
+++ b/src/Pure/Isar/proof.ML Thu Jan 08 21:13:40 2009 -0800
@@ -30,7 +30,6 @@
val enter_forward: state -> state
val goal_message: (unit -> Pretty.T) -> state -> state
val get_goal: state -> context * (thm list * thm)
- val schematic_goal: state -> bool
val show_main_goal: bool ref
val verbose: bool ref
val pretty_state: int -> state -> Pretty.T list
@@ -87,35 +86,40 @@
val local_goal: (context -> ((string * string) * (string * thm list) list) -> unit) ->
(theory -> 'a -> attribute) ->
(context * 'b list -> context * (term list list * (context -> context))) ->
- string -> Method.text option -> (thm list list -> state -> state Seq.seq) ->
+ string -> Method.text option -> (thm list list -> state -> state) ->
((Binding.T * 'a list) * 'b) list -> state -> state
- val local_qed: Method.text option * bool -> state -> state Seq.seq
+ val local_qed: Method.text option * bool -> state -> state
val theorem: Method.text option -> (thm list list -> context -> context) ->
(string * string list) list list -> context -> state
val theorem_i: Method.text option -> (thm list list -> context -> context) ->
(term * term list) list list -> context -> state
val global_qed: Method.text option * bool -> state -> context
- val local_terminal_proof: Method.text * Method.text option -> state -> state Seq.seq
- val local_default_proof: state -> state Seq.seq
- val local_immediate_proof: state -> state Seq.seq
- val local_done_proof: state -> state Seq.seq
- val local_skip_proof: bool -> state -> state Seq.seq
+ val local_terminal_proof: Method.text * Method.text option -> state -> state
+ val local_default_proof: state -> state
+ val local_immediate_proof: state -> state
+ val local_skip_proof: bool -> state -> state
+ val local_done_proof: state -> state
val global_terminal_proof: Method.text * Method.text option -> state -> context
val global_default_proof: state -> context
val global_immediate_proof: state -> context
+ val global_skip_proof: bool -> state -> context
val global_done_proof: state -> context
- val global_skip_proof: bool -> state -> context
- val have: Method.text option -> (thm list list -> state -> state Seq.seq) ->
+ val have: Method.text option -> (thm list list -> state -> state) ->
(Attrib.binding * (string * string list) list) list -> bool -> state -> state
- val have_i: Method.text option -> (thm list list -> state -> state Seq.seq) ->
+ val have_i: Method.text option -> (thm list list -> state -> state) ->
((Binding.T * attribute list) * (term * term list) list) list -> bool -> state -> state
- val show: Method.text option -> (thm list list -> state -> state Seq.seq) ->
+ val show: Method.text option -> (thm list list -> state -> state) ->
(Attrib.binding * (string * string list) list) list -> bool -> state -> state
- val show_i: Method.text option -> (thm list list -> state -> state Seq.seq) ->
+ val show_i: Method.text option -> (thm list list -> state -> state) ->
((Binding.T * attribute list) * (term * term list) list) list -> bool -> state -> state
+ val schematic_goal: state -> bool
val is_relevant: state -> bool
- val future_proof: (state -> ('a * context) future) -> state -> 'a future * context
- val future_terminal_proof: Method.text * Method.text option -> state -> context
+ val local_future_proof: (state -> ('a * state) Future.future) ->
+ state -> 'a Future.future * state
+ val global_future_proof: (state -> ('a * Proof.context) Future.future) ->
+ state -> 'a Future.future * context
+ val local_future_terminal_proof: Method.text * Method.text option -> bool -> state -> state
+ val global_future_terminal_proof: Method.text * Method.text option -> bool -> state -> context
end;
structure Proof: PROOF =
@@ -148,7 +152,7 @@
goal: thm, (*subgoals ==> statement*)
before_qed: Method.text option,
after_qed:
- (thm list list -> state -> state Seq.seq) *
+ (thm list list -> state -> state) *
(thm list list -> context -> context)};
fun make_goal (statement, messages, using, goal, before_qed, after_qed) =
@@ -312,12 +316,6 @@
let val (ctxt, (_, {using, goal, ...})) = find_goal state
in (ctxt, (using, goal)) end;
-fun schematic_goal state =
- let val (_, (_, {statement = (_, _, prop), ...})) = find_goal state in
- Term.exists_subterm Term.is_Var prop orelse
- Term.exists_type (Term.exists_subtype Term.is_TVar) prop
- end;
-
(** pretty_state **)
@@ -347,8 +345,7 @@
(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" ^
@@ -751,6 +748,13 @@
|> `before_qed |-> (refine o the_default Method.succeed_text)
|> Seq.maps (refine (Method.finish_text txt (Position.thread_data ())));
+fun check_result msg sq =
+ (case Seq.pull sq of
+ NONE => error msg
+ | SOME (s, _) => s);
+
+fun check_finish sq = check_result "Failed to finish proof" sq;
+
(* unstructured refinement *)
@@ -842,7 +846,7 @@
|> burrow (ProofContext.export goal_ctxt outer_ctxt);
val (after_local, after_global) = after_qed;
- fun after_local' x y = Position.setmp_thread_data_seq pos (fn () => after_local x y) ();
+ fun after_local' x y = Position.setmp_thread_data pos (fn () => after_local x y) ();
fun after_global' x y = Position.setmp_thread_data pos (fn () => after_global x y) ();
in
outer_state
@@ -871,61 +875,47 @@
|> tap (Variable.warn_extra_tfrees (context_of state) o context_of)
end;
-fun local_qed txt =
- end_proof false txt #>
- Seq.maps (generic_qed ProofContext.auto_bind_facts #->
+fun local_qeds txt =
+ end_proof false txt
+ #> Seq.map (generic_qed ProofContext.auto_bind_facts #->
(fn ((after_qed, _), results) => after_qed results));
+fun local_qed txt = local_qeds txt #> check_finish;
+
(* global goals *)
fun global_goal prepp before_qed after_qed propp ctxt =
init ctxt
- |> generic_goal (prepp #> ProofContext.auto_fixes) ""
- before_qed (K Seq.single, after_qed) propp;
+ |> generic_goal (prepp #> ProofContext.auto_fixes) "" before_qed (K I, after_qed) propp;
val theorem = global_goal ProofContext.bind_propp_schematic;
val theorem_i = global_goal ProofContext.bind_propp_schematic_i;
-fun check_result msg sq =
- (case Seq.pull sq of
- NONE => error msg
- | SOME (s', sq') => Seq.cons s' sq');
-
fun global_qeds txt =
end_proof true txt
#> Seq.map (generic_qed (K I) #> (fn (((_, after_qed), results), state) =>
- after_qed results (context_of state)))
- |> Seq.DETERM; (*backtracking may destroy theory!*)
+ after_qed results (context_of state)));
-fun global_qed txt =
- global_qeds txt
- #> check_result "Failed to finish proof"
- #> Seq.hd;
+fun global_qed txt = global_qeds txt #> check_finish;
(* concluding steps *)
-fun local_terminal_proof (text, opt_text) =
- proof (SOME text) #> Seq.maps (local_qed (opt_text, true));
+fun terminal_proof qed initial terminal =
+ proof (SOME initial) #> Seq.maps (qed terminal) #> check_finish;
+fun local_terminal_proof (text, opt_text) = terminal_proof local_qeds text (opt_text, true);
val local_default_proof = local_terminal_proof (Method.default_text, NONE);
val local_immediate_proof = local_terminal_proof (Method.this_text, NONE);
-val local_done_proof = proof (SOME Method.done_text) #> Seq.maps (local_qed (NONE, false));
fun local_skip_proof int = local_terminal_proof (Method.sorry_text int, NONE);
+val local_done_proof = terminal_proof local_qeds Method.done_text (NONE, false);
-fun global_term_proof immed (text, opt_text) =
- proof (SOME text)
- #> check_result "Terminal proof method failed"
- #> Seq.maps (global_qeds (opt_text, immed))
- #> check_result "Failed to finish proof (after successful terminal method)"
- #> Seq.hd;
-
-val global_terminal_proof = global_term_proof true;
+fun global_terminal_proof (text, opt_text) = terminal_proof global_qeds text (opt_text, true);
val global_default_proof = global_terminal_proof (Method.default_text, NONE);
val global_immediate_proof = global_terminal_proof (Method.this_text, NONE);
-val global_done_proof = global_term_proof false (Method.done_text, NONE);
fun global_skip_proof int = global_terminal_proof (Method.sorry_text int, NONE);
+val global_done_proof = terminal_proof global_qeds Method.done_text (NONE, false);
(* common goal statements *)
@@ -940,7 +930,7 @@
val testing = ref false;
val rule = ref (NONE: thm option);
fun fail_msg ctxt =
- "Local statement will fail to solve any pending goal" ::
+ "Local statement will fail to refine any pending goal" ::
(case ! rule of NONE => [] | SOME th => [ProofDisplay.string_of_rule ctxt "Failed" th])
|> cat_lines;
@@ -951,13 +941,14 @@
else if int then priority (ProofDisplay.string_of_rule ctxt "Successful" th)
else ();
val test_proof =
- (Seq.pull oo local_skip_proof) true
+ try (local_skip_proof true)
|> setmp_noncritical testing true
|> Exn.capture;
fun after_qed' results =
refine_goals print_rule (context_of state) (flat results)
- #> Seq.maps (after_qed results);
+ #> check_result "Failed to refine any pending goal"
+ #> after_qed results;
in
state
|> local_goal print_results prep_att prepp "show" before_qed after_qed' stmt
@@ -979,59 +970,89 @@
end;
-(* fork global proofs *)
+
+(** future proofs **)
+
+(* relevant proof states *)
+
+fun is_schematic t =
+ Term.exists_subterm Term.is_Var t orelse
+ Term.exists_type (Term.exists_subtype Term.is_TVar) t;
+
+fun schematic_goal state =
+ let val (_, (_, {statement = (_, _, prop), ...})) = find_goal state
+ in is_schematic prop end;
+
+fun is_relevant state =
+ (case try find_goal state of
+ NONE => true
+ | SOME (_, (_, {statement = (_, _, prop), goal, ...})) =>
+ is_schematic prop orelse not (Logic.protect prop aconv Thm.concl_of goal));
+
+
+(* full proofs *)
local
-fun is_original state =
- (case try find_goal state of
- NONE => false
- | SOME (_, (_, {statement = (_, _, prop), goal, ...})) =>
- Logic.protect prop aconv Thm.concl_of goal);
-
-in
-
-fun is_relevant state =
- can (assert_bottom false) state orelse
- can assert_forward state orelse
- not (is_original state) orelse
- schematic_goal state;
-
-fun future_proof fork_proof state =
+fun future_proof done get_context fork_proof state =
let
- val _ = is_relevant state andalso error "Cannot fork relevant proof";
-
+ val _ = assert_backward state;
val (goal_ctxt, (_, goal)) = find_goal state;
val {statement as (kind, propss, prop), messages, using, goal, before_qed, after_qed} = goal;
+ val _ = is_relevant state andalso error "Cannot fork relevant proof";
+
val prop' = Logic.protect prop;
val statement' = (kind, [[], [prop']], prop');
val goal' = Thm.adjust_maxidx_thm (Thm.maxidx_of goal)
(Drule.comp_no_flatten (goal, Thm.nprems_of goal) 1 Drule.protectI);
- fun after_qed' [[th]] = ProofContext.put_thms false (AutoBind.thisN, SOME [th]);
+
+ fun after_local' [[th]] = put_thms false (AutoBind.thisN, SOME [th]);
+ fun after_global' [[th]] = ProofContext.put_thms false (AutoBind.thisN, SOME [th]);
+ val after_qed' = (after_local', after_global');
val this_name = ProofContext.full_bname goal_ctxt AutoBind.thisN;
val result_ctxt =
state
- |> map_contexts (Variable.auto_fixes prop)
- |> map_goal I (K (statement', messages, using, goal', before_qed, (#1 after_qed, after_qed')))
+ |> map_contexts (Variable.declare_term prop)
+ |> map_goal I (K (statement', messages, using, goal', before_qed, after_qed'))
|> fork_proof;
- val future_thm = result_ctxt |> Future.map (fn (_, ctxt) =>
- ProofContext.get_fact_single ctxt (Facts.named this_name));
- val finished_goal = Goal.future_result goal_ctxt future_thm prop';
+ val future_thm = result_ctxt |> Future.map (fn (_, x) =>
+ ProofContext.get_fact_single (get_context x) (Facts.named this_name));
+ val finished_goal = exception_trace (fn () => Goal.future_result goal_ctxt future_thm prop');
val state' =
state
|> map_goal I (K (statement, messages, using, finished_goal, NONE, after_qed))
- |> global_done_proof;
+ |> done;
in (Future.map #1 result_ctxt, state') end;
+in
+
+fun local_future_proof x = future_proof local_done_proof context_of x;
+fun global_future_proof x = future_proof global_done_proof I x;
+
end;
-fun future_terminal_proof meths state =
- if is_relevant state orelse not (Future.enabled ()) then global_terminal_proof meths state
- else #2 (state |> future_proof (fn state' =>
- Future.fork_pri ~1 (fn () => ((), global_terminal_proof meths state'))));
+
+(* terminal proofs *)
+
+local
+
+fun future_terminal_proof proof1 proof2 meths int state =
+ if int orelse is_relevant state orelse not (Future.enabled ())
+ then proof1 meths state
+ else snd (state |> proof2 (fn state' => Future.fork_pri ~1 (fn () => ((), proof1 meths state'))));
+
+in
+
+fun local_future_terminal_proof x =
+ future_terminal_proof local_terminal_proof local_future_proof x;
+
+fun global_future_terminal_proof x =
+ future_terminal_proof global_terminal_proof global_future_proof x;
end;
+end;
+
--- a/src/Pure/Isar/theory_target.ML Thu Jan 08 12:25:22 2009 -0800
+++ b/src/Pure/Isar/theory_target.ML Thu Jan 08 21:13:40 2009 -0800
@@ -334,7 +334,7 @@
fun init_target _ NONE = global_target
| init_target thy (SOME target) =
- make_target target (Locale.test_locale thy (Locale.intern thy target))
+ make_target target (Locale.defined thy (Locale.intern thy target))
true (Class_Target.is_class thy target) ([], [], []) [];
fun init_ctxt (Target {target, new_locale, is_locale, is_class, instantiation, overloading}) =
@@ -384,7 +384,7 @@
fun context "-" thy = init NONE thy
| context target thy = init (SOME (locale_intern
- (Locale.test_locale thy (Locale.intern thy target)) thy target)) thy;
+ (Locale.defined thy (Locale.intern thy target)) thy target)) thy;
fun instantiation arities = init_lthy_ctxt (make_target "" false false false arities []);
fun instantiation_cmd raw_arities thy =
--- a/src/Pure/Isar/toplevel.ML Thu Jan 08 12:25:22 2009 -0800
+++ b/src/Pure/Isar/toplevel.ML Thu Jan 08 21:13:40 2009 -0800
@@ -1,5 +1,4 @@
(* Title: Pure/Isar/toplevel.ML
- ID: $Id$
Author: Markus Wenzel, TU Muenchen
Isabelle/Isar toplevel transactions.
@@ -66,6 +65,8 @@
val theory': (bool -> theory -> theory) -> transition -> transition
val begin_local_theory: bool -> (theory -> local_theory) -> transition -> transition
val end_local_theory: transition -> transition
+ val local_theory': xstring option -> (bool -> local_theory -> local_theory) ->
+ transition -> transition
val local_theory: xstring option -> (local_theory -> local_theory) -> transition -> transition
val present_local_theory: xstring option -> (node -> unit) -> transition -> transition
val local_theory_to_proof': xstring option -> (bool -> local_theory -> Proof.state) ->
@@ -512,14 +513,15 @@
(fn Theory (gthy, _) =>
let
val finish = loc_finish loc gthy;
- val lthy' = f (loc_begin loc gthy);
+ val lthy' = f int (loc_begin loc gthy);
in Theory (finish lthy', SOME lthy') end
| _ => raise UNDEF) #> tap g);
in
-fun local_theory loc f = local_theory_presentation loc f (K I);
-fun present_local_theory loc g = local_theory_presentation loc I g;
+fun local_theory' loc f = local_theory_presentation loc f (K I);
+fun local_theory loc f = local_theory' loc (K f);
+fun present_local_theory loc g = local_theory_presentation loc (K I) g;
end;
@@ -716,7 +718,7 @@
val (body_trs, end_tr) = split_last proof_trs;
val finish = Context.Theory o ProofContext.theory_of;
- val future_proof = Proof.future_proof
+ val future_proof = Proof.global_future_proof
(fn prf =>
Future.fork_pri ~1 (fn () =>
let val (states, State (result_node, _)) =
--- a/src/Pure/Tools/invoke.ML Thu Jan 08 12:25:22 2009 -0800
+++ b/src/Pure/Tools/invoke.ML Thu Jan 08 21:13:40 2009 -0800
@@ -88,7 +88,7 @@
|> (snd o ProofContext.note_thmss_i "" notes)
|> ProofContext.restore_naming ctxt
end) #>
- Proof.put_facts NONE #> Seq.single;
+ Proof.put_facts NONE;
in
state'
|> Proof.chain_facts chain_facts
--- a/src/Pure/context.ML Thu Jan 08 12:25:22 2009 -0800
+++ b/src/Pure/context.ML Thu Jan 08 21:13:40 2009 -0800
@@ -132,7 +132,15 @@
val copy_data = Datatab.map' invoke_copy;
val extend_data = Datatab.map' invoke_extend;
-fun merge_data pp = Datatab.join (invoke_merge pp) o pairself extend_data;
+
+fun merge_data pp (data1, data2) =
+ Datatab.keys (Datatab.merge (K true) (data1, data2))
+ |> Par_List.map (fn k =>
+ (case (Datatab.lookup data1 k, Datatab.lookup data2 k) of
+ (SOME x, NONE) => (k, invoke_extend k x)
+ | (NONE, SOME y) => (k, invoke_extend k y)
+ | (SOME x, SOME y) => (k, invoke_merge pp k (invoke_extend k x, invoke_extend k y))))
+ |> Datatab.make;
end;