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

Addition of multiplication and division in Pancake #936

Open
Kswin01 opened this issue Mar 16, 2023 · 1 comment
Open

Addition of multiplication and division in Pancake #936

Kswin01 opened this issue Mar 16, 2023 · 1 comment
Labels
Pancake

Comments

@Kswin01
Copy link

Kswin01 commented Mar 16, 2023

Necessary in some cases, and the current workarounds for not having access to multiplication and division are not the most elegant.
IlmariReissumies added a commit that referenced this issue Mar 20, 2023
@IlmariReissumies
Start on division and multiplication for Pancake.
8cf7359 
Adds binary division and multiplication to Pancake, and pushes it
down to loopLang. Next step: worry about how to push it to word.

While at it, I've modernised a couple of proofs to get rid of
TRY-style, and other needless detours.

This is a start on issue #936
@IlmariReissumies
Copy link
Member

I've been hacking on this for a couple of days. Multiplication should be unproblematic, but division less so.

The main issue is that not all target platforms have a division instruction that we can target, in particular ARMv7 and ag32. For those platforms, we'd have to decide to either not support division, or have the compiler insert a canned software implementation. (CakeML does the latter.) Either way, it requires making the Pancake compiler aware of what the target ISA is in a much earlier stage than is currently done.

What are people's thoughts on this? I personally think a software division implementation is somewhat contrary to the spirit of Pancake, and I'd rather not have division for such cases.

IlmariReissumies added a commit that referenced this issue May 24, 2023
@IlmariReissumies
Start on division and multiplication for Pancake.
e12a6ec 
Adds binary division and multiplication to Pancake, and pushes it
down to loopLang. Next step: worry about how to push it to word.

While at it, I've modernised a couple of proofs to get rid of
TRY-style, and other needless detours.

This is a start on issue #936
IlmariReissumies added a commit that referenced this issue May 25, 2023
@IlmariReissumies
Start on division and multiplication for Pancake.
7fff215 
Adds binary division and multiplication to Pancake, and pushes it
down to loopLang. Next step: worry about how to push it to word.

While at it, I've modernised a couple of proofs to get rid of
TRY-style, and other needless detours.

This is a start on issue #936
@IlmariReissumies IlmariReissumies mentioned this issue May 25, 2023
Merged
@mktnk3 mktnk3 added the Pancake label Jun 30, 2023
xdrr pushed a commit to xdrr/cakeml that referenced this issue Jul 8, 2023
@IlmariReissumies @xdrr
Start on division and multiplication for Pancake.
ab6fb0c 
Adds binary division and multiplication to Pancake, and pushes it
down to loopLang. Next step: worry about how to push it to word.

While at it, I've modernised a couple of proofs to get rid of
TRY-style, and other needless detours.

This is a start on issue CakeML#936
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
Pancake
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
3 participants
@IlmariReissumies @mktnk3 @Kswin01