lib/ProofGeneral/pgip.rnc
changeset 17735 e6948d8f5f73
child 23434 b2e7d4c29614
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/lib/ProofGeneral/pgip.rnc	Fri Sep 30 17:24:51 2005 +0200
     1.3 @@ -0,0 +1,906 @@
     1.4 +# 
     1.5 +# RELAX NG Schema for PGIP, the Proof General Interface Protocol                   
     1.6 +# 
     1.7 +# Authors:  David Aspinall, LFCS, University of Edinburgh       
     1.8 +#           Christoph Lueth, University of Bremen       
     1.9 +#
    1.10 +# Version: $Id$    
    1.11 +# 
    1.12 +# Status:   Prototype.
    1.13 +#
    1.14 +# For additional commentary, see accompanying commentary document available at
    1.15 +# http://proofgeneral.inf.ed.ac.uk/Kit/docs/commentary.pdf
    1.16 +#
    1.17 +# Advertised version: 2.0
    1.18 +# 
    1.19 +# Contents
    1.20 +# ========
    1.21 +#
    1.22 +#  0. Prelude
    1.23 +#  1. Top-level 
    1.24 +#  2. Component Control messages
    1.25 +#  3. Display Commands
    1.26 +#  4. Prover Configuration
    1.27 +#  5. Interface Configuration
    1.28 +#  6. Prover Control
    1.29 +#  7. Proof script markup and proof control
    1.30 +#
    1.31 +
    1.32 +# ==============================================================================
    1.33 +# 0. Prelude
    1.34 +# ==============================================================================
    1.35 +
    1.36 +include "pgml.rnc"                           # include PGML grammar
    1.37 +
    1.38 +name_attr = attribute name { text }          # names are user-level textual identifiers
    1.39 +thyname_attr = attribute thyname { text }    # names for theories (special case of name)
    1.40 +thmname_attr = attribute thmname { text }    # names for theorems (special case of name)
    1.41 +
    1.42 +datetime_attr = 
    1.43 +   attribute datetime { xsd:dateTime }       # CCYY-MM-DDHH:MM:SS plus timezone info
    1.44 +url_attr  = attribute url { xsd:anyURI }     # URLs  (often as "file:///localfilename.extn")
    1.45 +dir_attr  = attribute dir { text }           # Unix-style directory name (no final slash)
    1.46 +
    1.47 +systemdata_attr  = 
    1.48 +            attribute systemdata { text }?   # system-specific data (useful for "stateless" RPC)
    1.49 +
    1.50 +
    1.51 +objname = string
    1.52 +termobjname = string                         # (User-level) object names, semi-colon terminated
    1.53 +objnames = string                            # A sequence of objnames
    1.54 +
    1.55 +#termobjname  = xsd:string { pattern = "[^;]+;" }  # unfortunately these declarations don't 
    1.56 +#objnames = objname+                               #  work with the RNC->DTD tool trang
    1.57 +
    1.58 +
    1.59 +# ==============================================================================
    1.60 +# 1. Top-level Messages/documents
    1.61 +# ==============================================================================
    1.62 +
    1.63 +start = pgip                                 # Single message
    1.64 +      | pgips                                # A log of messages between components
    1.65 +      | displayconfig                        # displayconfig as a standalone element
    1.66 +      | pgipconfig                           # pgipconfig as a standalone element
    1.67 +
    1.68 +pgip = element pgip {                        #  A PGIP packet contains:
    1.69 +   pgip_attrs,                               #   - attributes with header information;
    1.70 +   (toprovermsg | todisplaymsg |             #   - a message with one of four channel types
    1.71 +    fromprovermsg | fromdisplaymsg 
    1.72 +   | internalmsg ) 
    1.73 +  }
    1.74 +
    1.75 +pgips = element pgips { pgip+ }
    1.76 +
    1.77 +pgip_attrs =
    1.78 + attribute tag { text }?,                   # message tag, e.g. name of origin component (diagnostic)
    1.79 + attribute id { text },                     # (unique) session id of this component 
    1.80 + attribute destid { text }?,                # session id of destination component
    1.81 + attribute class { pgip_class },            # general categorization of message
    1.82 + attribute refid { text }?,                 # component id this message responds to (usually destid)
    1.83 + attribute refseq { xsd:positiveInteger }?, # message sequence this message responds to
    1.84 + attribute seq { xsd:positiveInteger }      # sequence number of this message
    1.85 +
    1.86 +pgip_class = "pg"      # message sent TO proof general broker
    1.87 +           | "pa"      # message sent TO the proof assistant/other component
    1.88 +           | "pd"      # message sent TO display/front-end components
    1.89 +
    1.90 +toprovermsg =          # Messages sent to the prover (class "pa"):
    1.91 +   proverconfig        #   query Prover configuration, triggering interface configuration
    1.92 + | provercontrol       #   control some aspect of Prover
    1.93 + | improperproofcmd    #   issue a proof command 
    1.94 + | improperfilecmd     #   issue a file command
    1.95 + | properproofcmd      #   [ NB: not strictly needed: input PGIP processing not expected ]
    1.96 + | properfilecmd       #   [ NB: not strictly needed: input PGIP processing not expected ]
    1.97 + | proofctxt           #   issue a context command
    1.98 +
    1.99 +fromprovermsg =        # Messages from the prover to PG (class "pg"):
   1.100 +   kitconfig           #   messages to configure the interface 
   1.101 + | proveroutput        #   output messages from the prover, usually display in interface
   1.102 + | fileinfomsg         #   information messages concerning file-system access / prover state
   1.103 +
   1.104 +todisplaymsg =         # Messages sent to display components (class "pd"):
   1.105 +   brokermsg           #   status reports from broker
   1.106 + | dispmsg             #   display commands
   1.107 +                       #   - Further, all fromprovermsg can be relayed to display
   1.108 +
   1.109 +fromdisplaymsg =       # Messages sent from display components (class "pg"):
   1.110 +   dispcmd             #   display messages 
   1.111 + | brokercontrol       #   messages controlling broker & prover processes
   1.112 +		       #   - Further, all toprovermsg to be relayed to prover
   1.113 +
   1.114 +# ===========================================================================
   1.115 +# 2. Component Control
   1.116 +# ===========================================================================
   1.117 +
   1.118 +#
   1.119 +# Idea:  - broker knows how to manage some components (inc provers) as child processes,
   1.120 +#          communicate via pipes.  Configured by a fixed PGIP config file read on startup.
   1.121 +#        - other components may connect to running broker
   1.122 +#
   1.123 +# TODO: - describe startup protocol for component connecting to to running broker dynamically.
   1.124 +
   1.125 +# This is the element contained in the configuration file read by the 
   1.126 +# broker on startup.
   1.127 +pgipconfig = element pgipconfig { componentspec* }
   1.128 +
   1.129 +componentspec = 
   1.130 +   element componentspec {
   1.131 +      componentid_attr,         # Unique identifier for component class
   1.132 +      componentname_attr,       # Textual name of component class
   1.133 +      componenttype,            # Type of component: prover, display, auxiliary
   1.134 +      systemattrs,              # System attributes for connecting to component
   1.135 +      componentconnect          # How to connect to component
   1.136 +   }
   1.137 +
   1.138 +componentid_attr   = attribute componentid   { token }
   1.139 +componentname_attr = attribute componentname { text }
   1.140 +
   1.141 +componenttype = element componenttype {
   1.142 +     provercomponent 
   1.143 +   | displaycomponent 
   1.144 + # | filehandlercomponent 
   1.145 +   | parsercomponent 
   1.146 +   | othercomponent }
   1.147 +
   1.148 +provercomponent  = element provercomponent { empty }
   1.149 +displaycomponent = element displaycomponent { attribute active { xsd:boolean}? }
   1.150 +parsercomponent  = element parsercomponent  { componentid_attr }
   1.151 +othercomponent   = element othercomponent { empty }
   1.152 +
   1.153 +componentconnect =
   1.154 +   componentsubprocess | componentsocket | connectbyproxy
   1.155 +
   1.156 +componentsubprocess = 
   1.157 +   element syscommand { text }
   1.158 +componentsocket = 
   1.159 +   (element host { text }, element port { text })
   1.160 +connectbyproxy = 
   1.161 +   (element proxy { attribute host { text }    # Host to connect to
   1.162 +		  , attribute connect { 
   1.163 +                           "rsh" | "ssh" # Launch proxy via RSH or SSH, needs
   1.164 +			                 # authentication 
   1.165 +                         | "server"  # connect to running proxy on given port
   1.166 +                         }?
   1.167 +                  , attribute user { text } ? # user to connect as with RSH/SSH
   1.168 +		  , attribute port { text } ? # port to connect to running proxy
   1.169 +		  , componentconnect
   1.170 +		  })
   1.171 +
   1.172 +systemattrs = (
   1.173 +   attribute timeout { xsd:integer }?,  # timeout for communications
   1.174 +   attribute sync { xsd:boolean }?,     # whether to wait for ready
   1.175 +   attribute startup {		# what to do on broker startup:
   1.176 +             "boot"   |		# always start this component (default with displays)
   1.177 +             "manual" |		# start manually (default with provers)
   1.178 +             "ignore"		# never start this
   1.179 +             }?
   1.180 +   )
   1.181 +
   1.182 +# Control commands from display to broker
   1.183 +brokercontrol = 
   1.184 +    launchprover		# Launch a new prover
   1.185 +  | exitprover			# Request to terminate a running prover
   1.186 +  | restartprover		# Request to restart/reset a running prover
   1.187 +  | proversquery		# Query about known provers, running provers
   1.188 +  | shutdownbroker		# Ask broker to exit (should be wary of this!)
   1.189 +  | brokerstatusquery		# Ask broker for status report
   1.190 +  | pgipconfig			# Send config to broker
   1.191 +
   1.192 +provername_attr    = attribute provername { provername }
   1.193 +provername         = token
   1.194 +
   1.195 +proverid_attr     = attribute proverid  { proverid }
   1.196 +proverid          = token
   1.197 +
   1.198 +launchprover      = element launchprover { componentid_attr }
   1.199 +exitprover        = element exitprover { proverid_attr }
   1.200 +restartprover     = element restartprover { proverid_attr }
   1.201 +proversquery      = element proversavailable { empty }
   1.202 +brokerstatusquery = element brokerstatusquery { empty } 
   1.203 +shutdownbroker    = element shutdownbroker { attribute force { xsd:boolean }? } 
   1.204 +
   1.205 +# Control messages from broker to interface
   1.206 +brokermsg  = 
   1.207 +    brokerstatus		# response to brokerstatusquery:
   1.208 +  | proveravailmsg		# announce new prover is available
   1.209 +  | newprovermsg		# new prover has started 
   1.210 +  | proverstatemsg		# prover state has changed (busy/ready/exit)
   1.211 +
   1.212 +brokerstatus  = element brokerstatus 
   1.213 +                       { knownprovers, runningprovers, brokerinformation }
   1.214 +
   1.215 +knownprover   = element knownprover   { componentid_attr, provername }
   1.216 +runningprover = element runningprover { proverid_attr, provername }
   1.217 +
   1.218 +knownprovers   = element knownprovers { knownprover* }
   1.219 +runningprovers = element runningprovers { runningprover* }
   1.220 +brokerinformation = element brokerinformation { text }
   1.221 +
   1.222 +proveravailmsg  = element proveravailable { provername_attr,
   1.223 +                                            componentid_attr }
   1.224 +newprovermsg    = element proverstarted { provername_attr, 
   1.225 +		                          proverid_attr }
   1.226 +                  # QUESTION: do we want  componentid_attr 
   1.227 +                  # here as well, and do we want to be able to run multiple
   1.228 +                  # copies of the same prover? 
   1.229 +proverstatemsg = element proverstate { 
   1.230 +                       proverid_attr, provername_attr,
   1.231 +                       attribute proverstate {proverstate} } 
   1.232 +
   1.233 +proverstate    = ("ready" | "busy" | "exitus")
   1.234 +
   1.235 +# FIXME: This only allows provers to be available which are configured.
   1.236 +#        In the long run, we want to change configurations while running.
   1.237 +
   1.238 +
   1.239 +# ===========================================================================
   1.240 +# 3. Display Commands
   1.241 +# ===========================================================================
   1.242 +
   1.243 +# Messages exchanged between broker and display
   1.244 +
   1.245 +                        
   1.246 +dispcmd = dispfilecmd | dispobjcmd  # display commands go from display to broker
   1.247 +dispmsg = dispfilemsg | dispobjmsg  # display messages go from broker to display
   1.248 +   
   1.249 +
   1.250 +dispfilecmd = 
   1.251 +    loadparsefile		# parse and load file
   1.252 +  | newfilewith			# create new source file with given text
   1.253 +  | dispopenfile		# open (or create) new file 
   1.254 +  | savefile			# save opened file
   1.255 +  | discardfile			# discard changes to opened file
   1.256 +
   1.257 +dispfilemsg =
   1.258 +    newfile			# announce creation of new file (in response to load/open)
   1.259 +  | filestatus			#announce change in status of file in broker
   1.260 +
   1.261 +# unique identifier of loaded files
   1.262 +srcid_attr = attribute srcid { text }
   1.263 +
   1.264 +loadparsefile = element loadparsefile { url_attr, proverid_attr }
   1.265 +newfilewith   = element newfilewith   { url_attr, proverid_attr, text }
   1.266 +dispopenfile  = element dispopenfile { url_attr,
   1.267 +                                       proverid_attr,
   1.268 +                                       attribute overwrite { xsd:boolean }?}
   1.269 +savefile      = element savefile { srcid_attr,     
   1.270 +                                   url_attr? }
   1.271 +discardfile   = element discardfile { srcid_attr }
   1.272 +
   1.273 +newfile       = element newfile  { proverid_attr, srcid_attr, url_attr }
   1.274 +filestatus    = element filestatus  { proverid_attr, srcid_attr, newstatus_attr, 
   1.275 +				      datetime_attr} 
   1.276 +
   1.277 +newstatus_attr = attribute newstatus { "saved" | "changed" | "discarded" }
   1.278 +
   1.279 +dispobjcmd =
   1.280 +    setobjstate			# request of change of state 
   1.281 +  | editobj			# request edit operation of opbjects
   1.282 +  | createobj			# request creation of new objects
   1.283 +  | inputcmd		        # process the command (generated by an input event)
   1.284 +  | interruptprover		# send interrupt or kill signal to prover
   1.285 +
   1.286 +dispobjmsg = element dispobjmsg { 
   1.287 +      newobj+			# new objects have been created
   1.288 +    | delobj+			# objects have been deleted
   1.289 +    | replaceobjs		# objects are being replaced
   1.290 +    | objectstate+		# objects have changed state
   1.291 +    }
   1.292 +
   1.293 +newobj = element newobj {
   1.294 +	    proverid_attr,
   1.295 +            srcid_attr, 
   1.296 +	    objid_attr, 
   1.297 +            attribute objposition { objid } ?,
   1.298 +            objtype_attr ?,
   1.299 +            attribute objparent { objid }?,
   1.300 +            attribute objstate { objstate },
   1.301 +            (properscriptcmd | unparseable) }
   1.302 +
   1.303 +replaceobjs = element replaceobjs {
   1.304 +	                srcid_attr,
   1.305 +	                attribute replacedfrom { objid }? ,
   1.306 +			attribute replacedto { objid }?,
   1.307 +                        delobj*,
   1.308 +                        newobj+ }
   1.309 +
   1.310 +delobj = element delobj   { proverid_attr, srcid_attr, objid_attr }
   1.311 +
   1.312 +objectstate = element objstate
   1.313 +                       { proverid_attr, srcid_attr, objid_attr,
   1.314 +                         attribute newstate {objstate} }
   1.315 +
   1.316 +setobjstate = element setobjstate
   1.317 +                  {  objid_attr, attribute newstate {objstate} }
   1.318 +
   1.319 +editobj = element editobj { srcid_attr ?,
   1.320 +	                    attribute editfrom { objid }?,
   1.321 +                            attribute editto   { objid }?,
   1.322 +                            text }
   1.323 +createobj = element createobj { srcid_attr ?, 
   1.324 +                                attribute objposition { objid }?, 
   1.325 +                                text}
   1.326 +
   1.327 +inputcmd       = element inputcmd { improper_attr, text }
   1.328 +improper_attr  = attribute improper { xsd:boolean }
   1.329 +
   1.330 +interruptprover = element interruptprover 
   1.331 +                          { interruptlevel_attr, proverid_attr }
   1.332 +
   1.333 +interruptlevel_attr  = attribute interruptlevel { "interrupt" | "stop" | "kill" }
   1.334 +
   1.335 +objid_attr = attribute objid { objid } 
   1.336 +objid      = text 
   1.337 +
   1.338 +objstate = 
   1.339 +  ( "unparseable" | "parsed" | "being_processed" | "processed" | "outdated" )
   1.340 +
   1.341 +
   1.342 +# ==============================================================================
   1.343 +#  4. Prover Configuration
   1.344 +# ==============================================================================
   1.345 +
   1.346 +proverconfig =      
   1.347 +   askpgip			# what version of PGIP do you support?
   1.348 + | askpgml			# what version of PGML do you support?
   1.349 + | askconfig			# tell me about objects and operations
   1.350 + | askprefs			# what preference settings do you offer?
   1.351 + | setpref			# please set this preference value 
   1.352 + | getpref			# please tell me this preference value
   1.353 +
   1.354 +
   1.355 +
   1.356 +prefcat_attr = attribute prefcategory { text}   # e.g. "expert", "internal", etc.
   1.357 +                                                # could be used for tabs in dialog
   1.358 +
   1.359 +askpgip   = element askpgip   { empty }
   1.360 +askpgml   = element askpgml   { empty }
   1.361 +askconfig = element askconfig { empty }
   1.362 +askprefs  = element askprefs  { prefcat_attr? }
   1.363 +setpref   = element setpref   { name_attr, prefcat_attr?, pgipvalue }
   1.364 +getpref   = element getpref   { name_attr, prefcat_attr? }
   1.365 +
   1.366 + 
   1.367 +
   1.368 +# ==============================================================================
   1.369 +#  5. Interface Configuration
   1.370 +# ==============================================================================
   1.371 +
   1.372 +kitconfig =        
   1.373 +    usespgip			# I support PGIP, version ..
   1.374 +  | usespgml			# I support PGML, version ..
   1.375 +  | pgmlconfig			# configure PGML symbols
   1.376 +  | proverinfo			# Report assistant information
   1.377 +  | hasprefs			# I have preference settings ...
   1.378 +  | prefval			# the current value of a preference is
   1.379 +  | displayconfig		# configure the following object types and operations
   1.380 +  | setids			# inform the interface about some known objects
   1.381 +  | addids			# add some known identifiers
   1.382 +  | delids			# retract some known identifers
   1.383 +  | idvalue			# display the value of some identifier
   1.384 +  | menuadd			# add a menu entry
   1.385 +  | menudel			# remove a menu entry
   1.386 +
   1.387 +# version reporting
   1.388 +version_attr  = attribute version { text }
   1.389 +usespgml = element usespgml  { version_attr }
   1.390 +usespgip = element usespgip  { version_attr 
   1.391 +	                     , activecompspec
   1.392 +			     }
   1.393 +
   1.394 +# These data from the component spec which an active component can override, or which
   1.395 +# components initiating contact with the broker (e.g. incoming socket connections).
   1.396 +# There are some restrictions: if we start a tool, the componentid and the type must be the
   1.397 +# same as initially specified.
   1.398 +activecompspec =  ( componentid_attr?   # unique identifier of component class
   1.399 +	          , componentname_attr? # Textual name of this component (overrides initial spec)
   1.400 +		  , componenttype?      # Type of component
   1.401 +		  , acceptedpgipelems?  # list of accepted elements
   1.402 +		  )
   1.403 +
   1.404 +
   1.405 +acceptedpgipelems = element acceptedpgipelems { singlepgipelem* }
   1.406 +
   1.407 +singlepgipelem    = element pgipelem { 
   1.408 +   attribute async { xsd:boolean }?,  # true if this command supported asynchronously (deflt false)
   1.409 +   text }                             # (otherwise part of ready/sync stream)
   1.410 +
   1.411 +# PGML configuration
   1.412 +pgmlconfig = element pgmlconfig { pgmlconfigure+ }
   1.413 +
   1.414 +# Types for config settings: corresponding data values should conform to canonical
   1.415 +# representation for corresponding XML Schema 1.0 Datatypes.  (This representation is verbose
   1.416 +# but helps for error checking later)
   1.417 +#
   1.418 +# In detail:
   1.419 +#  pgipbool   = xsd:boolean = true | false
   1.420 +#  pgipint    = xsd:integer = (-)?(0-9)+     (canonical: no leading zeroes)
   1.421 +#  pgipstring = xsd:string  =  <any character sequence>
   1.422 +#  pgipchoice = cf xs:choice  = type1 | type2 | ... | typen
   1.423 +
   1.424 +pgiptype   = pgipbool | pgipint | pgipstring | pgipchoice | pgipconst
   1.425 +pgipbool   = element pgipbool { empty }
   1.426 +
   1.427 +pgipint    = element pgipint  { min_attr?, max_attr?, empty }
   1.428 +min_attr   = attribute min { xsd:integer }
   1.429 +max_attr   = attribute max { xsd:integer }
   1.430 +pgipstring = element pgipstring { empty }
   1.431 +pgipchoice = element pgipchoice { pgiptype+ }
   1.432 +pgipconst  = element pgipconst { name_attr?, text }
   1.433 +
   1.434 +pgipvalue  = text
   1.435 +
   1.436 +icon  = element icon { xsd:base64Binary }  # image data for an icon
   1.437 +
   1.438 +default_attr = attribute default { text }
   1.439 +descr_attr   = attribute descr { text }
   1.440 +
   1.441 +# icons for preference recommended size: 32x32 
   1.442 +# top level preferences: may be used in dialog for preference setting
   1.443 +# object preferences: may be used as an "emblem" to decorate 
   1.444 +# object icon (boolean preferences with default false, only)
   1.445 +haspref = element haspref  { 
   1.446 +   name_attr, descr_attr?, 
   1.447 +   default_attr?, icon?,
   1.448 +   pgiptype
   1.449 +}
   1.450 +
   1.451 +hasprefs = element hasprefs { prefcat_attr?, haspref* }
   1.452 +
   1.453 +prefval = element prefval { name_attr, pgipvalue } 
   1.454 +
   1.455 +# menu items (incomplete, FIXME)
   1.456 +path_attr = attribute path { text }
   1.457 +
   1.458 +menuadd  = element menuadd  { path_attr?, name_attr?, opn_attr? }
   1.459 +menudel  = element menudel  { path_attr?, name_attr? }
   1.460 +opn_attr = attribute operation { token }
   1.461 +
   1.462 +
   1.463 +# Display configuration information: 
   1.464 +# basic prover information, lexical structure of files, 
   1.465 +# an icon for the prover, help documents, and the 
   1.466 +# objects, types, and operations for building proof commands.
   1.467 +
   1.468 +# NB: the following object types have a fixed interpretation 
   1.469 +# in PGIP:  "comment", "theorem", "theory", "file" 
   1.470 +
   1.471 +displayconfig =
   1.472 +  element displayconfig { 
   1.473 +     welcomemsg?, icon?, helpdoc*, lexicalstructure*,
   1.474 +     objtype*, opn* }
   1.475 +
   1.476 +objtype = element objtype { name_attr, descr_attr?, icon?, hasprefs?, contains* }
   1.477 +
   1.478 +objtype_attr = attribute objtype { token }           # the name of an objtype
   1.479 +contains = element contains { objtype_attr, empty }  #  a container for other objtypes
   1.480 +
   1.481 +opn   = element opn { name_attr, inputform?, opsrc, optrg, opcmd, improper_attr? }
   1.482 +
   1.483 +opsrc = element opsrc { list { token* } }  # source types: a space separated list
   1.484 +optrg = element optrg { token }?           # single target type, empty for proof command
   1.485 +opcmd = element opcmd { text }             # prover command, with printf-style "%1"-args
   1.486 +
   1.487 +# interactive operations - require some input
   1.488 +inputform = element inputform { field+ }  
   1.489 +
   1.490 +# a field has a PGIP config type (int, string, bool, choice(c1...cn)) and a name; under that
   1.491 +# name, it will be substituted into the command Ex. field name=number opcmd="rtac %1 %number"
   1.492 +
   1.493 +field = element field { 
   1.494 +   name_attr, pgiptype,
   1.495 +   element prompt { text }
   1.496 +}
   1.497 +
   1.498 +# identifier tables: these list known items of particular objtype.
   1.499 +# Might be used for completion or menu selection, and inspection.
   1.500 +# May have a nested structure (but objtypes do not).
   1.501 +
   1.502 +setids  = element setids { idtable* }   # (with an empty idtable, clear table)
   1.503 +addids  = element addids { idtable* }
   1.504 +delids  = element delids { idtable* }
   1.505 +
   1.506 +# give value of some identifier (response to showid)
   1.507 +idvalue = element idvalue               
   1.508 +   {  name_attr, objtype_attr, pgmltext }
   1.509 +
   1.510 +idtable    = element idtable { context_attr?, objtype_attr, identifier* }
   1.511 +identifier = element identifier { token }
   1.512 +
   1.513 +context_attr = attribute context { token } # parent identifier (context) 
   1.514 +
   1.515 +instance_attr = attribute instance { text }
   1.516 +
   1.517 +# prover information: 
   1.518 +# name, instance (e.g. in case of major parameter of invocation);
   1.519 +# description, version, homepage,  welcome message, docs available
   1.520 +proverinfo = element proverinfo 
   1.521 +   { name_attr, version_attr?, instance_attr?,
   1.522 +     descr_attr?, url_attr?, filenameextns_attr?, 
   1.523 +## TEMP: these elements are duplicated in displayconfig, as they're
   1.524 +## moving there.  
   1.525 +      welcomemsg?, icon?, helpdoc*, lexicalstructure* }
   1.526 +
   1.527 +welcomemsg = element welcomemsg { text }
   1.528 +
   1.529 +# helpdoc: advertise availability of some documentation, given a canonical
   1.530 +# name, textual description, and URL or viewdoc argument.
   1.531 +# 
   1.532 +helpdoc = element helpdoc { name_attr, descr_attr, url_attr?, text } # text is arg to "viewdoc"
   1.533 +
   1.534 +filenameextns_attr = attribute filenameextns { objnames }
   1.535 +
   1.536 +# lexical structure of proof texts
   1.537 +lexicalstructure = 
   1.538 +   element lexicalstructure {
   1.539 +      keyword*,
   1.540 +      stringdelimiter*,
   1.541 +      escapecharacter?,
   1.542 +      commentdelimiter*,
   1.543 +      identifiersyntax?
   1.544 +   }
   1.545 +
   1.546 +keyword = element keyword {
   1.547 +   attribute word { text },
   1.548 +   shorthelp?,
   1.549 +   longhelp? }
   1.550 +
   1.551 +shorthelp = element shorthelp { text }   # one-line (tooltip style) help 
   1.552 +longhelp  = element longhelp { text }    # multi-line help
   1.553 +
   1.554 +stringdelimiter = element stringdelimiter { text }  # should be a single char
   1.555 +
   1.556 +# The escape character is used to escape strings and other special characters - in most languages it is \
   1.557 +escapecharacter = element escapecharacter { text }  # should be a single char
   1.558 +
   1.559 +commentdelimiter = element commentdelimiter { 
   1.560 +   attribute start { text },
   1.561 +   attribute end { text }?,
   1.562 +   empty
   1.563 +  }
   1.564 +
   1.565 +
   1.566 +# syntax for ids: id = initial allowed*  or id = allowed+ if initial empty
   1.567 +identifiersyntax = element identifiersyntax { 
   1.568 +   attribute initialchars { text }?,
   1.569 +   attribute allowedchars { text }
   1.570 +}
   1.571 +
   1.572 +# ==============================================================================
   1.573 +# 6. Prover Control
   1.574 +# ==============================================================================
   1.575 +
   1.576 +provercontrol = 
   1.577 +   proverinit			# reset prover to its initial state
   1.578 + | proverexit			# exit prover
   1.579 + | startquiet			# stop prover sending proof state displays, non-urgent messages
   1.580 + | stopquiet			# turn on normal proof state & message displays
   1.581 + | pgmlsymbolson		# activate use of symbols in PGML output (input always understood)
   1.582 + | pgmlsymbolsoff		# deactivate use of symbols in PGML output
   1.583 +
   1.584 +proverinit     = element proverinit { empty }  
   1.585 +proverexit     = element proverexit { empty }
   1.586 +startquiet     = element startquiet { empty }  
   1.587 +stopquiet      = element stopquiet  { empty }  
   1.588 +pgmlsymbolson  = element pgmlsymbolson { empty }
   1.589 +pgmlsymbolsoff = element pgmlsymbolsoff { empty }
   1.590 +
   1.591 +
   1.592 +# General prover output/responses
   1.593 +
   1.594 +# Nearly all prover output has an optional proverid attribute, except for the one which is 
   1.595 +# never seen by any display. This is set by the Broker to indicate the originating or referring
   1.596 +# prover. 
   1.597 +# Displays rendering these messages can rely on this attribute being set.
   1.598 +
   1.599 +proveroutput =
   1.600 +   ready			# prover is ready for input
   1.601 + | cleardisplay			# prover requests a display area to be cleared
   1.602 + | proofstate			# prover outputs the proof state
   1.603 + | normalresponse		# prover outputs some display
   1.604 + | errorresponse		# prover indicates an error/warning/debug condition, with message
   1.605 + | scriptinsert			# some text to insert literally into the proof script
   1.606 + | metainforesponse		# prover outputs some other meta-information to interface
   1.607 + | parseresult			# results of a <parsescript> request (see later)
   1.608 +
   1.609 +ready = element ready { empty }
   1.610 +
   1.611 +displayarea = "status"		# a status line
   1.612 +	    | "message"		# the message area (e.g. response buffer)
   1.613 +            | "display"		# the main display area (e.g. goals buffer)
   1.614 +	    | token		# prover-specified window name
   1.615 +
   1.616 +cleardisplay = 
   1.617 +   element cleardisplay {
   1.618 +      proverid_attr?,
   1.619 +      attribute area { 
   1.620 +         displayarea | "all" } }           
   1.621 +
   1.622 +
   1.623 +proofstate = 
   1.624 +  element proofstate { proverid_attr?, pgml }
   1.625 +
   1.626 +messagecategory =		# attribution of message
   1.627 +   "internal"			#  - internal debug message (interface should usually hide)
   1.628 + | "information"		#  - user-level debug/info message (interface may hide)
   1.629 + | "tracing"			#  - user-level "tracing" message (possibly voluminous)
   1.630 +
   1.631 +normalresponse =                           
   1.632 +  element normalresponse { 
   1.633 +    proverid_attr?,
   1.634 +    attribute area { displayarea },
   1.635 +    attribute messagecategory { messagecategory }?, # optional extra category (e.g. tracing/debug)
   1.636 +    attribute urgent { "y" }?,                      # indication that message must be displayed
   1.637 +    pgmltext 
   1.638 +}
   1.639 +
   1.640 +## Error messages:  these are different from ordinary messages in that
   1.641 +##		    they indicate an error condition in the prover, with a notion
   1.642 +##		    of fatality and (optionally) a location.  The interface may collect these
   1.643 +##		    messages in a log, display in a modal dialog, or in the specified
   1.644 +##		    display area if one is specified.
   1.645 +
   1.646 +errorresponse = 
   1.647 +   element errorresponse { 
   1.648 +     proverid_attr?,
   1.649 +     attribute area { displayarea }?,
   1.650 +     attribute fatality { fatality },
   1.651 +     location_attrs,
   1.652 +     pgmltext
   1.653 +  }
   1.654 +
   1.655 +fatality =	  # degree of error conditions:
   1.656 +   "nonfatal"     #  - warning message (interface should show message)
   1.657 + | "fatal"        #  - error message (interface must show message)
   1.658 + | "panic"        #  - shutdown condition, component exits (interface may show message)
   1.659 + | "log"          #  - log message (interface must not show message, write to broker log file)
   1.660 + | "debug"        #  - debug message (interface may show message, write to broker log file)
   1.661 +		   ## FIXME da: wondering if this is more appropriate than normal/internal above
   1.662 +
   1.663 +
   1.664 +# attributes describing a file location (for error messages, etc)
   1.665 +location_attrs = 
   1.666 +     attribute location_descr    { text }?,
   1.667 +     attribute location_url      { xsd:anyURI }?,
   1.668 +     attribute locationline      { xsd:positiveInteger }?,
   1.669 +     attribute locationcolumn    { xsd:positiveInteger }?,
   1.670 +     attribute locationcharacter { xsd:positiveInteger }?
   1.671 +
   1.672 +scriptinsert = element scriptinsert { proverid_attr?, metavarid_attr?, text }
   1.673 +
   1.674 +
   1.675 +# metainformation is an extensible place to put system-specific information
   1.676 +
   1.677 +value = element value { name_attr?, text }   # generic value holder
   1.678 +
   1.679 +metainforesponse = 
   1.680 +   element metainforesponse { 
   1.681 +      proverid_attr?,
   1.682 +      attribute infotype { text },      # categorization of data
   1.683 +      value* }                          # data values
   1.684 +
   1.685 +
   1.686 +# ==============================================================================
   1.687 +# 7. Proof script markup and proof control 
   1.688 +# ==============================================================================
   1.689 +
   1.690 +# properproofcmds are purely markup on native proof script text
   1.691 +properproofcmd =
   1.692 +    opengoal        # open a goal in ambient context
   1.693 +  | proofstep       # a specific proof command (perhaps configured via opcmd) 
   1.694 +  | closegoal       # complete & close current open proof (succeeds iff proven, may close nested pf)
   1.695 +  | giveupgoal      # close current open proof, retaining attempt in script (Isar oops)
   1.696 +  | postponegoal    # close current open proof, record as proof obl'n  (Isar sorry)  
   1.697 +  | comment         # a proof script comment; text probably ignored by prover 
   1.698 +  | whitespace      # a whitespace comment; text ignored by prover
   1.699 +  | spuriouscmd     # command ignored for undo, e.g. "print x", could be pruned from script
   1.700 +  | badcmd          # a command which should not be stored in the script (e.g. an improperproofcmd)
   1.701 +  | litcomment      # a literate comment (never passed to prover)
   1.702 +  | pragma	    # a document generating instruction (never passed to prover)
   1.703 +
   1.704 +# improperproofcmds are commands which are never stored in the script
   1.705 +improperproofcmd =
   1.706 +    dostep        # issue a properproofcmd (without passing in markup)
   1.707 +  | undostep      # undo the last proof step issued in currently open goal 
   1.708 +  | redostep      # redo the last undone step issued in currently open goal (optionally supported)
   1.709 +  | abortgoal     # give up on current open proof, close proof state, discard history
   1.710 +  | forget        # forget a theorem (or named target), outdating dependent theorems
   1.711 +  | restoregoal   # re-open previously postponed proof, outdating dependent theorems
   1.712 +
   1.713 +opengoal     = element opengoal     { display_attr?, thmname_attr?, text } # FIXME: add objprefval
   1.714 +proofstep    = element proofstep    { display_attr?, name_attr?, objtype_attr?, text }
   1.715 +closegoal    = element closegoal    { display_attr?, text }
   1.716 +giveupgoal   = element giveupgoal   { display_attr?, text }
   1.717 +postponegoal = element postponegoal { display_attr?, text }
   1.718 +comment      = element comment      { display_attr?, text }
   1.719 +whitespace   = element whitespace   { display_attr?, text }
   1.720 +
   1.721 +display_attr = attribute nodisplay { xsd:boolean }  # whether to display in documentation
   1.722 +
   1.723 +spuriouscmd  = element spuriouscmd { text }
   1.724 +badcmd       = element badcmd { text }
   1.725 +
   1.726 +litcomment  = element litcomment { format_attr?, (text | directive)* }
   1.727 +directive   = element directive { (proofctxt,pgml) }
   1.728 +format_attr = attribute format { token }
   1.729 +
   1.730 +pragma       = showhidecode | setformat
   1.731 +showhidecode = element showcode { attribute show { xsd:boolean } }
   1.732 +setformat    = element setformat { format_attr }
   1.733 +
   1.734 +dostep       = element dostep { text }
   1.735 +undostep     = element undostep { empty }
   1.736 +redostep     = element redostep { empty }
   1.737 +abortgoal    = element abortgoal { empty }
   1.738 +forget       = element forget { thyname_attr?, name_attr?, objtype_attr? }
   1.739 +restoregoal  = element restoregoal { thmname_attr }
   1.740 +
   1.741 +# empty objprefval element is used for object prefs in script markup 
   1.742 +objprefval = element objprefval { name_attr, val_attr, empty }
   1.743 +val_attr   = attribute value { text }
   1.744 +
   1.745 +
   1.746 +
   1.747 +
   1.748 +# =======================================================
   1.749 +# Inspecting the proof context, etc.
   1.750 +
   1.751 +proofctxt =
   1.752 +    askids         # please tell me about identifiers (given objtype in a theory)
   1.753 +  | showid         # print value of an object
   1.754 +  | askguise       # please tell me about the current state of the prover
   1.755 +  | parsescript    # parse a raw proof script into proofcmds
   1.756 +  | showproofstate # (re)display proof state (empty if outside a proof)
   1.757 +  | showctxt       # show proof context
   1.758 +  | searchtheorems # search for theorems (prover-specific arguments)  
   1.759 +  | setlinewidth   # set line width for printing
   1.760 +  | viewdoc        # request some on-line help (prover-specific arg)
   1.761 +
   1.762 +askids = element askids  { thyname_attr?, objtype_attr? }
   1.763 +	# Note that thyname_attr is *required* for certain objtypes (e.g. theorem).
   1.764 +	# This is because otherwise the list is enormous.
   1.765 +	# Perhaps we should make thyname_attr obligatory? 
   1.766 +	# With a blank entry (i.e. thyname="") allowed for listing theories, or for when 
   1.767 +	# you really do want to see everything.
   1.768 +
   1.769 +showid = element showid  { thyname_attr?, objtype_attr, name_attr }
   1.770 +
   1.771 +askguise = element askguise { empty }
   1.772 +
   1.773 +
   1.774 +# =======================================================
   1.775 +# Parsing proof scripts
   1.776 +
   1.777 +# NB: parsing needs only be supported for "proper" proof commands,
   1.778 +# which may appear in proof texts.  The groupdelimiters are purely
   1.779 +# markup hints to the interface for display structure on concrete syntax.
   1.780 +# The location attributes can be used by the prover in <parsescript> to
   1.781 +# generate error messages for particular locations; they can be used 
   1.782 +# in <parseresult> to pass position information back to the display,
   1.783 +# particularly in the case of (re-)parsing only part of a file.
   1.784 +# The parsing component MUST return the same location attributes
   1.785 +# (and system data attribute) that was passed in.
   1.786 +
   1.787 +parsescript = element parsescript
   1.788 +                 { location_attrs, systemdata_attr, text }
   1.789 +       
   1.790 +parseresult = element parseresult { location_attrs, systemdata_attr,
   1.791 +				    singleparseresult* }
   1.792 +
   1.793 +singleparseresult  = properscriptcmd | unparseable | errorresponse
   1.794 +
   1.795 +unparseable = element unparseable { text }
   1.796 +properscriptcmd = properproofcmd | properfilecmd | groupdelimiter
   1.797 +
   1.798 +
   1.799 +groupdelimiter = openblock | closeblock
   1.800 +openblock  = element openblock { metavarid_attr? }
   1.801 +closeblock = element closeblock { empty }
   1.802 +
   1.803 +# 
   1.804 +metavarid_attr = attribute metavarid { token }
   1.805 +
   1.806 +showproofstate = element showproofstate { empty }
   1.807 +showctxt       = element showctxt { empty }
   1.808 +searchtheorems = element searchtheorems { text }
   1.809 +setlinewidth   = element setlinewidth { xsd:positiveInteger }
   1.810 +viewdoc        = element viewdoc { text }
   1.811 +
   1.812 +
   1.813 +# =======================================================
   1.814 +# Theory/file handling
   1.815 +
   1.816 +properfilecmd =     # (NB: properfilecmds are purely markup on proof script text)
   1.817 +    opentheory      # begin construction of a new theory.  
   1.818 +  | theoryitem      # a step in a theory (e.g. declaration/definition of type/constant).
   1.819 +  | closetheory     # complete construction of the currently open theory
   1.820 +
   1.821 +improperfilecmd = 
   1.822 +    doitem	    # issue a proper file command (without passing in markup)
   1.823 +  | undoitem	    # undo last step (or named item) in theory construction
   1.824 +  | redoitem	    # redo last step (or named item) in theory construction (optionally supported)
   1.825 +  | aborttheory     # abort currently open theory
   1.826 +  | retracttheory   # retract a named theory
   1.827 +  | openfile        # lock a file for constructing a proof text 
   1.828 +  | closefile       # unlock a file, suggesting it has been processed
   1.829 +  | abortfile       # unlock a file, suggesting it hasn't been processed
   1.830 +  | loadfile        # load a file possibly containing theory definition(s)
   1.831 +  | changecwd       # change prover's working directory (or load path) for files
   1.832 +  | systemcmd       # system (other) command, parsed internally
   1.833 +
   1.834 +fileinfomsg = 
   1.835 +   informfileloaded       # prover informs interface a particular file is loaded
   1.836 + | informfileretracted    # prover informs interface a particular file is outdated
   1.837 + | informguise		  # prover informs interface about current state
   1.838 +
   1.839 +opentheory    = element opentheory    { thyname_attr, parentnames_attr?, text }
   1.840 +closetheory   = element closetheory   { text }
   1.841 +theoryitem    = element theoryitem    { name_attr?, objtype_attr?, text } # FIXME: add objprefval
   1.842 +
   1.843 +doitem        = element doitem        { text } 
   1.844 +undoitem      = element undoitem      { name_attr?, objtype_attr? } 
   1.845 +redoitem      = element redoitem      { name_attr?, objtype_attr? } 
   1.846 +aborttheory   = element aborttheory   { empty }
   1.847 +retracttheory = element retracttheory { thyname_attr }
   1.848 +
   1.849 +parentnames_attr = attribute parentnames { objnames }
   1.850 +
   1.851 +
   1.852 +# Below, url_attr will often be a file URL.  We assume for now that
   1.853 +# the prover and interface are running on same filesystem.
   1.854 +#
   1.855 +
   1.856 +openfile      = element openfile  { url_attr }	    # notify begin reading from given file
   1.857 +closefile     = element closefile { empty }	    # notify currently open file is complete
   1.858 +abortfile     = element abortfile { empty }	    # notify currently open file is discarded
   1.859 +loadfile      = element loadfile  { url_attr }	    # ask prover to read file directly
   1.860 +changecwd     = element changecwd { dir_attr }	    # ask prover to change current working dir
   1.861 +
   1.862 +# this one not yet implemented, but would be handy.  Perhaps could be 
   1.863 +# locatethy/locatefile instead.
   1.864 +#locateobj     = element locateobj { name_attr, objtype_attr } # ask prover for file defining obj
   1.865 +
   1.866 +informfileloaded    = element informfileloaded    { url_attr }  # prover indicates a processed file
   1.867 +informfileretracted = element informfileretracted { url_attr }  # prover indicates an undone file
   1.868 +informfilelocation  = element informfilelocation  { url_attr }  # response to locateobj
   1.869 +
   1.870 +informguise = 
   1.871 +   element informguise {
   1.872 +      element guisefile { url_attr }?,
   1.873 +      element guisetheory { thyname_attr }?,
   1.874 +      element guiseproof { thmname_attr?, proofpos_attr? }?
   1.875 +   }
   1.876 +
   1.877 +proofpos_attr = attribute proofpos { xsd:nonNegativeInteger }
   1.878 +
   1.879 +systemcmd     = element systemcmd     { text }		# "shell escape", arbitrary prover command!
   1.880 +
   1.881 +# ==============================================================================
   1.882 +# 8. Internal messages-- only used between communicating brokers.
   1.883 +# ==============================================================================
   1.884 +internalmsg  = launchcomp | stopcomp | registercomp | compstatus
   1.885 +
   1.886 +launchcomp   = element launchcomponent { componentspec }
   1.887 +	               # request to start an instance of this component remotely
   1.888 +stopcomp     = element stopcomponent { attribute sessionid { string } }
   1.889 +                       # request to stop component with this session id remotely
   1.890 +
   1.891 +registercomp = element registercomponent { activecompspec } 
   1.892 +                       # component has been started successfully
   1.893 +compstatus   = element componentstatus { componentstatus_attr    # status
   1.894 +	                               , componentid_attr?       # component id (for failure)
   1.895 +	                               , element text { text }?  # user-visible error message
   1.896 +				       , element info { text }?  # Additional info for log files.
   1.897 +				       }	
   1.898 +                       # component status: failed to start, or exited
   1.899 +
   1.900 +componentstatus_attr = attribute status { ("fail"   # component failed to start
   1.901 + 		                          |"exit"  # component exited
   1.902 +					  )}	
   1.903 +
   1.904 +# Local variables:
   1.905 +# fill-column: 95
   1.906 +# End:
   1.907 +# ==============================================================================
   1.908 +# end of `pgip.rnc'.
   1.909 +