# HG changeset patch # User wenzelm # Date 877603387 -7200 # Node ID 1030dd79720bf8c33a704b15ee0b1a0481c994b5 # Parent ddeb5a0fd08dfe4193fa4f84b34dd42e14712e65 tuned; diff -r ddeb5a0fd08d -r 1030dd79720b src/Pure/Thy/browser_info.ML --- a/src/Pure/Thy/browser_info.ML Thu Oct 23 12:13:15 1997 +0200 +++ b/src/Pure/Thy/browser_info.ML Thu Oct 23 12:43:07 1997 +0200 @@ -173,7 +173,7 @@ (*Make list of all theories and all theories that own a .thy file*) fun list_theories [] theories thy_files = (theories, thy_files) - | list_theories ((tname, ThyInfo {thy_time, ...}) :: ts) + | list_theories ((tname, {thy_time, ...}: thy_info) :: ts) theories thy_files = list_theories ts (tname :: theories) (if is_some thy_time andalso the thy_time <> "" then @@ -741,7 +741,7 @@ fun mk_graph tname abs_path = if not (!make_graph) then () else let val parents = map (fn (t, _) => tack_on (path_of t) t) - (filter (fn (_, ThyInfo {children,...}) => tname mem children) + (filter (fn (_, {children,...}) => tname mem children) (Symtab.dest(!loaded_thys))); val dir_name = relative_path diff -r ddeb5a0fd08d -r 1030dd79720b src/Pure/Thy/thm_database.ML --- a/src/Pure/Thy/thm_database.ML Thu Oct 23 12:13:15 1997 +0200 +++ b/src/Pure/Thy/thm_database.ML Thu Oct 23 12:43:07 1997 +0200 @@ -273,7 +273,7 @@ and in the theory's HTML file*) fun store_thm (name, thm) = let - val (thy_name, ThyInfo {path, children, parents, thy_time, ml_time, + val (thy_name, {path, children, parents, thy_time, ml_time, theory, thms, methods, data}) = thyinfo_of_sign (#sign (rep_thm thm)) @@ -290,7 +290,7 @@ val thm' = Thm.name_thm (name, thm) in loaded_thys := Symtab.update - ((thy_name, ThyInfo {path = path, children = children, parents = parents, + ((thy_name, {path = path, children = children, parents = parents, thy_time = thy_time, ml_time = ml_time, theory = theory, thms = thms', methods = methods, data = data}), @@ -329,12 +329,12 @@ (*Get all theorems belonging to a given theory*) fun thmtab_of_thy thy = - let val (_, ThyInfo {thms, ...}) = thyinfo_of_sign (sign_of thy); + let val (_, {thms, ...}) = thyinfo_of_sign (sign_of thy); in thms end; fun thmtab_of_name name = - let val ThyInfo {thms, ...} = the (get_thyinfo name); + let val {thms, ...} = the (get_thyinfo name); in thms end; @@ -361,15 +361,15 @@ fun delete_thms tname = let val tinfo = case get_thyinfo tname of - Some (ThyInfo {path, children, parents, thy_time, ml_time, theory, + Some ({path, children, parents, thy_time, ml_time, theory, methods, data, ...}) => - ThyInfo {path = path, children = children, parents = parents, + {path = path, children = children, parents = parents, thy_time = thy_time, ml_time = ml_time, theory = theory, thms = Symtab.null, methods = methods, data = data} | None => error ("Theory " ^ tname ^ " not stored by loader"); - val ThyInfo {theory, ...} = tinfo; + val {theory, ...} = tinfo; in loaded_thys := Symtab.update ((tname, tinfo), !loaded_thys); case theory of Some t => delete_thm_db t diff -r ddeb5a0fd08d -r 1030dd79720b src/Pure/Thy/thy_info.ML --- a/src/Pure/Thy/thy_info.ML Thu Oct 23 12:13:15 1997 +0200 +++ b/src/Pure/Thy/thy_info.ML Thu Oct 23 12:43:07 1997 +0200 @@ -1,27 +1,29 @@ (* Title: Pure/Thy/thy_info.ML ID: $Id$ - Author: Carsten Clasohm and Markus Wenzel and Sonia Mahjoub and - Tobias Nipkow and L C Paulson - Copyright 1994 TU Muenchen + Author: Stefan Berghofer and Markus Wenzel, TU Muenchen -Functions for storing and retrieving arbitrary theory information. +Theory loader info database. *) -(*Types for theory storage*) - +(* FIXME wipe out! *) (*Functions to handle arbitrary data added by the user; type "exn" is used to store data*) datatype thy_methods = ThyMethods of {merge: exn list -> exn, put: exn -> unit, get: unit -> exn}; -datatype thy_info = - ThyInfo of {path: string, - children: string list, parents: string list, - thy_time: string option, ml_time: string option, - theory: theory option, thms: thm Symtab.table, - methods: thy_methods Symtab.table, - data: exn Symtab.table * exn Symtab.table}; - (*thy_time, ml_time = None theory file has not been read yet + +type thy_info = + {path: string, + children: string list, parents: string list, + thy_time: string option, ml_time: string option, + theory: theory option, thms: thm Symtab.table, + methods: thy_methods Symtab.table, + data: exn Symtab.table * exn Symtab.table}; + +(* + path: directory where theory's files are located + + thy_time, ml_time = None theory file has not been read yet = Some "" theory was read but has either been marked as outdated or there is no such file for this theory (see e.g. 'virtual' theories @@ -44,8 +46,7 @@ if ML files has not been read, second element is identical to first one because get_thydata, which is meant to return the latest data, always accesses the 2nd element - *) - +*) signature THY_INFO = sig @@ -57,7 +58,6 @@ val theory_of_thm : thm -> theory val children_of : string -> string list val parents_of_name: string -> string list - val thyname_of_sign: Sign.sg -> string val thyinfo_of_sign: Sign.sg -> string * thy_info val add_thydata : string -> string * thy_methods -> unit @@ -70,111 +70,82 @@ end; - structure ThyInfo: THY_INFO = struct +(* loaded theories *) +fun mk_info (name, children, parents, theory) = + (name, + {path = "", children = children, parents = parents, thy_time = Some "", + ml_time = Some "", theory = Some theory, thms = Symtab.null, + methods = Symtab.null, data = (Symtab.null, Symtab.null)}: thy_info); + +(*preloaded theories*) val loaded_thys = - ref (Symtab.make [("ProtoPure", - ThyInfo {path = "", - children = ["Pure", "CPure"], parents = [], - thy_time = Some "", ml_time = Some "", - theory = Some proto_pure_thy, - thms = Symtab.null, methods = Symtab.null, - data = (Symtab.null, Symtab.null)}), - ("Pure", - ThyInfo {path = "", children = [], - parents = ["ProtoPure"], - thy_time = Some "", ml_time = Some "", - theory = Some pure_thy, thms = Symtab.null, - methods = Symtab.null, - data = (Symtab.null, Symtab.null)}), - ("CPure", - ThyInfo {path = "", - children = [], parents = ["ProtoPure"], - thy_time = Some "", ml_time = Some "", - theory = Some cpure_thy, - thms = Symtab.null, - methods = Symtab.null, - data = (Symtab.null, Symtab.null)}) - ]); + ref (Symtab.make (map mk_info + [("ProtoPure", ["Pure", "CPure"], [], Theory.proto_pure), + ("Pure", [], ["ProtoPure"], Theory.pure), + ("CPure", [], ["ProtoPure"], Theory.cpure)])); -(*Get thy_info for a loaded theory *) -fun get_thyinfo tname = Symtab.lookup (!loaded_thys, tname); +(* retrieve info *) + +fun err_not_stored name = + error ("Theory " ^ name ^ " not stored by loader"); + +fun get_thyinfo name = Symtab.lookup (! loaded_thys, name); -(*Get path where theory's files are located*) -fun path_of tname = - let val ThyInfo {path, ...} = the (get_thyinfo tname) - in path end; +fun the_thyinfo name = + (case get_thyinfo name of + Some info => info + | None => err_not_stored name); + +fun thyinfo_of_sign sg = + let val name = Sign.name_of sg + in (name, the_thyinfo name) end; -(*Guess the name of a theory object - (First the quick way by looking at the stamps; if that doesn't work, - we search loaded_thys for the first theory which fits.) -*) -fun thyname_of_sign sg = - let val ref xname = hd (#stamps (Sign.rep_sg sg)); - val opt_info = get_thyinfo xname; - - 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 - else - (case Symtab.find_first (eq_sg o snd) (!loaded_thys) of - Some (name, _) => name - | None => error ("Theory " ^ show_sg sg ^ " not stored by loader")) - end; - - -(*Guess to which theory a signature belongs and return it's thy_info*) -fun thyinfo_of_sign sg = - let val name = thyname_of_sign sg; - in (name, the (get_thyinfo name)) end; +(*path where theory's files are located*) +val path_of = #path o the_thyinfo; -(*Try to get the theory object corresponding to a given signature*) +(*try to get the theory object corresponding to a given signature*) fun theory_of_sign sg = (case thyinfo_of_sign sg of - (_, ThyInfo {theory = Some thy, ...}) => thy + (_, {theory = Some thy, ...}) => thy | _ => sys_error "theory_of_sign"); +(*try to get the theory object corresponding to a given theorem*) +val theory_of_thm = theory_of_sign o #sign o rep_thm; -(*Try to get the theory object corresponding to a given theorem*) -val theory_of_thm = theory_of_sign o #sign o rep_thm; +(*get all direct descendants of a theory*) +fun children_of t = + (case get_thyinfo t of + Some ({children, ...}) => children + | None => []); + +(*get all direct ancestors of a theory*) +fun parents_of_name t = + (case get_thyinfo t of + Some ({parents, ...}) => parents + | None => []); + +(*get theory object for a loaded theory*) +fun theory_of name = + (case get_thyinfo name of + Some ({theory = Some t, ...}) => t + | _ => err_not_stored name); -(*Get all direct descendants of a theory*) -fun children_of t = - case get_thyinfo t of Some (ThyInfo {children, ...}) => children - | None => []; - - -(*Get all direct ancestors of a theory*) -fun parents_of_name t = - case get_thyinfo t of Some (ThyInfo {parents, ...}) => parents - | None => []; - - -(*Get theory object for a loaded theory *) -fun theory_of name = - case get_thyinfo name of Some (ThyInfo {theory = Some t, ...}) => t - | _ => error ("Theory " ^ name ^ - " not stored by loader"); - - -(*Invoke every put method stored in a theory's methods table to initialize +(*invoke every put method stored in a theory's methods table to initialize the state of user defined variables*) fun put_thydata first tname = let val (methods, data) = case get_thyinfo tname of - Some (ThyInfo {methods, data, ...}) => + Some ({methods, data, ...}) => (methods, Symtab.dest ((if first then fst else snd) data)) - | None => error ("Theory " ^ tname ^ " not stored by loader"); + | None => err_not_stored tname; fun put_data (id, date) = case Symtab.lookup (methods, id) of @@ -190,9 +161,9 @@ (*Change theory object for an existent item of loaded_thys*) fun store_theory (thy, tname) = let val tinfo = case Symtab.lookup (!loaded_thys, tname) of - Some (ThyInfo {path, children, parents, thy_time, ml_time, thms, + Some ({path, children, parents, thy_time, ml_time, thms, methods, data, ...}) => - ThyInfo {path = path, children = children, parents = parents, + {path = path, children = children, parents = parents, thy_time = thy_time, ml_time = ml_time, theory = Some thy, thms = thms, methods = methods, data = data} @@ -204,12 +175,9 @@ (*Add data handling methods to theory*) fun add_thydata tname (new_methods as (id, ThyMethods {get, ...})) = - let val ThyInfo {path, children, parents, thy_time, ml_time, theory, - thms, methods, data} = - case get_thyinfo tname of - Some ti => ti - | None => error ("Theory " ^ tname ^ " not stored by loader"); - in loaded_thys := Symtab.update ((tname, ThyInfo {path = path, + let val {path, children, parents, thy_time, ml_time, theory, + thms, methods, data} = the_thyinfo tname; + in loaded_thys := Symtab.update ((tname, {path = path, children = children, parents = parents, thy_time = thy_time, ml_time = ml_time, theory = theory, thms = thms, methods = Symtab.update (new_methods, methods), data = data}), @@ -217,11 +185,9 @@ end; -(*Retrieve data associated with theory*) -fun get_thydata tname id = - let val d2 = case get_thyinfo tname of - Some (ThyInfo {data, ...}) => snd data - | None => error ("Theory " ^ tname ^ " not stored by loader"); - in Symtab.lookup (d2, id) end; +(*retrieve data associated with theory*) +fun get_thydata name id = + Symtab.lookup (snd (#data (the_thyinfo name)), id); + end; diff -r ddeb5a0fd08d -r 1030dd79720b src/Pure/Thy/thy_read.ML --- a/src/Pure/Thy/thy_read.ML Thu Oct 23 12:13:15 1997 +0200 +++ b/src/Pure/Thy/thy_read.ML Thu Oct 23 12:43:07 1997 +0200 @@ -66,7 +66,7 @@ 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 + else let val {thy_time, ml_time, ...} = the t in is_some thy_time andalso is_some ml_time end end; @@ -75,7 +75,7 @@ Return a pair of boolean values for .thy and for .ML *) fun thy_unchanged thy thy_file ml_file = case get_thyinfo thy of - Some (ThyInfo {thy_time, ml_time, ...}) => + Some {thy_time, ml_time, ...} => let val tn = is_none thy_time; val mn = is_none ml_time in if not tn andalso not mn then @@ -136,7 +136,7 @@ val tinfo = get_thyinfo name; in if is_some tinfo andalso path = "" then - let val ThyInfo {path = abs_path, ...} = the tinfo; + let val {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")) @@ -154,9 +154,9 @@ (*Remove theory from all child lists in loaded_thys *) fun unlink_thy tname = - let fun remove (ThyInfo {path, children, parents, thy_time, ml_time, + let fun remove ({path, children, parents, thy_time, ml_time, theory, thms, methods, data}) = - ThyInfo {path = path, children = children \ tname, parents = parents, + {path = path, children = children \ tname, parents = parents, thy_time = thy_time, ml_time = ml_time, theory = theory, thms = thms, methods = methods, data = data} in loaded_thys := Symtab.map remove (!loaded_thys) end; @@ -171,9 +171,9 @@ (*Change thy_time and ml_time for an existent item *) fun set_info tname thy_time ml_time = let val tinfo = case Symtab.lookup (!loaded_thys, tname) of - Some (ThyInfo {path, children, parents, theory, thms, + Some ({path, children, parents, theory, thms, methods, data, ...}) => - ThyInfo {path = path, children = children, parents = parents, + {path = path, children = children, parents = parents, thy_time = thy_time, ml_time = ml_time, theory = theory, thms = thms, methods = methods, data = data} @@ -186,7 +186,7 @@ let val t = get_thyinfo tname; in if is_none t then () else - let val ThyInfo {thy_time, ml_time, ...} = the t + let val {thy_time, ml_time, ...} = the t in set_info tname (if is_none thy_time then None else Some "") (if is_none ml_time then None else Some "") end @@ -217,11 +217,11 @@ (*Set absolute path for loaded theory *) fun set_path () = - let val ThyInfo {children, parents, thy_time, ml_time, theory, thms, + let val {children, parents, thy_time, ml_time, theory, thms, methods, data, ...} = the (Symtab.lookup (!loaded_thys, tname)); in loaded_thys := Symtab.update ((tname, - ThyInfo {path = abs_path, + {path = abs_path, children = children, parents = parents, thy_time = thy_time, ml_time = ml_time, theory = theory, thms = thms, @@ -245,7 +245,7 @@ (*Invoke every get method stored in the methods table and store result in data table*) fun save_data thy_only = - let val ThyInfo {path, children, parents, thy_time, ml_time, + let val {path, children, parents, thy_time, ml_time, theory, thms, methods, data} = the (get_thyinfo tname); fun get_data [] data = data @@ -257,7 +257,7 @@ val data' = (if thy_only then new_data else fst data, new_data) (* 2nd component must be up to date *) in loaded_thys := Symtab.update - ((tname, ThyInfo {path = path, + ((tname, {path = path, children = children, parents = parents, thy_time = thy_time, ml_time = ml_time, theory = theory, thms = thms, @@ -267,7 +267,7 @@ (*Make sure that loaded_thys contains an entry for tname*) fun init_thyinfo () = - let val tinfo = ThyInfo {path = "", children = [], parents = [], + let val tinfo = {path = "", children = [], parents = [], thy_time = None, ml_time = None, theory = None, thms = Symtab.null, methods = Symtab.null, @@ -372,7 +372,7 @@ fun reload_changed (t :: ts) = let val abspath = case get_thyinfo t of - Some (ThyInfo {path, ...}) => path + Some ({path, ...}) => path | None => ""; val (thy_file, ml_file) = get_filenames abspath t; @@ -388,7 +388,7 @@ If there are still children in the deleted theory's list schedule them for reloading *) fun collect_garbage no_garbage = - let fun collect ((tname, ThyInfo {children, ...}) :: ts) = + let fun collect ((tname, {children, ...}: thy_info) :: ts) = if tname mem no_garbage then collect ts else (writeln ("Theory \"" ^ tname ^ "\" is no longer linked with ProtoPure - removing it."); @@ -413,7 +413,7 @@ error ("Cyclic dependency of theories: " ^ child ^ "->" ^ base ^ result) else if is_some tinfo then - let val ThyInfo {children, ...} = the tinfo + let val {children, ...} = the tinfo in seq (find_it ("->" ^ curr ^ result)) children end else () @@ -429,14 +429,14 @@ fun add_child base = let val tinfo = case Symtab.lookup (!loaded_thys, base) of - Some (ThyInfo {path, children, parents, thy_time, ml_time, + Some ({path, children, parents, thy_time, ml_time, theory, thms, methods, data}) => - ThyInfo {path = path, + {path = path, children = child ins children, parents = parents, thy_time = thy_time, ml_time = ml_time, theory = theory, thms = thms, methods = methods, data = data} - | None => ThyInfo {path = "", children = [child], parents = [], + | None => {path = "", children = [child], parents = [], thy_time = None, ml_time = None, theory = None, thms = Symtab.null, methods = Symtab.null, @@ -480,13 +480,13 @@ val datas = let fun get_data t = - let val ThyInfo {data, ...} = the (get_thyinfo t) + let val {data, ...} = the (get_thyinfo t) in snd data end; in map (Symtab.dest o get_data) mergelist end; val methods = let fun get_methods t = - let val ThyInfo {methods, ...} = the (get_thyinfo t) + let val {methods, ...} = the (get_thyinfo t) in methods end; val ms = map get_methods mergelist; @@ -536,9 +536,9 @@ val dummy = let val tinfo = case Symtab.lookup (!loaded_thys, child) of - Some (ThyInfo {path, children, thy_time, ml_time, theory, thms, + Some ({path, children, thy_time, ml_time, theory, thms, data, ...}) => - ThyInfo {path = path, + {path = path, children = children, parents = mergelist, thy_time = thy_time, ml_time = ml_time, theory = theory, thms = thms,