diff --git a/tools/afp_dependencies.scala b/tools/afp_dependencies.scala --- a/tools/afp_dependencies.scala +++ b/tools/afp_dependencies.scala @@ -1,86 +1,79 @@ /* Author: Fabian Huch, TU Muenchen Tool to extract dependencies of AFP entries. */ package afp import isabelle._ object AFP_Dependencies { case class Dependency( entry: Metadata.Entry.Name, distrib_deps: List[Metadata.Entry.Name], afp_deps: List[Metadata.Entry.Name]) object JSON { private def from_dep(dependency: Dependency): (String, isabelle.JSON.T) = dependency.entry -> isabelle.JSON.Object( "distrib_deps" -> dependency.distrib_deps, - "afp_deps" -> dependency.afp_deps - ) + "afp_deps" -> dependency.afp_deps) - def from_dependency(dep: Dependency): isabelle.JSON.T = - isabelle.JSON.Object(from_dep(dep)) + def from_dependency(dep: Dependency): isabelle.JSON.T = isabelle.JSON.Object(from_dep(dep)) - def from_dependencies(deps: List[Dependency]): isabelle.JSON.T = - deps.map(from_dep).toMap + def from_dependencies(deps: List[Dependency]): isabelle.JSON.T = deps.map(from_dep).toMap } def afp_dependencies(afp_dir: Path): List[Dependency] = { val tree = Sessions.load_structure(Options.init(), Nil, List(afp_dir)) - val selected = tree.selection(Sessions.Selection(false, false, Nil, Nil, Nil, Nil)) - .build_graph.keys + val selected = + tree.selection(Sessions.Selection(false, false, Nil, Nil, Nil, Nil)).build_graph.keys - def get_entry(name: String): Option[String] = - { + def get_entry(name: String): Option[String] = { val info = tree(name) val dir = info.dir - if (selected.contains(dir.dir.expand)) - None - else - Some(dir.base.implode) + if (selected.contains(dir.dir.expand)) None else Some(dir.base.implode) } selected.groupBy(get_entry).toList.collect { case (Some(e), sessions) => - val dependencies = sessions.flatMap(tree.imports_graph.imm_preds) - .map(d => (d, get_entry(d))) + val dependencies = + sessions.flatMap(tree.imports_graph.imm_preds).map(d => (d, get_entry(d))) val distrib_deps = dependencies.collect { case (d, None) => d }.distinct val afp_deps = dependencies.collect { case (_, Some(d)) if d != e => d }.distinct Dependency(e, distrib_deps, afp_deps) } } val isabelle_tool = Isabelle_Tool("afp_dependencies", "extract dependencies between AFP entries", Scala_Project.here, { args => var output_file: Option[Path] = None val getopts = Getopts(""" Usage: isabelle afp_dependencies [OPTIONS] Options are: -o FILE output file name Extract dependencies between AFP entries. """, "o:" -> (arg => output_file = Some(Path.explode(arg)))) getopts(args) val afp_dir = Path.explode("$AFP").expand val progress = new Console_Progress() val res = afp_dependencies(afp_dir).map(JSON.from_dependency) val json = isabelle.JSON.Format(res) output_file match { case Some(file) => File.write(file, json) case None => progress.echo(json) } }) } diff --git a/tools/afp_site_gen.scala b/tools/afp_site_gen.scala --- a/tools/afp_site_gen.scala +++ b/tools/afp_site_gen.scala @@ -1,485 +1,485 @@ /* Author: Fabian Huch, TU Muenchen Generation and compilation of SSG project for the AFP website. */ package afp import isabelle.* import afp.Metadata.{Affiliation, Author, ACM, AMS, Classification, DOI, Email, Entry, Formatted, Homepage, Reference, Release, Topic, Unaffiliated} object AFP_Site_Gen { /* cache */ class Cache(layout: Hugo.Layout, progress: Progress = new Progress()) { private val doi_cache = Path.basic("dois.json") private var dois: Map[String, String] = { val file = layout.cache_dir + doi_cache if (file.file.exists) { val content = File.read(file) val json = try { isabelle.JSON.parse(content) } catch { case ERROR(msg) => error("Could not parse " + file.toString + ": " + msg) } JSON.to_dois(json) } else { progress.echo_warning("No DOI cache found - resolving might take some time") Map.empty } } def resolve_doi(doi: DOI): String = { dois.get(doi.identifier) match { case Some(value) => value case None => val res = doi.formatted() dois += (doi.identifier -> res) layout.write_cache(doi_cache, JSON.from_dois(dois)) res } } } /* json */ object JSON { type T = isabelle.JSON.T object Object { type T = isabelle.JSON.Object.T def apply(entries: isabelle.JSON.Object.Entry*): T = isabelle.JSON.Object.apply(entries: _*) } def opt(k: String, v: String): Object.T = if (v.isEmpty) Object() else Object(k -> v) def opt(k: String, v: Option[T]): Object.T = v.map(v => Object(k -> v)).getOrElse(Object()) def opt[A <: Iterable[_]](k: String, vals: A): Object.T = if (vals.isEmpty) Object() else Object(k -> vals) def from_dois(dois: Map[String, String]): Object.T = dois def to_dois(dois: T): Map[String, String] = dois match { case m: Map[_, _] if m.keySet.forall(_.isInstanceOf[String]) && m.values.forall(_.isInstanceOf[String]) => m.asInstanceOf[Map[String, String]] case _ => error("Could not read dois") } def from_email(email: Email): Object.T = Object( "user" -> email.user.split('.').toList, "host" -> email.host.split('.').toList) def from_authors(authors: List[Author]): Object.T = authors.map(author => author.id -> (Object( "name" -> author.name, "emails" -> author.emails.map(from_email), "homepages" -> author.homepages.map(_.url.toString)) ++ opt("orcid", author.orcid.map(orcid => Object( "id" -> orcid.identifier, "url" -> orcid.url.toString))))).toMap def from_classification(classification: Classification): Object.T = Object( "desc" -> classification.desc, "url" -> classification.url.toString, "type" -> (classification match { case _: ACM => "ACM" case _: AMS => "AMS" })) def from_topics(topics: List[Topic]): Object.T = Object(topics.map(topic => topic.name -> ( opt("classification", topic.classification.map(from_classification)) ++ opt("topics", from_topics(topic.sub_topics)))): _*) def from_affiliations(affiliations: List[Affiliation]): Object.T = { Utils.group_sorted(affiliations, (a: Affiliation) => a.author).view.mapValues( { author_affiliations => val homepage = author_affiliations.collectFirst { case homepage: Homepage => homepage } val email = author_affiliations.collectFirst { case email: Email => email } Object() ++ opt("homepage", homepage.map(_.url.toString)) ++ opt("email", email.map(from_email)) }).toMap } def from_change_history(entry: (Metadata.Date, String)): Object.T = Object( "date" -> entry._1.toString, "value" -> entry._2) def from_release(release: Release): Object.T = Object( "date" -> release.date.toString, "isabelle" -> release.isabelle) def from_related(related: Reference, cache: Cache): T = related match { case d: DOI => val href = d.url.toString cache.resolve_doi(d).replace(href, "" + href + "") case Formatted(text) => text } def from_entry(entry: Entry, cache: Cache): Object.T = ( Object( "title" -> entry.title, "authors" -> entry.authors.map(_.author).distinct, "affiliations" -> from_affiliations(entry.authors ++ entry.contributors), "date" -> entry.date.toString, "topics" -> entry.topics.map(_.id), "abstract" -> entry.`abstract`, "license" -> entry.license.name) ++ opt("contributors", entry.contributors.map(_.author).distinct) ++ opt("releases", entry.releases.sortBy(_.isabelle).reverse.map(from_release)) ++ opt("note", entry.note) ++ opt("history", entry.change_history.toList.sortBy(_._1).reverse.map(from_change_history)) ++ opt("extra", entry.extra) ++ opt("related", entry.related.map(from_related(_, cache)))) def from_keywords(keywords: List[String]): T = keywords.sorted.map(keyword => Object("keyword" -> keyword)) } /* stats */ def afp_stats(deps: Sessions.Deps, structure: AFP_Structure, entries: List[Entry]): JSON.T = { def round(int: Int): Int = Math.round(int.toFloat / 100) * 100 def nodes(entry: Entry): List[Document.Node.Name] = - structure.entry_sessions(entry.name) - .flatMap(session => deps(session.name).proper_session_theories) + structure.entry_sessions(entry.name).flatMap(session => + deps(session.name).proper_session_theories) val theorem_commands = List("theorem", "lemma", "corollary", "proposition", "schematic_goal") var entry_lines = Map.empty[Entry, Int] var entry_lemmas = Map.empty[Entry, Int] for { entry <- entries node <- nodes(entry) lines = split_lines(File.read(node.path)).map(_.trim) } { entry_lines += entry -> (entry_lines.getOrElse(entry, 0) + lines.count(_.nonEmpty)) entry_lemmas += entry -> (entry_lemmas.getOrElse(entry, 0) + lines.count(line => theorem_commands.exists(line.startsWith))) } val first_year = entries.flatMap(_.releases).map(_.date.getYear).min def years(upto: Int): List[Int] = Range.inclusive(first_year, upto).toList val current_year = Date.now().rep.getYear val all_years = years(current_year) // per Isabelle release year val by_year = entries.groupBy(_.date.getYear) val size_by_year = by_year.view.mapValues(_.length).toMap val loc_by_year = by_year.view.mapValues(_.map(entry_lines).sum).toMap val authors_by_year = by_year.view.mapValues(_.flatMap(_.authors).map(_.author)).toMap val num_lemmas = entries.map(entry_lemmas).sum val num_lines = entries.map(entry_lines).sum // accumulated def total_articles(year: Int): Int = years(year).map(size_by_year.getOrElse(_, 0)).sum def total_loc(year: Int): Int = round(years(year).map(loc_by_year.getOrElse(_, 0)).sum) def total_authors(year: Int): Int = years(year).flatMap(authors_by_year.getOrElse(_, Nil)).distinct.length def fresh_authors(year: Int): Int = total_authors(year) - total_authors(year - 1) val sorted = entries.sortBy(_.date) def map_repetitions(elems: List[String], to: String): List[String] = elems.foldLeft(("", List.empty[String])) { case((last, acc), s) => (s, acc :+ (if (last == s) to else s)) }._2 JSON.Object( "years" -> all_years, "num_lemmas" -> num_lemmas, "num_loc" -> num_lines, "articles_year" -> all_years.map(total_articles), "loc_years" -> all_years.map(total_loc), "author_years" -> all_years.map(fresh_authors), "author_years_cumulative" -> all_years.map(total_authors), "loc_articles" -> sorted.map(entry_lines), "all_articles" -> sorted.map(_.name), "article_years_unique" -> map_repetitions(sorted.map(_.date.getYear.toString), "")) } /* site generation */ def afp_site_gen( layout: Hugo.Layout, status_file: Option[Path], afp_structure: AFP_Structure, clean: Boolean = false, progress: Progress = new Progress() ): Unit = { /* clean old */ if (clean) { progress.echo("Cleaning up generated files...") layout.clean() } /* add topics */ progress.echo("Preparing topics...") val topics = afp_structure.load_topics val root_topics = Metadata.Topics.root_topics(topics) layout.write_data(Path.basic("topics.json"), JSON.from_topics(root_topics)) /* add licenses */ progress.echo("Preparing licenses...") val licenses = afp_structure.load_licenses /* add releases */ progress.echo("Preparing releases...") val releases = afp_structure.load_releases /* prepare authors and entries */ progress.echo("Preparing authors...") val authors = afp_structure.load_authors var seen_affiliations: List[Affiliation] = Nil val entries = afp_structure.entries.flatMap { name => val entry = afp_structure.load_entry(name, authors, topics, licenses, releases) seen_affiliations = seen_affiliations :++ entry.authors ++ entry.contributors Some(entry) } val seen_authors = Utils.group_sorted(seen_affiliations.distinct, (a: Affiliation) => a.author).map { case (id, affiliations) => val seen_emails = affiliations.collect { case e: Email => e } val seen_homepages = affiliations.collect { case h: Homepage => h } authors(id).copy(emails = seen_emails, homepages = seen_homepages) } layout.write_data(Path.basic("authors.json"), JSON.from_authors(seen_authors.toList)) /* extract keywords */ progress.echo("Extracting keywords...") var seen_keywords = Set.empty[String] val entry_keywords = entries.filterNot(_.statistics_ignore).map { entry => val scored_keywords = Rake.extract_keywords(entry.`abstract`) seen_keywords ++= scored_keywords.map(_._1) entry.name -> scored_keywords.map(_._1) }.toMap seen_keywords = seen_keywords.filter(k => !k.endsWith("s") || !seen_keywords.contains(k.stripSuffix("s"))) layout.write_static(Path.make(List("data", "keywords.json")), JSON.from_keywords(seen_keywords.toList)) def get_keywords(name: Metadata.Entry.Name): List[String] = entry_keywords.getOrElse(name, Nil).filter(seen_keywords.contains).take(8) /* add entries and theory listings */ progress.echo("Preparing entries...") val sessions_structure = afp_structure.sessions_structure val sessions_deps = Sessions.deps(sessions_structure) val browser_info = Browser_Info.context(sessions_structure) def theories_of(session_name: String): List[String] = sessions_deps(session_name).proper_session_theories.map(_.theory_base_name) def write_session_json(session_name: String, base: JSON.Object.T): Unit = { val session_json = base ++ JSON.Object( "title" -> session_name, "url" -> ("/sessions/" + session_name.toLowerCase), "theories" -> theories_of(session_name).map(thy_name => JSON.Object( "name" -> thy_name, "path" -> (browser_info.session_dir(session_name) + Path.basic(thy_name).html).implode ))) layout.write_content(Path.make(List("sessions", session_name + ".md")), session_json) } val cache = new Cache(layout, progress) val entry_sessions = entries.map(entry => entry -> afp_structure.entry_sessions(entry.name)).toMap val session_entry = entry_sessions.flatMap((entry, sessions) => sessions.map(session => session.name -> entry)).toMap entries.foreach { entry => val deps = for { session <- entry_sessions(entry) dep_session <- sessions_structure.imports_graph.imm_preds(session.name) if sessions_structure(dep_session).groups.contains("AFP") dep <- session_entry.get(dep_session) if dep != entry } yield dep.name val sessions = afp_structure.entry_sessions(entry.name).map { session => write_session_json(session.name, JSON.Object("entry" -> entry.name)) JSON.Object( "session" -> session.name, "theories" -> theories_of(session.name)) } val entry_json = JSON.from_entry(entry, cache) ++ JSON.Object( "dependencies" -> deps.distinct, "sessions" -> sessions, "url" -> ("/entries/" + entry.name + ".html"), "keywords" -> get_keywords(entry.name)) layout.write_content(Path.make(List("entries", entry.name + ".md")), entry_json) } for { (session_name, (info, _)) <- sessions_structure.imports_graph.iterator if !info.groups.contains("AFP") } write_session_json(session_name, JSON.Object("rss" -> false)) /* add statistics */ progress.echo("Preparing statistics...") val statistics_json = afp_stats(sessions_deps, afp_structure, entries.filterNot(_.statistics_ignore)) layout.write_data(Path.basic("statistics.json"), statistics_json) /* project */ progress.echo("Preparing project files") layout.copy_project() /* status */ status_file match { case Some(status_file) => progress.echo("Preparing devel version...") val status_json = isabelle.JSON.parse(File.read(status_file)) layout.write_data(Path.basic("status.json"), status_json) case None => } progress.echo("Finished sitegen preparation.") } /* build site */ def afp_build_site( out_dir: Path, layout: Hugo.Layout, do_watch: Boolean = false, clean: Boolean = false, progress: Progress = new Progress() ): Unit = { if (clean) { progress.echo("Cleaning output dir...") Hugo.clean(out_dir) } if (do_watch) { Hugo.watch(layout, out_dir, progress) } else { progress.echo("Building site...") Hugo.build(layout, out_dir) progress.echo("Build in " + (out_dir + Path.basic("index.html")).absolute.implode) } } /* tool wrapper */ val isabelle_tool = Isabelle_Tool("afp_site_gen", "generates afp website source", Scala_Project.here, { args => var base_dir = Path.explode("$AFP_BASE") var status_file: Option[Path] = None var hugo_dir = base_dir + Path.make(List("web", "hugo")) var out_dir: Path = base_dir + Path.make(List("web", "out")) var build_only = false var devel_mode = false var fresh = false val getopts = Getopts(""" Usage: isabelle afp_site_gen [OPTIONS] Options are: -B DIR afp base dir (default """" + base_dir.implode + """") -D FILE build status file for devel version -H DIR generated hugo project dir (default """" + hugo_dir.implode + """") -O DIR output dir for build (default """ + out_dir.implode + """) -b build only -d devel mode (overrides hugo dir, builds site in watch mode) -f fresh build: clean up existing hugo and build directories Generates the AFP website source. HTML files of entries are dynamically loaded. Providing a status file will build the development version of the archive. Site will be built from generated source if output dir is specified. """, "B:" -> (arg => base_dir = Path.explode(arg)), "D:" -> (arg => status_file = Some(Path.explode(arg))), "H:" -> (arg => hugo_dir = Path.explode(arg)), "O:" -> (arg => out_dir = Path.explode(arg)), "b" -> (_ => build_only = true), "d" -> (_ => devel_mode = true), "f" -> (_ => fresh = true)) getopts(args) status_file.foreach(path => if (!path.is_file || !path.file.exists()) error("Invalid status file: " + path)) if (devel_mode) hugo_dir = base_dir + Path.make(List("admin", "site")) val afp_structure = AFP_Structure(base_dir) val layout = Hugo.Layout(hugo_dir) val progress = new Console_Progress() if (!build_only) { progress.echo("Preparing site generation in " + hugo_dir.implode) afp_site_gen(layout = layout, status_file = status_file, afp_structure = afp_structure, clean = fresh, progress = progress) } afp_build_site(out_dir = out_dir, layout = layout, do_watch = devel_mode, clean = fresh, progress = progress) }) } \ No newline at end of file diff --git a/tools/hugo.scala b/tools/hugo.scala --- a/tools/hugo.scala +++ b/tools/hugo.scala @@ -1,116 +1,116 @@ /* Author: Fabian Huch, TU Muenchen AFP Hugo wrapper and project layout. */ package afp import isabelle.* object Hugo { val hugo_home = Isabelle_System.getenv("ISABELLE_HUGO") val hugo_static = Path.explode("$AFP_BASE") + Path.make(List("admin", "site")) class Layout private(private[Hugo] val src_dir: Path) { private def write(file: Path, content: String): Unit = { val path = src_dir + file if (!path.dir.file.exists()) path.dir.file.mkdirs() File.write(path, content) } val data_dir = src_dir + Path.basic("data") private def format(json: JSON.T): String = { json match { case elems: List[_] => elems.map(format).mkString("[", ",\n", "]") case JSON.Object(m) => m.map { case (k,v) => format(k) + ": " + format(v) }.mkString("{", ",\n", "}") case _ => isabelle.JSON.Format(json) } } def write_data(file: Path, content: JSON.T): Unit = write(Path.basic("data") + file, format(content)) val content_dir = src_dir + Path.basic("content") def write_content(file: Path, content: JSON.T): Unit = write(Path.basic("content") + file, format(content)) val static_dir = src_dir + Path.basic("static") def write_static(file: Path, content: JSON.T): Unit = write(Path.basic("static") + file, format(content)) private val generated_dirs = List( List("content", "entries"), List("content", "theories"), List("data"), List("resources"), List("static")).map(Path.make) val cache_dir = src_dir + Path.basic("cache") def write_cache(file: Path, content: JSON.T): Unit = write(Path.basic("cache") + file, format(content)) /* Static project files */ private val project_files = List( - List("content", "webapp"), - List("content", "_index.md"), - List("content", "about.md"), - List("content", "submission.md"), - List("content", "download.md"), - List("content", "help.md"), - List("content", "search.md"), - List("content", "statistics.md"), - List("content", "submission.md"), - List("themes"), - List("config.json")).map(Path.make) + List("content", "webapp"), + List("content", "_index.md"), + List("content", "about.md"), + List("content", "submission.md"), + List("content", "download.md"), + List("content", "help.md"), + List("content", "search.md"), + List("content", "statistics.md"), + List("content", "submission.md"), + List("themes"), + List("config.json")).map(Path.make) private val is_static_src = hugo_static.canonical.absolute == src_dir.canonical.absolute def copy_project(): Unit = { if (!is_static_src) project_files.foreach(file => Isabelle_System.copy_dir(hugo_static + file, src_dir + file)) } def clean(): Unit = { generated_dirs.foreach(file => Isabelle_System.rm_tree(src_dir + file)) if (!is_static_src) project_files.foreach(file => Isabelle_System.rm_tree(src_dir + file)) } } object Layout { def apply(src_dir: Path = Path.explode("$AFP_BASE") + Path.make(List("web", "hugo"))): Layout = new Layout(src_dir.canonical) } private lazy val exec = Path.explode(proper_string(hugo_home).getOrElse(error("No hugo component found"))) + Path.basic("hugo") private def source_specifier(layout: Layout, out_dir: Path): String = " -s " + quote(layout.src_dir.implode) + " -d " + quote(out_dir.canonical.implode) private def build_example(layout: Layout, out_dir: Path): Unit = { val env = Isabelle_System.settings(List("HUGO_IGNOREFILES" -> "[]")) Isabelle_System.bash(exec.implode + source_specifier(layout, out_dir: Path), env = env).check } def build(layout: Layout, out_dir: Path): Unit = { build_example(layout, out_dir) Isabelle_System.bash(exec.implode + source_specifier(layout, out_dir)).check } def watch(layout: Layout, out_dir: Path, progress: Progress = new Progress()): Unit = { build_example(layout, out_dir) Isabelle_System.bash( exec.implode + " server " + source_specifier(layout, out_dir), progress_stdout = progress.echo(_), progress_stderr = progress.echo_warning(_)).check } def clean(out_dir: Path): Unit = File.read_dir(out_dir).foreach(file => Isabelle_System.rm_tree(out_dir + Path.basic(file))) } \ No newline at end of file diff --git a/tools/metadata.scala b/tools/metadata.scala --- a/tools/metadata.scala +++ b/tools/metadata.scala @@ -1,460 +1,444 @@ /* Author: Fabian Huch, TU Muenchen AFP metadata model and TOML serialization. */ package afp import isabelle.* import java.time.LocalDate import java.net.URI import scala.collection.immutable.ListMap object Metadata { /* affiliations */ - sealed trait Affiliation { - def author: Author.ID - } + sealed trait Affiliation { def author: Author.ID } case class Unaffiliated(override val author: Author.ID) extends Affiliation case class Email(override val author: Author.ID, id: Email.ID, address: String) extends Affiliation { private val Address = "([^@]+)@(.+)".r val (user, host) = address match { case Address(user, host) => (user, host) case _ => error("Invalid address: " + address) } } object Email { type ID = String def apply(author: Author.ID, id: Email.ID, user: String, host: String): Email = Email(author, id, user + "@" + host) } case class Homepage(override val author: Author.ID, id: Homepage.ID, url: Url) extends Affiliation - object Homepage { - type ID = String - } + object Homepage { type ID = String } /* authors */ case class Orcid(identifier: String) { require( "^([0-9]{4})-([0-9]{4})-([0-9]{4})-([0-9]{3}[0-9X])$".r.matches(identifier), "Invalid format for orcid: " + quote(identifier)) def url: Url = Url("https://orcid.org/" + identifier) } case class Author( id: Author.ID, name: String, emails: List[Email] = Nil, homepages: List[Homepage] = Nil, orcid: Option[Orcid] = None ) - object Author { - type ID = String - } + object Author { type ID = String } type Authors = ListMap[Author.ID, Author] object Authors { def empty: Authors = Authors(Nil) def apply(authors: List[Author]): Authors = ListMap.from(authors.map(author => author.id -> author)) } /* topics */ sealed trait Classification { def desc: String def url: Url } case class ACM(id: String, override val desc: String) extends Classification { val url = Url("https://dl.acm.org/topic/ccs2012/" + id) } case class AMS(id: String, hierarchy: List[String]) extends Classification { val code: String = id.length match { case 2 => id + "-XX" case 3 => id + "xx" case 5 => id case _ => error("Invalid ams id:" + id) } override val desc: String = hierarchy.mkString(" / ") override val url: Url = Url("https://mathscinet.ams.org/mathscinet/msc/msc2020.html?t=" + code) } case class Topic( id: Topic.ID, name: String, classification: List[Classification] = Nil, sub_topics: List[Topic] = Nil ) { def all_topics: List[Topic] = this :: sub_topics.flatMap(_.all_topics) } - object Topic { - type ID = String - } + object Topic { type ID = String } type Topics = ListMap[Topic.ID, Topic] object Topics { def empty: Topics = Topics(Nil) def apply(root_topics: List[Topic]): Topics = ListMap.from(root_topics.flatMap(_.all_topics).map(topic => topic.id -> topic)) def root_topics(topics: Topics): List[Topic] = { val sub_topics = topics.values.flatMap(_.sub_topics).map(_.id).toSet topics.values.filterNot(topic => sub_topics.contains(topic.id)).toList } } /* releases */ type Date = LocalDate - object Isabelle { - type Version = String - } + object Isabelle { type Version = String } case class Release(entry: Entry.Name, date: Date, isabelle: Isabelle.Version) type Releases = ListMap[Entry.Name, List[Release]] object Releases { def empty: Releases = Releases(Nil) def apply(releases: List[Release]): Releases = Utils.group_sorted(releases, (release: Release) => release.entry) } /* license */ case class License(id: License.ID, name: String) - object License { - type ID = String - } + object License { type ID = String } type Licenses = ListMap[License.ID, License] object Licenses { def empty: Licenses = Licenses(Nil) def apply(licenses: List[License]): Licenses = ListMap.from(licenses.map(license => license.id -> license)) } /* references */ sealed trait Reference case class DOI(identifier: String) extends Reference { require("^10.([1-9][0-9]{3,})/(.+)".r.matches(identifier), "invalid format for DOI: " + quote(identifier)) def uri: URI = new URI("doi:" + identifier) def url: Url = Url("https://doi.org/" + identifier) def formatted(style: String = "apa"): String = Utils.fetch_text(url, Map("Accept" -> ("text/x-bibliography; style=" + style))) } case class Formatted(rep: String) extends Reference /* misc */ type Change_History = Map[Date, String] type Extra = Map[String, String] /* entry */ case class Entry( name: Entry.Name, title: String, authors: List[Affiliation], date: Date, topics: List[Topic], `abstract`: String, notifies: List[Email], license: License, note: String, contributors: List[Affiliation] = Nil, change_history: Change_History = Map.empty, extra: Extra = Map.empty, releases: List[Release] = Nil, statistics_ignore: Boolean = false, related: List[Reference] = Nil) - object Entry { - type Name = String - } + object Entry { type Name = String } type Entries = ListMap[Entry.Name, Entry] object Entries { def empty: Entries = Entries(Nil) def apply(entries: List[Entry]) = ListMap.from(entries.map(entry => entry.name -> entry)) } /* toml */ private def by_id[A](elems: Map[String, A], id: String): A = elems.getOrElse(id, error("Elem " + quote(id) + " not found in " + commas_quote(elems.keys))) object TOML { import isabelle.TOML.{Array, Boolean, Key, Local_Date, String, Table} /* affils */ def from_email(email: Email): Table = Table( "user" -> Array(email.user.split('.').map(String(_))), "host" -> Array(email.host.split('.').map(String(_)))) def to_email(author_id: Author.ID, email_id: Email.ID, email: Table): Email = { val user = email.array("user").string.values.map(_.rep) val host = email.array("host").string.values.map(_.rep) Email(author_id, email_id, user.mkString("."), host.mkString(".")) } /* author */ def from_author(author: Author): Table = Table( "name" -> String(author.name), "emails" -> Table(author.emails.map(e => e.id -> from_email(e))), "homepages" -> Table(author.homepages.map(h => h.id -> String(h.url.toString)))) ++ author.orcid.map(orcid => Table("orcid" -> String(orcid.identifier))).getOrElse(Table()) def to_author(author_id: Author.ID, author: Table): Author = { val emails = author.table("emails").table.values.map { case (id, email) => to_email(author_id, id, email) } val homepages = author.table("homepages").string.values.map { case (id, url) => Homepage(author = author_id, id = id, url = Url(url.rep)) } val orcid = author.string.get("orcid").map(_.rep).map(Orcid(_)) Author( id = author_id, name = author.string("name").rep, orcid = orcid, emails = emails, homepages = homepages) } def from_authors(authors: List[Author]): Table = Table(authors.map(author => author.id -> from_author(author))) def to_authors(authors: Table): List[Author] = authors.table.values.map(to_author) /* topics */ - def from_acm(acm: ACM): Table = - Table("id" -> String(acm.id), "desc" -> String(acm.desc)) + def from_acm(acm: ACM): Table = Table("id" -> String(acm.id), "desc" -> String(acm.desc)) - def to_acm(acm: Table): ACM = - ACM(acm.string("id").rep, acm.string("desc").rep) + def to_acm(acm: Table): ACM = ACM(acm.string("id").rep, acm.string("desc").rep) def from_ams(ams: AMS): Table = Table("id" -> String(ams.id), "hierarchy" -> Array(ams.hierarchy.map(String(_)))) def to_ams(ams: Table): AMS = AMS(ams.string("id").rep, ams.array("hierarchy").string.values.map(_.rep)) def from_classifications(classifications: List[Classification]): Table = Table(classifications.map { case acm: ACM => "acm" -> from_acm(acm) case ams: AMS => "ams" -> from_ams(ams) }) def to_classifications(classifications: Table): List[Classification] = classifications.table.values.map { case ("ams", ams) => to_ams(ams) case ("acm", acm) => to_acm(acm) case (c, _) => error("Unknown topic classification: " + quote(c)) } def from_topics(root_topics: List[Topic]): Table = Table(root_topics.map(t => t.name -> ( Table("classification" -> from_classifications(t.classification)) ++ from_topics(t.sub_topics)))) def to_topics(root_topics: Table): List[Topic] = { def to_topics_rec(topics: List[(Key, Table)], root: Topic.ID): List[Topic] = { topics.map { case (name, data) => val id = (if (root.nonEmpty) root + "/" else "") + name val classifications = to_classifications(data.table("classification")) val sub_topics = data.table.values.filterNot(_._1 == "classification") Topic(id, name, classifications, to_topics_rec(sub_topics, id)) } } to_topics_rec(root_topics.table.values, "") } /* releases */ def from_releases(releases: List[Release]): Table = Table(Utils.group_sorted(releases, (r: Release) => r.entry).view.mapValues { entry_releases => Table(entry_releases.map(r => r.date.toString -> String(r.isabelle))) }.toList) def to_releases(map: Table): List[Release] = map.table.values.flatMap { case (entry, releases) => releases.string.values.map { case (date, version) => Release(entry = entry, date = LocalDate.parse(date), isabelle = version.rep) } } /* affiliation */ def from_affiliations(affiliations: List[Affiliation]): Table = Table(Utils.group_sorted(affiliations, (a: Affiliation) => a.author).view.mapValues(vs => Table(vs.collect { case Email(_, id, _) => "email" -> String(id) case Homepage(_, id, _) => "homepage" -> String(id) })).toList) def to_affiliations(affiliations: Table, authors: Authors): List[Affiliation] = { def to_affiliation(affiliation: (Key, String), author: Author): Affiliation = { affiliation match { case ("email", id) => author.emails.find(_.id == id.rep) getOrElse error("Email not found: " + quote(id.rep)) case ("homepage", id) => author.homepages.find(_.id == id.rep) getOrElse error("Homepage not found: " + quote(id.rep)) case e => error("Unknown affiliation type: " + e) } } affiliations.table.values.flatMap { case (id, author_affiliations) => val author = by_id(authors, id) if (author_affiliations.is_empty) List(Unaffiliated(author.id)) else author_affiliations.string.values.map(to_affiliation(_, author)) } } def from_emails(emails: List[Email]): Table = Table(emails.map(email => email.author -> String(email.id))) def to_emails(emails: Table, authors: Authors): List[Email] = emails.string.values.map { case (author, id) => by_id(authors, author).emails.find(_.id == id.rep) getOrElse error("Email not found: " + quote(id.rep)) } /* license */ def from_licenses(licenses: List[License]): Table = Table(licenses.map(license => license.id -> Table("name" -> String(license.name)))) def to_licenses(licenses: Table): List[License] = { licenses.table.values.map { case (id, license) => License(id, license.string("name").rep) } } def to_license(license: String, licenses: Licenses): License = licenses.getOrElse(license.rep, error("No such license: " + quote(license.rep))) /* history */ def from_change_history(change_history: Change_History): Table = Table(change_history.map { case (date, str) => date.toString -> String(str) }) def to_change_history(change_history: Table): Change_History = change_history.string.values.map { case (date, entry) => LocalDate.parse(date) -> entry.rep }.toMap /* references */ def from_related(references: List[Reference]): Table = { val dois = references.collect { case d: DOI => d } val formatted = references.collect { case f: Formatted => f } Table( "dois" -> Array(dois.map(_.identifier).map(String(_))), "pubs" -> Array(formatted.map(_.rep).map(String(_)))) } def to_related(references: Table): List[Reference] = { val dois = references.array.get("dois").toList.flatMap(_.string.values.map(_.rep)) val pubs = references.array.get("pubs").toList.flatMap(_.string.values.map(_.rep)) dois.map(DOI(_)) ++ pubs.map(Formatted(_)) } /* entry */ def from_entry(entry: Entry): Table = { Table( "title" -> String(entry.title), "authors" -> from_affiliations(entry.authors), "contributors" -> from_affiliations(entry.contributors), "date" -> Local_Date(entry.date), "topics" -> Array(entry.topics.map(_.id).map(String(_))), "abstract" -> String(entry.`abstract`), "notify" -> from_emails(entry.notifies), "license" -> String(entry.license.id), "note" -> String(entry.note), "history" -> from_change_history(entry.change_history), "extra" -> Table(entry.extra.view.mapValues(String(_)).toList), "related" -> from_related(entry.related)) ++ (if (entry.statistics_ignore) Table("statistics_ignore" -> Boolean(true)) else Table()) } def to_entry( name: Entry.Name, entry: Table, authors: Authors, topics: Topics, licenses: Licenses, releases: List[Release] ): Entry = Entry( name = name, title = entry.string("title").rep, authors = to_affiliations(entry.table("authors"), authors), date = entry.local_date("date").rep, topics = entry.array("topics").string.values.map(_.rep).map(by_id(topics, _)), `abstract` = entry.string("abstract").rep, notifies = to_emails(entry.table("notify"), authors), license = to_license(entry.string("license"), licenses), note = entry.string("note").rep, contributors = to_affiliations(entry.table("contributors"), authors), change_history = to_change_history(entry.table("history")), extra = entry.table("extra").string.values.map((k, v) => (k, v.rep)).toMap, releases = releases, statistics_ignore = entry.boolean.get("statistics_ignore").map(_.rep).getOrElse(false), related = to_related(entry.table("related"))) } } diff --git a/tools/utils.scala b/tools/utils.scala --- a/tools/utils.scala +++ b/tools/utils.scala @@ -1,58 +1,58 @@ /* Author: Fabian Huch, TU Muenchen Utilities. */ package afp import isabelle.* import java.io.IOException import scala.collection.immutable.ListMap object Utils { - val TIMEOUT = 30*1000 + val TIMEOUT = 30 * 1000 def group_sorted[A, K](l: List[A], f: A => K): ListMap[K, List[A]] = l.foldLeft(ListMap.empty[K, List[A]]) { case (m, a) => m.updatedWith(f(a)) { case Some(as) => Some(as :+ a) case None => Some(List(a)) } } def grouped_sorted[A, K](l: List[A], f: A => K): ListMap[K, A] = group_sorted(l, f).map { case (k, v :: Nil) => k -> v case (k, vs) => error("Not distinct for " + quote(k.toString) + ": " + commas_quote(vs.map(_.toString))) } def the_entry[K, V](m: Map[K, V], k: K): V = m.getOrElse(k, error("Expected key " + quote(k.toString))) def fetch_text(url: Url, params: Map[String, String]): String = try { val conn = url.open_connection() conn.setConnectTimeout(TIMEOUT) conn.setReadTimeout(TIMEOUT) params.foreach { case (param, value) => conn.setRequestProperty(param, value) } File.read_stream(conn.getInputStream) } catch { case _: IOException => error("Could not read from " + quote(url.toString)) } def remove_at[A](i: Int, l: List[A]): List[A] = l.take(i) ++ l.drop(i + 1) def make_unique(prefix: String, elems: Set[String]): String = { if (!elems.contains(prefix)) prefix else { var num = 1 while (elems.contains(prefix + num)) { num += 1 } prefix + num } } def is_distinct[A](it: List[A]): Boolean = it.size == it.distinct.size } \ No newline at end of file