refactor: change definition of closed terms

src/Init/Prelude.lean

@@ -2660,7 +2660,8 @@ instance : Max UInt32 := maxOfLe
 instance : Min UInt32 := minOfLe
 
 /-- The number of distinct values representable by `UInt64`, that is, `2^64 = 18446744073709551616`. -/
-abbrev UInt64.size : Nat := 18446744073709551616
+@[noinline, reducible]
+def UInt64.size : Nat := 18446744073709551616
 
 /--
 Unsigned 64-bit integers.
@@ -2718,7 +2719,8 @@ instance : Inhabited UInt64 where
   default := UInt64.ofNatLT 0 (of_decide_eq_true rfl)
 
 /-- The number of distinct values representable by `USize`, that is, `2^System.Platform.numBits`. -/
-abbrev USize.size : Nat := (hPow 2 System.Platform.numBits)
+@[noinline, reducible]
+def USize.size : Nat := (hPow 2 System.Platform.numBits)
 
 theorem USize.size_eq : Or (Eq USize.size 4294967296) (Eq USize.size 18446744073709551616) :=
   show Or (Eq (hPow 2 System.Platform.numBits) 4294967296) (Eq (hPow 2 System.Platform.numBits) 18446744073709551616) from

src/Lean/Compiler/LCNF/ExtractClosed.lean

@@ -55,31 +55,54 @@ structure State where
 
 abbrev M := ReaderT Context $ StateRefT State CompilerM
 
+def extractionAllowlist : Std.HashSet Name := .ofArray #[
+  ``Lean.Name.mkStr,
+  ``Lean.Name.mkNum,
+  ``Lean.Name.mkStr1,
+  ``Lean.Name.mkStr2,
+  ``Lean.Name.mkStr3,
+  ``Lean.Name.mkStr4,
+  ``Lean.Name.mkStr5,
+  ``Lean.Name.mkStr6,
+  ``Lean.Name.mkStr7,
+  ``Lean.Name.mkStr8,
+  ``Lean.Name.str._override,
+  ``Lean.Name.num._override,
+  ``ByteArray.mk,
+]
+
 mutual
 
 partial def shouldExtractLetValue (isRoot : Bool) (v : LetValue) : M Bool := do
   match v with
   | .lit (.str _) => return true
-  | .lit (.nat v) =>
-    -- The old compiler's implementation used the runtime's `is_scalar` function, which
-    -- introduces a dependency on the architecture used by the compiler.
-    return !isRoot || v >= Nat.pow 2 63
+  | .lit (.nat v) => return !isRoot || v >= Nat.pow 2 63
   | .lit _ | .erased => return !isRoot
   | .const name _ args =>
     if (← read).sccDecls.any (·.name == name) then
       return false
+    -- TODO: cleanup never extract annotations in core
     if hasNeverExtractAttribute (← getEnv) name then
       return false
-    if isRoot then
-      if let some constInfo := (← getEnv).find? name then
-        let shouldExtract := match constInfo with
-        | .defnInfo val => val.type.isForall
-        | .ctorInfo _ => !(args.all isIrrelevantArg)
-        | _ => true
-        if !shouldExtract then
+    if let some constInfo := (← getEnv).find? name then
+      let shouldExtractCtor :=
+        constInfo.isCtor &&
+        !(isExtern (← getEnv) name) &&
+        (!(args.all isIrrelevantArg) || !isRoot)
+      -- TODO: check fully applied ctor
+      let shouldExtract := shouldExtractCtor || extractionAllowlist.contains name
+      if !shouldExtract then
+        return false
+    else
+      if let some decl := ← getMonoDecl? name then
+        if args.size >= decl.getArity then
           return false
+      if !(!isRoot && isClosedTermName (← getEnv) name) then
+        return false
     args.allM shouldExtractArg
-  | .fvar fnVar args => return (← shouldExtractFVar fnVar) && (← args.allM shouldExtractArg)
+  | .fvar fnVar args =>
+    -- TODO: finetune, this could make a pap an fap which we want to avoid
+    return (← shouldExtractFVar fnVar) && (← args.allM shouldExtractArg)
   | .proj _ _ baseVar => shouldExtractFVar baseVar
 
 partial def shouldExtractArg (arg : Arg) : M Bool := do