lib/ProofGeneral/pgip.rnc

NEWS: IsabelleText font;

# 
# 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'.