simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
authorwenzelm
Wed Mar 12 21:58:48 2014 +0100 (2014-03-12)
changeset 56069451d5b73f8cf
parent 56068 f74d0a4d8ae3
child 56070 1bc0bea908c3
simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
added command 'print_ML_antiquotations';
NEWS
etc/isar-keywords-ZF.el
etc/isar-keywords.el
src/Pure/Isar/isar_syn.ML
src/Pure/ML/ml_antiquote.ML
src/Pure/ML/ml_context.ML
src/Pure/ML/ml_thms.ML
src/Pure/Pure.thy
src/Pure/Thy/thy_output.ML
src/Tools/Code/code_runtime.ML
     1.1 --- a/NEWS	Wed Mar 12 21:29:46 2014 +0100
     1.2 +++ b/NEWS	Wed Mar 12 21:58:48 2014 +0100
     1.3 @@ -437,6 +437,10 @@
     1.4  theory merge).  Note that the softer Thm.eq_thm_prop is often more
     1.5  appropriate than Thm.eq_thm.
     1.6  
     1.7 +* Simplified programming interface to define ML antiquotations, see
     1.8 +ML_Context.antiquotation, to make it more close to the analogous
     1.9 +Thy_Output.antiquotation.  Minor INCOMPATIBILTY.
    1.10 +
    1.11  
    1.12  *** System ***
    1.13  
     2.1 --- a/etc/isar-keywords-ZF.el	Wed Mar 12 21:29:46 2014 +0100
     2.2 +++ b/etc/isar-keywords-ZF.el	Wed Mar 12 21:58:48 2014 +0100
     2.3 @@ -116,6 +116,7 @@
     2.4      "pretty_setmargin"
     2.5      "prf"
     2.6      "primrec"
     2.7 +    "print_ML_antiquotations"
     2.8      "print_abbrevs"
     2.9      "print_antiquotations"
    2.10      "print_ast_translation"
    2.11 @@ -285,6 +286,7 @@
    2.12      "locale_deps"
    2.13      "pr"
    2.14      "prf"
    2.15 +    "print_ML_antiquotations"
    2.16      "print_abbrevs"
    2.17      "print_antiquotations"
    2.18      "print_attributes"
     3.1 --- a/etc/isar-keywords.el	Wed Mar 12 21:29:46 2014 +0100
     3.2 +++ b/etc/isar-keywords.el	Wed Mar 12 21:58:48 2014 +0100
     3.3 @@ -170,6 +170,7 @@
     3.4      "primcorec"
     3.5      "primcorecursive"
     3.6      "primrec"
     3.7 +    "print_ML_antiquotations"
     3.8      "print_abbrevs"
     3.9      "print_antiquotations"
    3.10      "print_ast_translation"
    3.11 @@ -400,6 +401,7 @@
    3.12      "nitpick"
    3.13      "pr"
    3.14      "prf"
    3.15 +    "print_ML_antiquotations"
    3.16      "print_abbrevs"
    3.17      "print_antiquotations"
    3.18      "print_attributes"
     4.1 --- a/src/Pure/Isar/isar_syn.ML	Wed Mar 12 21:29:46 2014 +0100
     4.2 +++ b/src/Pure/Isar/isar_syn.ML	Wed Mar 12 21:58:48 2014 +0100
     4.3 @@ -842,11 +842,18 @@
     4.4        Toplevel.keep (Method.print_methods o Toplevel.context_of)));
     4.5  
     4.6  val _ =
     4.7 -  Outer_Syntax.improper_command @{command_spec "print_antiquotations"} "print antiquotations"
     4.8 +  Outer_Syntax.improper_command @{command_spec "print_antiquotations"}
     4.9 +    "print document antiquotations"
    4.10      (Scan.succeed (Toplevel.unknown_context o
    4.11        Toplevel.keep (Thy_Output.print_antiquotations o Toplevel.context_of)));
    4.12  
    4.13  val _ =
    4.14 +  Outer_Syntax.improper_command @{command_spec "print_ML_antiquotations"}
    4.15 +    "print ML antiquotations"
    4.16 +    (Scan.succeed (Toplevel.unknown_context o
    4.17 +      Toplevel.keep (ML_Context.print_antiquotations o Toplevel.context_of)));
    4.18 +
    4.19 +val _ =
    4.20    Outer_Syntax.improper_command @{command_spec "thy_deps"} "visualize theory dependencies"
    4.21      (Scan.succeed Isar_Cmd.thy_deps);
    4.22  
     5.1 --- a/src/Pure/ML/ml_antiquote.ML	Wed Mar 12 21:29:46 2014 +0100
     5.2 +++ b/src/Pure/ML/ml_antiquote.ML	Wed Mar 12 21:58:48 2014 +0100
     5.3 @@ -37,18 +37,15 @@
     5.4  (* specific antiquotations *)
     5.5  
     5.6  fun inline name scan =
     5.7 -  ML_Context.add_antiq name
     5.8 -    (Scan.depend (fn context => Scan.pass context scan >> (fn s => (context, K ("", s)))));
     5.9 +  ML_Context.antiquotation name scan (fn _ => fn s => fn ctxt => (K ("", s), ctxt));
    5.10  
    5.11  fun value name scan =
    5.12 -  ML_Context.add_antiq name
    5.13 -    (Scan.depend (fn context => Scan.pass context scan >> (fn s =>
    5.14 -      let
    5.15 -        val ctxt = Context.the_proof context;
    5.16 -        val (a, ctxt') = variant (Binding.name_of name) ctxt;
    5.17 -        val env = "val " ^ a ^ " = " ^ s ^ ";\n";
    5.18 -        val body = "Isabelle." ^ a;
    5.19 -      in (Context.Proof ctxt', (K (env, body))) end)));
    5.20 +  ML_Context.antiquotation name scan (fn _ => fn s => fn ctxt =>
    5.21 +    let
    5.22 +      val (a, ctxt') = variant (Binding.name_of name) ctxt;
    5.23 +      val env = "val " ^ a ^ " = " ^ s ^ ";\n";
    5.24 +      val body = "Isabelle." ^ a;
    5.25 +    in (K (env, body), ctxt') end);
    5.26  
    5.27  
    5.28  
     6.1 --- a/src/Pure/ML/ml_context.ML	Wed Mar 12 21:29:46 2014 +0100
     6.2 +++ b/src/Pure/ML/ml_context.ML	Wed Mar 12 21:58:48 2014 +0100
     6.3 @@ -23,9 +23,10 @@
     6.4    val get_stored_thm: unit -> thm
     6.5    val ml_store_thms: string * thm list -> unit
     6.6    val ml_store_thm: string * thm -> unit
     6.7 -  type antiq = Proof.context -> string * string
     6.8 -  val add_antiq: binding -> antiq context_parser -> theory -> theory
     6.9 -  val check_antiq: Proof.context -> xstring * Position.T -> string
    6.10 +  val print_antiquotations: Proof.context -> unit
    6.11 +  type decl = Proof.context -> string * string
    6.12 +  val antiquotation: binding -> 'a context_parser ->
    6.13 +    (Args.src -> 'a -> Proof.context -> decl * Proof.context) -> theory -> theory
    6.14    val trace_raw: Config.raw
    6.15    val trace: bool Config.T
    6.16    val eval_antiquotes: ML_Lex.token Antiquote.antiquote list * Position.T ->
    6.17 @@ -95,28 +96,36 @@
    6.18  
    6.19  (** ML antiquotations **)
    6.20  
    6.21 -(* antiquotation commands *)
    6.22 -
    6.23 -type antiq = Proof.context -> string * string;
    6.24 +(* theory data *)
    6.25  
    6.26 -structure Antiq_Parsers = Theory_Data
    6.27 +type decl = Proof.context -> string * string;  (*final context -> ML env, ML body*)
    6.28 +structure Antiquotations = Theory_Data
    6.29  (
    6.30 -  type T = antiq context_parser Name_Space.table;
    6.31 +  type T = (Args.src -> Proof.context -> decl * Proof.context) Name_Space.table;
    6.32    val empty : T = Name_Space.empty_table Markup.ML_antiquotationN;
    6.33    val extend = I;
    6.34    fun merge data : T = Name_Space.merge_tables data;
    6.35  );
    6.36  
    6.37 -val get_antiqs = Antiq_Parsers.get o Proof_Context.theory_of;
    6.38 +val get_antiquotations = Antiquotations.get o Proof_Context.theory_of;
    6.39 +
    6.40 +fun add_antiquotation name f thy = thy
    6.41 +  |> Antiquotations.map (Name_Space.define (Context.Theory thy) true (name, f) #> snd);
    6.42  
    6.43 -fun add_antiq name scan thy = thy
    6.44 -  |> Antiq_Parsers.map (Name_Space.define (Context.Theory thy) true (name, scan) #> snd);
    6.45 +fun print_antiquotations ctxt =
    6.46 +  Pretty.big_list "ML antiquotations:"
    6.47 +    (map (Pretty.mark_str o #1) (Name_Space.markup_table ctxt (get_antiquotations ctxt)))
    6.48 +  |> Pretty.writeln;
    6.49  
    6.50 -fun check_antiq ctxt = #1 o Name_Space.check (Context.Proof ctxt) (get_antiqs ctxt);
    6.51 +fun apply_antiquotation src ctxt =
    6.52 +  let val (src', f) = Args.check_src ctxt (get_antiquotations ctxt) src
    6.53 +  in f src' ctxt end;
    6.54  
    6.55 -fun antiquotation src ctxt =
    6.56 -  let val (src', scan) = Args.check_src ctxt (get_antiqs ctxt) src
    6.57 -  in Args.syntax scan src' ctxt end;
    6.58 +fun antiquotation name scan body =
    6.59 +  add_antiquotation name
    6.60 +    (fn src => fn orig_ctxt =>
    6.61 +      let val (x, _) = Args.syntax scan src orig_ctxt
    6.62 +      in body src x orig_ctxt end);
    6.63  
    6.64  
    6.65  (* parsing and evaluation *)
    6.66 @@ -159,7 +168,8 @@
    6.67            fun expand (Antiquote.Text tok) ctxt = (K ([], [tok]), ctxt)
    6.68              | expand (Antiquote.Antiq (ss, {range, ...})) ctxt =
    6.69                  let
    6.70 -                  val (decl, ctxt') = antiquotation (Token.read_antiq lex antiq (ss, #1 range)) ctxt;
    6.71 +                  val (decl, ctxt') =
    6.72 +                    apply_antiquotation (Token.read_antiq lex antiq (ss, #1 range)) ctxt;
    6.73                    val decl' = decl #> pairself (ML_Lex.tokenize #> map (ML_Lex.set_range range));
    6.74                  in (decl', ctxt') end;
    6.75  
    6.76 @@ -210,10 +220,12 @@
    6.77    eval verbose (#pos source) (ML_Lex.read_source source);
    6.78  
    6.79  fun eval_in ctxt verbose pos ants =
    6.80 -  Context.setmp_thread_data (Option.map Context.Proof ctxt) (fn () => eval verbose pos ants) ();
    6.81 +  Context.setmp_thread_data (Option.map Context.Proof ctxt)
    6.82 +    (fn () => eval verbose pos ants) ();
    6.83  
    6.84  fun eval_source_in ctxt verbose source =
    6.85 -  Context.setmp_thread_data (Option.map Context.Proof ctxt) (fn () => eval_source verbose source) ();
    6.86 +  Context.setmp_thread_data (Option.map Context.Proof ctxt)
    6.87 +    (fn () => eval_source verbose source) ();
    6.88  
    6.89  fun expression pos bind body ants =
    6.90    exec (fn () => eval false pos
     7.1 --- a/src/Pure/ML/ml_thms.ML	Wed Mar 12 21:29:46 2014 +0100
     7.2 +++ b/src/Pure/ML/ml_thms.ML	Wed Mar 12 21:58:48 2014 +0100
     7.3 @@ -35,11 +35,9 @@
     7.4  (* attribute source *)
     7.5  
     7.6  val _ = Theory.setup
     7.7 -  (ML_Context.add_antiq @{binding attributes}
     7.8 -    (Scan.depend (fn context => Parse_Spec.attribs >> (fn raw_srcs =>
     7.9 +  (ML_Context.antiquotation @{binding attributes} (Scan.lift Parse_Spec.attribs)
    7.10 +    (fn _ => fn raw_srcs => fn ctxt =>
    7.11        let
    7.12 -        val ctxt = Context.the_proof context;
    7.13 -
    7.14          val i = serial ();
    7.15          val srcs = map (Attrib.check_src ctxt) raw_srcs;
    7.16          val _ = map (Attrib.attribute ctxt) srcs;
    7.17 @@ -48,15 +46,13 @@
    7.18          val ml =
    7.19            ("val " ^ a ^ " = ML_Thms.the_attributes ML_context " ^
    7.20              string_of_int i ^ ";\n", "Isabelle." ^ a);
    7.21 -      in (Context.Proof ctxt', K ml) end))));
    7.22 +      in (K ml, ctxt') end));
    7.23  
    7.24  
    7.25  (* fact references *)
    7.26  
    7.27 -fun thm_binding kind is_single context thms =
    7.28 +fun thm_binding kind is_single thms ctxt =
    7.29    let
    7.30 -    val ctxt = Context.the_proof context;
    7.31 -
    7.32      val initial = null (get_thmss ctxt);
    7.33      val (name, ctxt') = ML_Antiquote.variant kind ctxt;
    7.34      val ctxt'' = cons_thms ((name, is_single), thms) ctxt';
    7.35 @@ -69,15 +65,11 @@
    7.36            val ml_env = "val [" ^ commas binds ^ "] = ML_Thms.the_thmss ML_context;\n";
    7.37          in (ml_env, ml_body) end
    7.38        else ("", ml_body);
    7.39 -  in (Context.Proof ctxt'', decl) end;
    7.40 +  in (decl, ctxt'') end;
    7.41  
    7.42  val _ = Theory.setup
    7.43 -  (ML_Context.add_antiq @{binding thm}
    7.44 -    (Scan.depend (fn context =>
    7.45 -      Scan.pass context Attrib.thm >> (thm_binding "thm" true context o single))) #>
    7.46 -   ML_Context.add_antiq @{binding thms}
    7.47 -    (Scan.depend (fn context =>
    7.48 -      Scan.pass context Attrib.thms >> thm_binding "thms" false context)));
    7.49 +  (ML_Context.antiquotation @{binding thm} (Attrib.thm >> single) (K (thm_binding "thm" true)) #>
    7.50 +   ML_Context.antiquotation @{binding thms} Attrib.thms (K (thm_binding "thms" false)));
    7.51  
    7.52  
    7.53  (* ad-hoc goals *)
    7.54 @@ -87,29 +79,26 @@
    7.55  val goal = Scan.unless (by || and_) Args.name_inner_syntax;
    7.56  
    7.57  val _ = Theory.setup
    7.58 -  (ML_Context.add_antiq @{binding lemma}
    7.59 -    (Scan.depend (fn context =>
    7.60 -      Args.mode "open" -- Parse.enum1 "and" (Scan.repeat1 goal) --
    7.61 -      (by |-- Method.parse -- Scan.option Method.parse)
    7.62 -     >> (fn ((is_open, raw_propss), (m1, m2)) =>
    7.63 -          let
    7.64 -            val ctxt = Context.proof_of context;
    7.65 -
    7.66 -            val _ = Context_Position.reports ctxt (maps Method.reports_of (m1 :: the_list m2));
    7.67 +  (ML_Context.antiquotation @{binding lemma}
    7.68 +    (Scan.lift (Args.mode "open" -- Parse.enum1 "and" (Scan.repeat1 goal) --
    7.69 +      (by |-- Method.parse -- Scan.option Method.parse)))
    7.70 +    (fn _ => fn ((is_open, raw_propss), (m1, m2)) => fn ctxt =>
    7.71 +      let
    7.72 +        val _ = Context_Position.reports ctxt (maps Method.reports_of (m1 :: the_list m2));
    7.73  
    7.74 -            val propss = burrow (map (rpair []) o Syntax.read_props ctxt) raw_propss;
    7.75 -            val prep_result = Goal.norm_result ctxt #> not is_open ? Thm.close_derivation;
    7.76 -            fun after_qed res goal_ctxt =
    7.77 -              Proof_Context.put_thms false (Auto_Bind.thisN,
    7.78 -                SOME (map prep_result (Proof_Context.export goal_ctxt ctxt (flat res)))) goal_ctxt;
    7.79 +        val propss = burrow (map (rpair []) o Syntax.read_props ctxt) raw_propss;
    7.80 +        val prep_result = Goal.norm_result ctxt #> not is_open ? Thm.close_derivation;
    7.81 +        fun after_qed res goal_ctxt =
    7.82 +          Proof_Context.put_thms false (Auto_Bind.thisN,
    7.83 +            SOME (map prep_result (Proof_Context.export goal_ctxt ctxt (flat res)))) goal_ctxt;
    7.84  
    7.85 -            val ctxt' = ctxt
    7.86 -              |> Proof.theorem NONE after_qed propss
    7.87 -              |> Proof.global_terminal_proof (m1, m2);
    7.88 -            val thms =
    7.89 -              Proof_Context.get_fact ctxt'
    7.90 -                (Facts.named (Proof_Context.full_name ctxt' (Binding.name Auto_Bind.thisN)));
    7.91 -          in thm_binding "lemma" (length (flat propss) = 1) context thms end))));
    7.92 +        val ctxt' = ctxt
    7.93 +          |> Proof.theorem NONE after_qed propss
    7.94 +          |> Proof.global_terminal_proof (m1, m2);
    7.95 +        val thms =
    7.96 +          Proof_Context.get_fact ctxt'
    7.97 +            (Facts.named (Proof_Context.full_name ctxt' (Binding.name Auto_Bind.thisN)));
    7.98 +      in thm_binding "lemma" (length (flat propss) = 1) thms ctxt end));
    7.99  
   7.100  end;
   7.101  
     8.1 --- a/src/Pure/Pure.thy	Wed Mar 12 21:29:46 2014 +0100
     8.2 +++ b/src/Pure/Pure.thy	Wed Mar 12 21:58:48 2014 +0100
     8.3 @@ -78,14 +78,15 @@
     8.4    and "finally" "ultimately" :: prf_chain % "proof"
     8.5    and "back" :: prf_script % "proof"
     8.6    and "Isabelle.command" :: control
     8.7 -  and "help" "print_commands" "print_options"
     8.8 -    "print_context" "print_theory" "print_syntax" "print_abbrevs" "print_defn_rules"
     8.9 +  and "help" "print_commands" "print_options" "print_context"
    8.10 +    "print_theory" "print_syntax" "print_abbrevs" "print_defn_rules"
    8.11      "print_theorems" "print_locales" "print_classes" "print_locale"
    8.12      "print_interps" "print_dependencies" "print_attributes"
    8.13      "print_simpset" "print_rules" "print_trans_rules" "print_methods"
    8.14 -    "print_antiquotations" "thy_deps" "locale_deps" "class_deps" "thm_deps"
    8.15 -    "print_binds" "print_facts" "print_cases" "print_statement" "thm"
    8.16 -    "prf" "full_prf" "prop" "term" "typ" "print_codesetup" "unused_thms"
    8.17 +    "print_antiquotations" "print_ML_antiquotations" "thy_deps"
    8.18 +    "locale_deps" "class_deps" "thm_deps" "print_binds" "print_facts"
    8.19 +    "print_cases" "print_statement" "thm" "prf" "full_prf" "prop"
    8.20 +    "term" "typ" "print_codesetup" "unused_thms"
    8.21      :: diag
    8.22    and "cd" :: control
    8.23    and "pwd" :: diag
     9.1 --- a/src/Pure/Thy/thy_output.ML	Wed Mar 12 21:29:46 2014 +0100
     9.2 +++ b/src/Pure/Thy/thy_output.ML	Wed Mar 12 21:58:48 2014 +0100
     9.3 @@ -112,11 +112,11 @@
     9.4      |> Pretty.chunks |> Pretty.writeln
     9.5    end;
     9.6  
     9.7 -fun antiquotation name scan out =
     9.8 +fun antiquotation name scan body =
     9.9    add_command name
    9.10      (fn src => fn state => fn ctxt =>
    9.11        let val (x, ctxt') = Args.syntax scan src ctxt
    9.12 -      in out {source = src, state = state, context = ctxt'} x end);
    9.13 +      in body {source = src, state = state, context = ctxt'} x end);
    9.14  
    9.15  
    9.16  
    10.1 --- a/src/Tools/Code/code_runtime.ML	Wed Mar 12 21:29:46 2014 +0100
    10.2 +++ b/src/Tools/Code/code_runtime.ML	Wed Mar 12 21:58:48 2014 +0100
    10.3 @@ -257,15 +257,12 @@
    10.4  
    10.5  in
    10.6  
    10.7 -fun ml_code_antiq context raw_const =
    10.8 +fun ml_code_antiq raw_const ctxt =
    10.9    let
   10.10 -    val ctxt = Context.the_proof context;
   10.11      val thy = Proof_Context.theory_of ctxt;
   10.12 -
   10.13      val const = Code.check_const thy raw_const;
   10.14      val is_first = is_first_occ ctxt;
   10.15 -    val ctxt' = register_const const ctxt;
   10.16 -  in (Context.Proof ctxt', print_code is_first const) end;
   10.17 +  in (print_code is_first const, register_const const ctxt) end;
   10.18  
   10.19  end; (*local*)
   10.20  
   10.21 @@ -356,9 +353,8 @@
   10.22  
   10.23  (** Isar setup **)
   10.24  
   10.25 -val _ = Theory.setup
   10.26 -  (ML_Context.add_antiq @{binding code}
   10.27 -    (Scan.depend (fn context => Scan.pass context Args.term >> ml_code_antiq context)));
   10.28 +val _ =
   10.29 +  Theory.setup (ML_Context.antiquotation @{binding code} Args.term (fn _ => ml_code_antiq));
   10.30  
   10.31  local
   10.32