From 86d21caf24e9c2664d1dff8aaf5bdfa55d96f259 Mon Sep 17 00:00:00 2001 From: rhiannon morris Date: Tue, 14 Mar 2023 03:22:26 +0100 Subject: [PATCH] put names into contexts, and contexts into errors --- exe/Main.idr | 2 +- lib/Quox/Context.idr | 6 ++ lib/Quox/Equal.idr | 136 +++++++++++++++++-------------- lib/Quox/Syntax/DimEq.idr | 10 +++ lib/Quox/Syntax/Subst.idr | 4 + lib/Quox/Syntax/Term/Base.idr | 8 ++ lib/Quox/Typechecker.idr | 66 ++++++++------- lib/Quox/Typing.idr | 149 ++++++++++++++++++---------------- lib/Quox/Typing/Context.idr | 122 +++++++++++++++++++++++++++- lib/Quox/Typing/Error.idr | 44 +++++----- tests/Tests/Equal.idr | 122 ++++++++++++++++++---------- tests/Tests/Typechecker.idr | 143 ++++++++++++++++---------------- tests/TypingImpls.idr | 32 ++++---- 13 files changed, 520 insertions(+), 324 deletions(-) diff --git a/exe/Main.idr b/exe/Main.idr index 628c038..a1c4c7c 100644 --- a/exe/Main.idr +++ b/exe/Main.idr @@ -58,7 +58,7 @@ tm : Term Three 1 2 tm = (Pi_ One "a" (BVT 0) (E (F "F" :@@ [BVT 0, FT "w"])) `DCloT` (K One ::: id)) - `CloT` (F "y" ::: TYPE (U 1) :# TYPE (U 2) ::: id) + `CloT` (F "y" ::: TYPE 1 :# TYPE 2 ::: id) main : IO Unit main = do diff --git a/lib/Quox/Context.idr b/lib/Quox/Context.idr index 9ffe7da..0d6f60d 100644 --- a/lib/Quox/Context.idr +++ b/lib/Quox/Context.idr @@ -174,6 +174,12 @@ zipWithLazy : forall tm1, tm2, tm3. Telescope (\n => Lazy (tm3 n)) from to zipWithLazy f = zipWith $ delay .: f +export +unzip : Telescope (\n => (tm1 n, tm2 n)) from to -> + (Telescope tm1 from to, Telescope tm2 from to) +unzip [<] = ([<], [<]) +unzip (tel :< (x, y)) = let (xs, ys) = unzip tel in (xs :< x, ys :< y) + export lengthPrf : Telescope _ from to -> Subset Nat (\len => len + from = to) diff --git a/lib/Quox/Equal.idr b/lib/Quox/Equal.idr index 12f13e3..d7a3b25 100644 --- a/lib/Quox/Equal.idr +++ b/lib/Quox/Equal.idr @@ -27,17 +27,18 @@ private %inline mode : HasCmpContext m => m EqMode mode = asks mode -private %inline -clashT : CanEqual q m => Term q d n -> Term q d n -> Term q d n -> m a -clashT ty s t = throwError $ ClashT !mode ty s t +parameters {auto _ : CanEqual q m} (ctx : EqContext q n) + private %inline + clashT : Term q 0 n -> Term q 0 n -> Term q 0 n -> m a + clashT ty s t = throwError $ ClashT ctx !mode ty s t -private %inline -clashTy : CanEqual q m => Term q d n -> Term q d n -> m a -clashTy s t = throwError $ ClashTy !mode s t + private %inline + clashTy : Term q 0 n -> Term q 0 n -> m a + clashTy s t = throwError $ ClashTy ctx !mode s t -private %inline -clashE : CanEqual q m => Elim q d n -> Elim q d n -> m a -clashE e f = throwError $ ClashE !mode e f + private %inline + clashE : Elim q 0 n -> Elim q 0 n -> m a + clashE e f = throwError $ ClashE ctx !mode e f ||| true if a term is syntactically a type, or is neutral. @@ -114,8 +115,12 @@ parameters {auto _ : HasErr q m} Right _ => throwError $ e t export %inline - ensureTyCon : HasErr q m => (t : Term q d n) -> m (So (isTyCon t)) - ensureTyCon = ensure NotType isTyCon + ensureTyCon : (ctx : EqContext q n) -> (t : Term q 0 n) -> m (So (isTyCon t)) + ensureTyCon ctx t = case nchoose $ isTyCon t of + Left y => pure y + Right n => + let (d ** ctx) = toTyContext ctx in + throwError $ NotType ctx (t // shift0 d) parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)} mutual @@ -125,13 +130,13 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)} ||| ||| ⚠ **assumes that `s`, `t` have already been checked against `ty`**. ⚠ export covering %inline - compare0 : TContext q 0 n -> (ty, s, t : Term q 0 n) -> m () + compare0 : EqContext q n -> (ty, s, t : Term q 0 n) -> m () compare0 ctx ty s t = - wrapErr (WhileComparingT (MkTyContext new ctx) !mode ty s t) $ do + wrapErr (WhileComparingT ctx !mode ty s t) $ do Element ty nty <- whnfT defs ty Element s ns <- whnfT defs s Element t nt <- whnfT defs t - tty <- ensureTyCon ty + tty <- ensureTyCon ctx ty compare0' ctx ty s t ||| converts an elim "Γ ⊢ e" to "Γ, x ⊢ e x", for comparing with @@ -141,7 +146,7 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)} toLamBody e = E $ weakE e :@ BVT 0 private covering - compare0' : TContext q 0 n -> + compare0' : EqContext q n -> (ty, s, t : Term q 0 n) -> (0 nty : NotRedex defs ty) => (0 tty : So (isTyCon ty)) => (0 ns : NotRedex defs s) => (0 nt : NotRedex defs t) => @@ -162,14 +167,14 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)} (Lam b, E e) => eta e b (E e, E f) => Elim.compare0 ctx e f - _ => throwError $ WrongType ty s t + _ => throwError $ WrongType ctx ty s t where - ctx' : TContext q 0 (S n) - ctx' = ctx :< arg + ctx' : EqContext q (S n) + ctx' = extendTy res.name arg ctx eta : Elim q 0 n -> ScopeTerm q 0 n -> m () eta e (S _ (Y b)) = compare0 ctx' res.term (toLamBody e) b - eta e (S _ (N _)) = clashT ty s t + eta e (S _ (N _)) = clashT ctx ty s t compare0' ctx ty@(Sig {fst, snd, _}) s t = local {mode := Equal} $ case (s, t) of @@ -183,7 +188,7 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)} compare0 ctx (sub1 snd (sFst :# fst)) sSnd tSnd (E e, E f) => compare0 ctx e f - _ => throwError $ WrongType ty s t + _ => throwError $ WrongType ctx ty s t compare0' ctx ty@(Enum tags) s t = local {mode := Equal} $ case (s, t) of @@ -191,9 +196,9 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)} -- Γ ⊢ `t = `t : {ts} -- -- t ∈ ts is in the typechecker, not here, ofc - (Tag t1, Tag t2) => unless (t1 == t2) $ clashT ty s t + (Tag t1, Tag t2) => unless (t1 == t2) $ clashT ctx ty s t (E e, E f) => compare0 ctx e f - _ => throwError $ WrongType ty s t + _ => throwError $ WrongType ctx ty s t compare0' _ (Eq {}) _ _ = -- ✨ uip ✨ @@ -204,25 +209,25 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)} compare0' ctx ty@(E _) s t = do -- a neutral type can only be inhabited by neutral values -- 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 + E e <- pure s | _ => throwError $ WrongType ctx ty s t + E f <- pure t | _ => throwError $ WrongType ctx ty s t Elim.compare0 ctx e f ||| compares two types, using the current variance `mode` for universes. ||| fails if they are not types, even if they would happen to be equal. export covering %inline - compareType : TContext q 0 n -> (s, t : Term q 0 n) -> m () + compareType : EqContext q n -> (s, t : Term q 0 n) -> m () compareType ctx s t = do Element s ns <- whnfT defs s Element t nt <- whnfT defs t - ts <- ensureTyCon s - tt <- ensureTyCon t - st <- either pure (const $ clashTy s t) $ + ts <- ensureTyCon ctx s + tt <- ensureTyCon ctx t + st <- either pure (const $ clashTy ctx s t) $ nchoose $ sameTyCon s t compareType' ctx s t private covering - compareType' : TContext q 0 n -> (s, t : Term q 0 n) -> + compareType' : EqContext q n -> (s, t : Term q 0 n) -> (0 ns : NotRedex defs s) => (0 ts : So (isTyCon s)) => (0 nt : NotRedex defs t) => (0 tt : So (isTyCon t)) => (0 st : So (sameTyCon s t)) => @@ -242,7 +247,7 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)} -- Γ ⊢ (π·x : A₁) → B₁ <: (π·x : A₂) → B₂ expectEqualQ sQty tQty local {mode $= flip} $ compareType ctx sArg tArg -- contra - compareType (ctx :< sArg) sRes.term tRes.term + compareType (extendTy sRes.name sArg ctx) sRes.term tRes.term compareType' ctx (Sig {fst = sFst, snd = sSnd, _}) (Sig {fst = tFst, snd = tSnd, _}) = do @@ -250,7 +255,7 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)} -- -------------------------------------- -- Γ ⊢ (x : A₁) × B₁ <: (x : A₂) × B₂ compareType ctx sFst tFst - compareType (ctx :< sFst) sSnd.term tSnd.term + compareType (extendTy sSnd.name sFst ctx) sSnd.term tSnd.term compareType' ctx (Eq {ty = sTy, l = sl, r = sr, _}) (Eq {ty = tTy, l = tl, r = tr, _}) = do @@ -258,8 +263,8 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)} -- Γ ⊢ l₁ = l₂ : A₁‹𝟎/i› Γ ⊢ r₁ = r₂ : A₁‹𝟏/i› -- ------------------------------------------------ -- Γ ⊢ Eq [i ⇒ A₁] l₁ r₂ <: Eq [i ⇒ A₂] l₂ r₂ - compareType ctx sTy.zero tTy.zero - compareType ctx sTy.one tTy.one + compareType (extendDim sTy.name Zero ctx) sTy.zero tTy.zero + compareType (extendDim sTy.name One ctx) sTy.one tTy.one local {mode := Equal} $ do Term.compare0 ctx sTy.zero sl tl Term.compare0 ctx sTy.one sr tr @@ -270,7 +275,7 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)} -- -- no subtyping based on tag subsets, since that would need -- a runtime coercion - unless (tags1 == tags2) $ clashTy s t + unless (tags1 == tags2) $ clashTy ctx s t compareType' ctx (E e) (E f) = do -- no fanciness needed here cos anything other than a neutral @@ -281,33 +286,33 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)} ||| ||| ⚠ **assumes the elim is already typechecked.** ⚠ private covering - computeElimType : TContext q 0 n -> (e : Elim q 0 n) -> + computeElimType : EqContext q 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 + pure $ ctx.tctx !! i computeElimType ctx (f :@ s) ne = do - (_, arg, res) <- expectPi defs !(computeElimType ctx f (noOr1 ne)) + (_, arg, res) <- expectPiE defs ctx !(computeElimType ctx f (noOr1 ne)) pure $ sub1 res (s :# arg) computeElimType ctx (CasePair {pair, ret, _}) _ = do pure $ sub1 ret pair computeElimType ctx (CaseEnum {tag, ret, _}) _ = do pure $ sub1 ret tag computeElimType ctx (f :% p) ne = do - (ty, _, _) <- expectEq defs !(computeElimType ctx f (noOr1 ne)) + (ty, _, _) <- expectEqE defs ctx !(computeElimType ctx f (noOr1 ne)) pure $ dsub1 ty p computeElimType ctx (_ :# ty) _ = do pure ty private covering - replaceEnd : TContext q 0 n -> + replaceEnd : EqContext q 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) <- expectEq defs !(computeElimType ctx e ne) + (ty, l, r) <- expectEqE defs ctx !(computeElimType ctx e ne) pure $ ends l r p :# dsub1 ty (K p) namespace Elim @@ -319,9 +324,9 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)} ||| ⚠ **assumes that they have both been typechecked, and have ||| equal types.** ⚠ export covering %inline - compare0 : TContext q 0 n -> (e, f : Elim q 0 n) -> m () + compare0 : EqContext q n -> (e, f : Elim q 0 n) -> m () compare0 ctx e f = - wrapErr (WhileComparingE (MkTyContext new ctx) !mode e f) $ do + wrapErr (WhileComparingE ctx !mode e f) $ do Element e ne <- whnfT defs e Element f nf <- whnfT defs f -- [fixme] there is a better way to do this "isSubSing" stuff for sure @@ -329,7 +334,7 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)} compare0' ctx e f ne nf private covering - compare0' : TContext q 0 n -> + compare0' : EqContext q n -> (e, f : Elim q 0 n) -> (0 ne : NotRedex defs e) -> (0 nf : NotRedex defs f) -> m () @@ -342,38 +347,40 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)} compare0' ctx e (f :% K q) ne 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@(F x) f@(F y) _ _ = unless (x == y) $ clashE ctx e f + compare0' ctx e@(F _) f _ _ = clashE ctx e f - compare0' ctx e@(B i) f@(B j) _ _ = unless (i == j) $ clashE e f - compare0' _ e@(B _) f _ _ = clashE e f + compare0' ctx e@(B i) f@(B j) _ _ = unless (i == j) $ clashE ctx e f + compare0' ctx e@(B _) f _ _ = clashE ctx e f compare0' ctx (e :@ s) (f :@ t) ne nf = local {mode := Equal} $ do compare0 ctx e f - (_, arg, _) <- expectPi defs !(computeElimType ctx e (noOr1 ne)) + (_, arg, _) <- expectPiE defs ctx !(computeElimType ctx e (noOr1 ne)) Term.compare0 ctx arg s t - compare0' _ e@(_ :@ _) f _ _ = clashE e f + compare0' ctx e@(_ :@ _) f _ _ = clashE ctx e f compare0' ctx (CasePair epi e eret ebody) (CasePair fpi f fret fbody) ne nf = local {mode := Equal} $ do compare0 ctx e f ety <- computeElimType ctx e (noOr1 ne) - compareType (ctx :< ety) eret.term fret.term - (fst, snd) <- expectSig defs ety - Term.compare0 (ctx :< fst :< snd.term) (substCasePairRet ety eret) - ebody.term fbody.term + compareType (extendTy eret.name ety ctx) eret.term fret.term + (fst, snd) <- expectSigE defs ctx ety + let [x, y] = ebody.names + Term.compare0 (extendTyN [< (x, fst), (y, snd.term)] ctx) + (substCasePairRet ety eret) + ebody.term fbody.term expectEqualQ epi fpi - compare0' _ e@(CasePair {}) f _ _ = clashE e f + compare0' ctx e@(CasePair {}) f _ _ = clashE ctx e f compare0' ctx (CaseEnum epi e eret earms) (CaseEnum fpi f fret farms) ne nf = local {mode := Equal} $ do compare0 ctx e f ety <- computeElimType ctx e (noOr1 ne) - compareType (ctx :< ety) eret.term fret.term - for_ !(expectEnum defs ety) $ \t => + compareType (extendTy eret.name ety ctx) eret.term fret.term + for_ !(expectEnumE defs ctx ety) $ \t => compare0 ctx (sub1 eret $ Tag t :# ety) !(lookupArm t earms) !(lookupArm t farms) expectEqualQ epi fpi @@ -382,7 +389,7 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)} lookupArm t arms = case lookup t arms of Just arm => pure arm Nothing => throwError $ TagNotIn t (fromList $ keys arms) - compare0' _ e@(CaseEnum {}) f _ _ = clashE e f + compare0' ctx e@(CaseEnum {}) f _ _ = clashE ctx e f compare0' ctx (s :# a) (t :# b) _ _ = Term.compare0 ctx !(bigger a b) s t @@ -392,10 +399,13 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)} compare0' ctx (s :# a) f _ _ = Term.compare0 ctx a s (E f) compare0' ctx e (t :# b) _ _ = Term.compare0 ctx b (E e) t - compare0' _ e@(_ :# _) f _ _ = clashE e f + compare0' ctx e@(_ :# _) f _ _ = clashE ctx e f parameters {auto _ : (HasDefs' q _ m, HasErr q m, Eq q)} (ctx : TyContext q d n) + -- [todo] only split on the dvars that are actually used anywhere in + -- the calls to `splits` + parameters (mode : EqMode) namespace Term export covering @@ -404,8 +414,8 @@ parameters {auto _ : (HasDefs' q _ m, HasErr q m, Eq q)} (ctx : TyContext q d n) defs <- ask runReaderT {m} (MkCmpContext {mode}) $ for_ (splits ctx.dctx) $ \th => - compare0 defs (map (// th) ctx.tctx) - (ty // th) (s // th) (t // th) + let ectx = makeEqContext ctx th in + compare0 defs ectx (ty // th) (s // th) (t // th) export covering compareType : (s, t : Term q d n) -> m () @@ -413,7 +423,8 @@ parameters {auto _ : (HasDefs' q _ m, HasErr q m, Eq q)} (ctx : TyContext q d n) defs <- ask runReaderT {m} (MkCmpContext {mode}) $ for_ (splits ctx.dctx) $ \th => - compareType defs (map (// th) ctx.tctx) (s // th) (t // th) + let ectx = makeEqContext ctx th in + compareType defs ectx (s // th) (t // th) namespace Elim ||| you don't have to pass the type in but the arguments must still be @@ -424,7 +435,8 @@ parameters {auto _ : (HasDefs' q _ m, HasErr q m, Eq q)} (ctx : TyContext q d n) defs <- ask runReaderT {m} (MkCmpContext {mode}) $ for_ (splits ctx.dctx) $ \th => - compare0 defs (map (// th) ctx.tctx) (e // th) (f // th) + let ectx = makeEqContext ctx th in + compare0 defs ectx (e // th) (f // th) namespace Term export covering %inline diff --git a/lib/Quox/Syntax/DimEq.idr b/lib/Quox/Syntax/DimEq.idr index f13ae14..39a2383 100644 --- a/lib/Quox/Syntax/DimEq.idr +++ b/lib/Quox/Syntax/DimEq.idr @@ -60,6 +60,16 @@ ifConsistent ZeroIsOne act = pure Nothing ifConsistent (C _) act = Just <$> act +export +fromGround' : Context' DimConst d -> DimEq' d +fromGround' [<] = [<] +fromGround' (ctx :< e) = fromGround' ctx :< Just (K e) + +export +fromGround : Context' DimConst d -> DimEq d +fromGround = C . fromGround' + + export %inline zeroEq : DimEq 0 zeroEq = C [<] diff --git a/lib/Quox/Syntax/Subst.idr b/lib/Quox/Syntax/Subst.idr index 39110a7..6e6ecd4 100644 --- a/lib/Quox/Syntax/Subst.idr +++ b/lib/Quox/Syntax/Subst.idr @@ -58,6 +58,10 @@ public export %inline shift : (by : Nat) -> Subst env from (by + from) shift by = Shift $ fromNat by +public export %inline +shift0 : (by : Nat) -> Subst env 0 by +shift0 by = rewrite sym $ plusZeroRightNeutral by in Shift $ fromNat by + public export (.) : CanSubstSelf f => Subst f from mid -> Subst f mid to -> Subst f from to diff --git a/lib/Quox/Syntax/Term/Base.idr b/lib/Quox/Syntax/Term/Base.idr index f694ace..18434da 100644 --- a/lib/Quox/Syntax/Term/Base.idr +++ b/lib/Quox/Syntax/Term/Base.idr @@ -165,6 +165,14 @@ public export %inline SY : Vect s BaseName -> f (s + n) -> Scoped s f n SY ns = S ns . Y +public export %inline +name : Scoped 1 f n -> BaseName +name (S [x] _) = x + +public export %inline +(.name) : Scoped 1 f n -> BaseName +s.name = name s + ||| more convenient Pi public export %inline Pi_ : (qty : q) -> (x : BaseName) -> diff --git a/lib/Quox/Typechecker.idr b/lib/Quox/Typechecker.idr index 21846fb..cc27f22 100644 --- a/lib/Quox/Typechecker.idr +++ b/lib/Quox/Typechecker.idr @@ -3,6 +3,8 @@ module Quox.Typechecker import public Quox.Typing import public Quox.Equal +import Data.List + %default total @@ -107,7 +109,7 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m} (subj : Term q d n) -> (0 nc : NotClo subj) => Term q d n -> m (CheckResult' q n) toCheckType ctx sg t ty = do - u <- expectTYPE !ask ty + u <- expectTYPE !ask ctx ty expectEqualQ zero sg.fst checkTypeNoWrap ctx t (Just u) pure $ zeroFor ctx @@ -122,18 +124,18 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m} check' ctx sg t@(Pi {}) ty = toCheckType ctx sg t ty check' ctx sg (Lam body) ty = do - (qty, arg, res) <- expectPi !ask ty + (qty, arg, res) <- expectPi !ask ctx ty -- if Ψ | Γ, x : A ⊢ σ · t ⇐ B ⊳ Σ, ρ·x -- with ρ ≤ σπ let qty' = sg.fst * qty - qout <- checkC (extendTy arg ctx) sg body.term res.term + qout <- checkC (extendTy body.name arg ctx) sg body.term res.term -- then Ψ | Γ ⊢ σ · (λx ⇒ t) ⇐ (π·x : A) → B ⊳ Σ popQ qty' qout check' ctx sg t@(Sig {}) ty = toCheckType ctx sg t ty check' ctx sg (Pair fst snd) ty = do - (tfst, tsnd) <- expectSig !ask ty + (tfst, tsnd) <- expectSig !ask ctx ty -- if Ψ | Γ ⊢ σ · s ⇐ A ⊳ Σ₁ qfst <- checkC ctx sg fst tfst let tsnd = sub1 tsnd (fst :# tfst) @@ -145,7 +147,7 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m} check' ctx sg t@(Enum _) ty = toCheckType ctx sg t ty check' ctx sg (Tag t) ty = do - tags <- expectEnum !ask ty + tags <- expectEnum !ask ctx ty -- if t ∈ ts unless (t `elem` tags) $ throwError $ TagNotIn t tags -- then Ψ | Γ ⊢ σ · t ⇐ {ts} ⊳ 𝟎 @@ -154,9 +156,9 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m} check' ctx sg t@(Eq {}) ty = toCheckType ctx sg t ty check' ctx sg (DLam body) ty = do - (ty, l, r) <- expectEq !ask ty + (ty, l, r) <- expectEq !ask ctx ty -- if Ψ, i | Γ ⊢ σ · t ⇐ A ⊳ Σ - qout <- checkC (extendDim ctx) sg body.term ty.term + qout <- checkC (extendDim body.name ctx) sg body.term ty.term -- if Ψ | Γ ⊢ t‹0› = l : A‹0› equal ctx ty.zero body.zero l -- if Ψ | Γ ⊢ t‹1› = r : A‹1› @@ -188,36 +190,36 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m} checkTypeC ctx arg u -- if Ψ | Γ, x : A ⊢₀ B ⇐ Type ℓ case res.body of - Y res => checkTypeC (extendTy arg ctx) res u - N res => checkTypeC ctx res u + Y res' => checkTypeC (extendTy res.name arg ctx) res' u + N res' => checkTypeC ctx res' u -- then Ψ | Γ ⊢₀ (π·x : A) → B ⇐ Type ℓ checkType' ctx t@(Lam {}) u = - throwError $ NotType t + throwError $ NotType ctx t checkType' ctx (Sig fst snd) u = do -- if Ψ | Γ ⊢₀ A ⇐ Type ℓ checkTypeC ctx fst u -- if Ψ | Γ, x : A ⊢₀ B ⇐ Type ℓ case snd.body of - Y snd => checkTypeC (extendTy fst ctx) snd u - N snd => checkTypeC ctx snd u + Y snd' => checkTypeC (extendTy snd.name fst ctx) snd' u + N snd' => checkTypeC ctx snd' u -- then Ψ | Γ ⊢₀ (x : A) × B ⇐ Type ℓ checkType' ctx t@(Pair {}) u = - throwError $ NotType t + throwError $ NotType ctx t checkType' ctx (Enum _) u = pure () -- Ψ | Γ ⊢₀ {ts} ⇐ Type ℓ checkType' ctx t@(Tag {}) u = - throwError $ NotType t + throwError $ NotType ctx t checkType' ctx (Eq t l r) u = do -- if Ψ, i | Γ ⊢₀ A ⇐ Type ℓ case t.body of - Y t => checkTypeC (extendDim ctx) t u - N t => checkTypeC ctx t u + Y t' => checkTypeC (extendDim t.name ctx) t' u + N t' => checkTypeC ctx t' u -- if Ψ | Γ ⊢₀ l ⇐ A‹0› check0 ctx t.zero l -- if Ψ | Γ ⊢₀ r ⇐ A‹1› @@ -225,7 +227,7 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m} -- then Ψ | Γ ⊢₀ Eq [i ⇒ A] l r ⇐ Type ℓ checkType' ctx t@(DLam {}) u = - throwError $ NotType t + throwError $ NotType ctx t checkType' ctx (E e) u = do -- if Ψ | Γ ⊢ σ · e ⇒ A' ⊳ Σ @@ -233,7 +235,7 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m} -- if Ψ | Γ ⊢ A' <: A case u of Just u => subtype ctx infres.type (TYPE u) - Nothing => ignore $ expectTYPE !ask infres.type + Nothing => ignore $ expectTYPE !ask ctx infres.type -- then Ψ | Γ ⊢ σ · e ⇐ A ⊳ Σ @@ -268,7 +270,7 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m} infer' ctx sg (fun :@ arg) = do -- if Ψ | Γ ⊢ σ · f ⇒ (π·x : A) → B ⊳ Σ₁ funres <- inferC ctx sg fun - (qty, argty, res) <- expectPi !ask funres.type + (qty, argty, res) <- expectPi !ask ctx funres.type -- if Ψ | Γ ⊢ σ ⨴ π · s ⇐ A ⊳ Σ₂ argout <- checkC ctx (subjMult sg qty) arg argty -- then Ψ | Γ ⊢ σ · f s ⇒ B[s] ⊳ Σ₁ + Σ₂ @@ -283,12 +285,13 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m} -- if Ψ | Γ ⊢ σ · pair ⇒ (x : A) × B ⊳ Σ₁ pairres <- inferC ctx sg pair -- if Ψ | Γ, p : (x : A) × B ⊢₀ ret ⇐ Type - checkTypeC (extendTy pairres.type ctx) ret.term Nothing - (tfst, tsnd) <- expectSig !ask pairres.type + checkTypeC (extendTy ret.name pairres.type ctx) ret.term Nothing + (tfst, tsnd) <- expectSig !ask ctx pairres.type -- if Ψ | Γ, x : A, y : B ⊢ σ · body ⇐ -- ret[(x, y) ∷ (x : A) × B/p] ⊳ Σ₂, ρ₁·x, ρ₂·y -- with ρ₁, ρ₂ ≤ πσ - let bodyctx = extendTyN [< tfst, tsnd.term] ctx + let [x, y] = body.names + bodyctx = extendTyN [< (x, tfst), (y, tsnd.term)] ctx bodyty = substCasePairRet pairres.type ret pisg = pi * sg.fst bodyout <- checkC bodyctx sg body.term bodyty @@ -298,35 +301,36 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m} qout = pi * pairres.qout + !(popQs [< pisg, pisg] bodyout) } - infer' ctx sg (CaseEnum pi t ret arms) {n} = do + infer' ctx sg (CaseEnum pi t ret arms) {d, n} = do -- if 1 ≤ π expectCompatQ one pi -- if Ψ | Γ ⊢ σ · t ⇒ {ts} ⊳ Σ₁ tres <- inferC ctx sg t -- if Ψ | Γ, x : {ts} ⊢₀ A ⇐ Type - checkTypeC (extendTy tres.type ctx) ret.term Nothing + checkTypeC (extendTy ret.name tres.type ctx) ret.term Nothing -- if for each "a ⇒ s" in arms, -- Ψ | Γ ⊢ σ · s ⇐ A[a ∷ {ts}/x] ⊳ Σ₂ -- for fixed Σ₂ - armres <- for (SortedMap.toList arms) $ \(a, s) => + let arms = SortedMap.toList arms + armres <- for arms $ \(a, s) => checkC ctx sg s (sub1 ret (Tag a :# tres.type)) - armout <- allEqual armres + armout <- allEqual (zip armres arms) -- then Ψ | Γ ⊢ σ · case ⋯ ⇒ ret[t/x] ⊳ πΣ₁ + Σ₂ pure $ InfRes { type = sub1 ret t, qout = pi * tres.qout + armout } where - allEqual : List (QOutput q n) -> m (QOutput q n) + allEqual : List (QOutput q n, TagVal, Term q d n) -> m (QOutput q n) allEqual [] = pure $ zeroFor ctx - allEqual lst@(x :: xs) = - if all (== x) xs then pure x - else throwError $ BadCaseQtys lst + allEqual lst@((x, _) :: xs) = + if all (\y => x == fst y) xs then pure x + else throwError $ BadCaseQtys ctx lst infer' ctx sg (fun :% dim) = do -- if Ψ | Γ ⊢ σ · f ⇒ Eq [i ⇒ A] l r ⊳ Σ InfRes {type, qout} <- inferC ctx sg fun - ty <- fst <$> expectEq !ask type + ty <- fst <$> expectEq !ask ctx 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 6eb081e..94a1b13 100644 --- a/lib/Quox/Typing.idr +++ b/lib/Quox/Typing.idr @@ -11,53 +11,6 @@ import public Quox.Reduce %default total -namespace TContext - export %inline - pushD : TContext q d n -> TContext q (S d) n - pushD tel = map (// shift 1) tel - - export %inline - zeroFor : IsQty q => Context tm n -> QOutput q n - zeroFor ctx = zero <$ ctx - -namespace TyContext - public export %inline - empty : {d : Nat} -> TyContext q d 0 - empty = MkTyContext {dctx = new, tctx = [<]} - - export %inline - extendTyN : Telescope (Term q d) from to -> - TyContext q d from -> TyContext q d to - extendTyN ss = {tctx $= (. ss)} - - export %inline - extendTy : Term q d n -> TyContext q d n -> TyContext q d (S n) - extendTy s = extendTyN [< s] - - export %inline - extendDim : TyContext q d n -> TyContext q (S d) n - extendDim = {dctx $= (: Dim d -> TyContext q d n -> TyContext q d n - eqDim p q = {dctx $= set p q} - - -namespace QOutput - parameters {auto _ : IsQty q} - export %inline - (+) : QOutput q n -> QOutput q n -> QOutput q n - (+) = zipWith (+) - - export %inline - (*) : q -> QOutput q n -> QOutput q n - (*) pi = map (pi *) - - export %inline - zeroFor : TyContext q _ n -> QOutput q n - zeroFor ctx = zeroFor ctx.tctx - - public export CheckResult' : Type -> Nat -> Type CheckResult' = QOutput @@ -98,37 +51,89 @@ parameters {auto _ : HasErr q m} (defs : Definitions' q _) tm q d n -> m (NonRedex tm q d n defs) whnfT = either (throwError . WhnfError) pure . whnf defs - export covering %inline - expectTYPE : Term q d n -> m Universe - expectTYPE s = - case fst !(whnfT s) of + parameters (ctx : Lazy (TyContext q d1 n)) (th : Lazy (DSubst d2 d1)) + export covering %inline + expectTYPE_ : Term q d2 n -> m Universe + expectTYPE_ s = case fst !(whnfT s) of TYPE l => pure l - _ => throwError $ ExpectedTYPE s + _ => throwError $ ExpectedTYPE ctx (s // th) - export covering %inline - expectPi : Term q d n -> m (q, Term q d n, ScopeTerm q d n) - expectPi s = - case fst !(whnfT s) of + export covering %inline + expectPi_ : Term q d2 n -> m (q, Term q d2 n, ScopeTerm q d2 n) + expectPi_ s = case fst !(whnfT s) of Pi {qty, arg, res, _} => pure (qty, arg, res) - _ => throwError $ ExpectedPi s + _ => throwError $ ExpectedPi ctx (s // th) - export covering %inline - expectSig : Term q d n -> m (Term q d n, ScopeTerm q d n) - expectSig s = - case fst !(whnfT s) of + export covering %inline + expectSig_ : Term q d2 n -> m (Term q d2 n, ScopeTerm q d2 n) + expectSig_ s = case fst !(whnfT s) of Sig {fst, snd, _} => pure (fst, snd) - _ => throwError $ ExpectedSig s + _ => throwError $ ExpectedSig ctx (s // th) - export covering %inline - expectEnum : Term q d n -> m (SortedSet TagVal) - expectEnum s = - case fst !(whnfT s) of + export covering %inline + expectEnum_ : Term q d2 n -> m (SortedSet TagVal) + expectEnum_ s = case fst !(whnfT s) of Enum tags => pure tags - _ => throwError $ ExpectedEnum s + _ => throwError $ ExpectedEnum ctx (s // th) - 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 !(whnfT s) of + export covering %inline + expectEq_ : Term q d2 n -> m (DScopeTerm q d2 n, Term q d2 n, Term q d2 n) + expectEq_ s = case fst !(whnfT s) of Eq {ty, l, r, _} => pure (ty, l, r) - _ => throwError $ ExpectedEq s + _ => throwError $ ExpectedEq ctx (s // th) + + + -- [fixme] refactor this stuff + + parameters (ctx : TyContext q d n) + export covering %inline + expectTYPE : Term q d n -> m Universe + expectTYPE = expectTYPE_ ctx id + + export covering %inline + expectPi : Term q d n -> m (q, Term q d n, ScopeTerm q d n) + expectPi = expectPi_ ctx id + + export covering %inline + expectSig : Term q d n -> m (Term q d n, ScopeTerm q d n) + expectSig = expectSig_ ctx id + + export covering %inline + expectEnum : Term q d n -> m (SortedSet TagVal) + expectEnum = expectEnum_ ctx id + + export covering %inline + expectEq : Term q d n -> m (DScopeTerm q d n, Term q d n, Term q d n) + expectEq = expectEq_ ctx id + + + parameters (ctx : EqContext q n) + export covering %inline + expectTYPEE : Term q 0 n -> m Universe + expectTYPEE t = + let ctx = delay (toTyContext ctx) in + expectTYPE_ (DPair.snd ctx) (shift0 $ DPair.fst ctx) t + + export covering %inline + expectPiE : Term q 0 n -> m (q, Term q 0 n, ScopeTerm q 0 n) + expectPiE t = + let ctx = delay (toTyContext ctx) in + expectPi_ (DPair.snd ctx) (shift0 $ DPair.fst ctx) t + + export covering %inline + expectSigE : Term q 0 n -> m (Term q 0 n, ScopeTerm q 0 n) + expectSigE t = + let ctx = delay (toTyContext ctx) in + expectSig_ (DPair.snd ctx) (shift0 $ DPair.fst ctx) t + + export covering %inline + expectEnumE : Term q 0 n -> m (SortedSet TagVal) + expectEnumE t = + let ctx = delay (toTyContext ctx) in + expectEnum_ (DPair.snd ctx) (shift0 $ DPair.fst ctx) t + + export covering %inline + expectEqE : Term q 0 n -> m (DScopeTerm q 0 n, Term q 0 n, Term q 0 n) + expectEqE t = + let ctx = delay (toTyContext ctx) in + expectEq_ (DPair.snd ctx) (shift0 $ DPair.fst ctx) t diff --git a/lib/Quox/Typing/Context.idr b/lib/Quox/Typing/Context.idr index 6538de2..53807c8 100644 --- a/lib/Quox/Typing/Context.idr +++ b/lib/Quox/Typing/Context.idr @@ -3,6 +3,8 @@ module Quox.Typing.Context import Quox.Syntax import Quox.Context +%default total + public export TContext : Type -> Nat -> Nat -> Type @@ -12,11 +14,125 @@ public export QOutput : Type -> Nat -> Type QOutput = Context' +public export +NContext : Nat -> Type +NContext = Context' BaseName + +public export +DimAssign : Nat -> Type +DimAssign = Context' DimConst + public export record TyContext q d n where constructor MkTyContext - dctx : DimEq d - tctx : TContext q d n - + dctx : DimEq d + dnames : NContext d + tctx : TContext q d n + tnames : NContext n %name TyContext ctx + + +public export +record EqContext q n where + constructor MkEqContext + -- (only used for errors; not needed by the actual equality test) + dassign : DimAssign dimLen + dnames : NContext dimLen + tctx : TContext q 0 n + tnames : NContext n +%name EqContext ctx + + +namespace TContext + export %inline + pushD : TContext q d n -> TContext q (S d) n + pushD tel = map (// shift 1) tel + + export %inline + zeroFor : IsQty q => Context tm n -> QOutput q n + zeroFor ctx = zero <$ ctx + +namespace TyContext + public export %inline + empty : TyContext q 0 0 + empty = MkTyContext {dctx = new, dnames = [<], tctx = [<], tnames = [<]} + + export %inline + extendTyN : Telescope (\n => (BaseName, Term q d n)) from to -> + TyContext q d from -> TyContext q d to + extendTyN xss ctx = + let (xs, ss) = unzip xss in {tctx $= (. ss), tnames $= (. xs)} ctx + + export %inline + extendTy : BaseName -> Term q d n -> TyContext q d n -> TyContext q d (S n) + extendTy x s = extendTyN [< (x, s)] + + export %inline + extendDim : BaseName -> TyContext q d n -> TyContext q (S d) n + extendDim x = {dctx $= (: Dim d -> TyContext q d n -> TyContext q d n + eqDim p q = {dctx $= set p q} + + +namespace QOutput + parameters {auto _ : IsQty q} + export %inline + (+) : QOutput q n -> QOutput q n -> QOutput q n + (+) = zipWith (+) + + export %inline + (*) : q -> QOutput q n -> QOutput q n + (*) pi = map (pi *) + + export %inline + zeroFor : TyContext q _ n -> QOutput q n + zeroFor ctx = zeroFor ctx.tctx + + +export +makeDAssign : DSubst d 0 -> DimAssign d +makeDAssign (Shift SZ) = [<] +makeDAssign (K e ::: th) = makeDAssign th :< e + +export +makeEqContext : TyContext q d n -> DSubst d 0 -> EqContext q n +makeEqContext ctx th = MkEqContext { + dassign = makeDAssign th, + dnames = ctx.dnames, + tctx = map (// th) ctx.tctx, + tnames = ctx.tnames +} + +namespace EqContext + public export %inline + empty : EqContext q 0 + empty = MkEqContext [<] [<] [<] [<] + + export %inline + extendTyN : Telescope (\n => (BaseName, Term q 0 n)) from to -> + EqContext q from -> EqContext q to + extendTyN tel ctx = + let (xs, ss) = unzip tel in {tctx $= (. ss), tnames $= (. xs)} ctx + + export %inline + extendTy : BaseName -> Term q 0 n -> EqContext q n -> EqContext q (S n) + extendTy x s = extendTyN [< (x, s)] + + export %inline + extendDim : BaseName -> DimConst -> EqContext q n -> EqContext q n + extendDim x e ctx = {dassign $= (:< e), dnames $= (:< x)} ctx + + export + toTyContext : (e : EqContext q n) -> (d ** TyContext q d n) + toTyContext (MkEqContext {dassign, dnames, tctx, tnames}) + with (lengthPrf0 dnames) + _ | Element d eq = + (d ** MkTyContext { + dctx = rewrite eq in fromGround dassign, + dnames = rewrite eq in dnames, + tctx = map (// shift0 d) tctx, + tnames + }) diff --git a/lib/Quox/Typing/Error.idr b/lib/Quox/Typing/Error.idr index 1e5fe90..9f1e131 100644 --- a/lib/Quox/Typing/Error.idr +++ b/lib/Quox/Typing/Error.idr @@ -12,26 +12,25 @@ import public Control.Monad.Either public export data Error q -= ExpectedTYPE (Term q d n) -| ExpectedPi (Term q d n) -| ExpectedSig (Term q d n) -| ExpectedEnum (Term q d n) -| ExpectedEq (Term q d n) += ExpectedTYPE (TyContext q d n) (Term q d n) +| ExpectedPi (TyContext q d n) (Term q d n) +| ExpectedSig (TyContext q d n) (Term q d n) +| ExpectedEnum (TyContext q d n) (Term q d n) +| ExpectedEq (TyContext q d n) (Term q d n) | BadUniverse Universe Universe | TagNotIn TagVal (SortedSet TagVal) -| BadCaseQtys (List (QOutput q n)) +| BadCaseQtys (TyContext q d n) (List (QOutput q n, TagVal, Term q d n)) --- first arg of ClashT is the type -| ClashT EqMode (Term q d n) (Term q d n) (Term q d n) -| ClashTy EqMode (Term q d n) (Term q d n) -| ClashE EqMode (Elim q d n) (Elim q d n) -| ClashU EqMode Universe Universe -| ClashQ q q -| ClashD (Dim d) (Dim d) -| NotInScope Name +-- first term arg of ClashT is the type +| ClashT (EqContext q n) EqMode (Term q 0 n) (Term q 0 n) (Term q 0 n) +| ClashTy (EqContext q n) EqMode (Term q 0 n) (Term q 0 n) +| ClashE (EqContext q n) EqMode (Elim q 0 n) (Elim q 0 n) +| ClashU EqMode Universe Universe +| ClashQ q q +| NotInScope Name -| NotType (Term q d n) -| WrongType (Term q d n) (Term q d n) (Term q d n) +| NotType (TyContext q d n) (Term q d n) +| WrongType (EqContext q n) (Term q 0 n) (Term q 0 n) (Term q 0 n) -- extra context | WhileChecking @@ -49,13 +48,13 @@ data Error q (Elim q d n) (Error q) | WhileComparingT - (TyContext q d n) EqMode - (Term q d n) -- type - (Term q d n) (Term q d n) -- lhs/rhs + (EqContext q n) EqMode + (Term q 0 n) -- type + (Term q 0 n) (Term q 0 n) -- lhs/rhs (Error q) | WhileComparingE - (TyContext q d n) EqMode - (Elim q d n) (Elim q d n) + (EqContext q n) EqMode + (Elim q 0 n) (Elim q 0 n) (Error q) | WhnfError WhnfError @@ -137,6 +136,3 @@ parameters {auto _ : HasErr q m} expectModeU : EqMode -> Universe -> Universe -> m () expectModeU mode = expect (ClashU mode) $ ucmp mode - export %inline - expectEqualD : Dim d -> Dim d -> m () - expectEqualD = expect ClashD (==) diff --git a/tests/Tests/Equal.idr b/tests/Tests/Equal.idr index af52df0..9bc1c58 100644 --- a/tests/Tests/Equal.idr +++ b/tests/Tests/Equal.idr @@ -46,6 +46,8 @@ parameters (ctx : TyContext Three 0 n) subE = subED 0 ctx equalE = equalED 0 ctx +empty01 : TyContext q 0 0 +empty01 = {dctx := ZeroIsOne} empty export @@ -116,7 +118,7 @@ tests = "equality & subtyping" :- [ testEq "0=1 ⊢ A ⇾ B = A ⊸ B" $ let tm1 = Arr Zero (FT "A") (FT "B") tm2 = Arr One (FT "A") (FT "B") in - equalT (MkTyContext ZeroIsOne [<]) (TYPE 0) tm1 tm2, + equalT empty01 (TYPE 0) tm1 tm2, todo "dependent function types", note "[todo] should π ≤ ρ ⊢ (ρ·A) → B <: (π·A) → B?" ], @@ -182,47 +184,54 @@ tests = "equality & subtyping" :- [ 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 (MkTyContext new [< ty, ty]) (BV 0) (BV 1), + equalE (extendTyN [< ("x", ty), ("y", ty)] empty) + (BV 0) (BV 1), testEq "∥ x : [(a ≡ a' : A) ∷ Type 0], y : [ditto] ⊢ x = y" $ let ty : forall n. Term Three 0 n := E (Eq0 (FT "A") (FT "a") (FT "a'") :# TYPE 0) in - equalE (MkTyContext new [< ty, ty]) (BV 0) (BV 1), + equalE (extendTyN [< ("x", ty), ("y", ty)] empty) + (BV 0) (BV 1), testEq "E ≔ a ≡ a' : A, EE ≔ E ∥ x : EE, y : EE ⊢ x = y" {globals = defGlobals `mergeLeft` fromList [("E", mkDef zero (TYPE 0) (Eq0 (FT "A") (FT "a") (FT "a'"))), ("EE", mkDef zero (TYPE 0) (FT "E"))]} $ - equalE (MkTyContext new [< FT "EE", FT "EE"]) (BV 0) (BV 1), + equalE (extendTyN [< ("x", FT "EE"), ("y", FT "EE")] empty) + (BV 0) (BV 1), testEq "E ≔ a ≡ a' : A, EE ≔ E ∥ x : EE, y : E ⊢ x = y" {globals = defGlobals `mergeLeft` fromList [("E", mkDef zero (TYPE 0) (Eq0 (FT "A") (FT "a") (FT "a'"))), ("EE", mkDef zero (TYPE 0) (FT "E"))]} $ - equalE (MkTyContext new [< FT "EE", FT "E"]) (BV 0) (BV 1), + equalE (extendTyN [< ("x", FT "EE"), ("y", FT "E")] empty) + (BV 0) (BV 1), testEq "E ≔ a ≡ a' : A ∥ x : E, y : E ⊢ x = y" {globals = defGlobals `mergeLeft` fromList [("E", mkDef zero (TYPE 0) (Eq0 (FT "A") (FT "a") (FT "a'")))]} $ - equalE (MkTyContext new [< FT "E", FT "E"]) (BV 0) (BV 1), + equalE (extendTyN [< ("x", FT "E"), ("y", FT "E")] empty) (BV 0) (BV 1), testEq "E ≔ a ≡ a' : A ∥ x : (E×E), y : (E×E) ⊢ x = y" {globals = defGlobals `mergeLeft` fromList [("E", mkDef zero (TYPE 0) (Eq0 (FT "A") (FT "a") (FT "a'")))]} $ let ty : forall n. Term Three 0 n := Sig (FT "E") $ S ["_"] $ N $ FT "E" in - equalE (MkTyContext new [< ty, ty]) (BV 0) (BV 1), + equalE (extendTyN [< ("x", ty), ("y", ty)] empty) (BV 0) (BV 1), - testEq "E ≔ a ≡ a' : A, F ≔ E × E ∥ x : F, y : F ⊢ x = y" + testEq "E ≔ a ≡ a' : A, W ≔ E × E ∥ x : W, y : W ⊢ x = y" {globals = defGlobals `mergeLeft` fromList [("E", mkDef zero (TYPE 0) (Eq0 (FT "A") (FT "a") (FT "a'"))), ("W", mkDef zero (TYPE 0) (FT "E" `And` FT "E"))]} $ - equalE (MkTyContext new [< FT "W", FT "W"]) (BV 0) (BV 1) + equalE + (extendTyN [< ("x", FT "W"), ("y", FT "W")] empty) + (BV 0) (BV 1) ], "term closure" :- [ testEq "[#0]{} = [#0] : A" $ - equalT (MkTyContext new [< FT "A"]) (FT "A") + equalT (extendTy "x" (FT "A") empty) + (FT "A") (CloT (BVT 0) id) (BVT 0), testEq "[#0]{a} = [a] : A" $ @@ -249,9 +258,12 @@ tests = "equality & subtyping" :- [ "term d-closure" :- [ testEq "★₀‹𝟎› = ★₀ : ★₁" $ - equalTD 1 empty (TYPE 1) (DCloT (TYPE 0) (K Zero ::: id)) (TYPE 0), + equalTD 1 + (extendDim "𝑗" empty) + (TYPE 1) (DCloT (TYPE 0) (K Zero ::: id)) (TYPE 0), testEq "(δ i ⇒ a)‹𝟎› = (δ i ⇒ a) : (a ≡ a : A)" $ - equalTD 1 empty + equalTD 1 + (extendDim "𝑗" empty) (Eq0 (FT "A") (FT "a") (FT "a")) (DCloT (["i"] :\\% FT "a") (K Zero ::: id)) (["i"] :\\% FT "a"), @@ -271,7 +283,7 @@ tests = "equality & subtyping" :- [ testNeq "A ≠ B" $ equalE empty (F "A") (F "B"), testEq "0=1 ⊢ A = B" $ - equalE (MkTyContext ZeroIsOne [<]) (F "A") (F "B"), + equalE empty01 (F "A") (F "B"), testEq "A : ★₁ ≔ ★₀ ⊢ A = (★₀ ∷ ★₁)" {globals = au_bu} $ equalE empty (F "A") (TYPE 0 :# TYPE 1), testEq "A : ★₁ ≔ ★₀ ⊢ [A] = ★₀" {globals = au_bu} $ @@ -294,20 +306,20 @@ tests = "equality & subtyping" :- [ ("B", mkDef Any (TYPE 3) (TYPE 2))]} $ subE empty (F "A") (F "B"), testEq "0=1 ⊢ A <: B" $ - subE (MkTyContext ZeroIsOne [<]) (F "A") (F "B") + subE empty01 (F "A") (F "B") ], "bound var" :- [ testEq "#0 = #0" $ - equalE (MkTyContext new [< TYPE 0]) (BV 0) (BV 0), + equalE (extendTy "A" (TYPE 0) empty) (BV 0) (BV 0), testEq "#0 <: #0" $ - subE (MkTyContext new [< TYPE 0]) (BV 0) (BV 0), + subE (extendTy "A" (TYPE 0) empty) (BV 0) (BV 0), testNeq "#0 ≠ #1" $ - equalE (MkTyContext new [< TYPE 0, TYPE 0]) (BV 0) (BV 1), + equalE (extendTyN [< ("A", TYPE 0), ("B", TYPE 0)] empty) (BV 0) (BV 1), testNeq "#0 ≮: #1" $ - subE (MkTyContext new [< TYPE 0, TYPE 0]) (BV 0) (BV 1), + subE (extendTyN [< ("A", TYPE 0), ("B", TYPE 0)] empty) (BV 0) (BV 1), testEq "0=1 ⊢ #0 = #1" $ - equalE (MkTyContext ZeroIsOne [< TYPE 0, TYPE 0]) (BV 0) (BV 1) + equalE (extendTyN [< ("A", TYPE 0), ("B", TYPE 0)] empty01) (BV 0) (BV 1) ], "application" :- [ @@ -343,26 +355,37 @@ tests = "equality & subtyping" :- [ testNeq "eq-AB @0 ≠ eq-AB @1" $ equalE empty (F "eq-AB" :% K Zero) (F "eq-AB" :% K One), testEq "𝑖 | ⊢ eq-AB @𝑖 = eq-AB @𝑖" $ - equalED 1 empty (F "eq-AB" :% BV 0) (F "eq-AB" :% BV 0), + equalED 1 + (extendDim "𝑖" empty) + (F "eq-AB" :% BV 0) (F "eq-AB" :% BV 0), testNeq "𝑖 | ⊢ eq-AB @𝑖 ≠ eq-AB @0" $ - equalED 1 empty (F "eq-AB" :% BV 0) (F "eq-AB" :% K Zero), + equalED 1 + (extendDim "𝑖" empty) + (F "eq-AB" :% BV 0) (F "eq-AB" :% K Zero), testEq "𝑖, 𝑖=0 | ⊢ eq-AB @𝑖 = eq-AB @0" $ - let ctx = MkTyContext (set (BV 0) (K Zero) new) [<] in - equalED 1 ctx (F "eq-AB" :% BV 0) (F "eq-AB" :% K Zero), + equalED 1 + (eqDim (BV 0) (K Zero) $ extendDim "𝑖" empty) + (F "eq-AB" :% BV 0) (F "eq-AB" :% K Zero), testNeq "𝑖, 𝑖=1 | ⊢ eq-AB @𝑖 ≠ eq-AB @0" $ - let ctx = MkTyContext (set (BV 0) (K One) new) [<] in - equalED 1 ctx (F "eq-AB" :% BV 0) (F "eq-AB" :% K Zero), + equalED 1 + (eqDim (BV 0) (K One) $ extendDim "𝑖" empty) + (F "eq-AB" :% BV 0) (F "eq-AB" :% K Zero), testNeq "𝑖, 𝑗 | ⊢ eq-AB @𝑖 ≠ eq-AB @𝑗" $ - equalED 2 empty (F "eq-AB" :% BV 1) (F "eq-AB" :% BV 0), + equalED 2 + (extendDim "𝑗" $ extendDim "𝑖" empty) + (F "eq-AB" :% BV 1) (F "eq-AB" :% BV 0), testEq "𝑖, 𝑗, 𝑖=𝑗 | ⊢ eq-AB @𝑖 = eq-AB @𝑗" $ - let ctx = MkTyContext (set (BV 0) (BV 1) new) [<] in - equalED 2 ctx (F "eq-AB" :% BV 1) (F "eq-AB" :% BV 0), - testNeq "𝑖, 𝑗, 𝑖=0, 𝑗=0 | ⊢ eq-AB @𝑖 ≠ eq-AB @𝑗" $ - let ctx : TyContext Three 2 0 := - MkTyContext (C [< Just $ K Zero, Just $ K Zero]) [<] in - equalED 2 empty (F "eq-AB" :% BV 1) (F "eq-AB" :% BV 0), + equalED 2 + (eqDim (BV 0) (BV 1) $ extendDim "𝑗" $ extendDim "𝑖" empty) + (F "eq-AB" :% BV 1) (F "eq-AB" :% BV 0), + testEq "𝑖, 𝑗, 𝑖=0, 𝑗=0 | ⊢ eq-AB @𝑖 = eq-AB @𝑗" $ + equalED 2 + (eqDim (BV 0) (K Zero) $ eqDim (BV 1) (K Zero) $ + extendDim "𝑗" $ extendDim "𝑖" empty) + (F "eq-AB" :% BV 1) (F "eq-AB" :% BV 0), testEq "0=1 | ⊢ eq-AB @𝑖 = eq-AB @𝑗" $ - equalED 2 (MkTyContext ZeroIsOne [<]) + equalED 2 + (extendDim "𝑗" $ extendDim "𝑖" empty01) (F "eq-AB" :% BV 1) (F "eq-AB" :% BV 0), testEq "eq-AB @0 = A" $ equalE empty (F "eq-AB" :% K Zero) (F "A"), testEq "eq-AB @1 = B" $ equalE empty (F "eq-AB" :% K One) (F "B"), @@ -393,38 +416,48 @@ tests = "equality & subtyping" :- [ testEq "#0{a} = a" $ equalE empty (CloE (BV 0) (F "a" ::: id)) (F "a"), testEq "#1{a} = #0" $ - equalE (MkTyContext new [< FT "A"]) + equalE (extendTy "x" (FT "A") empty) (CloE (BV 1) (F "a" ::: id)) (BV 0) ], "elim d-closure" :- [ note "0·eq-AB : (A ≡ B : ★₀)", testEq "(eq-AB #0)‹𝟎› = eq-AB 𝟎" $ - equalED 1 empty + equalED 1 + (extendDim "𝑖" empty) (DCloE (F "eq-AB" :% BV 0) (K Zero ::: id)) (F "eq-AB" :% K Zero), testEq "(eq-AB #0)‹𝟎› = A" $ - equalED 1 empty (DCloE (F "eq-AB" :% BV 0) (K Zero ::: id)) (F "A"), + equalED 1 + (extendDim "𝑖" empty) + (DCloE (F "eq-AB" :% BV 0) (K Zero ::: id)) (F "A"), testEq "(eq-AB #0)‹𝟏› = B" $ - equalED 1 empty (DCloE (F "eq-AB" :% BV 0) (K One ::: id)) (F "B"), + equalED 1 + (extendDim "𝑖" empty) + (DCloE (F "eq-AB" :% BV 0) (K One ::: id)) (F "B"), testNeq "(eq-AB #0)‹𝟏› ≠ A" $ - equalED 1 empty (DCloE (F "eq-AB" :% BV 0) (K One ::: id)) (F "A"), + equalED 1 + (extendDim "𝑖" empty) + (DCloE (F "eq-AB" :% BV 0) (K One ::: id)) (F "A"), testEq "(eq-AB #0)‹#0,𝟎› = (eq-AB #0)" $ - equalED 2 empty + equalED 2 + (extendDim "𝑗" $ extendDim "𝑖" empty) (DCloE (F "eq-AB" :% BV 0) (BV 0 ::: K Zero ::: id)) (F "eq-AB" :% BV 0), testNeq "(eq-AB #0)‹𝟎› ≠ (eq-AB 𝟎)" $ - equalED 2 empty + equalED 2 + (extendDim "𝑗" $ extendDim "𝑖" empty) (DCloE (F "eq-AB" :% BV 0) (BV 0 ::: K Zero ::: id)) (F "eq-AB" :% K Zero), testEq "#0‹𝟎› = #0 # term and dim vars distinct" $ - equalED 1 (MkTyContext new [< FT "A"]) + equalED 1 + (extendTy "x" (FT "A") $ extendDim "𝑖" empty) (DCloE (BV 0) (K Zero ::: id)) (BV 0), testEq "a‹𝟎› = a" $ - equalED 1 empty (DCloE (F "a") (K Zero ::: id)) (F "a"), + equalED 1 (extendDim "𝑖" empty) (DCloE (F "a") (K Zero ::: id)) (F "a"), testEq "(f [a])‹𝟎› = f‹𝟎› [a]‹𝟎›" $ let th = K Zero ::: id in - equalED 1 empty + equalED 1 (extendDim "𝑖" empty) (DCloE (F "f" :@ FT "a") th) (DCloE (F "f") th :@ DCloT (FT "a") th) ], @@ -433,8 +466,7 @@ tests = "equality & subtyping" :- [ testNeq "★₀ ≠ ★₀ ⇾ ★₀" $ equalT empty (TYPE 1) (TYPE 0) (Arr Zero (TYPE 0) (TYPE 0)), testEq "0=1 ⊢ ★₀ = ★₀ ⇾ ★₀" $ - equalT (MkTyContext ZeroIsOne [<]) - (TYPE 1) (TYPE 0) (Arr Zero (TYPE 0) (TYPE 0)), + equalT empty01 (TYPE 1) (TYPE 0) (Arr Zero (TYPE 0) (TYPE 0)), todo "others" ] ] diff --git a/tests/Tests/Typechecker.idr b/tests/Tests/Typechecker.idr index 6483e87..7aadb25 100644 --- a/tests/Tests/Typechecker.idr +++ b/tests/Tests/Typechecker.idr @@ -98,9 +98,12 @@ parameters (label : String) (act : Lazy (M ())) testTCFail = testThrows label (const True) $ runReaderT globals act -ctx, ctx01 : TContext Three 0 n -> TyContext Three 0 n -ctx = MkTyContext new -ctx01 = MkTyContext ZeroIsOne +ctx, ctx01 : Context (\n => (BaseName, Term Three 0 n)) n -> TyContext Three 0 n +ctx tel = MkTyContext new [<] (map snd tel) (map fst tel) +ctx01 tel = MkTyContext ZeroIsOne [<] (map snd tel) (map fst tel) + +empty01 : TyContext Three 0 0 +empty01 = {dctx := ZeroIsOne} empty inferredTypeEq : TyContext Three d n -> (exp, got : Term Three d n) -> M () inferredTypeEq ctx exp got = @@ -159,184 +162,184 @@ tests : Test tests = "typechecker" :- [ "universes" :- [ testTC "0 · ★₀ ⇐ ★₁ # by checkType" $ - checkType_ (ctx [<]) (TYPE 0) (Just 1), + checkType_ empty (TYPE 0) (Just 1), testTC "0 · ★₀ ⇐ ★₁ # by check" $ - check_ (ctx [<]) szero (TYPE 0) (TYPE 1), + check_ empty szero (TYPE 0) (TYPE 1), testTC "0 · ★₀ ⇐ ★₂" $ - checkType_ (ctx [<]) (TYPE 0) (Just 2), + checkType_ empty (TYPE 0) (Just 2), testTC "0 · ★₀ ⇐ ★_" $ - checkType_ (ctx [<]) (TYPE 0) Nothing, + checkType_ empty (TYPE 0) Nothing, testTCFail "0 · ★₁ ⇍ ★₀" $ - checkType_ (ctx [<]) (TYPE 1) (Just 0), + checkType_ empty (TYPE 1) (Just 0), testTCFail "0 · ★₀ ⇍ ★₀" $ - checkType_ (ctx [<]) (TYPE 0) (Just 0), + checkType_ empty (TYPE 0) (Just 0), testTC "0=1 ⊢ 0 · ★₁ ⇐ ★₀" $ - checkType_ (ctx01 [<]) (TYPE 1) (Just 0), + checkType_ empty01 (TYPE 1) (Just 0), testTCFail "1 · ★₀ ⇍ ★₁ # by check" $ - check_ (ctx [<]) sone (TYPE 0) (TYPE 1) + check_ empty sone (TYPE 0) (TYPE 1) ], "function types" :- [ note "A, B : ★₀; C, D : ★₁; P : A ⇾ ★₀", testTC "0 · A ⊸ B ⇐ ★₀" $ - check_ (ctx [<]) szero (Arr One (FT "A") (FT "B")) (TYPE 0), + check_ empty szero (Arr One (FT "A") (FT "B")) (TYPE 0), note "subtyping", testTC "0 · A ⊸ B ⇐ ★₁" $ - check_ (ctx [<]) szero (Arr One (FT "A") (FT "B")) (TYPE 1), + check_ empty szero (Arr One (FT "A") (FT "B")) (TYPE 1), testTC "0 · C ⊸ D ⇐ ★₁" $ - check_ (ctx [<]) szero (Arr One (FT "C") (FT "D")) (TYPE 1), + check_ empty szero (Arr One (FT "C") (FT "D")) (TYPE 1), testTCFail "0 · C ⊸ D ⇍ ★₀" $ - check_ (ctx [<]) szero (Arr One (FT "C") (FT "D")) (TYPE 0), + check_ empty szero (Arr One (FT "C") (FT "D")) (TYPE 0), testTC "0 · (1·x : A) → P x ⇐ ★₀" $ - check_ (ctx [<]) szero + check_ empty szero (Pi_ One "x" (FT "A") $ E $ F "P" :@ BVT 0) (TYPE 0), testTCFail "0 · A ⊸ P ⇍ ★₀" $ - check_ (ctx [<]) szero (Arr One (FT "A") $ FT "P") (TYPE 0), + check_ empty szero (Arr One (FT "A") $ FT "P") (TYPE 0), testTC "0=1 ⊢ 0 · A ⊸ P ⇐ ★₀" $ - check_ (ctx01 [<]) szero (Arr One (FT "A") $ FT "P") (TYPE 0) + check_ empty01 szero (Arr One (FT "A") $ FT "P") (TYPE 0) ], "pair types" :- [ note #""A × B" for "(_ : A) × B""#, testTC "0 · A × A ⇐ ★₀" $ - check_ (ctx [<]) szero (FT "A" `And` FT "A") (TYPE 0), + check_ empty szero (FT "A" `And` FT "A") (TYPE 0), testTCFail "0 · A × P ⇍ ★₀" $ - check_ (ctx [<]) szero (FT "A" `And` FT "P") (TYPE 0), + check_ empty szero (FT "A" `And` FT "P") (TYPE 0), testTC "0 · (x : A) × P x ⇐ ★₀" $ - check_ (ctx [<]) szero + check_ empty szero (Sig_ "x" (FT "A") $ E $ F "P" :@ BVT 0) (TYPE 0), testTC "0 · (x : A) × P x ⇐ ★₁" $ - check_ (ctx [<]) szero + check_ empty szero (Sig_ "x" (FT "A") $ E $ F "P" :@ BVT 0) (TYPE 1), testTC "0 · (A : ★₀) × A ⇐ ★₁" $ - check_ (ctx [<]) szero (Sig_ "A" (TYPE 0) $ BVT 0) (TYPE 1), + check_ empty szero (Sig_ "A" (TYPE 0) $ BVT 0) (TYPE 1), testTCFail "0 · (A : ★₀) × A ⇍ ★₀" $ - check_ (ctx [<]) szero (Sig_ "A" (TYPE 0) $ BVT 0) (TYPE 0), + check_ empty szero (Sig_ "A" (TYPE 0) $ BVT 0) (TYPE 0), testTCFail "1 · A × A ⇍ ★₀" $ - check_ (ctx [<]) sone (FT "A" `And` FT "A") (TYPE 0) + check_ empty sone (FT "A" `And` FT "A") (TYPE 0) ], "enum types" :- [ - testTC "0 · {} ⇐ ★₀" $ check_ (ctx [<]) szero (enum []) (TYPE 0), - testTC "0 · {} ⇐ ★₃" $ check_ (ctx [<]) szero (enum []) (TYPE 3), + testTC "0 · {} ⇐ ★₀" $ check_ empty szero (enum []) (TYPE 0), + testTC "0 · {} ⇐ ★₃" $ check_ empty szero (enum []) (TYPE 3), testTC "0 · {a,b,c} ⇐ ★₀" $ - check_ (ctx [<]) szero (enum ["a", "b", "c"]) (TYPE 0), + check_ empty szero (enum ["a", "b", "c"]) (TYPE 0), testTC "0 · {a,b,c} ⇐ ★₃" $ - check_ (ctx [<]) szero (enum ["a", "b", "c"]) (TYPE 3), - testTCFail "1 · {} ⇍ ★₀" $ check_ (ctx [<]) sone (enum []) (TYPE 0), - testTC "0=1 ⊢ 1 · {} ⇐ ★₀" $ check_ (ctx01 [<]) sone (enum []) (TYPE 0) + check_ empty szero (enum ["a", "b", "c"]) (TYPE 3), + testTCFail "1 · {} ⇍ ★₀" $ check_ empty sone (enum []) (TYPE 0), + testTC "0=1 ⊢ 1 · {} ⇐ ★₀" $ check_ empty01 sone (enum []) (TYPE 0) ], "free vars" :- [ note "A : ★₀", testTC "0 · A ⇒ ★₀" $ - inferAs (ctx [<]) szero (F "A") (TYPE 0), + inferAs empty szero (F "A") (TYPE 0), testTC "0 · [A] ⇐ ★₀" $ - check_ (ctx [<]) szero (FT "A") (TYPE 0), + check_ empty szero (FT "A") (TYPE 0), note "subtyping", testTC "0 · [A] ⇐ ★₁" $ - check_ (ctx [<]) szero (FT "A") (TYPE 1), + check_ empty szero (FT "A") (TYPE 1), note "(fail) runtime-relevant type", testTCFail "1 · A ⇏ ★₀" $ - infer_ (ctx [<]) sone (F "A"), + infer_ empty sone (F "A"), note "refl : (0·A : ★₀) → (1·x : A) → (x ≡ x : A) ≔ (λ A x ⇒ δ _ ⇒ x)", - testTC "1 · refl ⇒ ⋯" $ inferAs (ctx [<]) sone (F "refl") reflTy, - testTC "1 · [refl] ⇐ ⋯" $ check_ (ctx [<]) sone (FT "refl") reflTy + testTC "1 · refl ⇒ ⋯" $ inferAs empty sone (F "refl") reflTy, + testTC "1 · [refl] ⇐ ⋯" $ check_ empty sone (FT "refl") reflTy ], "bound vars" :- [ testTC "x : A ⊢ 1 · x ⇒ A ⊳ 1·x" $ - inferAsQ {n = 1} (ctx [< FT "A"]) sone + inferAsQ {n = 1} (ctx [< ("x", FT "A")]) sone (BV 0) (FT "A") [< one], testTC "x : A ⊢ 1 · [x] ⇐ A ⊳ 1·x" $ - checkQ {n = 1} (ctx [< FT "A"]) sone (BVT 0) (FT "A") [< one], + checkQ {n = 1} (ctx [< ("x", FT "A")]) sone (BVT 0) (FT "A") [< one], note "f2 : A ⊸ A ⊸ B", testTC "x : A ⊢ 1 · f2 [x] [x] ⇒ B ⊳ ω·x" $ - inferAsQ {n = 1} (ctx [< FT "A"]) sone + inferAsQ {n = 1} (ctx [< ("x", FT "A")]) sone (F "f2" :@@ [BVT 0, BVT 0]) (FT "B") [< Any] ], "lambda" :- [ note "linear & unrestricted identity", testTC "1 · (λ x ⇒ x) ⇐ A ⊸ A" $ - check_ (ctx [<]) sone (["x"] :\\ BVT 0) (Arr One (FT "A") (FT "A")), + check_ empty sone (["x"] :\\ BVT 0) (Arr One (FT "A") (FT "A")), testTC "1 · (λ x ⇒ x) ⇐ A → A" $ - check_ (ctx [<]) sone (["x"] :\\ BVT 0) (Arr Any (FT "A") (FT "A")), + check_ empty sone (["x"] :\\ BVT 0) (Arr Any (FT "A") (FT "A")), note "(fail) zero binding used relevantly", testTCFail "1 · (λ x ⇒ x) ⇍ A ⇾ A" $ - check_ (ctx [<]) sone (["x"] :\\ BVT 0) (Arr Zero (FT "A") (FT "A")), + check_ empty sone (["x"] :\\ BVT 0) (Arr Zero (FT "A") (FT "A")), note "(but ok in overall erased context)", testTC "0 · (λ x ⇒ x) ⇐ A ⇾ A" $ - check_ (ctx [<]) szero (["x"] :\\ BVT 0) (Arr Zero (FT "A") (FT "A")), + check_ empty szero (["x"] :\\ BVT 0) (Arr Zero (FT "A") (FT "A")), testTC "1 · (λ A x ⇒ refl A x) ⇐ ⋯ # (type of refl)" $ - check_ (ctx [<]) sone + check_ empty sone (["A", "x"] :\\ E (F "refl" :@@ [BVT 1, BVT 0])) reflTy, testTC "1 · (λ A x ⇒ δ i ⇒ x) ⇐ ⋯ # (def. and type of refl)" $ - check_ (ctx [<]) sone reflDef reflTy + check_ empty sone reflDef reflTy ], "pairs" :- [ testTC "1 · (a, a) ⇐ A × A" $ - check_ (ctx [<]) sone (Pair (FT "a") (FT "a")) (FT "A" `And` FT "A"), + check_ empty sone (Pair (FT "a") (FT "a")) (FT "A" `And` FT "A"), testTC "x : A ⊢ 1 · (x, x) ⇐ A × A ⊳ ω·x" $ - checkQ (ctx [< FT "A"]) sone + checkQ (ctx [< ("x", FT "A")]) sone (Pair (BVT 0) (BVT 0)) (FT "A" `And` FT "A") [< Any], testTC "1 · (a, δ i ⇒ a) ⇐ (x : A) × (x ≡ a)" $ - check_ (ctx [<]) sone + check_ empty sone (Pair (FT "a") (["i"] :\\% FT "a")) (Sig_ "x" (FT "A") $ Eq0 (FT "A") (BVT 0) (FT "a")) ], "unpairing" :- [ testTC "x : A × A ⊢ 1 · (case1 x return B of (l,r) ⇒ f2 l r) ⇒ B ⊳ 1·x" $ - inferAsQ (ctx [< FT "A" `And` FT "A"]) sone + inferAsQ (ctx [< ("x", FT "A" `And` FT "A")]) sone (CasePair One (BV 0) (SN $ FT "B") (SY ["l", "r"] $ E $ F "f2" :@@ [BVT 1, BVT 0])) (FT "B") [< One], testTC "x : A × A ⊢ 1 · (caseω x return B of (l,r) ⇒ f2 l r) ⇒ B ⊳ ω·x" $ - inferAsQ (ctx [< FT "A" `And` FT "A"]) sone + inferAsQ (ctx [< ("x", FT "A" `And` FT "A")]) sone (CasePair Any (BV 0) (SN $ FT "B") (SY ["l", "r"] $ E $ F "f2" :@@ [BVT 1, BVT 0])) (FT "B") [< Any], testTC "x : A × A ⊢ 0 · (caseω x return B of (l,r) ⇒ f2 l r) ⇒ B ⊳ 0·x" $ - inferAsQ (ctx [< FT "A" `And` FT "A"]) szero + inferAsQ (ctx [< ("x", FT "A" `And` FT "A")]) szero (CasePair Any (BV 0) (SN $ FT "B") (SY ["l", "r"] $ E $ F "f2" :@@ [BVT 1, BVT 0])) (FT "B") [< Zero], testTCFail "x : A × A ⊢ 1 · (case0 x return B of (l,r) ⇒ f2 l r) ⇏" $ - infer_ (ctx [< FT "A" `And` FT "A"]) sone + infer_ (ctx [< ("x", FT "A" `And` FT "A")]) sone (CasePair Zero (BV 0) (SN $ FT "B") (SY ["l", "r"] $ E $ F "f2" :@@ [BVT 1, BVT 0])), testTC "x : A × B ⊢ 1 · (caseω x return A of (l,r) ⇒ l) ⇒ A ⊳ ω·x" $ - inferAsQ (ctx [< FT "A" `And` FT "B"]) sone + inferAsQ (ctx [< ("x", FT "A" `And` FT "B")]) sone (CasePair Any (BV 0) (SN $ FT "A") (SY ["l", "r"] $ BVT 1)) (FT "A") [< Any], testTC "x : A × B ⊢ 0 · (case1 x return A of (l,r) ⇒ l) ⇒ A ⊳ 0·x" $ - inferAsQ (ctx [< FT "A" `And` FT "B"]) szero + inferAsQ (ctx [< ("x", FT "A" `And` FT "B")]) szero (CasePair One (BV 0) (SN $ FT "A") (SY ["l", "r"] $ BVT 1)) (FT "A") [< Zero], testTCFail "x : A × B ⊢ 1 · (case1 x return A of (l,r) ⇒ l) ⇏" $ - infer_ (ctx [< FT "A" `And` FT "B"]) sone + infer_ (ctx [< ("x", FT "A" `And` FT "B")]) sone (CasePair One (BV 0) (SN $ FT "A") (SY ["l", "r"] $ BVT 1)), note "fst : (0·A : ★₁) → (0·B : A ↠ ★₁) → ((x : A) × B x) ↠ A", note " ≔ (λ A B p ⇒ caseω p return A of (x, y) ⇒ x)", testTC "0 · ‹type of fst› ⇐ ★₂" $ - check_ (ctx [<]) szero fstTy (TYPE 2), + check_ empty szero fstTy (TYPE 2), testTC "1 · ‹def of fst› ⇐ ‹type of fst›" $ - check_ (ctx [<]) sone fstDef fstTy, + check_ empty sone fstDef fstTy, note "snd : (0·A : ★₁) → (0·B : A ↠ ★₁) → (ω·p : (x : A) × B x) → B (fst A B p)", note " ≔ (λ A B p ⇒ caseω p return p ⇒ B (fst A B p) of (x, y) ⇒ y)", testTC "0 · ‹type of snd› ⇐ ★₂" $ - check_ (ctx [<]) szero sndTy (TYPE 2), + check_ empty szero sndTy (TYPE 2), testTC "1 · ‹def of snd› ⇐ ‹type of snd›" $ - check_ (ctx [<]) sone sndDef sndTy, + check_ empty sone sndDef sndTy, testTC "0 · snd ★₀ (λ x ⇒ x) ⇒ (ω·p : (A : ★₀) × A) → fst ★₀ (λ x ⇒ x) p" $ - inferAs (ctx [<]) szero + inferAs empty szero (F "snd" :@@ [TYPE 0, ["x"] :\\ BVT 0]) (Pi_ Any "A" (Sig_ "A" (TYPE 0) $ BVT 0) $ (E $ F "fst" :@@ [TYPE 0, ["x"] :\\ BVT 0, BVT 0])) @@ -344,27 +347,27 @@ tests = "typechecker" :- [ "enums" :- [ testTC "1 · 'a ⇐ {a}" $ - check_ (ctx [<]) sone (Tag "a") (enum ["a"]), + check_ empty sone (Tag "a") (enum ["a"]), testTC "1 · 'a ⇐ {a, b, c}" $ - check_ (ctx [<]) sone (Tag "a") (enum ["a", "b", "c"]), + check_ empty sone (Tag "a") (enum ["a", "b", "c"]), testTCFail "1 · 'a ⇍ {b, c}" $ - check_ (ctx [<]) sone (Tag "a") (enum ["b", "c"]), + check_ empty sone (Tag "a") (enum ["b", "c"]), testTC "0=1 ⊢ 1 · 'a ⇐ {b, c}" $ - check_ (ctx01 [<]) sone (Tag "a") (enum ["b", "c"]) + check_ empty01 sone (Tag "a") (enum ["b", "c"]) ], "equalities" :- [ testTC "1 · (δ i ⇒ a) ⇐ a ≡ a" $ - check_ (ctx [<]) sone (DLam $ SN $ FT "a") + check_ empty sone (DLam $ SN $ FT "a") (Eq0 (FT "A") (FT "a") (FT "a")), testTC "0 · (λ p q ⇒ δ i ⇒ p) ⇐ (ω·p q : a ≡ a') → p ≡ q" $ - check_ (ctx [<]) szero + check_ empty szero (["p","q"] :\\ ["i"] :\\% BVT 1) (Pi_ Any "p" (Eq0 (FT "A") (FT "a") (FT "a")) $ Pi_ Any "q" (Eq0 (FT "A") (FT "a") (FT "a")) $ Eq0 (Eq0 (FT "A") (FT "a") (FT "a")) (BVT 1) (BVT 0)), testTC "0 · (λ p q ⇒ δ i ⇒ q) ⇐ (ω·p q : a ≡ a') → p ≡ q" $ - check_ (ctx [<]) szero + check_ empty szero (["p","q"] :\\ ["i"] :\\% BVT 0) (Pi_ Any "p" (Eq0 (FT "A") (FT "a") (FT "a")) $ Pi_ Any "q" (Eq0 (FT "A") (FT "a") (FT "a")) $ @@ -377,7 +380,7 @@ tests = "typechecker" :- [ note "1 · λ x y xy ⇒ δ i ⇒ p (xy i)", note " ⇐ (0·x y : A) → (1·xy : x ≡ y) → Eq [i ⇒ P (xy i)] (p x) (p y)", testTC "cong" $ - check_ (ctx [<]) sone + check_ empty sone (["x", "y", "xy"] :\\ ["i"] :\\% E (F "p" :@ E (BV 0 :% BV 0))) (Pi_ Zero "x" (FT "A") $ Pi_ Zero "y" (FT "A") $ @@ -390,7 +393,7 @@ tests = "typechecker" :- [ note "1 · λ eq ⇒ δ i ⇒ λ x ⇒ eq x i", note " ⇐ (1·eq : (1·x : A) → p x ≡ q x) → p ≡ q", testTC "funext" $ - check_ (ctx [<]) sone + check_ empty sone (["eq"] :\\ ["i"] :\\% ["x"] :\\ E (BV 1 :@ BVT 0 :% BV 0)) (Pi_ One "eq" (Pi_ One "x" (FT "A") diff --git a/tests/TypingImpls.idr b/tests/TypingImpls.idr index c7915ed..9b45b7f 100644 --- a/tests/TypingImpls.idr +++ b/tests/TypingImpls.idr @@ -17,6 +17,10 @@ export %hint showTyContext : (PrettyHL q, Show q) => Show (TyContext q d n) showTyContext = deriveShow +export %hint +showEqContext : (PrettyHL q, Show q) => Show (EqContext q n) +showEqContext = deriveShow + export %hint showTypingError : (PrettyHL q, Show q) => Show (Error q) showTypingError = deriveShow @@ -33,19 +37,19 @@ PrettyHL q => ToInfo (Error q) where toInfo (NotInScope x) = [("type", "NotInScope"), ("name", show x)] - toInfo (ExpectedTYPE t) = + toInfo (ExpectedTYPE _ t) = [("type", "ExpectedTYPE"), ("got", prettyStr True t)] - toInfo (ExpectedPi t) = + toInfo (ExpectedPi _ t) = [("type", "ExpectedPi"), ("got", prettyStr True t)] - toInfo (ExpectedSig t) = + toInfo (ExpectedSig _ t) = [("type", "ExpectedSig"), ("got", prettyStr True t)] - toInfo (ExpectedEnum t) = + toInfo (ExpectedEnum _ t) = [("type", "ExpectedEnum"), ("got", prettyStr True t)] - toInfo (ExpectedEq t) = + toInfo (ExpectedEq _ t) = [("type", "ExpectedEq"), ("got", prettyStr True t)] toInfo (BadUniverse k l) = @@ -56,22 +60,22 @@ PrettyHL q => ToInfo (Error q) where [("type", "TagNotIn"), ("tag", show t), ("set", show $ SortedSet.toList ts)] - toInfo (BadCaseQtys qouts) = + toInfo (BadCaseQtys _ qouts) = ("type", "BadCaseQtys") :: - [(show i, prettyStr True q) | (i, q) <- zip [1 .. length qouts] qouts] + [(show i, prettyStr True q) | (i, _, _, q) <- zip [1 .. length qouts] qouts] - toInfo (ClashT mode ty s t) = + toInfo (ClashT _ mode ty s t) = [("type", "ClashT"), ("mode", show mode), ("ty", prettyStr True ty), ("left", prettyStr True s), ("right", prettyStr True t)] - toInfo (ClashTy mode s t) = + toInfo (ClashTy _ mode s t) = [("type", "ClashTy"), ("mode", show mode), ("left", prettyStr True s), ("right", prettyStr True t)] - toInfo (ClashE mode e f) = + toInfo (ClashE _ mode e f) = [("type", "ClashE"), ("mode", show mode), ("left", prettyStr True e), @@ -85,14 +89,10 @@ PrettyHL q => ToInfo (Error q) where [("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) = + toInfo (NotType _ ty) = [("type", "NotType"), ("got", prettyStr True ty)] - toInfo (WrongType ty s t) = + toInfo (WrongType _ ty s t) = [("type", "WrongType"), ("ty", prettyStr True ty), ("left", prettyStr True s),