0d974dd42d
fix parse issue for typed lamda arguments
2026-02-27 20:45:01 -08:00
4c5cd4dec0
continue after import error, fix error order
2026-02-24 22:25:16 -08:00
983dde4de2
derive Show and Eq, improvements to LSP
2026-02-24 20:14:30 -08:00
69a7b6bed8
Fix LSP slowness, improve error messages
2026-02-23 20:48:25 -08:00
c54b856f0b
Don't allow uppercase pattern variables
2026-02-20 18:44:47 -08:00
587b2c4a60
Change FC end column to be one past the end
2026-02-18 10:39:56 -08:00
3201139523
improvements to type checking of record updates
2026-02-15 21:38:44 -08:00
a9718621e3
Initial LSP implementation/vscode support
Publish Playground / build (push) Has been cancelled
Publish Playground / deploy (push) Has been cancelled
2026-02-12 20:26:15 -08:00
6c4d01d4c4
check in import loop test, remove dead code/comment
2026-02-11 20:09:12 -08:00
340457cab7
[ repl ] don't exit early on error
2026-02-09 11:04:05 -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
c3e70c9ecc
operator sections
Publish Playground / build (push) Has been cancelled
Publish Playground / deploy (push) Has been cancelled
2026-01-31 13:21:23 -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
84c4008724
check in test from dependent record fix
2026-01-23 08:53:49 -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
a21dd2fd94
fix issue with try in parser, improve parse error message
2026-01-16 10:30:41 -08:00
9bbc7208d7
Surface erasure errors in editor, fix issue checking erasure after inlining
2025-12-26 13:01:30 -08:00
55e9476607
Change Show for List to include brackets
2025-12-08 08:25:01 -08:00
aa0a12f402
remove old files
2025-11-25 17:03:29 -08:00
30ff87c2e2
log issue
2025-11-17 09:34:13 -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
2853de310b
add some missing files, clean up a little
2025-11-10 22:28:32 -08:00
e8b00ad680
Updates to highlighting in playground
2025-11-05 09:02:32 -08:00
11ffd96a91
Remove erased function arguments
2025-10-23 22:34:14 -07:00
ddc73fb41a
Change Show FC format to match vscode's expectation
2025-10-11 21:47:34 -07:00
2a5e5ae4f5
add error for stray, incorrect constructors
2025-10-10 09:03:25 -07:00
be40c431fe
Add error when a constructor is used for a primitive argument.
...
Add testing for errors.
2025-10-06 15:21:54 -07:00
1432316fac
SortedMap uses any comparator
2025-09-01 15:48:20 -07:00
fcee117260
[ libs ] move prelude file to src
2025-07-27 15:02:53 -07:00
0c72d690e3
[ libs ] add DecEq to Prelude
2025-07-27 15:02:49 -07:00
bcf34c0941
[ auto ] try autos if a meta in their type is solved
...
Also cut tryEval if the result is a lambda
2025-07-27 14:52:24 -07:00
a79f92793b
[ fix ] solve autos in data declarations
2025-07-26 08:09:46 -07:00
0e110cd14f
[ unify ] unify literals correctly
2025-07-26 08:07:48 -07:00
cae4368cd9
misc cleanup
2025-04-22 20:30:29 -07:00
8faecfdf9b
record update syntax
2025-04-19 20:11:07 -07:00
549cca19e3
Add flags to TopEntry, detect duplicate constructors, fix issue with missing constructors in CompileExp.
2025-04-05 14:33:54 -07:00
5ab2a28bcf
Prep to switch from Def to CExp for backend passes.
2025-03-15 15:46:56 -07:00
e3ae301c9c
performance and code size improvements
...
- Use default case for constructors with no explicit match.
- self-compile is 15s now
- code size is 60% smaller
code size and self compile time on par with the idris-built version
2025-01-18 21:33:49 -08:00
5a6dcdb92b
try solving autos when a related constraint is added
2025-01-02 22:44:17 -08:00
9ed2b2077d
fixes and changes for porting
...
- forward declaration of records
- fixes to projections
- drop record accessors (use projections instead)
- changes to names to disambiguate
2025-01-01 20:21:07 -08:00
9a2eac0bd7
remove a Text.Parser dependency (about 10%), and alternate tokenizer
2024-12-28 21:51:55 -08:00
a6e68ac2a2
ability to run code and check output in tests
2024-12-28 13:19:15 -08:00
9655434b2a
add namespaces to names
2024-12-26 18:51:46 -08:00
8d8078f968
improvements to erasure checking
2024-12-06 20:34:40 -08:00
e265248b11
change syntax for javascript code literals
2024-11-25 21:53:23 -08:00
9e72ed67fc
refactoring
...
- move over to env for unify et al
- fix issue where constraint had short context
- drop parameters block - make it clear where context is being used
2024-11-12 21:34:43 -08:00
6abd97ee85
Improvements to grammar
2024-11-09 21:43:38 -08:00
