Notes on PGIP next steps
Here are some notes on desirable next steps for improving the emerging
PGIP support in provers.
Parse markup
- General idea: basic markup with
parsescript
, extra info added during processing with metainforesponse
- TODO: decide on some PGIP conventions for appropriate metainfo
- Term structure markup on parsed input is not needed for reordering but would be needed for renaming. Note that this couldn't
happen during parsing anyway; this form of meta information would refine the
parseresult
with the results of type-checking.
- Question: how would we anyway support provers which do not separate parsing and type-checking, but just parse and typecheck a block of text (perhaps even whole file) in one go? If we solve this we might support Agda, PML, Mizar, etc.
- Answer: this is part of the Prover Meta Model, where some provers do not distinguish between parsed and proved states, but collapse these two.
Dependency info
We'd like to have better dependency information so we can begin on supporting refactoring.
--
DavidAspinall - 27 Jun 2007