Commit Graph

611 Commits

Author SHA1 Message Date
Victor Maia
a0139cbd90 Inc version 2022-09-15 15:58:52 -03:00
Victor Taelin
a0e810ca4b
Merge pull request #365 from felipegchi/arity-16
Added maximum arity of 16
2022-09-15 15:58:23 -03:00
Felipe g
e0bf4ee86b Added maximum arity of 16 2022-09-15 12:00:49 -03:00
Victor Maia
d58784bfd0 Inc version 2022-09-07 22:00:04 -03:00
Victor Taelin
ec46af404d
Merge pull request #359 from developedby/kindelia-names
Handle U120 properly on kindelia compilation
2022-09-07 21:59:27 -03:00
Nicolas Abril
65c4cd715f Re-add special cases for U120.high and low 2022-09-07 21:44:29 -03:00
Nicolas Abril
24917cad72 Merge branch 'master' of https://github.com/Kindelia/Kind2 into kindelia-names 2022-09-07 21:31:55 -03:00
Nicolas Abril
d64eed4922 --amend 2022-09-07 21:31:52 -03:00
Nicolas Abril
7c09e0cbe9 Handle U120 properly on kindelia compilation
(U120.new num num) becomes a primitive num.

(U120.op num num) becomes a primitive op2.

Compilation fails on lhs (U120.new var _).
2022-09-07 21:11:43 -03:00
Victor Maia
d822149f4f Inc version 2022-09-07 14:20:46 -03:00
Victor Taelin
4629d55d3a
Merge pull request #358 from developedby/kindelia-names
More kindelia compiler improvements
2022-09-07 14:20:24 -03:00
Nicolas Abril
811c2eafb7 Merge branch 'master' of https://github.com/Kindelia/Kind2 into kindelia-names 2022-09-06 20:13:52 -03:00
Nicolas Abril
fa24180cb6 More kindelia compiler improvements
Add rule flattening to the kindelia compiler.
The algorithm is copied from the HVM, but instead of `>

Fix a bug where the variable linearizer didn't unbind >

Reorganize some of the compilation code, adding other >

This doesn't check for code
2022-09-06 20:05:43 -03:00
Victor Maia
26f55b3677 Inc version 2022-09-06 15:12:56 -03:00
Victor Maia
eae62b40e2 Merge branch 'master' of github.com:kindelia/kind2 2022-09-06 15:11:50 -03:00
Victor Maia
70004a7224 Inc version 2022-09-06 15:08:18 -03:00
Victor Taelin
0c831a1f8b
Merge pull request #357 from felipegchi/fix-load
Fix infinite loop
2022-09-06 15:07:23 -03:00
Victor Taelin
81a1240962
Merge pull request #356 from developedby/kindelia-names
Fixes and improvements for the kindelia compiler
2022-09-06 14:53:22 -03:00
Felipe g
8b6454426f Style removed useless parenthesis 2022-09-06 12:20:29 -03:00
Felipe g
7e614363b8 Fix infinite loop 2022-09-06 12:13:08 -03:00
Felipe g
4069f98ad9 Fix infinite loop 2022-09-06 12:06:52 -03:00
Victor Maia
3ff86299a1 Consider reductions of function before InvalidCall error 2022-09-04 21:48:44 -03:00
Nicolas Abril
06ebf9f05a Merge branch 'master' of https://github.com/Kindelia/Kind2 2022-09-03 13:32:22 -03:00
Nicolas Abril
2f9313abe0 Fixes and improvements for the kindelia compiler
Add an alternate name for function, to be used as the kindelia name.
Syntax is `Function.name #kdl_name (args) : type`

For functions that don't have a kindelia name, try to fit their names to 12 characters by truncating the last part of the name and inserting some random characters to avoid collisions. For example: `Fn.with_a_long_name` becomes `Fn.with_aF5m`, with the last 3 characters being random.
This takes the start of the function up to the last `.` as the namespace.

Compile entries with arity 0 as constructors.

Don't compile constructors of type Type.
This doesn't cover all cases of invalid constructors.
For example: `Fn (a: U60) : U60.if a Type U60` will still try to compile and fail.

Fix a bug where function applications where being compiled as constructors.

Don't compile erased arguments anymore.

Check for invalid Nil terms in compilation.
2022-09-03 13:26:58 -03:00
Victor Maia
bfa613ea5a Use ## for sub syntax 2022-09-03 00:28:20 -03:00
Victor Maia
f1dfa0a30d Add sub syntax 2022-09-03 00:18:07 -03:00
Victor Maia
5d504fc14d Rebuild 2022-09-02 19:15:29 -03:00
Victor Maia
b5ad5d4e7f Fix Kind2 unifier forgetting let equalities 2022-09-02 17:50:58 -03:00
Victor Maia
1cca987277 Move benchmarks out, update README 2022-09-02 14:23:13 -03:00
Victor Taelin
42d9b12f3f
Merge pull request #61 from developedby/lhs-eras
Add support for hiding arguments in the lhs or rules
2022-09-02 13:06:41 -03:00
Nicolas Abril
f8172c5f4b Add support for hiding arguments in the lhs or rules 2022-08-31 18:38:46 -03:00
Victor Maia
71d35d76cb Unbound var check fixes 2022-08-30 22:20:52 -03:00
Victor Maia
0db022773c Fix ann checker 2022-08-30 20:56:11 -03:00
Victor Maia
751c74f658 Rebuild 2022-08-25 13:31:03 -03:00
Victor Maia
863cc496cc Inc version and rebuild 2022-08-25 13:28:04 -03:00
Victor Maia
509b409fde Merge branch 'bootstrap' 2022-08-25 13:22:34 -03:00
Victor Taelin
fe9128ffb7
Merge pull request #50 from felipegchi/typechecker
Changed to the new checker
2022-08-25 13:21:07 -03:00
Felipe g
f94de71a41 Merge 2022-08-25 13:03:24 -03:00
Felipe g
4493a3f319 Regenerate checker 2022-08-25 12:55:14 -03:00
Felipe g
e185c8c736 Fix HOAS 2022-08-25 12:51:45 -03:00
Victor Maia
19fc3cbcbd Prevent checker from fully evaluating top-level types 2022-08-24 16:07:46 -03:00
Victor Taelin
aabc22c9ad
Merge pull request #55 from felipegchi/hole-fix
Fix hole equality problem
2022-08-24 14:53:01 -03:00
Felipe g
4083926d80 Fix hole problem 2022-08-24 14:46:04 -03:00
Victor Taelin
d6a6c5753f
Merge pull request #54 from felipegchi/fix-equal
Fix problem with values that was not reducing
2022-08-24 13:16:24 -03:00
Felipe g
eec440cba5 Regenerated type checker with the fix for Null values 2022-08-24 13:05:45 -03:00
Felipe g
32c075726f Fix problem with values that was not reducing 2022-08-24 13:01:58 -03:00
Victor Taelin
f7447ced16
Merge pull request #53 from Kindelia/revert-52-hole-fix
Revert "Fix hole equality" (temporarily)
2022-08-23 14:41:45 -03:00
Victor Taelin
dcf5b5a88f
Revert "Fix hole equality" 2022-08-23 14:41:29 -03:00
Felipe g
2e76854a1a Regenerated checker.hvm 2022-08-23 14:38:45 -03:00
Victor Taelin
7b96b49024
Merge pull request #52 from felipegchi/hole-fix
Fix hole equality
2022-08-23 14:12:35 -03:00