2 files changed, 64 insertions, 47 deletions
diff --git a/src/CC/Term/Raw.idr b/src/CC/Term/Raw.idr
new file mode 100644
index 0000000..ab729ae
--- /dev/null
+++ b/src/CC/Term/Raw.idr
@@ -0,0 +1,61 @@
+module CC.Term.Raw
+
+import CC.Name
+import CC.Term
+
+import Data.DPair
+import Data.List1
+
+-- Definition ------------------------------------------------------------------
+
+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
+
+%name RawTerm t, u
+
+-- Error Type ------------------------------------------------------------------
+
+export
+data NameError : Type -> Type where
+  Ok : ty -> NameError ty
+  Err : List1 Name -> NameError ty
+
+export
+Functor NameError where
+  map f (Ok v) = Ok (f v)
+  map f (Err errs) = Err errs
+
+export
+Applicative NameError where
+  pure = Ok
+
+  Ok f <*> Ok v = Ok (f v)
+  Ok f <*> Err ys = Err ys
+  Err xs <*> Ok v = Err xs
+  Err xs <*> Err ys = Err (xs ++ ys)
+
+export
+runNameError : NameError ty -> Either (List1 Name) ty
+runNameError (Ok x) = Right x
+runNameError (Err xs) = Left xs
+
+-- Translation -----------------------------------------------------------------
+
+export
+lookup : (ctx : Context) -> (n : Name) -> NameError $ Subset Nat (\k => IsVar k n ctx)
+lookup [<] n = Err (n ::: [])
+lookup (ctx :< m) n =
+  case decEquiv n m of
+    Yes eq => Ok (Element 0 (Here eq))
+    No _ => map (\p => Element (S p.fst) (There p.snd)) (lookup ctx 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
diff --git a/src/Main.idr b/src/Main.idr
index 05208eb..8d69017 100644
--- a/src/Main.idr
+++ b/src/Main.idr
@@ -2,16 +2,11 @@ module Main
 
 import CC.Name
 import CC.Term
+import CC.Term.Raw
 import CC.Thinning
 
-import Data.DPair
-import Data.List
-import Data.Nat
-import Data.Singleton
 import Data.String
 
-import Decidable.Equality
-
 import System
 import System.File.ReadWrite
 import System.File.Virtual
@@ -56,45 +51,6 @@ normalise env t = quote $ eval env t
 
 --------------------------------------------------------------------------------
 
-data RawTerm : Type where
-  RVar : (n : Name) -> RawTerm
-  RAbs : (n : Name) -> RawTerm -> RawTerm
-  RApp : RawTerm -> RawTerm -> RawTerm
-  RLet : (n : Name) -> RawTerm -> RawTerm -> RawTerm
-
-%name RawTerm t, u
-
-data NameError : Type -> Type where
-  Ok : ty -> NameError ty
-  Err : List1 Name -> NameError ty
-
-Functor NameError where
-  map f (Ok v) = Ok (f v)
-  map f (Err errs) = Err errs
-
-Applicative NameError where
-  pure = Ok
-
-  Ok f <*> Ok v = Ok (f v)
-  Ok f <*> Err ys = Err ys
-  Err xs <*> Ok v = Err xs
-  Err xs <*> Err ys = Err (xs ++ ys)
-
-lookup : (ctx : Context) -> (n : Name) -> NameError $ Subset Nat (\k => IsVar k n ctx)
-lookup [<] n = Err (n ::: [])
-lookup (ctx :< m) n =
-  case decEquiv n m of
-    Yes eq => Ok (Element 0 (Here eq))
-    No _ => map (\p => Element (S p.fst) (There p.snd)) (lookup ctx n)
-
-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
-
---------------------------------------------------------------------------------
-
 putErrLn : HasIO io => String -> io ()
 putErrLn str = do
   Right () <- fPutStrLn stderr str
@@ -318,8 +274,8 @@ mainWith getOpt getTerm = do
     | [_, "--help"] => putStrLn helpMsg
     | _ => putErrLn helpMsg >> exitFailure
   rawTerm <- getTerm
-  let Ok term = translate [<] rawTerm
-    | Err errs => for_ errs putErr >> exitFailure
+  let Right term = runNameError $ translate [<] rawTerm
+    | Left errs => for_ errs putErr >> exitFailure
   let nf : Term [<] = normalise [<] term
   putDoc (pretty nf)
   where