Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Soft casting with if/is #959

Merged
merged 19 commits into from
Jun 25, 2024
Merged

Soft casting with if/is #959

merged 19 commits into from
Jun 25, 2024

Conversation

rvcas
Copy link
Member

@rvcas rvcas commented Jun 11, 2024

closes #889

This PR introduces a long awaited feature that I have started calling soft casting.

The main idea is that there are many different payloads of type Data that one may encounter which may not necessarily
fit into one big enum style type in Aiken. We needed a syntax that would allow people to check if something is of a certain type or otherwise do something else. Given the conditional nature of this we decided it would make sense to enhance the existing if expressions to be able to attempt casting but without returning an error by using the provided else instead.

CleanShot 2024-06-11 at 19 56 49@2x

CleanShot 2024-06-11 at 19 59 36@2x

Unit tests within aiken passing

test if_soft_cast() {
  let d: Data = Foo { a: 1 }

  if d is Foo {
    d.a == 1
  } else {
    False
  }
}


test if_soft_cast_2() {
  let d: Data = Bazz(1)

  if d is Foo {
    d.a == 1
  } else if d is Bazz(y): Bar {
    y == 1
  } else {
    False
  }
}

test if_soft_cast_3() {
  let d: Data = Bazz(1)
  let x: Data = Buzz(2)

  if d is Foo {
    d.a == 1
  } else if d is Bazz(y): Bar {
    y == 1
  } else if x is Buzz(y): Bar {
    y == 2
  } else {
    False
  }
}

CleanShot 2024-06-11 at 20 03 35@2x

rvcas and others added 18 commits June 25, 2024 18:16
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.
@rvcas rvcas merged commit 5bdea11 into main Jun 25, 2024
9 checks passed
@rvcas rvcas deleted the rvcas/if-is branch June 25, 2024 22:50
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
Status: ✅ In Next Release
Development

Successfully merging this pull request may close these issues.

Provide a mechanism for non-terminating cast from Data
3 participants