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
109 stars 9 forks source link

Make --list-operators and --list-tactics work on incomplete developments #109

Open david-christiansen opened 9 years ago

david-christiansen commented 9 years ago

Right now, --list-operators only works on comlete developments. Now that Emacs uses the output for completion and highlighting, this means that the state the file was opened in has a big impact on user experience. If it could print arities for files that are syntactically valid but incomplete, that would make the highlighting much better.

As an easier alternative, it could also print the operators defined up to the point where the first incomplete theorem is found.

jozefg commented 9 years ago

Hm, this seems like a straightforward modification to how main.sml handles failure (at least I think?). If I'm correct I can do this :)

jonsterling commented 9 years ago

@jozefg Possibly... But if an operator is defined after an unfinished theorem, it won't show up I think. So we may need to have a mode in which we run a development, but don't actually try to ensure that theorems are evident.

jozefg commented 9 years ago

@jonsterling Oh I see, because the exception will cause it to bail out.. Though it might be interesting to consider processing the development AST right away and delay proving things until afterwards.

EDIT: perhaps I shouldn't be so hasty. Looking at the code now it would seem that it's possible but might require us to hang on to a lot of development environment's as we process a file which could be troubling memory wise..