sections

grammar.js

@@ -17,12 +17,24 @@ module.exports = grammar({
 
   rules: {
 
-    program : $ => repeat(choice($.definition, $.preprocess, $.axiom)),
+    program : $ => repeat1(choice($.definition, $.preprocess, $.axiom, $.section, $.variable)),
 
     identifier : $ => /[a-zA-Z_]\w*/,
 
     comment : $ => token(seq('--', /.*/)),
 
+    section : $ => seq(
+      'section', $.identifier,
+      $.program,
+      'end', $.identifier,
+    ),
+
+    variable : $ => seq(
+      choice('variable', 'hypothesis'),
+      repeat1($.param_block),
+      ';'
+    ),
+
     param_block : $ => seq(
       '(',
       field('param', repeat1($.identifier)),

src/grammar.json

@@ -2,7 +2,7 @@
   "name": "perga",
   "rules": {
     "program": {
-      "type": "REPEAT",
+      "type": "REPEAT1",
       "content": {
         "type": "CHOICE",
         "members": [
@@ -17,6 +17,14 @@
           {
             "type": "SYMBOL",
             "name": "axiom"
+          },
+          {
+            "type": "SYMBOL",
+            "name": "section"
+          },
+          {
+            "type": "SYMBOL",
+            "name": "variable"
           }
         ]
       }
@@ -41,6 +49,60 @@
         ]
       }
     },
+    "section": {
+      "type": "SEQ",
+      "members": [
+        {
+          "type": "STRING",
+          "value": "section"
+        },
+        {
+          "type": "SYMBOL",
+          "name": "identifier"
+        },
+        {
+          "type": "SYMBOL",
+          "name": "program"
+        },
+        {
+          "type": "STRING",
+          "value": "end"
+        },
+        {
+          "type": "SYMBOL",
+          "name": "identifier"
+        }
+      ]
+    },
+    "variable": {
+      "type": "SEQ",
+      "members": [
+        {
+          "type": "CHOICE",
+          "members": [
+            {
+              "type": "STRING",
+              "value": "variable"
+            },
+            {
+              "type": "STRING",
+              "value": "hypothesis"
+            }
+          ]
+        },
+        {
+          "type": "REPEAT1",
+          "content": {
+            "type": "SYMBOL",
+            "name": "param_block"
+          }
+        },
+        {
+          "type": "STRING",
+          "value": ";"
+        }
+      ]
+    },
     "param_block": {
       "type": "SEQ",
       "members": [

src/node-types.json

@@ -302,7 +302,7 @@
     "fields": {},
     "children": {
       "multiple": true,
-      "required": false,
+      "required": true,
       "types": [
         {
           "type": "axiom",
@@ -315,6 +315,33 @@
         {
           "type": "preprocess",
           "named": true
+        },
+        {
+          "type": "section",
+          "named": true
+        },
+        {
+          "type": "variable",
+          "named": true
+        }
+      ]
+    }
+  },
+  {
+    "type": "section",
+    "named": true,
+    "fields": {},
+    "children": {
+      "multiple": true,
+      "required": true,
+      "types": [
+        {
+          "type": "identifier",
+          "named": true
+        },
+        {
+          "type": "program",
+          "named": true
         }
       ]
     }
@@ -366,6 +393,21 @@
       ]
     }
   },
+  {
+    "type": "variable",
+    "named": true,
+    "fields": {},
+    "children": {
+      "multiple": true,
+      "required": true,
+      "types": [
+        {
+          "type": "param_block",
+          "named": true
+        }
+      ]
+    }
+  },
   {
     "type": "(",
     "named": false
@@ -430,6 +472,10 @@
     "type": "fun",
     "named": false
   },
+  {
+    "type": "hypothesis",
+    "named": false
+  },
   {
     "type": "identifier",
     "named": true
@@ -446,10 +492,18 @@
     "type": "post_command",
     "named": true
   },
+  {
+    "type": "section",
+    "named": false
+  },
   {
     "type": "star",
     "named": true
   },
+  {
+    "type": "variable",
+    "named": false
+  },
   {
     "type": "λ",
     "named": false

test/corpus/section.txt

@@ -0,0 +1,72 @@
+========
+Sections
+========
+
+section Test
+    variable (A B C : *);
+    hypothesis (x : A) (y : B) (z1 z2 : C);
+
+    section Nested
+        def foo (x : A) := y;
+    end Nested
+end Test
+
+----
+
+(program
+  (section
+    (identifier)
+    (program
+      (variable
+        (param_block
+          (identifier)
+          (identifier)
+          (identifier)
+          (expr
+            (app_term
+              (app
+                (term
+                  (sort
+                    (star))))))))
+      (variable
+        (param_block
+          (identifier)
+          (expr
+            (app_term
+              (app
+                (term
+                  (identifier))))))
+        (param_block
+          (identifier)
+          (expr
+            (app_term
+              (app
+                (term
+                  (identifier))))))
+        (param_block
+          (identifier)
+          (identifier)
+          (expr
+            (app_term
+              (app
+                (term
+                  (identifier)))))))
+      (section
+        (identifier)
+        (program
+          (definition
+            (identifier)
+            (param_block
+              (identifier)
+              (expr
+                (app_term
+                  (app
+                    (term
+                      (identifier))))))
+            (expr
+              (app_term
+                (app
+                  (term
+                    (identifier)))))))
+        (identifier)))
+    (identifier)))