diff --git a/Lake.lean b/Lake.lean index f6a629bc27..d30c8eb713 100644 --- a/Lake.lean +++ b/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 diff --git a/Lake/DSL.lean b/Lake/DSL.lean new file mode 100644 index 0000000000..2fc11ec266 --- /dev/null +++ b/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" diff --git a/Lake/Main.lean b/Lake/Main.lean index 01b5c45bf3..968893323d 100644 --- a/Lake/Main.lean +++ b/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