Updates to text files / comments

README.md

@@ -5,7 +5,7 @@ Newt is a dependently typed programming language that compiles to javascript. It
 my first attempt to write a dependent typed language. It is inspired by Idris,
 Elaboration Zoo, pi-forall, and various tutorials.
 
-The goal is to have inductive types, pattern matching, compile to javascript, and be self hosted. At the very least though, I'd like to be able to build a little browser toy to compile and run code.
+The goal is to have inductive types, pattern matching, compile to javascript, and be self hosted. At the very least though, I'd like to be able to build a little browser "playground" to compile and run code.
 
 ## Building
 
@@ -33,6 +33,13 @@ I have `Let` in the core language. Partly because I'd like this to make it into
 
 I've got no idea what I'm doing here. I worked off of Jesper Cockx "Elaborating Dependent (Co)pattern Matching", leaving out codata for now.
 
+## Issues
+
+- I need to do some erasure of values unused at runtime
+- I'm a little fuzzy on the "right way" to deal with constraints from unification
+- I'm a little fuzzy on how much to evaluate and when
+- I'm not postponing anything, and I suspect I will need to
+
 ## References
 
 "Unifiers as Equivalences" has unification with types.  Look into adapting some of that (or at least read/understand it).  Indexed types are mentioned here.

TODO.md

@@ -7,17 +7,17 @@
 - [ ] list syntax
 - [ ] operators
 - [ ] import
-- [ ] add {{ }} and solving
+- [ ] add {{ }} and solving autos
 - [ ] some solution for + (classes? ambiguity?)
-- [ ] surface execution failure in the editor
+- [ ] show compiler failure in the editor (exit code != 0)
-- [ ] write js files in out
+- [ ] write js files into `out` directory
-- [ ] detect extra clauses
+- [ ] detect extra clauses in case statements
-- [ ] test framework
+- [ ] add test framework
 - [ ] decide what to do for erasure
-- [ ] type at point
+- [ ] type at point in vscode
 - [ ] repl
 - [ ] LSP
-- [ ] don't match forced constructors
+- [ ] don't match forced constructors at runtime
   - maybe do this in codegen if there is only one case.
 - [ ] magic nat (codegen as number with appropriate pattern matching)
 - [ ] magic tuple? (codegen as array)

src/Lib/TT.idr

@@ -1,12 +1,5 @@
--- I'm not sure this is related, or just a note to self (Presheaves on Porpoise)
-
--- maybe watch https://www.youtube.com/watch?v=3gef0_NFz8Q
--- or drop the indices for now.
-
--- ***
--- Kovacs has icity on App, and passes it around, but I'm not sure where it is needed since the insertion happens based on Raw.
-
 module Lib.TT
+
 -- For FC
 import Lib.Parser.Impl
 import Lib.Prettier
@@ -243,6 +236,7 @@ solveMeta ctx ix tm = do
 
 
 -- REVIEW - might be easier if we inserted the meta without a bunch of explicit App
+-- I believe Kovacs is doing that.
 
 -- we need to walk the whole thing
 -- meta in Tm have a bunch of args, which should be the relevant