merged
authorpaulson
Sun, 06 Aug 2017 20:41:27 +0200
changeset 66357 3817ee41236d
parent 66354 8bf96de50193 (diff)
parent 66356 a6c9d7206853 (current diff)
child 66358 fab9a53158f8
child 66359 8ed88442d7bb
merged
--- 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))