TWiki
>
PG Web
>
PGIPImprovementsInProvers
(27 Jun 2007,
DavidAspinall
)
(raw view)
E
dit
A
ttach
---+ 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
E
dit
|
A
ttach
|
P
rint version
|
H
istory
: r1
|
B
acklinks
|
V
iew topic
|
Ra
w
edit
|
M
ore topic actions
Topic revision: r1 - 27 Jun 2007 - 06:56:57 -
DavidAspinall
PG
PG Web
PG Web Home
Changes
Index
Search
Notifications
RSS Feed
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