Commit Graph

877 Commits

Author SHA1 Message Date
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 d7ec2131ef
Automatically merge import lines from same module.
I slightly altered the way we parse import definitions to ensure we
  merge imports from the same modules (that aren't aliased) together.

  This prevents an annoying warning with duplicated import lines and
  makes it just more convenient overall.

  As a trade-off, we can no longer interleave import definitions with
  other definitions. This should be a minor setback only since the
  formatter was already ensuring that all import definitions would be
  grouped at the top.

  ---

  Note that, I originally attempted to implement this in the formatter
  instead of the parser. As it felt more appropriate there. However, the
  formatter operates on (unmutable) borrowed definitions, which makes it
  annoyingly hard to perform any AST manipulations. The `Document`
  returns by the format carries a lifetime that prevents the creation of
  intermediate local values.

  So instead, slightly tweaking the parser felt like the right thing to
  do.
2024-06-04 10:48:42 +02:00
KtorZ e9e26b969a
Preserve warning display rework, but without breaking the LSP quickfixes. 2024-05-30 19:20:11 +02:00
KtorZ 649e5163fc
Fix parsing of single hex-digits. 2024-05-30 17:19:48 +02:00
KtorZ 5694d9f9cb
Introduce 'fail once' and alter behavior of 'fail' keyword for properties. 2024-05-30 17:18:50 +02:00
microproofs 59cfa209d7 change uplc version number based on plutus version 2024-05-23 15:04:59 -04: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
KtorZ 5ce30b2632
Rename AList -> Pairs due to popular demand. 2024-05-23 16:45:40 +02:00
rvcas 7f38b55c1c
fix: comments in record patterns closes #946 2024-05-22 12:26:36 -04:00
rvcas 3bc3792aa3
feat: add plutus version to aiken.toml
relates to #907
2024-05-21 17:02:20 -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
microproofs 878298cc8e don't use generic data type lookup when you have a Record Variant as a function 2024-05-06 15:17:01 -04: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 ef70c6b8a8 Re-use generic id across builtin type-definitions.
This was somehow wrong and corrected by codegen later on, but we should be re-using the same generic id across an entire definition if the variable refers to the same element.
2024-05-06 15:17:01 -04:00
KtorZ 1070347203 Panic when encountering unknown generics.
This should not happen; if it does, it's an error from the type-checker. So instead of silently swallowing the error and adopting a behavior which is only _sometimes_ right, it is better to fail loudly and investigate.
2024-05-06 15:17:01 -04:00
microproofs b2661ef90a Better error message for compile time evaluation 2024-05-06 11:58:32 -04:00
microproofs a44ed4c1a8 Change prelude Map to AList 2024-05-04 14:04:12 -04:00
KtorZ b1f0dfdacd Implement parser & formatter for Pair annotations. 2024-05-04 14:04:12 -04:00
microproofs 58779401e8 fix: formatting was eating the space in pair after the , 2024-05-04 14:04:12 -04:00
microproofs fc0e88018e Chore:
Refactor get_uplc_type to account for constr types that don't exactly resolve to a uplc type
Check arg_stack in uplc generator has only 1 argument at the end of the generation
warning fixes
2024-05-04 14:04:12 -04:00
KtorZ 1091eba3c3 Review & fix acceptance tests
Temporarily using the 'specialize-dict-key' branch from the stdlib
  which makes use of Pair where relevant. Once this is merged back into
  'main' we should update the acceptance test toml files to keep getting
  them automatically upgraded.

  This commit also fixes an oversight in the reification of data-types
  now properly distinguishing between pairs and 2-tuples.

  Co-authored-by: Microproofs <kasey.white@cardanofoundation.org>
2024-05-04 14:04:12 -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 92a1da69d9 Add (possibly temporary) assertion on record access in codegen 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 5c59b816ea Add parser for 'Pair' pattern
And a few more tests along the way for others. Note that it is important here that we try to parse for a 'Pair' BEFORE we try to parse for a constructor pattern. Because the latter would swallow any Pair pattern.
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
KtorZ cbf3ef2854 Add new Prelude alias: 'Map' 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 30dd1f60e7 small simplification 2024-05-04 14:04:12 -04:00
microproofs 75b076552c feat: Do a major overhaul on how we check types to allow for match patterns instead of if statements
Also fix one more test
2024-05-04 14:04:12 -04:00
microproofs 3c332ca42a Few more places in codegen where we need to be able to deal with Pair records 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