From 981d71b6d8a43a60e0f4d83e3b427dd08eb65622 Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Thu, 19 Oct 2023 09:32:24 +1100 Subject: [PATCH] chore: bump toolchain to v4.2.0-rc3 --- Lean4Checker/Lean.lean | 31 ----- Lean4Checker/Tests/AddFalse.lean | 8 +- Lean4Checker/Tests/AddFalseConstructor.lean | 8 +- Lean4Checker/Tests/OpenPrivate.lean | 143 ++++++++++++++++++++ Main.lean | 4 +- lean-toolchain | 2 +- 6 files changed, 158 insertions(+), 38 deletions(-) create mode 100644 Lean4Checker/Tests/OpenPrivate.lean diff --git a/Lean4Checker/Lean.lean b/Lean4Checker/Lean.lean index 30f0fe1..e9d6ac7 100644 --- a/Lean4Checker/Lean.lean +++ b/Lean4Checker/Lean.lean @@ -15,13 +15,6 @@ 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) {} @@ -29,30 +22,6 @@ 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 := diff --git a/Lean4Checker/Tests/AddFalse.lean b/Lean4Checker/Tests/AddFalse.lean index 7fd86bc..85fad7a 100644 --- a/Lean4Checker/Tests/AddFalse.lean +++ b/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 diff --git a/Lean4Checker/Tests/AddFalseConstructor.lean b/Lean4Checker/Tests/AddFalseConstructor.lean index 12a7791..bafbc41 100644 --- a/Lean4Checker/Tests/AddFalseConstructor.lean +++ b/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 diff --git a/Lean4Checker/Tests/OpenPrivate.lean b/Lean4Checker/Tests/OpenPrivate.lean new file mode 100644 index 0000000..0d3686a --- /dev/null +++ b/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 diff --git a/Main.lean b/Main.lean index 81dcc5e..d921440 100644 --- a/Main.lean +++ b/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 diff --git a/lean-toolchain b/lean-toolchain index a0d7ae8..a61d282 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:4.1.0-rc1 +leanprover/lean4:v4.2.0-rc3