--- a/src/Pure/Thy/thm_database.ML Wed Oct 04 12:57:50 1995 +0100
+++ b/src/Pure/Thy/thm_database.ML Wed Oct 04 12:59:52 1995 +0100
@@ -4,19 +4,28 @@
Copyright 1995 TU Muenchen
*)
+datatype thm_db_type =
+ ThmDB of {count: int,
+ thy_idx: (Sign.sg * (string list * int list)) list,
+ const_idx: ((int * (string * thm)) list) Symtab.table};
+ (*count: number of theorems in database (used as unique ID for next thm)
+ thy_idx: constants and IDs of theorems
+ indexed by the theory's signature they belong to
+ const_idx: named theorems tagged by numbers and
+ indexed by the constants they contain*)
+
signature THMDB =
sig
- type thm_db_type
-
- val thm_db: thm_db_type
+ val thm_db: thm_db_type ref
val store_thm_db: string * thm -> thm
+ val delete_thm_db: theory -> unit
val thms_containing: string list -> (string * thm) list
val findI: int -> (string * thm)list
val findEs: int -> (string * thm)list
val findE: int -> int -> (string * thm)list
end;
-functor ThmDBFUN(): THMDB =
+functor ThmDBFun(): THMDB =
struct
(*** ignore and top_const could be turned into functor-parameters, but are
@@ -29,13 +38,11 @@
fun top_const (_ $ t) = (case head_of t of Const(c,_) => Some c
| _ => None);
-type thm_db_type = (int * ((int * (string * thm)) list) Symtab.table) ref;
-
(*Symtab which associates a constant with a list of theorems that contain the
- constant (theorems are represented as numbers)*)
-val thm_db = ref (0,
- (Symtab.make ([] : (string * ((int * (string * thm)) list)) list)));
- (*number of next theorem and symtab containing theorems*)
+ constant (theorems are tagged with numbers)*)
+val thm_db = ref (ThmDB
+ {count = 0, thy_idx = []:(Sign.sg * (string list * int list)) list,
+ const_idx = Symtab.make ([]:(string * ((int * (string * thm)) list)) list)});
(*list all relevant constants a term contains*)
fun list_consts t =
@@ -49,43 +56,75 @@
(*store a theorem in database*)
fun store_thm_db (named_thm as (name, thm)) =
- let val {prop, hyps, ...} = rep_thm thm;
+ let val {prop, hyps, sign, ...} = rep_thm thm;
val consts = distinct (flat (map list_consts (prop :: hyps)));
- val (num, db) = !thm_db;
+ val ThmDB {count, thy_idx, const_idx} = !thm_db;
- val tagged_thm = (num + 1, named_thm);
+ fun update_thys [] = [(sign, (consts, [count]))]
+ | update_thys ((thy as (thy_sign, (thy_consts, thy_nums))) :: ts) =
+ if Sign.eq_sg (sign, thy_sign) then
+ (thy_sign, (thy_consts union consts, count :: thy_nums)) :: ts
+ else thy :: update_thys ts;
- fun update_db warned [] result = result
- | update_db warned (c :: cs) result =
+ val tagged_thm = (count, named_thm);
+
+ fun update_db _ [] result = Some result
+ | update_db checked (c :: cs) result =
let
val old_thms = Symtab.lookup_multi (result, c);
- val (duplicate, warned') =
- case find_first (fn (_, (n, _)) => n = name) old_thms of
- Some (_, (_, t)) =>
- if same_thm (t, thm) then (true, warned)
- else
- (if not warned then
- writeln ("Warning: Duplicate theorem name " ^
- quote name ^ " used in theorem database")
- else ();
- (false, true))
- | None => (false, warned);
- in update_db warned' cs
- (if duplicate then result
- else (Symtab.update ((c, tagged_thm :: old_thms), result)))
+ val duplicate =
+ if checked then false
+ else case find_first (fn (_, (n, _)) => n = name) old_thms of
+ Some (_, (_, t)) => eq_thm (t, thm)
+ | None => false
+ in if duplicate then
+ (writeln ("Warning: Theorem database already contains copy of\
+ \ theorem " ^ quote name);
+ None)
+ else update_db true
+ cs (Symtab.update ((c, tagged_thm :: old_thms), result))
end;
+
+ val const_idx' = update_db false consts const_idx;
in if consts = [] then writeln ("Warning: Theorem " ^ name ^
" cannot be stored in ThmDB\n\t because it \
\contains no or only ignored constants.")
- else ();
- thm_db := (num+1, update_db false consts db);
+ else if is_some const_idx' then
+ thm_db := ThmDB {count = count+1, thy_idx = update_thys thy_idx,
+ const_idx = the const_idx'}
+ else ();
thm
end;
-(*intersection of two descending theorem lists*)
+(*remove all theorems with given signature from database*)
+fun delete_thm_db thy =
+ let
+ val sign = sign_of thy;
+
+ val ThmDB {count, thy_idx, const_idx} = !thm_db;
+
+ fun update_thys [] result = (result, [], [])
+ | update_thys ((thy as (thy_sign, (thy_consts, thy_nums))) :: ts)
+ result =
+ if Sign.eq_sg (sign, thy_sign) then
+ (result @ ts, thy_consts, thy_nums)
+ else update_thys ts (thy :: result);
+
+ val (thy_idx', thy_consts, thy_nums) = update_thys thy_idx [];
+
+ fun update_db [] result = result
+ | update_db (c :: cs) result =
+ let val thms' = filter_out (fn (num, _) => num mem thy_nums)
+ (Symtab.lookup_multi (result, c));
+ in update_db cs (Symtab.update ((c, thms'), result)) end;
+ in thm_db := ThmDB {count = count, thy_idx = thy_idx',
+ const_idx = update_db thy_consts const_idx}
+ end;
+
+(*intersection of two theorem lists with descending tags*)
infix desc_inter;
fun ([] : (int*'a) list) desc_inter (ys : (int*'a) list) = []
| xs desc_inter [] = []
@@ -98,7 +137,9 @@
fun thms_containing constants =
let fun collect [] _ result = map snd result
| collect (c :: cs) first result =
- let val new_thms = Symtab.lookup_multi (snd (!thm_db), c);
+ let val ThmDB {const_idx, ...} = !thm_db;
+
+ val new_thms = Symtab.lookup_multi (const_idx, c);
in collect cs false (if first then new_thms
else (result desc_inter new_thms))
end;
@@ -152,22 +193,22 @@
val As = Logic.strip_assums_hyp gi
in map (fn A => subst_bounds(frees,A)) As end;
-fun select_match(obj,signobj,named_thms,extract) =
- let fun matches(prop,tsig) =
+fun select_match(obj, signobj, named_thms, extract) =
+ let fun matches(prop, tsig) =
case extract prop of
None => false
- | Some pat => Pattern.matches tsig (pat,obj);
+ | Some pat => Pattern.matches tsig (pat, obj);
- fun select((p as (_,thm))::named_thms,sels) =
- let val {prop,sign,...} = rep_thm thm
+ fun select((p as (_,thm))::named_thms, sels) =
+ let val {prop, sign, ...} = rep_thm thm
in select(named_thms,
- if Sign.subsig(sign,signobj) andalso
+ if Sign.subsig(sign, signobj) andalso
matches(prop,#tsig(Sign.rep_sg signobj))
then p::sels else sels)
end
| select([],sels) = sels
- in select(named_thms,[]) end;
+ in select(named_thms, []) end;
fun find_matching(prop,sign,index,extract) =
(case top_const prop of
--- a/src/Pure/Thy/thy_read.ML Wed Oct 04 12:57:50 1995 +0100
+++ b/src/Pure/Thy/thy_read.ML Wed Oct 04 12:59:52 1995 +0100
@@ -15,7 +15,8 @@
ml_time: string option,
theory: theory option,
thms: thm Symtab.table,
- thy_simps: thm list, ml_simps: thm list};
+ thy_ss: Simplifier.simpset option,
+ simpset: Simplifier.simpset option};
(*meaning of special values:
thy_time, ml_time = None theory file has not been read yet
= Some "" theory was read but has either been marked
@@ -52,12 +53,12 @@
-> unit
val get_thm: theory -> string -> thm
val thms_of: theory -> (string * thm) list
+ val simpset_of: string -> Simplifier.simpset
val print_theory: theory -> unit
end;
-functor ReadthyFUN(structure ThySyn: THY_SYN and ThmDB: THMDB
- and Simplifier: SIMPLIFIER): READTHY =
+functor ReadthyFun(structure ThySyn: THY_SYN and ThmDB: THMDB): READTHY =
struct
open ThmDB Simplifier;
@@ -71,18 +72,19 @@
thy_time = Some "", ml_time = Some "",
theory = Some proto_pure_thy,
thms = Symtab.null,
- thy_simps = [], ml_simps = []}),
+ thy_ss = None, simpset = None}),
("Pure", ThyInfo {path = "", children = [],
thy_time = Some "", ml_time = Some "",
theory = Some pure_thy,
thms = Symtab.null,
- thy_simps = [], ml_simps = []}),
+ thy_ss = None, simpset = None}),
("CPure", ThyInfo {path = "",
children = [],
thy_time = Some "", ml_time = Some "",
theory = Some cpure_thy,
thms = Symtab.null,
- thy_simps = [], ml_simps = []})]);
+ thy_ss = None, simpset = None})
+ ]);
val loadpath = ref ["."]; (*default search path for theory files *)
@@ -134,18 +136,23 @@
end
| None => (false, false)
-(*Get list of simplifiers defined in .thy and .ML file*)
-fun get_simps tname =
- case get_thyinfo tname of
- Some (ThyInfo {thy_simps, ml_simps, ...}) => (thy_simps, ml_simps)
- | None => ([], []);
-
(*Get all direct ancestors of a theory*)
fun get_parents child =
let fun has_child (tname, ThyInfo {children, theory, ...}) =
if child mem children then Some tname else None;
in mapfilter has_child (Symtab.dest (!loaded_thys)) end;
+(*Get all descendants of a theory list *)
+fun get_descendants [] = []
+ | get_descendants (t :: ts) =
+ let val tinfo = get_thyinfo t
+ in if is_some tinfo then
+ let val ThyInfo {children, ...} = the tinfo
+ in children union (get_descendants (children union ts))
+ end
+ else []
+ end;
+
(*Get theory object for a loaded theory *)
fun get_theory name =
let val ThyInfo {theory, ...} = the (get_thyinfo name)
@@ -213,10 +220,10 @@
(*Remove theory from all child lists in loaded_thys *)
fun unlink_thy tname =
let fun remove (ThyInfo {path, children, thy_time, ml_time, theory, thms,
- thy_simps, ml_simps}) =
+ thy_ss, simpset}) =
ThyInfo {path = path, children = children \ tname,
thy_time = thy_time, ml_time = ml_time, theory = theory,
- thms = thms, thy_simps = thy_simps, ml_simps = ml_simps}
+ thms = thms, thy_ss = thy_ss, simpset = simpset}
in loaded_thys := Symtab.map remove (!loaded_thys) end;
(*Remove a theory from loaded_thys *)
@@ -225,15 +232,18 @@
(Symtab.dest (!loaded_thys)));
(*Change thy_time and ml_time for an existent item *)
-fun set_info thy_time ml_time tname =
- let val ThyInfo {path, children, theory, thms, thy_simps, ml_simps, ...} =
- the (Symtab.lookup (!loaded_thys, tname));
- in loaded_thys := Symtab.update
- ((tname,
- ThyInfo {path = path, children = children, thy_time = thy_time,
- ml_time = ml_time, theory = theory, thms = thms,
- thy_simps = thy_simps, ml_simps = ml_simps}),
- !loaded_thys)
+fun set_info tname thy_time ml_time =
+ let val tinfo = case Symtab.lookup (!loaded_thys, tname) of
+ Some (ThyInfo {path, children, theory, thms, thy_ss, simpset,...}) =>
+ ThyInfo {path = path, children = children,
+ thy_time = thy_time, ml_time = ml_time,
+ theory = theory, thms = thms,
+ thy_ss = thy_ss, simpset = simpset}
+ | None => ThyInfo {path = "", children = [],
+ thy_time = thy_time, ml_time = ml_time,
+ theory = None, thms = Symtab.null,
+ thy_ss = None, simpset = None};
+ in loaded_thys := Symtab.update ((tname, tinfo), !loaded_thys)
end;
(*Mark theory as changed since last read if it has been completly read *)
@@ -241,9 +251,10 @@
let val t = get_thyinfo tname;
in if is_none t then ()
else let val ThyInfo {thy_time, ml_time, ...} = the t
- in set_info (if is_none thy_time then None else Some "")
+ in set_info tname
+ (if is_none thy_time then None else Some "")
(if is_none ml_time then None else Some "")
- tname
+
end
end;
@@ -259,20 +270,17 @@
val (abs_path, _) = if thy_file = "" then split_filename ml_file
else split_filename thy_file;
val (thy_uptodate, ml_uptodate) = thy_unchanged tname thy_file ml_file;
- val (thy_simps, ml_simps) = get_simps tname;
- val old_simps = ref [];
(*Set absolute path for loaded theory *)
fun set_path () =
- let val ThyInfo {children, thy_time, ml_time, theory, thms,
- thy_simps, ml_simps, ...} =
+ let val ThyInfo {children, thy_time, ml_time, theory, thms, thy_ss,
+ simpset, ...} =
the (Symtab.lookup (!loaded_thys, tname));
in loaded_thys := Symtab.update ((tname,
ThyInfo {path = abs_path, children = children,
thy_time = thy_time, ml_time = ml_time,
theory = theory, thms = thms,
- thy_simps = thy_simps,
- ml_simps = ml_simps}),
+ thy_ss = thy_ss, simpset = simpset}),
!loaded_thys)
end;
@@ -293,78 +301,91 @@
fun delete_thms () =
let
val tinfo = case get_thyinfo tname of
- Some (ThyInfo {path, children, thy_time, ml_time, theory,
- thy_simps, ml_simps, ...}) =>
- ThyInfo {path = path, children = children,
- thy_time = thy_time, ml_time = ml_time,
- theory = theory, thms = Symtab.null,
- thy_simps = thy_simps, ml_simps = ml_simps}
+ Some (ThyInfo {path, children, thy_time, ml_time, theory, thy_ss,
+ simpset, ...}) =>
+ ThyInfo {path = path, children = children,
+ thy_time = thy_time, ml_time = ml_time,
+ theory = theory, thms = Symtab.null,
+ thy_ss = thy_ss, simpset = simpset}
| None => ThyInfo {path = "", children = [],
thy_time = None, ml_time = None,
theory = None, thms = Symtab.null,
- thy_simps = [], ml_simps = []};
- in loaded_thys := Symtab.update ((tname, tinfo), !loaded_thys) end;
+ thy_ss = None, simpset = None};
- fun update_simps (new_thy_simps, new_ml_simps) =
- let val ThyInfo {path, children, thy_time, ml_time, theory, thms,
- thy_simps, ml_simps} = the (get_thyinfo tname);
+ val ThyInfo {theory, ...} = tinfo;
+ in loaded_thys := Symtab.update ((tname, tinfo), !loaded_thys);
+ case theory of
+ Some t => delete_thm_db t
+ | None => ()
+ end;
- val (thy_simps', ml_simps') =
- (if is_none new_thy_simps then thy_simps else the new_thy_simps,
- if is_none new_ml_simps then ml_simps else the new_ml_simps);
- in loaded_thys := Symtab.update ((tname,
- ThyInfo {path = path, children = children,
- thy_time = thy_time, ml_time = ml_time, theory = theory,
- thms = thms, thy_simps = thy_simps',
- ml_simps = ml_simps'}), !loaded_thys)
+ fun save_thy_ss () =
+ let val ThyInfo {path, children, thy_time, ml_time, theory, thms,
+ simpset, ...} = the (get_thyinfo tname);
+ in loaded_thys := Symtab.update
+ ((tname, ThyInfo {path = path, children = children,
+ thy_time = thy_time, ml_time = ml_time,
+ theory = theory, thms = thms,
+ thy_ss = Some (!Simplifier.simpset),
+ simpset = simpset}),
+ !loaded_thys)
+ end;
+
+ fun save_simpset () =
+ let val ThyInfo {path, children, thy_time, ml_time, theory, thms,
+ thy_ss, ...} = the (get_thyinfo tname);
+ in loaded_thys := Symtab.update
+ ((tname, ThyInfo {path = path, children = children,
+ thy_time = thy_time, ml_time = ml_time,
+ theory = theory, thms = thms,
+ thy_ss = thy_ss,
+ simpset = Some (!Simplifier.simpset)}),
+ !loaded_thys)
end;
in if thy_uptodate andalso ml_uptodate then ()
else
(
- delete_thms ();
-
- if thy_uptodate orelse thy_file = "" then
- (Delsimps ml_simps;
- old_simps := #simps(rep_ss (!simpset));
- update_simps (None, Some []))
+ if thy_file = "" then ()
+ else if thy_uptodate then
+ simpset := let val ThyInfo {thy_ss, ...} = the (get_thyinfo tname);
+ in the thy_ss end
else
(writeln ("Reading \"" ^ name ^ ".thy\"");
- Delsimps (thy_simps @ ml_simps);
- old_simps := #simps(rep_ss (!simpset));
- update_simps (Some [], Some []); (*clear simp lists in case use_thy
- encounters an EROR exception*)
+ delete_thms ();
read_thy tname thy_file;
use (out_name tname);
+ save_thy_ss ();
if not (!delete_tmpfiles) then ()
- else delete_file (out_name tname);
-
- update_simps
- (Some (gen_rems same_thm (#simps(rep_ss (!simpset)), !old_simps)),
- None);
- old_simps := #simps(rep_ss (!simpset))
+ else delete_file (out_name tname)
);
- set_info (Some (file_info thy_file)) None tname;
+ set_info tname (Some (file_info thy_file)) None;
(*mark thy_file as successfully loaded*)
if ml_file = "" then ()
- else
- (writeln ("Reading \"" ^ name ^ ".ML\"");
- use ml_file;
+ else (writeln ("Reading \"" ^ name ^ ".ML\"");
+ use ml_file);
+ save_simpset ();
+
+ (*Store theory again because it could have been redefined*)
+ use_string
+ ["val _ = store_theory (" ^ tname ^ ".thy, " ^ quote tname ^ ");"];
- update_simps (None,
- Some (gen_rems same_thm (#simps(rep_ss (!simpset)), !old_simps)))
- );
-
- use_string
- ["val _ = (store_theory (" ^ tname ^ ".thy, " ^ quote tname ^ ");\
- \map store_thm_db (axioms_of " ^ tname ^ ".thy));"];
- (*Store theory again because it could have been redefined*)
+ (*Store axioms of theory
+ (but only if it's not a copy of an older theory)*)
+ let val parents = get_parents tname;
+ val fst_thy = get_theory (hd parents);
+ val this_thy = get_theory tname;
+ val axioms =
+ if length parents = 1
+ andalso Sign.eq_sg (sign_of fst_thy, sign_of this_thy) then []
+ else axioms_of this_thy;
+ in map store_thm_db axioms end;
(*Now set the correct info*)
- set_info (Some (file_info thy_file)) (Some (file_info ml_file)) tname;
+ set_info tname (Some (file_info thy_file)) (Some (file_info ml_file));
set_path ();
(*Mark theories that have to be reloaded*)
@@ -416,117 +437,114 @@
(*Remove all theories that are no descendants of ProtoPure.
If there are still children in the deleted theory's list
schedule them for reloading *)
- fun collect_garbage not_garbage =
+ fun collect_garbage no_garbage =
let fun collect ((tname, ThyInfo {children, ...}) :: ts) =
- if tname mem not_garbage then collect ts
+ if tname mem no_garbage then collect ts
else (writeln ("Theory \"" ^ tname ^
"\" is no longer linked with ProtoPure - removing it.");
remove_thy tname;
seq mark_outdated children)
| collect [] = ()
-
in collect (Symtab.dest (!loaded_thys)) end;
in collect_garbage ("ProtoPure" :: (load_order ["ProtoPure"] []));
reload_changed (load_order ["Pure", "CPure"] [])
end;
(*Merge theories to build a base for a new theory.
- Base members are only loaded if they are missing. *)
+ Base members are only loaded if they are missing.*)
fun mk_base bases child mk_draft =
- let (*List all descendants of a theory list *)
- fun list_descendants (t :: ts) =
- let val tinfo = get_thyinfo t
- in if is_some tinfo then
- let val ThyInfo {children, ...} = the tinfo
- in children union (list_descendants (ts union children))
- end
- else []
- end
- | list_descendants [] = [];
+ let (*Show the cycle that would be created by add_child *)
+ fun show_cycle base =
+ let fun find_it result curr =
+ let val tinfo = get_thyinfo curr
+ in if base = curr then
+ error ("Cyclic dependency of theories: "
+ ^ child ^ "->" ^ base ^ result)
+ else if is_some tinfo then
+ let val ThyInfo {children, ...} = the tinfo
+ in seq (find_it ("->" ^ curr ^ result)) children
+ end
+ else ()
+ end
+ in find_it "" child end;
- (*Show the cycle that would be created by add_child *)
- fun show_cycle base =
- let fun find_it result curr =
- let val tinfo = get_thyinfo curr
- in if base = curr then
- error ("Cyclic dependency of theories: "
- ^ child ^ "->" ^ base ^ result)
- else if is_some tinfo then
- let val ThyInfo {children, ...} = the tinfo
- in seq (find_it ("->" ^ curr ^ result)) children
- end
- else ()
- end
- in find_it "" child end;
+ (*Check if a cycle would be created by add_child *)
+ fun find_cycle base =
+ if base mem (get_descendants [child]) then show_cycle base
+ else ();
- (*Check if a cycle would be created by add_child *)
- fun find_cycle base =
- if base mem (list_descendants [child]) then show_cycle base
- else ();
+ (*Add child to child list of base *)
+ fun add_child base =
+ let val tinfo =
+ case Symtab.lookup (!loaded_thys, base) of
+ Some (ThyInfo {path, children, thy_time, ml_time,
+ theory, thms, thy_ss, simpset}) =>
+ ThyInfo {path = path, children = child ins children,
+ thy_time = thy_time, ml_time = ml_time,
+ theory = theory, thms = thms,
+ thy_ss = thy_ss, simpset = simpset}
+ | None => ThyInfo {path = "", children = [child],
+ thy_time = None, ml_time = None,
+ theory = None, thms = Symtab.null,
+ thy_ss = None, simpset = None};
+ in loaded_thys := Symtab.update ((base, tinfo), !loaded_thys) end;
- (*Add child to child list of base *)
- fun add_child base =
- let val tinfo =
- case Symtab.lookup (!loaded_thys, base) of
- Some (ThyInfo {path, children, thy_time, ml_time,
- theory, thms, thy_simps, ml_simps}) =>
- ThyInfo {path = path, children = child ins children,
- thy_time = thy_time, ml_time = ml_time,
- theory = theory, thms = thms,
- thy_simps = thy_simps, ml_simps = ml_simps}
- | None => ThyInfo {path = "", children = [child],
- thy_time = None, ml_time = None,
- theory = None, thms = Symtab.null,
- thy_simps = [], ml_simps = []};
- in loaded_thys := Symtab.update ((base, tinfo), !loaded_thys) end;
+ (*Load a base theory if not already done
+ and no cycle would be created *)
+ fun load base =
+ let val thy_loaded = already_loaded base
+ (*test this before child is added *)
+ in
+ if child = base then
+ error ("Cyclic dependency of theories: " ^ child
+ ^ "->" ^ child)
+ else
+ (find_cycle base;
+ add_child base;
+ if thy_loaded then ()
+ else (writeln ("Autoloading theory " ^ (quote base)
+ ^ " (used by " ^ (quote child) ^ ")");
+ use_thy base)
+ )
+ end;
- (*Load a base theory if not already done
- and no cycle would be created *)
- fun load base =
- let val thy_loaded = already_loaded base
- (*test this before child is added *)
- in
- if child = base then
- error ("Cyclic dependency of theories: " ^ child
- ^ "->" ^ child)
- else
- (find_cycle base;
- add_child base;
- if thy_loaded then ()
- else (writeln ("Autoloading theory " ^ (quote base)
- ^ " (used by " ^ (quote child) ^ ")");
- use_thy base)
- )
- end;
+ (*Get simpset for a theory*)
+ fun get_simpset tname =
+ let val ThyInfo {simpset, ...} = the (get_thyinfo tname);
+ in simpset end;
- (*Load all needed files and make a list of all real theories *)
- fun load_base (Thy b :: bs) =
- (load b;
- b :: (load_base bs))
- | load_base (File b :: bs) =
- (load b;
- load_base bs) (*don't add it to mergelist *)
- | load_base [] = [];
+ (*Load all needed files and make a list of all real theories *)
+ fun load_base (Thy b :: bs) =
+ (load b;
+ b :: (load_base bs))
+ | load_base (File b :: bs) =
+ (load b;
+ load_base bs) (*don't add it to mergelist *)
+ | load_base [] = [];
- val mergelist = (unlink_thy child;
- load_base bases);
- in writeln ("Loading theory " ^ (quote child));
- merge_thy_list mk_draft (map get_theory mergelist) end;
+ val dummy = unlink_thy child;
+ val mergelist = load_base bases;
+
+ val base_thy = (writeln ("Loading theory " ^ (quote child));
+ merge_thy_list mk_draft (map get_theory mergelist));
+ in simpset := foldr merge_ss (mapfilter get_simpset mergelist, empty_ss);
+ base_thy
+ end;
(*Change theory object for an existent item of loaded_thys
- or create a new item; also store axioms in Thm database*)
+ or create a new item*)
fun store_theory (thy, tname) =
let val tinfo = case Symtab.lookup (!loaded_thys, tname) of
Some (ThyInfo {path, children, thy_time, ml_time, thms,
- thy_simps, ml_simps, ...}) =>
+ thy_ss, simpset, ...}) =>
ThyInfo {path = path, children = children,
thy_time = thy_time, ml_time = ml_time,
theory = Some thy, thms = thms,
- thy_simps = thy_simps, ml_simps = ml_simps}
+ thy_ss = thy_ss, simpset = simpset}
| None => ThyInfo {path = "", children = [],
thy_time = None, ml_time = None,
theory = Some thy, thms = Symtab.null,
- thy_simps = [], ml_simps = []};
+ thy_ss = None, simpset = None};
in loaded_thys := Symtab.update ((tname, tinfo), !loaded_thys)
end;
@@ -569,15 +587,15 @@
fun store_thm (name, thm) =
let
val (thy_name, ThyInfo {path, children, thy_time, ml_time, theory, thms,
- thy_simps, ml_simps}) =
+ thy_ss, simpset}) =
thyinfo_of_sign (#sign (rep_thm thm));
- val thms' = Symtab.update_new ((name, thm), thms)
+ val (thms', duplicate) = (Symtab.update_new ((name, thm), thms), false)
handle Symtab.DUPLICATE s =>
- (if same_thm (the (Symtab.lookup (thms, name)), thm) then
+ (if eq_thm (the (Symtab.lookup (thms, name)), thm) then
(writeln ("Warning: Theory database already contains copy of\
\ theorem " ^ quote name);
- thms)
+ (thms, true))
else error ("Duplicate theorem name " ^ quote s
^ " used in theory database"));
in
@@ -585,9 +603,9 @@
((thy_name, ThyInfo {path = path, children = children,
thy_time = thy_time, ml_time = ml_time,
theory = theory, thms = thms',
- thy_simps = thy_simps, ml_simps = ml_simps}),
+ thy_ss = thy_ss, simpset = simpset}),
!loaded_thys);
- store_thm_db (name, thm)
+ if duplicate then thm else store_thm_db (name, thm)
end;
(*Store result of proof in loaded_thys and as ML value*)
@@ -613,11 +631,11 @@
(* Retrieve theorems *)
(*Get all theorems belonging to a given theory*)
-fun thmtab_ofthy thy =
+fun thmtab_of_thy thy =
let val (_, ThyInfo {thms, ...}) = thyinfo_of_sign (sign_of thy);
in thms end;
-fun thmtab_ofname name =
+fun thmtab_of_name name =
let val ThyInfo {thms, ...} = the (get_thyinfo name);
in thms end;
@@ -628,7 +646,7 @@
| get [] ng searched =
get (ng \\ searched) [] searched
| get (t::ts) ng searched =
- (case Symtab.lookup (thmtab_ofname t, name) of
+ (case Symtab.lookup (thmtab_of_name t, name) of
Some thm => thm
| None => get ts (ng union (get_parents t)) (t::searched));
@@ -636,8 +654,15 @@
in get [tname] [] [] end;
(*Get stored theorems of a theory*)
-val thms_of = Symtab.dest o thmtab_ofthy;
+val thms_of = Symtab.dest o thmtab_of_thy;
+(*Get simpset of a theory*)
+fun simpset_of tname =
+ case get_thyinfo tname of
+ Some (ThyInfo {simpset, ...}) =>
+ if is_some simpset then the simpset
+ else error ("Simpset of theory " ^ tname ^ " has not been stored yet")
+ | None => error ("Theory " ^ tname ^ " not stored by loader");
(* print theory *)