removed old thy data stuff;
authorwenzelm
Tue Nov 04 12:03:48 1997 +0100 (1997-11-04)
changeset 411193baba60ece2
parent 4110 d7c963600bda
child 4112 98c8f40f7bbe
removed old thy data stuff;
src/Pure/Thy/thy_info.ML
src/Pure/Thy/thy_read.ML
     1.1 --- a/src/Pure/Thy/thy_info.ML	Tue Nov 04 09:27:32 1997 +0100
     1.2 +++ b/src/Pure/Thy/thy_info.ML	Tue Nov 04 12:03:48 1997 +0100
     1.3 @@ -2,71 +2,44 @@
     1.4      ID:         $Id$
     1.5      Author:     Stefan Berghofer and Markus Wenzel, TU Muenchen
     1.6  
     1.7 -Theory loader info database.
     1.8 +Theory loader database.
     1.9  *)
    1.10  
    1.11 -(* FIXME wipe out! *)
    1.12 -(*Functions to handle arbitrary data added by the user; type "exn" is used
    1.13 -  to store data*)
    1.14 -datatype thy_methods =
    1.15 -  ThyMethods of {merge: exn list -> exn, put: exn -> unit, get: unit -> exn};
    1.16 -
    1.17 -
    1.18  type thy_info =
    1.19    {path: string,
    1.20      children: string list, parents: string list,
    1.21      thy_time: string option, ml_time: string option,
    1.22 -    theory: theory option, thms: thm Symtab.table,
    1.23 -    methods: thy_methods Symtab.table,
    1.24 -    data: exn Symtab.table * exn Symtab.table};
    1.25 +    theory: theory option};
    1.26  
    1.27  (*
    1.28 -        path: directory where theory's files are located
    1.29 -
    1.30 -        thy_time, ml_time = None     theory file has not been read yet
    1.31 -                          = Some ""  theory was read but has either been marked
    1.32 -                                     as outdated or there is no such file for
    1.33 -                                     this theory (see e.g. 'virtual' theories
    1.34 -                                     like Pure or theories without a ML file)
    1.35 -        theory = None  theory has not been read yet
    1.36 +  path: directory where theory's files are located
    1.37 +	(* FIXME do not store absolute path!!! *)
    1.38  
    1.39 -        parents: While 'children' contains all theories the theory depends
    1.40 -                 on (i.e. also ones quoted in the .thy file),
    1.41 -                 'parents' only contains the theories which were used to form
    1.42 -                 the base of this theory.
    1.43 +  thy_time, ml_time = None     theory file has not been read yet
    1.44 +                    = Some ""  theory was read but has either been marked
    1.45 +                               as outdated or there is no such file for
    1.46 +                               this theory (see e.g. 'virtual' theories
    1.47 +                               like Pure or theories without a ML file)
    1.48 +  theory = None  theory has not been read yet
    1.49  
    1.50 -        methods: three methods for each user defined data;
    1.51 -                 merge: merges data of ancestor theories
    1.52 -                 put: retrieves data from loaded_thys and stores it somewhere
    1.53 -                 get: retrieves data from somewhere and stores it
    1.54 -                      in loaded_thys
    1.55 -        data: user defined data; exn is used to allow arbitrary types;
    1.56 -              first element of pairs contains result that get returned after
    1.57 -              thy file was read, second element after ML file was read;
    1.58 -              if ML files has not been read, second element is identical to
    1.59 -              first one because get_thydata, which is meant to return the
    1.60 -              latest data, always accesses the 2nd element
    1.61 +  parents: While 'children' contains all theories the theory depends
    1.62 +           on (i.e. also ones quoted in the .thy file),
    1.63 +           'parents' only contains the theories which were used to form
    1.64 +           the base of this theory.
    1.65  *)
    1.66  
    1.67  signature THY_INFO =
    1.68  sig
    1.69 -  val loaded_thys    : thy_info Symtab.table ref
    1.70 -  val store_theory   : theory * string -> unit
    1.71 -
    1.72 -  val theory_of      : string -> theory
    1.73 -  val theory_of_sign : Sign.sg -> theory
    1.74 -  val theory_of_thm  : thm -> theory
    1.75 -  val children_of    : string -> string list
    1.76 +  val loaded_thys: thy_info Symtab.table ref
    1.77 +  val get_thyinfo: string -> thy_info option
    1.78 +  val store_theory: theory * string -> unit
    1.79 +  val path_of: string -> string
    1.80 +  val children_of: string -> string list
    1.81    val parents_of_name: string -> string list
    1.82    val thyinfo_of_sign: Sign.sg -> string * thy_info
    1.83 -
    1.84 -  val add_thydata    : string -> string * thy_methods -> unit
    1.85 -  val get_thydata    : string -> string -> exn option
    1.86 -  val put_thydata    : bool -> string -> unit
    1.87 -  val set_current_thy: string -> unit
    1.88 -  val get_thyinfo    : string -> thy_info option
    1.89 -
    1.90 -  val path_of        : string -> string
    1.91 +  val theory_of: string -> theory
    1.92 +  val theory_of_sign: Sign.sg -> theory
    1.93 +  val theory_of_thm: thm -> theory
    1.94  end;
    1.95  
    1.96  
    1.97 @@ -76,10 +49,8 @@
    1.98  (* loaded theories *)
    1.99  
   1.100  fun mk_info (name, children, parents, theory) =
   1.101 -  (name,
   1.102 -    {path = "", children = children, parents = parents, thy_time = Some "",
   1.103 -      ml_time = Some "", theory = Some theory, thms = Symtab.null,
   1.104 -      methods = Symtab.null, data = (Symtab.null, Symtab.null)}: thy_info);
   1.105 +  (name, {path = "", children = children, parents = parents,
   1.106 +    thy_time = Some "", ml_time = Some "", theory = Some theory}: thy_info);
   1.107  
   1.108  (*preloaded theories*)
   1.109  val loaded_thys =
   1.110 @@ -122,72 +93,33 @@
   1.111  (*get all direct descendants of a theory*)
   1.112  fun children_of t =
   1.113    (case get_thyinfo t of
   1.114 -    Some ({children, ...}) => children
   1.115 +    Some {children, ...} => children
   1.116    | None => []);
   1.117  
   1.118  (*get all direct ancestors of a theory*)
   1.119  fun parents_of_name t =
   1.120    (case get_thyinfo t of
   1.121 -    Some ({parents, ...}) => parents
   1.122 +    Some {parents, ...} => parents
   1.123    | None => []);
   1.124  
   1.125  (*get theory object for a loaded theory*)
   1.126  fun theory_of name =
   1.127    (case get_thyinfo name of
   1.128 -    Some ({theory = Some t, ...}) => t
   1.129 +    Some {theory = Some t, ...} => t
   1.130    | _ => err_not_stored name);
   1.131  
   1.132  
   1.133 -(*invoke every put method stored in a theory's methods table to initialize
   1.134 -  the state of user defined variables*)
   1.135 -fun put_thydata first tname =
   1.136 -  let val (methods, data) = 
   1.137 -        case get_thyinfo tname of
   1.138 -            Some ({methods, data, ...}) =>
   1.139 -              (methods, Symtab.dest ((if first then fst else snd) data))
   1.140 -          | None => err_not_stored tname;
   1.141 -
   1.142 -      fun put_data (id, date) =
   1.143 -            case Symtab.lookup (methods, id) of
   1.144 -                Some (ThyMethods {put, ...}) => put date
   1.145 -              | None => error ("No method defined for theory data \"" ^
   1.146 -                               id ^ "\"");
   1.147 -  in seq put_data data end;
   1.148 -
   1.149 -
   1.150 -val set_current_thy = put_thydata false;
   1.151 -
   1.152 +(* store_theory *)
   1.153  
   1.154 -(*Change theory object for an existent item of loaded_thys*)
   1.155 -fun store_theory (thy, tname) =
   1.156 -  let val tinfo = case Symtab.lookup (!loaded_thys, tname) of
   1.157 -               Some ({path, children, parents, thy_time, ml_time, thms,
   1.158 -                              methods, data, ...}) =>
   1.159 -                 {path = path, children = children, parents = parents,
   1.160 -                          thy_time = thy_time, ml_time = ml_time,
   1.161 -                          theory = Some thy, thms = thms,
   1.162 -                          methods = methods, data = data}
   1.163 -             | None => error ("store_theory: theory " ^ tname ^ " not found");
   1.164 -  in loaded_thys := Symtab.update ((tname, tinfo), !loaded_thys) end;
   1.165 -
   1.166 -
   1.167 -(*** Misc functions ***)
   1.168 -
   1.169 -(*Add data handling methods to theory*)
   1.170 -fun add_thydata tname (new_methods as (id, ThyMethods {get, ...})) =
   1.171 -  let val {path, children, parents, thy_time, ml_time, theory,
   1.172 -                   thms, methods, data} = the_thyinfo tname;
   1.173 -  in loaded_thys := Symtab.update ((tname, {path = path,
   1.174 -       children = children, parents = parents, thy_time = thy_time,
   1.175 -       ml_time = ml_time, theory = theory, thms = thms,
   1.176 -       methods = Symtab.update (new_methods, methods), data = data}),
   1.177 -       !loaded_thys)
   1.178 +fun store_theory (thy, name) =
   1.179 +  let
   1.180 +    val {path, children, parents, thy_time, ml_time, theory = _} =
   1.181 +      the_thyinfo name;
   1.182 +    val info = {path = path, children = children, parents = parents,
   1.183 +      thy_time = thy_time, ml_time = ml_time, theory = Some thy};
   1.184 +  in
   1.185 +    loaded_thys := Symtab.update ((name, info), ! loaded_thys)
   1.186    end;
   1.187  
   1.188  
   1.189 -(*retrieve data associated with theory*)
   1.190 -fun get_thydata name id =
   1.191 -  Symtab.lookup (snd (#data (the_thyinfo name)), id);
   1.192 -
   1.193 -
   1.194  end;
     2.1 --- a/src/Pure/Thy/thy_read.ML	Tue Nov 04 09:27:32 1997 +0100
     2.2 +++ b/src/Pure/Thy/thy_read.ML	Tue Nov 04 12:03:48 1997 +0100
     2.3 @@ -154,11 +154,9 @@
     2.4  
     2.5  (*Remove theory from all child lists in loaded_thys *)
     2.6  fun unlink_thy tname =
     2.7 -  let fun remove ({path, children, parents, thy_time, ml_time,
     2.8 -                           theory, thms, methods, data}) =
     2.9 +  let fun remove ({path, children, parents, thy_time, ml_time, theory}) =
    2.10          {path = path, children = children \ tname, parents = parents,
    2.11 -                 thy_time = thy_time, ml_time = ml_time, theory = theory, 
    2.12 -                 thms = thms, methods = methods, data = data}
    2.13 +                 thy_time = thy_time, ml_time = ml_time, theory = theory}
    2.14    in loaded_thys := Symtab.map remove (!loaded_thys) end;
    2.15  
    2.16  
    2.17 @@ -171,12 +169,9 @@
    2.18  (*Change thy_time and ml_time for an existent item *)
    2.19  fun set_info tname thy_time ml_time =
    2.20    let val tinfo = case Symtab.lookup (!loaded_thys, tname) of
    2.21 -          Some ({path, children, parents, theory, thms,
    2.22 -                         methods, data, ...}) =>
    2.23 +          Some ({path, children, parents, theory, thy_time = _, ml_time = _}) =>
    2.24              {path = path, children = children, parents = parents,
    2.25 -                     thy_time = thy_time, ml_time = ml_time,
    2.26 -                     theory = theory, thms = thms,
    2.27 -                     methods = methods, data = data}
    2.28 +                     thy_time = thy_time, ml_time = ml_time, theory = theory}
    2.29          | None => error ("set_info: theory " ^ tname ^ " not found");
    2.30    in loaded_thys := Symtab.update ((tname, tinfo), !loaded_thys) end;
    2.31  
    2.32 @@ -217,15 +212,13 @@
    2.33  
    2.34      (*Set absolute path for loaded theory *)
    2.35      fun set_path () =
    2.36 -      let val {children, parents, thy_time, ml_time, theory, thms,
    2.37 -                       methods, data, ...} =
    2.38 +      let val {path = _, children, parents, thy_time, ml_time, theory} =
    2.39              the (Symtab.lookup (!loaded_thys, tname));
    2.40        in loaded_thys := Symtab.update ((tname,
    2.41                            {path = abs_path,
    2.42                                     children = children, parents = parents,
    2.43                                     thy_time = thy_time, ml_time = ml_time,
    2.44 -                                   theory = theory, thms = thms,
    2.45 -                                   methods = methods, data = data}),
    2.46 +                                   theory = theory}),
    2.47                            !loaded_thys)
    2.48        end;
    2.49  
    2.50 @@ -242,36 +235,11 @@
    2.51           seq mark_outdated present
    2.52        end;
    2.53  
    2.54 -    (*Invoke every get method stored in the methods table and store result in
    2.55 -      data table*)
    2.56 -    fun save_data thy_only =
    2.57 -      let val {path, children, parents, thy_time, ml_time,
    2.58 -                       theory, thms, methods, data} = the (get_thyinfo tname);
    2.59 -
    2.60 -          fun get_data [] data = data
    2.61 -            | get_data ((id, ThyMethods {get, ...}) :: ms) data =
    2.62 -                get_data ms (Symtab.update ((id, get ()), data));
    2.63 -
    2.64 -          val new_data = get_data (Symtab.dest methods) Symtab.null;
    2.65 -
    2.66 -          val data' = (if thy_only then new_data else fst data, new_data)
    2.67 -                      (* 2nd component must be up to date *)
    2.68 -      in loaded_thys := Symtab.update
    2.69 -           ((tname, {path = path,
    2.70 -                             children = children, parents = parents,
    2.71 -                             thy_time = thy_time, ml_time = ml_time,
    2.72 -                             theory = theory, thms = thms,
    2.73 -                             methods = methods, data = data'}),
    2.74 -            !loaded_thys)
    2.75 -      end;
    2.76 -
    2.77      (*Make sure that loaded_thys contains an entry for tname*)
    2.78      fun init_thyinfo () =
    2.79      let val tinfo = {path = "", children = [], parents = [],
    2.80                               thy_time = None, ml_time = None,
    2.81 -                             theory = None, thms = Symtab.null,
    2.82 -                             methods = Symtab.null,
    2.83 -                             data = (Symtab.null, Symtab.null)};
    2.84 +                             theory = None};
    2.85      in if is_some (get_thyinfo tname) then ()
    2.86         else loaded_thys := Symtab.update ((tname, tinfo), !loaded_thys)
    2.87      end;
    2.88 @@ -284,7 +252,6 @@
    2.89            init_thyinfo ();
    2.90            read_thy tname thy_file;
    2.91            SymbolInput.use (out_name tname);
    2.92 -          save_data true;
    2.93  
    2.94            if not (!delete_tmpfiles) then ()
    2.95            else OS.FileSys.remove (out_name tname);
    2.96 @@ -298,7 +265,6 @@
    2.97         if ml_file = "" then ()
    2.98         else (writeln ("Reading \"" ^ name ^ ".ML\"");
    2.99               SymbolInput.use ml_file);
   2.100 -       save_data false;
   2.101  
   2.102         (*Store theory again because it could have been redefined*)
   2.103         use_strings
   2.104 @@ -417,17 +383,14 @@
   2.105          let val tinfo =
   2.106                case Symtab.lookup (!loaded_thys, base) of
   2.107                    Some ({path, children, parents, thy_time, ml_time,
   2.108 -                           theory, thms, methods, data}) =>
   2.109 +                           theory}) =>
   2.110                      {path = path,
   2.111                               children = child ins children, parents = parents,
   2.112                               thy_time = thy_time, ml_time = ml_time,
   2.113 -                             theory = theory, thms = thms,
   2.114 -                             methods = methods, data = data}
   2.115 +                             theory = theory}
   2.116                  | None => {path = "", children = [child], parents = [],
   2.117                                     thy_time = None, ml_time = None,
   2.118 -                                   theory = None, thms = Symtab.null,
   2.119 -                                   methods = Symtab.null,
   2.120 -                                   data = (Symtab.null, Symtab.null)};
   2.121 +                                   theory = None};
   2.122          in loaded_thys := Symtab.update ((base, tinfo), !loaded_thys) end;
   2.123  
   2.124        (*Load a base theory if not already done
   2.125 @@ -466,75 +429,16 @@
   2.126           if null mergelist then ProtoPure.thy
   2.127           else Theory.prep_ext_merge (map theory_of mergelist));
   2.128  
   2.129 -      val datas =
   2.130 -        let fun get_data t =
   2.131 -              let val {data, ...} = the (get_thyinfo t)
   2.132 -              in snd data end;
   2.133 -        in map (Symtab.dest o get_data) mergelist end;
   2.134 -
   2.135 -      val methods =
   2.136 -        let fun get_methods t =
   2.137 -              let val {methods, ...} = the (get_thyinfo t)
   2.138 -              in methods end;
   2.139 -
   2.140 -            val ms = map get_methods mergelist;
   2.141 -        in if null ms then Symtab.null
   2.142 -           else foldl (Symtab.merge (fn (x,y) => true)) (hd ms, tl ms)
   2.143 -        end;
   2.144 -
   2.145 -      (*merge two sorted association lists*)
   2.146 -      fun merge_two ([], d2) = d2
   2.147 -        | merge_two (d1, []) = d1
   2.148 -        | merge_two (l1 as ((p1 as (id1 : string, d1)) :: d1s),
   2.149 -                     l2 as ((p2 as (id2, d2)) :: d2s)) =
   2.150 -            if id1 < id2 then
   2.151 -              p1 :: merge_two (d1s, l2)
   2.152 -            else
   2.153 -              p2 :: merge_two (l1, d2s);
   2.154 -
   2.155 -      (*Merge multiple occurence of data; also call put for each merged list*)
   2.156 -      fun merge_multi [] None = []
   2.157 -        | merge_multi [] (Some (id, ds)) =
   2.158 -            let val ThyMethods {merge, put, ...} =
   2.159 -                  the (Symtab.lookup (methods, id));
   2.160 -             in put (merge ds); [id] end
   2.161 -        | merge_multi ((id, d) :: ds) None = merge_multi ds (Some (id, [d]))
   2.162 -        | merge_multi ((id, d) :: ds) (Some (id2, d2s)) =
   2.163 -            if id = id2 then
   2.164 -              merge_multi ds (Some (id2, d :: d2s))
   2.165 -            else
   2.166 -              let val ThyMethods {merge, put, ...} =
   2.167 -                    the (Symtab.lookup (methods, id2));
   2.168 -              in put (merge d2s);
   2.169 -                 id2 :: merge_multi ds (Some (id, [d]))
   2.170 -              end;
   2.171 -
   2.172 -      val merged =
   2.173 -        if null datas then []
   2.174 -        else merge_multi (foldl merge_two (hd datas, tl datas)) None;
   2.175 -
   2.176 -      val dummy =
   2.177 -        let val unmerged = map fst (Symtab.dest methods) \\ merged;
   2.178 -
   2.179 -            fun put_empty id =
   2.180 -              let val ThyMethods {merge, put, ...} =
   2.181 -                    the (Symtab.lookup (methods, id));
   2.182 -              in put (merge []) end;
   2.183 -        in seq put_empty unmerged end;
   2.184 -
   2.185        val dummy =
   2.186          let val tinfo = case Symtab.lookup (!loaded_thys, child) of
   2.187 -              Some ({path, children, thy_time, ml_time, theory, thms,
   2.188 -                             data, ...}) =>
   2.189 -                 {path = path,
   2.190 -                          children = children, parents = mergelist,
   2.191 -                          thy_time = thy_time, ml_time = ml_time,
   2.192 -                          theory = theory, thms = thms,
   2.193 -                          methods = methods, data = data}
   2.194 -             | None => error ("set_parents: theory " ^ child ^ " not found");
   2.195 +              Some ({path, children, parents = _, thy_time, ml_time, theory}) =>
   2.196 +                 {path = path, children = children, parents = mergelist,
   2.197 +                   thy_time = thy_time, ml_time = ml_time, theory = theory}
   2.198 +             | None => sys_error ("set_parents: theory " ^ child ^ " not found");
   2.199          in loaded_thys := Symtab.update ((child, tinfo), !loaded_thys) end;
   2.200  
   2.201 - in cur_thyname := child;
   2.202 + in
   2.203 +    cur_thyname := child;
   2.204      base_thy
   2.205   end;
   2.206