From db7d2ce73dda0798a03326bb7035ab50ea492ec2 Mon Sep 17 00:00:00 2001 From: Steve Dunham Date: Wed, 11 Sep 2024 16:00:56 -0700 Subject: [PATCH] Updates to text files / comments --- README.md | 9 ++++++++- TODO.md | 14 +++++++------- src/Lib/TT.idr | 10 ++-------- 3 files changed, 17 insertions(+), 16 deletions(-) diff --git a/README.md b/README.md index 596c7e7..efda4ce 100644 --- a/README.md +++ b/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. diff --git a/TODO.md b/TODO.md index 9572758..d0a6d67 100644 --- a/TODO.md +++ b/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 -- [ ] write js files in out -- [ ] detect extra clauses -- [ ] test framework +- [ ] show compiler failure in the editor (exit code != 0) +- [ ] write js files into `out` directory +- [ ] detect extra clauses in case statements +- [ ] 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) diff --git a/src/Lib/TT.idr b/src/Lib/TT.idr index c8a6ca2..1d2c695 100644 --- a/src/Lib/TT.idr +++ b/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