Notes on PGIP support for PML

-- DavidAspinall - 19 Jun 2007

Use cases for PML

Requirements:

  • showing syntax and typing errors
  • editing of a hole
    • editing the whole file will require re-parsing whole file
    • to start with, we probably will typecheck whole file every time
    • in step 2, we may think of optimising for editing a whole
    • in step 3, think about undo for replacing text
  • undo or putting back a hole
  • querying the context

Type-check file

  1. -> PML: type-check a whole file (sent as a string)
  2. <- Something naming holes and/or error messages

Notes:

  • Holes are just comments, can contain any text (not checked)
  • Do we want user-level names for holes? We certainly need system-level names (e.g., numbers)
  • Probably there is no concrete syntax in PML for hole names!

Idea for system-level hole identifiers:

But: these are then changed by edits, which might be bad. Alternative is to use goal numbers constructed for tree path, but paths get long quickly. PhoX uses some relative scheme for goal numbers which helps avoid this problem.

For interface access without clicking, we do want these numbers to be usable.

Solution: use both! <X,Y> with X the history number, Y the index of the goal as it appears in the file.

Displaying errors

  • PML produces three positions for an error, would like to distinguish these by colour
  • These are: position of error, then position of match, position of variant itself
  • Underlying graph of type system actually gives some dataflow, would be nice to display this in the interface (even animate it somehow)
  • Possible solution: use PGML markup for adding highlighting?
  • At the moment, PML only returns one error, this can be displayed using three markers in Eclipse with the same (or, related) error message
  • These could maybe be flagged with infos/warnings

[ Aside: in Proof General, students first assume that after an error they must do undo! This is wrong! ]

Querying operations

Holes/goals have certain attributes:

  • A hole name which is a parameter of the query
  • If hole is a proof, a special name for the conclusion of a the hole (e.g. $concl)
  • They have access to the variables of the environment, and their types

We want these query operations:

  • Find out the whole list of variables available (NB PGIP message has some space for returning information such as type; would also be useful to include location information
  • Values of variables
  • Normalised value of a term (including variables)
  • The type of a variable, if available (e.g. when there is a written type cast)
  • The head of the type of a term (representing a type)
  • Unnamed hypotheses? Maybe by the head variable (or free variable) of p in p >> v --- although this may not be unique
  • NB: also have KB completion of the hypotheses, which gives more information to user

Notes:

  • List of variables may be too long: how to solve this? By default may just show near or important variables at first approximation (e.g. age of constraint in typing map). PGIP message probably needs a bound here to limit size of result. Or perhaps a bound of interestingness in [0,1] (scrollbar). Interestingness may be related to result of KB.
  • CR has idea that PML should have no pretty printer for values, instead it will print out fragments of source text with substitution
  • Queries never change state

Other questions:

  • May have default query for each goal (made up by interface), that can be parameterised (e.g. set in some broker configuration file for the prover, for example). Or perhaps it is changed in menus.

Questions

  • Q. How does indentation work? A. by adding the and elements,
which can be used by the interface to optionally indent the code (like TAB in Emacs).

Remarks

  • Agda-style interaction: proof construction occurs by writing proof terms by filling holes
Topic revision: r2 - 19 Jun 2007 - 14:28:08 - 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