On Sun, 8 Apr 2012, Edward Z. Yang wrote:
I took a look at the YXML encoding for Isabelle, and I was surprised by
how simple the ADT was. To compare, here is Coq's base term type;
and it doesn't include all of the extra types referred to from it:
type ('constr, 'types) kind_of_term =
| Rel of int
| Var of identifier
| Meta of metavariable
| Evar of 'constr pexistential
| Sort of sorts
| Cast of 'constr * cast_kind * 'types
| Prod of name * 'types * 'types
| Lambda of name * 'types * 'constr
| LetIn of name * 'constr * 'types * 'constr
| App of 'constr * 'constr array
| Const of constant
| Ind of inductive
| Construct of constructor
| Case of case_info * 'constr * 'constr * 'constr array
| Fix of ('constr, 'types) pfixpoint
| CoFix of ('constr, 'types) pcofixpoint
You would have compare that to the datatypes for term and proofterm in
Isabelle, see src/Pure/term.ML and src/Pure/proofterm.ML, respectively.
XML/YXML alone does not do anything, it merely provides a simple tree
format to transport arbitrary ML datatype values. The wrapping for that
essentially duplicates the datatype specfification once more on each side
of the inter-process communication, but not more.
One of the appeals of PGIP is that it doesn't ask very much on the part
of the theorem prover. Just add some tags to your extant proof format;
if you dropped the tags, the text should look just like it did before.
I don't have a good sense for what an all encompassing Isabelle/JEdit
protocol looks like (what about tactics? communication of proof state?),
but it seems to demand much more radical restructuring on the parts of
the proof assistant.
I've found it very challenging to get a half-decent PGIP implementation in
Isabelle. In the historcial attempts at that, there is a famous comment
by David Aspinall and Christoph Lüth here (from 2004):
http://isabelle.in.tum.de/repos/isabelle/file/fc385ce6187d/src/Pure/proof_general.ML#l731
In particular this bit:
If we had proper parse trees it would be easy, although having a
fixed type of trees might be tricky with Isar's extensible parser.
Ex falso quodlibet consequitur ... or more appropiately "Lasciate ogne
speranza, voi ch'intrate" (Dante passing through the Gates of Hell).
Many discussions over many years later, all problems are basically solved,
although the way to do it turned out quite differently than first
anticipated in early PGIP drafts. (The main idea is to use YXML again to
sneak useful markup into messages produced by the prover.)
Makarius_______________________________________________
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
