chore: style
This commit is contained in:
Leonardo de Moura
parent
da416c12bc
commit
8207e05b0a
4 changed files with 207 additions and 220 deletions
|
|
@ -148,30 +148,29 @@ structure TagAttribute :=
|
|||
(ext : PersistentEnvExtension Name NameSet)
|
||||
|
||||
def registerTagAttribute (name : Name) (descr : String) (validate : Environment → Name → Except String Unit := fun _ _ => Except.ok ()) : IO TagAttribute :=
|
||||
do
|
||||
ext : PersistentEnvExtension Name NameSet ← registerPersistentEnvExtension {
|
||||
name := name,
|
||||
addImportedFn := fun _ => pure {},
|
||||
addEntryFn := fun (s : NameSet) n => s.insert n,
|
||||
exportEntriesFn := fun es =>
|
||||
let r : Array Name := es.fold (fun a e => a.push e) Array.empty;
|
||||
r.qsort Name.quickLt,
|
||||
statsFn := fun s => "tag attribute" ++ Format.line ++ "number of local entries: " ++ format s.size
|
||||
};
|
||||
let attrImpl : AttributeImpl := {
|
||||
name := name,
|
||||
descr := descr,
|
||||
add := fun env decl args persistent => do
|
||||
unless args.isMissing $ throw (IO.userError ("invalid attribute '" ++ toString name ++ "', unexpected argument"));
|
||||
unless persistent $ throw (IO.userError ("invalid attribute '" ++ toString name ++ "', must be persistent"));
|
||||
unless (env.getModuleIdxFor decl).isNone $
|
||||
throw (IO.userError ("invalid attribute '" ++ toString name ++ "', declaration is in an imported module"));
|
||||
match validate env decl with
|
||||
| Except.error msg => throw (IO.userError ("invalid attribute '" ++ toString name ++ "', " ++ msg))
|
||||
| _ => pure $ ext.addEntry env decl
|
||||
};
|
||||
registerAttribute attrImpl;
|
||||
pure { attr := attrImpl, ext := ext }
|
||||
do ext : PersistentEnvExtension Name NameSet ← registerPersistentEnvExtension {
|
||||
name := name,
|
||||
addImportedFn := fun _ => pure {},
|
||||
addEntryFn := fun (s : NameSet) n => s.insert n,
|
||||
exportEntriesFn := fun es =>
|
||||
let r : Array Name := es.fold (fun a e => a.push e) Array.empty;
|
||||
r.qsort Name.quickLt,
|
||||
statsFn := fun s => "tag attribute" ++ Format.line ++ "number of local entries: " ++ format s.size
|
||||
};
|
||||
let attrImpl : AttributeImpl := {
|
||||
name := name,
|
||||
descr := descr,
|
||||
add := fun env decl args persistent => do
|
||||
unless args.isMissing $ throw (IO.userError ("invalid attribute '" ++ toString name ++ "', unexpected argument"));
|
||||
unless persistent $ throw (IO.userError ("invalid attribute '" ++ toString name ++ "', must be persistent"));
|
||||
unless (env.getModuleIdxFor decl).isNone $
|
||||
throw (IO.userError ("invalid attribute '" ++ toString name ++ "', declaration is in an imported module"));
|
||||
match validate env decl with
|
||||
| Except.error msg => throw (IO.userError ("invalid attribute '" ++ toString name ++ "', " ++ msg))
|
||||
| _ => pure $ ext.addEntry env decl
|
||||
};
|
||||
registerAttribute attrImpl;
|
||||
pure { attr := attrImpl, ext := ext }
|
||||
|
||||
namespace TagAttribute
|
||||
|
||||
|
|
@ -197,33 +196,32 @@ structure ParametricAttribute (α : Type) :=
|
|||
def registerParametricAttribute {α : Type} [Inhabited α] (name : Name) (descr : String)
|
||||
(getParam : Environment → Name → Syntax → Except String α)
|
||||
(afterSet : Environment → Name → α → Except String Environment := fun env _ _ => Except.ok env) : IO (ParametricAttribute α) :=
|
||||
do
|
||||
ext : PersistentEnvExtension (Name × α) (NameMap α) ← registerPersistentEnvExtension {
|
||||
name := name,
|
||||
addImportedFn := fun _ => pure {},
|
||||
addEntryFn := fun (s : NameMap α) (p : Name × α) => s.insert p.1 p.2,
|
||||
exportEntriesFn := fun m =>
|
||||
let r : Array (Name × α) := m.fold (fun a n p => a.push (n, p)) Array.empty;
|
||||
r.qsort (fun a b => Name.quickLt a.1 b.1),
|
||||
statsFn := fun s => "parametric attribute" ++ Format.line ++ "number of local entries: " ++ format s.size
|
||||
};
|
||||
let attrImpl : AttributeImpl := {
|
||||
name := name,
|
||||
descr := descr,
|
||||
add := fun env decl args persistent => do
|
||||
unless persistent $ throw (IO.userError ("invalid attribute '" ++ toString name ++ "', must be persistent"));
|
||||
unless (env.getModuleIdxFor decl).isNone $
|
||||
throw (IO.userError ("invalid attribute '" ++ toString name ++ "', declaration is in an imported module"));
|
||||
match getParam env decl args with
|
||||
| Except.error msg => throw (IO.userError ("invalid attribute '" ++ toString name ++ "', " ++ msg))
|
||||
| Except.ok val => do
|
||||
let env := ext.addEntry env (decl, val);
|
||||
match afterSet env decl val with
|
||||
| Except.error msg => throw (IO.userError ("invalid attribute '" ++ toString name ++ "', " ++ msg))
|
||||
| Except.ok env => pure env
|
||||
};
|
||||
registerAttribute attrImpl;
|
||||
pure { attr := attrImpl, ext := ext }
|
||||
do ext : PersistentEnvExtension (Name × α) (NameMap α) ← registerPersistentEnvExtension {
|
||||
name := name,
|
||||
addImportedFn := fun _ => pure {},
|
||||
addEntryFn := fun (s : NameMap α) (p : Name × α) => s.insert p.1 p.2,
|
||||
exportEntriesFn := fun m =>
|
||||
let r : Array (Name × α) := m.fold (fun a n p => a.push (n, p)) Array.empty;
|
||||
r.qsort (fun a b => Name.quickLt a.1 b.1),
|
||||
statsFn := fun s => "parametric attribute" ++ Format.line ++ "number of local entries: " ++ format s.size
|
||||
};
|
||||
let attrImpl : AttributeImpl := {
|
||||
name := name,
|
||||
descr := descr,
|
||||
add := fun env decl args persistent => do
|
||||
unless persistent $ throw (IO.userError ("invalid attribute '" ++ toString name ++ "', must be persistent"));
|
||||
unless (env.getModuleIdxFor decl).isNone $
|
||||
throw (IO.userError ("invalid attribute '" ++ toString name ++ "', declaration is in an imported module"));
|
||||
match getParam env decl args with
|
||||
| Except.error msg => throw (IO.userError ("invalid attribute '" ++ toString name ++ "', " ++ msg))
|
||||
| Except.ok val => do
|
||||
let env := ext.addEntry env (decl, val);
|
||||
match afterSet env decl val with
|
||||
| Except.error msg => throw (IO.userError ("invalid attribute '" ++ toString name ++ "', " ++ msg))
|
||||
| Except.ok env => pure env
|
||||
};
|
||||
registerAttribute attrImpl;
|
||||
pure { attr := attrImpl, ext := ext }
|
||||
|
||||
namespace ParametricAttribute
|
||||
|
||||
|
|
@ -256,29 +254,28 @@ structure EnumAttributes (α : Type) :=
|
|||
(ext : PersistentEnvExtension (Name × α) (NameMap α))
|
||||
|
||||
def registerEnumAttributes {α : Type} [Inhabited α] (extName : Name) (attrDescrs : List (Name × String × α)) (validate : Environment → Name → α → Except String Unit := fun _ _ _ => Except.ok ()) : IO (EnumAttributes α) :=
|
||||
do
|
||||
ext : PersistentEnvExtension (Name × α) (NameMap α) ← registerPersistentEnvExtension {
|
||||
name := extName,
|
||||
addImportedFn := fun _ => pure {},
|
||||
addEntryFn := fun (s : NameMap α) (p : Name × α) => s.insert p.1 p.2,
|
||||
exportEntriesFn := fun m =>
|
||||
let r : Array (Name × α) := m.fold (fun a n p => a.push (n, p)) Array.empty;
|
||||
r.qsort (fun a b => Name.quickLt a.1 b.1),
|
||||
statsFn := fun s => "enumeration attribute extension" ++ Format.line ++ "number of local entries: " ++ format s.size
|
||||
};
|
||||
let attrs := attrDescrs.map $ fun ⟨name, descr, val⟩ => { AttributeImpl .
|
||||
name := name,
|
||||
descr := descr,
|
||||
add := fun env decl args persistent => do
|
||||
unless persistent $ throw (IO.userError ("invalid attribute '" ++ toString name ++ "', must be persistent"));
|
||||
unless (env.getModuleIdxFor decl).isNone $
|
||||
throw (IO.userError ("invalid attribute '" ++ toString name ++ "', declaration is in an imported module"));
|
||||
match validate env decl val with
|
||||
| Except.error msg => throw (IO.userError ("invalid attribute '" ++ toString name ++ "', " ++ msg))
|
||||
| _ => pure $ ext.addEntry env (decl, val)
|
||||
};
|
||||
attrs.mfor registerAttribute;
|
||||
pure { ext := ext, attrs := attrs }
|
||||
do ext : PersistentEnvExtension (Name × α) (NameMap α) ← registerPersistentEnvExtension {
|
||||
name := extName,
|
||||
addImportedFn := fun _ => pure {},
|
||||
addEntryFn := fun (s : NameMap α) (p : Name × α) => s.insert p.1 p.2,
|
||||
exportEntriesFn := fun m =>
|
||||
let r : Array (Name × α) := m.fold (fun a n p => a.push (n, p)) Array.empty;
|
||||
r.qsort (fun a b => Name.quickLt a.1 b.1),
|
||||
statsFn := fun s => "enumeration attribute extension" ++ Format.line ++ "number of local entries: " ++ format s.size
|
||||
};
|
||||
let attrs := attrDescrs.map $ fun ⟨name, descr, val⟩ => { AttributeImpl .
|
||||
name := name,
|
||||
descr := descr,
|
||||
add := fun env decl args persistent => do
|
||||
unless persistent $ throw (IO.userError ("invalid attribute '" ++ toString name ++ "', must be persistent"));
|
||||
unless (env.getModuleIdxFor decl).isNone $
|
||||
throw (IO.userError ("invalid attribute '" ++ toString name ++ "', declaration is in an imported module"));
|
||||
match validate env decl val with
|
||||
| Except.error msg => throw (IO.userError ("invalid attribute '" ++ toString name ++ "', " ++ msg))
|
||||
| _ => pure $ ext.addEntry env (decl, val)
|
||||
};
|
||||
attrs.mfor registerAttribute;
|
||||
pure { ext := ext, attrs := attrs }
|
||||
|
||||
namespace EnumAttributes
|
||||
|
||||
|
|
|
|||
|
|
@ -31,7 +31,7 @@ structure EnvironmentHeader :=
|
|||
(trustLevel : UInt32 := 0)
|
||||
(quotInit : Bool := false)
|
||||
(mainModule : Name := default _)
|
||||
(imports : Array Name := Array.empty)
|
||||
(imports : Array Name := #[])
|
||||
|
||||
/- TODO: mark opaque. -/
|
||||
structure Environment :=
|
||||
|
|
@ -43,7 +43,7 @@ structure Environment :=
|
|||
namespace Environment
|
||||
|
||||
instance : Inhabited Environment :=
|
||||
⟨{ const2ModIdx := {}, constants := {}, extensions := Array.empty }⟩
|
||||
⟨{ const2ModIdx := {}, constants := {}, extensions := #[] }⟩
|
||||
|
||||
def addAux (env : Environment) (cinfo : ConstantInfo) : Environment :=
|
||||
{ constants := env.constants.insert cinfo.name cinfo, .. env }
|
||||
|
|
@ -153,7 +153,7 @@ constant modifyState {σ : Type} (ext : EnvExtension σ) (env : Environment) (f
|
|||
end EnvExtension
|
||||
|
||||
private def mkEnvExtensionsRef : IO (IO.Ref (Array (EnvExtension EnvExtensionState))) :=
|
||||
IO.mkRef Array.empty
|
||||
IO.mkRef #[]
|
||||
|
||||
@[init mkEnvExtensionsRef]
|
||||
private constant envExtensionsRef : IO.Ref (Array (EnvExtension EnvExtensionState)) := default _
|
||||
|
|
@ -162,18 +162,17 @@ instance EnvExtension.Inhabited (σ : Type) [Inhabited σ] : Inhabited (EnvExten
|
|||
⟨{ idx := 0, stateInh := default _, mkInitial := default _ }⟩
|
||||
|
||||
unsafe def registerEnvExtensionUnsafe {σ : Type} [Inhabited σ] (mkInitial : IO σ) : IO (EnvExtension σ) :=
|
||||
do
|
||||
initializing ← IO.initializing;
|
||||
unless initializing $ throw (IO.userError ("failed to register environment, extensions can only be registered during initialization"));
|
||||
exts ← envExtensionsRef.get;
|
||||
let idx := exts.size;
|
||||
let ext : EnvExtension σ := {
|
||||
idx := idx,
|
||||
mkInitial := mkInitial,
|
||||
stateInh := default _
|
||||
};
|
||||
envExtensionsRef.modify (fun exts => exts.push (unsafeCast ext));
|
||||
pure ext
|
||||
do initializing ← IO.initializing;
|
||||
unless initializing $ throw (IO.userError ("failed to register environment, extensions can only be registered during initialization"));
|
||||
exts ← envExtensionsRef.get;
|
||||
let idx := exts.size;
|
||||
let ext : EnvExtension σ := {
|
||||
idx := idx,
|
||||
mkInitial := mkInitial,
|
||||
stateInh := default _
|
||||
};
|
||||
envExtensionsRef.modify (fun exts => exts.push (unsafeCast ext));
|
||||
pure ext
|
||||
|
||||
/- Environment extensions can only be registered during initialization.
|
||||
Reasons:
|
||||
|
|
@ -187,14 +186,13 @@ do exts ← envExtensionsRef.get; exts.mmap $ fun ext => ext.mkInitial
|
|||
|
||||
@[export lean_mk_empty_environment]
|
||||
def mkEmptyEnvironment (trustLevel : UInt32 := 0) : IO Environment :=
|
||||
do
|
||||
initializing ← IO.initializing;
|
||||
when initializing $ throw (IO.userError "environment objects cannot be created during initialization");
|
||||
exts ← mkInitialExtensionStates;
|
||||
pure { const2ModIdx := {},
|
||||
constants := {},
|
||||
header := { trustLevel := trustLevel },
|
||||
extensions := exts }
|
||||
do initializing ← IO.initializing;
|
||||
when initializing $ throw (IO.userError "environment objects cannot be created during initialization");
|
||||
exts ← mkInitialExtensionStates;
|
||||
pure { const2ModIdx := {},
|
||||
constants := {},
|
||||
header := { trustLevel := trustLevel },
|
||||
extensions := exts }
|
||||
|
||||
structure PersistentEnvExtensionState (α : Type) (σ : Type) :=
|
||||
(importedEntries : Array (Array α)) -- entries per imported module
|
||||
|
|
@ -219,14 +217,14 @@ def EnvExtensionEntry := NonScalar
|
|||
instance EnvExtensionEntry.inhabited : Inhabited EnvExtensionEntry := inferInstanceAs (Inhabited NonScalar)
|
||||
|
||||
instance PersistentEnvExtensionState.inhabited {α σ} [Inhabited σ] : Inhabited (PersistentEnvExtensionState α σ) :=
|
||||
⟨{importedEntries := Array.empty, state := default _ }⟩
|
||||
⟨{importedEntries := #[], state := default _ }⟩
|
||||
|
||||
instance PersistentEnvExtension.inhabited {α σ} [Inhabited σ] : Inhabited (PersistentEnvExtension α σ) :=
|
||||
⟨{ toEnvExtension := { idx := 0, stateInh := default _, mkInitial := default _ },
|
||||
name := default _,
|
||||
addImportedFn := fun _ => default _,
|
||||
addEntryFn := fun s _ => s,
|
||||
exportEntriesFn := fun _ => Array.empty,
|
||||
exportEntriesFn := fun _ => #[],
|
||||
statsFn := fun _ => Format.nil }⟩
|
||||
|
||||
namespace PersistentEnvExtension
|
||||
|
|
@ -251,7 +249,7 @@ ext.toEnvExtension.modifyState env $ fun ps => { state := f (ps.state), .. ps }
|
|||
end PersistentEnvExtension
|
||||
|
||||
private def mkPersistentEnvExtensionsRef : IO (IO.Ref (Array (PersistentEnvExtension EnvExtensionEntry EnvExtensionState))) :=
|
||||
IO.mkRef Array.empty
|
||||
IO.mkRef #[]
|
||||
|
||||
@[init mkPersistentEnvExtensionsRef]
|
||||
private constant persistentEnvExtensionsRef : IO.Ref (Array (PersistentEnvExtension EnvExtensionEntry EnvExtensionState)) := default _
|
||||
|
|
@ -264,26 +262,25 @@ structure PersistentEnvExtensionDescr (α σ : Type) :=
|
|||
(statsFn : σ → Format := fun _ => Format.nil)
|
||||
|
||||
unsafe def registerPersistentEnvExtensionUnsafe {α σ : Type} [Inhabited σ] (descr : PersistentEnvExtensionDescr α σ) : IO (PersistentEnvExtension α σ) :=
|
||||
do
|
||||
pExts ← persistentEnvExtensionsRef.get;
|
||||
when (pExts.any (fun ext => ext.name == descr.name)) $ throw (IO.userError ("invalid environment extension, '" ++ toString descr.name ++ "' has already been used"));
|
||||
ext ← registerEnvExtension (do
|
||||
state ← descr.addImportedFn Array.empty;
|
||||
let s : PersistentEnvExtensionState α σ := {
|
||||
importedEntries := Array.empty,
|
||||
state := state
|
||||
};
|
||||
pure s);
|
||||
let pExt : PersistentEnvExtension α σ := {
|
||||
toEnvExtension := ext,
|
||||
name := descr.name,
|
||||
addImportedFn := descr.addImportedFn,
|
||||
addEntryFn := descr.addEntryFn,
|
||||
exportEntriesFn := descr.exportEntriesFn,
|
||||
statsFn := descr.statsFn
|
||||
};
|
||||
persistentEnvExtensionsRef.modify (fun pExts => pExts.push (unsafeCast pExt));
|
||||
pure pExt
|
||||
do pExts ← persistentEnvExtensionsRef.get;
|
||||
when (pExts.any (fun ext => ext.name == descr.name)) $ throw (IO.userError ("invalid environment extension, '" ++ toString descr.name ++ "' has already been used"));
|
||||
ext ← registerEnvExtension (do
|
||||
state ← descr.addImportedFn #[];
|
||||
let s : PersistentEnvExtensionState α σ := {
|
||||
importedEntries := #[],
|
||||
state := state
|
||||
};
|
||||
pure s);
|
||||
let pExt : PersistentEnvExtension α σ := {
|
||||
toEnvExtension := ext,
|
||||
name := descr.name,
|
||||
addImportedFn := descr.addImportedFn,
|
||||
addEntryFn := descr.addEntryFn,
|
||||
exportEntriesFn := descr.exportEntriesFn,
|
||||
statsFn := descr.statsFn
|
||||
};
|
||||
persistentEnvExtensionsRef.modify (fun pExts => pExts.push (unsafeCast pExt));
|
||||
pure pExt
|
||||
|
||||
@[implementedBy registerPersistentEnvExtensionUnsafe]
|
||||
constant registerPersistentEnvExtension {α σ : Type} [Inhabited σ] (descr : PersistentEnvExtensionDescr α σ) : IO (PersistentEnvExtension α σ) := default _
|
||||
|
|
@ -403,22 +400,21 @@ constant saveModuleData (fname : @& String) (m : ModuleData) : IO Unit := defaul
|
|||
constant readModuleData (fname : @& String) : IO ModuleData := default _
|
||||
|
||||
def mkModuleData (env : Environment) : IO ModuleData :=
|
||||
do
|
||||
pExts ← persistentEnvExtensionsRef.get;
|
||||
let entries : Array (Name × Array EnvExtensionEntry) := pExts.size.fold
|
||||
(fun i result =>
|
||||
let state := (pExts.get! i).getState env;
|
||||
let exportEntriesFn := (pExts.get! i).exportEntriesFn;
|
||||
let extName := (pExts.get! i).name;
|
||||
result.push (extName, exportEntriesFn state))
|
||||
Array.empty;
|
||||
bytes ← serializeModifications (modListExtension.getState env);
|
||||
pure {
|
||||
imports := env.header.imports,
|
||||
constants := env.constants.foldStage2 (fun cs _ c => cs.push c) Array.empty,
|
||||
entries := entries,
|
||||
serialized := bytes
|
||||
}
|
||||
do pExts ← persistentEnvExtensionsRef.get;
|
||||
let entries : Array (Name × Array EnvExtensionEntry) := pExts.size.fold
|
||||
(fun i result =>
|
||||
let state := (pExts.get! i).getState env;
|
||||
let exportEntriesFn := (pExts.get! i).exportEntriesFn;
|
||||
let extName := (pExts.get! i).name;
|
||||
result.push (extName, exportEntriesFn state))
|
||||
#[];
|
||||
bytes ← serializeModifications (modListExtension.getState env);
|
||||
pure {
|
||||
imports := env.header.imports,
|
||||
constants := env.constants.foldStage2 (fun cs _ c => cs.push c) #[],
|
||||
entries := entries,
|
||||
serialized := bytes
|
||||
}
|
||||
|
||||
@[export lean_write_module]
|
||||
def writeModule (env : Environment) (fname : String) : IO Unit :=
|
||||
|
|
@ -443,54 +439,51 @@ private partial def getEntriesFor (mod : ModuleData) (extId : Name) : Nat → Ar
|
|||
let curr := mod.entries.get! i;
|
||||
if curr.1 == extId then curr.2 else getEntriesFor (i+1)
|
||||
else
|
||||
Array.empty
|
||||
#[]
|
||||
|
||||
private def setImportedEntries (env : Environment) (mods : Array ModuleData) : IO Environment :=
|
||||
do
|
||||
pExtDescrs ← persistentEnvExtensionsRef.get;
|
||||
pure $ mods.iterate env $ fun _ mod env =>
|
||||
pExtDescrs.iterate env $ fun _ extDescr env =>
|
||||
let entries := getEntriesFor mod extDescr.name 0;
|
||||
extDescr.toEnvExtension.modifyState env $ fun s =>
|
||||
{ importedEntries := s.importedEntries.push entries,
|
||||
.. s }
|
||||
do pExtDescrs ← persistentEnvExtensionsRef.get;
|
||||
pure $ mods.iterate env $ fun _ mod env =>
|
||||
pExtDescrs.iterate env $ fun _ extDescr env =>
|
||||
let entries := getEntriesFor mod extDescr.name 0;
|
||||
extDescr.toEnvExtension.modifyState env $ fun s =>
|
||||
{ importedEntries := s.importedEntries.push entries,
|
||||
.. s }
|
||||
|
||||
private def finalizePersistentExtensions (env : Environment) : IO Environment :=
|
||||
do
|
||||
pExtDescrs ← persistentEnvExtensionsRef.get;
|
||||
pExtDescrs.miterate env $ fun _ extDescr env => do
|
||||
let s := extDescr.toEnvExtension.getState env;
|
||||
newState ← extDescr.addImportedFn s.importedEntries;
|
||||
pure $ extDescr.toEnvExtension.setState env { state := newState, .. s }
|
||||
do pExtDescrs ← persistentEnvExtensionsRef.get;
|
||||
pExtDescrs.miterate env $ fun _ extDescr env => do
|
||||
let s := extDescr.toEnvExtension.getState env;
|
||||
newState ← extDescr.addImportedFn s.importedEntries;
|
||||
pure $ extDescr.toEnvExtension.setState env { state := newState, .. s }
|
||||
|
||||
@[export lean_import_modules]
|
||||
def importModules (modNames : List Name) (trustLevel : UInt32 := 0) : IO Environment :=
|
||||
do
|
||||
(_, mods) ← importModulesAux modNames ({}, Array.empty);
|
||||
let const2ModIdx := mods.iterate {} $ fun (modIdx) (mod : ModuleData) (m : HashMap Name ModuleIdx) =>
|
||||
mod.constants.iterate m $ fun _ cinfo m =>
|
||||
m.insert cinfo.name modIdx.val;
|
||||
constants ← mods.miterate SMap.empty $ fun _ (mod : ModuleData) (cs : ConstMap) =>
|
||||
mod.constants.miterate cs $ fun _ cinfo cs => do {
|
||||
when (cs.contains cinfo.name) $ throw (IO.userError ("import failed, environment already contains '" ++ toString cinfo.name ++ "'"));
|
||||
pure $ cs.insert cinfo.name cinfo
|
||||
};
|
||||
let constants := constants.switch;
|
||||
exts ← mkInitialExtensionStates;
|
||||
let env : Environment := {
|
||||
const2ModIdx := const2ModIdx,
|
||||
constants := constants,
|
||||
extensions := exts,
|
||||
header := {
|
||||
quotInit := !modNames.isEmpty, -- We assume `core.lean` initializes quotient module
|
||||
trustLevel := trustLevel,
|
||||
imports := modNames.toArray
|
||||
}
|
||||
};
|
||||
env ← setImportedEntries env mods;
|
||||
env ← finalizePersistentExtensions env;
|
||||
env ← mods.miterate env $ fun _ mod env => performModifications env mod.serialized;
|
||||
pure env
|
||||
do (_, mods) ← importModulesAux modNames ({}, #[]);
|
||||
let const2ModIdx := mods.iterate {} $ fun (modIdx) (mod : ModuleData) (m : HashMap Name ModuleIdx) =>
|
||||
mod.constants.iterate m $ fun _ cinfo m =>
|
||||
m.insert cinfo.name modIdx.val;
|
||||
constants ← mods.miterate SMap.empty $ fun _ (mod : ModuleData) (cs : ConstMap) =>
|
||||
mod.constants.miterate cs $ fun _ cinfo cs => do {
|
||||
when (cs.contains cinfo.name) $ throw (IO.userError ("import failed, environment already contains '" ++ toString cinfo.name ++ "'"));
|
||||
pure $ cs.insert cinfo.name cinfo
|
||||
};
|
||||
let constants := constants.switch;
|
||||
exts ← mkInitialExtensionStates;
|
||||
let env : Environment := {
|
||||
const2ModIdx := const2ModIdx,
|
||||
constants := constants,
|
||||
extensions := exts,
|
||||
header := {
|
||||
quotInit := !modNames.isEmpty, -- We assume `core.lean` initializes quotient module
|
||||
trustLevel := trustLevel,
|
||||
imports := modNames.toArray
|
||||
}
|
||||
};
|
||||
env ← setImportedEntries env mods;
|
||||
env ← finalizePersistentExtensions env;
|
||||
env ← mods.miterate env $ fun _ mod env => performModifications env mod.serialized;
|
||||
pure env
|
||||
|
||||
def regNamespacesExtension : IO (SimplePersistentEnvExtension Name NameSet) :=
|
||||
registerSimplePersistentEnvExtension {
|
||||
|
|
@ -529,26 +522,25 @@ env.addAux cinfo
|
|||
|
||||
@[export lean_display_stats]
|
||||
def displayStats (env : Environment) : IO Unit :=
|
||||
do
|
||||
pExtDescrs ← persistentEnvExtensionsRef.get;
|
||||
let numModules := ((pExtDescrs.get! 0).toEnvExtension.getState env).importedEntries.size;
|
||||
IO.println ("direct imports: " ++ toString env.header.imports);
|
||||
IO.println ("number of imported modules: " ++ toString numModules);
|
||||
IO.println ("number of consts: " ++ toString env.constants.size);
|
||||
IO.println ("number of imported consts: " ++ toString env.constants.stageSizes.1);
|
||||
IO.println ("number of local consts: " ++ toString env.constants.stageSizes.2);
|
||||
IO.println ("number of buckets for imported consts: " ++ toString env.constants.numBuckets);
|
||||
IO.println ("trust level: " ++ toString env.header.trustLevel);
|
||||
IO.println ("number of extensions: " ++ toString env.extensions.size);
|
||||
pExtDescrs.mfor $ fun extDescr => do {
|
||||
IO.println ("extension '" ++ toString extDescr.name ++ "'");
|
||||
let s := extDescr.toEnvExtension.getState env;
|
||||
let fmt := extDescr.statsFn s.state;
|
||||
unless fmt.isNil (IO.println (" " ++ toString (Format.nest 2 (extDescr.statsFn s.state))));
|
||||
IO.println (" number of imported entries: " ++ toString (s.importedEntries.foldl (fun sum es => sum + es.size) 0));
|
||||
pure ()
|
||||
};
|
||||
pure ()
|
||||
do pExtDescrs ← persistentEnvExtensionsRef.get;
|
||||
let numModules := ((pExtDescrs.get! 0).toEnvExtension.getState env).importedEntries.size;
|
||||
IO.println ("direct imports: " ++ toString env.header.imports);
|
||||
IO.println ("number of imported modules: " ++ toString numModules);
|
||||
IO.println ("number of consts: " ++ toString env.constants.size);
|
||||
IO.println ("number of imported consts: " ++ toString env.constants.stageSizes.1);
|
||||
IO.println ("number of local consts: " ++ toString env.constants.stageSizes.2);
|
||||
IO.println ("number of buckets for imported consts: " ++ toString env.constants.numBuckets);
|
||||
IO.println ("trust level: " ++ toString env.header.trustLevel);
|
||||
IO.println ("number of extensions: " ++ toString env.extensions.size);
|
||||
pExtDescrs.mfor $ fun extDescr => do {
|
||||
IO.println ("extension '" ++ toString extDescr.name ++ "'");
|
||||
let s := extDescr.toEnvExtension.getState env;
|
||||
let fmt := extDescr.statsFn s.state;
|
||||
unless fmt.isNil (IO.println (" " ++ toString (Format.nest 2 (extDescr.statsFn s.state))));
|
||||
IO.println (" number of imported entries: " ++ toString (s.importedEntries.foldl (fun sum es => sum + es.size) 0));
|
||||
pure ()
|
||||
};
|
||||
pure ()
|
||||
|
||||
end Environment
|
||||
end Lean
|
||||
|
|
|
|||
|
|
@ -89,10 +89,9 @@ def addRel (baseDir : String) : Nat → String
|
|||
| n+1 => addRel n ++ pathSep ++ ".."
|
||||
|
||||
def findLeanFile (modName : Name) (ext : String) : IO String :=
|
||||
do
|
||||
let fname := modNameToFileName modName;
|
||||
some fname ← findFile fname ext | throw (IO.userError ("module '" ++ toString modName ++ "' not found"));
|
||||
realPathNormalized fname
|
||||
do let fname := modNameToFileName modName;
|
||||
some fname ← findFile fname ext | throw (IO.userError ("module '" ++ toString modName ++ "' not found"));
|
||||
realPathNormalized fname
|
||||
|
||||
def findOLean (modName : Name) : IO String :=
|
||||
findLeanFile modName "olean"
|
||||
|
|
@ -110,22 +109,21 @@ do fname ← realPathNormalized fname;
|
|||
|
||||
@[export lean_module_name_of_file]
|
||||
def moduleNameOfFileName (fname : String) : IO Name :=
|
||||
do
|
||||
path ← findAtSearchPath fname;
|
||||
fname ← realPathNormalized fname;
|
||||
let fnameSuffix := fname.drop path.length;
|
||||
let fnameSuffix := if fnameSuffix.get 0 == pathSeparator then fnameSuffix.drop 1 else fnameSuffix;
|
||||
if path ++ pathSep ++ fnameSuffix != fname then
|
||||
throw (IO.userError ("failed to convert file '" ++ fname ++ "' to module name, path is not a prefix of the given file"))
|
||||
else do
|
||||
some extPos ← pure (fnameSuffix.revPosOf '.')
|
||||
| throw (IO.userError ("failed to convert file '" ++ fname ++ "' to module name, extension is missing"));
|
||||
let modNameStr := fnameSuffix.extract 0 extPos;
|
||||
let extStr := fnameSuffix.extract (extPos + 1) fnameSuffix.bsize;
|
||||
let parts := modNameStr.split pathSep;
|
||||
let modName := parts.foldl Name.mkString Name.anonymous;
|
||||
fname' ← findLeanFile modName extStr;
|
||||
unless (fname == fname') $ throw (IO.userError ("failed to convert file '" ++ fname ++ "' to module name, module name '" ++ toString modName ++ "' resolves to '" ++ fname' ++ "'"));
|
||||
pure modName
|
||||
do path ← findAtSearchPath fname;
|
||||
fname ← realPathNormalized fname;
|
||||
let fnameSuffix := fname.drop path.length;
|
||||
let fnameSuffix := if fnameSuffix.get 0 == pathSeparator then fnameSuffix.drop 1 else fnameSuffix;
|
||||
if path ++ pathSep ++ fnameSuffix != fname then
|
||||
throw (IO.userError ("failed to convert file '" ++ fname ++ "' to module name, path is not a prefix of the given file"))
|
||||
else do
|
||||
some extPos ← pure (fnameSuffix.revPosOf '.')
|
||||
| throw (IO.userError ("failed to convert file '" ++ fname ++ "' to module name, extension is missing"));
|
||||
let modNameStr := fnameSuffix.extract 0 extPos;
|
||||
let extStr := fnameSuffix.extract (extPos + 1) fnameSuffix.bsize;
|
||||
let parts := modNameStr.split pathSep;
|
||||
let modName := parts.foldl Name.mkString Name.anonymous;
|
||||
fname' ← findLeanFile modName extStr;
|
||||
unless (fname == fname') $ throw (IO.userError ("failed to convert file '" ++ fname ++ "' to module name, module name '" ++ toString modName ++ "' resolves to '" ++ fname' ++ "'"));
|
||||
pure modName
|
||||
|
||||
end Lean
|
||||
|
|
|
|||
|
|
@ -146,7 +146,7 @@ def isOfKind {α} : Syntax α → SyntaxNodeKind → Bool
|
|||
|
||||
def asNode {α} : Syntax α → SyntaxNode α
|
||||
| Syntax.node kind args => ⟨Syntax.node kind args, IsNode.mk kind args⟩
|
||||
| _ => ⟨Syntax.node nullKind Array.empty, IsNode.mk nullKind Array.empty⟩
|
||||
| _ => ⟨Syntax.node nullKind #[], IsNode.mk nullKind #[]⟩
|
||||
|
||||
def getNumArgs {α} (stx : Syntax α) : Nat :=
|
||||
stx.asNode.getNumArgs
|
||||
|
|
@ -354,7 +354,7 @@ Syntax.node nullKind args.toArray
|
|||
def mkOptionalNode {α} (arg : Option (Syntax α)) : Syntax α :=
|
||||
match arg with
|
||||
| some arg => Syntax.node nullKind #[arg]
|
||||
| none => Syntax.node nullKind Array.empty
|
||||
| none => Syntax.node nullKind #[]
|
||||
|
||||
/- Helper functions for creating string and numeric literals -/
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue