Commit Graph

77 Commits

Author SHA1 Message Date
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 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 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
KtorZ 00d1927dad Add few more test cases for the parser and type-checker. 2024-06-25 18:50:00 -04:00
rvcas aeb079334e chore: this test doesn't make sense anymore 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
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