Idea: Possible way to shorten the code of the MLIR Parser

[AtticusKuhn]

Here is an idea that could shorten the code for the lean-mlir parser substantially.

The gist of this idea is to not do any typechecking ourselves, but to syntactically transform the llvm expression into a lean expresion so that the lean compiler does the typechecking.

For example, we could have an elaborator which would elaborate

[llvm|{
^bb0(%arg0: i8, %arg1: i8):
    %0 = "llvm.mlir.constant"() <{value = 42 : i8}> : () -> i8
    %1 = "llvm.shl"(%0, %arg1) <{overflowFlags = #llvm.overflow<none>}> : (i8, i8) -> i8
    %2 = "llvm.add"(%1, %arg0) <{overflowFlags = #llvm.overflow<none>}> : (i8, i8) -> i8
    "llvm.return"(%2) : (i8) -> ()
}]

into

def bb0(varg0 varg1: BitVec 8) := do
   let v0 <- llvm.mlir.constant () {value := 42}
   let v1 <- llvm.shl (v0, varg1) {overflowFlags :=  overflowflag.none}
   let v2 <- llvm.add (v1, varg0) {overflowFlags :=  overflowflag.none}
   pure v2

This way, our macros would only do a syntactic transformation, and leave the type-checking to the lean compiler. The benefit of this idea is that we could drastically reduce the number of lines of code in the parser.

[AtticusKuhn]

cc: @alexkeizer because he knows a lot about the parser.

[alexkeizer]

It's an interesting idea! One thing to keep in mind, though, is that we intend to prove things about the programs defined by the macro, so we currently do our best to have the DSL generate IComs in a normal(-ish) form.

Now, this can work with your syntactic translation approach, it would involve doing a lot of reduction. This reduction can be quite fragile, and in fact, we've been trying to reduce the amount of full-blown reduction needed to more controlled approaches through simp-sets. This can be made to work with this approach as well, I'm sure, but you run the risk of in the process really only moved the complexity around.

Furthermore, having to do our own type checking means we have to, well, implement our own typechecking, yes, but it also means we get to generate our own, meaningful errors. Having Lean do the type-checking means letting Lean generate the type errors, and those are likely going to be in terms of the translation, making it a particularly leaky abstraction and not very user friendly.