feat: binary operator

[cpehle]

Implements creation of binary operator instructions. It might make sense to use the IRBuilderBase creation methods instead of these, since it contains a ton of convenience functions for creation of intrinsics and has a very homogeneous API, which would be easy albeit slightly tedious to wrap.

[tydeu]

@cpehle fyi, the Papyrus Builder and Script interfaces are for conveniently creating instructions -- the IR bindings & API are the back-end for that. As such, Papyrus will probably not include IRBuilder bindings. However, I am hoping to replicate most of its functionality in the Builder and Script interfaces.

[tydeu]

Also, on a more general note, the Lean standard code style for terms of type Prop is snake case..

[cpehle]

I meant convenient to implement, some of the functionality in IRBuilder would be tedious and error prone to replicate and more dependent on LLVM implementation details than otherwise, e.g. https://llvm.org/doxygen/classllvm_1_1IRBuilderBase.html#a09180737dfe9015739f3dedfe7da2883. My feeling is that would even be true for the more basic arithmetic operations, which is why I wanted to bring it up.

[tydeu]

@cpehle Sorry, but I am not sure what you are getting at. For instance, that example is just a call of an Intrinsic, the former already has bindings and I certainly hope to add the later at some point in the future.

[cpehle]

That function is ~5 lines of C++ code, creating a wrapper for it would be ~2-3 lines of C++ code and ~2 lines of simple Lean code. From a perspective of generating complete bindings quickly wrapping IRBuilder gives one a very homogenous interface for most of the remaining instructions (one doesn't have to pass in enum values manually) and the behaviour of the Create calls will be consistent independent of changes in LLVM.

[tydeu]

@cpehle

. From a perspective of generating complete bindings quickly wrapping IRBuilder gives one a very homogenous interface for most of the remaining instructions

Ah, there's the rub. My goal with Papyrus is not to generate complete bindings quickly -- one could probably just have used the C interface then (and potentially even done so automatically).

Put simply, Papyrus is a pet project for me to both better learn LLVM and Lean and to create the Script DSL. Papyrus Script is meant to be a DSL where one can write LLVM syntax, analyze it, reason about it, run it, and compile it -- all interactively. I also want it to be compatible with the various back-ends, optimization passes, and analysis systems people have written for LLVM . As I see it, this creates two over-arching (though sometimes conflicting) design goals: (1) minimize the overhead between LLVM and Lean representation so that it can easily interoperate with LLVM extensions, (2) represent as much of LLVM in pure Lean as possible so that it can be reasoned about and manipulated by Lean. I feel that having opaque definitions for things that could otherwise not be opaque is contrary to the latter goal.

[tydeu]

@cpehle On a different, code review, note, InstructionRef is a ValueRef. Instructions don't need to extend both or have Coe instances for both (they only need to extend/Coe to InstructionRef.

[cpehle]

@cpehle On a different, code review, note, InstructionRef is a ValueRef. Instructions don't need to extend both or have Coe instances for both (they only need to extend/Coe to InstructionRef.

Ah good to know, I was wondering why the other Refs did not implement them. I guess it would be possible to override it if that was necessary. I will remove them.

[tydeu]

@cpehle A note on the binop macros, you should be able to capture the op name with an antiquote (e.g., a $) and convert that to an ident instead of copying it multiple times. In fact you might just be able to directly capture it with $x and use it with $x.

[cpehle]

@cpehle A note on the binop macros, you should be able to capture the op name with an antiquote (e.g., a $) and convert that to an ident instead of copying it multiple times.

I figured that was possible but didn't quite know how to do it 😆.

[tydeu]

@cpehle makes sense! Fyi, I did some testing and something like this should work:

| `(op| add%$x $y) => 
  let fn := mkIdentFrom x x.getKind
  `($fn $y)

Despite appearances, that will in fact match all the binary ops not just add.

[cpehle]

Ok I'm running into the following issue, the code for the script generation fails as is with

+out/script/dump.lean:41:9-41:12: error: unknown identifier 'add'
+out/script/dump.lean:42:9-42:12: error: unknown identifier 'mul'
+out/script/dump.lean:43:9-43:12: error: unknown identifier 'sub'
...

modifying

def expandBinaryOpInst (name : Syntax) : (stx : Syntax) → MacroM Syntax
| `(binaryOpInst| add $ty:llvmType $s1:llvmValue, $s2:llvmValue) => do
  let s1x ← expandValueAsRefArrow s1
  let s2x ← expandValueAsRefArrow s2
  `(add $s1x $s2x $name)
| `(binaryOpInst| fadd $ty:llvmType $s1:llvmValue, $s2:llvmValue) => do
  let fn := mkIdentFrom x x.getKind
  let s1x ← expandValueAsRefArrow s1
  let s2x ← expandValueAsRefArrow s2
  `(fadd $s1x $s2x $name)
... 
| inst => Macro.throwErrorAt inst "ill-formed binary operator"

instead results in expansion to only "add" (or whatever other binOp is first). I guess I'm misunderstanding how the matching works.

[cpehle]

Ok, I found a solution which is certainly not concise, but seems to produce the correct expected result. I hope you are ok btw. with me wildly flaying trying to get this to work. If you prefer to work on this on your own pace and without too many outside contributions I would totally understand.

[tydeu]

@cpehle

Ok I'm running into the following issue, the code for the script generation fails as is with

+out/script/dump.lean:41:9-41:12: error: unknown identifier 'add'
+out/script/dump.lean:42:9-42:12: error: unknown identifier 'mul'
+out/script/dump.lean:43:9-43:12: error: unknown identifier 'sub'
...

That was because my example for converting the instruction to an identifier didn't add the proper namespace. A more accurate example would have been:

@[macro op]
def expandOp : Macro
| `(op| add%$x $y) => 
  let fn := mkCIdentFrom x (`Papyrus.Builder ++ x.getKind)
  `($fn $y)
| _ => Macro.throwUnsupported

[cpehle]

@cpehle

Ok I'm running into the following issue, the code for the script generation fails as is with

+out/script/dump.lean:41:9-41:12: error: unknown identifier 'add'
+out/script/dump.lean:42:9-42:12: error: unknown identifier 'mul'
+out/script/dump.lean:43:9-43:12: error: unknown identifier 'sub'
...

That was because my example for converting the instruction to an identifier didn't add the proper namespace. A more accurate example would have been:

@[macro op]
def expandOp : Macro
| `(op| add%$x $y) => 
  let fn := mkCIdentFrom x (`Papyrus.Builder ++ x.getKind)
  `($fn $y)
| _ => Macro.throwUnsupported

Makes sense, I figured it could be a namespace issue.

[tydeu]

@cpehle

hope you are ok btw. with me wildly flaying trying to get this to work. If you prefer to work on this on your own pace and without too many outside contributions I would totally understand.

If you are okay with "wildy flaying", I am more than happy to accept what contributions you can offer. However, it may be true that eating more of your time (and maybe even my time) than it would take me to write similar code. Thus, at the moment, I think it is more of question of whether you find this back-and-forth profitable for yourself or if there are other things you would rather be doing. Personally, I tend to enjoy these kinds of educational discussions, so you are not really inconveniencing me,.

[tydeu]

@cpehle

I thought about my previous comment some more. There are still some large refactors I would like to do to the script/instruction codebase, and thus more instructions do increase the refactoring burden for me. Therefore, while I do appreciate the contributions, and I do think will merge the two PRs, I would suggest holding off on PR'ing further instruction bindings for now.

[cpehle]

If you are okay with "wildy flaying", I a more than happy to accept what contributions you can offer. However, it may be true that eating more of your time (and maybe even my time) than it would take me to write similar code. Thus, at the moment, I think it is more of question of whether you find this back-and-forth profitable for yourself or if there are other things you would rather be doing. Personally, I tend to enjoy these kinds of educational discussions, so you are not really inconveniencing me,.

I find it very helpful, but I'm aware of the cost to get someone up to speed on an unfamiliar codebase, so I wanted to be mindful of your time. To me the most enjoyable part of open source is that one can learn from each other. I will try to clean the two pull requests up and then hold off on further increasing the API surface if that is not something you are keen to get contributions for right now.

[tydeu]

@cpehle Yeah, sorry about that. 😞 I had been mostly just adding the features I needed to accomplish some of the toy examples I had been playing around with without too much concern for the technical debt I was building, because I honestly wasn't expecting contributions. Give me a few weeks (at most) and I think I can get the repo to a much better state for them. If anything, I expected users (for whom the quality of the code itself would be less of concern) before I expected contributors. 😆