Commit Graph

1986 Commits

Author SHA1 Message Date
microproofs 9e78f0fc2a update for latest main 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
KtorZ db8eb6a108
Provide more context for some panics
Actually ran into them both, will open issues about those in a bit.
2024-05-01 12:04:47 +02:00
KtorZ 925a11be69
Check for args length when comparing types. Duh!
Fixes #917.
2024-05-01 10:48:15 +02:00
Christopher Valerio 24560e9acd
fix: fixing bash messages 2024-04-28 17:21:19 -06:00
Christopher Valerio 6c052f44a1
fix: Adding better error messages 2024-04-28 17:18:37 -06:00
Christopher Valerio 3c66da75d6
Improving errors 2024-04-28 17:13:48 -06:00
Christopher Valerio 063f3d0835
feat: Adding installation for fish and bash 2024-04-28 17:04:46 -06:00
Christopher Valerio c5faffe946
feat: adding oh-my-zsh support 2024-04-28 17:04:46 -06:00
Christopher Valerio 949f16f34a
rebase from main 2024-04-28 17:04:40 -06:00
microproofs 945a3f743b feat: builtin wrapper reduction optimization 2024-04-26 19:24:04 +02:00
Micah Kendall ff4ddfbe1b Simplifying PR per reviewers request 2024-04-12 21:40:27 -04:00
Micah Kendall d39dbd6697 fmt 2024-04-12 21:40:27 -04:00
Micah Kendall d25b8f91c7 feat: Emit keyword 2024-04-12 21:40:27 -04:00
rvcas 17ddbfaafa chore: remove dbg 2024-04-08 14:30:07 -04:00
rvcas 5fc338a1eb test: add some snapshot tests for export type 2024-04-08 14:30:07 -04:00
rvcas 5cb1e23008 fix: program generate should only run after params and args are validated 2024-04-08 14:30:07 -04:00
rvcas cac119338d feat(blueprint): a memoized program that only runs code gen every other time 2024-04-08 14:30:07 -04:00
rvcas aa3896e92a feat(export): allow trace levels to be controlled 2024-04-08 14:30:07 -04:00
rvcas 79ccc55499 feat(cli): print Export json to stdout
Co-authored-by: Kasey White <kwhitemsg@gmail.com>
2024-04-08 14:30:07 -04:00
rvcas dac3308620 feat(Project::export): use Export::from_function and transpose
Co-authored-by: Kasey White <kwhitemsg@gmail.com>
2024-04-08 14:30:07 -04:00
rvcas 8ed930ac5a feat: implement Export object based on blueprint
Co-authored-by: Kasey White <kwhitemsg@gmail.com>
2024-04-08 14:30:07 -04:00
rvcas 3cdb21ad6b feat(blueprint): make a helper public 2024-04-08 14:30:07 -04:00
rvcas a11b1fa56a chore: cleanup validator creator method 2024-04-08 14:30:07 -04:00
rvcas 9322020a5e feat(blueprint): re-export Error 2024-04-08 14:30:07 -04:00
rvcas f50f7e42db feat(project): create export type
Co-authored-by: Kasey White <kwhitemsg@gmail.com>
2024-04-08 14:30:07 -04:00
rvcas 9d49be46b8 chore: add some docs to the uplc crate 2024-04-08 14:30:07 -04:00
rvcas 033cc26313 fix: with_project no longer needs a seed 2024-04-08 14:30:07 -04:00
rvcas 1d462314c4 feat: use new generate_raw function 2024-04-08 14:30:07 -04:00
rvcas 7d67f1497c feat(export): implement basic command functionality 2024-04-08 14:30:07 -04:00
rvcas b63bd9b9e0 feat(cli): add empty export commands 2024-04-08 14:30:07 -04:00
rvcas b27fcf38e5
fix(check): collapse_links on tuple_index access closes #905 2024-04-02 19:45:16 -04:00
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