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