Theory loader database: theory and file dependencies, theory values
authorwenzelm
Wed Feb 03 17:29:48 1999 +0100 (1999-02-03)
changeset 621143d0efafa025
parent 6210 465cae203337
child 6212 974310f9ca7d
Theory loader database: theory and file dependencies, theory values
and user data.
src/Pure/Thy/thy_info.ML
     1.1 --- a/src/Pure/Thy/thy_info.ML	Wed Feb 03 17:29:12 1999 +0100
     1.2 +++ b/src/Pure/Thy/thy_info.ML	Wed Feb 03 17:29:48 1999 +0100
     1.3 @@ -1,132 +1,350 @@
     1.4  (*  Title:      Pure/Thy/thy_info.ML
     1.5      ID:         $Id$
     1.6 -    Author:     Stefan Berghofer and Markus Wenzel, TU Muenchen
     1.7 -
     1.8 -Theory loader database.
     1.9 -*)
    1.10 +    Author:     Markus Wenzel, TU Muenchen
    1.11  
    1.12 -type thy_info =
    1.13 -  {path: string,
    1.14 -    children: string list, parents: string list,
    1.15 -    thy_time: string option, ml_time: string option,
    1.16 -    theory: theory option};
    1.17 +Theory loader database: theory and file dependencies, theory values
    1.18 +and user data.
    1.19  
    1.20 -(*
    1.21 -  path: directory where theory's files are located
    1.22 -	(* FIXME do not store absolute path!!! *)
    1.23 -
    1.24 -  thy_time, ml_time = None     theory file has not been read yet
    1.25 -                    = Some ""  theory was read but has either been marked
    1.26 -                               as outdated or there is no such file for
    1.27 -                               this theory (see e.g. 'virtual' theories
    1.28 -                               like Pure or theories without a ML file)
    1.29 -  theory = None  theory has not been read yet
    1.30 -
    1.31 -  parents: While 'children' contains all theories the theory depends
    1.32 -           on (i.e. also ones quoted in the .thy file),
    1.33 -           'parents' only contains the theories which were used to form
    1.34 -           the base of this theory.
    1.35 +TODO:
    1.36 +  - check_thy: include ML stamp (!?!?);
    1.37 +  - check all these versions of 'use' (!!);
    1.38 +  - errors during require etc.: include initiators (!?);
    1.39 +  - data: ThyInfoFun;
    1.40 +  - remove operation (GC!?);
    1.41 +  - update_all operation (!?);
    1.42 +  - put_theory:
    1.43 +      . include data;
    1.44 +      . allow for undef entry only;
    1.45 +      . elim (via theory_ref);
    1.46 +  - stronger handling of missing files (!?!?);
    1.47 +  - register_theory: do not require finished parents (!?) (no?);
    1.48 +  - observe verbose flag;
    1.49  *)
    1.50  
    1.51  signature BASIC_THY_INFO =
    1.52  sig
    1.53    val theory: string -> theory
    1.54 -end
    1.55 +  val theory_of_sign: Sign.sg -> theory
    1.56 +  val theory_of_thm: thm -> theory
    1.57 +  val touch_thy: string -> unit
    1.58 +  val use_thy: string -> unit
    1.59 +  val update_thy: string -> unit
    1.60 +  val time_use_thy: string -> unit
    1.61 +end;
    1.62  
    1.63  signature THY_INFO =
    1.64  sig
    1.65    include BASIC_THY_INFO
    1.66 -  val mk_info: string * string list * string list * theory -> string * thy_info
    1.67 -  val loaded_thys: thy_info Symtab.table ref
    1.68 -  val get_thyinfo: string -> thy_info option
    1.69 -  val store_theory: theory -> unit
    1.70 -  val path_of: string -> string
    1.71 -  val children_of: string -> string list
    1.72 -  val parents_of_name: string -> string list
    1.73 -  val thyinfo_of_sign: Sign.sg -> string * thy_info
    1.74 -  val theory_of_sign: Sign.sg -> theory
    1.75 -  val theory_of_thm: thm -> theory
    1.76 +  val verbose: bool ref
    1.77 +  val names: unit -> string list
    1.78 +  val get_theory: string -> theory
    1.79 +  val put_theory: theory -> unit
    1.80 +  val load_file: Path.T -> unit
    1.81 +  val use_thy_only: string -> unit
    1.82 +  val begin_theory: string -> string list -> theory
    1.83 +  val end_theory: theory -> theory
    1.84 +  val finish_all: unit -> unit
    1.85 +  val register_theory: theory -> unit
    1.86  end;
    1.87  
    1.88 -
    1.89 -structure ThyInfo: THY_INFO =
    1.90 -struct
    1.91 -
    1.92 -(* loaded theories *)
    1.93 -
    1.94 -fun mk_info (name, children, parents, theory) =
    1.95 -  (name, {path = "", children = children, parents = parents,
    1.96 -    thy_time = Some "", ml_time = Some "", theory = Some theory}: thy_info);
    1.97 -
    1.98 -(*preloaded theories*)
    1.99 -val loaded_thys = ref (Symtab.empty: thy_info Symtab.table);
   1.100 -
   1.101 +signature PRIVATE_THY_INFO =
   1.102 +sig
   1.103 +  include THY_INFO
   1.104 +(* FIXME
   1.105 +  val init_data: Object.kind -> (Object.T * (Object.T -> Object.T) *
   1.106 +    (Object.T * Object.T -> Object.T) * (Sign.sg -> Object.T -> unit)) -> unit
   1.107 +  val print_data: Object.kind -> string -> unit
   1.108 +  val get_data: Object.kind -> (Object.T -> 'a) -> string -> 'a
   1.109 +  val put_data: Object.kind -> ('a -> Object.T) -> 'a -> unit
   1.110 +*)
   1.111 +end;
   1.112  
   1.113 -(* retrieve info *)
   1.114 -
   1.115 -fun err_not_stored name =
   1.116 -  error ("Theory " ^ quote name ^ " not stored by loader");
   1.117 -
   1.118 -fun get_thyinfo name = Symtab.lookup (! loaded_thys, name);
   1.119 -
   1.120 -fun the_thyinfo name =
   1.121 -  (case get_thyinfo name of
   1.122 -    Some info => info
   1.123 -  | None => err_not_stored name);
   1.124 -
   1.125 -fun thyinfo_of_sign sg =
   1.126 -  let val name = Sign.name_of sg
   1.127 -  in (name, the_thyinfo name) end;
   1.128 +structure ThyInfo: PRIVATE_THY_INFO =
   1.129 +struct
   1.130  
   1.131  
   1.132 -(*path where theory's files are located*)
   1.133 -val path_of = #path o the_thyinfo;
   1.134 +(** thy database **)
   1.135 +
   1.136 +(* messages *)
   1.137 +
   1.138 +val verbose = ref false;
   1.139 +
   1.140 +fun gen_msg txt [] = txt
   1.141 +  | gen_msg txt names = txt ^ " " ^ commas_quote names;
   1.142 +
   1.143 +fun loader_msg txt names = gen_msg ("Theory loader: " ^ txt) names;
   1.144 +
   1.145 +val show_path = space_implode " via " o map quote;
   1.146 +fun cycle_msg name names = loader_msg ("cyclic dependency of " ^ show_path (name :: names)) [];
   1.147  
   1.148  
   1.149 -(*try to get the theory object corresponding to a given signature*)
   1.150 -fun theory_of_sign sg =
   1.151 -  (case thyinfo_of_sign sg of
   1.152 -    (_, {theory = Some thy, ...}) => thy
   1.153 -  | _ => sys_error "theory_of_sign");
   1.154 +(* derived graph operations *)		(* FIXME more abstract (!?) *)
   1.155  
   1.156 -(*try to get the theory object corresponding to a given theorem*)
   1.157 -val theory_of_thm = theory_of_sign o #sign o rep_thm;
   1.158 +fun add_deps name parents G =
   1.159 +  foldl (fn (H, parent) => Graph.add_edge_acyclic (parent, name) H) (G, parents)
   1.160 +    handle Graph.CYCLES namess => error (cat_lines (map (cycle_msg name) namess));
   1.161  
   1.162 -(*get all direct descendants of a theory*)
   1.163 -fun children_of t =
   1.164 -  (case get_thyinfo t of
   1.165 -    Some {children, ...} => children
   1.166 -  | None => []);
   1.167 +fun del_deps name G =           (* FIXME GC (!?!?) *)
   1.168 +  foldl (fn (H, parent) => Graph.del_edge (parent, name) H) (G, Graph.imm_preds G name);
   1.169  
   1.170 -(*get all direct ancestors of a theory*)
   1.171 -fun parents_of_name t =
   1.172 -  (case get_thyinfo t of
   1.173 -    Some {parents, ...} => parents
   1.174 -  | None => []);
   1.175 -
   1.176 -(*get theory object for a loaded theory*)
   1.177 -fun theory name =
   1.178 -  (case get_thyinfo name of
   1.179 -    Some {theory = Some t, ...} => t
   1.180 -  | _ => err_not_stored name);
   1.181 +fun update_node name parents entry G =
   1.182 +  add_deps name parents
   1.183 +    (if can (Graph.get_node G) name then del_deps name G else Graph.new_node (name, entry) G);
   1.184  
   1.185  
   1.186 -(* store_theory *)
   1.187 +(* thy database *)
   1.188 +
   1.189 +type deps =
   1.190 +  {present: bool, outdated: bool,
   1.191 +    master: File.info option, files: (Path.T * File.info option) list} option;
   1.192 +
   1.193 +fun make_depends present outdated master files =
   1.194 +  Some {present = present, outdated = outdated, master = master, files = files}: deps;
   1.195  
   1.196 -fun store_theory thy =
   1.197 -  let
   1.198 -    val name = PureThy.get_name thy;
   1.199 -    val {path, children, parents, thy_time, ml_time, theory = _} =
   1.200 -      the_thyinfo name;
   1.201 -    val info = {path = path, children = children, parents = parents,
   1.202 -      thy_time = thy_time, ml_time = ml_time, theory = Some thy};
   1.203 -  in
   1.204 -    loaded_thys := Symtab.update ((name, info), ! loaded_thys)
   1.205 -  end;
   1.206 +type thy = deps * (theory * Object.T Symtab.table) option;
   1.207 +type kind = Object.kind * (Object.T * (Object.T -> unit));
   1.208 +
   1.209  
   1.210 +local
   1.211 +  val database = ref (Graph.empty: thy Graph.T, Symtab.empty: kind Symtab.table);
   1.212 +in
   1.213 +
   1.214 +fun get_thys () = #1 (! database);
   1.215 +fun get_kinds () = #2 (! database);
   1.216 +fun change_thys f = database := (f (get_thys ()), get_kinds ());
   1.217 +fun change_kinds f = database := (get_thys (), f (get_kinds ()));
   1.218  
   1.219  end;
   1.220  
   1.221  
   1.222 +(* access thy graph *)
   1.223 +
   1.224 +fun thy_graph f x = f (get_thys ()) x;
   1.225 +fun get_names () = map #1 (Graph.get_nodes (get_thys ()));
   1.226 +
   1.227 +
   1.228 +(* access thy *)
   1.229 +
   1.230 +fun lookup_thy name = Some (thy_graph Graph.get_node name) handle Graph.UNDEFINED _ => None;
   1.231 +
   1.232 +fun get_thy name =
   1.233 +  (case lookup_thy name of
   1.234 +    Some thy => thy
   1.235 +  | None => error (loader_msg "nothing known about theory" [name]));
   1.236 +
   1.237 +fun change_thy name f = (get_thy name; change_thys (Graph.map_node name f));
   1.238 +
   1.239 +
   1.240 +(* access deps *)
   1.241 +
   1.242 +val lookup_deps = apsome #1 o lookup_thy;
   1.243 +val get_deps = #1 o get_thy;
   1.244 +fun change_deps name f = change_thy name (fn (deps, x) => (f deps, x));
   1.245 +
   1.246 +fun get_files name = (case get_deps name of Some {files, ...} => files | _ => []);
   1.247 +fun is_finished name = is_none (get_deps name);
   1.248 +
   1.249 +
   1.250 +(* access theory *)
   1.251 +
   1.252 +fun get_theory name =
   1.253 +  (case get_thy name of
   1.254 +    (_, Some (theory, _)) => theory
   1.255 +  | _ => error (loader_msg "undefined theory entry for" [name]));
   1.256 +
   1.257 +val theory_of_sign = get_theory o Sign.name_of;
   1.258 +val theory_of_thm = theory_of_sign o Thm.sign_of_thm;
   1.259 +
   1.260 +fun put_theory theory =
   1.261 +  change_thy (PureThy.get_name theory) (fn (deps, _) => (deps, (Some (theory, Symtab.empty))));
   1.262 +
   1.263 +
   1.264 +
   1.265 +(** thy data **)  (* FIXME *)
   1.266 +
   1.267 +
   1.268 +
   1.269 +(** thy operations **)
   1.270 +
   1.271 +fun FIXME msg = writeln ("DEBUG:\n" ^ msg);
   1.272 +
   1.273 +
   1.274 +(* touch_thy -- mark as outdated *)
   1.275 +
   1.276 +fun touch_thy name = change_deps name
   1.277 +  (fn None => (warning (loader_msg "tried to touch finished theory" [name]); None)
   1.278 +    | Some {present, outdated = _, master, files} =>
   1.279 +        make_depends present true master files);
   1.280 +
   1.281 +
   1.282 +(* load_thy *)
   1.283 +
   1.284 +fun required_by [] = ""
   1.285 +  | required_by initiators = " (required by " ^ show_path (rev initiators) ^ ")";
   1.286 +
   1.287 +fun load_thy ml time initiators name parents =
   1.288 +  let
   1.289 +    val _ = if name mem_string initiators then error (cycle_msg name (rev initiators)) else ();
   1.290 +    val _ = writeln ("Loading theory " ^ quote name ^ required_by initiators);
   1.291 +
   1.292 +    val _ = seq touch_thy (thy_graph Graph.all_succs [name]);
   1.293 +    val master = ThyLoad.load_thy name ml time;
   1.294 +
   1.295 +    val files = get_files name;
   1.296 +    val missing_files = mapfilter (fn (path, None) => Some (Path.pack path) | _ => None) files;
   1.297 +  in
   1.298 +    if null missing_files then ()
   1.299 +    else warning (loader_msg ("unresolved dependencies on file(s) " ^ commas_quote missing_files ^
   1.300 +      "\nfor theory") [name]);
   1.301 +    change_deps name (fn _ => make_depends true false (Some master) files)
   1.302 +  end;
   1.303 +
   1.304 +
   1.305 +(* load_file *)
   1.306 +
   1.307 +fun load_file path =
   1.308 +  let
   1.309 +    fun provide name info (deps as Some {present, outdated, master, files}) =
   1.310 +          if exists (equal path o #1) files then
   1.311 +            make_depends present outdated master (overwrite (files, (path, Some info)))
   1.312 +          else (warning (loader_msg ("undeclared dependency on file " ^ quote (Path.pack path) ^
   1.313 +            "\nfor theory") [name]); deps)
   1.314 +      | provide _ _ None = None;
   1.315 +  in
   1.316 +    (case apsome PureThy.get_name (Context.get_context ()) of
   1.317 +      None => (ThyLoad.load_file path; ())
   1.318 +    | Some name =>
   1.319 +        if is_some (lookup_thy name) then change_deps name (provide name (ThyLoad.load_file path))
   1.320 +        else (ThyLoad.load_file path; ()))
   1.321 +  end;
   1.322 +
   1.323 +
   1.324 +(* require_thy *)
   1.325 +
   1.326 +fun init_deps master files = make_depends false false master (map (rpair None) files);
   1.327 +
   1.328 +fun load_deps name ml =
   1.329 +  let val (master, (parents, files)) = ThyLoad.deps_thy name ml
   1.330 +  in (Some (init_deps (Some master) files), parents) end;
   1.331 +
   1.332 +fun file_current (_, None) = false
   1.333 +  | file_current (path, info) = info = ThyLoad.check_file path;
   1.334 +
   1.335 +fun current_deps ml strict name =
   1.336 +  (case lookup_deps name of
   1.337 +    None => (false, load_deps name ml)
   1.338 +  | Some deps =>
   1.339 +      let val same_deps = (None, thy_graph Graph.imm_preds name) in
   1.340 +        (case deps of
   1.341 +          None => (true, same_deps)
   1.342 +        | Some {present, outdated, master, files} =>
   1.343 +            if present andalso not strict then (true, same_deps)
   1.344 +            else
   1.345 +              let val master' = Some (ThyLoad.check_thy name) in
   1.346 +                if master <> master' then (false, load_deps name ml)
   1.347 +                else (not outdated andalso forall file_current files, same_deps)
   1.348 +              end)
   1.349 +      end);
   1.350 +
   1.351 +fun outdated name =
   1.352 +  (case lookup_deps name of Some (Some {outdated, ...}) => outdated | _ => false);
   1.353 +
   1.354 +fun require_thy ml time strict keep_strict initiators name =
   1.355 +  let
   1.356 +    val require_parent =
   1.357 +      require_thy ml time (strict andalso keep_strict) keep_strict (name :: initiators);
   1.358 +    val (current, (new_deps, parents)) = current_deps ml strict name handle ERROR =>
   1.359 +      error (loader_msg "The error(s) above occurred while examining theory" [name] ^ "\n" ^
   1.360 +        required_by initiators);
   1.361 +    val pre_outdated = outdated name;
   1.362 +  in
   1.363 +    seq require_parent parents;
   1.364 +    if current andalso pre_outdated = outdated name then ()	(* FIXME ?? *)
   1.365 +    else
   1.366 +      ((case new_deps of
   1.367 +        Some deps => change_thys (update_node name parents (deps, None))
   1.368 +      | None => ()); load_thy ml time initiators name parents)
   1.369 +  end;
   1.370 +
   1.371 +val weak_use_thy = require_thy true false false false [];
   1.372 +val use_thy      = require_thy true false true false [];
   1.373 +val update_thy   = require_thy true false true true [];
   1.374 +val time_use_thy = require_thy true true true false [];
   1.375 +val use_thy_only = require_thy false false true false [];
   1.376 +
   1.377 +
   1.378 +(* begin / end theory *)		(* FIXME tune *)
   1.379 +
   1.380 +fun begin_theory name parents =
   1.381 +  let
   1.382 +    val _ = seq weak_use_thy parents;
   1.383 +    val theory = PureThy.begin_theory name (map get_theory parents);
   1.384 +    val _ = change_thys (update_node name parents (init_deps None [], Some (theory, Symtab.empty)));
   1.385 +  in theory end;
   1.386 +
   1.387 +fun end_theory theory =
   1.388 +  let val theory' = PureThy.end_theory theory
   1.389 +  in put_theory theory'; theory' end;
   1.390 +
   1.391 +
   1.392 +(* finish entries *)
   1.393 +
   1.394 +(* FIXME
   1.395 +fun finishs names =
   1.396 +  let
   1.397 +    fun err txt bads =
   1.398 +      error (loader_msg txt bads ^ "\n" ^ gen_msg "cannot mark" names ^ " as finished");
   1.399 +
   1.400 +    val all_preds = thy_graph Graph.all_preds names;
   1.401 +    val noncurrent = filter_out is_current all_preds;
   1.402 +    val unfinished = filter_out is_finished (all_preds \\ names);
   1.403 +  in
   1.404 +    if not (null noncurrent) then err "non-current theories" noncurrent
   1.405 +    else if not (null unfinished) then err "unfinished ancestor theories" unfinished
   1.406 +    else seq (fn name => change_thy name (apfst (K Finished)))
   1.407 +  end;
   1.408 +
   1.409 +fun finish name = finishs [name];
   1.410 +*)
   1.411 +
   1.412 +fun update_all () = ();         (* FIXME fake *)
   1.413 +
   1.414 +fun finish_all () = (update_all (); change_thys (Graph.map_nodes (fn (_, entry) => (None, entry))));
   1.415 +
   1.416 +
   1.417 +(* register existing theories *)
   1.418 +
   1.419 +fun register_theory theory =
   1.420 +  let
   1.421 +    val name = PureThy.get_name theory;
   1.422 +    val parents = Theory.parents_of theory;
   1.423 +    val parent_names = map PureThy.get_name parents;
   1.424 +
   1.425 +    fun err txt bads =
   1.426 +      error (loader_msg txt bads ^ "\n" ^ gen_msg "cannot register theory" [name]);
   1.427 +
   1.428 +    val unfinished = filter_out is_finished parent_names;
   1.429 +    fun get_variant (x, y_name) =
   1.430 +      if Theory.eq_thy (x, get_theory y_name) then None
   1.431 +      else Some y_name;
   1.432 +    val variants = mapfilter get_variant (parents ~~ parent_names);
   1.433 +
   1.434 +    fun register G =
   1.435 +      (Graph.new_node (name, (None, Some (theory, Symtab.empty))) G
   1.436 +        handle Graph.DUPLICATE _ => err "duplicate theory entry" [])
   1.437 +      |> add_deps name parent_names;
   1.438 +  in
   1.439 +    if not (null unfinished) then err "unfinished parent theories" unfinished
   1.440 +    else if not (null variants) then err "different versions of parent theories" variants
   1.441 +    else change_thys register
   1.442 +  end;
   1.443 +
   1.444 +
   1.445 +(*final declarations of this structure*)
   1.446 +val theory = get_theory;
   1.447 +val names = get_names;
   1.448 +
   1.449 +end;
   1.450 +
   1.451  structure BasicThyInfo: BASIC_THY_INFO = ThyInfo;
   1.452  open BasicThyInfo;