From 372e00b5208f93c537dea37bc162adbd86b95dc6 Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Mon, 11 Jul 2022 22:18:45 +0200 Subject: [PATCH] chore: hash field in `Name` was dropped --- Lake/Build/Data.lean | 18 +-- Lake/Build/Facets.lean | 26 ++-- Lake/Build/Index.lean | 18 +-- Lake/Build/IndexTargets.lean | 4 +- Lake/Build/Info.lean | 22 +-- Lake/Build/Key.lean | 8 +- Lake/Build/Roots.lean | 2 +- Lake/Build/Store.lean | 12 +- Lake/CLI/Build.lean | 46 +++--- Lake/Config/ExternLib.lean | 4 +- Lake/Config/FacetConfig.lean | 10 +- Lake/Config/Glob.lean | 12 +- Lake/Config/LeanExe.lean | 8 +- Lake/Config/LeanLib.lean | 4 +- Lake/Config/Load.lean | 7 +- Lake/Config/Module.lean | 7 +- Lake/Config/Opaque.lean | 4 +- Lake/Config/Package.lean | 6 +- Lake/Config/TargetConfig.lean | 10 +- Lake/Config/Workspace.lean | 4 +- Lake/DSL/Facets.lean | 8 +- Lake/Util/Casing.lean | 2 +- Lake/Util/Compare.lean | 21 +++ Lake/Util/Family.lean | 38 ++--- Lake/Util/Name.lean | 272 ++++------------------------------ 25 files changed, 190 insertions(+), 383 deletions(-) diff --git a/Lake/Build/Data.lean b/Lake/Build/Data.lean index 8006f1b..10fa881 100644 --- a/Lake/Build/Data.lean +++ b/Lake/Build/Data.lean @@ -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) diff --git a/Lake/Build/Facets.lean b/Lake/Build/Facets.lean index 9dbe018..9fa87f7 100644 --- a/Lake/Build/Facets.lean +++ b/Lake/Build/Facets.lean @@ -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 diff --git a/Lake/Build/Index.lean b/Lake/Build/Index.lean index 4aeada7..1322ec6 100644 --- a/Lake/Build/Index.lean +++ b/Lake/Build/Index.lean @@ -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 diff --git a/Lake/Build/IndexTargets.lean b/Lake/Build/IndexTargets.lean index ce2bd1d..992d631 100644 --- a/Lake/Build/IndexTargets.lean +++ b/Lake/Build/IndexTargets.lean @@ -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 diff --git a/Lake/Build/Info.lean b/Lake/Build/Info.lean index 3ba280d..56ae364 100644 --- a/Lake/Build/Info.lean +++ b/Lake/Build/Info.lean @@ -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. -/ diff --git a/Lake/Build/Key.lean b/Lake/Build/Key.lean index 3a60cdf..e42eba7 100644 --- a/Lake/Build/Key.lean +++ b/Lake/Build/Key.lean @@ -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 diff --git a/Lake/Build/Roots.lean b/Lake/Build/Roots.lean index 8755a93..9a5610c 100644 --- a/Lake/Build/Roots.lean +++ b/Lake/Build/Roots.lean @@ -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 diff --git a/Lake/Build/Store.lean b/Lake/Build/Store.lean index a16f255..cb88133 100644 --- a/Lake/Build/Store.lean +++ b/Lake/Build/Store.lean @@ -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 diff --git a/Lake/CLI/Build.lean b/Lake/CLI/Build.lean index a0634b7..8b7f9e4 100644 --- a/Lake/CLI/Build.lean +++ b/Lake/CLI/Build.lean @@ -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 ':' diff --git a/Lake/Config/ExternLib.lean b/Lake/Config/ExternLib.lean index 2203cf3..c7ff518 100644 --- a/Lake/Config/ExternLib.lean +++ b/Lake/Config/ExternLib.lean @@ -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 := diff --git a/Lake/Config/FacetConfig.lean b/Lake/Config/FacetConfig.lean index 0143b43..9f0edb4 100644 --- a/Lake/Config/FacetConfig.lean +++ b/Lake/Config/FacetConfig.lean @@ -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. -/ diff --git a/Lake/Config/Glob.lean b/Lake/Config/Glob.lean index 50219b9..227d10a 100644 --- a/Lake/Config/Glob.lean +++ b/Lake/Config/Glob.lean @@ -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 ++ ·) diff --git a/Lake/Config/LeanExe.lean b/Lake/Config/LeanExe.lean index a39c182..d6ae0e1 100644 --- a/Lake/Config/LeanExe.lean +++ b/Lake/Config/LeanExe.lean @@ -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 := diff --git a/Lake/Config/LeanLib.lean b/Lake/Config/LeanLib.lean index c63521f..c8f171b 100644 --- a/Lake/Config/LeanLib.lean +++ b/Lake/Config/LeanLib.lean @@ -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 := diff --git a/Lake/Config/Load.lean b/Lake/Config/Load.lean index af8a25b..314904b 100644 --- a/Lake/Config/Load.lean +++ b/Lake/Config/Load.lean @@ -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 diff --git a/Lake/Config/Module.lean b/Lake/Config/Module.lean index a3799d6..3b39db2 100644 --- a/Lake/Config/Module.lean +++ b/Lake/Config/Module.lean @@ -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 diff --git a/Lake/Config/Opaque.lean b/Lake/Config/Opaque.lean index 5ee9ab8..14d7812 100644 --- a/Lake/Config/Opaque.lean +++ b/Lake/Config/Opaque.lean @@ -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 diff --git a/Lake/Config/Package.lean b/Lake/Config/Package.lean index 9a32aaa..ac196db 100644 --- a/Lake/Config/Package.lean +++ b/Lake/Config/Package.lean @@ -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 diff --git a/Lake/Config/TargetConfig.lean b/Lake/Config/TargetConfig.lean index 0f28f89..4fad3ab 100644 --- a/Lake/Config/TargetConfig.lean +++ b/Lake/Config/TargetConfig.lean @@ -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 diff --git a/Lake/Config/Workspace.lean b/Lake/Config/Workspace.lean index 45d4290..d57215e 100644 --- a/Lake/Config/Workspace.lean +++ b/Lake/Config/Workspace.lean @@ -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. -/ diff --git a/Lake/DSL/Facets.lean b/Lake/DSL/Facets.lean index 87546c4..d575af0 100644 --- a/Lake/DSL/Facets.lean +++ b/Lake/DSL/Facets.lean @@ -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 diff --git a/Lake/Util/Casing.lean b/Lake/Util/Casing.lean index 9bb5c43..662c339 100644 --- a/Lake/Util/Casing.lean +++ b/Lake/Util/Casing.lean @@ -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 diff --git a/Lake/Util/Compare.lean b/Lake/Util/Compare.lean index 1342c57..15ce286 100644 --- a/Lake/Util/Compare.lean +++ b/Lake/Util/Compare.lean @@ -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 diff --git a/Lake/Util/Family.lean b/Lake/Util/Family.lean index 8c226d6..b3aa1fa 100644 --- a/Lake/Util/Family.lean +++ b/Lake/Util/Family.lean @@ -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. -/ diff --git a/Lake/Util/Name.lean b/Lake/Util/Name.lean index 0478b73..5a0be2a 100644 --- a/Lake/Util/Name.lean +++ b/Lake/Util/Name.lean @@ -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 - -def WellFormed.elimStr : WellFormed (Name.str p s h) → WellFormed p -| strWff w rfl => w +attribute [local simp] Name.quickCmpAux -def WellFormed.elimNum : WellFormed (Name.num p v h) → WellFormed p -| numWff 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] -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 ()