author | ballarin |
Fri, 15 Apr 2005 12:00:00 +0200 | |
changeset 15735 | 953f188e16c6 |
parent 15734 | 56a807868e23 |
child 15736 | 1bb0399a9517 |
src/Provers/classical.ML | file | annotate | diff | comparison | revisions | |
src/Provers/simplifier.ML | file | annotate | diff | comparison | revisions | |
src/Pure/Isar/ROOT.ML | file | annotate | diff | comparison | revisions | |
src/Pure/Isar/delta_data.ML | file | annotate | diff | comparison | revisions | |
src/Pure/Isar/proof_context.ML | file | annotate | diff | comparison | revisions |
--- a/src/Provers/classical.ML Thu Apr 14 19:30:57 2005 +0200 +++ b/src/Provers/classical.ML Fri Apr 15 12:00:00 2005 +0200 @@ -902,33 +902,37 @@ context_cs ctxt (get_local_claset ctxt) (get_context_cs ctxt); (* added for delta_claset: 06/01/05 *) +(* CB: changed "delta clasets" to context data, + moved counter to here, it is no longer a ref *) structure DeltaClasetArgs = struct - val name = "delta_claset"; - type T = claset; - val empty = empty_cs; + val name = "Provers/delta_claset"; + type T = claset * int; + fun init _ = (empty_cs, 0) + fun print ctxt cs = (); end; -structure DeltaClaset = DeltaDataFun(DeltaClasetArgs); -val get_delta_claset = DeltaClaset.get; -val put_delta_claset = DeltaClaset.put; - -val get_new_thm_id = ProofContext.get_delta_count_incr; - +structure DeltaClasetData = ProofDataFun(DeltaClasetArgs); +val get_delta_claset = #1 o DeltaClasetData.get; +fun put_delta_claset cs = DeltaClasetData.map (fn (_, i) => (cs, i)); +fun delta_increment ctxt = + let val ctxt' = DeltaClasetData.map (fn (ss, i) => (ss, i+1)) ctxt + in (ctxt', #2 (DeltaClasetData.get ctxt')) + end; local fun rename_thm' (ctxt,thm) = - let val new_id = get_new_thm_id ctxt - val new_name = "anon_" ^ (string_of_int new_id) + let val (new_ctxt, new_id) = delta_increment ctxt + val new_name = "anon_cla_" ^ (string_of_int new_id) in - Thm.name_thm(new_name,thm) + (new_ctxt, Thm.name_thm(new_name,thm)) end; in (* rename thm if call_atp is true *) -fun rename_thm (ctxt,thm) = if (!Proof.call_atp) then rename_thm' (ctxt,thm) else thm; +fun rename_thm (ctxt,thm) = if (!Proof.call_atp) then rename_thm' (ctxt,thm) else (ctxt, thm); end @@ -955,62 +959,62 @@ (* when dest/elim/intro rules are added to local_claset, they are also added to delta_claset in ProofContext.context *) fun safe_dest_local (ctxt,th) = let val thm_name = Thm.name_of_thm th - val th' = if (thm_name = "") then rename_thm (ctxt,th) else th - val delta_cs = get_delta_claset ctxt + val (ctxt', th') = if (thm_name = "") then rename_thm (ctxt,th) else (ctxt, th) + val delta_cs = get_delta_claset ctxt' val new_dcs = delta_cs addSDs [th'] - val ctxt' = put_delta_claset new_dcs ctxt + val ctxt'' = put_delta_claset new_dcs ctxt' in - change_local_cs (op addSDs) (ctxt',th) + change_local_cs (op addSDs) (ctxt'',th) end; fun safe_elim_local (ctxt, th)= let val thm_name = Thm.name_of_thm th - val th' = if (thm_name = "") then rename_thm (ctxt,th) else th - val delta_cs = get_delta_claset ctxt + val (ctxt', th') = if (thm_name = "") then rename_thm (ctxt,th) else (ctxt, th) + val delta_cs = get_delta_claset ctxt' val new_dcs = delta_cs addSEs [th'] - val ctxt' = put_delta_claset new_dcs ctxt + val ctxt'' = put_delta_claset new_dcs ctxt' in - change_local_cs (op addSEs) (ctxt',th) + change_local_cs (op addSEs) (ctxt'',th) end; fun safe_intro_local (ctxt, th) = let val thm_name = Thm.name_of_thm th - val th' = if (thm_name = "") then rename_thm (ctxt,th) else th - val delta_cs = get_delta_claset ctxt + val (ctxt', th') = if (thm_name = "") then rename_thm (ctxt,th) else (ctxt, th) + val delta_cs = get_delta_claset ctxt' val new_dcs = delta_cs addSIs [th'] - val ctxt' = put_delta_claset new_dcs ctxt + val ctxt'' = put_delta_claset new_dcs ctxt' in - change_local_cs (op addSIs) (ctxt',th) + change_local_cs (op addSIs) (ctxt'',th) end; fun haz_dest_local (ctxt, th)= let val thm_name = Thm.name_of_thm th - val th' = if (thm_name = "") then rename_thm (ctxt,th)else th - val delta_cs = get_delta_claset ctxt + val (ctxt', th') = if (thm_name = "") then rename_thm (ctxt,th)else (ctxt, th) + val delta_cs = get_delta_claset ctxt' val new_dcs = delta_cs addDs [th'] - val ctxt' = put_delta_claset new_dcs ctxt + val ctxt'' = put_delta_claset new_dcs ctxt' in - change_local_cs (op addDs) (ctxt',th) + change_local_cs (op addDs) (ctxt'',th) end; fun haz_elim_local (ctxt,th) = let val thm_name = Thm.name_of_thm th - val th' = if (thm_name = "") then rename_thm (ctxt,th) else th - val delta_cs = get_delta_claset ctxt + val (ctxt', th') = if (thm_name = "") then rename_thm (ctxt,th) else (ctxt, th) + val delta_cs = get_delta_claset ctxt' val new_dcs = delta_cs addEs [th'] - val ctxt' = put_delta_claset new_dcs ctxt + val ctxt'' = put_delta_claset new_dcs ctxt' in - change_local_cs (op addEs) (ctxt',th) + change_local_cs (op addEs) (ctxt'',th) end; fun haz_intro_local (ctxt,th) = let val thm_name = Thm.name_of_thm th - val th' = if (thm_name = "") then rename_thm (ctxt,th) else th - val delta_cs = get_delta_claset ctxt + val (ctxt', th') = if (thm_name = "") then rename_thm (ctxt,th) else (ctxt, th) + val delta_cs = get_delta_claset ctxt' val new_dcs = delta_cs addIs [th'] - val ctxt' = put_delta_claset new_dcs ctxt + val ctxt'' = put_delta_claset new_dcs ctxt' in - change_local_cs (op addIs) (ctxt',th) + change_local_cs (op addIs) (ctxt'',th) end; @@ -1156,7 +1160,8 @@ (** theory setup **) -val setup = [GlobalClaset.init, LocalClaset.init, setup_attrs, setup_methods]; +val setup = [GlobalClaset.init, LocalClaset.init, DeltaClasetData.init, + setup_attrs, setup_methods];
--- a/src/Provers/simplifier.ML Thu Apr 14 19:30:57 2005 +0200 +++ b/src/Provers/simplifier.ML Fri Apr 15 12:00:00 2005 +0200 @@ -321,32 +321,38 @@ (* Jia: added DeltaSimpsetArgs and DeltaSimpset for delta_simpset also added methods to retrieve them. *) +(* CB: changed "delta simpsets" to context data, + moved counter to here, it is no longer a ref *) structure DeltaSimpsetArgs = struct - val name = "delta_simpset"; - type T = Thm.thm list; (*the type is thm list*) - val empty = []; + val name = "Provers/delta_simpset"; + type T = Thm.thm list * int; (*the type is thm list * int*) + fun init _ = ([], 0); + fun print ctxt thms = (); end; -structure DeltaSimpset = DeltaDataFun(DeltaSimpsetArgs); -val get_delta_simpset = DeltaSimpset.get; -val put_delta_simpset = DeltaSimpset.put; +structure DeltaSimpsetData = ProofDataFun(DeltaSimpsetArgs); -val get_new_thm_id = ProofContext.get_delta_count_incr; +val get_delta_simpset = #1 o DeltaSimpsetData.get; +fun put_delta_simpset ss = DeltaSimpsetData.map (fn (_, i) => (ss, i)); +fun delta_increment ctxt = + let val ctxt' = DeltaSimpsetData.map (fn (ss, i) => (ss, i+1)) ctxt + in (ctxt', #2 (DeltaSimpsetData.get ctxt')) + end; (* Jia: added to rename a local thm if necessary *) local fun rename_thm' (ctxt,thm) = - let val new_id = get_new_thm_id ctxt - val new_name = "anon_" ^ (string_of_int new_id) + let val (new_ctxt, new_id) = delta_increment ctxt + val new_name = "anon_simp_" ^ (string_of_int new_id) in - Thm.name_thm(new_name,thm) + (new_ctxt, Thm.name_thm(new_name,thm)) end; in -fun rename_thm (ctxt,thm) = if (!Proof.call_atp) then rename_thm' (ctxt,thm) else thm; +fun rename_thm (ctxt,thm) = if (!Proof.call_atp) then rename_thm' (ctxt,thm) else (ctxt, thm); end @@ -371,11 +377,12 @@ fun simp_add_local (ctxt,th) = let val delta_ss = get_delta_simpset ctxt val thm_name = Thm.name_of_thm th - val th' = if (thm_name = "") then rename_thm (ctxt,th) else th + val (ctxt', th') = + if (thm_name = "") then rename_thm (ctxt,th) else (ctxt, th) val new_dss = th'::delta_ss - val ctxt' = put_delta_simpset new_dss ctxt + val ctxt'' = put_delta_simpset new_dss ctxt' in - change_local_ss (op addsimps) (ctxt',th) + change_local_ss (op addsimps) (ctxt'',th) end; val simp_del_local = change_local_ss (op delsimps); @@ -523,7 +530,8 @@ (** theory setup **) -val setup = [GlobalSimpset.init, LocalSimpset.init, setup_attrs]; +val setup = [GlobalSimpset.init, LocalSimpset.init, DeltaSimpsetData.init, + setup_attrs]; fun method_setup mods = [setup_methods mods]; fun easy_setup reflect trivs =
--- a/src/Pure/Isar/ROOT.ML Thu Apr 14 19:30:57 2005 +0200 +++ b/src/Pure/Isar/ROOT.ML Fri Apr 15 12:00:00 2005 +0200 @@ -11,7 +11,6 @@ use "rule_cases.ML"; use "proof_context.ML"; use "proof_data.ML"; -use "delta_data.ML"; (*for delta_{claset,simpset}, part of SPASS interface*) use "context_rules.ML"; use "args.ML"; use "attrib.ML";
--- a/src/Pure/Isar/delta_data.ML Thu Apr 14 19:30:57 2005 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,48 +0,0 @@ -(* Author: Jia Meng, Cambridge University Computer Laboratory (06/01/05) - $Id$ - Copyright 2004 University of Cambridge - -Used for delta_simpset and delta_claset -*) - -signature DELTA_DATA_ARGS = -sig - val name: string - type T - val empty: T -end; - -signature DELTA_DATA = -sig - type T - val get: ProofContext.context -> T - val put: T -> ProofContext.context -> ProofContext.context -end; - -functor DeltaDataFun(Args: DELTA_DATA_ARGS): DELTA_DATA = -struct - -type T = Args.T; - -exception Data of T; - -val key = Args.name; - -fun get ctxt = - let val delta_tab = ProofContext.get_delta ctxt - val delta_data = Symtab.lookup(delta_tab,key) - in - case delta_data of (SOME (Data d)) => d - | NONE => (Args.empty) - end; - -fun put delta_data ctxt = - let val delta_tab = ProofContext.get_delta ctxt - val new_tab = Symtab.update((key,Data delta_data),delta_tab) - in - ProofContext.put_delta new_tab ctxt - end; - -end; - -
--- 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));