src/Pure/Thy/thy_read.ML

     ID:         $Id$
     Author:     Carsten Clasohm and Markus Wenzel and Sonia Mahjoub and
                 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*)
 datatype thy_info = ThyInfo of {path: string,
                                 children: string list,
                                 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
                                      as outdated or there is no such file for
                                      this theory (see e.g. 'virtual' theories

   val thms_of: theory -> (string * thm) list
   val print_theory: theory -> unit
 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;
 
 val loaded_thys = ref (Symtab.make [("ProtoPure",
                                      ThyInfo {path = "",
                                        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 *)
 
 val delete_tmpfiles = ref true;         (*remove temporary files after use *)
 

             (file_info thy_file = the thy_time, false)
           else
             (false, false)
        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
   specified.*)

      else new_filename ()
   end;
 
 (*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 *)
 fun remove_thy tname =
   loaded_thys := Symtab.make (filter_out (fn (id, _) => id = tname)
                  (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, ...} =
+  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 *)
 fun mark_outdated tname =
   let val t = get_thyinfo tname;

   they were last read;
   loaded_thys is a thy_info list ref containing all theories that have
   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;
-
-         (*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;
-
-         (*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 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 ()
+  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,
+                       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;
+
+    (*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);
+
+          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 ();
-
-         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)
-              );
-         set_info (Some (file_info thy_file)) None tname;
+         (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 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))
+         );
+
+       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);
-
-         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*)
-
-         (*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;
+       if ml_file = "" then ()
+       else
+         (writeln ("Reading \"" ^ name ^ ".ML\"");
+          use ml_file;
+
+          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 ^ "); " ^
+
+       (*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];
+
+       (*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 ^ " ****");
     use_thy tname;
     writeln("\n**** Finished Theory " ^ tname ^ " ****"))

           (*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}) =>
+                                     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
             and no cycle would be created *)
           fun load base =

             | load_base (File b :: bs) =
                (load b;
                 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));
         merge_thy_list mk_draft (map get_theory mergelist) end;
 
 (*Change theory object for an existent item of loaded_thys
   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;
 
 
 (** store and retrieve theorems **)

 (* Store theorems *)
 
 (*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)
          else error ("Duplicate theorem name " ^ quote s
                      ^ " used in theory database"));
   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;
 
 (*Store result of proof in loaded_thys and as ML value*)
 

   (qed_thm := prove_goalw thy rths agoal tacsf;
    use_string ["val " ^ name ^ " = store_thm (" ^ quote name ^", !qed_thm);"]);
 
 
 (* 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);
   in thms end;

     Pretty.writeln (Pretty.big_list "stored theorems:" (map prt_thm thms))
   end;
 
 fun print_theory thy = (Drule.print_theory thy; print_thms thy);
 
-end
 end;