# HG changeset patch # User wenzelm # Date 918058855 -3600 # Node ID 27a94d4a8c15c2f651fedf1eb1d697b42be192cc # Parent aca4aca5a040dc56346fa22059484d99414a888d nuked; diff -r aca4aca5a040 -r 27a94d4a8c15 src/Pure/Thy/thy_read.ML --- a/src/Pure/Thy/thy_read.ML Wed Feb 03 17:20:35 1999 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,478 +0,0 @@ -(* 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 - - (* Additions for Proof General by David Aspinall *) - val use_thy_no_topml : string -> unit - val get_thy_filenames : string -> string -> string * string - val update_verbose : bool ref -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 = File.tmp_name (tname ^ "_thy.ML"); - - -(*Read a file specified by thy_file containing theory tname*) -fun read_thy tname thy_file = - let - val intext = File.read thy_file; - val outext = ThySyn.parse tname intext; - in - File.write (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_filenames1 give_error_if_none_found 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 - (if give_error_if_none_found then error else warning) - ("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; - -val get_filenames = get_filenames1 true; - -val get_thy_filenames = get_filenames1 false; - - -(*Remove theory from all child lists in loaded_thys *) -fun unlink_thy tname = - let fun remove ({path, children, parents, thy_time, ml_time, theory}) = - {path = path, children = children \ tname, parents = parents, - thy_time = thy_time, ml_time = ml_time, theory = theory} - 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, thy_time = _, ml_time = _}) => - {path = path, children = children, parents = parents, - thy_time = thy_time, ml_time = ml_time, theory = theory} - | 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. - no_mlfile is a flag which indicates that the ml file for this theory - should not be read, used to implement use_thy_no_topml. -*) -fun use_thy1 no_mlfile 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 {path = _, children, parents, thy_time, ml_time, theory} = - 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}), - !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 - - (*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}; - in if is_some (get_thyinfo tname) then () - else loaded_thys := Symtab.update ((tname, tinfo), !loaded_thys) - end - fun read_thy_file() = - if thy_file = "" then () - else - (writeln ("Reading \"" ^ name ^ ".thy\""); - init_thyinfo (); - read_thy tname thy_file; - Use.use (out_name tname); - if not (!delete_tmpfiles) then () - else OS.FileSys.remove (out_name tname); - thyfile2html tname abs_path) - - (*Add theory to list of all loaded theories (for index.html) - and it to its parents' sub-charts*) - fun add_theory path = - if path = "" then (*first time theory has been read*) - (mk_html tname abs_path old_parents; - mk_graph tname abs_path) (*Add it to graph definition file*) - else () - in if thy_uptodate andalso ml_uptodate then () - else - (read_thy_file(); - set_info tname (Some (file_info thy_file)) None; - (*mark thy_file as successfully loaded*) - - if (no_mlfile orelse ml_file = "") then () - else (writeln ("Reading \"" ^ name ^ ".ML\""); - Use.use ml_file); - - (*Store theory again because it could have been redefined*) - use_text false ("val _ = store_theory " ^ tname ^ ".thy;"); - - add_theory (path_of tname); - - (*Now set the correct info*) - set_info tname (Some (file_info thy_file)) (Some (file_info ml_file)); - set_path (); - mark_children tname; (*Mark theories that have to be reloaded*) - close_html () ) - end; - - -val use_thy = use_thy1 false false; -val use_thy_no_topml = use_thy1 true false; - - -fun time_use_thy tname = timeit(fn()=> - (writeln("\n**** Starting Theory " ^ tname ^ " ****"); - setmp Goals.proof_timing true use_thy tname; - writeln("\n**** Finished Theory " ^ tname ^ " ****")) - ); - - -val update_verbose = ref false; - -(*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 - (if !update_verbose then - (writeln - ("Not reading \"" ^ thy_file ^ - "\" (unchanged)" ^ - (if ml_file <> "" - then "\nNot reading \"" ^ ml_file ^ - "\" (unchanged)" - else ""))) - else ()) - 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}) => - {path = path, - children = child ins children, parents = parents, - thy_time = thy_time, ml_time = ml_time, - theory = theory} - | None => {path = "", children = [child], parents = [], - thy_time = None, ml_time = None, - theory = None}; - 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 ^ ")"); - (* autoloaded theories always use .ML files too *) - use_thy1 false 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 ThyInfo.theory mergelist)); - - val dummy = - let val tinfo = case Symtab.lookup (!loaded_thys, child) of - Some ({path, children, parents = _, thy_time, ml_time, theory}) => - {path = path, children = children, parents = mergelist, - thy_time = thy_time, ml_time = ml_time, theory = theory} - | None => sys_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.use; - val exit_use_dir = gen_use_dir Use.exit_use; - -end - -end;