# HG changeset patch # User clasohm # Date 753456199 -3600 # Node ID 0a2f744e008aa18e709bce8486c15b5158e75357 # Parent db9043a8e372614beb52710069e0c5ac32ab583f 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 diff -r db9043a8e372 -r 0a2f744e008a src/Pure/Thy/read.ML --- a/src/Pure/Thy/read.ML Tue Nov 16 14:13:11 1993 +0100 +++ b/src/Pure/Thy/read.ML Tue Nov 16 14:23:19 1993 +0100 @@ -1,7 +1,7 @@ (* Title: Pure/Thy/read ID: $Id$ Author: Sonia Mahjoub / Tobias Nipkow / L C Paulson - Copyright 1992 TU Muenchen + Copyright 1993 TU Muenchen Reading and writing the theory definition files. @@ -10,39 +10,43 @@ 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 - type thy_info - datatype BaseType = Thy of string + 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 base_on : BaseType list -> string -> Thm.theory + 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 - val set_loadpath : string list -> unit - val relations : string -> unit end; functor ReadthyFUN (structure ThySyn: THYSYN) : READTHY = struct -datatype thy_info = ThyInfo of {name: string, children: string list, - thy_info: string, ml_info: string, - theory: Thm.theory}; - -datatype BaseType = Thy of string +datatype basetype = Thy of string | File of string; -val loaded_thys = ref [ThyInfo {name = "pure", children = [], thy_info = "", - ml_info = "", theory = Thm.pure_thy}]; +val loaded_thys = ref [ThyInfo {name = "Pure", path = "", children = [], + thy_info = Some "", ml_info = Some "", + theory = Some Thm.pure_thy}]; -val loadpath = ref ["."]; +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"; @@ -60,7 +64,56 @@ let val instream = open_in file in close_in instream; true end handle Io _ => false; -exception FILE_NOT_FOUND; (*raised by find_file *) +(*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.*) @@ -70,41 +123,85 @@ tack_on curr name else find_it paths - | find_it [] = raise FILE_NOT_FOUND + | find_it [] = "" 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; + 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; -(*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; + 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; -(*Get thy_info for a loaded theory *) -fun get_thyinfo thy = - let fun do_search (t :: loaded : thy_info list) = +(*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 t else do_search loaded end - | do_search [] = error ("Internal error (get_thyinfo): theory " - ^ thy ^ " not found.") - in do_search (!loaded_thys) end; + in if name = thy then ts + else t :: (remove ts) + end + | remove [] = [] + in loaded_thys := remove (!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); +(*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; -(*Get theory object for a loaded theory *) -fun get_theory name = - let val ThyInfo {theory, ...} = get_thyinfo name - in theory 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; @@ -113,60 +210,34 @@ 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 = 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 " - ^ thy_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; + 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; - (*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, children, thy_info, ml_info, theory} - :: loaded) result = - do_remove loaded - (ThyInfo {name = name, children = children \ 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 *) + (*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; - (*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, children, theory, ...} = t - in if name = thy then - ThyInfo {name = name, children = children, - 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 *) + (*Mark all direct descendants of a theory as changed *) fun mark_children thy = - let val ThyInfo {children, ...} = get_thyinfo 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: \"" - ^ (space_implode "\",\"" children) ^ "\""); - seq (set_info "" "") children - handle THY_NOT_FOUND => () - (*If this theory was automatically loaded by a child - then the child cannot be found in loaded_thys *) + ^ " are now out-of-date: " + ^ (quote (space_implode "\",\"" children))); + seq mark_outdated children ) else () end @@ -175,43 +246,32 @@ else ( writeln ("Loading theory " ^ (quote name)); - if thy_uptodate orelse (thy_file = "") then () - else - ( - (*Allow dependency lists to be rebuild completely *) - remove_child thy; - - read_thy thy thy_file - ); + if thy_uptodate orelse thy_file = "" then () + else (read_thy thyl thy_file; + use (out_name thyl) + ); - (*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 thy_name ^ " " - ^ thy_name ^ ".thy;\n"); - close_out outstream - end; - use ".tmp.ML"; - delete_file ".tmp.ML" - ) - else if ml_file <> "" then use ml_file - else (); + 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 - handle THY_NOT_FOUND => error ("Could not find theory \"" ^ thy - ^ "\" (wrong filename?)")); + set_info (file_info thy_file) (file_info ml_file) thy_name; + set_path (); (*Mark theories that have to be reloaded.*) - mark_children thy; + mark_children thy_name; - delete_file (out_name thy) - ) + if !delete_tmpfiles then delete_file (out_name thyl) + else () + ) end; fun time_use_thy tname = timeit(fn()=> @@ -227,8 +287,12 @@ fun load_order [] result = result | load_order thys result = let fun next_level (t :: ts) = - let val ThyInfo {children, ...} = get_thyinfo t - in children union (next_level 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 [] = []; @@ -236,123 +300,150 @@ in load_order children ((result \\ children) @ children) 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 "" + 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; - + 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; + | 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 val childl = to_lower child; - - (*List all descendants of a theory list *) + let (*List all descendants of a theory list *) fun list_descendants (t :: ts) = - if already_loaded t then - let val ThyInfo {children, ...} = get_thyinfo t - in children union - (list_descendants (ts union children)) - end - else [] + 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 = - if base = curr then - error ("Cyclic dependency of theories: " - ^ childl ^ "->" ^ base ^ result) - else if already_loaded curr then - let val ThyInfo {children, ...} = get_thyinfo curr - in seq (find_it ("->" ^ curr ^ result)) children - end - else () - in find_it "" childl end; + 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 [childl]) then show_cycle base + if base mem (list_descendants [child]) then show_cycle base else (); (*Add child to child list of base *) - fun add_child (t :: loaded) base = - let val ThyInfo {name, children, thy_info, ml_info, theory} = t - in if name = base then - ThyInfo {name = name, - children = childl ins children, - thy_info = thy_info, ml_info = ml_info, - theory = theory} :: loaded - else - t :: (add_child loaded base) - end - | add_child [] base = - [ThyInfo {name = base, children = [childl], - thy_info = "", ml_info = "", - theory = Thm.pure_thy}]; - (*Thm.pure_thy is used as a dummy *) + 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; - fun do_load thy = - let val basel = to_lower thy; - - val thy_present = already_loaded basel + (*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 childl = basel then + if child = base then error ("Cyclic dependency of theories: " ^ child ^ "->" ^ child) else - (find_cycle thy; - loaded_thys := add_child (!loaded_thys) basel; + (find_cycle base; + add_child base; if thy_present then () - else (writeln ("Autoloading theory " ^ (quote thy) + else (writeln ("Autoloading theory " ^ (quote base) ^ " (used by " ^ (quote child) ^ ")"); - use_thy thy) + use_thy base) ) end; + (*Load all needed files and make a list of all real theories *) fun load_base (Thy b :: bs) = - (do_load b; - (to_lower b) :: (load_base bs)) + (load b; + b :: (load_base bs)) | load_base (File b :: bs) = - (do_load b; - load_base bs) (*don't add it to merge_theories' parameter *) + (load b; + load_base bs) (*don't add it to merge_theories' parameter *) | load_base [] = []; - - val (t :: ts) = load_base bases + + (*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, children, thy_info, ml_info, ...} = t - in if name = (to_lower thy_name) then - ThyInfo {name = name, children = children, + 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 = thy} :: loaded + theory = Some thy} :: loaded else t :: (make_change loaded) end | make_change [] = - [ThyInfo {name = (to_lower thy_name), children = [], thy_info = "", - ml_info = "", theory = thy}] + [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 *) @@ -360,22 +451,11 @@ (*Change the list of loaded theories *) fun set_loaded [] = - loaded_thys := [ThyInfo {name = "pure", children = [], thy_info = "", - ml_info = "", theory = Thm.pure_thy}] + loaded_thys := [ThyInfo {name = "Pure", path = "", children = [], + thy_info = Some "", ml_info = Some "", + theory = Some 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; +end -(*This function is for debugging purposes only *) -fun relations thy = - let val ThyInfo {children, ...} = get_thyinfo thy - in - writeln (thy ^ ": " ^ (space_implode ", " children)); - seq relations children - end - -end; - diff -r db9043a8e372 -r 0a2f744e008a src/Pure/Thy/syntax.ML --- a/src/Pure/Thy/syntax.ML Tue Nov 16 14:13:11 1993 +0100 +++ b/src/Pure/Thy/syntax.ML Tue Nov 16 14:23:19 1993 +0100 @@ -7,7 +7,7 @@ signature THYSYN = sig - datatype BaseType = Thy of string + datatype basetype = Thy of string | File of string val read: string list -> string @@ -115,8 +115,7 @@ axs ^ "\n\n" ^ vals end; -fun mk_struct (id, s) = "structure " ^ id ^ " =\nstruct\n" ^ s ^ "\nend;\n" - ^ "store_theory " ^ quote id ^ " " ^ id ^ ".thy;\n"; +fun mk_struct (id, s) = "structure " ^ id ^ " =\nstruct\n" ^ s ^ "\nend;\n"; fun mk_sext mfix trans = @@ -164,7 +163,7 @@ | mk_structure ((name, base), None) = mk_struct (name, "\nval thy = " ^ base ^ (quote name)); -datatype BaseType = Thy of string +datatype basetype = Thy of string | File of string; fun merge thys =