Commit Graph

1084 Commits

Author SHA1 Message Date
KtorZ 2cb2c7fa1f Add dedicated 'Pair' typed and untyped expression
Before this commit, we would parse 'Pair' as a user-defined
  data-types, and thus piggybacking on that whole record system. While
  perhaps handy for some things, it's also semantically wrong and
  induces a lot more complexity in codegen which now needs to
  systematically distinguish every data-type access between pairs, and
  others.

  So it's better to have it as a separate expression, and handle it
  similar to tuples (since it's fundamentally a 2-tuple with a special
  serialization).
2024-05-04 14:04:12 -04:00
KtorZ 92a1da69d9 Add (possibly temporary) assertion on record access in codegen 2024-05-04 14:04:12 -04:00
KtorZ 3dd94983bd Revert "fixing more pair issues"
This reverts commit b76cc7436294cd73e7bbaf656c76a8f8b0ad56a9.
2024-05-04 14:04:12 -04:00
microproofs 46c7cb797a fixing more pair issues 2024-05-04 14:04:12 -04:00
microproofs ebe415cfc9 fix errors 2024-05-04 14:04:12 -04:00
KtorZ 5c59b816ea Add parser for 'Pair' pattern
And a few more tests along the way for others. Note that it is important here that we try to parse for a 'Pair' BEFORE we try to parse for a constructor pattern. Because the latter would swallow any Pair pattern.
2024-05-04 14:04:12 -04:00
KtorZ 91a7e77ab4 Add 'Pair' pattern and rework internals to use it.
Currently, pattern-matching on 'Pair' is handled by treating Pair as a
  record, which comes as slightly odd given that it isn't actually a
  record and isn't user-defined. Thus now, every use of a record must
  distinguish between Pairs and other kind of records -- which screams
  for another variant constructor instead.

  We cannot use `Tuple` either for this, because then we have no ways to
  tell 2-tuples apart from pairs, which is the whole point here. So the
  most sensical thing to do is to define a new pattern `Pair` which is
  akin to tuples, but simpler since we know the number of elements and
  it's always 2.
2024-05-04 14:04:12 -04:00
KtorZ 897b5d1d7e Ensure type-aliases pretty-printing also work with Pair. 2024-05-04 14:04:12 -04:00
KtorZ 3020af7cd7 Revert 'unify' implementation back to its more elegant form
And add support for Pair.
2024-05-04 14:04:12 -04:00
KtorZ cbf3ef2854 Add new Prelude alias: 'Map' 2024-05-04 14:04:12 -04:00
microproofs 7b5ad961e2 fix: found issue with record access on Pairs 2024-05-04 14:04:12 -04:00
microproofs 30dd1f60e7 small simplification 2024-05-04 14:04:12 -04:00
microproofs 75b076552c feat: Do a major overhaul on how we check types to allow for match patterns instead of if statements
Also fix one more test
2024-05-04 14:04:12 -04:00
microproofs 3c332ca42a Few more places in codegen where we need to be able to deal with Pair records 2024-05-04 14:04:12 -04:00
microproofs 26f68c2fb4 fix: found various unify and type issues while running tests 2024-05-04 14:04:12 -04:00
microproofs fd226be51f add Pair type to prelude 2024-05-04 14:04:12 -04:00
microproofs a8c8cf41cf Finishing up codegen changes for pair 2024-05-04 14:04:12 -04:00
microproofs 963d275bb8 continue progress on pair adding 2024-05-04 14:04:12 -04:00
microproofs 21b60896f0 remove wild card match from tree functions
Start working on supporting Pair clauses
2024-05-04 14:04:12 -04:00
microproofs f950ae7d3d WIP: add new opcodes to Air and AirTree and update parts of codegen to handle the new pair type 2024-05-04 14:04:12 -04:00
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
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 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 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 61936cb91e fix(codegen): Add tracing when checking for a constr vs another primitive 2024-03-17 16:25:17 -04:00
KtorZ cdf564fc9d
Expand 'ExpectOnOpaqueType' error help and label. 2024-03-14 11:20:34 +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
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
KtorZ 59996850c1
Implement 'reify_constant' and rename reify to 'reify_data'
Both fullfill similar goal, but reify_constant sits one level above.
2024-03-07 01:17:06 +01:00
KtorZ 8ffa68d2f0
Fix && and || associativity.
Somehow, these have always been right-associative, when the natural thing to expect is left-associativity. It now matters when trying to crawl down binary tree to display them properly.
2024-03-07 01:17:05 +01:00
rvcas 25ebdc2527
fix: validator args unexpectedly unbound
closes #852
2024-03-06 14:15:00 -05:00
rvcas ad4840958c
chore: add test for validator args with no annotation 2024-03-06 11:19:32 -05:00
KtorZ 4097d1edb2
Fix negative integer literal parsing in fuzzer DSL. 2024-03-04 23:27:23 +01:00
KtorZ 3e922c0a52
Allow primitive literals, lists and tuples in fuzzer expressions. 2024-03-04 20:41:04 +01:00
microproofs c9dd281b45 disable assert that was blocking issue #844 2024-03-04 11:48:22 -05:00
microproofs 27eb1a3e04 Change all uses of interning besides the uplc parser to use the new CodeGenInterner 2024-03-04 11:03:23 -05:00
microproofs d971d9818b update tests and ensure identity reducer handles no_inline lambda 2024-03-04 10:52:56 -05:00
microproofs 06ca22c26a update inliner to handle no_inline functions 2024-03-04 10:52:56 -05:00
microproofs 4e928f39db start adding no inline flag to functions 2024-03-04 10:52:56 -05:00
KtorZ 362acd43a3
Rework and optimize PRNG
Using ByteArrays as vectors on-chain is a lot more efficient than relying on actul Data's list of values. From the Rust end, it doesn't change much as we were already manipulating vectors anyway.
2024-03-04 14:27:16 +01:00
KtorZ 30841fe000
Rework generate_raw to avoid need to intern in prop tests
Also, this commit makes `apply_term` automatically re-intern the
  program since it isn't safe to apply any term onto a UPLC program. In
  particular, terms that introduce new let-bindings (via lambdas) will
  mess with the already generated DeBruijn indices.

  The problem doesn't occur for pure constant terms like Data. So we
  still have a safe and fast version 'apply_data' when needed.
2024-03-03 19:33:27 +01:00
KtorZ 1134b8d7d0
Register tests as callable definitions.
Also move the registering of validators into the same place as they
  other and define a little cute function to avoid code-duplication.
2024-03-03 19:33:27 +01:00
KtorZ c2dc47fa0b
Refactor creation of CodeGenerator and management of known data_types and functions.
This was a mess to say to the least. The mess started when we wanted
  to make all definitions in codegen use immutable maps of references --
  which was and still is a good idea. Yet, the population of the data
  types and functions definitions was done somehow in a separate step,
  in a rather ad-hoc manner.

  This commit changes that to ensure the project's data_types and
  functions are populated while type checking the AST such that we need
  not to redo it after.

  The code for registering the data type definitions and function
  definitions was also duplicated in at least 3 places. It is now a
  method of the TypedModule.

  Note: this change isn't only just cosmetic, it's also necessary for
  the commit that follows which aims at adding tests to the set of
  available function definitions, thus allowing to make property tests
  callable.
2024-03-03 19:33:26 +01:00
KtorZ 26e563a9be
Hardened property-based testing framework. More tests, less bugs.
Those end-to-end tests are useful. Both for controlling the behavior of the shrinker, but also to double check the reification of Plutus Data back into untyped expressions.
  I had to work-around a few things to get opaque type and private types play nice. Also found a weird bug due to how we apply parameters after unique debruijn indexes have been also applied. A work-around is to re-intern the program.
2024-03-03 19:33:26 +01:00
KtorZ 70ea3c9598
Write boilerplate code for being able to easily test properties.
Loads of plumbing, but we now have at least some nice ways to test property execution and shrinking.
2024-03-03 19:33:26 +01:00
KtorZ bbc9fc5762
Yield proper user-facing error when inferring Fuzzer usage 2024-03-03 19:33:26 +01:00
KtorZ cf61387a41
Allow prop test argument to be (optionally) annotated. 2024-03-03 19:33:25 +01:00
KtorZ 93347d8e7b
Add Fuzzer to the prelude. 2024-03-03 19:33:25 +01:00
KtorZ 5b4fedd084
Add PRNG to the Prelude. 2024-03-03 19:33:25 +01:00
KtorZ 41fdcbdfae
Add via keywords to str_to_keyword 2024-03-03 19:33:25 +01:00
KtorZ bfcfc5c41b
Implement reification from Maps. 2024-03-03 19:33:25 +01:00
KtorZ 5272f5ecee
Adjust order in which Bool's constructors are declared in the prelude
True corresponds to Constr=1 and False corresponds to Constr=0; their position in the vector shall reflect that. Note that while this would in principle impact codegen for any other type, it doesn't for bool since we likely never looked up this type definition since it is well-known. It does now as the 'reify' function relies on this. Whoopsie.
2024-03-03 19:33:25 +01:00
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 d698f76e3c
fix(codegen): builtin calls for g1 and g2 where flipped
closes #840
2024-02-29 12:13:51 -05: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 c7dd4d0e48 feat(aiken-lang): expose integerToByteString and byteStringToInteger 2024-02-20 13:05:28 -05:00
rvcas 0ccfe60072
feat: support nested void matching 2024-02-13 21:29:24 -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
microproofs 056e3d76ea change check_validator_args to check type after each arg 2024-02-07 12:48:07 -05:00
microproofs 6c6be3f53d got past the errors and warnings 2024-02-07 12:37:37 -05:00
microproofs 51f1da2505 Removed AirStatements and AirExpressions
Still a WIP
2024-02-07 12:37:37 -05:00
microproofs b807d58e89 fix first compiler pass of errors 2024-02-07 12:37:37 -05:00
microproofs dc195b22d4 missed another hoist over 2024-02-07 12:36:35 -05:00
microproofs d1c784ed49 few more hoist over fixes 2024-02-07 12:36:35 -05:00
microproofs 3938d74bb6 missed a hoist over 2024-02-07 12:36:35 -05:00
microproofs 6b97ab71fe fix up code gen tests 2024-02-07 12:36:35 -05:00
microproofs 4ab3b61200 In most cases the context isn't need so I made the code more explicit about that 2024-02-07 12:36:35 -05:00
microproofs 575dde9885 fix: issue with reordering statements caused clause props to not be updated 2024-02-07 12:36:35 -05:00
microproofs 8702c736d0 fix warning 2024-02-07 12:36:35 -05:00
microproofs 806a74c192 fix all current errors 2024-02-07 12:36:35 -05:00
microproofs 9f96e4bc5a fix first compiler pass of errors 2024-02-07 12:36:35 -05:00
KtorZ a12c374258 Start turning AirTree statements into expressions (let)
Still many places to fix, WIP.
2024-02-07 12:36:35 -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
microproofs 3b4c6cb2aa fix: missing message error term in one place for type is void 2024-02-07 11:48:52 -05:00
microproofs e25be7643e discards will now check for type too. 2024-02-07 11:48:52 -05:00
microproofs 982eff449e chore: Release 2024-01-31 13:48:20 -05:00
microproofs 551941392e fix: assert had one minor edge case due to final clauses with lists 2024-01-31 00:05:09 -05:00
microproofs 444bccf19c fix: change list_access_to_uplc to properly handle list discards 2024-01-30 23:53:33 -05:00
microproofs a83220c8d9 fix: module_name was being overrided by the moduleselect field 2024-01-30 23:52:50 -05:00
microproofs 8584adc1b7 chore: Release 2024-01-25 15:10:11 -05:00
microproofs 78d2049d7b fix: Using the wrong match string for discards in FieldsExpose
Also need to return a lambda wrapped term from list_access_to_uplc under all conditions
2024-01-25 14:18:36 -05:00
rvcas defd36ad8c
chore: Release 2024-01-25 11:07:32 -05:00
microproofs 36a0b317ad fix condition to account for tail presence 2024-01-24 16:29:40 -05:00
microproofs 51f1f2b67f change redundant if branches 2024-01-24 16:29:40 -05:00
microproofs 3a44c45b48 fix: one builtin error wasn't be caught with a messaged exception 2024-01-24 16:29:40 -05:00
microproofs eda4e259d6 minor fix and some refactoring on the if statements 2024-01-24 16:29:40 -05:00
microproofs 82fc82ceee fix: used wrong index in tupleAcessor 2024-01-24 16:29:40 -05:00
microproofs 956c3d6cf0 feat: refactor code gen to avoid builtin errors when tracing is turned on 2024-01-24 16:29:40 -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
KtorZ bf96c3afd2
Add more tests & rename 'Invalid' -> 'Unfinished' 2024-01-20 10:26:33 +01:00
Matthias Benkort cb6fd59dbd
Fix minor typo in error label 2024-01-20 09:58:36 +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 2b4137dc24
Revert "minor refactor"
This reverts commit 21f0b3a6220fdafb8f6aad6855de89d8cdde0e1b.

  Rationale:

  The absence of clause guard was here done *on purpose*. Indeed,
  introducing a clause guard here forces either duplication or the use
  of a wildcard which is not "future proof".

  Should we make a change to that one day (e.g. add a new variant to
  TraceLevel), we won't get any compiler warning and we'll very likely
  forget to update that particular section of the code.

  So as much as possible, enforce complete pattern-match on variants
  make for code that is easier to maintain in the long-run.
2024-01-19 14:31:09 +01:00
microproofs af90b38bf8
minor refactor 2024-01-19 14:31:04 +01:00
KtorZ 6fa272bd34
Remove compiler-generated helper 'global' traces in compact mode.
Since there's no line number to show here, we don't have much choice. And the alternative of showing shorter traces as code is just ugly as hell.
2024-01-19 14:30:44 +01: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 627c6b576e
Move line_numbers under 'aiken-lang'
And add some unit tests to ensure things are working properly.
2024-01-19 14:30:15 +01:00
microproofs f79b37d551
Replace 'bool' with 'TraceLevel' in codegen
Co-authored-by: KtorZ <matthias.benkort@gmail.com>
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 d26524048e fix: headlist builtin on assoc lists
implement chooseunit for 0 args
2024-01-13 19:29:34 -05:00
microproofs c7af27a6ba fix: generic edge case with tuples that allowed 2 tuples and 3 tuples to use the same monomorphized function.
Also massively reduced the space taken up by generics in scripts when using generics with list and tuples
2024-01-13 17:46:32 -05:00
microproofs 4a8fecb70a fix: satisfy clippy's demands 2024-01-11 14:53:02 -05:00
rvcas 8b62873ef5
fix(format): post trace sequences getting wrapped in curlies closes #781 2024-01-09 22:39:55 -05:00
microproofs ff462fa8ea don't need clippy macro anymore :) 2024-01-08 18:08:50 -05:00
microproofs f722af1149 fix: accidentally put quotes around tail_name 2024-01-08 18:08:50 -05:00
microproofs 2216f387c3 refactor: change codegen uplc to have more type safety
Also refactor list_access_to_uplc
2024-01-08 18:08:50 -05:00
KtorZ 30a6b77116 Get rid of 'VoidMsg' in favor of an 'Option'. 2024-01-04 16:03:51 -05:00
microproofs c50a9cb5bd refactor: convert msgs to use AirMsg type instead of AirTree 2024-01-04 16:03:51 -05:00
microproofs 394cac86b8 feat: expect on a type now can take in a msg when in trace mode 2024-01-04 16:03:51 -05:00
microproofs 4fc65cc600 feat: change expect from data on constrs to take in a message term 2024-01-04 16:03:51 -05:00
microproofs c7a1ff0959 refactor how tracing is popped off to be in one location in uplc_gen 2024-01-04 16:03:51 -05:00
microproofs 355e38d6e2 feat: expects now print the line of code that failed 2024-01-04 16:03:51 -05:00
microproofs 412945af3a update aiken code gen test 2024-01-04 16:03:51 -05:00
microproofs aa51ce3e3e feat: add code messages when using expects on constrs 2024-01-04 16:03:51 -05:00
microproofs 71cfb6f6af feat: Add specific messages for using expect with booleans
TODO: fill out the rest of the expects with messages
2024-01-04 16:03:51 -05:00
rvcas 07122aaa88
feat: allow importing off validators in validators/tests/* 2023-12-11 18:27:08 -05:00
KtorZ 92488e535a
Fix type definitions for g1 & g2 elements. 2023-12-08 16:58:12 +01:00
microproofs 825e65d7a3 fix: zero arg functions were being compiled without the trace messages
Now traces are added before evaluating
2023-12-06 10:31:48 -05:00
rvcas 2647e4aae6
chore: Release 2023-12-04 22:14:03 -05:00
rvcas c50d4d1396
fix: forgot to handle None case for other_fun in validator 2023-11-29 21:24:30 -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 1f411cde0e
chore: needless dbg 2023-11-28 20:59:23 -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 7015a9badc
feat(lsp): hover support for the optional multi validator fn 2023-11-28 19:18:29 -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 a46a7e82b7
feat: implement hover on when clause patterns 2023-11-28 16:13:08 -05:00
rvcas f7dd2de17b
feat: implement hover info for tuple, list, and contructor pattern elements 2023-11-28 16:12:37 -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 45177cd08b fix: add missing type checks for the new bls primitives 2023-11-23 13:00:24 -05:00
microproofs 63f96d13ca fix: clippy warning 2023-11-22 19:17:45 -05:00
microproofs 78b0789cbc chore: unit test for pub in validator module warnings closes #681 2023-11-22 18:02:21 -05:00
rvcas abd18656e3 fix: unable to have newline after expect bool shortcut 2023-11-20 11:44:16 -05:00
rvcas 2ed91780f4 fix: call arg should be top level 2023-11-20 11:44:16 -05:00
rvcas 7118253401 fix: if branches, final_else, and anon fns should all be "top level" 2023-11-20 11:44:16 -05:00
rvcas 7680d33663 fix: panic in formatter when substracting u8 0 - 1 2023-11-20 11:44:16 -05:00
rvcas 6869f73033 fix: sequence formatting when not top level 2023-11-20 11:44:16 -05:00
rvcas b80db2f7f8 fix(bls): wrong types for equals functions 2023-11-15 15:55:56 -05:00
rvcas d53d2665b2 test(bls): g1 and g2 formatting 2023-11-15 15:55:56 -05:00
rvcas c910e0054e test(bls): constant parsing tests 2023-11-15 15:55:56 -05:00
rvcas 7073fd29b3 test(bls): literal parsing tests 2023-11-15 15:55:56 -05:00
microproofs 8b89ba3b93 feat: implement bls primitives in code gen 2023-11-15 15:55:56 -05:00
microproofs d51374aac1 feat: add conversion to data and from data for new primitive types 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
rvcas 90aea6476a feat: uplc g1 and g2 literal parsing 2023-11-15 15:55:56 -05:00
rvcas 49ae8152f8 feat(bls): add new aiken level builtins 2023-11-15 15:55:56 -05:00
rvcas 8a3a465237 feat(bls): add new types to aiken prelude 2023-11-15 15:55:56 -05:00
microproofs 0d2ac952d0 feat: implemented the Bls381-12 builtins and types
also implemented Keccak256 and Blake2b_224

TODO: cost model, flat serialization, pretty

Co-authored-by: rvcas <x@rvcas.dev>
2023-11-15 15:55:56 -05:00
microproofs 2f694b01cb chore: use insta snapshot for blueprint validator tests 2023-11-06 15:37:04 -05:00
microproofs 4eebd4628b chore: fix comment 2023-11-06 15:37:04 -05:00
microproofs 7427bac4a0 chore: remove unused code 2023-11-06 15:37:04 -05:00
microproofs 598ec5eaef Use a better algorithm for inlining single occurrences 2023-11-06 15:37:04 -05:00
microproofs 49bd4ba33d chore: Release 2023-10-25 19:00:03 -04:00
microproofs 4dd17dacf3 chore: rename uplc builder builtins 2023-10-22 17:08:48 -04: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 c0513da032
Add quickfix for unknown constructors. 2023-10-21 14:24:47 +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 763516eb96
Refactor and relocate document edits function for imports.
It's a bit 'off-topic' to keep these in aiken-lang as those functions are really just about lsp. Plus, it removes a bit some of the boilerplate and make the entire edition more readable and re-usable. Now we can tackle other similar errors with the same quickfix.
2023-10-21 11:31:01 +02:00
KtorZ 699d0a537c
Use (untyped) AST to find the right insert location for imports.
This removes the need to rely on the formatter to clear things up
  after insert a new import. While this is not so useful for imports, I
  wanted to experiment with the approach for future similar edits (for
  example, when suggesting an inline rewrite).
2023-10-21 10:43:00 +02:00
KtorZ 66ade8e3e3
Implement simple code action quickfix for unknown variable. 2023-10-20 18:01:07 +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