chore: hash field in Name was dropped
This commit is contained in:
Gabriel Ebner
tydeu
parent
5cd2d85515
commit
f76b488fd5
25 changed files with 190 additions and 383 deletions
|
|
@ -21,7 +21,7 @@ for the `lean.imports` facet or an active build target for `lean.c`.
|
|||
It is an open type, meaning additional mappings can be add lazily
|
||||
as needed (via `module_data`).
|
||||
-/
|
||||
opaque ModuleData (facet : WfName) : Type
|
||||
opaque ModuleData (facet : Name) : Type
|
||||
|
||||
/--
|
||||
The open type family which maps a package facet's name to it build data
|
||||
|
|
@ -31,7 +31,7 @@ for the facet `deps`.
|
|||
It is an open type, meaning additional mappings can be add lazily
|
||||
as needed (via `package_data`).
|
||||
-/
|
||||
opaque PackageData (facet : WfName) : Type
|
||||
opaque PackageData (facet : Name) : Type
|
||||
|
||||
/--
|
||||
The open type family which maps a (builtin) Lake target's (e.g., `extern_lib`)
|
||||
|
|
@ -41,7 +41,7 @@ the `externLib.static` facet.
|
|||
It is an open type, meaning additional mappings can be add lazily
|
||||
as needed (via `target_data`).
|
||||
-/
|
||||
opaque TargetData (facet : WfName) : Type
|
||||
opaque TargetData (facet : Name) : Type
|
||||
|
||||
/--
|
||||
The open type family which maps a custom target (package × target name) to
|
||||
|
|
@ -50,7 +50,7 @@ its build data in the Lake build store.
|
|||
It is an open type, meaning additional mappings can be add lazily
|
||||
as needed (via `custom_data`).
|
||||
-/
|
||||
opaque CustomData (target : WfName × WfName) : Type
|
||||
opaque CustomData (target : Name × Name) : Type
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
/-! ## Build Data -/
|
||||
|
|
@ -75,21 +75,21 @@ abbrev BuildData : BuildKey → Type
|
|||
scoped macro (name := packageDataDecl) doc?:optional(Parser.Command.docComment)
|
||||
"package_data " id:ident " : " ty:term : command => do
|
||||
let dty := mkCIdentFrom (← getRef) ``PackageData
|
||||
let key := WfName.quoteNameFrom id id.getId
|
||||
let key := Lake.quoteNameFrom id id.getId
|
||||
`($[$doc?]? family_def $id : $dty $key := $ty)
|
||||
|
||||
/-- Macro for declaring new `ModuleData`. -/
|
||||
scoped macro (name := moduleDataDecl) doc?:optional(Parser.Command.docComment)
|
||||
"module_data " id:ident " : " ty:term : command => do
|
||||
let dty := mkCIdentFrom (← getRef) ``ModuleData
|
||||
let key := WfName.quoteNameFrom id id.getId
|
||||
let key := Lake.quoteNameFrom id id.getId
|
||||
`($[$doc?]? family_def $id : $dty $key := $ty)
|
||||
|
||||
/-- Macro for declaring new `TargetData`. -/
|
||||
scoped macro (name := targetDataDecl) doc?:optional(Parser.Command.docComment)
|
||||
"target_data " id:ident " : " ty:term : command => do
|
||||
let dty := mkCIdentFrom (← getRef) ``TargetData
|
||||
let key := WfName.quoteNameFrom id id.getId
|
||||
let key := Lake.quoteNameFrom id id.getId
|
||||
`($[$doc?]? family_def $id : $dty $key := $ty)
|
||||
|
||||
/-- Macro for declaring new `CustomData`. -/
|
||||
|
|
@ -97,6 +97,6 @@ scoped macro (name := customDataDecl) doc?:optional(Parser.Command.docComment)
|
|||
"custom_data " pkg:ident tgt:ident " : " ty:term : command => do
|
||||
let dty := mkCIdentFrom (← getRef) ``CustomData
|
||||
let id := mkIdentFrom tgt (pkg.getId ++ tgt.getId)
|
||||
let pkg := WfName.quoteNameFrom pkg pkg.getId
|
||||
let tgt := WfName.quoteNameFrom tgt tgt.getId
|
||||
let pkg := Lake.quoteNameFrom pkg pkg.getId
|
||||
let tgt := Lake.quoteNameFrom pkg tgt.getId
|
||||
`($[$doc?]? family_def $id : $dty ($pkg, $tgt) := $ty)
|
||||
|
|
|
|||
|
|
@ -22,7 +22,7 @@ namespace Lake
|
|||
/-- A module facet name along with proof of its data type. -/
|
||||
structure ModuleFacet (α) where
|
||||
/-- The name of the module facet. -/
|
||||
name : WfName
|
||||
name : Name
|
||||
/-- Proof that module's facet build result is of type α. -/
|
||||
data_eq : ModuleData name = α
|
||||
deriving Repr
|
||||
|
|
@ -30,16 +30,16 @@ structure ModuleFacet (α) where
|
|||
instance (facet : ModuleFacet α) : FamilyDef ModuleData facet.name α :=
|
||||
⟨facet.data_eq⟩
|
||||
|
||||
instance [FamilyDef ModuleData facet α] : CoeDep WfName facet (ModuleFacet α) :=
|
||||
instance [FamilyDef ModuleData facet α] : CoeDep Name facet (ModuleFacet α) :=
|
||||
⟨facet, family_key_eq_type⟩
|
||||
|
||||
namespace Module
|
||||
abbrev leanBinFacet := &`lean.bin
|
||||
abbrev oleanFacet := &`olean
|
||||
abbrev ileanFacet := &`ilean
|
||||
abbrev cFacet := &`lean.c
|
||||
abbrev oFacet := &`lean.o
|
||||
abbrev dynlibFacet := &`dynlib
|
||||
abbrev leanBinFacet := `lean.bin
|
||||
abbrev oleanFacet := `olean
|
||||
abbrev ileanFacet := `ilean
|
||||
abbrev cFacet := `lean.c
|
||||
abbrev oFacet := `lean.o
|
||||
abbrev dynlibFacet := `dynlib
|
||||
end Module
|
||||
|
||||
/--
|
||||
|
|
@ -72,11 +72,11 @@ package_data extraDep : ActiveOpaqueTarget
|
|||
|
||||
-- ## Target Facets
|
||||
|
||||
abbrev LeanLib.staticFacet := &`leanLib.static
|
||||
abbrev LeanLib.sharedFacet := &`leanLib.shared
|
||||
abbrev LeanExe.exeFacet := &`leanExe
|
||||
abbrev ExternLib.staticFacet := &`externLib.static
|
||||
abbrev ExternLib.sharedFacet := &`externLib.shared
|
||||
abbrev LeanLib.staticFacet := `leanLib.static
|
||||
abbrev LeanLib.sharedFacet := `leanLib.shared
|
||||
abbrev LeanExe.exeFacet := `leanExe
|
||||
abbrev ExternLib.staticFacet := `externLib.static
|
||||
abbrev ExternLib.sharedFacet := `externLib.shared
|
||||
|
||||
/-- A Lean library's static binary. -/
|
||||
target_data leanLib.static : ActiveFileTarget
|
||||
|
|
|
|||
|
|
@ -27,21 +27,21 @@ namespace Lake
|
|||
|
||||
/-- A map from module facet names to build functions. -/
|
||||
abbrev ModuleBuildMap (m : Type → Type v) :=
|
||||
DRBMap WfName (cmp := WfName.quickCmp) fun k =>
|
||||
DRBMap Name (cmp := Name.quickCmp) fun k =>
|
||||
Module → IndexBuildFn m → m (ModuleData k)
|
||||
|
||||
@[inline] def ModuleBuildMap.empty : ModuleBuildMap m := DRBMap.empty
|
||||
|
||||
/-- A map from package facet names to build functions. -/
|
||||
abbrev PackageBuildMap (m : Type → Type v) :=
|
||||
DRBMap WfName (cmp := WfName.quickCmp) fun k =>
|
||||
DRBMap Name (cmp := Name.quickCmp) fun k =>
|
||||
Package → IndexBuildFn m → m (PackageData k)
|
||||
|
||||
@[inline] def PackageBuildMap.empty : PackageBuildMap m := DRBMap.empty
|
||||
|
||||
/-- A map from target facet names to build functions. -/
|
||||
abbrev TargetBuildMap (m : Type → Type v) :=
|
||||
DRBMap WfName (cmp := WfName.quickCmp) fun k =>
|
||||
DRBMap Name (cmp := Name.quickCmp) fun k =>
|
||||
Package → IndexBuildFn m → m (PackageData k)
|
||||
|
||||
@[inline] def TargetBuildMap.empty : PackageBuildMap m := DRBMap.empty
|
||||
|
|
@ -54,7 +54,7 @@ abbrev TargetBuildMap (m : Type → Type v) :=
|
|||
Converts a conveniently typed module facet build function into its
|
||||
dynamically typed equivalent.
|
||||
-/
|
||||
@[inline] def mkModuleFacetBuild {facet : WfName} (build : Module → IndexT m α)
|
||||
@[inline] def mkModuleFacetBuild {facet : Name} (build : Module → IndexT m α)
|
||||
[h : FamilyDef ModuleData facet α] : Module → IndexT m (ModuleData facet) :=
|
||||
cast (by rw [← h.family_key_eq_type]) build
|
||||
|
||||
|
|
@ -62,7 +62,7 @@ dynamically typed equivalent.
|
|||
Converts a conveniently typed package facet build function into its
|
||||
dynamically typed equivalent.
|
||||
-/
|
||||
@[inline] def mkPackageFacetBuild {facet : WfName} (build : Package → IndexT m α)
|
||||
@[inline] def mkPackageFacetBuild {facet : Name} (build : Package → IndexT m α)
|
||||
[h : FamilyDef PackageData facet α] : Package → IndexT m (PackageData facet) :=
|
||||
cast (by rw [← h.family_key_eq_type]) build
|
||||
|
||||
|
|
@ -70,7 +70,7 @@ dynamically typed equivalent.
|
|||
Converts a conveniently typed target facet build function into its
|
||||
dynamically typed equivalent.
|
||||
-/
|
||||
@[inline] def mkTargetFacetBuild (facet : WfName) (build : IndexT m α)
|
||||
@[inline] def mkTargetFacetBuild (facet : Name) (build : IndexT m α)
|
||||
[h : FamilyDef TargetData facet α] : IndexT m (TargetData facet) :=
|
||||
cast (by rw [← h.family_key_eq_type]) build
|
||||
|
||||
|
|
@ -111,12 +111,12 @@ the initial set of Lake package facets (e.g., `extraDep`).
|
|||
have : MonadLift BuildM m := ⟨liftM⟩
|
||||
PackageBuildMap.empty (m := m)
|
||||
-- Compute the package's transitive dependencies
|
||||
|>.insert &`deps (mkPackageFacetBuild <| fun pkg => do
|
||||
|>.insert `deps (mkPackageFacetBuild <| fun pkg => do
|
||||
let mut deps := #[]
|
||||
let mut depSet := PackageSet.empty
|
||||
for dep in pkg.dependencies do
|
||||
if let some depPkg ← findPackage? dep.name then
|
||||
for depDepPkg in (← recBuild <| depPkg.facet &`deps) do
|
||||
for depDepPkg in (← recBuild <| depPkg.facet `deps) do
|
||||
unless depSet.contains depDepPkg do
|
||||
deps := deps.push depDepPkg
|
||||
depSet := depSet.insert depDepPkg
|
||||
|
|
@ -126,7 +126,7 @@ the initial set of Lake package facets (e.g., `extraDep`).
|
|||
return deps
|
||||
)
|
||||
-- Build the `extraDepTarget` for the package and its transitive dependencies
|
||||
|>.insert &`extraDep (mkPackageFacetBuild <| fun pkg => do
|
||||
|>.insert `extraDep (mkPackageFacetBuild <| fun pkg => do
|
||||
let mut target := ActiveTarget.nil
|
||||
for dep in pkg.dependencies do
|
||||
if let some depPkg ← findPackage? dep.name then
|
||||
|
|
|
|||
|
|
@ -12,7 +12,7 @@ namespace Lake
|
|||
|
||||
-- # Module Facet Targets
|
||||
|
||||
@[inline] def Module.facetTarget (facet : WfName) (self : Module)
|
||||
@[inline] def Module.facetTarget (facet : Name) (self : Module)
|
||||
[FamilyDef ModuleData facet (ActiveBuildTarget α)] : OpaqueTarget :=
|
||||
self.facet facet |>.target
|
||||
|
||||
|
|
@ -35,7 +35,7 @@ Build the `extraDepTarget` of a package and its (transitive) dependencies
|
|||
and then build the target `facet` of library's modules recursively, constructing
|
||||
a single opaque target for the whole build.
|
||||
-/
|
||||
def LeanLib.buildModules (self : LeanLib) (facet : WfName)
|
||||
def LeanLib.buildModules (self : LeanLib) (facet : Name)
|
||||
[FamilyDef ModuleData facet (ActiveBuildTarget α)] : SchedulerM Job := do
|
||||
let buildMods : BuildM _ := do
|
||||
let mods ← self.getModuleArray
|
||||
|
|
|
|||
|
|
@ -20,14 +20,14 @@ namespace Lake
|
|||
|
||||
/-- The type of Lake's build info. -/
|
||||
inductive BuildInfo
|
||||
| moduleFacet (module : Module) (facet : WfName)
|
||||
| packageFacet (package : Package) (facet : WfName)
|
||||
| moduleFacet (module : Module) (facet : Name)
|
||||
| packageFacet (package : Package) (facet : Name)
|
||||
| staticLeanLib (lib : LeanLib)
|
||||
| sharedLeanLib (lib : LeanLib)
|
||||
| leanExe (exe : LeanExe)
|
||||
| staticExternLib (lib : ExternLib)
|
||||
| sharedExternLib (lib : ExternLib)
|
||||
| customTarget (package : Package) (target : WfName)
|
||||
| customTarget (package : Package) (target : Name)
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
/-! ## Build Info & Keys -/
|
||||
|
|
@ -35,13 +35,13 @@ inductive BuildInfo
|
|||
|
||||
/-! ### Build Key Helper Constructors -/
|
||||
|
||||
abbrev Module.facetBuildKey (facet : WfName) (self : Module) : BuildKey :=
|
||||
abbrev Module.facetBuildKey (facet : Name) (self : Module) : BuildKey :=
|
||||
.moduleFacet self.keyName facet
|
||||
|
||||
abbrev Package.facetBuildKey (facet : WfName) (self : Package) : BuildKey :=
|
||||
abbrev Package.facetBuildKey (facet : Name) (self : Package) : BuildKey :=
|
||||
.packageFacet self.name facet
|
||||
|
||||
abbrev Package.targetBuildKey (target : WfName) (self : Package) : BuildKey :=
|
||||
abbrev Package.targetBuildKey (target : Name) (self : Package) : BuildKey :=
|
||||
.customTarget self.name target
|
||||
|
||||
abbrev LeanLib.staticBuildKey (self : LeanLib) : BuildKey :=
|
||||
|
|
@ -136,7 +136,7 @@ Defined here because they need to import configurations, whereas the definitions
|
|||
there need to be imported by configurations.
|
||||
-/
|
||||
|
||||
abbrev Module.importFacet := &`lean.imports
|
||||
abbrev Module.importFacet := `lean.imports
|
||||
|
||||
/-- The direct × transitive imports of the Lean module. -/
|
||||
module_data lean.imports : Array Module × Array Module
|
||||
|
|
@ -155,7 +155,7 @@ and target facets.
|
|||
namespace Module
|
||||
|
||||
/-- Build info for the module's specified facet. -/
|
||||
abbrev facet (facet : WfName) (self : Module) : BuildInfo :=
|
||||
abbrev facet (facet : Name) (self : Module) : BuildInfo :=
|
||||
.moduleFacet self facet
|
||||
|
||||
variable (self : Module)
|
||||
|
|
@ -171,15 +171,15 @@ abbrev dynlib := self.facet dynlibFacet
|
|||
end Module
|
||||
|
||||
/-- Build info for the package's specified facet. -/
|
||||
abbrev Package.facet (facet : WfName) (self : Package) : BuildInfo :=
|
||||
abbrev Package.facet (facet : Name) (self : Package) : BuildInfo :=
|
||||
.packageFacet self facet
|
||||
|
||||
/-- Build info for the package's `extraDepTarget`. -/
|
||||
abbrev Package.extraDep (self : Package) : BuildInfo :=
|
||||
self.facet &`extraDep
|
||||
self.facet `extraDep
|
||||
|
||||
/-- Build info for a custom package target. -/
|
||||
abbrev Package.customTarget (target : WfName) (self : Package) : BuildInfo :=
|
||||
abbrev Package.customTarget (target : Name) (self : Package) : BuildInfo :=
|
||||
.customTarget self target
|
||||
|
||||
/-- Build info of the Lean library's static binary. -/
|
||||
|
|
|
|||
|
|
@ -9,10 +9,10 @@ namespace Lake
|
|||
|
||||
/-- The type of keys in the Lake build store. -/
|
||||
inductive BuildKey
|
||||
| moduleFacet (module : WfName) (facet : WfName)
|
||||
| packageFacet (package : WfName) (facet : WfName)
|
||||
| targetFacet (package : WfName) (target : WfName) (facet : WfName)
|
||||
| customTarget (package : WfName) (target : WfName)
|
||||
| moduleFacet (module : Name) (facet : Name)
|
||||
| packageFacet (package : Name) (facet : Name)
|
||||
| targetFacet (package : Name) (target : Name) (facet : Name)
|
||||
| customTarget (package : Name) (target : Name)
|
||||
deriving Inhabited, Repr, DecidableEq, Hashable
|
||||
|
||||
namespace BuildKey
|
||||
|
|
|
|||
|
|
@ -90,7 +90,7 @@ def LeanExe.recBuild (self : LeanExe) : IndexT m ActiveFileTarget := do
|
|||
for facet in mod.nativeFacets do
|
||||
arr := arr.push <| Target.active <| ← recBuild <| mod.facet facet.name
|
||||
return arr
|
||||
let deps := (← recBuild <| self.pkg.facet &`deps).push self.pkg
|
||||
let deps := (← recBuild <| self.pkg.facet `deps).push self.pkg
|
||||
for dep in deps do for lib in dep.externLibs do
|
||||
linkTargets := linkTargets.push <| Target.active <| ← lib.static.recBuild
|
||||
leanExeTarget self.file linkTargets self.linkArgs |>.activate
|
||||
|
|
|
|||
|
|
@ -32,7 +32,7 @@ set_option linter.unusedVariables false
|
|||
|
||||
/-- Derive an array of built module facets from the store. -/
|
||||
def collectModuleFacetArray (self : BuildStore)
|
||||
(facet : WfName) [FamilyDef ModuleData facet α] : Array α := Id.run do
|
||||
(facet : Name) [FamilyDef ModuleData facet α] : Array α := Id.run do
|
||||
let mut res : Array α := #[]
|
||||
for ⟨k, v⟩ in self do
|
||||
match k with
|
||||
|
|
@ -45,7 +45,7 @@ def collectModuleFacetArray (self : BuildStore)
|
|||
|
||||
/-- Derive a map of module names to built facets from the store. -/
|
||||
def collectModuleFacetMap (self : BuildStore)
|
||||
(facet : WfName) [FamilyDef ModuleData facet α] : NameMap α := Id.run do
|
||||
(facet : Name) [FamilyDef ModuleData facet α] : NameMap α := Id.run do
|
||||
let mut res := Lean.mkNameMap α
|
||||
for ⟨k, v⟩ in self do
|
||||
match k with
|
||||
|
|
@ -58,7 +58,7 @@ def collectModuleFacetMap (self : BuildStore)
|
|||
|
||||
/-- Derive an array of built package facets from the store. -/
|
||||
def collectPackageFacetArray (self : BuildStore)
|
||||
(facet : WfName) [FamilyDef PackageData facet α] : Array α := Id.run do
|
||||
(facet : Name) [FamilyDef PackageData facet α] : Array α := Id.run do
|
||||
let mut res : Array α := #[]
|
||||
for ⟨k, v⟩ in self do
|
||||
match k with
|
||||
|
|
@ -71,7 +71,7 @@ def collectPackageFacetArray (self : BuildStore)
|
|||
|
||||
/-- Derive an array of built target facets from the store. -/
|
||||
def collectTargetFacetArray (self : BuildStore)
|
||||
(facet : WfName) [FamilyDef TargetData facet α] : Array α := Id.run do
|
||||
(facet : Name) [FamilyDef TargetData facet α] : Array α := Id.run do
|
||||
let mut res : Array α := #[]
|
||||
for ⟨k, v⟩ in self do
|
||||
match k with
|
||||
|
|
@ -84,5 +84,5 @@ def collectTargetFacetArray (self : BuildStore)
|
|||
|
||||
/-- Derive an array of built external shared libraries from the store. -/
|
||||
def collectSharedExternLibs (self : BuildStore)
|
||||
[FamilyDef TargetData &`externLib.shared α] : Array α :=
|
||||
self.collectTargetFacetArray &`externLib.shared
|
||||
[FamilyDef TargetData `externLib.shared α] : Array α :=
|
||||
self.collectTargetFacetArray `externLib.shared
|
||||
|
|
|
|||
|
|
@ -25,18 +25,18 @@ def parsePackageSpec (ws : Workspace) (spec : String) : Except CliError Package
|
|||
| none => throw <| CliError.unknownPackage spec
|
||||
|
||||
open Module in
|
||||
def resolveModuleTarget (ws : Workspace) (mod : Module) (facet : WfName) : Except CliError OpaqueTarget :=
|
||||
if facet.isAnonymous || facet == &`bin then
|
||||
def resolveModuleTarget (ws : Workspace) (mod : Module) (facet : Name) : Except CliError OpaqueTarget :=
|
||||
if facet.isAnonymous || facet == `bin then
|
||||
return mod.facetTarget leanBinFacet
|
||||
else if facet == &`ilean then
|
||||
else if facet == `ilean then
|
||||
return mod.facetTarget ileanFacet
|
||||
else if facet == &`olean then
|
||||
else if facet == `olean then
|
||||
return mod.facetTarget oleanFacet
|
||||
else if facet == &`c then
|
||||
else if facet == `c then
|
||||
return mod.facetTarget cFacet
|
||||
else if facet == &`o then
|
||||
else if facet == `o then
|
||||
return mod.facetTarget oFacet
|
||||
else if facet == &`dynlib then
|
||||
else if facet == `dynlib then
|
||||
return mod.facetTarget dynlibFacet
|
||||
else if let some config := ws.findModuleFacetConfig? facet then
|
||||
if let some (.up ⟨_, h⟩) := config.result_eq_target? then
|
||||
|
|
@ -47,23 +47,23 @@ def resolveModuleTarget (ws : Workspace) (mod : Module) (facet : WfName) : Excep
|
|||
else
|
||||
throw <| CliError.unknownFacet "module" facet
|
||||
|
||||
def resolveLibTarget (lib : LeanLib) (facet : WfName) : Except CliError OpaqueTarget :=
|
||||
if facet.isAnonymous || facet == &`lean then
|
||||
def resolveLibTarget (lib : LeanLib) (facet : Name) : Except CliError OpaqueTarget :=
|
||||
if facet.isAnonymous || facet == `lean then
|
||||
return lib.leanTarget
|
||||
else if facet == &`static then
|
||||
else if facet == `static then
|
||||
return lib.staticLibTarget |>.withoutInfo
|
||||
else if facet == &`shared then
|
||||
else if facet == `shared then
|
||||
return lib.sharedLibTarget |>.withoutInfo
|
||||
else
|
||||
throw <| CliError.unknownFacet "library" facet
|
||||
|
||||
def resolveExeTarget (exe : LeanExe) (facet : WfName) : Except CliError OpaqueTarget :=
|
||||
if facet.isAnonymous || facet == &`exe then
|
||||
def resolveExeTarget (exe : LeanExe) (facet : Name) : Except CliError OpaqueTarget :=
|
||||
if facet.isAnonymous || facet == `exe then
|
||||
return exe.target |>.withoutInfo
|
||||
else
|
||||
throw <| CliError.unknownFacet "executable" facet
|
||||
|
||||
def resolveTargetInPackage (ws : Workspace) (pkg : Package) (target : WfName) (facet : WfName) : Except CliError OpaqueTarget :=
|
||||
def resolveTargetInPackage (ws : Workspace) (pkg : Package) (target : Name) (facet : Name) : Except CliError OpaqueTarget :=
|
||||
if let some config := pkg.findTargetConfig? target then
|
||||
if !facet.isAnonymous then
|
||||
throw <| CliError.invalidFacet target facet
|
||||
|
|
@ -94,16 +94,16 @@ def resolveDefaultPackageTarget (ws : Workspace) (pkg : Package) : Except CliErr
|
|||
return Target.collectOpaqueArray <| ←
|
||||
pkg.defaultTargets.mapM (resolveTargetInPackage ws pkg · .anonymous)
|
||||
|
||||
def resolvePackageTarget (ws : Workspace) (pkg : Package) (facet : WfName) : Except CliError OpaqueTarget :=
|
||||
def resolvePackageTarget (ws : Workspace) (pkg : Package) (facet : Name) : Except CliError OpaqueTarget :=
|
||||
if facet.isAnonymous then
|
||||
resolveDefaultPackageTarget ws pkg
|
||||
else if facet == &`exe then
|
||||
else if facet == `exe then
|
||||
return pkg.exeTarget.withoutInfo
|
||||
else if facet == &`staticLib then
|
||||
else if facet == `staticLib then
|
||||
return pkg.staticLibTarget.withoutInfo
|
||||
else if facet == &`sharedLib then
|
||||
else if facet == `sharedLib then
|
||||
return pkg.sharedLibTarget.withoutInfo
|
||||
else if facet == &`leanLib then
|
||||
else if facet == `leanLib then
|
||||
return pkg.leanLibTarget.withoutInfo
|
||||
else if let some config := ws.findPackageFacetConfig? facet then
|
||||
if let some (.up ⟨_, h⟩) := config.result_eq_target? then
|
||||
|
|
@ -114,7 +114,7 @@ def resolvePackageTarget (ws : Workspace) (pkg : Package) (facet : WfName) : Exc
|
|||
else
|
||||
throw <| CliError.unknownFacet "package" facet
|
||||
|
||||
def resolveTargetInWorkspace (ws : Workspace) (target : Name) (facet : WfName) : Except CliError OpaqueTarget :=
|
||||
def resolveTargetInWorkspace (ws : Workspace) (target : Name) (facet : Name) : Except CliError OpaqueTarget :=
|
||||
if let some (pkg, config) := ws.findTargetConfig? target then
|
||||
if !facet.isAnonymous then
|
||||
throw <| CliError.invalidFacet config.name facet
|
||||
|
|
@ -140,7 +140,7 @@ def resolveTargetInWorkspace (ws : Workspace) (target : Name) (facet : WfName) :
|
|||
else
|
||||
throw <| CliError.unknownTarget target
|
||||
|
||||
def resolveTargetBaseSpec (ws : Workspace) (spec : String) (facet : WfName) : Except CliError OpaqueTarget := do
|
||||
def resolveTargetBaseSpec (ws : Workspace) (spec : String) (facet : Name) : Except CliError OpaqueTarget := do
|
||||
match spec.splitOn "/" with
|
||||
| [spec] =>
|
||||
if spec.isEmpty then
|
||||
|
|
@ -166,7 +166,7 @@ def resolveTargetBaseSpec (ws : Workspace) (spec : String) (facet : WfName) : Ex
|
|||
else
|
||||
throw <| CliError.unknownModule mod
|
||||
else
|
||||
resolveTargetInPackage ws pkg (WfName.ofName targetSpec) facet
|
||||
resolveTargetInPackage ws pkg targetSpec facet
|
||||
| _ =>
|
||||
throw <| CliError.invalidTargetSpec spec '/'
|
||||
|
||||
|
|
@ -175,6 +175,6 @@ def parseTargetSpec (ws : Workspace) (spec : String) : Except CliError OpaqueTar
|
|||
| [spec] =>
|
||||
resolveTargetBaseSpec ws spec .anonymous
|
||||
| [rootSpec, facet] =>
|
||||
resolveTargetBaseSpec ws rootSpec (WfName.ofString facet)
|
||||
resolveTargetBaseSpec ws rootSpec (Name.ofString facet)
|
||||
| _ =>
|
||||
throw <| CliError.invalidTargetSpec spec ':'
|
||||
|
|
|
|||
|
|
@ -26,8 +26,8 @@ structure ExternLib where
|
|||
namespace ExternLib
|
||||
|
||||
/- The library's well-formed name. -/
|
||||
@[inline] def name (self : ExternLib) : WfName :=
|
||||
WfName.ofName self.config.name
|
||||
@[inline] def name (self : ExternLib) : Name :=
|
||||
self.config.name
|
||||
|
||||
/-- The external library's user-defined `target`. -/
|
||||
@[inline] def target (self : ExternLib) : FileTarget :=
|
||||
|
|
|
|||
|
|
@ -9,7 +9,7 @@ import Lake.Build.Store
|
|||
namespace Lake
|
||||
|
||||
/-- A facet's declarative configuration. -/
|
||||
structure FacetConfig (DataFam : WfName → Type u) (BuildFn : Type u → Type v) (name : WfName) where
|
||||
structure FacetConfig (DataFam : Name → Type u) (BuildFn : Type u → Type v) (name : Name) where
|
||||
/-- The type of the target's build result. -/
|
||||
resultType : Type u
|
||||
/-- The facet's build function. -/
|
||||
|
|
@ -52,8 +52,8 @@ def familyDefTarget (cfg : FacetConfig Fam Fn name)
|
|||
end FacetConfig
|
||||
|
||||
/-- A dependently typed configuration based on its registered name. -/
|
||||
structure NamedConfigDecl (β : WfName → Type u) where
|
||||
name : WfName
|
||||
structure NamedConfigDecl (β : Name → Type u) where
|
||||
name : Name
|
||||
config : β name
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
|
@ -63,7 +63,7 @@ abbrev ModuleFacetConfig := FacetConfig ModuleData (FacetBuildFn Module)
|
|||
hydrate_opaque_type OpaqueModuleFacetConfig ModuleFacetConfig name
|
||||
|
||||
/-- Try to find a module facet configuration in the package with the given name . -/
|
||||
def Package.findModuleFacetConfig? (name : WfName) (self : Package) : Option (ModuleFacetConfig name) :=
|
||||
def Package.findModuleFacetConfig? (name : Name) (self : Package) : Option (ModuleFacetConfig name) :=
|
||||
self.opaqueModuleFacetConfigs.find? name |>.map (·.get)
|
||||
|
||||
/-- A module facet declaration from a configuration file. -/
|
||||
|
|
@ -76,7 +76,7 @@ abbrev PackageFacetConfig := FacetConfig PackageData (FacetBuildFn Package)
|
|||
hydrate_opaque_type OpaquePackageFacetConfig PackageFacetConfig name
|
||||
|
||||
/-- Try to find a package configuration in the package with the given name . -/
|
||||
def Package.findPackageFacetConfig? (name : WfName) (self : Package) : Option (PackageFacetConfig name) :=
|
||||
def Package.findPackageFacetConfig? (name : Name) (self : Package) : Option (PackageFacetConfig name) :=
|
||||
self.opaquePackageFacetConfigs.find? name |>.map (·.get)
|
||||
|
||||
/-- A package facet declaration from a configuration file. -/
|
||||
|
|
|
|||
|
|
@ -24,13 +24,13 @@ deriving Inhabited, Repr
|
|||
instance : Coe Name Glob := ⟨Glob.one⟩
|
||||
|
||||
partial def forEachModuleIn [Monad m] [MonadLiftT IO m]
|
||||
(dir : FilePath) (f : WfName → m PUnit) : m PUnit := do
|
||||
(dir : FilePath) (f : Name → m PUnit) : m PUnit := do
|
||||
for entry in (← dir.readDir) do
|
||||
if (← liftM (m := IO) <| entry.path.isDir) then
|
||||
let n := WfName.ofString <| entry.fileName
|
||||
let n := Name.ofString <| entry.fileName
|
||||
f n *> forEachModuleIn entry.path (f <| n ++ ·)
|
||||
else if entry.path.extension == some "lean" then
|
||||
f <| WfName.ofString <| FilePath.withExtension entry.fileName "" |>.toString
|
||||
f <| Name.ofString <| FilePath.withExtension entry.fileName "" |>.toString
|
||||
|
||||
namespace Glob
|
||||
|
||||
|
|
@ -40,11 +40,9 @@ def «matches» (m : Name) : (self : Glob) → Bool
|
|||
| andSubmodules n => n.isPrefixOf m
|
||||
|
||||
nonrec def forEachModuleIn [Monad m] [MonadLiftT IO m]
|
||||
(dir : FilePath) (f : WfName → m PUnit) : (self : Glob) → m PUnit
|
||||
| one n => f (WfName.ofName n)
|
||||
(dir : FilePath) (f : Name → m PUnit) : (self : Glob) → m PUnit
|
||||
| one n => f n
|
||||
| submodules n =>
|
||||
let n := WfName.ofName n
|
||||
forEachModuleIn (Lean.modToFilePath dir n "") (f <| n ++ ·)
|
||||
| andSubmodules n =>
|
||||
let n := WfName.ofName n
|
||||
f n *> forEachModuleIn (Lean.modToFilePath dir n "") (f <| n ++ ·)
|
||||
|
|
|
|||
|
|
@ -41,8 +41,8 @@ def LeanExeConfig.toLeanLibConfig (self : LeanExeConfig) : LeanLibConfig where
|
|||
namespace LeanExe
|
||||
|
||||
/- The executable's well-formed name. -/
|
||||
@[inline] def name (self : LeanExe) : WfName :=
|
||||
WfName.ofName self.config.name
|
||||
@[inline] def name (self : LeanExe) : Name :=
|
||||
self.config.name
|
||||
|
||||
/-- Converts the executable into a library with a single module (the root). -/
|
||||
@[inline] def toLeanLib (self : LeanExe) : LeanLib :=
|
||||
|
|
@ -51,8 +51,8 @@ namespace LeanExe
|
|||
/-- The executable's root module. -/
|
||||
@[inline] def root (self : LeanExe) : Module where
|
||||
lib := self.toLeanLib
|
||||
name := WfName.ofName self.config.root
|
||||
keyName := WfName.ofName self.pkg.name |>.appendName self.config.root
|
||||
name := self.config.root
|
||||
keyName := self.pkg.name ++ self.config.root
|
||||
|
||||
/- Return the the root module if the name matches, otherwise return none. -/
|
||||
def isRoot? (name : Name) (self : LeanExe) : Option Module :=
|
||||
|
|
|
|||
|
|
@ -31,8 +31,8 @@ structure LeanLib where
|
|||
namespace LeanLib
|
||||
|
||||
/- The library's well-formed name. -/
|
||||
@[inline] def name (self : LeanLib) : WfName :=
|
||||
WfName.ofName self.config.name
|
||||
@[inline] def name (self : LeanLib) : Name :=
|
||||
self.config.name
|
||||
|
||||
/- The package's `srcDir` joined with the library's `srcDir`. -/
|
||||
@[inline] def srcDir (self : LeanLib) : FilePath :=
|
||||
|
|
|
|||
|
|
@ -44,7 +44,7 @@ unsafe def evalConstCheck (α) (env : Environment) (opts : Options) (type : Name
|
|||
| none => throw s!"unknown constant '{const}'"
|
||||
| some info =>
|
||||
match info.type with
|
||||
| Expr.const c _ _ =>
|
||||
| Expr.const c _ =>
|
||||
if c != type then
|
||||
throwUnexpectedType
|
||||
else
|
||||
|
|
@ -102,9 +102,8 @@ unsafe def loadUnsafe (dir : FilePath) (configOpts : NameMap String)
|
|||
let mkTagMap {α} (attr) (f : Name → IO α) : IO (NameMap α) :=
|
||||
attr.ext.getState env |>.foldM (init := {}) fun map declName =>
|
||||
return map.insert declName <| ← f declName
|
||||
let mkDTagMap {β} (attr : TagAttribute) (f : (n : WfName) → IO (β n)) : IO (DNameMap β) :=
|
||||
let mkDTagMap {β} (attr : TagAttribute) (f : (n : Name) → IO (β n)) : IO (DNameMap β) :=
|
||||
attr.ext.getState env |>.foldM (init := {}) fun map declName =>
|
||||
let declName := WfName.ofName declName
|
||||
return map.insert declName <| ← f declName
|
||||
let evalConst (α typeName declName) : IO α :=
|
||||
IO.ofExcept (evalConstCheck α env leanOpts typeName declName)
|
||||
|
|
@ -146,7 +145,7 @@ unsafe def loadUnsafe (dir : FilePath) (configOpts : NameMap String)
|
|||
(evalConstMap OpaqueTargetConfig.mk)
|
||||
let defaultTargets :=
|
||||
defaultTargetAttr.ext.getState env |>.fold (init := #[]) fun arr name =>
|
||||
arr.push <| WfName.ofName name
|
||||
arr.push name
|
||||
|
||||
-- Construct the Package
|
||||
if leanLibConfigs.isEmpty && leanExeConfigs.isEmpty && config.defaultFacet ≠ .none then
|
||||
|
|
|
|||
|
|
@ -12,12 +12,12 @@ open Std System
|
|||
/-- A buildable Lean module of a `LeanLib`. -/
|
||||
structure Module where
|
||||
lib : LeanLib
|
||||
name : WfName
|
||||
name : Name
|
||||
/--
|
||||
The name of the module as a key.
|
||||
Used to create private modules (e.g., executable roots).
|
||||
-/
|
||||
keyName : WfName := name
|
||||
keyName : Name := name
|
||||
deriving Inhabited
|
||||
|
||||
abbrev ModuleSet := RBTree Module (·.name.quickCmp ·.name)
|
||||
|
|
@ -28,7 +28,6 @@ abbrev ModuleMap (α) := RBMap Module α (·.name.quickCmp ·.name)
|
|||
|
||||
/-- Locate the named module in the library (if it is buildable and local to it). -/
|
||||
def LeanLib.findModule? (mod : Name) (self : LeanLib) : Option Module :=
|
||||
let mod := WfName.ofName mod
|
||||
if self.isBuildableModule mod then some {lib := self, name := mod} else none
|
||||
|
||||
/-- Get an `Array` of the library's modules. -/
|
||||
|
|
@ -81,7 +80,7 @@ abbrev pkg (self : Module) : Package :=
|
|||
|
||||
@[inline] def dynlibName (self : Module) : String :=
|
||||
-- NOTE: file name MUST be unique on Windows
|
||||
self.name.toStringWithSep "-"
|
||||
self.name.toStringWithSep "-" (escape := true)
|
||||
|
||||
@[inline] def dynlibFile (self : Module) : FilePath :=
|
||||
self.pkg.libDir / nameToSharedLib self.dynlibName
|
||||
|
|
|
|||
|
|
@ -15,10 +15,10 @@ declare_opaque_type OpaquePackage
|
|||
declare_opaque_type OpaqueWorkspace
|
||||
|
||||
/-- Opaque reference to a `ModuleFacetConfig` used for forward declaration. -/
|
||||
declare_opaque_type OpaqueModuleFacetConfig (name : WfName)
|
||||
declare_opaque_type OpaqueModuleFacetConfig (name : Name)
|
||||
|
||||
/-- Opaque reference to a `PackageFacetConfig` used for forward declaration. -/
|
||||
declare_opaque_type OpaquePackageFacetConfig (name : WfName)
|
||||
declare_opaque_type OpaquePackageFacetConfig (name : Name)
|
||||
|
||||
/-- Opaque reference to a `TargetConfig` used for forward declaration. -/
|
||||
declare_opaque_type OpaqueTargetConfig
|
||||
|
|
|
|||
|
|
@ -238,7 +238,7 @@ end PackageConfig
|
|||
-- # Package
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
abbrev DNameMap α := DRBMap WfName α WfName.quickCmp
|
||||
abbrev DNameMap α := DRBMap Name α Lean.Name.quickCmp
|
||||
|
||||
/-- A Lake package -- its location plus its configuration. -/
|
||||
structure Package where
|
||||
|
|
@ -247,7 +247,7 @@ structure Package where
|
|||
/-- The package's user-defined configuration. -/
|
||||
config : PackageConfig
|
||||
/-- The package's well-formed name. -/
|
||||
name : WfName := WfName.ofName config.name
|
||||
name : Name := config.name
|
||||
/-- Scripts for the package. -/
|
||||
scripts : NameMap Script := {}
|
||||
/- An `Array` of the package's dependencies. -/
|
||||
|
|
@ -268,7 +268,7 @@ structure Package where
|
|||
The names of the package's targets to build by default
|
||||
(i.e., on a bare `lake build` of the package).
|
||||
-/
|
||||
defaultTargets : Array WfName := #[]
|
||||
defaultTargets : Array Name := #[]
|
||||
deriving Inhabited
|
||||
|
||||
hydrate_opaque_type OpaquePackage Package
|
||||
|
|
|
|||
|
|
@ -11,9 +11,9 @@ namespace Lake
|
|||
/-- A custom target's declarative configuration. -/
|
||||
structure TargetConfig where
|
||||
/-- The name of the target. -/
|
||||
name : WfName
|
||||
name : Name
|
||||
/-- The name of the target's package. -/
|
||||
package : WfName
|
||||
package : Name
|
||||
/-- The type of the target's build result. -/
|
||||
resultType : Type
|
||||
/-- The target's build function. -/
|
||||
|
|
@ -21,11 +21,11 @@ structure TargetConfig where
|
|||
/-- Proof that target's build result is the correctly typed target.-/
|
||||
data_eq_target : CustomData (package, name) = ActiveBuildTarget resultType
|
||||
|
||||
family_def _nil_ : CustomData (&`✝, &`✝) := ActiveOpaqueTarget
|
||||
family_def _nil_ : CustomData (.anonymous, .anonymous) := ActiveOpaqueTarget
|
||||
|
||||
instance : Inhabited TargetConfig := ⟨{
|
||||
name := &`✝
|
||||
package := &`✝
|
||||
name := .anonymous
|
||||
package := .anonymous
|
||||
resultType := PUnit
|
||||
target := default
|
||||
data_eq_target := family_key_eq_type
|
||||
|
|
|
|||
|
|
@ -87,11 +87,11 @@ def findExternLib? (name : Name) (self : Workspace) : Option ExternLib :=
|
|||
self.packageArray.findSome? fun pkg => pkg.findExternLib? name
|
||||
|
||||
/-- Try to find a module facet configuration in the workspace with the given name. -/
|
||||
def findModuleFacetConfig? (name : WfName) (self : Workspace) : Option (ModuleFacetConfig name) :=
|
||||
def findModuleFacetConfig? (name : Name) (self : Workspace) : Option (ModuleFacetConfig name) :=
|
||||
self.packageArray.findSome? fun pkg => pkg.findModuleFacetConfig? name
|
||||
|
||||
/-- Try to find a package facet configuration in the workspace with the given name. -/
|
||||
def findPackageFacetConfig? (name : WfName) (self : Workspace) : Option (PackageFacetConfig name) :=
|
||||
def findPackageFacetConfig? (name : Name) (self : Workspace) : Option (PackageFacetConfig name) :=
|
||||
self.packageArray.findSome? fun pkg => pkg.findPackageFacetConfig? name
|
||||
|
||||
/-- Try to find a target configuration in the workspace with the given name. -/
|
||||
|
|
|
|||
|
|
@ -22,7 +22,7 @@ kw:"module_facet " sig:simpleDeclSig : command => do
|
|||
let attr ← withRef kw `(Term.attrInstance| moduleFacet)
|
||||
let attrs := #[attr] ++ expandAttrs attrs?
|
||||
let axm := mkIdentFrom id <| ``ModuleData ++ id.getId
|
||||
let name := WfName.quoteNameFrom id id.getId
|
||||
let name := Lake.quoteNameFrom id id.getId
|
||||
`(module_data $id : ActiveBuildTarget $ty
|
||||
$[$doc?]? @[$attrs,*] def $id : ModuleFacetDecl := {
|
||||
name := $name
|
||||
|
|
@ -43,7 +43,7 @@ kw:"package_facet " sig:simpleDeclSig : command => do
|
|||
let attr ← withRef kw `(Term.attrInstance| packageFacet)
|
||||
let attrs := #[attr] ++ expandAttrs attrs?
|
||||
let axm := mkIdentFrom id <| ``PackageData ++ id.getId
|
||||
let name := WfName.quoteNameFrom id id.getId
|
||||
let name := Lake.quoteNameFrom id id.getId
|
||||
`(package_data $id : ActiveBuildTarget $ty
|
||||
$[$doc?]? @[$attrs,*] def $id : PackageFacetDecl := {
|
||||
name := $name
|
||||
|
|
@ -64,8 +64,8 @@ kw:"target " sig:simpleDeclSig : command => do
|
|||
let attr ← withRef kw `(Term.attrInstance| target)
|
||||
let attrs := #[attr] ++ expandAttrs attrs?
|
||||
let axm := mkIdentFrom id <| ``CustomData ++ id.getId
|
||||
let name := WfName.quoteNameFrom id id.getId
|
||||
let pkgName ← withRef id `(WfName.ofName $(mkIdentFrom id `_package.name))
|
||||
let name := Lake.quoteNameFrom id id.getId
|
||||
let pkgName := mkIdentFrom id `_package.name
|
||||
`(family_def $id : CustomData ($pkgName, $name) := ActiveBuildTarget $ty
|
||||
$[$doc?]? @[$attrs,*] def $id : TargetConfig := {
|
||||
name := $name
|
||||
|
|
|
|||
|
|
@ -13,7 +13,7 @@ def toUpperCamelCaseString (str : String) : String :=
|
|||
|
||||
/-- Converts a snake case, kebab case, or lower camel case `Name` to upper camel case. -/
|
||||
def toUpperCamelCase (name : Name) : Name :=
|
||||
if let Name.str p s _ := name then
|
||||
if let Name.str p s := name then
|
||||
Name.mkStr (toUpperCamelCase p) <| toUpperCamelCaseString s
|
||||
else
|
||||
name
|
||||
|
|
|
|||
|
|
@ -47,6 +47,12 @@ theorem Nat.eq_of_compare
|
|||
{n n' : Nat} : compare n n' = Ordering.eq → n = n' := by
|
||||
simp only [compare]; exact eq_of_compareOfLessAndEq
|
||||
|
||||
@[simp]
|
||||
theorem Nat.compare_iff_eq
|
||||
{n n' : Nat} : compare n n' = Ordering.eq ↔ n = n' := by
|
||||
refine ⟨eq_of_compare, fun h => ?_⟩
|
||||
simp [h, compare, compareOfLessAndEq]
|
||||
|
||||
instance : EqOfCmp Nat compare where
|
||||
eq_of_cmp h := Nat.eq_of_compare h
|
||||
|
||||
|
|
@ -54,6 +60,21 @@ theorem String.eq_of_compare
|
|||
{s s' : String} : compare s s' = Ordering.eq → s = s' := by
|
||||
simp only [compare]; exact eq_of_compareOfLessAndEq
|
||||
|
||||
theorem List.lt_irrefl [LT α] (irrefl_α : ∀ a : α, ¬ a < a)
|
||||
: (a : List α) → ¬ a < a
|
||||
| _, .head _ _ h => irrefl_α _ h
|
||||
| _, .tail _ _ h3 => lt_irrefl irrefl_α _ h3
|
||||
|
||||
@[simp]
|
||||
theorem String.lt_irrefl (s : String) : ¬ s < s :=
|
||||
List.lt_irrefl (fun c => Nat.lt_irrefl c.1.1) _
|
||||
|
||||
@[simp]
|
||||
theorem String.compare_iff_eq
|
||||
{n n' : String} : compare n n' = Ordering.eq ↔ n = n' := by
|
||||
refine ⟨eq_of_compare, fun h => ?_⟩
|
||||
simp [h, compare, compareOfLessAndEq]
|
||||
|
||||
instance : EqOfCmp String compare where
|
||||
eq_of_cmp h := String.eq_of_compare h
|
||||
|
||||
|
|
|
|||
|
|
@ -33,7 +33,7 @@ In this approach, to define an open type family, one first defines an `opaque`
|
|||
type function with a single argument that serves as the key:
|
||||
|
||||
```lean
|
||||
opaque FooFam (key : WfName) : Type
|
||||
opaque FooFam (key : Name) : Type
|
||||
```
|
||||
|
||||
Note that, unlike Haskell, the key need not be a type. Lean's dependent type
|
||||
|
|
@ -43,21 +43,21 @@ we can use data as an index as well.
|
|||
Then, to add a mapping to this family, one defines an axioms:
|
||||
|
||||
```lean
|
||||
axiom FooFam.bar : FooFam &`bar = Nat
|
||||
axiom FooFam.bar : FooFam `bar = Nat
|
||||
```
|
||||
|
||||
To finish, one also defines an instance of the `FamilyDef` type class
|
||||
defined in this module using the axiom like so:
|
||||
|
||||
```lean
|
||||
instance : FamilyDef FooFam &`bar Nat := ⟨FooFam.bar⟩
|
||||
instance : FamilyDef FooFam `bar Nat := ⟨FooFam.bar⟩
|
||||
```
|
||||
|
||||
This module provides a `family_def` macro to define both the axiom and the
|
||||
instance in one go like so:
|
||||
|
||||
```lean
|
||||
family_def bar : FooFam &`bar := Nat
|
||||
family_def bar : FooFam `bar := Nat
|
||||
```
|
||||
|
||||
## Type Inference
|
||||
|
|
@ -69,18 +69,18 @@ FamilyDef {α : Type u} (Fam : α → Type v) (a : α) (β : outParam $ Type v)
|
|||
```
|
||||
|
||||
The key part being that `β` is an `outParam` so Lean's type class synthesis will
|
||||
smartly infer the defined type `Nat` when given the key of ``&`bar``. Thus, if
|
||||
smartly infer the defined type `Nat` when given the key of `` `bar``. Thus, if
|
||||
we have a function define like so:
|
||||
|
||||
```
|
||||
def foo (key : α) [FamilyDef FooFam key β] : β := ...
|
||||
```
|
||||
|
||||
Lean will smartly infer that the type of ``foo &`bar`` is `Nat`.
|
||||
Lean will smartly infer that the type of ``foo `bar`` is `Nat`.
|
||||
|
||||
However, filling in the right hand side of `foo` is not quite so easy.
|
||||
``FooFam &`bar = Nat`` is only true propositionally, so we have to manually
|
||||
`cast` a `Nat` to ``FooFam &`bar``and provide the proof (and the same is true
|
||||
``FooFam `bar = Nat`` is only true propositionally, so we have to manually
|
||||
`cast` a `Nat` to ``FooFam `bar``and provide the proof (and the same is true
|
||||
vice versa). Thus, this module provides two definitions, `toFamily : β → Fam a`
|
||||
and `ofFamily : Fam a → β`, to help with this conversion.
|
||||
|
||||
|
|
@ -89,21 +89,21 @@ and `ofFamily : Fam a → β`, to help with this conversion.
|
|||
Putting this all together, one can do something like the following:
|
||||
|
||||
```lean
|
||||
opaque FooFam (key : WfName) : Type
|
||||
opaque FooFam (key : Name) : Type
|
||||
|
||||
abbrev FooMap := DRBMap WfName FooFam WfName.quickCmp
|
||||
def FooMap.insert (self : FooMap) (key : WfName) [FamilyDef FooFam key α] (a : α) : FooMap :=
|
||||
abbrev FooMap := DRBMap Name FooFam Name.quickCmp
|
||||
def FooMap.insert (self : FooMap) (key : Name) [FamilyDef FooFam key α] (a : α) : FooMap :=
|
||||
DRBMap.insert self key (toFamily a)
|
||||
def FooMap.find? (self : FooMap) (key : WfName) [FamilyDef FooFam key α] : Option α :=
|
||||
def FooMap.find? (self : FooMap) (key : Name) [FamilyDef FooFam key α] : Option α :=
|
||||
ofFamily <$> DRBMap.find? self key
|
||||
|
||||
family_def bar : FooFam &`bar := Nat
|
||||
family_def baz : FooFam &`baz := String
|
||||
family_def bar : FooFam `bar := Nat
|
||||
family_def baz : FooFam `baz := String
|
||||
def foo := Id.run do
|
||||
let mut map : FooMap := {}
|
||||
map := map.insert &`bar 5
|
||||
map := map.insert &`baz "str"
|
||||
return map.find? &`bar
|
||||
map := map.insert `bar 5
|
||||
map := map.insert `baz "str"
|
||||
return map.find? `bar
|
||||
|
||||
#eval foo -- 5
|
||||
```
|
||||
|
|
@ -116,8 +116,8 @@ keys. Since mappings are defined through axioms, Lean WILL NOT catch violations
|
|||
of this rule itself, so extra care must be taken when defining mappings.
|
||||
|
||||
In Lake, this is solved by having its open type families be indexed by a
|
||||
`WfName` and defining each mapping using a name literal `name` and the
|
||||
declaration ``axiom Fam.name : Fam &`name = α`` thus causing a name clash
|
||||
`Name` and defining each mapping using a name literal `name` and the
|
||||
declaration ``axiom Fam.name : Fam `name = α`` thus causing a name clash
|
||||
if two keys overlap and thereby producing an error.
|
||||
-/
|
||||
|
||||
|
|
|
|||
|
|
@ -16,87 +16,36 @@ export Lean (Name NameMap)
|
|||
|
||||
namespace Name
|
||||
|
||||
@[simp] theorem beq_rfl (n : Name) : (n == n) = true := by
|
||||
simp only [BEq.beq]; induction n <;> simp [Name.beq, *]
|
||||
def ofString (str : String) : Name :=
|
||||
str.splitOn "." |>.foldl (fun n p => .str n p.trim) .anonymous
|
||||
|
||||
@[simp] theorem isPrefixOf_self {n : Name} : n.isPrefixOf n = true := by
|
||||
@[simp] protected theorem beq_false (m n : Name) : (m == n) = false ↔ ¬ (m = n) := by
|
||||
rw [← beq_iff_eq m n]; cases m == n <;> simp
|
||||
|
||||
@[simp] theorem isPrefixOf_self {n : Name} : n.isPrefixOf n := by
|
||||
cases n <;> simp [Name.isPrefixOf]
|
||||
|
||||
@[simp] theorem isPrefixOf_append {n m : Name} : n.isPrefixOf (n ++ m) = true := by
|
||||
simp only [HAppend.hAppend, Append.append]
|
||||
@[simp] theorem isPrefixOf_append {n m : Name} : n.isPrefixOf (n ++ m) := by
|
||||
show n.isPrefixOf (n.append m)
|
||||
induction m <;> simp [Name.isPrefixOf, Name.append, *]
|
||||
|
||||
/--
|
||||
The propositional condition of a `Name` being well-formed.
|
||||
A well-formed name has its has hash computable in the standard manner
|
||||
(i.e., via the internals of `mkStr` and `mkNum`).
|
||||
-/
|
||||
inductive WellFormed : Name → Prop
|
||||
| anonymousWff : WellFormed Name.anonymous
|
||||
| strWff {n p s} : WellFormed p → n = Name.mkStr p s → WellFormed n
|
||||
| numWff {n p v} : WellFormed p → n = Name.mkNum p v → WellFormed n
|
||||
attribute [local simp] Name.quickCmpAux
|
||||
|
||||
def WellFormed.elimStr : WellFormed (Name.str p s h) → WellFormed p
|
||||
| strWff w rfl => w
|
||||
@[simp]
|
||||
theorem quickCmpAux_iff_eq : ∀ n n', Name.quickCmpAux n n' = Ordering.eq ↔ n = n'
|
||||
| .anonymous, n => by cases n <;> simp
|
||||
| n, .anonymous => by cases n <;> simp
|
||||
| .num .., .str .. => by simp
|
||||
| .str .., .num .. => by simp
|
||||
| .num p₁ n₁, .num p₂ n₂ => by
|
||||
simp only [Name.quickCmpAux]; split <;>
|
||||
simp_all [quickCmpAux_iff_eq p₁ p₂, show ∀ p, (p → False) ↔ ¬ p from fun _ => .rfl]
|
||||
| .str p₁ s₁, .str p₂ s₂ => by
|
||||
simp only [Name.quickCmpAux]; split <;>
|
||||
simp_all [quickCmpAux_iff_eq p₁ p₂, show ∀ p, (p → False) ↔ ¬ p from fun _ => .rfl]
|
||||
|
||||
def WellFormed.elimNum : WellFormed (Name.num p v h) → WellFormed p
|
||||
| numWff w rfl => w
|
||||
|
||||
theorem eq_of_wf_quickCmpAux
|
||||
(n : Name) (w : WellFormed n) (n' : Name) (w' : WellFormed n')
|
||||
: Name.quickCmpAux n n' = Ordering.eq → n = n' := by
|
||||
revert n'
|
||||
induction w with
|
||||
| anonymousWff =>
|
||||
intro n' w'; cases w' <;> simp [Name.quickCmpAux, *]
|
||||
| @strWff n p s _ h ih =>
|
||||
intro n' w'
|
||||
cases w' with
|
||||
| anonymousWff =>
|
||||
simp [h, Name.quickCmpAux]
|
||||
| @strWff n' p' s' w' h' =>
|
||||
simp only [h, h', Name.quickCmpAux]
|
||||
intro h_cmp
|
||||
split at h_cmp
|
||||
next h_cmp_s =>
|
||||
let p_eq := ih p' w' h_cmp
|
||||
let s_eq := String.eq_of_compare h_cmp_s
|
||||
rw [s_eq, p_eq]
|
||||
next =>
|
||||
contradiction
|
||||
| @numWff n' p' v' w' h' =>
|
||||
simp [h, h', Name.quickCmpAux]
|
||||
| @numWff m p v _ h ih =>
|
||||
intro n' w'
|
||||
cases w' with
|
||||
| anonymousWff =>
|
||||
simp [h, Name.quickCmpAux]
|
||||
| @strWff n' p' s' w' h' =>
|
||||
simp [h, h', Name.quickCmpAux]
|
||||
| @numWff n' p' v' w' h' =>
|
||||
simp only [h, h', Name.quickCmpAux]
|
||||
intro h_cmp
|
||||
split at h_cmp
|
||||
next h_cmp_v =>
|
||||
let p_eq := ih p' w' h_cmp
|
||||
let v_eq := Nat.eq_of_compare h_cmp_v
|
||||
rw [v_eq, p_eq]
|
||||
next =>
|
||||
contradiction
|
||||
|
||||
theorem wf_of_append {n n' : Name}
|
||||
(w : WellFormed n) (w' : WellFormed n') : WellFormed (n.append n') := by
|
||||
induction w' with
|
||||
| anonymousWff =>
|
||||
simp [w, Name.append]
|
||||
| @strWff n' p s w' h' ih =>
|
||||
unfold Name.mkStr at h'
|
||||
simp only [Name.append, h']
|
||||
exact WellFormed.strWff ih rfl
|
||||
| @numWff n' p v w' h' ih =>
|
||||
unfold Name.mkNum at h'
|
||||
simp only [Name.append, h']
|
||||
exact WellFormed.numWff ih rfl
|
||||
theorem eq_of_quickCmpAux (n n') : Name.quickCmpAux n n' = Ordering.eq → n = n' :=
|
||||
(quickCmpAux_iff_eq n n').1
|
||||
|
||||
end Name
|
||||
|
||||
|
|
@ -124,179 +73,20 @@ theorem ne_iff_val_ne {a b : Subtype p} : a ≠ b ↔ a.val ≠ b.val :=
|
|||
|
||||
end Subtype
|
||||
|
||||
-- # Well-formed Names
|
||||
|
||||
|
||||
/--
|
||||
A `WellFormed` `Name`.
|
||||
Such a name has its hash provably computed in the standard manner.
|
||||
This allows us to prove that the `beq` and `quickCmp` functions' equality
|
||||
corresponds to propositional equality for this subtype.
|
||||
-/
|
||||
abbrev WfName :=
|
||||
{n : Name // Name.WellFormed n}
|
||||
|
||||
namespace WfName
|
||||
|
||||
def anonymous : WfName :=
|
||||
⟨Name.anonymous, Name.WellFormed.anonymousWff⟩
|
||||
|
||||
instance : Inhabited WfName := ⟨anonymous⟩
|
||||
|
||||
def isAnonymous : WfName → Bool
|
||||
| ⟨.anonymous, _⟩ => true
|
||||
| _ => false
|
||||
|
||||
@[inline] def mkStr : WfName → String → WfName
|
||||
| ⟨p, h⟩, s => ⟨Name.mkStr p s, Name.WellFormed.strWff h rfl⟩
|
||||
|
||||
@[inline] def mkNum : WfName → Nat → WfName
|
||||
| ⟨p, h⟩, v => ⟨Name.mkNum p v, Name.WellFormed.numWff h rfl⟩
|
||||
|
||||
def ofName : Name → WfName
|
||||
| .anonymous => anonymous
|
||||
| .str p s _ => mkStr (ofName p) s
|
||||
| .num p v _ => mkNum (ofName p) v
|
||||
|
||||
def ofString (str : String) : WfName :=
|
||||
str.splitOn "." |>.foldl (fun n p => mkStr n p.trim) anonymous
|
||||
|
||||
@[inline] protected def toString (escape := true) : WfName → String
|
||||
| ⟨n, _⟩ => n.toString escape
|
||||
|
||||
@[inline] protected def toStringWithSep (sep : String) (escape := true) : WfName → String
|
||||
| ⟨n, _⟩ => n.toStringWithSep sep escape
|
||||
|
||||
instance : ToString WfName := ⟨(·.toString)⟩
|
||||
|
||||
def isPrefixOf : WfName → WfName → Bool
|
||||
| ⟨n, _⟩, ⟨n', _⟩ => n.isPrefixOf n'
|
||||
|
||||
protected def append : WfName → WfName → WfName
|
||||
| ⟨n, w⟩, ⟨n', w'⟩ => ⟨n.append n', Name.wf_of_append w w'⟩
|
||||
|
||||
instance : Append WfName := ⟨WfName.append⟩
|
||||
|
||||
def appendName (n : WfName) : Name → WfName
|
||||
| .anonymous => n
|
||||
| .str p s _ => mkStr (appendName n p) s
|
||||
| .num p v _ => mkNum (appendName n p) v
|
||||
|
||||
instance : HAppend WfName Name WfName := ⟨appendName⟩
|
||||
|
||||
@[inline] protected def hash : WfName → UInt64
|
||||
| ⟨n, _⟩ => n.hash
|
||||
|
||||
instance : Hashable WfName := ⟨WfName.hash⟩
|
||||
|
||||
@[inline] protected def beq : WfName → WfName → Bool
|
||||
| ⟨n, _⟩, ⟨n', _⟩ => n.beq n'
|
||||
|
||||
instance : BEq WfName := ⟨WfName.beq⟩
|
||||
|
||||
theorem eq_of_beq_true : {n n' : WfName} → (n == n') = true → n = n' := by
|
||||
intro ⟨n, w⟩
|
||||
simp only [BEq.beq, WfName.beq, Subtype.eq_iff_val_eq]
|
||||
induction w with
|
||||
| anonymousWff =>
|
||||
intro ⟨n', w'⟩; cases w' <;> simp [Name.beq, *]
|
||||
| @strWff n p s _ h ih =>
|
||||
intro ⟨n', w'⟩
|
||||
simp only [Subtype.eq_iff_val_eq]
|
||||
cases w' with
|
||||
| anonymousWff =>
|
||||
simp [Name.mkStr, Name.beq, h]
|
||||
| @strWff n' p' s' w' h' =>
|
||||
simp only [Name.mkStr, Name.beq, h, h']
|
||||
simp only [BEq.beq, Bool.and_eq_true, decide_eq_true_eq]
|
||||
intro ⟨s_eq, p_beq⟩
|
||||
simp [s_eq, @ih ⟨p', w'⟩ p_beq]
|
||||
| @numWff n' p' v' w' h' =>
|
||||
simp only [Name.mkNum, Name.beq, h, h']
|
||||
exact False.elim
|
||||
| @numWff n p v _ h ih =>
|
||||
intro ⟨n', w'⟩
|
||||
simp only [Subtype.eq_iff_val_eq]
|
||||
cases w' with
|
||||
| anonymousWff =>
|
||||
simp [Name.mkNum, Name.beq, h]
|
||||
| @strWff n' p' s' w' h' =>
|
||||
simp only [Name.mkNum, Name.beq, h, h']
|
||||
exact False.elim
|
||||
| @numWff n' p' v' w' h' =>
|
||||
simp only [Name.mkNum, Name.beq, h, h']
|
||||
simp only [BEq.beq, Bool.and_eq_true, decide_eq_true_eq]
|
||||
intro ⟨n_beq, p_beq⟩
|
||||
simp [Nat.eq_of_beq_eq_true n_beq, @ih ⟨p', w'⟩ p_beq]
|
||||
|
||||
instance : LawfulBEq WfName where
|
||||
eq_of_beq := WfName.eq_of_beq_true
|
||||
rfl {n} := Name.beq_rfl n
|
||||
|
||||
theorem ne_of_beq_false {n n' : WfName} : (n == n') = false → n ≠ n' :=
|
||||
_root_.ne_of_beq_false
|
||||
|
||||
instance : DecidableEq WfName :=
|
||||
fun n n' => match h:WfName.beq n n' with
|
||||
| true => isTrue (eq_of_beq_true h)
|
||||
| false => isFalse (ne_of_beq_false h)
|
||||
|
||||
@[inline] def quickCmp : WfName → WfName → Ordering
|
||||
| ⟨n, _⟩, ⟨n', _⟩ => n.quickCmp n'
|
||||
|
||||
theorem eq_of_quickCmp :
|
||||
{n n' : WfName} → quickCmp n n' = Ordering.eq → n = n' := by
|
||||
intro ⟨n, w⟩ ⟨n', w'⟩
|
||||
simp only [quickCmp, Name.quickCmp, Subtype.eq_iff_val_eq]
|
||||
theorem eq_of_quickCmp {n n' : Name} : n.quickCmp n' = Ordering.eq → n = n' := by
|
||||
simp only [Lean.Name.quickCmp, Name.quickCmp, Subtype.eq_iff_val_eq]
|
||||
intro h_cmp; split at h_cmp
|
||||
next => exact Name.eq_of_wf_quickCmpAux n w n' w' h_cmp
|
||||
next => exact Name.eq_of_quickCmpAux n n' h_cmp
|
||||
next => contradiction
|
||||
|
||||
instance : EqOfCmp WfName WfName.quickCmp where
|
||||
eq_of_cmp h := WfName.eq_of_quickCmp h
|
||||
instance : EqOfCmp Name Name.quickCmp where
|
||||
eq_of_cmp h := eq_of_quickCmp h
|
||||
|
||||
open Syntax
|
||||
|
||||
def quoteNameFrom (ref : Syntax) : Name → Term
|
||||
| .anonymous => mkCIdentFrom ref ``anonymous
|
||||
| .str p s _ => mkApp (mkCIdentFrom ref ``mkStr)
|
||||
| .anonymous => mkCIdentFrom ref ``Name.anonymous
|
||||
| .str p s => mkApp (mkCIdentFrom ref ``Name.mkStr)
|
||||
#[quoteNameFrom ref p, quote s]
|
||||
| .num p v _ => mkApp (mkCIdentFrom ref ``mkNum)
|
||||
| .num p v => mkApp (mkCIdentFrom ref ``Name.mkNum)
|
||||
#[quoteNameFrom ref p, quote v]
|
||||
|
||||
protected def quoteFrom (ref : Syntax) : WfName → Term
|
||||
| ⟨n, _⟩ => quoteNameFrom ref n
|
||||
|
||||
instance : Quote WfName := ⟨WfName.quoteFrom Syntax.missing⟩
|
||||
|
||||
end WfName
|
||||
|
||||
-- ## Notation
|
||||
|
||||
/--
|
||||
A proven well-formed, unchecked name literal.
|
||||
|
||||
Lake augments name literals to produce well-formed names (`WfName`)
|
||||
instead of their plain counterparts. Well-formed names have additional
|
||||
properties that help ensure certain features of Lake work as intended.
|
||||
-/
|
||||
scoped macro:max (name := wfNameLit) "&" noWs stx:name : term =>
|
||||
if let some nm := stx.raw.isNameLit? then
|
||||
return WfName.quoteNameFrom stx nm
|
||||
else
|
||||
Macro.throwErrorAt stx "ill-formed name literal"
|
||||
|
||||
scoped notation "&`✝" => WfName.anonymous
|
||||
|
||||
@[scoped appUnexpander WfName.mkStr]
|
||||
def unexpandWfNameMkStr : PrettyPrinter.Unexpander
|
||||
| `($(_) &`✝ $s) => do
|
||||
let some s := s.raw.isStrLit? | throw ()
|
||||
let qn := quote (k := `term) <| Name.mkStr Name.anonymous s
|
||||
`(&$(⟨qn.raw[0]⟩):name)
|
||||
| `($(_) &$n:name $s) => do
|
||||
let some s := s.raw.isStrLit? | throw ()
|
||||
let some n := n.raw.isNameLit? | throw ()
|
||||
let qn := quote (k := `term) <| Name.mkStr n s
|
||||
`(&$(⟨qn.raw[0]⟩):name)
|
||||
| _ => throw ()
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue