Extract Terms and Values to a new module.

2 files changed, 59 insertions, 1 deletions

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