diff options
| author | Chloe Brown <chloe.brown.00@outlook.com> | 2023-03-25 17:13:16 +0000 |
|---|---|---|
| committer | Chloe Brown <chloe.brown.00@outlook.com> | 2023-03-25 17:13:16 +0000 |
| commit | 88ce0ee4ed72f75775da9c96668cad3e97554812 (patch) | |
| tree | 3215beb5d715cd4ab9be5128ccbbe6cdfed796fa /src/CC/Term/Raw.idr | |
| parent | 43463df9899d00f0f86c3b655b84a5d5ce75402d (diff) | |
Clean-up raw term constructors and parser.
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 |