# HG changeset patch # User wenzelm # Date 1303559589 -7200 # Node ID ae16b8abf1a84b34d9b379fcb9d3a0d5377f684d # Parent f270e3e18be5187911d43a3e921289665e78e332 proper binding/report of defined simprocs; tuned signature; diff -r f270e3e18be5 -r ae16b8abf1a8 src/Pure/Isar/args.ML --- a/src/Pure/Isar/args.ML Sat Apr 23 13:00:19 2011 +0200 +++ b/src/Pure/Isar/args.ML Sat Apr 23 13:53:09 2011 +0200 @@ -46,7 +46,8 @@ val named_typ: (string -> typ) -> typ parser val named_term: (string -> term) -> term parser val named_fact: (string -> thm list) -> thm list parser - val named_attribute: (string -> morphism -> attribute) -> (morphism -> attribute) parser + val named_attribute: + (string * Position.T -> morphism -> attribute) -> (morphism -> attribute) parser val typ_abbrev: typ context_parser val typ: typ context_parser val term: term context_parser @@ -176,10 +177,13 @@ fun named_text intern = internal_text || named >> evaluate Token.Text (intern o Token.content_of); fun named_typ readT = internal_typ || named >> evaluate Token.Typ (readT o Token.source_of); fun named_term read = internal_term || named >> evaluate Token.Term (read o Token.source_of); + fun named_fact get = internal_fact || named >> evaluate Token.Fact (get o Token.content_of) || alt_string >> evaluate Token.Fact (get o Token.source_of); + fun named_attribute att = - internal_attribute || named >> evaluate Token.Attribute (att o Token.content_of); + internal_attribute || + named >> evaluate Token.Attribute (fn tok => att (Token.content_of tok, Token.position_of tok)); (* terms and types *) diff -r f270e3e18be5 -r ae16b8abf1a8 src/Pure/Isar/isar_cmd.ML --- a/src/Pure/Isar/isar_cmd.ML Sat Apr 23 13:00:19 2011 +0200 +++ b/src/Pure/Isar/isar_cmd.ML Sat Apr 23 13:53:09 2011 +0200 @@ -20,8 +20,8 @@ val add_defs: (bool * bool) * ((binding * string) * Attrib.src list) list -> theory -> theory val declaration: {syntax: bool, pervasive: bool} -> Symbol_Pos.text * Position.T -> local_theory -> local_theory - val simproc_setup: string -> string list -> Symbol_Pos.text * Position.T -> string list -> - local_theory -> local_theory + val simproc_setup: string * Position.T -> string list -> Symbol_Pos.text * Position.T -> + string list -> local_theory -> local_theory val hide_class: bool -> xstring list -> theory -> theory val hide_type: bool -> xstring list -> theory -> theory val hide_const: bool -> xstring list -> theory -> theory @@ -214,7 +214,7 @@ ML_Lex.read pos txt |> ML_Context.expression pos "val proc: Morphism.morphism -> Simplifier.simpset -> cterm -> thm option" - ("Context.map_proof (Simplifier.def_simproc {name = " ^ ML_Syntax.print_string name ^ ", \ + ("Context.map_proof (Simplifier.def_simproc_cmd {name = " ^ ML_Syntax.make_binding name ^ ", \ \lhss = " ^ ML_Syntax.print_strings lhss ^ ", proc = proc, \ \identifier = Library.maps ML_Context.thms " ^ ML_Syntax.print_strings identifier ^ "})") |> Context.proof_map; diff -r f270e3e18be5 -r ae16b8abf1a8 src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Sat Apr 23 13:00:19 2011 +0200 +++ b/src/Pure/Isar/isar_syn.ML Sat Apr 23 13:53:09 2011 +0200 @@ -349,7 +349,7 @@ val _ = Outer_Syntax.local_theory "simproc_setup" "define simproc in ML" (Keyword.tag_ml Keyword.thy_decl) - (Parse.name -- + (Parse.position Parse.name -- (Parse.$$$ "(" |-- Parse.enum1 "|" Parse.term --| Parse.$$$ ")" --| Parse.$$$ "=") -- Parse.ML_source -- Scan.optional (Parse.$$$ "identifier" |-- Scan.repeat1 Parse.xname) [] >> (fn (((a, b), c), d) => Isar_Cmd.simproc_setup a b c d)); diff -r f270e3e18be5 -r ae16b8abf1a8 src/Pure/simplifier.ML --- a/src/Pure/simplifier.ML Sat Apr 23 13:00:19 2011 +0200 +++ b/src/Pure/simplifier.ML Sat Apr 23 13:53:09 2011 +0200 @@ -58,11 +58,11 @@ val cong_add: attribute val cong_del: attribute val map_simpset: (simpset -> simpset) -> theory -> theory - val get_simproc: Context.generic -> xstring -> simproc - val def_simproc: {name: string, lhss: string list, + val get_simproc: Proof.context -> xstring * Position.T -> simproc + val def_simproc: {name: binding, lhss: term list, proc: morphism -> simpset -> cterm -> thm option, identifier: thm list} -> local_theory -> local_theory - val def_simproc_i: {name: string, lhss: term list, + val def_simproc_cmd: {name: binding, lhss: string list, proc: morphism -> simpset -> cterm -> thm option, identifier: thm list} -> local_theory -> local_theory val cong_modifiers: Method.modifier parser list @@ -162,27 +162,28 @@ (* get simprocs *) -fun get_simproc context xname = +fun get_simproc ctxt (xname, pos) = let - val (space, tab) = Simprocs.get context; + val (space, tab) = Simprocs.get (Context.Proof ctxt); val name = Name_Space.intern space xname; in (case Symtab.lookup tab name of - SOME proc => proc + SOME proc => (Context_Position.report ctxt pos (Name_Space.markup space name); proc) | NONE => error ("Undefined simplification procedure: " ^ quote name)) end; -val _ = ML_Antiquote.value "simproc" (Scan.lift Args.name >> (fn name => - "Simplifier.get_simproc (ML_Context.the_generic_context ()) " ^ ML_Syntax.print_string name)); +val _ = + ML_Antiquote.value "simproc" (Scan.lift (Parse.position Args.name) >> (fn x => + "Simplifier.get_simproc (ML_Context.the_local_context ()) " ^ + ML_Syntax.print_pair ML_Syntax.print_string ML_Syntax.print_position x)); (* define simprocs *) local -fun gen_simproc prep {name, lhss, proc, identifier} lthy = +fun gen_simproc prep {name = b, lhss, proc, identifier} lthy = let - val b = Binding.name name; val naming = Local_Theory.naming_of lthy; val simproc = make_simproc {name = Name_Space.full_name naming b, @@ -211,8 +212,8 @@ in -val def_simproc = gen_simproc Syntax.read_terms; -val def_simproc_i = gen_simproc Syntax.check_terms; +val def_simproc = gen_simproc Syntax.check_terms; +val def_simproc_cmd = gen_simproc Syntax.read_terms; end; @@ -310,7 +311,7 @@ val simproc_att = Scan.peek (fn context => add_del :|-- (fn decl => - Scan.repeat1 (Args.named_attribute (decl o get_simproc context)) + Scan.repeat1 (Args.named_attribute (decl o get_simproc (Context.proof_of context))) >> (Library.apply o map Morphism.form))); end;