Extract Terms and Values to a new module.

4 files changed, 61 insertions, 44 deletions

diff --git a/obs.ipkg b/obs.ipkg
index 2de477f..d2454d3 100644
--- a/obs.ipkg
+++ b/obs.ipkg
@@ -11,4 +11,5 @@ main = Main
 
 modules
   = CC.Name
+  , CC.Term
   , Main
diff --git a/src/CC/Name.idr b/src/CC/Name.idr
index f1a66db..4c25f5c 100644
--- a/src/CC/Name.idr
+++ b/src/CC/Name.idr
@@ -1,6 +1,6 @@
 module CC.Name
 
-import Control.Relation
+import public Control.Relation
 
 import Decidable.Equality
 
diff --git a/src/CC/Term.idr b/src/CC/Term.idr
new file mode 100644
index 0000000..2bae041
--- /dev/null
+++ b/src/CC/Term.idr
@@ -0,0 +1,58 @@
+module CC.Term
+
+import CC.Name
+
+-- Definition ------------------------------------------------------------------
+
+public export
+Context : Type
+Context = SnocList Name
+
+public export
+data IsVar : Nat -> Name -> Context -> Type where
+  Here : (eq : m ~~ n) -> IsVar 0 m (ctx :< n)
+  There : IsVar k n ctx -> IsVar (S k) n (ctx :< _)
+
+public export
+data Term : Context -> Type where
+  Var : (k : Nat) -> (0 n : Name) -> (0 prf : IsVar k n ctx) -> Term ctx
+  Abs : (n : Name) -> Term (ctx :< n) -> Term ctx
+  App : Term ctx -> Term ctx -> Term ctx
+  Let : (n : Name) -> Term ctx -> Term (ctx :< n) -> Term ctx
+
+public export
+data Value : Context -> Type
+public export
+data Neutral : Context -> Type
+public export
+data Closure : Context -> Type
+
+public export
+data Env : (local, global : Context) -> Type where
+  Lin  : Env [<] global
+  (:<) : Env local global -> (p : (Name, Lazy (Value global))) -> Env (local :< fst p) global
+
+data Closure : Context -> Type where
+  Close : (n : Name) -> Env local global -> Term (local :< n) -> Closure global
+
+data Value where
+  Ntrl : Neutral ctx -> Value ctx
+  VAbs : Closure ctx -> Value ctx
+
+data Neutral where
+  VVar : (k : Nat) -> (0 n : Name) -> (0 prf : IsVar k n ctx) -> Neutral ctx
+  VApp : Neutral ctx -> Lazy (Value ctx) -> Neutral ctx
+
+%name IsVar prf
+%name Term t, u
+%name Value v
+%name Neutral n
+%name Closure close
+%name Env env
+
+-- Operations ------------------------------------------------------------------
+
+export
+index : Env local global -> (k : Nat) -> (0 prf : IsVar k n local) -> Value global
+index (env :< (n, v)) 0 (Here eq) = v
+index (env :< _) (S k) (There prf) = index env k prf
diff --git a/src/Main.idr b/src/Main.idr
index 9f4caf8..6a5fe1b 100644
--- a/src/Main.idr
+++ b/src/Main.idr
@@ -1,6 +1,7 @@
 module Main
 
 import CC.Name
+import CC.Term
 
 import Data.DPair
 import Data.List
@@ -19,51 +20,8 @@ import Text.Parser
 import Text.PrettyPrint.Prettyprinter
 import Text.PrettyPrint.Prettyprinter.Render.Terminal
 
-Context : Type
-Context = SnocList Name
-
-data IsVar : Nat -> Name -> Context -> Type where
-  Here : (eq : m ~~ n) -> IsVar 0 m (ctx :< n)
-  There : IsVar k n ctx -> IsVar (S k) n (ctx :< _)
-
-data Term : Context -> Type where
-  Var : (k : Nat) -> (0 n : Name) -> (0 prf : IsVar k n ctx) -> Term ctx
-  Abs : (n : Name) -> Term (ctx :< n) -> Term ctx
-  App : Term ctx -> Term ctx -> Term ctx
-  Let : (n : Name) -> Term ctx -> Term (ctx :< n) -> Term ctx
-
-data Value : Context -> Type
-data Neutral : Context -> Type
-data Closure : Context -> Type
-
-data Env : (local, global : Context) -> Type where
-  Lin  : Env [<] global
-  (:<) : Env local global -> (p : (Name, Lazy (Value global))) -> Env (local :< fst p) global
-
-data Closure : Context -> Type where
-  Close : (n : Name) -> Env local global -> Term (local :< n) -> Closure global
-
-data Value where
-  Ntrl : Neutral ctx -> Value ctx
-  VAbs : Closure ctx -> Value ctx
-
-data Neutral where
-  VVar : (k : Nat) -> (0 n : Name) -> (0 prf : IsVar k n ctx) -> Neutral ctx
-  VApp : Neutral ctx -> Lazy (Value ctx) -> Neutral ctx
-
-%name IsVar prf
-%name Term t, u
-%name Value v
-%name Neutral n
-%name Closure close
-%name Env env
-
 --------------------------------------------------------------------------------
 
-index : Env local global -> (k : Nat) -> (0 prf : IsVar k n local) -> Value global
-index (env :< (n, v)) 0 (Here eq) = v
-index (env :< _) (S k) (There prf) = index env k prf
-
 app : Closure ctx -> Lazy (Value ctx) -> Value ctx
 eval : Env local global -> Term local -> Value global