feat: persistent borrows

src/Lean/Compiler/LCNF/Basic.lean

@@ -342,6 +342,11 @@ def LetValue.toExpr (e : LetValue pu) : Expr :=
   | .unbox var _ => mkApp (.const `unbox []) (.fvar var)
   | .isShared fvarId _ => mkApp (.const `isShared []) (.fvar fvarId)
 
+def LetValue.isPersistent (val : LetValue .impure) : Bool :=
+  match val with
+  | .fap _ xs => xs.isEmpty -- all global constants are persistent
+  | _ => false
+
 structure LetDecl (pu : Purity) where
   fvarId : FVarId
   binderName : Name

src/Lean/Compiler/LCNF/ExplicitRC.lean

@@ -235,11 +235,6 @@ def withParams (ps : Array (Param .impure)) (x : RcM α) : RcM α := do
       { ctx with idx := ctx.idx + 1, varMap }
   withReader update x
 
-def LetValue.isPersistent (val : LetValue .impure) : Bool :=
-  match val with
-  | .fap _ xs => xs.isEmpty -- all global constants are persistent
-  | _ => false
-
 @[inline]
 def withLetDecl (decl : LetDecl .impure) (x : RcM α) : RcM α := do
   let update := fun ctx =>

src/Lean/Compiler/LCNF/InferBorrow.lean

@@ -390,9 +390,12 @@ where
       if let .fvar parent := args[1]! then
         if ← isOwned parent then ownFVar z (.forwardProjectionProp z)
     | .fap f args =>
-      let ps ← getParamInfo (.decl f)
-      ownFVar z (.functionCallResult z)
-      ownArgsUsingParams args ps (.functionCallArg z)
+      -- Constants remain alive at least until the end of execution and can thus effectively be seen
+      -- as a "borrowed" read.
+      if args.size > 0 then
+        let ps ← getParamInfo (.decl f)
+        ownFVar z (.functionCallResult z)
+        ownArgsUsingParams args ps (.functionCallArg z)
     | .fvar x args =>
       ownFVar z (.functionCallResult z); ownFVar x (.fvarCall z); ownArgs (.fvarCall z) args
     | .pap _ args => ownFVar z (.functionCallResult z); ownArgs (.partialApplication z) args

src/Lean/Compiler/LCNF/PropagateBorrow.lean

@@ -121,7 +121,10 @@ where
       if let .fvar parent := args[1]! then
         let parentVal ← getOwnedness parent
         join z parentVal
-    | .ctor .. | .fap .. | .fvar .. | .pap .. | .sproj .. | .uproj .. | .erased .. | .lit .. =>
+    | .fap _ args =>
+      let value := if args.isEmpty then .borrow else .own
+      join z value
+    | .ctor .. | .fvar .. | .pap .. | .sproj .. | .uproj .. | .erased .. | .lit .. =>
       join z .own
     | _ => unreachable!
 

tests/elab/compile_borrowed_reset_jp.lean

@@ -86,7 +86,6 @@ def testWithoutAnnotation (n : Nat) (p q : Prod Nat Nat) : Prod Nat Nat :=
 trace: [Compiler.inferBorrow] own _x.28: result of ctor call _x.28
 [Compiler.inferBorrow] own _x.30: result of ctor call _x.30
 [Compiler.inferBorrow] own n: argument to constructor call _x.30
-[Compiler.inferBorrow] own _x.29: result of function call _x.29
 [Compiler.inferBorrow] size: 2
     def testArrayWithAnnotation._closed_0 : obj :=
       let _x.1 := 0;
@@ -112,7 +111,6 @@ trace: [Compiler.inferBorrow] own _x.28: used in reset reuse _x.28
 [Compiler.inferBorrow] own n: argument to constructor call _x.28
 [Compiler.inferBorrow] own pair: used in reset reuse _x.29
 [Compiler.inferBorrow] own snd: fwd projection propagation snd
-[Compiler.inferBorrow] own _x.27: result of function call _x.27
 [Compiler.inferBorrow] size: 5
     def testArrayWithoutAnnotation n @&ps : obj :=
       let _x.1 := testArrayWithAnnotation._closed_0;
@@ -164,3 +162,48 @@ set_option trace.Compiler.inferBorrow true in
 def testArrayWithAnnotation'' (n : USize) (ps : @&Array (Nat × Nat)) : Nat × Nat :=
   let pair := ps[n]'sorry
   { pair with fst := n.toNat }
+
+
+def arrayConst : Array Nat := #[1,2,3,4]
+
+/--
+trace: [Compiler.inferBorrow] own y: result of function call y
+[Compiler.inferBorrow] own y: result of function call y
+[Compiler.inferBorrow] own y: result of function call y
+[Compiler.inferBorrow] own y: result of function call y
+[Compiler.inferBorrow] own y: result of function call y
+[Compiler.inferBorrow] own isZero: result of function call isZero
+[Compiler.inferBorrow] size: 15
+    def arrayConstReader @&x @&y @&ys : tobj :=
+      let _x.1 := 0;
+      jp _jp.2 @&_y.3 : tobj :=
+        let _x.4 := 1;
+        let y := Nat.add y _x.4;
+        let y := Nat.add y _x.4;
+        let y := Nat.add y _x.4;
+        let y := Nat.add y _x.4;
+        let y := Nat.add y _x.4;
+        let _x.5 := Array.get!Internal ◾ _x.1 _y.3 y;
+        return _x.5;
+      let isZero := Nat.decEq x _x.1;
+      cases isZero : tobj
+      | Bool.true =>
+        let _x.6 := arrayConst;
+        goto _jp.2 _x.6
+      | Bool.false =>
+        goto _jp.2 ys
+-/
+#guard_msgs in
+set_option trace.Compiler.inferBorrow true in
+def arrayConstReader (x y : Nat) (ys : @Array Nat) : Nat :=
+  let arr :=
+    match x with
+    | 0 => arrayConst
+    | _ + 1 => ys
+  let y := y + 1
+  let y := y + 1
+  let y := y + 1
+  let y := y + 1
+  let y := y + 1
+  arr[y]!
+