tuned oracle interface;
authorwenzelm
Sun Feb 04 22:02:19 2007 +0100 (2007-02-04 ago)
changeset 222399ddd3349d597
parent 22238 090f215ab631
child 22240 36cc1875619f
tuned oracle interface;
simproc_setup: added identifier;
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/isar_syn.ML
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Sun Feb 04 22:02:18 2007 +0100
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Sun Feb 04 22:02:19 2007 +0100
     1.3 @@ -14,13 +14,13 @@
     1.4    val typed_print_translation: bool * string -> theory -> theory
     1.5    val print_ast_translation: bool * string -> theory -> theory
     1.6    val token_translation: string -> theory -> theory
     1.7 -  val oracle: bstring * string * string -> theory -> theory
     1.8 +  val oracle: bstring -> string -> string -> theory -> theory
     1.9    val add_axioms: ((bstring * string) * Attrib.src list) list -> theory -> theory
    1.10    val add_defs: (bool * bool) * ((bstring * string) * Attrib.src list) list -> theory -> theory
    1.11    val apply_theorems: (thmref * Attrib.src list) list -> theory -> thm list * theory
    1.12    val apply_theorems_i: (thm list * attribute list) list -> theory -> thm list * theory
    1.13    val declaration: string -> local_theory -> local_theory
    1.14 -  val simproc_setup: string * string list * string -> local_theory -> local_theory
    1.15 +  val simproc_setup: string -> string list -> string -> string list -> local_theory -> local_theory
    1.16    val have: ((string * Attrib.src list) * (string * string list) list) list ->
    1.17      bool -> Proof.state -> Proof.state
    1.18    val hence: ((string * Attrib.src list) * (string * string list) list) list ->
    1.19 @@ -192,10 +192,10 @@
    1.20  
    1.21  (* oracles *)
    1.22  
    1.23 -fun oracle (name, T, oracle) =
    1.24 +fun oracle name typ oracle =
    1.25    let val txt =
    1.26      "local\n\
    1.27 -    \  type T = " ^ T ^ ";\n\
    1.28 +    \  type T = " ^ typ ^ ";\n\
    1.29      \  val oracle: theory -> T -> term = " ^ oracle ^ ";\n\
    1.30      \  val name = " ^ quote name ^ ";\n\
    1.31      \  exception Arg of T;\n\
    1.32 @@ -241,11 +241,12 @@
    1.33  
    1.34  (* simprocs *)
    1.35  
    1.36 -fun simproc_setup (name, pats, proc) =
    1.37 +fun simproc_setup name lhss proc identifier =
    1.38    ML_Context.use_let
    1.39 -    "val simproc: Morphism.morphism -> Simplifier.simpset -> cterm -> thm option"
    1.40 -  ("Context.map_proof (Simplifier.def_simproc " ^ ML_Syntax.print_string name ^ " " ^
    1.41 -    ML_Syntax.print_list ML_Syntax.print_string pats ^ " simproc)") proc
    1.42 +    "val proc: Morphism.morphism -> Simplifier.simpset -> cterm -> thm option"
    1.43 +  ("Context.map_proof (Simplifier.def_simproc {name = " ^ ML_Syntax.print_string name ^ ", \
    1.44 +    \lhss = " ^ ML_Syntax.print_strings lhss ^ ", proc = proc, \
    1.45 +    \identifier = Library.maps ML_Context.thms " ^ ML_Syntax.print_strings identifier ^ "})") proc
    1.46    |> Context.proof_map;
    1.47  
    1.48  
     2.1 --- a/src/Pure/Isar/isar_syn.ML	Sun Feb 04 22:02:18 2007 +0100
     2.2 +++ b/src/Pure/Isar/isar_syn.ML	Sun Feb 04 22:02:19 2007 +0100
     2.3 @@ -314,8 +314,9 @@
     2.4  val simproc_setupP =
     2.5    OuterSyntax.command "simproc_setup" "define simproc in ML" (K.tag_ml K.thy_decl)
     2.6      (P.opt_target --
     2.7 -      P.name -- (P.$$$ "(" |-- P.enum1 "|" P.term --| P.$$$ ")" --| P.$$$ "=") -- P.text
     2.8 -    >> (fn (((loc, x), y), z) => Toplevel.local_theory loc (IsarCmd.simproc_setup (x, y, z))));
     2.9 +      P.name -- (P.$$$ "(" |-- P.enum1 "|" P.term --| P.$$$ ")" --| P.$$$ "=") -- P.text --
    2.10 +      Scan.optional (P.$$$ "identifier" |-- Scan.repeat1 P.xname) []
    2.11 +    >> (fn ((((loc, a), b), c), d) => Toplevel.local_theory loc (IsarCmd.simproc_setup a b c d)));
    2.12  
    2.13  
    2.14  (* translation functions *)
    2.15 @@ -358,7 +359,7 @@
    2.16  val oracleP =
    2.17    OuterSyntax.command "oracle" "declare oracle" (K.tag_ml K.thy_decl)
    2.18      (P.name -- (P.$$$ "(" |-- P.text --| P.$$$ ")" --| P.$$$ "=")
    2.19 -      -- P.text >> (Toplevel.theory o IsarCmd.oracle o P.triple1));
    2.20 +      -- P.text >> (fn ((x, y), z) => Toplevel.theory (IsarCmd.oracle x y z)));
    2.21  
    2.22  
    2.23  (* local theories *)
    2.24 @@ -913,14 +914,14 @@
    2.25    outer_parse.ML, otherwise be prepared for unexpected errors*)
    2.26  
    2.27  val _ = OuterSyntax.add_keywords
    2.28 - ["!", "!!", "%", "(", ")", "+", ",", "--", ":", "::", ";", "<", "<=",
    2.29 -  "=", "==", "=>", "?", "[", "]", "advanced", "and", "assumes", "attach",
    2.30 -  "begin", "binder", "concl", "constrains", "defines", "fixes", "for",
    2.31 -  "imports", "if", "in", "includes", "infix", "infixl", "infixr",
    2.32 -  "is", "notes", "obtains", "open", "output", "overloaded", "shows",
    2.33 -  "structure", "unchecked", "uses", "where", "|", "\\<equiv>",
    2.34 -  "\\<leftharpoondown>", "\\<rightharpoonup>",
    2.35 -  "\\<rightleftharpoons>", "\\<subseteq>"];
    2.36 + ["!!", "!", "%", "(", ")", "+", ",", "--", ":", "::", ";", "<", "<=",
    2.37 +  "=", "==", "=>", "?", "[", "\\<equiv>", "\\<leftharpoondown>",
    2.38 +  "\\<rightharpoonup>", "\\<rightleftharpoons>", "\\<subseteq>", "]",
    2.39 +  "advanced", "and", "assumes", "attach", "begin", "binder", "concl",
    2.40 +  "constrains", "defines", "fixes", "for", "identifier", "if",
    2.41 +  "imports", "in", "includes", "infix", "infixl", "infixr", "is",
    2.42 +  "notes", "obtains", "open", "output", "overloaded", "shows",
    2.43 +  "structure", "unchecked", "uses", "where", "|"];
    2.44  
    2.45  val _ = OuterSyntax.add_parsers [
    2.46    (*theory structure*)