src/Pure/Thy/thy_read.ML

debugging concerning sort variables
theorems are now proved immediately after generating the syntax

(*  Title:      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.
*)

signature THY_READ =
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 time_use_thy   : string -> unit
  val use_dir        : string -> unit
  val exit_use_dir   : string -> unit
  val update         : unit -> unit
  val unlink_thy     : string -> unit
  val mk_base        : basetype list -> string -> theory
end;


structure ThyRead: THY_READ =
struct

open ThmDatabase ThyInfo BrowserInfo;


datatype basetype = Thy  of string
                  | File of string;


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


(*Directory given as parameter to use_thy. This is temporarily added to
  loadpath while the theory's ancestors are loaded.*)
val tmp_loadpath = ref [] : string list ref;


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

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


(*Read a file specified by thy_file containing theory tname*)
fun read_thy tname thy_file =
  let
    val intext = read_file thy_file;
    val outext = ThySyn.parse tname intext;
  in
    write_file (out_name tname) outext
  end;


(*Check if a theory was completly loaded *)
fun already_loaded thy =
  let val t = get_thyinfo thy
  in if is_none t then false
     else let val {thy_time, ml_time, ...} = the t
          in is_some thy_time andalso is_some ml_time 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 =
  case get_thyinfo thy of
      Some {thy_time, ml_time, ...} =>
       let val tn = is_none thy_time;
           val mn = is_none ml_time
       in if not tn andalso not mn then
            ((file_info thy_file = the thy_time),
             (file_info ml_file = the ml_time))
          else if not tn andalso mn then
            (file_info thy_file = the thy_time, false)
          else
            (false, false)
       end
    | None => (false, false)


(*Get all descendants of a theory list *)
fun get_descendants [] = []
  | get_descendants (t :: ts) =
      let val children = children_of t
      in children union (get_descendants (children union ts)) end;


(*Find a file using a list of paths if no absolute or relative path is
  specified.*)
fun find_file "" name =
      let fun find_it (cur :: paths) =
                if file_exists (tack_on cur name) then
                  (if cur = "." then name else tack_on cur name)
                else
                  find_it paths
           | find_it [] = ""
      in find_it (!tmp_loadpath @ !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 found = find_file path (name ^ ".thy");
            val absolute_path = absolute_path (OS.FileSys.getDir ());
            val thy_file = absolute_path found;
            val (thy_path, _) = split_filename thy_file;
            val found = find_file path (name ^ ".ML");
            val ml_file = if thy_file = "" then absolute_path found
                          else if file_exists (tack_on thy_path (name ^ ".ML"))
                          then tack_on thy_path (name ^ ".ML")
                          else "";
            val searched_dirs = if path = "" then (!tmp_loadpath @ !loadpath)
                                             else [path]
        in if thy_file = "" andalso ml_file = "" then
             error ("Could not find file \"" ^ name ^ ".thy\" or \""
                    ^ name ^ ".ML\" for theory \"" ^ name ^ "\"\n"
                    ^ "in the following directories: \"" ^
                    (space_implode "\", \"" searched_dirs) ^ "\"")
           else ();
           (thy_file, ml_file)
        end;

      val tinfo = get_thyinfo name;
  in if is_some tinfo andalso path = "" then
       let val {path = abs_path, ...} = the tinfo;
           val (thy_file, ml_file) = if abs_path = "" then new_filename ()
                                     else (find_file abs_path (name ^ ".thy"),
                                           find_file abs_path (name ^ ".ML"))
       in if thy_file = "" andalso ml_file = "" then
            (warning ("File \"" ^ (tack_on path name)
                      ^ ".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 tname =
  let fun remove ({path, children, parents, thy_time, ml_time,
                           theory, thms, methods, data}) =
        {path = path, children = children \ tname, parents = parents,
                 thy_time = thy_time, ml_time = ml_time, theory = theory, 
                 thms = thms, methods = methods, data = data}
  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 tname thy_time ml_time =
  let val tinfo = case Symtab.lookup (!loaded_thys, tname) of
          Some ({path, children, parents, theory, thms,
                         methods, data, ...}) =>
            {path = path, children = children, parents = parents,
                     thy_time = thy_time, ml_time = ml_time,
                     theory = theory, thms = thms,
                     methods = methods, data = data}
        | None => error ("set_info: theory " ^ tname ^ " not found");
  in loaded_thys := Symtab.update ((tname, tinfo), !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;
  in if is_none t then ()
     else
       let val {thy_time, ml_time, ...} = the t
       in set_info tname (if is_none thy_time then None else Some "")
                         (if is_none ml_time then None else Some "")
       end
  end;


(*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.
  tmp_loadpath is temporarily added to loadpath while the ancestors of a
  theory that the user specified as e.g. "ex/Nat" are loaded. Because of
  raised exceptions we cannot guarantee that it's value is always valid.
  Therefore this has to be assured by the first parameter of use_thy1 which
  is "true" if use_thy gets invoked by mk_base and "false" else.
*)
fun use_thy1 tmp_loadpath_valid name =
  let
    val (path, tname) = split_filename name;
    val dummy = (tmp_loadpath :=
      (if not tmp_loadpath_valid then (if path = "" then [] else [path])
       else !tmp_loadpath));
    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 old_parents = parents_of_name tname;

    (*Set absolute path for loaded theory *)
    fun set_path () =
      let val {children, parents, thy_time, ml_time, theory, thms,
                       methods, data, ...} =
            the (Symtab.lookup (!loaded_thys, tname));
      in loaded_thys := Symtab.update ((tname,
                          {path = abs_path,
                                   children = children, parents = parents,
                                   thy_time = thy_time, ml_time = ml_time,
                                   theory = theory, thms = thms,
                                   methods = methods, data = data}),
                          !loaded_thys)
      end;

    (*Mark all direct descendants of a theory as changed *)
    fun mark_children thy =
      let val children = children_of 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;

    (*Invoke every get method stored in the methods table and store result in
      data table*)
    fun save_data thy_only =
      let val {path, children, parents, thy_time, ml_time,
                       theory, thms, methods, data} = the (get_thyinfo tname);

          fun get_data [] data = data
            | get_data ((id, ThyMethods {get, ...}) :: ms) data =
                get_data ms (Symtab.update ((id, get ()), data));

          val new_data = get_data (Symtab.dest methods) Symtab.null;

          val data' = (if thy_only then new_data else fst data, new_data)
                      (* 2nd component must be up to date *)
      in loaded_thys := Symtab.update
           ((tname, {path = path,
                             children = children, parents = parents,
                             thy_time = thy_time, ml_time = ml_time,
                             theory = theory, thms = thms,
                             methods = methods, data = data'}),
            !loaded_thys)
      end;

    (*Make sure that loaded_thys contains an entry for tname*)
    fun init_thyinfo () =
    let val tinfo = {path = "", children = [], parents = [],
                             thy_time = None, ml_time = None,
                             theory = None, thms = Symtab.null,
                             methods = Symtab.null,
                             data = (Symtab.null, Symtab.null)};
    in if is_some (get_thyinfo tname) then ()
       else loaded_thys := Symtab.update ((tname, tinfo), !loaded_thys)
    end;
  in if thy_uptodate andalso ml_uptodate then ()
     else
      (if thy_file = "" then ()
       else
         (writeln ("Reading \"" ^ name ^ ".thy\"");

          init_thyinfo ();
          read_thy tname thy_file;
          SymbolInput.use (out_name tname);
          save_data true;

          if not (!delete_tmpfiles) then ()
          else OS.FileSys.remove (out_name tname);

          thyfile2html tname abs_path
         );
       
       set_info tname (Some (file_info thy_file)) None;
                                       (*mark thy_file as successfully loaded*)

       if ml_file = "" then ()
       else (writeln ("Reading \"" ^ name ^ ".ML\"");
             SymbolInput.use ml_file);
       save_data false;

       (*Store theory again because it could have been redefined*)
       use_strings
         ["val _ = store_theory (" ^ tname ^ ".thy, " ^ quote tname ^ ");"];

       (*Add theory to list of all loaded theories (for index.html)
         and add it to its parents' sub-charts*)
       let val path = path_of tname;
       in if path = "" then               (*first time theory has been read*)
          (
            (*Add theory to list of all loaded theories (for index.html)
              and add it to its parents' sub-charts*)
            mk_html tname abs_path old_parents;

            (*Add theory to graph definition file*)
            mk_graph tname abs_path
          )
          else ()
       end;

       (*Now set the correct info*)
       set_info tname (Some (file_info thy_file)) (Some (file_info ml_file));
       set_path ();

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

       (*Close HTML file*)
       close_html ()
      )
  end;


val use_thy = use_thy1 false;


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 in.*)
      fun load_order [] result = result
        | load_order thys result =
            let fun next_level [] = []
                  | next_level (t :: ts) =
                      let val children = children_of t
                      in children union (next_level ts) end;

                val descendants = next_level thys;
            in load_order descendants ((result \\ descendants) @ descendants)
            end;

      fun reload_changed (t :: ts) =
            let val abspath = case get_thyinfo t of
                                  Some ({path, ...}) => path
                                | None => "";

                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 ProtoPure.
       If there are still children in the deleted theory's list
       schedule them for reloading *)
     fun collect_garbage no_garbage =
       let fun collect ((tname, {children, ...}: thy_info) :: 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 tmp_loadpath := [];
     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.*)
fun mk_base bases child =
  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 {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 ();

      (*Add child to child list of base*)
      fun add_child base =
        let val tinfo =
              case Symtab.lookup (!loaded_thys, base) of
                  Some ({path, children, parents, thy_time, ml_time,
                           theory, thms, methods, data}) =>
                    {path = path,
                             children = child ins children, parents = parents,
                             thy_time = thy_time, ml_time = ml_time,
                             theory = theory, thms = thms,
                             methods = methods, data = data}
                | None => {path = "", children = [child], parents = [],
                                   thy_time = None, ml_time = None,
                                   theory = None, thms = Symtab.null,
                                   methods = Symtab.null,
                                   data = (Symtab.null, Symtab.null)};
        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
                              ^ " (required by " ^ quote child ^ ")");
                     use_thy1 true 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 mergelist *)
        | load_base [] = [];

      val dummy = unlink_thy child;
      val mergelist = load_base bases;

      val base_thy =
       (writeln ("Loading theory " ^ quote child);
         if null mergelist then ProtoPure.thy
         else Theory.prep_ext_merge (map theory_of mergelist));

      val datas =
        let fun get_data t =
              let val {data, ...} = the (get_thyinfo t)
              in snd data end;
        in map (Symtab.dest o get_data) mergelist end;

      val methods =
        let fun get_methods t =
              let val {methods, ...} = the (get_thyinfo t)
              in methods end;

            val ms = map get_methods mergelist;
        in if null ms then Symtab.null
           else foldl (Symtab.merge (fn (x,y) => true)) (hd ms, tl ms)
        end;

      (*merge two sorted association lists*)
      fun merge_two ([], d2) = d2
        | merge_two (d1, []) = d1
        | merge_two (l1 as ((p1 as (id1 : string, d1)) :: d1s),
                     l2 as ((p2 as (id2, d2)) :: d2s)) =
            if id1 < id2 then
              p1 :: merge_two (d1s, l2)
            else
              p2 :: merge_two (l1, d2s);

      (*Merge multiple occurence of data; also call put for each merged list*)
      fun merge_multi [] None = []
        | merge_multi [] (Some (id, ds)) =
            let val ThyMethods {merge, put, ...} =
                  the (Symtab.lookup (methods, id));
             in put (merge ds); [id] end
        | merge_multi ((id, d) :: ds) None = merge_multi ds (Some (id, [d]))
        | merge_multi ((id, d) :: ds) (Some (id2, d2s)) =
            if id = id2 then
              merge_multi ds (Some (id2, d :: d2s))
            else
              let val ThyMethods {merge, put, ...} =
                    the (Symtab.lookup (methods, id2));
              in put (merge d2s);
                 id2 :: merge_multi ds (Some (id, [d]))
              end;

      val merged =
        if null datas then []
        else merge_multi (foldl merge_two (hd datas, tl datas)) None;

      val dummy =
        let val unmerged = map fst (Symtab.dest methods) \\ merged;

            fun put_empty id =
              let val ThyMethods {merge, put, ...} =
                    the (Symtab.lookup (methods, id));
              in put (merge []) end;
        in seq put_empty unmerged end;

      val dummy =
        let val tinfo = case Symtab.lookup (!loaded_thys, child) of
              Some ({path, children, thy_time, ml_time, theory, thms,
                             data, ...}) =>
                 {path = path,
                          children = children, parents = mergelist,
                          thy_time = thy_time, ml_time = ml_time,
                          theory = theory, thms = thms,
                          methods = methods, data = data}
             | None => error ("set_parents: theory " ^ child ^ " not found");
        in loaded_thys := Symtab.update ((child, tinfo), !loaded_thys) end;

 in cur_thyname := child;
    base_thy
 end;


(*Temporarily enter a directory and load its ROOT.ML file;
  also do some work for HTML and graph generation*)
local

  fun gen_use_dir use_cmd dirname =
    let val old_dir = OS.FileSys.getDir ();
    in OS.FileSys.chDir dirname;
       if !make_html then init_html() else ();
       if !make_graph then init_graph dirname else ();
       use_cmd "ROOT.ML";
       finish_html();
       OS.FileSys.chDir old_dir
    end;

in

  val use_dir = gen_use_dir use;
  val exit_use_dir = gen_use_dir exit_use;

end

end;