refactor: remove dead package DSL code

Author: tydeu

Diff for: Lake/DSL/DeclUtil.lean

@@ -32,6 +32,14 @@ instance : Coe SimpleBinder FunBinder where
 
 ---
 
+def expandAttrs (attrs? : Option Attributes) : Array AttrInstance :=
+  if let some attrs := attrs? then
+    match attrs with
+    | `(Term.attributes| @[$attrs,*]) => attrs
+    | _ => #[]
+  else
+    #[]
+
 syntax structVal :=
   "{" manyIndent(group(Term.structInstField ", "?)) "}"
 
@@ -50,10 +58,25 @@ syntax declValOptTyped :=
 syntax simpleDeclSig :=
   ident Term.typeSpec declValSimple
 
-def expandAttrs (attrs? : Option Attributes) : Array AttrInstance :=
-  if let some attrs := attrs? then
-    match attrs with
-    | `(Term.attributes| @[$attrs,*]) => attrs
-    | _ => #[]
-  else
-    #[]
+syntax structDeclSig :=
+  ident (Command.whereStructInst <|> declValOptTyped <|> declValStruct)?
+
+def fixName (id : Ident) : Option Name → Ident
+| some n => mkIdentFrom id n
+| none => id
+
+def mkConfigStructDecl (name? : Option Name)
+(doc? : Option DocComment) (attrs : Array AttrInstance) (ty : Term)
+: (spec : Syntax) → MacroM Syntax
+| `(structDeclSig| $id:ident) =>
+  `($[$doc?]? @[$attrs,*] def $(fixName id name?) : $ty :=
+    {name := $(quote id.getId)})
+| `(structDeclSig| $id:ident where $ds;* $[$wds?]?) =>
+  `($[$doc?]? @[$attrs,*] def $(fixName id name?) : $ty where
+      name := $(quote id.getId); $ds;* $[$wds?]?)
+| `(structDeclSig| $id:ident $[: $ty?]? := $defn $[$wds?]?) =>
+  `($[$doc?]? @[$attrs,*] def $(fixName id name?) : $(ty?.getD ty) := $defn $[$wds?]?)
+| `(structDeclSig| $id:ident { $[$fs $[,]?]* } $[$wds?]?) => do
+  let defn ← `({ name := $(quote id.getId), $fs,* })
+  `($[$doc?]? @[$attrs,*] def $(fixName id name?) : $ty := $defn $[$wds?]?)
+| stx => Macro.throwErrorAt stx "ill-formed configuration syntax"

Diff for: Lake/DSL/Package.lean

@@ -10,56 +10,11 @@ import Lake.DSL.DeclUtil
 namespace Lake.DSL
 open Lean Parser Command
 
-syntax packageDeclWithBinders :=
-  (ppSpace "(" Term.simpleBinder ")")? -- dir
-  (ppSpace "(" Term.simpleBinder ")")? -- args
-  (declValSimple <|> declValStruct <|> declValDo)
-
-syntax packageDeclSpec :=
-  ident (Command.whereStructInst <|> declValTyped <|> packageDeclWithBinders)?
-
-def expandPackageBinders
-: Option SimpleBinder → Option SimpleBinder → MacroM (Bool × SimpleBinder × SimpleBinder)
-| none,     none      => do let hole ← `(Term.hole|_); return (false, hole, hole)
-| some dir, none      => return (true, dir, ← `(Term.hole|_))
-| none,     some args => return (true, ← `(Term.hole|_), args)
-| some dir, some args => return (true, dir, args)
-
-def mkSimplePackageDecl
-(doc? : Option DocComment) (attrs : Array AttrInstance) (id : Ident) (defn : Term)
-(dir? : Option SimpleBinder) (args? : Option SimpleBinder) (wds? : Option WhereDecls) : MacroM Syntax := do
-  let (hasBinders, dir, args) ← expandPackageBinders dir? args?
-  if hasBinders then
-    `($[$doc?]? @[$attrs,*] def $id : Packager :=
-        (fun $dir $args => $defn) $[$wds?]?)
-  else
-    `($[$doc?]? @[$attrs,*] def $id : PackageConfig := $defn $[$wds?]?)
-
 /-- The name given to the definition created by the `package` syntax. -/
 def packageDeclName := `_package
 
-def mkPackageDecl (doc? : Option DocComment) (attrs : Array AttrInstance) : Macro
-| `(packageDeclSpec| $id:ident) =>
-  `($[$doc?]? @[$attrs,*] def $(mkIdentFrom id packageDeclName) : PackageConfig :=
-    {name := $(quote id.getId)})
-| `(packageDeclSpec| $id:ident where $ds;* $[$wds?]?) =>
-  `($[$doc?]? @[$attrs,*] def $(mkIdentFrom id packageDeclName) : PackageConfig where
-      name := $(quote id.getId); $ds;* $[$wds?]?)
-| `(packageDeclSpec| $id:ident : $ty := $defn $[$wds?]?) =>
-  `($[$doc?]? @[$attrs,*] def $(mkIdentFrom id packageDeclName) : $ty := $defn $[$wds?]?)
-| `(packageDeclSpec| $id:ident $[($dir?)]? $[($args?)]? := $defn $[$wds?]?) =>
-  mkSimplePackageDecl doc? attrs (mkIdentFrom id packageDeclName) defn dir? args? wds?
-| `(packageDeclSpec| $id:ident $[($dir?)]? $[($args?)]? { $[$fs $[,]?]* } $[$wds?]?) => do
-  let defn ← `({ name := $(quote id.getId), $fs,* })
-  mkSimplePackageDecl doc? attrs (mkIdentFrom id packageDeclName) defn dir? args? wds?
-| `(packageDeclSpec| $id:ident $[($dir?)]? $[($args?)]? do $seq $[$wds?]?) => do
-  let (_, dir, args) ← expandPackageBinders dir? args?
-  `($[$doc?]? @[$attrs,*] def $(mkIdentFrom id packageDeclName) : IOPackager :=
-      (fun $dir $args => do $seq) $[$wds?]?)
-| stx => Macro.throwErrorAt stx "ill-formed package declaration"
-
 /--
-Command that declares the configuration of a Lake package.  Has many forms:
+Defines the configuration of a Lake package.  Has many forms:
 
 ```lean
 package «pkg-name»
@@ -68,12 +23,13 @@ package «pkg-name» where /- config opts -/
 package «pkg-name» : PackageConfig := /- config -/
 ```
 
-There can only be one package configuration per lakefile.
+There can only be one `package` declaration per Lake configuration file.
 The defined package configuration will be available for reference as `_package`.
 -/
 scoped macro (name := packageDecl)
 doc?:optional(docComment) attrs?:optional(Term.attributes)
-"package " spec:packageDeclSpec : command => do
+"package " sig:structDeclSig : command => do
   let attr ← `(Term.attrInstance| «package»)
+  let ty := mkCIdentFrom (← getRef) ``PackageConfig
   let attrs := #[attr] ++ expandAttrs attrs?
-  mkPackageDecl doc? attrs spec
+  mkConfigStructDecl packageDeclName doc? attrs ty sig

Diff for: Lake/DSL/Targets.lean

@@ -16,25 +16,6 @@ open Lean Parser Command
 -- # Lean Library & Executable Targets
 --------------------------------------------------------------------------------
 
-syntax targetDeclSpec :=
-  ident (Command.whereStructInst <|> declValOptTyped <|> declValStruct)?
-
-def mkTargetDecl
-(doc? : Option DocComment) (attrs : Array AttrInstance) (ty : Term)
-: (spec : Syntax) → MacroM Syntax
-| `(targetDeclSpec| $id:ident) =>
-  `($[$doc?]? @[$attrs,*] def $id : $ty :=
-    {name := $(quote id.getId)})
-| `(targetDeclSpec| $id:ident where $ds;* $[$wds?]?) =>
-  `($[$doc?]? @[$attrs,*] def $id : $ty where
-      name := $(quote id.getId); $ds;* $[$wds?]?)
-| `(targetDeclSpec| $id:ident $[: $ty?]? := $defn $[$wds?]?) =>
-  `($[$doc?]? @[$attrs,*] def $id : $(ty?.getD ty) := $defn $[$wds?]?)
-| `(targetDeclSpec| $id:ident { $[$fs $[,]?]* } $[$wds?]?) => do
-  let defn ← `({ name := $(quote id.getId), $fs,* })
-  `($[$doc?]? @[$attrs,*] def $id : $ty := $defn $[$wds?]?)
-| stx => Macro.throwErrorAt stx "ill-formed target declaration"
-
 /--
 Define a new Lean library target for the package.
 Can optionally be provided with a configuration of type `LeanLibConfig`.
@@ -49,11 +30,11 @@ lean_lib «target-name» := /- config -/
 -/
 scoped macro (name := leanLibDecl)
 doc?:optional(docComment) attrs?:optional(Term.attributes)
-"lean_lib " spec:targetDeclSpec : command => do
+"lean_lib " sig:structDeclSig : command => do
   let attr ← `(Term.attrInstance| leanLib)
   let ty := mkCIdentFrom (← getRef) ``LeanLibConfig
   let attrs := #[attr] ++ expandAttrs attrs?
-  mkTargetDecl doc? attrs ty spec
+  mkConfigStructDecl none doc? attrs ty sig
 
 /--
 Define a new Lean binary executable target for the package.
@@ -69,11 +50,11 @@ lean_exe «target-name» := /- config -/
 -/
 scoped macro (name := leanExeDecl)
 doc?:optional(docComment) attrs?:optional(Term.attributes)
-"lean_exe " spec:targetDeclSpec : command => do
+"lean_exe " sig:structDeclSig : command => do
   let attr ← `(Term.attrInstance| leanExe)
   let ty := mkCIdentFrom (← getRef) ``LeanExeConfig
   let attrs := #[attr] ++ expandAttrs attrs?
-  mkTargetDecl doc? attrs ty spec
+  mkConfigStructDecl none doc? attrs ty sig
 
 --------------------------------------------------------------------------------
 -- # External Library Target