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

put names into contexts, and contexts into errors

Browse source
This commit is contained in:
rhiannon morris 2023-03-14 03:22:26 +01:00
parent f4af1a5a78
commit 86d21caf24
13 changed files with 520 additions and 324 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
exe/Main.idr
View file

@ -58,7 +58,7 @@ tm : Term Three 1 2
tm = tm =
(Pi_ One "a" (BVT 0) (E (F "F" :@@ [BVT 0, FT "w"])) (Pi_ One "a" (BVT 0) (E (F "F" :@@ [BVT 0, FT "w"]))
`DCloT` (K One ::: id)) `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 : IO Unit
main = do main = do

6
lib/Quox/Context.idr
View file

@ -174,6 +174,12 @@ zipWithLazy : forall tm1, tm2, tm3.
Telescope (\n => Lazy (tm3 n)) from to Telescope (\n => Lazy (tm3 n)) from to
zipWithLazy f = zipWith $ delay .: f 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 export
lengthPrf : Telescope _ from to -> Subset Nat (\len => len + from = to) lengthPrf : Telescope _ from to -> Subset Nat (\len => len + from = to)

128
lib/Quox/Equal.idr
View file

@ -27,17 +27,18 @@ private %inline
mode : HasCmpContext m => m EqMode mode : HasCmpContext m => m EqMode
mode = asks mode mode = asks mode
parameters {auto _ : CanEqual q m} (ctx : EqContext q n)
private %inline private %inline
clashT : CanEqual q m => Term q d n -> Term q d n -> Term q d n -> m a clashT : Term q 0 n -> Term q 0 n -> Term q 0 n -> m a
clashT ty s t = throwError $ ClashT !mode ty s t clashT ty s t = throwError $ ClashT ctx !mode ty s t
private %inline private %inline
clashTy : CanEqual q m => Term q d n -> Term q d n -> m a clashTy : Term q 0 n -> Term q 0 n -> m a
clashTy s t = throwError $ ClashTy !mode s t clashTy s t = throwError $ ClashTy ctx !mode s t
private %inline private %inline
clashE : CanEqual q m => Elim q d n -> Elim q d n -> m a clashE : Elim q 0 n -> Elim q 0 n -> m a
clashE e f = throwError $ ClashE !mode e f clashE e f = throwError $ ClashE ctx !mode e f
||| true if a term is syntactically a type, or is neutral. ||| true if a term is syntactically a type, or is neutral.
@ -114,8 +115,12 @@ parameters {auto _ : HasErr q m}
Right _ => throwError $ e t Right _ => throwError $ e t
export %inline export %inline
ensureTyCon : HasErr q m => (t : Term q d n) -> m (So (isTyCon t)) ensureTyCon : (ctx : EqContext q n) -> (t : Term q 0 n) -> m (So (isTyCon t))
ensureTyCon = ensure NotType isTyCon 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, Eq q)}
mutual 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`**. ⚠ ||| ⚠ **assumes that `s`, `t` have already been checked against `ty`**. ⚠
export covering %inline 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 = 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 ty nty <- whnfT defs ty
Element s ns <- whnfT defs s Element s ns <- whnfT defs s
Element t nt <- whnfT defs t Element t nt <- whnfT defs t
tty <- ensureTyCon ty tty <- ensureTyCon ctx ty
compare0' ctx ty s t compare0' ctx ty s t
||| converts an elim "Γ ⊢ e" to "Γ, x ⊢ e x", for comparing with ||| 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 toLamBody e = E $ weakE e :@ BVT 0
private covering private covering
compare0' : TContext q 0 n -> compare0' : EqContext q n ->
(ty, s, t : Term q 0 n) -> (ty, s, t : Term q 0 n) ->
(0 nty : NotRedex defs ty) => (0 tty : So (isTyCon ty)) => (0 nty : NotRedex defs ty) => (0 tty : So (isTyCon ty)) =>
(0 ns : NotRedex defs s) => (0 nt : NotRedex defs t) => (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 (Lam b, E e) => eta e b
(E e, E f) => Elim.compare0 ctx e f (E e, E f) => Elim.compare0 ctx e f
_ => throwError $ WrongType ty s t _ => throwError $ WrongType ctx ty s t
where where
ctx' : TContext q 0 (S n) ctx' : EqContext q (S n)
ctx' = ctx :< arg ctx' = extendTy res.name arg ctx
eta : Elim q 0 n -> ScopeTerm q 0 n -> m () 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 _ (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} $ compare0' ctx ty@(Sig {fst, snd, _}) s t = local {mode := Equal} $
case (s, t) of 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 compare0 ctx (sub1 snd (sFst :# fst)) sSnd tSnd
(E e, E f) => compare0 ctx e f (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} $ compare0' ctx ty@(Enum tags) s t = local {mode := Equal} $
case (s, t) of case (s, t) of
@ -191,9 +196,9 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)}
-- Γ ⊢ `t = `t : {ts} -- Γ ⊢ `t = `t : {ts}
-- --
-- t ∈ ts is in the typechecker, not here, ofc -- 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 (E e, E f) => compare0 ctx e f
_ => throwError $ WrongType ty s t _ => throwError $ WrongType ctx ty s t
compare0' _ (Eq {}) _ _ = compare0' _ (Eq {}) _ _ =
-- ✨ uip ✨ -- ✨ uip ✨
@ -204,25 +209,25 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)}
compare0' ctx ty@(E _) s t = do compare0' ctx ty@(E _) s t = do
-- a neutral type can only be inhabited by neutral values -- a neutral type can only be inhabited by neutral values
-- e.g. an abstract value in an abstract type, bound variables, … -- e.g. an abstract value in an abstract type, bound variables, …
E e <- pure s | _ => throwError $ WrongType ty s t E e <- pure s | _ => throwError $ WrongType ctx ty s t
E f <- pure t | _ => throwError $ WrongType ty s t E f <- pure t | _ => throwError $ WrongType ctx ty s t
Elim.compare0 ctx e f Elim.compare0 ctx e f
||| compares two types, using the current variance `mode` for universes. ||| compares two types, using the current variance `mode` for universes.
||| fails if they are not types, even if they would happen to be equal. ||| fails if they are not types, even if they would happen to be equal.
export covering %inline 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 compareType ctx s t = do
Element s ns <- whnfT defs s Element s ns <- whnfT defs s
Element t nt <- whnfT defs t Element t nt <- whnfT defs t
ts <- ensureTyCon s ts <- ensureTyCon ctx s
tt <- ensureTyCon t tt <- ensureTyCon ctx t
st <- either pure (const $ clashTy s t) $ st <- either pure (const $ clashTy ctx s t) $
nchoose $ sameTyCon s t nchoose $ sameTyCon s t
compareType' ctx s t compareType' ctx s t
private covering 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 ns : NotRedex defs s) => (0 ts : So (isTyCon s)) =>
(0 nt : NotRedex defs t) => (0 tt : So (isTyCon t)) => (0 nt : NotRedex defs t) => (0 tt : So (isTyCon t)) =>
(0 st : So (sameTyCon s 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₂ -- Γ ⊢ (π·x : A₁) → B₁ <: (π·x : A₂) → B₂
expectEqualQ sQty tQty expectEqualQ sQty tQty
local {mode $= flip} $ compareType ctx sArg tArg -- contra 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, _}) compareType' ctx (Sig {fst = sFst, snd = sSnd, _})
(Sig {fst = tFst, snd = tSnd, _}) = do (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₂ -- Γ ⊢ (x : A₁) × B₁ <: (x : A₂) × B₂
compareType ctx sFst tFst 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, _}) compareType' ctx (Eq {ty = sTy, l = sl, r = sr, _})
(Eq {ty = tTy, l = tl, r = tr, _}) = do (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› -- Γ ⊢ l₁ = l₂ : A₁‹𝟎/i› Γ ⊢ r₁ = r₂ : A₁‹𝟏/i›
-- ------------------------------------------------ -- ------------------------------------------------
-- Γ ⊢ Eq [i ⇒ A₁] l₁ r₂ <: Eq [i ⇒ A₂] l₂ r₂ -- Γ ⊢ Eq [i ⇒ A₁] l₁ r₂ <: Eq [i ⇒ A₂] l₂ r₂
compareType ctx sTy.zero tTy.zero compareType (extendDim sTy.name Zero ctx) sTy.zero tTy.zero
compareType ctx sTy.one tTy.one compareType (extendDim sTy.name One ctx) sTy.one tTy.one
local {mode := Equal} $ do local {mode := Equal} $ do
Term.compare0 ctx sTy.zero sl tl Term.compare0 ctx sTy.zero sl tl
Term.compare0 ctx sTy.one sr tr 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 -- no subtyping based on tag subsets, since that would need
-- a runtime coercion -- a runtime coercion
unless (tags1 == tags2) $ clashTy s t unless (tags1 == tags2) $ clashTy ctx s t
compareType' ctx (E e) (E f) = do compareType' ctx (E e) (E f) = do
-- no fanciness needed here cos anything other than a neutral -- 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.** ⚠ ||| ⚠ **assumes the elim is already typechecked.** ⚠
private covering 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) -> (0 ne : NotRedex defs e) ->
m (Term q 0 n) m (Term q 0 n)
computeElimType ctx (F x) _ = do computeElimType ctx (F x) _ = do
defs <- lookupFree' defs x defs <- lookupFree' defs x
pure $ defs.type.get pure $ defs.type.get
computeElimType ctx (B i) _ = do computeElimType ctx (B i) _ = do
pure $ ctx !! i pure $ ctx.tctx !! i
computeElimType ctx (f :@ s) ne = do 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) pure $ sub1 res (s :# arg)
computeElimType ctx (CasePair {pair, ret, _}) _ = do computeElimType ctx (CasePair {pair, ret, _}) _ = do
pure $ sub1 ret pair pure $ sub1 ret pair
computeElimType ctx (CaseEnum {tag, ret, _}) _ = do computeElimType ctx (CaseEnum {tag, ret, _}) _ = do
pure $ sub1 ret tag pure $ sub1 ret tag
computeElimType ctx (f :% p) ne = do 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 pure $ dsub1 ty p
computeElimType ctx (_ :# ty) _ = do computeElimType ctx (_ :# ty) _ = do
pure ty pure ty
private covering private covering
replaceEnd : TContext q 0 n -> replaceEnd : EqContext q n ->
(e : Elim q 0 n) -> DimConst -> (0 ne : NotRedex defs e) -> (e : Elim q 0 n) -> DimConst -> (0 ne : NotRedex defs e) ->
m (Elim q 0 n) m (Elim q 0 n)
replaceEnd ctx e p ne = do 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) pure $ ends l r p :# dsub1 ty (K p)
namespace Elim 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 ||| ⚠ **assumes that they have both been typechecked, and have
||| equal types.** ⚠ ||| equal types.** ⚠
export covering %inline 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 = 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 e ne <- whnfT defs e
Element f nf <- whnfT defs f Element f nf <- whnfT defs f
-- [fixme] there is a better way to do this "isSubSing" stuff for sure -- [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 compare0' ctx e f ne nf
private covering private covering
compare0' : TContext q 0 n -> compare0' : EqContext q n ->
(e, f : Elim q 0 n) -> (e, f : Elim q 0 n) ->
(0 ne : NotRedex defs e) -> (0 nf : NotRedex defs f) -> (0 ne : NotRedex defs e) -> (0 nf : NotRedex defs f) ->
m () 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 (f :% K q) ne nf =
compare0 ctx e !(replaceEnd ctx f q $ noOr1 nf) compare0 ctx e !(replaceEnd ctx f q $ noOr1 nf)
compare0' _ e@(F x) f@(F y) _ _ = unless (x == y) $ clashE e f compare0' ctx e@(F x) f@(F y) _ _ = unless (x == y) $ clashE ctx e f
compare0' _ e@(F _) f _ _ = clashE 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' ctx e@(B i) f@(B j) _ _ = unless (i == j) $ clashE ctx e f
compare0' _ e@(B _) f _ _ = clashE e f compare0' ctx e@(B _) f _ _ = clashE ctx e f
compare0' ctx (e :@ s) (f :@ t) ne nf = compare0' ctx (e :@ s) (f :@ t) ne nf =
local {mode := Equal} $ do local {mode := Equal} $ do
compare0 ctx e f 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 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) compare0' ctx (CasePair epi e eret ebody)
(CasePair fpi f fret fbody) ne nf = (CasePair fpi f fret fbody) ne nf =
local {mode := Equal} $ do local {mode := Equal} $ do
compare0 ctx e f compare0 ctx e f
ety <- computeElimType ctx e (noOr1 ne) ety <- computeElimType ctx e (noOr1 ne)
compareType (ctx :< ety) eret.term fret.term compareType (extendTy eret.name ety ctx) eret.term fret.term
(fst, snd) <- expectSig defs ety (fst, snd) <- expectSigE defs ctx ety
Term.compare0 (ctx :< fst :< snd.term) (substCasePairRet ety eret) let [x, y] = ebody.names
Term.compare0 (extendTyN [< (x, fst), (y, snd.term)] ctx)
(substCasePairRet ety eret)
ebody.term fbody.term ebody.term fbody.term
expectEqualQ epi fpi 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) compare0' ctx (CaseEnum epi e eret earms)
(CaseEnum fpi f fret farms) ne nf = (CaseEnum fpi f fret farms) ne nf =
local {mode := Equal} $ do local {mode := Equal} $ do
compare0 ctx e f compare0 ctx e f
ety <- computeElimType ctx e (noOr1 ne) ety <- computeElimType ctx e (noOr1 ne)
compareType (ctx :< ety) eret.term fret.term compareType (extendTy eret.name ety ctx) eret.term fret.term
for_ !(expectEnum defs ety) $ \t => for_ !(expectEnumE defs ctx ety) $ \t =>
compare0 ctx (sub1 eret $ Tag t :# ety) compare0 ctx (sub1 eret $ Tag t :# ety)
!(lookupArm t earms) !(lookupArm t farms) !(lookupArm t earms) !(lookupArm t farms)
expectEqualQ epi fpi 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 lookupArm t arms = case lookup t arms of
Just arm => pure arm Just arm => pure arm
Nothing => throwError $ TagNotIn t (fromList $ keys arms) 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) _ _ = compare0' ctx (s :# a) (t :# b) _ _ =
Term.compare0 ctx !(bigger a b) s t 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 (s :# a) f _ _ = Term.compare0 ctx a s (E f)
compare0' ctx e (t :# b) _ _ = Term.compare0 ctx b (E e) t 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) 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) parameters (mode : EqMode)
namespace Term namespace Term
export covering export covering
@ -404,8 +414,8 @@ parameters {auto _ : (HasDefs' q _ m, HasErr q m, Eq q)} (ctx : TyContext q d n)
defs <- ask defs <- ask
runReaderT {m} (MkCmpContext {mode}) $ runReaderT {m} (MkCmpContext {mode}) $
for_ (splits ctx.dctx) $ \th => for_ (splits ctx.dctx) $ \th =>
compare0 defs (map (// th) ctx.tctx) let ectx = makeEqContext ctx th in
(ty // th) (s // th) (t // th) compare0 defs ectx (ty // th) (s // th) (t // th)
export covering export covering
compareType : (s, t : Term q d n) -> m () 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 defs <- ask
runReaderT {m} (MkCmpContext {mode}) $ runReaderT {m} (MkCmpContext {mode}) $
for_ (splits ctx.dctx) $ \th => 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 namespace Elim
||| you don't have to pass the type in but the arguments must still be ||| 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 defs <- ask
runReaderT {m} (MkCmpContext {mode}) $ runReaderT {m} (MkCmpContext {mode}) $
for_ (splits ctx.dctx) $ \th => 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 namespace Term
export covering %inline export covering %inline

10
lib/Quox/Syntax/DimEq.idr
View file

@ -60,6 +60,16 @@ ifConsistent ZeroIsOne act = pure Nothing
ifConsistent (C _) act = Just <$> act 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 export %inline
zeroEq : DimEq 0 zeroEq : DimEq 0
zeroEq = C [<] zeroEq = C [<]

4
lib/Quox/Syntax/Subst.idr
View file

@ -58,6 +58,10 @@ public export %inline
shift : (by : Nat) -> Subst env from (by + from) shift : (by : Nat) -> Subst env from (by + from)
shift by = Shift $ fromNat by 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 public export
(.) : CanSubstSelf f => Subst f from mid -> Subst f mid to -> Subst f from to (.) : CanSubstSelf f => Subst f from mid -> Subst f mid to -> Subst f from to

8
lib/Quox/Syntax/Term/Base.idr
View file

@ -165,6 +165,14 @@ public export %inline
SY : Vect s BaseName -> f (s + n) -> Scoped s f n SY : Vect s BaseName -> f (s + n) -> Scoped s f n
SY ns = S ns . Y 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 ||| more convenient Pi
public export %inline public export %inline
Pi_ : (qty : q) -> (x : BaseName) -> Pi_ : (qty : q) -> (x : BaseName) ->

66
lib/Quox/Typechecker.idr
View file

@ -3,6 +3,8 @@ module Quox.Typechecker
import public Quox.Typing import public Quox.Typing
import public Quox.Equal import public Quox.Equal
import Data.List
%default total %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 -> (subj : Term q d n) -> (0 nc : NotClo subj) => Term q d n ->
m (CheckResult' q n) m (CheckResult' q n)
toCheckType ctx sg t ty = do toCheckType ctx sg t ty = do
u <- expectTYPE !ask ty u <- expectTYPE !ask ctx ty
expectEqualQ zero sg.fst expectEqualQ zero sg.fst
checkTypeNoWrap ctx t (Just u) checkTypeNoWrap ctx t (Just u)
pure $ zeroFor ctx 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 t@(Pi {}) ty = toCheckType ctx sg t ty
check' ctx sg (Lam body) ty = do 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 -- if Ψ | Γ, x : A ⊢ σ · t ⇐ B ⊳ Σ, ρ·x
-- with ρ ≤ σπ -- with ρ ≤ σπ
let qty' = sg.fst * qty 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 ⊳ Σ -- then Ψ | Γ ⊢ σ · (λx ⇒ t) ⇐ (π·x : A) → B ⊳ Σ
popQ qty' qout popQ qty' qout
check' ctx sg t@(Sig {}) ty = toCheckType ctx sg t ty check' ctx sg t@(Sig {}) ty = toCheckType ctx sg t ty
check' ctx sg (Pair fst snd) ty = do check' ctx sg (Pair fst snd) ty = do
(tfst, tsnd) <- expectSig !ask ty (tfst, tsnd) <- expectSig !ask ctx ty
-- if Ψ | Γ ⊢ σ · s ⇐ A ⊳ Σ₁ -- if Ψ | Γ ⊢ σ · s ⇐ A ⊳ Σ₁
qfst <- checkC ctx sg fst tfst qfst <- checkC ctx sg fst tfst
let tsnd = sub1 tsnd (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 t@(Enum _) ty = toCheckType ctx sg t ty
check' ctx sg (Tag t) ty = do check' ctx sg (Tag t) ty = do
tags <- expectEnum !ask ty tags <- expectEnum !ask ctx ty
-- if t ∈ ts -- if t ∈ ts
unless (t `elem` tags) $ throwError $ TagNotIn t tags unless (t `elem` tags) $ throwError $ TagNotIn t tags
-- then Ψ | Γ ⊢ σ · t ⇐ {ts} ⊳ 𝟎 -- 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 t@(Eq {}) ty = toCheckType ctx sg t ty
check' ctx sg (DLam body) ty = do check' ctx sg (DLam body) ty = do
(ty, l, r) <- expectEq !ask ty (ty, l, r) <- expectEq !ask ctx ty
-- if Ψ, i | Γ ⊢ σ · t ⇐ A ⊳ Σ -- 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› -- if Ψ | Γ ⊢ t‹0› = l : A‹0›
equal ctx ty.zero body.zero l equal ctx ty.zero body.zero l
-- if Ψ | Γ ⊢ t‹1› = r : A‹1› -- if Ψ | Γ ⊢ t‹1› = r : A‹1›
@ -188,36 +190,36 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
checkTypeC ctx arg u checkTypeC ctx arg u
-- if Ψ | Γ, x : A ⊢₀ B ⇐ Type ℓ -- if Ψ | Γ, x : A ⊢₀ B ⇐ Type ℓ
case res.body of case res.body of
Y res => checkTypeC (extendTy arg ctx) res u Y res' => checkTypeC (extendTy res.name arg ctx) res' u
N res => checkTypeC ctx res u N res' => checkTypeC ctx res' u
-- then Ψ | Γ ⊢₀ (π·x : A) → B ⇐ Type ℓ -- then Ψ | Γ ⊢₀ (π·x : A) → B ⇐ Type ℓ
checkType' ctx t@(Lam {}) u = checkType' ctx t@(Lam {}) u =
throwError $ NotType t throwError $ NotType ctx t
checkType' ctx (Sig fst snd) u = do checkType' ctx (Sig fst snd) u = do
-- if Ψ | Γ ⊢₀ A ⇐ Type ℓ -- if Ψ | Γ ⊢₀ A ⇐ Type ℓ
checkTypeC ctx fst u checkTypeC ctx fst u
-- if Ψ | Γ, x : A ⊢₀ B ⇐ Type ℓ -- if Ψ | Γ, x : A ⊢₀ B ⇐ Type ℓ
case snd.body of case snd.body of
Y snd => checkTypeC (extendTy fst ctx) snd u Y snd' => checkTypeC (extendTy snd.name fst ctx) snd' u
N snd => checkTypeC ctx snd u N snd' => checkTypeC ctx snd' u
-- then Ψ | Γ ⊢₀ (x : A) × B ⇐ Type ℓ -- then Ψ | Γ ⊢₀ (x : A) × B ⇐ Type ℓ
checkType' ctx t@(Pair {}) u = checkType' ctx t@(Pair {}) u =
throwError $ NotType t throwError $ NotType ctx t
checkType' ctx (Enum _) u = pure () checkType' ctx (Enum _) u = pure ()
-- Ψ | Γ ⊢₀ {ts} ⇐ Type ℓ -- Ψ | Γ ⊢₀ {ts} ⇐ Type ℓ
checkType' ctx t@(Tag {}) u = checkType' ctx t@(Tag {}) u =
throwError $ NotType t throwError $ NotType ctx t
checkType' ctx (Eq t l r) u = do checkType' ctx (Eq t l r) u = do
-- if Ψ, i | Γ ⊢₀ A ⇐ Type ℓ -- if Ψ, i | Γ ⊢₀ A ⇐ Type ℓ
case t.body of case t.body of
Y t => checkTypeC (extendDim ctx) t u Y t' => checkTypeC (extendDim t.name ctx) t' u
N t => checkTypeC ctx t u N t' => checkTypeC ctx t' u
-- if Ψ | Γ ⊢₀ l ⇐ A‹0› -- if Ψ | Γ ⊢₀ l ⇐ A‹0›
check0 ctx t.zero l check0 ctx t.zero l
-- if Ψ | Γ ⊢₀ r ⇐ A‹1› -- if Ψ | Γ ⊢₀ r ⇐ A‹1›
@ -225,7 +227,7 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
-- then Ψ | Γ ⊢₀ Eq [i ⇒ A] l r ⇐ Type ℓ -- then Ψ | Γ ⊢₀ Eq [i ⇒ A] l r ⇐ Type ℓ
checkType' ctx t@(DLam {}) u = checkType' ctx t@(DLam {}) u =
throwError $ NotType t throwError $ NotType ctx t
checkType' ctx (E e) u = do checkType' ctx (E e) u = do
-- if Ψ | Γ ⊢ σ · e ⇒ A' ⊳ Σ -- if Ψ | Γ ⊢ σ · e ⇒ A' ⊳ Σ
@ -233,7 +235,7 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
-- if Ψ | Γ ⊢ A' <: A -- if Ψ | Γ ⊢ A' <: A
case u of case u of
Just u => subtype ctx infres.type (TYPE u) Just u => subtype ctx infres.type (TYPE u)
Nothing => ignore $ expectTYPE !ask infres.type Nothing => ignore $ expectTYPE !ask ctx infres.type
-- then Ψ | Γ ⊢ σ · e ⇐ A ⊳ Σ -- then Ψ | Γ ⊢ σ · e ⇐ A ⊳ Σ
@ -268,7 +270,7 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
infer' ctx sg (fun :@ arg) = do infer' ctx sg (fun :@ arg) = do
-- if Ψ | Γ ⊢ σ · f ⇒ (π·x : A) → B ⊳ Σ₁ -- if Ψ | Γ ⊢ σ · f ⇒ (π·x : A) → B ⊳ Σ₁
funres <- inferC ctx sg fun funres <- inferC ctx sg fun
(qty, argty, res) <- expectPi !ask funres.type (qty, argty, res) <- expectPi !ask ctx funres.type
-- if Ψ | Γ ⊢ σ ⨴ π · s ⇐ A ⊳ Σ₂ -- if Ψ | Γ ⊢ σ ⨴ π · s ⇐ A ⊳ Σ₂
argout <- checkC ctx (subjMult sg qty) arg argty argout <- checkC ctx (subjMult sg qty) arg argty
-- then Ψ | Γ ⊢ σ · f s ⇒ B[s] ⊳ Σ₁ + Σ₂ -- then Ψ | Γ ⊢ σ · f s ⇒ B[s] ⊳ Σ₁ + Σ₂
@ -283,12 +285,13 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
-- if Ψ | Γ ⊢ σ · pair ⇒ (x : A) × B ⊳ Σ₁ -- if Ψ | Γ ⊢ σ · pair ⇒ (x : A) × B ⊳ Σ₁
pairres <- inferC ctx sg pair pairres <- inferC ctx sg pair
-- if Ψ | Γ, p : (x : A) × B ⊢₀ ret ⇐ Type -- if Ψ | Γ, p : (x : A) × B ⊢₀ ret ⇐ Type
checkTypeC (extendTy pairres.type ctx) ret.term Nothing checkTypeC (extendTy ret.name pairres.type ctx) ret.term Nothing
(tfst, tsnd) <- expectSig !ask pairres.type (tfst, tsnd) <- expectSig !ask ctx pairres.type
-- if Ψ | Γ, x : A, y : B ⊢ σ · body ⇐ -- if Ψ | Γ, x : A, y : B ⊢ σ · body ⇐
-- ret[(x, y) ∷ (x : A) × B/p] ⊳ Σ₂, ρ₁·x, ρ₂·y -- ret[(x, y) ∷ (x : A) × B/p] ⊳ Σ₂, ρ₁·x, ρ₂·y
-- with ρ₁, ρ₂ ≤ πσ -- 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 bodyty = substCasePairRet pairres.type ret
pisg = pi * sg.fst pisg = pi * sg.fst
bodyout <- checkC bodyctx sg body.term bodyty 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) 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 ≤ π -- if 1 ≤ π
expectCompatQ one pi expectCompatQ one pi
-- if Ψ | Γ ⊢ σ · t ⇒ {ts} ⊳ Σ₁ -- if Ψ | Γ ⊢ σ · t ⇒ {ts} ⊳ Σ₁
tres <- inferC ctx sg t tres <- inferC ctx sg t
-- if Ψ | Γ, x : {ts} ⊢₀ A ⇐ Type -- 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, -- if for each "a ⇒ s" in arms,
-- Ψ | Γ ⊢ σ · s ⇐ A[a ∷ {ts}/x] ⊳ Σ₂ -- Ψ | Γ ⊢ σ · s ⇐ A[a ∷ {ts}/x] ⊳ Σ₂
-- for fixed Σ₂ -- 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)) checkC ctx sg s (sub1 ret (Tag a :# tres.type))
armout <- allEqual armres armout <- allEqual (zip armres arms)
-- then Ψ | Γ ⊢ σ · case ⋯ ⇒ ret[t/x] ⊳ πΣ₁ + Σ₂ -- then Ψ | Γ ⊢ σ · case ⋯ ⇒ ret[t/x] ⊳ πΣ₁ + Σ₂
pure $ InfRes { pure $ InfRes {
type = sub1 ret t, type = sub1 ret t,
qout = pi * tres.qout + armout qout = pi * tres.qout + armout
} }
where 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 [] = pure $ zeroFor ctx
allEqual lst@(x :: xs) = allEqual lst@((x, _) :: xs) =
if all (== x) xs then pure x if all (\y => x == fst y) xs then pure x
else throwError $ BadCaseQtys lst else throwError $ BadCaseQtys ctx lst
infer' ctx sg (fun :% dim) = do infer' ctx sg (fun :% dim) = do
-- if Ψ | Γ ⊢ σ · f ⇒ Eq [i ⇒ A] l r ⊳ Σ -- if Ψ | Γ ⊢ σ · f ⇒ Eq [i ⇒ A] l r ⊳ Σ
InfRes {type, qout} <- inferC ctx sg fun InfRes {type, qout} <- inferC ctx sg fun
ty <- fst <$> expectEq !ask type ty <- fst <$> expectEq !ask ctx type
-- then Ψ | Γ ⊢ σ · f p ⇒ A‹p› ⊳ Σ -- then Ψ | Γ ⊢ σ · f p ⇒ A‹p› ⊳ Σ
pure $ InfRes {type = dsub1 ty dim, qout} pure $ InfRes {type = dsub1 ty dim, qout}

139
lib/Quox/Typing.idr
View file

@ -11,53 +11,6 @@ import public Quox.Reduce
%default total %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 $= (:<? Nothing), tctx $= pushD}
export %inline
eqDim : Dim d -> 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 public export
CheckResult' : Type -> Nat -> Type CheckResult' : Type -> Nat -> Type
CheckResult' = QOutput 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) tm q d n -> m (NonRedex tm q d n defs)
whnfT = either (throwError . WhnfError) pure . whnf defs whnfT = either (throwError . WhnfError) pure . whnf defs
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 ctx (s // th)
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 ctx (s // th)
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 ctx (s // th)
export covering %inline
expectEnum_ : Term q d2 n -> m (SortedSet TagVal)
expectEnum_ s = case fst !(whnfT s) of
Enum tags => pure tags
_ => throwError $ ExpectedEnum ctx (s // th)
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 ctx (s // th)
-- [fixme] refactor this stuff
parameters (ctx : TyContext q d n)
export covering %inline export covering %inline
expectTYPE : Term q d n -> m Universe expectTYPE : Term q d n -> m Universe
expectTYPE s = expectTYPE = expectTYPE_ ctx id
case fst !(whnfT s) of
TYPE l => pure l
_ => throwError $ ExpectedTYPE s
export covering %inline export covering %inline
expectPi : Term q d n -> m (q, Term q d n, ScopeTerm q d n) expectPi : Term q d n -> m (q, Term q d n, ScopeTerm q d n)
expectPi s = expectPi = expectPi_ ctx id
case fst !(whnfT s) of
Pi {qty, arg, res, _} => pure (qty, arg, res)
_ => throwError $ ExpectedPi s
export covering %inline export covering %inline
expectSig : Term q d n -> m (Term q d n, ScopeTerm q d n) expectSig : Term q d n -> m (Term q d n, ScopeTerm q d n)
expectSig s = expectSig = expectSig_ ctx id
case fst !(whnfT s) of
Sig {fst, snd, _} => pure (fst, snd)
_ => throwError $ ExpectedSig s
export covering %inline export covering %inline
expectEnum : Term q d n -> m (SortedSet TagVal) expectEnum : Term q d n -> m (SortedSet TagVal)
expectEnum s = expectEnum = expectEnum_ ctx id
case fst !(whnfT s) of
Enum tags => pure tags
_ => throwError $ ExpectedEnum s
export covering %inline export covering %inline
expectEq : Term q d n -> m (DScopeTerm q d n, Term q d n, Term q d n) expectEq : Term q d n -> m (DScopeTerm q d n, Term q d n, Term q d n)
expectEq s = expectEq = expectEq_ ctx id
case fst !(whnfT s) of
Eq {ty, l, r, _} => pure (ty, l, r)
_ => throwError $ ExpectedEq s 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

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

@ -3,6 +3,8 @@ module Quox.Typing.Context
import Quox.Syntax import Quox.Syntax
import Quox.Context import Quox.Context
%default total
public export public export
TContext : Type -> Nat -> Nat -> Type TContext : Type -> Nat -> Nat -> Type
@ -12,11 +14,125 @@ public export
QOutput : Type -> Nat -> Type QOutput : Type -> Nat -> Type
QOutput = Context' QOutput = Context'
public export
NContext : Nat -> Type
NContext = Context' BaseName
public export
DimAssign : Nat -> Type
DimAssign = Context' DimConst
public export public export
record TyContext q d n where record TyContext q d n where
constructor MkTyContext constructor MkTyContext
dctx : DimEq d dctx : DimEq d
dnames : NContext d
tctx : TContext q d n tctx : TContext q d n
tnames : NContext n
%name TyContext ctx %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 $= (:<? Nothing), dnames $= (:< x), tctx $= pushD}
export %inline
eqDim : Dim d -> 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
})

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

@ -12,26 +12,25 @@ import public Control.Monad.Either
public export public export
data Error q data Error q
= ExpectedTYPE (Term q d n) = ExpectedTYPE (TyContext q d n) (Term q d n)
| ExpectedPi (Term q d n) | ExpectedPi (TyContext q d n) (Term q d n)
| ExpectedSig (Term q d n) | ExpectedSig (TyContext q d n) (Term q d n)
| ExpectedEnum (Term q d n) | ExpectedEnum (TyContext q d n) (Term q d n)
| ExpectedEq (Term q d n) | ExpectedEq (TyContext q d n) (Term q d n)
| BadUniverse Universe Universe | BadUniverse Universe Universe
| TagNotIn TagVal (SortedSet TagVal) | 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 -- first term arg of ClashT is the type
| ClashT EqMode (Term q d n) (Term q d n) (Term q d n) | ClashT (EqContext q n) EqMode (Term q 0 n) (Term q 0 n) (Term q 0 n)
| ClashTy EqMode (Term q d n) (Term q d n) | ClashTy (EqContext q n) EqMode (Term q 0 n) (Term q 0 n)
| ClashE EqMode (Elim q d n) (Elim q d n) | ClashE (EqContext q n) EqMode (Elim q 0 n) (Elim q 0 n)
| ClashU EqMode Universe Universe | ClashU EqMode Universe Universe
| ClashQ q q | ClashQ q q
| ClashD (Dim d) (Dim d)
| NotInScope Name | NotInScope Name
| NotType (Term q d n) | NotType (TyContext q d n) (Term q d n)
| WrongType (Term q d n) (Term 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 -- extra context
| WhileChecking | WhileChecking
@ -49,13 +48,13 @@ data Error q
(Elim q d n) (Elim q d n)
(Error q) (Error q)
| WhileComparingT | WhileComparingT
(TyContext q d n) EqMode (EqContext q n) EqMode
(Term q d n) -- type (Term q 0 n) -- type
(Term q d n) (Term q d n) -- lhs/rhs (Term q 0 n) (Term q 0 n) -- lhs/rhs
(Error q) (Error q)
| WhileComparingE | WhileComparingE
(TyContext q d n) EqMode (EqContext q n) EqMode
(Elim q d n) (Elim q d n) (Elim q 0 n) (Elim q 0 n)
(Error q) (Error q)
| WhnfError WhnfError | WhnfError WhnfError
@ -137,6 +136,3 @@ parameters {auto _ : HasErr q m}
expectModeU : EqMode -> Universe -> Universe -> m () expectModeU : EqMode -> Universe -> Universe -> m ()
expectModeU mode = expect (ClashU mode) $ ucmp mode expectModeU mode = expect (ClashU mode) $ ucmp mode
export %inline
expectEqualD : Dim d -> Dim d -> m ()
expectEqualD = expect ClashD (==)

122
tests/Tests/Equal.idr
View file

@ -46,6 +46,8 @@ parameters (ctx : TyContext Three 0 n)
subE = subED 0 ctx subE = subED 0 ctx
equalE = equalED 0 ctx equalE = equalED 0 ctx
empty01 : TyContext q 0 0
empty01 = {dctx := ZeroIsOne} empty
export export
@ -116,7 +118,7 @@ tests = "equality & subtyping" :- [
testEq "0=1 ⊢ A ⇾ B = A ⊸ B" $ testEq "0=1 ⊢ A ⇾ B = A ⊸ B" $
let tm1 = Arr Zero (FT "A") (FT "B") let tm1 = Arr Zero (FT "A") (FT "B")
tm2 = Arr One (FT "A") (FT "B") in 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", todo "dependent function types",
note "[todo] should π ≤ ρ ⊢ (ρ·A) → B <: (π·A) → B?" 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)" $ 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 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" $ testEq "∥ x : [(a ≡ a' : A) ∷ Type 0], y : [ditto] ⊢ x = y" $
let ty : forall n. Term Three 0 n := let ty : forall n. Term Three 0 n :=
E (Eq0 (FT "A") (FT "a") (FT "a'") :# TYPE 0) in 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" testEq "E ≔ a ≡ a' : A, EE ≔ E ∥ x : EE, y : EE ⊢ x = y"
{globals = defGlobals `mergeLeft` fromList {globals = defGlobals `mergeLeft` fromList
[("E", mkDef zero (TYPE 0) (Eq0 (FT "A") (FT "a") (FT "a'"))), [("E", mkDef zero (TYPE 0) (Eq0 (FT "A") (FT "a") (FT "a'"))),
("EE", mkDef zero (TYPE 0) (FT "E"))]} $ ("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" testEq "E ≔ a ≡ a' : A, EE ≔ E ∥ x : EE, y : E ⊢ x = y"
{globals = defGlobals `mergeLeft` fromList {globals = defGlobals `mergeLeft` fromList
[("E", mkDef zero (TYPE 0) (Eq0 (FT "A") (FT "a") (FT "a'"))), [("E", mkDef zero (TYPE 0) (Eq0 (FT "A") (FT "a") (FT "a'"))),
("EE", mkDef zero (TYPE 0) (FT "E"))]} $ ("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" testEq "E ≔ a ≡ a' : A ∥ x : E, y : E ⊢ x = y"
{globals = defGlobals `mergeLeft` fromList {globals = defGlobals `mergeLeft` fromList
[("E", mkDef zero (TYPE 0) (Eq0 (FT "A") (FT "a") (FT "a'")))]} $ [("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" testEq "E ≔ a ≡ a' : A ∥ x : (E×E), y : (E×E) ⊢ x = y"
{globals = defGlobals `mergeLeft` fromList {globals = defGlobals `mergeLeft` fromList
[("E", mkDef zero (TYPE 0) (Eq0 (FT "A") (FT "a") (FT "a'")))]} $ [("E", mkDef zero (TYPE 0) (Eq0 (FT "A") (FT "a") (FT "a'")))]} $
let ty : forall n. Term Three 0 n := let ty : forall n. Term Three 0 n :=
Sig (FT "E") $ S ["_"] $ N $ FT "E" in 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 {globals = defGlobals `mergeLeft` fromList
[("E", mkDef zero (TYPE 0) (Eq0 (FT "A") (FT "a") (FT "a'"))), [("E", mkDef zero (TYPE 0) (Eq0 (FT "A") (FT "a") (FT "a'"))),
("W", mkDef zero (TYPE 0) (FT "E" `And` FT "E"))]} $ ("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" :- [ "term closure" :- [
testEq "[#0]{} = [#0] : A" $ testEq "[#0]{} = [#0] : A" $
equalT (MkTyContext new [< FT "A"]) (FT "A") equalT (extendTy "x" (FT "A") empty)
(FT "A")
(CloT (BVT 0) id) (CloT (BVT 0) id)
(BVT 0), (BVT 0),
testEq "[#0]{a} = [a] : A" $ testEq "[#0]{a} = [a] : A" $
@ -249,9 +258,12 @@ tests = "equality & subtyping" :- [
"term d-closure" :- [ "term d-closure" :- [
testEq "★₀‹𝟎› = ★₀ : ★₁" $ 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)" $ testEq "(δ i ⇒ a)‹𝟎› = (δ i ⇒ a) : (a ≡ a : A)" $
equalTD 1 empty equalTD 1
(extendDim "𝑗" empty)
(Eq0 (FT "A") (FT "a") (FT "a")) (Eq0 (FT "A") (FT "a") (FT "a"))
(DCloT (["i"] :\\% FT "a") (K Zero ::: id)) (DCloT (["i"] :\\% FT "a") (K Zero ::: id))
(["i"] :\\% FT "a"), (["i"] :\\% FT "a"),
@ -271,7 +283,7 @@ tests = "equality & subtyping" :- [
testNeq "A ≠ B" $ testNeq "A ≠ B" $
equalE empty (F "A") (F "B"), equalE empty (F "A") (F "B"),
testEq "0=1 ⊢ A = 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} $ testEq "A : ★₁ ≔ ★₀ ⊢ A = (★₀ ∷ ★₁)" {globals = au_bu} $
equalE empty (F "A") (TYPE 0 :# TYPE 1), equalE empty (F "A") (TYPE 0 :# TYPE 1),
testEq "A : ★₁ ≔ ★₀ ⊢ [A] = ★₀" {globals = au_bu} $ testEq "A : ★₁ ≔ ★₀ ⊢ [A] = ★₀" {globals = au_bu} $
@ -294,20 +306,20 @@ tests = "equality & subtyping" :- [
("B", mkDef Any (TYPE 3) (TYPE 2))]} $ ("B", mkDef Any (TYPE 3) (TYPE 2))]} $
subE empty (F "A") (F "B"), subE empty (F "A") (F "B"),
testEq "0=1 ⊢ A <: B" $ testEq "0=1 ⊢ A <: B" $
subE (MkTyContext ZeroIsOne [<]) (F "A") (F "B") subE empty01 (F "A") (F "B")
], ],
"bound var" :- [ "bound var" :- [
testEq "#0 = #0" $ 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" $ 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" $ 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" $ 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" $ 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" :- [ "application" :- [
@ -343,26 +355,37 @@ tests = "equality & subtyping" :- [
testNeq "eq-AB @0 ≠ eq-AB @1" $ testNeq "eq-AB @0 ≠ eq-AB @1" $
equalE empty (F "eq-AB" :% K Zero) (F "eq-AB" :% K One), equalE empty (F "eq-AB" :% K Zero) (F "eq-AB" :% K One),
testEq "𝑖 | ⊢ eq-AB @𝑖 = eq-AB @𝑖" $ 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" $ 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" $ testEq "𝑖, 𝑖=0 | ⊢ eq-AB @𝑖 = eq-AB @0" $
let ctx = MkTyContext (set (BV 0) (K Zero) new) [<] in equalED 1
equalED 1 ctx (F "eq-AB" :% BV 0) (F "eq-AB" :% K Zero), (eqDim (BV 0) (K Zero) $ extendDim "𝑖" empty)
(F "eq-AB" :% BV 0) (F "eq-AB" :% K Zero),
testNeq "𝑖, 𝑖=1 | ⊢ eq-AB @𝑖 ≠ eq-AB @0" $ testNeq "𝑖, 𝑖=1 | ⊢ eq-AB @𝑖 ≠ eq-AB @0" $
let ctx = MkTyContext (set (BV 0) (K One) new) [<] in equalED 1
equalED 1 ctx (F "eq-AB" :% BV 0) (F "eq-AB" :% K Zero), (eqDim (BV 0) (K One) $ extendDim "𝑖" empty)
(F "eq-AB" :% BV 0) (F "eq-AB" :% K Zero),
testNeq "𝑖, 𝑗 | ⊢ eq-AB @𝑖 ≠ eq-AB @𝑗" $ 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 @𝑗" $ testEq "𝑖, 𝑗, 𝑖=𝑗 | ⊢ eq-AB @𝑖 = eq-AB @𝑗" $
let ctx = MkTyContext (set (BV 0) (BV 1) new) [<] in equalED 2
equalED 2 ctx (F "eq-AB" :% BV 1) (F "eq-AB" :% BV 0), (eqDim (BV 0) (BV 1) $ extendDim "𝑗" $ extendDim "𝑖" empty)
testNeq "𝑖, 𝑗, 𝑖=0, 𝑗=0 | ⊢ eq-AB @𝑖 ≠ eq-AB @𝑗" $ (F "eq-AB" :% BV 1) (F "eq-AB" :% BV 0),
let ctx : TyContext Three 2 0 := testEq "𝑖, 𝑗, 𝑖=0, 𝑗=0 | ⊢ eq-AB @𝑖 = eq-AB @𝑗" $
MkTyContext (C [< Just $ K Zero, Just $ K Zero]) [<] in equalED 2
equalED 2 empty (F "eq-AB" :% BV 1) (F "eq-AB" :% BV 0), (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 @𝑗" $ 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), (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 @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"), 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" $ testEq "#0{a} = a" $
equalE empty (CloE (BV 0) (F "a" ::: id)) (F "a"), equalE empty (CloE (BV 0) (F "a" ::: id)) (F "a"),
testEq "#1{a} = #0" $ testEq "#1{a} = #0" $
equalE (MkTyContext new [< FT "A"]) equalE (extendTy "x" (FT "A") empty)
(CloE (BV 1) (F "a" ::: id)) (BV 0) (CloE (BV 1) (F "a" ::: id)) (BV 0)
], ],
"elim d-closure" :- [ "elim d-closure" :- [
note "0·eq-AB : (A ≡ B : ★₀)", note "0·eq-AB : (A ≡ B : ★₀)",
testEq "(eq-AB #0)‹𝟎› = eq-AB 𝟎" $ testEq "(eq-AB #0)‹𝟎› = eq-AB 𝟎" $
equalED 1 empty equalED 1
(extendDim "𝑖" empty)
(DCloE (F "eq-AB" :% BV 0) (K Zero ::: id)) (DCloE (F "eq-AB" :% BV 0) (K Zero ::: id))
(F "eq-AB" :% K Zero), (F "eq-AB" :% K Zero),
testEq "(eq-AB #0)‹𝟎› = A" $ 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" $ 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" $ 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)" $ 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)) (DCloE (F "eq-AB" :% BV 0) (BV 0 ::: K Zero ::: id))
(F "eq-AB" :% BV 0), (F "eq-AB" :% BV 0),
testNeq "(eq-AB #0)‹𝟎› ≠ (eq-AB 𝟎)" $ 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)) (DCloE (F "eq-AB" :% BV 0) (BV 0 ::: K Zero ::: id))
(F "eq-AB" :% K Zero), (F "eq-AB" :% K Zero),
testEq "#0‹𝟎› = #0 # term and dim vars distinct" $ 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), (DCloE (BV 0) (K Zero ::: id)) (BV 0),
testEq "a‹𝟎› = a" $ 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]‹𝟎›" $ testEq "(f [a])‹𝟎› = f‹𝟎› [a]‹𝟎›" $
let th = K Zero ::: id in let th = K Zero ::: id in
equalED 1 empty equalED 1 (extendDim "𝑖" empty)
(DCloE (F "f" :@ FT "a") th) (DCloE (F "f" :@ FT "a") th)
(DCloE (F "f") th :@ DCloT (FT "a") th) (DCloE (F "f") th :@ DCloT (FT "a") th)
], ],
@ -433,8 +466,7 @@ tests = "equality & subtyping" :- [
testNeq "★₀ ≠ ★₀ ⇾ ★₀" $ testNeq "★₀ ≠ ★₀ ⇾ ★₀" $
equalT empty (TYPE 1) (TYPE 0) (Arr Zero (TYPE 0) (TYPE 0)), equalT empty (TYPE 1) (TYPE 0) (Arr Zero (TYPE 0) (TYPE 0)),
testEq "0=1 ⊢ ★₀ = ★₀ ⇾ ★₀" $ testEq "0=1 ⊢ ★₀ = ★₀ ⇾ ★₀" $
equalT (MkTyContext ZeroIsOne [<]) equalT empty01 (TYPE 1) (TYPE 0) (Arr Zero (TYPE 0) (TYPE 0)),
(TYPE 1) (TYPE 0) (Arr Zero (TYPE 0) (TYPE 0)),
todo "others" todo "others"
] ]
] ]

143
tests/Tests/Typechecker.idr
View file

@ -98,9 +98,12 @@ parameters (label : String) (act : Lazy (M ()))
testTCFail = testThrows label (const True) $ runReaderT globals act testTCFail = testThrows label (const True) $ runReaderT globals act
ctx, ctx01 : TContext Three 0 n -> TyContext Three 0 n ctx, ctx01 : Context (\n => (BaseName, Term Three 0 n)) n -> TyContext Three 0 n
ctx = MkTyContext new ctx tel = MkTyContext new [<] (map snd tel) (map fst tel)
ctx01 = MkTyContext ZeroIsOne 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 : TyContext Three d n -> (exp, got : Term Three d n) -> M ()
inferredTypeEq ctx exp got = inferredTypeEq ctx exp got =
@ -159,184 +162,184 @@ tests : Test
tests = "typechecker" :- [ tests = "typechecker" :- [
"universes" :- [ "universes" :- [
testTC "0 · ★₀ ⇐ ★₁ # by checkType" $ testTC "0 · ★₀ ⇐ ★₁ # by checkType" $
checkType_ (ctx [<]) (TYPE 0) (Just 1), checkType_ empty (TYPE 0) (Just 1),
testTC "0 · ★₀ ⇐ ★₁ # by check" $ testTC "0 · ★₀ ⇐ ★₁ # by check" $
check_ (ctx [<]) szero (TYPE 0) (TYPE 1), check_ empty szero (TYPE 0) (TYPE 1),
testTC "0 · ★₀ ⇐ ★₂" $ testTC "0 · ★₀ ⇐ ★₂" $
checkType_ (ctx [<]) (TYPE 0) (Just 2), checkType_ empty (TYPE 0) (Just 2),
testTC "0 · ★₀ ⇐ ★_" $ testTC "0 · ★₀ ⇐ ★_" $
checkType_ (ctx [<]) (TYPE 0) Nothing, checkType_ empty (TYPE 0) Nothing,
testTCFail "0 · ★₁ ⇍ ★₀" $ testTCFail "0 · ★₁ ⇍ ★₀" $
checkType_ (ctx [<]) (TYPE 1) (Just 0), checkType_ empty (TYPE 1) (Just 0),
testTCFail "0 · ★₀ ⇍ ★₀" $ testTCFail "0 · ★₀ ⇍ ★₀" $
checkType_ (ctx [<]) (TYPE 0) (Just 0), checkType_ empty (TYPE 0) (Just 0),
testTC "0=1 ⊢ 0 · ★₁ ⇐ ★₀" $ testTC "0=1 ⊢ 0 · ★₁ ⇐ ★₀" $
checkType_ (ctx01 [<]) (TYPE 1) (Just 0), checkType_ empty01 (TYPE 1) (Just 0),
testTCFail "1 · ★₀ ⇍ ★₁ # by check" $ testTCFail "1 · ★₀ ⇍ ★₁ # by check" $
check_ (ctx [<]) sone (TYPE 0) (TYPE 1) check_ empty sone (TYPE 0) (TYPE 1)
], ],
"function types" :- [ "function types" :- [
note "A, B : ★₀; C, D : ★₁; P : A ⇾ ★₀", note "A, B : ★₀; C, D : ★₁; P : A ⇾ ★₀",
testTC "0 · A ⊸ B ⇐ ★₀" $ 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", note "subtyping",
testTC "0 · A ⊸ B ⇐ ★₁" $ 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 ⇐ ★₁" $ 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 ⇍ ★₀" $ 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 ⇐ ★₀" $ testTC "0 · (1·x : A) → P x ⇐ ★₀" $
check_ (ctx [<]) szero check_ empty szero
(Pi_ One "x" (FT "A") $ E $ F "P" :@ BVT 0) (Pi_ One "x" (FT "A") $ E $ F "P" :@ BVT 0)
(TYPE 0), (TYPE 0),
testTCFail "0 · A ⊸ P ⇍ ★₀" $ 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 ⇐ ★₀" $ 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" :- [ "pair types" :- [
note #""A × B" for "(_ : A) × B""#, note #""A × B" for "(_ : A) × B""#,
testTC "0 · A × A ⇐ ★₀" $ 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 ⇍ ★₀" $ 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 ⇐ ★₀" $ testTC "0 · (x : A) × P x ⇐ ★₀" $
check_ (ctx [<]) szero check_ empty szero
(Sig_ "x" (FT "A") $ E $ F "P" :@ BVT 0) (TYPE 0), (Sig_ "x" (FT "A") $ E $ F "P" :@ BVT 0) (TYPE 0),
testTC "0 · (x : A) × P x ⇐ ★₁" $ testTC "0 · (x : A) × P x ⇐ ★₁" $
check_ (ctx [<]) szero check_ empty szero
(Sig_ "x" (FT "A") $ E $ F "P" :@ BVT 0) (TYPE 1), (Sig_ "x" (FT "A") $ E $ F "P" :@ BVT 0) (TYPE 1),
testTC "0 · (A : ★₀) × A ⇐ ★₁" $ 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 ⇍ ★₀" $ 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 ⇍ ★₀" $ 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" :- [ "enum types" :- [
testTC "0 · {} ⇐ ★₀" $ check_ (ctx [<]) szero (enum []) (TYPE 0), testTC "0 · {} ⇐ ★₀" $ check_ empty szero (enum []) (TYPE 0),
testTC "0 · {} ⇐ ★₃" $ check_ (ctx [<]) szero (enum []) (TYPE 3), testTC "0 · {} ⇐ ★₃" $ check_ empty szero (enum []) (TYPE 3),
testTC "0 · {a,b,c} ⇐ ★₀" $ 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} ⇐ ★₃" $ testTC "0 · {a,b,c} ⇐ ★₃" $
check_ (ctx [<]) szero (enum ["a", "b", "c"]) (TYPE 3), check_ empty szero (enum ["a", "b", "c"]) (TYPE 3),
testTCFail "1 · {} ⇍ ★₀" $ check_ (ctx [<]) sone (enum []) (TYPE 0), testTCFail "1 · {} ⇍ ★₀" $ check_ empty sone (enum []) (TYPE 0),
testTC "0=1 ⊢ 1 · {} ⇐ ★₀" $ check_ (ctx01 [<]) sone (enum []) (TYPE 0) testTC "0=1 ⊢ 1 · {} ⇐ ★₀" $ check_ empty01 sone (enum []) (TYPE 0)
], ],
"free vars" :- [ "free vars" :- [
note "A : ★₀", note "A : ★₀",
testTC "0 · A ⇒ ★₀" $ testTC "0 · A ⇒ ★₀" $
inferAs (ctx [<]) szero (F "A") (TYPE 0), inferAs empty szero (F "A") (TYPE 0),
testTC "0 · [A] ⇐ ★₀" $ testTC "0 · [A] ⇐ ★₀" $
check_ (ctx [<]) szero (FT "A") (TYPE 0), check_ empty szero (FT "A") (TYPE 0),
note "subtyping", note "subtyping",
testTC "0 · [A] ⇐ ★₁" $ testTC "0 · [A] ⇐ ★₁" $
check_ (ctx [<]) szero (FT "A") (TYPE 1), check_ empty szero (FT "A") (TYPE 1),
note "(fail) runtime-relevant type", note "(fail) runtime-relevant type",
testTCFail "1 · A ⇏ ★₀" $ 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)", 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 ⇒ ⋯" $ inferAs empty sone (F "refl") reflTy,
testTC "1 · [refl] ⇐ ⋯" $ check_ (ctx [<]) sone (FT "refl") reflTy testTC "1 · [refl] ⇐ ⋯" $ check_ empty sone (FT "refl") reflTy
], ],
"bound vars" :- [ "bound vars" :- [
testTC "x : A ⊢ 1 · x ⇒ A ⊳ 1·x" $ 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], (BV 0) (FT "A") [< one],
testTC "x : A ⊢ 1 · [x] ⇐ A ⊳ 1·x" $ 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", note "f2 : A ⊸ A ⊸ B",
testTC "x : A ⊢ 1 · f2 [x] [x] ⇒ B ⊳ ω·x" $ 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] (F "f2" :@@ [BVT 0, BVT 0]) (FT "B") [< Any]
], ],
"lambda" :- [ "lambda" :- [
note "linear & unrestricted identity", note "linear & unrestricted identity",
testTC "1 · (λ x ⇒ x) ⇐ A ⊸ A" $ 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" $ 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", note "(fail) zero binding used relevantly",
testTCFail "1 · (λ x ⇒ x) ⇍ A ⇾ A" $ 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)", note "(but ok in overall erased context)",
testTC "0 · (λ x ⇒ x) ⇐ A ⇾ A" $ 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)" $ 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])) (["A", "x"] :\\ E (F "refl" :@@ [BVT 1, BVT 0]))
reflTy, reflTy,
testTC "1 · (λ A x ⇒ δ i ⇒ x) ⇐ ⋯ # (def. and type of refl)" $ testTC "1 · (λ A x ⇒ δ i ⇒ x) ⇐ ⋯ # (def. and type of refl)" $
check_ (ctx [<]) sone reflDef reflTy check_ empty sone reflDef reflTy
], ],
"pairs" :- [ "pairs" :- [
testTC "1 · (a, a) ⇐ A × A" $ 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" $ 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], (Pair (BVT 0) (BVT 0)) (FT "A" `And` FT "A") [< Any],
testTC "1 · (a, δ i ⇒ a) ⇐ (x : A) × (x ≡ a)" $ testTC "1 · (a, δ i ⇒ a) ⇐ (x : A) × (x ≡ a)" $
check_ (ctx [<]) sone check_ empty sone
(Pair (FT "a") (["i"] :\\% FT "a")) (Pair (FT "a") (["i"] :\\% FT "a"))
(Sig_ "x" (FT "A") $ Eq0 (FT "A") (BVT 0) (FT "a")) (Sig_ "x" (FT "A") $ Eq0 (FT "A") (BVT 0) (FT "a"))
], ],
"unpairing" :- [ "unpairing" :- [
testTC "x : A × A ⊢ 1 · (case1 x return B of (l,r) ⇒ f2 l r) ⇒ B ⊳ 1·x" $ 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") (CasePair One (BV 0) (SN $ FT "B")
(SY ["l", "r"] $ E $ F "f2" :@@ [BVT 1, BVT 0])) (SY ["l", "r"] $ E $ F "f2" :@@ [BVT 1, BVT 0]))
(FT "B") [< One], (FT "B") [< One],
testTC "x : A × A ⊢ 1 · (caseω x return B of (l,r) ⇒ f2 l r) ⇒ B ⊳ ω·x" $ 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") (CasePair Any (BV 0) (SN $ FT "B")
(SY ["l", "r"] $ E $ F "f2" :@@ [BVT 1, BVT 0])) (SY ["l", "r"] $ E $ F "f2" :@@ [BVT 1, BVT 0]))
(FT "B") [< Any], (FT "B") [< Any],
testTC "x : A × A ⊢ 0 · (caseω x return B of (l,r) ⇒ f2 l r) ⇒ B ⊳ 0·x" $ 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") (CasePair Any (BV 0) (SN $ FT "B")
(SY ["l", "r"] $ E $ F "f2" :@@ [BVT 1, BVT 0])) (SY ["l", "r"] $ E $ F "f2" :@@ [BVT 1, BVT 0]))
(FT "B") [< Zero], (FT "B") [< Zero],
testTCFail "x : A × A ⊢ 1 · (case0 x return B of (l,r) ⇒ f2 l r) ⇏" $ 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") (CasePair Zero (BV 0) (SN $ FT "B")
(SY ["l", "r"] $ E $ F "f2" :@@ [BVT 1, BVT 0])), (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" $ 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") (CasePair Any (BV 0) (SN $ FT "A")
(SY ["l", "r"] $ BVT 1)) (SY ["l", "r"] $ BVT 1))
(FT "A") [< Any], (FT "A") [< Any],
testTC "x : A × B ⊢ 0 · (case1 x return A of (l,r) ⇒ l) ⇒ A ⊳ 0·x" $ 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") (CasePair One (BV 0) (SN $ FT "A")
(SY ["l", "r"] $ BVT 1)) (SY ["l", "r"] $ BVT 1))
(FT "A") [< Zero], (FT "A") [< Zero],
testTCFail "x : A × B ⊢ 1 · (case1 x return A of (l,r) ⇒ l) ⇏" $ 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") (CasePair One (BV 0) (SN $ FT "A")
(SY ["l", "r"] $ BVT 1)), (SY ["l", "r"] $ BVT 1)),
note "fst : (0·A : ★₁) → (0·B : A ↠ ★₁) → ((x : A) × B x) ↠ A", note "fst : (0·A : ★₁) → (0·B : A ↠ ★₁) → ((x : A) × B x) ↠ A",
note " ≔ (λ A B p ⇒ caseω p return A of (x, y) ⇒ x)", note " ≔ (λ A B p ⇒ caseω p return A of (x, y) ⇒ x)",
testTC "0 · ‹type of fst› ⇐ ★₂" $ 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›" $ 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 "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)", note " ≔ (λ A B p ⇒ caseω p return p ⇒ B (fst A B p) of (x, y) ⇒ y)",
testTC "0 · ‹type of snd› ⇐ ★₂" $ 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›" $ 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" $ 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]) (F "snd" :@@ [TYPE 0, ["x"] :\\ BVT 0])
(Pi_ Any "A" (Sig_ "A" (TYPE 0) $ BVT 0) $ (Pi_ Any "A" (Sig_ "A" (TYPE 0) $ BVT 0) $
(E $ F "fst" :@@ [TYPE 0, ["x"] :\\ BVT 0, BVT 0])) (E $ F "fst" :@@ [TYPE 0, ["x"] :\\ BVT 0, BVT 0]))
@ -344,27 +347,27 @@ tests = "typechecker" :- [
"enums" :- [ "enums" :- [
testTC "1 · 'a ⇐ {a}" $ testTC "1 · 'a ⇐ {a}" $
check_ (ctx [<]) sone (Tag "a") (enum ["a"]), check_ empty sone (Tag "a") (enum ["a"]),
testTC "1 · 'a ⇐ {a, b, c}" $ 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}" $ 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}" $ testTC "0=1 ⊢ 1 · 'a ⇐ {b, c}" $
check_ (ctx01 [<]) sone (Tag "a") (enum ["b", "c"]) check_ empty01 sone (Tag "a") (enum ["b", "c"])
], ],
"equalities" :- [ "equalities" :- [
testTC "1 · (δ i ⇒ a) ⇐ a ≡ a" $ 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")), (Eq0 (FT "A") (FT "a") (FT "a")),
testTC "0 · (λ p q ⇒ δ i ⇒ p) ⇐ (ω·p q : a ≡ a') → p ≡ q" $ testTC "0 · (λ p q ⇒ δ i ⇒ p) ⇐ (ω·p q : a ≡ a') → p ≡ q" $
check_ (ctx [<]) szero check_ empty szero
(["p","q"] :\\ ["i"] :\\% BVT 1) (["p","q"] :\\ ["i"] :\\% BVT 1)
(Pi_ Any "p" (Eq0 (FT "A") (FT "a") (FT "a")) $ (Pi_ Any "p" (Eq0 (FT "A") (FT "a") (FT "a")) $
Pi_ Any "q" (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)), Eq0 (Eq0 (FT "A") (FT "a") (FT "a")) (BVT 1) (BVT 0)),
testTC "0 · (λ p q ⇒ δ i ⇒ q) ⇐ (ω·p q : a ≡ a') → p ≡ q" $ testTC "0 · (λ p q ⇒ δ i ⇒ q) ⇐ (ω·p q : a ≡ a') → p ≡ q" $
check_ (ctx [<]) szero check_ empty szero
(["p","q"] :\\ ["i"] :\\% BVT 0) (["p","q"] :\\ ["i"] :\\% BVT 0)
(Pi_ Any "p" (Eq0 (FT "A") (FT "a") (FT "a")) $ (Pi_ Any "p" (Eq0 (FT "A") (FT "a") (FT "a")) $
Pi_ Any "q" (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 "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)", note " ⇐ (0·x y : A) → (1·xy : x ≡ y) → Eq [i ⇒ P (xy i)] (p x) (p y)",
testTC "cong" $ testTC "cong" $
check_ (ctx [<]) sone check_ empty sone
(["x", "y", "xy"] :\\ ["i"] :\\% E (F "p" :@ E (BV 0 :% BV 0))) (["x", "y", "xy"] :\\ ["i"] :\\% E (F "p" :@ E (BV 0 :% BV 0)))
(Pi_ Zero "x" (FT "A") $ (Pi_ Zero "x" (FT "A") $
Pi_ Zero "y" (FT "A") $ Pi_ Zero "y" (FT "A") $
@ -390,7 +393,7 @@ tests = "typechecker" :- [
note "1 · λ eq ⇒ δ i ⇒ λ x ⇒ eq x i", note "1 · λ eq ⇒ δ i ⇒ λ x ⇒ eq x i",
note " ⇐ (1·eq : (1·x : A) → p x ≡ q x) → p ≡ q", note " ⇐ (1·eq : (1·x : A) → p x ≡ q x) → p ≡ q",
testTC "funext" $ testTC "funext" $
check_ (ctx [<]) sone check_ empty sone
(["eq"] :\\ ["i"] :\\% ["x"] :\\ E (BV 1 :@ BVT 0 :% BV 0)) (["eq"] :\\ ["i"] :\\% ["x"] :\\ E (BV 1 :@ BVT 0 :% BV 0))
(Pi_ One "eq" (Pi_ One "eq"
(Pi_ One "x" (FT "A") (Pi_ One "x" (FT "A")

32
tests/TypingImpls.idr
View file

@ -17,6 +17,10 @@ export %hint
showTyContext : (PrettyHL q, Show q) => Show (TyContext q d n) showTyContext : (PrettyHL q, Show q) => Show (TyContext q d n)
showTyContext = deriveShow showTyContext = deriveShow
export %hint
showEqContext : (PrettyHL q, Show q) => Show (EqContext q n)
showEqContext = deriveShow
export %hint export %hint
showTypingError : (PrettyHL q, Show q) => Show (Error q) showTypingError : (PrettyHL q, Show q) => Show (Error q)
showTypingError = deriveShow showTypingError = deriveShow
@ -33,19 +37,19 @@ PrettyHL q => ToInfo (Error q) where
toInfo (NotInScope x) = toInfo (NotInScope x) =
[("type", "NotInScope"), [("type", "NotInScope"),
("name", show x)] ("name", show x)]
toInfo (ExpectedTYPE t) = toInfo (ExpectedTYPE _ t) =
[("type", "ExpectedTYPE"), [("type", "ExpectedTYPE"),
("got", prettyStr True t)] ("got", prettyStr True t)]
toInfo (ExpectedPi t) = toInfo (ExpectedPi _ t) =
[("type", "ExpectedPi"), [("type", "ExpectedPi"),
("got", prettyStr True t)] ("got", prettyStr True t)]
toInfo (ExpectedSig t) = toInfo (ExpectedSig _ t) =
[("type", "ExpectedSig"), [("type", "ExpectedSig"),
("got", prettyStr True t)] ("got", prettyStr True t)]
toInfo (ExpectedEnum t) = toInfo (ExpectedEnum _ t) =
[("type", "ExpectedEnum"), [("type", "ExpectedEnum"),
("got", prettyStr True t)] ("got", prettyStr True t)]
toInfo (ExpectedEq t) = toInfo (ExpectedEq _ t) =
[("type", "ExpectedEq"), [("type", "ExpectedEq"),
("got", prettyStr True t)] ("got", prettyStr True t)]
toInfo (BadUniverse k l) = toInfo (BadUniverse k l) =
@ -56,22 +60,22 @@ PrettyHL q => ToInfo (Error q) where
[("type", "TagNotIn"), [("type", "TagNotIn"),
("tag", show t), ("tag", show t),
("set", show $ SortedSet.toList ts)] ("set", show $ SortedSet.toList ts)]
toInfo (BadCaseQtys qouts) = toInfo (BadCaseQtys _ qouts) =
("type", "BadCaseQtys") :: ("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"), [("type", "ClashT"),
("mode", show mode), ("mode", show mode),
("ty", prettyStr True ty), ("ty", prettyStr True ty),
("left", prettyStr True s), ("left", prettyStr True s),
("right", prettyStr True t)] ("right", prettyStr True t)]
toInfo (ClashTy mode s t) = toInfo (ClashTy _ mode s t) =
[("type", "ClashTy"), [("type", "ClashTy"),
("mode", show mode), ("mode", show mode),
("left", prettyStr True s), ("left", prettyStr True s),
("right", prettyStr True t)] ("right", prettyStr True t)]
toInfo (ClashE mode e f) = toInfo (ClashE _ mode e f) =
[("type", "ClashE"), [("type", "ClashE"),
("mode", show mode), ("mode", show mode),
("left", prettyStr True e), ("left", prettyStr True e),
@ -85,14 +89,10 @@ PrettyHL q => ToInfo (Error q) where
[("type", "ClashQ"), [("type", "ClashQ"),
("left", prettyStr True pi), ("left", prettyStr True pi),
("right", prettyStr True rh)] ("right", prettyStr True rh)]
toInfo (ClashD p q) = toInfo (NotType _ ty) =
[("type", "ClashD"),
("left", prettyStr True p),
("right", prettyStr True q)]
toInfo (NotType ty) =
[("type", "NotType"), [("type", "NotType"),
("got", prettyStr True ty)] ("got", prettyStr True ty)]
toInfo (WrongType ty s t) = toInfo (WrongType _ ty s t) =
[("type", "WrongType"), [("type", "WrongType"),
("ty", prettyStr True ty), ("ty", prettyStr True ty),
("left", prettyStr True s), ("left", prettyStr True s),