From 32f38238ef66d43519402d6ba2d36ddc579efa3f Mon Sep 17 00:00:00 2001 From: rhiannon morris Date: Wed, 15 Mar 2023 15:54:51 +0100 Subject: [PATCH] pretty printing errors --- lib/Quox/Context.idr | 27 ++++- lib/Quox/Equal.idr | 76 ++++++++------- lib/Quox/Pretty.idr | 10 +- lib/Quox/Syntax/Dim.idr | 27 +++-- lib/Quox/Syntax/Qty/Three.idr | 7 +- lib/Quox/Syntax/Term/Pretty.idr | 36 +++++-- lib/Quox/Typechecker.idr | 21 ++-- lib/Quox/Typing.idr | 20 +--- lib/Quox/Typing/Context.idr | 121 +++++++++++++++++------ lib/Quox/Typing/Error.idr | 168 +++++++++++++++++++++++++++++++- tests/Tests.idr | 5 +- tests/Tests/Equal.idr | 35 ++++--- tests/Tests/Typechecker.idr | 13 ++- tests/TypingImpls.idr | 75 +------------- 14 files changed, 424 insertions(+), 217 deletions(-) diff --git a/lib/Quox/Context.idr b/lib/Quox/Context.idr index 0d6f60d..773fb06 100644 --- a/lib/Quox/Context.idr +++ b/lib/Quox/Context.idr @@ -2,6 +2,7 @@ module Quox.Context import Quox.Syntax.Shift import Quox.Pretty +import Quox.Name import Data.DPair import Data.Nat @@ -34,6 +35,14 @@ public export Context' : (a : Type) -> (len : Nat) -> Type Context' a = Context (\_ => a) +public export +NContext : Nat -> Type +NContext = Context' BaseName + + +public export +head : Context tm (S n) -> tm n +head (_ :< t) = t public export tail : Context tm (S n) -> Context tm n @@ -180,18 +189,26 @@ unzip : Telescope (\n => (tm1 n, tm2 n)) from to -> unzip [<] = ([<], [<]) unzip (tel :< (x, y)) = let (xs, ys) = unzip tel in (xs :< x, ys :< y) +export +unzip3 : Telescope (\n => (tm1 n, tm2 n, tm3 n)) from to -> + (Telescope tm1 from to, Telescope tm2 from to, Telescope tm3 from to) +unzip3 [<] = ([<], [<], [<]) +unzip3 (tel :< (x, y, z)) = + let (xs, ys, zs) = unzip3 tel in (xs :< x, ys :< y, zs :< z) + + export -lengthPrf : Telescope _ from to -> Subset Nat (\len => len + from = to) -lengthPrf [<] = Element 0 Refl +lengthPrf : Telescope _ from to -> (len ** len + from = to) +lengthPrf [<] = (0 ** Refl) lengthPrf (tel :< _) = - let len = lengthPrf tel in Element (S len.fst) (cong S len.snd) + let len = lengthPrf tel in (S len.fst ** cong S len.snd) export -lengthPrf0 : Context _ to -> Subset Nat (\len => len = to) +lengthPrf0 : Context _ to -> (len ** len = to) lengthPrf0 ctx = let len = lengthPrf ctx in - Element len.fst (rewrite sym $ plusZeroRightNeutral len.fst in len.snd) + (len.fst ** rewrite sym $ plusZeroRightNeutral len.fst in len.snd) public export %inline length : Telescope {} -> Nat diff --git a/lib/Quox/Equal.idr b/lib/Quox/Equal.idr index d7a3b25..fba3987 100644 --- a/lib/Quox/Equal.idr +++ b/lib/Quox/Equal.idr @@ -107,22 +107,14 @@ parameters (defs : Definitions' q g) E _ => pure False -parameters {auto _ : HasErr q m} - export %inline - ensure : (a -> Error q) -> (p : a -> Bool) -> (t : a) -> m (So (p t)) - ensure e p t = case nchoose $ p t of - Left y => pure y - Right _ => throwError $ e t +export +ensureTyCon : HasErr q m => + (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 => throwError $ NotType (toTyContext ctx) (t // shift0 ctx.dimLen) - export %inline - 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)} +parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, IsQty q)} mutual namespace Term ||| `compare0 ctx ty s t` compares `s` and `t` at type `ty`, according to @@ -153,24 +145,27 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)} m () compare0' ctx (TYPE _) s t = compareType ctx s t - compare0' ctx ty@(Pi {arg, res, _}) s t {n} = local {mode := Equal} $ + compare0' ctx ty@(Pi {qty, arg, res}) s t {n} = local {mode := Equal} $ case (s, t) of - -- Γ, x : A ⊢ s = t : B - -- ----------------------------------------- - -- Γ ⊢ (λx ⇒ s) = (λx ⇒ t) : (π·x : A) → B + -- Γ, x : A ⊢ s = t : B + -- ------------------------------------------- + -- Γ ⊢ (λ x ⇒ s) = (λ x ⇒ t) : (π·x : A) → B (Lam b1, Lam b2) => compare0 ctx' res.term b1.term b2.term -- Γ, x : A ⊢ s = e x : B - -- ---------------------------------- - -- Γ ⊢ (λx ⇒ s) = e : (π·x : A) → B + -- ----------------------------------- + -- Γ ⊢ (λ x ⇒ s) = e : (π·x : A) → B (E e, Lam b) => eta e b (Lam b, E e) => eta e b (E e, E f) => Elim.compare0 ctx e f - _ => throwError $ WrongType ctx ty s t + + (Lam _, t) => throwError $ WrongType ctx ty t + (E _, t) => throwError $ WrongType ctx ty t + (s, _) => throwError $ WrongType ctx ty s where ctx' : EqContext q (S n) - ctx' = extendTy res.name arg ctx + ctx' = extendTy qty 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 @@ -179,16 +174,19 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)} compare0' ctx ty@(Sig {fst, snd, _}) s t = local {mode := Equal} $ case (s, t) of -- Γ ⊢ s₁ = t₁ : A Γ ⊢ s₂ = t₂ : B{s₁/x} - -- ------------------------------------------- - -- Γ ⊢ (s₁,t₁) = (s₂,t₂) : (x : A) × B + -- -------------------------------------------- + -- Γ ⊢ (s₁, t₁) = (s₂,t₂) : (x : A) × B -- -- [todo] η for π ≥ 0 maybe (Pair sFst sSnd, Pair tFst tSnd) => do compare0 ctx fst sFst tFst compare0 ctx (sub1 snd (sFst :# fst)) sSnd tSnd - (E e, E f) => compare0 ctx e f - _ => throwError $ WrongType ctx ty s t + (E e, E f) => Elim.compare0 ctx e f + + (Pair {}, t) => throwError $ WrongType ctx ty t + (E _, t) => throwError $ WrongType ctx ty t + (s, _) => throwError $ WrongType ctx ty s compare0' ctx ty@(Enum tags) s t = local {mode := Equal} $ case (s, t) of @@ -197,8 +195,11 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)} -- -- t ∈ ts is in the typechecker, not here, ofc (Tag t1, Tag t2) => unless (t1 == t2) $ clashT ctx ty s t - (E e, E f) => compare0 ctx e f - _ => throwError $ WrongType ctx ty s t + (E e, E f) => Elim.compare0 ctx e f + + (Tag _, t) => throwError $ WrongType ctx ty t + (E _, t) => throwError $ WrongType ctx ty t + (s, _) => throwError $ WrongType ctx ty s compare0' _ (Eq {}) _ _ = -- ✨ uip ✨ @@ -209,8 +210,8 @@ 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 ctx ty s t - E f <- pure t | _ => throwError $ WrongType ctx ty s t + E e <- pure s | _ => throwError $ WrongType ctx ty s + E f <- pure t | _ => throwError $ WrongType ctx ty t Elim.compare0 ctx e f ||| compares two types, using the current variance `mode` for universes. @@ -247,7 +248,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 (extendTy sRes.name sArg ctx) sRes.term tRes.term + compareType (extendTy zero sRes.name sArg ctx) sRes.term tRes.term compareType' ctx (Sig {fst = sFst, snd = sSnd, _}) (Sig {fst = tFst, snd = tSnd, _}) = do @@ -255,7 +256,7 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)} -- -------------------------------------- -- Γ ⊢ (x : A₁) × B₁ <: (x : A₂) × B₂ compareType ctx sFst tFst - compareType (extendTy sSnd.name sFst ctx) sSnd.term tSnd.term + compareType (extendTy zero 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 @@ -365,10 +366,10 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)} local {mode := Equal} $ do compare0 ctx e f ety <- computeElimType ctx e (noOr1 ne) - compareType (extendTy eret.name ety ctx) eret.term fret.term + compareType (extendTy zero 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) + Term.compare0 (extendTyN [< (epi, x, fst), (epi, y, snd.term)] ctx) (substCasePairRet ety eret) ebody.term fbody.term expectEqualQ epi fpi @@ -379,7 +380,7 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)} local {mode := Equal} $ do compare0 ctx e f ety <- computeElimType ctx e (noOr1 ne) - compareType (extendTy eret.name ety ctx) eret.term fret.term + compareType (extendTy zero 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) @@ -402,7 +403,8 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)} compare0' ctx e@(_ :# _) f _ _ = clashE ctx e f -parameters {auto _ : (HasDefs' q _ m, HasErr q m, Eq q)} (ctx : TyContext q d n) +parameters {auto _ : (HasDefs' q _ m, HasErr q m, IsQty q)} + (ctx : TyContext q d n) -- [todo] only split on the dvars that are actually used anywhere in -- the calls to `splits` diff --git a/lib/Quox/Pretty.idr b/lib/Quox/Pretty.idr index 9deb2d4..96b9a36 100644 --- a/lib/Quox/Pretty.idr +++ b/lib/Quox/Pretty.idr @@ -172,11 +172,15 @@ export %inline pretty0M : (PrettyHL a, HasEnv m) => a -> m (Doc HL) pretty0M = local {prec := Outer} . prettyM +export %inline +runPretty : (unicode : Bool) -> Reader PrettyEnv a -> a +runPretty unicode act = + let env = MakePrettyEnv {dnames = [<], tnames = [<], unicode, prec = Outer} in + runReader env act + export %inline pretty0 : PrettyHL a => (unicode : Bool) -> a -> Doc HL -pretty0 unicode x = - let env = MakePrettyEnv {dnames = [], tnames = [], unicode, prec = Outer} in - runReader env $ prettyM x +pretty0 unicode = runPretty unicode . prettyM export diff --git a/lib/Quox/Syntax/Dim.idr b/lib/Quox/Syntax/Dim.idr index 5145d0e..0f90b35 100644 --- a/lib/Quox/Syntax/Dim.idr +++ b/lib/Quox/Syntax/Dim.idr @@ -1,8 +1,10 @@ module Quox.Syntax.Dim +import Quox.Name import Quox.Syntax.Var import Quox.Syntax.Subst import Quox.Pretty +import Quox.Context import Decidable.Equality import Control.Function @@ -31,29 +33,26 @@ data Dim : Nat -> Type where B : Var d -> Dim d %name Dim.Dim p, q -private %inline -drepr : Dim n -> Either DimConst (Var n) -drepr (K k) = Left k -drepr (B x) = Right x - -export Eq (Dim n) where (==) = (==) `on` drepr -export Ord (Dim n) where compare = compare `on` drepr - -export -Show (Dim n) where - show (K k) = showCon App "K" $ show k - show (B i) = showCon App "B" $ show i +%runElab deriveIndexed "Dim" [Eq, Ord, Show] export PrettyHL DimConst where - prettyM Zero = hl Dim <$> ifUnicode "𝟬" "0" - prettyM One = hl Dim <$> ifUnicode "𝟭" "1" + prettyM = pure . hl Dim . ends "0" "1" export PrettyHL (Dim n) where prettyM (K e) = prettyM e prettyM (B i) = prettyVar DVar DVarErr (!ask).dnames i +export +prettyDim : (dnames : NContext d) -> Dim d -> Doc HL +prettyDim dnames p = + let env = MakePrettyEnv { + dnames = toSnocList' dnames, tnames = [<], + unicode = True, prec = Outer + } in + runReader env $ prettyM p + ||| `endsOr l r x e` returns: ||| - `l` if `p` is `K Zero`; diff --git a/lib/Quox/Syntax/Qty/Three.idr b/lib/Quox/Syntax/Qty/Three.idr index 47cb1a4..6bc78ba 100644 --- a/lib/Quox/Syntax/Qty/Three.idr +++ b/lib/Quox/Syntax/Qty/Three.idr @@ -19,9 +19,9 @@ export PrettyHL Three where prettyM pi = hl Qty <$> case pi of - Zero => ifUnicode "𝟬" "0" - One => ifUnicode "𝟭" "1" - Any => ifUnicode "𝛚" "*" + Zero => pure "0" + One => pure "1" + Any => ifUnicode "ω" "#" public export DecEq Three where @@ -88,6 +88,7 @@ data IsGlobal3 : Pred Three where GZero : IsGlobal3 Zero GAny : IsGlobal3 Any +public export isGlobal3 : Dec1 IsGlobal3 isGlobal3 Zero = Yes GZero isGlobal3 One = No $ \case _ impossible diff --git a/lib/Quox/Syntax/Term/Pretty.idr b/lib/Quox/Syntax/Term/Pretty.idr index bcc4f69..a0e8cc7 100644 --- a/lib/Quox/Syntax/Term/Pretty.idr +++ b/lib/Quox/Syntax/Term/Pretty.idr @@ -3,6 +3,7 @@ module Quox.Syntax.Term.Pretty import Quox.Syntax.Term.Base import Quox.Syntax.Term.Split import Quox.Syntax.Term.Subst +import Quox.Context import Quox.Pretty import Data.Vect @@ -42,16 +43,26 @@ prettyUnivSuffix l = '0' => '₀'; '1' => '₁'; '2' => '₂'; '3' => '₃'; '4' => '₄' '5' => '₅'; '6' => '₆'; '7' => '₇'; '8' => '₈'; '9' => '₉'; _ => c +export +prettyUniverse : Universe -> Doc HL +prettyUniverse = hl Syntax . pretty + +export +prettyBind : PrettyHL a => PrettyHL q => Pretty.HasEnv m => + List q -> BaseName -> a -> m (Doc HL) +prettyBind qtys x s = do + var <- prettyQtyBinds qtys $ TV x + s <- withPrec Outer $ prettyM s + pure $ var <++> colonD <%%> hang 2 s + export prettyBindType : PrettyHL a => PrettyHL b => PrettyHL q => Pretty.HasEnv m => List q -> BaseName -> a -> Doc HL -> b -> m (Doc HL) prettyBindType qtys x s arr t = do - var <- prettyQtyBinds qtys $ TV x - s <- withPrec Outer $ prettyM s - t <- withPrec Outer $ under T x $ prettyM t - let bind = parens (var <++> colonD <%%> hang 2 s) - parensIfM Outer $ hang 2 $ bind <%%> t + bind <- prettyBind qtys x s + t <- withPrec Outer $ under T x $ prettyM t + parensIfM Outer $ hang 2 $ parens bind <++> arr <%%> t export prettyArm : PrettyHL a => Pretty.HasEnv m => @@ -144,7 +155,7 @@ parameters (showSubsts : Bool) prettyM (DLam (S i t)) = let GotDLams {names, body, _} = getDLams' i t.term Refl in prettyLams (Just !dlamD) D (toList names) body - prettyM (E e) = bracks <$> prettyM e + prettyM (E e) = prettyM e prettyM (CloT s th) = if showSubsts then parensIfM SApp . hang 2 =<< @@ -207,3 +218,16 @@ PrettyHL q => PrettyHL (Term q d n) where export covering %inline PrettyHL q => PrettyHL (Elim q d n) where prettyM = prettyM @{ElimSubst False} + + +export covering +prettyTerm : PrettyHL q => (unicode : Bool) -> + (dnames : NContext d) -> (tnames : NContext n) -> + Term q d n -> Doc HL +prettyTerm unicode dnames tnames term = + let env = MakePrettyEnv { + dnames = toSnocList' dnames, + tnames = toSnocList' tnames, + unicode, prec = Outer + } in + runReader env $ prettyM term diff --git a/lib/Quox/Typechecker.idr b/lib/Quox/Typechecker.idr index cc27f22..b24d6b1 100644 --- a/lib/Quox/Typechecker.idr +++ b/lib/Quox/Typechecker.idr @@ -128,7 +128,7 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m} -- if Ψ | Γ, x : A ⊢ σ · t ⇐ B ⊳ Σ, ρ·x -- with ρ ≤ σπ let qty' = sg.fst * qty - qout <- checkC (extendTy body.name arg ctx) sg body.term res.term + qout <- checkC (extendTy qty' body.name arg ctx) sg body.term res.term -- then Ψ | Γ ⊢ σ · (λx ⇒ t) ⇐ (π·x : A) → B ⊳ Σ popQ qty' qout @@ -190,8 +190,8 @@ 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 res.name arg ctx) res' u - N res' => checkTypeC ctx res' u + Y res' => checkTypeC (extendTy zero res.name arg ctx) res' u + N res' => checkTypeC ctx res' u -- then Ψ | Γ ⊢₀ (π·x : A) → B ⇐ Type ℓ checkType' ctx t@(Lam {}) u = @@ -202,8 +202,8 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m} checkTypeC ctx fst u -- if Ψ | Γ, x : A ⊢₀ B ⇐ Type ℓ case snd.body of - Y snd' => checkTypeC (extendTy snd.name fst ctx) snd' u - N snd' => checkTypeC ctx snd' u + Y snd' => checkTypeC (extendTy zero snd.name fst ctx) snd' u + N snd' => checkTypeC ctx snd' u -- then Ψ | Γ ⊢₀ (x : A) × B ⇐ Type ℓ checkType' ctx t@(Pair {}) u = @@ -285,15 +285,15 @@ 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 ret.name pairres.type ctx) ret.term Nothing + checkTypeC (extendTy zero 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 [x, y] = body.names - bodyctx = extendTyN [< (x, tfst), (y, tsnd.term)] ctx - bodyty = substCasePairRet pairres.type ret pisg = pi * sg.fst + bodyctx = extendTyN [< (pisg, x, tfst), (pisg, y, tsnd.term)] ctx + bodyty = substCasePairRet pairres.type ret bodyout <- checkC bodyctx sg body.term bodyty -- then Ψ | Γ ⊢ σ · case ⋯ ⇒ ret[pair/p] ⊳ πΣ₁ + Σ₂ pure $ InfRes { @@ -307,7 +307,7 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m} -- if Ψ | Γ ⊢ σ · t ⇒ {ts} ⊳ Σ₁ tres <- inferC ctx sg t -- if Ψ | Γ, x : {ts} ⊢₀ A ⇐ Type - checkTypeC (extendTy ret.name tres.type ctx) ret.term Nothing + checkTypeC (extendTy zero ret.name tres.type ctx) ret.term Nothing -- if for each "a ⇒ s" in arms, -- Ψ | Γ ⊢ σ · s ⇐ A[a ∷ {ts}/x] ⊳ Σ₂ -- for fixed Σ₂ @@ -325,7 +325,8 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m} allEqual [] = pure $ zeroFor ctx allEqual lst@((x, _) :: xs) = if all (\y => x == fst y) xs then pure x - else throwError $ BadCaseQtys ctx lst + else throwError $ BadCaseQtys ctx $ + map (\(qs, t, s) => (qs, Tag t, s)) lst infer' ctx sg (fun :% dim) = do -- if Ψ | Γ ⊢ σ · f ⇒ Eq [i ⇒ A] l r ⊳ Σ diff --git a/lib/Quox/Typing.idr b/lib/Quox/Typing.idr index 94a1b13..40e7339 100644 --- a/lib/Quox/Typing.idr +++ b/lib/Quox/Typing.idr @@ -110,30 +110,20 @@ parameters {auto _ : HasErr q m} (defs : Definitions' q _) 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 + expectTYPEE t = expectTYPE_ (toTyContext ctx) (shift0 ctx.dimLen) 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 + expectPiE t = expectPi_ (toTyContext ctx) (shift0 ctx.dimLen) 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 + expectSigE t = expectSig_ (toTyContext ctx) (shift0 ctx.dimLen) 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 + expectEnumE t = expectEnum_ (toTyContext ctx) (shift0 ctx.dimLen) 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 + expectEqE t = expectEq_ (toTyContext ctx) (shift0 ctx.dimLen) t diff --git a/lib/Quox/Typing/Context.idr b/lib/Quox/Typing/Context.idr index 53807c8..c1c9dd2 100644 --- a/lib/Quox/Typing/Context.idr +++ b/lib/Quox/Typing/Context.idr @@ -2,10 +2,15 @@ module Quox.Typing.Context import Quox.Syntax import Quox.Context +import Quox.Pretty %default total +public export +QContext : Type -> Nat -> Type +QContext = Context' + public export TContext : Type -> Nat -> Nat -> Type TContext q d = Context (Term q d) @@ -14,10 +19,6 @@ public export QOutput : Type -> Nat -> Type QOutput = Context' -public export -NContext : Nat -> Type -NContext = Context' BaseName - public export DimAssign : Nat -> Type DimAssign = Context' DimConst @@ -30,17 +31,19 @@ record TyContext q d n where dnames : NContext d tctx : TContext q d n tnames : NContext n + qtys : QContext q n -- only used for printing %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 + {dimLen : Nat} + dassign : DimAssign dimLen -- only used for printing + dnames : NContext dimLen -- only used for printing tctx : TContext q 0 n tnames : NContext n + qtys : QContext q n -- only used for printing %name EqContext ctx @@ -56,17 +59,20 @@ namespace TContext namespace TyContext public export %inline empty : TyContext q 0 0 - empty = MkTyContext {dctx = new, dnames = [<], tctx = [<], tnames = [<]} + empty = + MkTyContext {dctx = new, dnames = [<], tctx = [<], tnames = [<], qtys = [<]} export %inline - extendTyN : Telescope (\n => (BaseName, Term q d n)) from to -> + extendTyN : Telescope (\n => (q, 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 + let (qs, xs, ss) = unzip3 xss in + {qtys $= (. qs), 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)] + extendTy : q -> BaseName -> Term q d n -> TyContext q d n -> + TyContext q d (S n) + extendTy q x s = extendTyN [< (q, x, s)] export %inline extendDim : BaseName -> TyContext q d n -> TyContext q (S d) n @@ -98,41 +104,96 @@ 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 { +makeEqContext' : {d : Nat} -> 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 + tnames = ctx.tnames, + qtys = ctx.qtys } +export +makeEqContext : TyContext q d n -> DSubst d 0 -> EqContext q n +makeEqContext ctx@(MkTyContext {dnames, _}) th = + let (d' ** Refl) = lengthPrf0 dnames in makeEqContext' ctx th + namespace EqContext public export %inline empty : EqContext q 0 - empty = MkEqContext [<] [<] [<] [<] + empty = MkEqContext { + dassign = [<], dnames = [<], tctx = [<], tnames = [<], qtys = [<] + } export %inline - extendTyN : Telescope (\n => (BaseName, Term q 0 n)) from to -> + extendTyN : Telescope (\n => (q, 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 + let (qs, xs, ss) = unzip3 tel in + {qtys $= (. qs), 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)] + extendTy : q -> BaseName -> Term q 0 n -> EqContext q n -> EqContext q (S n) + extendTy q x s = extendTyN [< (q, 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 - }) + toTyContext : (e : EqContext q n) -> TyContext q e.dimLen n + toTyContext (MkEqContext {dimLen, dassign, dnames, tctx, tnames, qtys}) = + MkTyContext { + dctx = fromGround dassign, + tctx = map (// shift0 dimLen) tctx, + dnames, tnames, qtys + } + + +parameters {auto _ : (Eq q, PrettyHL q)} (unicode : Bool) + export covering + prettyTContext : QContext q n -> NContext n -> TContext q d n -> Doc HL + prettyTContext qs ns ctx = separate comma $ toList $ go qs ns ctx where + go : QContext q m -> NContext m -> TContext q d m -> SnocList (Doc HL) + go [<] [<] [<] = [<] + go (qs :< q) (xs :< x) (ctx :< t) = + go qs xs ctx :< runPretty unicode (prettyBind [q] x t) + + private + prettyDVars : NContext d -> Doc HL + prettyDVars ds = hseparate comma $ map (pretty0 unicode . DV) $ toList' ds + + export + prettyDimEq1 : (PrettyHL a, PrettyHL b) => NContext d -> a -> b -> Doc HL + prettyDimEq1 ds p q = runPretty unicode $ + local {dnames := toSnocList' ds} $ do + p <- pretty0M p; q <- pretty0M q + pure $ hsep [p, hl Syntax "=", q] + + export + prettyDimEqCons : NContext d -> DimEq' d -> Doc HL + prettyDimEqCons ds eqs = hseparate comma $ toList $ go ds eqs + where + go : NContext e -> Context (Maybe . Dim) e -> SnocList (Doc HL) + go [<] [<] = [<] + go (ds :< _) (eqs :< Nothing) = go ds eqs + go (ds :< x) (eqs :< Just d) = go ds eqs :< prettyDimEq1 ds (DV x) d + + export + prettyDimEq : NContext d -> DimEq d -> Doc HL + prettyDimEq ds ZeroIsOne = + prettyDVars ds <+> comma <++> prettyDimEq1 [<] Zero One + prettyDimEq ds (C eqs) = + prettyDVars ds <+> comma <%%> prettyDimEqCons ds eqs + + export covering + prettyTyContext : TyContext q d n -> Doc HL + prettyTyContext (MkTyContext dctx dnames tctx tnames qtys) = + sep [prettyDimEq dnames dctx <++> hl Syntax "|", + prettyTContext qtys tnames tctx] + + export covering + prettyEqContext : EqContext q n -> Doc HL + prettyEqContext (MkEqContext dassign dnames tctx tnames qtys) = + sep [prettyDimEqCons dnames (fromGround' dassign) <++> hl Syntax "|", + prettyTContext qtys tnames tctx] diff --git a/lib/Quox/Typing/Error.idr b/lib/Quox/Typing/Error.idr index 9f1e131..cf87e79 100644 --- a/lib/Quox/Typing/Error.idr +++ b/lib/Quox/Typing/Error.idr @@ -19,7 +19,7 @@ data Error q | ExpectedEq (TyContext q d n) (Term q d n) | BadUniverse Universe Universe | TagNotIn TagVal (SortedSet TagVal) -| BadCaseQtys (TyContext q d n) (List (QOutput q n, TagVal, Term q d n)) +| BadCaseQtys (TyContext q d n) (List (QOutput q n, Term q d n, Term q d n)) -- 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) @@ -30,7 +30,7 @@ data Error q | NotInScope Name | 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) +| WrongType (EqContext q n) (Term q 0 n) (Term q 0 n) -- extra context | WhileChecking @@ -136,3 +136,167 @@ parameters {auto _ : HasErr q m} expectModeU : EqMode -> Universe -> Universe -> m () expectModeU mode = expect (ClashU mode) $ ucmp mode + +private +prettyMode : EqMode -> Doc HL +prettyMode Equal = "equal to" +prettyMode Sub = "a subtype of" +prettyMode Super = "a supertype of" + +private +prettyModeU : EqMode -> Doc HL +prettyModeU Equal = "equal to" +prettyModeU Sub = "less than or equal to" +prettyModeU Super = "greater than or equal to" + +private +isTypeInUniverse : Maybe Universe -> Doc HL +isTypeInUniverse Nothing = "is a type" +isTypeInUniverse (Just k) = "is a type in universe" <++> prettyUniverse k + +parameters {auto _ : (Eq q, PrettyHL q)} (unicode : Bool) + private + termt : TyContext q d n -> Term q d n -> Doc HL + termt ctx = hang 4 . prettyTerm unicode ctx.dnames ctx.tnames + + private + terme : EqContext q n -> Term q 0 n -> Doc HL + terme ctx = hang 4 . prettyTerm unicode [<] ctx.tnames + + private + dissectCaseQtys : TyContext q d n -> + NContext n' -> List (QOutput q n', Term q d n, z) -> + List (Doc HL) + dissectCaseQtys ctx [<] arms = [] + dissectCaseQtys ctx (tel :< x) arms = + let qs = map (head . fst) arms + tl = dissectCaseQtys ctx tel (map (mapFst tail) arms) + in + if allSame qs then tl else + ("-" <++> asep [hsep [pretty0 unicode $ TV x, "is used with quantities"], + hseparate comma $ map (pretty0 unicode) qs]) :: tl + where + allSame : List q -> Bool + allSame [] = True + allSame (q :: qs) = all (== q) qs + + export + prettyWhnfError : WhnfError -> Doc HL + prettyWhnfError = \case + MissingEnumArm tag tags => + sep [hsep ["the tag", hl Tag $ pretty tag, "is not contained in"], + termt empty $ Enum $ fromList tags] + + -- [todo] only show some contexts, probably + export + prettyError : (showContext : Bool) -> Error q -> Doc HL + prettyError showContext = \case + ExpectedTYPE ctx s => + sep ["expected a type universe, but got", termt ctx s] + + ExpectedPi ctx s => + sep ["expected a function type, but got", termt ctx s] + + ExpectedSig ctx s => + sep ["expected a pair type, but got", termt ctx s] + + ExpectedEnum ctx s => + sep ["expected an enumeration type, but got", termt ctx s] + + ExpectedEq ctx s => + sep ["expected an equality type, but got", termt ctx s] + + BadUniverse k l => + sep ["the universe level", prettyUniverse k, + "is not strictly less than", prettyUniverse l] + + TagNotIn tag set => + sep [sep ["tag", prettyTag tag, "is not contained in"], + termt empty (Enum set)] + + BadCaseQtys ctx arms => + hang 4 $ sep $ + "inconsistent variable usage in case arms" :: + dissectCaseQtys ctx ctx.tnames arms + + ClashT ctx mode ty s t => + inEContext ctx $ + sep ["the term", terme ctx s, + hsep ["is not", prettyMode mode], terme ctx t, + "at type", terme ctx ty] + + ClashTy ctx mode a b => + inEContext ctx $ + sep ["the type", terme ctx a, + hsep ["is not", prettyMode mode], terme ctx b] + + ClashE ctx mode e f => + inEContext ctx $ + sep ["the term", terme ctx $ E e, + hsep ["is not", prettyMode mode], terme ctx $ E f] + + ClashU mode k l => + sep ["the universe level", prettyUniverse k, + hsep ["is not", prettyMode mode], prettyUniverse l] + + ClashQ pi rh => + sep ["the quantity", pretty0 unicode pi, + "is not equal to", pretty0 unicode rh] + + NotInScope x => + hsep [hl' Free $ pretty0 unicode x, "is not in scope"] + + NotType ctx s => + inTContext ctx $ + sep ["the term", termt ctx s, "is not a type"] + + WrongType ctx ty s => + inEContext ctx $ + sep ["the term", terme ctx s, + "cannot have type", terme ctx ty] + + WhileChecking ctx pi s a err => + vsep [inTContext ctx $ + sep ["while checking", termt ctx s, + "has type", termt ctx a, + hsep ["with quantity", pretty0 unicode pi]], + prettyError showContext err] + + WhileCheckingTy ctx a k err => + vsep [inTContext ctx $ + sep ["while checking", termt ctx a, + isTypeInUniverse k], + prettyError showContext err] + + WhileInferring ctx pi e err => + vsep [inTContext ctx $ + sep ["while inferring the type of", termt ctx $ E e, + hsep ["with quantity", pretty0 unicode pi]], + prettyError showContext err] + + WhileComparingT ctx mode s t a err => + vsep [inEContext ctx $ + sep ["while checking that", terme ctx s, + hsep ["is", prettyMode mode], terme ctx t, + "at type", terme ctx a], + prettyError showContext err] + + WhileComparingE ctx mode e f err => + vsep [inEContext ctx $ + sep ["while checking that", terme ctx $ E e, + hsep ["is", prettyMode mode], terme ctx $ E f], + prettyError showContext err] + + WhnfError err => prettyWhnfError err + where + inTContext : TyContext q d n -> Doc HL -> Doc HL + inTContext ctx doc = + if showContext then + vsep [sep ["in context", prettyTyContext unicode ctx], doc] + else doc + + inEContext : EqContext q n -> Doc HL -> Doc HL + inEContext ctx doc = + if showContext then + vsep [sep ["in context", prettyEqContext unicode ctx], doc] + else doc diff --git a/tests/Tests.idr b/tests/Tests.idr index c8c0ecf..300314a 100644 --- a/tests/Tests.idr +++ b/tests/Tests.idr @@ -17,7 +17,10 @@ allTests = [ Typechecker.tests, Lexer.tests, Parser.tests, - FromPTerm.tests + FromPTerm.tests, + todo "DimEq", + todo "Pretty term & dim", + todo "Pretty dctx/tctx/tyctx/eqctx" ] main : IO () diff --git a/tests/Tests/Equal.idr b/tests/Tests/Equal.idr index 9bc1c58..a339712 100644 --- a/tests/Tests/Equal.idr +++ b/tests/Tests/Equal.idr @@ -184,53 +184,55 @@ 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 (extendTyN [< ("x", ty), ("y", ty)] empty) + equalE (extendTyN [< (Any, "x", ty), (Any, "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 (extendTyN [< ("x", ty), ("y", ty)] empty) + equalE (extendTyN [< (Any, "x", ty), (Any, "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 (extendTyN [< ("x", FT "EE"), ("y", FT "EE")] empty) + equalE (extendTyN [< (Any, "x", FT "EE"), (Any, "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 (extendTyN [< ("x", FT "EE"), ("y", FT "E")] empty) + equalE (extendTyN [< (Any, "x", FT "EE"), (Any, "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 (extendTyN [< ("x", FT "E"), ("y", FT "E")] empty) (BV 0) (BV 1), + equalE (extendTyN [< (Any, "x", FT "E"), (Any, "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 (extendTyN [< ("x", ty), ("y", ty)] empty) (BV 0) (BV 1), + equalE (extendTyN [< (Any, "x", ty), (Any, "y", ty)] empty) + (BV 0) (BV 1), 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 - (extendTyN [< ("x", FT "W"), ("y", FT "W")] empty) + (extendTyN [< (Any, "x", FT "W"), (Any, "y", FT "W")] empty) (BV 0) (BV 1) ], "term closure" :- [ testEq "[#0]{} = [#0] : A" $ - equalT (extendTy "x" (FT "A") empty) + equalT (extendTy Any "x" (FT "A") empty) (FT "A") (CloT (BVT 0) id) (BVT 0), @@ -311,15 +313,18 @@ tests = "equality & subtyping" :- [ "bound var" :- [ testEq "#0 = #0" $ - equalE (extendTy "A" (TYPE 0) empty) (BV 0) (BV 0), + equalE (extendTy Any "A" (TYPE 0) empty) (BV 0) (BV 0), testEq "#0 <: #0" $ - subE (extendTy "A" (TYPE 0) empty) (BV 0) (BV 0), + subE (extendTy Any "A" (TYPE 0) empty) (BV 0) (BV 0), testNeq "#0 ≠ #1" $ - equalE (extendTyN [< ("A", TYPE 0), ("B", TYPE 0)] empty) (BV 0) (BV 1), + equalE (extendTyN [< (Any, "A", TYPE 0), (Any, "B", TYPE 0)] empty) + (BV 0) (BV 1), testNeq "#0 ≮: #1" $ - subE (extendTyN [< ("A", TYPE 0), ("B", TYPE 0)] empty) (BV 0) (BV 1), + subE (extendTyN [< (Any, "A", TYPE 0), (Any, "B", TYPE 0)] empty) + (BV 0) (BV 1), testEq "0=1 ⊢ #0 = #1" $ - equalE (extendTyN [< ("A", TYPE 0), ("B", TYPE 0)] empty01) (BV 0) (BV 1) + equalE (extendTyN [< (Any, "A", TYPE 0), (Any, "B", TYPE 0)] empty01) + (BV 0) (BV 1) ], "application" :- [ @@ -416,7 +421,7 @@ tests = "equality & subtyping" :- [ testEq "#0{a} = a" $ equalE empty (CloE (BV 0) (F "a" ::: id)) (F "a"), testEq "#1{a} = #0" $ - equalE (extendTy "x" (FT "A") empty) + equalE (extendTy Any "x" (FT "A") empty) (CloE (BV 1) (F "a" ::: id)) (BV 0) ], @@ -451,7 +456,7 @@ tests = "equality & subtyping" :- [ (F "eq-AB" :% K Zero), testEq "#0‹𝟎› = #0 # term and dim vars distinct" $ equalED 1 - (extendTy "x" (FT "A") $ extendDim "𝑖" empty) + (extendTy Any "x" (FT "A") $ extendDim "𝑖" empty) (DCloE (BV 0) (K Zero ::: id)) (BV 0), testEq "a‹𝟎› = a" $ equalED 1 (extendDim "𝑖" empty) (DCloE (F "a") (K Zero ::: id)) (F "a"), diff --git a/tests/Tests/Typechecker.idr b/tests/Tests/Typechecker.idr index 7aadb25..14f1d81 100644 --- a/tests/Tests/Typechecker.idr +++ b/tests/Tests/Typechecker.idr @@ -98,9 +98,16 @@ parameters (label : String) (act : Lazy (M ())) testTCFail = testThrows label (const True) $ runReaderT globals act -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) +anys : {n : Nat} -> QContext Three n +anys {n = 0} = [<] +anys {n = S n} = anys :< Any + +ctx, ctx01 : {n : Nat} -> Context (\n => (BaseName, Term Three 0 n)) n -> + TyContext Three 0 n +ctx tel = let (ns, ts) = unzip tel in + MkTyContext new [<] ts ns anys +ctx01 tel = let (ns, ts) = unzip tel in + MkTyContext ZeroIsOne [<] ts ns anys empty01 : TyContext Three 0 0 empty01 = {dctx := ZeroIsOne} empty diff --git a/tests/TypingImpls.idr b/tests/TypingImpls.idr index 9b45b7f..08d79cf 100644 --- a/tests/TypingImpls.idr +++ b/tests/TypingImpls.idr @@ -33,76 +33,5 @@ ToInfo WhnfError where ("list", show ts)] 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 (ExpectedEnum _ t) = - [("type", "ExpectedEnum"), - ("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 (TagNotIn t ts) = - [("type", "TagNotIn"), - ("tag", show t), - ("set", show $ SortedSet.toList ts)] - toInfo (BadCaseQtys _ qouts) = - ("type", "BadCaseQtys") :: - [(show i, prettyStr True q) | (i, _, _, q) <- zip [1 .. length qouts] qouts] - - 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) = - [("type", "ClashTy"), - ("mode", show mode), - ("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", show k), - ("right", show l)] - toInfo (ClashQ pi rh) = - [("type", "ClashQ"), - ("left", prettyStr True pi), - ("right", prettyStr True rh)] - toInfo (NotType _ ty) = - [("type", "NotType"), - ("got", prettyStr True ty)] - toInfo (WrongType _ ty s t) = - [("type", "WrongType"), - ("ty", prettyStr True ty), - ("left", prettyStr True s), - ("right", prettyStr True t)] - - -- [todo] add nested yamls to TAP and include context here - toInfo (WhileChecking _ _ _ _ err) = toInfo err - toInfo (WhileCheckingTy _ _ _ err) = toInfo err - toInfo (WhileInferring _ _ _ err) = toInfo err - toInfo (WhileComparingT _ _ _ _ _ err) = toInfo err - toInfo (WhileComparingE _ _ _ _ err) = toInfo err - - toInfo (WhnfError err) = toInfo err +(Eq q, PrettyHL q) => ToInfo (Error q) where + toInfo err = [("err", show $ prettyError True True err)]