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.

Sign up for GitHub

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

Jump to bottom

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 marzipankaiser mentioned this pull request Oct 4, 2022
Merged
@marzipankaiser
Copy link
Contributor Author

marzipankaiser commented Oct 4, 2022 •
edited
Loading

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
@marzipankaiser
Handle evidence for extern function definitions
4d1eeee
@marzipankaiser
Machine: Remove solved TODO comments regarding evidence
b78c7af 
Note: `params.map(transform)` should take care of evidence parameters, too
@marzipankaiser
Machine evidence: Shift by ev+1
5bbc445 
If the evidence is 0, we still want to `shift0 1` etc.
@marzipankaiser
Machine: Separate Evidence
177c64c 
* `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)!
@marzipankaiser
Use There to mean 1 instead of successor
67bd2ad
@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
Reviewers

@b-studios b-studios b-studios left review comments

@phischu phischu phischu approved these changes

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@marzipankaiser @b-studios @phischu