Commit Graph

47 Commits

Author SHA1 Message Date
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
rvcas a6b230aad4 fix: exhaustiveness on types from other modules 2023-08-01 21:13:50 -04:00
rvcas 1b8e94fe32
feat: expect boolean sugar 2023-07-15 20:50:02 -04:00
rvcas 3b351d36fb
fix(aiken-lang): assignment as last expr in when and if 2023-04-16 19:55:47 -04:00
rvcas 98c61ca151
feat(aiken-lang): anonymous functions
@MartinSchere noticed a weird error
where an unknown variable wasn't being reported
the type checker was incorrectly scoping
arguments for anonymous function definitions.
Luckily his compilation failed due to a FreeUnique
error during code gen which is good. But this may
have been the source of other mysterious FreeUnique
errors.

I also noticed that anonymous function allowed
arguments with the same name to be defined.

`fn(arg, arg)`

This now returns an error.
2023-04-16 16:38:43 -04:00
rvcas d8cbcde61d feat(validators): unused param warning
Params being unused were being incorrectly reported.
This was because params need to be initialized
at a scope above both the validator functions. This
manifested when using a multi-validator where one of
the params was not used in both validators.

The easy fix was to add a field called
`is_validator_param` to `ArgName`. Then
when infering a function we don't initialize args
that are validator params. We now handle this
in a scope that is created before in the match branch for
validator in the `infer_definition` function. In there
we call `.in_new_scope` and initialize params for usage
detection.
2023-03-30 21:15:27 -04:00
rvcas ed92869fb9
feat(validator): parsing and typechecking for double validators 2023-03-17 18:38:24 -04:00
KtorZ 660ca3fada Fix comment formatting wrongly assuming false invariant. 2023-03-16 18:44:11 -04:00
KtorZ 57e217e81c Add failing tests (fmt panic) on weird doc comments.
Isolated doc comments causes the compiler to panic with:

  ```
  'no consecutive empty lines'
  ```

  This is reproducible when doc comments are wrapped in sandwich between
  comments and newlines.
2023-03-16 18:44:11 -04:00
KtorZ a5e505e6b0 Remove unused let-binding from type-checking
The typed-AST produced as a result of type-checking the program will
  no longer contain unused let-bindings. They still raise warnings in
  the code so that developers are aware that they are being ignore.

  This is mainly done to prevent mistakes for people coming from an
  imperative background who may think that things like:

  ```
  let _ = foo(...)
  ```

  should have some side-effects. It does not, and it's similar to
  assigned variables that are never used / evaluated. We now properly
  strip those elements from the AST when encountered and raise proper
  warnings, even for discarded values.
2023-03-16 15:29:44 -04:00
KtorZ 78770d14b7
Emit warning when detecting an hex string interpreted as UTF-8 bytes.
This will probably save people minutes/hours of puzzled debugging. This is only a warning because there may be cases where one do actually want to specify an hex-encoded bytearray. In which case, they can get rid of the warning by using the plain bytearray syntax (i.e. as an array of bytes).
2023-02-19 10:10:42 +01:00
KtorZ 53fb821b62
Use double-quotes for utf-8 bytearrays, and @"..." for string literals
The core observation is that **in the context of Aiken** (i.e. on-chain logic)
  people do not generally want to use String. Instead, they want
  bytearrays.

  So, it should be easy to produce bytearrays when needed and it should
  be the default. Before this commit, `"foo"` would parse as a `String`.
  Now, it parses as a `ByteArray`, whose bytes are the UTF-8 bytes
  encoding of "foo".

  Now, to make this change really "fool-proof", we now want to:

  - [ ] Emit a parse error if we parse a UTF-8 bytearray literal in
    place where we would expect a `String`. For example, `trace`,
    `error` and `todo` can only be followed by a `String`.

    So when we see something like:

    ```
    trace "foo"
    ```

    we know it's a mistake and we can suggest users to use:

    ```
    trace @"foo"
    ```

    instead.

  - [ ] Emit a warning if we ever see a bytearray literals UTF-8, which
    is either 56 or 64 character long and is a valid hexadecimal string.
    For example:

    ```
    let policy_id = "29d222ce763455e3d7a09a665ce554f00ac89d2e99a1a83d267170c6"
    ```

    This is _most certainly_ a mistake, as this generates a ByteArray of
    56 bytes, which is effectively the hex-encoding of the provided string.

    In this scenario, we want to warn the user and inform them they probably meant to use:

    ```
    let policy_id = #"29d222ce763455e3d7a09a665ce554f00ac89d2e99a1a83d267170c6"
    ```
2023-02-19 10:09:22 +01:00
KtorZ e9e3f4f50a Implement TraceIfFalse type-checking and AST transformation.
This caused me some trouble. In my first approach, I ended up having
  multiple traces because nested values would be evaluated twice; once
  as condition, and once as part of the continuation.

  To prevent this, we can simply evaluate the condition once, and return
  plain True / False boolean as outcome. So this effectively transforms any
  expression:

  ```
  expr
  ```

  as

  ```
  if expr { True } else { trace("...", False) }
  ```
2023-02-16 20:29:41 -05:00
KtorZ 6a50bde666 Implement parser & formater for 'TraceIfFalse'
Interestingly enough, chumsky seems to fail when given a 'choice' with
  more than 25 elements. That's why this commit groups together some of
  the choices as another nested 'choice'.
2023-02-16 20:29:41 -05:00
rvcas c4a588f3dd test(check): if scoping 2023-02-16 00:05:55 -05:00
rvcas 7b0faa7c1c test(check): validator errors and warning 2023-02-16 00:05:55 -05:00
KtorZ 7abd76b6ad
Allow to trace expressions (and not only string literals)
This however enforces that the argument unifies to a `String`. So this
  is more flexible than the previous form, but does fundamentally the
  same thing.

  Fixes #378.
2023-02-15 21:07:56 +01:00
KtorZ 6649821200
Add type-checker sanity tests for list patterns. 2023-02-11 16:54:49 +01:00