src/Pure/Thy/thy_header.scala
author wenzelm
Sun Jul 10 11:18:35 2016 +0200 (2016-07-10)
changeset 63429 baedd4724f08
parent 63022 785a59235a15
child 63448 998acd66fbd7
permissions -rw-r--r--
tuned signature: more uniform Keyword.spec;
     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, CharSequenceReader}
    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, Option[String])]
    21 
    22   val CHAPTER = "chapter"
    23   val SECTION = "section"
    24   val SUBSECTION = "subsection"
    25   val SUBSUBSECTION = "subsubsection"
    26   val PARAGRAPH = "paragraph"
    27   val SUBPARAGRAPH = "subparagraph"
    28   val TEXT = "text"
    29   val TXT = "txt"
    30   val TEXT_RAW = "text_raw"
    31 
    32   val THEORY = "theory"
    33   val IMPORTS = "imports"
    34   val KEYWORDS = "keywords"
    35   val AND = "and"
    36   val BEGIN = "begin"
    37 
    38   private val bootstrap_header: Keywords =
    39     List(
    40       ("%", Keyword.no_spec, None),
    41       ("(", Keyword.no_spec, None),
    42       (")", Keyword.no_spec, None),
    43       (",", Keyword.no_spec, None),
    44       ("::", Keyword.no_spec, None),
    45       ("==", Keyword.no_spec, None),
    46       (AND, Keyword.no_spec, None),
    47       (BEGIN, Keyword.no_spec, None),
    48       (IMPORTS, Keyword.no_spec, None),
    49       (KEYWORDS, Keyword.no_spec, None),
    50       (CHAPTER, (((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
    51       (SECTION, (((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
    52       (SUBSECTION, (((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
    53       (SUBSUBSECTION, (((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
    54       (PARAGRAPH, (((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
    55       (SUBPARAGRAPH, (((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
    56       (TEXT, (((Keyword.DOCUMENT_BODY, Nil), Nil)), None),
    57       (TXT, (((Keyword.DOCUMENT_BODY, Nil), Nil)), None),
    58       (TEXT_RAW, (((Keyword.DOCUMENT_RAW, Nil), Nil)), None),
    59       (THEORY, ((Keyword.THY_BEGIN, Nil), List("theory")), None),
    60       ("ML", ((Keyword.THY_DECL, Nil), List("ML")), None))
    61 
    62   private val bootstrap_keywords =
    63     Keyword.Keywords.empty.add_keywords(bootstrap_header)
    64 
    65   lazy val bootstrap_syntax: Outer_Syntax =
    66     Outer_Syntax.init().add_keywords(bootstrap_header)
    67 
    68 
    69   /* file name */
    70 
    71   val PURE = "Pure"
    72   val ML_BOOTSTRAP = "ML_Bootstrap"
    73   val ML_ROOT = "ML_Root"
    74   val ml_roots = List("ROOT0.ML" -> "ML_Root0", "ROOT.ML" -> ML_ROOT)
    75   val bootstrap_thys = List(PURE, ML_BOOTSTRAP).map(a => a -> ("Bootstrap_" + a))
    76 
    77   private val Base_Name = new Regex(""".*?([^/\\:]+)""")
    78   private val Thy_Name = new Regex(""".*?([^/\\:]+)\.thy""")
    79 
    80   def base_name(s: String): String =
    81     s match { case Base_Name(name) => name case _ => error("Malformed import: " + quote(s)) }
    82 
    83   def thy_name(s: String): Option[String] =
    84     s match { case Thy_Name(name) => Some(name) case _ => None }
    85 
    86   def thy_name_bootstrap(s: String): Option[String] =
    87     s match {
    88       case Thy_Name(name) =>
    89         Some(bootstrap_thys.collectFirst({ case (a, b) if a == name => b }).getOrElse(name))
    90       case Base_Name(name) => ml_roots.collectFirst({ case (a, b) if a == name => b })
    91       case _ => None
    92     }
    93 
    94 
    95   /* header */
    96 
    97   val header: Parser[Thy_Header] =
    98   {
    99     val opt_files =
   100       $$$("(") ~! (rep1sep(name, $$$(",")) <~ $$$(")")) ^^ { case _ ~ x => x } |
   101       success(Nil)
   102 
   103     val keyword_spec =
   104       atom("outer syntax keyword specification", _.is_name) ~ opt_files ~ tags ^^
   105       { case x ~ y ~ z => ((x, y), z) }
   106 
   107     val keyword_decl =
   108       rep1(string) ~
   109       opt($$$("::") ~! keyword_spec ^^ { case _ ~ x => x }) ~
   110       opt($$$("==") ~! name ^^ { case _ ~ x => x }) ^^
   111       { case xs ~ y ~ z => xs.map((_, y.getOrElse(Keyword.no_spec), z)) }
   112 
   113     val keyword_decls =
   114       keyword_decl ~ rep($$$(AND) ~! keyword_decl ^^ { case _ ~ x => x }) ^^
   115       { case xs ~ yss => (xs :: yss).flatten }
   116 
   117     val args =
   118       position(theory_name) ~
   119       (opt($$$(IMPORTS) ~! rep1(position(theory_name))) ^^
   120         { case None => Nil case Some(_ ~ xs) => xs }) ~
   121       (opt($$$(KEYWORDS) ~! keyword_decls) ^^
   122         { case None => Nil case Some(_ ~ xs) => xs }) ~
   123       $$$(BEGIN) ^^
   124       { case x ~ ys ~ zs ~ _ => Thy_Header(x, ys, zs) }
   125 
   126     val heading =
   127       (command(CHAPTER) |
   128         command(SECTION) |
   129         command(SUBSECTION) |
   130         command(SUBSUBSECTION) |
   131         command(PARAGRAPH) |
   132         command(SUBPARAGRAPH) |
   133         command(TEXT) |
   134         command(TXT) |
   135         command(TEXT_RAW)) ~
   136       tags ~! document_source
   137 
   138     (rep(heading) ~ command(THEORY) ~ tags) ~! args ^^ { case _ ~ x => x }
   139   }
   140 
   141 
   142   /* read -- lazy scanning */
   143 
   144   def read(reader: Reader[Char], start: Token.Pos): Thy_Header =
   145   {
   146     val token = Token.Parsers.token(bootstrap_keywords)
   147     val toks = new mutable.ListBuffer[Token]
   148 
   149     @tailrec def scan_to_begin(in: Reader[Char])
   150     {
   151       token(in) match {
   152         case Token.Parsers.Success(tok, rest) =>
   153           toks += tok
   154           if (!tok.is_begin) scan_to_begin(rest)
   155         case _ =>
   156       }
   157     }
   158     scan_to_begin(reader)
   159 
   160     parse(commit(header), Token.reader(toks.toList, start)) match {
   161       case Success(result, _) => result
   162       case bad => error(bad.toString)
   163     }
   164   }
   165 
   166   def read(source: CharSequence, start: Token.Pos): Thy_Header =
   167     read(new CharSequenceReader(source), start)
   168 }
   169 
   170 
   171 sealed case class Thy_Header(
   172   name: (String, Position.T),
   173   imports: List[(String, Position.T)],
   174   keywords: Thy_Header.Keywords)
   175 {
   176   def decode_symbols: Thy_Header =
   177   {
   178     val f = Symbol.decode _
   179     Thy_Header((f(name._1), name._2), imports.map({ case (a, b) => (f(a), b) }),
   180       keywords.map({ case (a, ((x, y), z), c) =>
   181         (f(a), ((f(x), y.map(f)), z.map(f)), c.map(f)) }))
   182   }
   183 }