src/Pure/PIDE/prover.scala
author wenzelm
Sat, 25 Aug 2018 17:20:06 +0200
changeset 68805 57455c561849
parent 67835 c8e4ee2b5482
child 69572 09a6a7c04b45
permissions -rw-r--r--
clarified message;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
56385
76acce58aeab more general prover operations;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/PIDE/prover.scala
76acce58aeab more general prover operations;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
57923
cdae2467311d tuned comments;
wenzelm
parents: 57917
diff changeset
     3
    Options:    :folding=explicit:
56385
76acce58aeab more general prover operations;
wenzelm
parents:
diff changeset
     4
57923
cdae2467311d tuned comments;
wenzelm
parents: 57917
diff changeset
     5
Prover process wrapping.
56385
76acce58aeab more general prover operations;
wenzelm
parents:
diff changeset
     6
*/
76acce58aeab more general prover operations;
wenzelm
parents:
diff changeset
     7
76acce58aeab more general prover operations;
wenzelm
parents:
diff changeset
     8
package isabelle
76acce58aeab more general prover operations;
wenzelm
parents:
diff changeset
     9
76acce58aeab more general prover operations;
wenzelm
parents:
diff changeset
    10
67835
c8e4ee2b5482 tuned imports;
wenzelm
parents: 65345
diff changeset
    11
import java.io.{InputStream, OutputStream, BufferedOutputStream, IOException}
57915
448325de6e4f more abstract Prover.System_Process, which allows to bypass Isabelle_System.Managed_Process;
wenzelm
parents: 57906
diff changeset
    12
448325de6e4f more abstract Prover.System_Process, which allows to bypass Isabelle_System.Managed_Process;
wenzelm
parents: 57906
diff changeset
    13
56385
76acce58aeab more general prover operations;
wenzelm
parents:
diff changeset
    14
object Prover
76acce58aeab more general prover operations;
wenzelm
parents:
diff changeset
    15
{
76acce58aeab more general prover operations;
wenzelm
parents:
diff changeset
    16
  /* messages */
76acce58aeab more general prover operations;
wenzelm
parents:
diff changeset
    17
76acce58aeab more general prover operations;
wenzelm
parents:
diff changeset
    18
  sealed abstract class Message
62556
c115e69f457f more abstract Session.start, without prover command-line;
wenzelm
parents: 62310
diff changeset
    19
  type Receiver = Message => Unit
56385
76acce58aeab more general prover operations;
wenzelm
parents:
diff changeset
    20
56386
fe520afb8041 tuned signature -- pro forma;
wenzelm
parents: 56385
diff changeset
    21
  class Input(val name: String, val args: List[String]) extends Message
56385
76acce58aeab more general prover operations;
wenzelm
parents:
diff changeset
    22
  {
76acce58aeab more general prover operations;
wenzelm
parents:
diff changeset
    23
    override def toString: String =
76acce58aeab more general prover operations;
wenzelm
parents:
diff changeset
    24
      XML.Elem(Markup(Markup.PROVER_COMMAND, List((Markup.NAME, name))),
76acce58aeab more general prover operations;
wenzelm
parents:
diff changeset
    25
        args.map(s =>
76acce58aeab more general prover operations;
wenzelm
parents:
diff changeset
    26
          List(XML.Text("\n"), XML.elem(Markup.PROVER_ARG, YXML.parse_body(s)))).flatten).toString
76acce58aeab more general prover operations;
wenzelm
parents:
diff changeset
    27
  }
76acce58aeab more general prover operations;
wenzelm
parents:
diff changeset
    28
76acce58aeab more general prover operations;
wenzelm
parents:
diff changeset
    29
  class Output(val message: XML.Elem) extends Message
76acce58aeab more general prover operations;
wenzelm
parents:
diff changeset
    30
  {
76acce58aeab more general prover operations;
wenzelm
parents:
diff changeset
    31
    def kind: String = message.markup.name
76acce58aeab more general prover operations;
wenzelm
parents:
diff changeset
    32
    def properties: Properties.T = message.markup.properties
76acce58aeab more general prover operations;
wenzelm
parents:
diff changeset
    33
    def body: XML.Body = message.body
76acce58aeab more general prover operations;
wenzelm
parents:
diff changeset
    34
76acce58aeab more general prover operations;
wenzelm
parents:
diff changeset
    35
    def is_init = kind == Markup.INIT
76acce58aeab more general prover operations;
wenzelm
parents:
diff changeset
    36
    def is_exit = kind == Markup.EXIT
76acce58aeab more general prover operations;
wenzelm
parents:
diff changeset
    37
    def is_stdout = kind == Markup.STDOUT
76acce58aeab more general prover operations;
wenzelm
parents:
diff changeset
    38
    def is_stderr = kind == Markup.STDERR
76acce58aeab more general prover operations;
wenzelm
parents:
diff changeset
    39
    def is_system = kind == Markup.SYSTEM
76acce58aeab more general prover operations;
wenzelm
parents:
diff changeset
    40
    def is_status = kind == Markup.STATUS
76acce58aeab more general prover operations;
wenzelm
parents:
diff changeset
    41
    def is_report = kind == Markup.REPORT
76acce58aeab more general prover operations;
wenzelm
parents:
diff changeset
    42
    def is_syslog = is_init || is_exit || is_system || is_stderr
76acce58aeab more general prover operations;
wenzelm
parents:
diff changeset
    43
76acce58aeab more general prover operations;
wenzelm
parents:
diff changeset
    44
    override def toString: String =
76acce58aeab more general prover operations;
wenzelm
parents:
diff changeset
    45
    {
76acce58aeab more general prover operations;
wenzelm
parents:
diff changeset
    46
      val res =
76acce58aeab more general prover operations;
wenzelm
parents:
diff changeset
    47
        if (is_status || is_report) message.body.map(_.toString).mkString
76acce58aeab more general prover operations;
wenzelm
parents:
diff changeset
    48
        else Pretty.string_of(message.body)
76acce58aeab more general prover operations;
wenzelm
parents:
diff changeset
    49
      if (properties.isEmpty)
76acce58aeab more general prover operations;
wenzelm
parents:
diff changeset
    50
        kind.toString + " [[" + res + "]]"
76acce58aeab more general prover operations;
wenzelm
parents:
diff changeset
    51
      else
76acce58aeab more general prover operations;
wenzelm
parents:
diff changeset
    52
        kind.toString + " " +
76acce58aeab more general prover operations;
wenzelm
parents:
diff changeset
    53
          (for ((x, y) <- properties) yield x + "=" + y).mkString("{", ",", "}") + " [[" + res + "]]"
76acce58aeab more general prover operations;
wenzelm
parents:
diff changeset
    54
    }
76acce58aeab more general prover operations;
wenzelm
parents:
diff changeset
    55
  }
76acce58aeab more general prover operations;
wenzelm
parents:
diff changeset
    56
76acce58aeab more general prover operations;
wenzelm
parents:
diff changeset
    57
  class Protocol_Output(props: Properties.T, val bytes: Bytes)
76acce58aeab more general prover operations;
wenzelm
parents:
diff changeset
    58
    extends Output(XML.Elem(Markup(Markup.PROTOCOL, props), Nil))
76acce58aeab more general prover operations;
wenzelm
parents:
diff changeset
    59
  {
65309
3024fcd5a7f4 proper message text (see also fa62e095d8f1);
wenzelm
parents: 65218
diff changeset
    60
    lazy val text: String = bytes.text
56385
76acce58aeab more general prover operations;
wenzelm
parents:
diff changeset
    61
  }
76acce58aeab more general prover operations;
wenzelm
parents:
diff changeset
    62
}
76acce58aeab more general prover operations;
wenzelm
parents:
diff changeset
    63
56393
22f533e6a049 more abstract Prover.Syntax, as proposed by Carst Tankink;
wenzelm
parents: 56387
diff changeset
    64
65345
2fdd4431b30e clarified YXML vs. symbol encoding: operate on whole message;
wenzelm
parents: 65317
diff changeset
    65
class Prover(
62556
c115e69f457f more abstract Session.start, without prover command-line;
wenzelm
parents: 62310
diff changeset
    66
  receiver: Prover.Receiver,
65218
102b8e092860 more explicit Session.xml_cache;
wenzelm
parents: 64004
diff changeset
    67
  xml_cache: XML.Cache,
65316
c0fb8405416c simplified signature (despite 448325de6e4f);
wenzelm
parents: 65309
diff changeset
    68
  channel: System_Channel,
c0fb8405416c simplified signature (despite 448325de6e4f);
wenzelm
parents: 65309
diff changeset
    69
  process: Bash.Process) extends Protocol
56387
d92eb5c3960d more general prover operations;
wenzelm
parents: 56386
diff changeset
    70
{
57923
cdae2467311d tuned comments;
wenzelm
parents: 57917
diff changeset
    71
  /** receiver output **/
57916
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
    72
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
    73
  private def system_output(text: String)
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
    74
  {
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
    75
    receiver(new Prover.Output(XML.Elem(Markup(Markup.SYSTEM, Nil), List(XML.Text(text)))))
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
    76
  }
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
    77
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
    78
  private def protocol_output(props: Properties.T, bytes: Bytes)
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
    79
  {
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
    80
    receiver(new Prover.Protocol_Output(props, bytes))
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
    81
  }
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
    82
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
    83
  private def output(kind: String, props: Properties.T, body: XML.Body)
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
    84
  {
65316
c0fb8405416c simplified signature (despite 448325de6e4f);
wenzelm
parents: 65309
diff changeset
    85
    if (kind == Markup.INIT) channel.accepted()
56387
d92eb5c3960d more general prover operations;
wenzelm
parents: 56386
diff changeset
    86
59713
6da3efec20ca clarified modules;
wenzelm
parents: 59702
diff changeset
    87
    val main = XML.Elem(Markup(kind, props), Protocol_Message.clean_reports(body))
6da3efec20ca clarified modules;
wenzelm
parents: 59702
diff changeset
    88
    val reports = Protocol_Message.reports(props, body)
57916
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
    89
    for (msg <- main :: reports) receiver(new Prover.Output(xml_cache.elem(msg)))
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
    90
  }
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
    91
65317
b9f5cd845616 more informative session result;
wenzelm
parents: 65316
diff changeset
    92
  private def exit_message(result: Process_Result)
57916
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
    93
  {
65317
b9f5cd845616 more informative session result;
wenzelm
parents: 65316
diff changeset
    94
    output(Markup.EXIT, Markup.Process_Result(result),
b9f5cd845616 more informative session result;
wenzelm
parents: 65316
diff changeset
    95
      List(XML.Text("Return code: " + result.rc.toString)))
57916
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
    96
  }
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
    97
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
    98
56387
d92eb5c3960d more general prover operations;
wenzelm
parents: 56386
diff changeset
    99
57916
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   100
  /** process manager **/
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   101
65317
b9f5cd845616 more informative session result;
wenzelm
parents: 65316
diff changeset
   102
  private val process_result: Future[Process_Result] =
b9f5cd845616 more informative session result;
wenzelm
parents: 65316
diff changeset
   103
    Future.thread("process_result") {
b9f5cd845616 more informative session result;
wenzelm
parents: 65316
diff changeset
   104
      val rc = process.join
b9f5cd845616 more informative session result;
wenzelm
parents: 65316
diff changeset
   105
      val timing = process.get_timing
b9f5cd845616 more informative session result;
wenzelm
parents: 65316
diff changeset
   106
      Process_Result(rc, timing = timing)
b9f5cd845616 more informative session result;
wenzelm
parents: 65316
diff changeset
   107
    }
57916
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   108
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   109
  private def terminate_process()
56387
d92eb5c3960d more general prover operations;
wenzelm
parents: 56386
diff changeset
   110
  {
65316
c0fb8405416c simplified signature (despite 448325de6e4f);
wenzelm
parents: 65309
diff changeset
   111
    try { process.terminate }
57916
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   112
    catch {
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   113
      case exn @ ERROR(_) => system_output("Failed to terminate prover process: " + exn.getMessage)
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   114
    }
56387
d92eb5c3960d more general prover operations;
wenzelm
parents: 56386
diff changeset
   115
  }
d92eb5c3960d more general prover operations;
wenzelm
parents: 56386
diff changeset
   116
61556
0d4ee4168e41 clarified modules;
wenzelm
parents: 60215
diff changeset
   117
  private val process_manager = Standard_Thread.fork("process_manager")
57916
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   118
  {
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   119
    val (startup_failed, startup_errors) =
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   120
    {
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   121
      var finished: Option[Boolean] = None
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   122
      val result = new StringBuilder(100)
65316
c0fb8405416c simplified signature (despite 448325de6e4f);
wenzelm
parents: 65309
diff changeset
   123
      while (finished.isEmpty && (process.stderr.ready || !process_result.is_finished)) {
c0fb8405416c simplified signature (despite 448325de6e4f);
wenzelm
parents: 65309
diff changeset
   124
        while (finished.isEmpty && process.stderr.ready) {
57916
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   125
          try {
65316
c0fb8405416c simplified signature (despite 448325de6e4f);
wenzelm
parents: 65309
diff changeset
   126
            val c = process.stderr.read
57916
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   127
            if (c == 2) finished = Some(true)
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   128
            else result += c.toChar
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   129
          }
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   130
          catch { case _: IOException => finished = Some(false) }
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   131
        }
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   132
        Thread.sleep(10)
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   133
      }
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   134
      (finished.isEmpty || !finished.get, result.toString.trim)
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   135
    }
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   136
    if (startup_errors != "") system_output(startup_errors)
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   137
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   138
    if (startup_failed) {
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   139
      terminate_process()
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   140
      process_result.join
65317
b9f5cd845616 more informative session result;
wenzelm
parents: 65316
diff changeset
   141
      exit_message(Process_Result(127))
57916
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   142
    }
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   143
    else {
65316
c0fb8405416c simplified signature (despite 448325de6e4f);
wenzelm
parents: 65309
diff changeset
   144
      val (command_stream, message_stream) = channel.rendezvous()
57916
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   145
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   146
      command_input_init(command_stream)
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   147
      val stdout = physical_output(false)
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   148
      val stderr = physical_output(true)
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   149
      val message = message_output(message_stream)
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   150
65317
b9f5cd845616 more informative session result;
wenzelm
parents: 65316
diff changeset
   151
      val result = process_result.join
57916
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   152
      system_output("process terminated")
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   153
      command_input_close()
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   154
      for (thread <- List(stdout, stderr, message)) thread.join
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   155
      system_output("process_manager terminated")
65317
b9f5cd845616 more informative session result;
wenzelm
parents: 65316
diff changeset
   156
      exit_message(result)
57916
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   157
    }
65316
c0fb8405416c simplified signature (despite 448325de6e4f);
wenzelm
parents: 65309
diff changeset
   158
    channel.accepted()
57916
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   159
  }
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   160
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   161
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   162
  /* management methods */
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   163
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   164
  def join() { process_manager.join() }
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   165
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   166
  def terminate()
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   167
  {
62310
ab836dc7410e more gentle termination (like Bash.multi_kill without signal) to give prover a chance to conclude;
wenzelm
parents: 62307
diff changeset
   168
    system_output("Terminating prover process")
57916
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   169
    command_input_close()
62310
ab836dc7410e more gentle termination (like Bash.multi_kill without signal) to give prover a chance to conclude;
wenzelm
parents: 62307
diff changeset
   170
ab836dc7410e more gentle termination (like Bash.multi_kill without signal) to give prover a chance to conclude;
wenzelm
parents: 62307
diff changeset
   171
    var count = 10
ab836dc7410e more gentle termination (like Bash.multi_kill without signal) to give prover a chance to conclude;
wenzelm
parents: 62307
diff changeset
   172
    while (!process_result.is_finished && count > 0) {
ab836dc7410e more gentle termination (like Bash.multi_kill without signal) to give prover a chance to conclude;
wenzelm
parents: 62307
diff changeset
   173
      Thread.sleep(100)
ab836dc7410e more gentle termination (like Bash.multi_kill without signal) to give prover a chance to conclude;
wenzelm
parents: 62307
diff changeset
   174
      count -= 1
ab836dc7410e more gentle termination (like Bash.multi_kill without signal) to give prover a chance to conclude;
wenzelm
parents: 62307
diff changeset
   175
    }
ab836dc7410e more gentle termination (like Bash.multi_kill without signal) to give prover a chance to conclude;
wenzelm
parents: 62307
diff changeset
   176
    if (!process_result.is_finished) terminate_process()
57916
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   177
  }
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   178
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   179
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   180
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   181
  /** process streams **/
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   182
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   183
  /* command input */
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   184
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   185
  private var command_input: Option[Consumer_Thread[List[Bytes]]] = None
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   186
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   187
  private def command_input_close(): Unit = command_input.foreach(_.shutdown)
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   188
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   189
  private def command_input_init(raw_stream: OutputStream)
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   190
  {
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   191
    val name = "command_input"
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   192
    val stream = new BufferedOutputStream(raw_stream)
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   193
    command_input =
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   194
      Some(
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   195
        Consumer_Thread.fork(name)(
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   196
          consume =
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   197
            {
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   198
              case chunks =>
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   199
                try {
64004
b4ece7a3f2ca clarified stream operations;
wenzelm
parents: 63584
diff changeset
   200
                  Bytes(chunks.map(_.length).mkString("", ",", "\n")).write_stream(stream)
b4ece7a3f2ca clarified stream operations;
wenzelm
parents: 63584
diff changeset
   201
                  chunks.foreach(_.write_stream(stream))
57916
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   202
                  stream.flush
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   203
                  true
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   204
                }
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   205
                catch { case e: IOException => system_output(name + ": " + e.getMessage); false }
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   206
            },
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   207
          finish = { case () => stream.close; system_output(name + " terminated") }
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   208
        )
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   209
      )
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   210
  }
56387
d92eb5c3960d more general prover operations;
wenzelm
parents: 56386
diff changeset
   211
d92eb5c3960d more general prover operations;
wenzelm
parents: 56386
diff changeset
   212
57916
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   213
  /* physical output */
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   214
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   215
  private def physical_output(err: Boolean): Thread =
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   216
  {
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   217
    val (name, reader, markup) =
65316
c0fb8405416c simplified signature (despite 448325de6e4f);
wenzelm
parents: 65309
diff changeset
   218
      if (err) ("standard_error", process.stderr, Markup.STDERR)
c0fb8405416c simplified signature (despite 448325de6e4f);
wenzelm
parents: 65309
diff changeset
   219
      else ("standard_output", process.stdout, Markup.STDOUT)
56387
d92eb5c3960d more general prover operations;
wenzelm
parents: 56386
diff changeset
   220
61556
0d4ee4168e41 clarified modules;
wenzelm
parents: 60215
diff changeset
   221
    Standard_Thread.fork(name) {
57916
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   222
      try {
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   223
        var result = new StringBuilder(100)
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   224
        var finished = false
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   225
        while (!finished) {
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   226
          //{{{
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   227
          var c = -1
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   228
          var done = false
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   229
          while (!done && (result.length == 0 || reader.ready)) {
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   230
            c = reader.read
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   231
            if (c >= 0) result.append(c.asInstanceOf[Char])
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   232
            else done = true
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   233
          }
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   234
          if (result.length > 0) {
65345
2fdd4431b30e clarified YXML vs. symbol encoding: operate on whole message;
wenzelm
parents: 65317
diff changeset
   235
            output(markup, Nil, List(XML.Text(Symbol.decode(result.toString))))
57916
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   236
            result.length = 0
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   237
          }
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   238
          else {
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   239
            reader.close
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   240
            finished = true
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   241
          }
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   242
          //}}}
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   243
        }
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   244
      }
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   245
      catch { case e: IOException => system_output(name + ": " + e.getMessage) }
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   246
      system_output(name + " terminated")
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   247
    }
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   248
  }
56387
d92eb5c3960d more general prover operations;
wenzelm
parents: 56386
diff changeset
   249
d92eb5c3960d more general prover operations;
wenzelm
parents: 56386
diff changeset
   250
57916
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   251
  /* message output */
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   252
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   253
  private def message_output(stream: InputStream): Thread =
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   254
  {
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   255
    class EOF extends Exception
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   256
    class Protocol_Error(msg: String) extends Exception(msg)
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   257
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   258
    val name = "message_output"
61556
0d4ee4168e41 clarified modules;
wenzelm
parents: 60215
diff changeset
   259
    Standard_Thread.fork(name) {
57916
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   260
      val default_buffer = new Array[Byte](65536)
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   261
      var c = -1
56387
d92eb5c3960d more general prover operations;
wenzelm
parents: 56386
diff changeset
   262
57916
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   263
      def read_int(): Int =
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   264
      //{{{
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   265
      {
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   266
        var n = 0
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   267
        c = stream.read
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   268
        if (c == -1) throw new EOF
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   269
        while (48 <= c && c <= 57) {
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   270
          n = 10 * n + (c - 48)
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   271
          c = stream.read
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   272
        }
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   273
        if (c != 10)
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   274
          throw new Protocol_Error("malformed header: expected integer followed by newline")
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   275
        else n
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   276
      }
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   277
      //}}}
56387
d92eb5c3960d more general prover operations;
wenzelm
parents: 56386
diff changeset
   278
57916
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   279
      def read_chunk_bytes(): (Array[Byte], Int) =
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   280
      //{{{
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   281
      {
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   282
        val n = read_int()
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   283
        val buf =
60215
5fb4990dfc73 misc tuning, based on warnings by IntelliJ IDEA;
wenzelm
parents: 59735
diff changeset
   284
          if (n <= default_buffer.length) default_buffer
57916
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   285
          else new Array[Byte](n)
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   286
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   287
        var i = 0
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   288
        var m = 0
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   289
        do {
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   290
          m = stream.read(buf, i, n - i)
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   291
          if (m != -1) i += m
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   292
        }
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   293
        while (m != -1 && n > i)
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   294
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   295
        if (i != n)
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   296
          throw new Protocol_Error("bad chunk (unexpected EOF after " + i + " of " + n + " bytes)")
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   297
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   298
        (buf, n)
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   299
      }
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   300
      //}}}
56387
d92eb5c3960d more general prover operations;
wenzelm
parents: 56386
diff changeset
   301
57916
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   302
      def read_chunk(): XML.Body =
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   303
      {
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   304
        val (buf, n) = read_chunk_bytes()
65345
2fdd4431b30e clarified YXML vs. symbol encoding: operate on whole message;
wenzelm
parents: 65317
diff changeset
   305
        YXML.parse_body_failsafe(UTF8.decode_chars(Symbol.decode, buf, 0, n))
57916
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   306
      }
56387
d92eb5c3960d more general prover operations;
wenzelm
parents: 56386
diff changeset
   307
57916
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   308
      try {
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   309
        do {
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   310
          try {
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   311
            val header = read_chunk()
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   312
            header match {
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   313
              case List(XML.Elem(Markup(name, props), Nil)) =>
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   314
                val kind = name.intern
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   315
                if (kind == Markup.PROTOCOL) {
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   316
                  val (buf, n) = read_chunk_bytes()
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   317
                  protocol_output(props, Bytes(buf, 0, n))
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   318
                }
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   319
                else {
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   320
                  val body = read_chunk()
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   321
                  output(kind, props, body)
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   322
                }
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   323
              case _ =>
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   324
                read_chunk()
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   325
                throw new Protocol_Error("bad header: " + header.toString)
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   326
            }
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   327
          }
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   328
          catch { case _: EOF => }
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   329
        }
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   330
        while (c != -1)
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   331
      }
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   332
      catch {
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   333
        case e: IOException => system_output("Cannot read message:\n" + e.getMessage)
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   334
        case e: Protocol_Error => system_output("Malformed message:\n" + e.getMessage)
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   335
      }
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   336
      stream.close
56387
d92eb5c3960d more general prover operations;
wenzelm
parents: 56386
diff changeset
   337
57916
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   338
      system_output(name + " terminated")
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   339
    }
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   340
  }
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   341
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   342
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   343
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   344
  /** protocol commands **/
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   345
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   346
  def protocol_command_bytes(name: String, args: Bytes*): Unit =
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   347
    command_input match {
68805
57455c561849 clarified message;
wenzelm
parents: 67835
diff changeset
   348
      case Some(thread) if thread.is_active => thread.send(Bytes(name) :: args.toList)
57455c561849 clarified message;
wenzelm
parents: 67835
diff changeset
   349
      case _ => error("Inactive prover input thread for command " + quote(name))
57916
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   350
    }
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   351
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   352
  def protocol_command(name: String, args: String*)
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   353
  {
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   354
    receiver(new Prover.Input(name, args.toList))
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   355
    protocol_command_bytes(name, args.map(Bytes(_)): _*)
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
   356
  }
56387
d92eb5c3960d more general prover operations;
wenzelm
parents: 56386
diff changeset
   357
}