# HG changeset patch # User clasohm # Date 809954934 -7200 # Node ID b3f68a64438012d738fd8b2f61449ae08a1ad02e # Parent bfc93c86f0a147100559e99cc5bd58486485c604 added cleanup of global simpset to thy_read; replaced error by warning for duplicate names in theorem database diff -r bfc93c86f0a1 -r b3f68a644380 src/Pure/Thy/ROOT.ML --- a/src/Pure/Thy/ROOT.ML Fri Sep 01 13:27:48 1995 +0200 +++ b/src/Pure/Thy/ROOT.ML Fri Sep 01 13:28:54 1995 +0200 @@ -15,11 +15,14 @@ use "thy_syn.ML"; use "thm_database.ML"; +use "../../Provers/simplifier.ML"; use "thy_read.ML"; structure ThySyn = ThySynFun(val user_keywords = [] and user_sections = []); -structure ThmDB = ThmDBFun(); -structure Readthy = ReadthyFUN(structure ThySyn = ThySyn and ThmDB = ThmDB); +structure ThmDB = ThmDBFUN(); +structure Simplifier = SimplifierFUN(); +structure Readthy = ReadthyFUN(structure ThySyn = ThySyn and ThmDB = ThmDB + and Simplifier = Simplifier); open ThmDB Readthy; (* hide functors; saves space in PolyML *) @@ -28,9 +31,11 @@ fun init_thy_reader () = use_string - ["structure ThmDB = ThmDBFun();", + ["structure ThmDB = ThmDBFUN();", + "structure Simplifier = SimplifierFUN();", "structure Readthy = ReadthyFUN(structure ThySyn = ThySyn \ - \and ThmDB = ThmDB);", + \and ThmDB = ThmDB \ + \and Simplifier = Simplifier);", "Readthy.loaded_thys := !loaded_thys;", "ThmDB.thm_db := !thm_db;", "val first_init_readthy = false;", diff -r bfc93c86f0a1 -r b3f68a644380 src/Pure/Thy/thm_database.ML --- a/src/Pure/Thy/thm_database.ML Fri Sep 01 13:27:48 1995 +0200 +++ b/src/Pure/Thy/thm_database.ML Fri Sep 01 13:28:54 1995 +0200 @@ -16,7 +16,7 @@ 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 @@ -57,32 +57,29 @@ val tagged_thm = (num + 1, named_thm); - fun update_db _ [] result = result - | update_db warned (c :: cs) result = + fun update_db [] result = result + | update_db (c :: cs) result = let val old_thms = Symtab.lookup_multi (result, c); - val warned' = + val duplicate = case find_first (fn (_, (n, _)) => n = name) old_thms of Some (_, (_, t)) => - if eq_thm (t, thm) then - (if not warned then - writeln ("Warning: Theorem database already \ - \contains copy of theorem " ^ quote name) - else (); - true) - else error ("Duplicate theorem name " ^ quote name - ^ " used in theorem database") - | None => warned; - in update_db warned' cs - (if warned' then result + if same_thm (t, thm) then true + else + (writeln ("Warning: Duplicate theorem name " + ^ quote name ^ " used in theorem database"); + false) + | None => false; + in update_db cs + (if duplicate then result else (Symtab.update ((c, tagged_thm :: old_thms), result))) end; 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); + thm_db := (num+1, update_db consts db); thm end; diff -r bfc93c86f0a1 -r b3f68a644380 src/Pure/Thy/thy_read.ML --- a/src/Pure/Thy/thy_read.ML Fri Sep 01 13:27:48 1995 +0200 +++ b/src/Pure/Thy/thy_read.ML Fri Sep 01 13:28:54 1995 +0200 @@ -4,8 +4,8 @@ Tobias Nipkow and L C Paulson Copyright 1994 TU Muenchen -Functions for reading theory files, and storing and retrieving theories -and theorems. +Functions for reading theory files, and storing and retrieving theories, +theorems and the global simplifier set. *) (*Type for theory storage*) @@ -14,7 +14,8 @@ thy_time: string option, ml_time: string option, theory: theory option, - thms: thm Symtab.table}; + thms: thm Symtab.table, + thy_simps: thm list, ml_simps: thm list}; (*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 @@ -55,9 +56,11 @@ end; -functor ReadthyFUN(structure ThySyn: THY_SYN and ThmDB: THMDB): READTHY = +functor ReadthyFUN(structure ThySyn: THY_SYN and ThmDB: THMDB + and Simplifier: SIMPLIFIER): READTHY = struct -local open ThmDB in + +open ThmDB Simplifier; datatype basetype = Thy of string | File of string; @@ -67,16 +70,19 @@ children = ["Pure", "CPure"], thy_time = Some "", ml_time = Some "", theory = Some proto_pure_thy, - thms = Symtab.null}), + thms = Symtab.null, + thy_simps = [], ml_simps = []}), ("Pure", ThyInfo {path = "", children = [], thy_time = Some "", ml_time = Some "", theory = Some pure_thy, - thms = Symtab.null}), + thms = Symtab.null, + thy_simps = [], ml_simps = []}), ("CPure", ThyInfo {path = "", children = [], thy_time = Some "", ml_time = Some "", theory = Some cpure_thy, - thms = Symtab.null})]); + thms = Symtab.null, + thy_simps = [], ml_simps = []})]); val loadpath = ref ["."]; (*default search path for theory files *) @@ -128,6 +134,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 theory object for a loaded theory *) +fun get_theory name = + let val ThyInfo {theory, ...} = the (get_thyinfo name) + in the theory end; + exception FILE_NOT_FOUND; (*raised by find_file *) (*Find a file using a list of paths if no absolute or relative path is @@ -189,10 +212,11 @@ (*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}) = + let fun remove (ThyInfo {path, children, thy_time, ml_time, theory, thms, + thy_simps, ml_simps}) = ThyInfo {path = path, children = children \ tname, - thy_time = thy_time, ml_time = ml_time, - theory = theory, thms = thms} + thy_time = thy_time, ml_time = ml_time, theory = theory, + thms = thms, thy_simps = thy_simps, ml_simps = ml_simps} in loaded_thys := Symtab.map remove (!loaded_thys) end; (*Remove a theory from loaded_thys *) @@ -202,12 +226,14 @@ (*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, ...} = + 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}), !loaded_thys) + 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) end; (*Mark theory as changed since last read if it has been completly read *) @@ -227,81 +253,134 @@ completly been read by this and preceeding use_thy calls. If a theory changed since its last use its children are marked as changed *) fun use_thy name = - let val (path, tname) = split_filename name; - val (thy_file, ml_file) = get_filenames path tname; - 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; + let + val (path, tname) = split_filename name; + val (thy_file, ml_file) = get_filenames path tname; + 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, ...} = - 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}), - !loaded_thys) - end; + (*Set absolute path for loaded theory *) + fun set_path () = + let val ThyInfo {children, thy_time, ml_time, theory, thms, + thy_simps, ml_simps, ...} = + 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}), + !loaded_thys) + end; + + (*Mark all direct descendants of a theory as changed *) + fun mark_children thy = + let val ThyInfo {children, ...} = the (get_thyinfo thy); + val present = filter (is_some o get_thyinfo) children; + val loaded = filter already_loaded present; + in if loaded <> [] then + writeln ("The following children of theory " ^ (quote thy) + ^ " are now out-of-date: " + ^ (quote (space_implode "\",\"" loaded))) + else (); + seq mark_outdated present + end; - (*Mark all direct descendants of a theory as changed *) - fun mark_children thy = - let val ThyInfo {children, ...} = the (get_thyinfo thy); - val present = filter (is_some o get_thyinfo) children; - val loaded = filter already_loaded present; - in if loaded <> [] then - writeln ("The following children of theory " ^ (quote thy) - ^ " are now out-of-date: " - ^ (quote (space_implode "\",\"" loaded))) - else (); - seq mark_outdated present - end; + (*Remove theorems associated with a theory*) + 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} + | 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; + + 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); - (*Remove all theorems associated with a theory*) - fun delete_thms () = - let val tinfo = case Symtab.lookup (!loaded_thys, tname) of - Some (ThyInfo {path, children, thy_time, ml_time, theory, ...}) => - ThyInfo {path = path, children = children, - thy_time = thy_time, ml_time = ml_time, - theory = theory, thms = Symtab.null} - | None => ThyInfo {path = "", children = [], - thy_time = None, ml_time = None, - theory = None, thms = Symtab.null}; - in loaded_thys := Symtab.update ((tname, tinfo), !loaded_thys) end; - in if thy_uptodate andalso ml_uptodate then () + 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) + 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 [])) else - ( - delete_thms (); + (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*) + read_thy tname thy_file; + use (out_name tname); - if thy_uptodate orelse thy_file = "" then () - else (writeln ("Reading \"" ^ name ^ ".thy\""); - read_thy tname thy_file; - use (out_name tname); + if not (!delete_tmpfiles) then () + else delete_file (out_name tname); - if not (!delete_tmpfiles) then () - else delete_file (out_name tname) - ); - set_info (Some (file_info thy_file)) None tname; + update_simps + (Some (gen_rems same_thm (#simps(rep_ss (!simpset)), !old_simps)), + None); + old_simps := #simps(rep_ss (!simpset)) + ); + + set_info (Some (file_info thy_file)) None tname; (*mark thy_file as successfully loaded*) - if ml_file = "" then () - else (writeln ("Reading \"" ^ name ^ ".ML\""); - use ml_file); + if ml_file = "" then () + else + (writeln ("Reading \"" ^ name ^ ".ML\""); + use ml_file; - 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*) + update_simps (None, + Some (gen_rems same_thm (#simps(rep_ss (!simpset)), !old_simps))) + ); + + (*Store theory again because it could have been redefined*) + use_string + ["val _ = (store_theory (" ^ tname ^ ".thy, " ^ quote tname ^ "); " ^ - (*Now set the correct info*) - set_info (Some (file_info thy_file)) (Some (file_info ml_file)) tname; - set_path (); + (*Store new axioms in theorem database; ignore theories which are just + copies of existing ones*) + let val parents = get_parents tname; + val fst_thy = get_theory (hd parents); + val this_thy = get_theory tname; + in if length parents = 1 + andalso Sign.eq_sg (sign_of fst_thy, sign_of this_thy) then "" + else + "map store_thm_db (axioms_of " ^ tname ^ ".thy));" + end]; - (*Mark theories that have to be reloaded*) - mark_children tname - ) - end; + (*Now set the correct info*) + set_info (Some (file_info thy_file)) (Some (file_info ml_file)) tname; + set_path (); + + (*Mark theories that have to be reloaded*) + mark_children tname + ) + end; fun time_use_thy tname = timeit(fn()=> (writeln("\n**** Starting Theory " ^ tname ^ " ****"); @@ -400,13 +479,15 @@ let val tinfo = case Symtab.lookup (!loaded_thys, base) of Some (ThyInfo {path, children, thy_time, ml_time, - theory, thms}) => + 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} + 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}; + 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 @@ -437,11 +518,6 @@ load_base bs) (*don't add it to mergelist *) | load_base [] = []; - (*Get theory object for a loaded theory *) - fun get_theory name = - let val ThyInfo {theory, ...} = the (get_thyinfo name) - in the theory end; - val mergelist = (unlink_thy child; load_base bases); in writeln ("Loading theory " ^ (quote child)); @@ -451,13 +527,16 @@ or create a new item; also store axioms in Thm database*) fun store_theory (thy, tname) = let val tinfo = case Symtab.lookup (!loaded_thys, tname) of - Some (ThyInfo {path, children, thy_time, ml_time, thms, ...}) => + Some (ThyInfo {path, children, thy_time, ml_time, thms, + thy_simps, ml_simps, ...}) => ThyInfo {path = path, children = children, thy_time = thy_time, ml_time = ml_time, - theory = Some thy, thms = thms} + theory = Some thy, thms = thms, + thy_simps = thy_simps, ml_simps = ml_simps} | None => ThyInfo {path = "", children = [], thy_time = None, ml_time = None, - theory = Some thy, thms = Symtab.null}; + theory = Some thy, thms = Symtab.null, + thy_simps = [], ml_simps = []}; in loaded_thys := Symtab.update ((tname, tinfo), !loaded_thys) end; @@ -499,12 +578,13 @@ (*Store a theorem in the thy_info of its theory*) fun store_thm (name, thm) = let - val (thy_name, ThyInfo {path, children, thy_time, ml_time, theory, thms}) = + val (thy_name, ThyInfo {path, children, thy_time, ml_time, theory, thms, + thy_simps, ml_simps}) = thyinfo_of_sign (#sign (rep_thm thm)); val thms' = Symtab.update_new ((name, thm), thms) handle Symtab.DUPLICATE s => - (if eq_thm (the (Symtab.lookup (thms, name)), thm) then + (if same_thm (the (Symtab.lookup (thms, name)), thm) then (writeln ("Warning: Theory database already contains copy of\ \ theorem " ^ quote name); thms) @@ -513,8 +593,10 @@ in loaded_thys := Symtab.update ((thy_name, ThyInfo {path = path, children = children, - thy_time = thy_time, ml_time = ml_time, theory = theory, thms = thms'}), - ! loaded_thys); + thy_time = thy_time, ml_time = ml_time, + theory = theory, thms = thms', + thy_simps = thy_simps, ml_simps = ml_simps}), + !loaded_thys); store_thm_db (name, thm) end; @@ -540,12 +622,6 @@ (* Retrieve theorems *) -(*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 theorems belonging to a given theory*) fun thmtab_ofthy thy = let val (_, ThyInfo {thms, ...}) = thyinfo_of_sign (sign_of thy); @@ -586,5 +662,4 @@ fun print_theory thy = (Drule.print_theory thy; print_thms thy); -end end;