# HG changeset patch # User clasohm # Date 751670660 -3600 # Node ID 4cc5a34292a945822dccbae3101ec8cead8c9589 # Parent 0d10b8a501d5ecc52b58f4b74f1923a39624875c corrected some spelling mistakes; removed a bug that made it impossible to read theories that don't have a ML file; extended syntax for bases in syntax.ML: a string can be used to specify a theory that is to be read but is not merged into the base (useful for pseudo theories used to document the dependencies of ML files) diff -r 0d10b8a501d5 -r 4cc5a34292a9 src/Pure/Thy/read.ML --- a/src/Pure/Thy/read.ML Mon Oct 25 12:42:33 1993 +0100 +++ b/src/Pure/Thy/read.ML Tue Oct 26 22:24:20 1993 +0100 @@ -13,11 +13,13 @@ signature READTHY = sig type thy_info + datatype BaseType = Thy of string + | File of string val use_thy : string -> unit val update : unit -> unit val time_use_thy : string -> unit - val base_on : string list -> string -> Thm.theory + 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 @@ -29,11 +31,14 @@ functor ReadthyFUN (structure ThySyn: THYSYN) : READTHY = struct -datatype thy_info = ThyInfo of {name: string, childs: string list, +datatype thy_info = ThyInfo of {name: string, children: string list, thy_info: string, ml_info: string, theory: Thm.theory}; -val loaded_thys = ref [ThyInfo {name = "pure", childs = [], thy_info = "", +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 loadpath = ref ["."]; @@ -71,10 +76,6 @@ 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) = @@ -92,10 +93,10 @@ 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. *) + 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; + 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); @@ -109,7 +110,7 @@ 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 *) + 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; @@ -129,10 +130,10 @@ (*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} + let fun do_remove (ThyInfo {name, children, thy_info, ml_info, theory} :: loaded) result = do_remove loaded - (ThyInfo {name = name, childs = childs \ thy, + (ThyInfo {name = name, children = children \ thy, thy_info = thy_info, ml_info = ml_info, theory = theory} :: result) | do_remove [] result = result; @@ -144,9 +145,9 @@ 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 + let val ThyInfo {name, children, theory, ...} = t in if name = thy then - ThyInfo {name = name, childs = childs, + ThyInfo {name = name, children = children, thy_info = thy_new, ml_info = ml_new, theory = theory} :: loaded else @@ -156,20 +157,24 @@ 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 => () + fun mark_children thy = + let val ThyInfo {children, ...} = 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 *) + ) + else () end in if thy_uptodate andalso ml_uptodate then () else ( - writeln ("Loading theory " ^ name); + writeln ("Loading theory " ^ (quote name)); if thy_uptodate orelse (thy_file = "") then () else ( @@ -194,7 +199,8 @@ use ".tmp.ML"; delete_file ".tmp.ML" ) - else try_use ml_file; + else if ml_file <> "" then use ml_file + else (); (*Now set the correct info.*) (set_info (file_info thy_file) (file_info ml_file) thy @@ -202,7 +208,7 @@ ^ "\" (wrong filename?)")); (*Mark theories that have to be reloaded.*) - mark_childs thy; + mark_children thy; delete_file (out_name thy) ) @@ -221,13 +227,13 @@ 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) + let val ThyInfo {children, ...} = get_thyinfo t + in children union (next_level ts) end | next_level [] = []; - val childs = next_level thys - in load_order childs ((result \\ childs) @ childs) end; + val children = next_level thys + in load_order children ((result \\ children) @ children) end; fun reload_changed (t :: ts) = let val curr = get_thyinfo t; @@ -254,91 +260,98 @@ (*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 = +fun base_on bases 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 {children, ...} = get_thyinfo t + in children union + (list_descendants (ts union children)) + end + else [] + | list_descendants [] = []; - (*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; + (*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; + + (*Check if a cycle will be created by add_child *) + fun find_cycle base = + if base mem (list_descendants [childl]) 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 *) - (*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 *) + fun do_load thy = + let val basel = to_lower thy; - val thy_there = already_loaded basel + val thy_present = 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; + else + (find_cycle thy; + loaded_thys := add_child (!loaded_thys) basel; + if thy_present then () + else (writeln ("Autoloading theory " ^ (quote thy) + ^ " (used by " ^ (quote child) ^ ")"); + use_thy thy) + ) + end; + + fun load_base (Thy b :: bs) = + (do_load b; + (to_lower b) :: (load_base bs)) + | load_base (File b :: bs) = + (do_load b; + load_base bs) (*don't add it to merge_theories' parameter *) + | load_base [] = []; - 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; + val (t :: ts) = load_base bases + 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, childs, thy_info, ml_info, ...} = t + let val ThyInfo {name, children, thy_info, ml_info, ...} = t in if name = (to_lower thy_name) then - ThyInfo {name = name, childs = childs, + ThyInfo {name = name, children = children, 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 = "", + [ThyInfo {name = (to_lower thy_name), children = [], thy_info = "", ml_info = "", theory = thy}] in loaded_thys := make_change (!loaded_thys) end; @@ -347,7 +360,7 @@ (*Change the list of loaded theories *) fun set_loaded [] = - loaded_thys := [ThyInfo {name = "pure", childs = [], thy_info = "", + loaded_thys := [ThyInfo {name = "pure", children = [], thy_info = "", ml_info = "", theory = Thm.pure_thy}] | set_loaded ts = loaded_thys := ts; @@ -358,10 +371,10 @@ (*This function is for debugging purposes only *) fun relations thy = - let val ThyInfo {childs, ...} = get_thyinfo thy + let val ThyInfo {children, ...} = get_thyinfo thy in - writeln (thy ^ ": " ^ (space_implode ", " childs)); - seq relations childs + writeln (thy ^ ": " ^ (space_implode ", " children)); + seq relations children end end; diff -r 0d10b8a501d5 -r 4cc5a34292a9 src/Pure/Thy/syntax.ML --- a/src/Pure/Thy/syntax.ML Mon Oct 25 12:42:33 1993 +0100 +++ b/src/Pure/Thy/syntax.ML Tue Oct 26 22:24:20 1993 +0100 @@ -7,6 +7,9 @@ signature THYSYN = sig + datatype BaseType = Thy of string + | File of string + val read: string list -> string end; @@ -161,8 +164,16 @@ | mk_structure ((name, base), None) = mk_struct (name, "\nval thy = " ^ base ^ (quote name)); +datatype BaseType = Thy of string + | File of string; + fun merge thys = - "base_on " ^ (bracket (quote (space_implode "\",\"" thys))) ^ " "; + let fun make_list (Thy t :: ts) = + ("Thy \"" ^ t ^ "\"") :: make_list ts + | make_list (File t :: ts) = + ("File \"" ^ t ^ "\"") :: make_list ts + | make_list [] = [] + in "base_on " ^ (bracket (space_implode "," (make_list thys))) ^ " " end; @@ -321,6 +332,17 @@ (* "[(id, stg), ...]" *) +(*----------------------- BASE PARSER -------------------------*) + + +fun base toks = + let fun make_thy (b, toks) = (Thy b, toks); + + fun make_file (b, toks) = (File b, toks); + + val (b, toks) = make_thy (id toks) + handle _ => make_file (stg toks) + in (b, toks) end; (*----------------------- ML_TEXT -------------------------*) @@ -336,7 +358,7 @@ || empty >> K None; -val bases = id -- repeat("+" $$-- id) >> op:: ; +val bases = base -- repeat("+" $$-- base) >> op:: ; val theoryDef = !!(id --$$ "=" -- (bases >> merge) -- extension) >> mk_structure;