src/Pure/Thy/thy_header.scala
author wenzelm
Mon Jan 09 20:26:59 2017 +0100 (2017-01-09)
changeset 64854 f5aa712e6250
parent 64825 e78b62c289bb
child 65362 908a27a4b9c9
permissions -rw-r--r--
tuned signature;
     1 /*  Title:      Pure/Thy/thy_header.scala
     2     Author:     Makarius
     3 
     4 Static theory header information.
     5 */
     6 
     7 package isabelle
     8 
     9 
    10 import scala.annotation.tailrec
    11 import scala.collection.mutable
    12 import scala.util.parsing.input.Reader
    13 import scala.util.matching.Regex
    14 
    15 
    16 object Thy_Header extends Parse.Parser
    17 {
    18   /* bootstrap keywords */
    19 
    20   type Keywords = List[(String, Keyword.Spec)]
    21   type Abbrevs = List[(String, String)]
    22 
    23   val CHAPTER = "chapter"
    24   val SECTION = "section"
    25   val SUBSECTION = "subsection"
    26   val SUBSUBSECTION = "subsubsection"
    27   val PARAGRAPH = "paragraph"
    28   val SUBPARAGRAPH = "subparagraph"
    29   val TEXT = "text"
    30   val TXT = "txt"
    31   val TEXT_RAW = "text_raw"
    32 
    33   val THEORY = "theory"
    34   val IMPORTS = "imports"
    35   val KEYWORDS = "keywords"
    36   val ABBREVS = "abbrevs"
    37   val AND = "and"
    38   val BEGIN = "begin"
    39 
    40   val bootstrap_header: Keywords =
    41     List(
    42       ("%", Keyword.no_spec),
    43       ("(", Keyword.no_spec),
    44       (")", Keyword.no_spec),
    45       (",", Keyword.no_spec),
    46       ("::", Keyword.no_spec),
    47       ("=", Keyword.no_spec),
    48       (AND, Keyword.no_spec),
    49       (BEGIN, Keyword.quasi_command_spec),
    50       (IMPORTS, Keyword.quasi_command_spec),
    51       (KEYWORDS, Keyword.quasi_command_spec),
    52       (ABBREVS, Keyword.quasi_command_spec),
    53       (CHAPTER, (((Keyword.DOCUMENT_HEADING, Nil), Nil))),
    54       (SECTION, (((Keyword.DOCUMENT_HEADING, Nil), Nil))),
    55       (SUBSECTION, (((Keyword.DOCUMENT_HEADING, Nil), Nil))),
    56       (SUBSUBSECTION, (((Keyword.DOCUMENT_HEADING, Nil), Nil))),
    57       (PARAGRAPH, (((Keyword.DOCUMENT_HEADING, Nil), Nil))),
    58       (SUBPARAGRAPH, (((Keyword.DOCUMENT_HEADING, Nil), Nil))),
    59       (TEXT, (((Keyword.DOCUMENT_BODY, Nil), Nil))),
    60       (TXT, (((Keyword.DOCUMENT_BODY, Nil), Nil))),
    61       (TEXT_RAW, (((Keyword.DOCUMENT_RAW, Nil), Nil))),
    62       (THEORY, ((Keyword.THY_BEGIN, Nil), List("theory"))),
    63       ("ML", ((Keyword.THY_DECL, Nil), List("ML"))))
    64 
    65   private val bootstrap_keywords =
    66     Keyword.Keywords.empty.add_keywords(bootstrap_header)
    67 
    68   lazy val bootstrap_syntax: Outer_Syntax =
    69     Outer_Syntax.init().add_keywords(bootstrap_header)
    70 
    71 
    72   /* file name vs. theory name */
    73 
    74   val PURE = "Pure"
    75   val ML_BOOTSTRAP = "ML_Bootstrap"
    76   val ML_ROOT = "ML_Root"
    77   val ml_roots = List("ROOT0.ML" -> "ML_Root0", "ROOT.ML" -> ML_ROOT)
    78   val bootstrap_thys = List(PURE, ML_BOOTSTRAP).map(a => a -> ("Bootstrap_" + a))
    79 
    80   private val Base_Name = new Regex(""".*?([^/\\:]+)""")
    81   private val Thy_Name = new Regex(""".*?([^/\\:]+)\.thy""")
    82 
    83   def base_name(s: String): String =
    84     s match { case Base_Name(name) => name case _ => error("Malformed import: " + quote(s)) }
    85 
    86   def thy_name(s: String): Option[String] =
    87     s match { case Thy_Name(name) => Some(name) case _ => None }
    88 
    89   def thy_name_bootstrap(s: String): Option[String] =
    90     s match {
    91       case Thy_Name(name) =>
    92         Some(bootstrap_thys.collectFirst({ case (a, b) if a == name => b }).getOrElse(name))
    93       case Base_Name(name) => ml_roots.collectFirst({ case (a, b) if a == name => b })
    94       case _ => None
    95     }
    96 
    97   def is_ml_root(theory: String): Boolean =
    98     ml_roots.exists({ case (_, b) => b == theory })
    99 
   100   def is_bootstrap(theory: String): Boolean =
   101     bootstrap_thys.exists({ case (_, b) => b == theory })
   102 
   103 
   104   /* header */
   105 
   106   val header: Parser[Thy_Header] =
   107   {
   108     val opt_files =
   109       $$$("(") ~! (rep1sep(name, $$$(",")) <~ $$$(")")) ^^ { case _ ~ x => x } |
   110       success(Nil)
   111 
   112     val keyword_spec =
   113       atom("outer syntax keyword specification", _.is_name) ~ opt_files ~ tags ^^
   114       { case x ~ y ~ z => ((x, y), z) }
   115 
   116     val keyword_decl =
   117       rep1(string) ~
   118       opt($$$("::") ~! keyword_spec ^^ { case _ ~ x => x }) ^^
   119       { case xs ~ y => xs.map((_, y.getOrElse(Keyword.no_spec))) }
   120 
   121     val keyword_decls =
   122       keyword_decl ~ rep($$$(AND) ~! keyword_decl ^^ { case _ ~ x => x }) ^^
   123       { case xs ~ yss => (xs :: yss).flatten }
   124 
   125     val abbrevs =
   126       rep1(text ~ ($$$("=") ~! text) ^^ { case a ~ (_ ~ b) => (a, b) })
   127 
   128     val args =
   129       position(theory_name) ~
   130       (opt($$$(IMPORTS) ~! rep1(position(theory_name))) ^^
   131         { case None => Nil case Some(_ ~ xs) => xs }) ~
   132       (opt($$$(KEYWORDS) ~! keyword_decls) ^^
   133         { case None => Nil case Some(_ ~ xs) => xs }) ~
   134       (opt($$$(ABBREVS) ~! abbrevs) ^^
   135         { case None => Nil case Some(_ ~ xs) => xs }) ~
   136       $$$(BEGIN) ^^
   137       { case x ~ ys ~ zs ~ ws ~ _ => Thy_Header(x, ys, zs, ws) }
   138 
   139     val heading =
   140       (command(CHAPTER) |
   141         command(SECTION) |
   142         command(SUBSECTION) |
   143         command(SUBSUBSECTION) |
   144         command(PARAGRAPH) |
   145         command(SUBPARAGRAPH) |
   146         command(TEXT) |
   147         command(TXT) |
   148         command(TEXT_RAW)) ~
   149       tags ~! document_source
   150 
   151     (rep(heading) ~ command(THEORY) ~ tags) ~! args ^^ { case _ ~ x => x }
   152   }
   153 
   154 
   155   /* read -- lazy scanning */
   156 
   157   def read(reader: Reader[Char], start: Token.Pos, strict: Boolean = true): Thy_Header =
   158   {
   159     val token = Token.Parsers.token(bootstrap_keywords)
   160     def make_tokens(in: Reader[Char]): Stream[Token] =
   161       token(in) match {
   162         case Token.Parsers.Success(tok, rest) => tok #:: make_tokens(rest)
   163         case _ => Stream.empty
   164       }
   165 
   166     val tokens =
   167       if (strict) make_tokens(reader)
   168       else make_tokens(reader).dropWhile(tok => !tok.is_command(Thy_Header.THEORY))
   169 
   170     val tokens1 = tokens.takeWhile(tok => !tok.is_begin).toList
   171     val tokens2 = tokens.dropWhile(tok => !tok.is_begin).headOption.toList
   172 
   173     parse(commit(header), Token.reader(tokens1 ::: tokens2, start)) match {
   174       case Success(result, _) => result
   175       case bad => error(bad.toString)
   176     }
   177   }
   178 }
   179 
   180 
   181 sealed case class Thy_Header(
   182   name: (String, Position.T),
   183   imports: List[(String, Position.T)],
   184   keywords: Thy_Header.Keywords,
   185   abbrevs: Thy_Header.Abbrevs)
   186 {
   187   def decode_symbols: Thy_Header =
   188   {
   189     val f = Symbol.decode _
   190     Thy_Header((f(name._1), name._2),
   191       imports.map({ case (a, b) => (f(a), b) }),
   192       keywords.map({ case (a, ((b, c), d)) => (f(a), ((f(b), c.map(f)), d.map(f))) }),
   193       abbrevs.map({ case (a, b) => (f(a), f(b)) }))
   194   }
   195 }