-
Notifications
You must be signed in to change notification settings - Fork 345
/
DeclUtil.lean
103 lines (83 loc) · 3.33 KB
/
DeclUtil.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
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
/-
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.DSL.Config
import Lake.Util.Binder
import Lean.Parser.Command
namespace Lake.DSL
open Lean Parser Command
abbrev DocComment := TSyntax ``docComment
abbrev Attributes := TSyntax ``Term.attributes
abbrev AttrInstance := TSyntax ``Term.attrInstance
abbrev WhereDecls := TSyntax ``Term.whereDecls
---
def expandAttrs (attrs? : Option Attributes) : Array AttrInstance :=
if let some attrs := attrs? then
match attrs with
| `(Term.attributes| @[$attrs,*]) => attrs
| _ => #[]
else
#[]
/-- A single field assignment in a declarative configuration. -/
syntax declField :=
ident " := " term
@[inherit_doc declField] abbrev DeclField := TSyntax ``declField
syntax structVal :=
"{" manyIndent(group(declField ", "?)) "}"
syntax declValDo :=
ppSpace Term.do (Term.whereDecls)?
syntax declValStruct :=
ppSpace structVal (Term.whereDecls)?
syntax declValWhere :=
" where " sepByIndentSemicolon(declField) (Term.whereDecls)?
syntax declValTyped :=
Term.typeSpec declValSimple
syntax declValOptTyped :=
(Term.typeSpec)? declValSimple
syntax simpleDeclSig :=
ident Term.typeSpec declValSimple
syntax structDeclSig :=
ident (declValWhere <|> declValOptTyped <|> declValStruct)?
syntax bracketedSimpleBinder :=
"(" ident (" : " term)? ")"
syntax simpleBinder :=
ident <|> bracketedSimpleBinder
abbrev SimpleBinder := TSyntax ``simpleBinder
open Lean.Parser.Term in
def expandOptSimpleBinder (stx? : Option SimpleBinder) : MacroM FunBinder := do
match stx? with
| some stx =>
match stx with
| `(simpleBinder| $id:ident) =>
`(funBinder| $id)
| `(simpleBinder| ($id $[: $ty?]?)) =>
let ty := ty?.getD (← `(_))
`(funBinder| ($id : $ty))
| _ => `(funBinder| _)
| none => `(funBinder| _)
def fixName (id : Ident) : Option Name → Ident
| some n => mkIdentFrom id n
| none => id
def expandDeclField : TSyntax ``declField → MacroM (TSyntax ``Term.structInstField)
| `(declField| $id :=%$tk $val) => `(Term.structInstField| $id:ident :=%$tk $val)
| x => Macro.throwErrorAt x "ill-formed field declaration"
def mkConfigDecl (name? : Option Name)
(doc? : Option DocComment) (attrs : Array AttrInstance) (ty : Term)
: (spec : Syntax) → MacroM Syntax.Command
| `(structDeclSig| $id:ident) =>
`($[$doc?]? @[$attrs,*] abbrev $(fixName id name?) : $ty :=
{name := $(quote id.getId)})
| `(structDeclSig| $id:ident where $fs;* $[$wds?:whereDecls]?) => do
let fields ← fs.getElems.mapM expandDeclField
let defn ← `({ name := $(quote id.getId), $fields,* })
`($[$doc?]? @[$attrs,*] abbrev $(fixName id name?) : $ty := $defn $[$wds?:whereDecls]?)
| `(structDeclSig| $id:ident $[: $ty?]? :=%$defTk $defn $[$wds?]?) => do
let notice ← withRef defTk `(#eval IO.eprintln s!" warning: {__dir__}: `:=` syntax for configurations has been deprecated")
`($notice $[$doc?]? @[$attrs,*] abbrev $(fixName id name?) : $ty := $defn $[$wds?]?)
| `(structDeclSig| $id:ident { $[$fs $[,]?]* } $[$wds?:whereDecls]?) => do
let fields ← fs.mapM expandDeclField
let defn ← `({ name := $(quote id.getId), $fields,* })
`($[$doc?]? @[$attrs,*] abbrev $(fixName id name?) : $ty := $defn $[$wds?:whereDecls]?)
| stx => Macro.throwErrorAt stx "ill-formed configuration syntax"