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