Commit Graph

53 Commits

Author SHA1 Message Date
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
rvcas 87493bbba9
feat(register_values): refactor repeated code into register_function and register other_fun 2023-03-17 18:38:24 -04:00
KtorZ d59305a1b0
Provide better compiler feedback for type holes in annotations.
It is now possible to leave a hole in a type annotation and have the compiler fill-in the expected type of us.
  This is a pretty useful debugging tool when playing with complex functions.
2023-03-16 14:07:06 +01:00
rvcas 553eb88d3d fix(check): record field access properly restricted to single constr types 2023-03-08 23:50:16 -05:00
rvcas 41e725152e
feat(unify): cannot cast between string and data closes #432 2023-03-08 22:47:38 -05:00
rvcas a044c3580e feat: typecheck validators 2023-02-16 00:05:55 -05:00
rvcas 2e7fe191db feat(definitions):
* add parsing for new validator defs
* start adding typechecking
* add a unit test for parsing
2023-02-16 00:05:55 -05:00
KtorZ 3c7663cd3c
Basic exhaustivness check on list patterns
Before that commit, the type-checker would allow unsafe list patterns
  such as:

  ```
  let [x] = xs

  when xs is {
    [x] -> ...
    [x, ..] ->  ...
  }
  ```

  This is quite unsafe and can lead to confusing situations. Now at
  least the compiler warns about this. It isn't perfect though,
  especially in the presence of clause guards. But that's a start.
2023-02-11 16:20:28 +01:00
KtorZ 21fbd48b8d
Improve error on duplicate imports. 2023-02-10 17:07:08 +01:00
rvcas ddad05bf51
chore: leave a comment for later 2023-02-04 15:33:18 -05:00
rvcas c126f6acda feat: invert how casting is controlled
I decided to invert how I'm doing it. I'm passing
in a new argument to unify in environment called
allow_cast: bool and essentially at various
unification sites I can control whether or not I
want to allow casting to even occur. So we can
assume it's false by default always and then we
turn it on in a few places vs. just opening the
flood gates and locking it down at various sites
as they come up# Please enter the commit message
for your changes. Lines starting
2023-02-04 02:33:10 -05:00
rvcas 2b554d105a fix: when Data cast bypass 2023-02-04 02:33:10 -05:00
rvcas a9ed04ef22 feat: newer rules around casting Data
* you cannot cast FROM Data with a `let`
* you cannot cast FROM Data by passing
  Data to none Data when calling a function
* you MUST use `assert` to cast from data
* you can cast INTO Data with a `let`
* you can cast INTO Data by passing none Data
  to Data when calling a function
* You cannot assert cast Data without an
  annotation
2023-02-04 02:33:10 -05:00
rvcas 39e0716f5f
feat: better rules around Data casting
* you cannot cast to Data ever
* you can cast from Data to ANY TYPE
* you cannot cast via a function call arg hack
2023-02-02 00:43:45 -05:00
KtorZ 4459fdb360
Fix error reporting on cyclic definitions.
Fixes #292
2023-01-20 20:09:00 +01:00
rvcas 1adac64585 feat(imports): return a nice error if a validator module is imported 2023-01-15 18:54:35 -05:00
rvcas c66d07a54c feat: validator fns no longer need to be public
If the function doesn't match a script purpose
and is unused then it will till present as a
warning.
2023-01-15 12:33:10 -05:00
KtorZ 69f060e675
Rework all errors to provide better help text. 2022-12-23 19:27:06 +01:00
KtorZ ce0c6e0d0f
Use smart-constructor for UnexpectedLabeledArg errors.
Reduce duplications and keep the formatting of the error inside the error module.
2022-12-23 00:24:57 +01:00
KtorZ dca633da48
Refactor 'UnknownVariable' and 'UnknownTypeConstructor' as smart-constructor. 2022-12-23 00:09:07 +01:00
KtorZ aa2a235790
Suggest possible candidate on unknown imports.
## Before

  ```
  × Type-checking
  ╰─▶ Unknown module field 'ValidityRaneg' in module 'aiken/transaction'
  ```

  ## After

  ```
    × Type-checking
    ╰─▶ Unknown import 'ValidityRaneg' from module 'aiken/transaction'

     ╭─[../stdlib/validators/tmp.ak:2:1]
   2 │ use aiken/interval.{Interval, IntervalBound, IntervalBoundType}
   3 │ use aiken/transaction.{ScriptContext, ValidityRaneg}
     ·                                       ─────────────
   4 │
     ╰────
    help: Did you mean to import 'ValidityRange'?
  ```
2022-12-22 23:46:17 +01:00
KtorZ 666761efef
Make 'UnexpectedLabelArg' errors more helpful
## Before

  ```
   × Checking
   ╰─▶ Unexpected labeled argument

       t

     ╭─[/Users/mati/Devel/OpenSource/time_lock_aiken/validators/time_lock.ak:13:1]
  13 │   let now = when context.transaction.validity_range.lower_bound.bound_type is {
  14 │     Finite { t } -> t
     ·              ─
  15 │     NegativeInfinity -> 0
     ╰────
  ```

  ## After

  ```
    × Type-checking
    ╰─▶ Unexpected labeled argument 't'

      ╭─[../stdlib/validators/tmp.ak:10:1]
   10 │   let now = when context.transaction.validity_range.lower_bound.bound_type is {
   11 │     interval.Finite { t } -> t
      ·                       ─
   12 │     interval.NegativeInfinity -> 0
      ╰────
    help: The constructor 'Finite' does not have any labeled field. Its fields
          must therefore be matched only by position.

          Perhaps, try the following:

          ╰─▶  interval.Finite(t)
  ```
2022-12-22 21:45:49 +01:00