src/Pure/Tools/imports.scala
author wenzelm
Tue Nov 07 16:50:26 2017 +0100 (23 months ago)
changeset 67026 687c822ee5e3
parent 67025 961285f581e6
child 68204 a554da2811f2
permissions -rw-r--r--
tuned signature;
     1 /*  Title:      Pure/Tools/imports.scala
     2     Author:     Makarius
     3 
     4 Maintain theory imports wrt. session structure.
     5 */
     6 
     7 package isabelle
     8 
     9 
    10 import java.io.{File => JFile}
    11 
    12 
    13 object Imports
    14 {
    15   /* repository files */
    16 
    17   def repository_files(progress: Progress, start: Path, pred: JFile => Boolean = _ => true)
    18       : List[JFile] =
    19     Mercurial.find_repository(start) match {
    20       case None =>
    21         progress.echo_warning("Ignoring directory " + start + " (no Mercurial repository)")
    22         Nil
    23       case Some(hg) =>
    24         val start_path = start.canonical_file.toPath
    25         for {
    26           name <- hg.known_files()
    27           file = (hg.root + Path.explode(name)).file
    28           if pred(file) && File.canonical(file).toPath.startsWith(start_path)
    29         } yield file
    30     }
    31 
    32 
    33   /* report imports */
    34 
    35   sealed case class Report(
    36     info: Sessions.Info,
    37     declared_imports: Set[String],
    38     potential_imports: Option[List[String]],
    39     actual_imports: Option[List[String]])
    40   {
    41     def print(keywords: Keyword.Keywords, result: List[String]): String =
    42     {
    43       def print_name(name: String): String = Token.quote_name(keywords, name)
    44 
    45       "  session " + print_name(info.name) + ": " + result.map(print_name(_)).mkString(" ")
    46     }
    47   }
    48 
    49 
    50   /* update imports */
    51 
    52   sealed case class Update(range: Text.Range, old_text: String, new_text: String)
    53   {
    54     def edits: List[Text.Edit] =
    55       Text.Edit.replace(range.start, old_text, new_text)
    56 
    57     override def toString: String =
    58       range.toString + ": " + old_text + " -> " + new_text
    59   }
    60 
    61   def update_name(keywords: Keyword.Keywords, pos: Position.T, update: String => String)
    62     : Option[(JFile, Update)] =
    63   {
    64     val file =
    65       pos match {
    66         case Position.File(file) => Path.explode(file).canonical_file
    67         case _ => error("Missing file in position" + Position.here(pos))
    68       }
    69 
    70     val text = File.read(file)
    71 
    72     val range =
    73       pos match {
    74         case Position.Range(symbol_range) => Symbol.Text_Chunk(text).decode(symbol_range)
    75         case _ => error("Missing range in position" + Position.here(pos))
    76       }
    77 
    78     Token.read_name(keywords, range.substring(text)) match {
    79       case Some(tok) =>
    80         val s1 = tok.source
    81         val s2 = Token.quote_name(keywords, update(tok.content))
    82         if (s1 == s2) None else Some((file, Update(range, s1, s2)))
    83       case None => error("Name token expected" + Position.here(pos))
    84     }
    85   }
    86 
    87 
    88   /* collective operations */
    89 
    90   def imports(
    91     options: Options,
    92     operation_imports: Boolean = false,
    93     operation_repository_files: Boolean = false,
    94     operation_update: Boolean = false,
    95     update_message: String = "",
    96     progress: Progress = No_Progress,
    97     selection: Sessions.Selection = Sessions.Selection.empty,
    98     dirs: List[Path] = Nil,
    99     select_dirs: List[Path] = Nil,
   100     verbose: Boolean = false) =
   101   {
   102     val full_sessions = Sessions.load_structure(options, dirs = dirs, select_dirs = select_dirs)
   103     val selected_sessions = full_sessions.selection(selection)
   104 
   105     val deps =
   106       Sessions.deps(selected_sessions, full_sessions.global_theories,
   107         progress = progress, verbose = verbose).check_errors
   108 
   109     val root_keywords = Sessions.root_syntax.keywords
   110 
   111     if (operation_imports) {
   112       val report_imports: List[Report] =
   113         selected_sessions.build_topological_order.map((session_name: String) =>
   114           {
   115             val info = selected_sessions(session_name)
   116             val session_base = deps(session_name)
   117 
   118             val declared_imports =
   119               selected_sessions.imports_requirements(List(session_name)).toSet
   120 
   121             val extra_imports =
   122               (for {
   123                 (_, a) <- session_base.known.theories.iterator
   124                 if session_base.theory_qualifier(a) == info.name
   125                 b <- deps.all_known.get_file(a.path.file)
   126                 qualifier = session_base.theory_qualifier(b)
   127                 if !declared_imports.contains(qualifier)
   128               } yield qualifier).toSet
   129 
   130             val loaded_imports =
   131               selected_sessions.imports_requirements(
   132                 session_base.loaded_theories.keys.map(a =>
   133                   session_base.theory_qualifier(session_base.known.theories(a))))
   134               .toSet - session_name
   135 
   136             val minimal_imports =
   137               loaded_imports.filter(s1 =>
   138                 !loaded_imports.exists(s2 => selected_sessions.imports_graph.is_edge(s1, s2)))
   139 
   140             def make_result(set: Set[String]): Option[List[String]] =
   141               if (set.isEmpty) None
   142               else Some(selected_sessions.imports_topological_order.filter(set))
   143 
   144             Report(info, declared_imports, make_result(extra_imports),
   145               if (loaded_imports == declared_imports - session_name) None
   146               else make_result(minimal_imports))
   147           })
   148 
   149       progress.echo("\nPotential session imports:")
   150       for {
   151         report <- report_imports.sortBy(_.declared_imports.size)
   152         potential_imports <- report.potential_imports
   153       } progress.echo(report.print(root_keywords, potential_imports))
   154 
   155       progress.echo("\nActual session imports:")
   156       for {
   157         report <- report_imports
   158         actual_imports <- report.actual_imports
   159       } progress.echo(report.print(root_keywords, actual_imports))
   160     }
   161 
   162     if (operation_repository_files) {
   163       progress.echo("\nMercurial repository check:")
   164       val unused_files =
   165         for {
   166           (_, dir) <- Sessions.directories(dirs, select_dirs)
   167           file <- repository_files(progress, dir, file => file.getName.endsWith(".thy"))
   168           if deps.all_known.get_file(file).isEmpty
   169         } yield file
   170       unused_files.foreach(file => progress.echo("unused file " + quote(file.toString)))
   171     }
   172 
   173     if (operation_update) {
   174       progress.echo("\nUpdate theory imports" + update_message + ":")
   175       val updates =
   176         selected_sessions.build_topological_order.flatMap(session_name =>
   177           {
   178             val info = selected_sessions(session_name)
   179             val session_base = deps(session_name)
   180             val session_resources = new Resources(session_base)
   181             val imports_base = session_base.get_imports
   182             val imports_resources = new Resources(imports_base)
   183 
   184             def standard_import(qualifier: String, dir: String, s: String): String =
   185               imports_resources.standard_import(session_base, qualifier, dir, s)
   186 
   187             val updates_root =
   188               for {
   189                 (_, pos) <- info.theories.flatMap(_._2)
   190                 upd <- update_name(root_keywords, pos, standard_import(info.name, info.dir.implode, _))
   191               } yield upd
   192 
   193             val updates_theories =
   194               for {
   195                 (_, name) <- session_base.known.theories_local.toList
   196                 if session_base.theory_qualifier(name) == info.name
   197                 (_, pos) <- session_resources.check_thy(name, Token.Pos.file(name.node)).imports
   198                 upd <- update_name(session_base.overall_syntax.keywords, pos,
   199                   standard_import(session_base.theory_qualifier(name), name.master_dir, _))
   200               } yield upd
   201 
   202             updates_root ::: updates_theories
   203           })
   204 
   205       val file_updates = (Multi_Map.empty[JFile, Update] /: updates)(_ + _)
   206       val conflicts =
   207         file_updates.iterator_list.flatMap({ case (file, upds) =>
   208           Library.duplicates(upds.sortBy(_.range.start),
   209             (x: Update, y: Update) => x.range overlaps y.range) match
   210           {
   211             case Nil => None
   212             case bad => Some((file, bad))
   213           }
   214         })
   215       if (conflicts.nonEmpty)
   216         error(cat_lines(
   217           conflicts.map({ case (file, bad) =>
   218             "Conflicting updates for file " + file + bad.mkString("\n  ", "\n  ", "") })))
   219 
   220       for ((file, upds) <- file_updates.iterator_list.toList.sortBy(p => p._1.toString)) {
   221         progress.echo("file " + quote(file.toString))
   222         val edits =
   223           upds.sortBy(upd => - upd.range.start).flatMap(upd =>
   224             Text.Edit.replace(upd.range.start, upd.old_text, upd.new_text))
   225         val new_text =
   226           (File.read(file) /: edits)({ case (text, edit) =>
   227             edit.edit(text, 0) match {
   228               case (None, text1) => text1
   229               case (Some(_), _) => error("Failed to apply edit " + edit + " to file " + file)
   230             }
   231           })
   232         File.write_backup2(Path.explode(File.standard_path(file)), new_text)
   233       }
   234     }
   235   }
   236 
   237 
   238   /* Isabelle tool wrapper */
   239 
   240   val isabelle_tool =
   241     Isabelle_Tool("imports", "maintain theory imports wrt. session structure", args =>
   242     {
   243       var base_sessions: List[String] = Nil
   244       var select_dirs: List[Path] = Nil
   245       var operation_imports = false
   246       var operation_repository_files = false
   247       var requirements = false
   248       var operation_update = false
   249       var exclude_session_groups: List[String] = Nil
   250       var all_sessions = false
   251       var dirs: List[Path] = Nil
   252       var session_groups: List[String] = Nil
   253       var incremental_update = false
   254       var options = Options.init()
   255       var verbose = false
   256       var exclude_sessions: List[String] = Nil
   257 
   258       val getopts = Getopts("""
   259 Usage: isabelle imports [OPTIONS] [SESSIONS ...]
   260 
   261   Options are:
   262     -B NAME      include session NAME and all descendants
   263     -D DIR       include session directory and select its sessions
   264     -I           operation: report session imports
   265     -M           operation: Mercurial repository check for theory files
   266     -R           operate on requirements of selected sessions
   267     -U           operation: update theory imports to use session qualifiers
   268     -X NAME      exclude sessions from group NAME and all descendants
   269     -a           select all sessions
   270     -d DIR       include session directory
   271     -g NAME      select session group NAME
   272     -i           incremental update according to session graph structure
   273     -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
   274     -v           verbose
   275     -x NAME      exclude session NAME and all descendants
   276 
   277   Maintain theory imports wrt. session structure. At least one operation
   278   needs to be specified (see options -I -M -U).
   279 """,
   280       "B:" -> (arg => base_sessions = base_sessions ::: List(arg)),
   281       "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
   282       "I" -> (_ => operation_imports = true),
   283       "M" -> (_ => operation_repository_files = true),
   284       "R" -> (_ => requirements = true),
   285       "U" -> (_ => operation_update = true),
   286       "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
   287       "a" -> (_ => all_sessions = true),
   288       "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
   289       "g:" -> (arg => session_groups = session_groups ::: List(arg)),
   290       "i" -> (_ => incremental_update = true),
   291       "o:" -> (arg => options = options + arg),
   292       "v" -> (_ => verbose = true),
   293       "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
   294 
   295       val sessions = getopts(args)
   296       if (args.isEmpty || !(operation_imports || operation_repository_files || operation_update))
   297         getopts.usage()
   298 
   299       val selection =
   300         Sessions.Selection(requirements, all_sessions, base_sessions, exclude_session_groups,
   301           exclude_sessions, session_groups, sessions)
   302 
   303       val progress = new Console_Progress(verbose = verbose)
   304 
   305       if (operation_imports || operation_repository_files ||
   306           operation_update && !incremental_update)
   307       {
   308         imports(options, operation_imports = operation_imports,
   309           operation_repository_files = operation_repository_files,
   310           operation_update = operation_update,
   311           progress = progress, selection = selection, dirs = dirs, select_dirs = select_dirs,
   312           verbose = verbose)
   313       }
   314       else if (operation_update && incremental_update) {
   315         Sessions.load_structure(options, dirs = dirs, select_dirs = select_dirs).
   316           selection(selection).imports_topological_order.foreach(name =>
   317             {
   318               imports(options, operation_update = operation_update, progress = progress,
   319                 update_message = " for session " + quote(name),
   320                 selection = Sessions.Selection(sessions = List(name)),
   321                 dirs = dirs ::: select_dirs, verbose = verbose)
   322             })
   323       }
   324     })
   325 }