src/Pure/Thy/thy_info.scala
author wenzelm
Sat Mar 14 19:51:36 2015 +0100 (2015-03-14)
changeset 59695 a03e0561bdbf
parent 59444 d57e275b2d82
child 59705 740a0ca7e09b
permissions -rw-r--r--
clarified positions of theory imports;
wenzelm@43651
     1
/*  Title:      Pure/Thy/thy_info.scala
wenzelm@43651
     2
    Author:     Makarius
wenzelm@43651
     3
wenzelm@43651
     4
Theory and file dependencies.
wenzelm@43651
     5
*/
wenzelm@43651
     6
wenzelm@43651
     7
package isabelle
wenzelm@43651
     8
wenzelm@43651
     9
wenzelm@56208
    10
class Thy_Info(resources: Resources)
wenzelm@43651
    11
{
wenzelm@43651
    12
  /* messages */
wenzelm@43651
    13
wenzelm@44615
    14
  private def show_path(names: List[Document.Node.Name]): String =
wenzelm@44615
    15
    names.map(name => quote(name.theory)).mkString(" via ")
wenzelm@43651
    16
wenzelm@44615
    17
  private def cycle_msg(names: List[Document.Node.Name]): String =
wenzelm@43651
    18
    "Cyclic dependency of " + show_path(names)
wenzelm@43651
    19
wenzelm@44615
    20
  private def required_by(initiators: List[Document.Node.Name]): String =
wenzelm@43651
    21
    if (initiators.isEmpty) ""
wenzelm@44615
    22
    else "\n(required by " + show_path(initiators.reverse) + ")"
wenzelm@43651
    23
wenzelm@43651
    24
wenzelm@43651
    25
  /* dependencies */
wenzelm@43651
    26
wenzelm@50414
    27
  sealed case class Dep(
wenzelm@50414
    28
    name: Document.Node.Name,
wenzelm@51294
    29
    header: Document.Node.Header)
wenzelm@50414
    30
  {
wenzelm@56393
    31
    def loaded_files(syntax: Prover.Syntax): List[String] =
wenzelm@51294
    32
    {
wenzelm@56823
    33
      val string = resources.with_thy_reader(name, reader => Symbol.decode(reader.source.toString))
wenzelm@56392
    34
      resources.loaded_files(syntax, string)
wenzelm@51294
    35
    }
wenzelm@50414
    36
  }
wenzelm@48872
    37
wenzelm@48872
    38
  object Dependencies
wenzelm@48872
    39
  {
wenzelm@55488
    40
    val empty = new Dependencies(Nil, Nil, Multi_Map.empty, Multi_Map.empty)
wenzelm@48872
    41
  }
wenzelm@48872
    42
wenzelm@48872
    43
  final class Dependencies private(
wenzelm@48872
    44
    rev_deps: List[Dep],
wenzelm@48873
    45
    val keywords: Thy_Header.Keywords,
wenzelm@55488
    46
    val seen_names: Multi_Map[String, Document.Node.Name],
wenzelm@55488
    47
    val seen_positions: Multi_Map[String, Position.T])
wenzelm@48871
    48
  {
wenzelm@48873
    49
    def :: (dep: Dep): Dependencies =
wenzelm@55488
    50
      new Dependencies(dep :: rev_deps, dep.header.keywords ::: keywords,
wenzelm@55488
    51
        seen_names, seen_positions)
wenzelm@48873
    52
wenzelm@55488
    53
    def + (thy: (Document.Node.Name, Position.T)): Dependencies =
wenzelm@55488
    54
    {
wenzelm@55488
    55
      val (name, pos) = thy
wenzelm@55488
    56
      new Dependencies(rev_deps, keywords,
wenzelm@55488
    57
        seen_names + (name.theory -> name),
wenzelm@55488
    58
        seen_positions + (name.theory -> pos))
wenzelm@55488
    59
    }
wenzelm@48872
    60
wenzelm@48872
    61
    def deps: List[Dep] = rev_deps.reverse
wenzelm@48872
    62
wenzelm@55488
    63
    def errors: List[String] =
wenzelm@55488
    64
    {
wenzelm@55488
    65
      val header_errors = deps.flatMap(dep => dep.header.errors)
wenzelm@55488
    66
      val import_errors =
wenzelm@55488
    67
        (for {
wenzelm@55488
    68
          (theory, names) <- seen_names.iterator_list
wenzelm@56208
    69
          if !resources.loaded_theories(theory)
wenzelm@55488
    70
          if names.length > 1
wenzelm@55488
    71
        } yield
wenzelm@55488
    72
          "Incoherent imports for theory " + quote(theory) + ":\n" +
wenzelm@55488
    73
            cat_lines(names.flatMap(name =>
wenzelm@55488
    74
              seen_positions.get_list(theory).map(pos =>
wenzelm@55488
    75
                "  " + quote(name.node) + Position.here(pos))))
wenzelm@55488
    76
        ).toList
wenzelm@55488
    77
      header_errors ::: import_errors
wenzelm@55488
    78
    }
wenzelm@54549
    79
wenzelm@56393
    80
    lazy val syntax: Prover.Syntax = resources.base_syntax.add_keywords(keywords)
wenzelm@51294
    81
wenzelm@48872
    82
    def loaded_theories: Set[String] =
wenzelm@56208
    83
      (resources.loaded_theories /: rev_deps) { case (loaded, dep) => loaded + dep.name.theory }
wenzelm@48872
    84
wenzelm@56392
    85
    def loaded_files: List[Path] =
wenzelm@51294
    86
    {
wenzelm@51298
    87
      val dep_files =
wenzelm@59136
    88
        Par_List.map(
wenzelm@59136
    89
          (dep: Dep) =>
wenzelm@59136
    90
            dep.loaded_files(syntax).map(a => Path.explode(dep.name.master_dir) + Path.explode(a)),
wenzelm@59136
    91
          rev_deps)
wenzelm@59136
    92
      ((Nil: List[Path]) /: dep_files) { case (acc_files, files) => files ::: acc_files }
wenzelm@51294
    93
    }
wenzelm@59444
    94
wenzelm@59444
    95
    def deps_graph(parent_session: String, parent_loaded: String => Boolean): Graph_Display.Graph =
wenzelm@59444
    96
    {
wenzelm@59444
    97
      val parent_session_node =
wenzelm@59444
    98
        Graph_Display.Node("[" + parent_session + "]", "session." + parent_session)
wenzelm@59444
    99
wenzelm@59444
   100
      def node(name: Document.Node.Name): Graph_Display.Node =
wenzelm@59444
   101
        if (parent_loaded(name.theory)) parent_session_node
wenzelm@59444
   102
        else Graph_Display.Node(name.theory, "theory." + name.theory)
wenzelm@59444
   103
wenzelm@59444
   104
      (Graph_Display.empty_graph /: rev_deps) {
wenzelm@59444
   105
        case (g, dep) =>
wenzelm@59444
   106
          if (parent_loaded(dep.name.theory)) g
wenzelm@59444
   107
          else {
wenzelm@59444
   108
            val a = node(dep.name)
wenzelm@59695
   109
            val bs = dep.header.imports.map({ case (name, _) => node(name) })
wenzelm@59444
   110
            ((g /: (a :: bs))(_.default_node(_, Nil)) /: bs)(_.add_edge(_, a))
wenzelm@59444
   111
          }
wenzelm@59444
   112
      }
wenzelm@59444
   113
    }
wenzelm@48871
   114
  }
wenzelm@43651
   115
wenzelm@56801
   116
  private def require_thys(session: String, initiators: List[Document.Node.Name],
wenzelm@55488
   117
      required: Dependencies, thys: List[(Document.Node.Name, Position.T)]): Dependencies =
wenzelm@56801
   118
    (required /: thys)(require_thy(session, initiators, _, _))
wenzelm@44615
   119
wenzelm@56801
   120
  private def require_thy(session: String, initiators: List[Document.Node.Name],
wenzelm@55488
   121
      required: Dependencies, thy: (Document.Node.Name, Position.T)): Dependencies =
wenzelm@44615
   122
  {
wenzelm@55488
   123
    val (name, require_pos) = thy
wenzelm@55488
   124
    val theory = name.theory
wenzelm@55488
   125
wenzelm@55488
   126
    def message: String =
wenzelm@55488
   127
      "The error(s) above occurred for theory " + quote(theory) +
wenzelm@55488
   128
        required_by(initiators) + Position.here(require_pos)
wenzelm@55488
   129
wenzelm@55488
   130
    val required1 = required + thy
wenzelm@56208
   131
    if (required.seen_names.isDefinedAt(theory) || resources.loaded_theories(theory))
wenzelm@55488
   132
      required1
wenzelm@43651
   133
    else {
wenzelm@43651
   134
      try {
wenzelm@44615
   135
        if (initiators.contains(name)) error(cycle_msg(initiators))
wenzelm@51294
   136
        val header =
wenzelm@56801
   137
          try { resources.check_thy(session, name).cat_errors(message) }
wenzelm@54549
   138
          catch { case ERROR(msg) => cat_error(msg, message) }
wenzelm@59695
   139
        Dep(name, header) :: require_thys(session, name :: initiators, required1, header.imports)
wenzelm@43651
   140
      }
wenzelm@48707
   141
      catch {
wenzelm@48707
   142
        case e: Throwable =>
wenzelm@55488
   143
          Dep(name, Document.Node.bad_header(Exn.message(e))) :: required1
wenzelm@48707
   144
      }
wenzelm@43651
   145
    }
wenzelm@43651
   146
  }
wenzelm@43651
   147
wenzelm@56801
   148
  def dependencies(session: String, thys: List[(Document.Node.Name, Position.T)]): Dependencies =
wenzelm@56801
   149
    require_thys(session, Nil, Dependencies.empty, thys)
wenzelm@43651
   150
}