added system option "strict_facts";
authorwenzelm
Fri Jul 20 03:14:44 2018 +0200 (14 months ago)
changeset 686615820f0f379ae
parent 68660 4ce18f389f53
child 68666 4bee4828cfc3
added system option "strict_facts";
NEWS
etc/options
src/Pure/Isar/proof_context.ML
src/Pure/global_theory.ML
     1.1 --- a/NEWS	Wed Jul 18 20:51:23 2018 +0200
     1.2 +++ b/NEWS	Fri Jul 20 03:14:44 2018 +0200
     1.3 @@ -22,6 +22,12 @@
     1.4  * Global facts need to be closed: no free variables and no hypotheses.
     1.5  Rare INCOMPATIBILITY.
     1.6  
     1.7 +* Facts stemming from locale interpretation are subject to lazy
     1.8 +evaluation for improved performance. Rare INCOMPATIBILITY: errors
     1.9 +stemming from interpretation morphisms might be deferred and thus
    1.10 +difficult to locate; enable system option "strict_facts" temporarily to
    1.11 +avoid this.
    1.12 +
    1.13  * Marginal comments need to be written exclusively in the new-style form
    1.14  "\<comment> \<open>text\<close>", old ASCII variants like "-- {* ... *}" are no longer
    1.15  supported. INCOMPATIBILITY, use the command-line tool "isabelle
     2.1 --- a/etc/options	Wed Jul 18 20:51:23 2018 +0200
     2.2 +++ b/etc/options	Fri Jul 20 03:14:44 2018 +0200
     2.3 @@ -92,6 +92,8 @@
     2.4    -- "if true then some tools will OMIT some proofs"
     2.5  option skip_proofs : bool = false
     2.6    -- "skip over proofs (implicit 'sorry')"
     2.7 +option strict_facts : bool = false
     2.8 +  -- "force lazy facts when defined in context"
     2.9  
    2.10  
    2.11  section "Global Session Parameters"
     3.1 --- a/src/Pure/Isar/proof_context.ML	Wed Jul 18 20:51:23 2018 +0200
     3.2 +++ b/src/Pure/Isar/proof_context.ML	Fri Jul 20 03:14:44 2018 +0200
     3.3 @@ -1077,7 +1077,8 @@
     3.4  fun add_thms_lazy kind (b, ths) ctxt =
     3.5    let
     3.6      val name = full_name ctxt b;
     3.7 -    val ths' = ths
     3.8 +    val ths' =
     3.9 +      Global_Theory.check_thms_lazy ths
    3.10        |> Lazy.map_finished (Global_Theory.name_thms true false name #> map (Thm.kind_rule kind));
    3.11      val (_, ctxt') = add_facts {index = is_stmt ctxt} (b, ths') ctxt;
    3.12    in ctxt' end;
     4.1 --- a/src/Pure/global_theory.ML	Wed Jul 18 20:51:23 2018 +0200
     4.2 +++ b/src/Pure/global_theory.ML	Fri Jul 20 03:14:44 2018 +0200
     4.3 @@ -24,6 +24,7 @@
     4.4    val name_thm: bool -> bool -> string -> thm -> thm
     4.5    val name_thms: bool -> bool -> string -> thm list -> thm list
     4.6    val name_thmss: bool -> string -> (thm list * 'a) list -> (thm list * 'a) list
     4.7 +  val check_thms_lazy: thm list lazy -> thm list lazy
     4.8    val add_thms_lazy: string -> (binding * thm list lazy) -> theory -> theory
     4.9    val store_thm: binding * thm -> theory -> thm * theory
    4.10    val store_thm_open: binding * thm -> theory -> thm * theory
    4.11 @@ -156,12 +157,16 @@
    4.12      thy |> Data.map (Facts.add_static (Context.Theory thy) {strict = true, index = false} arg #> #2)
    4.13    end;
    4.14  
    4.15 +fun check_thms_lazy (thms: thm list lazy) =
    4.16 +  if Options.default_bool "strict_facts" then (Lazy.force thms; thms) else thms;
    4.17 +
    4.18  fun add_thms_lazy kind (b, thms) thy =
    4.19 -  if Binding.is_empty b then Thm.register_proofs thms thy
    4.20 +  if Binding.is_empty b then Thm.register_proofs (check_thms_lazy thms) thy
    4.21    else
    4.22      let
    4.23        val name = Sign.full_name thy b;
    4.24 -      val thms' = thms
    4.25 +      val thms' =
    4.26 +        check_thms_lazy thms
    4.27          |> Lazy.map_finished (name_thms true true name #> map (Thm.kind_rule kind));
    4.28      in thy |> Thm.register_proofs thms' |> add_facts (b, thms') end;
    4.29