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