# HG changeset patch # User wenzelm # Date 777303559 -7200 # Node ID 00365d2e0c501091258f4d2a5c74166df1302f68 # Parent c4092ae47210886ee49828de1d907e517e712bf6 added theory_of_sign, theory_of_thm; renamed get_thms to thms_of; improved store_thms etc.; diff -r c4092ae47210 -r 00365d2e0c50 src/Pure/Thy/thy_read.ML --- a/src/Pure/Thy/thy_read.ML Fri Aug 19 15:38:50 1994 +0200 +++ b/src/Pure/Thy/thy_read.ML Fri Aug 19 15:39:19 1994 +0200 @@ -1,10 +1,13 @@ (* Title: Pure/Thy/thy_read.ML ID: $Id$ - Author: Sonia Mahjoub / Tobias Nipkow / L C Paulson / Carsten Clasohm - Copyright 1994 TU Muenchen + Author: Carsten Clasohm and Markus Wenzel and Sonia Mahjoub and + Tobias Nipkow and L C Paulson + Copyright 1994 TU Muenchen +(* FIXME !? *) Reading and writing the theory definition files. +(* FIXME !? *) For theory XXX, the input file is called XXX.thy the output file is called .XXX.thy.ML and it then tries to read XXX.ML @@ -14,7 +17,7 @@ children: string list, thy_time: string option, ml_time: string option, - theory: Thm.theory option, + theory: theory option, thms: thm Symtab.table}; signature READTHY = @@ -33,24 +36,25 @@ 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 + val theory_of_sign: Sign.sg -> theory + val theory_of_thm: thm -> theory + val store_thm: string * thm -> thm + val qed: string -> unit + val get_thm: theory -> string -> thm + val thms_of: 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 (make [("Pure", ThyInfo {path = "", children = [], - thy_time = Some "", ml_time = Some "", +val loaded_thys = ref (Symtab.make [("Pure", ThyInfo {path = "", children = [], + thy_time = Some "", ml_time = Some "", theory = Some pure_thy, - thms = null})]); + thms = Symtab.null})]); val loadpath = ref ["."]; (*default search path for theory files *) @@ -61,10 +65,10 @@ (*Read a file specified by thy_file containing theory thy *) fun read_thy tname thy_file = - let + let val instream = open_in thy_file; val outstream = open_out (out_name tname); - in + in output (outstream, ThySyn.parse tname (input (instream, 999999))); close_out outstream; close_in instream @@ -75,28 +79,28 @@ handle Io _ => false; (*Get thy_info for a loaded theory *) -fun get_thyinfo tname = lookup (!loaded_thys, tname); +fun get_thyinfo tname = Symtab.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_time, ml_time, ...} = the t - in if is_none thy_time orelse is_none ml_time then false - else true + 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. Return a pair of boolean values for .thy and for .ML *) -fun thy_unchanged thy thy_file ml_file = +fun thy_unchanged thy thy_file ml_file = let val t = get_thyinfo thy in if is_some t then 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_time), + ((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) @@ -112,7 +116,7 @@ let fun find_it (curr :: paths) = if file_exists (tack_on curr name) then tack_on curr name - else + else find_it paths | find_it [] = "" in find_it (!loadpath) end @@ -123,7 +127,7 @@ (*Get absolute pathnames for a new or already loaded theory *) fun get_filenames path name = let fun make_absolute file = - if file = "" then "" else + if file = "" then "" else if hd (explode file) = "/" then file else tack_on (pwd ()) file; fun new_filename () = @@ -143,7 +147,7 @@ ^ "in the following directories: \"" ^ (space_implode "\", \"" searched_dirs) ^ "\"") else (); - (thy_file, ml_file) + (thy_file, ml_file) end; val tinfo = get_thyinfo name; @@ -166,33 +170,33 @@ (*Remove theory from all child lists in loaded_thys *) fun unlink_thy tname = let fun remove (ThyInfo {path, children, thy_time, ml_time, theory, thms}) = - ThyInfo {path = path, children = children \ tname, + 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; + in loaded_thys := Symtab.map remove (!loaded_thys) end; (*Remove a theory from loaded_thys *) fun remove_thy tname = - loaded_thys := make (filter_out (fn (id, _) => id = tname) - (alist_of (!loaded_thys))); + loaded_thys := Symtab.make (filter_out (fn (id, _) => id = tname) + (Symtab.dest (!loaded_thys))); (*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, + let val ThyInfo {path, children, theory, thms, ...} = + the (Symtab.lookup (!loaded_thys, tname)); + in loaded_thys := Symtab.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 tname = +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 +(*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 + 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 children are marked as changed *) fun use_thy name = @@ -200,14 +204,14 @@ 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 tname + val (thy_uptodate, ml_uptodate) = thy_unchanged tname thy_file ml_file; (*Set absolute path for loaded theory *) fun set_path () = - let val ThyInfo {children, thy_time, ml_time, theory, thms, ...} = - the (lookup (!loaded_thys, tname)); - in loaded_thys := update ((tname, + let val ThyInfo {children, thy_time, ml_time, theory, thms, ...} = + the (Symtab.lookup (!loaded_thys, tname)); + in loaded_thys := Symtab.update ((tname, ThyInfo {path = abs_path, children = children, thy_time = thy_time, ml_time = ml_time, theory = theory, thms = thms}), @@ -229,15 +233,15 @@ (*Remove all theorems associated with a theory*) fun delete_thms () = - let val tinfo = case lookup (!loaded_thys, tname) of + let val tinfo = case Symtab.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} + theory = theory, thms = Symtab.null} | None => ThyInfo {path = "", children = [], thy_time = None, ml_time = None, - theory = None, thms = null}; - in loaded_thys := update ((tname, tinfo), !loaded_thys) end; + theory = None, thms = Symtab.null}; + in loaded_thys := Symtab.update ((tname, tinfo), !loaded_thys) end; in if thy_uptodate andalso ml_uptodate then () else ( @@ -249,7 +253,7 @@ use (out_name tname) ); - if ml_file = "" then () + if ml_file = "" then () else (writeln ("Reading \"" ^ name ^ ".ML\""); use ml_file); @@ -263,14 +267,14 @@ mark_children tname; (*Remove temporary files*) - if not (!delete_tmpfiles) orelse (thy_file = "") orelse thy_uptodate + if not (!delete_tmpfiles) orelse (thy_file = "") orelse thy_uptodate then () else delete_file (out_name tname) ) end; fun time_use_thy tname = timeit(fn()=> - (writeln("\n**** Starting Theory " ^ tname ^ " ****"); + (writeln("\n**** Starting Theory " ^ tname ^ " ****"); use_thy tname; writeln("\n**** Finished Theory " ^ tname ^ " ****")) ); @@ -289,7 +293,7 @@ else next_level ts end | next_level [] = []; - + val children = next_level thys; in load_order children ((result \\ children) @ children) end; @@ -316,13 +320,13 @@ fun collect_garbage not_garbage = let fun collect ((tname, ThyInfo {children, ...}) :: ts) = if tname mem not_garbage then collect ts - else (writeln ("Theory \"" ^ tname + else (writeln ("Theory \"" ^ tname ^ "\" is no longer linked with Pure - removing it."); remove_thy tname; seq mark_outdated children) | collect [] = () - in collect (alist_of (!loaded_thys)) end; + in collect (Symtab.dest (!loaded_thys)) end; in collect_garbage ("Pure" :: (load_order ["Pure"] [])); reload_changed (load_order ["Pure"] []) end; @@ -345,7 +349,7 @@ fun show_cycle base = let fun find_it result curr = let val tinfo = get_thyinfo curr - in if base = curr then + in if base = curr then error ("Cyclic dependency of theories: " ^ child ^ "->" ^ base ^ result) else if is_some tinfo then @@ -355,24 +359,24 @@ else () end in find_it "" child end; - + (*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 val tinfo = - case lookup (!loaded_thys, base) of - Some (ThyInfo {path, children, thy_time, ml_time, + case Symtab.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}; + thy_time = None, ml_time = None, + theory = None, thms = Symtab.null}; in loaded_thys := Symtab.update ((base, tinfo), !loaded_thys) end; (*Load a base theory if not already done @@ -384,7 +388,7 @@ if child = base then error ("Cyclic dependency of theories: " ^ child ^ "->" ^ child) - else + else (find_cycle base; add_child base; if thy_present then () @@ -392,7 +396,7 @@ ^ " (used by " ^ (quote child) ^ ")"); use_thy base) ) - end; + end; (*Load all needed files and make a list of all real theories *) fun load_base (Thy b :: bs) = @@ -413,62 +417,91 @@ in writeln ("Loading theory " ^ (quote child)); merge_thy_list mk_draft (map get_theory mergelist) end; -(*Change theory object for an existent item of loaded_thys +(*Change theory object for an existent item of loaded_thys or create a new item *) fun store_theory (thy, tname) = - let val tinfo = case lookup (!loaded_thys, tname) of + let val tinfo = case Symtab.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}; + theory = Some thy, thms = Symtab.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)); + + +(** store and retrieve theorems **) + +(* thyinfo_of_sign *) + +fun thyinfo_of_sign sg = + let + val ref xname = hd (#stamps (Sign.rep_sg sg)); + val opt_info = get_thyinfo xname; - 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 + fun eq_sg (ThyInfo {theory = None, ...}) = false + | eq_sg (ThyInfo {theory = Some thy, ...}) = Sign.eq_sg (sg, sign_of thy); + + val show_sg = Pretty.str_of o Sign.pretty_sg; + in + if is_some opt_info andalso eq_sg (the opt_info) then + (xname, the opt_info) + else + (case Symtab.find_first (eq_sg o snd) (! loaded_thys) of + Some name_info => name_info + | None => error ("Theory " ^ show_sg sg ^ " not stored by loader")) end; -(*Store theorem in loaded_thys and a ML variable*) -fun qed name = use_string ["val " ^ name ^ " = store_thm (result(), " - ^ quote name ^ ");"]; + +(* theory_of_sign, theory_of_thm *) -fun name_of_thy thy = !(hd (stamps_of_thy thy)); +fun theory_of_sign sg = + (case thyinfo_of_sign sg of + (_, ThyInfo {theory = Some thy, ...}) => thy + | _ => sys_error "theory_of_sign"); -(*Retrieve a theorem specified by theory and name*) -fun get_thm thy tname = - let val thy_name = name_of_thy thy; +val theory_of_thm = theory_of_sign o #sign o rep_thm; + + +(* store theorems *) - 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; +(*store a theorem in the thy_info of its theory*) +fun store_thm (name, thm) = + let + val (thy_name, ThyInfo {path, children, thy_time, ml_time, theory, thms}) = + thyinfo_of_sign (#sign (rep_thm thm)); + val thms' = Symtab.update_new ((name, thm), thms) + handle Symtab.DUPLICATE s => error ("Duplicate theorem name " ^ quote s); + in + loaded_thys := Symtab.update + ((thy_name, ThyInfo {path = path, children = children, + thy_time = thy_time, ml_time = ml_time, theory = theory, thms = thms'}), + ! loaded_thys); + thm + end; + +(*store result of proof in loaded_thys and as ML value*) +fun qed name = + use_string ["val " ^ name ^ " = store_thm (" ^ quote name ^ ", result ());"]; -(*Retrieve all theorems belonging to the specified theory*) -fun get_thms thy = - let val thy_name = name_of_thy thy; + +(* retrieve theorems *) + +fun thmtab thy = + let val (_, ThyInfo {thms, ...}) = thyinfo_of_sign (sign_of thy) + in thms end; - 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; +(*get a stored theorem specified by theory and name*) +fun get_thm thy name = + (case Symtab.lookup (thmtab thy, name) of + Some thm => thm + | None => raise THEORY ("get_thm: no theorem " ^ quote name, [thy])); + +(*get stored theorems of a theory*) +val thms_of = Symtab.dest o thmtab; + + end; +