impredicative/predicative split

grammar.js

@@ -33,6 +33,7 @@ module.exports = grammar({
 
     star   : $ => "*",
     square : $ => choice('□', '[]'),
+    sort   : $ => choice($.star, $.square, seq($.square, /[0-9₀₁₂₃₄₅₆₇₈₉]+/)),
 
     labs : $ => seq(
       choice('λ', 'fun'),
@@ -52,8 +53,7 @@ module.exports = grammar({
 
     term : $ => choice(
       $.identifier,
-      $.star,
+      $.sort,
-      $.square,
       seq('(', $.expr, ')'),
     ),
 

src/grammar.json

@@ -94,6 +94,32 @@
         }
       ]
     },
+    "sort": {
+      "type": "CHOICE",
+      "members": [
+        {
+          "type": "SYMBOL",
+          "name": "star"
+        },
+        {
+          "type": "SYMBOL",
+          "name": "square"
+        },
+        {
+          "type": "SEQ",
+          "members": [
+            {
+              "type": "SYMBOL",
+              "name": "square"
+            },
+            {
+              "type": "PATTERN",
+              "value": "[0-9₀₁₂₃₄₅₆₇₈₉]+"
+            }
+          ]
+        }
+      ]
+    },
     "labs": {
       "type": "SEQ",
       "members": [
@@ -202,11 +228,7 @@
         },
         {
           "type": "SYMBOL",
-          "name": "star"
+          "name": "sort"
-        },
-        {
-          "type": "SYMBOL",
-          "name": "square"
         },
         {
           "type": "SEQ",

src/node-types.json

@@ -319,6 +319,25 @@
       ]
     }
   },
+  {
+    "type": "sort",
+    "named": true,
+    "fields": {},
+    "children": {
+      "multiple": false,
+      "required": true,
+      "types": [
+        {
+          "type": "square",
+          "named": true
+        },
+        {
+          "type": "star",
+          "named": true
+        }
+      ]
+    }
+  },
   {
     "type": "square",
     "named": true,
@@ -341,11 +360,7 @@
           "named": true
         },
         {
-          "type": "square",
+          "type": "sort",
-          "named": true
-        },
-        {
-          "type": "star",
           "named": true
         }
       ]

test/corpus/application.txt

@@ -17,7 +17,8 @@ def foo (A B : *) (f : A -> B) (x : A) :=
         (app_term
           (app
             (term
-              (star))))))
+              (sort
+                (star)))))))
     (param_block
       (identifier)
       (expr

test/corpus/arrows.txt

@@ -16,7 +16,8 @@ def foo (A B : *) (f : A -> A -> B) (x : A) := f x x;
         (app_term
           (app
             (term
-              (star))))))
+              (sort
+                (star)))))))
     (param_block
       (identifier)
       (expr

test/corpus/axioms.txt

@@ -14,4 +14,5 @@ axiom nat : *;
         (app_term
           (app
             (term
-              (star))))))))
+              (sort
+                (star)))))))))

test/corpus/include.txt

@@ -21,7 +21,8 @@ def baz : * := A;
         (app_term
           (app
             (term
-              (star))))))
+              (sort
+                (star)))))))
     (expr
       (app_term
         (app

test/corpus/labs.txt

@@ -18,7 +18,8 @@ def foo := fun (A : *) (x : A) : A => x;
               (app_term
                 (app
                   (term
-                    (star))))))
+                    (sort
+                      (star)))))))
           (param_block
             (identifier)
             (expr

test/corpus/pabs.txt

@@ -18,7 +18,8 @@ def rel := forall (A : *) (x : A), *;
               (app_term
                 (app
                   (term
-                    (star))))))
+                    (sort
+                      (star)))))))
           (param_block
             (identifier)
             (expr
@@ -30,4 +31,5 @@ def rel := forall (A : *) (x : A), *;
             (app_term
               (app
                 (term
-                  (star))))))))))
+                  (sort
+                    (star)))))))))))

test/corpus/params.txt

@@ -15,7 +15,8 @@ def foo (A : *) (x y z : A) := x;
         (app_term
           (app
             (term
-              (star))))))
+              (sort
+                (star)))))))
     (param_block
       (identifier)
       (identifier)

test/corpus/sorts.txt

@@ -0,0 +1,72 @@
+=====
+Sorts
+=====
+
+def foo (A : *) (B : □) (C : □₁) (D : []) (E : []1) (F : □1) (G : □₁₂₃) := A;
+
+---
+
+(program
+  (definition
+    (identifier)
+    (param_block
+      (identifier)
+      (expr
+        (app_term
+          (app
+            (term
+              (sort
+                (star)))))))
+    (param_block
+      (identifier)
+      (expr
+        (app_term
+          (app
+            (term
+              (sort
+                (square)))))))
+    (param_block
+      (identifier)
+      (expr
+        (app_term
+          (app
+            (term
+              (sort
+                (square)))))))
+    (param_block
+      (identifier)
+      (expr
+        (app_term
+          (app
+            (term
+              (sort
+                (square)))))))
+    (param_block
+      (identifier)
+      (expr
+        (app_term
+          (app
+            (term
+              (sort
+                (square)))))))
+    (param_block
+      (identifier)
+      (expr
+        (app_term
+          (app
+            (term
+              (sort
+                (square)))))))
+    (param_block
+      (identifier)
+      (expr
+        (app_term
+          (app
+            (term
+              (sort
+                (square)))))))
+    (expr
+      (app_term
+        (app
+          (term
+            (identifier)))))))