From 24604a93ef2a65809ba0ed5088ab1bdffb50cbb7 Mon Sep 17 00:00:00 2001 From: depsterr Date: Tue, 26 Jul 2022 06:09:57 +0200 Subject: [PATCH] identity types ! removed values that should not be improved eliminator computation improved conversion --- makefile | 2 +- src/Core/Check.idr | 68 ++++++++++++++++++++++++++++-------------- src/Core/Convert.idr | 47 ++++++++++++++++++++++------- src/Core/Normalize.idr | 65 +++++++++++----------------------------- src/Core/Term.idr | 13 ++++++++ src/Core/Value.idr | 21 +++++-------- src/Main.idr | 2 +- src/Parser/Parse.idr | 67 ++++++++++++++++++++++++++++++++++------- tests/nat-id.pi | 23 ++++++++++++++ 9 files changed, 201 insertions(+), 107 deletions(-) create mode 100644 tests/nat-id.pi diff --git a/makefile b/makefile index 41a516b..0b15bd4 100644 --- a/makefile +++ b/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 diff --git a/src/Core/Check.idr b/src/Core/Check.idr index 0683650..e4dd020 100644 --- a/src/Core/Check.idr +++ b/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 @@ -66,33 +51,70 @@ mutual -- terms types term infer : Ctx n -> Ctx n -> Term n -> PI Value infer trs tys TType = pure VType - infer trs tys TTop = pure VType - infer trs tys TBot = pure VType - infer trs tys TNat = pure VType - infer trs tys TStar = pure VTop - infer trs tys TZero = pure VNat + infer trs tys TTop = pure VType + infer trs tys TBot = pure VType + infer trs tys TNat = pure VType + infer trs tys TStar = pure VTop + infer trs tys TZero = pure VNat infer trs tys (TVar i) = pure (index i tys) 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) diff --git a/src/Core/Convert.idr b/src/Core/Convert.idr index 8c1efd9..0713d25 100644 --- a/src/Core/Convert.idr +++ b/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 - termGuard env1 env2 a1 a2 - termConv env1 env2 b1 b2 + (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 + 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 - termGuard env1 env2 c1 c2 - termConv env1 env2 st1 st2 + -- VApp + -- (VApp v1 v2 , VClos env (TApp t1 t2)) => (&&) <$> convert v1 (VClos env t1) <*> delay <$> convert v1 (VClos env t1) + -- (VClos env (TApp t1 t2), VApp v1 v2) => (&&) <$> convert v1 (VClos env t1) <*> delay <$> convert v1 (VClos env t1) - - _ => pure False + (v1, v2) => oops ("cannot convert \n" ++ show v1 ++ "\n\n" ++ show v2) where termConv : Ctx n -> Ctx m -> Term n -> Term m -> PI Bool termConv env1 env2 a1 a2 = do diff --git a/src/Core/Normalize.idr b/src/Core/Normalize.idr index aabc450..9066146 100644 --- a/src/Core/Normalize.idr +++ b/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 - z' <- eval env z - s' <- eval env s - assert_total (nind z' s' n) -- :( - where - 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 (VClos env1 (TNatInd _ z s)) (VClos env2 TZero) = eval env1 z + app f@(VClos env1 (TNatInd _ z s)) (VClos env2 (TSuc n)) = assert_total $ do + s' <- eval env1 s + sn <- app (VClos env1 s) (VClos env2 n) + app sn =<< app f (VClos env2 n) - app f@(VClos env (TNatInd _ z s)) x = logS ("ℕ-ind applied to " ++ show x) - >> pure (VApp f x) + app (VClos env1 (TSigInd _ _ c f)) (VClos env2 (TPair a b)) = assert_total $ do + 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 - 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 (VClos env (TJ _ _ _ _ d)) (VClos _ (TRefl _ _)) = eval env d 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 -whnf : Value -> PI Value -whnf (VClos env tr) = eval env tr -whnf (VApp f x) = do - f' <- whnf f - x' <- whnf x - app f' x' -whnf (VPair a b) = do - a' <- whnf a - b' <- whnf b - pure (VPair a' b') -whnf v = pure v + public export + whnf : Value -> PI Value + whnf (VClos env tr) = eval env tr + whnf (VApp f x) = do + f' <- whnf f + x' <- whnf x + app f' x' + whnf v = pure v diff --git a/src/Core/Term.idr b/src/Core/Term.idr index e74ee01..d5528fd 100644 --- a/src/Core/Term.idr +++ b/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) diff --git a/src/Core/Value.idr b/src/Core/Value.idr index 28f426d..f8b0f2e 100644 --- a/src/Core/Value.idr +++ b/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 @@ -38,13 +35,11 @@ ctx0 = [] public export Show Value where - show VType = "VType" - show VTop = "VTop" - 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 ++ ")" + show VType = "VType" + show VTop = "VTop" + show VStar = "VStar" + show VBot = "VBot" + show VNat = "VNat" + 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 ++ ")" diff --git a/src/Main.idr b/src/Main.idr index 4cd4f12..2d77fa4 100644 --- a/src/Main.idr +++ b/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) diff --git a/src/Parser/Parse.idr b/src/Parser/Parse.idr index 8e30466..72a38b5 100644 --- a/src/Parser/Parse.idr +++ b/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) @@ -200,13 +215,16 @@ mutual expr1 : (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n) expr1 n env = ttopind n env - <|> tbotind n env - <|> tsuc n env - <|> tnatind n env - <|> tsigind n env - <|> (do - t <- term n env - tapp n env t <|> pure t) + <|> tbotind n env + <|> 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) term : (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n) term n env = ttype @@ -258,8 +276,7 @@ mutual tsuc n env = do match PTSuc commit - m <- term n env - pure (TSuc m) + TSuc <$> term n env 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 diff --git a/tests/nat-id.pi b/tests/nat-id.pi new file mode 100644 index 0000000..d96c1f7 --- /dev/null +++ b/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))