From 7d2c3b5a8e4eb0c8d60aca13c300119051073e23 Mon Sep 17 00:00:00 2001 From: rhiannon morris Date: Sat, 11 Feb 2023 18:15:50 +0100 Subject: [PATCH] more typed equality, uip, etc --- lib/Quox/Equal.idr | 159 +++++++++++++++++++++--------------- lib/Quox/Typechecker.idr | 52 +++--------- lib/Quox/Typing.idr | 30 +++++++ tests/Tests.idr | 11 +-- tests/Tests/Equal.idr | 143 ++++++++++---------------------- tests/Tests/Typechecker.idr | 138 +++++++++++++++++++++++++++++++ tests/TypingImpls.idr | 61 ++++++++++++++ tests/quox-tests.ipkg | 4 +- 8 files changed, 381 insertions(+), 217 deletions(-) create mode 100644 tests/Tests/Typechecker.idr create mode 100644 tests/TypingImpls.idr diff --git a/lib/Quox/Equal.idr b/lib/Quox/Equal.idr index 852558d..a758de4 100644 --- a/lib/Quox/Equal.idr +++ b/lib/Quox/Equal.idr @@ -43,17 +43,31 @@ clashE e f = throwError $ ClashE !mode e f public export %inline -isType : (t : Term {}) -> Bool -isType (TYPE {}) = True -isType (Pi {}) = True -isType (Lam {}) = False -isType (Sig {}) = True -isType (Pair {}) = False -isType (Eq {}) = True -isType (DLam {}) = False -isType (E {}) = True -isType (CloT {}) = False -isType (DCloT {}) = False +isTyCon : (t : Term {}) -> Bool +isTyCon (TYPE {}) = True +isTyCon (Pi {}) = True +isTyCon (Lam {}) = False +isTyCon (Sig {}) = True +isTyCon (Pair {}) = False +isTyCon (Eq {}) = True +isTyCon (DLam {}) = False +isTyCon (E {}) = True +isTyCon (CloT {}) = False +isTyCon (DCloT {}) = False + +private +isSubSing : Term {} -> Bool +isSubSing ty = + let Element ty _ = pushSubsts ty in + case ty of + TYPE _ => False + Pi {res, _} => isSubSing res.term + Lam {} => False + Sig {fst, snd, _} => isSubSing fst && isSubSing snd.term + Pair {} => False + Eq {} => True + DLam {} => False + E e => False parameters {auto _ : HasErr q m} @@ -64,8 +78,8 @@ parameters {auto _ : HasErr q m} Right n => throwError $ e t export %inline - ensureType : (t : Term q d n) -> m (So (isType t)) - ensureType = ensure NotType isType + ensureType : (t : Term q d n) -> m (So (isTyCon t)) + ensureType = ensure NotType isTyCon parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)} mutual @@ -88,7 +102,7 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)} private covering compare0' : TContext q 0 n -> (ty, s, t : Term q 0 n) -> - (0 nty : NotRedex defs ty) => (0 tty : So (isType ty)) => + (0 nty : NotRedex defs ty) => (0 tty : So (isTyCon ty)) => (0 ns : NotRedex defs s) => (0 nt : NotRedex defs t) => m () compare0' ctx (TYPE _) s t = compareType ctx s t @@ -103,7 +117,7 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)} (Lam _ b1, Lam _ b2) => compare0 ctx' res.term b1.term b2.term (E e, Lam _ b) => eta e b (Lam _ b, E e) => eta e b - (E e, E f) => ignore $ compare0 ctx e f + (E e, E f) => compare0 ctx e f _ => throwError $ WrongType ty s t compare0' ctx ty@(Sig {fst, snd, _}) s t = local {mode := Equal} $ @@ -123,7 +137,7 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)} -- e.g. an abstract value in an abstract type, bound variables, … E e <- pure s | _ => throwError $ WrongType ty s t E f <- pure t | _ => throwError $ WrongType ty s t - ignore $ compare0 ctx e f + compare0 ctx e f export covering compareType : TContext q 0 n -> (s, t : Term q 0 n) -> m () @@ -136,8 +150,8 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)} private covering compareType' : TContext q 0 n -> (s, t : Term q 0 n) -> - (0 ns : NotRedex defs s) => (0 ts : So (isType s)) => - (0 nt : NotRedex defs t) => (0 tt : So (isType t)) => + (0 ns : NotRedex defs s) => (0 ts : So (isTyCon s)) => + (0 nt : NotRedex defs t) => (0 tt : So (isTyCon t)) => m () compareType' ctx s t = do let err : m () = clashT (TYPE UAny) s t @@ -170,80 +184,90 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)} E f <- pure t | _ => err -- no fanciness needed here cos anything other than a neutral -- has been inlined by whnfD - ignore $ compare0 ctx e f + compare0 ctx e f + + ||| assumes the elim is already typechecked! only does the work necessary + ||| to calculate the overall type + private covering + computeElimType : TContext q 0 n -> (e : Elim q 0 n) -> + (0 ne : NotRedex defs e) => + m (Term q 0 n) + computeElimType ctx (F x) = do + defs <- lookupFree' defs x + pure $ defs.type.get + computeElimType ctx (B i) = do + pure $ ctx !! i + computeElimType ctx (f :@ s) {ne} = do + (_, arg, res) <- computeElimType ctx f {ne = noOr1 ne} >>= expectPi defs + pure $ sub1 res (s :# arg) + computeElimType ctx (CasePair {pair, ret, _}) = do + pure $ sub1 ret pair + computeElimType ctx (f :% p) {ne} = do + (ty, _, _) <- computeElimType ctx f {ne = noOr1 ne} >>= expectEq defs + pure $ dsub1 ty p + computeElimType ctx (_ :# ty) = do + pure ty + + private covering + replaceEnd : TContext q 0 n -> + (e : Elim q 0 n) -> DimConst -> (0 ne : NotRedex defs e) -> + m (Elim q 0 n) + replaceEnd ctx e p ne = do + (ty, l, r) <- computeElimType ctx e >>= expectEq defs + pure $ ends l r p :# dsub1 ty (K p) namespace Elim + -- [fixme] the following code ends up repeating a lot of work in the + -- computeElimType calls. the results should be shared better + export covering %inline - compare0 : TContext q 0 n -> (e, f : Elim q 0 n) -> m (Term q 0 n) + compare0 : TContext q 0 n -> (e, f : Elim q 0 n) -> m () compare0 ctx e f = let Element e ne = whnfD defs e Element f nf = whnfD defs f in - compare0' ctx e f - - private - isSubSing : Term {} -> Bool - isSubSing (TYPE _) = False - isSubSing (Pi {res, _}) = isSubSing res.term - isSubSing (Lam {}) = False - isSubSing (Sig {fst, snd, _}) = isSubSing fst && isSubSing snd.term - isSubSing (Pair {}) = False - isSubSing (Eq {}) = True - isSubSing (DLam {}) = False - isSubSing (E e) = False - isSubSing (CloT tm th) = False - isSubSing (DCloT tm th) = False + -- [fixme] there is a better way to do this "isSubSing" stuff for sure + unless (isSubSing !(computeElimType ctx e)) $ compare0' ctx e f private covering compare0' : TContext q 0 n -> (e, f : Elim q 0 n) -> (0 ne : NotRedex defs e) => (0 nf : NotRedex defs f) => - m (Term q 0 n) - compare0' _ e@(F x) f@(F y) = do - d <- lookupFree' defs x - let ty = d.type - -- [fixme] there is a better way to do this for sure - unless (isSubSing ty.get0 || x == y) $ clashE e f - pure ty.get + m () + -- replace applied equalities with the appropriate end first + -- e.g. e : Eq [i ⇒ A] s t ⊢ e 0 = s : A‹0/i› + compare0' ctx (e :% K p) f {ne} = + compare0 ctx !(replaceEnd ctx e p $ noOr1 ne) f + compare0' ctx e (f :% K q) {nf} = + compare0 ctx e !(replaceEnd ctx f q $ noOr1 nf) + + compare0' _ e@(F x) f@(F y) = unless (x == y) $ clashE e f compare0' _ e@(F _) f = clashE e f - compare0' ctx e@(B i) f@(B j) = do - let ty = ctx !! i - -- [fixme] there is a better way to do this for sure - unless (isSubSing ty || i == j) $ clashE e f - pure ty + compare0' ctx e@(B i) f@(B j) = unless (i == j) $ clashE e f compare0' _ e@(B _) f = clashE e f - compare0' ctx (e :@ s) (f :@ t) = local {mode := Equal} $ do - Pi {arg, res, _} <- compare0 ctx e f - | ty => throwError $ ExpectedPi ty + compare0' ctx (e :@ s) (f :@ t) {ne} = local {mode := Equal} $ do + compare0 ctx e f + (_, arg, _) <- computeElimType ctx e {ne = noOr1 ne} >>= expectPi defs compare0 ctx arg s t - pure $ sub1 res (s :# arg) compare0' _ e@(_ :@ _) f = clashE e f compare0' ctx (CasePair epi e _ eret _ _ ebody) - (CasePair fpi f _ fret _ _ fbody) = + (CasePair fpi f _ fret _ _ fbody) {ne} = local {mode := Equal} $ do - ty@(Sig {fst, snd, _}) <- compare0 ctx e f - | ty => throwError $ ExpectedSig ty - unless (epi == fpi) $ throwError $ ClashQ epi fpi - compareType (ctx :< ty) eret.term fret.term - compare0 (ctx :< fst :< snd.term) (substCasePairRet ty eret) + compare0 ctx e f + ety <- computeElimType ctx e {ne = noOr1 ne} + compareType (ctx :< ety) eret.term fret.term + (fst, snd) <- expectSig defs ety + compare0 (ctx :< fst :< snd.term) (substCasePairRet ety eret) ebody.term fbody.term - pure $ sub1 eret e + unless (epi == fpi) $ throwError $ ClashQ epi fpi compare0' _ e@(CasePair {}) f = clashE e f - compare0' ctx (e :% p) (f :% q) = local {mode := Equal} $ do - Eq {ty, _} <- compare0 ctx e f - | ty => throwError $ ExpectedEq ty - unless (p == q) $ throwError $ ClashD p q - pure $ dsub1 ty p - compare0' _ e@(_ :% _) f = clashE e f - compare0' ctx (s :# a) (t :# b) = do compareType ctx a b compare0 ctx a s t - pure b compare0' _ e@(_ :# _) f = clashE e f @@ -268,14 +292,15 @@ parameters {auto _ : (HasDefs' q _ m, HasErr q m, Eq q)} compareType defs (map (/// th) ctx) (s /// th) (t /// th) namespace Elim - -- can't return the type since it might be different in each dsubst ☹ + ||| you don't have to pass the type in but the arguments must still be + ||| of the same type!! export covering %inline compare : (e, f : Elim q d n) -> m () compare e f = do defs <- ask runReaderT {m} (MakeEnv {mode}) $ for_ (splits eq) $ \th => - ignore $ compare0 defs (map (/// th) ctx) (e /// th) (f /// th) + compare0 defs (map (/// th) ctx) (e /// th) (f /// th) namespace Term export covering %inline diff --git a/lib/Quox/Typechecker.idr b/lib/Quox/Typechecker.idr index a8aa178..b56bbdf 100644 --- a/lib/Quox/Typechecker.idr +++ b/lib/Quox/Typechecker.idr @@ -19,37 +19,6 @@ public export CanTC q = CanTC' q IsGlobal -private covering %inline -expectTYPE : CanTC' q _ m => Term q d n -> m Universe -expectTYPE s = - case whnfD !ask s of - Element (TYPE l) _ => pure l - _ => throwError $ ExpectedTYPE s - -private covering %inline -expectPi : CanTC' q _ m => Term q d n -> - m (q, Term q d n, ScopeTerm q d n) -expectPi ty = - case whnfD !ask ty of - Element (Pi qty _ arg res) _ => pure (qty, arg, res) - _ => throwError $ ExpectedPi ty - -private covering %inline -expectSig : CanTC' q _ m => Term q d n -> - m (Term q d n, ScopeTerm q d n) -expectSig ty = - case whnfD !ask ty of - Element (Sig _ arg res) _ => pure (arg, res) - _ => throwError $ ExpectedSig ty - -private covering %inline -expectEq : CanTC' q _ m => Term q d n -> - m (DScopeTerm q d n, Term q d n, Term q d n) -expectEq ty = - case whnfD !ask ty of - Element (Eq _ ty l r) _ => pure (ty, l, r) - _ => throwError $ ExpectedEq ty - private popQs : HasErr q m => IsQty q => @@ -133,13 +102,13 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m} check' ctx sg (TYPE l) _ ty = do -- if ℓ < ℓ' then Ψ | Γ ⊢ Type ℓ · 0 ⇐ Type ℓ' ⊳ 𝟎 - l' <- expectTYPE ty + l' <- expectTYPE !ask ty expectEqualQ zero sg.fst unless (l < l') $ throwError $ BadUniverse l l' pure $ zeroFor ctx check' ctx sg (Pi qty _ arg res) _ ty = do - l <- expectTYPE ty + l <- expectTYPE !ask ty expectEqualQ zero sg.fst -- if Ψ | Γ ⊢ A · 0 ⇐ Type ℓ ⊳ 𝟎 ignore $ check0 ctx arg (TYPE l) @@ -151,14 +120,14 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m} pure $ zeroFor ctx check' ctx sg (Lam _ body) _ ty = do - (qty, arg, res) <- expectPi ty + (qty, arg, res) <- expectPi !ask ty -- if Ψ | Γ, x · πσ : A ⊢ t · σ ⇐ B ⊳ Σ, x · σπ qout <- check (extendTy arg (sg.fst * qty) ctx) sg body.term res.term -- then Ψ | Γ ⊢ λx. t · σ ⇐ (x · π : A) → B ⊳ Σ popQ (sg.fst * qty) qout check' ctx sg (Sig _ fst snd) _ ty = do - l <- expectTYPE ty + l <- expectTYPE !ask ty expectEqualQ zero sg.fst -- if Ψ | Γ ⊢ A · 0 ⇐ Type ℓ ⊳ 𝟎 ignore $ check0 ctx fst (TYPE l) @@ -170,7 +139,7 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m} pure $ zeroFor ctx check' ctx sg (Pair fst snd) _ ty = do - (tfst, tsnd) <- expectSig ty + (tfst, tsnd) <- expectSig !ask ty -- if Ψ | Γ ⊢ s · σ ⇐ A ⊳ Σ₁ qfst <- check ctx sg fst tfst let tsnd = sub1 tsnd (fst :# tfst) @@ -180,7 +149,7 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m} pure $ qfst + qsnd check' ctx sg (Eq i t l r) _ ty = do - u <- expectTYPE ty + u <- expectTYPE !ask ty expectEqualQ zero sg.fst -- if Ψ, i | Γ ⊢ A · 0 ⇐ Type ℓ ⊳ 𝟎 case t of @@ -194,7 +163,7 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m} pure $ zeroFor ctx check' ctx sg (DLam i body) _ ty = do - (ty, l, r) <- expectEq ty + (ty, l, r) <- expectEq !ask ty -- if Ψ, i | Γ ⊢ t · σ ⇐ A ⊳ Σ qout <- check (extendDim ctx) sg body.term ty.term let eqs = makeDimEq ctx.dctx @@ -234,7 +203,7 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m} infer' ctx sg (fun :@ arg) _ = do -- if Ψ | Γ ⊢ f · σ ⇒ (x · π : A) → B ⊳ Σ₁ funres <- infer ctx sg fun - (qty, argty, res) <- expectPi funres.type + (qty, argty, res) <- expectPi !ask funres.type -- if Ψ | Γ ⊢ s · σ∧π ⇐ A ⊳ Σ₂ -- (0∧π = σ∧0 = 0; σ∧π = σ otherwise) argout <- check ctx (subjMult sg qty) arg argty @@ -250,7 +219,7 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m} -- if Ψ | Γ ⊢ pair · 1 ⇒ (x : A) × B ⊳ Σ₁ pairres <- infer ctx sone pair ignore $ check0 (extendTy pairres.type zero ctx) ret.term (TYPE UAny) - (tfst, tsnd) <- expectSig pairres.type + (tfst, tsnd) <- expectSig !ask pairres.type -- if Ψ | Γ, x · π : A, y · π : B ⊢ σ body ⇐ ret[(x, y)] -- ⊳ Σ₂, x · π₁, y · π₂ -- if π₁, π₂ ≤ π @@ -263,11 +232,10 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m} qout = pi * pairres.qout + bodyout } - infer' ctx sg (fun :% dim) _ = do -- if Ψ | Γ ⊢ f · σ ⇒ Eq [i ⇒ A] l r ⊳ Σ InfRes {type, qout} <- infer ctx sg fun - (ty, _, _) <- expectEq type + (ty, _, _) <- expectEq !ask type -- then Ψ | Γ ⊢ f p · σ ⇒ A‹p› ⊳ Σ pure $ InfRes {type = dsub1 ty dim, qout} diff --git a/lib/Quox/Typing.idr b/lib/Quox/Typing.idr index 21f0b3f..2779c24 100644 --- a/lib/Quox/Typing.idr +++ b/lib/Quox/Typing.idr @@ -177,3 +177,33 @@ substCasePairRet : Term q d n -> ScopeTerm q d n -> Term q d (2 + n) substCasePairRet dty retty = let arg = Pair (BVT 0) (BVT 1) :# (dty // fromNat 2) in retty.term // (arg ::: shift 2) + + +parameters {auto _ : HasErr q m} (defs : Definitions' q _) + export covering %inline + expectTYPE : Term q d n -> m Universe + expectTYPE s = + case fst $ whnfD defs s of + TYPE l => pure l + _ => throwError $ ExpectedTYPE s + + export covering %inline + expectPi : Term q d n -> m (q, Term q d n, ScopeTerm q d n) + expectPi s = + case fst $ whnfD defs s of + Pi {qty, arg, res, _} => pure (qty, arg, res) + _ => throwError $ ExpectedPi s + + export covering %inline + expectSig : Term q d n -> m (Term q d n, ScopeTerm q d n) + expectSig s = + case fst $ whnfD defs s of + Sig {fst, snd, _} => pure (fst, snd) + _ => throwError $ ExpectedSig s + + export covering %inline + expectEq : Term q d n -> m (DScopeTerm q d n, Term q d n, Term q d n) + expectEq s = + case fst $ whnfD defs s of + Eq {ty, l, r, _} => pure (ty, l, r) + _ => throwError $ ExpectedEq s diff --git a/tests/Tests.idr b/tests/Tests.idr index 4da0382..27342ab 100644 --- a/tests/Tests.idr +++ b/tests/Tests.idr @@ -1,20 +1,17 @@ module Tests import TAP --- import Tests.Unicode --- import Tests.Lexer --- import Tests.Parser import Tests.Reduce import Tests.Equal +import Tests.Typechecker import System +allTests : List Test allTests = [ - -- Unicode.tests, - -- Lexer.tests, - -- Parser.tests, Reduce.tests, - Equal.tests + Equal.tests, + Typechecker.tests ] main = TAP.main !getTestOpts allTests diff --git a/tests/Tests/Equal.idr b/tests/Tests/Equal.idr index c08b1fc..e3e7ee9 100644 --- a/tests/Tests/Equal.idr +++ b/tests/Tests/Equal.idr @@ -1,65 +1,10 @@ module Tests.Equal -import Quox.Equal as Lib -import Quox.Pretty +import Quox.Equal import Quox.Syntax.Qty.Three +import public TypingImpls import TAP -export -ToInfo (Error Three) where - toInfo (NotInScope x) = - [("type", "NotInScope"), - ("name", show x)] - toInfo (ExpectedTYPE t) = - [("type", "ExpectedTYPE"), - ("got", prettyStr True t)] - toInfo (ExpectedPi t) = - [("type", "ExpectedPi"), - ("got", prettyStr True t)] - toInfo (ExpectedSig t) = - [("type", "ExpectedSig"), - ("got", prettyStr True t)] - toInfo (ExpectedEq t) = - [("type", "ExpectedEq"), - ("got", prettyStr True t)] - toInfo (BadUniverse k l) = - [("type", "BadUniverse"), - ("low", show k), - ("high", show l)] - toInfo (ClashT mode ty s t) = - [("type", "ClashT"), - ("mode", show mode), - ("ty", prettyStr True ty), - ("left", prettyStr True s), - ("right", prettyStr True t)] - toInfo (ClashE mode e f) = - [("type", "ClashE"), - ("mode", show mode), - ("left", prettyStr True e), - ("right", prettyStr True f)] - toInfo (ClashU mode k l) = - [("type", "ClashU"), - ("mode", show mode), - ("left", prettyStr True k), - ("right", prettyStr True l)] - toInfo (ClashQ pi rh) = - [("type", "ClashQ"), - ("left", prettyStr True pi), - ("right", prettyStr True rh)] - toInfo (ClashD p q) = - [("type", "ClashD"), - ("left", prettyStr True p), - ("right", prettyStr True q)] - toInfo (NotType ty) = - [("type", "NotType"), - ("actual", prettyStr True ty)] - toInfo (WrongType ty s t) = - [("type", "WrongType"), - ("ty", prettyStr True ty), - ("left", prettyStr True s), - ("right", prettyStr True t)] - - 0 M : Type -> Type M = ReaderT (Definitions Three) (Either (Error Three)) @@ -68,6 +13,7 @@ defGlobals = fromList [("A", mkAbstract Zero $ TYPE 0), ("B", mkAbstract Zero $ TYPE 0), ("a", mkAbstract Any $ FT "A"), + ("a'", mkAbstract Any $ FT "A"), ("b", mkAbstract Any $ FT "B"), ("f", mkAbstract Any $ Arr One (FT "A") (FT "A"))] @@ -100,6 +46,7 @@ export tests : Test tests = "equality & subtyping" :- [ note #""0=1 ⊢ 𝒥" means that 𝒥 holds in an inconsistent dim context"#, + note #""s{…}" for term substs; "s‹…›" for dim substs"#, "universes" :- [ testEq "★₀ ≡ ★₀" $ @@ -117,8 +64,8 @@ tests = "equality & subtyping" :- [ ], "pi" :- [ - note #""A ⊸ B" for (1 _ : A) → B"#, - note #""A ⇾ B" for (0 _ : A) → B"#, + note #""A ⊸ B" for (1·A) → B"#, + note #""A ⇾ B" for (0·A) → B"#, testEq "A ⊸ B ≡ A ⊸ B" $ let tm = Arr One (FT "A") (FT "B") in equalT [<] (TYPE 0) tm tm, @@ -168,32 +115,31 @@ tests = "equality & subtyping" :- [ "lambda" :- [ testEq "λ x ⇒ [x] ≡ λ x ⇒ [x]" $ equalT [<] (Arr One (FT "A") (FT "A")) - (Lam "x" $ TUsed $ BVT 0) - (Lam "x" $ TUsed $ BVT 0), + (["x"] :\\ BVT 0) + (["x"] :\\ BVT 0), testEq "λ x ⇒ [x] <: λ x ⇒ [x]" $ subT [<] (Arr One (FT "A") (FT "A")) - (Lam "x" $ TUsed $ BVT 0) - (Lam "x" $ TUsed $ BVT 0), + (["x"] :\\ BVT 0) + (["x"] :\\ BVT 0), testEq "λ x ⇒ [x] ≡ λ y ⇒ [y]" $ equalT [<] (Arr One (FT "A") (FT "A")) - (Lam "x" $ TUsed $ BVT 0) - (Lam "y" $ TUsed $ BVT 0), + (["x"] :\\ BVT 0) + (["y"] :\\ BVT 0), testEq "λ x ⇒ [x] <: λ y ⇒ [y]" $ equalT [<] (Arr One (FT "A") (FT "A")) - (Lam "x" $ TUsed $ BVT 0) - (Lam "y" $ TUsed $ BVT 0), + (["x"] :\\ BVT 0) + (["y"] :\\ BVT 0), testNeq "λ x y ⇒ [x] ≢ λ x y ⇒ [y]" $ equalT [<] (Arr One (FT "A") $ Arr One (FT "A") (FT "A")) - (Lam "x" $ TUsed $ Lam "y" $ TUsed $ BVT 1) - (Lam "x" $ TUsed $ Lam "y" $ TUsed $ BVT 0), + (["x", "y"] :\\ BVT 1) + (["x", "y"] :\\ BVT 0), testEq "λ x ⇒ [a] ≡ λ x ⇒ [a] (TUsed vs TUnused)" $ equalT [<] (Arr Zero (FT "B") (FT "A")) (Lam "x" $ TUsed $ FT "a") (Lam "x" $ TUnused $ FT "a"), - skipWith "(no η yet)" $ testEq "λ x ⇒ [f [x]] ≡ [f] (η)" $ equalT [<] (Arr One (FT "A") (FT "A")) - (Lam "x" $ TUsed $ E $ F "f" :@ BVT 0) + (["x"] :\\ E (F "f" :@ BVT 0)) (FT "f") ], @@ -208,7 +154,23 @@ tests = "equality & subtyping" :- [ (Eq0 (FT "A") (TYPE 0) (TYPE 0)) ], - todo "dim lambda", + "equalities" :- + let refl : Term q d n -> Term q d n -> Elim q d n + refl a x = (DLam "_" $ DUnused x) :# (Eq0 a x x) + in + [ + note #""refl [A] x" is an abbreviation for "(λᴰi ⇒ x) ∷ (x ≡ x : A)""#, + testEq "refl [A] a ≡ refl [A] a" $ + equalE [<] (refl (FT "A") (FT "a")) (refl (FT "A") (FT "a")), + testEq "p : (a ≡ a' : A), q : (a ≡ a' : A) ⊢ p ≡ q (free)" + {globals = + let def = mkAbstract Zero $ Eq0 (FT "A") (FT "a") (FT "a'") in + defGlobals `mergeLeft` fromList [("p", def), ("q", def)]} $ + equalE [<] (F "p") (F "q"), + testEq "x : (a ≡ a' : A), y : (a ≡ a' : A) ⊢ x ≡ y (bound)" $ + let ty : forall n. Term Three 0 n := Eq0 (FT "A") (FT "a") (FT "a'") in + equalE [< ty, ty] (BV 0) (BV 1) {n = 2} + ], "term closure" :- [ note "𝑖, 𝑗 for bound variables pointing outside of the current expr", @@ -230,8 +192,8 @@ tests = "equality & subtyping" :- [ (Lam "y" $ TUnused $ FT "a"), testEq "(λy. [𝑖]){y/y, a/𝑖} ≡ λy. [a] (TUsed)" $ equalT [<] (Arr Zero (FT "B") (FT "A")) - (CloT (Lam "y" $ TUsed $ BVT 1) (F "a" ::: id)) - (Lam "y" $ TUsed $ FT "a") + (CloT (["y"] :\\ BVT 1) (F "a" ::: id)) + (["y"] :\\ FT "a") ], todo "term d-closure", @@ -290,48 +252,29 @@ tests = "equality & subtyping" :- [ subE [<] (F "f" :@ FT "a") (F "f" :@ FT "a"), testEq "(λ x ⇒ [x] ∷ A ⊸ A) a ≡ ([a ∷ A] ∷ A) (β)" $ equalE [<] - ((Lam "x" (TUsed (BVT 0)) :# (Arr One (FT "A") (FT "A"))) - :@ FT "a") + (((["x"] :\\ BVT 0) :# Arr One (FT "A") (FT "A")) :@ FT "a") (E (FT "a" :# FT "A") :# FT "A"), testEq "(λ x ⇒ [x] ∷ A ⊸ A) a ≡ a (βυ)" $ equalE [<] - ((Lam "x" (TUsed (BVT 0)) :# (Arr One (FT "A") (FT "A"))) - :@ FT "a") + (((["x"] :\\ BVT 0) :# Arr One (FT "A") (FT "A")) :@ FT "a") (F "a"), testEq "(λ g ⇒ [g [a]] ∷ ⋯)) [f] ≡ (λ y ⇒ [f [y]] ∷ ⋯) [a] (β↘↙)" $ let a = FT "A"; a2a = (Arr One a a) in equalE [<] - ((Lam "g" (TUsed (E (BV 0 :@ FT "a"))) :# Arr One a2a a) :@ FT "f") - ((Lam "y" (TUsed (E (F "f" :@ BVT 0))) :# a2a) :@ FT "a"), + (((["g"] :\\ E (BV 0 :@ FT "a")) :# Arr One a2a a) :@ FT "f") + (((["y"] :\\ E (F "f" :@ BVT 0)) :# a2a) :@ FT "a"), testEq "(λ x ⇒ [x] ∷ A ⊸ A) a <: a" $ subE [<] - ((Lam "x" (TUsed (BVT 0)) :# (Arr One (FT "A") (FT "A"))) - :@ FT "a") + (((["x"] :\\ BVT 0) :# (Arr One (FT "A") (FT "A"))) :@ FT "a") (F "a"), testEq "id : A ⊸ A ≔ λ x ⇒ [x] ⊢ id [a] ≡ a" {globals = defGlobals `mergeLeft` fromList [("id", mkDef Any (Arr One (FT "A") (FT "A")) - (Lam "x" (TUsed (BVT 0))))]} $ + (["x"] :\\ BVT 0))]} $ equalE [<] (F "id" :@ FT "a") (F "a") ], - "dim application" :- - let refl : Term q d n -> Term q d n -> Elim q d n - refl a x = (DLam "_" $ DUnused x) :# (Eq0 a x x) - in - [ - note #""refl [A] x" is an abbreviation for "(λᴰi ⇒ x) ∷ (x ≡ x : A)""#, - testEq "refl [A] a ≡ refl [A] a" $ - equalE [<] (refl (FT "A") (FT "a")) (refl (FT "A") (FT "a")), - testEq "p : (a ≡ b : A), q : (a ≡ b : A) ⊢ p ≡ q" - {globals = - let def = mkAbstract Zero $ Eq0 (FT "A") (FT "a") (FT "b") in - fromList [("A", mkAbstract Zero $ TYPE 0), - ("a", mkAbstract Any $ FT "A"), - ("b", mkAbstract Any $ FT "A"), - ("p", def), ("q", def)]} $ - equalE [<] (F "p") (F "q") - ], + todo "dim application", todo "annotation", diff --git a/tests/Tests/Typechecker.idr b/tests/Tests/Typechecker.idr new file mode 100644 index 0000000..1e516b3 --- /dev/null +++ b/tests/Tests/Typechecker.idr @@ -0,0 +1,138 @@ +module Tests.Typechecker + +import Quox.Syntax +import Quox.Syntax.Qty.Three +import Quox.Typechecker as Lib +import public TypingImpls +import TAP + + +0 M : Type -> Type +M = ReaderT (Definitions Three) $ Either (Error Three) + + + +reflTy : IsQty q => Term q d n +reflTy = + Pi zero "A" (TYPE 0) $ TUsed $ + Pi zero "x" (BVT 0) $ TUsed $ + Eq0 (BVT 1) (BVT 0) (BVT 0) + +reflDef : IsQty q => Term q d n +reflDef = ["A","x"] :\\ ["i"] :\\% BVT 0 + +defGlobals : Definitions Three +defGlobals = fromList + [("A", mkAbstract Zero $ TYPE 0), + ("B", mkAbstract Zero $ TYPE 0), + ("C", mkAbstract Zero $ TYPE 1), + ("D", mkAbstract Zero $ TYPE 1), + ("a", mkAbstract Any $ FT "A"), + ("b", mkAbstract Any $ FT "B"), + ("f", mkAbstract Any $ Arr One (FT "A") (FT "A")), + ("refl", mkDef Any reflTy reflDef)] + +parameters (label : String) (act : Lazy (M ())) + {default defGlobals globals : Definitions Three} + testTC : Test + testTC = test label $ runReaderT globals act + + testTCFail : Test + testTCFail = testThrows label (const True) $ runReaderT globals act + + +ctxWith : DContext d -> Context (\i => (Term Three d i, Three)) n -> + TyContext Three d n +ctxWith dctx tqctx = + let (tctx, qctx) = unzip tqctx in MkTyContext {dctx, tctx, qctx} + +ctx : Context (\i => (Term Three 0 i, Three)) n -> TyContext Three 0 n +ctx = ctxWith DNil + +inferAs : TyContext Three d n -> (sg : SQty Three) -> + Elim Three d n -> Term Three d n -> M () +inferAs ctx sg e ty = do + ty' <- infer ctx sg e + catchError + (equalType (makeDimEq ctx.dctx) ctx.tctx ty ty'.type) + (\_ : Error Three => throwError $ ClashT Equal (TYPE UAny) ty ty'.type) + +infer_ : TyContext Three d n -> (sg : SQty Three) -> Elim Three d n -> M () +infer_ ctx sg e = ignore $ infer ctx sg e + +check_ : TyContext Three d n -> SQty Three -> + Term Three d n -> Term Three d n -> M () +check_ ctx sg s ty = ignore $ check ctx sg s ty + +export +tests : Test +tests = "typechecker" :- [ + "universes" :- [ + testTC "0 · ★₀ ⇐ ★₁" $ check_ (ctx [<]) szero (TYPE 0) (TYPE 1), + testTC "0 · ★₀ ⇐ ★₂" $ check_ (ctx [<]) szero (TYPE 0) (TYPE 2), + testTC "0 · ★₀ ⇐ ★_" $ check_ (ctx [<]) szero (TYPE 0) (TYPE UAny), + testTCFail "0 · ★₁ ⇍ ★₀" $ check_ (ctx [<]) szero (TYPE 1) (TYPE 0), + testTCFail "0 · ★₀ ⇍ ★₀" $ check_ (ctx [<]) szero (TYPE 0) (TYPE 0), + testTCFail "0 · ★_ ⇍ ★_" $ check_ (ctx [<]) szero (TYPE UAny) (TYPE UAny), + testTCFail "1 · ★₀ ⇍ ★₁" $ check_ (ctx [<]) sone (TYPE 0) (TYPE 1) + ], + + "function types" :- [ + note "A, B : ★₀; C, D : ★₁", + testTC "0 · (1·A) → B ⇐ ★₀" $ + check_ (ctx [<]) szero (Arr One (FT "A") (FT "B")) (TYPE 0), + testTC "0 · (1·A) → B ⇐ ★₁👈" $ + check_ (ctx [<]) szero (Arr One (FT "A") (FT "B")) (TYPE 1), + testTC "0 · (1·C) → D ⇐ ★₁" $ + check_ (ctx [<]) szero (Arr One (FT "C") (FT "D")) (TYPE 1), + testTCFail "0 · (1·C) → D ⇍ ★₀" $ + check_ (ctx [<]) szero (Arr One (FT "C") (FT "D")) (TYPE 0) + ], + + "free vars" :- [ + testTC "0 · A ⇒ ★₀" $ + inferAs (ctx [<]) szero (F "A") (TYPE 0), + testTC "0 · A ⇐👈 ★₀" $ + check_ (ctx [<]) szero (FT "A") (TYPE 0), + testTC "0 · A ⇐ ★₁👈" $ + check_ (ctx [<]) szero (FT "A") (TYPE 1), + testTCFail "1👈 · A ⇏ ★₀" $ + infer_ (ctx [<]) sone (F "A"), + note "refl : (0·A : ★₀) → (0·x : A) → (x ≡ x : A) ≔ (λ A x ⇒ λᴰ _ ⇒ x)", + testTC "1 · refl ⇒ {type of refl}" $ + inferAs (ctx [<]) sone (F "refl") reflTy, + testTC "1 · refl ⇐ {type of refl}" $ + check_ (ctx [<]) sone (FT "refl") reflTy + ], + + "lambda" :- [ + testTC #"1 · (λ A x ⇒ refl A x) ⇐ {type of refl, see "free vars"}"# $ + check_ (ctx [<]) sone + (["A", "x"] :\\ E (F "refl" :@@ [BVT 1, BVT 0])) + reflTy + ], + + "misc" :- [ + testTC "funext" + {globals = fromList + [("A", mkAbstract Zero $ TYPE 0), + ("B", mkAbstract Zero $ Arr Any (FT "A") (TYPE 0)), + ("f", mkAbstract Any $ + Pi Any "x" (FT "A") $ TUsed $ E $ F "B" :@ BVT 0), + ("g", mkAbstract Any $ + Pi Any "x" (FT "A") $ TUsed $ E $ F "B" :@ BVT 0)]} $ + -- 0·A : Type, 0·B : ω·A → Type, + -- ω·f, g : (ω·x : A) → B x + -- ⊢ + -- 0·funext : (ω·eq : (0·x : A) → f x ≡ g x) → f ≡ g + -- = λ eq ⇒ λᴰ i ⇒ λ x ⇒ eq x i + check_ (ctx [<]) szero + (["eq"] :\\ ["i"] :\\% ["x"] :\\ E (BV 1 :@ BVT 0 :% BV 0)) + (Pi Any "eq" + (Pi Zero "x" (FT "A") $ TUsed $ + Eq0 (E $ F "B" :@ BVT 0) + (E $ F "f" :@ BVT 0) (E $ F "g" :@ BVT 0)) $ TUsed $ + Eq0 (Pi Any "x" (FT "A") $ TUsed $ E $ F "B" :@ BVT 0) + (FT "f") (FT "g")) + ] +] diff --git a/tests/TypingImpls.idr b/tests/TypingImpls.idr new file mode 100644 index 0000000..b4451c8 --- /dev/null +++ b/tests/TypingImpls.idr @@ -0,0 +1,61 @@ +module TypingImpls + +import TAP +import public Quox.Typing +import public Quox.Pretty + +export +PrettyHL q => ToInfo (Error q) where + toInfo (NotInScope x) = + [("type", "NotInScope"), + ("name", show x)] + toInfo (ExpectedTYPE t) = + [("type", "ExpectedTYPE"), + ("got", prettyStr True t)] + toInfo (ExpectedPi t) = + [("type", "ExpectedPi"), + ("got", prettyStr True t)] + toInfo (ExpectedSig t) = + [("type", "ExpectedSig"), + ("got", prettyStr True t)] + toInfo (ExpectedEq t) = + [("type", "ExpectedEq"), + ("got", prettyStr True t)] + toInfo (BadUniverse k l) = + [("type", "BadUniverse"), + ("low", show k), + ("high", show l)] + toInfo (ClashT mode ty s t) = + [("type", "ClashT"), + ("mode", show mode), + ("ty", prettyStr True ty), + ("left", prettyStr True s), + ("right", prettyStr True t)] + toInfo (ClashE mode e f) = + [("type", "ClashE"), + ("mode", show mode), + ("left", prettyStr True e), + ("right", prettyStr True f)] + toInfo (ClashU mode k l) = + [("type", "ClashU"), + ("mode", show mode), + ("left", prettyStr True k), + ("right", prettyStr True l)] + toInfo (ClashQ pi rh) = + [("type", "ClashQ"), + ("left", prettyStr True pi), + ("right", prettyStr True rh)] + toInfo (ClashD p q) = + [("type", "ClashD"), + ("left", prettyStr True p), + ("right", prettyStr True q)] + toInfo (NotType ty) = + [("type", "NotType"), + ("actual", prettyStr True ty)] + toInfo (WrongType ty s t) = + [("type", "WrongType"), + ("ty", prettyStr True ty), + ("left", prettyStr True s), + ("right", prettyStr True t)] + + diff --git a/tests/quox-tests.ipkg b/tests/quox-tests.ipkg index 6c8cc64..95eac27 100644 --- a/tests/quox-tests.ipkg +++ b/tests/quox-tests.ipkg @@ -6,5 +6,7 @@ executable = quox-tests main = Tests modules = TermImpls, + TypingImpls, Tests.Reduce, - Tests.Equal + Tests.Equal, + Tests.Typechecker