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

Machine: Handle evidence #164

Merged
merged 13 commits into from
Nov 7, 2022
Merged

Machine: Handle evidence #164

merged 13 commits into from
Nov 7, 2022

Conversation

marzipankaiser
Copy link
Contributor

Handle evidence and use it to execute effect operations in the correct context.

Is not yet correctly implemented in the llvm backend (number of stacks to pop is ignored),
so widely untested.

@marzipankaiser
Copy link
Contributor Author

For some reason, fibonacci.effekt works on my machine but fails in the CI.

@marzipankaiser
Copy link
Contributor Author

Also, while I wanted to use infixAdd for my first draft, resolving that Symbol in the Context sometimes failed, so I added EviAdd.

@b-studios
Copy link
Collaborator

For some reason, fibonacci.effekt works on my machine but fails in the CI.

Maybe stack size?

@b-studios
Copy link
Collaborator

If we absolutely have to add EviAdd then I would call it something like ComposeEvidence.

@marzipankaiser
Copy link
Contributor Author

If we absolutely have to add EviAdd then I would call it something like ComposeEvidence.

Ah, yes, that's a better name.

@marzipankaiser
Copy link
Contributor Author

marzipankaiser commented Oct 4, 2022

f85fb62 uses "infixAdd" instead of ComposeEvidence. I'm not sure if that is preferable?

Note: the current implementation would break if the type of infixAdd changed from (Int, Int): Int.

@marzipankaiser
Copy link
Contributor Author

@phischu tested it on his machine and it was indeed the stack limit being reached.

@marzipankaiser marzipankaiser marked this pull request as ready for review October 4, 2022 13:57
@marzipankaiser marzipankaiser marked this pull request as draft October 4, 2022 14:06
@marzipankaiser marzipankaiser marked this pull request as ready for review October 4, 2022 14:15
@marzipankaiser marzipankaiser force-pushed the feature/machine-evidence branch 2 times, most recently from 8befd6b to 2eab1d4 Compare October 6, 2022 11:57
@marzipankaiser
Copy link
Contributor Author

I have now semi-splitted out evidence. It is still synonymous int in most places (i.e. machine.builtins.Evidence is machine.Type.Evidence etc), but can be used as if it weren't (there is a type alias Evidence, and builtins.Here (=0) and builtins.There(_) (=_+1) work for both construction and patterns).

@b-studios
Copy link
Collaborator

Why does There take another evidence? It should just alias the number 1 IIUC.

@marzipankaiser
Copy link
Contributor Author

I think both are reasonable. I understand Here and There as the constructors of the evidence type, so There just says "outside of the current region" and still needs specification/proof as to where exactly (like with e.g. Data.List.Relation.Unary.Any etc in Agda).

I am not strongly opposed to changing it to There : Evidence = 1, although I think it's nicer this way, as it allows to construct all possible evidence values without using + (on Int).

@marzipankaiser
Copy link
Contributor Author

After rethinking it, I changed There to be 1 now.

@marzipankaiser
Copy link
Contributor Author

(and rebased to current master)

marzipankaiser and others added 5 commits November 7, 2022 16:29
Note: `params.map(transform)` should take care of evidence parameters, too
If the evidence is 0, we still want to `shift0 1` etc.
* `LiteralEvidence` and `ComposeEvidence` to work with evidence
* Scala type alias `Evidence` and Machine type alias `builtins.Evidence`
* Alias `builtins.Here` and `builtins.There(_)` for literal evidence
* `PopStacks` now pops n+1 stacks (until the nth one)!
@b-studios b-studios merged commit 8c46e40 into master Nov 7, 2022
@b-studios b-studios deleted the feature/machine-evidence branch November 7, 2022 17:39
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

Successfully merging this pull request may close these issues.

3 participants