diff options
Diffstat (limited to 'src/CC/Term/Raw.idr')
| -rw-r--r-- | src/CC/Term/Raw.idr | 16 |
1 files changed, 8 insertions, 8 deletions
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 |