added let expressions

grammar.js

@@ -68,6 +68,22 @@ module.exports = grammar({
       seq('(', $.expr, ')'),
     ),
 
+    binding : $ => seq(
+      '(',
+      $.identifier,
+      ':=',
+      $.expr,
+      ')',
+    ),
+
+    let : $ => seq(
+      'let',
+      repeat1($.binding),
+      'in',
+      $.expr,
+      'end',
+    ),
+
     app : $ => repeat1($.term),
 
     axiom : $ => 'axiom',
@@ -81,6 +97,7 @@ module.exports = grammar({
     app_term : $ => choice(
       $.labs,
       $.pabs,
+      $.let,
       $.app,
     ),
 

src/grammar.json

@@ -243,6 +243,59 @@
         }
       ]
     },
+    "binding": {
+      "type": "SEQ",
+      "members": [
+        {
+          "type": "STRING",
+          "value": "("
+        },
+        {
+          "type": "SYMBOL",
+          "name": "identifier"
+        },
+        {
+          "type": "STRING",
+          "value": ":="
+        },
+        {
+          "type": "SYMBOL",
+          "name": "expr"
+        },
+        {
+          "type": "STRING",
+          "value": ")"
+        }
+      ]
+    },
+    "let": {
+      "type": "SEQ",
+      "members": [
+        {
+          "type": "STRING",
+          "value": "let"
+        },
+        {
+          "type": "REPEAT1",
+          "content": {
+            "type": "SYMBOL",
+            "name": "binding"
+          }
+        },
+        {
+          "type": "STRING",
+          "value": "in"
+        },
+        {
+          "type": "SYMBOL",
+          "name": "expr"
+        },
+        {
+          "type": "STRING",
+          "value": "end"
+        }
+      ]
+    },
     "app": {
       "type": "REPEAT1",
       "content": {
@@ -295,6 +348,10 @@
           "type": "SYMBOL",
           "name": "pabs"
         },
+        {
+          "type": "SYMBOL",
+          "name": "let"
+        },
         {
           "type": "SYMBOL",
           "name": "app"

src/node-types.json

@@ -30,6 +30,10 @@
           "type": "labs",
           "named": true
         },
+        {
+          "type": "let",
+          "named": true
+        },
         {
           "type": "pabs",
           "named": true
@@ -72,6 +76,25 @@
       }
     }
   },
+  {
+    "type": "binding",
+    "named": true,
+    "fields": {},
+    "children": {
+      "multiple": true,
+      "required": true,
+      "types": [
+        {
+          "type": "expr",
+          "named": true
+        },
+        {
+          "type": "identifier",
+          "named": true
+        }
+      ]
+    }
+  },
   {
     "type": "definition",
     "named": true,
@@ -148,6 +171,25 @@
       ]
     }
   },
+  {
+    "type": "let",
+    "named": true,
+    "fields": {},
+    "children": {
+      "multiple": true,
+      "required": true,
+      "types": [
+        {
+          "type": "binding",
+          "named": true
+        },
+        {
+          "type": "expr",
+          "named": true
+        }
+      ]
+    }
+  },
   {
     "type": "pabs",
     "named": true,
@@ -315,6 +357,10 @@
     "type": "comment",
     "named": true
   },
+  {
+    "type": "end",
+    "named": false
+  },
   {
     "type": "forall",
     "named": false
@@ -327,6 +373,14 @@
     "type": "identifier",
     "named": true
   },
+  {
+    "type": "in",
+    "named": false
+  },
+  {
+    "type": "let",
+    "named": false
+  },
   {
     "type": "post_command",
     "named": true

test/corpus/let.txt

@@ -0,0 +1,37 @@
+===
+Let
+===
+
+foo := let (x := a)
+           (y := x)
+       in
+           x
+       end;
+
+---
+
+(program
+  (definition
+    (identifier)
+    (expr
+      (app_term
+        (let
+          (binding
+            (identifier)
+            (expr
+              (app_term
+                (app
+                  (term
+                    (identifier))))))
+          (binding
+            (identifier)
+            (expr
+              (app_term
+                (app
+                  (term
+                    (identifier))))))
+          (expr
+            (app_term
+              (app
+                (term
+                  (identifier))))))))))