Commit Graph

144 Commits

Author SHA1 Message Date
KtorZ 7ec3f2e8df
DRY builtins types creation to ensure proper consistency. 2024-08-25 16:20:06 +02:00
KtorZ 9aa9070f56
Revise desugaring following feedback
- We now consistently desugar an expect in the last position as
    `Void`. Regardless of the pattern. Desugaring to a boolean value is
    deemed too confusing.

  - This commit also removes the desugaring for let-binding. It's only
    ever allowed for _expect_ which then behaves like a side effect.

  - We also now allow tests to return either `Bool` or `Void`. A test
    that returns `Void` is treated the same as a test returning `True`.
2024-08-23 16:04:40 +02:00
KtorZ fbe6f02fd1
Allow assignment as last expression
This is debatable, but I would argue that it's been sufficiently
  annoying for people and such a low-hanging fruit that we ought to do
  something about it.

  The strategy here is simple: when we find a sequence of expression
  that ends with an assignment (let or expect), we can simply desugar it
  into two expressions: the assignment followed by either `Void` or a
  boolean.

  The latter is used when the assignment pattern is itself a boolean;
  the next boolean becomes the expected value. The former, `Void`, is
  used for everything else. So said differently, any assignment
  implicitly _returns Void_, except for boolean which return the actual
  patterned bool.

  <table>
  <thead><tr><th>expression</th><th>desugar into</th></tr></thead>
  <tbody>
  <tr>
  <td>

  ```aiken
  fn expect_bool(data: Data) -> Void {
    expect _: Bool = data
  }
  ```
  </td>
  <td>

  ```aiken
  fn expect_bool(data: Data) -> Void {
    expect _: Bool = data
    Void
  }
  ```
  </td>
  </tr>
  <tr>
  <td>

  ```aiken
  fn weird_maths() -> Bool {
    expect 1 == 2
  }
  ```
  </td>
  <td>

  ```aiken
  fn weird_maths() -> Bool {
    expect True = 1 == 2
    True
  }
  ```
  </td>
  </tr>
  </tbody>
  </table>
2024-08-23 16:04:39 +02:00
Riley-Kilgore cab58e5aab One other place 2024-08-12 17:57:54 -04:00
Riley-Kilgore 213ad48de7 Fixed span calculation for backpassing (sort of) 2024-08-12 17:57:54 -04:00
KtorZ a6c5dbb5ad Thread down if/is pattern assignment type down to code-generation.
This isn't sufficient however, as the 'assignment' helper handling
  code generation doesn't perform any check when patterns are vars. This
  is curious, and need to be investigated further.
2024-08-08 00:39:44 -04:00
KtorZ 6de1d91104
Create dedicated error when environment isn't found.
This is less confusing that getting an 'UnknownModule' error reporting
  even a different module name than the one actually being important
  ('env').

  Also, this commit fixes a few errors found in the type-checker
  when reporting 'UnknownModule' errors. About half the time, we would
  actually attached _imported modules_ instead of _importable modules_
  to the error, making the neighboring suggestion quite worse (nay
  useless).
2024-08-04 14:48:03 +02:00
KtorZ bf5a406ffb Remove clause guards.
Closes #886.
2024-08-02 00:16:27 -04:00
KtorZ 67493ad847
Fix casting inferrence on patterns
The original goal for this commit was to allow casting from Data on
  patterns without annotation. For example, given some custom type
  'OrderDatum':

  ```
  expect OrderDatum { requested_handle, destination, .. }: OrderDatum = datum
  ```

  would work fine, but:

  ```
  expect OrderDatum { requested_handle, destination, .. } = datum
  ```

  Yet, the annotation feels unnecessary at this point because type can
  be inferred from the pattern itself. So this commit allows, whenever
  possible (ie when the pattern is neither a discard nor a var), to
  infer the type from a pattern.

  Along the way, I also found a couple of weird behaviours surrounding
  this kind of assignments, in particular in combination with let. I'll
  highlight those in the next PR (#979).
2024-07-24 12:42:24 +02:00
KtorZ d6fd37c80e
Rework 'compact' mode for traces
- Trace-if-false are now completely discarded in compact mode.

  - Only the label (i.e. first trace argument) is preserved.

  - When compiling with tracing _compact_, the first label MUST unify to
    a string. This shouldn't be an issue generally speaking and would
    enforce that traces follow the pattern

    ```
    label: arg_0[, arg_1, ..., arg_n]
    ```

  Note that what isn't obvious with these changes is that we now support
  what the "emit" keyword was trying to achieve; as we compile now with
  user-defined traces only, and in compact mode to only keep event
  labels in the final contract; while allowing larger payloads with
  verbose tracing.
2024-07-19 12:28:08 +02:00
KtorZ 5afcc9b0c1
Remove unnecessary code_gen patch.
This is a little weird but, prelude functions are handled slightly
  differently.
2024-07-19 12:28:07 +02:00
KtorZ f8236817fe
Allow serialisable (Data-able) arguments to trace
Somehow, we have to patch some function in gen_uplc because of the
  module name. I have to look further into this because it isn't normal.
2024-07-19 12:28:07 +02:00
KtorZ beb5ac4643
Add 'diagnostic' to the prelude, as well as companion functions.
This is not fully satisfactory as it pollutes a bit the prelude. Ideally, those functions should only be visible
  and usable by the underlying trace code. But for now, we'll just go with it.
2024-07-19 12:28:07 +02:00
KtorZ 754ed07408
Type-check variadic traces & desugarize them. 2024-07-18 10:02:23 +02:00
KtorZ f9719af23e
Allow variadic arguments in trace
Although, doesn't do anything with them yet. The idea is to simplify
  the use of trace to make it a lot more useful than it currently is.
2024-07-18 10:01:34 +02:00
KtorZ 976262c2e6
Allow discard in expect.
Fixes #967.
2024-07-17 18:11:09 +02:00
rvcas 5bdea11cc1 fix: add a new assignment kind instead of using a boolean 2024-06-25 18:50:00 -04:00
rvcas 579abb7d3d fix: no need to check exhaustiveness during if/is 2024-06-25 18:50:00 -04:00
rvcas 1b8805825b feat: impl if/is
This commit introduces a new feature into
the parser, typechecker, and formatter.
The work for code gen will be in the next commit.

I was able to leverage some existing infrastructure
by making using of `AssignmentPattern`. A new field
`is` was introduced into `IfBranch`. This field holds
a generic `Option<Is>` meaning a new generic has to be
introduced into `IfBranch`. When used in `UntypedExpr`,
`IfBranch` must use `AssignmentPattern`. When used in
`TypedExpr`, `IfBranch` must use `TypedPattern`.

The parser was updated such that we can support this
kind of psuedo grammar:

`if <expr:condition> [is [<pattern>: ]<annotation>]`

This can be read as, when parsing an `if` expression,
always expect an expression after the keyword `if`. And then
optionally there may be this `is` stuff, and within that you
may optionally expect a pattern followed by a colon. We will
always expect an annotation.

This first expression is still saved as the field
`condition` in `IfBranch`. If `pattern` is not there
AND `expr:condition` is `UntypedExpr::Var` we can set
the pattern to be `Pattern::Var` with the same name. From
there shadowing should allow this syntax sugar to feel
kinda magical within the `IfBranch` block that follow.

The typechecker doesn't need to be aware of the sugar
described above. The typechecker looks at `branch.is`
and if it's `Some(is)` then it'll use `infer_assignment`
for some help. Because of the way that `is` can inject
variables into the scope of the branch's block and since
it's basically just like how `expect` works minus the error
we get to re-use that helper method.

It's important to note that in the typechecker, if `is`
is `Some(_)` then we do not enforce that `condition` is
of type `Bool`. This is because the bool itself will be
whether or not the `is` itself holds true given a PlutusData
payload.

When `is` is None, we do exactly what was being done
previously so that plain `if` expressions remain unaffected
with no semantic changes.

The formatter had to be made aware of the new changes with
some simple changes that need no further explanation.
2024-06-25 18:50:00 -04:00
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
KtorZ b6da42baf2
Bump 'is_validator_param' up from 'ArgName' to '...Arg'
There's no reasons for this to be a property of only ArgName::Named to begin with. And now, with the extra indirection introduced for arg_name, it may leads to subtle issues when patterns args are used in validators.
2024-06-07 11:32:05 +02:00
KtorZ 4d42c6cb19
Introduce 'ArgBy' to allow defining function arg not only by name. 2024-06-07 11:17:16 +02:00
KtorZ 5694d9f9cb
Introduce 'fail once' and alter behavior of 'fail' keyword for properties. 2024-05-30 17:18:50 +02:00
rvcas 7f38b55c1c
fix: comments in record patterns closes #946 2024-05-22 12:26:36 -04: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 ea3e79c132
Renamed 'unseed' -> 'not_yet_inferred' 2024-05-16 23:33:23 +02:00
KtorZ 27b3536f09
Also preserve warnings when resetting scope for backtracking.
This is crucial as some checks regarding variable usages depends on
  warnings; so we may accidentally remove variables from the AST as a
  consequence of backtracking for deep inferrence.
2024-05-16 23:20:52 +02: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 a124bdbb05 Infer callee first in function call
The current inferrence system walks expressions from "top to bottom".
  Starting from definitions higher in the source file, and down. When a
  call is encountered, we use the information known for the callee
  definition we have at the moment it is inferred.

  This causes interesting issues in the case where the callee doesn't
  have annotations and in only partially known. For example:

  ```
  pub fn list(fuzzer: Option<a>) -> Option<List<a>> {
    inner(fuzzer, [])
  }

  fn inner(fuzzer, xs) -> Option<List<b>> {
    when fuzzer is {
      None -> Some(xs)
      Some(x) -> Some([x, ..xs])
    }
  }
  ```

  In this small program, we infer `list` first and run into `inner`.
  Yet, the arguments for `inner` are not annotated, so since we haven't
  inferred `inner` yet, we will create two unbound variables.

  And naturally, we will link the type of `[]` to being of the same type
  as `xs` -- which is still unbound at this point. The return type of
  `inner` is given by the annotation, so all-in-all, the unification
  will work without ever having to commit to a type of `[]`.

  It is only later, when `inner` is inferred, that we will generalise
  the unbound type of `xs` to a generic which the same as `b` in the
  annotation. At this point, `[]` is also typed with this same generic,
  which has a different id than `a` in `list` since it comes from
  another type definition.

  This is unfortunate and will cause issues down the line for the code
  generation. The problem doesn't occur when `inner`'s arguments are
  properly annotated or, when `inner` is actually inferred first.

  Hence, I saw two possible avenues for fixing this problem:

  1. Detect the presence of 'uncongruous generics' in definitions after
     they've all been inferred, and raise a user error asking for more
     annotations.

  2. Infer definitions in dependency order, with definitions used in
     other inferred first.

  This commit does (2) (although it may still be a good idea to do (1)
  eventually) since it offers a much better user experience. One way to
  do (2) is to construct a dependency graph between function calls, and
  ensure perform a topological sort.

  Building such graph is, however, quite tricky as it requires walking
  through the AST while maintaining scope etc. which is more-or-less
  already what the inferrence step is doing; so it feels like double
  work.

  Thus instead, this commit tries to do a deep-first inferrence and
  "pause" inferrence of definitions when encountering a call to fully
  infer the callee first. To achieve this properly, we must ensure that
  we do not infer the same definition again, so we "remember" already
  inferred definitions in the environment now.
2024-05-06 15:17:01 -04:00
KtorZ 7cb548a749 Fix ordinal index on pairs 2024-05-04 14:04:12 -04:00
KtorZ 2cb2c7fa1f Add dedicated 'Pair' typed and untyped expression
Before this commit, we would parse 'Pair' as a user-defined
  data-types, and thus piggybacking on that whole record system. While
  perhaps handy for some things, it's also semantically wrong and
  induces a lot more complexity in codegen which now needs to
  systematically distinguish every data-type access between pairs, and
  others.

  So it's better to have it as a separate expression, and handle it
  similar to tuples (since it's fundamentally a 2-tuple with a special
  serialization).
2024-05-04 14:04:12 -04:00
microproofs 7b5ad961e2 fix: found issue with record access on Pairs 2024-05-04 14:04:12 -04:00
microproofs 61a021f9e3 update pair to handle alias 2024-05-04 14:04:12 -04:00
Micah Kendall ff4ddfbe1b Simplifying PR per reviewers request 2024-04-12 21:40:27 -04:00
Micah Kendall d39dbd6697 fmt 2024-04-12 21:40:27 -04:00
Micah Kendall d25b8f91c7 feat: Emit keyword 2024-04-12 21:40:27 -04:00
rvcas b27fcf38e5
fix(check): collapse_links on tuple_index access closes #905 2024-04-02 19:45:16 -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 e71470747f
feat: fix some tests and add a failing one 2024-03-13 20:18:56 -04:00
KtorZ 9127dcdd6e
Add note on the type-casting check. 2024-03-13 20:18:56 -04:00
KtorZ 8f31b45e36
Fix allow_casting condition in unification
We should allow casting from any type to any type. Or at the very least, allow it for well-known types like List.
2024-03-13 20:18:56 -04:00
KtorZ f10cf73905
Rework 'is_opaque' to also check for inner types.
Also removed the duplication in infer_assignment and moved the check down.
2024-03-13 20:18:56 -04:00
KtorZ 3820d2af14
Remove potentially problematic use of ".." in pattern-match
Discard pattern are _dangerous_ is used recklessly. The problem comes
  from maintenance and when adding new fields. We usually don't get any
  compiler warnings which may lead to missing spots and confusing
  behaviors.

  So I have, in some cases, inline discard to explicitly list all
  fields. That's a bit more cumbersome to write but hopefully will catch
  a few things for us in the future.
2024-03-13 20:18:51 -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