faster compilation of ML with antiquotations: static ML_context is bound once in auxiliary structure Isabelle;
authorwenzelm
Sat Aug 11 22:17:46 2012 +0200 (2012-08-11)
changeset 4877637cd53e69840
parent 48775 92ceb058391f
child 48777 da0411d633ad
faster compilation of ML with antiquotations: static ML_context is bound once in auxiliary structure Isabelle;
src/FOL/FOL.thy
src/HOL/HOL.thy
src/Pure/Isar/isar_cmd.ML
src/Pure/ML/ml_antiquote.ML
src/Pure/ML/ml_context.ML
src/Pure/ML/ml_thms.ML
src/Pure/simplifier.ML
     1.1 --- a/src/FOL/FOL.thy	Sat Aug 11 21:32:46 2012 +0200
     1.2 +++ b/src/FOL/FOL.thy	Sat Aug 11 22:17:46 2012 +0200
     1.3 @@ -184,7 +184,7 @@
     1.4  
     1.5  setup {*
     1.6    ML_Antiquote.value @{binding claset}
     1.7 -    (Scan.succeed "Cla.claset_of (ML_Context.the_local_context ())")
     1.8 +    (Scan.succeed "Cla.claset_of ML_context")
     1.9  *}
    1.10  
    1.11  setup Cla.setup
     2.1 --- a/src/HOL/HOL.thy	Sat Aug 11 21:32:46 2012 +0200
     2.2 +++ b/src/HOL/HOL.thy	Sat Aug 11 22:17:46 2012 +0200
     2.3 @@ -847,7 +847,7 @@
     2.4  
     2.5  setup {*
     2.6    ML_Antiquote.value @{binding claset}
     2.7 -    (Scan.succeed "Classical.claset_of (ML_Context.the_local_context ())")
     2.8 +    (Scan.succeed "Classical.claset_of ML_context")
     2.9  *}
    2.10  
    2.11  setup Classical.setup
     3.1 --- a/src/Pure/Isar/isar_cmd.ML	Sat Aug 11 21:32:46 2012 +0200
     3.2 +++ b/src/Pure/Isar/isar_cmd.ML	Sat Aug 11 22:17:46 2012 +0200
     3.3 @@ -38,8 +38,8 @@
     3.4    val done_proof: Toplevel.transition -> Toplevel.transition
     3.5    val skip_proof: Toplevel.transition -> Toplevel.transition
     3.6    val ml_diag: bool -> Symbol_Pos.text * Position.T -> Toplevel.transition -> Toplevel.transition
     3.7 -  val diag_state: unit -> Toplevel.state
     3.8 -  val diag_goal: unit -> {context: Proof.context, facts: thm list, goal: thm}
     3.9 +  val diag_state: Proof.context -> Toplevel.state
    3.10 +  val diag_goal: Proof.context -> {context: Proof.context, facts: thm list, goal: thm}
    3.11    val display_drafts: Path.T list -> Toplevel.transition -> Toplevel.transition
    3.12    val print_drafts: Path.T list -> Toplevel.transition -> Toplevel.transition
    3.13    val print_context: Toplevel.transition -> Toplevel.transition
    3.14 @@ -297,18 +297,18 @@
    3.15      |> Option.map (Context.proof_of #> Diag_State.put state)
    3.16    in ML_Context.eval_text_in opt_ctxt verbose pos txt end);
    3.17  
    3.18 -fun diag_state () = Diag_State.get (ML_Context.the_local_context ());
    3.19 +val diag_state = Diag_State.get;
    3.20  
    3.21 -fun diag_goal () =
    3.22 -  Proof.goal (Toplevel.proof_of (diag_state ()))
    3.23 +fun diag_goal ctxt =
    3.24 +  Proof.goal (Toplevel.proof_of (diag_state ctxt))
    3.25      handle Toplevel.UNDEF => error "No goal present";
    3.26  
    3.27  val _ =
    3.28    Context.>> (Context.map_theory
    3.29     (ML_Antiquote.value (Binding.qualify true "Isar" (Binding.name "state"))
    3.30 -      (Scan.succeed "Isar_Cmd.diag_state ()") #>
    3.31 +      (Scan.succeed "Isar_Cmd.diag_state ML_context") #>
    3.32      ML_Antiquote.value (Binding.qualify true "Isar" (Binding.name "goal"))
    3.33 -      (Scan.succeed "Isar_Cmd.diag_goal ()")));
    3.34 +      (Scan.succeed "Isar_Cmd.diag_goal ML_context")));
    3.35  
    3.36  
    3.37  (* present draft files *)
     4.1 --- a/src/Pure/ML/ml_antiquote.ML	Sat Aug 11 21:32:46 2012 +0200
     4.2 +++ b/src/Pure/ML/ml_antiquote.ML	Sat Aug 11 22:17:46 2012 +0200
     4.3 @@ -20,10 +20,12 @@
     4.4  
     4.5  (* ML names *)
     4.6  
     4.7 +val init_context = ML_Syntax.reserved |> Name.declare "ML_context";
     4.8 +
     4.9  structure Names = Proof_Data
    4.10  (
    4.11    type T = Name.context;
    4.12 -  fun init _ = ML_Syntax.reserved;
    4.13 +  fun init _ = init_context;
    4.14  );
    4.15  
    4.16  fun variant a ctxt =
    4.17 @@ -73,7 +75,7 @@
    4.18        "Context.get_theory (ML_Context.the_global_context ()) " ^ ML_Syntax.print_string name)
    4.19      || Scan.succeed "ML_Context.the_global_context ()") #>
    4.20  
    4.21 -  value (Binding.name "context") (Scan.succeed "ML_Context.the_local_context ()") #>
    4.22 +  value (Binding.name "context") (Scan.succeed "ML_context") #>
    4.23  
    4.24    inline (Binding.name "typ") (Args.typ >> (ML_Syntax.atomic o ML_Syntax.print_typ)) #>
    4.25    inline (Binding.name "term") (Args.term >> (ML_Syntax.atomic o ML_Syntax.print_term)) #>
     5.1 --- a/src/Pure/ML/ml_context.ML	Sat Aug 11 21:32:46 2012 +0200
     5.2 +++ b/src/Pure/ML/ml_context.ML	Sat Aug 11 22:17:46 2012 +0200
     5.3 @@ -130,7 +130,11 @@
     5.4    Parse.!!! (Parse.position Parse.xname -- Args.parse --| Scan.ahead Parse.eof)
     5.5    >> (fn ((x, pos), y) => Args.src ((x, y), pos));
     5.6  
     5.7 -val begin_env = ML_Lex.tokenize "structure Isabelle =\nstruct\n";
     5.8 +val begin_env0 = ML_Lex.tokenize "structure Isabelle =\nstruct\n";
     5.9 +val begin_env =
    5.10 +  ML_Lex.tokenize
    5.11 +    "structure Isabelle =\nstruct\nval ML_context = ML_Context.the_local_context ()\n";
    5.12 +
    5.13  val end_env = ML_Lex.tokenize "end;";
    5.14  val reset_env = ML_Lex.tokenize "structure Isabelle = struct end";
    5.15  
    5.16 @@ -141,7 +145,7 @@
    5.17      val opt_ctxt = Option.map (Context.Proof o Context.proof_of) opt_context;
    5.18      val ((ml_env, ml_body), opt_ctxt') =
    5.19        if forall Antiquote.is_text ants
    5.20 -      then (([], map (fn Antiquote.Text tok => tok) ants), opt_ctxt)
    5.21 +      then ((begin_env0, map (fn Antiquote.Text tok => tok) ants), opt_ctxt)
    5.22        else
    5.23          let
    5.24            val ctxt =
    5.25 @@ -167,9 +171,9 @@
    5.26                  (no_decl, (Stack.pop scope, background));
    5.27  
    5.28            val (decls, (_, ctxt')) = fold_map expand ants (Stack.init ctxt, ctxt);
    5.29 -          val ml = decls |> map (fn decl => decl ctxt') |> split_list |> pairself flat;
    5.30 -        in (ml, SOME (Context.Proof ctxt')) end;
    5.31 -  in ((begin_env @ ml_env @ end_env, ml_body), opt_ctxt') end;
    5.32 +          val (ml_env, ml_body) = decls |> map (fn decl => decl ctxt') |> split_list |> pairself flat;
    5.33 +        in ((begin_env @ ml_env, ml_body), SOME (Context.Proof ctxt')) end;
    5.34 +  in ((ml_env @ end_env, ml_body), opt_ctxt') end;
    5.35  
    5.36  val trace_raw = Config.declare "ML_trace" (fn _ => Config.Bool false);
    5.37  val trace = Config.bool trace_raw;
     6.1 --- a/src/Pure/ML/ml_thms.ML	Sat Aug 11 21:32:46 2012 +0200
     6.2 +++ b/src/Pure/ML/ml_thms.ML	Sat Aug 11 22:17:46 2012 +0200
     6.3 @@ -46,7 +46,7 @@
     6.4            val (a, background') = background
     6.5              |> ML_Antiquote.variant "attributes" ||> put_attributes (i, srcs);
     6.6            val ml =
     6.7 -            ("val " ^ a ^ " = ML_Thms.the_attributes (ML_Context.the_local_context ()) " ^
     6.8 +            ("val " ^ a ^ " = ML_Thms.the_attributes ML_context " ^
     6.9                string_of_int i ^ ";\n", "Isabelle." ^ a);
    6.10          in (K ml, background') end))));
    6.11  
    6.12 @@ -54,8 +54,7 @@
    6.13  (* fact references *)
    6.14  
    6.15  fun thm_bind kind a i =
    6.16 -  "val " ^ a ^ " = ML_Thms.the_" ^ kind ^
    6.17 -    " (ML_Context.the_local_context ()) " ^ string_of_int i ^ ";\n";
    6.18 +  "val " ^ a ^ " = ML_Thms.the_" ^ kind ^ " ML_context " ^ string_of_int i ^ ";\n";
    6.19  
    6.20  fun thm_antiq kind scan = ML_Context.add_antiq (Binding.name kind)
    6.21    (fn _ => scan >> (fn ths => fn background =>
     7.1 --- a/src/Pure/simplifier.ML	Sat Aug 11 21:32:46 2012 +0200
     7.2 +++ b/src/Pure/simplifier.ML	Sat Aug 11 22:17:46 2012 +0200
     7.3 @@ -154,7 +154,7 @@
     7.4  
     7.5  val _ = Context.>> (Context.map_theory
     7.6    (ML_Antiquote.value (Binding.name "simpset")
     7.7 -    (Scan.succeed "Simplifier.simpset_of (ML_Context.the_local_context ())")));
     7.8 +    (Scan.succeed "Simplifier.simpset_of ML_context")));
     7.9  
    7.10  
    7.11  (* global simpset *)
    7.12 @@ -180,7 +180,7 @@
    7.13     (ML_Antiquote.value (Binding.name "simproc")
    7.14        (Args.context -- Scan.lift (Parse.position Args.name)
    7.15          >> (fn (ctxt, name) =>
    7.16 -          "Simplifier.the_simproc (ML_Context.the_local_context ()) " ^
    7.17 +          "Simplifier.the_simproc ML_context " ^
    7.18              ML_Syntax.print_string (check_simproc ctxt name)))));
    7.19  
    7.20