src/Pure/Thy/thy_header.scala
author wenzelm
Wed Nov 05 16:57:12 2014 +0100 (2014-11-05)
changeset 58900 1435cc20b022
parent 58899 0a793c580685
child 58903 38c72f5f6c2e
permissions -rw-r--r--
explicit type Keyword.Keywords;
     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   val HEADER = "header"
    19   val CHAPTER = "chapter"
    20   val SECTION = "section"
    21   val SUBSECTION = "subsection"
    22   val SUBSUBSECTION = "subsubsection"
    23 
    24   val THEORY = "theory"
    25   val IMPORTS = "imports"
    26   val KEYWORDS = "keywords"
    27   val AND = "and"
    28   val BEGIN = "begin"
    29 
    30   private val keywords =
    31     Keyword.Keywords(
    32       List("%", "(", ")", ",", "::", "==", AND, BEGIN,
    33         HEADER, CHAPTER, SECTION, SUBSECTION, SUBSUBSECTION, IMPORTS, KEYWORDS, THEORY))
    34 
    35 
    36   /* theory file name */
    37 
    38   private val Base_Name = new Regex(""".*?([^/\\:]+)""")
    39   private val Thy_Name = new Regex(""".*?([^/\\:]+)\.thy""")
    40 
    41   def base_name(s: String): String =
    42     s match { case Base_Name(name) => name case _ => error("Malformed import: " + quote(s)) }
    43 
    44   def thy_name(s: String): Option[String] =
    45     s match { case Thy_Name(name) => Some(name) case _ => None }
    46 
    47 
    48   /* header */
    49 
    50   val header: Parser[Thy_Header] =
    51   {
    52     val file_name = atom("file name", _.is_name)
    53 
    54     val opt_files =
    55       keyword("(") ~! (rep1sep(name, keyword(",")) <~ keyword(")")) ^^ { case _ ~ x => x } |
    56       success(Nil)
    57     val keyword_spec =
    58       atom("outer syntax keyword specification", _.is_name) ~ opt_files ~ tags ^^
    59       { case x ~ y ~ z => ((x, y), z) }
    60 
    61     val keyword_decl =
    62       rep1(string) ~
    63       opt(keyword("::") ~! keyword_spec ^^ { case _ ~ x => x }) ~
    64       opt(keyword("==") ~! name ^^ { case _ ~ x => x }) ^^
    65       { case xs ~ y ~ z => xs.map((_, y, z)) }
    66     val keyword_decls =
    67       keyword_decl ~ rep(keyword(AND) ~! keyword_decl ^^ { case _ ~ x => x }) ^^
    68       { case xs ~ yss => (xs :: yss).flatten }
    69 
    70     val file =
    71       keyword("(") ~! (file_name ~ keyword(")")) ^^ { case _ ~ (x ~ _) => (x, false) } |
    72       file_name ^^ (x => (x, true))
    73 
    74     val args =
    75       theory_name ~
    76       (opt(keyword(IMPORTS) ~! (rep1(theory_xname))) ^^
    77         { case None => Nil case Some(_ ~ xs) => xs }) ~
    78       (opt(keyword(KEYWORDS) ~! keyword_decls) ^^
    79         { case None => Nil case Some(_ ~ xs) => xs }) ~
    80       keyword(BEGIN) ^^
    81       { case x ~ ys ~ zs ~ _ => Thy_Header(x, ys, zs) }
    82 
    83     val heading =
    84       (keyword(HEADER) |
    85         keyword(CHAPTER) |
    86         keyword(SECTION) |
    87         keyword(SUBSECTION) |
    88         keyword(SUBSUBSECTION)) ~
    89       tags ~! document_source
    90 
    91     (rep(heading) ~ keyword(THEORY) ~ tags) ~! args ^^ { case _ ~ x => x }
    92   }
    93 
    94 
    95   /* read -- lazy scanning */
    96 
    97   def read(reader: Reader[Char]): Thy_Header =
    98   {
    99     val token = Token.Parsers.token(keywords)
   100     val toks = new mutable.ListBuffer[Token]
   101 
   102     @tailrec def scan_to_begin(in: Reader[Char])
   103     {
   104       token(in) match {
   105         case Token.Parsers.Success(tok, rest) =>
   106           toks += tok
   107           if (!tok.is_begin) scan_to_begin(rest)
   108         case _ =>
   109       }
   110     }
   111     scan_to_begin(reader)
   112 
   113     parse(commit(header), Token.reader(toks.toList)) match {
   114       case Success(result, _) => result
   115       case bad => error(bad.toString)
   116     }
   117   }
   118 
   119   def read(source: CharSequence): Thy_Header =
   120     read(new CharSequenceReader(source))
   121 
   122 
   123   /* keywords */
   124 
   125   type Keywords = List[(String, Option[Keyword.Spec], Option[String])]
   126 }
   127 
   128 
   129 sealed case class Thy_Header(
   130   name: String,
   131   imports: List[String],
   132   keywords: Thy_Header.Keywords)
   133 {
   134   def map(f: String => String): Thy_Header =
   135     Thy_Header(f(name), imports.map(f), keywords)
   136 
   137   def decode_symbols: Thy_Header =
   138   {
   139     val f = Symbol.decode _
   140     Thy_Header(f(name), imports.map(f),
   141       keywords.map({ case (a, b, c) =>
   142         (f(a), b.map({ case ((x, y), z) => ((f(x), y.map(f)), z.map(f)) }), c.map(f)) }))
   143   }
   144 }
   145