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

• 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.

• E.g. for a function

-- DavidAspinall - 27 Jun 2007