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