From 88ce0ee4ed72f75775da9c96668cad3e97554812 Mon Sep 17 00:00:00 2001 From: Chloe Brown Date: Sat, 25 Mar 2023 17:13:16 +0000 Subject: Clean-up raw term constructors and parser. --- src/CC/Term/Raw.idr | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) (limited to 'src/CC/Term/Raw.idr') 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 -- cgit v1.2.3