Fix various type related rules

- variant constructor can have zero arguments (e.g. `Just(int) | Nothing`) - type alias can be quantified with type parameter (e.g. `type List[a]` = ...`) - polymorphic types can have multiple type arguments (e.g. `List[a,b]`) - operator types can have multiple arguments (e.g. `(int, bool) => int`) or no arguments (e.g. `() => int`)
gruhn · Oct 7, 2024 · 20801ef · 20801ef
1 parent 0caf7d5
commit 20801ef
Show file tree

Hide file tree

Showing 3 changed files with 139 additions and 14 deletions.
diff --git a/grammar.js b/grammar.js
@@ -69,21 +69,39 @@ module.exports = grammar({
 
     // TODO: all types covered?
     type: $ => choice(
-      $.identifier, // basic type
+      prec('basic_type', $.identifier), // basic type
       $.operator_type,
       $.function_type,
       $.polymorphic_type,
-      $.sum_type, // QUESTION: are sum types allowed everywhere?
     ),
 
+    // QUESTION: function types always have exaclty one argument?
     function_type: $ => prec.right('function_type', seq($.type, '->', $.type)),
 
-    operator_type: $ => prec.right('operator_type', seq($.type, '=>', $.type)),
+    operator_type: $ => prec.right('operator_type', seq(
+      choice(
+        $.type, // single argument / no parens, e.g. `int => bool`
+        withParens(sepBy(',', $.type)), // zero or more arguments, e.g. `(int, int) => int`
+      ),
+      "=>",
+      $.type, // result type
+    )),
 
-    polymorphic_type: $ => seq($.identifier, '[', $.type, ']'),
+    polymorphic_type: $ => seq(
+      $.identifier, 
+      withBrackets(sepBy1(',', $.type))
+    ),
+
+    // TODO: can variant constructors have more than one argument?
+    variant_constructor: $ => prec('variant_constr', seq(
+      $.identifier, 
+      optional(withParens($.type))
+    )),
 
-    // TODO: can type constructors have more/less than one argument?
-    sum_type: $ => sepBy1('|', seq($.identifier, withParens($.type))),
+    // We say sum types must have at least two variant constructor.
+    // One variant constructor makes sense, but can't be distingished
+    // with a basic type like `int`.
+    sum_type: $ => sepBy1('|', $.variant_constructor),
 
     /////////// Module-level constructs ///////////
 
@@ -112,7 +130,7 @@ module.exports = grammar({
     ),
 
     typed_argument_list: $ => withParens(
-      sepBy1(
+      sepBy(
         ',',
         seq(
           $.identifier,
@@ -150,7 +168,16 @@ module.exports = grammar({
     // TODO: https://quint-lang.org/docs/lang#module-instances
 
     // TODO: type alias identifier must be all CAPS
-    type_alias: $ => seq('type', $.identifier, '=', $.type),
+    type_alias: $ => seq(
+      'type', 
+      $.identifier, 
+      optional(withBrackets(sepBy1(',', $.identifier))), // optional type arguments
+      '=', 
+      choice(
+        $.type, 
+        $.sum_type,
+      )
+    ),
 
     /////////// Namespaces and Imports  ///////////
 
@@ -329,6 +356,8 @@ module.exports = grammar({
     [
       'function_type',
       'operator_type',
+      'variant_constr',
+      'basic_type',
     ]
   ],
 

diff --git a/queries/helix-highlights.scm b/queries/helix-highlights.scm
@@ -93,6 +93,8 @@
 (polymorphic_type 
   (type) @type.parameter)
 
+(variant_constructor) @type.enum.variant
+
 (type) @type
 (int_literal) @constant.numeric.integer
 (comment) @comment

diff --git a/test/corpus/module-level-constructs.txt b/test/corpus/module-level-constructs.txt
@@ -81,7 +81,7 @@ var isArmed: bool
 Static Constant Value
 ========================
 
-pure val Nodes: Set[int] = 1 to 10
+pure val Nodes: Set[int] = 1.to(10)
 
 ---
 
@@ -93,7 +93,14 @@ pure val Nodes: Set[int] = 1 to 10
         (identifier)
         (type
           (identifier))))
-    (expr)))
+    (expr
+      (binary_expr
+        (expr
+          (int_literal))
+        (operator_application
+          (identifier)
+          (expr
+            (int_literal)))))))
 
 
 ==========================================
@@ -114,6 +121,23 @@ pure val eleven = 11;
 Two-Argument Operator
 ========================
 
+pure def fst(): int = 1
+
+---
+
+(source_file
+  (operator_definition
+    (identifier)
+    (typed_argument_list)
+    (type
+      (identifier))
+    (expr
+      (int_literal))))
+
+========================
+Two-Argument Operator
+========================
+
 pure def fst(x: int, y: int): int = 
   x
 
@@ -309,18 +333,88 @@ type INT_SET = Set[int]
 Sum Type
 ========================
 
-type Elem = S(str) | I(int)
+type Elem = S(str) | I(int) | Nil
 
 ---
 
 (source_file
   (type_alias
     (identifier)
-    (type
-      (sum_type
+    (sum_type
+      (variant_constructor
         (identifier)
         (type
-          (identifier))
+          (identifier)))
+      (variant_constructor
         (identifier)
+        (type
+          (identifier)))
+      (variant_constructor
+        (identifier)))))
+
+========================
+Operator Type
+========================
+
+type _ = int => int
+type _ = () => int
+type _ = (int) => int
+type _ = (int, bool) => int
+
+---
+
+(source_file
+  (type_alias
+    (identifier)
+    (type
+      (operator_type
+        (type
+          (identifier))
+        (type
+          (identifier)))))
+  (type_alias
+    (identifier)
+    (type
+      (operator_type
+        (type
+          (identifier)))))
+  (type_alias
+    (identifier)
+    (type
+      (operator_type
+        (type
+          (identifier))
+        (type
+          (identifier)))))
+  (type_alias
+    (identifier)
+    (type
+      (operator_type
+        (type
+          (identifier))
+        (type
+          (identifier))
         (type
           (identifier))))))
+
+========================
+Function Type
+========================
+
+type _ = bool -> int -> int
+
+---
+
+(source_file
+  (type_alias
+    (identifier)
+    (type
+      (function_type
+        (type
+          (identifier))
+        (type
+          (function_type
+            (type
+              (identifier))
+            (type
+              (identifier))))))))