dependencies of entries vs. sessions;
authorwenzelm
Mon Oct 09 20:26:02 2017 +0200 (19 months ago)
changeset 66821c0e8c199cb2e
parent 66820 fc516da7ee4f
child 66822 4642cf4a7ebb
dependencies of entries vs. sessions;
json output like "isabelle afp_dependencies";
misc tuning;
src/Pure/Admin/afp.scala
     1.1 --- a/src/Pure/Admin/afp.scala	Mon Oct 09 17:09:08 2017 +0200
     1.2 +++ b/src/Pure/Admin/afp.scala	Mon Oct 09 20:26:02 2017 +0200
     1.3 @@ -9,24 +9,78 @@
     1.4  
     1.5  object AFP
     1.6  {
     1.7 -  sealed case class Entry(name: String, sessions: List[String])
     1.8 +  def init(base_dir: Path = Path.explode("$AFP_BASE")): AFP =
     1.9 +    new AFP(base_dir)
    1.10  
    1.11 -  def init(base_dir: Path = Path.explode("$AFP_BASE")): AFP = new AFP(base_dir)
    1.12 +  sealed case class Entry(name: String, sessions: List[String])
    1.13 +  {
    1.14 +    def sessions_deps(afp_sessions: Sessions.T): List[String] =
    1.15 +      sessions.flatMap(afp_sessions.imports_graph.imm_preds(_)).distinct.sorted
    1.16 +  }
    1.17  }
    1.18  
    1.19  class AFP private(val base_dir: Path)
    1.20  {
    1.21 +  override def toString: String = base_dir.expand.toString
    1.22 +
    1.23    val main_dir: Path = base_dir + Path.explode("thys")
    1.24  
    1.25 +
    1.26 +  /* entries and sessions */
    1.27 +
    1.28    val entries: List[AFP.Entry] =
    1.29 -    (for (name <- Sessions.parse_roots(main_dir + Sessions.ROOTS))
    1.30 -    yield {
    1.31 +    (for (name <- Sessions.parse_roots(main_dir + Sessions.ROOTS)) yield {
    1.32        val sessions =
    1.33          Sessions.parse_root_entries(main_dir + Path.explode(name) + Sessions.ROOT).map(_.name)
    1.34        AFP.Entry(name, sessions)
    1.35      }).sortBy(_.name)
    1.36  
    1.37 -  val sessions: List[String] = entries.flatMap(_.sessions).sorted
    1.38 +  val sessions: List[String] = entries.flatMap(_.sessions)
    1.39 +  val sessions_set: Set[String] = sessions.toSet
    1.40 +
    1.41 +
    1.42 +  /* dependencies */
    1.43 +
    1.44 +  def dependencies(options: Options): Dependencies =
    1.45 +  {
    1.46 +    val (_, afp_sessions) =
    1.47 +      Sessions.load(options, dirs = List(main_dir)).
    1.48 +        selection(Sessions.Selection(sessions = sessions.toList))
    1.49 +
    1.50 +    val session_entries =
    1.51 +      (Multi_Map.empty[String, String] /: entries) { case (m1, e) =>
    1.52 +        (m1 /: e.sessions) { case (m2, s) => m2.insert(s, e.name) }
    1.53 +      }
    1.54  
    1.55 -  override def toString: String = base_dir.expand.toString
    1.56 +    val entries_graph: Graph[String, Unit] =
    1.57 +      (Graph.empty[String, Unit] /: entries) { case (g, e1) =>
    1.58 +        val name1 = e1.name
    1.59 +        val g1 = g.default_node(name1, ())
    1.60 +        (g1 /: e1.sessions_deps(afp_sessions)) { case (g2, s2) =>
    1.61 +          (g2 /: session_entries.get_list(s2)) { case (g3, name2) =>
    1.62 +            if (name1 == name2) g3 else g3.default_node(name2, ()).add_edge(name2, name1)
    1.63 +          }
    1.64 +        }
    1.65 +      }
    1.66 +
    1.67 +    new Dependencies(afp_sessions, entries_graph)
    1.68 +  }
    1.69 +
    1.70 +  final class Dependencies private [AFP](
    1.71 +    val afp_sessions: Sessions.T,
    1.72 +    val entries_graph: Graph[String, Unit])
    1.73 +  {
    1.74 +    def entries_json_text: String =
    1.75 +      (for (entry <- entries)
    1.76 +      yield {
    1.77 +        val distrib_deps = entry.sessions_deps(afp_sessions).filterNot(sessions_set)
    1.78 +        val afp_deps = entries_graph.imm_preds(entry.name).toList
    1.79 +        """
    1.80 + {""" + JSON.Format(entry.name) + """:
    1.81 +  {"distrib_deps": """ + JSON.Format(distrib_deps) + """,
    1.82 +   "afp_deps": """ + JSON.Format(afp_deps) + """
    1.83 +  }
    1.84 + }"""
    1.85 +      }).mkString("[", ", ", "\n]\n")
    1.86 +  }
    1.87  }