# HG changeset patch # User paulson # Date 826037579 -3600 # Node ID f21c8fab7c3c50d04d3a42d384771d700eb3b7f6 # Parent 31ad553d018b85315e0a7741072268ab696e9a58 Addition of oracles diff -r 31ad553d018b -r f21c8fab7c3c src/Pure/Thy/thy_parse.ML --- 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, diff -r 31ad553d018b -r f21c8fab7c3c src/Pure/theory.ML --- 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]; diff -r 31ad553d018b -r f21c8fab7c3c src/Pure/thm.ML --- 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;