Addition of oracles

--- a/src/Pure/Thy/thy_parse.ML	Tue Mar 05 13:18:58 1996 +0100
+++ b/src/Pure/Thy/thy_parse.ML	Tue Mar 05 15:52:59 1996 +0100
@@ -504,7 +504,8 @@
   "{", "}", "(", ")", "[", "]", "::", "==", "=>", "<="];
 
 val pure_sections =
- [section "classes" "|> add_classes" class_decls,
+ [section "oracle" "|> set_oracle" ident,
+  section "classes" "|> add_classes" class_decls,
   section "default" "|> add_defsort" sort,
   section "types" "" type_decls,
   section "arities" "|> add_arities" arity_decls,

--- a/src/Pure/theory.ML	Tue Mar 05 13:18:58 1996 +0100
+++ b/src/Pure/theory.ML	Tue Mar 05 15:52:59 1996 +0100
@@ -11,7 +11,8 @@
   type theory
   exception THEORY of string * theory list
   val rep_theory        : theory ->
-    {sign: Sign.sg, new_axioms: term Symtab.table, parents: theory list}
+    {sign: Sign.sg, oraopt: (Sign.sg * exn -> term) option,
+     new_axioms: term Symtab.table, parents: theory list}
   val sign_of           : theory -> Sign.sg
   val syn_of            : theory -> Syntax.syntax
   val stamps_of_thy     : theory -> string ref list
@@ -22,32 +23,34 @@
   val pure_thy          : theory
   val cpure_thy         : theory
   (*theory primitives*)
-  val add_classes     : (class * class list) list -> theory -> theory
-  val add_classrel    : (class * class) list -> theory -> theory
-  val add_defsort     : sort -> theory -> theory
-  val add_types       : (string * int * mixfix) list -> theory -> theory
-  val add_tyabbrs     : (string * string list * string * mixfix) list
+  val add_classes	: (class * class list) list -> theory -> theory
+  val add_classrel	: (class * class) list -> theory -> theory
+  val add_defsort	: sort -> theory -> theory
+  val add_types		: (string * int * mixfix) list -> theory -> theory
+  val add_tyabbrs	: (string * string list * string * mixfix) list
     -> theory -> theory
-  val add_tyabbrs_i   : (string * string list * typ * mixfix) list
+  val add_tyabbrs_i	: (string * string list * typ * mixfix) list
     -> theory -> theory
-  val add_arities     : (string * sort list * sort) list -> theory -> theory
-  val add_consts      : (string * string * mixfix) list -> theory -> theory
-  val add_consts_i    : (string * typ * mixfix) list -> theory -> theory
-  val add_syntax      : (string * string * mixfix) list -> theory -> theory
-  val add_syntax_i    : (string * typ * mixfix) list -> theory -> theory
-  val add_trfuns      :
+  val add_arities	: (string * sort list * sort) list -> theory -> theory
+  val add_consts	: (string * string * mixfix) list -> theory -> theory
+  val add_consts_i	: (string * typ * mixfix) list -> theory -> theory
+  val add_syntax	: (string * string * mixfix) list -> theory -> theory
+  val add_syntax_i	: (string * typ * mixfix) list -> theory -> theory
+  val add_trfuns	:
     (string * (Syntax.ast list -> Syntax.ast)) list *
     (string * (term list -> term)) list *
     (string * (term list -> term)) list *
     (string * (Syntax.ast list -> Syntax.ast)) list -> theory -> theory
   val add_trrules     : (string * string)Syntax.trrule list -> theory -> theory
-  val add_trrules_i   : Syntax.ast Syntax.trrule list -> theory -> theory
+  val add_trrules_i	: Syntax.ast Syntax.trrule list -> theory -> theory
   val cert_axm          : Sign.sg -> string * term -> string * term
   val read_axm          : Sign.sg -> string * string -> string * term
   val inferT_axm        : Sign.sg -> string * term -> string * term
-  val add_axioms      : (string * string) list -> theory -> theory
-  val add_axioms_i    : (string * term) list -> theory -> theory
-  val add_thyname     : string -> theory -> theory
+  val add_axioms	: (string * string) list -> theory -> theory
+  val add_axioms_i	: (string * term) list -> theory -> theory
+  val add_thyname	: string -> theory -> theory
+
+  val set_oracle	: (Sign.sg * exn -> term) -> theory -> theory
 
   val merge_theories    : theory * theory -> theory
   val merge_thy_list    : bool -> theory list -> theory
@@ -61,6 +64,7 @@
 datatype theory =
   Theory of {
     sign: Sign.sg,
+    oraopt: (Sign.sg * exn -> term) option,
     new_axioms: term Symtab.table,
     parents: theory list};
 
@@ -88,13 +92,16 @@
 (* the Pure theories *)
 
 val proto_pure_thy =
-  Theory {sign = Sign.proto_pure, new_axioms = Symtab.null, parents = []};
+  Theory {sign = Sign.proto_pure, oraopt = None, 
+	  new_axioms = Symtab.null, parents = []};
 
 val pure_thy =
-  Theory {sign = Sign.pure, new_axioms = Symtab.null, parents = []};
+  Theory {sign = Sign.pure, oraopt = None, 
+	  new_axioms = Symtab.null, parents = []};
 
 val cpure_thy =
-  Theory {sign = Sign.cpure, new_axioms = Symtab.null, parents = []};
+  Theory {sign = Sign.cpure, oraopt = None, 
+	  new_axioms = Symtab.null, parents = []};
 
 
 
@@ -103,7 +110,8 @@
 fun err_dup_axms names =
   error ("Duplicate axiom name(s) " ^ commas_quote names);
 
-fun ext_thy (thy as Theory {sign, new_axioms, parents}) sign1 new_axms =
+fun ext_thy (thy as Theory {sign, oraopt, new_axioms, parents}) 
+            sign1 new_axms =
   let
     val draft = Sign.is_draft sign;
     val new_axioms1 =
@@ -111,7 +119,8 @@
         handle Symtab.DUPS names => err_dup_axms names;
     val parents1 = if draft then parents else [thy];
   in
-    Theory {sign = sign1, new_axioms = new_axioms1, parents = parents1}
+    Theory {sign = sign1, oraopt = oraopt, 
+	    new_axioms = new_axioms1, parents = parents1}
   end;
 
 
@@ -187,6 +196,18 @@
 val add_axioms_i = ext_axms cert_axm;
 
 
+(** Set oracle of theory **)
+
+fun set_oracle oracle 
+               (thy as Theory {sign, oraopt = None, new_axioms, parents}) =
+      if Sign.is_draft sign then
+	Theory {sign = sign, 
+		oraopt = Some oracle, 
+		new_axioms = new_axioms, 
+		parents = parents}
+      else raise THEORY ("Can only set oracle of a draft", [thy])
+  | set_oracle _ thy = raise THEORY ("Oracle already set", [thy]);
+
 
 (** merge theories **)
 
@@ -198,15 +219,16 @@
     fun add_sign (sg, Theory {sign, ...}) =
       Sign.merge (sg, sign) handle TERM (msg, _) => error msg;
   in
-    (case (find_first is_union thys, exists is_draft thys) of
+    case (find_first is_union thys, exists is_draft thys) of
       (Some thy, _) => thy
     | (None, true) => raise THEORY ("Illegal merge of draft theories", thys)
     | (None, false) => Theory {
         sign =
           (if mk_draft then Sign.make_draft else I)
           (foldl add_sign (Sign.proto_pure, thys)),
+	oraopt = None,
         new_axioms = Symtab.null,
-        parents = thys})
+        parents = thys}
   end;
 
 fun merge_theories (thy1, thy2) = merge_thy_list false [thy1, thy2];

--- a/src/Pure/thm.ML	Tue Mar 05 13:18:58 1996 +0100
+++ b/src/Pure/thm.ML	Tue Mar 05 15:52:59 1996 +0100
@@ -74,7 +74,7 @@
     | Rename_params_rule of string list * int;
 
   datatype deriv = Infer  of rule * deriv list
-		 | Oracle of string * exn ;
+		 | Oracle of theory * Sign.sg * exn;
 
   (*meta theorems*)
   type thm
@@ -150,6 +150,8 @@
   val trace_simp        : bool ref
   val rewrite_cterm     : bool * bool -> meta_simpset ->
                           (meta_simpset -> thm -> thm option) -> cterm -> thm
+
+  val invoke_oracle	: theory * Sign.sg * exn -> thm
 end;
 
 structure Thm : THM =
@@ -320,7 +322,7 @@
 
 
 datatype deriv = Infer	of rule * deriv list
-	       | Oracle	of string * exn (*???*);
+	       | Oracle	of theory * Sign.sg * exn;
 
 
 val full_deriv = ref false;
@@ -515,7 +517,7 @@
   let
     fun get_ax [] = raise Match
       | get_ax (thy :: thys) =
-	  let val {sign, new_axioms, parents} = rep_theory thy
+	  let val {sign, new_axioms, parents, ...} = rep_theory thy
           in case Symtab.lookup (new_axioms, name) of
 		Some t => fix_shyps [] []
 		           (Thm {sign = sign, 
@@ -1732,6 +1734,25 @@
           prop = prop}
   end
 
+
+fun invoke_oracle (thy, sign, exn) =
+    case #oraopt(rep_theory thy) of
+	None => raise THM ("No oracle in supplied theory", 0, [])
+      | Some oracle => 
+	    let val sign' = Sign.merge(sign_of thy, sign)
+		val (prop, T, maxidx) = 
+		    Sign.certify_term sign' (oracle (sign', exn))
+            in if T<>propT then
+                  raise THM("Oracle's result must have type prop", 0, [])
+	       else fix_shyps [] []
+		     (Thm {sign = sign', 
+			   der = Oracle(thy,sign,exn),
+			   maxidx = maxidx,
+			   shyps = [], 
+			   hyps = [], 
+			   prop = prop})
+            end;
+
 end;
 
 open Thm;