Commit Graph

74 Commits

Author SHA1 Message Date
KtorZ 4003343444
Fix default annotation for spend's optional datum and mint argument.
When there's no type annotation in a validator handler signature, we
  provide default annotation to help the type-checker. However, for
  spend's datum and mint policy_id, those annotations mustn't be `Data`,
  but rather Option<Data> and Bytearray.

  Without that, when no annotation are provided, the compiler infer
  invalid types and fails with incongruous errors.
2024-08-27 18:42:10 +02:00
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
rvcas ff1464b462
feat: annotated data for option datum 2024-08-25 16:20:08 +02:00
KtorZ 7ec3f2e8df
DRY builtins types creation to ensure proper consistency. 2024-08-25 16:20:06 +02:00
rvcas f94e40daf4
fix: more test and issues with scoping/names 2024-08-25 16:20:03 +02:00
rvcas 471bbe2175
feat: append validator name to handlers 2024-08-25 16:20:02 +02:00
rvcas fff90f7df5
feat: fix inference comp issues 2024-08-25 16:20:02 +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 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 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 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 3020af7cd7 Revert 'unify' implementation back to its more elegant form
And add support for Pair.
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
rvcas d22ee6e086
chore: remove useless clone 2024-04-02 19:04:33 -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
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 25e9db4f6c Rename t1 -> lhs, t2 -> rhs in unify. 2024-03-21 11:59:34 -04:00
KtorZ bee2b712de Fixes #881. 2024-03-21 11:59:34 -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 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
KtorZ c169596c76
preserve type-aliases from annotations on calls. 2024-03-10 00:38:03 +01:00
KtorZ a578728a94
Resolve type aliases based on inferred types.
Before this commit, we would always show the 'declared form' of type aliases, with their generic, non-instantiated parameters. This now tries to unify the annotation with the underlying inferred type to provide even better alias pretty printing.
2024-03-08 16:01:21 +01:00
KtorZ ed9f5c6ef7
Preserve TypeAlias in types for better context/feedback. 2024-03-08 15:59:33 +01:00
rvcas 25ebdc2527
fix: validator args unexpectedly unbound
closes #852
2024-03-06 14:15:00 -05:00
KtorZ aadf3cfb48
Allow test definition to carry one parameter
The parameter is special as it takes no annotation but a 'via' keyword followed by an expression that should unify to a Fuzzer<a>, where Fuzzer<a> = fn(Seed) -> (Seed, a). The current commit only allow name identifiers for now. Ultimately, this may allow full expressions.
2024-03-03 19:33:24 +01:00
KtorZ 3c8460e6af Allow annotating Data for blueprint
This commit allows Data to be optionally annotated with a
  phantom-type. This doesn't change anything in codegen but we can now
  leverage this information to generate better blueprint schemas.
2024-02-07 11:48:52 -05:00
microproofs 4a8fecb70a fix: satisfy clippy's demands 2024-01-11 14:53:02 -05:00
rvcas 07122aaa88
feat: allow importing off validators in validators/tests/* 2023-12-11 18:27:08 -05:00
KtorZ 28b699c86a
Merge unused imported constructors and unused imported type with unused imported value
This was somewhat weirdly done, with a boolean 'imported' set on the
  formers; but an explicit new warning for values. I don't see the point
  of distinguishing them so I just merged them all into a single
  warning.

  I have however preserved the 'UnusedType' and 'UnusedConstructor'
  warnings since they were ALSO used for unused private constructors or
  types.
2023-10-22 00:27:33 +02:00
KtorZ f6eff7ec58
Fix incoherent 'UnknownVariable' being returned in type-check
I initially removed the 'UnkownTypeConstructor' since it wasn't used anywhere and was in fact dead-code. On second thoughts however, it is nicer to provide a slightly better error message when a constructor is missing as well as some valid suggestion. Prior to that commit, we would simply return a 'UnknownVariable' and the hint might suggest lowercase identifiers; which is wrong.
2023-10-21 14:10:45 +02:00
rvcas d808197507
chore: clippy fix 2023-09-13 18:17:59 -04:00
rvcas 60ac8ab591
fix(exhaustiveness): adjust helper method to get contructors properly 2023-08-03 16:14:42 -04:00
KtorZ 00b255e960
Remove now-dead code. 2023-08-02 09:22:21 +02:00
rvcas 75e18d485d fix: redundant might be wildcard which doesn't match technically 2023-08-01 21:13:50 -04:00
rvcas a6b230aad4 fix: exhaustiveness on types from other modules 2023-08-01 21:13:50 -04:00
rvcas 7e531d0da1 fix: wrong var for name in UnknownModule error 2023-08-01 21:13:50 -04:00
rvcas b6ac39f322 feat(exhaustiveness): show both clauses in redundant error 2023-08-01 21:13:50 -04:00
rvcas f1100e901d feat(exhaustiveness): pretty print missing patterns 2023-08-01 21:13:50 -04:00
rvcas a124a16a61
feat(tests): implement a way to express that tests can fail 2023-05-25 16:54:53 -04:00
rvcas 1444c9328d
fix some typos 2023-04-07 16:51:18 -04:00