--- a/src/Doc/Implementation/Prelim.thy Sun Aug 16 17:11:31 2015 +0200
+++ b/src/Doc/Implementation/Prelim.thy Sun Aug 16 18:19:30 2015 +0200
@@ -121,8 +121,8 @@
text %mlref \<open>
\begin{mldecls}
@{index_ML_type theory} \\
- @{index_ML Theory.eq_thy: "theory * theory -> bool"} \\
- @{index_ML Theory.subthy: "theory * theory -> bool"} \\
+ @{index_ML Context.eq_thy: "theory * theory -> bool"} \\
+ @{index_ML Context.subthy: "theory * theory -> bool"} \\
@{index_ML Theory.merge: "theory * theory -> theory"} \\
@{index_ML Theory.begin_theory: "string * Position.T -> theory list -> theory"} \\
@{index_ML Theory.parents_of: "theory -> theory list"} \\
@@ -133,10 +133,10 @@
\item Type @{ML_type theory} represents theory contexts.
- \item @{ML "Theory.eq_thy"}~@{text "(thy\<^sub>1, thy\<^sub>2)"} check strict
+ \item @{ML "Context.eq_thy"}~@{text "(thy\<^sub>1, thy\<^sub>2)"} check strict
identity of two theories.
- \item @{ML "Theory.subthy"}~@{text "(thy\<^sub>1, thy\<^sub>2)"} compares theories
+ \item @{ML "Context.subthy"}~@{text "(thy\<^sub>1, thy\<^sub>2)"} compares theories
according to the intrinsic graph structure of the construction.
This sub-theory relation is a nominal approximation of inclusion
(@{text "\<subseteq>"}) of the corresponding content (according to the
--- a/src/HOL/Matrix_LP/Compute_Oracle/compute.ML Sun Aug 16 17:11:31 2015 +0200
+++ b/src/HOL/Matrix_LP/Compute_Oracle/compute.ML Sun Aug 16 18:19:30 2015 +0200
@@ -607,7 +607,7 @@
val thy = theory_of computer
val _ = check_compatible computer th
val _ =
- Theory.subthy (theory_of_theorem th, thy) orelse raise Compute "modus_ponens: bad theory"
+ Context.subthy (theory_of_theorem th, thy) orelse raise Compute "modus_ponens: bad theory"
val th' = make_theorem computer (Thm.transfer thy raw_th') []
val varsubst = varsubst_of_theorem th
fun run vars_allowed t =
--- a/src/HOL/Tools/BNF/bnf_def.ML Sun Aug 16 17:11:31 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_def.ML Sun Aug 16 18:19:30 2015 +0200
@@ -809,7 +809,7 @@
end;
fun maybe_restore lthy_old lthy =
- lthy |> not (Theory.eq_thy (apply2 Proof_Context.theory_of (lthy_old, lthy)))
+ lthy |> not (Context.eq_thy (apply2 Proof_Context.theory_of (lthy_old, lthy)))
? Local_Theory.restore;
val map_bind_def =
--- a/src/HOL/Tools/Nitpick/nitpick.ML Sun Aug 16 17:11:31 2015 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Sun Aug 16 18:19:30 2015 +0200
@@ -220,7 +220,7 @@
(* FIXME: reintroduce code before new release:
val nitpick_thy = Thy_Info.get_theory "Nitpick"
- val _ = Theory.subthy (nitpick_thy, thy) orelse
+ val _ = Context.subthy (nitpick_thy, thy) orelse
error "You must import the theory \"Nitpick\" to use Nitpick"
*)
val {cards_assigns, maxes_assigns, iters_assigns, bitss, bisim_depths,
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Sun Aug 16 17:11:31 2015 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Sun Aug 16 18:19:30 2015 +0200
@@ -1358,13 +1358,14 @@
(* Ideally we would check against "Complex_Main", not "Hilbert_Choice", but any
theory will do as long as it contains all the "axioms" and "axiomatization"
commands. *)
-fun is_built_in_theory thy = Theory.subthy (thy, @{theory Hilbert_Choice})
+fun is_built_in_theory thy_id =
+ Context.subthy_id (thy_id, Context.theory_id @{theory Hilbert_Choice})
fun all_nondefs_of ctxt subst =
ctxt |> Spec_Rules.get
|> filter (curry (op =) Spec_Rules.Unknown o fst)
|> maps (snd o snd)
- |> filter_out (is_built_in_theory o Thm.theory_of_thm)
+ |> filter_out (is_built_in_theory o Thm.theory_id_of_thm)
|> map (subst_atomic subst o Thm.prop_of)
fun arity_of_built_in_const (s, T) =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Sun Aug 16 17:11:31 2015 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Sun Aug 16 18:19:30 2015 +0200
@@ -351,7 +351,7 @@
| normalize_eq t = t
fun if_thm_before th th' =
- if Theory.subthy (apply2 Thm.theory_of_thm (th, th')) then th else th'
+ if Context.subthy_id (apply2 Thm.theory_id_of_thm (th, th')) then th else th'
(* Hack: Conflate the facts about a class as seen from the outside with the corresponding low-level
facts, so that MaSh can learn from the low-level proofs. *)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Sun Aug 16 17:11:31 2015 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Sun Aug 16 18:19:30 2015 +0200
@@ -768,30 +768,39 @@
fun class_feature_of s = "s" ^ s
val local_feature = "local"
-fun crude_theory_ord p =
- if Theory.subthy p then
- if Theory.eq_thy p then EQUAL else LESS
- else if Theory.subthy (swap p) then
- GREATER
- else
- (case int_ord (apply2 (length o Theory.ancestors_of) p) of
- EQUAL => string_ord (apply2 Context.theory_name p)
- | order => order)
+fun crude_thm_ord ctxt =
+ let
+ val ancestor_lengths =
+ fold (fn thy => Symtab.update (Context.theory_name thy, length (Context.ancestors_of thy)))
+ (Theory.nodes_of (Proof_Context.theory_of ctxt)) Symtab.empty
+ val ancestor_length = Symtab.lookup ancestor_lengths o Context.theory_id_name
+ fun crude_theory_ord p =
+ if Context.eq_thy_id p then EQUAL
+ else if Context.proper_subthy_id p then LESS
+ else if Context.proper_subthy_id (swap p) then GREATER
+ else
+ (case apply2 ancestor_length p of
+ (SOME m, SOME n) =>
+ (case int_ord (m, n) of
+ EQUAL => string_ord (apply2 Context.theory_id_name p)
+ | ord => ord)
+ | _ => string_ord (apply2 Context.theory_id_name p))
+ in
+ fn p =>
+ (case crude_theory_ord (apply2 Thm.theory_id_of_thm p) of
+ EQUAL =>
+ (* The hack below is necessary because of odd dependencies that are not reflected in the theory
+ comparison. *)
+ let val q = apply2 (nickname_of_thm ctxt) p in
+ (* Hack to put "xxx_def" before "xxxI" and "xxxE" *)
+ (case bool_ord (apply2 (String.isSuffix "_def") (swap q)) of
+ EQUAL => string_ord q
+ | ord => ord)
+ end
+ | ord => ord)
+ end;
-fun crude_thm_ord ctxt p =
- (case crude_theory_ord (apply2 Thm.theory_of_thm p) of
- EQUAL =>
- (* The hack below is necessary because of odd dependencies that are not reflected in the theory
- comparison. *)
- let val q = apply2 (nickname_of_thm ctxt) p in
- (* Hack to put "xxx_def" before "xxxI" and "xxxE" *)
- (case bool_ord (apply2 (String.isSuffix "_def") (swap q)) of
- EQUAL => string_ord q
- | ord => ord)
- end
- | ord => ord)
-
-val thm_less_eq = Theory.subthy o apply2 Thm.theory_of_thm
+val thm_less_eq = Context.subthy_id o apply2 Thm.theory_id_of_thm
fun thm_less p = thm_less_eq p andalso not (thm_less_eq (swap p))
val freezeT = Type.legacy_freeze_type
@@ -1110,12 +1119,11 @@
find_maxes Symtab.empty ([], Graph.maximals G)
end
-fun strict_subthy thyp = Theory.subthy thyp andalso not (Theory.subthy (swap thyp))
-
fun maximal_wrt_access_graph _ _ [] = []
| maximal_wrt_access_graph ctxt access_G ((fact as (_, th)) :: facts) =
- let val thy = Thm.theory_of_thm th in
- fact :: filter_out (fn (_, th') => strict_subthy (Thm.theory_of_thm th', thy)) facts
+ let val thy_id = Thm.theory_id_of_thm th in
+ fact :: filter_out (fn (_, th') =>
+ Context.proper_subthy_id (Thm.theory_id_of_thm th', thy_id)) facts
|> map (nickname_of_thm ctxt o snd)
|> maximal_wrt_graph access_G
end
--- a/src/Pure/Isar/code.ML Sun Aug 16 17:11:31 2015 +0200
+++ b/src/Pure/Isar/code.ML Sun Aug 16 18:19:30 2015 +0200
@@ -339,7 +339,7 @@
val dataref = (snd o Code_Data.get) theory;
val (datatab, thy) = case Synchronized.value dataref
of SOME (datatab, thy) =>
- if Theory.eq_thy (theory, thy)
+ if Context.eq_thy (theory, thy)
then (datatab, thy)
else (Datatab.empty, theory)
| NONE => (Datatab.empty, theory)
--- a/src/Pure/Isar/proof.ML Sun Aug 16 17:11:31 2015 +0200
+++ b/src/Pure/Isar/proof.ML Sun Aug 16 18:19:30 2015 +0200
@@ -491,7 +491,7 @@
val thy = Proof_Context.theory_of ctxt;
val _ =
- Theory.subthy (Thm.theory_of_thm goal, thy) orelse
+ Context.subthy_id (Thm.theory_id_of_thm goal, Context.theory_id thy) orelse
error "Bad background theory of goal state";
val _ = Thm.no_prems goal orelse error (Proof_Display.string_of_goal ctxt goal);
--- a/src/Pure/Tools/thy_deps.ML Sun Aug 16 17:11:31 2015 +0200
+++ b/src/Pure/Tools/thy_deps.ML Sun Aug 16 18:19:30 2015 +0200
@@ -22,7 +22,7 @@
| gen_thy_deps prep_thy ctxt bounds =
let
val (upper, lower) = apply2 ((Option.map o map) (prep_thy ctxt)) bounds;
- val rel = Theory.subthy o swap;
+ val rel = Context.subthy o swap;
val pred =
(case upper of
SOME Bs => (fn thy => exists (fn B => rel (thy, B)) Bs)
@@ -38,7 +38,7 @@
val thy_deps =
gen_thy_deps (fn ctxt => fn thy =>
let val thy0 = Proof_Context.theory_of ctxt
- in if Theory.subthy (thy, thy0) then thy else raise THEORY ("Bad theory", [thy, thy0]) end);
+ in if Context.subthy (thy, thy0) then thy else raise THEORY ("Bad theory", [thy, thy0]) end);
val thy_deps_cmd = Graph_Display.display_graph oo gen_thy_deps Theory.check;
--- a/src/Pure/context.ML Sun Aug 16 17:11:31 2015 +0200
+++ b/src/Pure/context.ML Sun Aug 16 18:19:30 2015 +0200
@@ -34,7 +34,7 @@
type pretty
val parents_of: theory -> theory list
val ancestors_of: theory -> theory list
- val theory_name_id: theory_id -> string
+ val theory_id_name: theory_id -> string
val theory_name: theory -> string
val PureN: string
val display_names: theory -> string list
@@ -196,7 +196,7 @@
fun make_history name stage = {name = name, stage = stage};
fun make_ancestry parents ancestors = {parents = parents, ancestors = ancestors};
-val theory_name_id = #name o history_of_id;
+val theory_id_name = #name o history_of_id;
val theory_name = #name o history_of;
val parents_of = #parents o ancestry_of;
val ancestors_of = #ancestors o ancestry_of;
--- a/src/Pure/goal.ML Sun Aug 16 17:11:31 2015 +0200
+++ b/src/Pure/goal.ML Sun Aug 16 18:19:30 2015 +0200
@@ -209,7 +209,7 @@
| SOME st =>
let
val _ =
- Theory.subthy (Thm.theory_of_thm st, thy) orelse
+ Context.subthy_id (Thm.theory_id_of_thm st, Context.theory_id thy) orelse
err "Bad background theory of goal state";
val res =
(finish ctxt' st
--- a/src/Pure/more_thm.ML Sun Aug 16 17:11:31 2015 +0200
+++ b/src/Pure/more_thm.ML Sun Aug 16 18:19:30 2015 +0200
@@ -195,7 +195,7 @@
fun eq_thm_strict ths =
eq_thm ths andalso
let val (rep1, rep2) = apply2 Thm.rep_thm ths in
- Theory.eq_thy (#thy rep1, #thy rep2) andalso
+ Context.eq_thy (#thy rep1, #thy rep2) andalso
#maxidx rep1 = #maxidx rep2 andalso
#tags rep1 = #tags rep2
end;
--- a/src/Pure/theory.ML Sun Aug 16 17:11:31 2015 +0200
+++ b/src/Pure/theory.ML Sun Aug 16 18:19:30 2015 +0200
@@ -6,8 +6,6 @@
signature THEORY =
sig
- val eq_thy: theory * theory -> bool
- val subthy: theory * theory -> bool
val parents_of: theory -> theory list
val ancestors_of: theory -> theory list
val nodes_of: theory -> theory list
@@ -40,9 +38,6 @@
(** theory context operations **)
-val eq_thy = Context.eq_thy;
-val subthy = Context.subthy;
-
val parents_of = Context.parents_of;
val ancestors_of = Context.ancestors_of;
fun nodes_of thy = thy :: ancestors_of thy;
--- a/src/Pure/thm.ML Sun Aug 16 17:11:31 2015 +0200
+++ b/src/Pure/thm.ML Sun Aug 16 18:19:30 2015 +0200
@@ -71,6 +71,7 @@
val terms_of_tpairs: (term * term) list -> term list
val full_prop_of: thm -> term
val theory_of_thm: thm -> theory
+ val theory_id_of_thm: thm -> Context.theory_id
val theory_name_of_thm: thm -> string
val maxidx_of: thm -> int
val maxidx_thm: thm -> int -> int
@@ -206,10 +207,10 @@
let
val Cterm {thy, t, T, maxidx, sorts} = ct;
val _ =
- Theory.subthy (thy, thy') orelse
+ Context.subthy (thy, thy') orelse
raise CTERM ("transfer_cterm: not a super theory", [ct]);
in
- if Theory.eq_thy (thy, thy') then ct
+ if Context.eq_thy (thy, thy') then ct
else Cterm {thy = thy', t = t, T = T, maxidx = maxidx, sorts = sorts}
end;
@@ -400,7 +401,9 @@
(* basic components *)
val theory_of_thm = #thy o rep_thm;
-val theory_name_of_thm = Context.theory_name o #thy o rep_thm;
+val theory_id_of_thm = Context.theory_id o #thy o rep_thm;
+val theory_name_of_thm = Context.theory_id_name o theory_id_of_thm;
+
val maxidx_of = #maxidx o rep_thm;
fun maxidx_thm th i = Int.max (maxidx_of th, i);
val hyps_of = #hyps o rep_thm;
@@ -429,9 +432,9 @@
fun transfer thy' thm =
let
val Thm (der, {thy, tags, maxidx, shyps, hyps, tpairs, prop}) = thm;
- val _ = Theory.subthy (thy, thy') orelse raise THM ("transfer: not a super theory", 0, [thm]);
+ val _ = Context.subthy (thy, thy') orelse raise THM ("transfer: not a super theory", 0, [thm]);
in
- if Theory.eq_thy (thy, thy') then thm
+ if Context.eq_thy (thy, thy') then thm
else
Thm (der,
{thy = thy',
@@ -452,7 +455,7 @@
fun make_context NONE thy = Context.Theory thy
| make_context (SOME ctxt) thy =
- if Theory.subthy (thy, Proof_Context.theory_of ctxt) then Context.Proof ctxt
+ if Context.subthy (thy, Proof_Context.theory_of ctxt) then Context.Proof ctxt
else raise THEORY ("Bad context", [thy, Proof_Context.theory_of ctxt]);
(*explicit weakening: maps |- B to A |- B*)
@@ -572,7 +575,7 @@
fun err msg = raise THM ("future_result: " ^ msg, 0, [thm]);
val Thm (Deriv {promises, ...}, {thy, shyps, hyps, tpairs, prop, ...}) = thm;
- val _ = Theory.eq_thy (thy, orig_thy) orelse err "bad theory";
+ val _ = Context.eq_thy (thy, orig_thy) orelse err "bad theory";
val _ = prop aconv orig_prop orelse err "bad prop";
val _ = null tpairs orelse err "bad tpairs";
val _ = null hyps orelse err "bad hyps";