Commit Graph

276 Commits

Author SHA1 Message Date
KtorZ 6454266b06
Allow simple expressions as configuration in aiken.toml
This is currently extremely limited as it only supports (UTF-8)
  bytearrays and integers. We should seek to at least support hex bytes
  sequences, as well as bools, lists and possibly options.

  For the latter, we the rework on constant outlined in #992 is
  necessary.
2024-08-04 14:48:03 +02: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 fbe2f82582
Thread down environment module from cli down to the type-checker
We simply provide a flag with a free-form output which acts as
  the module to lookup in the 'env' folder. The strategy is to replace
  the environment module name on-the-fly when a user tries to import
  'env'.

  If the environment isn't found, an 'UnknownModule' error is raised
  (which I will slightly adjust in a following commits to something more
  related to environment)

  There are few important consequences to this design which may not seem
  immediately obvious:

  1. We parse and type-check every env modules, even if they aren't
     used. This ensures that code doesn't break with a compilation error
     simply because people forgot to type-check a given env.

     Note that compilation could still fail because the env module
     itself could provide an invalid API. So it only prevents each
     modules to be independently wrong when taken in isolation.

  2. Technically, this also means that one can import env modules in
     other env modules by their names. I don't know if it's a good or
     bad idea at this point but it doesn't really do any wrong;
     dependencies and cycles are handlded all-the-same.
2024-08-04 10:27:32 +02:00
KtorZ c9d0da0c22
Parse sources of conditional env modules.
Do nothing about it yet, but trigger an error if env/default.ak is
  missing; but only if there's any module at all under env.
2024-08-03 17:42:55 +02:00
KtorZ f14dfdf8e1
Allow pattern-matching on bytearrays
- Doesn't allow pattern-matching on G1/G2 elements and strings,
    because the use cases for those is unclear and it adds complexity to
    the feature.

  - We still _parse_ patterns on G1/G2 elements and strings, but emit an
    error in those cases.

  - The syntax is the same as for bytearray literals (i.e. supports hex,
    utf-8 strings or plain arrays of bytes).
2024-08-03 13:51:36 +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 0ebffa2b9e
Fix few error messages. 2024-06-13 14:54:47 +02: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 e9e26b969a
Preserve warning display rework, but without breaking the LSP quickfixes. 2024-05-30 19:20:11 +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 a3c14d881d
Merge branch 'fix/scope-when-backtracking' 2024-05-16 23:43:00 +02:00
KtorZ 7ff6eba869
Prefer '.clone_from' over mutating a clone.
Clippy says it's more efficient. I trust clippy. Clippy good.
2024-05-16 23:42:53 +02: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 e87063824c
Fix pretty-printing of recursive type-alias causing stack overflow.
Fixes #942.
2024-05-16 17:20:26 +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 7b71389519 Change pretty-printing of unbound variable to '?'
Until now, we would pretty-print unbound variable the same way we would pretty-print generics. This turned out to be very confusing when debugging, as they have a quite different semantic and it helps to visualize unbound types in definitions.
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
KtorZ 91a7e77ab4 Add 'Pair' pattern and rework internals to use it.
Currently, pattern-matching on 'Pair' is handled by treating Pair as a
  record, which comes as slightly odd given that it isn't actually a
  record and isn't user-defined. Thus now, every use of a record must
  distinguish between Pairs and other kind of records -- which screams
  for another variant constructor instead.

  We cannot use `Tuple` either for this, because then we have no ways to
  tell 2-tuples apart from pairs, which is the whole point here. So the
  most sensical thing to do is to define a new pattern `Pair` which is
  akin to tuples, but simpler since we know the number of elements and
  it's always 2.
2024-05-04 14:04:12 -04:00
KtorZ 897b5d1d7e Ensure type-aliases pretty-printing also work with Pair. 2024-05-04 14:04:12 -04:00
KtorZ 3020af7cd7 Revert 'unify' implementation back to its more elegant form
And add support for Pair.
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 26f68c2fb4 fix: found various unify and type issues while running tests 2024-05-04 14:04:12 -04:00
microproofs 61a021f9e3 update pair to handle alias 2024-05-04 14:04:12 -04:00
microproofs d05d8e7de6 Start working on separating pairs from 2 tuples in Aiken
co-authored-by: KtorZ <matthias.benkort@gmail.com>
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 d22ee6e086
chore: remove useless clone 2024-04-02 19:04:33 -04:00