src/Pure/Thy/read.ML

moved call of store_theory to end of use t.thy; use t.ML;
use_thy now needs the exact theory name (capital/lower letters);
improved handling of incompletly read theories;
added function unlink_thy, removed function relations;
added reference variable delete_tmpfile;
removed some bugs

(*  Title:      Pure/Thy/read
    ID:         $Id$
    Author:     Sonia Mahjoub / Tobias Nipkow / L C Paulson
    Copyright   1993  TU Muenchen

Reading and writing the theory definition files.

For theory XXX, the  input file is called XXX.thy
                the output file is called .XXX.thy.ML
                and it then tries to read XXX.ML
*)

datatype thy_info = ThyInfo of {name: string, path: string,
                                children: string list,
                                thy_info: string option, ml_info: string option,
                                theory: Thm.theory option};

signature READTHY =
sig
  datatype basetype = Thy  of string
                    | File of string

  val loadpath       : string list ref
  val delete_tmpfiles: bool ref

  val use_thy        : string -> unit
  val update         : unit -> unit
  val time_use_thy   : string -> unit
  val unlink_thy     : string -> unit
  val base_on        : basetype list -> string -> Thm.theory
  val store_theory   : string -> Thm.theory -> unit
  val list_loaded    : unit -> thy_info list
  val set_loaded     : thy_info list -> unit
end;


functor ReadthyFUN (structure ThySyn: THYSYN) : READTHY =
struct

datatype basetype = Thy  of string
                  | File of string;

val loaded_thys = ref [ThyInfo {name = "Pure", path = "", children = [], 
                                thy_info = Some "", ml_info = Some "", 
                                theory = Some Thm.pure_thy}];

val loadpath = ref ["."];           (*default search path for theory files *)

val delete_tmpfiles = ref true;         (*remove temporary files after use *)

(*Make name of the output ML file for a theory *)
fun out_name thy = "." ^ thy ^ ".thy.ML";

(*Read a file specified by thy_file containing theory thy *)
fun read_thy thy thy_file =
    let val instream  = open_in thy_file;
        val outstream = open_out (out_name thy)
    in  output (outstream, ThySyn.read (explode(input(instream, 999999))));
        close_out outstream;
        close_in instream
    end;

fun file_exists file =
  let val instream = open_in file in close_in instream; true end
    handle Io _ => false;

(*Get thy_info for a loaded theory *)
fun get_thyinfo thy =
  let fun do_search (t :: loaded : thy_info list) =
            let val ThyInfo {name, ...} = t
            in if name = thy then Some t else do_search loaded end
        | do_search [] = None
  in do_search (!loaded_thys) end;

(*Replace an item by the result of make_change *)
fun change_thyinfo make_change =
  let fun search (t :: loaded) =
            let val ThyInfo {name, path, children, thy_info, ml_info,
                             theory} = t
                val (new_t, continue) = make_change name path children thy_info
                                                    ml_info theory
            in if continue then            
                 new_t :: (search loaded)
               else
                 new_t :: loaded
            end
        | search [] = []
  in loaded_thys := search (!loaded_thys) end;

(*Check if a theory was already loaded *)
fun already_loaded thy =
  let val t = get_thyinfo thy
  in if is_none t then false
     else let val ThyInfo {thy_info, ml_info, ...} = the t
          in if is_none thy_info orelse is_none ml_info then false 
             else true end
  end;

(*Check if a theory file has changed since its last use.
  Return a pair of boolean values for .thy and for .ML *)
fun thy_unchanged thy thy_file ml_file = 
  let val t = get_thyinfo thy
  in if is_some t then
       let val ThyInfo {thy_info, ml_info, ...} = the t
           val tn = is_none thy_info;
           val mn = is_none ml_info
       in if not tn andalso not mn then
              ((file_info thy_file = the thy_info), 
               (file_info ml_file = the ml_info))
          else if not tn andalso mn then (true, false)
          else (false, false)
       end
     else (false, false)
  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.*)
fun find_file "" name =
      let fun find_it (curr :: paths) =
                if file_exists (tack_on curr name) then
                    tack_on curr name
                else 
                    find_it paths
           | find_it [] = ""
      in find_it (!loadpath) end
  | find_file path name =
      if file_exists (tack_on path name) then tack_on path name
                                         else "";

(*Get absolute pathnames for a new or already loaded theory *)
fun get_filenames path name =
  let fun new_filename () =
        let val thyl = to_lower name;
            val found = find_file path (thyl ^ ".thy")
                        handle FILE_NOT_FOUND => "";
            val thy_file = if found = "" then "" else tack_on (pwd ()) found;
            val (thy_path, _) = split_filename thy_file;
            val found = find_file path (thyl ^ ".ML");
            val ml_file = if thy_file = ""
                          then if found = "" then "" else tack_on (pwd ()) found
                          else if file_exists (tack_on thy_path (thyl ^ ".ML"))
                          then tack_on thy_path (thyl ^ ".ML")
                          else ""
        in if thy_file = "" andalso ml_file = "" then
             error ("Could find no .thy or .ML file for theory " ^ name)
           else ();
           (thy_file, ml_file) 
        end;

      val thy = get_thyinfo name
  in if is_some thy then
       let val thyl = to_lower name;
           val ThyInfo {path = abs_path, ...} = the thy;
           val (thy_file, ml_file) = if abs_path = "" then new_filename ()
                                     else (find_file abs_path (thyl ^ ".thy"),
                                           find_file abs_path (thyl ^ ".ML"))
       in if thy_file = "" andalso ml_file = "" then
            (writeln ("Warning: File \"" ^ (tack_on path thyl)
                      ^ ".thy\"\ncontaining theory \"" ^ name
                      ^ "\" no longer exists.");
             new_filename ()
            )
          else (thy_file, ml_file)
       end
     else new_filename ()
  end;

(*Remove theory from all child lists in loaded_thys *)
fun unlink_thy thy =
  let fun remove name path children thy_info ml_info theory =
            (ThyInfo {name = name, path = path, children = children \ thy, 
                      thy_info = thy_info, ml_info = ml_info,
                      theory = theory}, true)
  in change_thyinfo remove end;

(*Remove a theory from loaded_thys *)
fun remove_thy thy =
  let fun remove (t :: ts) =
            let val ThyInfo {name, ...} = t
            in if name = thy then ts
                             else t :: (remove ts)
            end
        | remove [] = []
  in loaded_thys := remove (!loaded_thys) end;

(*Change thy_info and ml_info for an existent item *)
fun set_info thy_new ml_new thy =
  let fun change name path children thy_info ml_info theory =
        if name = thy then
            (ThyInfo {name = name, path = path, children = children,
                      thy_info = Some thy_new, ml_info = Some ml_new,
                      theory = theory}, false)
        else
            (ThyInfo {name = name, path = path, children = children,
                      thy_info = thy_info, ml_info = ml_info,
                      theory = theory}, true)
  in change_thyinfo change end;

(*Mark theory as changed since last read if it has been completly read *)
fun mark_outdated thy =
  if already_loaded thy then set_info "" "" thy
                        else ();

(*Read .thy and .ML files that haven't been read yet or have changed since 
  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, thy_name) = split_filename name;
        val thyl = to_lower thy_name;
        val (thy_file, ml_file) = get_filenames path thy_name;
        val (abs_path, _) = if thy_file = "" then split_filename ml_file
                            else split_filename thy_file;
        val (thy_uptodate, ml_uptodate) = thy_unchanged thy_name 
                                                        thy_file ml_file;

         (*Set absolute path for loaded theory *)
         fun set_path () =
           let fun change name path children thy_info ml_info theory =
                 if name = thy_name then            
                   (ThyInfo {name = name, path = abs_path, children = children,
                             thy_info = thy_info, ml_info = ml_info,
                             theory = theory}, false)
                 else
                   (ThyInfo {name = name, path = path, children = children,
                             thy_info = thy_info, ml_info = ml_info,
                             theory = theory}, true)
           in change_thyinfo change end;

         (*Mark all direct descendants of a theory as changed *)
         fun mark_children thy =
           let val ThyInfo {children, ...} = the (get_thyinfo thy)
           in if children <> [] then
                  (writeln ("The following children of theory " ^ (quote thy)
                            ^ " are now out-of-date: "
                            ^ (quote (space_implode "\",\"" children)));
                   seq mark_outdated children
                  )
              else ()
           end

    in if thy_uptodate andalso ml_uptodate then ()
       else
       (
         writeln ("Loading theory " ^ (quote name));
         if thy_uptodate orelse thy_file = "" then ()
         else (read_thy thyl thy_file;
               use (out_name thyl)
              );
         
         if ml_file = "" then () else use ml_file;

         let val outstream = open_out ".tmp.ML"
         in
             output (outstream, "store_theory " ^ quote thy_name ^ " "
                                ^ thy_name ^ ".thy;\n");
             close_out outstream 
         end;
         use ".tmp.ML";
         delete_file ".tmp.ML";

         (*Now set the correct info.*)
         set_info (file_info thy_file) (file_info ml_file) thy_name;
         set_path ();

         (*Mark theories that have to be reloaded.*)
         mark_children thy_name;

         if !delete_tmpfiles then delete_file (out_name thyl)
                            else ()
        )
    end;

fun time_use_thy tname = timeit(fn()=>
   (writeln("\n**** Starting Theory " ^ tname ^ " ****");  
    use_thy tname;
    writeln("\n**** Finished Theory " ^ tname ^ " ****"))
   );

(*Load all thy or ML files that have been changed and also
  all theories that depend on them *)
fun update () =
  let (*List theories in the order they have to be loaded *)
      fun load_order [] result = result
        | load_order thys result =
            let fun next_level (t :: ts) =
                      let val thy = get_thyinfo t
                      in if is_some thy then
                             let val ThyInfo {children, ...} = the thy
                             in children union (next_level ts)
                             end
                         else []
                      end
                  | next_level [] = [];
                  
                val children = next_level thys
            in load_order children ((result \\ children) @ children) end;

      fun reload_changed (t :: ts) =
            let val thy = get_thyinfo t;

                fun abspath () =
                  if is_some thy then
                    let val ThyInfo {path, ...} = the thy in path end
                  else "";

                val (thy_file, ml_file) = get_filenames (abspath ()) t;
                val (thy_uptodate, ml_uptodate) =
                        thy_unchanged t thy_file ml_file;
            in if thy_uptodate andalso ml_uptodate then ()
                                                   else use_thy t;
               reload_changed ts
            end
        | reload_changed [] = ();

     (*Remove all theories that are no descendants of Pure.
       If there are still children in the deleted theory's list
       schedule them for reloading *)
     fun collect_garbage not_garbage =
       let fun collect (t :: ts) =
                 let val ThyInfo {name, children, ...} = t
                 in if name mem not_garbage then collect ts
                    else (writeln("Theory \"" ^ name 
                           ^ "\" is no longer linked with Pure - removing it.");
                          remove_thy name;
                          seq mark_outdated children
                         )
                 end
             | collect [] = ()

       in collect (!loaded_thys) end

  in collect_garbage ("Pure" :: (load_order ["Pure"] []));
     reload_changed (load_order ["Pure"] [])
  end;

(*Merge theories to build a base for a new theory.
  Base members are only loaded if they are missing. *)
fun base_on bases child =
      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 [] = [];

          (*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 will 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 fun add (t :: loaded) =
                      let val ThyInfo {name, path, children,
                                       thy_info, ml_info, theory} = t
                      in if name = base then
                           ThyInfo {name = name, path = path,
                                    children = child ins children,
                                    thy_info = thy_info, ml_info = ml_info,
                                    theory = theory} :: loaded
                         else
                           t :: (add loaded)
                      end
                  | add [] =
                      [ThyInfo {name = base, path = "", children = [child], 
                                thy_info = None, ml_info = None, theory = None}]
            in loaded_thys := add (!loaded_thys) end;       

          (*Load a base theory if not already done
            and no cycle would be created *)
          fun load base =
              let val thy_present = 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_present then ()
                   else (writeln ("Autoloading theory " ^ (quote base)
                                  ^ " (used by " ^ (quote child) ^ ")");
                         use_thy base)
                  )
              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 merge_theories' parameter *)
            | 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);
          val (t :: ts) = if mergelist = [] then ["Pure"] else mergelist
                                               (*we have to return something *)
     in foldl Thm.merge_theories (get_theory t, map get_theory ts) end;

(*Change theory object for an existent item of loaded_thys 
  or create a new item *)
fun store_theory thy_name thy =
  let fun make_change (t :: loaded) =
            let val ThyInfo {name, path, children, thy_info, ml_info, ...} = t
            in if name = thy_name then            
                    ThyInfo {name = name, path = path, children = children,
                             thy_info = thy_info, ml_info = ml_info,
                             theory = Some thy} :: loaded
               else
                    t :: (make_change loaded)
            end
        | make_change [] =
            [ThyInfo {name = thy_name, path = "", children = [],
                      thy_info = Some "", ml_info = Some "",
                      theory = Some thy}]
  in loaded_thys := make_change (!loaded_thys) end;

(*Create a list of all theories loaded by this structure *)
fun list_loaded () = (!loaded_thys);

(*Change the list of loaded theories *)
fun set_loaded [] =
      loaded_thys := [ThyInfo {name = "Pure", path = "", children = [],
                      thy_info = Some "", ml_info = Some "",
                      theory = Some Thm.pure_thy}]
  | set_loaded ts =
      loaded_thys := ts;

end