# HG changeset patch # User clasohm # Date 774271842 -7200 # Node ID 836cad329311780a93e929d8fac80fa62d6f4073 # Parent bf2f285aa316b58cfa10d4a3a128f73382326ea2 added check for concistency of filename and theory name; made loaded_thys a symtab instead of an association list; added store_thm, qed, get_thm, get_thms diff -r bf2f285aa316 -r 836cad329311 src/Pure/Thy/thy_parse.ML --- a/src/Pure/Thy/thy_parse.ML Fri Jul 15 12:24:05 1994 +0200 +++ b/src/Pure/Thy/thy_parse.ML Fri Jul 15 13:30:42 1994 +0200 @@ -49,7 +49,7 @@ type syntax val make_syntax: string list -> (string * (token list -> (string * string) * token list)) list -> syntax - val parse_thy: syntax -> string -> string + val parse_thy: syntax -> string -> string -> string val section: string -> string -> (token list -> string * token list) -> (string * (token list -> (string * string) * token list)) val axm_section: string -> string @@ -388,43 +388,49 @@ (* theory definition *) -fun mk_structure ((thy_name, old_thys), Some (extxt, postxt, mltxt)) = - "structure " ^ thy_name ^ " =\n\ - \struct\n\ - \\n\ - \local\n" - ^ trfun_defs ^ "\n\ - \in\n\ - \\n" - ^ mltxt ^ "\n\ - \\n\ - \val thy = (" ^ old_thys ^ " true)\n\n\ - \|> add_trfuns\n" - ^ trfun_args ^ "\n\ - \\n" - ^ extxt ^ "\n\ - \\n\ - \|> add_thyname " ^ quote thy_name ^ ";\n\ - \\n\ - \\n" - ^ postxt ^ "\n\ - \\n\ - \end;\n\ - \end;\n" - | mk_structure ((thy_name, old_thys), None) = - "structure " ^ thy_name ^ " =\n\ - \struct\n\ - \\n\ - \val thy = (" ^ old_thys ^ " false);\n\ - \\n\ - \end;\n"; +fun mk_structure tname ((thy_name, old_thys), Some (extxt, postxt, mltxt)) = + if (thy_name = tname) then + "structure " ^ thy_name ^ " =\n\ + \struct\n\ + \\n\ + \local\n" + ^ trfun_defs ^ "\n\ + \in\n\ + \\n" + ^ mltxt ^ "\n\ + \\n\ + \val thy = (" ^ old_thys ^ " true)\n\n\ + \|> add_trfuns\n" + ^ trfun_args ^ "\n\ + \\n" + ^ extxt ^ "\n\ + \\n\ + \|> add_thyname " ^ quote thy_name ^ ";\n\ + \\n\ + \\n" + ^ postxt ^ "\n\ + \\n\ + \end;\n\ + \end;\n" + else error ("use_thy: Filename \"" ^ tname ^ ".thy\" and theory name \"" + ^ thy_name ^ "\" are different") + | mk_structure tname ((thy_name, old_thys), None) = + if (thy_name = tname) then + "structure " ^ thy_name ^ " =\n\ + \struct\n\ + \\n\ + \val thy = (" ^ old_thys ^ " false);\n\ + \\n\ + \end;\n" + else error ("use_thy: Filename \"" ^ tname ^ ".thy\" and theory name \"" + ^ thy_name ^ "\" are different"); -fun theory_defn sectab = +fun theory_defn sectab tname = header -- optional (extension sectab >> Some) None -- eof - >> (mk_structure o #1); + >> (mk_structure tname o #1); -fun parse_thy (lex, sectab) str = - #1 (!! (theory_defn sectab) (tokenize lex str)); +fun parse_thy (lex, sectab) tname str = + #1 (!! (theory_defn sectab tname) (tokenize lex str)); (* standard sections *) diff -r bf2f285aa316 -r 836cad329311 src/Pure/Thy/thy_read.ML --- a/src/Pure/Thy/thy_read.ML Fri Jul 15 12:24:05 1994 +0200 +++ b/src/Pure/Thy/thy_read.ML Fri Jul 15 13:30:42 1994 +0200 @@ -1,7 +1,7 @@ (* Title: Pure/Thy/thy_read.ML ID: $Id$ Author: Sonia Mahjoub / Tobias Nipkow / L C Paulson / Carsten Clasohm - Copyright 1993 TU Muenchen + Copyright 1994 TU Muenchen Reading and writing the theory definition files. @@ -10,17 +10,19 @@ and it then tries to read XXX.ML *) -datatype thy_info = ThyInfo of {name: string, path: string, +datatype thy_info = ThyInfo of {path: string, children: string list, - thy_info: string option, ml_info: string option, - theory: Thm.theory option}; + thy_time: string option, + ml_time: string option, + theory: Thm.theory option, + thms: thm Symtab.table}; signature READTHY = sig datatype basetype = Thy of string | File of string - val loaded_thys : thy_info list ref + val loaded_thys : thy_info Symtab.table ref val loadpath : string list ref val delete_tmpfiles: bool ref @@ -28,35 +30,42 @@ val update : unit -> unit val time_use_thy : string -> unit val unlink_thy : string -> unit - val base_on : basetype list -> string -> bool -> Thm.theory - val store_theory : string -> Thm.theory -> unit + val base_on : basetype list -> string -> bool -> theory + val store_theory : theory * string -> unit + + val store_thm : thm * string -> thm + val qed : string -> unit + val get_thm : theory -> string -> thm + val get_thms : theory -> (string * thm) list end; functor ReadthyFUN(structure ThySyn: THY_SYN): READTHY = struct +open Symtab; 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 loaded_thys = ref (make [("Pure", ThyInfo {path = "", children = [], + thy_time = Some "", ml_time = Some "", + theory = Some pure_thy, + thms = null})]); 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"; +fun out_name tname = "." ^ tname ^ ".thy.ML"; (*Read a file specified by thy_file containing theory thy *) -fun read_thy thy thy_file = +fun read_thy tname thy_file = let val instream = open_in thy_file; - val outstream = open_out (out_name thy); + val outstream = open_out (out_name tname); in - output (outstream, ThySyn.parse (input (instream, 999999))); + output (outstream, ThySyn.parse tname (input (instream, 999999))); close_out outstream; close_in instream end; @@ -66,35 +75,16 @@ 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; +fun get_thyinfo tname = lookup (!loaded_thys, tname); (*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 + else let val ThyInfo {thy_time, ml_time, ...} = the t + in if is_none thy_time orelse is_none ml_time then false + else true + end end; (*Check if a theory file has changed since its last use. @@ -102,12 +92,12 @@ 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 + let val ThyInfo {thy_time, ml_time, ...} = the t + val tn = is_none thy_time; + val mn = is_none ml_time in if not tn andalso not mn then - ((file_info thy_file = the thy_info), - (file_info ml_file = the ml_info)) + ((file_info thy_file = the thy_time), + (file_info ml_file = the ml_time)) else if not tn andalso mn then (true, false) else (false, false) end @@ -156,9 +146,9 @@ (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 tinfo = get_thyinfo name; + in if is_some tinfo andalso path = "" then + let val ThyInfo {path = abs_path, ...} = the tinfo; val (thy_file, ml_file) = if abs_path = "" then new_filename () else (find_file abs_path (name ^ ".thy"), find_file abs_path (name ^ ".ML")) @@ -174,40 +164,31 @@ 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; +fun unlink_thy tname = + let fun remove (ThyInfo {path, children, thy_time, ml_time, theory, thms}) = + ThyInfo {path = path, children = children \ tname, + thy_time = thy_time, ml_time = ml_time, + theory = theory, thms = thms} + in loaded_thys := mapst remove (!loaded_thys) 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; +fun remove_thy tname = + loaded_thys := make (filter_out (fn (id, _) => id = tname) + (alist_of (!loaded_thys))); -(*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; +(*Change thy_time and ml_time for an existent item *) +fun set_info thy_time ml_time tname = + let val ThyInfo {path, children, theory, thms, ...} = + the (lookup (!loaded_thys, tname)); + in loaded_thys := update ((tname, + ThyInfo {path = path, children = children, + thy_time = Some thy_time, ml_time = Some ml_time, + theory = theory, thms = thms}), !loaded_thys) + 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 (); +fun mark_outdated tname = + if already_loaded tname then set_info "" "" tname else (); (*Read .thy and .ML files that haven't been read yet or have changed since they were last read; @@ -215,25 +196,23 @@ 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; + let val (path, tname) = split_filename name; + val (thy_file, ml_file) = get_filenames path tname; 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 + val (thy_uptodate, ml_uptodate) = thy_unchanged tname 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; + let val ThyInfo {children, thy_time, ml_time, theory, thms, ...} = + the (lookup (!loaded_thys, tname)); + in loaded_thys := update ((tname, + ThyInfo {path = abs_path, children = children, + thy_time = thy_time, ml_time = ml_time, + theory = theory, thms = thms}), + !loaded_thys) + end; (*Mark all direct descendants of a theory as changed *) fun mark_children thy = @@ -246,35 +225,47 @@ seq mark_outdated loaded ) else () - end + end; + (*Remove all theorems associated with a theory*) + fun delete_thms () = + let val tinfo = case lookup (!loaded_thys, tname) of + Some (ThyInfo {path, children, thy_time, ml_time, theory, ...}) => + ThyInfo {path = path, children = children, + thy_time = thy_time, ml_time = ml_time, + theory = theory, thms = null} + | None => ThyInfo {path = "", children = [], + thy_time = None, ml_time = None, + theory = None, thms = null}; + in loaded_thys := update ((tname, tinfo), !loaded_thys) end; in if thy_uptodate andalso ml_uptodate then () else ( + delete_thms (); + if thy_uptodate orelse thy_file = "" then () else (writeln ("Reading \"" ^ name ^ ".thy\""); - read_thy thy_name thy_file; - use (out_name thy_name) + read_thy tname thy_file; + use (out_name tname) ); if ml_file = "" then () else (writeln ("Reading \"" ^ name ^ ".ML\""); use ml_file); - use_string ["store_theory " ^ quote thy_name ^ " " ^ thy_name - ^ ".thy;"]; + use_string ["store_theory (" ^ tname ^ ".thy, " ^ quote tname ^ ");"]; (*Now set the correct info*) - set_info (file_info thy_file) (file_info ml_file) thy_name; + set_info (file_info thy_file) (file_info ml_file) tname; set_path (); (*Mark theories that have to be reloaded*) - mark_children thy_name; + mark_children tname; (*Remove temporary files*) if not (!delete_tmpfiles) orelse (thy_file = "") orelse thy_uptodate then () - else delete_file (out_name thy_name) + else delete_file (out_name tname) ) end; @@ -294,13 +285,12 @@ 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 + in children union (next_level ts) end else next_level ts end | next_level [] = []; - val children = next_level thys + val children = next_level thys; in load_order children ((result \\ children) @ children) end; fun reload_changed (t :: ts) = @@ -324,19 +314,15 @@ 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 + let fun collect ((tname, ThyInfo {children, ...}) :: ts) = + if tname mem not_garbage then collect ts + else (writeln ("Theory \"" ^ tname + ^ "\" is no longer linked with Pure - removing it."); + remove_thy tname; + seq mark_outdated children) | collect [] = () - in collect (!loaded_thys) end - + in collect (alist_of (!loaded_thys)) end; in collect_garbage ("Pure" :: (load_order ["Pure"] [])); reload_changed (load_order ["Pure"] []) end; @@ -370,28 +356,24 @@ end in find_it "" child end; - (*Check if a cycle will be created by add_child *) + (*Check if a cycle would 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; + let val tinfo = + case lookup (!loaded_thys, base) of + Some (ThyInfo {path, children, thy_time, ml_time, + theory, thms}) => + ThyInfo {path = path, children = child ins children, + thy_time = thy_time, ml_time = ml_time, + theory = theory, thms = thms} + | None => ThyInfo {path = "", children = [child], + thy_time = None, ml_time = None, + theory = None, thms = null}; + in loaded_thys := Symtab.update ((base, tinfo), !loaded_thys) end; (*Load a base theory if not already done and no cycle would be created *) @@ -433,21 +415,60 @@ (*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; +fun store_theory (thy, tname) = + let val tinfo = case lookup (!loaded_thys, tname) of + Some (ThyInfo {path, children, thy_time, ml_time, thms, ...}) => + ThyInfo {path = path, children = children, + thy_time = thy_time, ml_time = ml_time, + theory = Some thy, thms = thms} + | None => ThyInfo {path = "", children = [], + thy_time = Some "", ml_time = Some "", + theory = Some thy, thms = null}; + in loaded_thys := Symtab.update ((tname, tinfo), !loaded_thys) end; + +(*Store a theorem in the ThyInfo of the theory it is associated with*) +fun store_thm (thm, tname) = + let val thy_name = !(hd (stamps_of_thm thm)); + + val ThyInfo {path, children, thy_time, ml_time, theory, thms} = + case get_thyinfo thy_name of + Some tinfo => tinfo + | None => error ("store_thm: Theory \"" ^ thy_name + ^ "\" is not stored in loaded_thys"); + in loaded_thys := + Symtab.update ((thy_name, ThyInfo {path = path, children = children, + thy_time = thy_time, ml_time = ml_time, + theory = theory, + thms = Symtab.update ((tname, thm), thms)}), + !loaded_thys); + thm + end; +(*Store theorem in loaded_thys and a ML variable*) +fun qed name = use_string ["val " ^ name ^ " = store_thm (result(), " + ^ quote name ^ ");"]; + +fun name_of_thy thy = !(hd (stamps_of_thy thy)); + +(*Retrieve a theorem specified by theory and name*) +fun get_thm thy tname = + let val thy_name = name_of_thy thy; + + val ThyInfo {thms, ...} = + case get_thyinfo thy_name of + Some tinfo => tinfo + | None => error ("get_thm: Theory \"" ^ thy_name + ^ "\" is not stored in loaded_thys"); + in the (lookup (thms, tname)) end; + +(*Retrieve all theorems belonging to the specified theory*) +fun get_thms thy = + let val thy_name = name_of_thy thy; + + val ThyInfo {thms, ...} = + case get_thyinfo thy_name of + Some tinfo => tinfo + | None => error ("get_thms: Theory \"" ^ thy_name + ^ "\" is not stored in loaded_thys"); + in alist_of thms end; end; - diff -r bf2f285aa316 -r 836cad329311 src/Pure/Thy/thy_syn.ML --- a/src/Pure/Thy/thy_syn.ML Fri Jul 15 12:24:05 1994 +0200 +++ b/src/Pure/Thy/thy_syn.ML Fri Jul 15 13:30:42 1994 +0200 @@ -14,7 +14,7 @@ signature THY_SYN = sig - val parse: string -> string + val parse: string -> string -> string end; functor ThySynFun(ThySynData: THY_SYN_DATA): THY_SYN =