Commit Graph

2175 Commits

Author SHA1 Message Date
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
KtorZ b28d4a6e9f
Add input reference to ReferenceInputNotFound error.
Fixes #974.
2024-08-01 15:29:39 +02:00
KtorZ 34d5bc71b1
Add one more edge-case test for multiline. 2024-08-01 15:21:53 +02:00
KtorZ 91aa435f37
Fix 'multiline' truncating last character of each line.
Fixes #987.
2024-08-01 15:20:43 +02:00
KtorZ b8bb480bff
Fix 'aiken new' workflow template 2024-07-26 13:56:26 +02:00
rvcas 4645fd3e28
chore: Release 2024-07-25 08:28:15 -04:00
KtorZ 53b5a5ccee
Screw windows too, until next non-alpha. 2024-07-25 12:24:47 +02:00
KtorZ 9dc4c915f3
Manually set windows version. 2024-07-25 12:07:27 +02:00
KtorZ 9e08f9b4e6
Re-add wix file for Windows release. 2024-07-25 11:48:27 +02:00
KtorZ 26c3e95a06
screw musl targets, for now. 2024-07-25 11:29:52 +02:00
KtorZ 49190b485a
chore: Release 2024-07-25 09:58:06 +02:00
Matthias Benkort 594a304190
Merge pull request #980 from aiken-lang/multivalidator-plus-optimization
Mutlivalidator is now an opcode to help minimize validator size
2024-07-25 09:47:47 +02:00
microproofs c286ada08d
clippy fix 2024-07-24 11:29:55 -04:00
microproofs dfce9c1d96
feat: Add multivalidator as an AIR tree opcode.
feat: Add uplc eval optimization
2024-07-24 10:00:08 -04:00
KtorZ 67493ad847
Fix casting inferrence on patterns
The original goal for this commit was to allow casting from Data on
  patterns without annotation. For example, given some custom type
  'OrderDatum':

  ```
  expect OrderDatum { requested_handle, destination, .. }: OrderDatum = datum
  ```

  would work fine, but:

  ```
  expect OrderDatum { requested_handle, destination, .. } = datum
  ```

  Yet, the annotation feels unnecessary at this point because type can
  be inferred from the pattern itself. So this commit allows, whenever
  possible (ie when the pattern is neither a discard nor a var), to
  infer the type from a pattern.

  Along the way, I also found a couple of weird behaviours surrounding
  this kind of assignments, in particular in combination with let. I'll
  highlight those in the next PR (#979).
2024-07-24 12:42:24 +02:00
KtorZ 30ddfa23d9
Provide better parse errors in trace when using comma instead of colon. 2024-07-19 12:28:08 +02:00
KtorZ 2922c0aa6f
Display expected patterns/tokens in parse error when applicable.
We've never been using those 'expected' tokens captured during
  parsing, which is lame because they contain useful information!

  This is much better than merely showing our infamous

    "Try removing it!"
2024-07-19 12:28:08 +02:00
KtorZ d6fd37c80e
Rework 'compact' mode for traces
- Trace-if-false are now completely discarded in compact mode.

  - Only the label (i.e. first trace argument) is preserved.

  - When compiling with tracing _compact_, the first label MUST unify to
    a string. This shouldn't be an issue generally speaking and would
    enforce that traces follow the pattern

    ```
    label: arg_0[, arg_1, ..., arg_n]
    ```

  Note that what isn't obvious with these changes is that we now support
  what the "emit" keyword was trying to achieve; as we compile now with
  user-defined traces only, and in compact mode to only keep event
  labels in the final contract; while allowing larger payloads with
  verbose tracing.
2024-07-19 12:28:08 +02:00
KtorZ a9d782e206
re-introduce code-gen patch, but with a test.
Actually, this has been a bug for a long time it seems. Calling any
  prelude functions using a qualified import would result in a codegen
  crash. Whoopsie.

  This is now fixed as shown by the regression test.
2024-07-19 12:28:07 +02:00
KtorZ 5afcc9b0c1
Remove unnecessary code_gen patch.
This is a little weird but, prelude functions are handled slightly
  differently.
2024-07-19 12:28:07 +02:00
KtorZ f8236817fe
Allow serialisable (Data-able) arguments to trace
Somehow, we have to patch some function in gen_uplc because of the
  module name. I have to look further into this because it isn't normal.
2024-07-19 12:28:07 +02:00
KtorZ beb5ac4643
Add 'diagnostic' to the prelude, as well as companion functions.
This is not fully satisfactory as it pollutes a bit the prelude. Ideally, those functions should only be visible
  and usable by the underlying trace code. But for now, we'll just go with it.
2024-07-19 12:28:07 +02:00
KtorZ 754ed07408
Type-check variadic traces & desugarize them. 2024-07-18 10:02:23 +02:00
KtorZ f9719af23e
Allow variadic arguments in trace
Although, doesn't do anything with them yet. The idea is to simplify
  the use of trace to make it a lot more useful than it currently is.
2024-07-18 10:01:34 +02:00
KtorZ 976262c2e6
Allow discard in expect.
Fixes #967.
2024-07-17 18:11:09 +02:00
KtorZ 0145237bbe
Version wix boilerplate. 2024-07-16 17:33:49 +02:00
rvcas 5bdea11cc1 fix: add a new assignment kind instead of using a boolean 2024-06-25 18:50:00 -04:00
microproofs f1cfc84e67 Fix tree traversal node selection for a few of the enum variants 2024-06-25 18:50:00 -04:00
microproofs 9907dd6c64 Fix unit tests 2024-06-25 18:50:00 -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 f695276bf7 Fix codegen tree traversal to be updated for the otherwise field and future proof the traversal function 2024-06-25 18:50:00 -04:00
microproofs b5ac5bc949 Add current fixed tests and start working on codegen fix 2024-06-25 18:50:00 -04:00
microproofs f0f1296906 Fix more 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 41b941e0e3 Fix castfromData in record access cases 2024-06-25 18:50:00 -04:00
KtorZ 00d1927dad Add few more test cases for the parser and type-checker. 2024-06-25 18:50:00 -04:00
rvcas aeb079334e chore: this test doesn't make sense anymore 2024-06-25 18:50:00 -04:00
rvcas 8f343abaa1 chore: add new snapshots 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 579abb7d3d fix: no need to check exhaustiveness during if/is 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
rvcas 1b8805825b feat: impl if/is
This commit introduces a new feature into
the parser, typechecker, and formatter.
The work for code gen will be in the next commit.

I was able to leverage some existing infrastructure
by making using of `AssignmentPattern`. A new field
`is` was introduced into `IfBranch`. This field holds
a generic `Option<Is>` meaning a new generic has to be
introduced into `IfBranch`. When used in `UntypedExpr`,
`IfBranch` must use `AssignmentPattern`. When used in
`TypedExpr`, `IfBranch` must use `TypedPattern`.

The parser was updated such that we can support this
kind of psuedo grammar:

`if <expr:condition> [is [<pattern>: ]<annotation>]`

This can be read as, when parsing an `if` expression,
always expect an expression after the keyword `if`. And then
optionally there may be this `is` stuff, and within that you
may optionally expect a pattern followed by a colon. We will
always expect an annotation.

This first expression is still saved as the field
`condition` in `IfBranch`. If `pattern` is not there
AND `expr:condition` is `UntypedExpr::Var` we can set
the pattern to be `Pattern::Var` with the same name. From
there shadowing should allow this syntax sugar to feel
kinda magical within the `IfBranch` block that follow.

The typechecker doesn't need to be aware of the sugar
described above. The typechecker looks at `branch.is`
and if it's `Some(is)` then it'll use `infer_assignment`
for some help. Because of the way that `is` can inject
variables into the scope of the branch's block and since
it's basically just like how `expect` works minus the error
we get to re-use that helper method.

It's important to note that in the typechecker, if `is`
is `Some(_)` then we do not enforce that `condition` is
of type `Bool`. This is because the bool itself will be
whether or not the `is` itself holds true given a PlutusData
payload.

When `is` is None, we do exactly what was being done
previously so that plain `if` expressions remain unaffected
with no semantic changes.

The formatter had to be made aware of the new changes with
some simple changes that need no further explanation.
2024-06-25 18:50:00 -04:00
rvcas b2c42febaf chore: move if_branch to helper parser 2024-06-25 18:50:00 -04:00
Dima S d99c014bf7 chore: correct the usage of a legacy numeric constant 2024-06-25 17:49:36 -04:00
rvcas de870e2529
feat: warning on compiler version mismatch 2024-06-13 20:26:44 -04:00
KtorZ 0ebffa2b9e
Fix few error messages. 2024-06-13 14:54:47 +02:00
KtorZ 858dfccc82
Authorize complete patterns as function args.
This is mainly a syntactic trick/sugar, but it's been pretty annoying
  to me for a while that we can't simply pattern-match/destructure
  single-variant constructors directly from the args list. A classic
  example is when writing property tests:

  ```ak
  test foo(params via both(bytearray(), int())) {
    let (bytes, ix) = params
    ...
  }
  ```

  Now can be replaced simply with:

  ```
  test foo((bytes, ix) via both(bytearray(), int())) {
    ...
  }
  ```

  If feels natural, especially coming from the JavaScript, Haskell or
  Rust worlds and is mostly convenient. Behind the scene, the compiler
  does nothing more than re-writing the AST as the first form, with
  pre-generated arg names. Then, we fully rely on the existing
  type-checking capabilities and thus, works in a seamless way as if we
  were just pattern matching inline.
2024-06-07 15:42:25 +02:00
KtorZ b6da42baf2
Bump 'is_validator_param' up from 'ArgName' to '...Arg'
There's no reasons for this to be a property of only ArgName::Named to begin with. And now, with the extra indirection introduced for arg_name, it may leads to subtle issues when patterns args are used in validators.
2024-06-07 11:32:05 +02:00
KtorZ 4d42c6cb19
Introduce 'ArgBy' to allow defining function arg not only by name. 2024-06-07 11:17:16 +02:00
KtorZ 216dab99d4
chore: Release 2024-06-06 11:19:34 +02:00
KtorZ d7ec2131ef
Automatically merge import lines from same module.
I slightly altered the way we parse import definitions to ensure we
  merge imports from the same modules (that aren't aliased) together.

  This prevents an annoying warning with duplicated import lines and
  makes it just more convenient overall.

  As a trade-off, we can no longer interleave import definitions with
  other definitions. This should be a minor setback only since the
  formatter was already ensuring that all import definitions would be
  grouped at the top.

  ---

  Note that, I originally attempted to implement this in the formatter
  instead of the parser. As it felt more appropriate there. However, the
  formatter operates on (unmutable) borrowed definitions, which makes it
  annoyingly hard to perform any AST manipulations. The `Document`
  returns by the format carries a lifetime that prevents the creation of
  intermediate local values.

  So instead, slightly tweaking the parser felt like the right thing to
  do.
2024-06-04 10:48:42 +02:00
KtorZ 2070576e46
New LSP quickfix for 'use let' warning. 2024-05-30 19:30:41 +02:00
KtorZ e9e26b969a
Preserve warning display rework, but without breaking the LSP quickfixes. 2024-05-30 19:20:11 +02:00
KtorZ 649e5163fc
Fix parsing of single hex-digits. 2024-05-30 17:19:48 +02:00
KtorZ 5694d9f9cb
Introduce 'fail once' and alter behavior of 'fail' keyword for properties. 2024-05-30 17:18:50 +02:00
Matthias Benkort 28515e70ec
Merge pull request #950 from hadelive/k256-error
Fix k256 error does not implement clone
2024-05-30 13:42:57 +02:00
hade 740e140c89
fix: custom k256 error 2024-05-30 16:13:51 +07:00
hade b367ec2113
fix: fmt check 2024-05-30 16:09:32 +07:00
hade ad3c9f24b7
chore: minimal pallas dependencies 2024-05-30 15:09:05 +07:00
rvcas cb4c01f46b
chore: remove msi and update cargo dist 2024-05-23 21:07:44 -04:00
rvcas 338fc0eba6
chore: Release 2024-05-23 16:45:10 -04:00
rvcas ed73df302a
fix: completions should not work on windows 2024-05-23 16:43:56 -04:00
rvcas ff50d4d2cf
chore: Release 2024-05-23 16:23:59 -04:00
microproofs 59cfa209d7 change uplc version number based on plutus version 2024-05-23 15:04:59 -04:00
KtorZ e2bc3a9fc4
Update blueprint generation to work with Pairs.
Closes #938.
2024-05-23 18:15:46 +02:00
KtorZ c48f15a957
revert #903 'feat: Emit keyword'
While we agree on the idea of having some ways of emitting events, the
  design hasn't been completely fleshed out and it is unclear whether
  events should have a well-defined format independent of the framework
  / compiler and what this format should be.

  So we need more time discussing and agreeing about what use case we
  are actually trying to solve with that.

  Irrespective of that, some cleanup was also needed on the UPLC side
  anyway since the PR introduced a lot of needless duplications.
2024-05-23 17:22:12 +02:00
KtorZ 5ce30b2632
Rename AList -> Pairs due to popular demand. 2024-05-23 16:45:40 +02:00
KtorZ 8e0f32a577
Fix negative evaluation costs
Whoopsie.
2024-05-23 11:21:47 +02:00
microproofs 3d06129d9b add test for curry optimization that is a reduced case of #945 2024-05-22 15:46:32 -04:00
rvcas c3ad52b50f
feat: add compiler version to aiken.toml 2024-05-22 15:35:57 -04:00
microproofs d6cc450ce4 The actual issue with #945 is that the curry builtin reducer could sometimes place fully applied builtins that could evaluate and fail above where they were actually used. This happened with builtins that were called with the same constants enough times for the curry builtin to try hoist to a higher scope. This is now fixed by detecting which builtins are safe to evaluate in advance before we hoist fully applied builtins 2024-05-22 15:22:31 -04:00
rvcas c1a913f420
fix(config): add default for plutus version 2024-05-22 13:59:56 -04:00
rvcas 7f38b55c1c
fix: comments in record patterns closes #946 2024-05-22 12:26:36 -04:00
microproofs c16bd06e97 make sure traverse_uplc_with_helper is always passing the arg to lambda before running the with function.
Breaks #945 again
2024-05-22 11:58:05 -04:00
rvcas edf82f773c
chore: update snapshots 2024-05-22 11:30:02 -04:00
rvcas f5c4f4cb37
chore(plutus_version): use a cuter name in the config field 2024-05-21 17:13:12 -04:00
microproofs 489eff7f5b Closes #945
Switch to depth first optimization passes instead of breadth first for inlining. Need to think more on how to do breadth first optimization passes
2024-05-21 17:12:57 -04:00
rvcas e28b0df840
fix: add v3 mapping for builtin semantics relates to #907 2024-05-21 17:06:18 -04:00
rvcas 050d003b27
feat: use plutus version in convert command
relates to #907
2024-05-21 17:05:02 -04:00
rvcas f306f1715a
feat: use plutus version in address command
relates to #907
2024-05-21 17:04:25 -04:00
rvcas 3bc3792aa3
feat: add plutus version to aiken.toml
relates to #907
2024-05-21 17:02:20 -04:00
rvcas 4ca73c4cdf
fix: closes #898
This is the best we can do for this without
rearchitecting when we rewrite backpassing to
plain ol' assignments. In this case, if we see
a var and there is no annotation (thus probably not a cast),
then it's safe to rewrite to a `let` instead of an `expect`.
This way, we don't get a warning that is **unfixable**.
We are not trying to solve every little warning edge
case with this fix. We simply just can't allow there
to be a warning that the user can't make go away through
some means. All other edge cases like pattern matching on
a single contructor type with expect warnings can be fixed
via other means.
2024-05-21 15:21:24 -04:00
microproofs c1c2cd97b7 New test 103 and clippy fixes 2024-05-21 11:56:12 -04:00
KtorZ a3c14d881d
Merge branch 'fix/scope-when-backtracking' 2024-05-16 23:43:00 +02:00
KtorZ 7ff6eba869
Prefer '.clone_from' over mutating a clone.
Clippy says it's more efficient. I trust clippy. Clippy good.
2024-05-16 23:42:53 +02:00
KtorZ ea3e79c132
Renamed 'unseed' -> 'not_yet_inferred' 2024-05-16 23:33:23 +02:00
KtorZ 27b3536f09
Also preserve warnings when resetting scope for backtracking.
This is crucial as some checks regarding variable usages depends on
  warnings; so we may accidentally remove variables from the AST as a
  consequence of backtracking for deep inferrence.
2024-05-16 23:20:52 +02:00
KtorZ e87063824c
Fix pretty-printing of recursive type-alias causing stack overflow.
Fixes #942.
2024-05-16 17:20:26 +02:00
KtorZ eadf709411
Fix scope management issue when deep-inferring callee.
Fixes #941.

  However, this currently breaks the stdlib somehow with some FreeUnique on the shrinker step of the optimizer.
2024-05-15 13:18:51 +02:00
KtorZ 1ed4fa1c69
Show warning when ignoring modules + restyle warnings slightly
Fixes #916.
2024-05-14 13:27:19 +02:00
KtorZ 81219cfbdd
Check for data-type serialisability after generic instantiation
Fixes #939.
2024-05-14 10:58:58 +02:00
KtorZ 26ef25ba8d
Make comparison of non-serialisable types illegal.
Fixes #940.
2024-05-14 10:45:15 +02:00
KtorZ c5de9adcd3
Add some log output / feedback to completion --install 2024-05-10 17:31:48 +02:00
rvcas c86978b5ac
fix: clippy and add docs to the new flag 2024-05-10 10:51:29 -04:00
KtorZ 8c67be55ce
Fixes #921: top-level Miller-loop needs not to be serialisable
This is a bit tricky, but in a similar way where we allow functions to
  be returned by functions, this must also work for MillerLoopResult.
2024-05-10 13:52:23 +02:00
KtorZ 83c0566afb
Merge remote-tracking branch 'freexploit/add-completion-install' 2024-05-10 13:11:10 +02:00
Christopher Valerio 6df1fcb9b0
Merge branch 'aiken-lang:main' into add-completion-install 2024-05-08 10:03:34 -06:00
rvcas f8ce46d0f4 chore(ci): run cargo dist init 2024-05-08 11:05:30 -04:00
microproofs 878298cc8e don't use generic data type lookup when you have a Record Variant as a function 2024-05-06 15:17:01 -04:00
KtorZ a124bdbb05 Infer callee first in function call
The current inferrence system walks expressions from "top to bottom".
  Starting from definitions higher in the source file, and down. When a
  call is encountered, we use the information known for the callee
  definition we have at the moment it is inferred.

  This causes interesting issues in the case where the callee doesn't
  have annotations and in only partially known. For example:

  ```
  pub fn list(fuzzer: Option<a>) -> Option<List<a>> {
    inner(fuzzer, [])
  }

  fn inner(fuzzer, xs) -> Option<List<b>> {
    when fuzzer is {
      None -> Some(xs)
      Some(x) -> Some([x, ..xs])
    }
  }
  ```

  In this small program, we infer `list` first and run into `inner`.
  Yet, the arguments for `inner` are not annotated, so since we haven't
  inferred `inner` yet, we will create two unbound variables.

  And naturally, we will link the type of `[]` to being of the same type
  as `xs` -- which is still unbound at this point. The return type of
  `inner` is given by the annotation, so all-in-all, the unification
  will work without ever having to commit to a type of `[]`.

  It is only later, when `inner` is inferred, that we will generalise
  the unbound type of `xs` to a generic which the same as `b` in the
  annotation. At this point, `[]` is also typed with this same generic,
  which has a different id than `a` in `list` since it comes from
  another type definition.

  This is unfortunate and will cause issues down the line for the code
  generation. The problem doesn't occur when `inner`'s arguments are
  properly annotated or, when `inner` is actually inferred first.

  Hence, I saw two possible avenues for fixing this problem:

  1. Detect the presence of 'uncongruous generics' in definitions after
     they've all been inferred, and raise a user error asking for more
     annotations.

  2. Infer definitions in dependency order, with definitions used in
     other inferred first.

  This commit does (2) (although it may still be a good idea to do (1)
  eventually) since it offers a much better user experience. One way to
  do (2) is to construct a dependency graph between function calls, and
  ensure perform a topological sort.

  Building such graph is, however, quite tricky as it requires walking
  through the AST while maintaining scope etc. which is more-or-less
  already what the inferrence step is doing; so it feels like double
  work.

  Thus instead, this commit tries to do a deep-first inferrence and
  "pause" inferrence of definitions when encountering a call to fully
  infer the callee first. To achieve this properly, we must ensure that
  we do not infer the same definition again, so we "remember" already
  inferred definitions in the environment now.
2024-05-06 15:17:01 -04:00
KtorZ 7b71389519 Change pretty-printing of unbound variable to '?'
Until now, we would pretty-print unbound variable the same way we would pretty-print generics. This turned out to be very confusing when debugging, as they have a quite different semantic and it helps to visualize unbound types in definitions.
2024-05-06 15:17:01 -04:00
KtorZ ef70c6b8a8 Re-use generic id across builtin type-definitions.
This was somehow wrong and corrected by codegen later on, but we should be re-using the same generic id across an entire definition if the variable refers to the same element.
2024-05-06 15:17:01 -04:00
KtorZ 1070347203 Panic when encountering unknown generics.
This should not happen; if it does, it's an error from the type-checker. So instead of silently swallowing the error and adopting a behavior which is only _sometimes_ right, it is better to fail loudly and investigate.
2024-05-06 15:17:01 -04:00
microproofs b2661ef90a Better error message for compile time evaluation 2024-05-06 11:58:32 -04:00
microproofs 68f1dcc65d Add comment as a reminder to future me 2024-05-06 11:48:10 -04:00
microproofs 2f61f59b60 Closes #909 2024-05-06 11:35:05 -04:00
microproofs a44ed4c1a8 Change prelude Map to AList 2024-05-04 14:04:12 -04:00
KtorZ b1f0dfdacd Implement parser & formatter for Pair annotations. 2024-05-04 14:04:12 -04:00
microproofs 58779401e8 fix: formatting was eating the space in pair after the , 2024-05-04 14:04:12 -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 1091eba3c3 Review & fix acceptance tests
Temporarily using the 'specialize-dict-key' branch from the stdlib
  which makes use of Pair where relevant. Once this is merged back into
  'main' we should update the acceptance test toml files to keep getting
  them automatically upgraded.

  This commit also fixes an oversight in the reification of data-types
  now properly distinguishing between pairs and 2-tuples.

  Co-authored-by: Microproofs <kasey.white@cardanofoundation.org>
2024-05-04 14:04:12 -04:00
KtorZ 03a5a9293c Replace snapshot test for export recursive function
This test contains a pattern match on a 2-tuple, which induced a
  slight code change in UPLC as expected.
2024-05-04 14:04:12 -04:00
KtorZ 7cb548a749 Fix ordinal index on pairs 2024-05-04 14:04:12 -04:00
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 390bccd406 Fix blueprint validator test snapshot. 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 d7574e738f fix: remaining cargo tests 2024-05-04 14:04:12 -04:00
microproofs 999e408a28 fix some more tests 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 cb1ca84dad fixing more tests 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
Christopher Valerio 24560e9acd
fix: fixing bash messages 2024-04-28 17:21:19 -06:00
Christopher Valerio 6c052f44a1
fix: Adding better error messages 2024-04-28 17:18:37 -06:00
Christopher Valerio 3c66da75d6
Improving errors 2024-04-28 17:13:48 -06:00
Christopher Valerio 063f3d0835
feat: Adding installation for fish and bash 2024-04-28 17:04:46 -06:00
Christopher Valerio c5faffe946
feat: adding oh-my-zsh support 2024-04-28 17:04:46 -06:00
Christopher Valerio 949f16f34a
rebase from main 2024-04-28 17:04:40 -06:00