Commit Graph

162 Commits

Author SHA1 Message Date
rvcas
b27fcf38e5 fix(check): collapse_links on tuple_index access closes #905 2024-04-02 19:45:16 -04:00
rvcas
b5f27026e2 fix: confusing public validator closes #902 2024-03-29 11:32:04 -04:00
rvcas
ce2c723d0c chore: remove some dbg macros 2024-03-29 11:28:22 -04:00
KtorZ
a3f7b48ec3 Allow downcasting to data in piped function calls.
We have been a bit too strict on disallowing 'allow_cast' propagations. This is really only problematic for nested elements like Tuple's elements or App's args. However, for linked and unbound var it is probably okay, and it certainly is as well for function arguments.
2024-03-25 11:57:13 -04:00
KtorZ
96387e3437 Fixes #767
Co-authored-by: @rvcas <x@rvcas.dev>
2024-03-22 16:05:32 +01:00
rvcas
a09069b828 fix: binop associativity formatting
it seems we can fix this by changing which side
gets subtracted by 1 depending on the op associativity.
BinOp::Or & BinOp::And are right associative while the
other bin ops are left associative.

closes #893

Co-authored-by: Kasey White <kwhitemsg@gmail.com>
2024-03-21 20:12:49 -04:00
KtorZ
0f9dbfd874 Fixes #883. 2024-03-21 18:20:19 +01:00
rvcas
ee280bc309 fix: only allow casting on top level Data 2024-03-21 11:59:34 -04:00
rvcas
c20ff6b160 fix: contains_opaque was never intended to be used for type equality 2024-03-21 11:59:34 -04:00
KtorZ
5cec2544b3 Nonsensical prints to be removed. 2024-03-21 11:59:34 -04:00
KtorZ
dc9bab4f5c Add extra test case. 2024-03-21 11:59:34 -04:00
KtorZ
bee2b712de Fixes #881. 2024-03-21 11:59:34 -04:00
rvcas
4f8e900aac fix: Discard not taken into account in backpassing
closes #890

Co-authored-by: Kasey White <kwhitemsg@gmail.com>
2024-03-20 17:53:17 -04:00
rvcas
898ef74457 fix: spans for backpassing args
closes #882

Co-authored-by: Kasey White <kwhitemsg@gmail.com>
2024-03-20 17:27:17 -04:00
KtorZ
3055c5ef52 Do not allow casting when rhs or lhs contain an opaque type.
Also slightly extended the check test 'framework' to allow registering side-dependency and using them from another module. This allows to check the interplay between opaque type from within and outside of their host module.
2024-03-14 11:00:17 +01:00
rvcas
191a3e9134 chore: weird thing from rebase 2024-03-13 20:21:33 -04:00
rvcas
e71470747f feat: fix some tests and add a failing one 2024-03-13 20:18:56 -04:00
KtorZ
961806617f Add more failing tests for expecting on into opaque types. 2024-03-13 20:18:55 -04:00
rvcas
7af4ef53ab feat: block expects on opaque types 2024-03-13 20:17:54 -04:00
microproofs
b16880a170 feat(annotation): not passing annotation into lambda when backpassing
Co-authored-by: Lucas Rosa <x@rvcas.dev>
2024-03-13 19:08:53 -04:00
rvcas
7b32d4ae30 chore: add a test for formatting assignment patterns 2024-03-12 08:10:33 -04:00
rvcas
b6b52ba508 feat(backpassing): implements multi patterns
The main trick here was transforming Assignment
to contain `Vec<UntypedPattern, Option<Annotation>>`
in a field called patterns. This then meant that I
could remove the `pattern` and `annotation` field
from `Assignment`. The parser handles `=` and `<-`
just fine because in the future `=` with multi
patterns will mean some kind of optimization on tuples.
But, since we don't have that optimization yet, when
someone uses multi patterns with an `=` there will be an
error returned from the type checker right where `infer_seq`
looks for `backpassing`. From there the rest of the work
was in `Project::backpassing` where I only needed to rework
some things to work with a list of patterns instead of just one.
2024-03-12 08:10:33 -04:00
KtorZ
a57dcf3307 Allow backpassing with expect. 2024-03-11 00:20:29 +01:00
KtorZ
df898bf239 Rework monadic-bind into function backpassing.
This is more holistic and less awkward than having monadic bind working only with some pre-defined type. Backpassing work with _any_ function, and can be implemented relatively easily by rewriting the AST on-the-fly.

  Also, it is far easier to explain than trying to explain what a monadic bind is, how its behavior differs from type to type and why it isn't generally available for any monadic type.
2024-03-11 00:16:22 +01:00
KtorZ
ee54266d1f Forbid non-serializable inhabitants in compound data-types. 2024-03-09 22:25:51 +01:00
KtorZ
37627e3527 Fix indentation of pipelines. 2024-03-09 20:44:51 +01:00
KtorZ
d581183cc6 Fix formatter discarding nul bytes. 2024-03-09 18:59:35 +01:00
KtorZ
d6cc9bdfbe Allow implicit discard when right-hand side is Void.
This is the most intuitive/expected behavior. Otherwise, it forces a pointless let-binding to 'Void' or into a discard.
2024-03-09 01:28:29 +01:00
KtorZ
8ffa68d2f0 Fix && and || associativity.
Somehow, these have always been right-associative, when the natural thing to expect is left-associativity. It now matters when trying to crawl down binary tree to display them properly.
2024-03-07 01:17:05 +01:00
rvcas
ad4840958c chore: add test for validator args with no annotation 2024-03-06 11:19:32 -05:00
KtorZ
bbc9fc5762 Yield proper user-facing error when inferring Fuzzer usage 2024-03-03 19:33:26 +01:00
rvcas
ff5491caa0 fix(check): only disallow ml_result in data 2024-02-29 11:19:26 -05:00
KtorZ
d27ea98a8f Rework tracing arguments to --keep-traces & --trace-level
This allows for a more fine-grained control over how the traces are showed. Now users can instrument the compiler to preserve only their user-defined traces, or the only the compiler, or all, or none. We also want to add another trace level on top of that: 'compact' to only show line numbers; which will work for both user-defined and/or compiler-generated traces.
2024-01-19 14:30:15 +01:00
rvcas
07122aaa88 feat: allow importing off validators in validators/tests/* 2023-12-11 18:27:08 -05:00
rvcas
1f411cde0e chore: needless dbg 2023-11-28 20:59:23 -05:00
rvcas
6ce30bd949 fix: allow spread operator on positional constructors closes #677 2023-11-27 23:11:17 -05:00
rvcas
2980e8e21d fix: use a distinct warning for discarded let assignments to avoid confusion closes #763 2023-11-27 21:23:10 -05:00
microproofs
78b0789cbc chore: unit test for pub in validator module warnings closes #681 2023-11-22 18:02:21 -05:00
rvcas
abd18656e3 fix: unable to have newline after expect bool shortcut 2023-11-20 11:44:16 -05:00
rvcas
7680d33663 fix: panic in formatter when substracting u8 0 - 1 2023-11-20 11:44:16 -05:00
rvcas
6869f73033 fix: sequence formatting when not top level 2023-11-20 11:44:16 -05:00
rvcas
d53d2665b2 test(bls): g1 and g2 formatting 2023-11-15 15:55:56 -05:00
rvcas
55f89a7ff4 fix: incorrect 'unused::constructor'
`ExprTyper` was not incrementing the usage of a constructor
when infering `RecordAccess`.

closes #554
2023-10-12 17:44:57 -04:00
rvcas
135dbd8335 feat: handle pipe fn infer TODOs
This improves error messages for `a |> b(x)`.

We need to do a special check when looping over the args
and unifying. This information is within a function that does not belong
to pipe typer so I used a closure to forward along a way to add
metadata to the error when the first argument in the loop has a
unification error. Simply adding the metadata at the pipe typer
level is not good enough because then we may annotate regular
unification errors from the args.
2023-10-03 01:17:15 -04:00
rvcas
9a4f181a0f chore: clippy fix 2023-09-13 17:19:31 -04:00
KtorZ
8ba5946c32 Preserve escape sequence after formatting
Bumped into this randomly. We do correctly parse escape sequence, but
  the format would simply but the unescaped string back on save. Now it
  properly re-escapes strings before flushing them back. I also removed
  the escape sequence for 'backspace' and 'new page' form feed as I
  don't see any use case for those in an Aiken program really...
2023-09-08 12:12:15 +02:00
rvcas
0ff64e3bac test: check and format tests for logical op chain 2023-08-15 09:58:35 -04:00
rvcas
ab3a418b9c feat(parser): add support for and/or chaining 2023-08-15 09:58:35 -04:00
rvcas
60ac8ab591 fix(exhaustiveness): adjust helper method to get contructors properly 2023-08-03 16:14:42 -04:00
KtorZ
675b737898 Check exhaustiveness behavior on pattern guards. 2023-08-02 10:40:59 +02:00