Commit Graph

830 Commits

Author SHA1 Message Date
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
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 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 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
microproofs c51741cc35 fix: mutually recursive zero arg function calls were reaching an unreachable 2024-03-08 22:58:03 -05: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 d55b7844f0 feat: impl serde for TypeAliasAnnotation 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
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 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
rvcas fab6d5aff7
chore: fix fmt 2024-03-07 19:32:33 -05:00
KtorZ 23a22a65cb
Handle (recursive) generic types during reification.
Also moved a bunch of functions from code-gen back into _tipo_, as
  they're better suited and generic enough to be reused elsewhere.
2024-03-07 18:07:52 +01:00
microproofs a3fbe6c155 fix tests 2024-03-06 23:27:10 -05:00
microproofs e217423145 mixed up pair builtin 2024-03-06 23:27:10 -05:00
microproofs bdd84dc952 fixing the tests lead to me create a new function for converting from data 2024-03-06 23:27:10 -05:00
microproofs 892da06e14 add more runtime checking for a few of the data to primitive conversions 2024-03-06 23:27:10 -05:00
KtorZ bff822ea7f
Rework unit test report to leverage new reification
And also provide slightly better errors when traces, or trace-if-false operators are present.
2024-03-07 01:20:40 +01:00