chore: bump toolchain to v4.2.0-rc3

Lean4Checker/Lean.lean

@@ -15,44 +15,13 @@ namespace Lean
 
 namespace NameSet
 
-/-- The union of two `NameSet`s. -/
-def append (s t : NameSet) : NameSet :=
-  s.mergeBy (fun _ _ _ => .unit) t
-
-instance : Append NameSet where
-  append := NameSet.append
-
 def ofList (names : List Name) : NameSet :=
   names.foldl (fun s n => s.insert n) {}
 
 end NameSet
 
 def HashMap.keyNameSet (m : HashMap Name α) : NameSet :=
   m.fold (fun s n _ => s.insert n) {}
-
-/-- Like `Expr.getUsedConstants`, but produce a `NameSet`. -/
-def Expr.getUsedConstants' (e : Expr) : NameSet :=
-  e.foldConsts {} fun c cs => cs.insert c
-
-namespace ConstantInfo
-
-/-- Return all names appearing in the type or value of a `ConstantInfo`. -/
-def getUsedConstants (c : ConstantInfo) : NameSet :=
-  c.type.getUsedConstants' ++ match c.value? with
-  | some v => v.getUsedConstants'
-  | none => match c with
-    | .inductInfo val => .ofList val.ctors
-    | .opaqueInfo val => val.value.getUsedConstants'
-    | .ctorInfo val => ({} : NameSet).insert val.name
-    | .recInfo val => .ofList val.all
-    | _ => {}
-
-def inductiveVal! : ConstantInfo → InductiveVal
-  | .inductInfo val => val
-  | _ => panic! "Expected a `ConstantInfo.inductInfo`."
-
-end ConstantInfo
-
 namespace Environment
 
 def importsOf (env : Environment) (n : Name) : Array Import :=

Lean4Checker/Tests/AddFalse.lean

@@ -1,11 +1,15 @@
-import Lean
+import Lean4Checker.Tests.OpenPrivate
+
+open private mk from Lean.Environment
 
 open Lean in
 elab "add_false" : command => do
   modifyEnv fun env =>
     let constants := env.constants.insert `false $ ConstantInfo.thmInfo
       { name := `false, levelParams := [], type := .const ``False [], value := .const ``False [] }
-    { env with constants }
+    -- Before `Environment.mk` became private, we could just use
+    -- `{ env with constants }`
+    mk env.const2ModIdx constants env.extensions env.extraConstNames env.header
 
 add_false
 

Lean4Checker/Tests/AddFalseConstructor.lean

@@ -1,4 +1,6 @@
-import Lean
+import Lean4Checker.Tests.OpenPrivate
+
+open private mk from Lean.Environment
 
 open Lean in
 elab "add_false_constructor" : command => do
@@ -12,7 +14,9 @@ elab "add_false_constructor" : command => do
         numParams := 0
         numFields := 0
         isUnsafe := false }
-    { env with constants }
+    -- Before `Environment.mk` became private, we could just use
+    -- `{ env with constants }`
+    mk env.const2ModIdx constants env.extensions env.extraConstNames env.header
 
 add_false_constructor
 

Lean4Checker/Tests/OpenPrivate.lean

@@ -0,0 +1,143 @@
+/-
+Copyright (c) 2021 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mario Carneiro
+-/
+import Lean.Elab.Command
+import Lean.Util.FoldConsts
+import Lean.Parser.Module
+
+open Lean Parser.Tactic Elab Command
+
+namespace Lean
+
+/-- Collects the names of private declarations referenced in definition `n`. -/
+def Meta.collectPrivateIn [Monad m] [MonadEnv m] [MonadError m]
+  (n : Name) (set := NameSet.empty) : m NameSet := do
+  let c ← getConstInfo n
+  let traverse value := Expr.foldConsts value set fun c a =>
+    if isPrivateName c then a.insert c else a
+  if let some value := c.value? then return traverse value
+  if let some c := (← getEnv).find? (n ++ `_cstage1) then
+    if let some value := c.value? then return traverse value
+  return traverse c.type
+
+/-- Get the module index given a module name. -/
+def Environment.moduleIdxForModule? (env : Environment) (mod : Name) : Option ModuleIdx :=
+  (env.allImportedModuleNames.indexOf? mod).map fun idx => idx.val
+
+instance : DecidableEq ModuleIdx := instDecidableEqNat
+
+/-- Get the list of declarations in a module (referenced by index). -/
+def Environment.declsInModuleIdx (env : Environment) (idx : ModuleIdx) : List Name :=
+  env.const2ModIdx.fold (fun acc n i => if i = idx then n :: acc else acc) []
+
+/-- Add info to the info tree corresponding to a module name. -/
+def Elab.addModuleInfo [Monad m] [MonadInfoTree m] (stx : Ident) : m Unit := do
+  -- HACK: The server looks specifically for ofCommandInfo nodes on `import` syntax
+  -- to do go-to-def for modules, so we have to add something that looks like an import
+  -- to the info tree. (Ideally this would be an `.ofModuleInfo` node instead.)
+  pushInfoLeaf <| .ofCommandInfo {
+    elaborator := `import
+    stx := Unhygienic.run `(Parser.Module.import| import $stx) |>.raw.copyHeadTailInfoFrom stx
+  }
+
+namespace Elab.Command
+
+/-- Core elaborator for `open private` and `export private`. -/
+def elabOpenPrivateLike (ids : Array Ident) (tgts mods : Option (Array Ident))
+  (f : (priv full user : Name) → CommandElabM Name) : CommandElabM Unit := do
+  let mut names := NameSet.empty
+  for tgt in tgts.getD #[] do
+    let n ← resolveGlobalConstNoOverloadWithInfo tgt
+    names ← Meta.collectPrivateIn n names
+  for mod in mods.getD #[] do
+    let some modIdx := (← getEnv).moduleIdxForModule? mod.getId
+      | throwError "unknown module {mod}"
+    addModuleInfo mod
+    for declName in (← getEnv).declsInModuleIdx modIdx do
+      if isPrivateName declName then
+        names := names.insert declName
+  let appendNames (msg : String) : String := Id.run do
+    let mut msg := msg
+    for c in names do
+      if let some name := privateToUserName? c then
+        msg := msg ++ s!"{name}\n"
+    msg
+  if ids.isEmpty && !names.isEmpty then
+    logInfo (appendNames "found private declarations:\n")
+  let mut decls := #[]
+  for id in ids do
+    let n := id.getId
+    let mut found := []
+    for c in names do
+      if n.isSuffixOf c then
+        addConstInfo id c
+        found := c::found
+    match found with
+    | [] => throwError appendNames s!"'{n}' not found in the provided declarations:\n"
+    | [c] =>
+      if let some name := privateToUserName? c then
+        let new ← f c name n
+        decls := decls.push (OpenDecl.explicit n new)
+      else unreachable!
+    | _ => throwError s!"provided name is ambiguous: found {found.map privateToUserName?}"
+  modifyScope fun scope => Id.run do
+    let mut openDecls := scope.openDecls
+    for decl in decls do
+      openDecls := decl::openDecls
+    { scope with openDecls := openDecls }
+
+/--
+The command `open private a b c in foo bar` will look for private definitions named `a`, `b`, `c`
+in declarations `foo` and `bar` and open them in the current scope. This does not make the
+definitions public, but rather makes them accessible in the current section by the short name `a`
+instead of the (unnameable) internal name for the private declaration, something like
+`_private.Other.Module.0.Other.Namespace.foo.a`, which cannot be typed directly because of the `0`
+name component.
+
+It is also possible to specify the module instead with
+`open private a b c from Other.Module`.
+-/
+syntax (name := openPrivate) "open private" (ppSpace ident)*
+  (" in" (ppSpace ident)*)? (" from" (ppSpace ident)*)? : command
+
+/-- Elaborator for `open private`. -/
+@[command_elab openPrivate] def elabOpenPrivate : CommandElab
+| `(open private $ids* $[in $tgts*]? $[from $mods*]?) =>
+  elabOpenPrivateLike ids tgts mods fun c _ _ => pure c
+| _ => throwUnsupportedSyntax
+
+/--
+The command `export private a b c in foo bar` is similar to `open private`, but instead of opening
+them in the current scope it will create public aliases to the private definition. The definition
+will exist at exactly the original location and name, as if the `private` keyword was not used
+originally.
+
+It will also open the newly created alias definition under the provided short name, like
+`open private`.
+It is also possible to specify the module instead with
+`export private a b c from Other.Module`.
+-/
+syntax (name := exportPrivate) "export private" (ppSpace ident)*
+  (" in" (ppSpace ident)*)? (" from" (ppSpace ident)*)? : command
+
+/-- Elaborator for `export private`. -/
+@[command_elab exportPrivate] def elabExportPrivate : CommandElab
+| `(export private $ids* $[in $tgts*]? $[from $mods*]?) =>
+  elabOpenPrivateLike ids tgts mods fun c name _ => liftCoreM do
+    let cinfo ← getConstInfo c
+    if (← getEnv).contains name then
+      throwError s!"'{name}' has already been declared"
+    let decl := Declaration.defnDecl {
+      name := name,
+      levelParams := cinfo.levelParams,
+      type := cinfo.type,
+      value := mkConst c (cinfo.levelParams.map mkLevelParam),
+      hints := ReducibilityHints.abbrev,
+      safety := if cinfo.isUnsafe then DefinitionSafety.unsafe else DefinitionSafety.safe
+    }
+    addDecl decl
+    compileDecl decl
+    pure name
+| _ => throwUnsupportedSyntax

Main.lean

@@ -59,7 +59,7 @@ and add it to the environment.
 partial def replayConstant (name : Name) : M Unit := do
   if ← isTodo name then
     let some ci := (← read).newConstants.find? name | unreachable!
-    replayConstants ci.getUsedConstants
+    replayConstants ci.getUsedConstantsAsSet
     -- Check that this name is still pending: a mutual block may have taken care of it.
     if (← get).pending.contains name then
       match ci with
@@ -84,7 +84,7 @@ partial def replayConstant (name : Name) : M Unit := do
         -- Make sure we are really finished with the constructors.
         for (_, ctors) in ctorInfo do
           for ctor in ctors do
-            replayConstants ctor.getUsedConstants
+            replayConstants ctor.getUsedConstantsAsSet
         let types : List InductiveType := ctorInfo.map fun ⟨ci, ctors⟩ =>
           { name := ci.name
             type := ci.type

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:4.1.0-rc1
+leanprover/lean4:v4.2.0-rc3