[ agda ] data type with predefined signature

owo-lang · May 16, 2019 · d46240a · d46240a
1 parent a142312
commit d46240a
Show file tree

Hide file tree

Showing 4 changed files with 180 additions and 171 deletions.
diff --git a/grammar/agda.bnf b/grammar/agda.bnf
@@ -79,8 +79,18 @@ whereClause ::= KW_WHERE layout { pin=1 }
 whereSignatureClause ::= KW_WHERE layoutSignature? { pin=1 }
 whereRecordClause ::= KW_WHERE layoutRecord { pin=1 }
 
-data ::= (KW_DATA | KW_CODATA) dataSignature whereSignatureClause { pin=1 }
-record ::= KW_RECORD dataSignature whereRecordClause { pin=1 }
+data ::= dataKeyword dataSignature whereSignatureClause? {
+	extends=declaration
+}
+dataBody ::= dataKeyword nameDecl+ whereSignatureClause {
+	extends=declaration
+}
+private dataKeyword ::= KW_DATA | KW_CODATA
+
+record ::= KW_RECORD dataSignature whereRecordClause {
+	pin=1
+	extends=declaration
+}
 
 recordDecl ::=
    recordDeclKeywords
@@ -111,6 +121,7 @@ declaration ::=
  | implementation
  | module
  | block
+ | dataBody
  | data
  | record
  | alias
@@ -144,11 +155,12 @@ private indentationLayout ::=
   (declaration (LAYOUT_SEP? declaration)*)?
  LAYOUT_END? { pin=1 }
 
-layoutSignature ::= signature | indentationSignatureLayout
+layoutSignature ::= blockOrSig | indentationSignatureLayout
 private indentationSignatureLayout ::=
  LAYOUT_START
-  (signature (LAYOUT_SEP? signature)*)?
+  (blockOrSig (LAYOUT_SEP? blockOrSig)*)?
  LAYOUT_END? { pin=1 }
+private blockOrSig ::= block | signature
 
 layoutRecord ::= recordDecl | indentationRecordLayout
 private indentationRecordLayout ::=
@@ -181,14 +193,13 @@ private atomic ::=
  | parenExp
 
 atomicExp ::=
-   UNDERSCORE
- | QUESTION_MARK
+   QUESTION_MARK
  | HOLE
  | UNIVERSE
  | NUMBER
  | FLOAT
  | OPEN_PAREN CLOSE_PAREN
-nameExp ::= IDENTIFIER (DOT IDENTIFIER)*
+nameExp ::= IDENTIFIER (DOT IDENTIFIER)* | UNDERSCORE
 typeExp ::= argPrefix ARROW? exp
 type2Exp ::= exp ARROW exp
 asExp ::= exp AS nameExp

diff --git a/src/org/ice1000/tt/editing/agda/lex-highlight.kt b/src/org/ice1000/tt/editing/agda/lex-highlight.kt
@@ -106,7 +106,7 @@ object AgdaHighlighter : SyntaxHighlighter {
 		AgdaTypes.NUMBER -> NUMBER_KEY
 		AgdaTypes.STR_LIT -> STR_LIT_KEY
 		AgdaTypes.CHR_LIT -> CHR_LIT_KEY
-		AgdaTypes.HOLE -> HOLE_KEY
+		AgdaTypes.HOLE, AgdaTypes.QUESTION_MARK -> HOLE_KEY
 		AgdaTypes.ARROW -> ARROW_KEY
 		AgdaTypes.OPEN_PAREN, AgdaTypes.CLOSE_PAREN -> PAREN_KEY
 		AgdaTypes.OPEN_IDIOM_BRACKET, AgdaTypes.CLOSE_IDIOM_BRACKET -> BRACK_KEY

diff --git a/testData/parse/agda/BetterExampleOfDot.txt b/testData/parse/agda/BetterExampleOfDot.txt
@@ -33,27 +33,26 @@ FILE
           PsiElement(IDENTIFIER)('Equality')
       PsiWhiteSpace('\n')
       PsiWhiteSpace('\n')
-      AgdaDeclarationImpl(DECLARATION)
-        AgdaDataImpl(DATA)
-          PsiElement(KW_DATA)('data')
+      AgdaDataImpl(DATA)
+        PsiElement(KW_DATA)('data')
+        PsiWhiteSpace(' ')
+        AgdaDataSignatureImpl(DATA_SIGNATURE)
+          AgdaNameDeclImpl(NAME_DECL)
+            PsiElement(IDENTIFIER)('CannotContruct')
           PsiWhiteSpace(' ')
-          AgdaDataSignatureImpl(DATA_SIGNATURE)
-            AgdaNameDeclImpl(NAME_DECL)
-              PsiElement(IDENTIFIER)('CannotContruct')
+          PsiElement(COLON)(':')
+          PsiWhiteSpace(' ')
+          AgdaType2ExpImpl(TYPE_2_EXP)
+            AgdaNameExpImpl(NAME_EXP)
+              PsiElement(IDENTIFIER)('ℕ')
             PsiWhiteSpace(' ')
-            PsiElement(COLON)(':')
+            PsiElement(ARROW)('→')
             PsiWhiteSpace(' ')
-            AgdaType2ExpImpl(TYPE_2_EXP)
-              AgdaNameExpImpl(NAME_EXP)
-                PsiElement(IDENTIFIER)('ℕ')
-              PsiWhiteSpace(' ')
-              PsiElement(ARROW)('→')
-              PsiWhiteSpace(' ')
-              AgdaAtomicExpImpl(ATOMIC_EXP)
-                PsiElement(UNIVERSE)('Set')
-          PsiWhiteSpace(' ')
-          AgdaWhereSignatureClauseImpl(WHERE_SIGNATURE_CLAUSE)
-            PsiElement(KW_WHERE)('where')
+            AgdaAtomicExpImpl(ATOMIC_EXP)
+              PsiElement(UNIVERSE)('Set')
+        PsiWhiteSpace(' ')
+        AgdaWhereSignatureClauseImpl(WHERE_SIGNATURE_CLAUSE)
+          PsiElement(KW_WHERE)('where')
       PsiWhiteSpace('\n')
       PsiWhiteSpace('\n')
       AgdaSignatureImpl(SIGNATURE)
@@ -168,24 +167,25 @@ FILE
                     PsiElement(CLOSE_PAREN)(')')
       PsiWhiteSpace('\n')
       AgdaWithAbstractionImpl(WITH_ABSTRACTION)
-        AgdaAppExpImpl(APP_EXP)
-          AgdaNameExpImpl(NAME_EXP)
-            PsiElement(IDENTIFIER)('test')
-          PsiWhiteSpace(' ')
+        AgdaLhsImpl(LHS)
           AgdaAppExpImpl(APP_EXP)
             AgdaNameExpImpl(NAME_EXP)
-              PsiElement(IDENTIFIER)('a')
+              PsiElement(IDENTIFIER)('test')
             PsiWhiteSpace(' ')
             AgdaAppExpImpl(APP_EXP)
               AgdaNameExpImpl(NAME_EXP)
-                PsiElement(IDENTIFIER)('b')
+                PsiElement(IDENTIFIER)('a')
               PsiWhiteSpace(' ')
               AgdaAppExpImpl(APP_EXP)
                 AgdaNameExpImpl(NAME_EXP)
-                  PsiElement(IDENTIFIER)('theory')
+                  PsiElement(IDENTIFIER)('b')
                 PsiWhiteSpace(' ')
-                AgdaNameExpImpl(NAME_EXP)
-                  PsiElement(IDENTIFIER)('p')
+                AgdaAppExpImpl(APP_EXP)
+                  AgdaNameExpImpl(NAME_EXP)
+                    PsiElement(IDENTIFIER)('theory')
+                  PsiWhiteSpace(' ')
+                  AgdaNameExpImpl(NAME_EXP)
+                    PsiElement(IDENTIFIER)('p')
         PsiWhiteSpace(' ')
         PsiElement(KW_WITH)('with')
         PsiWhiteSpace('  ')