lib/ProofGeneral/pgip.rnc
author blanchet
Fri Apr 26 12:09:51 2013 +0200 (2013-04-26)
changeset 51790 22517d04d20b
parent 33686 8e33ca8832b1
permissions -rw-r--r--
more intuitive syntax for equality-style discriminators of nullary constructors
aspinall@17735
     1
# 
aspinall@17735
     2
# RELAX NG Schema for PGIP, the Proof General Interface Protocol                   
aspinall@17735
     3
# 
aspinall@17735
     4
# Authors:  David Aspinall, LFCS, University of Edinburgh       
aspinall@23434
     5
#           Christoph Lüth, University of Bremen       
aspinall@17735
     6
#
aspinall@17735
     7
# Status:   Prototype.
aspinall@17735
     8
#
aspinall@17735
     9
# For additional commentary, see accompanying commentary document available at
aspinall@17735
    10
# http://proofgeneral.inf.ed.ac.uk/Kit/docs/commentary.pdf
aspinall@17735
    11
#
aspinall@17735
    12
# Advertised version: 2.0
aspinall@17735
    13
# 
aspinall@17735
    14
# Contents
aspinall@17735
    15
# ========
aspinall@17735
    16
#
aspinall@17735
    17
#  0. Prelude
aspinall@17735
    18
#  1. Top-level 
aspinall@17735
    19
#  2. Component Control messages
aspinall@17735
    20
#  3. Display Commands
aspinall@17735
    21
#  4. Prover Configuration
aspinall@17735
    22
#  5. Interface Configuration
aspinall@17735
    23
#  6. Prover Control
aspinall@17735
    24
#  7. Proof script markup and proof control
aspinall@17735
    25
#
aspinall@23434
    26
#
aspinall@23434
    27
# ===============================================================================
aspinall@23434
    28
#
aspinall@23434
    29
# Note on datatypes.  (see e.g. http://books.xmlschemata.org/relaxng):
aspinall@23434
    30
#
aspinall@23434
    31
#  token  : any string possibly with spaces, but spaces are normalised/collapsed
aspinall@23434
    32
#	    (i.e. tokenised).  Same as XML Schema xs:token
aspinall@23434
    33
#  string : any string, whitespaces preserved.  Same as XML Schema xs:string
aspinall@23434
    34
#	    (NB: attributes are normalised by XML 1.0 parsers so
aspinall@23434
    35
#	     spaces/newlines must be quoted)
aspinall@23434
    36
#  text	  : text nodes/mixed content (whitespace may be lost in mixed content)
aspinall@23434
    37
#
aspinall@23434
    38
# So: attributes should usually be tokens or more restrictive; (sometimes: strings for printing)
aspinall@23434
    39
#     element contents may be string (preserving whitespace), token (tokenising), 
aspinall@23434
    40
#       or text (which may contain further nodes).
aspinall@17735
    41
aspinall@17735
    42
# ==============================================================================
aspinall@17735
    43
# 0. Prelude
aspinall@17735
    44
# ==============================================================================
aspinall@17735
    45
aspinall@17735
    46
include "pgml.rnc"                           # include PGML grammar
aspinall@17735
    47
aspinall@23434
    48
name_attr = attribute name { token }         # names are user-level textual identifiers (space-collapsed)
aspinall@23434
    49
thyname_attr = attribute thyname { token }   # names for theories (special case of name)
aspinall@23434
    50
thmname_attr = attribute thmname { token }   # names for theorems (special case of name)
aspinall@17735
    51
aspinall@17735
    52
datetime_attr = 
aspinall@17735
    53
   attribute datetime { xsd:dateTime }       # CCYY-MM-DDHH:MM:SS plus timezone info
aspinall@17735
    54
url_attr  = attribute url { xsd:anyURI }     # URLs  (often as "file:///localfilename.extn")
aspinall@23434
    55
dir_attr  = attribute dir { string }         # Unix-style directory name (no final slash)
aspinall@17735
    56
aspinall@17735
    57
systemdata_attr  = 
aspinall@23434
    58
            attribute systemdata { token }?   # system-specific data (useful for "stateless" RPC)
aspinall@17735
    59
aspinall@23434
    60
objname = token	     # an identifier name (convention: any characters except semi-colon)
aspinall@23434
    61
objnames = token     # sequence of names in an attribute: semi-colon separated
aspinall@17735
    62
aspinall@23434
    63
#objnames = string                            # A sequence of objnames
aspinall@23434
    64
#termobjname  = string { pattern = "[^;]+;" }  # unfortunately these declarations don't 
aspinall@23434
    65
#objnames = objname | (termobjname, objname)
aspinall@17735
    66
#objnames = objname+                               #  work with the RNC->DTD tool trang
aspinall@17735
    67
aspinall@17735
    68
aspinall@17735
    69
# ==============================================================================
aspinall@17735
    70
# 1. Top-level Messages/documents
aspinall@17735
    71
# ==============================================================================
aspinall@17735
    72
aspinall@17735
    73
start = pgip                                 # Single message
aspinall@17735
    74
      | pgips                                # A log of messages between components
aspinall@17735
    75
      | displayconfig                        # displayconfig as a standalone element
aspinall@17735
    76
      | pgipconfig                           # pgipconfig as a standalone element
aspinall@23434
    77
      | pgipdoc                              # A proof script document 
aspinall@17735
    78
aspinall@17735
    79
pgip = element pgip {                        #  A PGIP packet contains:
aspinall@17735
    80
   pgip_attrs,                               #   - attributes with header information;
aspinall@17735
    81
   (toprovermsg | todisplaymsg |             #   - a message with one of four channel types
aspinall@17735
    82
    fromprovermsg | fromdisplaymsg 
aspinall@17735
    83
   | internalmsg ) 
aspinall@17735
    84
  }
aspinall@17735
    85
aspinall@17735
    86
pgips = element pgips { pgip+ }
aspinall@17735
    87
aspinall@17735
    88
pgip_attrs =
aspinall@23434
    89
 attribute tag { token }?,                  # message tag, e.g. name of origin component (diagnostic)
aspinall@23434
    90
 attribute id { token },                    # (unique) session id of this component 
aspinall@23434
    91
 attribute destid { token }?,               # session id of destination component
aspinall@17735
    92
 attribute class { pgip_class },            # general categorization of message
aspinall@23434
    93
 attribute refid { token }?,                # component id this message responds to (usually destid)
aspinall@17735
    94
 attribute refseq { xsd:positiveInteger }?, # message sequence this message responds to
aspinall@17735
    95
 attribute seq { xsd:positiveInteger }      # sequence number of this message
aspinall@17735
    96
aspinall@23434
    97
pgip_class = "pg"      # message sent TO proof general broker (e.g. FROM proof assistant).
aspinall@17735
    98
           | "pa"      # message sent TO the proof assistant/other component
aspinall@17735
    99
           | "pd"      # message sent TO display/front-end components
aspinall@17735
   100
aspinall@17735
   101
toprovermsg =          # Messages sent to the prover (class "pa"):
aspinall@17735
   102
   proverconfig        #   query Prover configuration, triggering interface configuration
aspinall@17735
   103
 | provercontrol       #   control some aspect of Prover
aspinall@17735
   104
 | improperproofcmd    #   issue a proof command 
aspinall@17735
   105
 | improperfilecmd     #   issue a file command
aspinall@17735
   106
 | properproofcmd      #   [ NB: not strictly needed: input PGIP processing not expected ]
aspinall@17735
   107
 | properfilecmd       #   [ NB: not strictly needed: input PGIP processing not expected ]
aspinall@17735
   108
 | proofctxt           #   issue a context command
aspinall@17735
   109
aspinall@17735
   110
fromprovermsg =        # Messages from the prover to PG (class "pg"):
aspinall@17735
   111
   kitconfig           #   messages to configure the interface 
aspinall@17735
   112
 | proveroutput        #   output messages from the prover, usually display in interface
aspinall@17735
   113
 | fileinfomsg         #   information messages concerning file-system access / prover state
aspinall@17735
   114
aspinall@17735
   115
todisplaymsg =         # Messages sent to display components (class "pd"):
aspinall@17735
   116
   brokermsg           #   status reports from broker
aspinall@17735
   117
 | dispmsg             #   display commands
aspinall@17735
   118
                       #   - Further, all fromprovermsg can be relayed to display
aspinall@17735
   119
aspinall@17735
   120
fromdisplaymsg =       # Messages sent from display components (class "pg"):
aspinall@17735
   121
   dispcmd             #   display messages 
aspinall@17735
   122
 | brokercontrol       #   messages controlling broker & prover processes
aspinall@17735
   123
		       #   - Further, all toprovermsg to be relayed to prover
aspinall@17735
   124
aspinall@17735
   125
# ===========================================================================
aspinall@17735
   126
# 2. Component Control
aspinall@17735
   127
# ===========================================================================
aspinall@17735
   128
aspinall@17735
   129
#
aspinall@17735
   130
# Idea:  - broker knows how to manage some components (inc provers) as child processes,
aspinall@17735
   131
#          communicate via pipes.  Configured by a fixed PGIP config file read on startup.
aspinall@17735
   132
#        - other components may connect to running broker
aspinall@17735
   133
#
aspinall@17735
   134
# TODO: - describe startup protocol for component connecting to to running broker dynamically.
aspinall@17735
   135
aspinall@17735
   136
# This is the element contained in the configuration file read by the 
aspinall@17735
   137
# broker on startup.
aspinall@17735
   138
pgipconfig = element pgipconfig { componentspec* }
aspinall@17735
   139
aspinall@17735
   140
componentspec = 
aspinall@17735
   141
   element componentspec {
aspinall@17735
   142
      componentid_attr,         # Unique identifier for component class
aspinall@17735
   143
      componentname_attr,       # Textual name of component class
aspinall@17735
   144
      componenttype,            # Type of component: prover, display, auxiliary
aspinall@23434
   145
      startupattrs,		# Describing startup behaviour
aspinall@23434
   146
      systemattrs,              # System attributes for component
aspinall@17735
   147
      componentconnect          # How to connect to component
aspinall@17735
   148
   }
aspinall@17735
   149
aspinall@17735
   150
componentid_attr   = attribute componentid   { token }
aspinall@23434
   151
componentname_attr = attribute componentname { token }
aspinall@17735
   152
aspinall@17735
   153
componenttype = element componenttype {
aspinall@17735
   154
     provercomponent 
aspinall@17735
   155
   | displaycomponent 
aspinall@17735
   156
 # | filehandlercomponent 
aspinall@17735
   157
   | parsercomponent 
aspinall@17735
   158
   | othercomponent }
aspinall@17735
   159
aspinall@17735
   160
provercomponent  = element provercomponent { empty }
aspinall@17735
   161
displaycomponent = element displaycomponent { attribute active { xsd:boolean}? }
aspinall@17735
   162
parsercomponent  = element parsercomponent  { componentid_attr }
aspinall@17735
   163
othercomponent   = element othercomponent { empty }
aspinall@17735
   164
aspinall@17735
   165
componentconnect =
aspinall@17735
   166
   componentsubprocess | componentsocket | connectbyproxy
aspinall@17735
   167
aspinall@17735
   168
componentsubprocess = 
aspinall@23434
   169
   element syscommand { string }
aspinall@17735
   170
componentsocket = 
aspinall@23434
   171
   (element host { token }, element port { xsd:positiveInteger })
aspinall@17735
   172
connectbyproxy = 
aspinall@23434
   173
   (element proxy { attribute host { token }    # Host to connect to
aspinall@17735
   174
		  , attribute connect { 
aspinall@17735
   175
                           "rsh" | "ssh" # Launch proxy via RSH or SSH, needs
aspinall@17735
   176
			                 # authentication 
aspinall@17735
   177
                         | "server"  # connect to running proxy on given port
aspinall@17735
   178
                         }?
aspinall@23434
   179
                  , attribute user { token } ? # user to connect as with RSH/SSH
aspinall@23434
   180
                  , attribute path { token } ? # path of pgipkit on remote
aspinall@23434
   181
		  , attribute port { xsd:positiveInteger } ? # port to connect to running proxy
aspinall@17735
   182
		  , componentconnect
aspinall@17735
   183
		  })
aspinall@17735
   184
aspinall@23434
   185
# Attributes describing when to start the component.
aspinall@23434
   186
startupattrs =
aspinall@23434
   187
  attribute startup {		# what to do on broker startup:
aspinall@17735
   188
             "boot"   |		# always start this component (default with displays)
aspinall@17735
   189
             "manual" |		# start manually (default with provers)
aspinall@23434
   190
             "ignore"		# never start this component
aspinall@17735
   191
             }?
aspinall@23434
   192
aspinall@23434
   193
# System attributes describing behaviour of component. 
aspinall@23434
   194
systemattrs = (
aspinall@23434
   195
    attribute timeout { xsd:integer }?  # timeout for communications
aspinall@23434
   196
  , attribute sync { xsd:boolean }?     # whether to wait for ready
aspinall@23434
   197
  , attribute nestedgoals { xsd:boolean}? # Does prover allow nested goals?
aspinall@23434
   198
  )
aspinall@17735
   199
aspinall@17735
   200
# Control commands from display to broker
aspinall@17735
   201
brokercontrol = 
aspinall@17735
   202
    launchprover		# Launch a new prover
aspinall@17735
   203
  | exitprover			# Request to terminate a running prover
aspinall@17735
   204
  | restartprover		# Request to restart/reset a running prover
aspinall@17735
   205
  | proversquery		# Query about known provers, running provers
aspinall@17735
   206
  | shutdownbroker		# Ask broker to exit (should be wary of this!)
aspinall@17735
   207
  | brokerstatusquery		# Ask broker for status report
aspinall@17735
   208
  | pgipconfig			# Send config to broker
aspinall@17735
   209
aspinall@17735
   210
provername_attr    = attribute provername { provername }
aspinall@17735
   211
provername         = token
aspinall@17735
   212
aspinall@17735
   213
proverid_attr     = attribute proverid  { proverid }
aspinall@17735
   214
proverid          = token
aspinall@17735
   215
aspinall@17735
   216
launchprover      = element launchprover { componentid_attr }
aspinall@17735
   217
exitprover        = element exitprover { proverid_attr }
aspinall@17735
   218
restartprover     = element restartprover { proverid_attr }
aspinall@17735
   219
proversquery      = element proversavailable { empty }
aspinall@17735
   220
brokerstatusquery = element brokerstatusquery { empty } 
aspinall@17735
   221
shutdownbroker    = element shutdownbroker { attribute force { xsd:boolean }? } 
aspinall@17735
   222
aspinall@17735
   223
# Control messages from broker to interface
aspinall@17735
   224
brokermsg  = 
aspinall@17735
   225
    brokerstatus		# response to brokerstatusquery:
aspinall@17735
   226
  | proveravailmsg		# announce new prover is available
aspinall@17735
   227
  | newprovermsg		# new prover has started 
aspinall@17735
   228
  | proverstatemsg		# prover state has changed (busy/ready/exit)
aspinall@17735
   229
aspinall@17735
   230
brokerstatus  = element brokerstatus 
aspinall@17735
   231
                       { knownprovers, runningprovers, brokerinformation }
aspinall@17735
   232
aspinall@17735
   233
knownprover   = element knownprover   { componentid_attr, provername }
aspinall@23434
   234
runningprover = element runningprover { componentid_attr, proverid_attr, provername }
aspinall@17735
   235
aspinall@17735
   236
knownprovers   = element knownprovers { knownprover* }
aspinall@17735
   237
runningprovers = element runningprovers { runningprover* }
aspinall@23434
   238
brokerinformation = element brokerinformation { string }
aspinall@17735
   239
aspinall@17735
   240
proveravailmsg  = element proveravailable { provername_attr,
aspinall@17735
   241
                                            componentid_attr }
aspinall@23434
   242
newprovermsg    = element proverstarted { proverid_attr
aspinall@23434
   243
					, componentid_attr
aspinall@23434
   244
		                        , provername_attr
aspinall@23434
   245
		                        }
aspinall@17735
   246
proverstatemsg = element proverstate { 
aspinall@17735
   247
                       proverid_attr, provername_attr,
aspinall@17735
   248
                       attribute proverstate {proverstate} } 
aspinall@17735
   249
aspinall@17735
   250
proverstate    = ("ready" | "busy" | "exitus")
aspinall@17735
   251
aspinall@17735
   252
# FIXME: This only allows provers to be available which are configured.
aspinall@17735
   253
#        In the long run, we want to change configurations while running.
aspinall@17735
   254
aspinall@17735
   255
aspinall@17735
   256
# ===========================================================================
aspinall@17735
   257
# 3. Display Commands
aspinall@17735
   258
# ===========================================================================
aspinall@17735
   259
aspinall@17735
   260
# Messages exchanged between broker and display
aspinall@17735
   261
aspinall@17735
   262
                        
aspinall@17735
   263
dispcmd = dispfilecmd | dispobjcmd  # display commands go from display to broker
aspinall@17735
   264
dispmsg = dispfilemsg | dispobjmsg  # display messages go from broker to display
aspinall@17735
   265
   
aspinall@17735
   266
aspinall@17735
   267
dispfilecmd = 
aspinall@17735
   268
    loadparsefile		# parse and load file
aspinall@17735
   269
  | newfilewith			# create new source file with given text
aspinall@17735
   270
  | dispopenfile		# open (or create) new file 
aspinall@17735
   271
  | savefile			# save opened file
aspinall@17735
   272
  | discardfile			# discard changes to opened file
aspinall@17735
   273
aspinall@17735
   274
dispfilemsg =
aspinall@17735
   275
    newfile			# announce creation of new file (in response to load/open)
aspinall@23434
   276
  | filestatus			# announce change in status of file in broker
aspinall@17735
   277
aspinall@17735
   278
# unique identifier of loaded files
aspinall@23434
   279
srcid_attr = attribute srcid { token }
aspinall@17735
   280
aspinall@17735
   281
loadparsefile = element loadparsefile { url_attr, proverid_attr }
aspinall@23434
   282
newfilewith   = element newfilewith   { url_attr, proverid_attr, string }
aspinall@17735
   283
dispopenfile  = element dispopenfile { url_attr,
aspinall@17735
   284
                                       proverid_attr,
aspinall@17735
   285
                                       attribute overwrite { xsd:boolean }?}
aspinall@17735
   286
savefile      = element savefile { srcid_attr,     
aspinall@17735
   287
                                   url_attr? }
aspinall@17735
   288
discardfile   = element discardfile { srcid_attr }
aspinall@17735
   289
aspinall@17735
   290
newfile       = element newfile  { proverid_attr, srcid_attr, url_attr }
aspinall@23434
   291
filestatus    = element filestatus  { proverid_attr, srcid_attr, newstatus_attr, url_attr?,
aspinall@17735
   292
				      datetime_attr} 
aspinall@17735
   293
aspinall@17735
   294
newstatus_attr = attribute newstatus { "saved" | "changed" | "discarded" }
aspinall@17735
   295
aspinall@17735
   296
dispobjcmd =
aspinall@17735
   297
    setobjstate			# request of change of state 
aspinall@23434
   298
  | editobj			# request edit operation of objects
aspinall@17735
   299
  | createobj			# request creation of new objects
aspinall@23434
   300
# Suggested May 06: probably add re-load flags instead 
aspinall@23434
   301
#  | reloadobjs                  # request relisting of all objects
aspinall@17735
   302
  | inputcmd		        # process the command (generated by an input event)
aspinall@17735
   303
  | interruptprover		# send interrupt or kill signal to prover
aspinall@17735
   304
aspinall@17735
   305
dispobjmsg = element dispobjmsg { 
aspinall@17735
   306
      newobj+			# new objects have been created
aspinall@17735
   307
    | delobj+			# objects have been deleted
aspinall@17735
   308
    | replaceobjs		# objects are being replaced
aspinall@17735
   309
    | objectstate+		# objects have changed state
aspinall@17735
   310
    }
aspinall@17735
   311
aspinall@17735
   312
newobj = element newobj {
aspinall@17735
   313
	    proverid_attr,
aspinall@17735
   314
            srcid_attr, 
aspinall@17735
   315
	    objid_attr, 
aspinall@17735
   316
            attribute objposition { objid } ?,
aspinall@17735
   317
            objtype_attr ?,
aspinall@17735
   318
            attribute objparent { objid }?,
aspinall@17735
   319
            attribute objstate { objstate },
aspinall@23434
   320
	    # FIXME: would like to include metainfo here
aspinall@23434
   321
            # as (properscriptcmd, metainfo*) | unparseable
aspinall@17735
   322
            (properscriptcmd | unparseable) }
aspinall@17735
   323
aspinall@17735
   324
replaceobjs = element replaceobjs {
aspinall@17735
   325
	                srcid_attr,
aspinall@17735
   326
	                attribute replacedfrom { objid }? ,
aspinall@17735
   327
			attribute replacedto { objid }?,
aspinall@23434
   328
                        delobj*,    # actually, either of delobj or 
aspinall@23434
   329
                        newobj* }   # newobj can be empty but not both.
aspinall@17735
   330
aspinall@17735
   331
delobj = element delobj   { proverid_attr, srcid_attr, objid_attr }
aspinall@17735
   332
aspinall@17735
   333
objectstate = element objstate
aspinall@17735
   334
                       { proverid_attr, srcid_attr, objid_attr,
aspinall@17735
   335
                         attribute newstate {objstate} }
aspinall@17735
   336
aspinall@17735
   337
setobjstate = element setobjstate
aspinall@17735
   338
                  {  objid_attr, attribute newstate {objstate} }
aspinall@17735
   339
aspinall@17735
   340
editobj = element editobj { srcid_attr ?,
aspinall@17735
   341
	                    attribute editfrom { objid }?,
aspinall@17735
   342
                            attribute editto   { objid }?,
aspinall@23434
   343
                            string }
aspinall@17735
   344
createobj = element createobj { srcid_attr ?, 
aspinall@17735
   345
                                attribute objposition { objid }?, 
aspinall@23434
   346
                                string }
aspinall@17735
   347
aspinall@23434
   348
# Suggested May 06: probably add re-load flags instead 
aspinall@23434
   349
# reloadobjs = element reloadobjs { srcid_attr }
aspinall@23434
   350
aspinall@23434
   351
inputcmd       = element inputcmd { improper_attr, string }
aspinall@17735
   352
improper_attr  = attribute improper { xsd:boolean }
aspinall@17735
   353
aspinall@17735
   354
interruptprover = element interruptprover 
aspinall@17735
   355
                          { interruptlevel_attr, proverid_attr }
aspinall@17735
   356
aspinall@17735
   357
interruptlevel_attr  = attribute interruptlevel { "interrupt" | "stop" | "kill" }
aspinall@17735
   358
aspinall@17735
   359
objid_attr = attribute objid { objid } 
aspinall@23434
   360
objid      = token 
aspinall@17735
   361
aspinall@17735
   362
objstate = 
aspinall@17735
   363
  ( "unparseable" | "parsed" | "being_processed" | "processed" | "outdated" )
aspinall@17735
   364
aspinall@17735
   365
aspinall@17735
   366
# ==============================================================================
aspinall@17735
   367
#  4. Prover Configuration
aspinall@17735
   368
# ==============================================================================
aspinall@17735
   369
aspinall@17735
   370
proverconfig =      
aspinall@17735
   371
   askpgip			# what version of PGIP do you support?
aspinall@17735
   372
 | askpgml			# what version of PGML do you support?
aspinall@17735
   373
 | askconfig			# tell me about objects and operations
aspinall@17735
   374
 | askprefs			# what preference settings do you offer?
aspinall@17735
   375
 | setpref			# please set this preference value 
aspinall@17735
   376
 | getpref			# please tell me this preference value
aspinall@17735
   377
aspinall@17735
   378
aspinall@17735
   379
aspinall@23434
   380
prefcat_attr = attribute prefcategory { token }   # e.g. "expert", "internal", etc.
aspinall@23434
   381
                                                      # could be used for tabs in dialog
aspinall@17735
   382
aspinall@17735
   383
askpgip   = element askpgip   { empty }
aspinall@17735
   384
askpgml   = element askpgml   { empty }
aspinall@17735
   385
askconfig = element askconfig { empty }
aspinall@17735
   386
askprefs  = element askprefs  { prefcat_attr? }
aspinall@17735
   387
setpref   = element setpref   { name_attr, prefcat_attr?, pgipvalue }
aspinall@17735
   388
getpref   = element getpref   { name_attr, prefcat_attr? }
aspinall@17735
   389
aspinall@17735
   390
 
aspinall@17735
   391
aspinall@17735
   392
# ==============================================================================
aspinall@17735
   393
#  5. Interface Configuration
aspinall@17735
   394
# ==============================================================================
aspinall@17735
   395
aspinall@17735
   396
kitconfig =        
aspinall@17735
   397
    usespgip			# I support PGIP, version ..
aspinall@17735
   398
  | usespgml			# I support PGML, version ..
aspinall@17735
   399
  | pgmlconfig			# configure PGML symbols
aspinall@17735
   400
  | proverinfo			# Report assistant information
aspinall@17735
   401
  | hasprefs			# I have preference settings ...
aspinall@17735
   402
  | prefval			# the current value of a preference is
aspinall@17735
   403
  | displayconfig		# configure the following object types and operations
aspinall@17735
   404
  | setids			# inform the interface about some known objects
aspinall@17735
   405
  | addids			# add some known identifiers
aspinall@17735
   406
  | delids			# retract some known identifers
aspinall@17735
   407
  | idvalue			# display the value of some identifier
aspinall@17735
   408
  | menuadd			# add a menu entry
aspinall@17735
   409
  | menudel			# remove a menu entry
aspinall@17735
   410
aspinall@17735
   411
# version reporting
aspinall@23434
   412
version_attr  = attribute version { token }
aspinall@17735
   413
usespgml = element usespgml  { version_attr }
aspinall@17735
   414
usespgip = element usespgip  { version_attr 
aspinall@17735
   415
	                     , activecompspec
aspinall@17735
   416
			     }
aspinall@17735
   417
aspinall@17735
   418
# These data from the component spec which an active component can override, or which
aspinall@17735
   419
# components initiating contact with the broker (e.g. incoming socket connections).
aspinall@17735
   420
# There are some restrictions: if we start a tool, the componentid and the type must be the
aspinall@17735
   421
# same as initially specified.
aspinall@17735
   422
activecompspec =  ( componentid_attr?   # unique identifier of component class
aspinall@17735
   423
	          , componentname_attr? # Textual name of this component (overrides initial spec)
aspinall@17735
   424
		  , componenttype?      # Type of component
aspinall@23434
   425
		  , systemattrs         # system attributes
aspinall@17735
   426
		  , acceptedpgipelems?  # list of accepted elements
aspinall@17735
   427
		  )
aspinall@17735
   428
aspinall@17735
   429
aspinall@17735
   430
acceptedpgipelems = element acceptedpgipelems { singlepgipelem* }
aspinall@17735
   431
aspinall@17735
   432
singlepgipelem    = element pgipelem { 
aspinall@17735
   433
   attribute async { xsd:boolean }?,  # true if this command supported asynchronously (deflt false)
aspinall@23434
   434
				      # (otherwise part of usual ready/sync stream)
aspinall@23434
   435
   attribute attributes { text }?,    # comma-separated list of supported optional attribute names
aspinall@23434
   436
				      # useful for: times attribute
aspinall@23434
   437
   text }                             # the unadorned name of the PGIP element (*not* an element)
aspinall@17735
   438
aspinall@17735
   439
# PGML configuration
aspinall@17735
   440
pgmlconfig = element pgmlconfig { pgmlconfigure+ }
aspinall@17735
   441
aspinall@17735
   442
# Types for config settings: corresponding data values should conform to canonical
aspinall@23434
   443
# representation for corresponding XML Schema 1.0 Datatypes.  
aspinall@17735
   444
#
aspinall@17735
   445
# In detail:
aspinall@23434
   446
#  pgipnull   = empty
aspinall@17735
   447
#  pgipbool   = xsd:boolean = true | false
aspinall@17735
   448
#  pgipint    = xsd:integer = (-)?(0-9)+     (canonical: no leading zeroes)
aspinall@23434
   449
#  pgipstring = string  =  <any non-empty character sequence>
aspinall@17735
   450
#  pgipchoice = cf xs:choice  = type1 | type2 | ... | typen
aspinall@17735
   451
aspinall@23434
   452
pgiptype   = pgipnull | pgipbool | pgipint | pgipstring | pgipchoice | pgipconst
aspinall@17735
   453
aspinall@23434
   454
pgipnull   = element pgipnull { descr_attr?, empty }
aspinall@23434
   455
pgipbool   = element pgipbool { descr_attr?, empty }
aspinall@23434
   456
pgipint    = element pgipint  { min_attr?, max_attr?, descr_attr?, empty }
aspinall@17735
   457
min_attr   = attribute min { xsd:integer }
aspinall@17735
   458
max_attr   = attribute max { xsd:integer }
aspinall@23434
   459
pgipstring = element pgipstring { descr_attr?, empty }
aspinall@23434
   460
pgipconst  = element pgipconst { name_attr, descr_attr? } 
aspinall@23434
   461
      # FIXME: Temporary fix because Isabelle does it wrong -- should be empty }
aspinall@17735
   462
pgipchoice = element pgipchoice { pgiptype+ }
aspinall@17735
   463
aspinall@23434
   464
# Notes on pgipchoice:
aspinall@23434
   465
# 1. Choices must not be nested (i.e. must not contain other choices)
aspinall@23434
   466
# 2. The description attributes for pgipbool, pgipint, pgipstring and pgipconst
aspinall@23434
   467
#    are for use with pgipchoice: they can be used as a user-visible label
aspinall@23434
   468
#    when representing the choice to the user (e.g. in a pull-down menu).
aspinall@23434
   469
# 3. A pgipchoice should have an unambiguous representation as a string. That means
aspinall@23434
   470
#    all constants in the choice must have different names, and a choice must not
aspinall@23434
   471
#    contain more than one each of pgipint, pgipstring and pgipbool.
aspinall@23434
   472
aspinall@23434
   473
pgipvalue  = string
aspinall@17735
   474
aspinall@17735
   475
icon  = element icon { xsd:base64Binary }  # image data for an icon
aspinall@17735
   476
aspinall@23434
   477
# The default value of a preference as a string (using the unambiguous
aspinall@23434
   478
# conversion to string mentioned above). A string value will always be quoted
aspinall@23434
   479
# to distinguish it from constants or integers.
aspinall@23434
   480
default_attr = attribute default { token }
aspinall@23434
   481
aspinall@23434
   482
# Description of a choice.  If multi-line, first line is short tip.
aspinall@23434
   483
descr_attr   = attribute descr { string }
aspinall@17735
   484
aspinall@17735
   485
# icons for preference recommended size: 32x32 
aspinall@17735
   486
# top level preferences: may be used in dialog for preference setting
aspinall@17735
   487
# object preferences: may be used as an "emblem" to decorate 
aspinall@17735
   488
# object icon (boolean preferences with default false, only)
aspinall@17735
   489
haspref = element haspref  { 
aspinall@17735
   490
   name_attr, descr_attr?, 
aspinall@17735
   491
   default_attr?, icon?,
aspinall@17735
   492
   pgiptype
aspinall@17735
   493
}
aspinall@17735
   494
aspinall@23434
   495
aspinall@23434
   496
aspinall@17735
   497
hasprefs = element hasprefs { prefcat_attr?, haspref* }
aspinall@17735
   498
aspinall@17735
   499
prefval = element prefval { name_attr, pgipvalue } 
aspinall@17735
   500
aspinall@17735
   501
# menu items (incomplete, FIXME)
aspinall@23434
   502
path_attr = attribute path { token }
aspinall@17735
   503
aspinall@17735
   504
menuadd  = element menuadd  { path_attr?, name_attr?, opn_attr? }
aspinall@17735
   505
menudel  = element menudel  { path_attr?, name_attr? }
aspinall@17735
   506
opn_attr = attribute operation { token }
aspinall@17735
   507
aspinall@17735
   508
aspinall@17735
   509
# Display configuration information: 
aspinall@17735
   510
# basic prover information, lexical structure of files, 
aspinall@17735
   511
# an icon for the prover, help documents, and the 
aspinall@17735
   512
# objects, types, and operations for building proof commands.
aspinall@17735
   513
aspinall@17735
   514
# NB: the following object types have a fixed interpretation 
aspinall@23434
   515
# in PGIP:
aspinall@23434
   516
#        "identifier":   an identifier in the identifier syntax
aspinall@23434
   517
#           "comment":   an arbitrary sequence of characters
aspinall@23434
   518
#	    "theorem":   a theorem name or text
aspinall@23434
   519
#	    "theory" :   a theory name or text
aspinall@23434
   520
#	    "file" :     a file name
aspinall@17735
   521
aspinall@17735
   522
displayconfig =
aspinall@17735
   523
  element displayconfig { 
aspinall@17735
   524
     welcomemsg?, icon?, helpdoc*, lexicalstructure*,
aspinall@17735
   525
     objtype*, opn* }
aspinall@17735
   526
aspinall@23434
   527
objtype = element objtype { name_attr, descr_attr?, icon?,  contains*, hasprefs?  }
aspinall@17735
   528
aspinall@17735
   529
objtype_attr = attribute objtype { token }           # the name of an objtype
aspinall@17735
   530
contains = element contains { objtype_attr, empty }  #  a container for other objtypes
aspinall@17735
   531
aspinall@23434
   532
opn = element opn { 
aspinall@23434
   533
   name_attr, 
aspinall@23434
   534
   descr_attr?,
aspinall@23434
   535
   inputform?,	  # FIXME: can maybe remove this?
aspinall@23434
   536
   opsrc*,	  # FIXME: incompat change wanted: have list of source elts, not spaces
aspinall@23434
   537
   optrg, 
aspinall@23434
   538
   opcmd, 
aspinall@23434
   539
   improper_attr? }
aspinall@17735
   540
aspinall@23434
   541
opsrc = 
aspinall@23434
   542
   element opsrc {	  
aspinall@23434
   543
      name_attr?,         # %name as an alternative to %number
aspinall@23434
   544
      selnumber_attr?,    # explicit number for %number, the nth item selected
aspinall@23434
   545
      prompt_attr?,	  # prompt in form or tooltip in template
aspinall@23434
   546
      listwithsep_attr?,  # list of args of this type with given separator
aspinall@23434
   547
      list { token* } }   # source types: a space separated list
aspinall@23434
   548
			  # FIXME incompat change wanted: just have one source here
aspinall@23434
   549
			  # FIXME: need to add optional pgiptype
aspinall@23434
   550
aspinall@23434
   551
listwithsep_attr =  attribute listwithsep { token }
aspinall@23434
   552
selnumber_attr =    attribute selnumber { xsd:positiveInteger }
aspinall@23434
   553
prompt_attr =       attribute prompt { string }
aspinall@23434
   554
aspinall@23434
   555
optrg = 
aspinall@23434
   556
   element optrg { token }?           # single target type, empty for proof command
aspinall@23434
   557
opcmd = 
aspinall@23434
   558
   element opcmd { string }           # prover command, with printf-style "%1"-args
aspinall@23434
   559
					   #  (whitespace preserved here: literal text)
aspinall@17735
   560
aspinall@17735
   561
# interactive operations - require some input
aspinall@17735
   562
inputform = element inputform { field+ }  
aspinall@17735
   563
aspinall@17735
   564
# a field has a PGIP config type (int, string, bool, choice(c1...cn)) and a name; under that
aspinall@17735
   565
# name, it will be substituted into the command Ex. field name=number opcmd="rtac %1 %number"
aspinall@17735
   566
aspinall@17735
   567
field = element field { 
aspinall@17735
   568
   name_attr, pgiptype,
aspinall@23434
   569
   element prompt { string }
aspinall@17735
   570
}
aspinall@17735
   571
aspinall@17735
   572
# identifier tables: these list known items of particular objtype.
aspinall@17735
   573
# Might be used for completion or menu selection, and inspection.
aspinall@17735
   574
# May have a nested structure (but objtypes do not).
aspinall@17735
   575
aspinall@17735
   576
setids  = element setids { idtable* }   # (with an empty idtable, clear table)
aspinall@17735
   577
addids  = element addids { idtable* }
aspinall@17735
   578
delids  = element delids { idtable* }
aspinall@17735
   579
aspinall@23434
   580
# give value of some identifier (response to showid; same values returned)
aspinall@17735
   581
idvalue = element idvalue               
aspinall@23434
   582
   {  thyname_attr?, name_attr, objtype_attr, pgmltext }
aspinall@17735
   583
aspinall@17735
   584
idtable    = element idtable { context_attr?, objtype_attr, identifier* }
aspinall@17735
   585
identifier = element identifier { token }
aspinall@17735
   586
aspinall@17735
   587
context_attr = attribute context { token } # parent identifier (context) 
aspinall@17735
   588
aspinall@17735
   589
# prover information: 
aspinall@17735
   590
# name, instance (e.g. in case of major parameter of invocation);
aspinall@17735
   591
# description, version, homepage,  welcome message, docs available
aspinall@17735
   592
proverinfo = element proverinfo 
aspinall@17735
   593
   { name_attr, version_attr?, instance_attr?,
aspinall@17735
   594
     descr_attr?, url_attr?, filenameextns_attr?, 
aspinall@17735
   595
## TEMP: these elements are duplicated in displayconfig, as they're
aspinall@17735
   596
## moving there.  
aspinall@17735
   597
      welcomemsg?, icon?, helpdoc*, lexicalstructure* }
aspinall@17735
   598
aspinall@23434
   599
instance_attr = attribute instance { token }
aspinall@23434
   600
aspinall@23434
   601
welcomemsg = element welcomemsg { string }
aspinall@17735
   602
aspinall@17735
   603
# helpdoc: advertise availability of some documentation, given a canonical
aspinall@17735
   604
# name, textual description, and URL or viewdoc argument.
aspinall@17735
   605
# 
aspinall@23434
   606
helpdoc = element helpdoc { name_attr, descr_attr, url_attr?, token } # token string is arg to "viewdoc"
aspinall@17735
   607
aspinall@23434
   608
filenameextns_attr = attribute filenameextns { xsd:NMTOKENS } # space-separated extensions sans "."
aspinall@17735
   609
aspinall@17735
   610
# lexical structure of proof texts
aspinall@17735
   611
lexicalstructure = 
aspinall@17735
   612
   element lexicalstructure {
aspinall@17735
   613
      keyword*,
aspinall@17735
   614
      stringdelimiter*,
aspinall@17735
   615
      escapecharacter?,
aspinall@17735
   616
      commentdelimiter*,
aspinall@17735
   617
      identifiersyntax?
aspinall@17735
   618
   }
aspinall@17735
   619
aspinall@17735
   620
keyword = element keyword {
aspinall@23434
   621
   attribute word { token },
aspinall@17735
   622
   shorthelp?,
aspinall@17735
   623
   longhelp? }
aspinall@17735
   624
aspinall@23434
   625
shorthelp = element shorthelp { string }   # one-line (tooltip style) help 
aspinall@23434
   626
longhelp  = element longhelp { string }    # multi-line help
aspinall@17735
   627
aspinall@23434
   628
stringdelimiter = element stringdelimiter { token }  # should be a single char
aspinall@17735
   629
aspinall@17735
   630
# The escape character is used to escape strings and other special characters - in most languages it is \
aspinall@23434
   631
escapecharacter = element escapecharacter { token }  # should be a single char
aspinall@17735
   632
aspinall@17735
   633
commentdelimiter = element commentdelimiter { 
aspinall@23434
   634
   attribute start { token },
aspinall@23434
   635
   attribute end { token }?,
aspinall@17735
   636
   empty
aspinall@17735
   637
  }
aspinall@17735
   638
aspinall@17735
   639
aspinall@17735
   640
# syntax for ids: id = initial allowed*  or id = allowed+ if initial empty
aspinall@17735
   641
identifiersyntax = element identifiersyntax { 
aspinall@23434
   642
   attribute initialchars { token }?,
aspinall@23434
   643
   attribute allowedchars { token }
aspinall@17735
   644
}
aspinall@17735
   645
aspinall@17735
   646
# ==============================================================================
aspinall@17735
   647
# 6. Prover Control
aspinall@17735
   648
# ==============================================================================
aspinall@17735
   649
aspinall@17735
   650
provercontrol = 
aspinall@17735
   651
   proverinit			# reset prover to its initial state
aspinall@17735
   652
 | proverexit			# exit prover
aspinall@17735
   653
 | startquiet			# stop prover sending proof state displays, non-urgent messages
aspinall@17735
   654
 | stopquiet			# turn on normal proof state & message displays
aspinall@17735
   655
 | pgmlsymbolson		# activate use of symbols in PGML output (input always understood)
aspinall@17735
   656
 | pgmlsymbolsoff		# deactivate use of symbols in PGML output
aspinall@23434
   657
 | setproverflag		# set/clear a standard control flag (supersedes above)
aspinall@17735
   658
aspinall@17735
   659
proverinit     = element proverinit { empty }  
aspinall@17735
   660
proverexit     = element proverexit { empty }
aspinall@23434
   661
startquiet     = element startquiet { empty }      # DEPRECATED 
aspinall@23434
   662
stopquiet      = element stopquiet  { empty }      # DEPRECATED 
aspinall@23434
   663
pgmlsymbolson  = element pgmlsymbolson { empty }   # DEPRECATED
aspinall@23434
   664
pgmlsymbolsoff = element pgmlsymbolsoff { empty }  # DEPRECATED
aspinall@17735
   665
aspinall@23434
   666
setproverflag  = element setproverflag { flagname_attr, 
aspinall@23434
   667
					 attribute value { xsd:boolean } }
aspinall@23434
   668
flagname_attr  = 
aspinall@23434
   669
   attribute flagname { "quiet" 
aspinall@23434
   670
		      | "pgmlsymbols" 
aspinall@23434
   671
		      | "metainfo:thmdeps" 
aspinall@23434
   672
		      }
aspinall@17735
   673
aspinall@17735
   674
# General prover output/responses
aspinall@17735
   675
aspinall@23434
   676
# Prover output has an otional proverid_attribute. This is set by the broker when relaying 
aspinall@23434
   677
# prover output to displays. When producing output, provers can and should not set this
aspinall@23434
   678
# attribute. 
aspinall@17735
   679
aspinall@17735
   680
proveroutput =
aspinall@17735
   681
   ready			# prover is ready for input
aspinall@17735
   682
 | cleardisplay			# prover requests a display area to be cleared
aspinall@17735
   683
 | proofstate			# prover outputs the proof state
aspinall@17735
   684
 | normalresponse		# prover outputs some display
aspinall@17735
   685
 | errorresponse		# prover indicates an error/warning/debug condition, with message
aspinall@17735
   686
 | scriptinsert			# some text to insert literally into the proof script
aspinall@17735
   687
 | metainforesponse		# prover outputs some other meta-information to interface
aspinall@17735
   688
 | parseresult			# results of a <parsescript> request (see later)
aspinall@17735
   689
aspinall@17735
   690
ready = element ready { empty }
aspinall@17735
   691
aspinall@17735
   692
displayarea = "status"		# a status line
aspinall@23434
   693
	    | "message"		# the message area (e.g. response buffer, perhaps swapped into view)
aspinall@23434
   694
            | "display"		# the main display area (e.g. goals buffer, usually persistent)
aspinall@17735
   695
	    | token		# prover-specified window name
aspinall@17735
   696
aspinall@17735
   697
cleardisplay = 
aspinall@17735
   698
   element cleardisplay {
aspinall@17735
   699
      proverid_attr?,
aspinall@17735
   700
      attribute area { 
aspinall@17735
   701
         displayarea | "all" } }           
aspinall@17735
   702
aspinall@17735
   703
aspinall@17735
   704
proofstate = 
aspinall@17735
   705
  element proofstate { proverid_attr?, pgml }
aspinall@17735
   706
aspinall@17735
   707
messagecategory =		# attribution of message
aspinall@17735
   708
   "internal"			#  - internal debug message (interface should usually hide)
aspinall@17735
   709
 | "information"		#  - user-level debug/info message (interface may hide)
aspinall@17735
   710
 | "tracing"			#  - user-level "tracing" message (possibly voluminous)
aspinall@17735
   711
aspinall@17735
   712
normalresponse =                           
aspinall@17735
   713
  element normalresponse { 
aspinall@23434
   714
    proverid_attr?,				    # if no proverid, assume message is from broker
aspinall@17735
   715
    attribute area { displayarea },
aspinall@17735
   716
    attribute messagecategory { messagecategory }?, # optional extra category (e.g. tracing/debug)
aspinall@23434
   717
    attribute urgent { xsd:boolean }?,              # message should be brought to users attention
aspinall@17735
   718
    pgmltext 
aspinall@17735
   719
}
aspinall@17735
   720
aspinall@17735
   721
## Error messages:  these are different from ordinary messages in that
aspinall@23434
   722
## they indicate an error condition in the prover, with a notion
aspinall@23434
   723
## of fatality and (optionally) a location.  The interface may collect these
aspinall@23434
   724
## messages in a log, display in a modal dialog, or in the specified
aspinall@23434
   725
## display area if one is given
aspinall@23434
   726
## 
aspinall@23434
   727
## Error responses are also taken to indicate failure of a command to be processed, but only in
aspinall@23434
   728
## the special case of a response with fatality "fatal".  If any errorresponse with
aspinall@23434
   729
## fatality=fatal is sent before <ready/>, the PGIP command which triggered the message is
aspinall@23434
   730
## considered to have failed.  If the command is a scripting command, it will not be added to
aspinall@23434
   731
## the successfully processed part of the document.  A "nonfatal" error also indicates some
aspinall@23434
   732
## serious problem with the sent command, but it is not considered to have failed.  This is the
aspinall@23434
   733
## ordinary response for
aspinall@17735
   734
aspinall@17735
   735
errorresponse = 
aspinall@17735
   736
   element errorresponse { 
aspinall@23434
   737
     proverid_attr?,				   #  ... as above ...
aspinall@17735
   738
     attribute area { displayarea }?,
aspinall@17735
   739
     attribute fatality { fatality },
aspinall@17735
   740
     location_attrs,
aspinall@17735
   741
     pgmltext
aspinall@17735
   742
  }
aspinall@17735
   743
aspinall@17735
   744
fatality =	  # degree of error conditions:
aspinall@23434
   745
   "info"	  #  - info message
aspinall@23434
   746
 | "warning"      #  - warning message
aspinall@23434
   747
 | "nonfatal"     #  - error message, recovered and state updated
aspinall@23434
   748
 | "fatal"        #  - error message, command has failed
aspinall@17735
   749
 | "panic"        #  - shutdown condition, component exits (interface may show message)
aspinall@23434
   750
 | "log"          #  - system-level log message (interface does not show message; written to log file)
aspinall@23434
   751
 | "debug"        #  - system-level debug message (interface may show message; written to log file)
aspinall@17735
   752
aspinall@17735
   753
# attributes describing a file location (for error messages, etc)
aspinall@17735
   754
location_attrs = 
aspinall@23434
   755
     attribute location_descr    { string }?,
aspinall@17735
   756
     attribute location_url      { xsd:anyURI }?,
aspinall@17735
   757
     attribute locationline      { xsd:positiveInteger }?,
aspinall@17735
   758
     attribute locationcolumn    { xsd:positiveInteger }?,
aspinall@23434
   759
     attribute locationcharacter { xsd:positiveInteger }?,
aspinall@23434
   760
     attribute locationlength    { xsd:positiveInteger }?
aspinall@17735
   761
aspinall@23434
   762
# instruction to insert some literal text into the document
aspinall@23434
   763
scriptinsert = element scriptinsert { proverid_attr?, metavarid_attr?, string }
aspinall@17735
   764
aspinall@17735
   765
aspinall@17735
   766
# metainformation is an extensible place to put system-specific information
aspinall@17735
   767
aspinall@23434
   768
value = element value { name_attr?, text }        # generic value holder [ deprecated: use metainfo ]
aspinall@23434
   769
metainfo = element metainfo { name_attr?, text }  # generic info holder
aspinall@17735
   770
aspinall@17735
   771
metainforesponse = 
aspinall@17735
   772
   element metainforesponse { 
aspinall@17735
   773
      proverid_attr?,
aspinall@23434
   774
      attribute infotype { token },      # categorization of data
aspinall@23434
   775
      (value | metainfo)* }              # data values/text
aspinall@17735
   776
aspinall@17735
   777
aspinall@17735
   778
# ==============================================================================
aspinall@17735
   779
# 7. Proof script markup and proof control 
aspinall@17735
   780
# ==============================================================================
aspinall@17735
   781
aspinall@23434
   782
# properproofcmds are purely markup on native proof script (plain) text
aspinall@17735
   783
properproofcmd =
aspinall@17735
   784
    opengoal        # open a goal in ambient context
aspinall@17735
   785
  | proofstep       # a specific proof command (perhaps configured via opcmd) 
aspinall@17735
   786
  | closegoal       # complete & close current open proof (succeeds iff proven, may close nested pf)
aspinall@17735
   787
  | giveupgoal      # close current open proof, retaining attempt in script (Isar oops)
aspinall@17735
   788
  | postponegoal    # close current open proof, record as proof obl'n  (Isar sorry)  
aspinall@17735
   789
  | comment         # a proof script comment; text probably ignored by prover 
aspinall@23434
   790
  | doccomment      # a proof script document comment; text maybe processed by prover 
aspinall@17735
   791
  | whitespace      # a whitespace comment; text ignored by prover
aspinall@17735
   792
  | spuriouscmd     # command ignored for undo, e.g. "print x", could be pruned from script
aspinall@17735
   793
  | badcmd          # a command which should not be stored in the script (e.g. an improperproofcmd)
aspinall@23434
   794
  | litcomment      # a PGIP literate comment (never passed to prover)
aspinall@17735
   795
  | pragma	    # a document generating instruction (never passed to prover)
aspinall@17735
   796
aspinall@17735
   797
# improperproofcmds are commands which are never stored in the script
aspinall@17735
   798
improperproofcmd =
aspinall@17735
   799
    dostep        # issue a properproofcmd (without passing in markup)
aspinall@17735
   800
  | undostep      # undo the last proof step issued in currently open goal 
aspinall@17735
   801
  | redostep      # redo the last undone step issued in currently open goal (optionally supported)
aspinall@17735
   802
  | abortgoal     # give up on current open proof, close proof state, discard history
aspinall@17735
   803
  | forget        # forget a theorem (or named target), outdating dependent theorems
aspinall@17735
   804
  | restoregoal   # re-open previously postponed proof, outdating dependent theorems
aspinall@17735
   805
aspinall@23434
   806
# In future we may allow input to contain markup; for now it is treated uniformly as plain text.
aspinall@23434
   807
aspinall@23434
   808
opengoal     = element opengoal     { display_attr?, thmname_attr?, string } # FIXME: add objprefval
aspinall@23434
   809
proofstep    = element proofstep    { display_attr?, name_attr?, objtype_attr?, string }
aspinall@23434
   810
closegoal    = element closegoal    { display_attr?, string }
aspinall@23434
   811
giveupgoal   = element giveupgoal   { display_attr?, string }
aspinall@23434
   812
postponegoal = element postponegoal { display_attr?, string }
aspinall@23434
   813
comment      = element comment      { display_attr?, string }
aspinall@23434
   814
doccomment   = element doccomment   { display_attr?, string }
aspinall@23434
   815
whitespace   = element whitespace   { display_attr?, string }
aspinall@17735
   816
aspinall@17735
   817
display_attr = attribute nodisplay { xsd:boolean }  # whether to display in documentation
aspinall@17735
   818
aspinall@23434
   819
spuriouscmd  = element spuriouscmd { string }  # no semantic effect (e.g. print)
aspinall@23434
   820
badcmd       = element badcmd { string }       # illegal in script (e.g. undo)
aspinall@23434
   821
nonscripting = element nonscripting { string } # non-scripting text (different doc type)
aspinall@17735
   822
aspinall@17735
   823
litcomment  = element litcomment { format_attr?, (text | directive)* }
aspinall@17735
   824
directive   = element directive { (proofctxt,pgml) }
aspinall@17735
   825
format_attr = attribute format { token }
aspinall@17735
   826
aspinall@17735
   827
pragma       = showhidecode | setformat
aspinall@17735
   828
showhidecode = element showcode { attribute show { xsd:boolean } }
aspinall@17735
   829
setformat    = element setformat { format_attr }
aspinall@17735
   830
aspinall@23434
   831
dostep       = element dostep { string }
aspinall@23434
   832
undostep     = element undostep { times_attr? }
aspinall@23434
   833
redostep     = element redostep { times_attr? }
aspinall@17735
   834
abortgoal    = element abortgoal { empty }
aspinall@17735
   835
forget       = element forget { thyname_attr?, name_attr?, objtype_attr? }
aspinall@17735
   836
restoregoal  = element restoregoal { thmname_attr }
aspinall@17735
   837
aspinall@23434
   838
times_attr   = attribute times { xsd:positiveInteger }
aspinall@23434
   839
aspinall@17735
   840
# empty objprefval element is used for object prefs in script markup 
aspinall@17735
   841
objprefval = element objprefval { name_attr, val_attr, empty }
aspinall@23434
   842
val_attr   = attribute value { token }
aspinall@17735
   843
aspinall@17735
   844
aspinall@17735
   845
aspinall@17735
   846
aspinall@17735
   847
# =======================================================
aspinall@17735
   848
# Inspecting the proof context, etc.
aspinall@17735
   849
aspinall@23434
   850
# NB: ids/refs/parent: work in progress, liable to change.
aspinall@23434
   851
aspinall@17735
   852
proofctxt =
aspinall@23434
   853
    askids         # tell me about identifiers (given objtype in a theory)
aspinall@23434
   854
  | askrefs        # tell me about dependencies (references) of an identifier
aspinall@23434
   855
#  | askparent      # tell me the container for some identifier
aspinall@23434
   856
  | showid         # print the value of some object
aspinall@23434
   857
  | askguise       # tell me about the current state of the prover
aspinall@17735
   858
  | parsescript    # parse a raw proof script into proofcmds
aspinall@17735
   859
  | showproofstate # (re)display proof state (empty if outside a proof)
aspinall@17735
   860
  | showctxt       # show proof context
aspinall@17735
   861
  | searchtheorems # search for theorems (prover-specific arguments)  
aspinall@17735
   862
  | setlinewidth   # set line width for printing
aspinall@17735
   863
  | viewdoc        # request some on-line help (prover-specific arg)
aspinall@17735
   864
aspinall@17735
   865
askids = element askids  { thyname_attr?, objtype_attr? }
aspinall@17735
   866
	# Note that thyname_attr is *required* for certain objtypes (e.g. theorem).
aspinall@17735
   867
	# This is because otherwise the list is enormous.
aspinall@17735
   868
	# Perhaps we should make thyname_attr obligatory? 
aspinall@17735
   869
	# With a blank entry (i.e. thyname="") allowed for listing theories, or for when 
aspinall@23434
   870
	# you really do want to see everything (could be a shell-style glob)
aspinall@23434
   871
aspinall@23434
   872
aspinall@23434
   873
# askids:    container -> identifiers contained within
aspinall@23434
   874
# askparent: identifier + type + context -> container
aspinall@23434
   875
# askrers:   identifier + type + context -> identifiers which are referenced 
aspinall@23434
   876
#
aspinall@23434
   877
askrefs = element askrefs { url_attr?, thyname_attr?, objtype_attr?, name_attr? }
aspinall@23434
   878
# TODO: maybe include guises here as indication of reference point.  
aspinall@23434
   879
# setrefs in reply to askrefs only really needs identifiers, but it's nice to
aspinall@23434
   880
# support voluntary information too.
aspinall@23434
   881
setrefs = element setrefs { url_attr?, thyname_attr?, objtype_attr?, name_attr?, idtable*, fileurl* }
aspinall@23434
   882
fileurl = element fileurl { url_attr }
aspinall@23434
   883
# telldeps = element telldeps { thyname_attr?, objtype_attr, name_attr?, identifier* }
aspinall@23434
   884
# Idea: for a theory dependency we return a single file (URL), the containing file.
aspinall@23434
   885
#       for a file dependency we return urls of parent files,
aspinall@23434
   886
#       for theorem dependency we return theory
aspinall@23434
   887
#       for term dependency we return definition (point in file)
aspinall@23434
   888
aspinall@17735
   889
aspinall@17735
   890
showid = element showid  { thyname_attr?, objtype_attr, name_attr }
aspinall@17735
   891
aspinall@17735
   892
askguise = element askguise { empty }
aspinall@17735
   893
aspinall@23434
   894
showproofstate = element showproofstate { empty }
aspinall@23434
   895
showctxt       = element showctxt { empty }
aspinall@23434
   896
searchtheorems = element searchtheorems { string }
aspinall@23434
   897
setlinewidth   = element setlinewidth { xsd:positiveInteger }
aspinall@23434
   898
viewdoc        = element viewdoc { token }
aspinall@23434
   899
aspinall@17735
   900
aspinall@17735
   901
# =======================================================
aspinall@23434
   902
# Proof script documents and parsing proof scripts
aspinall@23434
   903
aspinall@23434
   904
# A PGIP document is a sequence of script commands, each of which
aspinall@23434
   905
# may have meta information attached.
aspinall@23434
   906
properscriptcmdmetainfo = properscriptcmd, metainfo*
aspinall@23434
   907
pgipdoc = element pgipdoc { properscriptcmdmetainfo* }
aspinall@23434
   908
aspinall@17735
   909
aspinall@17735
   910
# NB: parsing needs only be supported for "proper" proof commands,
aspinall@17735
   911
# which may appear in proof texts.  The groupdelimiters are purely
aspinall@17735
   912
# markup hints to the interface for display structure on concrete syntax.
aspinall@17735
   913
# The location attributes can be used by the prover in <parsescript> to
aspinall@17735
   914
# generate error messages for particular locations; they can be used 
aspinall@17735
   915
# in <parseresult> to pass position information back to the display,
aspinall@17735
   916
# particularly in the case of (re-)parsing only part of a file.
aspinall@17735
   917
# The parsing component MUST return the same location attributes
aspinall@17735
   918
# (and system data attribute) that was passed in.
aspinall@17735
   919
aspinall@17735
   920
parsescript = element parsescript
aspinall@23434
   921
                 { location_attrs, systemdata_attr, string }
aspinall@17735
   922
       
aspinall@17735
   923
parseresult = element parseresult { location_attrs, systemdata_attr,
aspinall@17735
   924
				    singleparseresult* }
aspinall@17735
   925
aspinall@23434
   926
# Really we'd like parsing to return properscriptcmdmetainfo as a single
aspinall@23434
   927
# result (and similarly for newobj).  
aspinall@23434
   928
# Unfortunately, although this is an XML-transparent extension, it
aspinall@23434
   929
# messes up the Haskell schema-fixed code rather extensively, so for
aspinall@23434
   930
# now we just treat metainfo at the same level as the other results,
aspinall@23434
   931
# although it should only appear following a properscriptcmd.
aspinall@17735
   932
aspinall@23434
   933
singleparseresult  = properscriptcmd | metainfo | unparseable | errorresponse
aspinall@23434
   934
aspinall@23434
   935
unparseable = element unparseable { string }
aspinall@17735
   936
properscriptcmd = properproofcmd | properfilecmd | groupdelimiter
aspinall@17735
   937
aspinall@17735
   938
aspinall@23434
   939
aspinall@23434
   940
aspinall@17735
   941
groupdelimiter = openblock | closeblock
aspinall@23434
   942
openblock  = element openblock { 
aspinall@23434
   943
   name_attr?, objtype_attr?, 
aspinall@23434
   944
   metavarid_attr?, positionid_attr?,
aspinall@23434
   945
   fold_attr?, indent_attr? }
aspinall@17735
   946
closeblock = element closeblock { empty }
aspinall@17735
   947
aspinall@17735
   948
# 
aspinall@23434
   949
metavarid_attr  = attribute metavarid { token }
aspinall@23434
   950
positionid_attr = attribute positionid { token }
aspinall@23434
   951
fold_attr       = attribute fold { xsd:boolean }
aspinall@23434
   952
indent_attr     = attribute indent { xsd:integer }
aspinall@17735
   953
aspinall@17735
   954
aspinall@17735
   955
# =======================================================
aspinall@17735
   956
# Theory/file handling
aspinall@17735
   957
aspinall@17735
   958
properfilecmd =     # (NB: properfilecmds are purely markup on proof script text)
aspinall@17735
   959
    opentheory      # begin construction of a new theory.  
aspinall@17735
   960
  | theoryitem      # a step in a theory (e.g. declaration/definition of type/constant).
aspinall@17735
   961
  | closetheory     # complete construction of the currently open theory
aspinall@17735
   962
aspinall@17735
   963
improperfilecmd = 
aspinall@17735
   964
    doitem	    # issue a proper file command (without passing in markup)
aspinall@17735
   965
  | undoitem	    # undo last step (or named item) in theory construction
aspinall@17735
   966
  | redoitem	    # redo last step (or named item) in theory construction (optionally supported)
aspinall@17735
   967
  | aborttheory     # abort currently open theory
aspinall@17735
   968
  | retracttheory   # retract a named theory
aspinall@23434
   969
  | openfile        # signal a file is being opened for constructing a proof text interactively
aspinall@23434
   970
  | closefile       # close the currently open file, suggesting it has been processed
aspinall@17735
   971
  | abortfile       # unlock a file, suggesting it hasn't been processed
aspinall@23434
   972
  | loadfile        # load (i.e. process directly) a file possibly containing theory definition(s)
aspinall@23434
   973
  | retractfile     # retract a given file (including all contained theories) 
aspinall@17735
   974
  | changecwd       # change prover's working directory (or load path) for files
aspinall@17735
   975
  | systemcmd       # system (other) command, parsed internally
aspinall@17735
   976
aspinall@17735
   977
fileinfomsg = 
aspinall@17735
   978
   informfileloaded       # prover informs interface a particular file is loaded
aspinall@17735
   979
 | informfileretracted    # prover informs interface a particular file is outdated
aspinall@17735
   980
 | informguise		  # prover informs interface about current state
aspinall@17735
   981
aspinall@23434
   982
opentheory    = element opentheory    { thyname_attr, parentnames_attr?, string }
aspinall@23434
   983
closetheory   = element closetheory   { string }
aspinall@23434
   984
theoryitem    = element theoryitem    { name_attr?, objtype_attr?, string } # FIXME: add objprefval
aspinall@17735
   985
aspinall@23434
   986
doitem        = element doitem        { string } 
aspinall@23434
   987
undoitem      = element undoitem      { name_attr?, objtype_attr?, times_attr? } 
aspinall@23434
   988
redoitem      = element redoitem      { name_attr?, objtype_attr?, times_attr? } 
aspinall@17735
   989
aborttheory   = element aborttheory   { empty }
aspinall@17735
   990
retracttheory = element retracttheory { thyname_attr }
aspinall@17735
   991
aspinall@17735
   992
parentnames_attr = attribute parentnames { objnames }
aspinall@17735
   993
aspinall@17735
   994
aspinall@17735
   995
# Below, url_attr will often be a file URL.  We assume for now that
aspinall@17735
   996
# the prover and interface are running on same filesystem.
aspinall@17735
   997
#
aspinall@17735
   998
aspinall@17735
   999
openfile      = element openfile  { url_attr }	    # notify begin reading from given file
aspinall@17735
  1000
closefile     = element closefile { empty }	    # notify currently open file is complete
aspinall@17735
  1001
abortfile     = element abortfile { empty }	    # notify currently open file is discarded
aspinall@17735
  1002
loadfile      = element loadfile  { url_attr }	    # ask prover to read file directly
aspinall@23434
  1003
retractfile   = element retractfile { url_attr }    # ask prover to retract file
aspinall@23434
  1004
changecwd     = element changecwd { url_attr }	    # ask prover to change current working dir
aspinall@17735
  1005
aspinall@17735
  1006
# this one not yet implemented, but would be handy.  Perhaps could be 
aspinall@17735
  1007
# locatethy/locatefile instead.
aspinall@17735
  1008
#locateobj     = element locateobj { name_attr, objtype_attr } # ask prover for file defining obj
aspinall@17735
  1009
aspinall@23434
  1010
informfileloaded    = element informfileloaded    { completed_attr?, 
aspinall@23434
  1011
						    url_attr }  # prover indicates a processed file
aspinall@23434
  1012
informfileretracted = element informfileretracted { completed_attr?, 
aspinall@23434
  1013
						    url_attr }  # prover indicates an undone file
aspinall@23434
  1014
informfileoutdated = element informfileoutdated { completed_attr?, 
aspinall@23434
  1015
						    url_attr }  # prover indicates an outdated file
aspinall@23434
  1016
aspinall@17735
  1017
informfilelocation  = element informfilelocation  { url_attr }  # response to locateobj
aspinall@17735
  1018
aspinall@23434
  1019
completed_attr = attribute completed { xsd:boolean }  # false if not completed (absent=>true)
aspinall@23434
  1020
						      # (the prover is requesting a lock)
aspinall@23434
  1021
aspinall@23434
  1022
aspinall@23434
  1023
aspinall@17735
  1024
informguise = 
aspinall@17735
  1025
   element informguise {
aspinall@17735
  1026
      element guisefile { url_attr }?,
aspinall@17735
  1027
      element guisetheory { thyname_attr }?,
aspinall@17735
  1028
      element guiseproof { thmname_attr?, proofpos_attr? }?
aspinall@17735
  1029
   }
aspinall@17735
  1030
aspinall@17735
  1031
proofpos_attr = attribute proofpos { xsd:nonNegativeInteger }
aspinall@17735
  1032
aspinall@23434
  1033
systemcmd     = element systemcmd     { string }	# "shell escape", arbitrary prover command!
aspinall@17735
  1034
aspinall@17735
  1035
# ==============================================================================
aspinall@23434
  1036
# 8. Internal messages: only used between communicating brokers.
aspinall@17735
  1037
# ==============================================================================
aspinall@17735
  1038
internalmsg  = launchcomp | stopcomp | registercomp | compstatus
aspinall@17735
  1039
aspinall@17735
  1040
launchcomp   = element launchcomponent { componentspec }
aspinall@17735
  1041
	               # request to start an instance of this component remotely
aspinall@23434
  1042
stopcomp     = element stopcomponent { attribute sessionid { token } }
aspinall@17735
  1043
                       # request to stop component with this session id remotely
aspinall@17735
  1044
aspinall@17735
  1045
registercomp = element registercomponent { activecompspec } 
aspinall@17735
  1046
                       # component has been started successfully
aspinall@17735
  1047
compstatus   = element componentstatus { componentstatus_attr    # status
aspinall@17735
  1048
	                               , componentid_attr?       # component id (for failure)
aspinall@23434
  1049
	                               , element text { string }?  # user-visible error message
aspinall@23434
  1050
				       , element info { string }?  # Additional info for log files.
aspinall@17735
  1051
				       }	
aspinall@17735
  1052
                       # component status: failed to start, or exited
aspinall@17735
  1053
aspinall@17735
  1054
componentstatus_attr = attribute status { ("fail"   # component failed to start
aspinall@17735
  1055
 		                          |"exit"  # component exited
aspinall@17735
  1056
					  )}	
aspinall@17735
  1057
aspinall@17735
  1058
# Local variables:
aspinall@17735
  1059
# fill-column: 95
aspinall@17735
  1060
# End:
aspinall@17735
  1061
# ==============================================================================
aspinall@17735
  1062
# end of `pgip.rnc'.
aspinall@17735
  1063