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