# HG changeset patch # User wenzelm # Date 769357856 -7200 # Node ID e960fe156cd8ea15afac99d2dc3cdb6de0fe3d1b # Parent b074205ac50adee95f75794f7730338d8d9fbd75 (was Thy/read.ML) minor changes to accomodate new ThyScan and ThyParse; diff -r b074205ac50a -r e960fe156cd8 src/Pure/Thy/thy_read.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/Thy/thy_read.ML Thu May 19 16:30:56 1994 +0200 @@ -0,0 +1,456 @@ +(* Title: Pure/Thy/thy_read.ML + 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 THY_READ = +sig + datatype basetype = Thy of string + | File of string + + val loaded_thys : thy_info list ref + 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 +end; + + +functor ThyReadFun(structure ThyParse: THY_PARSE): THY_READ = +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 + open ThyParse; + val instream = open_in thy_file; + val outstream = open_out (out_name thy); + in + output (outstream, parse_thy pure_syntax (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 make_absolute file = + if file = "" then "" else + if hd (explode file) = "/" then file else tack_on (pwd ()) file; + + fun new_filename () = + let val found = find_file path (name ^ ".thy") + handle FILE_NOT_FOUND => ""; + val thy_file = make_absolute found; + val (thy_path, _) = split_filename thy_file; + val found = find_file path (name ^ ".ML"); + val ml_file = if thy_file = "" then make_absolute 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 (!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 thy = get_thyinfo name + in if is_some thy andalso path = "" then + let val ThyInfo {path = abs_path, ...} = the thy; + 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 + (writeln ("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 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 (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) + val loaded = filter already_loaded children + in if loaded <> [] then + (writeln ("The following children of theory " ^ (quote thy) + ^ " are now out-of-date: " + ^ (quote (space_implode "\",\"" loaded))); + seq mark_outdated loaded + ) + else () + end + + in if thy_uptodate andalso ml_uptodate then () + else + ( + if thy_uptodate orelse thy_file = "" then () + else (writeln ("Reading \"" ^ name ^ ".thy\""); + read_thy thy_name thy_file; + use (out_name thy_name) + ); + + if ml_file = "" then () + else (writeln ("Reading \"" ^ name ^ ".ML\""); + use ml_file); + + use_string ("store_theory " ^ quote thy_name ^ " " + ^ thy_name ^ ".thy"); + + (*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; + + (*Remove temporary files*) + if not (!delete_tmpfiles) orelse (thy_file = "") orelse thy_uptodate + then () + else delete_file (out_name thy_name) + ) + 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 next_level ts + 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 writeln ("Loading theory " ^ (quote child)); + 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; + +end; +