--- 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;