Commit Graph

2651 Commits

Author SHA1 Message Date
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
cc99eceda8 chore: update changelog 2024-03-12 08:10:33 -04:00
rvcas
5840ce34af chore: commit an ignore we can all use without accidentally commiting test files/folders 2024-03-12 08:10:33 -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