Commit Graph

308 Commits

Author SHA1 Message Date
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
Micah Kendall
d25b8f91c7 feat: Emit keyword 2024-04-12 21:40:27 -04: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
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
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
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
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
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
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
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
bfcfc5c41b Implement reification from Maps. 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
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
rvcas
0ccfe60072 feat: support nested void matching 2024-02-13 21:29:24 -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
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
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
microproofs
e25be7643e discards will now check for type too. 2024-02-07 11:48:52 -05:00
microproofs
a83220c8d9 fix: module_name was being overrided by the moduleselect field 2024-01-30 23:52:50 -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
microproofs
51f1f2b67f change redundant if branches 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
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
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
microproofs
f79b37d551 Replace 'bool' with 'TraceLevel' in codegen
Co-authored-by: KtorZ <matthias.benkort@gmail.com>
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