#
# RELAX NG Schema for PGIP, the Proof General Interface Protocol
#
# Authors: David Aspinall, LFCS, University of Edinburgh
# Christoph Lüth, University of Bremen
#
# Version: $Id$
#
# Status: Prototype.
#
# For additional commentary, see accompanying commentary document available at
# http://proofgeneral.inf.ed.ac.uk/Kit/docs/commentary.pdf
#
# Advertised version: 2.0
#
# Contents
# ========
#
# 0. Prelude
# 1. Top-level
# 2. Component Control messages
# 3. Display Commands
# 4. Prover Configuration
# 5. Interface Configuration
# 6. Prover Control
# 7. Proof script markup and proof control
#
#
# ===============================================================================
#
# Note on datatypes. (see e.g. http://books.xmlschemata.org/relaxng):
#
# token : any string possibly with spaces, but spaces are normalised/collapsed
# (i.e. tokenised). Same as XML Schema xs:token
# string : any string, whitespaces preserved. Same as XML Schema xs:string
# (NB: attributes are normalised by XML 1.0 parsers so
# spaces/newlines must be quoted)
# text : text nodes/mixed content (whitespace may be lost in mixed content)
#
# So: attributes should usually be tokens or more restrictive; (sometimes: strings for printing)
# element contents may be string (preserving whitespace), token (tokenising),
# or text (which may contain further nodes).
# ==============================================================================
# 0. Prelude
# ==============================================================================
include "pgml.rnc" # include PGML grammar
name_attr = attribute name { token } # names are user-level textual identifiers (space-collapsed)
thyname_attr = attribute thyname { token } # names for theories (special case of name)
thmname_attr = attribute thmname { token } # names for theorems (special case of name)
datetime_attr =
attribute datetime { xsd:dateTime } # CCYY-MM-DDHH:MM:SS plus timezone info
url_attr = attribute url { xsd:anyURI } # URLs (often as "file:///localfilename.extn")
dir_attr = attribute dir { string } # Unix-style directory name (no final slash)
systemdata_attr =
attribute systemdata { token }? # system-specific data (useful for "stateless" RPC)
objname = token # an identifier name (convention: any characters except semi-colon)
objnames = token # sequence of names in an attribute: semi-colon separated
#objnames = string # A sequence of objnames
#termobjname = string { pattern = "[^;]+;" } # unfortunately these declarations don't
#objnames = objname | (termobjname, objname)
#objnames = objname+ # work with the RNC->DTD tool trang
# ==============================================================================
# 1. Top-level Messages/documents
# ==============================================================================
start = pgip # Single message
| pgips # A log of messages between components
| displayconfig # displayconfig as a standalone element
| pgipconfig # pgipconfig as a standalone element
| pgipdoc # A proof script document
pgip = element pgip { # A PGIP packet contains:
pgip_attrs, # - attributes with header information;
(toprovermsg | todisplaymsg | # - a message with one of four channel types
fromprovermsg | fromdisplaymsg
| internalmsg )
}
pgips = element pgips { pgip+ }
pgip_attrs =
attribute tag { token }?, # message tag, e.g. name of origin component (diagnostic)
attribute id { token }, # (unique) session id of this component
attribute destid { token }?, # session id of destination component
attribute class { pgip_class }, # general categorization of message
attribute refid { token }?, # component id this message responds to (usually destid)
attribute refseq { xsd:positiveInteger }?, # message sequence this message responds to
attribute seq { xsd:positiveInteger } # sequence number of this message
pgip_class = "pg" # message sent TO proof general broker (e.g. FROM proof assistant).
| "pa" # message sent TO the proof assistant/other component
| "pd" # message sent TO display/front-end components
toprovermsg = # Messages sent to the prover (class "pa"):
proverconfig # query Prover configuration, triggering interface configuration
| provercontrol # control some aspect of Prover
| improperproofcmd # issue a proof command
| improperfilecmd # issue a file command
| properproofcmd # [ NB: not strictly needed: input PGIP processing not expected ]
| properfilecmd # [ NB: not strictly needed: input PGIP processing not expected ]
| proofctxt # issue a context command
fromprovermsg = # Messages from the prover to PG (class "pg"):
kitconfig # messages to configure the interface
| proveroutput # output messages from the prover, usually display in interface
| fileinfomsg # information messages concerning file-system access / prover state
todisplaymsg = # Messages sent to display components (class "pd"):
brokermsg # status reports from broker
| dispmsg # display commands
# - Further, all fromprovermsg can be relayed to display
fromdisplaymsg = # Messages sent from display components (class "pg"):
dispcmd # display messages
| brokercontrol # messages controlling broker & prover processes
# - Further, all toprovermsg to be relayed to prover
# ===========================================================================
# 2. Component Control
# ===========================================================================
#
# Idea: - broker knows how to manage some components (inc provers) as child processes,
# communicate via pipes. Configured by a fixed PGIP config file read on startup.
# - other components may connect to running broker
#
# TODO: - describe startup protocol for component connecting to to running broker dynamically.
# This is the element contained in the configuration file read by the
# broker on startup.
pgipconfig = element pgipconfig { componentspec* }
componentspec =
element componentspec {
componentid_attr, # Unique identifier for component class
componentname_attr, # Textual name of component class
componenttype, # Type of component: prover, display, auxiliary
startupattrs, # Describing startup behaviour
systemattrs, # System attributes for component
componentconnect # How to connect to component
}
componentid_attr = attribute componentid { token }
componentname_attr = attribute componentname { token }
componenttype = element componenttype {
provercomponent
| displaycomponent
# | filehandlercomponent
| parsercomponent
| othercomponent }
provercomponent = element provercomponent { empty }
displaycomponent = element displaycomponent { attribute active { xsd:boolean}? }
parsercomponent = element parsercomponent { componentid_attr }
othercomponent = element othercomponent { empty }
componentconnect =
componentsubprocess | componentsocket | connectbyproxy
componentsubprocess =
element syscommand { string }
componentsocket =
(element host { token }, element port { xsd:positiveInteger })
connectbyproxy =
(element proxy { attribute host { token } # Host to connect to
, attribute connect {
"rsh" | "ssh" # Launch proxy via RSH or SSH, needs
# authentication
| "server" # connect to running proxy on given port
}?
, attribute user { token } ? # user to connect as with RSH/SSH
, attribute path { token } ? # path of pgipkit on remote
, attribute port { xsd:positiveInteger } ? # port to connect to running proxy
, componentconnect
})
# Attributes describing when to start the component.
startupattrs =
attribute startup { # what to do on broker startup:
"boot" | # always start this component (default with displays)
"manual" | # start manually (default with provers)
"ignore" # never start this component
}?
# System attributes describing behaviour of component.
systemattrs = (
attribute timeout { xsd:integer }? # timeout for communications
, attribute sync { xsd:boolean }? # whether to wait for ready
, attribute nestedgoals { xsd:boolean}? # Does prover allow nested goals?
)
# Control commands from display to broker
brokercontrol =
launchprover # Launch a new prover
| exitprover # Request to terminate a running prover
| restartprover # Request to restart/reset a running prover
| proversquery # Query about known provers, running provers
| shutdownbroker # Ask broker to exit (should be wary of this!)
| brokerstatusquery # Ask broker for status report
| pgipconfig # Send config to broker
provername_attr = attribute provername { provername }
provername = token
proverid_attr = attribute proverid { proverid }
proverid = token
launchprover = element launchprover { componentid_attr }
exitprover = element exitprover { proverid_attr }
restartprover = element restartprover { proverid_attr }
proversquery = element proversavailable { empty }
brokerstatusquery = element brokerstatusquery { empty }
shutdownbroker = element shutdownbroker { attribute force { xsd:boolean }? }
# Control messages from broker to interface
brokermsg =
brokerstatus # response to brokerstatusquery:
| proveravailmsg # announce new prover is available
| newprovermsg # new prover has started
| proverstatemsg # prover state has changed (busy/ready/exit)
brokerstatus = element brokerstatus
{ knownprovers, runningprovers, brokerinformation }
knownprover = element knownprover { componentid_attr, provername }
runningprover = element runningprover { componentid_attr, proverid_attr, provername }
knownprovers = element knownprovers { knownprover* }
runningprovers = element runningprovers { runningprover* }
brokerinformation = element brokerinformation { string }
proveravailmsg = element proveravailable { provername_attr,
componentid_attr }
newprovermsg = element proverstarted { proverid_attr
, componentid_attr
, provername_attr
}
proverstatemsg = element proverstate {
proverid_attr, provername_attr,
attribute proverstate {proverstate} }
proverstate = ("ready" | "busy" | "exitus")
# FIXME: This only allows provers to be available which are configured.
# In the long run, we want to change configurations while running.
# ===========================================================================
# 3. Display Commands
# ===========================================================================
# Messages exchanged between broker and display
dispcmd = dispfilecmd | dispobjcmd # display commands go from display to broker
dispmsg = dispfilemsg | dispobjmsg # display messages go from broker to display
dispfilecmd =
loadparsefile # parse and load file
| newfilewith # create new source file with given text
| dispopenfile # open (or create) new file
| savefile # save opened file
| discardfile # discard changes to opened file
dispfilemsg =
newfile # announce creation of new file (in response to load/open)
| filestatus # announce change in status of file in broker
# unique identifier of loaded files
srcid_attr = attribute srcid { token }
loadparsefile = element loadparsefile { url_attr, proverid_attr }
newfilewith = element newfilewith { url_attr, proverid_attr, string }
dispopenfile = element dispopenfile { url_attr,
proverid_attr,
attribute overwrite { xsd:boolean }?}
savefile = element savefile { srcid_attr,
url_attr? }
discardfile = element discardfile { srcid_attr }
newfile = element newfile { proverid_attr, srcid_attr, url_attr }
filestatus = element filestatus { proverid_attr, srcid_attr, newstatus_attr, url_attr?,
datetime_attr}
newstatus_attr = attribute newstatus { "saved" | "changed" | "discarded" }
dispobjcmd =
setobjstate # request of change of state
| editobj # request edit operation of objects
| createobj # request creation of new objects
# Suggested May 06: probably add re-load flags instead
# | reloadobjs # request relisting of all objects
| inputcmd # process the command (generated by an input event)
| interruptprover # send interrupt or kill signal to prover
dispobjmsg = element dispobjmsg {
newobj+ # new objects have been created
| delobj+ # objects have been deleted
| replaceobjs # objects are being replaced
| objectstate+ # objects have changed state
}
newobj = element newobj {
proverid_attr,
srcid_attr,
objid_attr,
attribute objposition { objid } ?,
objtype_attr ?,
attribute objparent { objid }?,
attribute objstate { objstate },
# FIXME: would like to include metainfo here
# as (properscriptcmd, metainfo*) | unparseable
(properscriptcmd | unparseable) }
replaceobjs = element replaceobjs {
srcid_attr,
attribute replacedfrom { objid }? ,
attribute replacedto { objid }?,
delobj*, # actually, either of delobj or
newobj* } # newobj can be empty but not both.
delobj = element delobj { proverid_attr, srcid_attr, objid_attr }
objectstate = element objstate
{ proverid_attr, srcid_attr, objid_attr,
attribute newstate {objstate} }
setobjstate = element setobjstate
{ objid_attr, attribute newstate {objstate} }
editobj = element editobj { srcid_attr ?,
attribute editfrom { objid }?,
attribute editto { objid }?,
string }
createobj = element createobj { srcid_attr ?,
attribute objposition { objid }?,
string }
# Suggested May 06: probably add re-load flags instead
# reloadobjs = element reloadobjs { srcid_attr }
inputcmd = element inputcmd { improper_attr, string }
improper_attr = attribute improper { xsd:boolean }
interruptprover = element interruptprover
{ interruptlevel_attr, proverid_attr }
interruptlevel_attr = attribute interruptlevel { "interrupt" | "stop" | "kill" }
objid_attr = attribute objid { objid }
objid = token
objstate =
( "unparseable" | "parsed" | "being_processed" | "processed" | "outdated" )
# ==============================================================================
# 4. Prover Configuration
# ==============================================================================
proverconfig =
askpgip # what version of PGIP do you support?
| askpgml # what version of PGML do you support?
| askconfig # tell me about objects and operations
| askprefs # what preference settings do you offer?
| setpref # please set this preference value
| getpref # please tell me this preference value
prefcat_attr = attribute prefcategory { token } # e.g. "expert", "internal", etc.
# could be used for tabs in dialog
askpgip = element askpgip { empty }
askpgml = element askpgml { empty }
askconfig = element askconfig { empty }
askprefs = element askprefs { prefcat_attr? }
setpref = element setpref { name_attr, prefcat_attr?, pgipvalue }
getpref = element getpref { name_attr, prefcat_attr? }
# ==============================================================================
# 5. Interface Configuration
# ==============================================================================
kitconfig =
usespgip # I support PGIP, version ..
| usespgml # I support PGML, version ..
| pgmlconfig # configure PGML symbols
| proverinfo # Report assistant information
| hasprefs # I have preference settings ...
| prefval # the current value of a preference is
| displayconfig # configure the following object types and operations
| setids # inform the interface about some known objects
| addids # add some known identifiers
| delids # retract some known identifers
| idvalue # display the value of some identifier
| menuadd # add a menu entry
| menudel # remove a menu entry
# version reporting
version_attr = attribute version { token }
usespgml = element usespgml { version_attr }
usespgip = element usespgip { version_attr
, activecompspec
}
# These data from the component spec which an active component can override, or which
# components initiating contact with the broker (e.g. incoming socket connections).
# There are some restrictions: if we start a tool, the componentid and the type must be the
# same as initially specified.
activecompspec = ( componentid_attr? # unique identifier of component class
, componentname_attr? # Textual name of this component (overrides initial spec)
, componenttype? # Type of component
, systemattrs # system attributes
, acceptedpgipelems? # list of accepted elements
)
acceptedpgipelems = element acceptedpgipelems { singlepgipelem* }
singlepgipelem = element pgipelem {
attribute async { xsd:boolean }?, # true if this command supported asynchronously (deflt false)
# (otherwise part of usual ready/sync stream)
attribute attributes { text }?, # comma-separated list of supported optional attribute names
# useful for: times attribute
text } # the unadorned name of the PGIP element (*not* an element)
# PGML configuration
pgmlconfig = element pgmlconfig { pgmlconfigure+ }
# Types for config settings: corresponding data values should conform to canonical
# representation for corresponding XML Schema 1.0 Datatypes.
#
# In detail:
# pgipnull = empty
# pgipbool = xsd:boolean = true | false
# pgipint = xsd:integer = (-)?(0-9)+ (canonical: no leading zeroes)
# pgipstring = string = <any non-empty character sequence>
# pgipchoice = cf xs:choice = type1 | type2 | ... | typen
pgiptype = pgipnull | pgipbool | pgipint | pgipstring | pgipchoice | pgipconst
pgipnull = element pgipnull { descr_attr?, empty }
pgipbool = element pgipbool { descr_attr?, empty }
pgipint = element pgipint { min_attr?, max_attr?, descr_attr?, empty }
min_attr = attribute min { xsd:integer }
max_attr = attribute max { xsd:integer }
pgipstring = element pgipstring { descr_attr?, empty }
pgipconst = element pgipconst { name_attr, descr_attr? }
# FIXME: Temporary fix because Isabelle does it wrong -- should be empty }
pgipchoice = element pgipchoice { pgiptype+ }
# Notes on pgipchoice:
# 1. Choices must not be nested (i.e. must not contain other choices)
# 2. The description attributes for pgipbool, pgipint, pgipstring and pgipconst
# are for use with pgipchoice: they can be used as a user-visible label
# when representing the choice to the user (e.g. in a pull-down menu).
# 3. A pgipchoice should have an unambiguous representation as a string. That means
# all constants in the choice must have different names, and a choice must not
# contain more than one each of pgipint, pgipstring and pgipbool.
pgipvalue = string
icon = element icon { xsd:base64Binary } # image data for an icon
# The default value of a preference as a string (using the unambiguous
# conversion to string mentioned above). A string value will always be quoted
# to distinguish it from constants or integers.
default_attr = attribute default { token }
# Description of a choice. If multi-line, first line is short tip.
descr_attr = attribute descr { string }
# 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)
haspref = element haspref {
name_attr, descr_attr?,
default_attr?, icon?,
pgiptype
}
hasprefs = element hasprefs { prefcat_attr?, haspref* }
prefval = element prefval { name_attr, pgipvalue }
# menu items (incomplete, FIXME)
path_attr = attribute path { token }
menuadd = element menuadd { path_attr?, name_attr?, opn_attr? }
menudel = element menudel { path_attr?, name_attr? }
opn_attr = attribute operation { token }
# Display configuration information:
# basic prover information, lexical structure of files,
# an icon for the prover, help documents, and the
# objects, types, and operations for building proof commands.
# NB: the following object types have a fixed interpretation
# in PGIP:
# "identifier": an identifier in the identifier syntax
# "comment": an arbitrary sequence of characters
# "theorem": a theorem name or text
# "theory" : a theory name or text
# "file" : a file name
displayconfig =
element displayconfig {
welcomemsg?, icon?, helpdoc*, lexicalstructure*,
objtype*, opn* }
objtype = element objtype { name_attr, descr_attr?, icon?, contains*, hasprefs? }
objtype_attr = attribute objtype { token } # the name of an objtype
contains = element contains { objtype_attr, empty } # a container for other objtypes
opn = element opn {
name_attr,
descr_attr?,
inputform?, # FIXME: can maybe remove this?
opsrc*, # FIXME: incompat change wanted: have list of source elts, not spaces
optrg,
opcmd,
improper_attr? }
opsrc =
element opsrc {
name_attr?, # %name as an alternative to %number
selnumber_attr?, # explicit number for %number, the nth item selected
prompt_attr?, # prompt in form or tooltip in template
listwithsep_attr?, # list of args of this type with given separator
list { token* } } # source types: a space separated list
# FIXME incompat change wanted: just have one source here
# FIXME: need to add optional pgiptype
listwithsep_attr = attribute listwithsep { token }
selnumber_attr = attribute selnumber { xsd:positiveInteger }
prompt_attr = attribute prompt { string }
optrg =
element optrg { token }? # single target type, empty for proof command
opcmd =
element opcmd { string } # prover command, with printf-style "%1"-args
# (whitespace preserved here: literal text)
# interactive operations - require some input
inputform = 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"
field = element field {
name_attr, pgiptype,
element prompt { string }
}
# identifier tables: these list known items of particular objtype.
# Might be used for completion or menu selection, and inspection.
# May have a nested structure (but objtypes do not).
setids = element setids { idtable* } # (with an empty idtable, clear table)
addids = element addids { idtable* }
delids = element delids { idtable* }
# give value of some identifier (response to showid; same values returned)
idvalue = element idvalue
{ thyname_attr?, name_attr, objtype_attr, pgmltext }
idtable = element idtable { context_attr?, objtype_attr, identifier* }
identifier = element identifier { token }
context_attr = attribute context { token } # parent identifier (context)
# prover information:
# name, instance (e.g. in case of major parameter of invocation);
# description, version, homepage, welcome message, docs available
proverinfo = element proverinfo
{ name_attr, version_attr?, instance_attr?,
descr_attr?, url_attr?, filenameextns_attr?,
## TEMP: these elements are duplicated in displayconfig, as they're
## moving there.
welcomemsg?, icon?, helpdoc*, lexicalstructure* }
instance_attr = attribute instance { token }
welcomemsg = element welcomemsg { string }
# helpdoc: advertise availability of some documentation, given a canonical
# name, textual description, and URL or viewdoc argument.
#
helpdoc = element helpdoc { name_attr, descr_attr, url_attr?, token } # token string is arg to "viewdoc"
filenameextns_attr = attribute filenameextns { xsd:NMTOKENS } # space-separated extensions sans "."
# lexical structure of proof texts
lexicalstructure =
element lexicalstructure {
keyword*,
stringdelimiter*,
escapecharacter?,
commentdelimiter*,
identifiersyntax?
}
keyword = element keyword {
attribute word { token },
shorthelp?,
longhelp? }
shorthelp = element shorthelp { string } # one-line (tooltip style) help
longhelp = element longhelp { string } # multi-line help
stringdelimiter = element stringdelimiter { token } # should be a single char
# The escape character is used to escape strings and other special characters - in most languages it is \
escapecharacter = element escapecharacter { token } # should be a single char
commentdelimiter = element commentdelimiter {
attribute start { token },
attribute end { token }?,
empty
}
# syntax for ids: id = initial allowed* or id = allowed+ if initial empty
identifiersyntax = element identifiersyntax {
attribute initialchars { token }?,
attribute allowedchars { token }
}
# ==============================================================================
# 6. Prover Control
# ==============================================================================
provercontrol =
proverinit # reset prover to its initial state
| proverexit # exit prover
| startquiet # stop prover sending proof state displays, non-urgent messages
| stopquiet # turn on normal proof state & message displays
| pgmlsymbolson # activate use of symbols in PGML output (input always understood)
| pgmlsymbolsoff # deactivate use of symbols in PGML output
| setproverflag # set/clear a standard control flag (supersedes above)
proverinit = element proverinit { empty }
proverexit = element proverexit { empty }
startquiet = element startquiet { empty } # DEPRECATED
stopquiet = element stopquiet { empty } # DEPRECATED
pgmlsymbolson = element pgmlsymbolson { empty } # DEPRECATED
pgmlsymbolsoff = element pgmlsymbolsoff { empty } # DEPRECATED
setproverflag = element setproverflag { flagname_attr,
attribute value { xsd:boolean } }
flagname_attr =
attribute flagname { "quiet"
| "pgmlsymbols"
| "metainfo:thmdeps"
}
# General prover output/responses
# Prover output has an otional proverid_attribute. This is set by the broker when relaying
# prover output to displays. When producing output, provers can and should not set this
# attribute.
proveroutput =
ready # prover is ready for input
| cleardisplay # prover requests a display area to be cleared
| proofstate # prover outputs the proof state
| normalresponse # prover outputs some display
| errorresponse # prover indicates an error/warning/debug condition, with message
| scriptinsert # some text to insert literally into the proof script
| metainforesponse # prover outputs some other meta-information to interface
| parseresult # results of a <parsescript> request (see later)
ready = element ready { empty }
displayarea = "status" # a status line
| "message" # the message area (e.g. response buffer, perhaps swapped into view)
| "display" # the main display area (e.g. goals buffer, usually persistent)
| token # prover-specified window name
cleardisplay =
element cleardisplay {
proverid_attr?,
attribute area {
displayarea | "all" } }
proofstate =
element proofstate { proverid_attr?, pgml }
messagecategory = # attribution of message
"internal" # - internal debug message (interface should usually hide)
| "information" # - user-level debug/info message (interface may hide)
| "tracing" # - user-level "tracing" message (possibly voluminous)
normalresponse =
element normalresponse {
proverid_attr?, # if no proverid, assume message is from broker
attribute area { displayarea },
attribute messagecategory { messagecategory }?, # optional extra category (e.g. tracing/debug)
attribute urgent { xsd:boolean }?, # message should be brought to users attention
pgmltext
}
## Error messages: these are different from ordinary messages in that
## they indicate an error condition in the prover, with a notion
## of fatality and (optionally) a location. The interface may collect these
## messages in a log, display in a modal dialog, or in the specified
## display area if one is given
##
## Error responses are also taken to indicate failure of a command to be processed, but only in
## the special case of a response with fatality "fatal". If any errorresponse with
## fatality=fatal is sent before <ready/>, the PGIP command which triggered the message is
## considered to have failed. If the command is a scripting command, it will not be added to
## the successfully processed part of the document. A "nonfatal" error also indicates some
## serious problem with the sent command, but it is not considered to have failed. This is the
## ordinary response for
errorresponse =
element errorresponse {
proverid_attr?, # ... as above ...
attribute area { displayarea }?,
attribute fatality { fatality },
location_attrs,
pgmltext
}
fatality = # degree of error conditions:
"info" # - info message
| "warning" # - warning message
| "nonfatal" # - error message, recovered and state updated
| "fatal" # - error message, command has failed
| "panic" # - shutdown condition, component exits (interface may show message)
| "log" # - system-level log message (interface does not show message; written to log file)
| "debug" # - system-level debug message (interface may show message; written to log file)
# attributes describing a file location (for error messages, etc)
location_attrs =
attribute location_descr { string }?,
attribute location_url { xsd:anyURI }?,
attribute locationline { xsd:positiveInteger }?,
attribute locationcolumn { xsd:positiveInteger }?,
attribute locationcharacter { xsd:positiveInteger }?,
attribute locationlength { xsd:positiveInteger }?
# instruction to insert some literal text into the document
scriptinsert = element scriptinsert { proverid_attr?, metavarid_attr?, string }
# metainformation is an extensible place to put system-specific information
value = element value { name_attr?, text } # generic value holder [ deprecated: use metainfo ]
metainfo = element metainfo { name_attr?, text } # generic info holder
metainforesponse =
element metainforesponse {
proverid_attr?,
attribute infotype { token }, # categorization of data
(value | metainfo)* } # data values/text
# ==============================================================================
# 7. Proof script markup and proof control
# ==============================================================================
# properproofcmds are purely markup on native proof script (plain) text
properproofcmd =
opengoal # open a goal in ambient context
| proofstep # a specific proof command (perhaps configured via opcmd)
| closegoal # complete & close current open proof (succeeds iff proven, may close nested pf)
| giveupgoal # close current open proof, retaining attempt in script (Isar oops)
| postponegoal # close current open proof, record as proof obl'n (Isar sorry)
| comment # a proof script comment; text probably ignored by prover
| doccomment # a proof script document comment; text maybe processed by prover
| whitespace # a whitespace comment; text ignored by prover
| spuriouscmd # command ignored for undo, e.g. "print x", could be pruned from script
| badcmd # a command which should not be stored in the script (e.g. an improperproofcmd)
| litcomment # a PGIP literate comment (never passed to prover)
| pragma # a document generating instruction (never passed to prover)
# improperproofcmds are commands which are never stored in the script
improperproofcmd =
dostep # issue a properproofcmd (without passing in markup)
| undostep # undo the last proof step issued in currently open goal
| redostep # redo the last undone step issued in currently open goal (optionally supported)
| abortgoal # give up on current open proof, close proof state, discard history
| forget # forget a theorem (or named target), outdating dependent theorems
| restoregoal # re-open previously postponed proof, outdating dependent theorems
# In future we may allow input to contain markup; for now it is treated uniformly as plain text.
opengoal = element opengoal { display_attr?, thmname_attr?, string } # FIXME: add objprefval
proofstep = element proofstep { display_attr?, name_attr?, objtype_attr?, string }
closegoal = element closegoal { display_attr?, string }
giveupgoal = element giveupgoal { display_attr?, string }
postponegoal = element postponegoal { display_attr?, string }
comment = element comment { display_attr?, string }
doccomment = element doccomment { display_attr?, string }
whitespace = element whitespace { display_attr?, string }
display_attr = attribute nodisplay { xsd:boolean } # whether to display in documentation
spuriouscmd = element spuriouscmd { string } # no semantic effect (e.g. print)
badcmd = element badcmd { string } # illegal in script (e.g. undo)
nonscripting = element nonscripting { string } # non-scripting text (different doc type)
litcomment = element litcomment { format_attr?, (text | directive)* }
directive = element directive { (proofctxt,pgml) }
format_attr = attribute format { token }
pragma = showhidecode | setformat
showhidecode = element showcode { attribute show { xsd:boolean } }
setformat = element setformat { format_attr }
dostep = element dostep { string }
undostep = element undostep { times_attr? }
redostep = element redostep { times_attr? }
abortgoal = element abortgoal { empty }
forget = element forget { thyname_attr?, name_attr?, objtype_attr? }
restoregoal = element restoregoal { thmname_attr }
times_attr = attribute times { xsd:positiveInteger }
# empty objprefval element is used for object prefs in script markup
objprefval = element objprefval { name_attr, val_attr, empty }
val_attr = attribute value { token }
# =======================================================
# Inspecting the proof context, etc.
# NB: ids/refs/parent: work in progress, liable to change.
proofctxt =
askids # tell me about identifiers (given objtype in a theory)
| askrefs # tell me about dependencies (references) of an identifier
# | askparent # tell me the container for some identifier
| showid # print the value of some object
| askguise # tell me about the current state of the prover
| parsescript # parse a raw proof script into proofcmds
| showproofstate # (re)display proof state (empty if outside a proof)
| showctxt # show proof context
| searchtheorems # search for theorems (prover-specific arguments)
| setlinewidth # set line width for printing
| viewdoc # request some on-line help (prover-specific arg)
askids = element askids { thyname_attr?, objtype_attr? }
# Note that thyname_attr is *required* for certain objtypes (e.g. theorem).
# This is because otherwise the list is enormous.
# Perhaps we should make thyname_attr obligatory?
# With a blank entry (i.e. thyname="") allowed for listing theories, or for when
# you really do want to see everything (could be a shell-style glob)
# askids: container -> identifiers contained within
# askparent: identifier + type + context -> container
# askrers: identifier + type + context -> identifiers which are referenced
#
askrefs = element askrefs { url_attr?, thyname_attr?, objtype_attr?, name_attr? }
# TODO: maybe include guises here as indication of reference point.
# setrefs in reply to askrefs only really needs identifiers, but it's nice to
# support voluntary information too.
setrefs = element setrefs { url_attr?, thyname_attr?, objtype_attr?, name_attr?, idtable*, fileurl* }
fileurl = element fileurl { url_attr }
# telldeps = element telldeps { thyname_attr?, objtype_attr, name_attr?, identifier* }
# Idea: for a theory dependency we return a single file (URL), the containing file.
# for a file dependency we return urls of parent files,
# for theorem dependency we return theory
# for term dependency we return definition (point in file)
showid = element showid { thyname_attr?, objtype_attr, name_attr }
askguise = element askguise { empty }
showproofstate = element showproofstate { empty }
showctxt = element showctxt { empty }
searchtheorems = element searchtheorems { string }
setlinewidth = element setlinewidth { xsd:positiveInteger }
viewdoc = element viewdoc { token }
# =======================================================
# Proof script documents and parsing proof scripts
# A PGIP document is a sequence of script commands, each of which
# may have meta information attached.
properscriptcmdmetainfo = properscriptcmd, metainfo*
pgipdoc = element pgipdoc { properscriptcmdmetainfo* }
# NB: parsing needs only be supported for "proper" proof commands,
# which may appear in proof texts. The groupdelimiters are purely
# markup hints to the interface for display structure on concrete syntax.
# The location attributes can be used by the prover in <parsescript> to
# generate error messages for particular locations; they can be used
# in <parseresult> to pass position information back to the display,
# particularly in the case of (re-)parsing only part of a file.
# The parsing component MUST return the same location attributes
# (and system data attribute) that was passed in.
parsescript = element parsescript
{ location_attrs, systemdata_attr, string }
parseresult = element parseresult { location_attrs, systemdata_attr,
singleparseresult* }
# Really we'd like parsing to return properscriptcmdmetainfo as a single
# result (and similarly for newobj).
# Unfortunately, although this is an XML-transparent extension, it
# messes up the Haskell schema-fixed code rather extensively, so for
# now we just treat metainfo at the same level as the other results,
# although it should only appear following a properscriptcmd.
singleparseresult = properscriptcmd | metainfo | unparseable | errorresponse
unparseable = element unparseable { string }
properscriptcmd = properproofcmd | properfilecmd | groupdelimiter
groupdelimiter = openblock | closeblock
openblock = element openblock {
name_attr?, objtype_attr?,
metavarid_attr?, positionid_attr?,
fold_attr?, indent_attr? }
closeblock = element closeblock { empty }
#
metavarid_attr = attribute metavarid { token }
positionid_attr = attribute positionid { token }
fold_attr = attribute fold { xsd:boolean }
indent_attr = attribute indent { xsd:integer }
# =======================================================
# Theory/file handling
properfilecmd = # (NB: properfilecmds are purely markup on proof script text)
opentheory # begin construction of a new theory.
| theoryitem # a step in a theory (e.g. declaration/definition of type/constant).
| closetheory # complete construction of the currently open theory
improperfilecmd =
doitem # issue a proper file command (without passing in markup)
| undoitem # undo last step (or named item) in theory construction
| redoitem # redo last step (or named item) in theory construction (optionally supported)
| aborttheory # abort currently open theory
| retracttheory # retract a named theory
| openfile # signal a file is being opened for constructing a proof text interactively
| closefile # close the currently open file, suggesting it has been processed
| abortfile # unlock a file, suggesting it hasn't been processed
| loadfile # load (i.e. process directly) a file possibly containing theory definition(s)
| retractfile # retract a given file (including all contained theories)
| changecwd # change prover's working directory (or load path) for files
| systemcmd # system (other) command, parsed internally
fileinfomsg =
informfileloaded # prover informs interface a particular file is loaded
| informfileretracted # prover informs interface a particular file is outdated
| informguise # prover informs interface about current state
opentheory = element opentheory { thyname_attr, parentnames_attr?, string }
closetheory = element closetheory { string }
theoryitem = element theoryitem { name_attr?, objtype_attr?, string } # FIXME: add objprefval
doitem = element doitem { string }
undoitem = element undoitem { name_attr?, objtype_attr?, times_attr? }
redoitem = element redoitem { name_attr?, objtype_attr?, times_attr? }
aborttheory = element aborttheory { empty }
retracttheory = element retracttheory { thyname_attr }
parentnames_attr = attribute parentnames { objnames }
# Below, url_attr will often be a file URL. We assume for now that
# the prover and interface are running on same filesystem.
#
openfile = element openfile { url_attr } # notify begin reading from given file
closefile = element closefile { empty } # notify currently open file is complete
abortfile = element abortfile { empty } # notify currently open file is discarded
loadfile = element loadfile { url_attr } # ask prover to read file directly
retractfile = element retractfile { url_attr } # ask prover to retract file
changecwd = element changecwd { url_attr } # ask prover to change current working dir
# this one not yet implemented, but would be handy. Perhaps could be
# locatethy/locatefile instead.
#locateobj = element locateobj { name_attr, objtype_attr } # ask prover for file defining obj
informfileloaded = element informfileloaded { completed_attr?,
url_attr } # prover indicates a processed file
informfileretracted = element informfileretracted { completed_attr?,
url_attr } # prover indicates an undone file
informfileoutdated = element informfileoutdated { completed_attr?,
url_attr } # prover indicates an outdated file
informfilelocation = element informfilelocation { url_attr } # response to locateobj
completed_attr = attribute completed { xsd:boolean } # false if not completed (absent=>true)
# (the prover is requesting a lock)
informguise =
element informguise {
element guisefile { url_attr }?,
element guisetheory { thyname_attr }?,
element guiseproof { thmname_attr?, proofpos_attr? }?
}
proofpos_attr = attribute proofpos { xsd:nonNegativeInteger }
systemcmd = element systemcmd { string } # "shell escape", arbitrary prover command!
# ==============================================================================
# 8. Internal messages: only used between communicating brokers.
# ==============================================================================
internalmsg = launchcomp | stopcomp | registercomp | compstatus
launchcomp = element launchcomponent { componentspec }
# request to start an instance of this component remotely
stopcomp = element stopcomponent { attribute sessionid { token } }
# request to stop component with this session id remotely
registercomp = element registercomponent { activecompspec }
# component has been started successfully
compstatus = element componentstatus { componentstatus_attr # status
, componentid_attr? # component id (for failure)
, element text { string }? # user-visible error message
, element info { string }? # Additional info for log files.
}
# component status: failed to start, or exited
componentstatus_attr = attribute status { ("fail" # component failed to start
|"exit" # component exited
)}
# Local variables:
# fill-column: 95
# End:
# ==============================================================================
# end of `pgip.rnc'.