src/Pure/Thy/thy_header.scala

special theories are always global;

/*  Title:      Pure/Thy/thy_header.scala
    Author:     Makarius

Static theory header information.
*/

package isabelle


import scala.annotation.tailrec
import scala.collection.mutable
import scala.util.parsing.input.Reader
import scala.util.matching.Regex


object Thy_Header extends Parse.Parser
{
  /* bootstrap keywords */

  type Keywords = List[(String, Keyword.Spec)]
  type Abbrevs = List[(String, String)]

  val CHAPTER = "chapter"
  val SECTION = "section"
  val SUBSECTION = "subsection"
  val SUBSUBSECTION = "subsubsection"
  val PARAGRAPH = "paragraph"
  val SUBPARAGRAPH = "subparagraph"
  val TEXT = "text"
  val TXT = "txt"
  val TEXT_RAW = "text_raw"

  val THEORY = "theory"
  val IMPORTS = "imports"
  val KEYWORDS = "keywords"
  val ABBREVS = "abbrevs"
  val AND = "and"
  val BEGIN = "begin"

  val bootstrap_header: Keywords =
    List(
      ("%", Keyword.Spec.none),
      ("(", Keyword.Spec.none),
      (")", Keyword.Spec.none),
      (",", Keyword.Spec.none),
      ("::", Keyword.Spec.none),
      ("=", Keyword.Spec.none),
      (AND, Keyword.Spec.none),
      (BEGIN, Keyword.Spec(Keyword.QUASI_COMMAND)),
      (IMPORTS, Keyword.Spec(Keyword.QUASI_COMMAND)),
      (KEYWORDS, Keyword.Spec(Keyword.QUASI_COMMAND)),
      (ABBREVS, Keyword.Spec(Keyword.QUASI_COMMAND)),
      (CHAPTER, Keyword.Spec(Keyword.DOCUMENT_HEADING)),
      (SECTION, Keyword.Spec(Keyword.DOCUMENT_HEADING)),
      (SUBSECTION, Keyword.Spec(Keyword.DOCUMENT_HEADING)),
      (SUBSUBSECTION, Keyword.Spec(Keyword.DOCUMENT_HEADING)),
      (PARAGRAPH, Keyword.Spec(Keyword.DOCUMENT_HEADING)),
      (SUBPARAGRAPH, Keyword.Spec(Keyword.DOCUMENT_HEADING)),
      (TEXT, Keyword.Spec(Keyword.DOCUMENT_BODY)),
      (TXT, Keyword.Spec(Keyword.DOCUMENT_BODY)),
      (TEXT_RAW, Keyword.Spec(Keyword.DOCUMENT_RAW)),
      (THEORY, Keyword.Spec(Keyword.THY_BEGIN, tags = List("theory"))),
      ("ML", Keyword.Spec(Keyword.THY_DECL, tags = List("ML"))))

  private val bootstrap_keywords =
    Keyword.Keywords.empty.add_keywords(bootstrap_header)

  lazy val bootstrap_syntax: Outer_Syntax =
    Outer_Syntax.init().add_keywords(bootstrap_header)


  /* file name vs. theory name */

  val PURE = "Pure"
  val ML_BOOTSTRAP = "ML_Bootstrap"
  val ml_roots = List("ROOT0.ML" -> "ML_Root0", "ROOT.ML" -> "ML_Root")
  val bootstrap_thys = List(PURE, ML_BOOTSTRAP).map(a => a -> ("Bootstrap_" + a))

  val bootstrap_global_theories = (ml_roots ::: bootstrap_thys).map(p => (p._2 -> PURE))

  private val Thy_File_Name = new Regex(""".*?([^/\\:]+)\.thy""")
  private val Import_Name = new Regex(""".*?([^/\\:]+)""")

  def import_name(s: String): String =
    s match { case Import_Name(name) => name case _ => error("Malformed import: " + quote(s)) }

  def theory_name(s: String): String =
    s match {
      case Thy_File_Name(name) =>
        bootstrap_thys.collectFirst({ case (a, b) if a == name => b }).getOrElse(name)
      case Import_Name(name) =>
        ml_roots.collectFirst({ case (a, b) if a == name => b }).getOrElse("")
      case _ => ""
    }

  def is_ml_root(theory: String): Boolean =
    ml_roots.exists({ case (_, b) => b == theory })

  def is_bootstrap(theory: String): Boolean =
    bootstrap_thys.exists({ case (_, b) => b == theory })


  /* header */

  val header: Parser[Thy_Header] =
  {
    val opt_files =
      $$$("(") ~! (rep1sep(name, $$$(",")) <~ $$$(")")) ^^ { case _ ~ x => x } |
      success(Nil)

    val keyword_spec =
      atom("outer syntax keyword specification", _.is_name) ~ opt_files ~ tags ^^
      { case x ~ y ~ z => Keyword.Spec(x, y, z) }

    val keyword_decl =
      rep1(string) ~
      opt($$$("::") ~! keyword_spec ^^ { case _ ~ x => x }) ^^
      { case xs ~ y => xs.map((_, y.getOrElse(Keyword.Spec.none))) }

    val keyword_decls =
      keyword_decl ~ rep($$$(AND) ~! keyword_decl ^^ { case _ ~ x => x }) ^^
      { case xs ~ yss => (xs :: yss).flatten }

    val abbrevs =
      rep1(text ~ ($$$("=") ~! text) ^^ { case a ~ (_ ~ b) => (a, b) })

    val args =
      position(theory_name) ~
      (opt($$$(IMPORTS) ~! rep1(position(theory_name))) ^^
        { case None => Nil case Some(_ ~ xs) => xs }) ~
      (opt($$$(KEYWORDS) ~! keyword_decls) ^^
        { case None => Nil case Some(_ ~ xs) => xs }) ~
      (opt($$$(ABBREVS) ~! abbrevs) ^^
        { case None => Nil case Some(_ ~ xs) => xs }) ~
      $$$(BEGIN) ^^
      { case x ~ ys ~ zs ~ ws ~ _ => Thy_Header(x, ys, zs, ws) }

    val heading =
      (command(CHAPTER) |
        command(SECTION) |
        command(SUBSECTION) |
        command(SUBSUBSECTION) |
        command(PARAGRAPH) |
        command(SUBPARAGRAPH) |
        command(TEXT) |
        command(TXT) |
        command(TEXT_RAW)) ~
      tags ~! document_source

    (rep(heading) ~ command(THEORY) ~ tags) ~! args ^^ { case _ ~ x => x }
  }


  /* read -- lazy scanning */

  def read(reader: Reader[Char], start: Token.Pos, strict: Boolean = true): Thy_Header =
  {
    val token = Token.Parsers.token(bootstrap_keywords)
    def make_tokens(in: Reader[Char]): Stream[Token] =
      token(in) match {
        case Token.Parsers.Success(tok, rest) => tok #:: make_tokens(rest)
        case _ => Stream.empty
      }

    val tokens =
      if (strict) make_tokens(reader)
      else make_tokens(reader).dropWhile(tok => !tok.is_command(Thy_Header.THEORY))

    val tokens1 = tokens.takeWhile(tok => !tok.is_begin).toList
    val tokens2 = tokens.dropWhile(tok => !tok.is_begin).headOption.toList

    parse(commit(header), Token.reader(tokens1 ::: tokens2, start)) match {
      case Success(result, _) => result
      case bad => error(bad.toString)
    }
  }
}


sealed case class Thy_Header(
  name: (String, Position.T),
  imports: List[(String, Position.T)],
  keywords: Thy_Header.Keywords,
  abbrevs: Thy_Header.Abbrevs)
{
  def decode_symbols: Thy_Header =
  {
    val f = Symbol.decode _
    Thy_Header((f(name._1), name._2),
      imports.map({ case (a, b) => (f(a), b) }),
      keywords.map({ case (a, Keyword.Spec(b, c, d)) =>
        (f(a), Keyword.Spec(f(b), c.map(f), d.map(f))) }),
      abbrevs.map({ case (a, b) => (f(a), f(b)) }))
  }
}