src/Pure/Thy/thy_header.scala
author wenzelm
Sat Dec 16 14:40:21 2017 +0100 (18 months ago)
changeset 67212 f5d44a01030c
parent 67164 39f57f0757f1
child 67215 03d0c958d65a
permissions -rw-r--r--
tuned;
     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.Spec.none),
    43       ("(", Keyword.Spec.none),
    44       (")", Keyword.Spec.none),
    45       (",", Keyword.Spec.none),
    46       ("::", Keyword.Spec.none),
    47       ("=", Keyword.Spec.none),
    48       (AND, Keyword.Spec.none),
    49       (BEGIN, Keyword.Spec(Keyword.QUASI_COMMAND)),
    50       (IMPORTS, Keyword.Spec(Keyword.QUASI_COMMAND)),
    51       (KEYWORDS, Keyword.Spec(Keyword.QUASI_COMMAND)),
    52       (ABBREVS, Keyword.Spec(Keyword.QUASI_COMMAND)),
    53       (CHAPTER, Keyword.Spec(Keyword.DOCUMENT_HEADING)),
    54       (SECTION, Keyword.Spec(Keyword.DOCUMENT_HEADING)),
    55       (SUBSECTION, Keyword.Spec(Keyword.DOCUMENT_HEADING)),
    56       (SUBSUBSECTION, Keyword.Spec(Keyword.DOCUMENT_HEADING)),
    57       (PARAGRAPH, Keyword.Spec(Keyword.DOCUMENT_HEADING)),
    58       (SUBPARAGRAPH, Keyword.Spec(Keyword.DOCUMENT_HEADING)),
    59       (TEXT, Keyword.Spec(Keyword.DOCUMENT_BODY)),
    60       (TXT, Keyword.Spec(Keyword.DOCUMENT_BODY)),
    61       (TEXT_RAW, Keyword.Spec(Keyword.DOCUMENT_RAW)),
    62       (THEORY, Keyword.Spec(Keyword.THY_BEGIN, tags = List("theory"))),
    63       ("ML", Keyword.Spec(Keyword.THY_DECL, tags = List("ML"))))
    64 
    65   private val bootstrap_keywords =
    66     Keyword.Keywords.empty.add_keywords(bootstrap_header)
    67 
    68   val bootstrap_syntax: Outer_Syntax =
    69     Outer_Syntax.empty.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_roots = List("ROOT0.ML" -> "ML_Root0", "ROOT.ML" -> "ML_Root")
    77   val bootstrap_thys = List(PURE, ML_BOOTSTRAP).map(a => a -> ("Bootstrap_" + a))
    78 
    79   val bootstrap_global_theories = (ml_roots ::: bootstrap_thys).map(p => (p._2 -> PURE))
    80 
    81   private val Thy_File_Name = new Regex(""".*?([^/\\:]+)\.thy""")
    82   private val File_Name = new Regex(""".*?([^/\\:]+)""")
    83 
    84   def is_base_name(s: String): Boolean =
    85     s != "" && !s.exists("/\\:".contains(_))
    86 
    87   def import_name(s: String): String =
    88     s match {
    89       case File_Name(name) if !name.endsWith(".thy") => name
    90       case _ => error("Malformed theory import: " + quote(s))
    91     }
    92 
    93   def theory_name(s: String): String =
    94     s match {
    95       case Thy_File_Name(name) => bootstrap_name(name)
    96       case File_Name(name) =>
    97         ml_roots.collectFirst({ case (a, b) if a == name => b }).getOrElse("")
    98       case _ => ""
    99     }
   100 
   101   def is_ml_root(theory: String): Boolean =
   102     ml_roots.exists({ case (_, b) => b == theory })
   103 
   104   def is_bootstrap(theory: String): Boolean =
   105     bootstrap_thys.exists({ case (_, b) => b == theory })
   106 
   107   def bootstrap_name(theory: String): String =
   108     bootstrap_thys.collectFirst({ case (a, b) if a == theory => b }).getOrElse(theory)
   109 
   110 
   111   /* header */
   112 
   113   val header: Parser[Thy_Header] =
   114   {
   115     val opt_files =
   116       $$$("(") ~! (rep1sep(name, $$$(",")) <~ $$$(")")) ^^ { case _ ~ x => x } |
   117       success(Nil)
   118 
   119     val keyword_spec =
   120       atom("outer syntax keyword specification", _.is_name) ~ opt_files ~ tags ^^
   121       { case x ~ y ~ z => Keyword.Spec(x, y, z) }
   122 
   123     val keyword_decl =
   124       rep1(string) ~
   125       opt($$$("::") ~! keyword_spec ^^ { case _ ~ x => x }) ^^
   126       { case xs ~ y => xs.map((_, y.getOrElse(Keyword.Spec.none))) }
   127 
   128     val keyword_decls =
   129       keyword_decl ~ rep($$$(AND) ~! keyword_decl ^^ { case _ ~ x => x }) ^^
   130       { case xs ~ yss => (xs :: yss).flatten }
   131 
   132     val abbrevs =
   133       rep1sep(text ~ ($$$("=") ~! text) ^^ { case a ~ (_ ~ b) => (a, b) }, $$$("and"))
   134 
   135     val args =
   136       position(theory_name) ~
   137       (opt($$$(IMPORTS) ~! rep1(position(theory_name))) ^^
   138         { case None => Nil case Some(_ ~ xs) => xs }) ~
   139       (opt($$$(KEYWORDS) ~! keyword_decls) ^^
   140         { case None => Nil case Some(_ ~ xs) => xs }) ~
   141       (opt($$$(ABBREVS) ~! abbrevs) ^^
   142         { case None => Nil case Some(_ ~ xs) => xs }) ~
   143       $$$(BEGIN) ^^
   144       { case (name, pos) ~ imports ~ keywords ~ abbrevs ~ _ =>
   145           val f = Symbol.decode _
   146           Thy_Header((f(name), pos),
   147             imports.map({ case (a, b) => (f(a), b) }),
   148             keywords.map({ case (a, Keyword.Spec(b, c, d)) =>
   149               (f(a), Keyword.Spec(f(b), c.map(f), d.map(f))) }),
   150             abbrevs.map({ case (a, b) => (f(a), f(b)) }))
   151       }
   152 
   153     val heading =
   154       (command(CHAPTER) |
   155         command(SECTION) |
   156         command(SUBSECTION) |
   157         command(SUBSUBSECTION) |
   158         command(PARAGRAPH) |
   159         command(SUBPARAGRAPH) |
   160         command(TEXT) |
   161         command(TXT) |
   162         command(TEXT_RAW)) ~
   163       tags ~! document_source
   164 
   165     (rep(heading) ~ command(THEORY) ~ tags) ~! args ^^ { case _ ~ x => x }
   166   }
   167 
   168 
   169   /* read -- lazy scanning */
   170 
   171   private def read_tokens(reader: Reader[Char], strict: Boolean): (List[Token], List[Token]) =
   172   {
   173     val token = Token.Parsers.token(bootstrap_keywords)
   174     def make_tokens(in: Reader[Char]): Stream[Token] =
   175       token(in) match {
   176         case Token.Parsers.Success(tok, rest) => tok #:: make_tokens(rest)
   177         case _ => Stream.empty
   178       }
   179 
   180     val all_tokens = make_tokens(reader)
   181     val drop_tokens =
   182       if (strict) Nil
   183       else all_tokens.takeWhile(tok => !tok.is_command(Thy_Header.THEORY)).toList
   184 
   185     val tokens = all_tokens.drop(drop_tokens.length)
   186     val tokens1 = tokens.takeWhile(tok => !tok.is_begin).toList
   187     val tokens2 = tokens.dropWhile(tok => !tok.is_begin).headOption.toList
   188 
   189     (drop_tokens, tokens1 ::: tokens2)
   190   }
   191 
   192   def read(reader: Reader[Char], start: Token.Pos, strict: Boolean = true): Thy_Header =
   193   {
   194     val (_, tokens0) = read_tokens(reader, true)
   195     val text = Scan.reader_decode_utf8(reader, Token.implode(tokens0))
   196 
   197     val (drop_tokens, tokens) = read_tokens(Scan.char_reader(text), strict)
   198     val pos = (start /: drop_tokens)(_.advance(_))
   199 
   200     parse(commit(header), Token.reader(tokens, pos)) match {
   201       case Success(result, _) => result
   202       case bad => error(bad.toString)
   203     }
   204   }
   205 }
   206 
   207 sealed case class Thy_Header(
   208   name: (String, Position.T),
   209   imports: List[(String, Position.T)],
   210   keywords: Thy_Header.Keywords,
   211   abbrevs: Thy_Header.Abbrevs)