diff --git a/src/Lean/Elab/Import.lean b/src/Lean/Elab/Import.lean index 8cc0c67219..2be41ac7f3 100644 --- a/src/Lean/Elab/Import.lean +++ b/src/Lean/Elab/Import.lean @@ -8,9 +8,9 @@ import Lean.Data.Json namespace Lean.Elab -def headerToImports (header : Syntax) : List Import := - let imports := if header[0].isNone then [{ module := `Init : Import }] else [] - imports ++ header[1].getArgs.toList.map fun stx => +def headerToImports (header : Syntax) : Array Import := + let imports := if header[0].isNone then #[{ module := `Init : Import }] else #[] + imports ++ header[1].getArgs.map fun stx => -- `stx` is of the form `(Module.import "import" "runtime"? id) let runtime := !stx[1].isNone let id := stx[2].getId @@ -27,7 +27,7 @@ def processHeader (header : Syntax) (opts : Options) (messages : MessageLog) (in let pos := inputCtx.fileMap.toPosition spos pure (env, messages.add { fileName := inputCtx.fileName, data := toString e, pos := pos }) -def parseImports (input : String) (fileName : Option String := none) : IO (List Import × Position × MessageLog) := do +def parseImports (input : String) (fileName : Option String := none) : IO (Array Import × Position × MessageLog) := do let fileName := fileName.getD "" let inputCtx := Parser.mkInputContext input fileName let (header, parserState, messages) ← Parser.parseHeader inputCtx diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean index ffe54d2352..9f4043ccd4 100644 --- a/src/Lean/Environment.lean +++ b/src/Lean/Environment.lean @@ -33,6 +33,8 @@ structure Import where runtimeOnly : Bool := false deriving Repr, Inhabited +instance : Coe Name Import := ⟨({module := ·})⟩ + instance : ToString Import := ⟨fun imp => toString imp.module ++ if imp.runtimeOnly then " (runtime)" else ""⟩ /-- @@ -731,73 +733,77 @@ def throwAlreadyImported (s : ImportState) (const2ModIdx : HashMap Name ModuleId let constModName := s.moduleNames[const2ModIdx[cname].get!.toNat]! throw <| IO.userError s!"import {modName} failed, environment already contains '{cname}' from {constModName}" +abbrev ImportStateM := StateRefT ImportState IO + +@[inline] nonrec def ImportStateM.run (x : ImportStateM α) (s : ImportState := {}) : IO (α × ImportState) := + x.run s + +partial def importModulesCore (imports : Array Import) : ImportStateM Unit := do + for i in imports do + if i.runtimeOnly || (← get).moduleNameSet.contains i.module then + continue + modify fun s => { s with moduleNameSet := s.moduleNameSet.insert i.module } + let mFile ← findOLean i.module + unless (← mFile.pathExists) do + throw <| IO.userError s!"object file '{mFile}' of module {i.module} does not exist" + let (mod, region) ← readModuleData mFile + importModulesCore mod.imports + modify fun s => { s with + moduleData := s.moduleData.push mod + regions := s.regions.push region + moduleNames := s.moduleNames.push i.module + } + +def finalizeImport (s : ImportState) (imports : Array Import) (opts : Options) (trustLevel : UInt32 := 0) : IO Environment := do + let numConsts := s.moduleData.foldl (init := 0) fun numConsts mod => + numConsts + mod.constants.size + mod.extraConstNames.size + let mut const2ModIdx : HashMap Name ModuleIdx := mkHashMap (capacity := numConsts) + let mut constantMap : HashMap Name ConstantInfo := mkHashMap (capacity := numConsts) + for h:modIdx in [0:s.moduleData.size] do + let mod := s.moduleData[modIdx]'h.upper + for cname in mod.constNames, cinfo in mod.constants do + match constantMap.insert' cname cinfo with + | (constantMap', replaced) => + constantMap := constantMap' + if replaced then + throwAlreadyImported s const2ModIdx modIdx cname + const2ModIdx := const2ModIdx.insert cname modIdx + for cname in mod.extraConstNames do + const2ModIdx := const2ModIdx.insert cname modIdx + let constants : ConstMap := SMap.fromHashMap constantMap false + let exts ← mkInitialExtensionStates + let env : Environment := { + const2ModIdx := const2ModIdx + constants := constants + extraConstNames := {} + extensions := exts + header := { + quotInit := !imports.isEmpty -- We assume `core.lean` initializes quotient module + trustLevel := trustLevel + imports := imports + regions := s.regions + moduleNames := s.moduleNames + moduleData := s.moduleData + } + } + let env ← setImportedEntries env s.moduleData + let env ← finalizePersistentExtensions env s.moduleData opts + pure env + @[export lean_import_modules] -partial def importModules (imports : List Import) (opts : Options) (trustLevel : UInt32 := 0) : IO Environment := profileitIO "import" opts do +def importModules (imports : Array Import) (opts : Options) (trustLevel : UInt32 := 0) : IO Environment := profileitIO "import" opts do + let imports := imports for imp in imports do if imp.module matches .anonymous then throw <| IO.userError "import failed, trying to import module with anonymous name" withImporting do - let (_, s) ← importMods imports |>.run {} - let mut numConsts := 0 - for mod in s.moduleData do - numConsts := numConsts + mod.constants.size + mod.extraConstNames.size - let mut modIdx : Nat := 0 - let mut const2ModIdx : HashMap Name ModuleIdx := mkHashMap (capacity := numConsts) - let mut constantMap : HashMap Name ConstantInfo := mkHashMap (capacity := numConsts) - for mod in s.moduleData do - for cname in mod.constNames, cinfo in mod.constants do - match constantMap.insert' cname cinfo with - | (constantMap', replaced) => - constantMap := constantMap' - if replaced then - throwAlreadyImported s const2ModIdx modIdx cname - const2ModIdx := const2ModIdx.insert cname modIdx - for cname in mod.extraConstNames do - const2ModIdx := const2ModIdx.insert cname modIdx - modIdx := modIdx + 1 - let constants : ConstMap := SMap.fromHashMap constantMap false - let exts ← mkInitialExtensionStates - let env : Environment := { - const2ModIdx := const2ModIdx - constants := constants - extraConstNames := {} - extensions := exts - header := { - quotInit := !imports.isEmpty -- We assume `core.lean` initializes quotient module - trustLevel := trustLevel - imports := imports.toArray - regions := s.regions - moduleNames := s.moduleNames - moduleData := s.moduleData - } - } - let env ← setImportedEntries env s.moduleData - let env ← finalizePersistentExtensions env s.moduleData opts - pure env -where - importMods : List Import → StateRefT ImportState IO Unit - | [] => pure () - | i::is => do - if i.runtimeOnly || (← get).moduleNameSet.contains i.module then - importMods is - else do - modify fun s => { s with moduleNameSet := s.moduleNameSet.insert i.module } - let mFile ← findOLean i.module - unless (← mFile.pathExists) do - throw <| IO.userError s!"object file '{mFile}' of module {i.module} does not exist" - let (mod, region) ← readModuleData mFile - importMods mod.imports.toList - modify fun s => { s with - moduleData := s.moduleData.push mod - regions := s.regions.push region - moduleNames := s.moduleNames.push i.module - } - importMods is + let (_, s) ← importModulesCore imports |>.run + finalizeImport s imports opts trustLevel /-- Create environment object from imports and free compacted regions after calling `act`. No live references to the environment object or imported objects may exist after `act` finishes. -/ -unsafe def withImportModules {α : Type} (imports : List Import) (opts : Options) (trustLevel : UInt32 := 0) (x : Environment → IO α) : IO α := do +unsafe def withImportModules {α : Type} (imports : Array Import) (opts : Options) (trustLevel : UInt32 := 0) (x : Environment → IO α) : IO α := do let env ← importModules imports opts trustLevel try x env finally env.freeRegions diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean index c0ffdd37e1..4c3ef01d83 100644 --- a/src/Lean/Server/FileWorker.lean +++ b/src/Lean/Server/FileWorker.lean @@ -207,7 +207,7 @@ section Initialization -- NOTE: we assume for now that `lakefile.lean` does not have any non-stdlib deps -- NOTE: lake does not exist in stage 0 (yet?) if path.fileName != "lakefile.lean" && (← System.FilePath.pathExists lakePath) then - let pkgSearchPath ← lakeSetupSearchPath lakePath m (Lean.Elab.headerToImports headerStx).toArray hOut + let pkgSearchPath ← lakeSetupSearchPath lakePath m (Lean.Elab.headerToImports headerStx) hOut srcSearchPath ← initSrcSearchPath (← getBuildDir) pkgSearchPath Elab.processHeader headerStx opts msgLog m.mkInputContext catch e => -- should be from `lake print-paths` diff --git a/tests/bench/dag_hassorry_issue.lean b/tests/bench/dag_hassorry_issue.lean index 2c32c0fc23..0117f40e41 100644 --- a/tests/bench/dag_hassorry_issue.lean +++ b/tests/bench/dag_hassorry_issue.lean @@ -52,6 +52,6 @@ def test (n : Nat) : CoreM Unit := do def main (args : List String) : IO Unit := do let [size] := args | throw (IO.userError s!"unexpected number of arguments, numeral expected") initSearchPath (← findSysroot) - let env ← importModules [{ module := `Init.Prelude }] {} 0 + let env ← importModules #[{ module := `Init.Prelude }] {} 0 discard <| test size.toNat! |>.toIO { fileName := "", fileMap := default } { env } IO.println "ok" diff --git a/tests/lean/1240.lean b/tests/lean/1240.lean index 85a71fd16f..0e4e9711f9 100644 --- a/tests/lean/1240.lean +++ b/tests/lean/1240.lean @@ -2,4 +2,4 @@ import Lean.Elab.Frontend open Lean Elab in #eval show IO _ from do - discard <| importModules [Import.mk Name.anonymous false] {} 0 + discard <| importModules #[Import.mk Name.anonymous false] {} 0 diff --git a/tests/lean/1240.lean.expected.out b/tests/lean/1240.lean.expected.out index 6e891d454f..da063cf845 100644 --- a/tests/lean/1240.lean.expected.out +++ b/tests/lean/1240.lean.expected.out @@ -1,2 +1,2 @@ -1240.lean:4:0-5:64: error: import failed, trying to import module with anonymous name +1240.lean:4:0-5:65: error: import failed, trying to import module with anonymous name diff --git a/tests/lean/ctor_layout.lean b/tests/lean/ctor_layout.lean index 9bc09cce05..e9b7c43daa 100644 --- a/tests/lean/ctor_layout.lean +++ b/tests/lean/ctor_layout.lean @@ -4,7 +4,7 @@ open Lean open Lean.IR unsafe def main : IO Unit := -withImportModules [{module := `Lean.Compiler.IR.Basic}] {} 0 fun env => do +withImportModules #[{module := `Lean.Compiler.IR.Basic}] {} 0 fun env => do let ctorLayout ← IO.ofExcept $ getCtorLayout env `Lean.IR.Expr.reuse; ctorLayout.fieldInfo.forM $ fun finfo => IO.println (format finfo); IO.println "---"; diff --git a/tests/lean/run/instances.lean b/tests/lean/run/instances.lean index 49942b8d8f..b1ca83050a 100644 --- a/tests/lean/run/instances.lean +++ b/tests/lean/run/instances.lean @@ -7,7 +7,7 @@ instance : ToFormat InstanceEntry where format e := format e.val unsafe def tst1 : IO Unit := -withImportModules [{module := `Lean}] {} 0 fun env => do +withImportModules #[{module := `Lean}] {} 0 fun env => do let aux : MetaM Unit := do let insts ← getGlobalInstancesIndex IO.println (format insts) diff --git a/tests/lean/run/instuniv.lean b/tests/lean/run/instuniv.lean index 7a63752a49..ce16db5705 100644 --- a/tests/lean/run/instuniv.lean +++ b/tests/lean/run/instuniv.lean @@ -3,7 +3,7 @@ import Lean open Lean unsafe def tst : IO Unit := - withImportModules [{module := `Init.Data.Array}] {} 0 fun env => + withImportModules #[{module := `Init.Data.Array}] {} 0 fun env => match env.find? `Array.foldl with | some info => do IO.println (info.instantiateTypeLevelParams [levelZero, levelZero]) diff --git a/tests/lean/run/meta1.lean b/tests/lean/run/meta1.lean index da46919903..87da33b6a3 100644 --- a/tests/lean/run/meta1.lean +++ b/tests/lean/run/meta1.lean @@ -3,17 +3,17 @@ import Lean.Meta open Lean open Lean.Meta -unsafe def tstInferType (mods : List Name) (e : Expr) : IO Unit := +unsafe def tstInferType (mods : Array Name) (e : Expr) : IO Unit := withImportModules (mods.map $ fun m => {module := m}) {} 0 fun env => do let (type, _, _) ← (inferType e : MetaM _).toIO { fileName := "", fileMap := default } { env := env } {} {}; IO.println (toString e ++ " : " ++ toString type) -unsafe def tstWHNF (mods : List Name) (e : Expr) (t := TransparencyMode.default) : IO Unit := +unsafe def tstWHNF (mods : Array Name) (e : Expr) (t := TransparencyMode.default) : IO Unit := withImportModules (mods.map $ fun m => {module := m}) {} 0 fun env => do let (s, _, _) ← (whnf e : MetaM _).toIO { fileName := "", fileMap := default } { env := env }; IO.println (toString e ++ " ==> " ++ toString s) -unsafe def tstIsProp (mods : List Name) (e : Expr) : IO Unit := +unsafe def tstIsProp (mods : Array Name) (e : Expr) : IO Unit := withImportModules (mods.map $ fun m => {module := m}) {} 0 fun env => do let (b, _, _) ← (isProp e : MetaM _).toIO { fileName := "", fileMap := default } { env := env }; IO.println (toString e ++ ", isProp: " ++ toString b) @@ -24,13 +24,13 @@ let nat := mkConst `Nat []; let bool := mkConst `Bool []; mkAppN map #[nat, bool] -#eval tstInferType [`Init.Data.List] t1 +#eval tstInferType #[`Init.Data.List] t1 def t2 : Expr := let prop := mkSort levelZero; mkForall `x BinderInfo.default prop prop -#eval tstInferType [`Init.Core] t2 +#eval tstInferType #[`Init.Core] t2 def t3 : Expr := let nat := mkConst `Nat []; @@ -39,21 +39,21 @@ let zero := mkLit (Literal.natVal 0); let p := mkAppN natLe #[mkBVar 0, zero]; mkForall `x BinderInfo.default nat p -#eval tstInferType [`Init.Data.Nat] t3 +#eval tstInferType #[`Init.Data.Nat] t3 def t4 : Expr := let nat := mkConst `Nat []; let p := mkAppN (mkConst `Nat.succ []) #[mkBVar 0]; mkLambda `x BinderInfo.default nat p -#eval tstInferType [`Init.Core] t4 +#eval tstInferType #[`Init.Core] t4 def t5 : Expr := let add := mkConst `Nat.add []; mkAppN add #[mkLit (Literal.natVal 3), mkLit (Literal.natVal 5)] -#eval tstWHNF [`Init.Data.Nat] t5 -#eval tstWHNF [`Init.Data.Nat] t5 TransparencyMode.reducible +#eval tstWHNF #[`Init.Data.Nat] t5 +#eval tstWHNF #[`Init.Data.Nat] t5 TransparencyMode.reducible set_option pp.all true #check @List.cons Nat @@ -70,20 +70,20 @@ let four := mkLit (Literal.natVal 4); let xs := mkApp (mkApp cons one) (mkApp (mkApp cons four) nil); mkAppN map #[nat, nat, f, xs] -#eval tstInferType [`Init.Data.List] t6 -#eval tstWHNF [`Init.Data.List] t6 +#eval tstInferType #[`Init.Data.List] t6 +#eval tstWHNF #[`Init.Data.List] t6 -#eval tstInferType [] $ mkSort levelZero +#eval tstInferType #[] $ mkSort levelZero -#eval tstInferType [`Init.Data.List] $ mkLambda `a BinderInfo.implicit (mkSort levelOne) (mkLambda `x BinderInfo.default (mkBVar 0) (mkLambda `xs BinderInfo.default (mkApp (mkConst `List [levelZero]) (mkBVar 1)) (mkBVar 0))) +#eval tstInferType #[`Init.Data.List] $ mkLambda `a BinderInfo.implicit (mkSort levelOne) (mkLambda `x BinderInfo.default (mkBVar 0) (mkLambda `xs BinderInfo.default (mkApp (mkConst `List [levelZero]) (mkBVar 1)) (mkBVar 0))) def t7 : Expr := let nat := mkConst `Nat []; let one := mkLit (Literal.natVal 1); mkLet `x nat one one -#eval tstInferType [`Init.Core] $ t7 -#eval tstWHNF [`Init.Core] $ t7 +#eval tstInferType #[`Init.Core] $ t7 +#eval tstWHNF #[`Init.Core] $ t7 def t8 : Expr := let nat := mkConst `Nat []; @@ -91,43 +91,43 @@ let one := mkLit (Literal.natVal 1); let add := mkConst `Nat.add []; mkLet `x nat one (mkAppN add #[one, mkBVar 0]) -#eval tstInferType [`Init.Core] $ t8 -#eval tstWHNF [`Init.Core] $ t8 +#eval tstInferType #[`Init.Core] $ t8 +#eval tstWHNF #[`Init.Core] $ t8 def t9 : Expr := let nat := mkConst `Nat []; mkLet `a (mkSort levelOne) nat (mkForall `x BinderInfo.default (mkBVar 0) (mkBVar 1)) -#eval tstInferType [`Init.Core] $ t9 -#eval tstWHNF [`Init.Core] $ t9 +#eval tstInferType #[`Init.Core] $ t9 +#eval tstWHNF #[`Init.Core] $ t9 -#eval tstInferType [`Init.Core] $ mkLit (Literal.natVal 10) -#eval tstInferType [`Init.Core] $ mkLit (Literal.strVal "hello") -#eval tstInferType [`Init.Core] $ mkMData {} $ mkLit (Literal.natVal 10) +#eval tstInferType #[`Init.Core] $ mkLit (Literal.natVal 10) +#eval tstInferType #[`Init.Core] $ mkLit (Literal.strVal "hello") +#eval tstInferType #[`Init.Core] $ mkMData {} $ mkLit (Literal.natVal 10) def t10 : Expr := let nat := mkConst `Nat []; let refl := mkApp (mkConst `Eq.refl [levelOne]) nat; mkLambda `a BinderInfo.default nat (mkApp refl (mkBVar 0)) -#eval tstInferType [`Init.Core] t10 -#eval tstIsProp [`Init.Core] t10 +#eval tstInferType #[`Init.Core] t10 +#eval tstIsProp #[`Init.Core] t10 -#eval tstIsProp [`Init.Core] (mkAppN (mkConst `And []) #[mkConst `True [], mkConst `True []]) +#eval tstIsProp #[`Init.Core] (mkAppN (mkConst `And []) #[mkConst `True [], mkConst `True []]) -#eval tstIsProp [`Init.Core] (mkConst `And []) +#eval tstIsProp #[`Init.Core] (mkConst `And []) -- Example where isPropQuick fails -#eval tstIsProp [`Init.Core] (mkAppN (mkConst `id [levelZero]) #[mkSort levelZero, mkAppN (mkConst `And []) #[mkConst `True [], mkConst +#eval tstIsProp #[`Init.Core] (mkAppN (mkConst `id [levelZero]) #[mkSort levelZero, mkAppN (mkConst `And []) #[mkConst `True [], mkConst `True []]]) -#eval tstIsProp [`Init.Core] (mkAppN (mkConst `Eq [levelOne]) #[mkConst `Nat [], mkLit (Literal.natVal 0), mkLit (Literal.natVal 1)]) +#eval tstIsProp #[`Init.Core] (mkAppN (mkConst `Eq [levelOne]) #[mkConst `Nat [], mkLit (Literal.natVal 0), mkLit (Literal.natVal 1)]) -#eval tstIsProp [`Init.Core] $ +#eval tstIsProp #[`Init.Core] $ mkForall `x BinderInfo.default (mkConst `Nat []) (mkAppN (mkConst `Eq [levelOne]) #[mkConst `Nat [], mkBVar 0, mkLit (Literal.natVal 1)]) -#eval tstIsProp [`Init.Core] $ +#eval tstIsProp #[`Init.Core] $ mkApp (mkLambda `x BinderInfo.default (mkConst `Nat []) (mkAppN (mkConst `Eq [levelOne]) #[mkConst `Nat [], mkBVar 0, mkLit (Literal.natVal 1)])) diff --git a/tests/lean/run/meta3.lean b/tests/lean/run/meta3.lean index b5bed1dff2..9c25b19142 100644 --- a/tests/lean/run/meta3.lean +++ b/tests/lean/run/meta3.lean @@ -21,8 +21,8 @@ do let v? ← getExprMVarAssignment? m.mvarId!; | some v => pure v | none => throwError "metavariable is not assigned") -unsafe def run (mods : List Name) (x : MetaM Unit) (opts : Options := dbgOpt) : IO Unit := -withImportModules (mods.map $ fun m => {module := m}) {} 0 fun env => do +unsafe def run (mods : Array Name) (x : MetaM Unit) (opts : Options := dbgOpt) : IO Unit := + withImportModules (mods.map $ fun m => {module := m}) {} 0 fun env => do let x : MetaM Unit := do { x; printTraces }; discard $ x.toIO { options := opts, fileName := "", fileMap := default } { env := env }; pure () @@ -56,4 +56,4 @@ do let d : DiscrTree Nat true := {}; print (format vs); pure () -#eval run [`Init.Data.Nat] tst1 +#eval run #[`Init.Data.Nat] tst1 diff --git a/tests/pkg/user_attr_app/Main.lean b/tests/pkg/user_attr_app/Main.lean index bdf86de03c..9c4935e8b3 100644 --- a/tests/pkg/user_attr_app/Main.lean +++ b/tests/pkg/user_attr_app/Main.lean @@ -13,4 +13,4 @@ def tst : MetaM Unit := do unsafe def main : IO Unit := do initSearchPath (← Lean.findSysroot) ["build/lib"] - withImportModules [{ module := `UserAttr.Tst : Import }] {} 0 fun env => pure () + withImportModules #[{ module := `UserAttr.Tst : Import }] {} 0 fun env => pure ()