Commit Graph

164 Commits

Author SHA1 Message Date
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
microproofs
ebe415cfc9 fix errors 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
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
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
Micah Kendall
ff4ddfbe1b Simplifying PR per reviewers request 2024-04-12 21:40:27 -04:00
Micah Kendall
d25b8f91c7 feat: Emit keyword 2024-04-12 21:40:27 -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
KtorZ
ed9f5c6ef7 Preserve TypeAlias in types for better context/feedback. 2024-03-08 15:59:33 +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
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
rvcas
d698f76e3c fix(codegen): builtin calls for g1 and g2 where flipped
closes #840
2024-02-29 12:13:51 -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
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
KtorZ
a12c374258 Start turning AirTree statements into expressions (let)
Still many places to fix, WIP.
2024-02-07 12:36:35 -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
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
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
36a0b317ad fix condition to account for tail presence 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
956c3d6cf0 feat: refactor code gen to avoid builtin errors when tracing is turned on 2024-01-24 16:29:40 -05: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
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
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
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