(*
* 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