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.

  • E.g. for a function

-- DavidAspinall - 27 Jun 2007

This topic: PG > PGIPImprovementsInProvers
Topic revision: r1 - 27 Jun 2007 - 06:56:57 - DavidAspinall
This site is powered by the TWiki collaboration platformCopyright © by the contributing authors. All material on this collaboration platform is the property of the contributing authors.
Ideas, requests, problems regarding TWiki? Send feedback
This Wiki uses Cookies