1/*  Title:      Pure/Thy/export.scala
2    Author:     Makarius
3
4Manage theory exports: compressed blobs.
5*/
6
7package isabelle
8
9
10import scala.annotation.tailrec
11import scala.util.matching.Regex
12
13
14object Export
15{
16  /* SQL data model */
17
18  object Data
19  {
20    val session_name = SQL.Column.string("session_name").make_primary_key
21    val theory_name = SQL.Column.string("theory_name").make_primary_key
22    val name = SQL.Column.string("name").make_primary_key
23    val compressed = SQL.Column.bool("compressed")
24    val body = SQL.Column.bytes("body")
25
26    val table =
27      SQL.Table("isabelle_exports", List(session_name, theory_name, name, compressed, body))
28
29    def where_equal(session_name: String, theory_name: String = "", name: String = ""): SQL.Source =
30      "WHERE " + Data.session_name.equal(session_name) +
31        (if (theory_name == "") "" else " AND " + Data.theory_name.equal(theory_name)) +
32        (if (name == "") "" else " AND " + Data.name.equal(name))
33  }
34
35  def read_name(db: SQL.Database, session_name: String, theory_name: String, name: String): Boolean =
36  {
37    val select =
38      Data.table.select(List(Data.name), Data.where_equal(session_name, theory_name, name))
39    db.using_statement(select)(stmt => stmt.execute_query().next())
40  }
41
42  def read_names(db: SQL.Database, session_name: String, theory_name: String): List[String] =
43  {
44    val select = Data.table.select(List(Data.name), Data.where_equal(session_name, theory_name))
45    db.using_statement(select)(stmt =>
46      stmt.execute_query().iterator(res => res.string(Data.name)).toList)
47  }
48
49  def read_theory_names(db: SQL.Database, session_name: String): List[String] =
50  {
51    val select =
52      Data.table.select(List(Data.theory_name), Data.where_equal(session_name), distinct = true)
53    db.using_statement(select)(stmt =>
54      stmt.execute_query().iterator(_.string(Data.theory_name)).toList)
55  }
56
57  def read_theory_exports(db: SQL.Database, session_name: String): List[(String, String)] =
58  {
59    val select = Data.table.select(List(Data.theory_name, Data.name), Data.where_equal(session_name))
60    db.using_statement(select)(stmt =>
61      stmt.execute_query().iterator(res =>
62        (res.string(Data.theory_name), res.string(Data.name))).toList)
63  }
64
65  def message(msg: String, theory_name: String, name: String): String =
66    msg + " " + quote(name) + " for theory " + quote(theory_name)
67
68  def compound_name(a: String, b: String): String = a + ":" + b
69
70  sealed case class Entry(
71    session_name: String,
72    theory_name: String,
73    name: String,
74    body: Future[(Boolean, Bytes)])
75  {
76    override def toString: String = compound_name(theory_name, name)
77
78    def write(db: SQL.Database)
79    {
80      val (compressed, bytes) = body.join
81      db.using_statement(Data.table.insert())(stmt =>
82      {
83        stmt.string(1) = session_name
84        stmt.string(2) = theory_name
85        stmt.string(3) = name
86        stmt.bool(4) = compressed
87        stmt.bytes(5) = bytes
88        stmt.execute()
89      })
90    }
91
92    def uncompressed(cache: XZ.Cache = XZ.cache()): Bytes =
93    {
94      val (compressed, bytes) = body.join
95      if (compressed) bytes.uncompress(cache = cache) else bytes
96    }
97
98    def uncompressed_yxml(cache: XZ.Cache = XZ.cache()): XML.Body =
99      YXML.parse_body(UTF8.decode_permissive(uncompressed(cache = cache)))
100  }
101
102  def make_regex(pattern: String): Regex =
103  {
104    @tailrec def make(result: List[String], depth: Int, chs: List[Char]): Regex =
105      chs match {
106        case '*' :: '*' :: rest => make("[^:]*" :: result, depth, rest)
107        case '*' :: rest => make("[^:/]*" :: result, depth, rest)
108        case '?' :: rest => make("[^:/]" :: result, depth, rest)
109        case '\\' :: c :: rest => make(("\\" + c) :: result, depth, rest)
110        case '{' :: rest => make("(" :: result, depth + 1, rest)
111        case ',' :: rest if depth > 0 => make("|" :: result, depth, rest)
112        case '}' :: rest if depth > 0 => make(")" :: result, depth - 1, rest)
113        case c :: rest if ".+()".contains(c) => make(("\\" + c) :: result, depth, rest)
114        case c :: rest => make(c.toString :: result, depth, rest)
115        case Nil => result.reverse.mkString.r
116      }
117    make(Nil, 0, pattern.toList)
118  }
119
120  def make_matcher(pattern: String): (String, String) => Boolean =
121  {
122    val regex = make_regex(pattern)
123    (theory_name: String, name: String) =>
124      regex.pattern.matcher(compound_name(theory_name, name)).matches
125  }
126
127  def make_entry(session_name: String, args: Markup.Export.Args, body: Bytes,
128    cache: XZ.Cache = XZ.cache()): Entry =
129  {
130    Entry(session_name, args.theory_name, args.name,
131      if (args.compress) Future.fork(body.maybe_compress(cache = cache))
132      else Future.value((false, body)))
133  }
134
135  def read_entry(db: SQL.Database, session_name: String, theory_name: String, name: String)
136    : Option[Entry] =
137  {
138    val select =
139      Data.table.select(List(Data.compressed, Data.body),
140        Data.where_equal(session_name, theory_name, name))
141    db.using_statement(select)(stmt =>
142    {
143      val res = stmt.execute_query()
144      if (res.next()) {
145        val compressed = res.bool(Data.compressed)
146        val body = res.bytes(Data.body)
147        Some(Entry(session_name, theory_name, name, Future.value(compressed, body)))
148      }
149      else None
150    })
151  }
152
153
154  /* database consumer thread */
155
156  def consumer(db: SQL.Database, cache: XZ.Cache = XZ.cache()): Consumer = new Consumer(db, cache)
157
158  class Consumer private[Export](db: SQL.Database, cache: XZ.Cache)
159  {
160    private val export_errors = Synchronized[List[String]](Nil)
161
162    private val consumer =
163      Consumer_Thread.fork(name = "export")(consume = (entry: Entry) =>
164        {
165          entry.body.join
166          db.transaction {
167            if (read_name(db, entry.session_name, entry.theory_name, entry.name)) {
168              val err = message("Duplicate export", entry.theory_name, entry.name)
169              export_errors.change(errs => err :: errs)
170            }
171            else entry.write(db)
172          }
173          true
174        })
175
176    def apply(session_name: String, args: Markup.Export.Args, body: Bytes): Unit =
177      consumer.send(make_entry(session_name, args, body, cache = cache))
178
179    def shutdown(close: Boolean = false): List[String] =
180    {
181      consumer.shutdown()
182      if (close) db.close()
183      export_errors.value.reverse
184    }
185  }
186
187
188  /* abstract provider */
189
190  object Provider
191  {
192    def database(db: SQL.Database, session_name: String, theory_name: String): Provider =
193      new Provider {
194        def apply(export_name: String): Option[Entry] =
195          read_entry(db, session_name, theory_name, export_name)
196      }
197
198    def snapshot(snapshot: Document.Snapshot): Provider =
199      new Provider {
200        def apply(export_name: String): Option[Entry] =
201          snapshot.exports_map.get(export_name)
202      }
203  }
204
205  trait Provider
206  {
207    def apply(export_name: String): Option[Entry]
208
209    def uncompressed_yxml(export_name: String, cache: XZ.Cache = XZ.cache()): XML.Body =
210      apply(export_name) match {
211        case Some(entry) => entry.uncompressed_yxml(cache = cache)
212        case None => Nil
213      }
214  }
215
216
217  /* export to file-system */
218
219  def export_files(
220    store: Sessions.Store,
221    session_name: String,
222    export_dir: Path,
223    progress: Progress = No_Progress,
224    export_list: Boolean = false,
225    export_patterns: List[String] = Nil,
226    export_prefix: String = "")
227  {
228    using(store.open_database(session_name))(db =>
229    {
230      db.transaction {
231        val export_names = read_theory_exports(db, session_name)
232
233        // list
234        if (export_list) {
235          (for ((theory_name, name) <- export_names) yield compound_name(theory_name, name)).
236            sorted.foreach(progress.echo(_))
237        }
238
239        // export
240        if (export_patterns.nonEmpty) {
241          val exports =
242            (for {
243              export_pattern <- export_patterns.iterator
244              matcher = make_matcher(export_pattern)
245              (theory_name, name) <- export_names if matcher(theory_name, name)
246            } yield (theory_name, name)).toSet
247          for {
248            (theory_name, group) <- exports.toList.groupBy(_._1).toList.sortBy(_._1)
249            name <- group.map(_._2).sorted
250            entry <- read_entry(db, session_name, theory_name, name)
251          } {
252            val path = export_dir + Path.basic(theory_name) + Path.explode(name)
253            progress.echo(export_prefix + "export " + path)
254            Isabelle_System.mkdirs(path.dir)
255            Bytes.write(path, entry.uncompressed(cache = store.xz_cache))
256          }
257        }
258      }
259    })
260  }
261
262
263  /* Isabelle tool wrapper */
264
265  val default_export_dir = Path.explode("export")
266
267  val isabelle_tool = Isabelle_Tool("export", "retrieve theory exports", args =>
268  {
269    /* arguments */
270
271    var export_dir = default_export_dir
272    var dirs: List[Path] = Nil
273    var export_list = false
274    var no_build = false
275    var options = Options.init()
276    var system_mode = false
277    var export_patterns: List[String] = Nil
278
279    val getopts = Getopts("""
280Usage: isabelle export [OPTIONS] SESSION
281
282  Options are:
283    -O DIR       output directory for exported files (default: """ + default_export_dir + """)
284    -d DIR       include session directory
285    -l           list exports
286    -n           no build of session
287    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
288    -s           system build mode for session image
289    -x PATTERN   extract files matching pattern (e.g. "*:**" for all)
290
291  List or export theory exports for SESSION: named blobs produced by
292  isabelle build. Option -l or -x is required; option -x may be repeated.
293
294  The PATTERN language resembles glob patterns in the shell, with ? and *
295  (both excluding ":" and "/"), ** (excluding ":"), and [abc] or [^abc],
296  and variants {pattern1,pattern2,pattern3}.
297""",
298      "O:" -> (arg => export_dir = Path.explode(arg)),
299      "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
300      "l" -> (_ => export_list = true),
301      "n" -> (_ => no_build = true),
302      "o:" -> (arg => options = options + arg),
303      "s" -> (_ => system_mode = true),
304      "x:" -> (arg => export_patterns ::= arg))
305
306    val more_args = getopts(args)
307    val session_name =
308      more_args match {
309        case List(session_name) if export_list || export_patterns.nonEmpty => session_name
310        case _ => getopts.usage()
311      }
312
313    val progress = new Console_Progress()
314
315
316    /* build */
317
318    if (!no_build) {
319      val rc =
320        progress.interrupt_handler {
321          Build.build_logic(options, session_name, progress = progress,
322            dirs = dirs, system_mode = system_mode)
323        }
324      if (rc != 0) sys.exit(rc)
325    }
326
327
328    /* export files */
329
330    val store = Sessions.store(options, system_mode)
331    export_files(store, session_name, export_dir, progress = progress,
332      export_list = export_list, export_patterns = export_patterns)
333  })
334}
335