new syntax, also block comments are totally broken

grammar.js

@@ -12,30 +12,17 @@ module.exports = grammar({
 
   extras: $ => [
     $.comment,
-    $.block_comment,
     /\s/,
   ],
 
   rules: {
 
-    program : $ => repeat(choice($.definition, $.preprocess)),
+    program : $ => repeat(choice($.definition, $.preprocess, $.axiom)),
 
     identifier : $ => /[a-zA-Z_]\w*/,
 
     comment : $ => token(seq('--', /.*/)),
 
-    block_comment: $ => token(seq(
-      '[*',
-      repeat(choice(
-        /[^\[\]*]/,
-        /\[[^*]/,
-        /\*[^\]]/,
-        /\[\*/,
-        /\*\]/,
-      )),
-      '*]'
-    )),
-
     param_block : $ => seq(
       '(',
       field('param', repeat1($.identifier)),
@@ -72,6 +59,7 @@ module.exports = grammar({
       '(',
       $.identifier,
       repeat($.param_block),
+      optional($.ascription),
       ':=',
       $.expr,
       ')',
@@ -112,12 +100,21 @@ module.exports = grammar({
       field('type', $.expr),
     ),
 
+    axiom : $ => seq(
+      'axiom',
+      field('name', $.identifier),
+      repeat($.param_block),
+      $.ascription,
+      ';'
+    ),
+
     definition : $ => seq(
+      'def',
       field('name', $.identifier),
       repeat($.param_block),
       optional($.ascription),
       ':=',
-      choice($.expr, $.axiom),
+      choice($.expr),
       ';',
     ),
 

src/grammar.json

@@ -13,6 +13,10 @@
           {
             "type": "SYMBOL",
             "name": "preprocess"
+          },
+          {
+            "type": "SYMBOL",
+            "name": "axiom"
           }
         ]
       }
@@ -37,50 +41,6 @@
         ]
       }
     },
-    "block_comment": {
-      "type": "TOKEN",
-      "content": {
-        "type": "SEQ",
-        "members": [
-          {
-            "type": "STRING",
-            "value": "[*"
-          },
-          {
-            "type": "REPEAT",
-            "content": {
-              "type": "CHOICE",
-              "members": [
-                {
-                  "type": "PATTERN",
-                  "value": "[^\\[\\]*]"
-                },
-                {
-                  "type": "PATTERN",
-                  "value": "\\[[^*]"
-                },
-                {
-                  "type": "PATTERN",
-                  "value": "\\*[^\\]]"
-                },
-                {
-                  "type": "PATTERN",
-                  "value": "\\[\\*"
-                },
-                {
-                  "type": "PATTERN",
-                  "value": "\\*\\]"
-                }
-              ]
-            }
-          },
-          {
-            "type": "STRING",
-            "value": "*]"
-          }
-        ]
-      }
-    },
     "param_block": {
       "type": "SEQ",
       "members": [
@@ -261,6 +221,18 @@
             "name": "param_block"
           }
         },
+        {
+          "type": "CHOICE",
+          "members": [
+            {
+              "type": "SYMBOL",
+              "name": "ascription"
+            },
+            {
+              "type": "BLANK"
+            }
+          ]
+        },
         {
           "type": "STRING",
           "value": ":="
@@ -311,9 +283,37 @@
       }
     },
     "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,
@@ -398,6 +398,10 @@
     "definition": {
       "type": "SEQ",
       "members": [
+        {
+          "type": "STRING",
+          "value": "def"
+        },
         {
           "type": "FIELD",
           "name": "name",
@@ -435,10 +439,6 @@
             {
               "type": "SYMBOL",
               "name": "expr"
-            },
-            {
-              "type": "SYMBOL",
-              "name": "axiom"
             }
           ]
         },
@@ -475,10 +475,6 @@
       "type": "SYMBOL",
       "name": "comment"
     },
-    {
-      "type": "SYMBOL",
-      "name": "block_comment"
-    },
     {
       "type": "PATTERN",
       "value": "\\s"

src/node-types.json

@@ -76,6 +76,36 @@
       }
     }
   },
+  {
+    "type": "axiom",
+    "named": true,
+    "fields": {
+      "name": {
+        "multiple": false,
+        "required": true,
+        "types": [
+          {
+            "type": "identifier",
+            "named": true
+          }
+        ]
+      }
+    },
+    "children": {
+      "multiple": true,
+      "required": true,
+      "types": [
+        {
+          "type": "ascription",
+          "named": true
+        },
+        {
+          "type": "param_block",
+          "named": true
+        }
+      ]
+    }
+  },
   {
     "type": "binding",
     "named": true,
@@ -84,6 +114,10 @@
       "multiple": true,
       "required": true,
       "types": [
+        {
+          "type": "ascription",
+          "named": true
+        },
         {
           "type": "expr",
           "named": true
@@ -122,10 +156,6 @@
           "type": "ascription",
           "named": true
         },
-        {
-          "type": "axiom",
-          "named": true
-        },
         {
           "type": "expr",
           "named": true
@@ -266,6 +296,10 @@
       "multiple": true,
       "required": false,
       "types": [
+        {
+          "type": "axiom",
+          "named": true
+        },
         {
           "type": "definition",
           "named": true
@@ -347,11 +381,7 @@
   },
   {
     "type": "axiom",
-    "named": true
+    "named": false
-  },
-  {
-    "type": "block_comment",
-    "named": true
   },
   {
     "type": "command",
@@ -361,6 +391,10 @@
     "type": "comment",
     "named": true
   },
+  {
+    "type": "def",
+    "named": false
+  },
   {
     "type": "end",
     "named": false

test/corpus/application.txt

@@ -2,10 +2,11 @@
 Application
 ===========
 
-foo (A B : *) (f : A -> B) (x : A) := 
+def foo (A B : *) (f : A -> B) (x : A) := 
     (fun (x : B) => x) (f x);
 
 ---
+
 (program
   (definition
     (identifier)

test/corpus/arrows.txt

@@ -2,7 +2,7 @@
 Arrows
 ======
 
-foo (A B : *) (f : A -> A -> B) (x : A) := f x x;
+def foo (A B : *) (f : A -> A -> B) (x : A) := f x x;
 
 ---
 

test/corpus/axioms.txt

@@ -2,17 +2,16 @@
 Axioms
 ======
 
-nat : * := axiom;
+axiom nat : *;
 
 -----
 
 (program
-  (definition
+  (axiom
     (identifier)
     (ascription
       (expr
         (app_term
           (app
             (term
-              (star))))))
+              (star))))))))
-    (axiom)))

test/corpus/comments.txt

@@ -2,23 +2,9 @@
 Comments
 ========
 
--- here's a comment
+[* foo [* nested *] *]
-
+axiom nat : *;
-foo := 
+[* bar *]
-    -- and a comment in the middle
-    [* and a [* nested *] block comment *]
-    *;
 
 ---
 
-(program
-  (comment)
-  (definition
-    (identifier)
-    (comment)
-    (block_comment)
-    (expr
-      (app_term
-        (app
-          (term
-            (star)))))))

test/corpus/include.txt

@@ -4,7 +4,7 @@ Include
 
 @include foo.pg
 
-baz : * := A;
+def baz : * := A;
 
 @include bar.pg
 

test/corpus/labs.txt

@@ -2,7 +2,7 @@
 Lambda Abstraction
 ==================
 
-foo := fun (A : *) (x : A) => x;
+def foo := fun (A : *) (x : A) => x;
 
 ----------
 

test/corpus/let.txt

@@ -2,7 +2,8 @@
 Let
 ===
 
-foo := let (x := a)
+def foo :=
+    let (x : bar := a)
         (y := x)
         (f (x : A) := x)
     in
@@ -19,6 +20,12 @@ foo := let (x := a)
         (let
           (binding
             (identifier)
+            (ascription
+              (expr
+                (app_term
+                  (app
+                    (term
+                      (identifier))))))
             (expr
               (app_term
                 (app

test/corpus/pabs.txt

@@ -2,7 +2,7 @@
 Pi Abstraction
 ==============
 
-rel := forall (A : *) (x : A), *;
+def rel := forall (A : *) (x : A), *;
 
 ----------
 

test/corpus/params.txt

@@ -2,7 +2,7 @@
 Definition
 ==========
 
-foo (A : *) (x y z : A) := x;
+def foo (A : *) (x y z : A) := x;
 
 ---