identity types !

removed values that should not be
improved eliminator computation
improved conversion

makefile

@@ -4,4 +4,4 @@ all:
 run:
 	./build/exec/pi
 test:
-	for file in ./tests/*; do ./build/exec/pi $$file; done
+	@for file in ./tests/*.pi; do ./build/exec/pi $$file; done

src/Core/Check.idr

@@ -36,21 +36,6 @@ mutual
                            check (v :: trs) !(extT tys env a) (VClos (v :: env) b) sc
                          _ => oops "expected pi"
 
-      -- pi and sigma could be inferred /shrug
-      TPi a b    => case xpt of
-                         VType => do
-                           v <- VGen <$> fresh
-                           guardS "Pi a" =<< check trs tys VType a 
-                           check (v :: trs) !(extT tys trs a) VType b
-                         _ => oops "expected type"
-
-      TSigma a b => case xpt of
-                         VType => do
-                           v <- VGen <$> fresh
-                           guardS "Σ a" =<< check trs tys VType a 
-                           check trs tys (VClos trs (TPi a TType)) b
-                         _ => oops "expected type"
-
       TPair  x y => case xpt of
                          (VClos env (TSigma a b)) => do
                            guardS "Pair a" =<< check trs tys (VClos env a) x
@@ -75,24 +60,61 @@ mutual
   infer trs tys (TApp f x) = infer trs tys f >>= whnf >>=
                               \case
                                  VClos env (TPi a b) => do
-                                   guardS "app x" =<< check trs tys (VClos env a) x
+                                   guardS ("app x:\n" ++ show !(whnf (VClos env a))) =<< check trs tys (VClos env a) x
                                    tr <- whnf (VClos trs x)
                                    pure (VClos (tr :: env) b)
 
                                  _ => oops "expected infer pi"
 
+  infer trs tys (TPi a b) = do
+    v <- VGen <$> fresh
+    guardS "Pi a" =<< check trs tys VType a 
+    guardS "Pi b" =<< check (v :: trs) !(extT tys trs a) VType b
+    pure VType
+
+  infer trs tys (TSigma a b) = do
+    guardS "Σ a" =<< check trs tys VType a
+    guardS "Σ b" =<< check trs tys (VClos trs (TPi a TType)) b
+    pure VType
+
+  infer trs tys (TId ty a b) = do
+    guardS "Id ty" =<< check trs tys VType ty
+    guardS "Id a"  =<< check trs tys (VClos trs ty) a
+    guardS "Id b"  =<< check trs tys (VClos trs ty) b
+    pure VType
+
   infer trs tys (TSuc n)  = do 
     guardS "suc n" =<< check trs tys VNat n
     pure VNat
 
+  infer trs tys (TRefl ty tr) = do
+    guardS "Refl ty" =<< check trs tys VType ty
+    guardS "Refl tr" =<< check trs tys (VClos trs ty) tr
+    pure (VClos trs (TId ty tr tr))
+
   infer trs tys (TNatInd c z s) = do
     guardS "ℕ C" =<< check trs tys (VClos trs (TPi TNat TType)) c
-    guardS "ℕ z" =<< check trs tys (VApp (VClos trs c) (VNatTr 0)) z
+    guardS "ℕ z" =<< check trs tys (VApp (VClos trs c) (VClos [] TZero)) z
     guardS "ℕ s" =<< check trs tys (VClos trs (TPi TNat 
                                               (TPi (TApp (weakTr c) (TVar 0)) 
                                                    (TApp (weakTr2 c) (TSuc (TVar (FS FZ))))))) s
     pure (VClos trs (TPi TNat (TApp (weakTr c) (TVar 0))))
 
+  infer trs tys (TJ ty a b c d) = do
+    guardS "J ty" =<< check trs tys VType ty
+    guardS "J a"  =<< check trs tys (VClos trs ty) a
+    guardS "J b"  =<< check trs tys (VClos trs ty) b
+    guardS "J c"  =<< check trs tys
+                            (VClos trs (TPi ty {- a : A -}
+                                            (TPi (weakTr ty) {- b : A -}
+                                                 (TPi (TId (weakTr2 ty)
+                                                           (TVar (FS FZ))
+                                                           (TVar FZ)) {- Id A a b -}
+                                                      TType)))) c
+    guardS "J d"  =<< check trs tys (VClos trs (c `TApp` a `TApp` a `TApp` TRefl ty a)) d
+    pure (VClos trs (TPi (TId ty a b) (weakTr c `TApp` weakTr a `TApp` weakTr b `TApp` TVar 0)))
+                                                                 
+
   infer trs tys (TSigInd a b c f) = do
     guardS "Σ A" =<< check trs tys VType a
     guardS "Σ B" =<< check trs tys (VClos trs (TPi a TType)) b
@@ -116,7 +138,7 @@ mutual
     guardS "⊥ C" =<< check trs tys (VClos trs (TPi TBot TType)) c
     pure (VClos trs (TPi TBot (TApp (weakTr c) (TVar 0))))
 
-  infer trs tys x          = oops ("cannot infer type" ++ show x)
+  infer trs tys x          = oops ("cannot infer type " ++ show x)
 
 public export
 typecheck : Term 0 -> Term 0 -> Either String (Bool, List String)

src/Core/Convert.idr

@@ -30,7 +30,6 @@ convert u1 u2 = do
       (VNat, VNat)   => pure True
 
       (VGen k1, VGen k2) => pure (k1 == k2)
-      (VNatTr n, VNatTr m) => pure (n == m)
 
       (VApp f1 x1, VApp f2 x2) => (&&) <$> convert f1 f2 <*> delay <$> convert x1 x2
 
@@ -43,18 +42,39 @@ convert u1 u2 = do
         guardS (show a1 ++ " | " ++ show a2) =<< convert (VClos env1 a1) (VClos env2 a2)
         convert (VClos (v :: env1) b1) (VClos (v :: env2) b2)
 
-      (VPair a1 b1, VPair a2 b2) => (&&) <$> convert a1 a2 <*> delay <$> convert b1 b2
+      (VClos env1 (TSigma a1 b1), VClos env2 (TSigma a2 b2)) => do
+        termGuard env1 env2 a1 a2
+        termConv  env1 env2 b1 b2
 
-      (VClos env1 (TBotInd c1), VClos env2 (TBotInd c2)) => termConv env1 env2 c1 c2
+      (VClos env1 (TPair a1 b1), VClos env2 (TPair a2 b2)) => do
+        termGuard env1 env2 a1 a2
+        termConv  env1 env2 b1 b2
+
+      (VClos env1 (TId ty1 a1 b1), VClos env2 (TId ty2 a2 b2)) => do
+        termGuard env1 env2 ty1 ty2
+        termGuard env1 env2 a1 a2
+        termConv  env1 env2 b1 b2
+        
+      (VClos env1 (TRefl ty1 tr1), VClos env2 (TRefl ty2 tr2)) => do
+        termGuard env1 env2 ty1 ty2
+        termConv  env1 env2 tr1 tr2
 
       (VClos env1 (TNatInd c1 z1 s1), VClos env2 (TNatInd c2 z2 s2)) => do
         termGuard env1 env2 c1 c2
         termGuard env1 env2 z1 z2
         termConv  env1 env2 s1 s2
 
-      (VClos env1 (TSigma a1 b1), VClos env2 (TSigma a2 b2)) => do
+      (VClos _ TZero, VClos _ TZero) => pure True
+
+      (VClos env1 (TSuc n1), VClos env2 (TSuc n2)) => do
+        termConv env1 env2 n1 n2
+
+      (VClos env1 (TJ ty1 a1 b1 c1 d1), VClos env2 (TJ ty2 a2 b2 c2 d2)) => do
+        termGuard env1 env2 ty1 ty2
         termGuard env1 env2 a1  a2
-        termConv  env1 env2 b1 b2
+        termGuard env1 env2 b1  b2
+        termGuard env1 env2 c1  c2
+        termConv  env1 env2 d1  d2
 
       (VClos env1 (TSigInd a1 b1 c1 f1), VClos env2 (TSigInd a2 b2 c2 f2)) => do
         termGuard env1 env2 a1 a2
@@ -62,6 +82,12 @@ convert u1 u2 = do
         termGuard env1 env2 c1 c2
         termConv  env1 env2 f1 f2
 
+      (VClos env1 (TBotInd c1), VClos env2 (TBotInd c2)) => termConv env1 env2 c1 c2
+
+      (VClos env1 (TTopInd c1 st1), VClos env2 (TTopInd c2 st2)) => do
+        termGuard env1 env2 c1 c2
+        termConv  env1 env2 st1 st2
+
       -- η rules
       -- fresh cannot appear in vsc, so this is fine
       (vsc, VClos env (TLam (TApp sc (TVar 0)))) => do
@@ -71,12 +97,11 @@ convert u1 u2 = do
         v <- VGen <$> fresh
         convert vsc (VClos (v :: env) sc)
 
-      (VClos env1 (TTopInd c1 st1), VClos env2 (TTopInd c2 st2)) => do
+      -- VApp
-        termGuard env1 env2 c1 c2
+      --     (VApp v1 v2 , VClos env (TApp t1 t2)) => (&&) <$> convert v1 (VClos env t1) <*> delay <$> convert v1 (VClos env t1)
-        termConv  env1 env2 st1 st2
+      --  (VClos env (TApp t1 t2), VApp v1 v2) => (&&) <$> convert v1 (VClos env t1) <*> delay <$> convert v1 (VClos env t1)
 
-
+      (v1, v2) => oops ("cannot convert \n" ++ show v1 ++ "\n\n" ++ show v2)
-      _ => pure False
   where
     termConv : Ctx n -> Ctx m -> Term n -> Term m -> PI Bool
     termConv env1 env2 a1 a2 = do

src/Core/Normalize.idr

@@ -19,31 +19,19 @@ mutual
   app (VClos env (TLam sc))       x = eval (x :: env) sc
 
   app (VClos env (TTopInd c st)) VTop = eval env st
-  app f@(VClos env (TTopInd c st))  x = logS ("⊤-ind applied to " ++ show x)
-                                               >> pure (VApp f x)
 
-  app (VClos env (TNatInd _ z s)) (VNatTr n) = do
+  app (VClos env1 (TNatInd _ z s)) (VClos env2 TZero)      = eval env1 z
-    z'  <- eval env z
+  app f@(VClos env1 (TNatInd _ z s)) (VClos env2 (TSuc n)) = assert_total $ do
-    s'  <- eval env s
+    s' <- eval env1 s
-    assert_total (nind z' s' n) -- :(
+    sn <- app (VClos env1 s) (VClos env2 n)
-    where
+    app sn =<< app f (VClos env2 n)
-      nind : Value -> Value -> Nat -> PI Value
-      nind z s 0     = pure z
-      nind z s (S n) = do
-        rec <- nind z s n
-        sn <- app s (VNatTr n)
-        app sn rec
 
-  app f@(VClos env (TNatInd _ z s)) x = logS ("ℕ-ind applied to " ++ show x)
+  app (VClos env1 (TSigInd _ _ c f)) (VClos env2 (TPair a b)) = assert_total $ do
-                                        >> pure (VApp f x)
+    f' <- eval env1 f
+    fa <- app f' (VClos env2 a)
+    app fa (VClos env2 b)
 
-  app (VClos env (TSigInd _ _ c f)) (VPair a b) = do
+  app (VClos env (TJ _ _ _ _ d)) (VClos _ (TRefl _ _)) = eval env d
-    f' <- eval env f
-    fa <- app f' a
-    app fa b
-
-  app f@(VClos env (TSigInd _ _ c p)) x = logS ("Σ-ind applied to " ++ show x)
-                                          >> pure (VApp f x)
 
   app f x = pure (VApp f x)
 
@@ -55,39 +43,22 @@ mutual
   eval env TStar       = pure VStar
   eval env TBot        = pure VBot
   eval env TNat        = pure VNat
-  eval env TZero       = pure (VNatTr 0)
   eval env (TApp f x)  = do
     f' <- eval env f
     x' <- eval env x
     assert_total (app f' x') -- :(
 
-  eval env (TSuc n)    = do
-    n' <- eval env n
-    case n' of
-         VNatTr n => pure (VNatTr (S n))
-         x        => logS ("suc applied to " ++ show x)
-                     >> pure (VClos env (TSuc n))
-
-  eval env (TPair a b) = do
-    a' <- eval env a
-    b' <- eval env b
-    pure (VPair a' b')
-
   eval env (TLet ty tr tri) = do
     tr' <- eval env tr
     eval (tr' :: env) tri
 
   eval env tr         = pure (VClos env tr)
 
-public export
+  public export
-whnf : Value -> PI Value
+  whnf : Value -> PI Value
-whnf (VClos env tr) = eval env tr
+  whnf (VClos env tr) = eval env tr
-whnf (VApp f x) = do
+  whnf (VApp f x) = do
     f' <- whnf f
     x' <- whnf x
     app f' x'
-whnf (VPair a b) = do
+  whnf v              = pure v
-  a' <- whnf a
-  b' <- whnf b
-  pure (VPair a' b')
-whnf v              = pure v

src/Core/Term.idr

@@ -30,6 +30,10 @@ data Term : (_ : Index) -> Type where
   TPair   : Term n -> Term n -> Term n                     -- Sum constructor _,_
   TSigInd : Term n -> Term n -> Term n -> Term n -> Term n -- A B C f : (x : Σ _ : A , B _) → C x
 
+  TId     : Term n -> Term n -> Term n -> Term n                     -- Id Type (Id A x y)
+  TRefl   : Term n -> Term n -> Term n                               -- Refl A x
+  TJ      : Term n -> Term n -> Term n -> Term n -> Term n -> Term n -- A a b C d : (p : Id A a b) → C p
+
   TLet    : Term n -> Term n -> Term (S n) -> Term n       -- let _ : #0 := #1 in #2
 
   TLam    : Term (S n) -> Term n                 -- Lambda abstraction (λ _ . Scope)
@@ -59,6 +63,12 @@ Show (Term n) where
   show (TSigma a b)    = "Σ (" ++ show a ++ ") (" ++ show b ++ ")"
   show (TPair a b)     = "Pair (" ++ show a ++ ") (" ++ show b ++ ")"
   show (TSigInd a b c f) = "Σ-ind (" ++ show a ++ ") (" ++ show b ++ ") (" ++ show c ++ ") (" ++ show f ++ ")"
+
+  show (TId ty x y)  = "Id (" ++ show ty ++ ") (" ++ show x ++ ") (" ++ show y ++ ")"
+  show (TRefl ty tr) = "Refl (" ++ show ty ++ ") (" ++ show tr ++ ")"
+  show (TJ ty a b c d) = "J (" ++ show ty ++ ") (" ++ show a ++ ") (" ++ show b ++ ") (" 
+                            ++ show c ++ ") (" ++ show d ++ ")"
+
   show (TLet ty tr itr) = "let : (" ++ show ty ++ ") := (" ++ show tr ++ ") in (" ++ show itr ++ ")"
 
   show (TLam sc)       = "λ (" ++ show sc ++ ")"
@@ -85,6 +95,9 @@ weakTr = go 0
     go n (TSigma a b)      = TSigma (go n a) (go n b)
     go n (TPair a b)       = TPair (go n a) (go n b)
     go n (TSigInd a b c f) = TSigInd (go n a) (go n b) (go n c) (go n f)
+    go n (TId ty a b)      = TId (go n ty) (go n a) (go n b)
+    go n (TRefl ty tr)     = TRefl (go n ty) (go n tr)
+    go n (TJ ty a b c d)   = TJ (go n ty) (go n a) (go n b) (go n c) (go n d)
     go n (TLet ty tr itr)  = TLet (go n ty) (go n tr) (go (FS n) itr)
     go n (TLam sc)         = TLam (go (FS n) sc)
     go n (TPi  ty sc)      = TPi (go n ty) (go (FS n) sc)

src/Core/Value.idr

@@ -18,9 +18,6 @@ mutual
     VBot   : Value
 
     VNat   : Value
-    VNatTr : Nat -> Value
-
-    VPair  : Value -> Value -> Value
 
     VGen   : Nat   -> Value
     VApp   : Value -> Value  -> Value
@@ -43,8 +40,6 @@ Show Value where
   show VStar         = "VStar"
   show VBot          = "VBot"
   show VNat          = "VNat"
-  show (VPair a b) = "VPair (" ++ show a ++ ") (" ++ show b ++ ")"
-  show (VNatTr n)  = "V" ++ show n
   show (VGen i)      = "VGen " ++ show i
   show (VApp f x)    = "VApp (" ++ show f ++ ") (" ++ show x ++ ")"
   show (VClos e t)   = "VClos (" ++ assert_total (show e) ++ ") (" ++ show t ++ ")"

src/Main.idr

@@ -36,9 +36,9 @@ repl n env = do
 main : IO ()
 main = getArgs >>= \case
           (_ :: x :: _) => do
+            putStr (x ++ ": ")
             res <- readFile x >>= unwrap >>= unwrap . parsetoplevel
                               >>= unwrap . (`typecheck` TTop)
-            putStr (x ++ ": ")
             if fst res
                then putStrLn ("Success !")
                else unwrap   (Left res)

src/Parser/Parse.idr

@@ -41,6 +41,9 @@ data PiTokenKind
   | PTSuc
   | PTNatInd
   | PTSigInd
+  | PTId
+  | PTRefl
+  | PTJ
 
 Eq PiTokenKind where
   (==) PTLambda     PTLambda     = True
@@ -68,6 +71,9 @@ Eq PiTokenKind where
   (==) PTSuc        PTSuc        = True
   (==) PTNatInd     PTNatInd     = True
   (==) PTSigInd     PTSigInd     = True
+  (==) PTId         PTId         = True
+  (==) PTRefl       PTRefl       = True
+  (==) PTJ          PTJ          = True
   (==) _            _            = False
 
 Show PiTokenKind where
@@ -96,6 +102,9 @@ Show PiTokenKind where
   show PTSuc        = "PTSuc"
   show PTNatInd     = "PTNatInd"
   show PTSigInd     = "PTSigInd"
+  show PTId         = "PTId"
+  show PTRefl       = "PTRefl"
+  show PTJ          = "PTJ"
 
 PiToken : Type
 PiToken = Token PiTokenKind
@@ -132,6 +141,9 @@ TokenKind PiTokenKind where
   tokValue PTSuc        _ = ()
   tokValue PTNatInd     _ = ()
   tokValue PTSigInd     _ = ()
+  tokValue PTId         _ = ()
+  tokValue PTRefl       _ = ()
+  tokValue PTJ          _ = ()
 
 ignored : WithBounds PiToken -> Bool
 ignored (MkBounded (Tok PTIgnore _) _ _) = True
@@ -145,7 +157,10 @@ keywords = [
   ("in",    PTIn),
   ("let",   PTLet),
   ("suc",   PTSuc),
-  ("Type",  PTType)
+  ("Type",  PTType),
+  ("J",     PTJ),
+  ("Id",    PTId),
+  ("refl",  PTRefl)
 ]
 
 tokenmap : List (Lexer, PiTokenKind)
@@ -204,6 +219,9 @@ mutual
             <|> tsuc n env
             <|> tnatind n env
             <|> tsigind n env
+            <|> tid n env
+            <|> trefl n env
+            <|> tj n env
             <|> (do
               t <- term n env
               tapp n env t <|> pure t)
@@ -258,8 +276,7 @@ mutual
   tsuc n env = do
     match PTSuc
     commit
-    m <- term n env
+    TSuc <$> term n env
-    pure (TSuc m)
 
   tnatind : (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n)
   tnatind n env = do
@@ -302,6 +319,34 @@ mutual
     f <- term n env
     pure (TSigInd a b c f)
 
+  tid : (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n)
+  tid n env = do
+    match PTId
+    commit
+    ty <- term n env
+    a  <- term n env
+    b  <- term n env
+    pure (TId ty a b)
+
+  trefl : (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n)
+  trefl n env = do
+    match PTRefl
+    commit
+    ty <- term n env
+    tr <- term n env
+    pure (TRefl ty tr)
+
+  tj : (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n)
+  tj n env = do
+    match PTJ
+    commit
+    ty <- term n env
+    a  <- term n env
+    b  <- term n env
+    c  <- term n env
+    d  <- term n env
+    pure (TJ ty a b c d)
+
   tlet : (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n)
   tlet n env = do
     match PTLet
@@ -384,7 +429,7 @@ parsePi : (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n) -> List
 parsePi n env parseEntry toks =
   case parse parseEntry $ filter (not . ignored) toks of
     Right (l, []) => Right l
-    Right e => Left "contains tokens that were not consumed"
+    Right (_, l) => Left ("contains tokens that were not consumed: " ++ show l)
     Left e  => (Left . show . map getErr) e
   where
     getErr : ParsingError tok -> String

tests/nat-id.pi

@@ -0,0 +1,23 @@
+let sucf : ℕ → ℕ
+  ≔ λn. suc n
+
+let add : ℕ → ℕ → ℕ
+  ≔ ℕ-ind (λ_. ℕ → ℕ) (λn.n) (λn.λan.λm. suc (an m))
+
+let add_id_l : Π (n : ℕ) Id ℕ n (add 0 n)
+  ≔ λn. refl ℕ n
+
+let ap : Π (A : Type) Π (B : Type) Π (f : A → B)
+         Π (x : A) Π (y : A) Id A x y → Id B (f x) (f y)
+  ≔ λA.λB.λf.λx.λy. J A x y (λa.λb.λ_. Id B (f a) (f b)) (refl B (f x))
+
+let add_id_r : Π (n : ℕ) Id ℕ n (add n 0)
+  ≔ ℕ-ind (λn. Id ℕ n (add n 0))
+          (refl ℕ 0)
+          (λn.λp. ap ℕ ℕ sucf n (add n 0) p)
+
+let add_assoc : Π (n : ℕ) Π (m : ℕ) Π (p : ℕ)
+                Id ℕ (add (add n m) p) (add n (add m p))
+  ≔ ℕ-ind (λn. Π (m : ℕ) Π (p : ℕ) Id ℕ (add (add n m) p) (add n (add m p)))
+          (λm.λp. refl ℕ (add m p))
+          (λn.λpn.λm.λp. ap ℕ ℕ sucf (add (add n m) p) (add n (add m p)) (pn m p))