Commit Graph

390 Commits

Author SHA1 Message Date
ad4dce9d0e Use List String for module name, add abstraction for loading files (prep for LSP)
Some checks failed
Publish Playground / build (push) Has been cancelled
Publish Playground / deploy (push) Has been cancelled
2026-02-11 19:53:59 -08:00
6a16dc6150 better name for metas
Some checks failed
Publish Playground / build (push) Has been cancelled
Publish Playground / deploy (push) Has been cancelled
2026-02-11 13:32:45 -08:00
eb9921212c use record update for top 2026-02-11 13:32:09 -08:00
340457cab7 [ repl ] don't exit early on error 2026-02-09 11:04:05 -08:00
a17a9c4342 fix pipe issue in REPL, add ability to dump top in repl 2026-02-09 10:36:59 -08:00
08ed4178cf Fix FC on imports - make empty bounds the identity 2026-02-09 10:16:56 -08:00
d36f6ddacb Add missing import in vscode, fix add missing cases at EOF
Some checks failed
Publish Playground / build (push) Has been cancelled
Publish Playground / deploy (push) Has been cancelled
2026-02-07 22:25:18 -08:00
bca61f95a0 Improve error locations 2026-02-07 16:55:33 -08:00
2766a4ae01 Unsolved metas are errors 2026-02-07 16:26:07 -08:00
00296f4d10 Allow local names to override imports 2026-02-07 11:02:51 -08:00
0c206a94ab Forward declaration syntax for data
Allow:
```newt
data Foo : U
```
as a forward declaration for data. (The `Foo : U` syntax still works for
now.)
2026-02-07 07:52:00 -08:00
9249c4c641 Invalidate on :load 2026-02-04 20:56:58 -08:00
d803af10aa Add Foldable class 2026-01-31 16:29:16 -08:00
c3e70c9ecc operator sections
Some checks failed
Publish Playground / build (push) Has been cancelled
Publish Playground / deploy (push) Has been cancelled
2026-01-31 13:21:23 -08:00
eed5c09508 Minor changes 2026-01-31 12:52:01 -08:00
f3a18fa658 Fix stray skolem issue
Sometimes a Bound variable on the LHS became Defined to itself.
This commit also resurfaces INFO messages, to aid finding the root
cause of errors.
2026-01-31 12:49:39 -08:00
56821c1711 Add some stray files
Some checks failed
Publish Playground / build (push) Has been cancelled
Publish Playground / deploy (push) Has been cancelled
2026-01-23 12:00:00 -08:00
3dd9955533 Postpone non-linear solutions 2026-01-23 08:49:30 -08:00
43401156eb Fix error in parser combinator 2026-01-18 22:03:34 -08:00
77a052ca98 remove unused fatal flag in parser 2026-01-16 10:39:31 -08:00
a21dd2fd94 fix issue with try in parser, improve parse error message 2026-01-16 10:30:41 -08:00
61f82a9d5d Add REPL 2026-01-08 21:47:58 -08:00
31cc891046 names from types on add missing cases 2026-01-05 21:25:55 -08:00
2ca43b6350 Dependent records
The projection functions needed `foo` -> `self .foo` in the types
2026-01-05 20:52:35 -08:00
c56270c183 Track module dependencies 2025-12-31 21:30:05 -08:00
bfe79d65ea remove redundant $ 2025-12-30 22:00:27 -08:00
0dfa96cb5e use new case syntax instead of the 2025-12-29 10:48:22 -08:00
f4d1e86319 Optional type annotation on case scrutinee 2025-12-29 10:24:15 -08:00
223b1563a9 pattern matching can dot with applied vars 2025-12-29 09:51:30 -08:00
70348f3e5d Show Either
Some checks failed
Publish Playground / build (push) Has been cancelled
Publish Playground / deploy (push) Has been cancelled
2025-12-26 19:52:18 -08:00
d19f39fa18 additional cast from AoC
Some checks failed
Publish Playground / build (push) Has been cancelled
Publish Playground / deploy (push) Has been cancelled
2025-12-26 13:02:27 -08:00
9bbc7208d7 Surface erasure errors in editor, fix issue checking erasure after inlining 2025-12-26 13:01:30 -08:00
6590efa91c top.errors doesn't need to be an IORef 2025-12-17 09:37:05 -08:00
e871ede85f Library additions from AoC 2025-12-16 20:14:19 -08:00
fe3e25f009 AoC todos and tweaks 2025-12-13 14:51:26 -08:00
55e9476607 Change Show for List to include brackets 2025-12-08 08:25:01 -08:00
6c836a6ef4 Day 8 2025-12-08 08:22:54 -08:00
75716091af Update Combinatory.newt, fix parse error 2025-11-15 14:18:12 -08:00
63687499dc check impossible clauses
Also clean up some comments.

We now have types in constraints, but are still using values from
context.
2025-11-14 21:45:19 -08:00
79113fbce5 add impossible clauses (not checked yet) 2025-11-14 10:53:35 -08:00
d763be55d4 Update LiftLambda to erase Zero args 2025-10-26 09:42:12 -07:00
7055874dbb Remove old aoc2023 directory 2025-10-25 13:32:58 -07:00
551e31d589 Fix issue when multiple constructors are defined on one line. Update aoc2024 tests to not use debugStr. 2025-10-24 14:50:26 -07:00
8aee58c23b erase arts in lifted where functions 2025-10-24 11:09:57 -07:00
11ffd96a91 Remove erased function arguments 2025-10-23 22:34:14 -07:00
6a4da51e8a use if/then/else for some constructor cases 2025-10-20 15:22:00 -07:00
15b892510e Map Bool-shaped things to javascript bool, add if/then and tertiary to code gen 2025-10-20 11:08:12 -07:00
2794f8fe85 Cleanup some old comments, use record update a bit more 2025-10-11 21:47:38 -07:00
ddc73fb41a Change Show FC format to match vscode's expectation 2025-10-11 21:47:34 -07:00
c39d1354c8 Primitive "Add missing cases" for vscode 2025-10-11 13:17:44 -07:00