# HG changeset patch # User nipkow # Date 1525784779 -7200 # Node ID 6a63a4ce756bb6d81a93af2e66391ce4736bb11e # Parent 2277fe496d787f9fc4ba82b5e7e4be3f901fd07c# Parent bdbf759ddbac3939a0bd9ec748b68c42bbcdd887 merged diff -r bdbf759ddbac -r 6a63a4ce756b NEWS --- a/NEWS Tue May 08 12:16:10 2018 +0200 +++ b/NEWS Tue May 08 15:06:19 2018 +0200 @@ -278,10 +278,6 @@ HOL-Computational_Algebra.Field_as_Ring explicitly in case of need. INCOMPATIBILITY. -* Fact mod_mult_self4 (on nat) renamed to mod_mult_self3', to avoid -clash with fact mod_mult_self4 (on more generic semirings). -INCOMPATIBILITY. - * Facts sum.commute(_restrict) and prod.commute(_restrict) renamed to sum.swap(_restrict) and prod.swap(_restrict), to avoid name clashes on interpretation of abstract locales. INCOMPATIBILITY. @@ -318,6 +314,18 @@ * Code generation: Code generation takes an explicit option "case_insensitive" to accomodate case-insensitive file systems. +* Fact mod_mult_self4 (on nat) renamed to Suc_mod_mult_self3, to avoid +clash with fact mod_mult_self4 (on more generic semirings). +INCOMPATIBILITY. + +* Eliminated some theorem aliasses: + + even_times_iff ~> even_mult_iff + mod_2_not_eq_zero_eq_one_nat ~> not_mod_2_eq_0_eq_1 + even_of_nat ~> even_int_iff + +INCOMPATIBILITY. + *** System *** diff -r bdbf759ddbac -r 6a63a4ce756b src/Doc/System/Server.thy --- a/src/Doc/System/Server.thy Tue May 08 12:16:10 2018 +0200 +++ b/src/Doc/System/Server.thy Tue May 08 15:06:19 2018 +0200 @@ -897,10 +897,14 @@ \end{tabular} \begin{tabular}{ll} + \<^bold>\type\ \export =\ \\ + \quad~~\{name: string, base64: bool, body: string}\ \\ + \<^bold>\type\ \node_results =\ \\ + \quad~~\{status: node_status, messages: [message], exports: [export]}\ \\ \<^bold>\type\ \use_theories_results =\ \\ \quad\{ok: bool,\ \\ \quad~~\errors: [message],\ \\ - \quad~~\nodes: [node \ {status: node_status, messages: [message]}]}\ \\ + \quad~~\nodes: [node \ node_results]}\ \\ \end{tabular} \<^medskip> @@ -916,6 +920,14 @@ invocations of \<^verbatim>\use_theories\ are idempotent: it could make sense to do that with different values for \pretty_margin\ or \unicode_symbols\ to get different formatting for \errors\ or \messages\. + + The \exports\ can be arbitrary binary resources produced by a theory. An + \export\ \name\ roughly follows file-system standards: ``\<^verbatim>\/\'' separated + list of base names (excluding special names like ``\<^verbatim>\.\'' or ``\<^verbatim>\..\''). The + \base64\ field specifies the format of the \body\ string: it is true for a + byte vector that cannot be represented as plain text in UTF-8 encoding, + which means the string needs to be decoded as in + \<^verbatim>\java.util.Base64.getDecoder.decode(String)\. \ diff -r bdbf759ddbac -r 6a63a4ce756b src/HOL/Divides.thy --- a/src/HOL/Divides.thy Tue May 08 12:16:10 2018 +0200 +++ b/src/HOL/Divides.thy Tue May 08 15:06:19 2018 +0200 @@ -1295,10 +1295,6 @@ subsubsection \Lemmas of doubtful value\ -lemma mod_mult_self3': - "Suc (k * n + m) mod n = Suc m mod n" - by (fact Suc_mod_mult_self3) - lemma mod_Suc_eq_Suc_mod: "Suc m mod n = Suc (m mod n) mod n" by (simp add: mod_simps) @@ -1327,16 +1323,6 @@ then show ?thesis .. qed -lemmas even_times_iff = even_mult_iff \ \FIXME duplicate\ - -lemma mod_2_not_eq_zero_eq_one_nat: - fixes n :: nat - shows "n mod 2 \ 0 \ n mod 2 = 1" - by (fact not_mod_2_eq_0_eq_1) - -lemma even_int_iff [simp]: "even (int n) \ even n" - by (fact even_of_nat) - lemma is_unit_int: "is_unit (k::int) \ k = 1 \ k = - 1" by auto diff -r bdbf759ddbac -r 6a63a4ce756b src/HOL/Groebner_Basis.thy --- a/src/HOL/Groebner_Basis.thy Tue May 08 12:16:10 2018 +0200 +++ b/src/HOL/Groebner_Basis.thy Tue May 08 15:06:19 2018 +0200 @@ -78,7 +78,7 @@ context semiring_parity begin -declare even_times_iff [algebra] +declare even_mult_iff [algebra] declare even_power [algebra] end diff -r bdbf759ddbac -r 6a63a4ce756b src/HOL/Presburger.thy --- a/src/HOL/Presburger.thy Tue May 08 12:16:10 2018 +0200 +++ b/src/HOL/Presburger.thy Tue May 08 15:06:19 2018 +0200 @@ -435,7 +435,7 @@ context semiring_parity begin -declare even_times_iff [presburger] +declare even_mult_iff [presburger] declare even_power [presburger] diff -r bdbf759ddbac -r 6a63a4ce756b src/HOL/Tools/string_syntax.ML --- a/src/HOL/Tools/string_syntax.ML Tue May 08 12:16:10 2018 +0200 +++ b/src/HOL/Tools/string_syntax.ML Tue May 08 15:06:19 2018 +0200 @@ -117,7 +117,7 @@ c $ string_tr [t] $ u | string_tr [Free (str, _)] = mk_string_syntax (plain_strings_of str) - | string_tr ts = raise TERM ("char_tr", ts); + | string_tr ts = raise TERM ("string_tr", ts); fun list_ast_tr' [args] = Ast.Appl [Ast.Constant @{syntax_const "_String"}, diff -r bdbf759ddbac -r 6a63a4ce756b src/HOL/Transcendental.thy --- a/src/HOL/Transcendental.thy Tue May 08 12:16:10 2018 +0200 +++ b/src/HOL/Transcendental.thy Tue May 08 15:06:19 2018 +0200 @@ -4173,10 +4173,10 @@ lemma cos_zero_iff_int: "cos x = 0 \ (\n. odd n \ x = of_int n * (pi/2))" proof safe assume "cos x = 0" - then show "\n. odd n \ x = of_int n * (pi/2)" - apply (simp add: cos_zero_iff) - apply safe - apply (metis even_int_iff of_int_of_nat_eq) + then show "\n. odd n \ x = of_int n * (pi / 2)" + unfolding cos_zero_iff + apply (auto simp add: cos_zero_iff) + apply (metis even_of_nat of_int_of_nat_eq) apply (rule_tac x="- (int n)" in exI) apply simp done @@ -4196,7 +4196,7 @@ then show "\n. even n \ x = of_int n * (pi / 2)" apply (simp add: sin_zero_iff) apply safe - apply (metis even_int_iff of_int_of_nat_eq) + apply (metis even_of_nat of_int_of_nat_eq) apply (rule_tac x="- (int n)" in exI) apply simp done diff -r bdbf759ddbac -r 6a63a4ce756b src/Pure/General/bytes.scala --- a/src/Pure/General/bytes.scala Tue May 08 12:16:10 2018 +0200 +++ b/src/Pure/General/bytes.scala Tue May 08 15:06:19 2018 +0200 @@ -56,6 +56,12 @@ new Bytes(a, 0, n) } + def base64(s: String): Bytes = + { + val a = Base64.getDecoder.decode(s) + new Bytes(a, 0, a.length) + } + /* read */ @@ -160,6 +166,12 @@ Base64.getEncoder.encodeToString(b) } + def maybe_base64: (Boolean, String) = + { + val s = text + if (this == Bytes(s)) (false, s) else (true, base64) + } + override def toString: String = { val str = text diff -r bdbf759ddbac -r 6a63a4ce756b src/Pure/Isar/class.ML --- a/src/Pure/Isar/class.ML Tue May 08 12:16:10 2018 +0200 +++ b/src/Pure/Isar/class.ML Tue May 08 15:06:19 2018 +0200 @@ -196,13 +196,13 @@ ([Pretty.keyword1 "class", Pretty.brk 1, Name_Space.pretty ctxt class_space class, Pretty.str ":", Pretty.fbrk, Pretty.block [Pretty.str "supersort: ", prt_supersort class]] @ - (case try (Axclass.get_info thy) class of - NONE => [] - | SOME {params, ...} => + (case (these o Option.map #params o try (Axclass.get_info thy)) class of + [] => [] + | params => [Pretty.fbrk, Pretty.big_list "parameters:" (map prt_param params)]) @ - (case Symtab.lookup arities class of - NONE => [] - | SOME ars => + (case (these o Symtab.lookup arities) class of + [] => [] + | ars => [Pretty.fbrk, Pretty.big_list "instances:" (map (prt_arity class) (sort (Name_Space.extern_ord ctxt type_space) ars))])); in diff -r bdbf759ddbac -r 6a63a4ce756b src/Pure/PIDE/command.scala --- a/src/Pure/PIDE/command.scala Tue May 08 12:16:10 2018 +0200 +++ b/src/Pure/PIDE/command.scala Tue May 08 15:06:19 2018 +0200 @@ -28,7 +28,7 @@ object Results { type Entry = (Long, XML.Tree) - val empty = new Results(SortedMap.empty) + val empty: Results = new Results(SortedMap.empty) def make(args: TraversableOnce[Results.Entry]): Results = (empty /: args)(_ + _) def merge(args: TraversableOnce[Results]): Results = (empty /: args)(_ ++ _) @@ -68,7 +68,39 @@ } - /* markup */ + /* exports */ + + object Exports + { + type Entry = (Long, Export.Entry) + val empty: Exports = new Exports(SortedMap.empty) + def merge(args: TraversableOnce[Exports]): Exports = (empty /: args)(_ ++ _) + } + + final class Exports private(private val rep: SortedMap[Long, Export.Entry]) + { + def iterator: Iterator[Exports.Entry] = rep.iterator + + def + (entry: Exports.Entry): Exports = + if (rep.isDefinedAt(entry._1)) this + else new Exports(rep + entry) + + def ++ (other: Exports): Exports = + if (this eq other) this + else if (rep.isEmpty) other + else (this /: other.iterator)(_ + _) + + override def hashCode: Int = rep.hashCode + override def equals(that: Any): Boolean = + that match { + case other: Exports => rep == other.rep + case _ => false + } + override def toString: String = iterator.mkString("Exports(", ", ", ")") + } + + + /* markups */ object Markup_Index { @@ -175,6 +207,9 @@ def merge_results(states: List[State]): Results = Results.merge(states.map(_.results)) + def merge_exports(states: List[State]): Exports = + Exports.merge(states.map(_.exports)) + def merge_markups(states: List[State]): Markups = Markups.merge(states.map(_.markups)) @@ -183,7 +218,8 @@ Markup_Tree.merge(states.map(_.markup(index)), range, elements) def merge(command: Command, states: List[State]): State = - State(command, states.flatMap(_.status), merge_results(states), merge_markups(states)) + State(command, states.flatMap(_.status), merge_results(states), + merge_exports(states), merge_markups(states)) /* XML data representation */ @@ -213,7 +249,7 @@ val blobs_info: Blobs_Info = (blobs_names.map(name => Exn.Res((node_name(name), None)): Blob), blobs_index) val command = Command(id, node_name(node), blobs_info, span) - State(command, status, results, markups) + State(command, status, results, Exports.empty, markups) } } @@ -221,6 +257,7 @@ command: Command, status: List[Markup] = Nil, results: Results = Results.empty, + exports: Exports = Exports.empty, markups: Markups = Markups.empty) { lazy val consolidated: Boolean = @@ -245,7 +282,7 @@ { val markups1 = markups.redirect(other_command.id) if (markups1.is_empty) None - else Some(new State(other_command, Nil, Results.empty, markups1)) + else Some(new State(other_command, markups = markups1)) } private def add_status(st: Markup): State = @@ -254,6 +291,9 @@ private def add_result(entry: Results.Entry): State = copy(results = results + entry) + def add_export(entry: Exports.Entry): State = + copy(exports = exports + entry) + private def add_markup( status: Boolean, chunk_name: Symbol.Text_Chunk.Name, m: Text.Markup): State = { @@ -342,7 +382,7 @@ Output.warning("Ignored message without serial number: " + message) this } - } + } } diff -r bdbf759ddbac -r 6a63a4ce756b src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Tue May 08 12:16:10 2018 +0200 +++ b/src/Pure/PIDE/document.scala Tue May 08 15:06:19 2018 +0200 @@ -721,6 +721,22 @@ } } + def add_export(id: Document_ID.Generic, entry: Command.Exports.Entry): (Command.State, State) = + { + execs.get(id) match { + case Some(st) => + val new_st = st.add_export(entry) + (new_st, copy(execs = execs + (id -> new_st))) + case None => + commands.get(id) match { + case Some(st) => + val new_st = st.add_export(entry) + (new_st, copy(commands = commands + (id -> new_st))) + case None => fail + } + } + } + def assign(id: Document_ID.Version, update: Assign_Update): (List[Command], State) = { val version = the_version(id) diff -r bdbf759ddbac -r 6a63a4ce756b src/Pure/PIDE/markup.ML --- a/src/Pure/PIDE/markup.ML Tue May 08 12:16:10 2018 +0200 +++ b/src/Pure/PIDE/markup.ML Tue May 08 15:06:19 2018 +0200 @@ -203,7 +203,8 @@ val command_timing: Properties.entry val theory_timing: Properties.entry val exportN: string - type export_args = {id: string option, theory_name: string, name: string, compress: bool} + type export_args = + {id: string option, serial: serial, theory_name: string, name: string, compress: bool} val export: export_args -> Properties.T val loading_theory: string -> Properties.T val dest_loading_theory: Properties.T -> string option @@ -642,9 +643,10 @@ val theory_timing = (functionN, "theory_timing"); val exportN = "export"; -type export_args = {id: string option, theory_name: string, name: string, compress: bool} -fun export ({id, theory_name, name, compress}: export_args) = - [(functionN, exportN), (idN, the_default "" id), +type export_args = + {id: string option, serial: serial, theory_name: string, name: string, compress: bool} +fun export ({id, serial, theory_name, name, compress}: export_args) = + [(functionN, exportN), (idN, the_default "" id), (serialN, Value.print_int serial), ("theory_name", theory_name), (nameN, name), ("compress", Value.print_bool compress)]; fun loading_theory name = [("function", "loading_theory"), ("name", name)]; diff -r bdbf759ddbac -r 6a63a4ce756b src/Pure/PIDE/markup.scala --- a/src/Pure/PIDE/markup.scala Tue May 08 12:16:10 2018 +0200 +++ b/src/Pure/PIDE/markup.scala Tue May 08 15:06:19 2018 +0200 @@ -571,7 +571,8 @@ val EXPORT = "export" object Export { - sealed case class Args(id: Option[String], theory_name: String, name: String, compress: Boolean) + sealed case class Args( + id: Option[String], serial: Long, theory_name: String, name: String, compress: Boolean) val THEORY_NAME = "theory_name" val COMPRESS = "compress" @@ -579,16 +580,26 @@ def dest_inline(props: Properties.T): Option[(Args, Bytes)] = props match { case - List((THEORY_NAME, theory_name), (NAME, name), (COMPRESS, Value.Boolean(compress)), - (EXPORT, hex)) => Some((Args(None, theory_name, name, compress), Bytes.hex(hex))) + List( + (SERIAL, Value.Long(serial)), + (THEORY_NAME, theory_name), + (NAME, name), + (COMPRESS, Value.Boolean(compress)), + (EXPORT, hex)) => + Some((Args(None, serial, theory_name, name, compress), Bytes.hex(hex))) case _ => None } def unapply(props: Properties.T): Option[Args] = props match { - case List((FUNCTION, EXPORT), (ID, id), - (THEORY_NAME, theory_name), (PATH, name), (COMPRESS, Value.Boolean(compress))) => - Some(Args(proper_string(id), theory_name, name, compress)) + case List( + (FUNCTION, EXPORT), + (ID, id), + (SERIAL, Value.Long(serial)), + (THEORY_NAME, theory_name), + (NAME, name), + (COMPRESS, Value.Boolean(compress))) => + Some(Args(proper_string(id), serial, theory_name, name, compress)) case _ => None } } diff -r bdbf759ddbac -r 6a63a4ce756b src/Pure/PIDE/session.scala --- a/src/Pure/PIDE/session.scala Tue May 08 12:16:10 2018 +0200 +++ b/src/Pure/PIDE/session.scala Tue May 08 15:06:19 2018 +0200 @@ -409,15 +409,13 @@ Output.warning("Ignoring bad prover output: " + output.message.toString) } - def accumulate(state_id: Document_ID.Generic, message: XML.Elem) + def change_command(f: Document.State => (Command.State, Document.State)) { try { - val st = global_state.change_result(_.accumulate(state_id, message, xml_cache)) + val st = global_state.change_result(f) change_buffer.invoke(false, List(st.command)) } - catch { - case _: Document.State.Fail => bad_output() - } + catch { case _: Document.State.Fail => bad_output() } } output match { @@ -430,13 +428,16 @@ case Protocol.Command_Timing(state_id, timing) if prover.defined => val message = XML.elem(Markup.STATUS, List(XML.Elem(Markup.Timing(timing), Nil))) - accumulate(state_id, xml_cache.elem(message)) + change_command(_.accumulate(state_id, xml_cache.elem(message), xml_cache)) case Protocol.Theory_Timing(_, _) => // FIXME - case Markup.Export(_) => - // FIXME + case Markup.Export(args) + if args.id.isDefined && Value.Long.unapply(args.id.get).isDefined => + val id = Value.Long.unapply(args.id.get).get + val entry = (args.serial, Export.make_entry("", args, msg.bytes)) + change_command(_.add_export(id, entry)) case Markup.Assign_Update => msg.text match { @@ -474,7 +475,7 @@ case _ => output.properties match { case Position.Id(state_id) => - accumulate(state_id, output.message) + change_command(_.accumulate(state_id, output.message, xml_cache)) case _ if output.is_init => prover.get.options(session_options) diff -r bdbf759ddbac -r 6a63a4ce756b src/Pure/Thy/export.ML --- a/src/Pure/Thy/export.ML Tue May 08 12:16:10 2018 +0200 +++ b/src/Pure/Thy/export.ML Tue May 08 15:06:19 2018 +0200 @@ -1,26 +1,39 @@ (* Title: Pure/Thy/export.ML Author: Makarius -Manage theory exports. +Manage theory exports: compressed blobs. *) signature EXPORT = sig - val export: theory -> string -> Output.output -> unit - val export_uncompressed: theory -> string -> Output.output -> unit + val export: theory -> string -> string -> unit + val export_raw: theory -> string -> string list -> unit end; structure Export: EXPORT = struct -fun gen_export compress thy name output = +fun check_name name = + let + fun err () = error ("Bad export name " ^ quote name); + fun check_elem elem = + if member (op =) ["", ".", ".."] elem then err () + else ignore (Path.basic elem handle ERROR _ => err ()); + + val elems = space_explode "/" name; + val _ = null elems andalso err (); + val _ = List.app check_elem elems; + in name end; + +fun gen_export compress thy name body = (Output.try_protocol_message o Markup.export) {id = Position.get_id (Position.thread_data ()), + serial = serial (), theory_name = Context.theory_long_name thy, - name = name, - compress = compress} [output]; + name = check_name name, + compress = compress} body; -val export = gen_export true; -val export_uncompressed = gen_export false; +fun export thy name body = gen_export (size body > 60) thy name [body]; +fun export_raw thy name body = gen_export false thy name body; end; diff -r bdbf759ddbac -r 6a63a4ce756b src/Pure/Thy/export.scala --- a/src/Pure/Thy/export.scala Tue May 08 12:16:10 2018 +0200 +++ b/src/Pure/Thy/export.scala Tue May 08 15:06:19 2018 +0200 @@ -1,7 +1,7 @@ /* Title: Pure/Thy/export.scala Author: Makarius -Manage theory exports. +Manage theory exports: compressed blobs. */ package isabelle @@ -33,31 +33,39 @@ stmt.execute_query().iterator(res => res.string(Data.name)).toList) } + def message(msg: String, theory_name: String, name: String): String = + msg + " " + quote(name) + " for theory " + quote(theory_name) + sealed case class Entry( - session_name: String, theory_name: String, name: String, compressed: Boolean, body: Bytes) + session_name: String, + theory_name: String, + name: String, + compressed: Boolean, + body: Future[Bytes]) { override def toString: String = theory_name + ":" + name - def message(msg: String): String = - msg + " " + quote(name) + " for theory " + quote(theory_name) - - lazy val compressed_body: Bytes = if (compressed) body else body.compress() - lazy val uncompressed_body: Bytes = if (compressed) body.uncompress() else body - def write(db: SQL.Database) { + val bytes = body.join db.using_statement(Data.table.insert())(stmt => { stmt.string(1) = session_name stmt.string(2) = theory_name stmt.string(3) = name stmt.bool(4) = compressed - stmt.bytes(5) = body + stmt.bytes(5) = bytes stmt.execute() }) } } + def make_entry(session_name: String, args: Markup.Export.Args, body: Bytes): Entry = + { + Entry(session_name, args.theory_name, args.name, args.compress, + if (args.compress) Future.fork(body.compress()) else Future.value(body)) + } + def read_entry(db: SQL.Database, session_name: String, theory_name: String, name: String): Entry = { val select = @@ -69,9 +77,9 @@ if (res.next()) { val compressed = res.bool(Data.compressed) val body = res.bytes(Data.body) - Entry(session_name, theory_name, name, compressed, body) + Entry(session_name, theory_name, name, compressed, Future.value(body)) } - else error(Entry(session_name, theory_name, name, false, Bytes.empty).message("Bad export")) + else error(message("Bad export", theory_name, name)) }) } @@ -87,27 +95,21 @@ private val export_errors = Synchronized[List[String]](Nil) private val consumer = - Consumer_Thread.fork(name = "export")(consume = (future: Future[Entry]) => + Consumer_Thread.fork(name = "export")(consume = (entry: Entry) => { - val entry = future.join - + entry.body.join db.transaction { if (read_names(db, entry.session_name, entry.theory_name).contains(entry.name)) { - export_errors.change(errs => entry.message("Duplicate export") :: errs) + val err = message("Duplicate export", entry.theory_name, entry.name) + export_errors.change(errs => err :: errs) } else entry.write(db) } true }) - def apply(session_name: String, args: Markup.Export.Args, body: Bytes) - { - consumer.send( - if (args.compress) - Future.fork(Entry(session_name, args.theory_name, args.name, true, body.compress())) - else - Future.value(Entry(session_name, args.theory_name, args.name, false, body))) - } + def apply(session_name: String, args: Markup.Export.Args, body: Bytes): Unit = + consumer.send(make_entry(session_name, args, body)) def shutdown(close: Boolean = false): List[String] = { diff -r bdbf759ddbac -r 6a63a4ce756b src/Pure/Thy/thy_resources.scala --- a/src/Pure/Thy/thy_resources.scala Tue May 08 12:16:10 2018 +0200 +++ b/src/Pure/Thy/thy_resources.scala Tue May 08 15:06:19 2018 +0200 @@ -72,6 +72,16 @@ (_, tree) <- state.command_results(version, command).iterator } yield (tree, pos)).toList } + + def exports(node_name: Document.Node.Name): List[Export.Entry] = + { + val node = version.nodes(node_name) + Command.Exports.merge( + for { + command <- node.commands.iterator + st <- state.command_states(version, command).iterator + } yield st.exports).iterator.map(_._2).toList + } } class Session private[Thy_Resources]( diff -r bdbf759ddbac -r 6a63a4ce756b src/Pure/Tools/server_commands.scala --- a/src/Pure/Tools/server_commands.scala Tue May 08 12:16:10 2018 +0200 +++ b/src/Pure/Tools/server_commands.scala Tue May 08 15:06:19 2018 +0200 @@ -212,7 +212,13 @@ ("messages" -> (for { (tree, pos) <- result.messages(name) if Protocol.is_exported(tree) - } yield output_message(tree, pos))))) + } yield output_message(tree, pos))) + + ("exports" -> + (for { entry <- result.exports(name) } + yield { + val (base64, body) = entry.body.join.maybe_base64 + JSON.Object("name" -> entry.name, "base64" -> base64, "body" -> body) + })))) (result_json, result) }