lean mutualrec.lean 2>&1 | hask-opt --lz-canonicalize --lean-lower --convert-scf-to-std --ptr-lower | mlir-translate --mlir-to-llvmir | ~/work/llvm-project/build/bin/opt -O3 -S | vim

direct-lower-ir.ll

define i8* @l_even(i8* %0) !dbg !3 {
  %2 = call i8* @lean_unsigned_to_nat(i64 0), !dbg !7
  %3 = call i8 @lean_nat_dec_eq(i8* %0, i8* %2), !dbg !9
  %4 = icmp eq i8 %3, 0, !dbg !10
  br i1 %4, label %5, label %9, !dbg !11

5:                                                ; preds = %1
  %6 = call i8* @lean_unsigned_to_nat(i64 1), !dbg !12
  %7 = call i8* @lean_nat_sub(i8* %0, i8* %6), !dbg !13
  %8 = call i8* @l_odd(i8* %7), !dbg !14
  br label %16, !dbg !15

9:                                                ; preds = %1
  br i1 true, label %10, label %12, !dbg !16

10:                                               ; preds = %9
  %11 = call i8* @lean_unsigned_to_nat(i64 1), !dbg !17
  br label %13, !dbg !18

12:                                               ; preds = %9
  br label %13, !dbg !19

13:                                               ; preds = %12, %10
  %14 = phi i8* [ undef, %12 ], [ %11, %10 ]
  br label %15, !dbg !20

15:                                               ; preds = %13
  br label %16, !dbg !21

16:                                               ; preds = %15, %5
  %17 = phi i8* [ %14, %15 ], [ %8, %5 ]
  br label %18, !dbg !22

18:                                               ; preds = %16
  ret i8* %17, !dbg !23
}

define i8* @l_odd(i8* %0) !dbg !24 {
  %2 = call i8* @lean_unsigned_to_nat(i64 0), !dbg !25
  %3 = call i8 @lean_nat_dec_eq(i8* %0, i8* %2), !dbg !27
  %4 = icmp eq i8 %3, 0, !dbg !28
  br i1 %4, label %5, label %9, !dbg !29

5:                                                ; preds = %1
  %6 = call i8* @lean_unsigned_to_nat(i64 1), !dbg !30
  %7 = call i8* @lean_nat_sub(i8* %0, i8* %6), !dbg !31
  %8 = call i8* @l_even(i8* %7), !dbg !32
  br label %16, !dbg !33

9:                                                ; preds = %1
  br i1 true, label %10, label %12, !dbg !34

10:                                               ; preds = %9
  %11 = call i8* @lean_unsigned_to_nat(i64 0), !dbg !35
  br label %13, !dbg !36

12:                                               ; preds = %9
  br label %13, !dbg !37

13:                                               ; preds = %12, %10
  %14 = phi i8* [ undef, %12 ], [ %11, %10 ]
  br label %15, !dbg !38

15:                                               ; preds = %13
  br label %16, !dbg !39

16:                                               ; preds = %15, %5
  %17 = phi i8* [ %14, %15 ], [ %8, %5 ]
  br label %18, !dbg !40

18:                                               ; preds = %16
  ret i8* %17, !dbg !41
}

mutualrec.lean

--  RUN: ./run-lean.sh %s | FileCheck %s --check-prefix=CHECK-INTERPRET

--- CHECK-INTERPRET: 1
--- CHECK-INTERPRET: 0
--- CHECK-INTERPRET: 1
--- CHECK-INTERPRET: 0

-- RUN: lean %s 2>&1 | hask-opt  --lz-canonicalize  --lean-lower --convert-scf-to-std --ptr-lower | mlir-translate --mlir-to-llvmir |  opt -O3 -S | FileCheck %s --check-prefix=CHECK-LLVM

-- | todo: make this a better regex based match.
-- CHECK-LLVM: define i8* @l_even(i8* %0) local_unnamed_addr !dbg !3 {
-- CHECK-LLVM: tailrecurse
-- CHECK-LLVM: l_odd.exit
-- CHECK-LLVM: }


-- TODO: why is a join point created?
-- func @l_even(%arg0: !lz.value) -> !lz.value {
--   %0 = call @l_odd(%arg0) : (!lz.value) -> !lz.value
--   lz.return %0 : !lz.value
-- }
-- func @l_odd(%arg0: !lz.value) -> !lz.value {
--   %0 = call @l_even(%arg0) : (!lz.value) -> !lz.value
--   lz.return %0 : !lz.value
-- }

set_option trace.compiler.ir.init true

mutual 
  partial def even (a : Nat) : Nat := if a == 0 then 1 else odd (a - 1)
  partial def odd (a : Nat) : Nat := if a == 0 then 0 else even (a - 1)
end

-- | This example is not so interesting because dead code elimination gets rid of the work.
def main (xs: List String) : IO Unit := do
   IO.println (even 0)
   IO.println (even 1)
   IO.println (even 2)
   IO.println (even 3)

mutualrec.mlir

module  {
  func private @lean_unbox_float(!lz.value) -> f64
  func private @lean_io_mk_world() -> !lz.value
  func private @lean_dec_ref(!lz.value)
  func private @lean_box(i64) -> !lz.value
  func private @lean_io_result_mk_ok(!lz.value) -> !lz.value
  func private @lean_mark_persistent(!lz.value)
  func private @lean_string_push(!lz.value, i32) -> !lz.value
  "ptr.global"() {type = !lz.value, value = @l_main___closed__2} : () -> ()
  "ptr.global"() {type = !lz.value, value = @l_main___closed__3} : () -> ()
  "ptr.global"() {type = !lz.value, value = @l_main___closed__4} : () -> ()
  func private @lean_nat_dec_eq(!lz.value, !lz.value) -> i8
  func private @lean_nat_sub(!lz.value, !lz.value) -> !lz.value
  func private @l_IO_print___at_IO_println___spec__1(!lz.value, !lz.value) -> !lz.value
  "ptr.global"() {type = !lz.value, value = @l_main___closed__1} : () -> ()
  func private @l_Nat_repr(!lz.value) -> !lz.value
  func @l_even(%arg0: !lz.value) -> !lz.value {
    %0 = "lz.int"() {value = 0 : i64} : () -> !lz.value
    %1 = call @lean_nat_dec_eq(%arg0, %0) : (!lz.value, !lz.value) -> i8
    "lz.caseIntRet"(%1) ( {
      %2 = "lz.int"() {value = 1 : i64} : () -> !lz.value
      %3 = call @lean_nat_sub(%arg0, %2) : (!lz.value, !lz.value) -> !lz.value
      %4 = call @l_odd(%3) : (!lz.value) -> !lz.value
      lz.return %4 : !lz.value
    },  {
      %2 = "lz.int"() {value = 1 : i64} : () -> !lz.value
      lz.return %2 : !lz.value
    }) {alt0 = 0 : i64, alt1 = 1 : i64} : (i8) -> ()
  }
  func @l_odd(%arg0: !lz.value) -> !lz.value {
    %0 = "lz.int"() {value = 0 : i64} : () -> !lz.value
    %1 = call @lean_nat_dec_eq(%arg0, %0) : (!lz.value, !lz.value) -> i8
    "lz.caseIntRet"(%1) ( {
      %2 = "lz.int"() {value = 1 : i64} : () -> !lz.value
      %3 = call @lean_nat_sub(%arg0, %2) : (!lz.value, !lz.value) -> !lz.value
      %4 = call @l_even(%3) : (!lz.value) -> !lz.value
      lz.return %4 : !lz.value
    },  {
      %2 = "lz.int"() {value = 0 : i64} : () -> !lz.value
      lz.return %2 : !lz.value
    }) {alt0 = 0 : i64, alt1 = 1 : i64} : (i8) -> ()
  }
  func @l_IO_println___at_main___spec__1(%arg0: !lz.value, %arg1: !lz.value) -> !lz.value {
    %0 = call @l_Nat_repr(%arg0) : (!lz.value) -> !lz.value
    %c10_i32 = constant 10 : i32
    %1 = call @lean_string_push(%0, %c10_i32) : (!lz.value, i32) -> !lz.value
    %2 = call @l_IO_print___at_IO_println___spec__1(%1, %arg1) : (!lz.value, !lz.value) -> !lz.value
    lz.return %2 : !lz.value
  }
  func @_init_l_main___closed__1() -> !lz.value {
    %0 = "lz.int"() {value = 0 : i64} : () -> !lz.value
    %1 = call @l_even(%0) : (!lz.value) -> !lz.value
    lz.return %1 : !lz.value
  }
  func @_init_l_main___closed__2() -> !lz.value {
    %0 = "lz.int"() {value = 1 : i64} : () -> !lz.value
    %1 = call @l_even(%0) : (!lz.value) -> !lz.value
    lz.return %1 : !lz.value
  }
  func @_init_l_main___closed__3() -> !lz.value {
    %0 = "lz.int"() {value = 2 : i64} : () -> !lz.value
    %1 = call @l_even(%0) : (!lz.value) -> !lz.value
    lz.return %1 : !lz.value
  }
  func @_init_l_main___closed__4() -> !lz.value {
    %0 = "lz.int"() {value = 3 : i64} : () -> !lz.value
    %1 = call @l_even(%0) : (!lz.value) -> !lz.value
    lz.return %1 : !lz.value
  }
  func @main_lean_custom_entrypoint_hack(%arg0: !lz.value, %arg1: !lz.value) -> !lz.value {
    %0 = "ptr.loadglobal"() {value = @l_main___closed__1} : () -> !lz.value
    %1 = call @l_IO_println___at_main___spec__1(%0, %arg1) : (!lz.value, !lz.value) -> !lz.value
    "lz.caseRet"(%1) ( {
      %2 = "lz.project"(%1) {value = 1 : i64} : (!lz.value) -> !lz.value
      %3 = "ptr.loadglobal"() {value = @l_main___closed__2} : () -> !lz.value
      %4 = call @l_IO_println___at_main___spec__1(%3, %2) : (!lz.value, !lz.value) -> !lz.value
      "lz.caseRet"(%4) ( {
        %5 = "lz.project"(%4) {value = 1 : i64} : (!lz.value) -> !lz.value
        %6 = "ptr.loadglobal"() {value = @l_main___closed__3} : () -> !lz.value
        %7 = call @l_IO_println___at_main___spec__1(%6, %5) : (!lz.value, !lz.value) -> !lz.value
        "lz.caseRet"(%7) ( {
          %8 = "lz.project"(%7) {value = 1 : i64} : (!lz.value) -> !lz.value
          %9 = "ptr.loadglobal"() {value = @l_main___closed__4} : () -> !lz.value
          %10 = call @l_IO_println___at_main___spec__1(%9, %8) : (!lz.value, !lz.value) -> !lz.value
          lz.return %10 : !lz.value
        },  {
          %8 = "lz.project"(%7) {value = 0 : i64} : (!lz.value) -> !lz.value
          %9 = "lz.project"(%7) {value = 1 : i64} : (!lz.value) -> !lz.value
          %10 = "lz.construct"(%8, %9) {dataconstructor = @"1", size = 2 : i64} : (!lz.value, !lz.value) -> !lz.value
          lz.return %10 : !lz.value
        }) : (!lz.value) -> ()
      },  {
        %5 = "lz.project"(%4) {value = 0 : i64} : (!lz.value) -> !lz.value
        %6 = "lz.project"(%4) {value = 1 : i64} : (!lz.value) -> !lz.value
        %7 = "lz.construct"(%5, %6) {dataconstructor = @"1", size = 2 : i64} : (!lz.value, !lz.value) -> !lz.value
        lz.return %7 : !lz.value
      }) : (!lz.value) -> ()
    },  {
      %2 = "lz.project"(%1) {value = 0 : i64} : (!lz.value) -> !lz.value
      %3 = "lz.project"(%1) {value = 1 : i64} : (!lz.value) -> !lz.value
      %4 = "lz.construct"(%2, %3) {dataconstructor = @"1", size = 2 : i64} : (!lz.value, !lz.value) -> !lz.value
      lz.return %4 : !lz.value
    }) : (!lz.value) -> ()
  }
  func private @initialize_Init(!lz.value) -> !lz.value
  func private @init_lean_custom_entrypoint_hack(%arg0: !lz.value) -> !lz.value {
    %0 = call @lean_io_mk_world() : () -> !lz.value
    %1 = call @initialize_Init(%0) : (!lz.value) -> !lz.value
    call @lean_dec_ref(%1) : (!lz.value) -> ()
    %2 = call @_init_l_main___closed__1() : () -> !lz.value
    "ptr.storeglobal"(%2) {value = @l_main___closed__1} : (!lz.value) -> ()
    call @lean_mark_persistent(%2) : (!lz.value) -> ()
    %3 = call @_init_l_main___closed__2() : () -> !lz.value
    "ptr.storeglobal"(%3) {value = @l_main___closed__2} : (!lz.value) -> ()
    call @lean_mark_persistent(%3) : (!lz.value) -> ()
    %4 = call @_init_l_main___closed__3() : () -> !lz.value
    "ptr.storeglobal"(%4) {value = @l_main___closed__3} : (!lz.value) -> ()
    call @lean_mark_persistent(%4) : (!lz.value) -> ()
    %5 = call @_init_l_main___closed__4() : () -> !lz.value
    "ptr.storeglobal"(%5) {value = @l_main___closed__4} : (!lz.value) -> ()
    call @lean_mark_persistent(%5) : (!lz.value) -> ()
    %c0_i64 = constant 0 : i64
    %6 = call @lean_box(%c0_i64) : (i64) -> !lz.value
    %7 = call @lean_io_result_mk_ok(%6) : (!lz.value) -> !lz.value
    return %7 : !lz.value
  }
}

o3-ir.ll

define i8* @l_even(i8* %0) local_unnamed_addr !dbg !3 {
  %2 = tail call i8* @lean_unsigned_to_nat(i64 0), !dbg !7
  %3 = tail call i8 @lean_nat_dec_eq(i8* %0, i8* %2), !dbg !9
  %4 = icmp eq i8 %3, 0, !dbg !10
  br i1 %4, label %.lr.ph, label %l_odd.exit, !dbg !11

.lr.ph:                                           ; preds = %1, %tailrecurse
  %.tr1 = phi i8* [ %11, %tailrecurse ], [ %0, %1 ]
  %5 = tail call i8* @lean_unsigned_to_nat(i64 1), !dbg !12
  %6 = tail call i8* @lean_nat_sub(i8* %.tr1, i8* %5), !dbg !13
  %7 = tail call i8* @lean_unsigned_to_nat(i64 0), !dbg !14
  %8 = tail call i8 @lean_nat_dec_eq(i8* %6, i8* %7), !dbg !18
  %9 = icmp eq i8 %8, 0, !dbg !19
  br i1 %9, label %tailrecurse, label %l_odd.exit, !dbg !20

tailrecurse:                                      ; preds = %.lr.ph
  %10 = tail call i8* @lean_unsigned_to_nat(i64 1), !dbg !21
  %11 = tail call i8* @lean_nat_sub(i8* %6, i8* %10), !dbg !22
  %12 = tail call i8* @lean_unsigned_to_nat(i64 0), !dbg !7
  %13 = tail call i8 @lean_nat_dec_eq(i8* %11, i8* %12), !dbg !9
  %14 = icmp eq i8 %13, 0, !dbg !10
  br i1 %14, label %.lr.ph, label %l_odd.exit, !dbg !11

l_odd.exit:                                       ; preds = %tailrecurse, %.lr.ph, %1
  %.sink = phi i64 [ 1, %1 ], [ 1, %tailrecurse ], [ 0, %.lr.ph ]
  %15 = tail call i8* @lean_unsigned_to_nat(i64 %.sink), !dbg !23
  ret i8* %15, !dbg !24
}

define i8* @l_odd(i8* %0) local_unnamed_addr !dbg !16 {
  %2 = tail call i8* @lean_unsigned_to_nat(i64 0), !dbg !25
  %3 = tail call i8 @lean_nat_dec_eq(i8* %0, i8* %2), !dbg !26
  %4 = icmp eq i8 %3, 0, !dbg !27
  br i1 %4, label %5, label %9, !dbg !28

5:                                                ; preds = %1
  %6 = tail call i8* @lean_unsigned_to_nat(i64 1), !dbg !29
  %7 = tail call i8* @lean_nat_sub(i8* %0, i8* %6), !dbg !30
  %8 = tail call i8* @l_even(i8* %7), !dbg !31
  br label %11, !dbg !32

9:                                                ; preds = %1
  %10 = tail call i8* @lean_unsigned_to_nat(i64 0), !dbg !33
  br label %11, !dbg !34

11:                                               ; preds = %5, %9
  %12 = phi i8* [ %10, %9 ], [ %8, %5 ]
  ret i8* %12, !dbg !35
}