From 88ce0ee4ed72f75775da9c96668cad3e97554812 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Sat, 25 Mar 2023 17:13:16 +0000
Subject: Clean-up raw term constructors and parser.

---
 src/CC/Term/Parse.idr | 15 +++++++++------
 1 file changed, 9 insertions(+), 6 deletions(-)

(limited to 'src/CC/Term/Parse.idr')

diff --git a/src/CC/Term/Parse.idr b/src/CC/Term/Parse.idr
index cef4f0e..3615956 100644
--- a/src/CC/Term/Parse.idr
+++ b/src/CC/Term/Parse.idr
@@ -94,6 +94,9 @@ tokenMap =
 parens : {b : Bool} -> Grammar state CCToken b ty -> Grammar state CCToken True ty
 parens p = match TPOpen >> commit >> p >>= (\t => match TPClose *> commit *> pure t)
 
+parseIdent : Grammar state CCToken True Name
+parseIdent = MkName <$> (bounds $ match TIdent)
+
 parseTerm : Grammar state CCToken True RawTerm
 parseLambda : Grammar state CCToken True RawTerm
 parseLet : Grammar state CCToken True RawTerm
@@ -105,17 +108,17 @@ parseTerm = parseLambda <|> parseLet <|> parseSpine
 parseLambda = do
   match TLambda
   commit
-  names <- sepBy1 (match TComma >> commit) (MkName <$> (bounds $ match TIdent))
+  names <- sepBy1 (match TComma >> commit) parseIdent
   commit
   match TFatArrow
   commit
   t <- parseTerm
-  pure $ foldr1By RAbs (flip RAbs t) names
+  pure $ foldr1By Abs (flip Abs t) names
 
 parseLet = do
   match TLet
   commit
-  n <- bounds $ match TIdent
+  n <- parseIdent
   commit
   match TDef
   commit
@@ -123,12 +126,12 @@ parseLet = do
   match TSemi
   commit
   u <- parseTerm
-  pure $ RLet (MkName n) t u
+  pure $ Let n t u
 
-parseSpine = foldl1 RApp <$> some parseAtom
+parseSpine = foldl1 App <$> some parseAtom
 
 parseAtom =
-  (RVar <$> MkName <$> (bounds $ match TIdent <* commit)) <|>
+  (Var <$> parseIdent <* commit) <|>
   (parens parseTerm)
 
 parseSrc : Grammar state CCToken True RawTerm
-- 
cgit v1.2.3