Commit Graph

86 Commits

Author SHA1 Message Date
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
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
1cca987277 Move benchmarks out, update README 2022-09-02 14:23:13 -03:00
Victor Maia
0db022773c Fix ann checker 2022-08-30 20:56:11 -03:00
Victor Maia
863cc496cc Inc version and rebuild 2022-08-25 13:28:04 -03:00
Victor Maia
19fc3cbcbd Prevent checker from fully evaluating top-level types 2022-08-24 16:07:46 -03:00
Victor Maia
73e1e70785 Update HVM 2022-08-19 17:31:39 -03:00
Victor Maia
e21cd202af Inc version 2022-08-19 13:27:30 -03:00
Victor Maia
02cc798cf0 Inc version 2022-08-19 13:18:29 -03:00
Victor Maia
60cf29dfeb Stringify string literals on Rust side 2022-08-17 21:42:45 -03:00
Victor Maia
b109ee674f Fix expected/detected flipped 2022-08-17 21:22:58 -03:00
Victor Maia
e8cc429948 Hide hole numbers 2022-08-17 16:29:09 -03:00
Victor Maia
a7c3b0ab7b Implement HVM.log 2022-08-17 16:24:36 -03:00
Victor Maia
dde08af0cb Fix <= parser 2022-08-16 12:40:16 -03:00
Victor Maia
826e121674 Sigma.new syntax 2022-08-13 22:40:04 -03:00
Victor Maia
5a13856ada Annotated lambdas 2022-08-13 22:20:15 -03:00
Victor Maia
14b16122e7 Update HVM 2022-08-13 21:40:20 -03:00
Victor Maia
04156eaa77 Udpate HVM 2022-08-13 21:32:00 -03:00
Victor Maia
d6987d1793 Inc version 2022-08-13 21:30:14 -03:00
Victor Maia
e4417d2732 Increase max HVM arity 2022-08-13 21:28:50 -03:00
Victor Maia
41fd37b7ef Add parens 2022-08-13 21:23:05 -03:00
Victor Maia
399a1dec1e Add space 2022-08-13 20:45:20 -03:00
Victor Maia
710036dc5d Sigma syntax sugar 2022-08-13 20:44:01 -03:00
Victor Maia
54d3f87c03 Fix display of origin on new errors 2022-08-13 19:45:58 -03:00
Victor Maia
08b6879bf4 Fix issue with last commit 2022-08-13 19:03:37 -03:00
Victor Maia
130f25eee4 Improve hole filling by moving conversion to an Unify function 2022-08-13 18:25:31 -03:00
Victor Maia
4d8144bd9f Fix the syntax that only Sipher could ever manage to notice that was broken 2022-08-13 14:22:36 -03:00
Victor Maia
5d3dffb5d7 More stringifier fixes 2022-08-13 14:12:15 -03:00
Victor Maia
b61a8d5eac Stringifier fixes 2022-08-13 14:10:25 -03:00
Victor Maia
36e7ba99fc Omit () on forall body 2022-08-13 13:55:56 -03:00
Victor Maia
6d2054b57e Update HVM 2022-08-11 14:48:26 -03:00
Victor Maia
1da8314e38 Inc version 2022-08-11 14:34:47 -03:00
Victor Maia
4eee13ec34 Update HVM 2022-08-11 14:26:03 -03:00
Victor Maia
65fecd1d02 Eval before conversion, fixes #38 2022-08-11 13:23:15 -03:00
Victor Maia
7fbe8ab727 Fix Kind2->KDL ctr compiler 2022-08-09 15:24:27 -03:00
Victor Maia
84ff4f54e2 Add missing case on monad syntax 2022-08-09 13:57:18 -03:00
Victor Maia
e023947255 Omit most parenthesis; arrow lambda syntax (x => y) 2022-08-05 05:03:25 -03:00
Victor Maia
727e334609 Update HVM, reduction improvements 2022-07-27 19:59:40 -03:00
Victor Maia
dd66be414f Update HVM, fixes reduction bugs 2022-07-27 18:59:09 -03:00
Victor Maia
7d8327c394 Remove accidental line 2022-07-27 18:03:35 -03:00
Victor Maia
e948648062 Fix stringifier and deriver 2022-07-27 17:26:04 -03:00
Victor Maia
7c1a7aa793 Stringify sugars and lists 2022-07-27 16:19:46 -03:00
Victor Maia
c7e18e936d Inc version 2022-07-27 01:13:19 -03:00
Victor Maia
af1b3890d0 Proper reduction of default cases; fixes #32 2022-07-27 01:09:28 -03:00
Victor Maia
4c21332cad Inc version 2022-07-26 17:33:49 -03:00
Victor Maia
be09477634 Show unbound var name 2022-07-26 17:12:39 -03:00