Commit Graph

153 Commits

Author SHA1 Message Date
microproofs 7c52094b15
Making progress on using interning in gen_uplc
Done interning for uniqueness. Now to fix the static optimization

Remove unused function

Fixing issues. Have a few remaining tests
2024-09-12 17:03:36 -04:00
KtorZ 6a438bc8cd Fix missing locations from generated handler code. 2024-09-03 16:21:53 -04:00
microproofs a6bc0f7157 Fix positioning on unwrap_void 2024-09-03 16:21:53 -04:00
microproofs 2be76d7cda Use Delay error directly when casting from data without traces 2024-09-03 16:21:53 -04:00
KtorZ cd0a9440e8
Allow any expression as constants
This is only a start. It compiles, but with a few TODOs left open. In particular, it doesn't currently handle constants depending on other constants or functions; nor does it hoist constants.
2024-08-29 16:24:12 +02:00
KtorZ 7ec3f2e8df
DRY builtins types creation to ensure proper consistency. 2024-08-25 16:20:06 +02:00
microproofs 72059eacee
Fix: Recursion issue where the static param optimization on recursive functions that were passed as arguments to other functions 2024-08-08 19:36:16 -04:00
microproofs 56ff4ec678 Fixing other tests 2024-08-08 00:39:44 -04:00
microproofs 33370b8637 Fix minor issues found when testing 2024-08-08 00:39:44 -04:00
KtorZ f5c4e185d4 Redact compiledCode & hash in generated blueprint tests
The point of those tests is to ensure that blueprints are generated
  properly, irrespective of the generated code. It is annoying to
  constantly get those test failing every time we introduce an
  optimization or something that would slightly change the generated
  UPLC.
2024-08-08 00:39:44 -04:00
microproofs 8a461d5bd5 Few minor changes, clippy fixes, and test fixes 2024-08-08 00:39:44 -04:00
microproofs 4cf81a19b1 Update most of the tests and builder functions to use the new delay_branch_functions 2024-08-08 00:39:44 -04:00
microproofs d7e9fef4d3 Create new helper functions to take care of force and delaying branch terms 2024-08-08 00:39:44 -04:00
KtorZ 23a3134642 Rework choose_data_xxx API to include force/delay inside functions. 2024-08-08 00:39:44 -04:00
KtorZ 021679b8ac Force unwrap_xxx_or inside function body
Otherwise, it becomes the responsibility of the caller to force the result; which may be easily forgotten.
2024-08-08 00:39:44 -04:00
microproofs a132a2e486 Fix unwrap issues 2024-08-08 00:39:44 -04:00
KtorZ aefbc6e1b9 Define a safer API for unwrap_xxx_or and choose_data_xxx
Cloning a 'Term' is potentially dangerous, so we don't want this to
  happen by mistake. So instead, we pass in var names and turn them into
  terms when necessary.
2024-08-08 00:39:44 -04:00
KtorZ 9610237616 Refactor unknown_data_to_type, break down into smaller functions. 2024-08-08 00:39:44 -04:00
KtorZ c3a61706b5 Factor out common UPLC logic for converting Data to Bool. 2024-08-08 00:39:44 -04:00
microproofs 05504b9762 Fix out of order expect check. Also fix no_inline error in code gen. @acceptance_107 2024-08-08 00:39:44 -04:00
microproofs 0be5229f1c Only 2 errors and todos left to finish 2024-08-08 00:39:44 -04:00
microproofs dd5badd884 Start work on revamping assignment so we can handle soft casting properly 2024-08-08 00:39:44 -04:00
KtorZ f14dfdf8e1
Allow pattern-matching on bytearrays
- Doesn't allow pattern-matching on G1/G2 elements and strings,
    because the use cases for those is unclear and it adds complexity to
    the feature.

  - We still _parse_ patterns on G1/G2 elements and strings, but emit an
    error in those cases.

  - The syntax is the same as for bytearray literals (i.e. supports hex,
    utf-8 strings or plain arrays of bytes).
2024-08-03 13:51:36 +02:00
KtorZ 1c58da4d86 Support mk_cons builtin
While this builtin is readily available through the Aiken syntax
  `[head, ..tail]`, there's no reason to not support its builtin form
  even though we may not encourage its usage. For completeness and to
  avoid bad surprises, it is now supported.

  Fixes #964.
2024-08-02 00:17:16 -04:00
KtorZ bf5a406ffb Remove clause guards.
Closes #886.
2024-08-02 00:16:27 -04:00
microproofs 4bd9125b86 Fix delay of arguments to be exactly the same as codegen tests 2024-06-25 18:50:00 -04:00
microproofs cc9df04093 Fix missing delay in list_access_to_uplc. Also fix one of the unit tests. 2024-06-25 18:50:00 -04:00
microproofs e09f6bbc87 delay otherwise branch to prevent premature errors 2024-06-25 18:50:00 -04:00
microproofs df939e20ce missed a Air Op Code and updated how we pass in otherwise for assignment 2024-06-25 18:50:00 -04:00
rvcas 5024bd3f9c feat: code gen support for if/is
Co-authored-by: Kasey White <kwhitemsg@gmail.com>
2024-06-25 18:50:00 -04:00
microproofs fc0e88018e Chore:
Refactor get_uplc_type to account for constr types that don't exactly resolve to a uplc type
Check arg_stack in uplc generator has only 1 argument at the end of the generation
warning fixes
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
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 26f68c2fb4 fix: found various unify and type issues while running tests 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 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
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
microproofs 61936cb91e fix(codegen): Add tracing when checking for a constr vs another primitive 2024-03-17 16:25:17 -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 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
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 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
microproofs c9dd281b45 disable assert that was blocking issue #844 2024-03-04 11:48:22 -05: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