# HG changeset patch # User wenzelm # Date 878641428 -3600 # Node ID 93baba60ece25d6f6c18a495bfa8a53daffa000a # Parent d7c963600bda813580647989615cd2799b4fd407 removed old thy data stuff; diff -r d7c963600bda -r 93baba60ece2 src/Pure/Thy/thy_info.ML --- a/src/Pure/Thy/thy_info.ML Tue Nov 04 09:27:32 1997 +0100 +++ b/src/Pure/Thy/thy_info.ML Tue Nov 04 12:03:48 1997 +0100 @@ -2,71 +2,44 @@ ID: $Id$ Author: Stefan Berghofer and Markus Wenzel, TU Muenchen -Theory loader info database. +Theory loader database. *) -(* 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}; - - 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}; + theory: theory option}; (* - 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 - like Pure or theories without a ML file) - theory = None theory has not been read yet + path: directory where theory's files are located + (* FIXME do not store absolute path!!! *) - parents: While 'children' contains all theories the theory depends - on (i.e. also ones quoted in the .thy file), - 'parents' only contains the theories which were used to form - the base of this theory. + 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 + like Pure or theories without a ML file) + theory = None theory has not been read yet - methods: three methods for each user defined data; - merge: merges data of ancestor theories - put: retrieves data from loaded_thys and stores it somewhere - get: retrieves data from somewhere and stores it - in loaded_thys - data: user defined data; exn is used to allow arbitrary types; - first element of pairs contains result that get returned after - thy file was read, second element after ML file was read; - 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 + parents: While 'children' contains all theories the theory depends + on (i.e. also ones quoted in the .thy file), + 'parents' only contains the theories which were used to form + the base of this theory. *) signature THY_INFO = sig - val loaded_thys : thy_info Symtab.table ref - val store_theory : theory * string -> unit - - val theory_of : string -> theory - val theory_of_sign : Sign.sg -> theory - val theory_of_thm : thm -> theory - val children_of : string -> string list + val loaded_thys: thy_info Symtab.table ref + val get_thyinfo: string -> thy_info option + val store_theory: theory * string -> unit + val path_of: string -> string + val children_of: string -> string list val parents_of_name: string -> string list val thyinfo_of_sign: Sign.sg -> string * thy_info - - val add_thydata : string -> string * thy_methods -> unit - val get_thydata : string -> string -> exn option - val put_thydata : bool -> string -> unit - val set_current_thy: string -> unit - val get_thyinfo : string -> thy_info option - - val path_of : string -> string + val theory_of: string -> theory + val theory_of_sign: Sign.sg -> theory + val theory_of_thm: thm -> theory end; @@ -76,10 +49,8 @@ (* 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); + (name, {path = "", children = children, parents = parents, + thy_time = Some "", ml_time = Some "", theory = Some theory}: thy_info); (*preloaded theories*) val loaded_thys = @@ -122,72 +93,33 @@ (*get all direct descendants of a theory*) fun children_of t = (case get_thyinfo t of - Some ({children, ...}) => children + Some {children, ...} => children | None => []); (*get all direct ancestors of a theory*) fun parents_of_name t = (case get_thyinfo t of - Some ({parents, ...}) => parents + 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 + Some {theory = Some t, ...} => t | _ => err_not_stored name); -(*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 ({methods, data, ...}) => - (methods, Symtab.dest ((if first then fst else snd) data)) - | None => err_not_stored tname; - - fun put_data (id, date) = - case Symtab.lookup (methods, id) of - Some (ThyMethods {put, ...}) => put date - | None => error ("No method defined for theory data \"" ^ - id ^ "\""); - in seq put_data data end; - - -val set_current_thy = put_thydata false; - +(* store_theory *) -(*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 ({path, children, parents, thy_time, ml_time, thms, - methods, data, ...}) => - {path = path, children = children, parents = parents, - thy_time = thy_time, ml_time = ml_time, - theory = Some thy, thms = thms, - methods = methods, data = data} - | None => error ("store_theory: theory " ^ tname ^ " not found"); - in loaded_thys := Symtab.update ((tname, tinfo), !loaded_thys) end; - - -(*** Misc functions ***) - -(*Add data handling methods to theory*) -fun add_thydata tname (new_methods as (id, ThyMethods {get, ...})) = - 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}), - !loaded_thys) +fun store_theory (thy, name) = + let + val {path, children, parents, thy_time, ml_time, theory = _} = + the_thyinfo name; + val info = {path = path, children = children, parents = parents, + thy_time = thy_time, ml_time = ml_time, theory = Some thy}; + in + loaded_thys := Symtab.update ((name, info), ! loaded_thys) end; -(*retrieve data associated with theory*) -fun get_thydata name id = - Symtab.lookup (snd (#data (the_thyinfo name)), id); - - end; diff -r d7c963600bda -r 93baba60ece2 src/Pure/Thy/thy_read.ML --- a/src/Pure/Thy/thy_read.ML Tue Nov 04 09:27:32 1997 +0100 +++ b/src/Pure/Thy/thy_read.ML Tue Nov 04 12:03:48 1997 +0100 @@ -154,11 +154,9 @@ (*Remove theory from all child lists in loaded_thys *) fun unlink_thy tname = - let fun remove ({path, children, parents, thy_time, ml_time, - theory, thms, methods, data}) = + let fun remove ({path, children, parents, thy_time, ml_time, theory}) = {path = path, children = children \ tname, parents = parents, - thy_time = thy_time, ml_time = ml_time, theory = theory, - thms = thms, methods = methods, data = data} + thy_time = thy_time, ml_time = ml_time, theory = theory} in loaded_thys := Symtab.map remove (!loaded_thys) end; @@ -171,12 +169,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 ({path, children, parents, theory, thms, - methods, data, ...}) => + Some ({path, children, parents, theory, thy_time = _, ml_time = _}) => {path = path, children = children, parents = parents, - thy_time = thy_time, ml_time = ml_time, - theory = theory, thms = thms, - methods = methods, data = data} + thy_time = thy_time, ml_time = ml_time, theory = theory} | None => error ("set_info: theory " ^ tname ^ " not found"); in loaded_thys := Symtab.update ((tname, tinfo), !loaded_thys) end; @@ -217,15 +212,13 @@ (*Set absolute path for loaded theory *) fun set_path () = - let val {children, parents, thy_time, ml_time, theory, thms, - methods, data, ...} = + let val {path = _, children, parents, thy_time, ml_time, theory} = the (Symtab.lookup (!loaded_thys, tname)); in loaded_thys := Symtab.update ((tname, {path = abs_path, children = children, parents = parents, thy_time = thy_time, ml_time = ml_time, - theory = theory, thms = thms, - methods = methods, data = data}), + theory = theory}), !loaded_thys) end; @@ -242,36 +235,11 @@ seq mark_outdated present end; - (*Invoke every get method stored in the methods table and store result in - data table*) - fun save_data thy_only = - let val {path, children, parents, thy_time, ml_time, - theory, thms, methods, data} = the (get_thyinfo tname); - - fun get_data [] data = data - | get_data ((id, ThyMethods {get, ...}) :: ms) data = - get_data ms (Symtab.update ((id, get ()), data)); - - val new_data = get_data (Symtab.dest methods) Symtab.null; - - 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, {path = path, - children = children, parents = parents, - thy_time = thy_time, ml_time = ml_time, - theory = theory, thms = thms, - methods = methods, data = data'}), - !loaded_thys) - end; - (*Make sure that loaded_thys contains an entry for tname*) fun init_thyinfo () = let val tinfo = {path = "", children = [], parents = [], thy_time = None, ml_time = None, - theory = None, thms = Symtab.null, - methods = Symtab.null, - data = (Symtab.null, Symtab.null)}; + theory = None}; in if is_some (get_thyinfo tname) then () else loaded_thys := Symtab.update ((tname, tinfo), !loaded_thys) end; @@ -284,7 +252,6 @@ init_thyinfo (); read_thy tname thy_file; SymbolInput.use (out_name tname); - save_data true; if not (!delete_tmpfiles) then () else OS.FileSys.remove (out_name tname); @@ -298,7 +265,6 @@ if ml_file = "" then () else (writeln ("Reading \"" ^ name ^ ".ML\""); SymbolInput.use ml_file); - save_data false; (*Store theory again because it could have been redefined*) use_strings @@ -417,17 +383,14 @@ let val tinfo = case Symtab.lookup (!loaded_thys, base) of Some ({path, children, parents, thy_time, ml_time, - theory, thms, methods, data}) => + theory}) => {path = path, children = child ins children, parents = parents, thy_time = thy_time, ml_time = ml_time, - theory = theory, thms = thms, - methods = methods, data = data} + theory = theory} | None => {path = "", children = [child], parents = [], thy_time = None, ml_time = None, - theory = None, thms = Symtab.null, - methods = Symtab.null, - data = (Symtab.null, Symtab.null)}; + theory = None}; in loaded_thys := Symtab.update ((base, tinfo), !loaded_thys) end; (*Load a base theory if not already done @@ -466,75 +429,16 @@ if null mergelist then ProtoPure.thy else Theory.prep_ext_merge (map theory_of mergelist)); - val datas = - let fun get_data 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 {methods, ...} = the (get_thyinfo t) - in methods end; - - val ms = map get_methods mergelist; - in if null ms then Symtab.null - else foldl (Symtab.merge (fn (x,y) => true)) (hd ms, tl ms) - end; - - (*merge two sorted association lists*) - fun merge_two ([], d2) = d2 - | merge_two (d1, []) = d1 - | merge_two (l1 as ((p1 as (id1 : string, d1)) :: d1s), - l2 as ((p2 as (id2, d2)) :: d2s)) = - if id1 < id2 then - p1 :: merge_two (d1s, l2) - else - p2 :: merge_two (l1, d2s); - - (*Merge multiple occurence of data; also call put for each merged list*) - fun merge_multi [] None = [] - | merge_multi [] (Some (id, ds)) = - let val ThyMethods {merge, put, ...} = - the (Symtab.lookup (methods, id)); - in put (merge ds); [id] end - | merge_multi ((id, d) :: ds) None = merge_multi ds (Some (id, [d])) - | merge_multi ((id, d) :: ds) (Some (id2, d2s)) = - if id = id2 then - merge_multi ds (Some (id2, d :: d2s)) - else - let val ThyMethods {merge, put, ...} = - the (Symtab.lookup (methods, id2)); - in put (merge d2s); - id2 :: merge_multi ds (Some (id, [d])) - end; - - val merged = - if null datas then [] - else merge_multi (foldl merge_two (hd datas, tl datas)) None; - - val dummy = - let val unmerged = map fst (Symtab.dest methods) \\ merged; - - fun put_empty id = - let val ThyMethods {merge, put, ...} = - the (Symtab.lookup (methods, id)); - in put (merge []) end; - in seq put_empty unmerged end; - val dummy = let val tinfo = case Symtab.lookup (!loaded_thys, child) of - Some ({path, children, thy_time, ml_time, theory, thms, - data, ...}) => - {path = path, - children = children, parents = mergelist, - thy_time = thy_time, ml_time = ml_time, - theory = theory, thms = thms, - methods = methods, data = data} - | None => error ("set_parents: theory " ^ child ^ " not found"); + Some ({path, children, parents = _, thy_time, ml_time, theory}) => + {path = path, children = children, parents = mergelist, + thy_time = thy_time, ml_time = ml_time, theory = theory} + | None => sys_error ("set_parents: theory " ^ child ^ " not found"); in loaded_thys := Symtab.update ((child, tinfo), !loaded_thys) end; - in cur_thyname := child; + in + cur_thyname := child; base_thy end;