# HG changeset patch # User clasohm # Date 812807992 -3600 # Node ID 8f40ff1299d814d5dad44d4506b5eec0b727450c # Parent af4107a031500e1a445b532d3f8415f49491e6f3 added removal of theorems if theory is to be reloaded; changed functions for local simpsets diff -r af4107a03150 -r 8f40ff1299d8 src/Pure/Thy/thm_database.ML --- 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 diff -r af4107a03150 -r 8f40ff1299d8 src/Pure/Thy/thy_read.ML --- 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 *)