src/Pure/Thy/thy_info.ML
author wenzelm
Mon Feb 23 14:50:30 2015 +0100 (2015-02-23)
changeset 59564 fdc03c8daacc
parent 59366 e94df7f6b608
child 60937 51425cbe8ce9
permissions -rw-r--r--
Goal.prove_multi is superseded by the fully general Goal.prove_common;
berghofe@3604
     1
(*  Title:      Pure/Thy/thy_info.ML
wenzelm@6211
     2
    Author:     Markus Wenzel, TU Muenchen
berghofe@3604
     3
wenzelm@37978
     4
Global theory info database, with auto-loading according to theory and
wenzelm@15801
     5
file dependencies.
wenzelm@3976
     6
*)
berghofe@3604
     7
berghofe@3604
     8
signature THY_INFO =
berghofe@3604
     9
sig
wenzelm@26614
    10
  val get_names: unit -> string list
wenzelm@7288
    11
  val lookup_theory: string -> theory option
wenzelm@6211
    12
  val get_theory: string -> theory
wenzelm@26983
    13
  val master_directory: string -> Path.T
wenzelm@29421
    14
  val remove_thy: string -> unit
wenzelm@59366
    15
  val use_theories:
wenzelm@59366
    16
    {document: bool, last_timing: Toplevel.transition -> Time.time option, master_dir: Path.T} ->
wenzelm@59366
    17
    (string * Position.T) list -> unit
wenzelm@48927
    18
  val use_thys: (string * Position.T) list -> unit
wenzelm@48927
    19
  val use_thy: string * Position.T -> unit
wenzelm@58856
    20
  val script_thy: Position.T -> string -> theory -> theory
wenzelm@37954
    21
  val register_thy: theory -> unit
wenzelm@24080
    22
  val finish: unit -> unit
berghofe@3604
    23
end;
berghofe@3604
    24
wenzelm@37216
    25
structure Thy_Info: THY_INFO =
wenzelm@6211
    26
struct
berghofe@3604
    27
wenzelm@6211
    28
(** thy database **)
wenzelm@6211
    29
wenzelm@6211
    30
(* messages *)
wenzelm@6211
    31
wenzelm@55797
    32
val show_path = space_implode " via " o map quote;
wenzelm@6211
    33
wenzelm@55797
    34
fun cycle_msg names = "Cyclic dependency of " ^ show_path names;
berghofe@3604
    35
berghofe@3604
    36
wenzelm@6666
    37
(* derived graph operations *)
berghofe@3604
    38
wenzelm@50862
    39
fun add_deps name parents G = String_Graph.add_deps_acyclic (name, parents) G
wenzelm@50862
    40
  handle String_Graph.CYCLES namess => error (cat_lines (map cycle_msg namess));
berghofe@3604
    41
wenzelm@37984
    42
fun new_entry name parents entry =
wenzelm@50862
    43
  String_Graph.new_node (name, entry) #> add_deps name parents;
wenzelm@37977
    44
berghofe@3604
    45
wenzelm@59178
    46
(* global thys *)
wenzelm@6211
    47
wenzelm@6211
    48
type deps =
wenzelm@41955
    49
 {master: (Path.T * SHA1.digest),  (*master dependencies for thy file*)
wenzelm@48927
    50
  imports: (string * Position.T) list};  (*source specification of imports (partially qualified)*)
wenzelm@23886
    51
wenzelm@38148
    52
fun make_deps master imports : deps = {master = master, imports = imports};
wenzelm@6211
    53
wenzelm@59178
    54
fun master_dir (d: deps option) =
wenzelm@59178
    55
  the_default Path.current (Option.map (Path.dir o #1 o #master) d);
wenzelm@59178
    56
wenzelm@44225
    57
fun base_name s = Path.implode (Path.base (Path.explode s));
wenzelm@23967
    58
wenzelm@6211
    59
local
wenzelm@59178
    60
  val global_thys =
wenzelm@59178
    61
    Synchronized.var "Thy_Info.thys"
wenzelm@59178
    62
      (String_Graph.empty: (deps option * theory option) String_Graph.T);
wenzelm@6211
    63
in
wenzelm@59178
    64
  fun get_thys () = Synchronized.value global_thys;
wenzelm@59178
    65
  fun change_thys f = Synchronized.change global_thys f;
berghofe@3604
    66
end;
wenzelm@5209
    67
wenzelm@50862
    68
fun get_names () = String_Graph.topological_order (get_thys ());
wenzelm@6211
    69
wenzelm@6211
    70
wenzelm@6211
    71
(* access thy *)
wenzelm@6211
    72
wenzelm@59178
    73
fun lookup thys name = try (String_Graph.get_node thys) name;
wenzelm@59178
    74
fun lookup_thy name = lookup (get_thys ()) name;
wenzelm@7935
    75
wenzelm@59178
    76
fun get thys name =
wenzelm@59178
    77
  (case lookup thys name of
skalberg@15531
    78
    SOME thy => thy
wenzelm@55797
    79
  | NONE => error ("Theory loader: nothing known about theory " ^ quote name));
wenzelm@6211
    80
wenzelm@59178
    81
fun get_thy name = get (get_thys ()) name;
wenzelm@59178
    82
wenzelm@6211
    83
wenzelm@6211
    84
(* access deps *)
wenzelm@6211
    85
skalberg@15570
    86
val lookup_deps = Option.map #1 o lookup_thy;
wenzelm@6211
    87
wenzelm@59178
    88
val master_directory = master_dir o #1 o get_thy;
wenzelm@7191
    89
wenzelm@6211
    90
wenzelm@6211
    91
(* access theory *)
wenzelm@6211
    92
wenzelm@7687
    93
fun lookup_theory name =
wenzelm@7687
    94
  (case lookup_thy name of
wenzelm@38142
    95
    SOME (_, SOME theory) => SOME theory
skalberg@15531
    96
  | _ => NONE);
wenzelm@7288
    97
wenzelm@6211
    98
fun get_theory name =
wenzelm@7288
    99
  (case lookup_theory name of
wenzelm@23871
   100
    SOME theory => theory
wenzelm@55797
   101
  | _ => error ("Theory loader: undefined entry for theory " ^ quote name));
wenzelm@6211
   102
wenzelm@56208
   103
val get_imports = Resources.imports_of o get_theory;
wenzelm@44337
   104
wenzelm@6211
   105
wenzelm@6211
   106
wenzelm@6211
   107
(** thy operations **)
wenzelm@6211
   108
wenzelm@59178
   109
(* remove *)
wenzelm@29421
   110
wenzelm@59178
   111
fun remove name thys =
wenzelm@59178
   112
  (case lookup thys name of
wenzelm@59178
   113
    NONE => thys
wenzelm@59178
   114
  | SOME (NONE, _) => error ("Cannot update finished theory " ^ quote name)
wenzelm@59178
   115
  | SOME _ =>
wenzelm@59178
   116
      let
wenzelm@59178
   117
        val succs = String_Graph.all_succs thys [name];
wenzelm@59178
   118
        val _ = writeln ("Theory loader: removing " ^ commas_quote succs);
wenzelm@59178
   119
      in fold String_Graph.del_node succs thys end);
wenzelm@29421
   120
wenzelm@59178
   121
val remove_thy = change_thys o remove;
wenzelm@59178
   122
wenzelm@7099
   123
wenzelm@59178
   124
(* update *)
wenzelm@59178
   125
wenzelm@59178
   126
fun update deps theory thys =
wenzelm@43640
   127
  let
wenzelm@43640
   128
    val name = Context.theory_name theory;
wenzelm@43640
   129
    val parents = map Context.theory_name (Theory.parents_of theory);
wenzelm@59178
   130
wenzelm@59178
   131
    val thys' = remove name thys;
wenzelm@59178
   132
    val _ = map (get thys') parents;
wenzelm@59178
   133
  in new_entry name parents (SOME deps, SOME theory) thys' end;
wenzelm@59178
   134
wenzelm@59178
   135
fun update_thy deps theory = change_thys (update deps theory);
wenzelm@43640
   136
wenzelm@7099
   137
wenzelm@24209
   138
(* scheduling loader tasks *)
wenzelm@24209
   139
wenzelm@51330
   140
datatype result =
wenzelm@53375
   141
  Result of {theory: theory, exec_id: Document_ID.exec,
wenzelm@53375
   142
    present: unit -> unit, commit: unit -> unit, weight: int};
wenzelm@51331
   143
wenzelm@53375
   144
fun theory_result theory =
wenzelm@53375
   145
  Result {theory = theory, exec_id = Document_ID.none, present = I, commit = I, weight = 0};
wenzelm@51330
   146
wenzelm@51330
   147
fun result_theory (Result {theory, ...}) = theory;
wenzelm@51331
   148
fun result_present (Result {present, ...}) = present;
wenzelm@51331
   149
fun result_commit (Result {commit, ...}) = commit;
wenzelm@51331
   150
fun result_ord (Result {weight = i, ...}, Result {weight = j, ...}) = int_ord (j, i);
wenzelm@51331
   151
wenzelm@53375
   152
fun join_theory (Result {theory, exec_id, ...}) =
wenzelm@54370
   153
  let
wenzelm@54370
   154
    (*toplevel proofs and diags*)
wenzelm@54370
   155
    val _ = Future.join_tasks (maps Future.group_snapshot (Execution.peek exec_id));
wenzelm@54370
   156
    (*fully nested proofs*)
wenzelm@54370
   157
    val res = Exn.capture Thm.join_theory_proofs theory;
wenzelm@54370
   158
  in res :: map Exn.Exn (maps Task_Queue.group_status (Execution.peek exec_id)) end;
wenzelm@43641
   159
wenzelm@37977
   160
datatype task =
wenzelm@55461
   161
  Task of Path.T * string list * (theory list -> result) |
wenzelm@37977
   162
  Finished of theory;
wenzelm@37977
   163
wenzelm@37977
   164
fun task_finished (Task _) = false
wenzelm@37977
   165
  | task_finished (Finished _) = true;
wenzelm@24209
   166
wenzelm@44162
   167
fun task_parents deps (parents: string list) = map (the o AList.lookup (op =) deps) parents;
wenzelm@44162
   168
wenzelm@29118
   169
local
wenzelm@29118
   170
wenzelm@44162
   171
val schedule_seq =
wenzelm@50862
   172
  String_Graph.schedule (fn deps => fn (_, task) =>
wenzelm@44162
   173
    (case task of
wenzelm@55461
   174
      Task (_, parents, body) =>
wenzelm@51331
   175
        let
wenzelm@51331
   176
          val result = body (task_parents deps parents);
wenzelm@53190
   177
          val _ = Par_Exn.release_all (join_theory result);
wenzelm@51331
   178
          val _ = result_present result ();
wenzelm@51331
   179
          val _ = result_commit result ();
wenzelm@51331
   180
        in result_theory result end
wenzelm@44162
   181
    | Finished thy => thy)) #> ignore;
wenzelm@29000
   182
wenzelm@51284
   183
val schedule_futures = uninterruptible (fn _ => fn tasks =>
wenzelm@51284
   184
  let
wenzelm@51331
   185
    val futures = tasks
wenzelm@51284
   186
      |> String_Graph.schedule (fn deps => fn (name, task) =>
wenzelm@51284
   187
        (case task of
wenzelm@55461
   188
          Task (_, parents, body) =>
wenzelm@51284
   189
            (singleton o Future.forks)
wenzelm@51284
   190
              {name = "theory:" ^ name, group = NONE,
wenzelm@51284
   191
                deps = map (Future.task_of o #2) deps, pri = 0, interrupts = true}
wenzelm@51284
   192
              (fn () =>
wenzelm@51284
   193
                (case filter (not o can Future.join o #2) deps of
wenzelm@51330
   194
                  [] => body (map (result_theory o Future.join) (task_parents deps parents))
wenzelm@51284
   195
                | bad =>
wenzelm@55797
   196
                    error
wenzelm@55797
   197
                      ("Failed to load theory " ^ quote name ^
wenzelm@55797
   198
                        " (unresolved " ^ commas_quote (map #1 bad) ^ ")")))
wenzelm@51331
   199
        | Finished theory => Future.value (theory_result theory)));
wenzelm@51331
   200
wenzelm@51331
   201
    val results1 = futures
wenzelm@51331
   202
      |> maps (fn future =>
wenzelm@51331
   203
          (case Future.join_result future of
wenzelm@53190
   204
            Exn.Res result => join_theory result
wenzelm@51331
   205
          | Exn.Exn exn => [Exn.Exn exn]));
wenzelm@51331
   206
wenzelm@51331
   207
    val results2 = futures
wenzelm@51331
   208
      |> map_filter (Exn.get_res o Future.join_result)
wenzelm@51331
   209
      |> sort result_ord
wenzelm@51331
   210
      |> Par_List.map (fn result => Exn.capture (result_present result) ());
wenzelm@51331
   211
wenzelm@51331
   212
    (* FIXME more precise commit order (!?) *)
wenzelm@51331
   213
    val results3 = futures
wenzelm@51331
   214
      |> map (fn future => Exn.capture (fn () => result_commit (Future.join future) ()) ());
wenzelm@51284
   215
wenzelm@54370
   216
    (* FIXME avoid global Execution.reset (!??) *)
wenzelm@53192
   217
    val results4 = map Exn.Exn (maps Task_Queue.group_status (Execution.reset ()));
wenzelm@51284
   218
wenzelm@51331
   219
    val _ = Par_Exn.release_all (results1 @ results2 @ results3 @ results4);
wenzelm@51284
   220
  in () end);
wenzelm@29429
   221
wenzelm@24209
   222
in
wenzelm@24209
   223
wenzelm@32794
   224
fun schedule_tasks tasks =
wenzelm@59180
   225
  if Multithreading.enabled () then schedule_futures tasks else schedule_seq tasks;
wenzelm@24209
   226
wenzelm@24209
   227
end;
wenzelm@24209
   228
wenzelm@24209
   229
wenzelm@23967
   230
(* require_thy -- checking database entries wrt. the file-system *)
berghofe@15065
   231
wenzelm@7211
   232
local
wenzelm@6211
   233
wenzelm@37977
   234
fun required_by _ [] = ""
wenzelm@37977
   235
  | required_by s initiators = s ^ "(required by " ^ show_path (rev initiators) ^ ")";
wenzelm@37977
   236
wenzelm@54458
   237
fun load_thy document last_timing initiators update_time deps text (name, pos) keywords parents =
wenzelm@37977
   238
  let
wenzelm@59178
   239
    val _ = remove_thy name;
wenzelm@58843
   240
    val _ = writeln ("Loading theory " ^ quote name ^ required_by " " initiators);
wenzelm@56333
   241
    val _ = Output.try_protocol_message (Markup.loading_theory name) [];
wenzelm@37977
   242
wenzelm@41548
   243
    val {master = (thy_path, _), imports} = deps;
wenzelm@38134
   244
    val dir = Path.dir thy_path;
wenzelm@51294
   245
    val header = Thy_Header.make (name, pos) imports keywords;
wenzelm@48927
   246
wenzelm@48927
   247
    val _ = Position.reports (map #2 imports ~~ map Theory.get_markup parents);
wenzelm@37977
   248
wenzelm@53375
   249
    val exec_id = Document_ID.make ();
wenzelm@53375
   250
    val _ =
wenzelm@53375
   251
      Execution.running Document_ID.none exec_id [] orelse
wenzelm@53375
   252
        raise Fail ("Failed to register execution: " ^ Document_ID.print exec_id);
wenzelm@53375
   253
wenzelm@53375
   254
    val text_pos = Position.put_id (Document_ID.print exec_id) (Path.position thy_path);
wenzelm@51331
   255
    val (theory, present, weight) =
wenzelm@56208
   256
      Resources.load_thy document last_timing update_time dir header text_pos text
wenzelm@48638
   257
        (if name = Context.PureN then [ML_Context.the_global_context ()] else parents);
wenzelm@43640
   258
    fun commit () = update_thy deps theory;
wenzelm@53375
   259
  in
wenzelm@53375
   260
    Result {theory = theory, exec_id = exec_id, present = present, commit = commit, weight = weight}
wenzelm@53375
   261
  end;
wenzelm@37977
   262
wenzelm@48898
   263
fun check_deps dir name =
wenzelm@6211
   264
  (case lookup_deps name of
wenzelm@51293
   265
    SOME NONE => (true, NONE, Position.none, get_imports name, [])
wenzelm@23893
   266
  | NONE =>
wenzelm@56208
   267
      let val {master, text, theory_pos, imports, keywords} = Resources.check_thy dir name
wenzelm@51293
   268
      in (false, SOME (make_deps master imports, text), theory_pos, imports, keywords) end
wenzelm@42129
   269
  | SOME (SOME {master, ...}) =>
wenzelm@42003
   270
      let
wenzelm@48928
   271
        val {master = master', text = text', theory_pos = theory_pos', imports = imports',
wenzelm@56208
   272
          keywords = keywords'} = Resources.check_thy dir name;
wenzelm@42003
   273
        val deps' = SOME (make_deps master' imports', text');
wenzelm@42003
   274
        val current =
wenzelm@42003
   275
          #2 master = #2 master' andalso
wenzelm@42003
   276
            (case lookup_theory name of
wenzelm@42003
   277
              NONE => false
wenzelm@56208
   278
            | SOME theory => Resources.loaded_files_current theory);
wenzelm@51293
   279
      in (current, deps', theory_pos', imports', keywords') end);
wenzelm@6211
   280
wenzelm@23967
   281
in
wenzelm@23967
   282
wenzelm@54458
   283
fun require_thys document last_timing initiators dir strs tasks =
wenzelm@54458
   284
      fold_map (require_thy document last_timing initiators dir) strs tasks |>> forall I
wenzelm@54458
   285
and require_thy document last_timing initiators dir (str, require_pos) tasks =
wenzelm@6211
   286
  let
wenzelm@21858
   287
    val path = Path.expand (Path.explode str);
wenzelm@21858
   288
    val name = Path.implode (Path.base path);
wenzelm@56208
   289
    val node_name = File.full_path dir (Resources.thy_path path);
wenzelm@55461
   290
    fun check_entry (Task (node_name', _, _)) =
wenzelm@55461
   291
          if node_name = node_name' then ()
wenzelm@55461
   292
          else
wenzelm@55797
   293
            error ("Incoherent imports for theory " ^ quote name ^
wenzelm@55461
   294
              Position.here require_pos ^ ":\n" ^
wenzelm@55488
   295
              "  " ^ Path.print node_name ^ "\n" ^
wenzelm@55488
   296
              "  " ^ Path.print node_name')
wenzelm@55461
   297
      | check_entry _ = ();
wenzelm@7066
   298
  in
wenzelm@50862
   299
    (case try (String_Graph.get_node tasks) name of
wenzelm@55461
   300
      SOME task => (check_entry task; (task_finished task, tasks))
wenzelm@23967
   301
    | NONE =>
wenzelm@23967
   302
        let
wenzelm@43651
   303
          val dir' = Path.append dir (Path.dir path);
wenzelm@43651
   304
          val _ = member (op =) initiators name andalso error (cycle_msg initiators);
wenzelm@43651
   305
wenzelm@51293
   306
          val (current, deps, theory_pos, imports, keywords) = check_deps dir' name
wenzelm@55797
   307
            handle ERROR msg =>
wenzelm@55797
   308
              cat_error msg
wenzelm@55797
   309
                ("The error(s) above occurred for theory " ^ quote name ^
wenzelm@55797
   310
                  Position.here require_pos ^ required_by "\n" initiators);
wenzelm@37981
   311
wenzelm@48927
   312
          val parents = map (base_name o #1) imports;
wenzelm@48898
   313
          val (parents_current, tasks') =
wenzelm@54458
   314
            require_thys document last_timing (name :: initiators)
wenzelm@48898
   315
              (Path.append dir (master_dir (Option.map #1 deps))) imports tasks;
wenzelm@6211
   316
wenzelm@23967
   317
          val all_current = current andalso parents_current;
wenzelm@37977
   318
          val task =
wenzelm@37977
   319
            if all_current then Finished (get_theory name)
wenzelm@37977
   320
            else
wenzelm@37980
   321
              (case deps of
wenzelm@37980
   322
                NONE => raise Fail "Malformed deps"
wenzelm@42003
   323
              | SOME (dep, text) =>
wenzelm@48876
   324
                  let
wenzelm@48876
   325
                    val update_time = serial ();
wenzelm@48928
   326
                    val load =
wenzelm@54458
   327
                      load_thy document last_timing initiators update_time dep
wenzelm@51293
   328
                        text (name, theory_pos) keywords;
wenzelm@55461
   329
                  in Task (node_name, parents, load) end);
wenzelm@48874
   330
wenzelm@48874
   331
          val tasks'' = new_entry name parents task tasks';
wenzelm@48898
   332
        in (all_current, tasks'') end)
wenzelm@7066
   333
  end;
wenzelm@6484
   334
wenzelm@23967
   335
end;
wenzelm@23967
   336
wenzelm@23967
   337
wenzelm@37979
   338
(* use_thy *)
wenzelm@23967
   339
wenzelm@54458
   340
fun use_theories {document, last_timing, master_dir} imports =
wenzelm@54458
   341
  schedule_tasks (snd (require_thys document last_timing [] master_dir imports String_Graph.empty));
wenzelm@23967
   342
wenzelm@54458
   343
val use_thys = use_theories {document = false, last_timing = K NONE, master_dir = Path.current};
wenzelm@37949
   344
val use_thy = use_thys o single;
wenzelm@7211
   345
wenzelm@59364
   346
wenzelm@57626
   347
(* toplevel scripting -- without maintaining database *)
wenzelm@57626
   348
wenzelm@58856
   349
fun script_thy pos txt thy =
wenzelm@57626
   350
  let
wenzelm@58856
   351
    val trs =
wenzelm@58928
   352
      Outer_Syntax.parse thy pos txt
wenzelm@58856
   353
      |> map (Toplevel.modify_init (K thy));
wenzelm@57626
   354
    val end_pos = if null trs then pos else Toplevel.pos_of (List.last trs);
wenzelm@57626
   355
    val end_state = fold (Toplevel.command_exception true) trs Toplevel.toplevel;
wenzelm@57626
   356
  in Toplevel.end_theory end_pos end_state end;
wenzelm@6211
   357
wenzelm@6211
   358
wenzelm@37977
   359
(* register theory *)
wenzelm@6211
   360
wenzelm@37954
   361
fun register_thy theory =
wenzelm@6211
   362
  let
wenzelm@16454
   363
    val name = Context.theory_name theory;
wenzelm@56208
   364
    val {master, ...} = Resources.check_thy (Resources.master_directory theory) name;
wenzelm@56208
   365
    val imports = Resources.imports_of theory;
wenzelm@6211
   366
  in
wenzelm@59178
   367
    change_thys (fn thys =>
wenzelm@59178
   368
      let
wenzelm@59178
   369
        val thys' = remove name thys;
wenzelm@59178
   370
        val _ = writeln ("Registering theory " ^ quote name);
wenzelm@59178
   371
      in update (make_deps master imports) theory thys' end)
wenzelm@6211
   372
  end;
wenzelm@6211
   373
wenzelm@24080
   374
wenzelm@24080
   375
(* finish all theories *)
wenzelm@24080
   376
wenzelm@50862
   377
fun finish () = change_thys (String_Graph.map (fn _ => fn (_, entry) => (NONE, entry)));
wenzelm@24080
   378
wenzelm@6211
   379
end;