max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: reserve public import syntax (#9061)

Browse source 
This PR adds the `public import` syntax to be used by the experimental
module system
This commit is contained in:
Sebastian Ullrich 2025-06-28 15:11:34 +02:00 • committed by GitHub
parent e844f9c82c
commit d7e35c77ca
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
3 changed files with 10 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/Lean/Elab/Import.lean
View file

@ -22,9 +22,14 @@ def HeaderSyntax.imports (stx : HeaderSyntax) (includeInit : Bool := true) : Arr
| `(Parser.Module.header| $[module%$moduleTk]? $[prelude%$preludeTk]? $importsStx*) =>
let imports := if preludeTk.isNone && includeInit then #[{ module := `Init : Import }] else #[]
imports ++ importsStx.map fun
-- TODO: delete together with `private` keyword
| `(Parser.Module.import| $[private%$privateTk]? $[meta%$metaTk]? import $[all%$allTk]? $n) =>
{ module := n.getId, importAll := allTk.isSome, isExported := privateTk.isNone
isMeta := metaTk.isSome }
| `(Parser.Module.import| $[public%$publicTk]? $[meta%$metaTk]? import $[all%$allTk]? $n) =>
{ module := n.getId, importAll := allTk.isSome
isExported := publicTk.isSome || moduleTk.isNone
isMeta := metaTk.isSome }
| _ => unreachable!
| _ => unreachable!
@ -53,8 +58,6 @@ def processHeaderCore
throw <| .userError "cannot use `import all` without `module`"
if i.importAll && mainModule.getRoot != i.module.getRoot then
throw <| .userError "cannot use `import all` across module path roots"
if !isModule && !i.isExported then
throw <| .userError "cannot use `private import` without `module`"
let env ←
importModules (leakEnv := leakEnv) (loadExts := true) (level := level)
imports opts trustLevel plugins arts

2
src/Lean/Elab/ParseImportsFast.lean
View file

@ -204,6 +204,8 @@ def main : Parser :=
keywordCore "module" (fun _ s => s) (fun _ s => { s with isModule := true }) >>
keywordCore "prelude" (fun _ s => s.pushImport `Init) (fun _ s => s) >>
many (keywordCore "private" (setIsExported true) (setIsExported false) >>
-- TODO: unset exported when absent and remove `private`
keywordCore "public" (setIsExported true) (setIsExported true) >>
keywordCore "meta" (setIsMeta false) (setIsMeta true) >>
keyword "import" >>
keywordCore "all" (setImportAll false) (setImportAll true) >>

4
src/Lean/Parser/Module.lean
View file

@ -13,11 +13,13 @@ namespace Parser
namespace Module
def moduleTk := leading_parser "module"
def «prelude» := leading_parser "prelude"
-- TODO: delete
def «private» := leading_parser (withAnonymousAntiquot := false) "private"
def «public» := leading_parser (withAnonymousAntiquot := false) "public"
def «meta» := leading_parser (withAnonymousAntiquot := false) "meta"
def «all» := leading_parser (withAnonymousAntiquot := false) "all"
def «import» := leading_parser
atomic (optional «private» >> optional «meta» >> "import ") >>
atomic (optional («private» <|> «public») >> optional «meta» >> "import ") >>
optional all >>
identWithPartialTrailingDot
def header := leading_parser optional (moduleTk >> ppLine >> ppLine) >>