Extract Terms and Values to a new module.

1 files changed, 1 insertions, 43 deletions

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