aya: port bnf

aya-prover · Jul 2, 2024 · 59599b4 · 59599b4
1 parent 00121e8
commit 59599b4
Show file tree

Hide file tree

Showing 2 changed files with 17 additions and 16 deletions.
diff --git a/src/main/grammar/AyaPsiParser.bnf b/src/main/grammar/AyaPsiParser.bnf
@@ -153,10 +153,9 @@ private stmt_with_recover ::= !(<<eof>>) stmt {
   recoverWhile = stmt_recover
 }
 private stmt_recover ::= !(stmt_first)
-private stmt_first ::= KW_PUBLIC | KW_PRIVATE | KW_OPEN | KW_IMPORT | KW_MODULE
-                     | KW_EXAMPLE | DOC_COMMENT
+private stmt_first ::= KW_IMPORT | KW_MODULE | DOC_COMMENT | KW_PUBLIC
                      | KW_DEF | KW_CLASS | KW_PRIM | KW_DATA | KW_VARIABLE
-                     | KW_OPAQUE | KW_INLINE | KW_OVERLAP
+                     | declModifier
 
 private repl ::= REPL_COMMAND? expr
 
@@ -195,7 +194,7 @@ bindBlock ::= (tighters | loosers)+
 tighters ::= KW_TIGHTER qualifiedId+
 loosers ::= KW_LOOSER qualifiedId+
 
-fnDecl ::= declModifiers*
+fnDecl ::= declModifier*
  KW_DEF declNameOrInfix
  tele* type? fnBody bindBlock? { pin=2 }
 private simpleBody ::= IMPLIES expr { pin=1 }
@@ -211,27 +210,29 @@ primName ::= weakId
 primDecl ::= KW_PRIM primName tele* type? { pin=1 }
 
 // IMPORTANT NOTE: Adding all of these to stmt_first or you will get parser errors!
-declModifiers ::= KW_PRIVATE
-                | KW_EXAMPLE
-                | KW_OPAQUE
-                | KW_INLINE
-                | KW_OVERLAP
-                | KW_OPEN
+declModifier ::= KW_PRIVATE
+               | KW_EXAMPLE
+               | KW_OPAQUE
+               | KW_INLINE
+               | KW_OVERLAP
+               | KW_PARTIAL
+               | KW_OPEN
 
 classDecl
-  ::= declModifiers*
+  ::= declModifier*
       KW_CLASS declNameOrInfix (KW_EXTENDS <<commaSep weakId>>)?
       bindBlock?
       (BAR classMember)*
 
+memberModifier ::= KW_CLASSIFIYING | KW_OVERRIDE | KW_COERCE
 classMember
-  ::= KW_CLASSIFIYING? KW_OVERRIDE?            declNameOrInfix tele* type? IMPLIES expr bindBlock?
-    | KW_CLASSIFIYING? KW_OVERRIDE? KW_COERCE? declNameOrInfix tele* type               bindBlock? {
+  ::= memberModifier* declNameOrInfix tele* type? IMPLIES expr bindBlock?
+    | memberModifier* declNameOrInfix tele* type               bindBlock? {
   mixin="org.aya.intellij.psi.impl.AyaPsiGenericDeclImpl"
   implements="org.aya.intellij.psi.AyaPsiGenericDecl"
 }
 
-dataDecl ::= declModifiers*
+dataDecl ::= declModifier*
  KW_DATA declNameOrInfix?
  tele* type? bindBlock? dataBody* { pin=2 }
 

diff --git a/src/main/java/org/aya/intellij/inspection/warning/BadModifierInspection.kt b/src/main/java/org/aya/intellij/inspection/warning/BadModifierInspection.kt
@@ -4,7 +4,7 @@ import com.intellij.codeInspection.*
 import com.intellij.openapi.project.Project
 import org.aya.intellij.AyaBundle
 import org.aya.intellij.actions.lsp.AyaLsp
-import org.aya.intellij.psi.concrete.AyaPsiDeclModifiers
+import org.aya.intellij.psi.concrete.AyaPsiDeclModifier
 import org.aya.intellij.psi.concrete.AyaPsiVisitor
 import org.aya.producer.error.BadModifierWarn
 
@@ -19,7 +19,7 @@ class BadModifierInspection : WarningInspection() {
 
   override fun buildVisitor(lsp: AyaLsp, holder: ProblemsHolder, isOnTheFly: Boolean) = object : AyaPsiVisitor() {
     // TODO: also ModifierProblem::class.java
-    override fun visitDeclModifiers(mod: AyaPsiDeclModifiers) = lsp.warningsAt(mod, BadModifierWarn::class.java).forEach { _ ->
+    override fun visitDeclModifier(mod: AyaPsiDeclModifier) = lsp.warningsAt(mod, BadModifierWarn::class.java).forEach { _ ->
       holder.registerProblem(
         holder.manager.createProblemDescriptor(
           mod, mod,