Commit Graph

67 Commits

Author SHA1 Message Date
KtorZ 858dfccc82
Authorize complete patterns as function args.
This is mainly a syntactic trick/sugar, but it's been pretty annoying
  to me for a while that we can't simply pattern-match/destructure
  single-variant constructors directly from the args list. A classic
  example is when writing property tests:

  ```ak
  test foo(params via both(bytearray(), int())) {
    let (bytes, ix) = params
    ...
  }
  ```

  Now can be replaced simply with:

  ```
  test foo((bytes, ix) via both(bytearray(), int())) {
    ...
  }
  ```

  If feels natural, especially coming from the JavaScript, Haskell or
  Rust worlds and is mostly convenient. Behind the scene, the compiler
  does nothing more than re-writing the AST as the first form, with
  pre-generated arg names. Then, we fully rely on the existing
  type-checking capabilities and thus, works in a seamless way as if we
  were just pattern matching inline.
2024-06-07 15:42:25 +02:00
rvcas 4ca73c4cdf
fix: closes #898
This is the best we can do for this without
rearchitecting when we rewrite backpassing to
plain ol' assignments. In this case, if we see
a var and there is no annotation (thus probably not a cast),
then it's safe to rewrite to a `let` instead of an `expect`.
This way, we don't get a warning that is **unfixable**.
We are not trying to solve every little warning edge
case with this fix. We simply just can't allow there
to be a warning that the user can't make go away through
some means. All other edge cases like pattern matching on
a single contructor type with expect warnings can be fixed
via other means.
2024-05-21 15:21:24 -04:00
KtorZ eadf709411
Fix scope management issue when deep-inferring callee.
Fixes #941.

  However, this currently breaks the stdlib somehow with some FreeUnique on the shrinker step of the optimizer.
2024-05-15 13:18:51 +02:00
KtorZ 81219cfbdd
Check for data-type serialisability after generic instantiation
Fixes #939.
2024-05-14 10:58:58 +02:00
KtorZ 26ef25ba8d
Make comparison of non-serialisable types illegal.
Fixes #940.
2024-05-14 10:45:15 +02:00
KtorZ 8c67be55ce
Fixes #921: top-level Miller-loop needs not to be serialisable
This is a bit tricky, but in a similar way where we allow functions to
  be returned by functions, this must also work for MillerLoopResult.
2024-05-10 13:52:23 +02:00
KtorZ 7cb548a749 Fix ordinal index on pairs 2024-05-04 14:04:12 -04:00
KtorZ 925a11be69
Check for args length when comparing types. Duh!
Fixes #917.
2024-05-01 10:48:15 +02:00
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 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 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 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
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 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
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
KtorZ 4f7f39292d
Fix subtle bug in pattern rendering
When rendering missing or redundant patterns, linked-list would
  wrongly suggest the last nil constructor as a pattern on non-empty
  list.

  For example, before this commit, the exhaustivness checker would yield:

  ```
  [(_, True), []]
  ```

  as a suggestion, for being the result of being a list pattern with a
  single argument being `(_, True) :: Nil`. Blindly following the
  compiler suggestion here would cause a type unification error (since
  `[]` doesn't unify with a 2-tuple).

  Indeed, we mustn't render the Nil constructor when rendering non-empty
  lists! So the correct suggestion should be:

  ```
  [(_, True)]
  ```
2023-08-02 10:31:35 +02:00
KtorZ 00b255e960
Remove now-dead code. 2023-08-02 09:22:21 +02:00
rvcas f3cab94ae1 test(check): a bunch of tests for the new exhaustiveness stuff 2023-08-01 21:13:50 -04:00