rhi/quox
rhi/quox
1
0
Fork 0
Code Issues 15 Pull requests 1 Releases Wiki Activity

pretty printing errors

Browse source
This commit is contained in:
rhiannon morris 2023-03-15 15:54:51 +01:00
parent 54ba4e237f
commit 32f38238ef
14 changed files with 424 additions and 217 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

27
lib/Quox/Context.idr
View file

@ -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

76
lib/Quox/Equal.idr
View file

@ -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`

10
lib/Quox/Pretty.idr
View file

@ -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

27
lib/Quox/Syntax/Dim.idr
View file

@ -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`;

7
lib/Quox/Syntax/Qty/Three.idr
View file

@ -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

36
lib/Quox/Syntax/Term/Pretty.idr
View file

@ -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

21
lib/Quox/Typechecker.idr
View file

@ -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 ⊳ Σ

20
lib/Quox/Typing.idr
View file

@ -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

121
lib/Quox/Typing/Context.idr
View file

@ -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]

168
lib/Quox/Typing/Error.idr
View file

@ -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

5
tests/Tests.idr
View file

@ -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 ()

35
tests/Tests/Equal.idr
View file

@ -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"),

13
tests/Tests/Typechecker.idr
View file

@ -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

75
tests/TypingImpls.idr
View file

@ -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)]