search

jonsterling / JonPRL

An proof refinement logic for computational type theory. Inspired by Nuprl. [For up-to-date development, see JonPRL's successor, RedPRL: https://github.com/redprl/sml-redprl]
http://www.jonprl.org
MIT License
110 stars 9 forks source link

incremental, server interface #9

Open jonsterling opened 9 years ago

jonsterling commented 9 years ago

It would be nice to work with the refiner interactively (i.e. not just through the SML/NJ top-level).

I think the first step is to get a very simple top-level interface running, like Coq's coqtop or Epigram 2's cochon. This could serve as the basis for a more advanced (perhaps Emacs-based) interface.

jonsterling commented 9 years ago

It probably makes sense to consider the state at a particular time as a zipper. Tactics which are entered at the top-level are applied to the subgoal in focus, and you may zip through the tree using meta-commands.

When the tree has no more holes in it, it is then directly translatable into a single tactic script, where branches are translated using THENL. The interaction at the top-level, then, is a process by which the operator incrementally constructs a tactic script which proves the main goal.

jonsterling commented 9 years ago

The new DEVELOPMENT machinery (which replaces the old LIBRARY) should be the right basis on which to build this.