Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Message-Id: <9411031045.AA26789@bolverk.cs.cornell.edu>
To: Konrad Slind <slind@informatik.tu-muenchen.de>
Cc: info-hol@leopard.cs.byu.edu
Subject: Re: bhogan@bedlam: HOL90 on a PC
In-Reply-To: Your message of "Thu, 03 Nov 1994 10:49:53 +0100." <94Nov3.105003met.8082@sunbroy14.informatik.tu-muenchen.de>
Date: Thu, 03 Nov 1994 05:45:44 -0500
From: Chet Murthy <murthy@cs.cornell.edu>


> >>>>> "KS" == Konrad Slind <slind@informatik.tu-muenchen.de> writes:

    KS> Yeah maybe. The results would have to be readable, e.g., keep
    KS> comments, try to preserve original indentation, etc.

Gilles Kahn has good ideas (and implementations) for doing this very
effectively.

    KS> If it's so trivial, how come it doesn't exist? It's not like
    KS> there's no demand for it!

The best way to do this would be to adapt Centaur's already-existing
technology for SML-editing to handle CAML-light parsing and printing.
Then, you could translate between the languages by choosing the parser
and printer correctly, and use stuff written in Typol to do whatever
simple sorts of modifications needed to get done in between.

    >> There is already agreement over at least one common abstract
    >> syntax -- Edinburgh LF.  I suspect that *all* term-languages
    >> for provers could be easily translated into LF -- certainly
    >> Constructions and Nuprl can, and I'd bet that HOL could, too.

    KS> I suspect that a major
    KS> problem would be that many theorem provers have hard-wired
    KS> their parsers into their implementation.

Well, Coq V5.10 uses an interpreted grammer which gets loaded almost
completely (the only exceptions being the rules for grammars and
pretty-printing rules) from user-files.

For instance, I was able to add the ability to parse LEGO syntax by
writing a LEGO-style grammar, and adding a single production to the
standard Coq grammar of the form:

<term> ::= "LEGO" "[" <lego-term> "]"

This allowed me to write:

      LEGO[<something in lego's syntax>]

Of course, all of this was completely dynamic.

This code, of course, is completely independent of the actual Coq
implementation.  I just followed along in the footsteps of
Cardelli/Abadi/Matthes.  And the same technique could be used to add
extensible parsing to *any* system (as Cardelli et. al. stated in
their paper).

--chet--