From bd7739d02e7fcac2be2eceac2f7b9c65e7fb6ad2 Mon Sep 17 00:00:00 2001
From: tydeu <tydeu@hatpress.net>
Date: Tue, 19 Jul 2022 12:45:15 -0400
Subject: [PATCH] chore: add sanity check for
 `SemanticTokenType/Modifier.names`

---
 src/Lean/Data/Lsp/LanguageFeatures.lean | 14 +++++++++++++-
 1 file changed, 13 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Data/Lsp/LanguageFeatures.lean b/src/Lean/Data/Lsp/LanguageFeatures.lean
index 5b015fb823..82b7981b73 100644
--- a/src/Lean/Data/Lsp/LanguageFeatures.lean
+++ b/src/Lean/Data/Lsp/LanguageFeatures.lean
@@ -252,6 +252,7 @@ inductive SemanticTokenType where
   | regexp
   | operator
   | decorator
+  deriving ToJson, FromJson
 
 -- must be in the same order as the constructors
 def SemanticTokenType.names : Array String :=
@@ -263,6 +264,11 @@ def SemanticTokenType.names : Array String :=
 def SemanticTokenType.toNat (type : SemanticTokenType) : Nat :=
   type.toCtorIdx
 
+-- sanity check
+theorem SemanticTokenType.names_toNat_eq_toJson {v : SemanticTokenType} :
+names[v.toNat]?.map (toString <| toJson ·) = some (toString <| toJson v) := by
+  cases v <;> (dsimp only [toNat, toCtorIdx, names]; native_decide)
+
 /--
 The semantic token modifiers included by default in the LSP specification.
 Not used by the Lean core, but implementing them here allows them to be
@@ -279,15 +285,21 @@ inductive SemanticTokenModifier where
   | modification
   | documentation
   | defaultLibrary
+  deriving ToJson, FromJson
 
 -- must be in the same order as the constructors
 def SemanticTokenModifier.names : Array String :=
   #["declaration", "definition", "readonly", "static", "deprecated", "abstract",
     "async", "modification", "documentation", "defaultLibrary"]
 
-def SemanticTokenModifier.toNat (modifier : SemanticTokenType) : Nat :=
+def SemanticTokenModifier.toNat (modifier : SemanticTokenModifier) : Nat :=
   modifier.toCtorIdx
 
+-- sanity check
+theorem SemanticTokenModifier.names_toNat_eq_toJson {v : SemanticTokenModifier} :
+names[v.toNat]?.map (toString <| toJson ·) = some (toString <| toJson v) := by
+  cases v <;> (dsimp only [toNat, toCtorIdx, names]; native_decide)
+
 structure SemanticTokensLegend where
   tokenTypes : Array String
   tokenModifiers : Array String