Commit Graph

1953 Commits

Author SHA1 Message Date
rvcas 7c5b9aa35e
feat(lsp): find_node for TypedArgVia 2024-04-02 19:22:19 -04:00
rvcas d22ee6e086
chore: remove useless clone 2024-04-02 19:04:33 -04:00
rvcas e02bc2a58a
feat(lsp): find_node should traverse tail of list 2024-04-02 17:55:04 -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
microproofs 21b1e29f09 chore: clippy fix 2024-03-27 16:39:52 -04:00
microproofs a6003c3be9 chore: push changes in blueprint snapshot test 2024-03-27 15:57:29 -04:00
microproofs a5a0734629 fix: casting a field type to Data with expect and traces on was assuming the raw Data was of type constr 2024-03-27 15:52:23 -04:00
rvcas 075668b52e
chore: Release 2024-03-25 22:09:37 -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 4e8042fd06
chore: Release 2024-03-22 16:10:17 +01:00
KtorZ 96387e3437
Fixes #767
Co-authored-by: @rvcas <x@rvcas.dev>
2024-03-22 16:05:32 +01:00
rvcas a09069b828
fix: binop associativity formatting
it seems we can fix this by changing which side
gets subtracted by 1 depending on the op associativity.
BinOp::Or & BinOp::And are right associative while the
other bin ops are left associative.

closes #893

Co-authored-by: Kasey White <kwhitemsg@gmail.com>
2024-03-21 20:12:49 -04:00
KtorZ 0f9dbfd874
Fixes #883. 2024-03-21 18:20:19 +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 25e9db4f6c Rename t1 -> lhs, t2 -> rhs in unify. 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
microproofs 8495f98c1d remove print 2024-03-17 16:26:10 -04:00
microproofs 61936cb91e fix(codegen): Add tracing when checking for a constr vs another primitive 2024-03-17 16:25:17 -04:00
KtorZ d1ba8db889
Do not generate documentation for empty modules. 2024-03-15 21:40:57 +01:00
KtorZ 6515efeb73
Implementing remaining shrinking strategies.
This makes the search for counterexample slower in some cases by 30-40% with the hope of finding better counterexamples. We might want to add a flag '--simplification-level' to the command-line to let users decide on the level of simplifications.
2024-03-15 13:36:05 +01:00
Matthias Benkort b09e0316fa
Merge pull request #877 from aiken-lang/dependencies-pruning
Only compile modules the project depends on
2024-03-15 00:25:00 +01:00
KtorZ 9986bc6bfd
Remove duplication between docs & compile
And move some logic out of project/lib to be near the CheckedModule
  instead. The project API is already quite heavy and long, so making it
  more lightweight is generally what we want to tend to.
2024-03-15 00:05:39 +01:00
KtorZ 1caed3e87c
Use BTreeSet instead of HashSet whenever possible. 2024-03-14 23:08:39 +01:00
Matthias Benkort 3f254dbe6b
Merge pull request #875 from aiken-lang/rvcas/expect_opaque
block expects on opaque types
2024-03-14 19:43:47 +01:00
KtorZ fd50473a32
Only compile modules the project depends on
This changes ensure that we only compile modules from dependencies
  that are used (or transitively used) in the project. This allows to
  discard entire compilation steps at a module level, for modules that
  we do not use.

  The main goal of this change isn't performances. It's about making
  dependencies management slightly easier in the time we decide whether
  and how we want to manage transitive dependencies in Aiken.

  A concrete case here is aiken-lang/stdlib, which will soon depend on
  aiken-lang/fuzz. However, we do not want to require every single
  project depending on stdlib to also require fuzz. So instead, we want
  to seggregate fuzz API from stdlib in separate module, and only
  compile those if they appear in the pruned dependency graph.

  While the goal isn't performances, here are some benchmarks analyzing
  the performances of deps pruning on a simple project depends on a few
  modules from stdlib:

	Benchmark 1: ./aiken-without-deps-pruning check scratchpad
	  Time (mean ± σ):     190.3 ms ± 101.1 ms    [User: 584.5 ms, System: 14.2 ms]
	  Range (min … max):   153.0 ms … 477.7 ms    10 runs

	Benchmark 2: ./aiken-with-deps-pruning check scratchpad
	  Time (mean ± σ):     162.3 ms ±  46.3 ms    [User: 572.6 ms, System: 14.0 ms]
	  Range (min … max):   142.8 ms … 293.7 ms    10 runs

  As we can see, this change seems to have an overall positive impact on
  the compilation time.
2024-03-14 19:41:50 +01:00
KtorZ 038c5b2d34
Rewrite run_n_times to not be recursive but mutates arguments.
We reach a stack-overflow for n > 2000 otherwise. Mutation works well here and is a valid use-case.
2024-03-14 14:18:38 +01:00
KtorZ cdf564fc9d
Expand 'ExpectOnOpaqueType' error help and label. 2024-03-14 11:20:34 +01:00
KtorZ 0343aeca34
Fix remaining insta snapshots. 2024-03-14 11:06:53 +01: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 9127dcdd6e
Add note on the type-casting check. 2024-03-13 20:18:56 -04:00
KtorZ 8f31b45e36
Fix allow_casting condition in unification
We should allow casting from any type to any type. Or at the very least, allow it for well-known types like List.
2024-03-13 20:18:56 -04:00
KtorZ f10cf73905
Rework 'is_opaque' to also check for inner types.
Also removed the duplication in infer_assignment and moved the check down.
2024-03-13 20:18:56 -04:00
KtorZ 22b618116e
rename function argument for clarity
is_assignment was a bit confusing to me since we do actually categorize expect as 'assignment'. So this is more about whether this is a *let* assignment. Hence 'is_let'.
2024-03-13 20:18:55 -04:00
KtorZ 502a13756a
remove irrelevant comment. 2024-03-13 20:18:55 -04:00
KtorZ 961806617f
Add more failing tests for expecting on into opaque types. 2024-03-13 20:18:55 -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
microproofs 1d72838f83 fix: awkward assignment formatting
Co-authored-by: Lucas Rosa <x@rvcas.dev>
2024-03-13 19:10:06 -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 7b32d4ae30 chore: add a test for formatting assignment patterns 2024-03-12 08:10:33 -04:00
rvcas 945b4155cd fix(assignment-patterns): allow trailing 2024-03-12 08:10:33 -04:00
rvcas 97247ce949 chore: assignment patterns refactor tuple into struct 2024-03-12 08:10:33 -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
Matthias Benkort f02b9b0f0c
Merge pull request #871 from aiken-lang/backpassing
Backpassing
2024-03-11 01:06:17 +01:00
KtorZ 4fbb4fe2db
Handle fuzzer failing unexpected
We shouldn't panic here but bubble the error up to the user to inform
  them about a possibly ill-formed fuzzer.

  Fixes #864.
2024-03-11 01:04:46 +01:00
KtorZ 7e8e959251
Fix spans and error reporting for backpassing. 2024-03-11 00:20:29 +01:00
KtorZ a57dcf3307
Allow backpassing with expect. 2024-03-11 00:20:29 +01:00
KtorZ 435dd0d213
Refactor AssignmentKind to allow backpassing on both let and expect.
The 3rd kind of assignment kind (Bind) is gone and now reflected through a boolean parameter. Note that this parameter is completely erased by the type-checker so that the rest of the pipeline (i.e. code-generation) doesn't have to make any assumption. They simply can't see a backpassing let or expect.
2024-03-11 00:16:23 +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 1f530f3b24
Experiment with monadic bind. 2024-03-11 00:16:22 +01:00
KtorZ 0e0bed3c9d
Collect traces from last prop-test run on failure 2024-03-10 19:24:25 +01:00
KtorZ d4069148c7
Remove UnitTestResult's output field
Dead-code. Also renamed 'logs' to 'traces'.
2024-03-10 19:00:01 +01:00
KtorZ be7d07fa99
Always show test traces (unless manually turned off with flag)
On both failures and success.
2024-03-10 18:53:11 +01:00
KtorZ c169596c76
preserve type-aliases from annotations on calls. 2024-03-10 00:38:03 +01:00
KtorZ 191e4d47b3
Remove dead-code: 'Layer' 2024-03-09 23:14:44 +01:00
Matthias Benkort ec18127191
Merge pull request #869 from aiken-lang/non-serialisable-types
Forbid non-serializable inhabitants in compound data-types.
2024-03-09 22:39:41 +01:00
KtorZ 80a9393db7
Add --include-dependencies to 'aiken docs'
Fixes #867.
2024-03-09 22:35:38 +01:00
KtorZ ee54266d1f
Forbid non-serializable inhabitants in compound data-types. 2024-03-09 22:25:51 +01:00
KtorZ 37627e3527
Fix indentation of pipelines. 2024-03-09 20:44:51 +01:00
KtorZ 6ba74125c7
Remove extra newlines in test report and only print coverage on success. 2024-03-09 20:32:42 +01:00
KtorZ 22b86a5f82
Add --max-success for running more or less prop runs on demand. 2024-03-09 19:17:57 +01:00
KtorZ d581183cc6
Fix formatter discarding nul bytes. 2024-03-09 18:59:35 +01:00
microproofs b761d6a76d fix: function aliases were leading to free uniques 2024-03-09 12:46:12 -05:00
microproofs bffa678178 fix: mutually recursive zero arg functions needed to have their function bodies delayed 2024-03-09 10:04:30 -05:00
Matthias Benkort 7f0df40b4e
Merge pull request #862 from SundaeSwap-finance/pi/summary-check-count
Include the number of tests / checks run as part of the summary
2024-03-09 13:10:16 +01:00
microproofs c51741cc35 fix: mutually recursive zero arg function calls were reaching an unreachable 2024-03-08 22:58:03 -05:00
Pi Lanningham ebd6c3a56e Cargo fmt 2024-03-08 20:43:27 -05:00
Pi Lanningham ace58e368c Correctly report the checks count
It might be slightly cleaner and more extensible to change  to return a summary, potentially even making  track the tests, coverage, etc. so it can be serialized to JSON. But, for now, this is much simpler, and the approach that KtorZ suggested.
2024-03-08 20:40:50 -05:00
KtorZ 77faee672e
cargo fmt --all 2024-03-09 01:28:48 +01:00
KtorZ bbe7c0bc01
report prop test coverage labels on success. 2024-03-09 01:28:29 +01:00
KtorZ 96da70149d
Count labels in properties.
We'll piggyback on the tracing capabilities of the VM to provide labelling for prop tests. To ensure we do not interfere with normal traces, we only count traces that starts with a NUL byte as label. That convention is assumed to be known of the companion fuzz library that should then provide the labelling capabilities as a dedicated function.
2024-03-09 01:28:29 +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 cb0ae0c074 feat: impl some conversion methods on CheckedModule 2024-03-08 19:19:07 -05:00
rvcas d55b7844f0 feat: impl serde for TypeAliasAnnotation 2024-03-08 19:19:07 -05:00
rvcas 2b5ed95df5 feat: serialize as cbor 2024-03-08 19:19:07 -05:00
rvcas 836e853827 fix: bring back vec1 2024-03-08 19:19:07 -05:00
rvcas 9d99b509b2 chore: this should be gone 2024-03-08 19:19:07 -05:00
rvcas fe6710935d feat: impl serde on errythang 2024-03-08 19:19:07 -05:00
Pi Lanningham e944f10372 Add an optional check count; when we run a command that runs tests, we can set this to Some(x) and it'll print in the summary 2024-03-08 17:36:32 -05:00
KtorZ a9d596f4cb
Memoize simplification steps during property-based shrinking.
I've been benchmarking that through the shrink of 'large' lists, and the cache brings about 1.5x speed increase. For small and simple cases, the cache as no visible effects (positive or negative).
2024-03-08 18:58:51 +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
KtorZ 877d10ef22
Use inferred Fuzzer inner type for unify error when possible. 2024-03-08 15:57:41 +01:00
microproofs eb07365e73 fix tests 2024-03-08 00:12:44 -05:00
microproofs 94f383762c step up the optimizations a bit more by inlining a small function 2024-03-08 00:12:44 -05:00
microproofs bf429fbdbf remove unused import 2024-03-08 00:12:44 -05:00
microproofs dcec8ecfe6 remove unused special function 2024-03-08 00:12:44 -05:00
microproofs 541d96f558 remove comment line 2024-03-08 00:12:44 -05:00
microproofs 275db2fd11 update tests 2024-03-08 00:12:44 -05:00
microproofs ae396c0224 Fix opaque type destructuring in code gen 2024-03-08 00:12:44 -05:00
microproofs 1edd1a1fa3 change currying to happen with 3 or more occurrences 2024-03-08 00:12:44 -05:00
microproofs e9122de061 more identity reduce testing 2024-03-08 00:12:44 -05:00