clarified modules -- simplified bootstrap;
authorwenzelm
Tue Apr 05 20:03:24 2016 +0200 (2016-04-05)
changeset 62876507c90523113
parent 62875 5a0c06491974
child 62877 741560a5283b
clarified modules -- simplified bootstrap;
src/Doc/Implementation/ML.thy
src/HOL/Tools/Quickcheck/narrowing_generators.ML
src/Pure/Isar/outer_syntax.ML
src/Pure/ML/ml_context.ML
src/Pure/ML/ml_env.ML
src/Pure/ML/ml_thms.ML
src/Pure/Thy/thy_info.ML
src/Pure/Tools/debugger.ML
src/Pure/conjunction.ML
src/Pure/context.ML
src/Pure/drule.ML
src/Pure/pure_syn.ML
src/Pure/raw_simplifier.ML
src/Tools/Code/code_runtime.ML
src/Tools/Spec_Check/gen_construction.ML
src/Tools/Spec_Check/spec_check.ML
     1.1 --- a/src/Doc/Implementation/ML.thy	Tue Apr 05 19:41:58 2016 +0200
     1.2 +++ b/src/Doc/Implementation/ML.thy	Tue Apr 05 20:03:24 2016 +0200
     1.3 @@ -616,15 +616,15 @@
     1.4  
     1.5  text %mlref \<open>
     1.6    \begin{mldecls}
     1.7 -  @{index_ML ML_Context.the_generic_context: "unit -> Context.generic"} \\
     1.8 +  @{index_ML Context.the_generic_context: "unit -> Context.generic"} \\
     1.9    @{index_ML "Context.>>": "(Context.generic -> Context.generic) -> unit"} \\
    1.10    @{index_ML ML_Thms.bind_thms: "string * thm list -> unit"} \\
    1.11    @{index_ML ML_Thms.bind_thm: "string * thm -> unit"} \\
    1.12    \end{mldecls}
    1.13  
    1.14 -    \<^descr> @{ML "ML_Context.the_generic_context ()"} refers to the theory context of
    1.15 +    \<^descr> @{ML "Context.the_generic_context ()"} refers to the theory context of
    1.16      the ML toplevel --- at compile time. ML code needs to take care to refer to
    1.17 -    @{ML "ML_Context.the_generic_context ()"} correctly. Recall that evaluation
    1.18 +    @{ML "Context.the_generic_context ()"} correctly. Recall that evaluation
    1.19      of a function body is delayed until actual run-time.
    1.20  
    1.21      \<^descr> @{ML "Context.>>"}~\<open>f\<close> applies context transformation \<open>f\<close> to the implicit
     2.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Tue Apr 05 19:41:58 2016 +0200
     2.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Tue Apr 05 20:03:24 2016 +0200
     2.3 @@ -280,7 +280,7 @@
     2.4                    val output_value = the_default "NONE"
     2.5                      (try (snd o split_last o filter_out (fn s => s = "") o split_lines) response)
     2.6                    val ml_code = "\nval _ = Context.set_thread_data (SOME (Context.map_proof (" ^ put_ml
     2.7 -                    ^ " (fn () => " ^ output_value ^ ")) (ML_Context.the_generic_context ())))";
     2.8 +                    ^ " (fn () => " ^ output_value ^ ")) (Context.the_generic_context ())))";
     2.9                    val ctxt' = ctxt
    2.10                      |> put (fn () => error ("Bad evaluation for " ^ quote put_ml))
    2.11                      |> Context.proof_map (exec false ml_code);
     3.1 --- a/src/Pure/Isar/outer_syntax.ML	Tue Apr 05 19:41:58 2016 +0200
     3.2 +++ b/src/Pure/Isar/outer_syntax.ML	Tue Apr 05 20:03:24 2016 +0200
     3.3 @@ -120,7 +120,7 @@
     3.4          NONE => ()
     3.5        | SOME cmd' => err_dup_command name [command_pos cmd, command_pos cmd']);
     3.6      val _ =
     3.7 -      Context_Position.report_generic (ML_Context.the_generic_context ())
     3.8 +      Context_Position.report_generic (Context.the_generic_context ())
     3.9          (command_pos cmd) (command_markup true (name, cmd));
    3.10    in Data.map (Symtab.update (name, cmd)) thy end;
    3.11  
     4.1 --- a/src/Pure/ML/ml_context.ML	Tue Apr 05 19:41:58 2016 +0200
     4.2 +++ b/src/Pure/ML/ml_context.ML	Tue Apr 05 20:03:24 2016 +0200
     4.3 @@ -6,9 +6,6 @@
     4.4  
     4.5  signature ML_CONTEXT =
     4.6  sig
     4.7 -  val the_generic_context: unit -> Context.generic
     4.8 -  val the_global_context: unit -> theory
     4.9 -  val the_local_context: unit -> Proof.context
    4.10    val thm: xstring -> thm
    4.11    val thms: xstring -> thm list
    4.12    val exec: (unit -> unit) -> Context.generic -> Context.generic
    4.13 @@ -35,12 +32,8 @@
    4.14  
    4.15  (** implicit ML context **)
    4.16  
    4.17 -val the_generic_context = Context.the_thread_data;
    4.18 -val the_global_context = Context.theory_of o the_generic_context;
    4.19 -val the_local_context = Context.proof_of o the_generic_context;
    4.20 -
    4.21 -fun thm name = Proof_Context.get_thm (the_local_context ()) name;
    4.22 -fun thms name = Proof_Context.get_thms (the_local_context ()) name;
    4.23 +fun thm name = Proof_Context.get_thm (Context.the_local_context ()) name;
    4.24 +fun thms name = Proof_Context.get_thms (Context.the_local_context ()) name;
    4.25  
    4.26  fun exec (e: unit -> unit) context =
    4.27    (case Context.setmp_thread_data (SOME context) (fn () => (e (); Context.thread_data ())) () of
    4.28 @@ -123,7 +116,7 @@
    4.29    (ML_Lex.tokenize
    4.30      ("structure " ^ name ^ " =\nstruct\n\
    4.31       \val ML_context = Context_Position.set_visible " ^ Bool.toString visible ^
    4.32 -     " (ML_Context.the_local_context ());\n\
    4.33 +     " (Context.the_local_context ());\n\
    4.34       \val ML_print_depth =\n\
    4.35       \  let val default = ML_Options.get_print_depth ()\n\
    4.36       \  in fn () => ML_Options.get_print_depth_default default end;\n"),
    4.37 @@ -233,7 +226,7 @@
    4.38      eval ML_Compiler.flags (#1 range)
    4.39       (ML_Lex.read "Context.set_thread_data (SOME (let val " @ ML_Lex.read_set_range range name @
    4.40        ML_Lex.read (": " ^ constraint ^ " =") @ ants @
    4.41 -      ML_Lex.read ("in " ^ body ^ " end (ML_Context.the_generic_context ())));")));
    4.42 +      ML_Lex.read ("in " ^ body ^ " end (Context.the_generic_context ())));")));
    4.43  
    4.44  end;
    4.45  
     5.1 --- a/src/Pure/ML/ml_env.ML	Tue Apr 05 19:41:58 2016 +0200
     5.2 +++ b/src/Pure/ML/ml_env.ML	Tue Apr 05 20:03:24 2016 +0200
     5.3 @@ -130,7 +130,7 @@
     5.4    let
     5.5      fun lookup sel1 sel2 name =
     5.6        if SML then
     5.7 -        Context.the_thread_data ()
     5.8 +        Context.the_generic_context ()
     5.9          |> (fn context => Symtab.lookup (sel1 (#sml_tables (Env.get context))) name)
    5.10        else
    5.11          Context.thread_data ()
    5.12 @@ -139,7 +139,7 @@
    5.13  
    5.14      fun all sel1 sel2 () =
    5.15        (if SML then
    5.16 -        Context.the_thread_data ()
    5.17 +        Context.the_generic_context ()
    5.18          |> (fn context => Symtab.dest (sel1 (#sml_tables (Env.get context))))
    5.19        else
    5.20          Context.thread_data ()
     6.1 --- a/src/Pure/ML/ml_thms.ML	Tue Apr 05 19:41:58 2016 +0200
     6.2 +++ b/src/Pure/ML/ml_thms.ML	Tue Apr 05 20:03:24 2016 +0200
     6.3 @@ -113,7 +113,7 @@
     6.4    fun merge _ = [];
     6.5  );
     6.6  
     6.7 -fun get_stored_thms () = Stored_Thms.get (ML_Context.the_global_context ());
     6.8 +fun get_stored_thms () = Stored_Thms.get (Context.the_global_context ());
     6.9  val get_stored_thm = hd o get_stored_thms;
    6.10  
    6.11  fun ml_store get (name, ths) =
     7.1 --- a/src/Pure/Thy/thy_info.ML	Tue Apr 05 19:41:58 2016 +0200
     7.2 +++ b/src/Pure/Thy/thy_info.ML	Tue Apr 05 20:03:24 2016 +0200
     7.3 @@ -260,7 +260,7 @@
     7.4      val text_pos = Position.put_id (Document_ID.print exec_id) (Path.position thy_path);
     7.5      val (theory, present, weight) =
     7.6        Resources.load_thy document symbols last_timing update_time dir header text_pos text
     7.7 -        (if name = Context.PureN then [ML_Context.the_global_context ()] else parents);
     7.8 +        (if name = Context.PureN then [Context.the_global_context ()] else parents);
     7.9      fun commit () = update_thy deps theory;
    7.10    in
    7.11      Result {theory = theory, exec_id = exec_id, present = present, commit = commit, weight = weight}
     8.1 --- a/src/Pure/Tools/debugger.ML	Tue Apr 05 19:41:58 2016 +0200
     8.2 +++ b/src/Pure/Tools/debugger.ML	Tue Apr 05 20:03:24 2016 +0200
     8.3 @@ -155,7 +155,7 @@
     8.4  
     8.5  fun eval_context thread_name index SML toks =
     8.6    let
     8.7 -    val context = ML_Context.the_generic_context ();
     8.8 +    val context = Context.the_generic_context ();
     8.9      val context1 =
    8.10        if SML orelse forall (fn Antiquote.Text tok => ML_Lex.is_improper tok | _ => false) toks
    8.11        then context
     9.1 --- a/src/Pure/conjunction.ML	Tue Apr 05 19:41:58 2016 +0200
     9.2 +++ b/src/Pure/conjunction.ML	Tue Apr 05 20:03:24 2016 +0200
     9.3 @@ -30,7 +30,7 @@
     9.4  
     9.5  (** abstract syntax **)
     9.6  
     9.7 -fun certify t = Thm.global_cterm_of (Context.the_theory (Context.the_thread_data ())) t;
     9.8 +fun certify t = Thm.global_cterm_of (Context.the_global_context ()) t;
     9.9  val read_prop = certify o Simple_Syntax.read_prop;
    9.10  
    9.11  val true_prop = certify Logic.true_prop;
    9.12 @@ -76,7 +76,7 @@
    9.13  val A_B = read_prop "A &&& B";
    9.14  
    9.15  val conjunction_def =
    9.16 -  Thm.unvarify_axiom (Context.the_theory (Context.the_thread_data ())) "Pure.conjunction_def";
    9.17 +  Thm.unvarify_axiom (Context.the_global_context ()) "Pure.conjunction_def";
    9.18  
    9.19  fun conjunctionD which =
    9.20    Drule.implies_intr_list [A, B] (Thm.assume (which (A, B))) COMP
    9.21 @@ -137,7 +137,7 @@
    9.22  
    9.23  local
    9.24  
    9.25 -val bootstrap_thy = Context.theory_of (Context.the_thread_data ());
    9.26 +val bootstrap_thy = Context.the_global_context ();
    9.27  
    9.28  fun conjs n =
    9.29    let
    10.1 --- a/src/Pure/context.ML	Tue Apr 05 19:41:58 2016 +0200
    10.2 +++ b/src/Pure/context.ML	Tue Apr 05 20:03:24 2016 +0200
    10.3 @@ -74,9 +74,11 @@
    10.4    val proof_of: generic -> Proof.context  (*total*)
    10.5    (*thread data*)
    10.6    val thread_data: unit -> generic option
    10.7 -  val the_thread_data: unit -> generic
    10.8    val set_thread_data: generic option -> unit
    10.9    val setmp_thread_data: generic option -> ('a -> 'b) -> 'a -> 'b
   10.10 +  val the_generic_context: unit -> generic
   10.11 +  val the_global_context: unit -> theory
   10.12 +  val the_local_context: unit -> Proof.context
   10.13    val >> : (generic -> generic) -> unit
   10.14    val >>> : (generic -> 'a * generic) -> 'a
   10.15  end;
   10.16 @@ -496,19 +498,22 @@
   10.17      SOME (SOME context) => SOME context
   10.18    | _ => NONE);
   10.19  
   10.20 -fun the_thread_data () =
   10.21 +fun set_thread_data context = Thread.setLocal (tag, context);
   10.22 +fun setmp_thread_data context = Library.setmp_thread_data tag (thread_data ()) context;
   10.23 +
   10.24 +fun the_generic_context () =
   10.25    (case thread_data () of
   10.26      SOME context => context
   10.27    | _ => error "Unknown context");
   10.28  
   10.29 -fun set_thread_data context = Thread.setLocal (tag, context);
   10.30 -fun setmp_thread_data context = Library.setmp_thread_data tag (thread_data ()) context;
   10.31 +val the_global_context = theory_of o the_generic_context;
   10.32 +val the_local_context = proof_of o the_generic_context;
   10.33  
   10.34  end;
   10.35  
   10.36  fun >>> f =
   10.37    let
   10.38 -    val (res, context') = f (the_thread_data ());
   10.39 +    val (res, context') = f (the_generic_context ());
   10.40      val _ = set_thread_data (SOME context');
   10.41    in res end;
   10.42  
    11.1 --- a/src/Pure/drule.ML	Tue Apr 05 19:41:58 2016 +0200
    11.2 +++ b/src/Pure/drule.ML	Tue Apr 05 20:03:24 2016 +0200
    11.3 @@ -134,7 +134,7 @@
    11.4  (*The premises of a theorem, as a cterm list*)
    11.5  val cprems_of = strip_imp_prems o Thm.cprop_of;
    11.6  
    11.7 -fun certify t = Thm.global_cterm_of (Context.the_theory (Context.the_thread_data ())) t;
    11.8 +fun certify t = Thm.global_cterm_of (Context.the_global_context ()) t;
    11.9  
   11.10  val implies = certify Logic.implies;
   11.11  fun mk_implies (A, B) = Thm.apply (Thm.apply implies A) B;
   11.12 @@ -570,7 +570,7 @@
   11.13  
   11.14  local
   11.15    val A = certify (Free ("A", propT));
   11.16 -  val axiom = Thm.unvarify_axiom (Context.the_theory (Context.the_thread_data ()));
   11.17 +  val axiom = Thm.unvarify_axiom (Context.the_global_context ());
   11.18    val prop_def = axiom "Pure.prop_def";
   11.19    val term_def = axiom "Pure.term_def";
   11.20    val sort_constraint_def = axiom "Pure.sort_constraint_def";
   11.21 @@ -645,7 +645,7 @@
   11.22    store_standard_thm (Binding.concealed (Binding.make ("sort_constraint_eq", @{here})))
   11.23      (Thm.equal_intr
   11.24        (Thm.implies_intr CA (Thm.implies_elim (Thm.assume CA)
   11.25 -        (Thm.unvarify_global (Context.the_theory (Context.the_thread_data ())) sort_constraintI)))
   11.26 +        (Thm.unvarify_global (Context.the_global_context ()) sort_constraintI)))
   11.27        (implies_intr_list [A, C] (Thm.assume A)));
   11.28  
   11.29  end;
    12.1 --- a/src/Pure/pure_syn.ML	Tue Apr 05 19:41:58 2016 +0200
    12.2 +++ b/src/Pure/pure_syn.ML	Tue Apr 05 20:03:24 2016 +0200
    12.3 @@ -55,7 +55,7 @@
    12.4        (fn _ => Toplevel.init_theory (fn () => error "Missing theory initialization")));
    12.5  
    12.6  
    12.7 -val bootstrap_thy = ML_Context.the_global_context ();
    12.8 +val bootstrap_thy = Context.the_global_context ();
    12.9  
   12.10  val _ = Theory.setup (Config.put_global Outer_Syntax.bootstrap false);
   12.11  
    13.1 --- a/src/Pure/raw_simplifier.ML	Tue Apr 05 19:41:58 2016 +0200
    13.2 +++ b/src/Pure/raw_simplifier.ML	Tue Apr 05 20:03:24 2016 +0200
    13.3 @@ -1392,11 +1392,10 @@
    13.4    Variable.gen_all ctxt;
    13.5  
    13.6  val hhf_ss =
    13.7 -  simpset_of (empty_simpset (Context.proof_of (Context.the_thread_data ()))
    13.8 -    addsimps Drule.norm_hhf_eqs);
    13.9 +  simpset_of (empty_simpset (Context.the_local_context ()) addsimps Drule.norm_hhf_eqs);
   13.10  
   13.11  val hhf_protect_ss =
   13.12 -  simpset_of (empty_simpset (Context.proof_of (Context.the_thread_data ()))
   13.13 +  simpset_of (empty_simpset (Context.the_local_context ())
   13.14      addsimps Drule.norm_hhf_eqs |> add_eqcong Drule.protect_cong);
   13.15  
   13.16  in
    14.1 --- a/src/Tools/Code/code_runtime.ML	Tue Apr 05 19:41:58 2016 +0200
    14.2 +++ b/src/Tools/Code/code_runtime.ML	Tue Apr 05 20:03:24 2016 +0200
    14.3 @@ -88,7 +88,7 @@
    14.4    let
    14.5      val code = (prelude
    14.6        ^ "\nval _ = Context.set_thread_data (SOME (Context.map_proof (" ^ put_ml
    14.7 -      ^ " (fn () => " ^ value ^ ")) (ML_Context.the_generic_context ())))");
    14.8 +      ^ " (fn () => " ^ value ^ ")) (Context.the_generic_context ())))");
    14.9      val ctxt' = ctxt
   14.10        |> put (fn () => error ("Bad evaluation for " ^ quote put_ml))
   14.11        |> Context.proof_map (exec ctxt false code);
   14.12 @@ -539,7 +539,7 @@
   14.13        ML_Compiler0.use_text notifying_context
   14.14          {line = 0, file = Path.implode filepath, verbose = false, debug = false}
   14.15          (File.read filepath);
   14.16 -    val thy'' = Context.the_theory (Context.the_thread_data ());
   14.17 +    val thy'' = Context.the_global_context ();
   14.18      val names = Loaded_Values.get thy'';
   14.19    in (names, thy'') end;
   14.20  
    15.1 --- a/src/Tools/Spec_Check/gen_construction.ML	Tue Apr 05 19:41:58 2016 +0200
    15.2 +++ b/src/Tools/Spec_Check/gen_construction.ML	Tue Apr 05 20:03:24 2016 +0200
    15.3 @@ -155,7 +155,7 @@
    15.4  
    15.5  (*produce compilable string*)
    15.6  fun build_check ctxt name (ty, spec) =
    15.7 -  "Spec_Check.checkGen (ML_Context.the_local_context ()) ("
    15.8 +  "Spec_Check.checkGen (Context.the_local_context ()) ("
    15.9    ^ compose_generator ctxt ty ^ ", SOME (" ^ compose_printer ctxt ty ^ ")) (\""
   15.10    ^ name ^ "\", Property.pred (" ^ spec ^ "));";
   15.11  
    16.1 --- a/src/Tools/Spec_Check/spec_check.ML	Tue Apr 05 19:41:58 2016 +0200
    16.2 +++ b/src/Tools/Spec_Check/spec_check.ML	Tue Apr 05 20:03:24 2016 +0200
    16.3 @@ -192,5 +192,5 @@
    16.4  
    16.5  end;
    16.6  
    16.7 -fun check_property s = Spec_Check.check_property (ML_Context.the_local_context ()) s;
    16.8 +fun check_property s = Spec_Check.check_property (Context.the_local_context ()) s;
    16.9