(* * prooftree --- proof tree display for Proof General * * Copyright (C) 2011 - 2016 Hendrik Tews * * This file is part of "prooftree". * * "prooftree" is free software: you can redistribute it and/or * modify it under the terms of the GNU General Public License as * published by the Free Software Foundation, either version 3 of the * License, or (at your option) any later version. * * "prooftree" is distributed in the hope that it will be useful, * but WITHOUT ANY WARRANTY; without even the implied warranty of * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU * General Public License in file COPYING in this or one of the parent * directories for more details. * * You should have received a copy of the GNU General Public License * along with "prooftree". If not, see . * * $Id: input.ml,v 1.43 2016/01/23 12:57:14 tews Exp $ *) (** Reading commands from nonblocking stdin *) (***************************************************************************** *****************************************************************************) (** {2 Communition Protocol with Proof General} The communication protocol with Proof General is mostly one-way: Proof General sends display messages to Prooftree and Prooftree never requests information for the proof-tree display from Proof General. Prooftree sends a notification to Proof General when the proof-tree window is closed. It also sends proof commands to Proof General on request of the user. The communication protocol between Proof General and Prooftree is split into two parts: The display messages, which are sent from Proof General to Prooftree and the notification messages, which are sent from Prooftree to Proof General. {3 Display Messages} The protocol for the display messages is designed such that Prooftree always knows in advance how many bytes it has to read until the end of a message. All display messages consist of {ul {- a first line of exactly 16 bytes (including the new line) of the form "second line 157\n", where the number is the length of the second line (including its final newline).} {- a second line containing the display command and the length of the additional data sections, if the command has data sections.} {- the data sections (if any), where the last character of each data sections is a newline.} } All data is UTF-8 encoded. Some data sections have a prover specific format. Currently, [prooftree] only supports Coq. In the following list of commands, ``%d'' stands for a positive integer and %s for a string which contains no white space. ``\{cheated | not-cheated\}'' denotes the alternative of either ``cheated'' or ``not-cheated''. An integer following the keyword state is a state number. An integer following some xxx-bytes denotes the number of bytes of the next section, including the final newline of that section. A ``[ \ ]'' at the end of a line denotes line continuation without newline. Prooftree understands the following display commands in the following format. The first 16-byte line that preceeds every display-command line is ommitted in the following list. {ul {- {v configure for "PA" and protocol version NN v} Configure Prooftree for proof assistant PA and communication protocol version NN. If proof assistant PA or version NN is not supported, Prooftree displays an error message and exits. The name PA might contain arbitrary characters but no quotation mark ( '"' ). There must always be exectly one configure message, which must be the first message. } {- {v current-goals state %d current-sequent %s \ {cheated | not-cheated} {new-layer | current-layer} proof-name-bytes %d \ command-bytes %d sequent-text-bytes %d additional-id-bytes %d \ existential-bytes %d\n\ \n\ \n\ \n\ \n\ \n v} The [current-goals] command tells [prooftree] about a new proof state with a new set of open goals. This corresponds to either of the following cases: {ol {- The initial proof state of a newly started proof} {- A proof command has been applied to the old current sequent, yielding a new current sequent and possibly additional new open subgoals} {- The old current goal has been solved (by some proof command) and the new current sequent is one of the previously spawned subgoals} {- A new set of proof-tree root goal nodes is associated with the current proof. This happens for instance, when Coq transformes open existential variables into proof goals with the command [Grab Existential Variables].} } For case 1 or case 4 [new-layer] must be given. Otherwise, [current-layer] must be specified and [prooftree] decides with the help of its internal state whether case 2 or 3 applies. For the second and the third case, the set of open goals does not need to represent the total set of all open subgoals, but it must contain all newly spawned subgoals. The state number in the [current-goals] command is for undo. It is interpreted as the state that has been reached after processing the current command. [current-sequent %s] denotes the ID of the current sequent. The cheated flag tells [prooftree] whether the new proof state was obtained by a cheating command such as [admit] or [sorry]. The data sections are : {ol {- Full name of the proof} {- The proof command that yielded this proof state} {- Text of the current sequent} {- ID's of additionally open sequents (as space separated list of strings)} {- Prover specific information about existential variables.} } The second data section is ignored for initial proof states. The text of newly created additional goals other then the current goal is expected to arrive separately with an [update-sequent] command. } {- {v update-sequent state %d sequent %s proof-name-bytes %d \ sequent-text-bytes %d\n\ \n\ \n v} The update sequent command updates the text of some known sequent. Such updates are necessary for newly spawned subgoals. But also when existential variables get instantiated. The state number is for undo and the sequent ID denotes the sequent to update. The data sections are: {ol {- Full name of the proof} {- new sequent text} } } {- {v switch-goal state %d sequent %s proof-name-bytes %d\n \n v} Switch goal tells [proftree] that the current goal has changed without changing or solving the old current goal. The state number is for undo and the only data section is: {ol {- Full name of the proof} } } {- {v branch-finished state %d {cheated | not-cheated} \ proof-name-bytes %d command-bytes %d existential-bytes %d\n\ \n\ \n\ \n v} [branch-finished] tells [prooftree] the last proof command that closed the current branch. If there are still open subgoals, the proof will hopefully continue with one of them, which is not yet known. The cheated flag tells [prooftree] whether the new proof state was obtained by a cheating command such as [admit] or [sorry]. The data sections are : {ol {- Full name of the proof} {- The last proof command} {- Prover specific information about existential variables.} } } {- {v proof-complete state %d proof-name-bytes %d\n\ \n v} [proof-complete] tells Prooftree that the current proof has been completed and will further not be updated. The only data section is: {ol {- Full name of the proof} } } {- {v undo-to state %d\n v} The state number here is not for undo, it is the undo-state. Undo tells [prooftree] to change the display to the state before the first command with a state strictly greater than [undo-state] has been processed. } {- {v quit-proof proof-name-bytes %d\n\ \n v} Quit closes the window for the indicated proof. Cloned windows are not closed. The only data section is: {ol {- Full name of the proof whoose window should be delected} } } } {3 Notification Messages} The notification messages are sent from Prooftree to Proof General as a consequence of certain user interactions. There are 3 different notification messages: for stopping the proof-tree display, for undo and for sending proof scripts. All notification messages are preceeded with a newline and the string [emacs exec:], followed by a space, for easy recognition in Proof General. The remaining part of the messages have the following format. {ul {- {v stop-displaying v} Prooftree sends this message to Proof General when the user closed the proof-tree display of a proof currently under development. Proof General then stops sending display commands for that proof. } {- {v undo %d v} Prooftree sends the undo message, when the user selected an undo for a certain sequent from the context menu. The integer is the undo state number of the proof command child node of the selected sequent. } {- {v insert-proof-script %d\n