Thm.add_oracle interface: replaced old bstring by binding;
authorwenzelm
Thu Mar 05 19:48:02 2009 +0100 (2009-03-05)
changeset 30288a32700e45ab3
parent 30287 39b931e00ba9
child 30289 b28caca9157f
Thm.add_oracle interface: replaced old bstring by binding;
doc-src/IsarImplementation/Thy/Logic.thy
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/skip_proof.ML
src/Pure/codegen.ML
src/Pure/thm.ML
src/Tools/Compute_Oracle/compute.ML
src/Tools/nbe.ML
     1.1 --- a/doc-src/IsarImplementation/Thy/Logic.thy	Thu Mar 05 18:19:20 2009 +0100
     1.2 +++ b/doc-src/IsarImplementation/Thy/Logic.thy	Thu Mar 05 19:48:02 2009 +0100
     1.3 @@ -556,7 +556,7 @@
     1.4    @{index_ML Thm.generalize: "string list * string list -> int -> thm -> thm"} \\
     1.5    @{index_ML Thm.instantiate: "(ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm"} \\
     1.6    @{index_ML Thm.axiom: "theory -> string -> thm"} \\
     1.7 -  @{index_ML Thm.add_oracle: "bstring * ('a -> cterm) -> theory
     1.8 +  @{index_ML Thm.add_oracle: "binding * ('a -> cterm) -> theory
     1.9    -> (string * ('a -> thm)) * theory"} \\
    1.10    \end{mldecls}
    1.11    \begin{mldecls}
    1.12 @@ -613,7 +613,7 @@
    1.13    \item @{ML Thm.axiom}~@{text "thy name"} retrieves a named
    1.14    axiom, cf.\ @{text "axiom"} in \figref{fig:prim-rules}.
    1.15  
    1.16 -  \item @{ML Thm.add_oracle}~@{text "(name, oracle)"} produces a named
    1.17 +  \item @{ML Thm.add_oracle}~@{text "(binding, oracle)"} produces a named
    1.18    oracle rule, essentially generating arbitrary axioms on the fly,
    1.19    cf.\ @{text "axiom"} in \figref{fig:prim-rules}.
    1.20  
     2.1 --- a/src/Pure/Isar/isar_cmd.ML	Thu Mar 05 18:19:20 2009 +0100
     2.2 +++ b/src/Pure/Isar/isar_cmd.ML	Thu Mar 05 19:48:02 2009 +0100
     2.3 @@ -150,10 +150,12 @@
     2.4      val oracle = SymbolPos.content (SymbolPos.explode (oracle_txt, pos));
     2.5      val txt =
     2.6        "local\n\
     2.7 -      \  val name = " ^ quote name ^ ";\n\
     2.8 +      \  val name = " ^ ML_Syntax.print_string name ^ ";\n\
     2.9 +      \  val pos = " ^ ML_Syntax.print_position pos ^ ";\n\
    2.10 +      \  val binding = Binding.make (name, pos);\n\
    2.11        \  val oracle = " ^ oracle ^ ";\n\
    2.12        \in\n\
    2.13 -      \  val " ^ name ^ " = snd (Context.>>> (Context.map_theory_result (Thm.add_oracle (name, oracle))));\n\
    2.14 +      \  val " ^ name ^ " = snd (Context.>>> (Context.map_theory_result (Thm.add_oracle (binding, oracle))));\n\
    2.15        \end;\n";
    2.16    in Context.theory_map (ML_Context.exec (fn () => ML_Context.eval false pos txt)) end;
    2.17  
     3.1 --- a/src/Pure/Isar/skip_proof.ML	Thu Mar 05 18:19:20 2009 +0100
     3.2 +++ b/src/Pure/Isar/skip_proof.ML	Thu Mar 05 19:48:02 2009 +0100
     3.3 @@ -20,7 +20,7 @@
     3.4  (* oracle setup *)
     3.5  
     3.6  val (_, skip_proof) = Context.>>> (Context.map_theory_result
     3.7 -  (Thm.add_oracle ("skip_proof", fn (thy, prop) =>
     3.8 +  (Thm.add_oracle (Binding.name "skip_proof", fn (thy, prop) =>
     3.9      if ! quick_and_dirty then Thm.cterm_of thy prop
    3.10      else error "Proof may be skipped in quick_and_dirty mode only!")));
    3.11  
     4.1 --- a/src/Pure/codegen.ML	Thu Mar 05 18:19:20 2009 +0100
     4.2 +++ b/src/Pure/codegen.ML	Thu Mar 05 19:48:02 2009 +0100
     4.3 @@ -938,7 +938,7 @@
     4.4    in e () end;
     4.5  
     4.6  val (_, evaluation_conv) = Context.>>> (Context.map_theory_result
     4.7 -  (Thm.add_oracle ("evaluation", fn ct =>
     4.8 +  (Thm.add_oracle (Binding.name "evaluation", fn ct =>
     4.9      let
    4.10        val thy = Thm.theory_of_cterm ct;
    4.11        val t = Thm.term_of ct;
     5.1 --- a/src/Pure/thm.ML	Thu Mar 05 18:19:20 2009 +0100
     5.2 +++ b/src/Pure/thm.ML	Thu Mar 05 19:48:02 2009 +0100
     5.3 @@ -151,7 +151,7 @@
     5.4    val proof_of: thm -> proof
     5.5    val join_proof: thm -> unit
     5.6    val extern_oracles: theory -> xstring list
     5.7 -  val add_oracle: bstring * ('a -> cterm) -> theory -> (string * ('a -> thm)) * theory
     5.8 +  val add_oracle: binding * ('a -> cterm) -> theory -> (string * ('a -> thm)) * theory
     5.9  end;
    5.10  
    5.11  structure Thm:> THM =
    5.12 @@ -1698,7 +1698,7 @@
    5.13  
    5.14  structure Oracles = TheoryDataFun
    5.15  (
    5.16 -  type T = stamp NameSpace.table;
    5.17 +  type T = serial NameSpace.table;
    5.18    val empty = NameSpace.empty_table;
    5.19    val copy = I;
    5.20    val extend = I;
    5.21 @@ -1708,13 +1708,12 @@
    5.22  
    5.23  val extern_oracles = map #1 o NameSpace.extern_table o Oracles.get;
    5.24  
    5.25 -fun add_oracle (bname, oracle) thy =
    5.26 +fun add_oracle (b, oracle) thy =
    5.27    let
    5.28      val naming = Sign.naming_of thy;
    5.29 -    val name = NameSpace.full_name naming (Binding.name bname);
    5.30 -    val thy' = thy |> Oracles.map (fn (space, tab) =>
    5.31 -      (NameSpace.declare naming (Binding.name bname) space |> snd,
    5.32 -        Symtab.update_new (name, stamp ()) tab handle Symtab.DUP dup => err_dup_ora dup));
    5.33 +    val (name, tab') = NameSpace.bind naming (b, serial ()) (Oracles.get thy)
    5.34 +      handle Symtab.DUP _ => err_dup_ora (Binding.str_of b);
    5.35 +    val thy' = Oracles.put tab' thy;
    5.36    in ((name, invoke_oracle (Theory.check_thy thy') name oracle), thy') end;
    5.37  
    5.38  end;
     6.1 --- a/src/Tools/Compute_Oracle/compute.ML	Thu Mar 05 18:19:20 2009 +0100
     6.2 +++ b/src/Tools/Compute_Oracle/compute.ML	Thu Mar 05 19:48:02 2009 +0100
     6.3 @@ -371,7 +371,7 @@
     6.4  fun merge_shyps shyps1 shyps2 = Sorttab.keys (add_shyps shyps2 (add_shyps shyps1 Sorttab.empty))
     6.5  
     6.6  val (_, export_oracle) = Context.>>> (Context.map_theory_result
     6.7 -  (Thm.add_oracle ("compute", fn (thy, hyps, shyps, prop) =>
     6.8 +  (Thm.add_oracle (Binding.name "compute", fn (thy, hyps, shyps, prop) =>
     6.9      let
    6.10          val shyptab = add_shyps shyps Sorttab.empty
    6.11          fun delete s shyptab = Sorttab.delete s shyptab handle Sorttab.UNDEF _ => shyptab
     7.1 --- a/src/Tools/nbe.ML	Thu Mar 05 18:19:20 2009 +0100
     7.2 +++ b/src/Tools/nbe.ML	Thu Mar 05 19:48:02 2009 +0100
     7.3 @@ -466,7 +466,7 @@
     7.4  (* evaluation oracle *)
     7.5  
     7.6  val (_, norm_oracle) = Context.>>> (Context.map_theory_result
     7.7 -  (Thm.add_oracle ("norm", fn (thy, t, naming, program, vs_ty_t, deps) =>
     7.8 +  (Thm.add_oracle (Binding.name "norm", fn (thy, t, naming, program, vs_ty_t, deps) =>
     7.9      Thm.cterm_of thy (Logic.mk_equals (t, eval thy t naming program vs_ty_t deps)))));
    7.10  
    7.11  fun add_triv_classes thy =