--- a/src/HOL/Tools/Function/function_common.ML Mon Feb 19 16:47:05 2018 +0000
+++ b/src/HOL/Tools/Function/function_common.ML Tue Feb 20 09:34:03 2018 +0000
@@ -276,8 +276,7 @@
fun retrieve_function_data ctxt t =
Item_Net.retrieve (get_functions ctxt) t
- |> (map o apsnd)
- (transform_function_data (Morphism.transfer_morphism (Proof_Context.theory_of ctxt)));
+ |> (map o apsnd) (transform_function_data (Morphism.transfer_morphism' ctxt));
val add_function_data =
transform_function_data Morphism.trim_context_morphism #>
--- a/src/HOL/Tools/Function/partial_function.ML Mon Feb 19 16:47:05 2018 +0000
+++ b/src/HOL/Tools/Function/partial_function.ML Tue Feb 20 09:34:03 2018 +0000
@@ -60,7 +60,7 @@
fun lookup_mode ctxt =
Symtab.lookup (Modes.get (Context.Proof ctxt))
- #> Option.map (transform_setup_data (Morphism.transfer_morphism (Proof_Context.theory_of ctxt)));
+ #> Option.map (transform_setup_data (Morphism.transfer_morphism' ctxt));
(*** Automated monotonicity proofs ***)
--- a/src/HOL/Tools/Quotient/quotient_info.ML Mon Feb 19 16:47:05 2018 +0000
+++ b/src/HOL/Tools/Quotient/quotient_info.ML Tue Feb 20 09:34:03 2018 +0000
@@ -106,7 +106,7 @@
fun lookup_quotmaps_generic context name =
Symtab.lookup (get_quotmaps context) name
- |> Option.map (transform_quotmaps (Morphism.transfer_morphism (Context.theory_of context)))
+ |> Option.map (transform_quotmaps (Morphism.transfer_morphism'' context))
val lookup_quotmaps = lookup_quotmaps_generic o Context.Proof
val lookup_quotmaps_global = lookup_quotmaps_generic o Context.Theory
@@ -172,7 +172,7 @@
fun lookup_quotients_generic context name =
Symtab.lookup (get_quotients context) name
- |> Option.map (transform_quotients (Morphism.transfer_morphism (Context.theory_of context)))
+ |> Option.map (transform_quotients (Morphism.transfer_morphism'' context))
val lookup_quotients = lookup_quotients_generic o Context.Proof
val lookup_quotients_global = lookup_quotients_generic o Context.Theory
@@ -211,7 +211,7 @@
fun dest_quotconsts_generic context =
maps #2 (Symtab.dest (get_quotconsts context))
- |> map (transform_quotconsts (Morphism.transfer_morphism (Context.theory_of context)))
+ |> map (transform_quotconsts (Morphism.transfer_morphism'' context))
val dest_quotconsts = dest_quotconsts_generic o Context.Proof
val dest_quotconsts_global = dest_quotconsts_generic o Context.Theory
--- a/src/HOL/Tools/Transfer/transfer.ML Mon Feb 19 16:47:05 2018 +0000
+++ b/src/HOL/Tools/Transfer/transfer.ML Tue Feb 20 09:34:03 2018 +0000
@@ -868,7 +868,7 @@
end
fun lookup_pred_data ctxt type_name = Symtab.lookup (get_pred_data ctxt) type_name
- |> Option.map (morph_pred_data (Morphism.transfer_morphism (Proof_Context.theory_of ctxt)))
+ |> Option.map (morph_pred_data (Morphism.transfer_morphism' ctxt))
fun update_pred_data type_name qinfo ctxt =
Data.map (map_pred_data (Symtab.update (type_name, qinfo))) ctxt
--- a/src/HOL/Tools/inductive.ML Mon Feb 19 16:47:05 2018 +0000
+++ b/src/HOL/Tools/inductive.ML Tue Feb 20 09:34:03 2018 +0000
@@ -257,14 +257,14 @@
fun the_inductive ctxt term =
Item_Net.retrieve (#infos (rep_data ctxt)) term
|> the_single
- |> apsnd (transform_result (Morphism.transfer_morphism (Proof_Context.theory_of ctxt)))
+ |> apsnd (transform_result (Morphism.transfer_morphism' ctxt))
fun the_inductive_global ctxt name =
#infos (rep_data ctxt)
|> Item_Net.content
|> filter (fn ({names, ...}, _) => member op = names name)
|> the_single
- |> apsnd (transform_result (Morphism.transfer_morphism (Proof_Context.theory_of ctxt)))
+ |> apsnd (transform_result (Morphism.transfer_morphism' ctxt))
fun put_inductives info =
map_data (fn (infos, monos, equations) =>
--- a/src/HOL/Tools/typedef.ML Mon Feb 19 16:47:05 2018 +0000
+++ b/src/HOL/Tools/typedef.ML Tue Feb 20 09:34:03 2018 +0000
@@ -72,7 +72,7 @@
fun get_info_generic context =
Symtab.lookup_list (Data.get context) #>
- map (transform_info (Morphism.transfer_morphism (Context.theory_of context)));
+ map (transform_info (Morphism.transfer_morphism'' context));
val get_info = get_info_generic o Context.Proof;
val get_info_global = get_info_generic o Context.Theory;
--- a/src/Pure/Concurrent/future.ML Mon Feb 19 16:47:05 2018 +0000
+++ b/src/Pure/Concurrent/future.ML Tue Feb 20 09:34:03 2018 +0000
@@ -31,6 +31,8 @@
val join_result: 'a future -> 'a Exn.result
val joins: 'a future list -> 'a list
val join: 'a future -> 'a
+ val forked_results: {name: string, deps: Task_Queue.task list} ->
+ (unit -> 'a) list -> 'a Exn.result list
val task_context: string -> group -> ('a -> 'b) -> 'a -> 'b
val value_result: 'a Exn.result -> 'a future
val value: 'a -> 'a future
@@ -539,6 +541,24 @@
fun join x = Exn.release (join_result x);
+(* forked results: nested parallel evaluation *)
+
+fun forked_results {name, deps} es =
+ Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
+ let
+ val (group, pri) =
+ (case worker_task () of
+ SOME task =>
+ (new_group (SOME (Task_Queue.group_of_task task)), Task_Queue.pri_of_task task)
+ | NONE => (new_group NONE, 0));
+ val futures =
+ forks {name = name, group = SOME group, deps = deps, pri = pri, interrupts = true} es;
+ in
+ restore_attributes join_results futures
+ handle exn => (if Exn.is_interrupt exn then cancel_group group else (); Exn.reraise exn)
+ end) ();
+
+
(* task context for running thread *)
fun task_context name group f x =
--- a/src/Pure/Concurrent/lazy.ML Mon Feb 19 16:47:05 2018 +0000
+++ b/src/Pure/Concurrent/lazy.ML Tue Feb 20 09:34:03 2018 +0000
@@ -13,12 +13,16 @@
val lazy_name: string -> (unit -> 'a) -> 'a lazy
val lazy: (unit -> 'a) -> 'a lazy
val peek: 'a lazy -> 'a Exn.result option
+ val is_pending: 'a lazy -> bool
val is_running: 'a lazy -> bool
val is_finished: 'a lazy -> bool
val force_result: 'a lazy -> 'a Exn.result
val force: 'a lazy -> 'a
- val force_list: 'a lazy list -> 'a list
+ val force_value: 'a lazy -> 'a lazy
+ val trim_value: 'a lazy -> 'a lazy
val map: ('a -> 'b) -> 'a lazy -> 'b lazy
+ val map_finished: ('a -> 'b) -> 'a lazy -> 'b lazy
+ val consolidate: 'a lazy list -> 'a lazy list
val future: Future.params -> 'a lazy -> 'a future
end;
@@ -45,16 +49,18 @@
Expr _ => NONE
| Result res => Future.peek res);
-fun pending (Value _) = false
- | pending (Lazy var) =
+
+(* status *)
+
+fun is_value (Value _) = true
+ | is_value (Lazy _) = false;
+
+fun is_pending (Value _) = false
+ | is_pending (Lazy var) =
(case Synchronized.value var of
Expr _ => true
| Result _ => false);
-
-
-(* status *)
-
fun is_running (Value _) = false
| is_running (Lazy var) =
(case Synchronized.value var of
@@ -105,12 +111,29 @@
fun force x = Exn.release (force_result x);
-fun force_list xs =
- (List.app (fn x => if pending x then ignore (force_result x) else ()) xs;
- map force xs);
+fun force_value x = if is_value x then x else value (force x);
+fun trim_value x = if is_pending x then x else force_value x;
+
+
+(* map *)
fun map f x = lazy_name "Lazy.map" (fn () => f (force x));
+fun map_finished f x = if is_finished x then value (f (force x)) else map f x;
+
+
+(* consolidate in parallel *)
+
+fun consolidate xs =
+ let
+ val pending =
+ xs |> map_filter (fn x => if is_pending x then SOME (fn () => force_result x) else NONE);
+ val _ =
+ if Multithreading.relevant pending then
+ ignore (Future.forked_results {name = "Lazy.consolidate", deps = []} pending)
+ else List.app (fn e => ignore (e ())) pending;
+ in xs end;
+
(* future evaluation *)
--- a/src/Pure/Concurrent/multithreading.ML Mon Feb 19 16:47:05 2018 +0000
+++ b/src/Pure/Concurrent/multithreading.ML Tue Feb 20 09:34:03 2018 +0000
@@ -9,6 +9,7 @@
val max_threads: unit -> int
val max_threads_update: int -> unit
val enabled: unit -> bool
+ val relevant: 'a list -> bool
val sync_wait: Time.time option -> ConditionVar.conditionVar -> Mutex.mutex -> bool Exn.result
val trace: int ref
val tracing: int -> (unit -> string) -> unit
@@ -41,6 +42,8 @@
fun max_threads_update m = max_threads_state := max_threads_result m;
fun enabled () = max_threads () > 1;
+val relevant = (fn [] => false | [_] => false | _ => enabled ());
+
end;
--- a/src/Pure/Concurrent/par_list.ML Mon Feb 19 16:47:05 2018 +0000
+++ b/src/Pure/Concurrent/par_list.ML Tue Feb 20 09:34:03 2018 +0000
@@ -16,7 +16,6 @@
signature PAR_LIST =
sig
- val managed_results: string -> ('a -> 'b) -> 'a list -> 'b Exn.result list
val map_name: string -> ('a -> 'b) -> 'a list -> 'b list
val map_independent: ('a -> 'b) -> 'a list -> 'b list
val map: ('a -> 'b) -> 'a list -> 'b list
@@ -29,27 +28,12 @@
structure Par_List: PAR_LIST =
struct
-fun managed_results name f xs =
- if null xs orelse null (tl xs) orelse not (Multithreading.enabled ())
- then map (Exn.capture f) xs
- else
- Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
- let
- val (group, pri) =
- (case Future.worker_task () of
- SOME task =>
- (Future.new_group (SOME (Task_Queue.group_of_task task)), Task_Queue.pri_of_task task)
- | NONE => (Future.new_group NONE, 0));
- val futures =
- Future.forks {name = name, group = SOME group, deps = [], pri = pri, interrupts = true}
- (map (fn x => fn () => f x) xs);
- val results =
- restore_attributes Future.join_results futures
- handle exn =>
- (if Exn.is_interrupt exn then Future.cancel_group group else (); Exn.reraise exn);
- in results end) ();
+fun forked_results name f xs =
+ if Multithreading.relevant xs
+ then Future.forked_results {name = name, deps = []} (map (fn x => fn () => f x) xs)
+ else map (Exn.capture f) xs;
-fun map_name name f xs = Par_Exn.release_first (managed_results name f xs);
+fun map_name name f xs = Par_Exn.release_first (forked_results name f xs);
fun map f = map_name "Par_List.map" f;
fun map_independent f = map (Exn.interruptible_capture f) #> Par_Exn.release_all;
@@ -57,7 +41,7 @@
let
exception FOUND of 'b;
val results =
- managed_results "Par_List.get_some"
+ forked_results "Par_List.get_some"
(fn x => (case f x of NONE => () | SOME y => raise FOUND y)) xs;
in
(case get_first (fn Exn.Exn (FOUND res) => SOME res | _ => NONE) results of
--- a/src/Pure/Isar/attrib.ML Mon Feb 19 16:47:05 2018 +0000
+++ b/src/Pure/Isar/attrib.ML Tue Feb 20 09:34:03 2018 +0000
@@ -39,6 +39,7 @@
(string * thm list) list * Proof.context
val generic_notes: string -> fact list -> Context.generic ->
(string * thm list) list * Context.generic
+ val lazy_notes: string -> binding * thm list lazy -> Context.generic -> Context.generic
val eval_thms: Proof.context -> (Facts.ref * Token.src list) list -> thm list
val attribute_syntax: attribute context_parser -> Token.src -> attribute
val setup: binding -> attribute context_parser -> string -> theory -> theory
@@ -195,6 +196,9 @@
fun generic_notes kind facts context = context |>
Context.mapping_result (global_notes kind facts) (local_notes kind facts);
+fun lazy_notes kind arg =
+ Context.mapping (Global_Theory.add_thms_lazy kind arg) (Proof_Context.add_thms_lazy kind arg);
+
fun eval_thms ctxt srcs = ctxt
|> Proof_Context.note_thmss ""
(map_facts_refs
--- a/src/Pure/Isar/class_declaration.ML Mon Feb 19 16:47:05 2018 +0000
+++ b/src/Pure/Isar/class_declaration.ML Tue Feb 20 09:34:03 2018 +0000
@@ -174,6 +174,8 @@
| filter_element (Element.Defines _) =
error ("\"defines\" element not allowed in class specification.")
| filter_element (Element.Notes _) =
+ error ("\"notes\" element not allowed in class specification.")
+ | filter_element (Element.Lazy_Notes _) =
error ("\"notes\" element not allowed in class specification.");
val inferred_elems = map_filter filter_element raw_inferred_elems;
fun fold_element_types f (Element.Fixes fxs) = fold (fn (_, SOME T, _) => f T) fxs
--- a/src/Pure/Isar/element.ML Mon Feb 19 16:47:05 2018 +0000
+++ b/src/Pure/Isar/element.ML Tue Feb 20 09:34:03 2018 +0000
@@ -20,7 +20,8 @@
Constrains of (string * 'typ) list |
Assumes of (Attrib.binding * ('term * 'term list) list) list |
Defines of (Attrib.binding * ('term * 'term list)) list |
- Notes of string * (Attrib.binding * ('fact * Token.src list) list) list
+ Notes of string * (Attrib.binding * ('fact * Token.src list) list) list |
+ Lazy_Notes of string * (binding * 'fact lazy)
type context = (string, string, Facts.ref) ctxt
type context_i = (typ, term, thm list) ctxt
val map_ctxt: {binding: binding -> binding, typ: 'typ -> 'a, term: 'term -> 'b,
@@ -51,7 +52,6 @@
val satisfy_morphism: witness list -> morphism
val eq_morphism: theory -> thm list -> morphism option
val init: context_i -> Context.generic -> Context.generic
- val init': context_i -> Context.generic -> Context.generic
val activate_i: context_i -> Proof.context -> context_i * Proof.context
val activate: (typ, term, Facts.ref) ctxt -> Proof.context -> context_i * Proof.context
end;
@@ -82,7 +82,8 @@
Constrains of (string * 'typ) list |
Assumes of (Attrib.binding * ('term * 'term list) list) list |
Defines of (Attrib.binding * ('term * 'term list)) list |
- Notes of string * (Attrib.binding * ('fact * Token.src list) list) list;
+ Notes of string * (Attrib.binding * ('fact * Token.src list) list) list |
+ Lazy_Notes of string * (binding * 'fact lazy);
type context = (string, string, Facts.ref) ctxt;
type context_i = (typ, term, thm list) ctxt;
@@ -96,7 +97,8 @@
| Defines defs => Defines (defs |> map (fn ((a, atts), (t, ps)) =>
((binding a, map attrib atts), (term t, map pattern ps))))
| Notes (kind, facts) => Notes (kind, facts |> map (fn ((a, atts), bs) =>
- ((binding a, map attrib atts), bs |> map (fn (ths, btts) => (fact ths, map attrib btts)))));
+ ((binding a, map attrib atts), bs |> map (fn (ths, btts) => (fact ths, map attrib btts)))))
+ | Lazy_Notes (kind, (a, ths)) => Lazy_Notes (kind, (binding a, Lazy.map fact ths));
fun map_ctxt_attrib attrib =
map_ctxt {binding = I, typ = I, term = I, pattern = I, fact = I, attrib = attrib};
@@ -180,13 +182,17 @@
fun prt_note (a, ths) =
Pretty.block (Pretty.breaks (flat (prt_binding a " =" :: map prt_fact ths)));
+
+ fun notes_kind "" = "notes"
+ | notes_kind kind = "notes " ^ kind;
in
fn Fixes fixes => pretty_items "fixes" "and" (map prt_fix fixes)
| Constrains xs => pretty_items "constrains" "and" (map prt_constrain xs)
| Assumes asms => pretty_items "assumes" "and" (map prt_asm asms)
| Defines defs => pretty_items "defines" "and" (map prt_def defs)
- | Notes ("", facts) => pretty_items "notes" "and" (map prt_note facts)
- | Notes (kind, facts) => pretty_items ("notes " ^ kind) "and" (map prt_note facts)
+ | Notes (kind, facts) => pretty_items (notes_kind kind) "and" (map prt_note facts)
+ | Lazy_Notes (kind, (a, ths)) =>
+ pretty_items (notes_kind kind) "and" [prt_note ((a, []), [(Lazy.force ths, [])])]
end;
val pretty_ctxt = gen_pretty_ctxt true;
@@ -500,15 +506,8 @@
|> fold Variable.auto_fixes (map #1 asms)
|> Proof_Context.add_assms Local_Defs.def_export (map #2 asms);
in ctxt' end)
- | init (Notes (kind, facts)) = Attrib.generic_notes kind facts #> #2;
-
-fun init' elem context =
- context
- |> Context.mapping I (Thm.unchecked_hyps #> Context_Position.not_really)
- |> init elem
- |> Context.mapping I (fn ctxt =>
- let val ctxt0 = Context.proof_of context
- in ctxt |> Context_Position.restore_visible ctxt0 |> Thm.restore_hyps ctxt0 end);
+ | init (Notes (kind, facts)) = Attrib.generic_notes kind facts #> #2
+ | init (Lazy_Notes (kind, ths)) = Attrib.lazy_notes kind ths;
(* activate *)
--- a/src/Pure/Isar/expression.ML Mon Feb 19 16:47:05 2018 +0000
+++ b/src/Pure/Isar/expression.ML Tue Feb 20 09:34:03 2018 +0000
@@ -239,7 +239,8 @@
| extract_elem (Constrains csts) = map (#2 #> single #> map mk_type) csts
| extract_elem (Assumes asms) = map (#2 #> map mk_propp) asms
| extract_elem (Defines defs) = map (fn (_, (t, ps)) => [mk_propp (t, ps)]) defs
- | extract_elem (Notes _) = [];
+ | extract_elem (Notes _) = []
+ | extract_elem (Lazy_Notes _) = [];
fun restore_elem (Fixes fixes, css) =
(fixes ~~ css) |> map (fn ((x, _, mx), cs) =>
@@ -251,7 +252,8 @@
(asms ~~ css) |> map (fn ((b, _), cs) => (b, map dest_propp cs)) |> Assumes
| restore_elem (Defines defs, css) =
(defs ~~ css) |> map (fn ((b, _), [c]) => (b, dest_propp c)) |> Defines
- | restore_elem (Notes notes, _) = Notes notes;
+ | restore_elem (elem as Notes _, _) = elem
+ | restore_elem (elem as Lazy_Notes _, _) = elem;
fun prep (_, pats) (ctxt, t :: ts) =
let val ctxt' = Variable.auto_fixes t ctxt
@@ -298,7 +300,8 @@
ctxt |> fold_map (fn (x, T) => prep_var (Binding.name x, SOME T, NoSyn)) csts |> snd
| declare_elem _ (Assumes _) ctxt = ctxt
| declare_elem _ (Defines _) ctxt = ctxt
- | declare_elem _ (Notes _) ctxt = ctxt;
+ | declare_elem _ (Notes _) ctxt = ctxt
+ | declare_elem _ (Lazy_Notes _) ctxt = ctxt;
(** Finish locale elements **)
@@ -346,7 +349,8 @@
| finish_elem _ _ _ (Constrains _) = Constrains []
| finish_elem ctxts parms do_close (Assumes asms) = closeup ctxts parms do_close (Assumes asms)
| finish_elem ctxts parms do_close (Defines defs) = closeup ctxts parms do_close (Defines defs)
- | finish_elem _ _ _ (Notes facts) = Notes facts;
+ | finish_elem _ _ _ (elem as Notes _) = elem
+ | finish_elem _ _ _ (elem as Lazy_Notes _) = elem;
end;
@@ -592,7 +596,8 @@
in (spec', (fold Term.add_frees ts' xs, env, defs)) end
| eval_text ctxt _ (Defines defs) (spec, binds) =
(spec, fold (bind_def ctxt o #1 o #2) defs binds)
- | eval_text _ _ (Notes _) text = text;
+ | eval_text _ _ (Notes _) text = text
+ | eval_text _ _ (Lazy_Notes _) text = text;
fun eval_inst ctxt (loc, morph) text =
let
@@ -772,9 +777,7 @@
[(Attrib.internal o K) Locale.witness_add])])) defs)
| defines_to_notes _ e = e;
-fun is_hyp (elem as Assumes asms) = true
- | is_hyp (elem as Defines defs) = true
- | is_hyp _ = false;
+val is_hyp = fn Assumes _ => true | Defines _ => true | _ => false;
fun gen_add_locale prep_decl
binding raw_predicate_binding raw_import raw_body thy =
--- a/src/Pure/Isar/locale.ML Mon Feb 19 16:47:05 2018 +0000
+++ b/src/Pure/Isar/locale.ML Tue Feb 20 09:34:03 2018 +0000
@@ -59,8 +59,8 @@
val add_declaration: string -> bool -> declaration -> Proof.context -> Proof.context
(* Activation *)
+ val activate_facts: morphism option -> string * morphism -> Context.generic -> Context.generic
val activate_declarations: string * morphism -> Proof.context -> Proof.context
- val activate_facts: morphism option -> string * morphism -> Context.generic -> Context.generic
val init: string -> theory -> Proof.context
(* Reasoning about locales *)
@@ -407,6 +407,34 @@
(pretty_reg (Context.proof_of context) Morphism.identity (name, morph) |>
Pretty.string_of));
+fun init_element elem context =
+ context
+ |> Context.mapping I (Thm.unchecked_hyps #> Context_Position.not_really)
+ |> Element.init elem
+ |> Context.mapping I (fn ctxt =>
+ let val ctxt0 = Context.proof_of context
+ in ctxt |> Context_Position.restore_visible ctxt0 |> Thm.restore_hyps ctxt0 end);
+
+
+(* Potentially lazy notes *)
+
+fun lazy_notes thy loc =
+ rev (#notes (the_locale thy loc)) |> maps (fn ((kind, notes), _) =>
+ notes |> map (fn ((b, atts), facts) =>
+ if null atts andalso forall (null o #2) facts andalso false (* FIXME *)
+ then Lazy_Notes (kind, (b, Lazy.value (maps #1 facts)))
+ else Notes (kind, [((b, atts), facts)])));
+
+fun consolidate_notes elems =
+ (elems
+ |> map_filter (fn Lazy_Notes (_, (_, ths)) => SOME ths | _ => NONE)
+ |> Lazy.consolidate;
+ elems);
+
+fun force_notes (Lazy_Notes (kind, (b, ths))) = Notes (kind, [((b, []), [(Lazy.force ths, [])])])
+ | force_notes elem = elem;
+
+
(* Declarations, facts and entire locale content *)
fun activate_syntax_decls (name, morph) context =
@@ -427,15 +455,11 @@
NONE => Morphism.identity
| SOME export => collect_mixins context (name, morph $> export) $> export);
val morph' = transfer input $> morph $> mixin;
- val notes' =
- grouped 100 Par_List.map
- (Element.transform_ctxt morph' o Notes o #1) (#notes (the_locale thy name));
+ val notes' = grouped 100 Par_List.map (Element.transform_ctxt morph') (lazy_notes thy name);
in
- input
- |> fold_rev
- (fn elem => fn res => activ_elem (Element.transform_ctxt (transfer res) elem) res) notes'
- handle ERROR msg => activate_err msg (name, morph) context
- end;
+ (notes', input) |-> fold (fn elem => fn res =>
+ activ_elem (Element.transform_ctxt (transfer res) elem) res)
+ end handle ERROR msg => activate_err msg (name, morph) context;
fun activate_all name thy activ_elem transfer (marked, input) =
let
@@ -455,6 +479,16 @@
(** Public activation functions **)
+fun activate_facts export dep context =
+ context
+ |> Context_Position.set_visible_generic false
+ |> pair (Idents.get context)
+ |> roundup (Context.theory_of context)
+ (activate_notes init_element Morphism.transfer_morphism'' context export)
+ (the_default Morphism.identity export) dep
+ |-> Idents.put
+ |> Context_Position.restore_visible_generic context;
+
fun activate_declarations dep = Context.proof_map (fn context =>
context
|> Context_Position.set_visible_generic false
@@ -463,16 +497,6 @@
|-> Idents.put
|> Context_Position.restore_visible_generic context);
-fun activate_facts export dep context =
- context
- |> Context_Position.set_visible_generic false
- |> pair (Idents.get context)
- |> roundup (Context.theory_of context)
- (activate_notes Element.init' (Morphism.transfer_morphism o Context.theory_of) context export)
- (the_default Morphism.identity export) dep
- |-> Idents.put
- |> Context_Position.restore_visible_generic context;
-
fun init name thy =
let
val context = Context.Proof (Proof_Context.init_global thy);
@@ -481,7 +505,7 @@
context
|> Context_Position.set_visible_generic false
|> pair empty_idents
- |> activate_all name thy Element.init' (Morphism.transfer_morphism o Context.theory_of)
+ |> activate_all name thy init_element Morphism.transfer_morphism''
|-> (fn marked' => Idents.put (merge_idents (marked, marked')))
|> Context_Position.restore_visible_generic context
|> Context.proof_of
@@ -674,10 +698,13 @@
let
val locale_ctxt = init name thy;
fun cons_elem (elem as Notes _) = show_facts ? cons elem
+ | cons_elem (elem as Lazy_Notes _) = show_facts ? cons elem
| cons_elem elem = cons elem;
val elems =
activate_all name thy cons_elem (K (Morphism.transfer_morphism thy)) (empty_idents, [])
- |> snd |> rev;
+ |> snd |> rev
+ |> consolidate_notes
+ |> map force_notes;
in
Pretty.keyword1 "locale" :: Pretty.brk 1 :: pretty_name locale_ctxt name ::
maps (fn elem => [Pretty.fbrk, Pretty.chunks (Element.pretty_ctxt locale_ctxt elem)]) elems
--- a/src/Pure/Isar/proof_context.ML Mon Feb 19 16:47:05 2018 +0000
+++ b/src/Pure/Isar/proof_context.ML Tue Feb 20 09:34:03 2018 +0000
@@ -129,6 +129,7 @@
val restore_stmt: Proof.context -> Proof.context -> Proof.context
val add_thms_dynamic: binding * (Context.generic -> thm list) ->
Proof.context -> string * Proof.context
+ val add_thms_lazy: string -> (binding * thm list lazy) -> Proof.context -> Proof.context
val note_thmss: string -> (Thm.binding * (thm list * attribute list) list) list ->
Proof.context -> (string * thm list) list * Proof.context
val put_thms: bool -> string * thm list option -> Proof.context -> Proof.context
@@ -1062,27 +1063,36 @@
local
-fun update_thms _ (b, NONE) ctxt = ctxt |> map_facts (Facts.del (full_name ctxt b))
- | update_thms flags (b, SOME ths) ctxt = ctxt |> map_facts
- (Facts.add_static (Context.Proof ctxt) flags (b, ths) #> snd);
+fun add_facts {index} arg ctxt = ctxt
+ |> map_facts_result (Facts.add_static (Context.Proof ctxt) {strict = false, index = index} arg);
+
+fun update_facts flags (b, SOME ths) ctxt = ctxt |> add_facts flags (b, Lazy.value ths) |> #2
+ | update_facts _ (b, NONE) ctxt = ctxt |> map_facts (Facts.del (full_name ctxt b));
in
-fun note_thmss kind = fold_map (fn ((b, more_atts), raw_facts) => fn ctxt =>
+fun add_thms_lazy kind (b, ths) ctxt =
let
val name = full_name ctxt b;
- val facts = Global_Theory.name_thmss false name raw_facts;
+ val ths' = Lazy.map (Global_Theory.name_thms true false name #> map (Thm.kind_rule kind)) ths;
+ val (_, ctxt') = add_facts {index = is_stmt ctxt} (b, ths') ctxt;
+ in ctxt' end;
+
+fun note_thmss kind = fold_map (fn ((b, more_atts), facts) => fn ctxt =>
+ let
+ val name = full_name ctxt b;
+ val facts' = Global_Theory.name_thmss false name facts;
fun app (ths, atts) =
fold_map (Thm.proof_attributes (surround (Thm.kind kind) (atts @ more_atts))) ths;
- val (res, ctxt') = fold_map app facts ctxt;
+ val (res, ctxt') = fold_map app facts' ctxt;
val thms = Global_Theory.name_thms false false name (flat res);
- val index = is_stmt ctxt;
- in ((name, thms), ctxt' |> update_thms {strict = false, index = index} (b, SOME thms)) end);
+ val (_, ctxt'') = ctxt' |> add_facts {index = is_stmt ctxt} (b, Lazy.value thms);
+ in ((name, thms), ctxt'') end);
fun put_thms index thms ctxt = ctxt
|> map_naming (K Name_Space.local_naming)
|> Context_Position.set_visible false
- |> update_thms {strict = false, index = index} (apfst Binding.name thms)
+ |> update_facts {index = index} (apfst Binding.name thms)
|> Context_Position.restore_visible ctxt
|> restore_naming ctxt;
--- a/src/Pure/PIDE/execution.ML Mon Feb 19 16:47:05 2018 +0000
+++ b/src/Pure/PIDE/execution.ML Tue Feb 20 09:34:03 2018 +0000
@@ -162,13 +162,12 @@
fun fork_prints exec_id =
(case Inttab.lookup (#2 (get_state ())) exec_id of
SOME (_, prints) =>
- if null prints orelse null (tl prints) orelse not (Multithreading.enabled ())
- then List.app (fn {body, ...} => body ()) (rev prints)
- else
+ if Multithreading.relevant prints then
let val pos = Position.thread_data () in
List.app (fn {name, pri, body} =>
ignore (fork {name = name, pos = pos, pri = pri} body)) (rev prints)
end
+ else List.app (fn {body, ...} => body ()) (rev prints)
| NONE => raise Fail (unregistered exec_id));
--- a/src/Pure/facts.ML Mon Feb 19 16:47:05 2018 +0000
+++ b/src/Pure/facts.ML Tue Feb 20 09:34:03 2018 +0000
@@ -40,7 +40,7 @@
val could_unify: T -> term -> (thm * Position.T) list
val merge: T * T -> T
val add_static: Context.generic -> {strict: bool, index: bool} ->
- binding * thm list -> T -> string * T
+ binding * thm list lazy -> T -> string * T
val add_dynamic: Context.generic -> binding * (Context.generic -> thm list) -> T -> string * T
val del: string -> T -> T
val hide: bool -> string -> T -> T
@@ -130,7 +130,7 @@
(* datatypes *)
-datatype fact = Static of thm list | Dynamic of Context.generic -> thm list;
+datatype fact = Static of thm list lazy | Dynamic of Context.generic -> thm list;
datatype T = Facts of
{facts: fact Name_Space.table,
@@ -178,7 +178,7 @@
fun lookup context facts name =
(case Name_Space.lookup (facts_of facts) name of
NONE => NONE
- | SOME (Static ths) => SOME {dynamic = false, thms = ths}
+ | SOME (Static ths) => SOME {dynamic = false, thms = Lazy.force ths}
| SOME (Dynamic f) => SOME {dynamic = true, thms = f context});
fun retrieve context facts (xname, pos) =
@@ -203,23 +203,34 @@
local
+fun fold_static_lazy f =
+ Name_Space.fold_table (fn (a, Static ths) => f (a, ths) | _ => I) o facts_of;
+
+fun consolidate facts =
+ let
+ val pending =
+ (facts, []) |-> fold_static_lazy (fn (_, ths) => if Lazy.is_pending ths then cons ths else I);
+ val _ = Lazy.consolidate pending;
+ in facts end;
+
fun included verbose prev_facts facts name =
not (exists (fn prev => defined prev name) prev_facts orelse
not verbose andalso is_concealed facts name);
in
-fun fold_static f =
- Name_Space.fold_table (fn (a, Static ths) => f (a, ths) | _ => I) o facts_of;
+fun fold_static f facts =
+ fold_static_lazy (f o apsnd Lazy.force) (consolidate facts);
fun dest_static verbose prev_facts facts =
fold_static (fn (a, ths) => included verbose prev_facts facts a ? cons (a, ths)) facts []
|> sort_by #1;
fun dest_all context verbose prev_facts facts =
- Name_Space.fold_table (fn (a, fact) =>
- let val ths = (case fact of Static ths => ths | Dynamic f => f context)
- in included verbose prev_facts facts a ? cons (a, ths) end) (facts_of facts) []
+ (facts_of (consolidate facts), [])
+ |-> Name_Space.fold_table (fn (a, fact) =>
+ let val ths = (case fact of Static ths => Lazy.force ths | Dynamic f => f context)
+ in included verbose prev_facts facts a ? cons (a, ths) end)
|> sort_by #1;
end;
@@ -245,24 +256,23 @@
in make_facts facts' props' end;
-(* add static entries *)
+(* add entries *)
+
+fun add_prop pos th =
+ Net.insert_term (K false) (Thm.full_prop_of th, (th, pos));
fun add_static context {strict, index} (b, ths) (Facts {facts, props}) =
let
- val ths' = map Thm.trim_context ths;
- val pos = Binding.pos_of (Binding.default_pos b);
-
+ val ths' = ths
+ |> index ? Lazy.force_value
+ |> Lazy.map_finished (map Thm.trim_context);
val (name, facts') =
if Binding.is_empty b then ("", facts)
else Name_Space.define context strict (b, Static ths') facts;
-
val props' = props
- |> index ? fold (fn th => Net.insert_term (K false) (Thm.full_prop_of th, (th, pos))) ths';
+ |> index ? fold (add_prop (Binding.pos_of (Binding.default_pos b))) (Lazy.force ths');
in (name, make_facts facts' props') end;
-
-(* add dynamic entries *)
-
fun add_dynamic context (b, f) (Facts {facts, props}) =
let val (name, facts') = Name_Space.define context true (b, Dynamic f) facts;
in (name, make_facts facts' props) end;
--- a/src/Pure/global_theory.ML Mon Feb 19 16:47:05 2018 +0000
+++ b/src/Pure/global_theory.ML Tue Feb 20 09:34:03 2018 +0000
@@ -24,6 +24,7 @@
val name_thm: bool -> bool -> string -> thm -> thm
val name_thms: bool -> bool -> string -> thm list -> thm list
val name_thmss: bool -> string -> (thm list * 'a) list -> (thm list * 'a) list
+ val add_thms_lazy: string -> (binding * thm list lazy) -> theory -> theory
val store_thms: binding * thm list -> theory -> thm list * theory
val store_thm: binding * thm -> theory -> thm * theory
val store_thm_open: binding * thm -> theory -> thm * theory
@@ -124,19 +125,28 @@
(* enter_thms *)
-fun register_proofs thms thy = (thms, Thm.register_proofs thms thy);
+fun register_proofs thms thy = (thms, Thm.register_proofs (Lazy.value thms) thy);
-fun enter_thms pre_name post_name app_att (b, thms) thy =
- if Binding.is_empty b
- then app_att thms thy |-> register_proofs
+fun add_facts arg thy =
+ thy |> Data.map (Facts.add_static (Context.Theory thy) {strict = true, index = false} arg #> #2);
+
+fun add_thms_lazy kind (b, thms) thy =
+ if Binding.is_empty b then Thm.register_proofs thms thy
else
let
val name = Sign.full_name thy b;
- val (thms', thy') = app_att (pre_name name thms) thy |>> post_name name |-> register_proofs;
- val thms'' = map (Thm.transfer thy') thms';
- val thy'' = thy' |> Data.map
- (Facts.add_static (Context.Theory thy') {strict = true, index = false} (b, thms'') #> snd);
- in (thms'', thy'') end;
+ val thms' = Lazy.map_finished (name_thms true true name #> map (Thm.kind_rule kind)) thms;
+ in thy |> Thm.register_proofs thms' |> add_facts (b, thms') end;
+
+fun enter_thms pre_name post_name app_att (b, thms) thy =
+ if Binding.is_empty b then app_att thms thy |-> register_proofs
+ else
+ let
+ val name = Sign.full_name thy b;
+ val (thms', thy') =
+ app_att (pre_name name thms) thy |>> post_name name |-> register_proofs;
+ val thy'' = thy' |> add_facts (b, Lazy.value thms');
+ in (map (Thm.transfer thy'') thms', thy'') end;
(* store_thm(s) *)
--- a/src/Pure/more_thm.ML Mon Feb 19 16:47:05 2018 +0000
+++ b/src/Pure/more_thm.ML Tue Feb 20 09:34:03 2018 +0000
@@ -112,7 +112,7 @@
val tag: string * string -> attribute
val untag: string -> attribute
val kind: string -> attribute
- val register_proofs: thm list -> theory -> theory
+ val register_proofs: thm list lazy -> theory -> theory
val consolidate_theory: theory -> unit
val show_consts_raw: Config.raw
val show_consts: bool Config.T
@@ -643,17 +643,21 @@
structure Proofs = Theory_Data
(
- type T = thm list;
+ type T = thm list lazy list;
val empty = [];
fun extend _ = empty;
fun merge _ = empty;
);
-fun register_proofs more_thms =
- Proofs.map (fold (cons o Thm.trim_context) more_thms);
+fun register_proofs ths =
+ (Proofs.map o cons) (Lazy.map_finished (map Thm.trim_context) ths);
fun consolidate_theory thy =
- Thm.consolidate (map (Thm.transfer thy) (rev (Proofs.get thy)));
+ let
+ val proofs = Proofs.get thy;
+ val pending = fold (fn ths => if Lazy.is_pending ths then cons ths else I) [] proofs;
+ val _ = Lazy.consolidate pending;
+ in Thm.consolidate (maps (map (Thm.transfer thy) o Lazy.force) (rev proofs)) end;
--- a/src/Pure/morphism.ML Mon Feb 19 16:47:05 2018 +0000
+++ b/src/Pure/morphism.ML Tue Feb 20 09:34:03 2018 +0000
@@ -39,6 +39,8 @@
val fact_morphism: string -> (thm list -> thm list) -> morphism
val thm_morphism: string -> (thm -> thm) -> morphism
val transfer_morphism: theory -> morphism
+ val transfer_morphism': Proof.context -> morphism
+ val transfer_morphism'': Context.generic -> morphism
val trim_context_morphism: morphism
val instantiate_morphism:
((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list -> morphism
@@ -120,6 +122,9 @@
fun thm_morphism a thm = morphism a {binding = [], typ = [], term = [], fact = [map thm]};
val transfer_morphism = thm_morphism "transfer" o Thm.transfer;
+val transfer_morphism' = transfer_morphism o Proof_Context.theory_of;
+val transfer_morphism'' = transfer_morphism o Context.theory_of;
+
val trim_context_morphism = thm_morphism "trim_context" Thm.trim_context;
fun instantiate_morphism ([], []) = identity
--- a/src/Pure/par_tactical.ML Mon Feb 19 16:47:05 2018 +0000
+++ b/src/Pure/par_tactical.ML Tue Feb 20 09:34:03 2018 +0000
@@ -41,20 +41,22 @@
in
fun PARALLEL_GOALS tac st =
- if not (Multithreading.enabled ()) orelse Thm.nprems_of st <= 1 then DETERM tac st
- else
- let val subgoals = map (Thm.adjust_maxidx_cterm ~1) (Drule.strip_imp_prems (Thm.cprop_of st)) in
- if exists (fn sg => Thm.maxidx_of_cterm sg >= 0) subgoals then DETERM tac st
- else
- let
- fun try_tac g =
- (case SINGLE tac g of
- NONE => raise FAILED ()
- | SOME g' => g');
- val results = Par_List.map (try_tac o Goal.init) subgoals;
- in EVERY (map retrofit (rev results)) st end
- handle FAILED () => Seq.empty
- end;
+ let
+ val goals =
+ Drule.strip_imp_prems (Thm.cprop_of st)
+ |> map (Thm.adjust_maxidx_cterm ~1);
+ in
+ if Multithreading.relevant goals andalso forall (fn g => Thm.maxidx_of_cterm g = ~1) goals then
+ let
+ fun try_goal g =
+ (case SINGLE tac (Goal.init g) of
+ NONE => raise FAILED ()
+ | SOME st' => st');
+ val results = Par_List.map try_goal goals;
+ in EVERY (map retrofit (rev results)) st
+ end handle FAILED () => Seq.empty
+ else DETERM tac st
+ end;
end;
--- a/src/Pure/proofterm.ML Mon Feb 19 16:47:05 2018 +0000
+++ b/src/Pure/proofterm.ML Tue Feb 20 09:34:03 2018 +0000
@@ -199,7 +199,7 @@
val consolidate =
maps (fn PBody {thms, ...} => map (thm_node_consolidate o #2) thms)
- #> Lazy.force_list #> ignore;
+ #> Lazy.consolidate #> map Lazy.force #> ignore;
fun make_thm_node name prop body =
Thm_Node {name = name, prop = prop, body = body,