Commit Graph

130 Commits

Author SHA1 Message Date
KtorZ 0510ca58f7
Implement record access syntax for validator handlers.
This is a little trick which detects record access and replace them
  with a simple var. The var itself is the validator handler name,
  though since it contains dots, it cannot be referred to by users
  explicitly. Yet fundamentally, it is semantically equivalent to just
  calling the function by its name.

  Note that this commit also removes the weird backdoor for allowing
  importing validators in modules starting with `tests`. Allowing
  validators handler to be used in importable module requires more work
  and is arguably useful; so we will wait until someone complain and
  reconsider the proper way to do it.
2024-08-27 17:16:15 +02:00
KtorZ d74e36d0bc
Introduce 'Never' type as a safe alternative to always None options
Unfortunately, as documented in:

  https://github.com/IntersectMBO/cardano-ledger/issues/4571

  Some Option fields in the script context certificates are going to
  remain set to None, at least until the next Hard fork. There's a risk
  that people permanently lock their funds if they expect deposits on
  registration credentials to ever be `Some`.

  So, we introduce a special type that emulate an `Option` that can only
  ever be `None`. We call it `Never` and it is the first type of this
  kind (i.e. with constructors indexes not starting at 0).
2024-08-27 14:40:39 +02:00
rvcas 4589c51cd3
feat: enforcement that spend first arg is option 2024-08-25 16:20:07 +02:00
KtorZ f9acbd3bcb
DRY handlers generation from validator 2024-08-25 16:20:07 +02:00
KtorZ fe205e360f
Update remaining script context e2e tests. 2024-08-25 16:20:06 +02:00
KtorZ 7ec3f2e8df
DRY builtins types creation to ensure proper consistency. 2024-08-25 16:20:06 +02:00
rvcas 5b61a75088
feat: handler withdraw purpose 2024-08-25 16:20:06 +02:00
microproofs 953ee6b5d1
Fix ordering for ScriptInfo type 2024-08-25 16:20:05 +02:00
rvcas c2c4bddfb3
feat: new check for valid purpose names 2024-08-25 16:20:05 +02:00
KtorZ 5cf0a4d294
Fix validator arity check
For now, this panics, but ideally, we should return a "unknown
  purpose" error when we cannot map the name to an arity.
2024-08-25 16:20:04 +02:00
KtorZ 972e9bd763
Define ScriptPurpose & ScriptContext types in prelude, fix codegen new v3 wrapper. 2024-08-25 16:20:04 +02:00
rvcas 7f26db401c
feat: handler implicit some and none 2024-08-25 16:20:03 +02:00
rvcas 0d8d80e5a7
feat: transform TypedValidator in a function of handlers 2024-08-25 16:20:03 +02:00
rvcas b984f0455a
feat: return a vec instead of Option 2024-08-25 16:20:02 +02:00
rvcas 0de5cbc74e
feat: implement new validator parsing 2024-08-25 16:20:01 +02: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 9d8fdf787c
Improve formatter on long-lines, in particular bin-ops. 2024-08-06 19:25:35 +02:00
KtorZ 91e0e2493a
Provide better errors on unknown type in cyclic definitions.
Let's consider the following case:

  ```
  type Var =
    Integer

  type Vars =
    List<Var>
  ```

  This incorrectly reports an infinite cycle; due to the inability to
  properly type-check `Var` which is also a dependent var of `Vars`. Yet
  the real issue here being that `Integer` is an unknown type.

  This commit also upgrades miette to 7.2.0, so that we can also display
  a better error output when the problem is actually a cycle.
2024-08-06 19:24:48 +02:00
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 2dca0c4185
Ensure env modules dependencies are properly handled.
We figure out dependencies by looking at 'use' definition in parsed
  modules. However, in the case of environment modules, we must consider
  all of them when seeing "use env". Without that, the env modules are
  simply compiled in parallel and may not yet have been compiled when
  they are needed as actual dependencies.
2024-08-04 10:33:58 +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 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
rvcas 5bdea11cc1 fix: add a new assignment kind instead of using a boolean 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
KtorZ c48f15a957
revert #903 'feat: Emit keyword'
While we agree on the idea of having some ways of emitting events, the
  design hasn't been completely fleshed out and it is unclear whether
  events should have a well-defined format independent of the framework
  / compiler and what this format should be.

  So we need more time discussing and agreeing about what use case we
  are actually trying to solve with that.

  Irrespective of that, some cleanup was also needed on the UPLC side
  anyway since the PR introduced a lot of needless duplications.
2024-05-23 17:22:12 +02:00
rvcas 7f38b55c1c
fix: comments in record patterns closes #946 2024-05-22 12:26:36 -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 3dd94983bd Revert "fixing more pair issues"
This reverts commit b76cc7436294cd73e7bbaf656c76a8f8b0ad56a9.
2024-05-04 14:04:12 -04:00
microproofs 46c7cb797a fixing more pair issues 2024-05-04 14:04:12 -04:00
microproofs ebe415cfc9 fix errors 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
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 d25b8f91c7 feat: Emit keyword 2024-04-12 21:40:27 -04:00
rvcas 7c5b9aa35e
feat(lsp): find_node for TypedArgVia 2024-04-02 19:22:19 -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
rvcas 97247ce949 chore: assignment patterns refactor tuple into struct 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 435dd0d213
Refactor AssignmentKind to allow backpassing on both let and expect.
The 3rd kind of assignment kind (Bind) is gone and now reflected through a boolean parameter. Note that this parameter is completely erased by the type-checker so that the rest of the pipeline (i.e. code-generation) doesn't have to make any assumption. They simply can't see a backpassing let or expect.
2024-03-11 00:16:23 +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 1f530f3b24
Experiment with monadic bind. 2024-03-11 00:16:22 +01:00
KtorZ 191e4d47b3
Remove dead-code: 'Layer' 2024-03-09 23:14:44 +01:00