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

The constrained output type in output variables with enum type #73

Open
verifierlife opened this issue Aug 31, 2022 · 1 comment
Open

Comments

@verifierlife
Copy link

verifierlife commented Aug 31, 2022

This file prompts:
Error at line 5: 72 function main may not use constrained output type (subrange or enumeration)
function main (choice: payload) returns (wolf, golds, cabbage, farmer: side);

Why it happens?
Some solutions please.


--farmer2.lus
type payload = enum { Empty, Wolf, Goat, Cabbage };
type side = enum { Left, Right };

function main(choice : payload) returns (wolf, goat, cabbage, farmer : side);

node testMain(choice : payload[2]) returns (wolf, goat, cabbage, farmer : side[2]);
var
wolf_0: side;
wolf_1: side;
golt_0: side;
golt_1: side;
cabbage_0: side;
cabbage_1: side;
farmer_0: side;
farmer_1: side;
let
wolf_0, golt_0, cabbage_0, farmer_0 = main(choice[0]);
wolf_1, golt_1, cabbage_1, farmer_1 = main(choice[1]);
wolf = [wolf_0, wolf_1];
goat = [goat_0, goat_1];
cabbage = [cabbage_0, cabbage_1];
farmer = [farmer_0, farmer_1];
tel;

@agacek
Copy link
Collaborator

agacek commented Aug 31, 2022

JKind (currently) doesn't allow functions to have constrained output types. I believe the reasoning is that a constrained output type means we would have to include assertions everywhere that function is used to ensure that the result value is within the constrained range.

You have two options:

  1. You can use a node instead of a function, though this requires you to explicitly specify the behavior of the node.
  2. You can return a type like int which requires you to have a way of converting that int into the constrained range.

Looking at your example, it's hard for me to tell what you are trying to accomplish with this function. I suspect that you want a node instead.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants