# HG changeset patch # User clasohm # Date 751293771 -3600 # Node ID 208ab8773a7320926803bd36bc2476355f74955a # Parent 075db6ac7f2f379851d654241b6e75bf84e722c8 changes in Readthy: - reads needed base theories automatically - keeps a time stamp for all read files - update function - checks for cycles - path list that is searched for files - reads theories that are created in .ML files - etc. diff -r 075db6ac7f2f -r 208ab8773a73 src/Pure/Thy/ROOT.ML --- a/src/Pure/Thy/ROOT.ML Fri Oct 22 13:39:23 1993 +0100 +++ b/src/Pure/Thy/ROOT.ML Fri Oct 22 13:42:51 1993 +0100 @@ -26,6 +26,11 @@ structure Lex = LexicalFUN (Keyword); structure Parse = ParseFUN (Lex); structure ThySyn = ThySynFUN (Parse); -structure Readthy = ReadthyFUN (ThySyn); +(*This structure is only defined to be compatible with older versions of + READTHY. Don't use it in newly created theory/ROOT.ML files! Instead + define a new structure. Otherwise Poly/ML won't save a reference variable + defined inside the functor. *) +structure Readthy = ReadthyFUN (structure ThySyn = ThySyn); open Readthy; + diff -r 075db6ac7f2f -r 208ab8773a73 src/Pure/Thy/read.ML --- a/src/Pure/Thy/read.ML Fri Oct 22 13:39:23 1993 +0100 +++ b/src/Pure/Thy/read.ML Fri Oct 22 13:42:51 1993 +0100 @@ -12,27 +12,40 @@ signature READTHY = sig - val split_filename : string -> string * string + type thy_info + + val use_thy : string -> unit + val update : unit -> unit val time_use_thy : string -> unit - val use_thy : string -> unit + val base_on : string 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 + val set_loadpath : string list -> unit + val relations : string -> unit end; -functor ReadthyFUN (ThySyn: THYSYN): READTHY = +functor ReadthyFUN (structure ThySyn: THYSYN) : READTHY = struct -(*Convert Unix filename of the form path/file to "path/" and "file" ; - if filename contains no slash, then it returns "" and "file" *) -fun split_filename name = - let val (file,path) = take_prefix (apr(op<>,"/")) (rev (explode name)) - in (implode(rev path), implode(rev file)) end; +datatype thy_info = ThyInfo of {name: string, childs: string list, + thy_info: string, ml_info: string, + theory: Thm.theory}; -(*create name of the output ML file for the theory*) +val loaded_thys = ref [ThyInfo {name = "pure", childs = [], thy_info = "", + ml_info = "", theory = Thm.pure_thy}]; + +val loadpath = ref ["."]; + + +(*Make name of the output ML file for a theory *) fun out_name thy = "." ^ thy ^ ".thy.ML"; -fun read_thy path thy = - let val instream = open_in (path ^ thy ^ ".thy") - val outstream = open_out (path ^ out_name thy) +(*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 @@ -42,20 +55,314 @@ let val instream = open_in file in close_in instream; true end handle Io _ => false; -(*Use the file if it exists*) -fun try_use file = - if file_exists file then use file else (); +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 [] = raise FILE_NOT_FOUND + in find_it (!loadpath) end + | find_file path name = + if file_exists (tack_on path name) then tack_on path name + else raise FILE_NOT_FOUND; + +(*Use the file if it exists *) +fun try_use file = + if file_exists file then use file else (); + +(*Check if a theory was already loaded *) +fun already_loaded thy = + let fun do_search ((ThyInfo {name, ...}) :: loaded) = + if name = thy then true else do_search loaded + | do_search [] = false + in do_search (!loaded_thys) end; + +(*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 t else do_search loaded end + | do_search [] = error ("Internal error (get_thyinfo): theory " + ^ thy ^ " not found.") + in do_search (!loaded_thys) 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 = + if already_loaded thy then + let val ThyInfo {thy_info, ml_info, ...} = get_thyinfo thy; + in ((file_info (thy_file) = thy_info), (file_info (ml_file) = ml_info)) + end + else (false, false); + +(*Get theory object for a loaded theory *) +fun get_theory name = + let val ThyInfo {theory, ...} = get_thyinfo name + in theory 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. + If a theory changed since its last use its childs are marked as changed *) +fun use_thy name = + let val (path, thy_name) = split_filename name; + val thy = to_lower thy_name; + val thy_file = (find_file path (thy ^ ".thy") + handle FILE_NOT_FOUND => ""); + val (thy_path, _) = split_filename thy_file; + val ml_file = if thy_file = "" + then (find_file path (thy ^ ".ML") + handle FILE_NOT_FOUND => + error ("Could find no .thy or .ML file for theory " + ^ name)) + else if file_exists (thy_path ^ thy ^ ".ML") + then thy_path ^ thy ^ ".ML" + else "" + val (thy_uptodate, ml_uptodate) = thy_unchanged thy thy_file ml_file; -(*Read and convert the theory to a .XXX.thy.ML file and also try to read XXX.ML*) -fun use_thy name = - let val (path,thy) = split_filename name - in read_thy path thy; - use (path ^ out_name thy); - try_use (path ^ thy ^ ".ML") + (*Remove theory from all child lists in loaded_thys. + Afterwards add_child should be called for the (new) base theories *) + fun remove_child thy = + let fun do_remove (ThyInfo {name, childs, thy_info, ml_info, theory} + :: loaded) result = + do_remove loaded + (ThyInfo {name = name, childs = childs \ thy, + thy_info = thy_info, ml_info = ml_info, + theory = theory} :: result) + | do_remove [] result = result; + in loaded_thys := do_remove (!loaded_thys) [] end; + + exception THY_NOT_FOUND; (*Raised by set_info *) + + (*Change thy_info and ml_info for an existent item or create + a new item with empty child list *) + fun set_info thy_new ml_new thy = + let fun make_change (t :: loaded) = + let val ThyInfo {name, childs, theory, ...} = t + in if name = thy then + ThyInfo {name = name, childs = childs, + thy_info = thy_new, ml_info = ml_new, + theory = theory} :: loaded + else + t :: (make_change loaded) + end + | make_change [] = raise THY_NOT_FOUND + in loaded_thys := make_change (!loaded_thys) end; + + (*Mark all direct and indirect descendants of a theory as changed *) + fun mark_childs thy = + let val ThyInfo {childs, ...} = get_thyinfo thy + in writeln ("Marking childs of modified theory " ^ thy ^ " (" ^ + (space_implode "," childs) ^ ")"); + seq (set_info "" "") childs + handle THY_NOT_FOUND => () + (*If this theory was automatically loaded by a child + then the child cannot be found in loaded_thys *) + end + + in if thy_uptodate andalso ml_uptodate then () + else + ( + writeln ("Loading theory " ^ name); + if thy_uptodate orelse (thy_file = "") then () + else + ( + (*Allow dependency lists to be rebuild completely *) + remove_child thy; + + read_thy thy thy_file + ); + + (*Actually read files!*) + if thy_uptodate orelse (thy_file = "") then () + else use (out_name thy); + if (thy_file = "") then (*theory object created in .ML file*) + ( + use ml_file; + let val outstream = open_out (".tmp.ML") + in + output (outstream, "store_theory " ^ quote name ^ " " ^ name + ^ ".thy;\n"); + close_out outstream + end; + use ".tmp.ML"; + delete_file ".tmp.ML" + ) + else try_use ml_file; + + (*Now set the correct info.*) + (set_info (file_info thy_file) (file_info ml_file) thy + handle THY_NOT_FOUND => error ("Could not find theory \"" ^ name + ^ "\" (wrong filename?)")); + + (*Mark theories that have to be reloaded.*) + mark_childs thy; + + delete_file (out_name thy) + ) end; fun time_use_thy tname = timeit(fn()=> - (writeln("\n**** Starting Theory " ^ tname ^ " ****"); use_thy tname; - writeln("\n**** Finished Theory " ^ tname ^ " ****"))); + (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 ThyInfo {childs, ...} = get_thyinfo t + in childs union (next_level ts) + end + | next_level [] = []; + + val childs = next_level thys + in load_order childs ((result \\ childs) @ childs) end; + + fun reload_changed (t :: ts) = + let val curr = get_thyinfo t; + val thy_file = (find_file "" (t ^ ".thy") + handle FILE_NOT_FOUND => ""); + val (thy_path, _) = split_filename thy_file; + val ml_file = if thy_file = "" + then (find_file "" (t ^ ".ML") + handle FILE_NOT_FOUND => + error ("Could find no .thy or .ML file for theory " + ^ t)) + else if file_exists (thy_path ^ t ^ ".ML") + then thy_path ^ t ^ ".ML" + else "" + 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 [] = () + in 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 (t :: ts) child = + let val childl = to_lower child; + + fun load_base base = + let val basel = to_lower base; + + (*List all descendants of a theory list *) + fun list_descendants (t :: ts) = + if already_loaded t then + let val ThyInfo {childs, ...} = get_thyinfo t + in childs union (list_descendants (ts union childs)) + end + else [] + | list_descendants [] = []; + + (*Show the cycle that would be created by add_child *) + fun show_cycle () = + let fun find_it result curr = + if basel = curr then + error ("Cyclic dependency of theories: " + ^ childl ^ "->" ^ basel ^ result) + else if already_loaded curr then + let val ThyInfo {childs, ...} = get_thyinfo curr + in seq (find_it ("->" ^ curr ^ result)) childs + end + else () + in find_it "" childl end; + + (*Check if a cycle will be created by add_child *) + fun find_cycle () = + if basel mem (list_descendants [childl]) then show_cycle () + else (); + + (*Add child to child list of base *) + fun add_child (t :: loaded) = + let val ThyInfo {name, childs, thy_info, ml_info, + theory} = t + in if name = basel then + ThyInfo {name = name, childs = childl ins childs, + thy_info = thy_info, ml_info = ml_info, + theory = theory} :: loaded + else + t :: (add_child loaded) + end + | add_child [] = + [ThyInfo {name = basel, childs = [childl], + thy_info = "", ml_info = "", + theory = Thm.pure_thy}]; + (*Thm.pure_thy is used as a dummy *) + + val thy_there = already_loaded basel + (*test this before child is added *) + in + if childl = basel then + error ("Cyclic dependency of theories: " ^ child + ^ "->" ^ child) + else find_cycle (); + loaded_thys := add_child (!loaded_thys); + if thy_there then () + else (writeln ("Autoloading theory " ^ base + ^ " (used by " ^ child ^ ")"); + use_thy base + ) + end; + + val (tl :: tls) = map to_lower (t :: ts) + in seq load_base (t :: ts); + foldl Thm.merge_theories (get_theory tl, map get_theory tls) + end + | base_on [] _ = raise Match; + +(*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, childs, thy_info, ml_info, ...} = t + in if name = (to_lower thy_name) then + ThyInfo {name = name, childs = childs, + thy_info = thy_info, ml_info = ml_info, + theory = thy} :: loaded + else + t :: (make_change loaded) + end + | make_change [] = + [ThyInfo {name = (to_lower thy_name), childs = [], thy_info = "", + ml_info = "", theory = 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", childs = [], thy_info = "", + ml_info = "", theory = Thm.pure_thy}] + | set_loaded ts = + loaded_thys := ts; + +(*Change the path list that is to be searched for .thy and .ML files *) +fun set_loadpath new_path = + loadpath := new_path; + +(*This function is for debugging purposes only *) +fun relations thy = + let val ThyInfo {childs, ...} = get_thyinfo thy + in + writeln (thy ^ ": " ^ (space_implode ", " childs)); + seq relations childs + end end; + diff -r 075db6ac7f2f -r 208ab8773a73 src/Pure/Thy/syntax.ML --- a/src/Pure/Thy/syntax.ML Fri Oct 22 13:39:23 1993 +0100 +++ b/src/Pure/Thy/syntax.ML Fri Oct 22 13:42:51 1993 +0100 @@ -112,7 +112,8 @@ axs ^ "\n\n" ^ vals end; -fun mk_struct (id, s) = "structure " ^ id ^ " =\nstruct\n" ^ s ^ "\nend\n"; +fun mk_struct (id, s) = "structure " ^ id ^ " =\nstruct\n" ^ s ^ "\nend;\n" + ^ "store_theory " ^ quote id ^ " " ^ id ^ ".thy;\n"; fun mk_sext mfix trans = @@ -148,22 +149,20 @@ let val noext = ("[]", "[]", "[]", "[]", "[]", "[]"); val basethy = - if tinfix = "[]" then base - else mk_ext_thy (base, name ^ "(type infix)", noext, mk_simple_sext tinfix); + if tinfix = "[]" then base ^ (quote name) + else mk_ext_thy (base ^ (quote name), name ^ "(type infix)", noext, mk_simple_sext tinfix); val sext = if mfix = "[]" andalso trans = "[]" andalso ml = "" then "None" else mk_sext mfix trans; - val thy = "\nval thy = " ^ mk_ext_thy (basethy, name, ext, sext); + val thy = "val thy = " ^ mk_ext_thy (basethy, name, ext, sext); in mk_struct (name, preamble ^ ml ^ postamble ^ thy ^ "\nend") end - | mk_structure ((name, base), None) = mk_struct (name, "\nval thy = " ^ base); - + | mk_structure ((name, base), None) = + mk_struct (name, "\nval thy = " ^ base ^ (quote name)); -fun merge (t :: ts) = - foldl (fn (base, thy) => "(merge_theories (" ^ base ^ ", " ^ thy ^ ".thy))") - (t ^ ".thy", ts) - | merge [] = raise Match; +fun merge thys = + "base_on " ^ (bracket (quote (space_implode "\",\"" thys))) ^ " ";