feat: add simple DSL for package configurations

Lake.lean

@@ -1,5 +1,5 @@
 /-
-Copyright (c) 2021 Microsoft Corporation. All rights reserved.
+Copyright (c) 2021 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
@@ -14,6 +14,7 @@ import Lake.BuildTop
 import Lake.Cli
 import Lake.CliT
 import Lake.Compile
+import Lake.DSL
 import Lake.Git
 import Lake.Glob
 import Lake.Help

Lake/DSL.lean

@@ -0,0 +1,54 @@
+import Lean.Parser
+import Lake.Package
+
+open Lean Parser
+namespace Lake.DSL
+
+syntax packageStruct :=
+  "{" manyIndent(group(Term.structInstField optional(", "))) "}"
+
+syntax packageDeclValSpecial :=
+  (packageStruct <|> (ppSpace Term.do)) (Term.whereDecls)?
+
+syntax packageDeclWithBinders :=
+  (ppSpace "(" Term.simpleBinder ")")? -- dir
+  (ppSpace "(" Term.simpleBinder ")")? -- args
+  ppSpace (Command.declValSimple <|> packageDeclValSpecial)
+
+syntax packageDeclTyped :=
+  Term.typeSpec Command.declValSimple
+
+scoped syntax (name := packageDecl) declModifiers
+"package" (Term.whereDecls <|> packageDeclTyped <|> packageDeclWithBinders) : command
+
+def expandPackageBinders
+: (dir? : Option Syntax) → (args? : Option Syntax) → MacroM (Bool × Syntax × Syntax)
+| none,     none      => do let hole ← `(_); (false, hole, hole)
+| some dir, none      => do (true, dir, ← `(_))
+| none,     some args => do (true, ← `(_), args)
+| some dir, some args => do (true, dir, args)
+
+def mkPackageDef (defn : Syntax) (mods : Syntax)
+(dir? : Option Syntax) (args? : Option Syntax) (wds? : Option Syntax) : MacroM Syntax := do
+  let (hasBinders, dir, args) ← expandPackageBinders dir? args?
+  if hasBinders then
+    `($mods:declModifiers def $(mkIdent `package) : Packager :=
+        (fun $dir $args => $defn) $[$wds?]?)
+  else
+    `($mods:declModifiers def $(mkIdent `package) : PackageConfig := $defn $[$wds?]?)
+
+@[macro packageDecl]
+def expandPackageDecl : Macro
+| `($mods:declModifiers package where $[$ds]*) =>
+  `($mods:declModifiers def $(mkIdent `package) : PackageConfig where $[$ds]*)
+| `($mods:declModifiers package : $ty := $defn $[$wds?]?) =>
+  `($mods:declModifiers def $(mkIdent `package) : $ty := $defn $[$wds?]?)
+| `($mods:declModifiers package $[($dir?)]? $[($args?)]? := $defn $[$wds?]?) =>
+  mkPackageDef defn mods dir? args? wds?
+| `($mods:declModifiers package $[($dir?)]? $[($args?)]? { $[$fs $[,]?]* } $[$wds?]?) => do
+  mkPackageDef (← `({ $[$fs]* })) mods dir? args? wds?
+| `($mods:declModifiers package $[($dir?)]? $[($args?)]? do $seq $[$wds?]?) => do
+  let (_, dir, args) ← expandPackageBinders dir? args?
+  `($mods:declModifiers def $(mkIdent `package) : IOPackager :=
+      (fun $dir $args => do $seq) $[$wds?]?)
+| stx => Macro.throwErrorAt stx "ill-formed package declaration"

Lake/Main.lean

@@ -3,8 +3,7 @@ Copyright (c) 2017 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Gabriel Ebner, Sebastian Ullrich, Mac Malone
 -/
-import Lake.Cli
-import Lake.SearchPath
+import Lake
 
 def main (args : List String) : IO UInt32 := do
   try