more equality & tests
This commit is contained in:
parent
3b9da2a1e5
commit
a6f43a772e
7 changed files with 361 additions and 207 deletions
|
|
@ -120,11 +120,11 @@ NonRedexTerm q d n defs = Subset (Term q d n) (NotRedex defs)
|
|||
|
||||
parameters {0 isGlobal : _} (defs : Definitions' q isGlobal)
|
||||
namespace Term
|
||||
export %inline
|
||||
export covering %inline
|
||||
whnfD : Term q d n -> NonRedexTerm q d n defs
|
||||
whnfD = whnf $ \x => lookupElim x defs
|
||||
|
||||
namespace Elim
|
||||
export %inline
|
||||
export covering %inline
|
||||
whnfD : Elim q d n -> NonRedexElim q d n defs
|
||||
whnfD = whnf $ \x => lookupElim x defs
|
||||
|
|
|
|||
|
|
@ -55,36 +55,52 @@ isTyCon (E {}) = True
|
|||
isTyCon (CloT {}) = False
|
||||
isTyCon (DCloT {}) = False
|
||||
|
||||
private
|
||||
isSubSing : Term {} -> Bool
|
||||
isSubSing ty =
|
||||
let Element ty _ = pushSubsts ty in
|
||||
case ty of
|
||||
TYPE _ => False
|
||||
Pi {res, _} => isSubSing res.term
|
||||
Lam {} => False
|
||||
Sig {fst, snd, _} => isSubSing fst && isSubSing snd.term
|
||||
Pair {} => False
|
||||
Eq {} => True
|
||||
DLam {} => False
|
||||
E e => False
|
||||
public export %inline
|
||||
sameTyCon : (s, t : Term q d n) ->
|
||||
(0 ts : So (isTyCon s)) => (0 tt : So (isTyCon t)) =>
|
||||
Bool
|
||||
sameTyCon (TYPE {}) (TYPE {}) = True
|
||||
sameTyCon (TYPE {}) _ = False
|
||||
sameTyCon (Pi {}) (Pi {}) = True
|
||||
sameTyCon (Pi {}) _ = False
|
||||
sameTyCon (Sig {}) (Sig {}) = True
|
||||
sameTyCon (Sig {}) _ = False
|
||||
sameTyCon (Eq {}) (Eq {}) = True
|
||||
sameTyCon (Eq {}) _ = False
|
||||
sameTyCon (E {}) (E {}) = True
|
||||
sameTyCon (E {}) _ = False
|
||||
|
||||
|
||||
parameters (defs : Definitions' q g)
|
||||
private
|
||||
isSubSing : Term q 0 n -> Bool
|
||||
isSubSing ty =
|
||||
let Element ty nc = whnfD defs ty in
|
||||
case ty of
|
||||
TYPE _ => False
|
||||
Pi {res, _} => isSubSing res.term
|
||||
Lam {} => False
|
||||
Sig {fst, snd, _} => isSubSing fst && isSubSing snd.term
|
||||
Pair {} => False
|
||||
Eq {} => True
|
||||
DLam {} => False
|
||||
E (s :# _) => isSubSing s
|
||||
E _ => 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 n => throwError $ e t
|
||||
Left y => pure y
|
||||
Right _ => throwError $ e t
|
||||
|
||||
export %inline
|
||||
ensureType : (t : Term q d n) -> m (So (isTyCon t))
|
||||
ensureType = ensure NotType isTyCon
|
||||
ensureTyCon : HasErr q m => (t : Term q d n) -> m (So (isTyCon t))
|
||||
ensureTyCon = ensure NotType isTyCon
|
||||
|
||||
parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)}
|
||||
mutual
|
||||
-- [todo] remove cumulativity & subtyping, it's too much of a pain
|
||||
-- mugen might be good
|
||||
namespace Term
|
||||
export covering %inline
|
||||
compare0 : TContext q 0 n -> (ty, s, t : Term q 0 n) -> m ()
|
||||
|
|
@ -92,7 +108,7 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)}
|
|||
let Element ty nty = whnfD defs ty
|
||||
Element s ns = whnfD defs s
|
||||
Element t nt = whnfD defs t
|
||||
tty <- ensureType ty
|
||||
tty <- ensureTyCon ty
|
||||
compare0' ctx ty s t
|
||||
|
||||
private %inline
|
||||
|
|
@ -107,9 +123,9 @@ 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 = local {mode := Equal} $
|
||||
compare0' ctx ty@(Pi {arg, res, _}) s t {n} = local {mode := Equal} $
|
||||
let ctx' = ctx :< arg
|
||||
eta : Elim q 0 ? -> ScopeTerm q 0 ? -> m ()
|
||||
eta : Elim q 0 n -> ScopeTerm q 0 n -> m ()
|
||||
eta e (TUsed b) = compare0 ctx' res.term (toLamBody e) b
|
||||
eta e (TUnused _) = clashT ty s t
|
||||
in
|
||||
|
|
@ -117,7 +133,7 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)}
|
|||
(Lam _ b1, Lam _ b2) => compare0 ctx' res.term b1.term b2.term
|
||||
(E e, Lam _ b) => eta e b
|
||||
(Lam _ b, E e) => eta e b
|
||||
(E e, E f) => compare0 ctx e f
|
||||
(E e, E f) => Elim.compare0 ctx e f
|
||||
_ => throwError $ WrongType ty s t
|
||||
|
||||
compare0' ctx ty@(Sig {fst, snd, _}) s t = local {mode := Equal} $
|
||||
|
|
@ -137,75 +153,72 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)}
|
|||
-- e.g. an abstract value in an abstract type, bound variables, …
|
||||
E e <- pure s | _ => throwError $ WrongType ty s t
|
||||
E f <- pure t | _ => throwError $ WrongType ty s t
|
||||
compare0 ctx e f
|
||||
Elim.compare0 ctx e f
|
||||
|
||||
export covering
|
||||
compareType : TContext q 0 n -> (s, t : Term q 0 n) -> m ()
|
||||
compareType ctx s t = do
|
||||
let Element s ns = whnfD defs s
|
||||
Element t nt = whnfD defs t
|
||||
sok <- ensureType s
|
||||
tok <- ensureType t
|
||||
ts <- ensureTyCon s
|
||||
tt <- ensureTyCon t
|
||||
st <- either pure (const $ clashT (TYPE UAny) s t) $
|
||||
nchoose $ sameTyCon s t
|
||||
compareType' ctx s t
|
||||
|
||||
private covering
|
||||
compareType' : TContext q 0 n -> (s, t : Term q 0 n) ->
|
||||
(0 ns : NotRedex defs s) => (0 ts : So (isTyCon s)) =>
|
||||
(0 nt : NotRedex defs t) => (0 tt : So (isTyCon t)) =>
|
||||
(0 st : So (sameTyCon s t)) =>
|
||||
m ()
|
||||
compareType' ctx s t = do
|
||||
let err : m () = clashT (TYPE UAny) s t
|
||||
case s of
|
||||
TYPE k => do
|
||||
TYPE l <- pure t | _ => err
|
||||
expectModeU !mode k l
|
||||
compareType' ctx (TYPE k) (TYPE l) =
|
||||
expectModeU !mode k l
|
||||
|
||||
Pi {qty = sQty, arg = sArg, res = sRes, _} => do
|
||||
Pi {qty = tQty, arg = tArg, res = tRes, _} <- pure t | _ => err
|
||||
expectEqualQ sQty tQty
|
||||
compareType ctx tArg sArg -- contra
|
||||
-- [todo] is using sArg also ok for subtyping?
|
||||
compareType (ctx :< sArg) sRes.term tRes.term
|
||||
compareType' ctx (Pi {qty = sQty, arg = sArg, res = sRes, _})
|
||||
(Pi {qty = tQty, arg = tArg, res = tRes, _}) = do
|
||||
expectEqualQ sQty tQty
|
||||
local {mode $= flip} $ compareType ctx sArg tArg -- contra
|
||||
compareType (ctx :< sArg) sRes.term tRes.term
|
||||
|
||||
Sig {fst = sFst, snd = sSnd, _} => do
|
||||
Sig {fst = tFst, snd = tSnd, _} <- pure t | _ => err
|
||||
compareType ctx sFst tFst
|
||||
compareType (ctx :< sFst) sSnd.term tSnd.term
|
||||
compareType' ctx (Sig {fst = sFst, snd = sSnd, _})
|
||||
(Sig {fst = tFst, snd = tSnd, _}) = do
|
||||
compareType ctx sFst tFst
|
||||
compareType (ctx :< sFst) sSnd.term tSnd.term
|
||||
|
||||
Eq {ty = sTy, l = sl, r = sr, _} => do
|
||||
Eq {ty = tTy, l = tl, r = tr, _} <- pure t | _ => err
|
||||
compareType ctx sTy.zero tTy.zero
|
||||
compareType ctx sTy.one tTy.one
|
||||
local {mode := Equal} $ do
|
||||
compare0 ctx sTy.zero sl tl
|
||||
compare0 ctx sTy.one sr tr
|
||||
compareType' ctx (Eq {ty = sTy, l = sl, r = sr, _})
|
||||
(Eq {ty = tTy, l = tl, r = tr, _}) = do
|
||||
compareType ctx sTy.zero tTy.zero
|
||||
compareType ctx sTy.one tTy.one
|
||||
local {mode := Equal} $ do
|
||||
Term.compare0 ctx sTy.zero sl tl
|
||||
Term.compare0 ctx sTy.one sr tr
|
||||
|
||||
E e => do
|
||||
E f <- pure t | _ => err
|
||||
-- no fanciness needed here cos anything other than a neutral
|
||||
-- has been inlined by whnfD
|
||||
compare0 ctx e f
|
||||
compareType' ctx (E e) (E f) = do
|
||||
-- no fanciness needed here cos anything other than a neutral
|
||||
-- has been inlined by whnfD
|
||||
Elim.compare0 ctx e f
|
||||
|
||||
||| assumes the elim is already typechecked! only does the work necessary
|
||||
||| to calculate the overall type
|
||||
private covering
|
||||
computeElimType : TContext q 0 n -> (e : Elim q 0 n) ->
|
||||
(0 ne : NotRedex defs e) =>
|
||||
(0 ne : NotRedex defs e) ->
|
||||
m (Term q 0 n)
|
||||
computeElimType ctx (F x) = do
|
||||
computeElimType ctx (F x) _ = do
|
||||
defs <- lookupFree' defs x
|
||||
pure $ defs.type.get
|
||||
computeElimType ctx (B i) = do
|
||||
computeElimType ctx (B i) _ = do
|
||||
pure $ ctx !! i
|
||||
computeElimType ctx (f :@ s) {ne} = do
|
||||
(_, arg, res) <- computeElimType ctx f {ne = noOr1 ne} >>= expectPi defs
|
||||
computeElimType ctx (f :@ s) ne = do
|
||||
(_, arg, res) <- expectPi defs !(computeElimType ctx f (noOr1 ne))
|
||||
pure $ sub1 res (s :# arg)
|
||||
computeElimType ctx (CasePair {pair, ret, _}) = do
|
||||
computeElimType ctx (CasePair {pair, ret, _}) _ = do
|
||||
pure $ sub1 ret pair
|
||||
computeElimType ctx (f :% p) {ne} = do
|
||||
(ty, _, _) <- computeElimType ctx f {ne = noOr1 ne} >>= expectEq defs
|
||||
computeElimType ctx (f :% p) ne = do
|
||||
(ty, _, _) <- expectEq defs !(computeElimType ctx f (noOr1 ne))
|
||||
pure $ dsub1 ty p
|
||||
computeElimType ctx (_ :# ty) = do
|
||||
computeElimType ctx (_ :# ty) _ = do
|
||||
pure ty
|
||||
|
||||
private covering
|
||||
|
|
@ -213,13 +226,12 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)}
|
|||
(e : Elim q 0 n) -> DimConst -> (0 ne : NotRedex defs e) ->
|
||||
m (Elim q 0 n)
|
||||
replaceEnd ctx e p ne = do
|
||||
(ty, l, r) <- computeElimType ctx e >>= expectEq defs
|
||||
(ty, l, r) <- expectEq defs !(computeElimType ctx e ne)
|
||||
pure $ ends l r p :# dsub1 ty (K p)
|
||||
|
||||
namespace Elim
|
||||
-- [fixme] the following code ends up repeating a lot of work in the
|
||||
-- computeElimType calls. the results should be shared better
|
||||
|
||||
export covering %inline
|
||||
compare0 : TContext q 0 n -> (e, f : Elim q 0 n) -> m ()
|
||||
compare0 ctx e f =
|
||||
|
|
@ -227,48 +239,50 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)}
|
|||
Element f nf = whnfD defs f
|
||||
in
|
||||
-- [fixme] there is a better way to do this "isSubSing" stuff for sure
|
||||
unless (isSubSing !(computeElimType ctx e)) $ compare0' ctx e f
|
||||
unless (isSubSing defs !(computeElimType ctx e ne)) $
|
||||
compare0' ctx e f ne nf
|
||||
|
||||
private covering
|
||||
compare0' : TContext 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 ()
|
||||
-- replace applied equalities with the appropriate end first
|
||||
-- e.g. e : Eq [i ⇒ A] s t ⊢ e 0 = s : A‹0/i›
|
||||
compare0' ctx (e :% K p) f {ne} =
|
||||
-- e.g. e : Eq [i ⇒ A] s t ⊢ e 𝟎 = s : A‹𝟎/i›
|
||||
compare0' ctx (e :% K p) f ne nf =
|
||||
compare0 ctx !(replaceEnd ctx e p $ noOr1 ne) f
|
||||
compare0' ctx e (f :% K q) {nf} =
|
||||
compare0' ctx e (f :% K q) ne nf =
|
||||
compare0 ctx e !(replaceEnd ctx f q $ noOr1 nf)
|
||||
|
||||
compare0' _ e@(F x) f@(F y) = unless (x == y) $ clashE e f
|
||||
compare0' _ e@(F _) f = clashE e f
|
||||
compare0' _ e@(F x) f@(F y) _ _ = unless (x == y) $ clashE e f
|
||||
compare0' _ e@(F _) f _ _ = clashE e f
|
||||
|
||||
compare0' ctx e@(B i) f@(B j) = unless (i == j) $ clashE e f
|
||||
compare0' _ e@(B _) f = clashE e f
|
||||
compare0' ctx e@(B i) f@(B j) _ _ = unless (i == j) $ clashE e f
|
||||
compare0' _ e@(B _) f _ _ = clashE e f
|
||||
|
||||
compare0' ctx (e :@ s) (f :@ t) {ne} = local {mode := Equal} $ do
|
||||
compare0 ctx e f
|
||||
(_, arg, _) <- computeElimType ctx e {ne = noOr1 ne} >>= expectPi defs
|
||||
compare0 ctx arg s t
|
||||
compare0' _ e@(_ :@ _) f = clashE e f
|
||||
|
||||
compare0' ctx (CasePair epi e _ eret _ _ ebody)
|
||||
(CasePair fpi f _ fret _ _ fbody) {ne} =
|
||||
compare0' ctx (e :@ s) (f :@ t) ne nf =
|
||||
local {mode := Equal} $ do
|
||||
compare0 ctx e f
|
||||
ety <- computeElimType ctx e {ne = noOr1 ne}
|
||||
(_, arg, _) <- expectPi defs !(computeElimType ctx e (noOr1 ne))
|
||||
Term.compare0 ctx arg s t
|
||||
compare0' _ e@(_ :@ _) f _ _ = clashE e f
|
||||
|
||||
compare0' ctx (CasePair epi e _ eret _ _ ebody)
|
||||
(CasePair fpi f _ fret _ _ fbody) ne nf =
|
||||
local {mode := Equal} $ do
|
||||
compare0 ctx e f
|
||||
ety <- computeElimType ctx e (noOr1 ne)
|
||||
compareType (ctx :< ety) eret.term fret.term
|
||||
(fst, snd) <- expectSig defs ety
|
||||
compare0 (ctx :< fst :< snd.term) (substCasePairRet ety eret)
|
||||
Term.compare0 (ctx :< fst :< snd.term) (substCasePairRet ety eret)
|
||||
ebody.term fbody.term
|
||||
unless (epi == fpi) $ throwError $ ClashQ epi fpi
|
||||
compare0' _ e@(CasePair {}) f = clashE e f
|
||||
compare0' _ e@(CasePair {}) f _ _ = clashE e f
|
||||
|
||||
compare0' ctx (s :# a) (t :# b) = do
|
||||
compareType ctx a b
|
||||
compare0 ctx a s t
|
||||
compare0' _ e@(_ :# _) f = clashE e f
|
||||
compare0' ctx (s :# a) (t :# _) _ _ = Term.compare0 ctx a s t
|
||||
compare0' ctx (s :# a) f _ _ = Term.compare0 ctx a s (E f)
|
||||
compare0' ctx e (t :# b) _ _ = Term.compare0 ctx b (E e) t
|
||||
compare0' _ e@(_ :# _) f _ _ = clashE e f
|
||||
|
||||
|
||||
parameters {auto _ : (HasDefs' q _ m, HasErr q m, Eq q)}
|
||||
|
|
|
|||
|
|
@ -90,7 +90,7 @@ mutual
|
|||
||| `CasePair 𝜋 𝑒 𝑟 𝐴 𝑥 𝑦 𝑡` is
|
||||
||| `𝐜𝐚𝐬𝐞 𝜋 · 𝑒 𝐫𝐞𝐭𝐮𝐫𝐧 𝑟 ⇒ 𝐴 𝐨𝐟 { (𝑥, 𝑦) ⇒ 𝑡 }`
|
||||
CasePair : (qty : q) -> (pair : Elim q d n) ->
|
||||
(r : Name) -> (ret : ScopeTerm q d n) ->
|
||||
(r : Name) -> (ret : ScopeTerm q d n) ->
|
||||
(x, y : Name) -> (body : ScopeTermN 2 q d n) ->
|
||||
Elim q d n
|
||||
|
||||
|
|
@ -146,6 +146,11 @@ public export %inline
|
|||
Eq0 : (ty, l, r : Term q d n) -> Term q d n
|
||||
Eq0 {ty, l, r} = Eq {i = "_", ty = DUnused ty, l, r}
|
||||
|
||||
||| non dependent pair type
|
||||
public export %inline
|
||||
And : (fst, snd : Term q d n) -> Term q d n
|
||||
And {fst, snd} = Sig {x = "_", fst, snd = TUnused snd}
|
||||
|
||||
||| same as `F` but as a term
|
||||
public export %inline
|
||||
FT : Name -> Term q d n
|
||||
|
|
|
|||
|
|
@ -109,7 +109,7 @@ record InferResult q d n where
|
|||
|
||||
|
||||
public export
|
||||
data EqMode = Equal | Sub
|
||||
data EqMode = Equal | Sub | Super
|
||||
%runElab derive "EqMode" [Generic, Meta, Eq, Ord, DecEq, Show]
|
||||
|
||||
|
||||
|
|
@ -138,8 +138,15 @@ HasErr q = MonadError (Error q)
|
|||
|
||||
export %inline
|
||||
ucmp : EqMode -> Universe -> Universe -> Bool
|
||||
ucmp Sub = (<=)
|
||||
ucmp Equal = (==)
|
||||
ucmp Sub = (<=)
|
||||
ucmp Super = (>=)
|
||||
|
||||
export %inline
|
||||
flip : EqMode -> EqMode
|
||||
flip Equal = Equal
|
||||
flip Sub = Super
|
||||
flip Super = Sub
|
||||
|
||||
|
||||
parameters {auto _ : HasErr q m}
|
||||
|
|
@ -172,7 +179,7 @@ lookupFree' defs x =
|
|||
Nothing => throwError $ NotInScope x
|
||||
|
||||
|
||||
export
|
||||
public export
|
||||
substCasePairRet : Term q d n -> ScopeTerm q d n -> Term q d (2 + n)
|
||||
substCasePairRet dty retty =
|
||||
let arg = Pair (BVT 0) (BVT 1) :# (dty // fromNat 2) in
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue