--- 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 *)