--- a/lib/ProofGeneral/pgip.rnc Sat May 11 18:16:17 2013 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,1063 +0,0 @@
-#
-# RELAX NG Schema for PGIP, the Proof General Interface Protocol
-#
-# Authors: David Aspinall, LFCS, University of Edinburgh
-# Christoph Lüth, University of Bremen
-#
-# 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'.
-