Commit Graph

183 Commits

Author SHA1 Message Date
KtorZ 14f1025f0b
Display counterexamples as Aiken values instead of raw UPLC. 2024-03-03 19:33:24 +01:00
KtorZ c766f44601
Allow Fuzzer with type parameter
Also fix shrinker first reduction, as well as passing of List/Tuples to fuzzer.
2024-03-03 19:33:24 +01:00
KtorZ a703db4d14
Borrow integrated shrinking approach from MiniThesis. 2024-03-03 19:33:24 +01:00
KtorZ 3762473a60
Add preliminary plumbing to run property test through the CLI.
This is very very rough at the moment. But it does a couple of thing:

  1. The 'ArgVia' now contains an Expr/TypedExpr which should unify to a Fuzzer. This is to avoid having to introduce custom logic to handle fuzzer referencing. So this now accepts function call, field access etc.. so long as they unify to the right thing.

  2. I've done quite a lot of cleanup in aiken-project mostly around the tests and the naming surrounding them. What we used to call 'Script' is now called 'Test' and is an enum between UnitTest (ex-Script) and PropertyTest. I've moved some boilerplate and relevant function under those module Impl.

  3. I've completed the end-to-end pipeline of:
     - Compiling the property test
     - Compiling the fuzzer
     - Generating an initial seed
     - Running property tests sequentially, threading the seed through each step.

   An interesting finding is that, I had to wrap the prop test in a similar wrapper that we use for validator, to ensure we convert primitive types wrapped in Data back to UPLC terms. This is necessary because the fuzzer return a ProtoPair (and soon an Array) which holds 'Data'.

  At the moment, we do nothing with the size, though the size should ideally grow after each iteration (up to a certain cap).

  In addition, there are a couple of todo/fixme that I left in the code as reminders of what's left to do beyond the obvious (error and success reporting, testing, etc..)
2024-03-03 19:33:24 +01: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
rvcas ff5491caa0
fix(check): only disallow ml_result in data 2024-02-29 11:19:26 -05:00
rvcas 2018a18d15
fix: error message for bls elements in a type def
closes #840
2024-02-27 21:21:18 -05:00
rvcas ac0c73a56a
chore: clippy fixes 2024-02-13 20:26:12 -05:00
rvcas 3582c5569d
fix: no single when clause warning sometimes
While looking at some code, I noticed that this
warning would show up even if an error for a
non-exhaustive when/is shows up for the same when/is
expression. This isn't a useful situation to show this
warning because things are not exhaustive yet so we should
let the user finish and only provide the errors. If things
are exhaustive then the code proceeds and if a warning was set
when there's only one clause pattern then this warning message
can be pushed because that's when it's actually useful.
2024-02-13 20:12:40 -05:00
rvcas 4c5a449d83
chore: improve a comment/doc 2024-02-13 19:46:34 -05: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
KtorZ 20ce19dfb1 Fix error hint when expecting 0 generic parameters. 2024-02-07 11:48:52 -05:00
KtorZ 54a1b50138
Make behavior between curly- and paren-delimited blocks consistent.
Note that the formatter rewrite parens-block sequences as curly-block
  sequences anyway. Albeit weird looking syntax, they are valid
  nonetheless.

  I also clarified a bit the hints and description of the
  'illegal::return' error as it would mistakenly say 'function' instead
  of 'block'.
2024-01-20 10:37:07 +01:00
rvcas 25a837ab3f
feat: parser and check fixes
- do not erase sequences if the sole expression is an assignment
- emit parse error if an assignment is assigned to an assignment
- do not allow assignments in logical op chains
2024-01-19 14:32:21 -05:00
KtorZ 59c784778e
Convert span's start to line number + col
This requires to make line numbers a first-class citizen in the module
  hierarchy but it is fortunately not _too involved_.
2024-01-19 14:30:15 +01:00
KtorZ e67d5863a1
Introduce 'compact' trace level verbosity
For now, it only shows the span start. We'll change that in the next commit to show a line number and a column.
2024-01-19 14:30:15 +01: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
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
rvcas 1503b525b2
feat(lsp): implement quickfix for utf8 byte array is valid hex string warning 2023-11-28 21:02:15 -05:00
rvcas 832ca81a8c
fix(lsp): when desugaring and/or chains we should use the whole span of the chain for the generated BinOp locations 2023-11-28 19:19:56 -05:00
rvcas 2159053cb5
fix: using the word pattern here reads better and applies more broadly like for lists 2023-11-28 16:15:24 -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
KtorZ 4adedaac15
Remove unnecessary 'Rc' in function signature. 2023-11-25 13:09:26 +01:00
microproofs 63f96d13ca fix: clippy warning 2023-11-22 19:17:45 -05:00
rvcas 6869f73033 fix: sequence formatting when not top level 2023-11-20 11:44:16 -05:00
microproofs 8b89ba3b93 feat: implement bls primitives in code gen 2023-11-15 15:55:56 -05:00
rvcas 3675762c3e feat(bls): aiken level g1 and g2 literals 2023-11-15 15:55:56 -05:00
KtorZ 46c58dbd61
Implement quickfixes for redundant imports. 2023-10-22 00:29:09 +02: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
KtorZ 5986163ba7
Add quickfix for unknown alias & data types. 2023-10-21 13:57:06 +02:00
KtorZ c550b4766d
Implement quickfix for 'UnknownModule'. 2023-10-21 12:59:48 +02:00
KtorZ c4221730bf
Define 'ExtraData' trait for errors
This should allow passing some extra information to LSP diagnostic in order to provide quickfix actions, such as auto-imports.
2023-10-20 18:00:12 +02:00
rvcas e5801f9c19
feat: support doc comments for functions args and validator params
- Add support to the formatter for these doc comments
- Add a new field to `Arg` `doc: Option<String>`
- Don't attach docs immediately after typechecking a module
  - instead we should do it on demand in docs, build, and lsp
  - the check command doesn't need to have any docs attached
  - doing it more lazily defers the computation until later making
    typechecking feedback a bit faster
- Add support for function arg and validator param docs in
  `attach_module_docs` methods
- Update some snapshots
- Add put_doc to Arg

closes #685
2023-10-16 13:38:23 -04:00
rvcas e8bcbecf31
chore: avoid cloning name 2023-10-12 17:50:44 -04:00
rvcas 55f89a7ff4
fix: incorrect 'unused::constructor'
`ExprTyper` was not incrementing the usage of a constructor
when infering `RecordAccess`.

closes #554
2023-10-12 17:44:57 -04:00
rvcas 52dfc13f8f
chore: explain a weird if condition 2023-10-12 17:24:11 -04:00
rvcas 135dbd8335 feat: handle pipe fn infer TODOs
This improves error messages for `a |> b(x)`.

We need to do a special check when looping over the args
and unifying. This information is within a function that does not belong
to pipe typer so I used a closure to forward along a way to add
metadata to the error when the first argument in the loop has a
unification error. Simply adding the metadata at the pipe typer
level is not good enough because then we may annotate regular
unification errors from the args.
2023-10-03 01:17:15 -04:00
rvcas d808197507
chore: clippy fix 2023-09-13 18:17:59 -04:00
rvcas e4ef386c44 feat(tipo): inference for and/or chains 2023-08-15 09:58:35 -04:00
Pi Lanningham f464eb3702 Cargo fmt + clippy, with latest rust 2023-08-07 19:00:39 -04:00
rvcas 266b6bbb7d
fix(exhaustiveness): for constructor use correct name because import aliases 2023-08-03 16:28:47 -04:00
rvcas 60ac8ab591
fix(exhaustiveness): adjust helper method to get contructors properly 2023-08-03 16:14:42 -04:00
KtorZ 4f7f39292d
Fix subtle bug in pattern rendering
When rendering missing or redundant patterns, linked-list would
  wrongly suggest the last nil constructor as a pattern on non-empty
  list.

  For example, before this commit, the exhaustivness checker would yield:

  ```
  [(_, True), []]
  ```

  as a suggestion, for being the result of being a list pattern with a
  single argument being `(_, True) :: Nil`. Blindly following the
  compiler suggestion here would cause a type unification error (since
  `[]` doesn't unify with a 2-tuple).

  Indeed, we mustn't render the Nil constructor when rendering non-empty
  lists! So the correct suggestion should be:

  ```
  [(_, True)]
  ```
2023-08-02 10:31:35 +02:00
KtorZ 00b255e960
Remove now-dead code. 2023-08-02 09:22:21 +02:00
rvcas f3cab94ae1 test(check): a bunch of tests for the new exhaustiveness stuff 2023-08-01 21:13:50 -04: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