-
Notifications
You must be signed in to change notification settings - Fork 350
/
Script.lean
46 lines (39 loc) · 1.36 KB
/
Script.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
/-
Copyright (c) 2021 Mac Malone. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mac Malone
-/
import Lake.Config.Package
import Lake.DSL.Attributes
import Lake.DSL.DeclUtil
/-! # Script Declarations
DSL definitions to define a Lake script for a package.
-/
namespace Lake.DSL
open Lean Parser Command
syntax scriptDeclSpec :=
ident (ppSpace simpleBinder)? (declValSimple <|> declValDo)
/--
Define a new Lake script for the package.
**Example**
```
/-- Display a greeting -/
script «script-name» (args) do
if h : 0 < args.length then
IO.println s!"Hello, {args[0]'h}!"
else
IO.println "Hello, world!"
return 0
```
-/
scoped syntax (name := scriptDecl)
(docComment)? optional(Term.attributes) "script " scriptDeclSpec : command
@[macro scriptDecl]
def expandScriptDecl : Macro
| `($[$doc?]? $[$attrs?]? script $id:ident $[$args?]? do $seq $[$wds?:whereDecls]?) => do
`($[$doc?]? $[$attrs?]? script $id:ident $[$args?]? := do $seq $[$wds?:whereDecls]?)
| `($[$doc?]? $[$attrs?]? script $id:ident $[$args?]? := $defn $[$wds?:whereDecls]?) => do
let args ← expandOptSimpleBinder args?
let attrs := #[← `(Term.attrInstance| «script»)] ++ expandAttrs attrs?
`($[$doc?]? @[$attrs,*] def $id : ScriptFn := fun $args => $defn $[$wds?:whereDecls]?)
| stx => Macro.throwErrorAt stx "ill-formed script declaration"