From 9275d39107e5b8956929b25819c43cabfc1b7329 Mon Sep 17 00:00:00 2001
From: depsterr <depsterr@protonmail.com>
Date: Mon, 1 Aug 2022 18:26:13 +0200
Subject: [PATCH] slight parser optimization

---
 src/Parser/Parse.idr | 18 ++++++++++++------
 1 file changed, 12 insertions(+), 6 deletions(-)

diff --git a/src/Parser/Parse.idr b/src/Parser/Parse.idr
index 8bb0e4a..fe68ca4 100644
--- a/src/Parser/Parse.idr
+++ b/src/Parser/Parse.idr
@@ -222,16 +222,23 @@ lexPi str =
 {- Basic idea, parsing has a list of the identifiers to convert to -}
 {- de bruijn indecies, and a Nat to keep track of context size -}
 mutual
+  -- has pi, sigma, and arrows, strongest binding
   expr : List String -> (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n)
   expr defs n env = tpi defs n env
                 <|> tsigma defs n env
                 <|> (do 
                   e <- expr1 defs n env
-                  tarr defs n env e <|> tapp defs n env e <|> pure e)
-
+                  tarr defs n env e <|> pure e)
 
+  -- handles application of expr2s (and terms)
   expr1 : List String -> (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n)
-  expr1 defs n env = ttopind defs n env
+  expr1 defs n env = do 
+                   e <- expr2 defs n env
+                   tapp defs n env e <|> pure e
+
+  -- anything which has an application in it (and induction principle) or a term
+  expr2 : List String -> (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n)
+  expr2 defs n env = ttopind defs n env
                  <|> tbotind defs n env
                  <|> tsuc defs n env
                  <|> tnatind defs n env
@@ -239,10 +246,9 @@ mutual
                  <|> tid defs n env
                  <|> trefl defs n env
                  <|> tj defs n env
-                 <|> (do
-                   t <- term defs n env
-                   tapp defs n env t <|> pure t)
+                 <|> term defs n env
 
+  -- terms, no application
   term : List String -> (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n)
   term defs n env = ttype
                 <|> ttop