PGIPImprovementsInProvers < PG

PG Web>PGIPImprovementsInProvers (27 Jun 2007, DavidAspinall) (raw view)EditAttach

---+ 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 


-- Main.DavidAspinall - 27 Jun 2007

Topic revision: r1 - 27 Jun 2007 - 06:56:57 - DavidAspinall

Copyright © 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