1.1 --- a/src/Pure/Thy/ROOT.ML Fri Oct 22 13:39:23 1993 +0100
1.2 +++ b/src/Pure/Thy/ROOT.ML Fri Oct 22 13:42:51 1993 +0100
1.3 @@ -26,6 +26,11 @@
1.4 structure Lex = LexicalFUN (Keyword);
1.5 structure Parse = ParseFUN (Lex);
1.6 structure ThySyn = ThySynFUN (Parse);
1.7 -structure Readthy = ReadthyFUN (ThySyn);
1.8
1.9 +(*This structure is only defined to be compatible with older versions of
1.10 + READTHY. Don't use it in newly created theory/ROOT.ML files! Instead
1.11 + define a new structure. Otherwise Poly/ML won't save a reference variable
1.12 + defined inside the functor. *)
1.13 +structure Readthy = ReadthyFUN (structure ThySyn = ThySyn);
1.14 open Readthy;
1.15 +
2.1 --- a/src/Pure/Thy/read.ML Fri Oct 22 13:39:23 1993 +0100
2.2 +++ b/src/Pure/Thy/read.ML Fri Oct 22 13:42:51 1993 +0100
2.3 @@ -12,27 +12,40 @@
2.4
2.5 signature READTHY =
2.6 sig
2.7 - val split_filename : string -> string * string
2.8 + type thy_info
2.9 +
2.10 + val use_thy : string -> unit
2.11 + val update : unit -> unit
2.12 val time_use_thy : string -> unit
2.13 - val use_thy : string -> unit
2.14 + val base_on : string list -> string -> Thm.theory
2.15 + val store_theory : string -> Thm.theory -> unit
2.16 + val list_loaded : unit -> thy_info list
2.17 + val set_loaded : thy_info list -> unit
2.18 + val set_loadpath : string list -> unit
2.19 + val relations : string -> unit
2.20 end;
2.21
2.22
2.23 -functor ReadthyFUN (ThySyn: THYSYN): READTHY =
2.24 +functor ReadthyFUN (structure ThySyn: THYSYN) : READTHY =
2.25 struct
2.26
2.27 -(*Convert Unix filename of the form path/file to "path/" and "file" ;
2.28 - if filename contains no slash, then it returns "" and "file" *)
2.29 -fun split_filename name =
2.30 - let val (file,path) = take_prefix (apr(op<>,"/")) (rev (explode name))
2.31 - in (implode(rev path), implode(rev file)) end;
2.32 +datatype thy_info = ThyInfo of {name: string, childs: string list,
2.33 + thy_info: string, ml_info: string,
2.34 + theory: Thm.theory};
2.35
2.36 -(*create name of the output ML file for the theory*)
2.37 +val loaded_thys = ref [ThyInfo {name = "pure", childs = [], thy_info = "",
2.38 + ml_info = "", theory = Thm.pure_thy}];
2.39 +
2.40 +val loadpath = ref ["."];
2.41 +
2.42 +
2.43 +(*Make name of the output ML file for a theory *)
2.44 fun out_name thy = "." ^ thy ^ ".thy.ML";
2.45
2.46 -fun read_thy path thy =
2.47 - let val instream = open_in (path ^ thy ^ ".thy")
2.48 - val outstream = open_out (path ^ out_name thy)
2.49 +(*Read a file specified by thy_file containing theory thy *)
2.50 +fun read_thy thy thy_file =
2.51 + let val instream = open_in thy_file;
2.52 + val outstream = open_out (out_name thy)
2.53 in output (outstream, ThySyn.read (explode(input(instream, 999999))));
2.54 close_out outstream;
2.55 close_in instream
2.56 @@ -42,20 +55,314 @@
2.57 let val instream = open_in file in close_in instream; true end
2.58 handle Io _ => false;
2.59
2.60 -(*Use the file if it exists*)
2.61 -fun try_use file =
2.62 - if file_exists file then use file else ();
2.63 +exception FILE_NOT_FOUND; (*raised by find_file *)
2.64
2.65 -(*Read and convert the theory to a .XXX.thy.ML file and also try to read XXX.ML*)
2.66 +(*Find a file using a list of paths if no absolute or relative path is
2.67 + specified.*)
2.68 +fun find_file "" name =
2.69 + let fun find_it (curr :: paths) =
2.70 + if file_exists (tack_on curr name) then
2.71 + tack_on curr name
2.72 + else
2.73 + find_it paths
2.74 + | find_it [] = raise FILE_NOT_FOUND
2.75 + in find_it (!loadpath) end
2.76 + | find_file path name =
2.77 + if file_exists (tack_on path name) then tack_on path name
2.78 + else raise FILE_NOT_FOUND;
2.79 +
2.80 +(*Use the file if it exists *)
2.81 +fun try_use file =
2.82 + if file_exists file then use file else ();
2.83 +
2.84 +(*Check if a theory was already loaded *)
2.85 +fun already_loaded thy =
2.86 + let fun do_search ((ThyInfo {name, ...}) :: loaded) =
2.87 + if name = thy then true else do_search loaded
2.88 + | do_search [] = false
2.89 + in do_search (!loaded_thys) end;
2.90 +
2.91 +(*Get thy_info for a loaded theory *)
2.92 +fun get_thyinfo thy =
2.93 + let fun do_search (t :: loaded : thy_info list) =
2.94 + let val ThyInfo {name, ...} = t
2.95 + in if name = thy then t else do_search loaded end
2.96 + | do_search [] = error ("Internal error (get_thyinfo): theory "
2.97 + ^ thy ^ " not found.")
2.98 + in do_search (!loaded_thys) end;
2.99 +
2.100 +(*Check if a theory file has changed since its last use.
2.101 + Return a pair of boolean values for .thy and for .ML. *)
2.102 +fun thy_unchanged thy thy_file ml_file =
2.103 + if already_loaded thy then
2.104 + let val ThyInfo {thy_info, ml_info, ...} = get_thyinfo thy;
2.105 + in ((file_info (thy_file) = thy_info), (file_info (ml_file) = ml_info))
2.106 + end
2.107 + else (false, false);
2.108 +
2.109 +(*Get theory object for a loaded theory *)
2.110 +fun get_theory name =
2.111 + let val ThyInfo {theory, ...} = get_thyinfo name
2.112 + in theory end;
2.113 +
2.114 +(*Read .thy and .ML files that haven't been read yet or have changed since
2.115 + they were last read;
2.116 + loaded_thys is a thy_info list ref containing all theories that have
2.117 + completly been read by this and preceeding use_thy calls.
2.118 + If a theory changed since its last use its childs are marked as changed *)
2.119 fun use_thy name =
2.120 - let val (path,thy) = split_filename name
2.121 - in read_thy path thy;
2.122 - use (path ^ out_name thy);
2.123 - try_use (path ^ thy ^ ".ML")
2.124 + let val (path, thy_name) = split_filename name;
2.125 + val thy = to_lower thy_name;
2.126 + val thy_file = (find_file path (thy ^ ".thy")
2.127 + handle FILE_NOT_FOUND => "");
2.128 + val (thy_path, _) = split_filename thy_file;
2.129 + val ml_file = if thy_file = ""
2.130 + then (find_file path (thy ^ ".ML")
2.131 + handle FILE_NOT_FOUND =>
2.132 + error ("Could find no .thy or .ML file for theory "
2.133 + ^ name))
2.134 + else if file_exists (thy_path ^ thy ^ ".ML")
2.135 + then thy_path ^ thy ^ ".ML"
2.136 + else ""
2.137 + val (thy_uptodate, ml_uptodate) = thy_unchanged thy thy_file ml_file;
2.138 +
2.139 + (*Remove theory from all child lists in loaded_thys.
2.140 + Afterwards add_child should be called for the (new) base theories *)
2.141 + fun remove_child thy =
2.142 + let fun do_remove (ThyInfo {name, childs, thy_info, ml_info, theory}
2.143 + :: loaded) result =
2.144 + do_remove loaded
2.145 + (ThyInfo {name = name, childs = childs \ thy,
2.146 + thy_info = thy_info, ml_info = ml_info,
2.147 + theory = theory} :: result)
2.148 + | do_remove [] result = result;
2.149 + in loaded_thys := do_remove (!loaded_thys) [] end;
2.150 +
2.151 + exception THY_NOT_FOUND; (*Raised by set_info *)
2.152 +
2.153 + (*Change thy_info and ml_info for an existent item or create
2.154 + a new item with empty child list *)
2.155 + fun set_info thy_new ml_new thy =
2.156 + let fun make_change (t :: loaded) =
2.157 + let val ThyInfo {name, childs, theory, ...} = t
2.158 + in if name = thy then
2.159 + ThyInfo {name = name, childs = childs,
2.160 + thy_info = thy_new, ml_info = ml_new,
2.161 + theory = theory} :: loaded
2.162 + else
2.163 + t :: (make_change loaded)
2.164 + end
2.165 + | make_change [] = raise THY_NOT_FOUND
2.166 + in loaded_thys := make_change (!loaded_thys) end;
2.167 +
2.168 + (*Mark all direct and indirect descendants of a theory as changed *)
2.169 + fun mark_childs thy =
2.170 + let val ThyInfo {childs, ...} = get_thyinfo thy
2.171 + in writeln ("Marking childs of modified theory " ^ thy ^ " (" ^
2.172 + (space_implode "," childs) ^ ")");
2.173 + seq (set_info "" "") childs
2.174 + handle THY_NOT_FOUND => ()
2.175 + (*If this theory was automatically loaded by a child
2.176 + then the child cannot be found in loaded_thys *)
2.177 + end
2.178 +
2.179 + in if thy_uptodate andalso ml_uptodate then ()
2.180 + else
2.181 + (
2.182 + writeln ("Loading theory " ^ name);
2.183 + if thy_uptodate orelse (thy_file = "") then ()
2.184 + else
2.185 + (
2.186 + (*Allow dependency lists to be rebuild completely *)
2.187 + remove_child thy;
2.188 +
2.189 + read_thy thy thy_file
2.190 + );
2.191 +
2.192 + (*Actually read files!*)
2.193 + if thy_uptodate orelse (thy_file = "") then ()
2.194 + else use (out_name thy);
2.195 + if (thy_file = "") then (*theory object created in .ML file*)
2.196 + (
2.197 + use ml_file;
2.198 + let val outstream = open_out (".tmp.ML")
2.199 + in
2.200 + output (outstream, "store_theory " ^ quote name ^ " " ^ name
2.201 + ^ ".thy;\n");
2.202 + close_out outstream
2.203 + end;
2.204 + use ".tmp.ML";
2.205 + delete_file ".tmp.ML"
2.206 + )
2.207 + else try_use ml_file;
2.208 +
2.209 + (*Now set the correct info.*)
2.210 + (set_info (file_info thy_file) (file_info ml_file) thy
2.211 + handle THY_NOT_FOUND => error ("Could not find theory \"" ^ name
2.212 + ^ "\" (wrong filename?)"));
2.213 +
2.214 + (*Mark theories that have to be reloaded.*)
2.215 + mark_childs thy;
2.216 +
2.217 + delete_file (out_name thy)
2.218 + )
2.219 end;
2.220
2.221 fun time_use_thy tname = timeit(fn()=>
2.222 - (writeln("\n**** Starting Theory " ^ tname ^ " ****"); use_thy tname;
2.223 - writeln("\n**** Finished Theory " ^ tname ^ " ****")));
2.224 + (writeln("\n**** Starting Theory " ^ tname ^ " ****");
2.225 + use_thy tname;
2.226 + writeln("\n**** Finished Theory " ^ tname ^ " ****"))
2.227 + );
2.228 +
2.229 +(*Load all thy or ML files that have been changed and also
2.230 + all theories that depend on them *)
2.231 +fun update () =
2.232 + let (*List theories in the order they have to be loaded *)
2.233 + fun load_order [] result = result
2.234 + | load_order thys result =
2.235 + let fun next_level (t :: ts) =
2.236 + let val ThyInfo {childs, ...} = get_thyinfo t
2.237 + in childs union (next_level ts)
2.238 + end
2.239 + | next_level [] = [];
2.240 +
2.241 + val childs = next_level thys
2.242 + in load_order childs ((result \\ childs) @ childs) end;
2.243 +
2.244 + fun reload_changed (t :: ts) =
2.245 + let val curr = get_thyinfo t;
2.246 + val thy_file = (find_file "" (t ^ ".thy")
2.247 + handle FILE_NOT_FOUND => "");
2.248 + val (thy_path, _) = split_filename thy_file;
2.249 + val ml_file = if thy_file = ""
2.250 + then (find_file "" (t ^ ".ML")
2.251 + handle FILE_NOT_FOUND =>
2.252 + error ("Could find no .thy or .ML file for theory "
2.253 + ^ t))
2.254 + else if file_exists (thy_path ^ t ^ ".ML")
2.255 + then thy_path ^ t ^ ".ML"
2.256 + else ""
2.257 + val (thy_uptodate, ml_uptodate) =
2.258 + thy_unchanged t thy_file ml_file;
2.259 +
2.260 + in if thy_uptodate andalso ml_uptodate then ()
2.261 + else use_thy t;
2.262 + reload_changed ts
2.263 + end
2.264 + | reload_changed [] = ()
2.265 + in reload_changed (load_order ["pure"] []) end;
2.266 +
2.267 +(*Merge theories to build a base for a new theory.
2.268 + Base members are only loaded if they are missing. *)
2.269 +fun base_on (t :: ts) child =
2.270 + let val childl = to_lower child;
2.271 +
2.272 + fun load_base base =
2.273 + let val basel = to_lower base;
2.274 +
2.275 + (*List all descendants of a theory list *)
2.276 + fun list_descendants (t :: ts) =
2.277 + if already_loaded t then
2.278 + let val ThyInfo {childs, ...} = get_thyinfo t
2.279 + in childs union (list_descendants (ts union childs))
2.280 + end
2.281 + else []
2.282 + | list_descendants [] = [];
2.283 +
2.284 + (*Show the cycle that would be created by add_child *)
2.285 + fun show_cycle () =
2.286 + let fun find_it result curr =
2.287 + if basel = curr then
2.288 + error ("Cyclic dependency of theories: "
2.289 + ^ childl ^ "->" ^ basel ^ result)
2.290 + else if already_loaded curr then
2.291 + let val ThyInfo {childs, ...} = get_thyinfo curr
2.292 + in seq (find_it ("->" ^ curr ^ result)) childs
2.293 + end
2.294 + else ()
2.295 + in find_it "" childl end;
2.296 +
2.297 + (*Check if a cycle will be created by add_child *)
2.298 + fun find_cycle () =
2.299 + if basel mem (list_descendants [childl]) then show_cycle ()
2.300 + else ();
2.301 +
2.302 + (*Add child to child list of base *)
2.303 + fun add_child (t :: loaded) =
2.304 + let val ThyInfo {name, childs, thy_info, ml_info,
2.305 + theory} = t
2.306 + in if name = basel then
2.307 + ThyInfo {name = name, childs = childl ins childs,
2.308 + thy_info = thy_info, ml_info = ml_info,
2.309 + theory = theory} :: loaded
2.310 + else
2.311 + t :: (add_child loaded)
2.312 + end
2.313 + | add_child [] =
2.314 + [ThyInfo {name = basel, childs = [childl],
2.315 + thy_info = "", ml_info = "",
2.316 + theory = Thm.pure_thy}];
2.317 + (*Thm.pure_thy is used as a dummy *)
2.318 +
2.319 + val thy_there = already_loaded basel
2.320 + (*test this before child is added *)
2.321 + in
2.322 + if childl = basel then
2.323 + error ("Cyclic dependency of theories: " ^ child
2.324 + ^ "->" ^ child)
2.325 + else find_cycle ();
2.326 + loaded_thys := add_child (!loaded_thys);
2.327 + if thy_there then ()
2.328 + else (writeln ("Autoloading theory " ^ base
2.329 + ^ " (used by " ^ child ^ ")");
2.330 + use_thy base
2.331 + )
2.332 + end;
2.333 +
2.334 + val (tl :: tls) = map to_lower (t :: ts)
2.335 + in seq load_base (t :: ts);
2.336 + foldl Thm.merge_theories (get_theory tl, map get_theory tls)
2.337 + end
2.338 + | base_on [] _ = raise Match;
2.339 +
2.340 +(*Change theory object for an existent item of loaded_thys
2.341 + or create a new item *)
2.342 +fun store_theory thy_name thy =
2.343 + let fun make_change (t :: loaded) =
2.344 + let val ThyInfo {name, childs, thy_info, ml_info, ...} = t
2.345 + in if name = (to_lower thy_name) then
2.346 + ThyInfo {name = name, childs = childs,
2.347 + thy_info = thy_info, ml_info = ml_info,
2.348 + theory = thy} :: loaded
2.349 + else
2.350 + t :: (make_change loaded)
2.351 + end
2.352 + | make_change [] =
2.353 + [ThyInfo {name = (to_lower thy_name), childs = [], thy_info = "",
2.354 + ml_info = "", theory = thy}]
2.355 + in loaded_thys := make_change (!loaded_thys) end;
2.356 +
2.357 +(*Create a list of all theories loaded by this structure *)
2.358 +fun list_loaded () = (!loaded_thys);
2.359 +
2.360 +(*Change the list of loaded theories *)
2.361 +fun set_loaded [] =
2.362 + loaded_thys := [ThyInfo {name = "pure", childs = [], thy_info = "",
2.363 + ml_info = "", theory = Thm.pure_thy}]
2.364 + | set_loaded ts =
2.365 + loaded_thys := ts;
2.366 +
2.367 +(*Change the path list that is to be searched for .thy and .ML files *)
2.368 +fun set_loadpath new_path =
2.369 + loadpath := new_path;
2.370 +
2.371 +(*This function is for debugging purposes only *)
2.372 +fun relations thy =
2.373 + let val ThyInfo {childs, ...} = get_thyinfo thy
2.374 + in
2.375 + writeln (thy ^ ": " ^ (space_implode ", " childs));
2.376 + seq relations childs
2.377 + end
2.378
2.379 end;
2.380 +
3.1 --- a/src/Pure/Thy/syntax.ML Fri Oct 22 13:39:23 1993 +0100
3.2 +++ b/src/Pure/Thy/syntax.ML Fri Oct 22 13:42:51 1993 +0100
3.3 @@ -112,7 +112,8 @@
3.4 axs ^ "\n\n" ^ vals
3.5 end;
3.6
3.7 -fun mk_struct (id, s) = "structure " ^ id ^ " =\nstruct\n" ^ s ^ "\nend\n";
3.8 +fun mk_struct (id, s) = "structure " ^ id ^ " =\nstruct\n" ^ s ^ "\nend;\n"
3.9 + ^ "store_theory " ^ quote id ^ " " ^ id ^ ".thy;\n";
3.10
3.11
3.12 fun mk_sext mfix trans =
3.13 @@ -148,22 +149,20 @@
3.14 let
3.15 val noext = ("[]", "[]", "[]", "[]", "[]", "[]");
3.16 val basethy =
3.17 - if tinfix = "[]" then base
3.18 - else mk_ext_thy (base, name ^ "(type infix)", noext, mk_simple_sext tinfix);
3.19 + if tinfix = "[]" then base ^ (quote name)
3.20 + else mk_ext_thy (base ^ (quote name), name ^ "(type infix)", noext, mk_simple_sext tinfix);
3.21 val sext =
3.22 if mfix = "[]" andalso trans = "[]" andalso ml = "" then "None"
3.23 else mk_sext mfix trans;
3.24 - val thy = "\nval thy = " ^ mk_ext_thy (basethy, name, ext, sext);
3.25 + val thy = "val thy = " ^ mk_ext_thy (basethy, name, ext, sext);
3.26 in
3.27 mk_struct (name, preamble ^ ml ^ postamble ^ thy ^ "\nend")
3.28 end
3.29 - | mk_structure ((name, base), None) = mk_struct (name, "\nval thy = " ^ base);
3.30 + | mk_structure ((name, base), None) =
3.31 + mk_struct (name, "\nval thy = " ^ base ^ (quote name));
3.32
3.33 -
3.34 -fun merge (t :: ts) =
3.35 - foldl (fn (base, thy) => "(merge_theories (" ^ base ^ ", " ^ thy ^ ".thy))")
3.36 - (t ^ ".thy", ts)
3.37 - | merge [] = raise Match;
3.38 +fun merge thys =
3.39 + "base_on " ^ (bracket (quote (space_implode "\",\"" thys))) ^ " ";
3.40
3.41
3.42