proper binding/report of defined simprocs;
authorwenzelm
Sat Apr 23 13:53:09 2011 +0200 (2011-04-23)
changeset 42464ae16b8abf1a8
parent 42463 f270e3e18be5
child 42465 1ba52683512a
proper binding/report of defined simprocs;
tuned signature;
src/Pure/Isar/args.ML
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/isar_syn.ML
src/Pure/simplifier.ML
     1.1 --- a/src/Pure/Isar/args.ML	Sat Apr 23 13:00:19 2011 +0200
     1.2 +++ b/src/Pure/Isar/args.ML	Sat Apr 23 13:53:09 2011 +0200
     1.3 @@ -46,7 +46,8 @@
     1.4    val named_typ: (string -> typ) -> typ parser
     1.5    val named_term: (string -> term) -> term parser
     1.6    val named_fact: (string -> thm list) -> thm list parser
     1.7 -  val named_attribute: (string -> morphism -> attribute) -> (morphism -> attribute) parser
     1.8 +  val named_attribute:
     1.9 +    (string * Position.T -> morphism -> attribute) -> (morphism -> attribute) parser
    1.10    val typ_abbrev: typ context_parser
    1.11    val typ: typ context_parser
    1.12    val term: term context_parser
    1.13 @@ -176,10 +177,13 @@
    1.14  fun named_text intern = internal_text || named >> evaluate Token.Text (intern o Token.content_of);
    1.15  fun named_typ readT = internal_typ || named >> evaluate Token.Typ (readT o Token.source_of);
    1.16  fun named_term read = internal_term || named >> evaluate Token.Term (read o Token.source_of);
    1.17 +
    1.18  fun named_fact get = internal_fact || named >> evaluate Token.Fact (get o Token.content_of) ||
    1.19    alt_string >> evaluate Token.Fact (get o Token.source_of);
    1.20 +
    1.21  fun named_attribute att =
    1.22 -  internal_attribute || named >> evaluate Token.Attribute (att o Token.content_of);
    1.23 +  internal_attribute ||
    1.24 +  named >> evaluate Token.Attribute (fn tok => att (Token.content_of tok, Token.position_of tok));
    1.25  
    1.26  
    1.27  (* terms and types *)
     2.1 --- a/src/Pure/Isar/isar_cmd.ML	Sat Apr 23 13:00:19 2011 +0200
     2.2 +++ b/src/Pure/Isar/isar_cmd.ML	Sat Apr 23 13:53:09 2011 +0200
     2.3 @@ -20,8 +20,8 @@
     2.4    val add_defs: (bool * bool) * ((binding * string) * Attrib.src list) list -> theory -> theory
     2.5    val declaration: {syntax: bool, pervasive: bool} ->
     2.6      Symbol_Pos.text * Position.T -> local_theory -> local_theory
     2.7 -  val simproc_setup: string -> string list -> Symbol_Pos.text * Position.T -> string list ->
     2.8 -    local_theory -> local_theory
     2.9 +  val simproc_setup: string * Position.T -> string list -> Symbol_Pos.text * Position.T ->
    2.10 +    string list -> local_theory -> local_theory
    2.11    val hide_class: bool -> xstring list -> theory -> theory
    2.12    val hide_type: bool -> xstring list -> theory -> theory
    2.13    val hide_const: bool -> xstring list -> theory -> theory
    2.14 @@ -214,7 +214,7 @@
    2.15    ML_Lex.read pos txt
    2.16    |> ML_Context.expression pos
    2.17      "val proc: Morphism.morphism -> Simplifier.simpset -> cterm -> thm option"
    2.18 -    ("Context.map_proof (Simplifier.def_simproc {name = " ^ ML_Syntax.print_string name ^ ", \
    2.19 +    ("Context.map_proof (Simplifier.def_simproc_cmd {name = " ^ ML_Syntax.make_binding name ^ ", \
    2.20        \lhss = " ^ ML_Syntax.print_strings lhss ^ ", proc = proc, \
    2.21        \identifier = Library.maps ML_Context.thms " ^ ML_Syntax.print_strings identifier ^ "})")
    2.22    |> Context.proof_map;
     3.1 --- a/src/Pure/Isar/isar_syn.ML	Sat Apr 23 13:00:19 2011 +0200
     3.2 +++ b/src/Pure/Isar/isar_syn.ML	Sat Apr 23 13:53:09 2011 +0200
     3.3 @@ -349,7 +349,7 @@
     3.4  
     3.5  val _ =
     3.6    Outer_Syntax.local_theory "simproc_setup" "define simproc in ML" (Keyword.tag_ml Keyword.thy_decl)
     3.7 -    (Parse.name --
     3.8 +    (Parse.position Parse.name --
     3.9        (Parse.$$$ "(" |-- Parse.enum1 "|" Parse.term --| Parse.$$$ ")" --| Parse.$$$ "=") --
    3.10        Parse.ML_source -- Scan.optional (Parse.$$$ "identifier" |-- Scan.repeat1 Parse.xname) []
    3.11      >> (fn (((a, b), c), d) => Isar_Cmd.simproc_setup a b c d));
     4.1 --- a/src/Pure/simplifier.ML	Sat Apr 23 13:00:19 2011 +0200
     4.2 +++ b/src/Pure/simplifier.ML	Sat Apr 23 13:53:09 2011 +0200
     4.3 @@ -58,11 +58,11 @@
     4.4    val cong_add: attribute
     4.5    val cong_del: attribute
     4.6    val map_simpset: (simpset -> simpset) -> theory -> theory
     4.7 -  val get_simproc: Context.generic -> xstring -> simproc
     4.8 -  val def_simproc: {name: string, lhss: string list,
     4.9 +  val get_simproc: Proof.context -> xstring * Position.T -> simproc
    4.10 +  val def_simproc: {name: binding, lhss: term list,
    4.11      proc: morphism -> simpset -> cterm -> thm option, identifier: thm list} ->
    4.12      local_theory -> local_theory
    4.13 -  val def_simproc_i: {name: string, lhss: term list,
    4.14 +  val def_simproc_cmd: {name: binding, lhss: string list,
    4.15      proc: morphism -> simpset -> cterm -> thm option, identifier: thm list} ->
    4.16      local_theory -> local_theory
    4.17    val cong_modifiers: Method.modifier parser list
    4.18 @@ -162,27 +162,28 @@
    4.19  
    4.20  (* get simprocs *)
    4.21  
    4.22 -fun get_simproc context xname =
    4.23 +fun get_simproc ctxt (xname, pos) =
    4.24    let
    4.25 -    val (space, tab) = Simprocs.get context;
    4.26 +    val (space, tab) = Simprocs.get (Context.Proof ctxt);
    4.27      val name = Name_Space.intern space xname;
    4.28    in
    4.29      (case Symtab.lookup tab name of
    4.30 -      SOME proc => proc
    4.31 +      SOME proc => (Context_Position.report ctxt pos (Name_Space.markup space name); proc)
    4.32      | NONE => error ("Undefined simplification procedure: " ^ quote name))
    4.33    end;
    4.34  
    4.35 -val _ = ML_Antiquote.value "simproc" (Scan.lift Args.name >> (fn name =>
    4.36 -  "Simplifier.get_simproc (ML_Context.the_generic_context ()) " ^ ML_Syntax.print_string name));
    4.37 +val _ =
    4.38 +  ML_Antiquote.value "simproc" (Scan.lift (Parse.position Args.name) >> (fn x =>
    4.39 +    "Simplifier.get_simproc (ML_Context.the_local_context ()) " ^
    4.40 +      ML_Syntax.print_pair ML_Syntax.print_string  ML_Syntax.print_position x));
    4.41  
    4.42  
    4.43  (* define simprocs *)
    4.44  
    4.45  local
    4.46  
    4.47 -fun gen_simproc prep {name, lhss, proc, identifier} lthy =
    4.48 +fun gen_simproc prep {name = b, lhss, proc, identifier} lthy =
    4.49    let
    4.50 -    val b = Binding.name name;
    4.51      val naming = Local_Theory.naming_of lthy;
    4.52      val simproc = make_simproc
    4.53        {name = Name_Space.full_name naming b,
    4.54 @@ -211,8 +212,8 @@
    4.55  
    4.56  in
    4.57  
    4.58 -val def_simproc = gen_simproc Syntax.read_terms;
    4.59 -val def_simproc_i = gen_simproc Syntax.check_terms;
    4.60 +val def_simproc = gen_simproc Syntax.check_terms;
    4.61 +val def_simproc_cmd = gen_simproc Syntax.read_terms;
    4.62  
    4.63  end;
    4.64  
    4.65 @@ -310,7 +311,7 @@
    4.66  val simproc_att =
    4.67    Scan.peek (fn context =>
    4.68      add_del :|-- (fn decl =>
    4.69 -      Scan.repeat1 (Args.named_attribute (decl o get_simproc context))
    4.70 +      Scan.repeat1 (Args.named_attribute (decl o get_simproc (Context.proof_of context)))
    4.71        >> (Library.apply o map Morphism.form)));
    4.72  
    4.73  end;