time_use made pervasive;
authorwenzelm
Fri Feb 05 21:01:53 1999 +0100 (1999-02-05)
changeset 6241d3c6184ca6c5
parent 6240 3231375b701f
child 6242 3d75f5a99f60
time_use made pervasive;
load_file: time option;
tuned;
src/Pure/Thy/thy_info.ML
     1.1 --- a/src/Pure/Thy/thy_info.ML	Fri Feb 05 20:58:17 1999 +0100
     1.2 +++ b/src/Pure/Thy/thy_info.ML	Fri Feb 05 21:01:53 1999 +0100
     1.3 @@ -6,7 +6,6 @@
     1.4  and user data.
     1.5  
     1.6  TODO:
     1.7 -  - check all these versions of 'use' (!!);
     1.8    - data: ThyInfoFun;
     1.9    - remove operation (GC!?);
    1.10    - update_all operation (!?);
    1.11 @@ -15,9 +14,8 @@
    1.12        . allow for undef entry only;
    1.13        . elim (via theory_ref);
    1.14    - stronger handling of missing files (!?!?);
    1.15 -  - register_theory: do not require finished parents (!?) (no?);
    1.16 +  - register_theory: do not require final parents (!?) (no?);
    1.17    - observe verbose flag;
    1.18 -  - touch_thy: msg;
    1.19  *)
    1.20  
    1.21  signature BASIC_THY_INFO =
    1.22 @@ -25,6 +23,8 @@
    1.23    val theory: string -> theory
    1.24    val theory_of_sign: Sign.sg -> theory
    1.25    val theory_of_thm: thm -> theory
    1.26 +(*val use: string -> unit*)             (*exported later*)
    1.27 +  val time_use: string -> unit
    1.28    val touch_thy: string -> unit
    1.29    val use_thy: string -> unit
    1.30    val update_thy: string -> unit
    1.31 @@ -38,12 +38,13 @@
    1.32    val names: unit -> string list
    1.33    val get_theory: string -> theory
    1.34    val put_theory: theory -> unit
    1.35 -  val load_file: Path.T -> unit
    1.36 -  val time_load_file: Path.T -> unit
    1.37 +  val loaded_files: string -> (Path.T * File.info) list
    1.38 +  val load_file: bool -> Path.T -> unit
    1.39 +  val use: string -> unit
    1.40    val use_thy_only: string -> unit
    1.41    val begin_theory: string -> string list -> theory
    1.42    val end_theory: theory -> theory
    1.43 -  val finish_all: unit -> unit
    1.44 +  val finalize_all: unit -> unit
    1.45    val register_theory: theory -> unit
    1.46  end;
    1.47  
    1.48 @@ -83,7 +84,7 @@
    1.49  fun if_verbose f x = if ! verbose then f x else ();
    1.50  
    1.51  
    1.52 -(* derived graph operations *)		(* FIXME more abstract (!?) *)
    1.53 +(* derived graph operations *)          (* FIXME more abstract (!?) *)
    1.54  
    1.55  fun add_deps name parents G =
    1.56    foldl (fn (H, parent) => Graph.add_edge_acyclic (parent, name) H) (G, parents)
    1.57 @@ -101,12 +102,12 @@
    1.58  
    1.59  type deps =
    1.60    {present: bool, outdated: bool,
    1.61 -    master: (Path.T * File.info) list, files: (Path.T * (Path.T * File.info) option) list} option;
    1.62 +    master: (Path.T * File.info) list, files: (Path.T * (Path.T * File.info) option) list};
    1.63  
    1.64 -fun make_depends present outdated master files =
    1.65 -  Some {present = present, outdated = outdated, master = master, files = files}: deps;
    1.66 +fun make_deps present outdated master files =
    1.67 +  {present = present, outdated = outdated, master = master, files = files}: deps;
    1.68  
    1.69 -type thy = deps * (theory * Object.T Symtab.table) option;
    1.70 +type thy = deps option * (theory * Object.T Symtab.table) option;
    1.71  type kind = Object.kind * (Object.T * (Object.T -> unit));
    1.72  
    1.73  
    1.74 @@ -146,8 +147,9 @@
    1.75  val get_deps = #1 o get_thy;
    1.76  fun change_deps name f = change_thy name (fn (deps, x) => (f deps, x));
    1.77  
    1.78 +fun is_final name = is_none (get_deps name);
    1.79  fun get_files name = (case get_deps name of Some {files, ...} => files | _ => []);
    1.80 -fun is_finished name = is_none (get_deps name);
    1.81 +val loaded_files = mapfilter #2 o get_files;
    1.82  
    1.83  
    1.84  (* access theory *)
    1.85 @@ -164,22 +166,36 @@
    1.86    change_thy (PureThy.get_name theory) (fn (deps, _) => (deps, (Some (theory, Symtab.empty))));
    1.87  
    1.88  
    1.89 -
    1.90  (** thy data **)  (* FIXME *)
    1.91  
    1.92  
    1.93  
    1.94  (** thy operations **)
    1.95  
    1.96 -fun FIXME msg = writeln ("DEBUG:\n" ^ msg);
    1.97 +(* maintain 'outdated' flag *)
    1.98  
    1.99 +fun is_outdated name =
   1.100 +  (case lookup_deps name of
   1.101 +    Some (Some {outdated, ...}) => outdated
   1.102 +  | _ => false);
   1.103  
   1.104 -(* touch_thy -- mark as outdated *)
   1.105 +fun outdate_thy name =
   1.106 +  if is_final name then ()
   1.107 +  else change_deps name (apsome (fn {present, outdated = _, master, files} =>
   1.108 +    make_deps present true master files));
   1.109  
   1.110 -fun touch_thy name = change_deps name
   1.111 -  (fn None => (warning (loader_msg "tried to touch finished theory" [name]); None)
   1.112 -    | Some {present, outdated = _, master, files} =>
   1.113 -        make_depends present true master files);
   1.114 +fun touch_thy name =
   1.115 +  if is_outdated name then ()
   1.116 +  else if is_final name then warning (loader_msg "tried to touch final theory" [name])
   1.117 +  else
   1.118 +    (case filter_out is_outdated (thy_graph Graph.all_succs [name]) \ name of
   1.119 +      [] => outdate_thy name
   1.120 +    | names =>
   1.121 +       (warning (loader_msg "the following theories become out-of-date:" names);
   1.122 +        seq outdate_thy names; outdate_thy name));
   1.123 +
   1.124 +val untouch_deps = apsome (fn {present, outdated = _, master, files}: deps =>
   1.125 +  make_deps present false master files);
   1.126  
   1.127  
   1.128  (* load_thy *)
   1.129 @@ -201,19 +217,20 @@
   1.130      if null missing_files then ()
   1.131      else warning (loader_msg ("unresolved dependencies on file(s) " ^ commas_quote missing_files ^
   1.132        "\nfor theory") [name]);
   1.133 -    change_deps name (fn _ => make_depends true false master files)
   1.134 +    change_deps name (fn _ => Some (make_deps true false master files))
   1.135    end;
   1.136  
   1.137  
   1.138  (* load_file *)
   1.139  
   1.140 -fun load_file path =
   1.141 +fun run_file path =
   1.142    let
   1.143      fun provide name info (deps as Some {present, outdated, master, files}) =
   1.144 -          if exists (equal path o #1) files then
   1.145 -            make_depends present outdated master (overwrite (files, (path, Some info)))
   1.146 -          else (warning (loader_msg ("undeclared dependency on file " ^ quote (Path.pack path) ^
   1.147 -            "\nfor theory") [name]); deps)
   1.148 +          if present then deps
   1.149 +          else if exists (equal path o #1) files then
   1.150 +            Some (make_deps present outdated master (overwrite (files, (path, Some info))))
   1.151 +          else (warning (loader_msg "undeclared dependency of theory" [name] ^
   1.152 +            ": " ^ quote (Path.pack path)); deps)
   1.153        | provide _ _ None = None;
   1.154    in
   1.155      (case apsome PureThy.get_name (Context.get_context ()) of
   1.156 @@ -223,18 +240,22 @@
   1.157          else (ThyLoad.load_file path; ()))
   1.158    end;
   1.159  
   1.160 +fun load_file false path = run_file path
   1.161 +  | load_file true path =
   1.162 +      let val name = Path.pack path in
   1.163 +        timeit (fn () =>
   1.164 +         (writeln ("\n**** Starting file " ^ quote name ^ " ****");
   1.165 +          run_file path;
   1.166 +          writeln ("**** Finished file " ^ quote name ^ " ****\n")))
   1.167 +      end;
   1.168  
   1.169 -fun time_load_file path =
   1.170 -  let val s = Path.pack path in
   1.171 -    timeit (fn () =>
   1.172 -     (writeln ("\n**** Starting " ^ s ^ " ****"); load_file path;
   1.173 -      writeln ("\n**** Finished " ^ s ^ " ****")))
   1.174 -  end;
   1.175 +val use = load_file false o Path.unpack;
   1.176 +val time_use = load_file true o Path.unpack;
   1.177  
   1.178  
   1.179  (* require_thy *)
   1.180  
   1.181 -fun init_deps master files = make_depends false false master (map (rpair None) files);
   1.182 +fun init_deps master files = Some (make_deps false false master (map (rpair None) files));
   1.183  
   1.184  fun load_deps name ml =
   1.185    let val (master, (parents, files)) = ThyLoad.deps_thy name ml
   1.186 @@ -259,39 +280,34 @@
   1.187                end)
   1.188        end);
   1.189  
   1.190 -fun outdated name =
   1.191 -  (case lookup_deps name of Some (Some {outdated, ...}) => outdated | _ => false);
   1.192 -
   1.193 -fun untouch None = None
   1.194 -  | untouch (Some {present, outdated = _, master, files}) =
   1.195 -      make_depends present false master files;
   1.196 -
   1.197  fun require_thy ml time strict keep_strict initiators name =
   1.198    let
   1.199      val require_parent =
   1.200        require_thy ml time (strict andalso keep_strict) keep_strict (name :: initiators);
   1.201      val (current, (new_deps, parents)) = current_deps ml strict name handle ERROR =>
   1.202 -      error (loader_msg "The error(s) above occurred while examining theory" [name] ^ "\n" ^
   1.203 -        required_by initiators);
   1.204 +      error (loader_msg "The error(s) above occurred while examining theory" [name] ^
   1.205 +        (if null initiators then "" else "\n" ^ required_by initiators));
   1.206      val parents_current = map require_parent parents;
   1.207    in
   1.208      if current andalso forall I parents_current then true
   1.209      else
   1.210        ((case new_deps of
   1.211 -        Some deps => change_thys (update_node name parents (untouch deps, None))
   1.212 +        Some deps => change_thys (update_node name parents (untouch_deps deps, None))
   1.213        | None => ());
   1.214          load_thy ml time initiators name parents;
   1.215          false)
   1.216    end;
   1.217  
   1.218 -val weak_use_thy = K () o require_thy true false false false [];
   1.219 -val use_thy      = K () o require_thy true false true false [];
   1.220 -val update_thy   = K () o require_thy true false true true [];
   1.221 -val time_use_thy = K () o require_thy true true true false [];
   1.222 -val use_thy_only = K () o require_thy false false true false [];
   1.223 +fun gen_use_thy f name = (f name; Context.context (get_theory name));
   1.224 +
   1.225 +val weak_use_thy = gen_use_thy (require_thy true false false false []);
   1.226 +val use_thy      = gen_use_thy (require_thy true false true false []);
   1.227 +val update_thy   = gen_use_thy (require_thy true false true true []);
   1.228 +val time_use_thy = gen_use_thy (require_thy true true true false []);
   1.229 +val use_thy_only = gen_use_thy (require_thy false false true false []);
   1.230  
   1.231  
   1.232 -(* begin / end theory *)		(* FIXME tune *)
   1.233 +(* begin / end theory *)                (* FIXME tune *)
   1.234  
   1.235  fun begin_theory name parents =
   1.236    let
   1.237 @@ -305,7 +321,7 @@
   1.238    in put_theory theory'; theory' end;
   1.239  
   1.240  
   1.241 -(* finish entries *)
   1.242 +(* finalize entries *)
   1.243  
   1.244  (* FIXME
   1.245  fun finishs names =
   1.246 @@ -327,7 +343,7 @@
   1.247  
   1.248  fun update_all () = ();         (* FIXME fake *)
   1.249  
   1.250 -fun finish_all () =
   1.251 +fun finalize_all () =
   1.252    (update_all (); change_thys (Graph.map_nodes (fn (_, entry) => (None, entry))));
   1.253  
   1.254  
   1.255 @@ -342,7 +358,7 @@
   1.256      fun err txt bads =
   1.257        error (loader_msg txt bads ^ "\n" ^ gen_msg "cannot register theory" [name]);
   1.258  
   1.259 -    val unfinished = filter_out is_finished parent_names;
   1.260 +    val nonfinal = filter_out is_final parent_names;
   1.261      fun get_variant (x, y_name) =
   1.262        if Theory.eq_thy (x, get_theory y_name) then None
   1.263        else Some y_name;
   1.264 @@ -353,7 +369,7 @@
   1.265          handle Graph.DUPLICATE _ => err "duplicate theory entry" [])
   1.266        |> add_deps name parent_names;
   1.267    in
   1.268 -    if not (null unfinished) then err "unfinished parent theories" unfinished
   1.269 +    if not (null nonfinal) then err "non-final parent theories" nonfinal
   1.270      else if not (null variants) then err "different versions of parent theories" variants
   1.271      else change_thys register
   1.272    end;