add declare-requires

RelationalAI · Apr 27, 2024 · 7599d31 · 7599d31
1 parent a472ffd
commit 7599d31
Show file tree

Hide file tree

Showing 9 changed files with 151 additions and 109 deletions.
diff --git a/dist/index.cjs b/dist/index.cjs
diff --git a/dist/index.cjs.d.ts b/dist/index.cjs.d.ts
@@ -1,8 +1,8 @@
 import { LRLanguage, LanguageSupport } from "@codemirror/language";
 declare namespace relTerms {
     const RawStringSequence: 1;
-    const spaces: 160;
-    const newLine: 161;
+    const spaces: 164;
+    const newLine: 165;
     const LineComment: 2;
     const BlockComment: 3;
     const Rel: 4;
@@ -27,10 +27,10 @@ declare namespace relTerms {
     const RawStringLiteral: 24;
     const LhsId: 27;
     const ConstructorId: 28;
-    const ParenOpId: 32;
-    const Operator: 33;
-    const QualifiedName: 34;
-    const QualifiedNameId: 35;
+    const QualifiedName: 32;
+    const QualifiedNameId: 33;
+    const ParenOpId: 39;
+    const Operator: 40;
     const QualifiedKeyword: 41;
     const QualifiedNameElem: 59;
     const Bindings: 60;
@@ -46,20 +46,21 @@ declare namespace relTerms {
     const V1Bindings: 72;
     const V1BasicActual: 73;
     const ApplicationExpression: 74;
-    const BoundedExpression: 114;
-    const V1LogicalAbstractExpression: 116;
-    const V1AbstractExpression: 130;
-    const InterpolationMultilineLiteral: 131;
-    const BoundDeclaration: 134;
-    const ValueTypeDeclaration: 135;
-    const EntityTypeDeclaration: 136;
-    const ConstraintDeclaration: 137;
-    const ModuleDeclaration: 138;
-    const WithUseDeclaration: 139;
-    const Alias: 141;
-    const AliasId: 142;
-    const ImportDeclaration: 143;
-    const NamespaceDeclaration: 145;
+    const BoundedExpression: 115;
+    const V1LogicalAbstractExpression: 117;
+    const V1AbstractExpression: 131;
+    const InterpolationMultilineLiteral: 132;
+    const BoundDeclaration: 135;
+    const DeclareBoundDeclaration: 136;
+    const ValueTypeDeclaration: 139;
+    const EntityTypeDeclaration: 140;
+    const ConstraintDeclaration: 141;
+    const ModuleDeclaration: 142;
+    const WithUseDeclaration: 143;
+    const Alias: 145;
+    const AliasId: 146;
+    const ImportDeclaration: 147;
+    const NamespaceDeclaration: 149;
 }
 declare const relLanguage: LRLanguage;
 declare function rel(): LanguageSupport;

diff --git a/dist/index.d.ts b/dist/index.d.ts
@@ -1,8 +1,8 @@
 import { LRLanguage, LanguageSupport } from "@codemirror/language";
 declare namespace relTerms {
     const RawStringSequence: 1;
-    const spaces: 160;
-    const newLine: 161;
+    const spaces: 164;
+    const newLine: 165;
     const LineComment: 2;
     const BlockComment: 3;
     const Rel: 4;
@@ -27,10 +27,10 @@ declare namespace relTerms {
     const RawStringLiteral: 24;
     const LhsId: 27;
     const ConstructorId: 28;
-    const ParenOpId: 32;
-    const Operator: 33;
-    const QualifiedName: 34;
-    const QualifiedNameId: 35;
+    const QualifiedName: 32;
+    const QualifiedNameId: 33;
+    const ParenOpId: 39;
+    const Operator: 40;
     const QualifiedKeyword: 41;
     const QualifiedNameElem: 59;
     const Bindings: 60;
@@ -46,20 +46,21 @@ declare namespace relTerms {
     const V1Bindings: 72;
     const V1BasicActual: 73;
     const ApplicationExpression: 74;
-    const BoundedExpression: 114;
-    const V1LogicalAbstractExpression: 116;
-    const V1AbstractExpression: 130;
-    const InterpolationMultilineLiteral: 131;
-    const BoundDeclaration: 134;
-    const ValueTypeDeclaration: 135;
-    const EntityTypeDeclaration: 136;
-    const ConstraintDeclaration: 137;
-    const ModuleDeclaration: 138;
-    const WithUseDeclaration: 139;
-    const Alias: 141;
-    const AliasId: 142;
-    const ImportDeclaration: 143;
-    const NamespaceDeclaration: 145;
+    const BoundedExpression: 115;
+    const V1LogicalAbstractExpression: 117;
+    const V1AbstractExpression: 131;
+    const InterpolationMultilineLiteral: 132;
+    const BoundDeclaration: 135;
+    const DeclareBoundDeclaration: 136;
+    const ValueTypeDeclaration: 139;
+    const EntityTypeDeclaration: 140;
+    const ConstraintDeclaration: 141;
+    const ModuleDeclaration: 142;
+    const WithUseDeclaration: 143;
+    const Alias: 145;
+    const AliasId: 146;
+    const ImportDeclaration: 147;
+    const NamespaceDeclaration: 149;
 }
 declare const relLanguage: LRLanguage;
 declare function rel(): LanguageSupport;

diff --git a/dist/index.js b/dist/index.js
diff --git a/src/parser.js b/src/parser.js
diff --git a/src/parser.terms.js b/src/parser.terms.js
@@ -1,8 +1,8 @@
 // This file was generated by lezer-generator. You probably shouldn't edit it.
 export const
   RawStringSequence = 1,
-  spaces = 160,
-  newLine = 161,
+  spaces = 164,
+  newLine = 165,
   LineComment = 2,
   BlockComment = 3,
   Rel = 4,
@@ -27,10 +27,10 @@ export const
   RawStringLiteral = 24,
   LhsId = 27,
   ConstructorId = 28,
-  ParenOpId = 32,
-  Operator = 33,
-  QualifiedName = 34,
-  QualifiedNameId = 35,
+  QualifiedName = 32,
+  QualifiedNameId = 33,
+  ParenOpId = 39,
+  Operator = 40,
   QualifiedKeyword = 41,
   QualifiedNameElem = 59,
   Bindings = 60,
@@ -46,17 +46,18 @@ export const
   V1Bindings = 72,
   V1BasicActual = 73,
   ApplicationExpression = 74,
-  BoundedExpression = 114,
-  V1LogicalAbstractExpression = 116,
-  V1AbstractExpression = 130,
-  InterpolationMultilineLiteral = 131,
-  BoundDeclaration = 134,
-  ValueTypeDeclaration = 135,
-  EntityTypeDeclaration = 136,
-  ConstraintDeclaration = 137,
-  ModuleDeclaration = 138,
-  WithUseDeclaration = 139,
-  Alias = 141,
-  AliasId = 142,
-  ImportDeclaration = 143,
-  NamespaceDeclaration = 145
+  BoundedExpression = 115,
+  V1LogicalAbstractExpression = 117,
+  V1AbstractExpression = 131,
+  InterpolationMultilineLiteral = 132,
+  BoundDeclaration = 135,
+  DeclareBoundDeclaration = 136,
+  ValueTypeDeclaration = 139,
+  EntityTypeDeclaration = 140,
+  ConstraintDeclaration = 141,
+  ModuleDeclaration = 142,
+  WithUseDeclaration = 143,
+  Alias = 145,
+  AliasId = 146,
+  ImportDeclaration = 147,
+  NamespaceDeclaration = 149
diff --git a/src/syntax.grammar b/src/syntax.grammar
@@ -34,6 +34,7 @@
 declaration[@isGroup=Declaration]
     { DefinitionDeclaration
     | BoundDeclaration
+    | DeclareBoundDeclaration
     | ValueTypeDeclaration
     | EntityTypeDeclaration
     | ConstraintDeclaration
@@ -80,11 +81,15 @@ Annotation { AnnotationKeyword ( !annot "(" AnnotationParams ")" )? }
  */
 
 DefinitionDeclaration {
-    Docstring? Annotation* kw<"def"> LhsId v1FormalsBracket* v1FormalsParen? ( "=" v1expression | "{" v1expression "}" )
+    Docstring? Annotation* kw<"def"> extraLhsId v1FormalsBracket* v1FormalsParen? ( "=" v1expression | "{" v1expression "}" )
 }
 
 BoundDeclaration {
-    Docstring? Annotation* kw<"bound"> LhsId v1FormalsBracket* v1FormalsParen? ( "=" v1expression | "{" v1expression "}" )?
+    Docstring? Annotation* kw<"bound"> extraLhsId v1FormalsBracket* v1FormalsParen? ( "=" v1expression | "{" v1expression "}" )?
+}
+
+DeclareBoundDeclaration {
+    Docstring? Annotation* kw<"declare"> extraLhsId ( "(" Bindings ")" kw<"requires"> v1expression )?
 }
 
 ValueTypeDeclaration {
@@ -112,7 +117,7 @@ WithUseDeclaration {
 }
 
 ImportDeclaration {
-    kw<"from"> LhsId kw<"import"> ("..." | commaSep1<Alias>)
+    Docstring? Annotation* kw<"from"> LhsId kw<"import"> ("..." | commaSep1<Alias>)
 }
 
 id { BasicId | ConstructorId | kw<"value"> | kw<"entity"> | kw<"type"> }
@@ -121,9 +126,13 @@ ParenOpId { "(" Operator !parenOp ")" }
 
 LhsId
     { id
-    | ParenOpId
     | QualifiedName
     | emphasisKeyword
+    }
+
+extraLhsId
+    { LhsId
+    | ParenOpId
     | kw<"implies">
     | kw<"iff">
     | kw<"xor">
@@ -277,10 +286,13 @@ BasicExpression
 
     | kw<"if"> v1expression kw<"then"> v1expression kw<"else"> v1expression kw<"end">
     | ( kw<"forall"> | "∀" ) "(" V1Bindings ":" v1expression ")"
+    | kw<"forall"> "(" "(" Bindings !bind ")" "|" v1expression ")"
 
     | BoundedExpression
 
     // logic expressions
+    | !quant kw<"exists"> "(" "(" Bindings !bind ")" "|" v1expression ")"
+    | !quant (kw<"exists"> | "∃") "(" V1Bindings ":" v1expression ")"
     | !quant (kw<"exists"> | "∃") BasicExpression
     | !quant (kw<"exists"> | "∃") V1LogicalAbstractExpression
     | !not ( kw<"not"> | op<"¬"> ) BasicExpression

diff --git a/test/Declarations.test.txt b/test/Declarations.test.txt
@@ -165,3 +165,28 @@ Rel(
                 BasicExpression(IntLiteral)),
             Keyword),
         Keyword))
+
+# Declare Bound Declaration
+
+declare foo (x...) requires {(:hi, FilePos, String)}(x...)
+
+==>
+
+Rel(
+    DeclareBoundDeclaration(
+        Keyword,
+        LhsId(BasicId),
+        Bindings(VarDecl(BasicId)),
+        Keyword,
+        BasicExpression(
+            ApplicationExpression(
+                BasicExpression(
+                    BoundedExpression(
+                        BasicExpression(
+                            BoundedExpression(
+                                ProductExpression(
+                                    ProductExpression(
+                                        BasicExpression(RelnameLiteral),
+                                        BasicExpression(BasicId)),
+                                    BasicExpression(BasicId)))))),
+                V1NocommaActual(BasicExpression(BasicId))))))
diff --git a/test/Identifiers.test.txt b/test/Identifiers.test.txt
@@ -89,15 +89,15 @@ Rel(
             BasicExpression(IntLiteral)),
         DefinitionDeclaration(
             Keyword,
-            LhsId(Keyword),
+            Keyword,
             BasicExpression(IntLiteral)),
         DefinitionDeclaration(
             Keyword,
-            LhsId(Keyword),
+            Keyword,
             BasicExpression(IntLiteral)),
         DefinitionDeclaration(
             Keyword,
-            LhsId(Keyword),
+            Keyword,
             BasicExpression(IntLiteral)),
         Keyword))