From bd8cb07309aa551c47762e0ead1eb28f09f33399 Mon Sep 17 00:00:00 2001
From: depsterr <depsterr@protonmail.com>
Date: Wed, 8 Jun 2022 15:11:55 +0200
Subject: [PATCH] additional work on inductives, code compiles, inductives
 unusable

---
 TODO.md           |  4 +---
 src/Check.idr     |  8 ++++----
 src/Convert.idr   |  2 +-
 src/Inductive.idr | 23 +++++++++++++++++++++++
 src/Normalize.idr |  8 ++++----
 src/Term.idr      | 19 -------------------
 src/Tests.idr     | 27 ++++++++++++++++-----------
 src/Value.idr     | 18 +++++++++---------
 8 files changed, 58 insertions(+), 51 deletions(-)
 create mode 100644 src/Inductive.idr

diff --git a/TODO.md b/TODO.md
index 606b94f..03a188e 100644
--- a/TODO.md
+++ b/TODO.md
@@ -1,5 +1,3 @@
 # Inductives
 
-figure out model for terms, current one is nice but makes values incredibly inconvenient.
-
-Update rest of code to fit new terms, or remodel terms again with a global environment of inductive definitions, rather than introducing them in the terms. With this one could also index values by this inductive environment.
+ * Add support for them in type checking, conversion, etc
diff --git a/src/Check.idr b/src/Check.idr
index f2df073..86f14f7 100644
--- a/src/Check.idr
+++ b/src/Check.idr
@@ -18,7 +18,7 @@ import Convert
 mutual
   public export
   -- terms types expected term
-  check : Ctx n -> Ctx n -> Value -> Term n -> PI Bool
+  check : Ctx n v -> Ctx n v -> Value v -> Term n v -> PI Bool
   check trs tys xpt' tr = do
     xpt <- whnf xpt'
     case tr of
@@ -40,8 +40,8 @@ mutual
       _       => convert xpt =<< infer trs tys tr
 
   -- terms types term
-  infer : Ctx n -> Ctx n -> Term n -> PI Value
-  infer trs tys (TVar i _) = pure (index (natToFinLT i) tys)
+  infer : Ctx n v -> Ctx n v -> Term n v -> PI (Value v)
+  infer trs tys (TVar i) = pure (index i tys)
   infer trs tys TType      = pure VType
   infer trs tys (TApp f x) = infer trs tys f >>= whnf >>=
                               \case
@@ -54,6 +54,6 @@ mutual
   infer trs tys _          = oops "cannot infer type"
 
 public export
-typecheck : Term 0 -> Term 0 -> Either String (Bool, List String)
+typecheck : Term 0 [] -> Term 0 [] -> Either String (Bool, List String)
 typecheck tr ty = resolve $ (&&) <$> check [] [] VType ty 
                                  <*> delay <$> check [] [] (VClos [] ty) tr
diff --git a/src/Convert.idr b/src/Convert.idr
index 6946278..0293244 100644
--- a/src/Convert.idr
+++ b/src/Convert.idr
@@ -15,7 +15,7 @@ import Data.Vect
 %default total
 
 public export
-convert : Value -> Value -> PI Bool
+convert : Value v -> Value v -> PI Bool
 convert u1 u2 = do
   u1' <- whnf u1
   u2' <- whnf u2
diff --git a/src/Inductive.idr b/src/Inductive.idr
new file mode 100644
index 0000000..69d2fc0
--- /dev/null
+++ b/src/Inductive.idr
@@ -0,0 +1,23 @@
+module Inductive
+
+import Data.Vect
+
+import Term
+
+{-
+  The type of a constructor, indexed like terms
+-}
+public export
+data Constructor : (ctx : Index) -> (tags : Vect n Nat) -> Type where
+  Tr   : Term n v      -> Constructor n v                          -- a term
+  Sum  : Constructor n v -> Constructor (S n) v -> Constructor n v -- Σ _ : #0 , #1
+
+
+{-
+  The type of an inductive definition. It is a vector of constructors.
+'s indexed by the number of constructors as well as the indecies for terms.
+-}
+public export
+Inductive : Nat -> Index -> Vect n Nat -> Type
+Inductive cons ctx tags = Vect cons (Constructor ctx (cons :: tags))
+
diff --git a/src/Normalize.idr b/src/Normalize.idr
index 273c37f..90b7486 100644
--- a/src/Normalize.idr
+++ b/src/Normalize.idr
@@ -15,13 +15,13 @@ import Data.Vect
 
 mutual
   public export
-  app : Value -> Value -> PI Value
+  app : Value v -> Value v -> PI (Value v)
   app (VClos env (TLam sc)) x = eval (x :: env) sc
   app f                     x = pure (VApp f x)
 
   public export
-  eval : Ctx n -> Term n -> PI Value
-  eval env (TVar i _) = pure (index (natToFinLT i) env)
+  eval : Ctx n v -> Term n v -> PI (Value v)
+  eval env (TVar i)   = pure (index i env)
   eval env (TApp f x) = do
     f' <- eval env f
     x' <- eval env x
@@ -30,7 +30,7 @@ mutual
   eval env tr         = pure (VClos env tr)
 
 public export
-whnf : Value -> PI Value
+whnf : Value v -> PI (Value v)
 whnf (VApp f x) = do
   f' <- whnf f
   x' <- whnf x
diff --git a/src/Term.idr b/src/Term.idr
index 4bb3715..2a58e52 100644
--- a/src/Term.idr
+++ b/src/Term.idr
@@ -28,29 +28,11 @@ mutual
     TApp   : Term n v -> Term n v -> Term n v                 -- Appliction
     TVar   : Fin n -> Term n v                                -- Variable
     TLet   : Term n v -> Term n v -> Term (S n) v -> Term n v -- Let        (let _ = #1 : #0 in #2)
-    TIDef  : Inductive m n v -> Term n (m :: v) -> Term n v   -- Inductive definition
     TIType : Fin (len v) -> Term n v                          -- Inductive type
     TIElim : Fin (len v) -> Term n v                          -- Inductive eliminator
     TICons : (n : Fin (len v)) -> Fin (index n v) -> Term m v -- Inductive constructor
 
 
-  {-
-    The type of a constructor, indexed like terms
-  -}
-  public export
-  data Constructor : (ctx : Index) -> (tags : Vect n Nat) -> Type where
-    Tr   : Term n v      -> Constructor n v                          -- a term
-    Sum  : Constructor n v -> Constructor (S n) v -> Constructor n v -- Σ _ : #0 , #1
-
-
-  {-
-    The type of an inductive definition. It is a vector of constructors.
-It's indexed by the number of constructors as well as the indecies for terms.
-  -}
-  public export
-  Inductive : Nat -> Index -> Vect n Nat -> Type
-  Inductive cons ctx tags = Vect cons (Constructor ctx (cons :: tags))
-
 {-
    Use some different brackets to make it easier to read
 -}
@@ -62,7 +44,6 @@ Show (Term n v) where
   show (TApp f x) = "App (" ++ show f ++ ") (" ++ show x ++ ")"
   show (TVar i) = "Var " ++ show i
   show (TLet tr ty sc) = "Let <" ++ show tr ++ "> : <" ++ show ty ++ "> in <" ++ show sc ++ ">"
-  show (TIDef _ t) = "IDef [...] in " ++ show t
   show (TIType n) = "IType[#" ++ show n ++ "]"
   show (TIElim n) = "IElim[#" ++ show n ++ "]"
   show (TICons n m) = "ICons[#" ++ show n ++ "][#" ++ show m ++ "]"
diff --git a/src/Tests.idr b/src/Tests.idr
index 5f86d09..f052676 100644
--- a/src/Tests.idr
+++ b/src/Tests.idr
@@ -12,31 +12,36 @@ import Control.Monad.Identity
 import Control.Monad.Either
 
 import Data.Nat
+import Data.Fin
+import Data.Vect
 
 %default total
 
-a : {p, q : Nat} -> lt p q = True -> LT p q
-a {p} {q} eq = ltReflectsLT p q eq
-
 {- λA. λx. x : ∏ (A : Type) → A → A -}
 test_id : Either String (Bool, List String)
-test_id = typecheck (TLam (TLam (TVar 0 (a Refl))))
-                    (TPi TType (TPi (TVar 0 (a Refl)) (TVar 1 (a Refl))))
+test_id = typecheck (TLam (TLam (TVar 0)))
+                    (TPi TType (TPi (TVar 0) (TVar 1)))
 
 {- λA. λB. λf. λx. f x : ∏ (A : Type) ∏ (B : A → Type) ∏ (f : ∏ (x : A) B x) ∏ (x : A) B x -}
 test_app : Either String (Bool, List String)
-test_app = typecheck (TLam (TLam (TLam (TLam (TApp (TVar 1 (a Refl)) (TVar 0 (a Refl)))))))
+test_app = typecheck (TLam (TLam (TLam (TLam (TApp (TVar 1) (TVar 0))))))
                      (TPi TType 
-                          (TPi (TPi (TVar 0 (a Refl)) TType)
-                               (TPi (TPi (TVar 1 (a Refl)) (TApp (TVar 1 (a Refl)) (TVar 0 (a Refl)))) 
-                                    (TPi (TVar 2 (a Refl)) (TApp (TVar 2 (a Refl)) (TVar 0 (a Refl)))))))
+                          (TPi (TPi (TVar 0) TType)
+                               (TPi (TPi (TVar 1) (TApp (TVar 1) (TVar 0))) 
+                                    (TPi (TVar 2) (TApp (TVar 2) (TVar 0))))))
 
 {- λf. λx. f x ≃ λf. λx. (λy. f y) x -}
 eta_test : Either String (Bool, List String)
 eta_test = resolve action
   where
+    term1 : Term 0 []
+    term1 = TLam (TLam (TApp (TVar 1) (TVar 0)))
+
+    term2 : Term 0 []
+    term2 = TLam (TLam (TApp (TLam (TApp (TVar 2) (TVar 0))) (TVar 0)))
+
     action : PI Bool
     action = do
-      x <- eval ctx0 (TLam (TLam (TApp (TVar 1 (a Refl)) (TVar 0 (a Refl)))))
-      y <- eval ctx0 (TLam (TLam (TApp (TLam (TApp (TVar 2 (a Refl)) (TVar 0 (a Refl)))) (TVar 0 (a Refl)))))
+      x <- eval ctx0 term1
+      y <- eval ctx0 term2 
       convert x y
diff --git a/src/Value.idr b/src/Value.idr
index 4364773..80c717f 100644
--- a/src/Value.idr
+++ b/src/Value.idr
@@ -9,22 +9,22 @@ import Data.Vect
 
 mutual
   public export
-  data Value : Type where
-    VType : Value
-    VGen  : Nat   -> Value
-    VApp  : Value -> Value  -> Value
-    VClos : Ctx n -> Term n -> Value
+  data Value : (tags : Vect n Nat) -> Type where
+    VType : Value v
+    VGen  : Nat     -> Value v
+    VApp  : Value v -> Value v  -> Value v
+    VClos : Ctx n v -> Term n v -> Value v
 
   public export
-  Ctx : Index -> Type
-  Ctx i = Vect i Value
+  Ctx : Index -> Vect n Nat -> Type
+  Ctx i v = Vect i (Value v)
 
 public export
-ctx0 : Ctx 0
+ctx0 : Ctx 0 v
 ctx0 = []
 
 public export
-Show Value where
+Show (Value v) where
   show VType       = "VType"
   show (VGen i)    = "VGen " ++ show i
   show (VApp f x)  = "VApp (" ++ show f ++ ") (" ++ show x ++ ")"