(*  Title:      Pure/Thy/thy_info.ML

    Author:     Markus Wenzel, TU Muenchen

Global theory info database, with auto-loading according to theory and

file dependencies.

*)

signature THY_INFO =

sig

  datatype action = Update | Remove

  val add_hook: (action -> string -> unit) -> unit

  val get_names: unit -> string list

  val lookup_theory: string -> theory option

  val get_theory: string -> theory

  val is_finished: string -> bool

  val master_directory: string -> Path.T

  val loaded_files: string -> Path.T list

  val remove_thy: string -> unit

  val kill_thy: string -> unit

  val use_thys_wrt: Path.T -> string list -> unit

  val use_thys: string list -> unit

  val use_thy: string -> unit

  val toplevel_begin_theory: Path.T option -> string ->

    string list -> (Path.T * bool) list -> theory

  val register_thy: theory -> unit

  val finish: unit -> unit

end;

structure Thy_Info: THY_INFO =

struct

(** theory loader actions and hooks **)

datatype action = Update | Remove;

local

  val hooks = Unsynchronized.ref ([]: (action -> string -> unit) list);

in

  fun add_hook f = NAMED_CRITICAL "Thy_Info" (fn () => Unsynchronized.change hooks (cons f));

  fun perform action name = List.app (fn f => (try (fn () => f action name) (); ())) (! hooks);

end;

(** thy database **)

(* messages *)

fun loader_msg txt [] = "Theory loader: " ^ txt

  | loader_msg txt names = "Theory loader: " ^ txt ^ " " ^ commas_quote names;

val show_path = space_implode " via " o map quote;

fun cycle_msg names = loader_msg ("cyclic dependency of " ^ show_path names) [];

(* derived graph operations *)

fun add_deps name parents G = Graph.add_deps_acyclic (name, parents) G

  handle Graph.CYCLES namess => error (cat_lines (map cycle_msg namess));

fun new_entry name parents entry =

  Graph.new_node (name, entry) #> add_deps name parents;

(* thy database *)

type deps =

 {master: (Path.T * Thy_Load.file_ident),  (*master dependencies for thy file*)

  imports: string list};  (*source specification of imports (partially qualified)*)

fun make_deps master imports : deps = {master = master, imports = imports};

fun master_dir (d: deps option) = the_default Path.current (Option.map (Path.dir o #1 o #master) d);

fun base_name s = Path.implode (Path.base (Path.explode s));

local

  val database = Unsynchronized.ref (Graph.empty: (deps option * theory option) Graph.T);

in

  fun get_thys () = ! database;

  fun change_thys f = NAMED_CRITICAL "Thy_Info" (fn () => Unsynchronized.change database f);

end;

(* access thy graph *)

fun thy_graph f x = f (get_thys ()) x;

fun get_names () = Graph.topological_order (get_thys ());

(* access thy *)

fun lookup_thy name =

  SOME (thy_graph Graph.get_node name) handle Graph.UNDEF _ => NONE;

val known_thy = is_some o lookup_thy;

fun get_thy name =

  (case lookup_thy name of

    SOME thy => thy

  | NONE => error (loader_msg "nothing known about theory" [name]));

(* access deps *)

val lookup_deps = Option.map #1 o lookup_thy;

val get_deps = #1 o get_thy;

val is_finished = is_none o get_deps;

val master_directory = master_dir o get_deps;

fun get_parents name =

  thy_graph Graph.imm_preds name handle Graph.UNDEF _ =>

    error (loader_msg "nothing known about theory" [name]);

(* access theory *)

fun lookup_theory name =

  (case lookup_thy name of

    SOME (_, SOME theory) => SOME theory

  | _ => NONE);

fun get_theory name =

  (case lookup_theory name of

    SOME theory => theory

  | _ => error (loader_msg "undefined theory entry for" [name]));

fun loaded_files name = NAMED_CRITICAL "Thy_Info" (fn () =>

  (case get_deps name of

    NONE => []

  | SOME {master = (thy_path, _), ...} => thy_path :: Thy_Load.loaded_files (get_theory name)));

(** thy operations **)

(* remove theory *)

fun remove_thy name = NAMED_CRITICAL "Thy_Info" (fn () =>

  if is_finished name then error (loader_msg "attempt to change finished theory" [name])

  else

    let

      val succs = thy_graph Graph.all_succs [name];

      val _ = Output.urgent_message (loader_msg "removing" succs);

      val _ = List.app (perform Remove) succs;

      val _ = change_thys (Graph.del_nodes succs);

    in () end);

fun kill_thy name = NAMED_CRITICAL "Thy_Info" (fn () =>

  if known_thy name then remove_thy name

  else ());

(* scheduling loader tasks *)

datatype task =

  Task of string list * (theory list -> (theory * (unit -> unit))) |

  Finished of theory;

fun task_finished (Task _) = false

  | task_finished (Finished _) = true;

local

fun schedule_seq task_graph =

  ((Graph.topological_order task_graph, Symtab.empty) |-> fold (fn name => fn tab =>

    (case Graph.get_node task_graph name of

      Task (parents, body) =>

        let

          val (thy, after_load) = body (map (the o Symtab.lookup tab) parents);

          val _ = after_load ();

        in Symtab.update (name, thy) tab end

    | Finished thy => Symtab.update (name, thy) tab))) |> ignore;

fun schedule_futures task_graph = uninterruptible (fn _ => fn () =>

  let

    val tasks = Graph.topological_order task_graph;

    val futures = (tasks, Symtab.empty) |-> fold (fn name => fn tab =>

      (case Graph.get_node task_graph name of

        Task (parents, body) =>

          let

            val get = the o Symtab.lookup tab;

            val deps = map (`get) (Graph.imm_preds task_graph name);

            fun failed (future, parent) = if can Future.join future then NONE else SOME parent;

            val future = Future.fork_deps (map #1 deps) (fn () =>

              (case map_filter failed deps of

                [] => body (map (#1 o Future.join o get) parents)

              | bad => error (loader_msg

                  ("failed to load " ^ quote name ^ " (unresolved " ^ commas_quote bad ^ ")") [])));

          in Symtab.update (name, future) tab end

      | Finished thy => Symtab.update (name, Future.value (thy, I)) tab));

    val _ =

      tasks |> maps (fn name =>

        let

          val (thy, after_load) = Future.join (the (Symtab.lookup futures name));

          val _ = Global_Theory.join_proofs thy;

          val _ = after_load ();

        in [] end handle exn => [Exn.Exn exn])

      |> rev |> Exn.release_all;

  in () end) ();

in

fun schedule_tasks tasks =

  if not (Multithreading.enabled ()) then schedule_seq tasks

  else if Multithreading.self_critical () then

     (warning (loader_msg "no multithreading within critical section" []);

      schedule_seq tasks)

  else schedule_futures tasks;

end;

(* require_thy -- checking database entries wrt. the file-system *)

local

fun required_by _ [] = ""

  | required_by s initiators = s ^ "(required by " ^ show_path (rev initiators) ^ ")";

fun load_thy initiators update_time (deps: deps) text name parent_thys =

  let

    val _ = kill_thy name;

    val _ = Output.urgent_message ("Loading theory " ^ quote name ^ required_by " " initiators);

    val {master = (thy_path, _), imports} = deps;

    val dir = Path.dir thy_path;

    val pos = Path.position thy_path;

    val uses = map (apfst Path.explode) (#3 (Thy_Header.read pos text));

    fun init _ =

      Thy_Load.begin_theory dir name imports parent_thys uses

      |> Present.begin_theory update_time dir uses;

    val (after_load, theory) = Outer_Syntax.load_thy name init pos text;

    val parents = map Context.theory_name parent_thys;

    fun after_load' () =

     (after_load ();

      NAMED_CRITICAL "Thy_Info" (fn () =>

       (map get_theory parents;

        change_thys (new_entry name parents (SOME deps, SOME theory));

        perform Update name)));

  in (theory, after_load') end;

fun check_deps dir name =

  (case lookup_deps name of

    SOME NONE => (true, NONE, get_parents name, NONE)

  | NONE =>

      let val {master, text, imports, ...} = Thy_Load.deps_thy dir name

      in (false, SOME (make_deps master imports), imports, SOME text) end

  | SOME (SOME {master, imports}) =>

      let val master' = Thy_Load.check_thy dir name in

        if #2 master <> #2 master' then

          let val {text = text', imports = imports', ...} = Thy_Load.deps_thy dir name;

          in (false, SOME (make_deps master' imports'), imports', SOME text') end

        else

          let

            val current =

              (case lookup_theory name of

                NONE => false

              | SOME theory => Thy_Load.all_current theory);

            val deps' = SOME (make_deps master' imports);

          in (current, deps', imports, NONE) end

      end);

in

fun require_thys initiators dir strs tasks =

      fold_map (require_thy initiators dir) strs tasks |>> forall I

and require_thy initiators dir str tasks =

  let

    val path = Path.expand (Path.explode str);

    val name = Path.implode (Path.base path);

    val dir' = Path.append dir (Path.dir path);

    val _ = member (op =) initiators name andalso error (cycle_msg initiators);

  in

    (case try (Graph.get_node tasks) name of

      SOME task => (task_finished task, tasks)

    | NONE =>

        let

          val (current, deps, imports, opt_text) = check_deps dir' name

            handle ERROR msg => cat_error msg

              (loader_msg "the error(s) above occurred while examining theory" [name] ^

                required_by "\n" initiators);

          val parents = map base_name imports;

          val (parents_current, tasks') =

            require_thys (name :: initiators) (Path.append dir (master_dir deps)) imports tasks;

          val all_current = current andalso parents_current;

          val task =

            if all_current then Finished (get_theory name)

            else

              (case deps of

                NONE => raise Fail "Malformed deps"

              | SOME (dep as {master = (thy_path, _), ...}) =>

                  let

                    val text = (case opt_text of SOME text => text | NONE => File.read thy_path);

                    val update_time = serial ();

                  in Task (parents, load_thy initiators update_time dep text name) end);

        in (all_current, new_entry name parents task tasks') end)

  end;

end;

(* use_thy *)

fun use_thys_wrt dir arg =

  schedule_tasks (snd (require_thys [] dir arg Graph.empty));

val use_thys = use_thys_wrt Path.current;

val use_thy = use_thys o single;

(* toplevel begin theory -- without maintaining database *)

fun toplevel_begin_theory master name imports uses =

  let

    val dir = (case master of SOME dir => dir | NONE => Thy_Load.get_master_path ());

    val _ = kill_thy name;

    val _ = use_thys_wrt dir imports;

    val parent_thys = map (get_theory o base_name) imports;

  in Thy_Load.begin_theory dir name imports parent_thys uses end;

(* register theory *)

fun register_thy theory =

  let

    val name = Context.theory_name theory;

    val master = Thy_Load.check_thy (Thy_Load.master_directory theory) name;

    val parents = map Context.theory_name (Theory.parents_of theory);

    val imports = Thy_Load.imports_of theory;

    val deps = make_deps master imports;

  in

    NAMED_CRITICAL "Thy_Info" (fn () =>

     (kill_thy name;

      Output.urgent_message ("Registering theory " ^ quote name);

      map get_theory parents;

      change_thys (new_entry name parents (SOME deps, SOME theory));

      perform Update name))

  end;

(* finish all theories *)

fun finish () = change_thys (Graph.map (fn _ => fn (_, entry) => (NONE, entry)));

end;