diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean index 2dad82a0ebd9..8ca5425982d2 100644 --- a/src/Init/Prelude.lean +++ b/src/Init/Prelude.lean @@ -3673,7 +3673,7 @@ def panic {α : Sort u} [Inhabited α] (msg : String) : α := panicCore msg -- TODO: this be applied directly to `Inhabited`'s definition when we remove the above workaround -attribute [nospecialize] Inhabited +attribute [weak_specialize] Inhabited /-- The `>>=` operator is overloaded via instances of `bind`. diff --git a/src/Lean/Compiler/LCNF/ExplicitRC.lean b/src/Lean/Compiler/LCNF/ExplicitRC.lean index 01af8cf8e550..e37bda71fc8e 100644 --- a/src/Lean/Compiler/LCNF/ExplicitRC.lean +++ b/src/Lean/Compiler/LCNF/ExplicitRC.lean @@ -31,9 +31,12 @@ namespace Lean.Compiler.LCNF open ImpureType /-! -The following section contains the derived value analysis. It figures out a dependency tree of +The following section contains the derived value analysis. It figures out a dependency graph of values that were derived from other values through projections or `Array` accesses. This information is later used in the derived borrow analysis to reduce reference counting pressure. + +When a derived value has more than one parent, it is derived from one of the parent values but we +cannot statically determine which one. -/ /-- @@ -41,10 +44,10 @@ Contains information about values derived through various forms of projection fr -/ structure DerivedValInfo where /-- - The variable this value was derived from. This is always set except for parameters as they have no - value to be derived from. + The set of variables this value may derive from. This is always set except for parameters as they + have no value to be derived from. -/ - parent? : Option FVarId + parents : Array FVarId /-- The set of variables that were derived from this value. -/ @@ -56,59 +59,75 @@ abbrev DerivedValMap := Std.HashMap FVarId DerivedValInfo namespace CollectDerivedValInfo structure State where + /-- + The dependency graph of values. + -/ varMap : DerivedValMap := {} - borrowedParams : FVarIdHashSet := {} + /-- + The set of values that are to be interpreted as being borrowed by nature. This currently includes: + - borrowed parameters + - variables that are initialized from constants + -/ + borrowedValues : FVarIdHashSet := {} abbrev M := StateRefT State CompilerM @[inline] -def visitParam (p : Param .impure) : M Unit := +def addDerivedValue (parents : Array FVarId) (child : FVarId) : M Unit := do modify fun s => { s with - varMap := s.varMap.insert p.fvarId { - parent? := none - children := {} - } - borrowedParams := - if p.borrow && p.type.isPossibleRef then - s.borrowedParams.insert p.fvarId - else - s.borrowedParams + varMap := + let varMap := parents.foldl (init := s.varMap) + (·.modify · (fun info => { info with children := info.children.insert child })) + varMap.insert child { parents := parents, children := {} } } @[inline] -def addDerivedValue (parent : FVarId) (child : FVarId) : M Unit := do - modify fun s => { s with - varMap := - s.varMap - |>.modify parent (fun info => { info with children := info.children.insert child }) - |>.insert child { parent? := some parent, children := {} } - } +def addBorrowedValue (fvarId : FVarId) : M Unit := do + modify fun s => { s with borrowedValues := s.borrowedValues.insert fvarId } -def removeFromParent (child : FVarId) : M Unit := do - if let some parent := (← get).varMap.get? child |>.bind (·.parent?) then - modify fun s => { s with - varMap := s.varMap.modify parent fun info => - { info with children := info.children.erase child } - } +@[inline] +def visitParam (p : Param .impure) : M Unit := do + addDerivedValue #[] p.fvarId + if p.borrow && p.type.isPossibleRef then + addBorrowedValue p.fvarId + +def removeFromParents (child : FVarId) : M Unit := do + if let some entry := (← get).varMap.get? child then + for parent in entry.parents do + modify fun s => { s with + varMap := s.varMap.modify parent fun info => + { info with children := info.children.erase child } + } partial def collectCode (code : Code .impure) : M Unit := do match code with | .let decl k => match decl.value with | .oproj _ parent => - addDerivedValue parent decl.fvarId + addDerivedValue #[parent] decl.fvarId -- Keep in sync with PropagateBorrow, InferBorrow | .fap ``Array.getInternal args => if let .fvar parent := args[1]! then - addDerivedValue parent decl.fvarId + addDerivedValue #[parent] decl.fvarId | .fap ``Array.get!Internal args => + let mut parents := #[] + /- + Because execution may continue after a panic, the value resulting from a get!InternalBorrowed + may be derived from either the `Inhabited` instance or the `Array` argument. + -/ + if let .fvar parent := args[1]! then + parents := parents.push parent if let .fvar parent := args[2]! then - addDerivedValue parent decl.fvarId + parents := parents.push parent + addDerivedValue parents decl.fvarId | .fap ``Array.uget args => if let .fvar parent := args[1]! then - addDerivedValue parent decl.fvarId + addDerivedValue #[parent] decl.fvarId + | .fap _ #[] => + addDerivedValue #[] decl.fvarId + addBorrowedValue decl.fvarId | .reset _ target => - removeFromParent target + removeFromParents target | _ => pure () collectCode k | .jp decl k => @@ -125,8 +144,8 @@ Collect the derived value tree as well as the set of parameters that take object -/ def collect (ps : Array (Param .impure)) (code : Code .impure) : CompilerM (DerivedValMap × FVarIdHashSet) := do - let ⟨_, { varMap, borrowedParams }⟩ ← go |>.run {} - return ⟨varMap, borrowedParams⟩ + let ⟨_, { varMap, borrowedValues }⟩ ← go |>.run {} + return ⟨varMap, borrowedValues⟩ where go : M Unit := do ps.forM visitParam @@ -170,13 +189,21 @@ def LiveVars.erase (liveVars : LiveVars) (fvarId : FVarId) : LiveVars := let borrows := liveVars.borrows.erase fvarId { vars, borrows } +@[inline] +def LiveVars.insertBorrow (liveVars : LiveVars) (fvarId : FVarId) : LiveVars := + { liveVars with borrows := liveVars.borrows.insert fvarId } + +@[inline] +def LiveVars.insertLive (liveVars : LiveVars) (fvarId : FVarId) : LiveVars := + { liveVars with vars := liveVars.vars.insert fvarId } + abbrev JPLiveVarMap := FVarIdMap LiveVars structure Context where /-- - The set of all parameters that are borrowed and take potential objects as arguments. + The set of all values that are borrowed and potentially objects -/ - borrowedParams : FVarIdHashSet + borrowedValues : FVarIdHashSet /-- The derived value tree. -/ @@ -277,18 +304,21 @@ def withCollectLiveVars (x : RcM α) : RcM (α × LiveVars) := do return (ret, collected) /-- -Traverse the transitive closure of values derived from `fvarId` and add them to `s` if they pass -`shouldAdd`. +Traverse the transitive closure of values derived from `fvarId` and add them to `s` if: +- they pass `shouldAdd`. +- all their parents are accessible -/ @[specialize] -partial def addDescendants (fvarId : FVarId) (derivedValMap : DerivedValMap) (s : FVarIdHashSet) - (shouldAdd : FVarId → Bool := fun _ => true) : FVarIdHashSet := +partial def addDescendants (fvarId : FVarId) (derivedValMap : DerivedValMap) (liveVars : LiveVars) + (shouldAdd : FVarId → Bool := fun _ => true) : LiveVars := if let some info := derivedValMap.get? fvarId then - info.children.fold (init := s) fun s child => - let s := if shouldAdd child then s.insert child else s - addDescendants child derivedValMap s shouldAdd + info.children.fold (init := liveVars) fun liveVars child => + let cinfo := derivedValMap.get! child + let parentsOk := cinfo.parents.all fun fvarId => (liveVars.vars.contains fvarId || liveVars.borrows.contains fvarId) + let liveVars := if parentsOk && shouldAdd child then liveVars.insertBorrow child else liveVars + addDescendants child derivedValMap liveVars shouldAdd else - s + liveVars /-- Mark `fvarId` as live from here on out and if there are any derived values that are not live anymore @@ -299,20 +329,21 @@ alive after all). def useVar (fvarId : FVarId) (shouldBorrow : FVarId → Bool := fun _ => true) : RcM Unit := do if !(← isLive fvarId) then let derivedValMap := (← read).derivedValMap + modifyLive fun liveVars => { liveVars with vars := liveVars.vars.insert fvarId } modifyLive fun liveVars => - { liveVars with - borrows := addDescendants fvarId derivedValMap liveVars.borrows fun y => - !liveVars.vars.contains y && shouldBorrow y - vars := liveVars.vars.insert fvarId - } + addDescendants fvarId derivedValMap liveVars fun y => + !liveVars.vars.contains y && shouldBorrow y def useArgs (args : Array (Arg .impure)) : RcM Unit := do args.forM fun arg => match arg with | .fvar fvarId => useVar fvarId fun y => - -- If a value is used as an argument we are going to mark it live anyways so don't mark it - -- as borrowed. + /- + If we are in a situation like `f x y` where `x` would imply that `y` remains borrowed we are + going to mark `y` as being live instead of borrowed later on anyways. Instead we skip this + intermediate state and don't even begin to consider it as borrowed. + -/ args.all fun arg => match arg with | .fvar z => y != z @@ -341,9 +372,9 @@ def setRetLiveVars : RcM Unit := do let derivedValMap := (← read).derivedValMap -- At the end of a function no values are live and all borrows derived from parameters will still -- be around. - let borrows := (← read).borrowedParams.fold (init := {}) fun borrows x => - addDescendants x derivedValMap (borrows.insert x) - modifyLive fun _ => { vars := {}, borrows } + let liveVars := (← read).borrowedValues.fold (init := {}) fun liveVars x => + addDescendants x derivedValMap (liveVars.insertBorrow x) + modifyLive (fun _ => liveVars) @[inline] def addInc (fvarId : FVarId) (k : Code .impure) (n : Nat := 1) : RcM (Code .impure) := do @@ -625,9 +656,9 @@ partial def Code.explicitRc (code : Code .impure) : RcM (Code .impure) := do def Decl.explicitRc (decl : Decl .impure) : CompilerM (Decl .impure) := do let value ← decl.value.mapCodeM fun code => do - let ⟨derivedValMap, borrowedParams⟩ ← CollectDerivedValInfo.collect decl.params code + let ⟨derivedValMap, borrowedValues⟩ ← CollectDerivedValInfo.collect decl.params code go code |>.run { - borrowedParams, + borrowedValues, derivedValMap, } |>.run' {} return { decl with value } diff --git a/src/Lean/Compiler/LCNF/InferBorrow.lean b/src/Lean/Compiler/LCNF/InferBorrow.lean index 3bba71d6dd77..7dc7841a15c2 100644 --- a/src/Lean/Compiler/LCNF/InferBorrow.lean +++ b/src/Lean/Compiler/LCNF/InferBorrow.lean @@ -384,6 +384,8 @@ where if let .fvar parent := args[1]! then if ← isOwned parent then ownFVar z (.forwardProjectionProp z) | .fap ``Array.get!Internal args => + if let .fvar parent := args[1]! then + if ← isOwned parent then ownFVar z (.forwardProjectionProp z) if let .fvar parent := args[2]! then if ← isOwned parent then ownFVar z (.forwardProjectionProp z) | .fap ``Array.uget args => diff --git a/src/Lean/Compiler/LCNF/PropagateBorrow.lean b/src/Lean/Compiler/LCNF/PropagateBorrow.lean index 11ac5ea7dfd0..bed5f5f49109 100644 --- a/src/Lean/Compiler/LCNF/PropagateBorrow.lean +++ b/src/Lean/Compiler/LCNF/PropagateBorrow.lean @@ -114,6 +114,9 @@ where let parentVal ← getOwnedness parent join z parentVal | .fap ``Array.get!Internal args => + if let .fvar parent := args[1]! then + let parentVal ← getOwnedness parent + join z parentVal if let .fvar parent := args[2]! then let parentVal ← getOwnedness parent join z parentVal diff --git a/src/Lean/Compiler/LCNF/SimpleGroundExpr.lean b/src/Lean/Compiler/LCNF/SimpleGroundExpr.lean index 2c45eb26e7e1..8a4553ccb615 100644 --- a/src/Lean/Compiler/LCNF/SimpleGroundExpr.lean +++ b/src/Lean/Compiler/LCNF/SimpleGroundExpr.lean @@ -178,10 +178,11 @@ partial def compileToSimpleGroundExpr (code : Code .impure) : CompilerM (Option where go (code : Code .impure) : DetectM SimpleGroundExpr := do match code with - | .let decl (.return fvarId) => + | .let decl (.return fvarId) | .let decl (.inc _ _ _ true (.return fvarId)) => guard <| decl.fvarId == fvarId compileFinalLet decl.value | .let decl k => compileNonFinalLet decl k + | .inc (persistent := true) (k := k) .. => go k | _ => failure @[inline] diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h index e44444704908..b4202aa74af4 100644 --- a/stage0/src/stdlib_flags.h +++ b/stage0/src/stdlib_flags.h @@ -11,7 +11,7 @@ options get_default_options() { opts = opts.update({"debug", "terminalTacticsAsSorry"}, false); // switch to `true` for ABI-breaking changes affecting meta code; // see also next option! - opts = opts.update({"interpreter", "prefer_native"}, false); + opts = opts.update({"interpreter", "prefer_native"}, true); // switch to `false` when enabling `prefer_native` should also affect use // of built-in parsers in quotations; this is usually the case, but setting // both to `true` may be necessary for handling non-builtin parsers with diff --git a/tests/elab/9806.lean.out.expected b/tests/elab/9806.lean.out.expected index b7c1e770af61..540423bdc435 100644 --- a/tests/elab/9806.lean.out.expected +++ b/tests/elab/9806.lean.out.expected @@ -4,7 +4,8 @@ true let _x.1 := 1; let _x.2 := Bool.repr._redArg _x.1; return _x.2 -[Compiler.result] size: 1 +[Compiler.result] size: 2 def _private.elab.«9806».0._eval : tobj := let _x.1 := _private.elab.«9806».0._eval._closed_0; + inc[persistent] _x.1; return _x.1 diff --git a/tests/elab/Reparen.lean.out.expected b/tests/elab/Reparen.lean.out.expected index c4c49bc1aacb..0d9b46c6ac45 100644 --- a/tests/elab/Reparen.lean.out.expected +++ b/tests/elab/Reparen.lean.out.expected @@ -3619,7 +3619,7 @@ def panic {α : Sort u} [Inhabited α] (msg : String) : α := panicCore msg -- TODO: this be applied directly to `Inhabited`'s definition when we remove the above workaround -attribute [nospecialize] Inhabited +attribute [weak_specialize] Inhabited /-- The `>>=` operator is overloaded via instances of `bind`. diff --git a/tests/elab/boxing_bug.lean b/tests/elab/boxing_bug.lean index 08171a49f63c..9f7749c81226 100644 --- a/tests/elab/boxing_bug.lean +++ b/tests/elab/boxing_bug.lean @@ -23,6 +23,7 @@ trace: [Compiler.IR] [result] ret x_1 def instSemiringUInt8 : obj := let x_1 : obj := instSemiringUInt8._closed_0; + inc x_1; ret x_1 -/ #guard_msgs in diff --git a/tests/elab/compile_multi_panic.lean b/tests/elab/compile_multi_panic.lean index 78dd88e12e15..5a107c2b40db 100644 --- a/tests/elab/compile_multi_panic.lean +++ b/tests/elab/compile_multi_panic.lean @@ -3,19 +3,19 @@ module public section + /-- trace: [Compiler.explicitRc] size: 1 def test1._closed_0 : obj := let _x.1 := ""; return _x.1 -[Compiler.explicitRc] size: 8 +[Compiler.explicitRc] size: 7 def test1 @&xs : obj := let _x.1 := test1._closed_0; let _x.2 := 0; let _x.3 := Array.get!InternalBorrowed ◾ _x.1 xs _x.2; let _x.4 := 1; let _x.5 := Array.get!InternalBorrowed ◾ _x.1 xs _x.4; - dec[persistent][ref] _x.1; inc _x.3; let _x.6 := String.append _x.3 _x.5; return _x.6 @@ -77,7 +77,7 @@ trace: [Compiler.explicitRc] size: 4 dec[ref] xs; let r := box res; return r -[Compiler.explicitRc] size: 23 +[Compiler.explicitRc] size: 21 def test3 @&xs : obj := let _x.1 := test1._closed_0; jp _jp.2 _y.3 : obj := @@ -86,12 +86,10 @@ trace: [Compiler.explicitRc] size: 4 cases _x.5 : obj | Bool.false => let _x.6 := outOfBounds._redArg _x.1; - dec[persistent][ref] _x.1; let _x.7 := String.append _y.3 _x.6; dec _x.6; return _x.7 | Bool.true => - dec[persistent][ref] _x.1; let _x.8 := Array.ugetBorrowed ◾ xs _x.4 ◾; let _x.9 := String.append _y.3 _x.8; return _x.9; diff --git a/tests/elab/compile_recursive_array_access.lean b/tests/elab/compile_recursive_array_access.lean index 222ea307ff74..338cfa317c55 100644 --- a/tests/elab/compile_recursive_array_access.lean +++ b/tests/elab/compile_recursive_array_access.lean @@ -10,7 +10,7 @@ inductive NAryTree where deriving Inhabited /-- -trace: [Compiler.explicitRc] size: 20 +trace: [Compiler.explicitRc] size: 21 def followPath @&tree @&path : obj := cases tree : obj | NAryTree.tip => @@ -21,6 +21,7 @@ trace: [Compiler.explicitRc] size: 20 return x.1 | _ => let _x.2 := instInhabitedNAryTree.default._closed_0; + inc[persistent][ref] _x.2; return _x.2 | NAryTree.node => cases path : obj @@ -30,11 +31,11 @@ trace: [Compiler.explicitRc] size: 20 let tail.5 := oproj[1] path; let _x.6 := instInhabitedNAryTree.default; let _x.7 := Array.get!InternalBorrowed ◾ _x.6 ys.3 head.4; - dec[persistent][ref] _x.6; let _x.8 := followPath _x.7 tail.5; return _x.8 | _ => let _x.9 := instInhabitedNAryTree.default._closed_0; + inc[persistent][ref] _x.9; return _x.9 [Compiler.explicitRc] size: 3 def followPath._boxed tree path : obj := diff --git a/tests/elab/computedFieldsCode.lean.out.expected b/tests/elab/computedFieldsCode.lean.out.expected index ccdea68d89a0..949e62f708e8 100644 --- a/tests/elab/computedFieldsCode.lean.out.expected +++ b/tests/elab/computedFieldsCode.lean.out.expected @@ -281,12 +281,12 @@ def f._closed_1 : tobj := let x_1 : tagged := ctor_5[Exp.a4._impl]; let x_2 : tobj := f._closed_0; + inc x_2; let x_3 : tobj := Exp.app._override x_2 x_1; ret x_3 def f._closed_2 : u64 := let x_1 : tobj := f._closed_1; let x_2 : u64 := Exp.hash._override x_1; - dec x_1; ret x_2 def f : u64 := let x_1 : u64 := f._closed_2; diff --git a/tests/elab/ctorMixedRelevance.lean b/tests/elab/ctorMixedRelevance.lean index fdf2f9edaf90..8f1c326768fe 100644 --- a/tests/elab/ctorMixedRelevance.lean +++ b/tests/elab/ctorMixedRelevance.lean @@ -15,6 +15,7 @@ trace: [Compiler.IR] [result] ret x_1 def test1 : obj := let x_1 : obj := test1._closed_0; + inc x_1; ret x_1 -/ #guard_msgs in @@ -32,6 +33,7 @@ trace: [Compiler.IR] [result] ret x_5 def test2 : obj := let x_1 : obj := test2._closed_0; + inc x_1; ret x_1 -/ #guard_msgs in diff --git a/tests/elab/extractClosed.lean b/tests/elab/extractClosed.lean index c38a9f255e08..27174bc670f1 100644 --- a/tests/elab/extractClosed.lean +++ b/tests/elab/extractClosed.lean @@ -7,6 +7,7 @@ trace: [Compiler.IR] [result] ret x_3 def f : obj := let x_1 : obj := f._closed_0; + inc x_1; ret x_1 -/ #guard_msgs in diff --git a/tests/elab/simple_ground_extraction.lean b/tests/elab/simple_ground_extraction.lean index 9445ba69803b..a79f7c791efe 100644 --- a/tests/elab/simple_ground_extraction.lean +++ b/tests/elab/simple_ground_extraction.lean @@ -9,9 +9,10 @@ trace: [Compiler.simpleGround] Marked stringTest1._closed_0 as simple ground exp def stringTest1._closed_0 : obj := let _x.1 := "literal"; return _x.1 -[Compiler.saveImpure] size: 1 +[Compiler.saveImpure] size: 2 def stringTest1 : obj := let _x.1 := stringTest1._closed_0; + inc[persistent][ref] _x.1; return _x.1 -/ #guard_msgs in @@ -39,27 +40,33 @@ trace: [Compiler.simpleGround] Marked stringTest2._closed_0 as simple ground exp def stringTest2._closed_2 : obj := let _x.1 := "C"; return _x.1 -[Compiler.saveImpure] size: 3 +[Compiler.saveImpure] size: 4 def stringTest2._closed_3 : tobj := let _x.1 := ctor_0[List.nil]; let _x.2 := stringTest2._closed_2; + inc[persistent][ref] _x.2; let _x.3 := ctor_1[List.cons] _x.2 _x.1; return _x.3 -[Compiler.saveImpure] size: 3 +[Compiler.saveImpure] size: 5 def stringTest2._closed_4 : tobj := let _x.1 := stringTest2._closed_3; let _x.2 := stringTest2._closed_1; + inc[persistent] _x.1; + inc[persistent][ref] _x.2; let _x.3 := ctor_1[List.cons] _x.2 _x.1; return _x.3 -[Compiler.saveImpure] size: 3 +[Compiler.saveImpure] size: 5 def stringTest2._closed_5 : tobj := let _x.1 := stringTest2._closed_4; let _x.2 := stringTest2._closed_0; + inc[persistent] _x.1; + inc[persistent][ref] _x.2; let _x.3 := ctor_1[List.cons] _x.2 _x.1; return _x.3 -[Compiler.saveImpure] size: 1 +[Compiler.saveImpure] size: 2 def stringTest2 : tobj := let _x.1 := stringTest2._closed_5; + inc[persistent] _x.1; return _x.1 -/ #guard_msgs in @@ -72,14 +79,16 @@ open Lean /-- trace: [Compiler.simpleGround] Marked nameTest1._closed_0 as simple ground expr [Compiler.simpleGround] Marked nameTest1 as simple ground expr -[Compiler.saveImpure] size: 2 +[Compiler.saveImpure] size: 3 def nameTest1._closed_0 : tobj := let _x.1 := stringTest2._closed_0; + inc[persistent][ref] _x.1; let _x.2 := Lean.Name.mkStr1 _x.1; return _x.2 -[Compiler.saveImpure] size: 1 +[Compiler.saveImpure] size: 2 def nameTest1 : tobj := let _x.1 := nameTest1._closed_0; + inc[persistent] _x.1; return _x.1 -/ #guard_msgs in @@ -90,15 +99,18 @@ def nameTest1 : Name := `A /-- trace: [Compiler.simpleGround] Marked nameTest2._closed_0 as simple ground expr [Compiler.simpleGround] Marked nameTest2 as simple ground expr -[Compiler.saveImpure] size: 3 +[Compiler.saveImpure] size: 5 def nameTest2._closed_0 : tobj := let _x.1 := stringTest2._closed_1; let _x.2 := stringTest2._closed_0; + inc[persistent][ref] _x.1; + inc[persistent][ref] _x.2; let _x.3 := Lean.Name.mkStr2 _x.2 _x.1; return _x.3 -[Compiler.saveImpure] size: 1 +[Compiler.saveImpure] size: 2 def nameTest2 : tobj := let _x.1 := nameTest2._closed_0; + inc[persistent] _x.1; return _x.1 -/ #guard_msgs in @@ -109,16 +121,20 @@ def nameTest2 : Name := `A.B /-- trace: [Compiler.simpleGround] Marked nameTest3._closed_0 as simple ground expr [Compiler.simpleGround] Marked nameTest3 as simple ground expr -[Compiler.saveImpure] size: 4 +[Compiler.saveImpure] size: 7 def nameTest3._closed_0 : tobj := let _x.1 := stringTest2._closed_2; let _x.2 := stringTest2._closed_1; let _x.3 := stringTest2._closed_0; + inc[persistent][ref] _x.1; + inc[persistent][ref] _x.2; + inc[persistent][ref] _x.3; let _x.4 := Lean.Name.mkStr3 _x.3 _x.2 _x.1; return _x.4 -[Compiler.saveImpure] size: 1 +[Compiler.saveImpure] size: 2 def nameTest3 : tobj := let _x.1 := nameTest3._closed_0; + inc[persistent] _x.1; return _x.1 -/ #guard_msgs in @@ -134,17 +150,22 @@ trace: [Compiler.simpleGround] Marked nameTest4._closed_0 as simple ground expr def nameTest4._closed_0 : obj := let _x.1 := "D"; return _x.1 -[Compiler.saveImpure] size: 5 +[Compiler.saveImpure] size: 9 def nameTest4._closed_1 : tobj := let _x.1 := nameTest4._closed_0; let _x.2 := stringTest2._closed_2; let _x.3 := stringTest2._closed_1; let _x.4 := stringTest2._closed_0; + inc[persistent][ref] _x.1; + inc[persistent][ref] _x.2; + inc[persistent][ref] _x.3; + inc[persistent][ref] _x.4; let _x.5 := Lean.Name.mkStr4 _x.4 _x.3 _x.2 _x.1; return _x.5 -[Compiler.saveImpure] size: 1 +[Compiler.saveImpure] size: 2 def nameTest4 : tobj := let _x.1 := nameTest4._closed_1; + inc[persistent] _x.1; return _x.1 -/ #guard_msgs in @@ -160,18 +181,24 @@ trace: [Compiler.simpleGround] Marked nameTest5._closed_0 as simple ground expr def nameTest5._closed_0 : obj := let _x.1 := "E"; return _x.1 -[Compiler.saveImpure] size: 6 +[Compiler.saveImpure] size: 11 def nameTest5._closed_1 : tobj := let _x.1 := nameTest5._closed_0; let _x.2 := nameTest4._closed_0; let _x.3 := stringTest2._closed_2; let _x.4 := stringTest2._closed_1; let _x.5 := stringTest2._closed_0; + inc[persistent][ref] _x.1; + inc[persistent][ref] _x.2; + inc[persistent][ref] _x.3; + inc[persistent][ref] _x.4; + inc[persistent][ref] _x.5; let _x.6 := Lean.Name.mkStr5 _x.5 _x.4 _x.3 _x.2 _x.1; return _x.6 -[Compiler.saveImpure] size: 1 +[Compiler.saveImpure] size: 2 def nameTest5 : tobj := let _x.1 := nameTest5._closed_1; + inc[persistent] _x.1; return _x.1 -/ #guard_msgs in @@ -187,7 +214,7 @@ trace: [Compiler.simpleGround] Marked nameTest6._closed_0 as simple ground expr def nameTest6._closed_0 : obj := let _x.1 := "F"; return _x.1 -[Compiler.saveImpure] size: 7 +[Compiler.saveImpure] size: 13 def nameTest6._closed_1 : tobj := let _x.1 := nameTest6._closed_0; let _x.2 := nameTest5._closed_0; @@ -195,11 +222,18 @@ trace: [Compiler.simpleGround] Marked nameTest6._closed_0 as simple ground expr let _x.4 := stringTest2._closed_2; let _x.5 := stringTest2._closed_1; let _x.6 := stringTest2._closed_0; + inc[persistent][ref] _x.1; + inc[persistent][ref] _x.2; + inc[persistent][ref] _x.3; + inc[persistent][ref] _x.4; + inc[persistent][ref] _x.5; + inc[persistent][ref] _x.6; let _x.7 := Lean.Name.mkStr6 _x.6 _x.5 _x.4 _x.3 _x.2 _x.1; return _x.7 -[Compiler.saveImpure] size: 1 +[Compiler.saveImpure] size: 2 def nameTest6 : tobj := let _x.1 := nameTest6._closed_1; + inc[persistent] _x.1; return _x.1 -/ #guard_msgs in @@ -215,7 +249,7 @@ trace: [Compiler.simpleGround] Marked nameTest7._closed_0 as simple ground expr def nameTest7._closed_0 : obj := let _x.1 := "G"; return _x.1 -[Compiler.saveImpure] size: 8 +[Compiler.saveImpure] size: 15 def nameTest7._closed_1 : tobj := let _x.1 := nameTest7._closed_0; let _x.2 := nameTest6._closed_0; @@ -224,11 +258,19 @@ trace: [Compiler.simpleGround] Marked nameTest7._closed_0 as simple ground expr let _x.5 := stringTest2._closed_2; let _x.6 := stringTest2._closed_1; let _x.7 := stringTest2._closed_0; + inc[persistent][ref] _x.1; + inc[persistent][ref] _x.2; + inc[persistent][ref] _x.3; + inc[persistent][ref] _x.4; + inc[persistent][ref] _x.5; + inc[persistent][ref] _x.6; + inc[persistent][ref] _x.7; let _x.8 := Lean.Name.mkStr7 _x.7 _x.6 _x.5 _x.4 _x.3 _x.2 _x.1; return _x.8 -[Compiler.saveImpure] size: 1 +[Compiler.saveImpure] size: 2 def nameTest7 : tobj := let _x.1 := nameTest7._closed_1; + inc[persistent] _x.1; return _x.1 -/ #guard_msgs in @@ -244,7 +286,7 @@ trace: [Compiler.simpleGround] Marked nameTest8._closed_0 as simple ground expr def nameTest8._closed_0 : obj := let _x.1 := "H"; return _x.1 -[Compiler.saveImpure] size: 9 +[Compiler.saveImpure] size: 17 def nameTest8._closed_1 : tobj := let _x.1 := nameTest8._closed_0; let _x.2 := nameTest7._closed_0; @@ -254,11 +296,20 @@ trace: [Compiler.simpleGround] Marked nameTest8._closed_0 as simple ground expr let _x.6 := stringTest2._closed_2; let _x.7 := stringTest2._closed_1; let _x.8 := stringTest2._closed_0; + inc[persistent][ref] _x.1; + inc[persistent][ref] _x.2; + inc[persistent][ref] _x.3; + inc[persistent][ref] _x.4; + inc[persistent][ref] _x.5; + inc[persistent][ref] _x.6; + inc[persistent][ref] _x.7; + inc[persistent][ref] _x.8; let _x.9 := Lean.Name.mkStr8 _x.8 _x.7 _x.6 _x.5 _x.4 _x.3 _x.2 _x.1; return _x.9 -[Compiler.saveImpure] size: 1 +[Compiler.saveImpure] size: 2 def nameTest8 : tobj := let _x.1 := nameTest8._closed_1; + inc[persistent] _x.1; return _x.1 -/ #guard_msgs in @@ -278,67 +329,85 @@ trace: [Compiler.simpleGround] Marked nameTest9._closed_0 as simple ground expr [Compiler.simpleGround] Marked nameTest9._closed_8 as simple ground expr [Compiler.simpleGround] Marked nameTest9._closed_9 as simple ground expr [Compiler.simpleGround] Marked nameTest9 as simple ground expr -[Compiler.saveImpure] size: 3 +[Compiler.saveImpure] size: 4 def nameTest9._closed_0 : tobj := let _x.1 := stringTest2._closed_0; let _x.2 := ctor_0[Lean.Name.anonymous._impl]; + inc[persistent][ref] _x.1; let _x.3 := Lean.Name.str._override _x.2 _x.1; return _x.3 -[Compiler.saveImpure] size: 3 +[Compiler.saveImpure] size: 5 def nameTest9._closed_1 : tobj := let _x.1 := stringTest2._closed_1; let _x.2 := nameTest9._closed_0; + inc[persistent][ref] _x.1; + inc[persistent] _x.2; let _x.3 := Lean.Name.str._override _x.2 _x.1; return _x.3 -[Compiler.saveImpure] size: 3 +[Compiler.saveImpure] size: 5 def nameTest9._closed_2 : tobj := let _x.1 := stringTest2._closed_2; let _x.2 := nameTest9._closed_1; + inc[persistent][ref] _x.1; + inc[persistent] _x.2; let _x.3 := Lean.Name.str._override _x.2 _x.1; return _x.3 -[Compiler.saveImpure] size: 3 +[Compiler.saveImpure] size: 5 def nameTest9._closed_3 : tobj := let _x.1 := nameTest4._closed_0; let _x.2 := nameTest9._closed_2; + inc[persistent][ref] _x.1; + inc[persistent] _x.2; let _x.3 := Lean.Name.str._override _x.2 _x.1; return _x.3 -[Compiler.saveImpure] size: 3 +[Compiler.saveImpure] size: 5 def nameTest9._closed_4 : tobj := let _x.1 := nameTest5._closed_0; let _x.2 := nameTest9._closed_3; + inc[persistent][ref] _x.1; + inc[persistent] _x.2; let _x.3 := Lean.Name.str._override _x.2 _x.1; return _x.3 -[Compiler.saveImpure] size: 3 +[Compiler.saveImpure] size: 5 def nameTest9._closed_5 : tobj := let _x.1 := nameTest6._closed_0; let _x.2 := nameTest9._closed_4; + inc[persistent][ref] _x.1; + inc[persistent] _x.2; let _x.3 := Lean.Name.str._override _x.2 _x.1; return _x.3 -[Compiler.saveImpure] size: 3 +[Compiler.saveImpure] size: 5 def nameTest9._closed_6 : tobj := let _x.1 := nameTest7._closed_0; let _x.2 := nameTest9._closed_5; + inc[persistent][ref] _x.1; + inc[persistent] _x.2; let _x.3 := Lean.Name.str._override _x.2 _x.1; return _x.3 -[Compiler.saveImpure] size: 3 +[Compiler.saveImpure] size: 5 def nameTest9._closed_7 : tobj := let _x.1 := nameTest8._closed_0; let _x.2 := nameTest9._closed_6; + inc[persistent][ref] _x.1; + inc[persistent] _x.2; let _x.3 := Lean.Name.str._override _x.2 _x.1; return _x.3 [Compiler.saveImpure] size: 1 def nameTest9._closed_8 : obj := let _x.1 := "I"; return _x.1 -[Compiler.saveImpure] size: 3 +[Compiler.saveImpure] size: 5 def nameTest9._closed_9 : tobj := let _x.1 := nameTest9._closed_8; let _x.2 := nameTest9._closed_7; + inc[persistent][ref] _x.1; + inc[persistent] _x.2; let _x.3 := Lean.Name.str._override _x.2 _x.1; return _x.3 -[Compiler.saveImpure] size: 1 +[Compiler.saveImpure] size: 2 def nameTest9 : tobj := let _x.1 := nameTest9._closed_9; + inc[persistent] _x.1; return _x.1 -/ #guard_msgs in @@ -349,15 +418,17 @@ def nameTest9 : Name := `A.B.C.D.E.F.G.H.I /-- trace: [Compiler.simpleGround] Marked nameTest10._closed_0 as simple ground expr [Compiler.simpleGround] Marked nameTest10 as simple ground expr -[Compiler.saveImpure] size: 3 +[Compiler.saveImpure] size: 4 def nameTest10._closed_0 : tobj := let _x.1 := 1; let _x.2 := nameTest3._closed_0; + inc[persistent] _x.2; let _x.3 := Lean.Name.num._override _x.2 _x.1; return _x.3 -[Compiler.saveImpure] size: 1 +[Compiler.saveImpure] size: 2 def nameTest10 : tobj := let _x.1 := nameTest10._closed_0; + inc[persistent] _x.1; return _x.1 -/ #guard_msgs in @@ -373,15 +444,18 @@ trace: [Compiler.simpleGround] Marked nameTest11._closed_0 as simple ground expr def nameTest11._closed_0 : obj := let _x.1 := "AHHHH"; return _x.1 -[Compiler.saveImpure] size: 3 +[Compiler.saveImpure] size: 5 def nameTest11._closed_1 : tobj := let _x.1 := nameTest11._closed_0; let _x.2 := nameTest3._closed_0; + inc[persistent][ref] _x.1; + inc[persistent] _x.2; let _x.3 := Lean.Name.str._override _x.2 _x.1; return _x.3 -[Compiler.saveImpure] size: 1 +[Compiler.saveImpure] size: 2 def nameTest11 : tobj := let _x.1 := nameTest11._closed_1; + inc[persistent] _x.1; return _x.1 -/ #guard_msgs in @@ -404,22 +478,24 @@ trace: [Compiler.simpleGround] Marked testWithScalars._closed_0 as simple ground def testWithScalars._closed_0 : obj := let _x.1 := "W"; return _x.1 -[Compiler.saveImpure] size: 10 +[Compiler.saveImpure] size: 11 def testWithScalars._closed_1 : obj := let _x.1 := 3; let _x.2 := 2; let _x.3 := 1; let _x.4 := 0; let _x.5 := testWithScalars._closed_0; + inc[persistent][ref] _x.5; let _x.6 := ctor_0.0.15[WithScalars.mk] _x.5; sset _x.6[1, 0] := _x.4; sset _x.6[1, 8] := _x.3; sset _x.6[1, 12] := _x.2; sset _x.6[1, 14] := _x.1; return _x.6 -[Compiler.saveImpure] size: 1 +[Compiler.saveImpure] size: 2 def testWithScalars : obj := let _x.1 := testWithScalars._closed_1; + inc[persistent][ref] _x.1; return _x.1 -/ #guard_msgs in @@ -439,16 +515,18 @@ trace: [Compiler.simpleGround] Marked testWithUSize._closed_0 as simple ground e def testWithUSize._closed_0 : obj := let _x.1 := "U"; return _x.1 -[Compiler.saveImpure] size: 4 +[Compiler.saveImpure] size: 5 def testWithUSize._closed_1 : obj := let _x.1 := 0; let _x.2 := testWithUSize._closed_0; + inc[persistent][ref] _x.2; let _x.3 := ctor_0.1.0[WithUSize.mk] _x.2; uset _x.3[1] := _x.1; return _x.3 -[Compiler.saveImpure] size: 1 +[Compiler.saveImpure] size: 2 def testWithUSize : obj := let _x.1 := testWithUSize._closed_1; + inc[persistent][ref] _x.1; return _x.1 -/ #guard_msgs in @@ -472,7 +550,7 @@ trace: [Compiler.simpleGround] Marked testWithUSizeAndScalars._closed_0 as simpl def testWithUSizeAndScalars._closed_0 : obj := let _x.1 := "WUAS"; return _x.1 -[Compiler.saveImpure] size: 12 +[Compiler.saveImpure] size: 13 def testWithUSizeAndScalars._closed_1 : obj := let _x.1 := 4; let _x.2 := 3; @@ -480,6 +558,7 @@ trace: [Compiler.simpleGround] Marked testWithUSizeAndScalars._closed_0 as simpl let _x.4 := 1; let _x.5 := 0; let _x.6 := testWithUSizeAndScalars._closed_0; + inc[persistent][ref] _x.6; let _x.7 := ctor_0.1.15[WithUSizeAndScalars.mk] _x.6; sset _x.7[2, 0] := _x.5; sset _x.7[2, 8] := _x.4; @@ -487,9 +566,10 @@ trace: [Compiler.simpleGround] Marked testWithUSizeAndScalars._closed_0 as simpl sset _x.7[2, 14] := _x.2; uset _x.7[1] := _x.1; return _x.7 -[Compiler.saveImpure] size: 1 +[Compiler.saveImpure] size: 2 def testWithUSizeAndScalars : obj := let _x.1 := testWithUSizeAndScalars._closed_1; + inc[persistent][ref] _x.1; return _x.1 -/ #guard_msgs in @@ -509,9 +589,10 @@ trace: [Compiler.simpleGround] Marked uint8Pair._closed_0 as simple ground expr let _x.4 := box _x.1; let _x.5 := ctor_0[Prod.mk] _x.3 _x.4; return _x.5 -[Compiler.saveImpure] size: 1 +[Compiler.saveImpure] size: 2 def uint8Pair : obj := let _x.1 := uint8Pair._closed_0; + inc[persistent][ref] _x.1; return _x.1 -/ #guard_msgs in @@ -531,9 +612,10 @@ trace: [Compiler.simpleGround] Marked uint16Pair._closed_0 as simple ground expr let _x.4 := box _x.1; let _x.5 := ctor_0[Prod.mk] _x.3 _x.4; return _x.5 -[Compiler.saveImpure] size: 1 +[Compiler.saveImpure] size: 2 def uint16Pair : obj := let _x.1 := uint16Pair._closed_0; + inc[persistent][ref] _x.1; return _x.1 -/ #guard_msgs in @@ -559,15 +641,18 @@ trace: [Compiler.simpleGround] Marked uint64Pair._closed_0._boxed_const_1 as sim let _x.1 := 3; let _x.2 := box _x.1; return _x.2 -[Compiler.saveImpure] size: 3 +[Compiler.saveImpure] size: 5 def uint64Pair._closed_0 : obj := let _x.1 := uint64Pair._closed_0._boxed_const_1; let _x.2 := uint64Pair._closed_0._boxed_const_2; + inc[persistent] _x.2; + inc[persistent] _x.1; let _x.3 := ctor_0[Prod.mk] _x.1 _x.2; return _x.3 -[Compiler.saveImpure] size: 1 +[Compiler.saveImpure] size: 2 def uint64Pair : obj := let _x.1 := uint64Pair._closed_0; + inc[persistent][ref] _x.1; return _x.1 -/ #guard_msgs in @@ -591,15 +676,18 @@ trace: [Compiler.simpleGround] Marked usizePair._closed_0._boxed_const_1 as simp let _x.1 := 3; let _x.2 := box _x.1; return _x.2 -[Compiler.saveImpure] size: 3 +[Compiler.saveImpure] size: 5 def usizePair._closed_0 : obj := let _x.1 := usizePair._closed_0._boxed_const_1; let _x.2 := usizePair._closed_0._boxed_const_2; + inc[persistent] _x.2; + inc[persistent] _x.1; let _x.3 := ctor_0[Prod.mk] _x.1 _x.2; return _x.3 -[Compiler.saveImpure] size: 1 +[Compiler.saveImpure] size: 2 def usizePair : obj := let _x.1 := usizePair._closed_0; + inc[persistent][ref] _x.1; return _x.1 -/ #guard_msgs in @@ -620,9 +708,10 @@ trace: [Compiler.simpleGround] Marked arrayNatTest._closed_0 as simple ground ex let _x.6 := Array.push ◾ _x.5 _x.1; let _x.7 := Array.push ◾ _x.6 _x.3; return _x.7 -[Compiler.saveImpure] size: 1 +[Compiler.saveImpure] size: 2 def arrayNatTest : obj := let _x.1 := arrayNatTest._closed_0; + inc[persistent][ref] _x.1; return _x.1 -/ #guard_msgs in @@ -638,9 +727,10 @@ trace: [Compiler.simpleGround] Marked emptyArrayTest._closed_0 as simple ground let _x.1 := 0; let _x.2 := Array.mkEmpty ◾ _x.1; return _x.2 -[Compiler.saveImpure] size: 1 +[Compiler.saveImpure] size: 2 def emptyArrayTest : obj := let _x.1 := emptyArrayTest._closed_0; + inc[persistent][ref] _x.1; return _x.1 -/ #guard_msgs in @@ -661,18 +751,21 @@ trace: [Compiler.simpleGround] Marked arrayStringTest._closed_0 as simple ground def arrayStringTest._closed_1 : obj := let _x.1 := "world"; return _x.1 -[Compiler.saveImpure] size: 6 +[Compiler.saveImpure] size: 8 def arrayStringTest._closed_2 : obj := let _x.1 := arrayStringTest._closed_1; let _x.2 := arrayStringTest._closed_0; let _x.3 := 2; let _x.4 := Array.mkEmpty ◾ _x.3; + inc[persistent][ref] _x.2; let _x.5 := Array.push ◾ _x.4 _x.2; + inc[persistent][ref] _x.1; let _x.6 := Array.push ◾ _x.5 _x.1; return _x.6 -[Compiler.saveImpure] size: 1 +[Compiler.saveImpure] size: 2 def arrayStringTest : obj := let _x.1 := arrayStringTest._closed_2; + inc[persistent][ref] _x.1; return _x.1 -/ #guard_msgs in @@ -697,9 +790,10 @@ trace: [Compiler.simpleGround] Marked arrayUInt8Test._closed_0 as simple ground let _x.10 := box _x.1; let _x.11 := Array.push ◾ _x.9 _x.10; return _x.11 -[Compiler.saveImpure] size: 1 +[Compiler.saveImpure] size: 2 def arrayUInt8Test : obj := let _x.1 := arrayUInt8Test._closed_0; + inc[persistent][ref] _x.1; return _x.1 -/ #guard_msgs in @@ -724,9 +818,10 @@ trace: [Compiler.simpleGround] Marked arrayUInt16Test._closed_0 as simple ground let _x.10 := box _x.1; let _x.11 := Array.push ◾ _x.9 _x.10; return _x.11 -[Compiler.saveImpure] size: 1 +[Compiler.saveImpure] size: 2 def arrayUInt16Test : obj := let _x.1 := arrayUInt16Test._closed_0; + inc[persistent][ref] _x.1; return _x.1 -/ #guard_msgs in @@ -755,20 +850,24 @@ trace: [Compiler.simpleGround] Marked arrayUInt64._closed_0._boxed_const_1 as si let _x.1 := 11; let _x.2 := box _x.1; return _x.2 -[Compiler.saveImpure] size: 8 +[Compiler.saveImpure] size: 11 def arrayUInt64._closed_0 : obj := let _x.1 := 3; let _x.2 := Array.mkEmpty ◾ _x.1; let _x.3 := arrayUInt64._closed_0._boxed_const_3; + inc[persistent] _x.3; let _x.4 := Array.push ◾ _x.2 _x.3; let _x.5 := arrayUInt64._closed_0._boxed_const_2; + inc[persistent] _x.5; let _x.6 := Array.push ◾ _x.4 _x.5; let _x.7 := arrayUInt64._closed_0._boxed_const_1; + inc[persistent] _x.7; let _x.8 := Array.push ◾ _x.6 _x.7; return _x.8 -[Compiler.saveImpure] size: 1 +[Compiler.saveImpure] size: 2 def arrayUInt64 : obj := let _x.1 := arrayUInt64._closed_0; + inc[persistent][ref] _x.1; return _x.1 -/ #guard_msgs in @@ -797,20 +896,24 @@ trace: [Compiler.simpleGround] Marked arrayUSize._closed_0._boxed_const_1 as sim let _x.1 := 17; let _x.2 := box _x.1; return _x.2 -[Compiler.saveImpure] size: 8 +[Compiler.saveImpure] size: 11 def arrayUSize._closed_0 : obj := let _x.1 := 3; let _x.2 := Array.mkEmpty ◾ _x.1; let _x.3 := arrayUSize._closed_0._boxed_const_3; + inc[persistent] _x.3; let _x.4 := Array.push ◾ _x.2 _x.3; let _x.5 := arrayUSize._closed_0._boxed_const_2; + inc[persistent] _x.5; let _x.6 := Array.push ◾ _x.4 _x.5; let _x.7 := arrayUSize._closed_0._boxed_const_1; + inc[persistent] _x.7; let _x.8 := Array.push ◾ _x.6 _x.7; return _x.8 -[Compiler.saveImpure] size: 1 +[Compiler.saveImpure] size: 2 def arrayUSize : obj := let _x.1 := arrayUSize._closed_0; + inc[persistent][ref] _x.1; return _x.1 -/ #guard_msgs in @@ -835,18 +938,21 @@ trace: [Compiler.simpleGround] Marked arrayNatPair._closed_0 as simple ground ex let _x.2 := 3; let _x.3 := ctor_0[Prod.mk] _x.2 _x.1; return _x.3 -[Compiler.saveImpure] size: 6 +[Compiler.saveImpure] size: 8 def arrayNatPair._closed_2 : obj := let _x.1 := arrayNatPair._closed_1; let _x.2 := arrayNatPair._closed_0; let _x.3 := 2; let _x.4 := Array.mkEmpty ◾ _x.3; + inc[persistent][ref] _x.2; let _x.5 := Array.push ◾ _x.4 _x.2; + inc[persistent][ref] _x.1; let _x.6 := Array.push ◾ _x.5 _x.1; return _x.6 -[Compiler.saveImpure] size: 1 +[Compiler.saveImpure] size: 2 def arrayNatPair : obj := let _x.1 := arrayNatPair._closed_2; + inc[persistent][ref] _x.1; return _x.1 -/ #guard_msgs in @@ -872,9 +978,10 @@ trace: [Compiler.simpleGround] Marked byteArrayTest._closed_0 as simple ground e let _x.11 := Array.push ◾ _x.9 _x.10; let _x.12 := ByteArray.mk _x.11; return _x.12 -[Compiler.saveImpure] size: 1 +[Compiler.saveImpure] size: 2 def byteArrayTest : obj := let _x.1 := byteArrayTest._closed_0; + inc[persistent][ref] _x.1; return _x.1 -/ #guard_msgs in @@ -891,14 +998,16 @@ trace: [Compiler.simpleGround] Marked emptyByteArrayTest._closed_0 as simple gro let _x.1 := 0; let _x.2 := Array.mkEmpty ◾ _x.1; return _x.2 -[Compiler.saveImpure] size: 2 +[Compiler.saveImpure] size: 3 def emptyByteArrayTest._closed_1 : obj := let _x.1 := emptyByteArrayTest._closed_0; + inc[persistent][ref] _x.1; let _x.2 := ByteArray.mk _x.1; return _x.2 -[Compiler.saveImpure] size: 1 +[Compiler.saveImpure] size: 2 def emptyByteArrayTest : obj := let _x.1 := emptyByteArrayTest._closed_1; + inc[persistent][ref] _x.1; return _x.1 -/ #guard_msgs in