accommodated new ascriptions

grammar.js

@@ -37,6 +37,7 @@ module.exports = grammar({
     labs : $ => seq(
       choice('λ', 'fun'),
       repeat1($.param_block),
+      optional($.ascription),
       choice('=>', '⇒'),
       $.expr,
     ),
@@ -44,6 +45,7 @@ module.exports = grammar({
     pabs : $ => seq(
       choice('∏', 'forall'),
       repeat1($.param_block),
+      optional($.ascription),
       ',',
       $.expr,
     ),
@@ -75,8 +77,6 @@ module.exports = grammar({
 
     app : $ => repeat1($.term),
 
-    axiom : $ => 'axiom',
-
     arrow : $ => prec.left(1, seq(
       $.app_term,
       choice('->', '→'),

src/grammar.json

@@ -117,6 +117,18 @@
             "name": "param_block"
           }
         },
+        {
+          "type": "CHOICE",
+          "members": [
+            {
+              "type": "SYMBOL",
+              "name": "ascription"
+            },
+            {
+              "type": "BLANK"
+            }
+          ]
+        },
         {
           "type": "CHOICE",
           "members": [
@@ -159,6 +171,18 @@
             "name": "param_block"
           }
         },
+        {
+          "type": "CHOICE",
+          "members": [
+            {
+              "type": "SYMBOL",
+              "name": "ascription"
+            },
+            {
+              "type": "BLANK"
+            }
+          ]
+        },
         {
           "type": "STRING",
           "value": ","
@@ -282,38 +306,6 @@
         "name": "term"
       }
     },
-    "axiom": {
-      "type": "SEQ",
-      "members": [
-        {
-          "type": "STRING",
-          "value": "axiom"
-        },
-        {
-          "type": "FIELD",
-          "name": "name",
-          "content": {
-            "type": "SYMBOL",
-            "name": "identifier"
-          }
-        },
-        {
-          "type": "REPEAT",
-          "content": {
-            "type": "SYMBOL",
-            "name": "param_block"
-          }
-        },
-        {
-          "type": "SYMBOL",
-          "name": "ascription"
-        },
-        {
-          "type": "STRING",
-          "value": ";"
-        }
-      ]
-    },
     "arrow": {
       "type": "PREC_LEFT",
       "value": 1,
@@ -395,6 +387,38 @@
         }
       ]
     },
+    "axiom": {
+      "type": "SEQ",
+      "members": [
+        {
+          "type": "STRING",
+          "value": "axiom"
+        },
+        {
+          "type": "FIELD",
+          "name": "name",
+          "content": {
+            "type": "SYMBOL",
+            "name": "identifier"
+          }
+        },
+        {
+          "type": "REPEAT",
+          "content": {
+            "type": "SYMBOL",
+            "name": "param_block"
+          }
+        },
+        {
+          "type": "SYMBOL",
+          "name": "ascription"
+        },
+        {
+          "type": "STRING",
+          "value": ";"
+        }
+      ]
+    },
     "definition": {
       "type": "SEQ",
       "members": [

src/node-types.json

@@ -194,6 +194,10 @@
       "multiple": true,
       "required": true,
       "types": [
+        {
+          "type": "ascription",
+          "named": true
+        },
         {
           "type": "expr",
           "named": true
@@ -232,6 +236,10 @@
       "multiple": true,
       "required": true,
       "types": [
+        {
+          "type": "ascription",
+          "named": true
+        },
         {
           "type": "expr",
           "named": true

test/corpus/labs.txt

@@ -2,7 +2,7 @@
 Lambda Abstraction
 ==================
 
-def foo := fun (A : *) (x : A) => x;
+def foo := fun (A : *) (x : A) : A => x;
 
 ----------
 
@@ -26,6 +26,12 @@ def foo := fun (A : *) (x : A) => x;
                 (app
                   (term
                     (identifier))))))
+          (ascription
+            (expr
+              (app_term
+                (app
+                  (term
+                    (identifier))))))
           (expr
             (app_term
               (app