1/* Title: Pure/Thy/thy_header.scala 2 Author: Makarius 3 4Static theory header information. 5*/ 6 7package isabelle 8 9 10import scala.annotation.tailrec 11import scala.collection.mutable 12import scala.util.parsing.input.Reader 13import scala.util.matching.Regex 14 15 16object 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 = 80 (Sessions.root_name :: (ml_roots ::: bootstrap_thys).map(_._2)).map(_ -> PURE) 81 82 private val Thy_File_Name = new Regex(""".*?([^/\\:]+)\.thy""") 83 private val File_Name = new Regex(""".*?([^/\\:]+)""") 84 85 def is_base_name(s: String): Boolean = 86 s != "" && !s.exists("/\\:".contains(_)) 87 88 def file_name(s: String): Option[String] = 89 s match { 90 case File_Name(s) => Some(s) 91 case _ => None 92 } 93 94 def import_name(s: String): String = 95 s match { 96 case File_Name(name) if !name.endsWith(".thy") => name 97 case _ => error("Malformed theory import: " + quote(s)) 98 } 99 100 def theory_name(s: String): String = 101 s match { 102 case Thy_File_Name(name) => bootstrap_name(name) 103 case File_Name(name) => 104 if (name == Sessions.root_name) name 105 else ml_roots.collectFirst({ case (a, b) if a == name => b }).getOrElse("") 106 case _ => "" 107 } 108 109 def is_ml_root(theory: String): Boolean = 110 ml_roots.exists({ case (_, b) => b == theory }) 111 112 def is_bootstrap(theory: String): Boolean = 113 bootstrap_thys.exists({ case (_, b) => b == theory }) 114 115 def bootstrap_name(theory: String): String = 116 bootstrap_thys.collectFirst({ case (a, b) if a == theory => b }).getOrElse(theory) 117 118 119 /* header */ 120 121 val header: Parser[Thy_Header] = 122 { 123 val opt_files = 124 $$$("(") ~! (rep1sep(name, $$$(",")) <~ $$$(")")) ^^ { case _ ~ x => x } | 125 success(Nil) 126 127 val keyword_spec = 128 atom("outer syntax keyword specification", _.is_name) ~ opt_files ~ tags ^^ 129 { case x ~ y ~ z => Keyword.Spec(x, y, z) } 130 131 val keyword_decl = 132 rep1(string) ~ 133 opt($$$("::") ~! keyword_spec ^^ { case _ ~ x => x }) ^^ 134 { case xs ~ y => xs.map((_, y.getOrElse(Keyword.Spec.none))) } 135 136 val keyword_decls = 137 keyword_decl ~ rep($$$(AND) ~! keyword_decl ^^ { case _ ~ x => x }) ^^ 138 { case xs ~ yss => (xs :: yss).flatten } 139 140 val abbrevs = 141 rep1sep(rep1(text) ~ ($$$("=") ~! rep1(text)), $$$("and")) ^^ 142 { case res => for ((as ~ (_ ~ bs)) <- res; a <- as; b <- bs) yield (a, b) } 143 144 val args = 145 position(theory_name) ~ 146 (opt($$$(IMPORTS) ~! rep1(position(theory_name))) ^^ 147 { case None => Nil case Some(_ ~ xs) => xs }) ~ 148 (opt($$$(KEYWORDS) ~! keyword_decls) ^^ 149 { case None => Nil case Some(_ ~ xs) => xs }) ~ 150 (opt($$$(ABBREVS) ~! abbrevs) ^^ 151 { case None => Nil case Some(_ ~ xs) => xs }) ~ 152 $$$(BEGIN) ^^ 153 { case (name, pos) ~ imports ~ keywords ~ abbrevs ~ _ => 154 val f = Symbol.decode _ 155 Thy_Header((f(name), pos), 156 imports.map({ case (a, b) => (f(a), b) }), 157 keywords.map({ case (a, Keyword.Spec(b, c, d)) => 158 (f(a), Keyword.Spec(f(b), c.map(f), d.map(f))) }), 159 abbrevs.map({ case (a, b) => (f(a), f(b)) })) 160 } 161 162 val heading = 163 (command(CHAPTER) | 164 command(SECTION) | 165 command(SUBSECTION) | 166 command(SUBSUBSECTION) | 167 command(PARAGRAPH) | 168 command(SUBPARAGRAPH) | 169 command(TEXT) | 170 command(TXT) | 171 command(TEXT_RAW)) ~ 172 tags ~! document_source 173 174 (rep(heading) ~ command(THEORY) ~ tags) ~! args ^^ { case _ ~ x => x } 175 } 176 177 178 /* read -- lazy scanning */ 179 180 private def read_tokens(reader: Reader[Char], strict: Boolean): (List[Token], List[Token]) = 181 { 182 val token = Token.Parsers.token(bootstrap_keywords) 183 def make_tokens(in: Reader[Char]): Stream[Token] = 184 token(in) match { 185 case Token.Parsers.Success(tok, rest) => tok #:: make_tokens(rest) 186 case _ => Stream.empty 187 } 188 189 val all_tokens = make_tokens(reader) 190 val drop_tokens = 191 if (strict) Nil 192 else all_tokens.takeWhile(tok => !tok.is_command(Thy_Header.THEORY)).toList 193 194 val tokens = all_tokens.drop(drop_tokens.length) 195 val tokens1 = tokens.takeWhile(tok => !tok.is_begin).toList 196 val tokens2 = tokens.dropWhile(tok => !tok.is_begin).headOption.toList 197 198 (drop_tokens, tokens1 ::: tokens2) 199 } 200 201 def read(reader: Reader[Char], start: Token.Pos, strict: Boolean = true): Thy_Header = 202 { 203 val (_, tokens0) = read_tokens(reader, true) 204 val text = Scan.reader_decode_utf8(reader, Token.implode(tokens0)) 205 206 val (drop_tokens, tokens) = read_tokens(Scan.char_reader(text), strict) 207 val pos = (start /: drop_tokens)(_.advance(_)) 208 209 parse(commit(header), Token.reader(tokens, pos)) match { 210 case Success(result, _) => result 211 case bad => error(bad.toString) 212 } 213 } 214} 215 216sealed case class Thy_Header( 217 name: (String, Position.T), 218 imports: List[(String, Position.T)], 219 keywords: Thy_Header.Keywords, 220 abbrevs: Thy_Header.Abbrevs) 221