Clean-up raw term constructors and parser.

2 files changed, 17 insertions, 14 deletions

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
diff --git a/src/CC/Term/Raw.idr b/src/CC/Term/Raw.idr
index ab729ae..833daf5 100644
--- a/src/CC/Term/Raw.idr
+++ b/src/CC/Term/Raw.idr
@@ -10,10 +10,10 @@ import Data.List1
 
 public export
 data RawTerm : Type where
-  RVar : (n : Name) -> RawTerm
-  RAbs : (n : Name) -> RawTerm -> RawTerm
-  RApp : RawTerm -> RawTerm -> RawTerm
-  RLet : (n : Name) -> RawTerm -> RawTerm -> RawTerm
+  Var : (n : Name) -> RawTerm
+  Abs : (n : Name) -> RawTerm -> RawTerm
+  App : RawTerm -> RawTerm -> RawTerm
+  Let : (n : Name) -> RawTerm -> RawTerm -> RawTerm
 
 %name RawTerm t, u
 
@@ -55,7 +55,7 @@ lookup (ctx :< m) n =
 
 export
 translate : (ctx : Context) -> RawTerm -> NameError (Term ctx)
-translate ctx (RVar n) = (\p => Var p.fst n p.snd) <$> lookup ctx n
-translate ctx (RAbs n t) = pure (Abs n) <*> translate (ctx :< n) t
-translate ctx (RApp t u) = [| App (translate ctx t) (translate ctx u) |]
-translate ctx (RLet n t u) = pure (Let n) <*> translate ctx t <*> translate (ctx :< n) u
+translate ctx (Var n) = (\p => Var p.fst n p.snd) <$> lookup ctx n
+translate ctx (Abs n t) = pure (Abs n) <*> translate (ctx :< n) t
+translate ctx (App t u) = [| App (translate ctx t) (translate ctx u) |]
+translate ctx (Let n t u) = pure (Let n) <*> translate ctx t <*> translate (ctx :< n) u