From e26a040bb753ed990f38886eba0b996a84f2ea7e Mon Sep 17 00:00:00 2001
From: tydeu <tydeu@hatpress.net>
Date: Wed, 8 Jun 2022 17:06:03 -0400
Subject: [PATCH] feat: syntax for defining extra lib & exe targets

---
 Lake/Config/Load.lean          | 12 ++++++--
 Lake/Config/Package.lean       | 35 +++++++----------------
 Lake/Config/Targets.lean       | 30 +++++++++++++-------
 Lake/DSL.lean                  |  3 +-
 Lake/DSL/Attributes.lean       |  6 ++++
 Lake/DSL/DeclUtil.lean         | 14 +++++++++
 Lake/DSL/Package.lean          |  5 +---
 Lake/DSL/Targets.lean          | 52 ++++++++++++++++++++++++++++++++++
 examples/targets/lakefile.lean | 33 ++++++---------------
 9 files changed, 121 insertions(+), 69 deletions(-)
 create mode 100644 Lake/DSL/Targets.lean

diff --git a/Lake/Config/Load.lean b/Lake/Config/Load.lean
index 6d0ca76..f98d331 100644
--- a/Lake/Config/Load.lean
+++ b/Lake/Config/Load.lean
@@ -40,8 +40,6 @@ unsafe def evalScriptDecl
     env.evalConstCheck ScriptFn leanOpts ``ScriptFn declName
   return {fn, doc? := (← findDocString? env declName)}
 
-namespace Package
-
 deriving instance BEq, Hashable for Import
 
 /- Cache for the imported header environment of Lake configuration files. -/
@@ -62,6 +60,8 @@ def processHeader (header : Syntax) (opts : Options) (trustLevel : UInt32)
     modify (·.add { fileName := inputCtx.fileName, data := toString e, pos })
     mkEmptyEnvironment
 
+namespace Package
+
 /-- Unsafe implementation of `load`. -/
 unsafe def loadUnsafe (dir : FilePath) (args : List String := [])
 (configFile := dir / defaultConfigFile) (leanOpts := Options.empty)
@@ -97,7 +97,13 @@ unsafe def loadUnsafe (dir : FilePath) (args : List String := [])
       let config := {config with dependencies := depsExt.getState env ++ config.dependencies}
       let scripts ← scriptAttr.ext.getState env |>.foldM (init := {})
         fun m d => return m.insert d <| ← evalScriptDecl env d leanOpts
-      return {dir, config, scripts}
+      let libs ← leanLibAttr.ext.getState env |>.foldM (init := {}) fun m d =>
+        let eval := env.evalConstCheck LeanLibConfig leanOpts ``LeanLibConfig d
+        return m.insert d <| ← IO.ofExcept eval.run.run
+      let exes ← leanExeAttr.ext.getState env |>.foldM (init := {}) fun m d =>
+        let eval := env.evalConstCheck LeanExeConfig leanOpts ``LeanExeConfig d
+        return m.insert d <| ← IO.ofExcept eval.run.run
+      return {dir, config, scripts, libs, exes}
     | _ => error s!"configuration file has multiple `package` declarations"
   else
     error s!"package configuration `{configFile}` has errors"
diff --git a/Lake/Config/Package.lean b/Lake/Config/Package.lean
index e4075ac..13ef3a4 100644
--- a/Lake/Config/Package.lean
+++ b/Lake/Config/Package.lean
@@ -217,12 +217,6 @@ structure PackageConfig extends WorkspaceConfig where
   -/
   moreLinkArgs : Array String := #[]
 
-  /-- Additional library targets for the package. -/
-  libConfigs : NameMap LeanLibConfig := {}
-
-  /-- Additional binary executable targets for the package. -/
-  exeConfigs : NameMap LeanExeConfig := {}
-
 deriving Inhabited
 
 namespace PackageConfig
@@ -252,13 +246,12 @@ structure Package where
   dir : FilePath
   /-- The package's configuration. -/
   config : PackageConfig
-  /--
-  A `NameMap` of scripts for the package.
-
-  A `Script` is a `(args : List String) → IO UInt32` definition with
-  a `@[script]` tag that can be run by `lake run <script> [-- <args>]`.
-  -/
+  /-- Scripts for the package. -/
   scripts : NameMap Script := {}
+  /-- Additional Lean library targets for the package. -/
+  libs : NameMap LeanLibConfig := {}
+  /-- Additional Lean binary executable targets for the package. -/
+  exes : NameMap LeanExeConfig := {}
   deriving Inhabited
 
 namespace OpaquePackage
@@ -312,21 +305,13 @@ def extraDepTarget (self : Package) : OpaqueTarget :=
 def defaultFacet (self : Package) : PackageFacet :=
    self.config.defaultFacet
 
-/-- The package's `libConfigs` configuration. -/
-def libConfigs (self : Package) : NameMap LeanLibConfig :=
-  self.config.libConfigs
-
 /-- Get the package's library configuration with the given name. -/
 def findLib? (self : Package) (name : Name) : Option LeanLibConfig :=
-  self.libConfigs.find? name
-
-/-- The package's `exeConfigs` configuration. -/
-def exeConfigs (self : Package) : NameMap LeanExeConfig :=
-  self.config.exeConfigs
+  self.libs.find? name
 
 /-- Get the package's executable configuration with the given name. -/
 def findExe? (self : Package) (name : Name) : Option LeanExeConfig :=
-  self.exeConfigs.find? name
+  self.exes.find? name
 
 /-- The package's `moreServerArgs` configuration. -/
 def moreServerArgs (self : Package) : Array String :=
@@ -418,12 +403,12 @@ def getModuleArray (self : Package) : IO (Array Name) :=
 
 /-- Whether the given module is considered local to the package. -/
 def isLocalModule (mod : Name) (self : Package) : Bool :=
-  self.libConfigs.any (fun _ lib => lib.isLocalModule mod) ||
+  self.libs.any (fun _ lib => lib.isLocalModule mod) ||
   self.builtinLibConfig.isLocalModule mod
 
 /-- Whether the given module is in the package (i.e., can build it). -/
 def hasModule (mod : Name) (self : Package) : Bool :=
-  self.libConfigs.any (fun _ lib => lib.hasModule mod) ||
-  self.exeConfigs.any (fun _ exe => exe.root == mod) ||
+  self.libs.any (fun _ lib => lib.hasModule mod) ||
+  self.exes.any (fun _ exe => exe.root == mod) ||
   self.builtinLibConfig.hasModule mod ||
   self.config.binRoot == mod
diff --git a/Lake/Config/Targets.lean b/Lake/Config/Targets.lean
index b38ce3b..d1dd56b 100644
--- a/Lake/Config/Targets.lean
+++ b/Lake/Config/Targets.lean
@@ -16,12 +16,15 @@ open Lean System
 
 /-- A Lean library's declarative configuration. -/
 structure LeanLibConfig where
+  /-- The name of the target. -/
+  name : Name
+
   /--
   The name of the library.
-  Used as a base for the file names of the library's
-  static and dynamic binaries.
+  Used as a base for the file names of its static and dynamic binaries.
+  Defaults to the upper camel case name of the target.
   -/
-  name : String
+  libName := toUpperCamelCase name |>.toString (escape := false)
 
   /--
   The root module(s) of the library.
@@ -72,11 +75,11 @@ def getModuleArray (self : LeanLibConfig) (srcDir : FilePath) : IO (Array Name)
 
 /-- The file name of package's static library (i.e., `lib{libName}.a`) -/
 def staticLibFileName (self : LeanLibConfig) : FilePath :=
-  s!"lib{self.name}.a"
+  s!"lib{self.libName}.a"
 
 /-- The file name of package's shared library. -/
 def sharedLibFileName (self : LeanLibConfig) : FilePath :=
-  s!"{self.name}.{sharedLibExt}"
+  s!"{self.libName}.{sharedLibExt}"
 
 /--
 The arguments to pass to `leanc` when linking the shared library.
@@ -93,6 +96,9 @@ end LeanLibConfig
 
 /-- A Lean executable's declarative configuration. -/
 structure LeanExeConfig where
+  /-- The name of the target. -/
+  name : Name
+
   /--
   The root module of the binary executable.
   Should include a `main` definition that will serve
@@ -100,14 +106,16 @@ structure LeanExeConfig where
 
   The root is built by recursively building its
   local imports (i.e., fellow modules of the workspace).
+
+  Defaults to the upper camel case name of the target.
   -/
-  root : Name
+  root : Name := toUpperCamelCase name
 
   /--
-  The file name of the binary executable.
-  Defaults to the executable's root with any `.` replaced with a `-`.
+  The name of the binary executable.
+  Defaults to the target name with any `.` replaced with a `-`.
   -/
-  name : String := root.toStringWithSep "-" (escape := false)
+  exeName : String := name.toStringWithSep "-" (escape := false)
 
   /--
   Whether to expose symbols within the executable to the Lean interpreter.
@@ -134,10 +142,10 @@ namespace LeanExeConfig
 
 /--
 The file name of binary executable
-(i.e., `name` plus the platform's `exeExtension`).
+(i.e., `exeName` plus the platform's `exeExtension`).
 -/
 def fileName (self : LeanExeConfig) : FilePath :=
-  FilePath.withExtension self.name FilePath.exeExtension
+  FilePath.withExtension self.exeName FilePath.exeExtension
 
 /--
 The arguments to pass to `leanc` when linking the binary executable.
diff --git a/Lake/DSL.lean b/Lake/DSL.lean
index abf6cce..a73652f 100644
--- a/Lake/DSL.lean
+++ b/Lake/DSL.lean
@@ -6,7 +6,8 @@ Authors: Mac Malone
 import Lake.DSL.DeclUtil
 import Lake.DSL.Attributes
 import Lake.DSL.Extensions
+import Lake.DSL.Config
 import Lake.DSL.Package
 import Lake.DSL.Script
 import Lake.DSL.Require
-import Lake.DSL.Config
+import Lake.DSL.Targets
diff --git a/Lake/DSL/Attributes.lean b/Lake/DSL/Attributes.lean
index d9fac00..fcc3a17 100644
--- a/Lake/DSL/Attributes.lean
+++ b/Lake/DSL/Attributes.lean
@@ -13,3 +13,9 @@ initialize packageAttr : TagAttribute ←
 
 initialize scriptAttr : TagAttribute ←
   registerTagAttribute `script "Lake script attribute"
+
+initialize leanLibAttr : TagAttribute ←
+  registerTagAttribute `leanLib "Lake Lean library target attribute"
+
+initialize leanExeAttr : TagAttribute ←
+  registerTagAttribute `leanExe "Lake Lean executable target attribute"
diff --git a/Lake/DSL/DeclUtil.lean b/Lake/DSL/DeclUtil.lean
index 169054d..4f6655e 100644
--- a/Lake/DSL/DeclUtil.lean
+++ b/Lake/DSL/DeclUtil.lean
@@ -16,3 +16,17 @@ syntax declValDo :=
 
 syntax declValStruct :=
   ppSpace structVal (Term.whereDecls)?
+
+syntax declValTyped :=
+  Term.typeSpec declValSimple
+
+syntax declValOptTyped :=
+  (Term.typeSpec)? declValSimple
+
+def expandAttrs (attrs? : Option Syntax) : Array Syntax :=
+  if let some attrs := attrs? then
+    match attrs with
+    | `(Term.attributes| @[$attrs,*]) => attrs
+    | _ => #[]
+  else
+    #[]
diff --git a/Lake/DSL/Package.lean b/Lake/DSL/Package.lean
index 47257e2..30d384e 100644
--- a/Lake/DSL/Package.lean
+++ b/Lake/DSL/Package.lean
@@ -15,11 +15,8 @@ syntax packageDeclWithBinders :=
   (ppSpace "(" Term.simpleBinder ")")? -- args
   (declValSimple <|> declValStruct <|> declValDo)
 
-syntax packageDeclTyped :=
-  Term.typeSpec declValSimple
-
 syntax packageDeclSpec :=
-  ident (Command.whereStructInst <|> packageDeclTyped <|> packageDeclWithBinders)?
+  ident (Command.whereStructInst <|> declValTyped <|> packageDeclWithBinders)?
 
 scoped syntax (name := packageDecl)
 (docComment)? "package " packageDeclSpec : command
diff --git a/Lake/DSL/Targets.lean b/Lake/DSL/Targets.lean
new file mode 100644
index 0000000..b3b624d
--- /dev/null
+++ b/Lake/DSL/Targets.lean
@@ -0,0 +1,52 @@
+/-
+Copyright (c) 2022 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+import Lake.DSL.DeclUtil
+import Lake.DSL.Attributes
+import Lake.Config.Targets
+
+namespace Lake.DSL
+open Lean Parser Command
+
+syntax targetDeclSpec :=
+  ident (Command.whereStructInst <|> declValOptTyped <|> declValStruct)?
+
+def mkTargetDecl
+(doc? : Option Syntax) (attrs : Array Syntax) (ty : Syntax)
+: (spec : Syntax) → MacroM Syntax
+| `(targetDeclSpec| $id:ident) =>
+  `($[$doc?:docComment]? @[$attrs,*] def $id : $ty :=
+    {name := $(quote id.getId)})
+| `(targetDeclSpec| $id:ident where $[$ds]*) =>
+  `($[$doc?:docComment]? @[$attrs,*] def $id : $ty where
+      name := $(quote id.getId) $[$ds]*)
+| `(targetDeclSpec| $id:ident $[: $ty?]? := $defn $[$wds?]?) =>
+  `($[$doc?:docComment]? @[$attrs,*] def $id : $(ty?.getD ty) := $defn $[$wds?]?)
+| `(targetDeclSpec| $id:ident { $[$fs $[,]?]* } $[$wds?]?) => do
+  let defn ← `({ name := $(quote id.getId), $[$fs]* })
+  `($[$doc?:docComment]? @[$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`.
+-/
+scoped macro (name := leanLibDecl)
+doc?:optional(docComment) attrs?:optional(Term.attributes)
+"lean_lib " spec:targetDeclSpec : command => do
+  let ty := mkCIdentFrom (← getRef) ``LeanLibConfig
+  let attrs := expandAttrs attrs? |>.push <| ← `(Term.attrInstance| leanLib)
+  mkTargetDecl doc? attrs ty spec
+
+/--
+Define a new Lean binary executable target for the package.
+Can optionally be provided with a configuration of type `LeanExeConfig`.
+-/
+scoped macro (name := leanExeDecl)
+doc?:optional(docComment) attrs?:optional(Term.attributes)
+"lean_exe " spec:targetDeclSpec : command => do
+  let ty := mkCIdentFrom (← getRef) ``LeanExeConfig
+  let attrs := expandAttrs attrs? |>.push <| ← `(Term.attrInstance| leanExe)
+  mkTargetDecl doc? attrs ty spec
diff --git a/examples/targets/lakefile.lean b/examples/targets/lakefile.lean
index 5b81c78..446fb27 100644
--- a/examples/targets/lakefile.lean
+++ b/examples/targets/lakefile.lean
@@ -3,29 +3,12 @@ open Lake DSL
 
 package targets {
   srcDir := "src"
-  libConfigs :=
-    Std.RBMap.empty
-    |>.insert `foo {
-      name := "foo"
-    }
-    |>.insert `bar {
-      name := "bar"
-    }
-    |>.insert `baz {
-      name := "baz"
-    }
-  exeConfigs :=
-    Std.RBMap.empty
-    |>.insert `a {
-      root := `a
-      name := "a"
-    }
-    |>.insert `b {
-      root := `b
-      name := "b"
-    }
-    |>.insert `c {
-      root := `c
-      name := "c"
-    }
 }
+
+lean_lib foo
+lean_lib bar
+lean_lib baz
+
+lean_exe a
+lean_exe b
+lean_exe c