Skip to content

Commit b8de0d2

Browse files
augustepoirouxaugustepoiroux
committed
Update protected extraction status to match v4.23.0 change
1 parent 02c5db3 commit b8de0d2

File tree

3 files changed

+45
-26
lines changed

3 files changed

+45
-26
lines changed

‎REPL/Extract/Declaration.lean‎

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -15,9 +15,10 @@ def getModifiers (stx : Syntax) (ctx: ContextInfo): DeclModifiers :=
1515
{ docString := stx[0].getOptional?.map (fun stx =>
1616
{ content := stx.prettyPrint.pretty, range := stx.toRange ctx }),
1717
visibility := (stx[2].getOptional?.map (·.prettyPrint.pretty.trim)).getD "regular",
18-
computeKind := (stx[3].getOptional?.map (·.prettyPrint.pretty.trim)).getD "regular",
19-
recKind := (stx[5].getOptional?.map (·.prettyPrint.pretty.trim)).getD "default",
20-
isUnsafe := !stx[4].isNone,
18+
computeKind := (stx[4].getOptional?.map (·.prettyPrint.pretty.trim)).getD "regular",
19+
isProtected := !stx[3].isNone,
20+
isUnsafe := !stx[5].isNone,
21+
recKind := (stx[6].getOptional?.map (·.prettyPrint.pretty.trim)).getD "default",
2122
attributes := stx[1].getArgs.toList.flatMap parseAttributes, }
2223
| _ => {}
2324
where

‎REPL/JSON.lean‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -128,9 +128,10 @@ deriving ToJson
128128
/-- See `Lean.Elab.Modifiers` -/
129129
structure DeclModifiers where
130130
docString : Option DocString := none
131-
visibility : String := "regular" -- "regular", "private", "protected", or "public"
131+
visibility : String := "regular" -- "regular", "private", or "public"
132132
computeKind : String := "regular" -- "regular", "meta", or "noncomputable"
133133
recKind : String := "default" -- "default", "partial", or "nonrec"
134+
isProtected : Bool := false
134135
isUnsafe : Bool := false
135136
attributes : List String := []
136137
deriving ToJson

‎test/extract_declaration.expected.out‎

Lines changed: 39 additions & 22 deletions
Original file line numberDiff line numberDiff line change
@@ -38,6 +38,7 @@
3838
{"visibility": "regular",
3939
"recKind": "default",
4040
"isUnsafe": false,
41+
"isProtected": false,
4142
"docString": null,
4243
"computeKind": "regular",
4344
"attributes": []},
@@ -83,6 +84,7 @@
8384
{"visibility": "regular",
8485
"recKind": "default",
8586
"isUnsafe": false,
87+
"isProtected": false,
8688
"docString": null,
8789
"computeKind": "regular",
8890
"attributes": []},
@@ -138,6 +140,7 @@
138140
{"visibility": "regular",
139141
"recKind": "default",
140142
"isUnsafe": false,
143+
"isProtected": false,
141144
"docString":
142145
{"range":
143146
{"synthetic": false,
@@ -193,6 +196,7 @@
193196
{"visibility": "regular",
194197
"recKind": "default",
195198
"isUnsafe": false,
199+
"isProtected": false,
196200
"docString": null,
197201
"computeKind": "regular",
198202
"attributes": []},
@@ -244,6 +248,7 @@
244248
{"visibility": "regular",
245249
"recKind": "default",
246250
"isUnsafe": false,
251+
"isProtected": false,
247252
"docString": null,
248253
"computeKind": "regular",
249254
"attributes": []},
@@ -282,6 +287,7 @@
282287
{"visibility": "regular",
283288
"recKind": "default",
284289
"isUnsafe": false,
290+
"isProtected": false,
285291
"docString": null,
286292
"computeKind": "regular",
287293
"attributes": []},
@@ -296,24 +302,24 @@
296302
"pp":
297303
" := ParserDescr.trailingNode `Demo.«term_≋_» 68 69 ParserDescr.binary `andthen ParserDescr.symbol \" ≋ \" ParserDescr.cat `term 69 ",
298304
"constants":
299-
["ParserDescr.symbol._@._hyg.226",
300-
"ParserDescr.binary._@._hyg.226",
301-
"ParserDescr.cat._@._hyg.226",
302-
"ParserDescr.trailingNode._@._hyg.226"]},
305+
["ParserDescr.cat._@._hyg.202",
306+
"ParserDescr.symbol._@._hyg.202",
307+
"ParserDescr.binary._@._hyg.202",
308+
"ParserDescr.trailingNode._@._hyg.202"]},
303309
"type":
304310
{"range":
305311
{"synthetic": true,
306312
"start": {"line": 35, "column": 0},
307313
"finish": {"line": 35, "column": 32}},
308314
"pp": " Lean.TrailingParserDescr ",
309-
"constants": ["Lean.TrailingParserDescr._@._hyg.226"]},
315+
"constants": ["Lean.TrailingParserDescr._@._hyg.202"]},
310316
"signature":
311317
{"range":
312318
{"synthetic": true,
313319
"start": {"line": 35, "column": 0},
314320
"finish": {"line": 35, "column": 32}},
315321
"pp": " : Lean.TrailingParserDescr ",
316-
"constants": ["Lean.TrailingParserDescr._@._hyg.226"]},
322+
"constants": ["Lean.TrailingParserDescr._@._hyg.202"]},
317323
"scope":
318324
{"varDecls": ["variable {α : Type u}"],
319325
"openDecl": [],
@@ -332,6 +338,7 @@
332338
{"visibility": "regular",
333339
"recKind": "default",
334340
"isUnsafe": false,
341+
"isProtected": false,
335342
"docString": null,
336343
"computeKind": "meta",
337344
"attributes": ["scoped term_parser 1000"]},
@@ -346,25 +353,25 @@
346353
"pp":
347354
" := fun | `( $ lhs ≋ $ rhs ) => ` `( BEq.beq\n\n $ lhs $ rhs ) | _ => no_error_if_unused% throw Lean.Macro.Exception.unsupportedSyntax ",
348355
"constants":
349-
["Lean.Macro.Exception.unsupportedSyntax._@._hyg.255",
350-
"throw._@._hyg.255",
351-
"rhs._@._hyg.223",
356+
["rhs._@._hyg.199",
357+
"throw._@._hyg.221",
358+
"Lean.Macro.Exception.unsupportedSyntax._@._hyg.221",
352359
"BEq.beq",
353-
"lhs._@._hyg.223"]},
360+
"lhs._@._hyg.199"]},
354361
"type":
355362
{"range":
356363
{"synthetic": true,
357364
"start": {"line": 35, "column": 0},
358365
"finish": {"line": 35, "column": 32}},
359366
"pp": " Macro ",
360-
"constants": ["Macro._@._hyg.255"]},
367+
"constants": ["Macro._@._hyg.221"]},
361368
"signature":
362369
{"range":
363370
{"synthetic": true,
364371
"start": {"line": 35, "column": 0},
365372
"finish": {"line": 35, "column": 32}},
366373
"pp": " : Macro ",
367-
"constants": ["Macro._@._hyg.255"]},
374+
"constants": ["Macro._@._hyg.221"]},
368375
"scope":
369376
{"varDecls": ["variable {α : Type u}"],
370377
"openDecl": [],
@@ -383,6 +390,7 @@
383390
{"visibility": "regular",
384391
"recKind": "default",
385392
"isUnsafe": false,
393+
"isProtected": false,
386394
"docString": null,
387395
"computeKind": "meta",
388396
"attributes": ["macro Demo.«term_≋_»"]},
@@ -395,27 +403,28 @@
395403
"start": {"line": 35, "column": 0},
396404
"finish": {"line": 35, "column": 32}},
397405
"pp":
398-
" := fun | `( $ f : ident $ lhs $ rhs ) => withRef f `( $ lhs ≋ $ rhs ) | _ => throw ( ) ",
406+
" := fun | `( $ f : ident $ lhs $ rhs ) => withRef f `( $ lhs ≋ $ rhs ) | _ => throw ( ) ",
399407
"constants":
400-
["throw._@._hyg.225",
401-
"rhs._@._hyg.223",
402-
"lhs._@._hyg.223",
403-
"f._@._hyg.225",
404-
"withRef._@._hyg.225"]},
408+
["rhs._@._hyg.199",
409+
"throw._@._hyg.201",
410+
"_@._hyg.201",
411+
"withRef._@._hyg.201",
412+
"f._@._hyg.201",
413+
"lhs._@._hyg.199"]},
405414
"type":
406415
{"range":
407416
{"synthetic": true,
408417
"start": {"line": 35, "column": 0},
409418
"finish": {"line": 35, "column": 32}},
410419
"pp": " Lean.PrettyPrinter.Unexpander ",
411-
"constants": ["Lean.PrettyPrinter.Unexpander._@._hyg.225"]},
420+
"constants": ["Lean.PrettyPrinter.Unexpander._@._hyg.201"]},
412421
"signature":
413422
{"range":
414423
{"synthetic": true,
415424
"start": {"line": 35, "column": 0},
416425
"finish": {"line": 35, "column": 32}},
417426
"pp": " : Lean.PrettyPrinter.Unexpander ",
418-
"constants": ["Lean.PrettyPrinter.Unexpander._@._hyg.225"]},
427+
"constants": ["Lean.PrettyPrinter.Unexpander._@._hyg.201"]},
419428
"scope":
420429
{"varDecls": ["variable {α : Type u}"],
421430
"openDecl": [],
@@ -428,12 +437,13 @@
428437
"start": {"line": 35, "column": 0},
429438
"finish": {"line": 35, "column": 32}},
430439
"pp":
431-
" @[ scoped app_unexpander BEq.beq ] meta def _aux___unexpand_BEq_beq_1 : Lean.PrettyPrinter.Unexpander := fun | `( $ f : ident $ lhs $ rhs ) => withRef f `( $ lhs ≋ $ rhs ) | _ => throw ( ) ",
440+
" @[ scoped app_unexpander BEq.beq ] meta def _aux___unexpand_BEq_beq_1 : Lean.PrettyPrinter.Unexpander := fun | `( $ f : ident $ lhs $ rhs ) => withRef f `( $ lhs ≋ $ rhs ) | _ => throw ( ) ",
432441
"name": "_aux___unexpand_BEq_beq_1",
433442
"modifiers":
434443
{"visibility": "regular",
435444
"recKind": "default",
436445
"isUnsafe": false,
446+
"isProtected": false,
437447
"docString": null,
438448
"computeKind": "meta",
439449
"attributes": ["scoped app_unexpander BEq.beq"]},
@@ -478,6 +488,7 @@
478488
{"visibility": "regular",
479489
"recKind": "default",
480490
"isUnsafe": false,
491+
"isProtected": false,
481492
"docString": null,
482493
"computeKind": "regular",
483494
"attributes": []},
@@ -524,6 +535,7 @@
524535
{"visibility": "regular",
525536
"recKind": "default",
526537
"isUnsafe": false,
538+
"isProtected": false,
527539
"docString": null,
528540
"computeKind": "regular",
529541
"attributes": []},
@@ -568,6 +580,7 @@
568580
{"visibility": "private",
569581
"recKind": "default",
570582
"isUnsafe": false,
583+
"isProtected": false,
571584
"docString": null,
572585
"computeKind": "regular",
573586
"attributes": []},
@@ -619,6 +632,7 @@
619632
{"visibility": "private",
620633
"recKind": "default",
621634
"isUnsafe": false,
635+
"isProtected": false,
622636
"docString": null,
623637
"computeKind": "noncomputable",
624638
"attributes": []},
@@ -668,9 +682,10 @@
668682
"/--\n dododo-/\nprotected partial def prot_part_def (a : Nat) : Nat := a",
669683
"name": "prot_part_def",
670684
"modifiers":
671-
{"visibility": "protected",
685+
{"visibility": "regular",
672686
"recKind": "partial",
673687
"isUnsafe": false,
688+
"isProtected": true,
674689
"docString":
675690
{"range":
676691
{"synthetic": false,
@@ -727,6 +742,7 @@
727742
{"visibility": "regular",
728743
"recKind": "default",
729744
"isUnsafe": false,
745+
"isProtected": false,
730746
"docString": null,
731747
"computeKind": "regular",
732748
"attributes": ["simp", "instance"]},
@@ -771,6 +787,7 @@
771787
{"visibility": "public",
772788
"recKind": "default",
773789
"isUnsafe": false,
790+
"isProtected": false,
774791
"docString": null,
775792
"computeKind": "regular",
776793
"attributes": []},

0 commit comments

Comments
 (0)