# HG changeset patch
# User wenzelm
# Date 1519046797 -3600
# Node ID 50db601cba270136094b1f8a7351ffb5973b726b
# Parent  a5ab9ea36cd566419794392d38aef63dd48e9364
store facts as lazy values;

diff -r a5ab9ea36cd5 -r 50db601cba27 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Mon Feb 19 14:18:29 2018 +0100
+++ b/src/Pure/Isar/proof_context.ML	Mon Feb 19 14:26:37 2018 +0100
@@ -1062,9 +1062,11 @@
 
 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_thms flags arg ctxt =
+  ctxt |> map_facts_result (Facts.add_static (Context.Proof ctxt) flags arg);
+
+fun update_thms flags (b, SOME ths) ctxt = ctxt |> add_thms flags (b, Lazy.value ths) |> #2
+  | update_thms _ (b, NONE) ctxt = ctxt |> map_facts (Facts.del (full_name ctxt b));
 
 in
 
@@ -1077,7 +1079,8 @@
     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_thms {strict = false, index = index} (b, Lazy.value thms);
+  in ((name, thms), ctxt'') end);
 
 fun put_thms index thms ctxt = ctxt
   |> map_naming (K Name_Space.local_naming)
diff -r a5ab9ea36cd5 -r 50db601cba27 src/Pure/facts.ML
--- a/src/Pure/facts.ML	Mon Feb 19 14:18:29 2018 +0100
+++ b/src/Pure/facts.ML	Mon Feb 19 14:26:37 2018 +0100
@@ -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,38 @@
 
 local
 
+fun fold_static_lazy f =
+  Name_Space.fold_table (fn (a, Static ths) => f (a, ths) | _ => I) o facts_of;
+
+fun force facts =
+  let
+    val pending =
+      (facts, []) |-> fold_static_lazy (fn (_, ths) =>
+        if Lazy.is_pending ths then cons (fn () => Lazy.force_result ths) else I);
+  in
+    if Multithreading.relevant pending then
+      ignore (Future.forked_results {name = "Facts.force", deps = []} pending)
+    else List.app (fn e => ignore (e ())) pending
+  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) (tap force 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 (tap force 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 +260,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;
diff -r a5ab9ea36cd5 -r 50db601cba27 src/Pure/global_theory.ML
--- a/src/Pure/global_theory.ML	Mon Feb 19 14:18:29 2018 +0100
+++ b/src/Pure/global_theory.ML	Mon Feb 19 14:26:37 2018 +0100
@@ -135,7 +135,8 @@
       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);
+        (Facts.add_static (Context.Theory thy') {strict = true, index = false}
+          (b, Lazy.value thms'') #> snd);
     in (thms'', thy'') end;