1/*  Title:      Pure/Tools/imports.scala
2    Author:     Makarius
3
4Maintain theory imports wrt. session structure.
5*/
6
7package isabelle
8
9
10import java.io.{File => JFile}
11
12
13object 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 deps =
103      Sessions.load_structure(options, dirs = dirs, select_dirs = select_dirs).
104        selection_deps(selection, progress = progress, verbose = verbose).check_errors
105
106    val root_keywords = Sessions.root_syntax.keywords
107
108    if (operation_imports) {
109      val report_imports: List[Report] =
110        deps.sessions_structure.build_topological_order.map((session_name: String) =>
111          {
112            val info = deps.sessions_structure(session_name)
113            val session_base = deps(session_name)
114
115            val declared_imports =
116              deps.sessions_structure.imports_requirements(List(session_name)).toSet
117
118            val extra_imports =
119              (for {
120                a <- session_base.known.theory_names
121                if session_base.theory_qualifier(a) == info.name
122                b <- deps.all_known.get_file(a.path.file)
123                qualifier = session_base.theory_qualifier(b)
124                if !declared_imports.contains(qualifier)
125              } yield qualifier).toSet
126
127            val loaded_imports =
128              deps.sessions_structure.imports_requirements(
129                session_base.loaded_theories.keys.map(a =>
130                  session_base.theory_qualifier(session_base.known.theories(a).name)))
131              .toSet - session_name
132
133            val minimal_imports =
134              loaded_imports.filter(s1 =>
135                !loaded_imports.exists(s2 => deps.sessions_structure.imports_graph.is_edge(s1, s2)))
136
137            def make_result(set: Set[String]): Option[List[String]] =
138              if (set.isEmpty) None
139              else Some(deps.sessions_structure.imports_topological_order.filter(set))
140
141            Report(info, declared_imports, make_result(extra_imports),
142              if (loaded_imports == declared_imports - session_name) None
143              else make_result(minimal_imports))
144          })
145
146      progress.echo("\nPotential session imports:")
147      for {
148        report <- report_imports.sortBy(_.declared_imports.size)
149        potential_imports <- report.potential_imports
150      } progress.echo(report.print(root_keywords, potential_imports))
151
152      progress.echo("\nActual session imports:")
153      for {
154        report <- report_imports
155        actual_imports <- report.actual_imports
156      } progress.echo(report.print(root_keywords, actual_imports))
157    }
158
159    if (operation_repository_files) {
160      progress.echo("\nMercurial repository check:")
161      val unused_files =
162        for {
163          (_, dir) <- Sessions.directories(dirs, select_dirs)
164          file <- repository_files(progress, dir, file => file.getName.endsWith(".thy"))
165          if deps.all_known.get_file(file).isEmpty
166        } yield file
167      unused_files.foreach(file => progress.echo("unused file " + quote(file.toString)))
168    }
169
170    if (operation_update) {
171      progress.echo("\nUpdate theory imports" + update_message + ":")
172      val updates =
173        deps.sessions_structure.build_topological_order.flatMap(session_name =>
174          {
175            val info = deps.sessions_structure(session_name)
176            val session_base = deps(session_name)
177            val session_resources = new Resources(session_base)
178            val imports_base = session_base.get_imports
179            val imports_resources = new Resources(imports_base)
180
181            def standard_import(qualifier: String, dir: String, s: String): String =
182              imports_resources.standard_import(session_base, qualifier, dir, s)
183
184            val updates_root =
185              for {
186                (_, pos) <- info.theories.flatMap(_._2)
187                upd <- update_name(root_keywords, pos, standard_import(info.name, info.dir.implode, _))
188              } yield upd
189
190            val updates_theories =
191              (for {
192                name <- session_base.known.theories_local.iterator.map(p => p._2.name)
193                if session_base.theory_qualifier(name) == info.name
194                (_, pos) <- session_resources.check_thy(name, Token.Pos.file(name.node)).imports
195                upd <- update_name(session_base.overall_syntax.keywords, pos,
196                  standard_import(session_base.theory_qualifier(name), name.master_dir, _))
197              } yield upd).toList
198
199            updates_root ::: updates_theories
200          })
201
202      val file_updates = (Multi_Map.empty[JFile, Update] /: updates)(_ + _)
203      val conflicts =
204        file_updates.iterator_list.flatMap({ case (file, upds) =>
205          Library.duplicates(upds.sortBy(_.range.start),
206            (x: Update, y: Update) => x.range overlaps y.range) match
207          {
208            case Nil => None
209            case bad => Some((file, bad))
210          }
211        })
212      if (conflicts.nonEmpty)
213        error(cat_lines(
214          conflicts.map({ case (file, bad) =>
215            "Conflicting updates for file " + file + bad.mkString("\n  ", "\n  ", "") })))
216
217      for ((file, upds) <- file_updates.iterator_list.toList.sortBy(p => p._1.toString)) {
218        progress.echo("file " + quote(file.toString))
219        val edits =
220          upds.sortBy(upd => - upd.range.start).flatMap(upd =>
221            Text.Edit.replace(upd.range.start, upd.old_text, upd.new_text))
222        val new_text =
223          (File.read(file) /: edits)({ case (text, edit) =>
224            edit.edit(text, 0) match {
225              case (None, text1) => text1
226              case (Some(_), _) => error("Failed to apply edit " + edit + " to file " + file)
227            }
228          })
229        File.write_backup2(Path.explode(File.standard_path(file)), new_text)
230      }
231    }
232  }
233
234
235  /* Isabelle tool wrapper */
236
237  val isabelle_tool =
238    Isabelle_Tool("imports", "maintain theory imports wrt. session structure", args =>
239    {
240      var base_sessions: List[String] = Nil
241      var select_dirs: List[Path] = Nil
242      var operation_imports = false
243      var operation_repository_files = false
244      var requirements = false
245      var operation_update = false
246      var exclude_session_groups: List[String] = Nil
247      var all_sessions = false
248      var dirs: List[Path] = Nil
249      var session_groups: List[String] = Nil
250      var incremental_update = false
251      var options = Options.init()
252      var verbose = false
253      var exclude_sessions: List[String] = Nil
254
255      val getopts = Getopts("""
256Usage: isabelle imports [OPTIONS] [SESSIONS ...]
257
258  Options are:
259    -B NAME      include session NAME and all descendants
260    -D DIR       include session directory and select its sessions
261    -I           operation: report session imports
262    -M           operation: Mercurial repository check for theory files
263    -R           operate on requirements of selected sessions
264    -U           operation: update theory imports to use session qualifiers
265    -X NAME      exclude sessions from group NAME and all descendants
266    -a           select all sessions
267    -d DIR       include session directory
268    -g NAME      select session group NAME
269    -i           incremental update according to session graph structure
270    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
271    -v           verbose
272    -x NAME      exclude session NAME and all descendants
273
274  Maintain theory imports wrt. session structure. At least one operation
275  needs to be specified (see options -I -M -U).
276""",
277      "B:" -> (arg => base_sessions = base_sessions ::: List(arg)),
278      "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
279      "I" -> (_ => operation_imports = true),
280      "M" -> (_ => operation_repository_files = true),
281      "R" -> (_ => requirements = true),
282      "U" -> (_ => operation_update = true),
283      "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
284      "a" -> (_ => all_sessions = true),
285      "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
286      "g:" -> (arg => session_groups = session_groups ::: List(arg)),
287      "i" -> (_ => incremental_update = true),
288      "o:" -> (arg => options = options + arg),
289      "v" -> (_ => verbose = true),
290      "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
291
292      val sessions = getopts(args)
293      if (args.isEmpty || !(operation_imports || operation_repository_files || operation_update))
294        getopts.usage()
295
296      val selection =
297        Sessions.Selection(requirements, all_sessions, base_sessions, exclude_session_groups,
298          exclude_sessions, session_groups, sessions)
299
300      val progress = new Console_Progress(verbose = verbose)
301
302      if (operation_imports || operation_repository_files ||
303          operation_update && !incremental_update)
304      {
305        imports(options, operation_imports = operation_imports,
306          operation_repository_files = operation_repository_files,
307          operation_update = operation_update,
308          progress = progress, selection = selection, dirs = dirs, select_dirs = select_dirs,
309          verbose = verbose)
310      }
311      else if (operation_update && incremental_update) {
312        Sessions.load_structure(options, dirs = dirs, select_dirs = select_dirs).
313          selection(selection).imports_topological_order.foreach(name =>
314            {
315              imports(options, operation_update = operation_update, progress = progress,
316                update_message = " for session " + quote(name),
317                selection = Sessions.Selection(sessions = List(name)),
318                dirs = dirs ::: select_dirs, verbose = verbose)
319            })
320      }
321    })
322}
323