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