Skip to content

Commit ea232b3

Browse files
joehendrixjoehendrix
committed
Position information
1 parent a46786c commit ea232b3

35 files changed

+3540
-2528
lines changed

‎Strata/DDM/AST.lean‎

Lines changed: 345 additions & 281 deletions
Large diffs are not rendered by default.

‎Strata/DDM/BuiltinDialects/Init.lean‎

Lines changed: 50 additions & 49 deletions
Original file line numberDiff line numberDiff line change
@@ -11,44 +11,45 @@ namespace Strata
1111
open Elab
1212
open Parser (minPrec)
1313

14+
def SyntaxCat.mkOpt (c:SyntaxCat) : SyntaxCat := { ann := .none, name := q`Init.Option, args := #[c] }
15+
def SyntaxCat.mkSeq (c:SyntaxCat) : SyntaxCat := { ann := .none, name := q`Init.Seq, args := #[c] }
16+
def SyntaxCat.mkCommaSepBy (c:SyntaxCat) : SyntaxCat := { ann := .none, name := q`Init.CommaSepBy, args := #[c] }
17+
1418
def initDialect : Dialect := BuiltinM.create! "Init" #[] do
15-
let Ident : ArgDeclKind := .cat <| .atom q`Init.Ident
16-
let Num : SyntaxCat := .atom q`Init.Num
17-
let Str : SyntaxCat := .atom q`Init.Str
19+
let Ident : ArgDeclKind := .cat <| .atom .none q`Init.Ident
20+
let Num : SyntaxCat := .atom .none q`Init.Num
21+
let Str : SyntaxCat := .atom .none q`Init.Str
1822

1923
declareAtomicCat q`Init.Ident
2024
declareAtomicCat q`Init.Num
2125
declareAtomicCat q`Init.Decimal
2226
declareAtomicCat q`Init.Str
2327

2428
declareCat q`Init.Option #["a"]
25-
let mkOpt (c:SyntaxCat) : SyntaxCat := .app (.atom q`Init.Option) c
2629

2730
declareCat q`Init.Seq #["a"]
28-
let mkSeq (c:SyntaxCat) : SyntaxCat := .app (.atom q`Init.Seq) c
2931

3032
declareCat q`Init.CommaSepBy #["a"]
31-
let mkCommaSepBy (c:SyntaxCat) : SyntaxCat := .app (.atom q`Init.CommaSepBy) c
3233

3334
let QualifiedIdent := q`Init.QualifiedIdent
3435
declareCat QualifiedIdent
3536
declareOp {
3637
name := "qualifiedIdentType",
37-
argDecls := #[],
38+
argDecls := .empty,
3839
category := QualifiedIdent,
3940
syntaxDef := .ofList [.str "Type"],
4041
}
4142
declareOp {
4243
name := "qualifiedIdentImplicit",
43-
argDecls := #[
44+
argDecls := .ofArray #[
4445
{ ident := "name", kind := Ident }
4546
],
4647
category := QualifiedIdent,
4748
syntaxDef := .ofList [.ident 0 0],
4849
}
4950
declareOp {
5051
name := "qualifiedIdentExplicit",
51-
argDecls := #[
52+
argDecls := .ofArray #[
5253
{ ident := "dialect", kind := Ident },
5354
{ ident := "name", kind := Ident }
5455
],
@@ -57,27 +58,27 @@ def initDialect : Dialect := BuiltinM.create! "Init" #[] do
5758
}
5859

5960
let TypeExprId := q`Init.TypeExpr
60-
let TypeExpr : ArgDeclKind := .cat (.atom TypeExprId)
61+
let TypeExpr : ArgDeclKind := .cat (.atom .none TypeExprId)
6162
declareCat TypeExprId
6263
declareOp {
6364
name := "TypeIdent",
64-
argDecls := #[
65-
{ ident := "value", kind := .cat <| .atom QualifiedIdent }
65+
argDecls := .ofArray #[
66+
{ ident := "value", kind := .cat <| .atom .none QualifiedIdent }
6667
]
6768
category := TypeExprId,
6869
syntaxDef := .ofList [.ident 0 maxPrec]
6970
}
7071
declareOp {
7172
name := "TypeParen",
72-
argDecls := #[
73+
argDecls := .ofArray #[
7374
{ ident := "value", kind := TypeExpr }
7475
]
7576
category := TypeExprId,
7677
syntaxDef := .ofList [.str "(", .ident 0 0, .str ")"]
7778
}
7879
declareOp {
7980
name := "TypeArrow",
80-
argDecls := #[
81+
argDecls := .ofArray #[
8182
{ ident := "lhs", kind := TypeExpr },
8283
{ ident := "rhs", kind := TypeExpr }
8384
]
@@ -86,7 +87,7 @@ def initDialect : Dialect := BuiltinM.create! "Init" #[] do
8687
}
8788
declareOp {
8889
name := "TypeApp",
89-
argDecls := #[
90+
argDecls := .ofArray #[
9091
{ ident := "fn", kind := TypeExpr },
9192
{ ident := "val", kind := TypeExpr }
9293
]
@@ -98,7 +99,7 @@ def initDialect : Dialect := BuiltinM.create! "Init" #[] do
9899
declareCat «Type»
99100
declareOp {
100101
name := "mkType",
101-
argDecls := #[
102+
argDecls := .ofArray #[
102103
{ ident := "type", kind := TypeExpr }
103104
],
104105
category := «Type»,
@@ -109,25 +110,25 @@ def initDialect : Dialect := BuiltinM.create! "Init" #[] do
109110
declareCat Expr
110111
declareOp {
111112
name := "exprIdent",
112-
argDecls := #[
113+
argDecls := .ofArray #[
113114
{ ident := "value", kind := Ident }
114115
],
115116
category := Expr,
116117
syntaxDef := .ofList [.ident 0 0],
117118
}
118119
declareOp {
119120
name := "exprParen",
120-
argDecls := #[
121-
{ ident := "value", kind := .cat (.atom Expr) }
121+
argDecls := .ofArray #[
122+
{ ident := "value", kind := .cat (.atom .none Expr) }
122123
],
123124
category := Expr,
124125
syntaxDef := .ofList [.str "(", .ident 0 0, .str ")"]
125126
}
126127
declareOp {
127128
name := "exprApp",
128-
argDecls := #[
129+
argDecls := .ofArray #[
129130
{ ident := "function", kind := Ident },
130-
{ ident := "args", kind := .cat <| mkCommaSepBy (.atom Expr) }
131+
{ ident := "args", kind := .cat <| .mkCommaSepBy (.atom .none Expr) }
131132
],
132133
category := Expr,
133134
syntaxDef := .ofList [.ident 0 0, .str "(", .ident 1 0, .str ")"]
@@ -137,61 +138,61 @@ def initDialect : Dialect := BuiltinM.create! "Init" #[] do
137138
declareCat MetadataArg
138139
declareOp {
139140
name := "MetadataArgParen",
140-
argDecls := #[
141-
{ ident := "value", kind := .cat (.atom MetadataArg) }
141+
argDecls := .ofArray #[
142+
{ ident := "value", kind := .cat (.atom .none MetadataArg) }
142143
],
143144
category := MetadataArg,
144145
syntaxDef := .ofList [.str "(", .ident 0 0, .str ")"]
145146
}
146147
declareOp {
147148
name := "MetadataArgNum",
148-
argDecls := #[
149+
argDecls := .ofArray #[
149150
{ ident := "value", kind := .cat Num }
150151
],
151152
category := MetadataArg,
152153
syntaxDef := .ofList [.ident 0 0]
153154
}
154155
declareOp {
155156
name := "MetadataArgIdent",
156-
argDecls := #[
157+
argDecls := .ofArray #[
157158
{ ident := "value", kind := Ident }
158159
],
159160
category := MetadataArg,
160161
syntaxDef := .ofList [.ident 0 0]
161162
}
162163
declareOp {
163164
name := "MetadataArgTrue",
164-
argDecls := #[],
165+
argDecls := .empty,
165166
category := MetadataArg,
166167
syntaxDef := .ofList [.str "true"]
167168
}
168169
declareOp {
169170
name := "MetadataArgFalse",
170-
argDecls := #[],
171+
argDecls := .empty,
171172
category := MetadataArg,
172173
syntaxDef := .ofList [.str "false"]
173174
}
174175
declareOp {
175176
name := "MetadataArgSome",
176-
argDecls := #[
177-
{ ident := "value", kind := .cat (.atom MetadataArg) }
177+
argDecls := .ofArray #[
178+
{ ident := "value", kind := .cat (.atom .none MetadataArg) }
178179
],
179180
category := MetadataArg,
180181
syntaxDef := .ofList [.str "some", .ident 0 appPrec]
181182
}
182183
declareOp {
183-
name := "MetadataArgNone",
184-
argDecls := #[],
185-
category := MetadataArg,
184+
name := "MetadataArgNone"
185+
argDecls := .empty
186+
category := MetadataArg
186187
syntaxDef := .ofList [.str "none"]
187188
}
188189

189190
let MetadataArgs := q`Init.MetadataArgs
190191
declareCat MetadataArgs
191192
declareOp {
192193
name := "MetadataArgsMk",
193-
argDecls := #[
194-
{ ident := "args", kind := .cat <| mkCommaSepBy <| .atom MetadataArg }
194+
argDecls := .ofArray #[
195+
{ ident := "args", kind := .cat <| .mkCommaSepBy <| .atom .none MetadataArg }
195196
],
196197
category := MetadataArgs,
197198
syntaxDef := .ofList [.str "(", .ident 0 0, .str ")"]
@@ -201,9 +202,9 @@ def initDialect : Dialect := BuiltinM.create! "Init" #[] do
201202
declareCat MetadataAttr
202203
declareOp {
203204
name := "MetadataAttrMk",
204-
argDecls := #[
205-
{ ident := "name", kind := .cat <| .atom QualifiedIdent },
206-
{ ident := "args", kind := .cat <| mkOpt <| .atom MetadataArgs }
205+
argDecls := .ofArray #[
206+
{ ident := "name", kind := .cat <| .atom .none QualifiedIdent },
207+
{ ident := "args", kind := .cat <| .mkOpt <| .atom .none MetadataArgs }
207208
],
208209
category := MetadataAttr,
209210
syntaxDef := .ofList [.ident 0 0, .ident 1 0]
@@ -213,8 +214,8 @@ def initDialect : Dialect := BuiltinM.create! "Init" #[] do
213214
declareCat Metadata
214215
declareOp {
215216
name := "MetadataMk",
216-
argDecls := #[
217-
{ ident := "attrs", kind := .cat <| mkCommaSepBy <| .atom MetadataAttr }
217+
argDecls := .ofArray #[
218+
{ ident := "attrs", kind := .cat <| .mkCommaSepBy <| .atom .none MetadataAttr }
218219
],
219220
category := Metadata,
220221
syntaxDef := .ofList [.str "@[", .ident 0 0, .str "]"]
@@ -227,7 +228,7 @@ def initDialect : Dialect := BuiltinM.create! "Init" #[] do
227228
declareCat BindingType
228229
declareOp {
229230
name := "mkBindingType",
230-
argDecls := #[
231+
argDecls := .ofArray #[
231232
{ ident := "type", kind := TypeExpr }
232233
],
233234
category := BindingType,
@@ -239,7 +240,7 @@ def initDialect : Dialect := BuiltinM.create! "Init" #[] do
239240
declareCat TypeP
240241
declareOp {
241242
name := "mkTypeP",
242-
argDecls := #[
243+
argDecls := .ofArray #[
243244
{ ident := "type", kind := TypeExpr }
244245
],
245246
category := TypeP,
@@ -250,7 +251,7 @@ def initDialect : Dialect := BuiltinM.create! "Init" #[] do
250251
declareCat SyntaxAtomPrec
251252
declareOp {
252253
name := "syntaxAtomPrec",
253-
argDecls := #[
254+
argDecls := .ofArray #[
254255
{ ident := "value", kind := .cat Num }
255256
],
256257
category := SyntaxAtomPrec,
@@ -261,27 +262,27 @@ def initDialect : Dialect := BuiltinM.create! "Init" #[] do
261262
declareCat SyntaxAtom
262263
declareOp {
263264
name := "syntaxAtomIdent",
264-
argDecls := #[
265+
argDecls := .ofArray #[
265266
{ ident := "ident", kind := Ident },
266-
{ ident := "prec", kind := .cat <| mkOpt <| .atom SyntaxAtomPrec }
267+
{ ident := "prec", kind := .cat <| .mkOpt <| .atom .none SyntaxAtomPrec }
267268
],
268269
category := SyntaxAtom,
269270
syntaxDef := .ofList [.ident 0 0, .ident 1 0],
270271
metadata := .empty,
271272
}
272273
declareOp {
273274
name := "syntaxAtomString",
274-
argDecls := #[
275+
argDecls := .ofArray #[
275276
{ ident := "value", kind := .cat Str }
276277
],
277278
category := SyntaxAtom,
278279
syntaxDef := .ofList [.ident 0 0],
279280
}
280281
declareOp {
281282
name := "syntaxAtomIndent",
282-
argDecls := #[
283+
argDecls := .ofArray #[
283284
{ ident := "indent", kind := .cat Num },
284-
{ ident := "args", kind := .cat <| mkSeq <| .atom SyntaxAtom }
285+
{ ident := "args", kind := .cat <| .mkSeq <| .atom .none SyntaxAtom }
285286
],
286287
category := SyntaxAtom,
287288
syntaxDef := .ofList [.str "indent", .str "(", .ident 0 0, .str ", ", .ident 1 0, .str ")"],
@@ -291,8 +292,8 @@ def initDialect : Dialect := BuiltinM.create! "Init" #[] do
291292
declareCat SyntaxDef
292293
declareOp {
293294
name := "mkSyntaxDef",
294-
argDecls := #[
295-
{ ident := "args", kind := .cat <| mkSeq (.atom SyntaxAtom) }
295+
argDecls := .ofArray #[
296+
{ ident := "args", kind := .cat <| .mkSeq (.atom .none SyntaxAtom) }
296297
],
297298
category := SyntaxDef,
298299
syntaxDef := .ofList [.ident 0 0],

0 commit comments

Comments
 (0)