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