--- a/NEWS Sun Aug 06 11:10:22 2017 +0200
+++ b/NEWS Sun Aug 06 20:41:27 2017 +0200
@@ -116,6 +116,11 @@
*** HOL ***
+* Command and antiquotation "value" with modified default strategy:
+terms without free variables are always evaluated using plain evaluation
+only, with no fallback on normalization by evaluation.
+Minor INCOMPATIBILITY.
+
* Notions of squarefreeness, n-th powers, and prime powers in
HOL-Computational_Algebra and HOL-Number_Theory.
--- a/src/HOL/Tools/value_command.ML Sun Aug 06 11:10:22 2017 +0200
+++ b/src/HOL/Tools/value_command.ML Sun Aug 06 20:41:27 2017 +0200
@@ -17,9 +17,7 @@
fun default_value ctxt t =
if null (Term.add_frees t [])
- then case try (Code_Evaluation.dynamic_value_strict ctxt) t of
- SOME t' => t'
- | NONE => Nbe.dynamic_value ctxt t
+ then Code_Evaluation.dynamic_value_strict ctxt t
else Nbe.dynamic_value ctxt t;
structure Evaluator = Theory_Data
--- a/src/HOL/ex/Adhoc_Overloading_Examples.thy Sun Aug 06 11:10:22 2017 +0200
+++ b/src/HOL/ex/Adhoc_Overloading_Examples.thy Sun Aug 06 20:41:27 2017 +0200
@@ -38,7 +38,7 @@
adhoc_overloading
vars term_vars
-value "vars (Fun ''f'' [Var 0, Var 1])"
+value [nbe] "vars (Fun ''f'' [Var 0, Var 1])"
fun rule_vars :: "('a, 'b) term \<times> ('a, 'b) term \<Rightarrow> 'b set" where
"rule_vars (l, r) = vars l \<union> vars r"
@@ -46,7 +46,7 @@
adhoc_overloading
vars rule_vars
-value "vars (Var 1, Var 0)"
+value [nbe] "vars (Var 1, Var 0)"
definition trs_vars :: "(('a, 'b) term \<times> ('a, 'b) term) set \<Rightarrow> 'b set" where
"trs_vars R = \<Union>(rule_vars ` R)"
@@ -54,7 +54,7 @@
adhoc_overloading
vars trs_vars
-value "vars {(Var 1, Var 0)}"
+value [nbe] "vars {(Var 1, Var 0)}"
text \<open>Sometimes it is necessary to add explicit type constraints
before a variant can be determined.\<close>
--- a/src/HOL/ex/Normalization_by_Evaluation.thy Sun Aug 06 11:10:22 2017 +0200
+++ b/src/HOL/ex/Normalization_by_Evaluation.thy Sun Aug 06 20:41:27 2017 +0200
@@ -68,20 +68,20 @@
lemma "map (%f. f True) ([id, g, Not] @ fs) = [True, g True, False] @ map (%f. f True) fs"
by normalization rule
lemma "rev [a, b, c] = [c, b, a]" by normalization
-value "rev (a#b#cs) = rev cs @ [b, a]"
-value "map (%F. F [a,b,c::'x]) (map map [f,g,h])"
-value "map (%F. F ([a,b,c] @ ds)) (map map ([f,g,h]@fs))"
-value "map (%F. F [Z,S Z,S(S Z)]) (map map [S,add (S Z),mul (S(S Z)),id])"
+value [nbe] "rev (a#b#cs) = rev cs @ [b, a]"
+value [nbe] "map (%F. F [a,b,c::'x]) (map map [f,g,h])"
+value [nbe] "map (%F. F ([a,b,c] @ ds)) (map map ([f,g,h]@fs))"
+value [nbe] "map (%F. F [Z,S Z,S(S Z)]) (map map [S,add (S Z),mul (S(S Z)),id])"
lemma "map (%x. case x of None \<Rightarrow> False | Some y \<Rightarrow> True) [None, Some ()] = [False, True]"
by normalization
-value "case xs of [] \<Rightarrow> True | x#xs \<Rightarrow> False"
-value "map (%x. case x of None \<Rightarrow> False | Some y \<Rightarrow> True) xs = P"
+value [nbe] "case xs of [] \<Rightarrow> True | x#xs \<Rightarrow> False"
+value [nbe] "map (%x. case x of None \<Rightarrow> False | Some y \<Rightarrow> True) xs = P"
lemma "let x = y in [x, x] = [y, y]" by normalization
lemma "Let y (%x. [x,x]) = [y, y]" by normalization
-value "case n of Z \<Rightarrow> True | S x \<Rightarrow> False"
+value [nbe] "case n of Z \<Rightarrow> True | S x \<Rightarrow> False"
lemma "(%(x,y). add x y) (S z,S z) = S (add z (S z))" by normalization
-value "filter (%x. x) ([True,False,x]@xs)"
-value "filter Not ([True,False,x]@xs)"
+value [nbe] "filter (%x. x) ([True,False,x]@xs)"
+value [nbe] "filter Not ([True,False,x]@xs)"
lemma "[x,y,z] @ [a,b,c] = [x, y, z, a, b, c]" by normalization
lemma "(%(xs, ys). xs @ ys) ([a, b, c], [d, e, f]) = [a, b, c, d, e, f]" by normalization
@@ -106,7 +106,7 @@
lemma "[Suc 0, 0] = [Suc 0, 0]" by normalization
lemma "max (Suc 0) 0 = Suc 0" by normalization
lemma "(42::rat) / 1704 = 1 / 284 + 3 / 142" by normalization
-value "Suc 0 \<in> set ms"
+value [nbe] "Suc 0 \<in> set ms"
(* non-left-linear patterns, equality by extensionality *)
@@ -115,13 +115,13 @@
lemma "(f o g) x = f (g x)" by normalization
lemma "(f o id) x = f x" by normalization
lemma "(id :: bool \<Rightarrow> bool) = id" by normalization
-value "(\<lambda>x. x)"
+value [nbe] "(\<lambda>x. x)"
(* Church numerals: *)
-value "(%m n f x. m f (n f x)) (%f x. f(f(f(x)))) (%f x. f(f(f(x))))"
-value "(%m n f x. m (n f) x) (%f x. f(f(f(x)))) (%f x. f(f(f(x))))"
-value "(%m n. n m) (%f x. f(f(f(x)))) (%f x. f(f(f(x))))"
+value [nbe] "(%m n f x. m f (n f x)) (%f x. f(f(f(x)))) (%f x. f(f(f(x))))"
+value [nbe] "(%m n f x. m (n f) x) (%f x. f(f(f(x)))) (%f x. f(f(f(x))))"
+value [nbe] "(%m n. n m) (%f x. f(f(f(x)))) (%f x. f(f(f(x))))"
(* handling of type classes in connection with equality *)
--- a/src/HOL/ex/Transitive_Closure_Table_Ex.thy Sun Aug 06 11:10:22 2017 +0200
+++ b/src/HOL/ex/Transitive_Closure_Table_Ex.thy Sun Aug 06 20:41:27 2017 +0200
@@ -24,7 +24,7 @@
values "{x. test\<^sup>*\<^sup>* A x}"
values "{x. test\<^sup>*\<^sup>* x C}"
-value "test\<^sup>*\<^sup>* A C"
-value "test\<^sup>*\<^sup>* C A"
+value [nbe] "test\<^sup>*\<^sup>* A C"
+value [nbe] "test\<^sup>*\<^sup>* C A"
end
--- a/src/Pure/System/isabelle_tool.scala Sun Aug 06 11:10:22 2017 +0200
+++ b/src/Pure/System/isabelle_tool.scala Sun Aug 06 20:41:27 2017 +0200
@@ -115,6 +115,7 @@
Options.isabelle_tool,
Profiling_Report.isabelle_tool,
Remote_DMG.isabelle_tool,
+ Server.isabelle_tool,
Update_Cartouches.isabelle_tool,
Update_Header.isabelle_tool,
Update_Then.isabelle_tool,
--- a/src/Pure/System/system_channel.scala Sun Aug 06 11:10:22 2017 +0200
+++ b/src/Pure/System/system_channel.scala Sun Aug 06 20:41:27 2017 +0200
@@ -18,7 +18,7 @@
class System_Channel private
{
- private val server = new ServerSocket(0, 2, InetAddress.getByName("127.0.0.1"))
+ private val server = new ServerSocket(0, 50, InetAddress.getByName("127.0.0.1"))
val server_name: String = "127.0.0.1:" + server.getLocalPort
override def toString: String = server_name
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/server.scala Sun Aug 06 20:41:27 2017 +0200
@@ -0,0 +1,180 @@
+/* Title: Pure/Tools/server.scala
+ Author: Makarius
+
+Resident Isabelle servers.
+*/
+
+package isabelle
+
+
+import java.io.{BufferedReader, BufferedWriter, InputStreamReader, OutputStreamWriter,
+ IOException}
+import java.net.{Socket, ServerSocket, InetAddress}
+
+
+object Server
+{
+ /* per-user servers */
+
+ object Data
+ {
+ val database = Path.explode("$ISABELLE_HOME_USER/servers.db")
+
+ val name = SQL.Column.string("name", primary_key = true)
+ val port = SQL.Column.int("port")
+ val password = SQL.Column.string("password")
+ val table = SQL.Table("isabelle_servers", List(name, port, password))
+
+ sealed case class Entry(name: String, port: Int, password: String)
+ {
+ def print: String =
+ "server " + quote(name) + " = 127.0.0.1:" + port + " (password " + quote(password) + ")"
+
+ def active: Boolean =
+ try { (new Socket(InetAddress.getByName("127.0.0.1"), port)).close; true }
+ catch { case _: IOException => false }
+ }
+ }
+
+ def list(db: SQLite.Database): List[Data.Entry] =
+ if (db.tables.contains(Data.table.name)) {
+ db.using_statement(Data.table.select())(stmt =>
+ stmt.execute_query().iterator(res =>
+ Data.Entry(
+ res.string(Data.name),
+ res.int(Data.port),
+ res.string(Data.password))).toList.sortBy(_.name))
+ }
+ else Nil
+
+ def find(db: SQLite.Database, name: String): Option[Data.Entry] =
+ list(db).find(entry => entry.name == name && entry.active)
+
+ def start(name: String = "", port: Int = 0): (Data.Entry, Option[Thread]) =
+ {
+ using(SQLite.open_database(Data.database))(db =>
+ db.transaction {
+ find(db, name) match {
+ case Some(entry) => (entry, None)
+ case None =>
+ val server = new Server(port)
+ val entry = Data.Entry(name, server.port, server.password)
+
+ Isabelle_System.bash("chmod 600 " + File.bash_path(Data.database)).check
+ db.create_table(Data.table)
+ db.using_statement(Data.table.delete(Data.name.where_equal(name)))(_.execute)
+ db.using_statement(Data.table.insert())(stmt =>
+ {
+ stmt.string(1) = entry.name
+ stmt.int(2) = entry.port
+ stmt.string(3) = entry.password
+ stmt.execute()
+ })
+
+ (entry, Some(server.thread))
+ }
+ })
+ }
+
+ def stop(name: String = ""): Boolean =
+ {
+ using(SQLite.open_database(Data.database))(db =>
+ db.transaction {
+ find(db, name) match {
+ case Some(entry) =>
+ // FIXME shutdown server
+ db.using_statement(Data.table.delete(Data.name.where_equal(name)))(_.execute)
+ true
+ case None =>
+ false
+ }
+ })
+ }
+
+
+ /* Isabelle tool wrapper */
+
+ val isabelle_tool =
+ Isabelle_Tool("server", "manage resident Isabelle servers", args =>
+ {
+ var operation_list = false
+ var name = ""
+ var port = 0
+
+ val getopts =
+ Getopts("""
+Usage: isabelle server [OPTIONS]
+
+ Options are:
+ -L list servers
+ -n NAME explicit server name
+ -p PORT explicit server port
+
+ Manage resident Isabelle servers.
+""",
+ "L" -> (_ => operation_list = true),
+ "n:" -> (arg => name = arg),
+ "p:" -> (arg => port = Value.Int.parse(arg)))
+
+ val more_args = getopts(args)
+ if (more_args.nonEmpty) getopts.usage()
+
+ if (operation_list) {
+ for (entry <- using(SQLite.open_database(Data.database))(list(_)) if entry.active)
+ Console.println(entry.print)
+ }
+ else {
+ val (entry, thread) = start(name, port)
+ Console.println(entry.print)
+ thread.foreach(_.join)
+ }
+ })
+}
+
+class Server private(_port: Int)
+{
+ private val server_socket = new ServerSocket(_port, 50, InetAddress.getByName("127.0.0.1"))
+ def port: Int = server_socket.getLocalPort
+ def close { server_socket.close }
+
+ val password: String = Library.UUID()
+
+ private def handle_connection(socket: Socket)
+ {
+ val reader = new BufferedReader(new InputStreamReader(socket.getInputStream, UTF8.charset))
+ val writer = new BufferedWriter(new OutputStreamWriter(socket.getOutputStream, UTF8.charset))
+
+ def println(s: String)
+ {
+ writer.write(s)
+ writer.newLine()
+ writer.flush()
+ }
+
+ reader.readLine() match {
+ case null =>
+ case bad if bad != password => println("BAD PASSWORD")
+ case _ =>
+ var finished = false
+ while (!finished) {
+ reader.readLine() match {
+ case null => println("FINISHED"); finished = true
+ case line => println("ECHO " + line)
+ }
+ }
+ }
+ }
+
+ lazy val thread: Thread =
+ Standard_Thread.fork("server") {
+ var finished = false
+ while (!finished) {
+ Exn.capture(server_socket.accept) match {
+ case Exn.Res(socket) =>
+ Standard_Thread.fork("server_connection")
+ { try { handle_connection(socket) } finally { socket.close } }
+ case Exn.Exn(_) => finished = true
+ }
+ }
+ }
+}
--- a/src/Pure/build-jars Sun Aug 06 11:10:22 2017 +0200
+++ b/src/Pure/build-jars Sun Aug 06 20:41:27 2017 +0200
@@ -140,6 +140,7 @@
Tools/main.scala
Tools/print_operation.scala
Tools/profiling_report.scala
+ Tools/server.scala
Tools/simplifier_trace.scala
Tools/spell_checker.scala
Tools/task_statistics.scala
--- a/src/Pure/library.scala Sun Aug 06 11:10:22 2017 +0200
+++ b/src/Pure/library.scala Sun Aug 06 20:41:27 2017 +0200
@@ -259,4 +259,9 @@
def proper_list[A](list: List[A]): Option[List[A]] =
if (list == null || list.isEmpty) None else Some(list)
+
+
+ /* UUID */
+
+ def UUID(): String = java.util.UUID.randomUUID().toString
}
--- a/src/Tools/VSCode/src/grammar.scala Sun Aug 06 11:10:22 2017 +0200
+++ b/src/Tools/VSCode/src/grammar.scala Sun Aug 06 20:41:27 2017 +0200
@@ -9,8 +9,6 @@
import isabelle._
-import java.util.UUID
-
object Grammar
{
@@ -47,7 +45,7 @@
"name": "Isabelle",
"scopeName": "source.isabelle",
"fileTypes": ["thy"],
- "uuid": """ + JSON.Format(UUID.randomUUID().toString) + """,
+ "uuid": """ + JSON.Format(Library.UUID()) + """,
"repository": {
"comment": {
"patterns": [
--- a/src/Tools/jEdit/src/plugin.scala Sun Aug 06 11:10:22 2017 +0200
+++ b/src/Tools/jEdit/src/plugin.scala Sun Aug 06 20:41:27 2017 +0200
@@ -12,7 +12,6 @@
import javax.swing.JOptionPane
import java.io.{File => JFile}
-import java.util.UUID
import org.gjt.sp.jedit.{jEdit, EBMessage, EBPlugin, Buffer, View, Debug, PerspectiveManager}
import org.gjt.sp.jedit.textarea.JEditTextArea
@@ -398,7 +397,7 @@
/* HTTP server */
- val http_root: String = "/" + UUID.randomUUID().toString
+ val http_root: String = "/" + Library.UUID()
val http_server: HTTP.Server = HTTP.server(Document_Model.http_handlers(http_root))