chore: split up & simplify importModules
This commit is contained in:
tydeu
Mac Malone
parent
b2119313bd
commit
926663505e
12 changed files with 109 additions and 103 deletions
|
|
@ -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 "<input>"
|
||||
let inputCtx := Parser.mkInputContext input fileName
|
||||
let (header, parserState, messages) ← Parser.parseHeader inputCtx
|
||||
|
|
|
|||
|
|
@ -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,20 +733,34 @@ 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}"
|
||||
|
||||
@[export lean_import_modules]
|
||||
partial def importModules (imports : List Import) (opts : Options) (trustLevel : UInt32 := 0) : IO Environment := profileitIO "import" opts do
|
||||
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
|
||||
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 mod in s.moduleData do
|
||||
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) =>
|
||||
|
|
@ -754,7 +770,6 @@ partial def importModules (imports : List Import) (opts : Options) (trustLevel :
|
|||
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 := {
|
||||
|
|
@ -765,7 +780,7 @@ partial def importModules (imports : List Import) (opts : Options) (trustLevel :
|
|||
header := {
|
||||
quotInit := !imports.isEmpty -- We assume `core.lean` initializes quotient module
|
||||
trustLevel := trustLevel
|
||||
imports := imports.toArray
|
||||
imports := imports
|
||||
regions := s.regions
|
||||
moduleNames := s.moduleNames
|
||||
moduleData := s.moduleData
|
||||
|
|
@ -774,30 +789,21 @@ partial def importModules (imports : List Import) (opts : Options) (trustLevel :
|
|||
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
|
||||
|
||||
@[export lean_import_modules]
|
||||
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) ← 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
|
||||
|
||||
|
|
|
|||
|
|
@ -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`
|
||||
|
|
|
|||
|
|
@ -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 := "<test>", fileMap := default } { env }
|
||||
IO.println "ok"
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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 "---";
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
|
|
|||
|
|
@ -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])
|
||||
|
|
|
|||
|
|
@ -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)]))
|
||||
|
|
|
|||
|
|
@ -21,7 +21,7 @@ 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 :=
|
||||
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 };
|
||||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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 ()
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue