support experimental lightweight function syntax

grammar.js

@@ -27,7 +27,7 @@ module.exports = grammar({
     )),
 
     identifier : $ => /[a-zA-Z_]\w*/,
-    symbol     : $ => /[!@#$%^&*-+=<>,./?\[\]{}\\|`~'\"∧∨⊙×≅]+/,
+    symbol     : $ => /[!@#$%^&*-+=<>,./?{}\\|`~'\"∧∨⊙×≅]+/,
 
     comment : $ => token(seq('--', /.*/)),
 
@@ -75,15 +75,22 @@ module.exports = grammar({
     labs : $ => seq(
       choice('λ', 'fun'),
       repeat1($.param_block),
-      optional($.ascription),
       choice('=>', '⇒'),
       $.expr,
     ),
 
+    labs_alt : $ => seq(
+      '[',
+      field('param', repeat1($.identifier)),
+      ':',
+      field('type', $.expr),
+      ']',
+      $.expr,
+    ),
+
     pabs : $ => seq(
       choice('∏', 'forall'),
       repeat1($.param_block),
-      optional($.ascription),
       ',',
       $.expr,
     ),
@@ -103,7 +110,8 @@ module.exports = grammar({
 
     // HACK:
     // completely ignore precedence and associativity for treesitter
-    // this is enough to get the syntax highlighting right
+    // the syntax tree is completely wrong, but it's good enough for syntax
+    // highlighting
     binex : $ => seq(
       $.app,
       optional(seq($.symbol, $.binex)),
@@ -137,6 +145,7 @@ module.exports = grammar({
 
     app_term : $ => choice(
       $.labs,
+      $.labs_alt,
       $.pabs,
       $.let,
       $.binex,

src/grammar.json

@@ -39,7 +39,7 @@
     },
     "symbol": {
       "type": "PATTERN",
-      "value": "[!@#$%^&*-+=<>,./?\\[\\]{}\\\\|`~'\\\"∧∨⊙×≅]+"
+      "value": "[!@#$%^&*-+=<>,./?{}\\\\|`~'\\\"∧∨⊙×≅]+"
     },
     "comment": {
       "type": "TOKEN",
@@ -288,18 +288,6 @@
             "name": "param_block"
           }
         },
-        {
-          "type": "CHOICE",
-          "members": [
-            {
-              "type": "SYMBOL",
-              "name": "ascription"
-            },
-            {
-              "type": "BLANK"
-            }
-          ]
-        },
         {
           "type": "CHOICE",
           "members": [
@@ -319,6 +307,46 @@
         }
       ]
     },
+    "labs_alt": {
+      "type": "SEQ",
+      "members": [
+        {
+          "type": "STRING",
+          "value": "["
+        },
+        {
+          "type": "FIELD",
+          "name": "param",
+          "content": {
+            "type": "REPEAT1",
+            "content": {
+              "type": "SYMBOL",
+              "name": "identifier"
+            }
+          }
+        },
+        {
+          "type": "STRING",
+          "value": ":"
+        },
+        {
+          "type": "FIELD",
+          "name": "type",
+          "content": {
+            "type": "SYMBOL",
+            "name": "expr"
+          }
+        },
+        {
+          "type": "STRING",
+          "value": "]"
+        },
+        {
+          "type": "SYMBOL",
+          "name": "expr"
+        }
+      ]
+    },
     "pabs": {
       "type": "SEQ",
       "members": [
@@ -342,18 +370,6 @@
             "name": "param_block"
           }
         },
-        {
-          "type": "CHOICE",
-          "members": [
-            {
-              "type": "SYMBOL",
-              "name": "ascription"
-            },
-            {
-              "type": "BLANK"
-            }
-          ]
-        },
         {
           "type": "STRING",
           "value": ","
@@ -552,6 +568,10 @@
           "type": "SYMBOL",
           "name": "labs"
         },
+        {
+          "type": "SYMBOL",
+          "name": "labs_alt"
+        },
         {
           "type": "SYMBOL",
           "name": "pabs"

src/node-types.json

@@ -30,6 +30,10 @@
           "type": "labs",
           "named": true
         },
+        {
+          "type": "labs_alt",
+          "named": true
+        },
         {
           "type": "let",
           "named": true
@@ -244,10 +248,6 @@
       "multiple": true,
       "required": true,
       "types": [
-        {
-          "type": "ascription",
-          "named": true
-        },
         {
           "type": "expr",
           "named": true
@@ -259,6 +259,42 @@
       ]
     }
   },
+  {
+    "type": "labs_alt",
+    "named": true,
+    "fields": {
+      "param": {
+        "multiple": true,
+        "required": true,
+        "types": [
+          {
+            "type": "identifier",
+            "named": true
+          }
+        ]
+      },
+      "type": {
+        "multiple": false,
+        "required": true,
+        "types": [
+          {
+            "type": "expr",
+            "named": true
+          }
+        ]
+      }
+    },
+    "children": {
+      "multiple": false,
+      "required": true,
+      "types": [
+        {
+          "type": "expr",
+          "named": true
+        }
+      ]
+    }
+  },
   {
     "type": "let",
     "named": true,
@@ -301,10 +337,6 @@
       "multiple": true,
       "required": true,
       "types": [
-        {
-          "type": "ascription",
-          "named": true
-        },
         {
           "type": "expr",
           "named": true
@@ -539,10 +571,18 @@
     "type": "=>",
     "named": false
   },
+  {
+    "type": "[",
+    "named": false
+  },
   {
     "type": "[]",
     "named": false
   },
+  {
+    "type": "]",
+    "named": false
+  },
   {
     "type": "axiom",
     "named": false

test/corpus/labs.txt

@@ -2,7 +2,8 @@
 Lambda Abstraction
 ==================
 
-def foo := fun (A : ★) (x : A) : A => x;
+def foo := fun (A B : ★) (x : A) (y : B) => x;
+def bar := [A B : ★][x : A][y : B] x;
 
 ----------
 
@@ -13,6 +14,7 @@ def foo := fun (A : ★) (x : A) : A => x;
           (app_term
             (labs
               (param_block
+                (identifier)
                 (identifier)
                 (expr
                   (app_term
@@ -29,7 +31,8 @@ def foo := fun (A : ★) (x : A) : A => x;
                       (app
                         (term
                           (identifier)))))))
-              (ascription
+              (param_block
+                (identifier)
                 (expr
                   (app_term
                     (binex
@@ -41,4 +44,44 @@ def foo := fun (A : ★) (x : A) : A => x;
                   (binex
                     (app
                       (term
-                        (identifier)))))))))))
+                        (identifier))))))))))
+      (definition
+        (identifier)
+        (expr
+          (app_term
+            (labs_alt
+              (identifier)
+              (identifier)
+              (expr
+                (app_term
+                  (binex
+                    (app
+                      (term
+                        (sort
+                          (star)))))))
+              (expr
+                (app_term
+                  (labs_alt
+                    (identifier)
+                    (expr
+                      (app_term
+                        (binex
+                          (app
+                            (term
+                              (identifier))))))
+                    (expr
+                      (app_term
+                        (labs_alt
+                          (identifier)
+                          (expr
+                            (app_term
+                              (binex
+                                (app
+                                  (term
+                                    (identifier))))))
+                          (expr
+                            (app_term
+                              (binex
+                                (app
+                                  (term
+                                    (identifier)))))))))))))))))