[ProofPower] PP and XML

[Gregg Reynolds]

Roger Bishop Jones wrote:
> 
> Is anyone else interested in ProofPower and XML?
> 
Else than me?  Dunno.  I certainly am.

I haven't had time to look at your stuff, but I have some ideas about PP
and XML and LP.  BTW as chance has it I came across your webpages over
the weekend whilst googling for something or other.  Quite a collection
of stuff - it's now on my bibsonomy list.

As it stands now, sieve et al. do a pretty good job, and are generic
enough to support all kinds of LP stuff.  You could probably do
interesting XMLish things with sieve as it stands.  An obvious
enhancement would be to replace =FOO expressions with <FOO...> tags of
some sort, and to require a </FOO...> endtag.

The most obvious enhancement would be to enhance sieve et al. to support
utf-8.

One could of course reimplement a sieve-like tool; you could probably do
it entirely in XSL.  But sieve is already written and has some nice
features.

On the other hand, I don't think it's wise to be too religious about
XML.  It's a pretty cluttered language; if you have a text with a lot of
markup it's pretty hard to read without a specialized XML editor.  Even
then, you have to worry about DTDs or schemas.  I think my ideal LP tool
would support XML in various ways but not require it.  I personally
would would rather work in one of the "tagless" markup languages like
the kind used for wikis.  *This* is much easier on the eyes (and
fingers) than <emph rank="2">this</emph>.  See
http://www.bibsonomy.org/user/mobileink and filter on "markup" to get a
list of such languages.  ETSET looks promising for latex-based litprog,
but any of them would work.

Actually if I were to start from scratch, I'd use antlr
(http://www.antlr.org) and write language-specific parsers extended to
support some kind of markup language in comments.  Antlr is way cool,
and perfect for an LP project.  It lets you pass off different sections
of text to different grammars, so you could in principle combine parsers
for any language in a single LP tool.

Then it would be a relatively simple matter to support cross-references
among docs, so that you could e.g. you could write a reference to a
chunk of C code (with some kind of identifier) in your LP master
document and have the tool parse the C code and insert the referenced chunk.

For example, for C, instead of

	... some C code ...
	/*
	=TEX
	some markup
	=C_CODE
	*/
	.. more C code...

we could do something like:

	... some C code
	/*<TEX xref="123" some markup  >*/
	... more C code ...
	/*<xref="123a" more markup ...>*/
	... yet more C code ...
	/*</TEX  yet more markup...>*/

Now our LP master doc can refer to the xref id to extract the code and
markup between /*<TEX and /*</TEX  ... >*/ and do interesting things
with it.  By the same token, one could put the documentation entirely in
the LP master, and annotate the C to reference doc strings by the same
two-way xref mechanism.  Either way, a clever editor would be able to
toggle the LP stuff on and off (show/hide). An antlr-based tool could
pass the C code to a C parser and format it appropriately, and pass the
markup to the appropriate parser for recognition and typesetting.  This
frees the LP text from source-code ordering.  Lots of interesting
possibilities.

So this is a bit off-topic for the PP list, but it does suggest an
enhancement.  Such a tool might be good for doing implementation LP
based on a Z/HOL specification.  One could add C code to the spec doc
itself, with explanation of how the refinement from Z to C works.
Alternatively one could just reference the LP-coded C files from within
the Z spec, which becomes a spec/implementation combination.  Or a
separate Refinement doc could reference chunks of the Spec doc and
chunks of C code.

-gregg