# HG changeset patch
# User wenzelm
# Date 1519074441 -3600
# Node ID 857da80611ab936c7fabafc7bbb18f9662df3ad7
# Parent  96801289bbadcca804c154260c8d08a85615bf5e
support for lazy notes in global/local context and Element.Lazy_Notes: name binding and fact without attributes;
register_proofs is now based on lazy thms, but Thm.consolidate_theory will eventually force this (in parallel);
support for lazy notes for locale activation (still inactive);

diff -r 96801289bbad -r 857da80611ab src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Mon Feb 19 18:18:43 2018 +0100
+++ b/src/Pure/Isar/attrib.ML	Mon Feb 19 22:07:21 2018 +0100
@@ -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
diff -r 96801289bbad -r 857da80611ab src/Pure/Isar/class_declaration.ML
--- a/src/Pure/Isar/class_declaration.ML	Mon Feb 19 18:18:43 2018 +0100
+++ b/src/Pure/Isar/class_declaration.ML	Mon Feb 19 22:07:21 2018 +0100
@@ -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
diff -r 96801289bbad -r 857da80611ab src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Mon Feb 19 18:18:43 2018 +0100
+++ b/src/Pure/Isar/element.ML	Mon Feb 19 22:07:21 2018 +0100
@@ -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,
@@ -81,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;
@@ -95,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};
@@ -179,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;
@@ -499,7 +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;
+  | init (Notes (kind, facts)) = Attrib.generic_notes kind facts #> #2
+  | init (Lazy_Notes (kind, ths)) = Attrib.lazy_notes kind ths;
 
 
 (* activate *)
diff -r 96801289bbad -r 857da80611ab src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Mon Feb 19 18:18:43 2018 +0100
+++ b/src/Pure/Isar/expression.ML	Mon Feb 19 22:07:21 2018 +0100
@@ -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
diff -r 96801289bbad -r 857da80611ab src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Mon Feb 19 18:18:43 2018 +0100
+++ b/src/Pure/Isar/locale.ML	Mon Feb 19 22:07:21 2018 +0100
@@ -407,8 +407,6 @@
     (pretty_reg (Context.proof_of context) Morphism.identity (name, morph) |>
       Pretty.string_of));
 
-(* Declarations, facts and entire locale content *)
-
 fun init_element elem context =
   context
   |> Context.mapping I (Thm.unchecked_hyps #> Context_Position.not_really)
@@ -417,6 +415,28 @@
       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 =
   let
     val thy = Context.theory_of context;
@@ -435,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
@@ -682,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
diff -r 96801289bbad -r 857da80611ab src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Mon Feb 19 18:18:43 2018 +0100
+++ b/src/Pure/Isar/proof_context.ML	Mon Feb 19 22:07:21 2018 +0100
@@ -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
@@ -1070,6 +1071,13 @@
 
 in
 
+fun add_thms_lazy kind (b, ths) ctxt =
+  let
+    val name = full_name ctxt b;
+    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;
diff -r 96801289bbad -r 857da80611ab src/Pure/global_theory.ML
--- a/src/Pure/global_theory.ML	Mon Feb 19 18:18:43 2018 +0100
+++ b/src/Pure/global_theory.ML	Mon Feb 19 22:07:21 2018 +0100
@@ -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,18 +125,27 @@
 
 (* 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 thy'' = thy' |> Data.map
-        (Facts.add_static (Context.Theory thy') {strict = true, index = false}
-          (b, Lazy.value thms') #> snd);
+      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;
 
 
diff -r 96801289bbad -r 857da80611ab src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Mon Feb 19 18:18:43 2018 +0100
+++ b/src/Pure/more_thm.ML	Mon Feb 19 22:07:21 2018 +0100
@@ -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;