--- a/src/Pure/Isar/proof_context.ML Thu Apr 14 19:30:57 2005 +0200
+++ b/src/Pure/Isar/proof_context.ML Fri Apr 15 12:00:00 2005 +0200
@@ -5,13 +5,6 @@
Proof context information.
*)
-(*Jia: changed: datatype context
- affected files: make_context, map_context, init, put_data, add_syntax, map_defaults, del_bind, upd_bind, qualified, hide_thms, put_thms, reset_thms, gen_assms, map_fixes, add_cases
-
- added: put_delta, get_delta
- 06/01/05
-*)
-
val show_structs = ref false;
signature PROOF_CONTEXT =
@@ -163,11 +156,6 @@
val thms_containing_limit: int ref
val print_thms_containing: context -> int option -> string list -> unit
val setup: (theory -> theory) list
-
- val get_delta: context -> Object.T Symtab.table (* Jia: (claset, simpset) *)
- val put_delta: Object.T Symtab.table -> context -> context
- val get_delta_count_incr: context -> int
-
end;
signature PRIVATE_PROOF_CONTEXT =
@@ -213,20 +201,17 @@
typ Vartab.table * (*type constraints*)
sort Vartab.table * (*default sorts*)
string list * (*used type variables*)
- term list Symtab.table,
- delta: Object.T Symtab.table (* difference between local and global claset and simpset*),
- delta_count: int ref (* number of local anonymous thms *)
-}; (*type variable occurrences*)
+ term list Symtab.table}; (*type variable occurrences*)
exception CONTEXT of string * context;
-fun make_context (thy, syntax, data, asms, binds, thms, cases, defs, delta, delta_count) =
+fun make_context (thy, syntax, data, asms, binds, thms, cases, defs) =
Context {thy = thy, syntax = syntax, data = data, asms = asms, binds = binds,
- thms = thms, cases = cases, defs = defs, delta = delta, delta_count = delta_count};
+ thms = thms, cases = cases, defs = defs};
-fun map_context f (Context {thy, syntax, data, asms, binds, thms, cases, defs, delta, delta_count}) =
- make_context (f (thy, syntax, data, asms, binds, thms, cases, defs, delta, delta_count));
+fun map_context f (Context {thy, syntax, data, asms, binds, thms, cases, defs}) =
+ make_context (f (thy, syntax, data, asms, binds, thms, cases, defs));
fun theory_of (Context {thy, ...}) = thy;
val sign_of = Theory.sign_of o theory_of;
@@ -324,30 +309,9 @@
fun put_data kind f x ctxt =
(lookup_data ctxt kind;
- map_context (fn (thy, syntax, data, asms, binds, thms, cases, defs, delta,delta_count) =>
+ map_context (fn (thy, syntax, data, asms, binds, thms, cases, defs) =>
(thy, syntax, Symtab.update ((Object.name_of_kind kind, f x), data),
- asms, binds, thms, cases, defs, delta, delta_count)) ctxt);
-
-
-(* added get_delta and put_delta *)
-
-fun get_delta (ctxt as Context {delta, ...}) = delta;
-
-fun get_delta_count (ctxt as Context {delta_count, ...}) = !delta_count;
-
-fun get_delta_count_incr (ctxt as Context {delta_count, ...}) =
- let val current_delta_count = !delta_count
- in
- (delta_count:=(!delta_count)+1;current_delta_count)
-end;
-
-fun incr_delta_count (ctxt as Context {delta_count, ...}) = (delta_count:=(!delta_count)+1);
-
-(* replace the old delta by new delta *)
-(* count not changed! *)
-fun put_delta new_delta ctxt =
- map_context (fn (thy, syntax, data, asms, binds, thms, cases, defs,delta, delta_count) =>
- (thy, syntax, data, asms, binds, thms, cases, defs, new_delta,delta_count)) ctxt;
+ asms, binds, thms, cases, defs)) ctxt);
(* init context *)
@@ -356,7 +320,7 @@
let val data = Symtab.map (fn (_, (f, _)) => f thy) (ProofDataData.get thy) in
make_context (thy, (Theory.syn_of thy, [], []), data, (([], []), []), Vartab.empty,
(false, NameSpace.empty, Symtab.empty, FactIndex.empty), [],
- (Vartab.empty, Vartab.empty, [], Symtab.empty), Symtab.empty, ref 0)
+ (Vartab.empty, Vartab.empty, [], Symtab.empty))
end;
@@ -410,7 +374,7 @@
in
fun add_syntax decls =
- map_context (fn (thy, (syn, structs, mixfixed), data, asms, binds, thms, cases, defs, delta, delta_count) =>
+ map_context (fn (thy, (syn, structs, mixfixed), data, asms, binds, thms, cases, defs) =>
let
val is_logtype = Sign.is_logtype (Theory.sign_of thy);
val structs' = structs @ List.mapPartial prep_struct decls;
@@ -421,7 +385,7 @@
|> Syntax.extend_const_gram is_logtype ("", false) mxs_output
|> Syntax.extend_const_gram is_logtype ("", true) mxs
|> Syntax.extend_trfuns ([], trs, [], []);
- in (thy, (syn', structs', fixed @ mixfixed), data, asms, binds, thms, cases, defs, delta, delta_count) end)
+ in (thy, (syn', structs', fixed @ mixfixed), data, asms, binds, thms, cases, defs) end)
fun syn_of (Context {syntax = (syn, structs, _), ...}) =
syn |> Syntax.extend_trfuns (Syntax.struct_trfuns structs);
@@ -718,8 +682,8 @@
SOME T => Vartab.update (((x, ~1), T), types)
| NONE => types));
-fun map_defaults f = map_context (fn (thy, syntax, data, asms, binds, thms, cases, defs, delta, delta_count) =>
- (thy, syntax, data, asms, binds, thms, cases, f defs, delta, delta_count));
+fun map_defaults f = map_context (fn (thy, syntax, data, asms, binds, thms, cases, defs) =>
+ (thy, syntax, data, asms, binds, thms, cases, f defs));
fun declare_syn (ctxt, t) =
ctxt
@@ -870,8 +834,8 @@
fun del_bind (ctxt, xi) =
ctxt
- |> map_context (fn (thy, syntax, data, asms, binds, thms, cases, defs, delta, delta_count) =>
- (thy, syntax, data, asms, Vartab.update ((xi, NONE), binds), thms, cases, defs, delta, delta_count));
+ |> map_context (fn (thy, syntax, data, asms, binds, thms, cases, defs) =>
+ (thy, syntax, data, asms, Vartab.update ((xi, NONE), binds), thms, cases, defs));
fun upd_bind (ctxt, ((x, i), t)) =
let
@@ -882,8 +846,8 @@
in
ctxt
|> declare_term t'
- |> map_context (fn (thy, syntax, data, asms, binds, thms, cases, defs, delta, delta_count) =>
- (thy, syntax, data, asms, Vartab.update (((x, i), SOME (t', T)), binds), thms, cases, defs, delta, delta_count))
+ |> map_context (fn (thy, syntax, data, asms, binds, thms, cases, defs) =>
+ (thy, syntax, data, asms, Vartab.update (((x, i), SOME (t', T)), binds), thms, cases, defs))
end;
fun del_upd_bind (ctxt, (xi, NONE)) = del_bind (ctxt, xi)
@@ -1049,27 +1013,27 @@
fun cond_extern (Context {thms = (_, space, _, _), ...}) = NameSpace.cond_extern space;
fun qualified q = map_context (fn (thy, syntax, data, asms, binds,
- (_, space, tab, index), cases, defs, delta, delta_count) =>
- (thy, syntax, data, asms, binds, (q, space, tab, index), cases, defs, delta, delta_count));
+ (_, space, tab, index), cases, defs) =>
+ (thy, syntax, data, asms, binds, (q, space, tab, index), cases, defs));
fun restore_qualified (Context {thms, ...}) = qualified (#1 thms);
fun hide_thms fully names =
- map_context (fn (thy, syntax, data, asms, binds, (q, space, tab, index), cases, defs, delta, delta_count) =>
+ map_context (fn (thy, syntax, data, asms, binds, (q, space, tab, index), cases, defs) =>
(thy, syntax, data, asms, binds, (q, NameSpace.hide fully (space, names), tab, index),
- cases, defs, delta, delta_count));
+ cases, defs));
(* put_thm(s) *)
fun gen_put_thms _ _ ("", _) ctxt = ctxt
| gen_put_thms override_q acc (name, ths) ctxt = ctxt |> map_context
- (fn (thy, syntax, data, asms, binds, (q, space, tab, index), cases, defs, delta, delta_count) =>
+ (fn (thy, syntax, data, asms, binds, (q, space, tab, index), cases, defs) =>
if not override_q andalso not q andalso NameSpace.is_qualified name then
raise CONTEXT ("Attempt to declare qualified name " ^ quote name, ctxt)
else (thy, syntax, data, asms, binds, (q, NameSpace.extend' acc (space, [name]),
Symtab.update ((name, SOME ths), tab),
- FactIndex.add (is_known ctxt) (index, (name, ths))), cases, defs, delta, delta_count));
+ FactIndex.add (is_known ctxt) (index, (name, ths))), cases, defs));
fun gen_put_thm q acc (name, th) = gen_put_thms q acc (name, [th]);
@@ -1084,9 +1048,9 @@
(* reset_thms *)
fun reset_thms name =
- map_context (fn (thy, syntax, data, asms, binds, (q, space, tab, index), cases, defs, delta, delta_count) =>
+ map_context (fn (thy, syntax, data, asms, binds, (q, space, tab, index), cases, defs) =>
(thy, syntax, data, asms, binds, (q, space, Symtab.update ((name, NONE), tab), index),
- cases, defs, delta,delta_count));
+ cases, defs));
(* note_thmss *)
@@ -1189,9 +1153,9 @@
val asmss = map #2 results;
val thmss = map #3 results;
val ctxt3 = ctxt2 |> map_context
- (fn (thy, syntax, data, ((asms_ct, asms_th), fixes), binds, thms, cases, defs, delta, delta_count) =>
+ (fn (thy, syntax, data, ((asms_ct, asms_th), fixes), binds, thms, cases, defs) =>
(thy, syntax, data, ((asms_ct @ [(cprops, exp)], asms_th @ asmss), fixes), binds, thms,
- cases, defs, delta, delta_count));
+ cases, defs));
val ctxt4 = ctxt3 |> put_thms ("prems", prems_of ctxt3);
in (warn_extra_tfrees ctxt ctxt4, thmss) end;
@@ -1237,8 +1201,8 @@
local
fun map_fixes f =
- map_context (fn (thy, syntax, data, (assumes, fixes), binds, thms, cases, defs, delta, delta_count) =>
- (thy, syntax, data, (assumes, f fixes), binds, thms, cases, defs, delta, delta_count));
+ map_context (fn (thy, syntax, data, (assumes, fixes), binds, thms, cases, defs) =>
+ (thy, syntax, data, (assumes, f fixes), binds, thms, cases, defs));
fun err_dups ctxt xs = raise CONTEXT ("Duplicate variable(s): " ^ commas_quote xs, ctxt);
@@ -1330,8 +1294,8 @@
| SOME c => prep_case ctxt name xs c);
-fun add_cases xs = map_context (fn (thy, syntax, data, asms, binds, thms, cases, defs, delta, delta_count) =>
- (thy, syntax, data, asms, binds, thms, rev (filter_out (equal "" o #1) xs) @ cases, defs, delta, delta_count));
+fun add_cases xs = map_context (fn (thy, syntax, data, asms, binds, thms, cases, defs) =>
+ (thy, syntax, data, asms, binds, thms, rev (filter_out (equal "" o #1) xs) @ cases, defs));