PGIP

<?xml encoding="UTF-8"?>

<!--

RELAX NG Schema for PGIP, the Proof General Interface Protocol                   

Authors:  David Aspinall, LFCS, University of Edinburgh       
          Christoph Lueth, University of Bremen       

Version: $Id: pgip.rnc,v 1.28 2003/08/26 03:39:53 da Exp $    

Status:  Experimental.                                           
For additional commentary, see the Proof General Kit white paper,
available from http://www.proofgeneral.org/kit

Advertised version: 1.0

-->

<!ENTITY % pgml SYSTEM "pgml.dtd">
%pgml;

<!-- include PGML grammar -->

<!-- ========== PGIP MESSAGES ========== -->

<!-- change prover's working directory (or load path) for files -->

<!ENTITY % fileinfomsg "informfileloaded|informfileretracted">

<!-- ========== GENERAL PROVER OUTPUT/RESPONSES ========== -->

<!ENTITY % proveroutput "ready|cleardisplay|normalresponse|errorresponse
                         |scriptinsert|metainforesponse|parseresult
                         |unparseresult">

<!--  ========== INTERFACE CONFIGURATION ========== -->

<!ENTITY % kitconfig "usespgip|usespgml|pgmlconfig|proverinfo|hasprefs
                      |prefval|guiconfig|setids|addids|delids|menuadd
                      |menudel">

<!-- ========== THEORY/FILE HANDLING COMMANDS ========== -->

<!ENTITY % filecmd "opentheory|closetheory|retracttheory|openfile
                    |closefile|abortfile|loadfile|changecwd">

<!-- ========= PROOF CONTEXT/ETC COMMANDS =========== -->

<!ENTITY % proofctxt "askids|showid|setid|parsescript|unparsecmds
                      |showproofstate|showctxt|searchtheorems
                      |setlinewidth|viewdoc">

<!-- data values -->

<!-- ========== PROOF CONTROL COMMANDS ========== -->

<!ENTITY % proofcmd "opengoal|proofstep|undostep|closegoal|abortgoal
                     |giveupgoal|postponegoal|forget|restoregoal">

<!-- text is arg to "viewdoc" -->

<!-- ========== PROVER CONTROL ========== -->

<!ENTITY % provercontrol "proverinit|proverexit|startquiet|stopquiet">

<!-- information messages concerning  -->

<!--  ========== PROVER CONFIGURATION ========== -->

<!ENTITY % proverconfig "askpgip|askpgml|askconfig|askprefs|setpref
                         |getpref">

<!-- issue a file command -->

<!ENTITY % kitmsg "%kitconfig;|%proveroutput;|%fileinfomsg;">

<!-- for a message sent TO proof general -->

<!ENTITY % provermsg "%proverconfig;|%provercontrol;|%proofcmd;
                      |%proofctxt;|%filecmd;">

<!--
pgips is the type of a log between
two components.
-->

<!ELEMENT pgip (%provermsg;|%kitmsg;)>

<!-- or an interface message -->

<!ELEMENT pgips (pgip)+>

<!-- sequence number of this message -->

<!ENTITY % pgip_class "pa|pg">

<!ATTLIST pgip
  origin CDATA #IMPLIED
  id CDATA #REQUIRED
  class (%pgip_class;) #REQUIRED
  refseq CDATA #IMPLIED
  refid CDATA #IMPLIED
  seq CDATA #REQUIRED>

<!-- please tell me this preference value -->

<!ENTITY % name_attr "
  name CDATA #REQUIRED">

<!-- identifiers must be XML tokens -->

<!ENTITY % prefcat_attr "
  prefcategory CDATA #REQUIRED">

<!--
e.g. "expert", "internal", etc.
could be used for tabs in dialog
-->

<!ELEMENT askpgip EMPTY>

<!ELEMENT askpgml EMPTY>

<!ELEMENT askconfig EMPTY>

<!ELEMENT askprefs EMPTY>
<!ATTLIST askprefs
  prefcategory CDATA #IMPLIED>

<!ELEMENT setpref (#PCDATA)>
<!ATTLIST setpref
  %name_attr;
  prefcategory CDATA #IMPLIED>

<!ELEMENT getpref EMPTY>
<!ATTLIST getpref
  %name_attr;
  prefcategory CDATA #IMPLIED>

<!-- remove a menu entry -->

<!-- version reporting -->

<!ENTITY % version_attr "
  version CDATA #REQUIRED">

<!ELEMENT usespgml EMPTY>
<!ATTLIST usespgml
  %version_attr;>

<!ELEMENT usespgip EMPTY>
<!ATTLIST usespgip
  %version_attr;>

<!-- PGML configuration -->

<!ELEMENT pgmlconfig (%pgmlconfigure;)+>

<!--
Types for config settings: corresponding data values should conform
to representation for corresponding XML Schema 1.0 Datatypes.
(This representation is verbose but helps for error checking later)
-->

<!ENTITY % pgiptype "pgipbool|pgipint|pgipstring|pgipchoice">

<!ELEMENT pgipbool EMPTY>

<!ELEMENT pgipint EMPTY>
<!ATTLIST pgipint
  min CDATA #IMPLIED
  max CDATA #IMPLIED>

<!ENTITY % min_attr "
  min CDATA #REQUIRED">

<!ENTITY % max_attr "
  max CDATA #REQUIRED">

<!ELEMENT pgipstring EMPTY>

<!ELEMENT pgipchoice (pgipchoiceitem)+>

<!ELEMENT pgipchoiceitem (#PCDATA)>

<!ELEMENT icon (#PCDATA)>

<!-- image data for an icon -->

<!-- preferences -->

<!ENTITY % default_attr "
  default CDATA #REQUIRED">

<!ENTITY % descr_attr "
  descr CDATA #REQUIRED">

<!--
icons for preference recommended size: 32x32 
top level preferences: may be used in dialog for preference setting
object preferences: may be used as an "emblem" to decorate 
object icon (boolean preferences with default false, only)
-->

<!ELEMENT haspref (icon?,(%pgiptype;))>
<!ATTLIST haspref
  %name_attr;
  descr CDATA #IMPLIED
  default CDATA #IMPLIED>

<!ELEMENT hasprefs (haspref)*>
<!ATTLIST hasprefs
  prefcategory CDATA #IMPLIED>

<!ELEMENT prefval (#PCDATA)>
<!ATTLIST prefval
  %name_attr;>

<!-- menu items (incomplete) -->

<!ENTITY % path_attr "
  path CDATA #REQUIRED">

<!ELEMENT menuadd (#PCDATA)>
<!ATTLIST menuadd
  path CDATA #IMPLIED
  name CDATA #IMPLIED>

<!ELEMENT menudel (#PCDATA)>
<!ATTLIST menudel
  path CDATA #IMPLIED
  name CDATA #IMPLIED>

<!-- GUI configuration information: objects, types, and operations -->

<!ELEMENT guiconfig (objtype*,opn*)>

<!ELEMENT objtype (icon?,hasprefs?,contains*)>
<!ATTLIST objtype
  %name_attr;
  descr CDATA #IMPLIED>

<!ENTITY % objtype_attr "
  objtype CDATA #REQUIRED">

<!-- the name of an objtype -->

<!ELEMENT contains EMPTY>
<!ATTLIST contains
  %objtype_attr;>

<!-- source types: a space separated list -->

<!ENTITY % optrg "optrg?">

<!--  -->

<!ELEMENT opn (inputform?,opsrc,(%optrg;),opcmd)>
<!ATTLIST opn
  %name_attr;>

<!ELEMENT optrg (#PCDATA)>

<!ELEMENT opsrc (#PCDATA)>

<!-- single target type, empty for proofstate -->

<!ELEMENT opcmd (#PCDATA)>

<!-- prover command, with printf-style "%1"-args -->

<!-- interactive operations - require some input -->

<!ELEMENT inputform (field)+>

<!--
a field has a PGIP config type (int, string, bool, choice(c1...cn))
and a name; under that name, it will be substituted into the command
Ex. field name=number  opcmd="rtac %1 %number"
-->

<!ELEMENT field ((%pgiptype;),prompt)>
<!ATTLIST field
  %name_attr;>

<!ELEMENT prompt (#PCDATA)>

<!--
identifier tables: these list known items of particular objtype.
Might be used for completion or menu selection.
May have a nested structure (but objtypes do not).
-->

<!ELEMENT idtable (identifier|idtable)*>
<!ATTLIST idtable
  %objtype_attr;>

<!ELEMENT setids (idtable)>

<!-- (with an empty idtable, clear table) -->

<!ELEMENT addids (idtable)>

<!ELEMENT delids (idtable)>

<!ELEMENT identifier (#PCDATA)>

<!--
prover information: 
name, description, version, homepage, 
welcome message, docs available
-->

<!ELEMENT proverinfo (welcomemsg?,icon?,helpdoc*)>
<!ATTLIST proverinfo
  %name_attr;
  descr CDATA #IMPLIED
  version CDATA #IMPLIED
  url CDATA #IMPLIED>

<!ELEMENT welcomemsg (#PCDATA)>

<!ENTITY % url_attr "
  url CDATA #REQUIRED">

<!-- FIXME: schema for URL? -->

<!--
helpdoc: advertise availability of some documentation, given a canonical
name, textual description, and URL or viewdoc argument.

-->

<!ELEMENT helpdoc (#PCDATA)>
<!ATTLIST helpdoc
  %name_attr;
  %descr_attr;
  url CDATA #IMPLIED>

<!-- turn on normal proof state & message displays -->

<!ELEMENT proverinit EMPTY>

<!ELEMENT proverexit EMPTY>

<!-- exit prover -->

<!ELEMENT startquiet EMPTY>

<!ELEMENT stopquiet EMPTY>

<!-- result of a <unparsecmds> request (see later) -->

<!ELEMENT ready EMPTY>

<!ENTITY % displayarea "message|display">

<!-- the main display area (goals buffer) -->

<!ELEMENT cleardisplay EMPTY>
<!ATTLIST cleardisplay
  area (%displayarea;|all) #REQUIRED>

<!ENTITY % displaytext "(#PCDATA|pgml)*">

<!-- grammar for displayed text  -->

<!ELEMENT normalresponse %displaytext;>
<!ATTLIST normalresponse
  area (%displayarea;) #REQUIRED
  category CDATA #IMPLIED
  urgent (y) #IMPLIED>

<!ENTITY % fatality "nonfatal|fatal|panic">

<!-- degree of errors -->

<!ELEMENT errorresponse %displaytext;>
<!ATTLIST errorresponse
  fatality (%fatality;) #REQUIRED
  location CDATA #IMPLIED
  locationline CDATA #IMPLIED
  locationcolumn CDATA #IMPLIED>

<!ELEMENT scriptinsert (#PCDATA)>

<!-- metainformation is an extensible place to put system-specific information -->

<!ELEMENT value (#PCDATA)>
<!ATTLIST value
  name CDATA #IMPLIED>

<!-- generic value holder -->

<!ELEMENT metainforesponse (value)*>
<!ATTLIST metainforesponse
  infotype CDATA #REQUIRED>

<!-- re-open previously postponed proof, outdating dependent theorems -->

<!ENTITY % thmname_attr "
  thmname CDATA #REQUIRED">

<!-- theorem names -->

<!ENTITY % aname_attr "
  aname CDATA #REQUIRED">

<!-- anchors in proof text -->

<!ELEMENT opengoal (#PCDATA)>
<!ATTLIST opengoal
  %thmname_attr;>

<!-- text is theorem to be proved -->

<!ELEMENT proofstep (#PCDATA)>
<!ATTLIST proofstep
  aname CDATA #IMPLIED>

<!-- text is proof command -->

<!ELEMENT undostep EMPTY>

<!ELEMENT closegoal EMPTY>

<!ELEMENT abortgoal EMPTY>

<!ELEMENT giveupgoal EMPTY>

<!ELEMENT postponegoal EMPTY>

<!ELEMENT forget EMPTY>
<!ATTLIST forget
  thyname CDATA #IMPLIED
  aname CDATA #IMPLIED>

<!ELEMENT restoregoal EMPTY>
<!ATTLIST restoregoal
  %thmname_attr;>

<!-- request some on-line help (prover-specific arg) -->

<!ENTITY % thyname_attr "
  thyname CDATA #REQUIRED">

<!-- theory name -->

<!ELEMENT askids EMPTY>
<!ATTLIST askids
  thyname CDATA #IMPLIED
  %objtype_attr;>

<!ELEMENT showid EMPTY>
<!ATTLIST showid
  thyname CDATA #IMPLIED
  %objtype_attr;
  %name_attr;>

<!ELEMENT setid (setpref*,obvalue)>
<!ATTLIST setid
  %name_attr;
  %objtype_attr;>

<!ELEMENT obvalue (#PCDATA)>

<!-- text constructed with opcmds -->

<!--
NB: unparsing need only be supported for "proper" proof commands,
approximated by properscriptcmd
-->

<!ENTITY % properscriptcmd "%proofcmd;|%filecmd;|setid">

<!ELEMENT parsescript (#PCDATA)>

<!ELEMENT parseresult (%properscriptcmd;)*>

<!ELEMENT unparsecmds (%properscriptcmd;)*>

<!ELEMENT unparseresult (#PCDATA)>

<!ELEMENT showproofstate EMPTY>

<!ELEMENT showctxt EMPTY>

<!ELEMENT searchtheorems (#PCDATA)>

<!ELEMENT setlinewidth (#PCDATA)>

<!ELEMENT viewdoc (#PCDATA)>

<!-- prover informs interface a particular file is outdated -->

<!--
Below, url_attr will often be a file URL.  
We assume for now that the prover and interface are running on same
filesystem
-->

<!ATTLIST changecwd
  dir CDATA #REQUIRED>

<!-- Unix directory name  -->

<!ELEMENT opentheory (#PCDATA)>
<!ATTLIST opentheory
  %thyname_attr;>

<!ELEMENT closetheory EMPTY>
<!ATTLIST closetheory
  %thyname_attr;>

<!ELEMENT retracttheory EMPTY>
<!ATTLIST retracttheory
  %thyname_attr;>

<!--
FIXME: maybe add a command to ask prover for the file corresponding
to some theory (prover searches it's search path / cwd).
-->

<!ELEMENT loadfile EMPTY>
<!ATTLIST loadfile
  %url_attr;>

<!ELEMENT openfile EMPTY>
<!ATTLIST openfile
  %url_attr;>

<!ELEMENT closefile EMPTY>
<!ATTLIST closefile
  %url_attr;>

<!ELEMENT abortfile EMPTY>
<!ATTLIST abortfile
  %url_attr;>

<!ELEMENT usefile EMPTY>
<!ATTLIST usefile
  %url_attr;>

<!ELEMENT changecwd EMPTY>

<!ELEMENT informfileloaded EMPTY>
<!ATTLIST informfileloaded
  %thyname_attr;
  %url_attr;>

<!ELEMENT informfileretracted EMPTY>
<!ATTLIST informfileretracted
  %thyname_attr;
  %url_attr;>