refactor: DynamicType -> FamilyDef
Uses more principled terminology (i.e., its really an open type family)
This commit is contained in:
tydeu
parent
66e807146b
commit
7049a8da5f
12 changed files with 270 additions and 124 deletions
|
|
@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
|
|||
Authors: Mac Malone
|
||||
-/
|
||||
import Lake.Build.Key
|
||||
import Lake.Util.DynamicType
|
||||
import Lake.Util.Family
|
||||
|
||||
open Lean
|
||||
namespace Lake
|
||||
|
|
@ -14,22 +14,42 @@ namespace Lake
|
|||
--------------------------------------------------------------------------------
|
||||
|
||||
/--
|
||||
Type of build data associated with a module facet in the Lake build store.
|
||||
For example a transitive × direct import pair for `imports` or an active build
|
||||
target for `lean.c`.
|
||||
The open type family which maps a module facet's name to it build data
|
||||
in the Lake build store. For example, a transitive × direct import pair
|
||||
for the `lean.imports` facet or an active build target for `lean.c`.
|
||||
|
||||
It is a dynamic type, meaning additional alternatives can be add lazily
|
||||
as needed.
|
||||
It is an open type, meaning additional mappings can be add lazily
|
||||
as needed (via `module_data`).
|
||||
-/
|
||||
opaque ModuleData (facet : WfName) : Type
|
||||
|
||||
/-- Type of build data associated with package facets (e.g., `extraDep`). -/
|
||||
/--
|
||||
The open type family which maps a package facet's name to it build data
|
||||
in the Lake build store. For example, a transitive dependencies of the package
|
||||
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
|
||||
|
||||
/-- Type of build data associated with Lake targets (e.g., `extern_lib`). -/
|
||||
/--
|
||||
The open type family which maps a (builtin) Lake target's (e.g., `extern_lib`)
|
||||
facet to its associated build data. For example, an active build target for
|
||||
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
|
||||
|
||||
/-- Type of build data associated with custom targets. -/
|
||||
/--
|
||||
The open type family which maps a custom target's name to 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) : Type
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
|
@ -37,9 +57,9 @@ opaque CustomData (target : WfName) : Type
|
|||
--------------------------------------------------------------------------------
|
||||
|
||||
/--
|
||||
Type of the build data associated with a key in the Lake build store.
|
||||
It is dynamic type composed of the three separate dynamic types for modules,
|
||||
packages, and targets.
|
||||
A mapping between a build key and its associated build data in the store.
|
||||
It is a simple type function composed of the separate open type families for
|
||||
modules facets, package facets, Lake target facets, and custom targets.
|
||||
-/
|
||||
abbrev BuildData : BuildKey → Type
|
||||
| .moduleFacet _ f => ModuleData f
|
||||
|
|
@ -56,25 +76,25 @@ 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.quoteFrom id <| WfName.ofName <| id.getId
|
||||
`($[$doc?]? dynamic_data $id : $dty $key := $ty)
|
||||
`($[$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.quoteFrom id <| WfName.ofName <| id.getId
|
||||
`($[$doc?]? dynamic_data $id : $dty $key := $ty)
|
||||
`($[$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.quoteFrom id <| WfName.ofName <| id.getId
|
||||
`($[$doc?]? dynamic_data $id : $dty $key := $ty)
|
||||
`($[$doc?]? family_def $id : $dty $key := $ty)
|
||||
|
||||
/-- Macro for declaring new `CustomData`. -/
|
||||
scoped macro (name := customDataDecl) doc?:optional(Parser.Command.docComment)
|
||||
"custom_data " id:ident " : " ty:term : command => do
|
||||
let dty := mkCIdentFrom (← getRef) ``CustomData
|
||||
let key := WfName.quoteFrom id <| WfName.ofName <| id.getId
|
||||
`($[$doc?]? dynamic_data $id : $dty $key := $ty)
|
||||
`($[$doc?]? family_def $id : $dty $key := $ty)
|
||||
|
|
|
|||
|
|
@ -27,11 +27,11 @@ structure ModuleFacet (α) where
|
|||
data_eq : ModuleData name = α
|
||||
deriving Repr
|
||||
|
||||
instance (facet : ModuleFacet α) : DynamicType ModuleData facet.name α :=
|
||||
instance (facet : ModuleFacet α) : FamilyDef ModuleData facet.name α :=
|
||||
⟨facet.data_eq⟩
|
||||
|
||||
instance [DynamicType ModuleData facet α] : CoeDep WfName facet (ModuleFacet α) :=
|
||||
⟨facet, eq_dynamic_type⟩
|
||||
instance [FamilyDef ModuleData facet α] : CoeDep WfName facet (ModuleFacet α) :=
|
||||
⟨facet, family_key_eq_type⟩
|
||||
|
||||
namespace Module
|
||||
abbrev leanBinFacet := &`lean.bin
|
||||
|
|
|
|||
|
|
@ -55,24 +55,24 @@ Converts a conveniently typed module facet build function into its
|
|||
dynamically typed equivalent.
|
||||
-/
|
||||
@[inline] def mkModuleFacetBuild {facet : WfName} (build : Module → IndexT m α)
|
||||
[h : DynamicType ModuleData facet α] : Module → IndexT m (ModuleData facet) :=
|
||||
cast (by rw [← h.eq_dynamic_type]) build
|
||||
[h : FamilyDef ModuleData facet α] : Module → IndexT m (ModuleData facet) :=
|
||||
cast (by rw [← h.family_key_eq_type]) build
|
||||
|
||||
/--
|
||||
Converts a conveniently typed package facet build function into its
|
||||
dynamically typed equivalent.
|
||||
-/
|
||||
@[inline] def mkPackageFacetBuild {facet : WfName} (build : Package → IndexT m α)
|
||||
[h : DynamicType PackageData facet α] : Package → IndexT m (PackageData facet) :=
|
||||
cast (by rw [← h.eq_dynamic_type]) build
|
||||
[h : FamilyDef PackageData facet α] : Package → IndexT m (PackageData facet) :=
|
||||
cast (by rw [← h.family_key_eq_type]) build
|
||||
|
||||
/--
|
||||
Converts a conveniently typed target facet build function into its
|
||||
dynamically typed equivalent.
|
||||
-/
|
||||
@[inline] def mkTargetFacetBuild (facet : WfName) (build : IndexT m α)
|
||||
[h : DynamicType TargetData facet α] : IndexT m (TargetData facet) :=
|
||||
cast (by rw [← h.eq_dynamic_type]) build
|
||||
[h : FamilyDef TargetData facet α] : IndexT m (TargetData facet) :=
|
||||
cast (by rw [← h.family_key_eq_type]) build
|
||||
|
||||
section
|
||||
variable [Monad m] [MonadLiftT BuildM m] [MonadBuildStore m]
|
||||
|
|
@ -146,7 +146,7 @@ the initial set of Lake package facets (e.g., `extraDep`).
|
|||
build mod
|
||||
else if let some config := (← getWorkspace).findModuleFacetConfig? facet then
|
||||
if h : facet = config.name then
|
||||
have : DynamicType ModuleData facet (ActiveBuildTarget config.resultType) :=
|
||||
have : FamilyDef ModuleData facet (ActiveBuildTarget config.resultType) :=
|
||||
⟨by simp [h]⟩
|
||||
mkModuleFacetBuild config.build mod
|
||||
else
|
||||
|
|
@ -158,7 +158,7 @@ the initial set of Lake package facets (e.g., `extraDep`).
|
|||
build pkg
|
||||
else if let some config := pkg.findPackageFacetConfig? facet then
|
||||
if h : facet = config.name then
|
||||
have : DynamicType PackageData facet (ActiveBuildTarget config.resultType) :=
|
||||
have : FamilyDef PackageData facet (ActiveBuildTarget config.resultType) :=
|
||||
⟨by simp [h]⟩
|
||||
mkPackageFacetBuild config.build pkg
|
||||
else
|
||||
|
|
@ -168,9 +168,9 @@ the initial set of Lake package facets (e.g., `extraDep`).
|
|||
| .customTarget pkg target =>
|
||||
if let some config := pkg.findTargetConfig? target then
|
||||
if h : target = config.name then
|
||||
have h' : DynamicType CustomData target (ActiveBuildTarget config.resultType) :=
|
||||
have h' : FamilyDef CustomData target (ActiveBuildTarget config.resultType) :=
|
||||
⟨by simp [h]⟩
|
||||
liftM <| cast (by rw [← h'.eq_dynamic_type]) <| config.target.activate
|
||||
liftM <| cast (by rw [← h'.family_key_eq_type]) <| config.target.activate
|
||||
else
|
||||
error "target's name in the configuration does not match the name it was registered with"
|
||||
else
|
||||
|
|
@ -200,23 +200,23 @@ Recursively build the given info using the Lake build index
|
|||
and a topological / suspending scheduler and return the dynamic result.
|
||||
-/
|
||||
@[inline] def buildIndexTop (info : BuildInfo)
|
||||
[DynamicType BuildData info.key α] : CycleT BuildKey m α := do
|
||||
[FamilyDef BuildData info.key α] : CycleT BuildKey m α := do
|
||||
cast (by simp) <| buildIndexTop' (m := m) info
|
||||
|
||||
end
|
||||
|
||||
/- Build the given Lake target using the given Lake build store. -/
|
||||
@[inline] def BuildInfo.buildIn (store : BuildStore) (self : BuildInfo)
|
||||
[DynamicType BuildData self.key α] : BuildM α := do
|
||||
[FamilyDef BuildData self.key α] : BuildM α := do
|
||||
failOnBuildCycle <| ← EStateT.run' (m := BuildM) store <| buildIndexTop self
|
||||
|
||||
/- Build the given Lake target in a fresh build store. -/
|
||||
@[inline] def BuildInfo.build (self : BuildInfo) [DynamicType BuildData self.key α] : BuildM α :=
|
||||
@[inline] def BuildInfo.build (self : BuildInfo) [FamilyDef BuildData self.key α] : BuildM α :=
|
||||
buildIn BuildStore.empty self
|
||||
|
||||
export BuildInfo (build buildIn)
|
||||
|
||||
/-- An opaque target that builds the Lake target in a fresh build store. -/
|
||||
@[inline] def BuildInfo.target (self : BuildInfo)
|
||||
[DynamicType BuildData self.key (ActiveBuildTarget α)] : OpaqueTarget :=
|
||||
[FamilyDef BuildData self.key (ActiveBuildTarget α)] : OpaqueTarget :=
|
||||
BuildTarget.mk' () <| self.build <&> (·.task)
|
||||
|
|
|
|||
|
|
@ -13,7 +13,7 @@ namespace Lake
|
|||
-- # Module Facet Targets
|
||||
|
||||
@[inline] def Module.facetTarget (facet : WfName) (self : Module)
|
||||
[DynamicType ModuleData facet (ActiveBuildTarget α)] : OpaqueTarget :=
|
||||
[FamilyDef ModuleData facet (ActiveBuildTarget α)] : OpaqueTarget :=
|
||||
self.facet facet |>.target
|
||||
|
||||
@[inline] def Module.oleanTarget (self : Module) : FileTarget :=
|
||||
|
|
@ -36,7 +36,7 @@ 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)
|
||||
[DynamicType ModuleData facet (ActiveBuildTarget α)] : SchedulerM Job := do
|
||||
[FamilyDef ModuleData facet (ActiveBuildTarget α)] : SchedulerM Job := do
|
||||
let buildMods : BuildM _ := do
|
||||
let mods ← self.getModuleArray
|
||||
let modTargets ← failOnBuildCycle <| ← EStateT.run' BuildStore.empty
|
||||
|
|
|
|||
|
|
@ -74,37 +74,37 @@ abbrev BuildInfo.key : (self : BuildInfo) → BuildKey
|
|||
|
||||
/-! ### Instances for deducing data types of `BuildInfo` keys -/
|
||||
|
||||
instance [DynamicType ModuleData f α]
|
||||
: DynamicType BuildData (BuildInfo.key (.moduleFacet m f)) α where
|
||||
eq_dynamic_type := by unfold BuildData; simp
|
||||
instance [FamilyDef ModuleData f α]
|
||||
: FamilyDef BuildData (BuildInfo.key (.moduleFacet m f)) α where
|
||||
family_key_eq_type := by unfold BuildData; simp
|
||||
|
||||
instance [DynamicType PackageData f α]
|
||||
: DynamicType BuildData (BuildInfo.key (.packageFacet p f)) α where
|
||||
eq_dynamic_type := by unfold BuildData; simp
|
||||
instance [FamilyDef PackageData f α]
|
||||
: FamilyDef BuildData (BuildInfo.key (.packageFacet p f)) α where
|
||||
family_key_eq_type := by unfold BuildData; simp
|
||||
|
||||
instance [DynamicType CustomData t α]
|
||||
: DynamicType BuildData (BuildInfo.key (.customTarget p t)) α where
|
||||
eq_dynamic_type := by unfold BuildData; simp
|
||||
instance [FamilyDef CustomData t α]
|
||||
: FamilyDef BuildData (BuildInfo.key (.customTarget p t)) α where
|
||||
family_key_eq_type := by unfold BuildData; simp
|
||||
|
||||
instance [DynamicType TargetData LeanLib.staticFacet α]
|
||||
: DynamicType BuildData (BuildInfo.key (.staticLeanLib l)) α where
|
||||
eq_dynamic_type := by unfold BuildData; simp
|
||||
instance [FamilyDef TargetData LeanLib.staticFacet α]
|
||||
: FamilyDef BuildData (BuildInfo.key (.staticLeanLib l)) α where
|
||||
family_key_eq_type := by unfold BuildData; simp
|
||||
|
||||
instance [DynamicType TargetData LeanLib.sharedFacet α]
|
||||
: DynamicType BuildData (BuildInfo.key (.sharedLeanLib l)) α where
|
||||
eq_dynamic_type := by unfold BuildData; simp
|
||||
instance [FamilyDef TargetData LeanLib.sharedFacet α]
|
||||
: FamilyDef BuildData (BuildInfo.key (.sharedLeanLib l)) α where
|
||||
family_key_eq_type := by unfold BuildData; simp
|
||||
|
||||
instance [DynamicType TargetData LeanExe.facet α]
|
||||
: DynamicType BuildData (BuildInfo.key (.leanExe x)) α where
|
||||
eq_dynamic_type := by unfold BuildData; simp
|
||||
instance [FamilyDef TargetData LeanExe.facet α]
|
||||
: FamilyDef BuildData (BuildInfo.key (.leanExe x)) α where
|
||||
family_key_eq_type := by unfold BuildData; simp
|
||||
|
||||
instance [DynamicType TargetData ExternLib.staticFacet α]
|
||||
: DynamicType BuildData (BuildInfo.key (.staticExternLib l)) α where
|
||||
eq_dynamic_type := by unfold BuildData; simp
|
||||
instance [FamilyDef TargetData ExternLib.staticFacet α]
|
||||
: FamilyDef BuildData (BuildInfo.key (.staticExternLib l)) α where
|
||||
family_key_eq_type := by unfold BuildData; simp
|
||||
|
||||
instance [DynamicType TargetData ExternLib.sharedFacet α]
|
||||
: DynamicType BuildData (BuildInfo.key (.sharedExternLib l)) α where
|
||||
eq_dynamic_type := by unfold BuildData; simp
|
||||
instance [FamilyDef TargetData ExternLib.sharedFacet α]
|
||||
: FamilyDef BuildData (BuildInfo.key (.sharedExternLib l)) α where
|
||||
family_key_eq_type := by unfold BuildData; simp
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
/-! ## Recursive Building -/
|
||||
|
|
@ -119,7 +119,7 @@ abbrev IndexBuildFn (m : Type → Type v) :=
|
|||
abbrev IndexT (m : Type → Type v) := EquipT (IndexBuildFn m) m
|
||||
|
||||
/-- Build the given info using the Lake build index. -/
|
||||
@[inline] def BuildInfo.recBuild (self : BuildInfo) [DynamicType BuildData self.key α] : IndexT m α :=
|
||||
@[inline] def BuildInfo.recBuild (self : BuildInfo) [FamilyDef BuildData self.key α] : IndexT m α :=
|
||||
fun build => cast (by simp) <| build self
|
||||
|
||||
export BuildInfo (recBuild)
|
||||
|
|
|
|||
|
|
@ -32,57 +32,57 @@ set_option linter.unusedVariables false
|
|||
|
||||
/-- Derive an array of built module facets from the store. -/
|
||||
def collectModuleFacetArray (self : BuildStore)
|
||||
(facet : WfName) [DynamicType ModuleData facet α] : Array α := Id.run do
|
||||
(facet : WfName) [FamilyDef ModuleData facet α] : Array α := Id.run do
|
||||
let mut res : Array α := #[]
|
||||
for ⟨k, v⟩ in self do
|
||||
match k with
|
||||
| .moduleFacet m f =>
|
||||
if h : f = facet then
|
||||
have of_data := by unfold BuildData; simp [h, eq_dynamic_type]
|
||||
have of_data := by unfold BuildData; simp [h, family_key_eq_type]
|
||||
res := res.push <| cast of_data v
|
||||
| _ => pure ()
|
||||
return res
|
||||
|
||||
/-- Derive a map of module names to built facets from the store. -/
|
||||
def collectModuleFacetMap (self : BuildStore)
|
||||
(facet : WfName) [DynamicType ModuleData facet α] : NameMap α := Id.run do
|
||||
(facet : WfName) [FamilyDef ModuleData facet α] : NameMap α := Id.run do
|
||||
let mut res := Lean.mkNameMap α
|
||||
for ⟨k, v⟩ in self do
|
||||
match k with
|
||||
| .moduleFacet m f =>
|
||||
if h : f = facet then
|
||||
have of_data := by unfold BuildData; simp [h, eq_dynamic_type]
|
||||
have of_data := by unfold BuildData; simp [h, family_key_eq_type]
|
||||
res := res.insert m <| cast of_data v
|
||||
| _ => pure ()
|
||||
return res
|
||||
|
||||
/-- Derive an array of built package facets from the store. -/
|
||||
def collectPackageFacetArray (self : BuildStore)
|
||||
(facet : WfName) [DynamicType PackageData facet α] : Array α := Id.run do
|
||||
(facet : WfName) [FamilyDef PackageData facet α] : Array α := Id.run do
|
||||
let mut res : Array α := #[]
|
||||
for ⟨k, v⟩ in self do
|
||||
match k with
|
||||
| .packageFacet _ f =>
|
||||
if h : f = facet then
|
||||
have of_data := by unfold BuildData; simp [h, eq_dynamic_type]
|
||||
have of_data := by unfold BuildData; simp [h, family_key_eq_type]
|
||||
res := res.push <| cast of_data v
|
||||
| _ => pure ()
|
||||
return res
|
||||
|
||||
/-- Derive an array of built target facets from the store. -/
|
||||
def collectTargetFacetArray (self : BuildStore)
|
||||
(facet : WfName) [DynamicType TargetData facet α] : Array α := Id.run do
|
||||
(facet : WfName) [FamilyDef TargetData facet α] : Array α := Id.run do
|
||||
let mut res : Array α := #[]
|
||||
for ⟨k, v⟩ in self do
|
||||
match k with
|
||||
| .targetFacet _ _ f =>
|
||||
if h : f = facet then
|
||||
have of_data := by unfold BuildData; simp [h, eq_dynamic_type]
|
||||
have of_data := by unfold BuildData; simp [h, family_key_eq_type]
|
||||
res := res.push <| cast of_data v
|
||||
| _ => pure ()
|
||||
return res
|
||||
|
||||
/-- Derive an array of built external shared libraries from the store. -/
|
||||
def collectSharedExternLibs (self : BuildStore)
|
||||
[DynamicType TargetData &`externLib.shared α] : Array α :=
|
||||
[FamilyDef TargetData &`externLib.shared α] : Array α :=
|
||||
self.collectTargetFacetArray &`externLib.shared
|
||||
|
|
|
|||
|
|
@ -26,13 +26,13 @@ instance : Inhabited ModuleFacetConfig := ⟨{
|
|||
name := Module.leanBinFacet
|
||||
resultType := PUnit
|
||||
build := default
|
||||
data_eq_target := eq_dynamic_type
|
||||
data_eq_target := family_key_eq_type
|
||||
}⟩
|
||||
|
||||
hydrate_opaque_type OpaqueModuleFacetConfig ModuleFacetConfig
|
||||
|
||||
instance {cfg : ModuleFacetConfig}
|
||||
: DynamicType ModuleData cfg.name (ActiveBuildTarget cfg.resultType) :=
|
||||
: FamilyDef ModuleData cfg.name (ActiveBuildTarget cfg.resultType) :=
|
||||
⟨cfg.data_eq_target⟩
|
||||
|
||||
/-- Try to find a module facet configuration in the package with the given name . -/
|
||||
|
|
|
|||
|
|
@ -25,13 +25,13 @@ instance : Inhabited PackageFacetConfig := ⟨{
|
|||
name := &`extraDep
|
||||
resultType := PUnit
|
||||
build := default
|
||||
data_eq_target := eq_dynamic_type
|
||||
data_eq_target := family_key_eq_type
|
||||
}⟩
|
||||
|
||||
hydrate_opaque_type OpaquePackageFacetConfig PackageFacetConfig
|
||||
|
||||
instance (cfg : PackageFacetConfig)
|
||||
: DynamicType PackageData cfg.name (ActiveBuildTarget cfg.resultType) :=
|
||||
: FamilyDef PackageData cfg.name (ActiveBuildTarget cfg.resultType) :=
|
||||
⟨cfg.data_eq_target⟩
|
||||
|
||||
/-- Try to find a package configuration in the package with the given name . -/
|
||||
|
|
|
|||
|
|
@ -25,13 +25,13 @@ instance : Inhabited TargetConfig := ⟨{
|
|||
name := &`_nil_
|
||||
resultType := PUnit
|
||||
target := default
|
||||
data_eq_target := eq_dynamic_type
|
||||
data_eq_target := family_key_eq_type
|
||||
}⟩
|
||||
|
||||
hydrate_opaque_type OpaqueTargetConfig TargetConfig
|
||||
|
||||
instance dynamicTypeOfTargetConfig {cfg : TargetConfig}
|
||||
: DynamicType CustomData cfg.name (ActiveBuildTarget cfg.resultType) :=
|
||||
instance FamilyDefOfTargetConfig {cfg : TargetConfig}
|
||||
: FamilyDef CustomData cfg.name (ActiveBuildTarget cfg.resultType) :=
|
||||
⟨cfg.data_eq_target⟩
|
||||
|
||||
/-- Try to find a target configuration in the package with the given name . -/
|
||||
|
|
|
|||
|
|
@ -1,44 +0,0 @@
|
|||
/-
|
||||
Copyright (c) 2022 Mac Malone. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Mac Malone
|
||||
-/
|
||||
import Lean.Parser.Command
|
||||
|
||||
open Lean
|
||||
namespace Lake
|
||||
|
||||
class DynamicType {α : Type u} (Δ : α → Type v) (a : α) (β : outParam $ Type v) : Prop where
|
||||
eq_dynamic_type : Δ a = β
|
||||
|
||||
export DynamicType (eq_dynamic_type)
|
||||
|
||||
attribute [simp] eq_dynamic_type
|
||||
|
||||
@[inline] def toDynamic (a : α) [DynamicType Δ a β] (b : β) : Δ a :=
|
||||
cast eq_dynamic_type.symm b
|
||||
|
||||
@[inline] def ofDynamic (a : α) [DynamicType Δ a β] (b : Δ a) : β :=
|
||||
cast eq_dynamic_type b
|
||||
|
||||
/--
|
||||
The syntax:
|
||||
|
||||
```lean
|
||||
dynamic_data foo : Data 0 := Nat
|
||||
```
|
||||
|
||||
Declares a new alternative for the dynamic `Data` type via the
|
||||
production of an axiom `foo : Data 0 = Nat` and an instance of `DynamicType`
|
||||
that uses this axiom for key `0`.
|
||||
-/
|
||||
scoped macro (name := dynamicDataDecl) doc?:optional(Parser.Command.docComment)
|
||||
"dynamic_data " id:ident " : " dty:ident key:term " := " ty:term : command => do
|
||||
let tid := extractMacroScopes dty.getId |>.name
|
||||
if let (tid, _) :: _ ← Macro.resolveGlobalName tid then
|
||||
let app := Syntax.mkApp dty #[key]
|
||||
let axm := mkIdentFrom dty <| `_root_ ++ tid ++ id.getId
|
||||
`($[$doc?]? @[simp] axiom $axm : $app = $ty
|
||||
instance : DynamicType $dty $key $ty := ⟨$axm⟩)
|
||||
else
|
||||
Macro.throwErrorAt dty s!"unknown identifier '{tid}'"
|
||||
170
Lake/Util/Family.lean
Normal file
170
Lake/Util/Family.lean
Normal file
|
|
@ -0,0 +1,170 @@
|
|||
/-
|
||||
Copyright (c) 2022 Mac Malone. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Mac Malone
|
||||
-/
|
||||
import Lean.Parser.Command
|
||||
|
||||
/-!
|
||||
# Open Type Families in Lean
|
||||
|
||||
This module contains utilities for defining **open type families** in Lean.
|
||||
|
||||
The concept of type families originated in Haskell with the paper
|
||||
(*Type checking with open type functions*](https://doi.org/10.1145/1411204.1411215)
|
||||
by Schrijvers *et al.* and is essentially just a fancy name for a function from
|
||||
an input *index* to an output type. However, it tends to imply some additional
|
||||
restrictions on syntax or functionality as opposed to a proper type function.
|
||||
The design here has some such limitations so the name was similarly adopted.
|
||||
|
||||
Type families come in two forms: open and closed.
|
||||
A *closed* type family is an ordinary total function.
|
||||
An *open* type family, on the other hand, is a partial function that allows
|
||||
additional input to output mappings to be defined as needed.
|
||||
|
||||
Lean does not (currently) directly support open type families.
|
||||
However, it does support type class *functional dependencies* (via `outParam`),
|
||||
and simple open type families can be modeled through functional dependencies,
|
||||
which is what we do here.
|
||||
|
||||
## Defining Families
|
||||
|
||||
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
|
||||
```
|
||||
|
||||
Note that, unlike Haskell, the key need not be a type. Lean's dependent type
|
||||
theory does not have Haskell's strict separation of types and data and thus
|
||||
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
|
||||
```
|
||||
|
||||
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⟩
|
||||
```
|
||||
|
||||
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
|
||||
```
|
||||
|
||||
## Type Inference
|
||||
|
||||
The signature of the type class `FamilyDef` is
|
||||
|
||||
```
|
||||
FamilyDef {α : Type u} (Fam : α → Type v) (a : α) (β : outParam $ Type v) : Prop
|
||||
```
|
||||
|
||||
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
|
||||
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`.
|
||||
|
||||
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
|
||||
vice versa). Thus, this module provides two definitions, `toFamily : β → Fam a`
|
||||
and `ofFamily : Fam a → β`, to help with this conversion.
|
||||
|
||||
## Full Example
|
||||
|
||||
Putting this all together, one can do something like the following:
|
||||
|
||||
```lean
|
||||
opaque FooFam (key : WfName) : Type
|
||||
|
||||
abbrev FooMap := DRBMap WfName FooFam WfName.quickCmp
|
||||
def FooMap.insert (self : FooMap) (key : WfName) [FamilyDef FooFam key α] (a : α) : FooMap :=
|
||||
DRBMap.insert self key (toFamily a)
|
||||
def FooMap.find? (self : FooMap) (key : WfName) [FamilyDef FooFam key α] : Option α :=
|
||||
ofFamily <$> DRBMap.find? self key
|
||||
|
||||
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
|
||||
|
||||
#eval foo -- 5
|
||||
```
|
||||
|
||||
## Type Safety
|
||||
|
||||
In order to maintain type safety, `a = b → Fam a = Fam b` must actually hold.
|
||||
That is, one must not define mapping to two different types with equivalent
|
||||
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
|
||||
if two keys overlap and thereby producing an error.
|
||||
-/
|
||||
|
||||
open Lean
|
||||
namespace Lake
|
||||
|
||||
/-! ## API Documentation -/
|
||||
|
||||
/--
|
||||
Defines a single mapping of the **open type family** `Fam`, namely `Fam a = β`.
|
||||
See the module documentation of `Lake.Util.Family` for details what an open type
|
||||
family is in Lake.
|
||||
-/
|
||||
class FamilyDef {α : Type u} (Fam : α → Type v) (a : α) (β : outParam $ Type v) : Prop where
|
||||
family_key_eq_type : Fam a = β
|
||||
|
||||
export FamilyDef (family_key_eq_type)
|
||||
|
||||
-- Simplifies proofs involving open type families.
|
||||
attribute [simp] family_key_eq_type
|
||||
|
||||
/-- Cast a datum from its individual type to its general family. -/
|
||||
@[macroInline] def toFamily [FamilyDef Fam a β] (b : β) : Fam a :=
|
||||
cast family_key_eq_type.symm b
|
||||
|
||||
/-- Cast a datum from its general family to its individual type. -/
|
||||
@[macroInline] def ofFamily [FamilyDef Fam a β] (b : Fam a) : β :=
|
||||
cast family_key_eq_type b
|
||||
|
||||
/--
|
||||
The syntax:
|
||||
|
||||
```lean
|
||||
family_def foo : Fam 0 := Nat
|
||||
```
|
||||
|
||||
Declares a new mapping for the open type family `Fam` type via the
|
||||
production of an axiom `Fam.foo : Data 0 = Nat` and an instance of `FamilyDef`
|
||||
that uses this axiom for key `0`.
|
||||
-/
|
||||
scoped macro (name := familyDef) doc?:optional(Parser.Command.docComment)
|
||||
"family_def " id:ident " : " fam:ident key:term " := " ty:term : command => do
|
||||
let tid := extractMacroScopes fam.getId |>.name
|
||||
if let (tid, _) :: _ ← Macro.resolveGlobalName tid then
|
||||
let app := Syntax.mkApp fam #[key]
|
||||
let axm := mkIdentFrom fam <| `_root_ ++ tid ++ id.getId
|
||||
`($[$doc?]? @[simp] axiom $axm : $app = $ty
|
||||
instance : FamilyDef $fam $key $ty := ⟨$axm⟩)
|
||||
else
|
||||
Macro.throwErrorAt fam s!"unknown family '{tid}'"
|
||||
|
|
@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
|
|||
Authors: Mac Malone
|
||||
-/
|
||||
import Lake.Util.DRBMap
|
||||
import Lake.Util.DynamicType
|
||||
import Lake.Util.Family
|
||||
import Lake.Util.Store
|
||||
|
||||
open Std
|
||||
|
|
@ -18,6 +18,6 @@ instance [Monad m] : MonadStore κ α (StateT (RBMap κ α cmp) m) where
|
|||
fetch? k := return (← get).find? k
|
||||
store k a := modify (·.insert k a)
|
||||
|
||||
@[inline] instance [MonadDStore κ β m] [t : DynamicType β k α] : MonadStore1 k α m where
|
||||
fetch? := cast (by rw [t.eq_dynamic_type]) <| fetch? (m := m) k
|
||||
store a := store k <| cast t.eq_dynamic_type.symm a
|
||||
@[inline] instance [MonadDStore κ β m] [t : FamilyDef β k α] : MonadStore1 k α m where
|
||||
fetch? := cast (by rw [t.family_key_eq_type]) <| fetch? (m := m) k
|
||||
store a := store k <| cast t.family_key_eq_type.symm a
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue