wball/perga
1
0
Fork 0
Code Issues 15 Pull requests Projects Releases Packages Wiki Activity Actions

updated TODOs

Browse source
This commit is contained in:
William Ball 2024-11-14 22:02:25 -08:00
parent 9ef9a8b6ba
commit 51d97b15f5
1 changed files with 4 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
README.org
View file

@ -80,8 +80,11 @@ The error messages currently aren't terrible, but it would be nice to have, e.g.
*** TODO Improve β-equivalence check *** TODO Improve β-equivalence check
The check for β-equivalence could certainly be a lot smarter. Right now it just fully normalizes both terms and checks if the normal forms are equal, which isn't the best strategy. This is much less of an issue without [[Inductive Definitions][inductive definitions]]/recursion, as far less computation gets done in general, let alone at the type level. That being said, it's certainly not a bad idea. The check for β-equivalence could certainly be a lot smarter. Right now it just fully normalizes both terms and checks if the normal forms are equal, which isn't the best strategy. This is much less of an issue without [[Inductive Definitions][inductive definitions]]/recursion, as far less computation gets done in general, let alone at the type level. That being said, it's certainly not a bad idea.
*** TODO Better testing *** DONE Better testing
Using some kind of testing framework, like [[https://hackage.haskell.org/package/QuickCheck][QuickCheck]] and/or [[https://hackage.haskell.org/package/HUnit][HUnit]] seems like a good idea. I would like to avoid regressions as I keep working on this, and a suite of unit tests would make me feel much more comfortable. Using some kind of testing framework, like [[https://hackage.haskell.org/package/QuickCheck][QuickCheck]] and/or [[https://hackage.haskell.org/package/HUnit][HUnit]] seems like a good idea. I would like to avoid regressions as I keep working on this, and a suite of unit tests would make me feel much more comfortable.
*** DONE Switch to =Text=
Currently I use =String= everywhere. Switching to =Text= should be straightforward, and would improve performance and Unicode support.
*** TODO TUI *** TODO TUI
This is definitely a stretch goal, but I'm imagining a TUI split into two panels. On the left you can see the term you are building with holes in it. On the right you have the focused hole's type as well as the types of everything in scope (like Coq and Lean show while you're in the middle of a proof). Then you can interact with the system by entering commands (e.g. =intros=, =apply=, etc.) which changes the proof term on the left. You'd also just be able to type in the left window as well, and edit the proof term directly. This way you'd get the benefits of working with tactics, making it way faster to construct proof terms, and the benefits of working with proof terms directly, namely transparency and simplicity. I'll probably want to look into [[https://hackage.haskell.org/package/brick][brick]] in order to make this happen. This is definitely a stretch goal, but I'm imagining a TUI split into two panels. On the left you can see the term you are building with holes in it. On the right you have the focused hole's type as well as the types of everything in scope (like Coq and Lean show while you're in the middle of a proof). Then you can interact with the system by entering commands (e.g. =intros=, =apply=, etc.) which changes the proof term on the left. You'd also just be able to type in the left window as well, and edit the proof term directly. This way you'd get the benefits of working with tactics, making it way faster to construct proof terms, and the benefits of working with proof terms directly, namely transparency and simplicity. I'll probably want to look into [[https://hackage.haskell.org/package/brick][brick]] in order to make this happen.