quox/lib/Quox/Equal.idr

296 lines
9.6 KiB
Idris
Raw Normal View History

2022-02-26 20:18:16 -05:00
module Quox.Equal
import public Quox.Syntax
2022-08-22 04:17:08 -04:00
import public Quox.Definition
import public Quox.Typing
import public Control.Monad.Either
import public Control.Monad.Reader
import Data.Maybe
2022-02-26 20:18:16 -05:00
private %inline
2023-02-10 15:40:44 -05:00
ClashE : EqMode -> Term q d n -> Elim q d n -> Elim q d n -> Error q
ClashE mode ty = ClashT mode ty `on` E
2022-02-26 20:18:16 -05:00
2023-01-08 08:59:25 -05:00
2022-02-26 20:18:16 -05:00
public export
record Env where
2023-01-08 08:59:25 -05:00
constructor MakeEnv
mode : EqMode
2023-01-08 14:44:25 -05:00
public export
0 HasEnv : (Type -> Type) -> Type
HasEnv = MonadReader Env
2023-01-08 14:44:25 -05:00
public export
0 CanEqual : (q : Type) -> (Type -> Type) -> Type
CanEqual q m = (HasErr q m, HasEnv m)
2023-01-08 14:44:25 -05:00
private %inline
mode : HasEnv m => m EqMode
2023-01-08 14:44:25 -05:00
mode = asks mode
private %inline
2023-02-10 15:40:44 -05:00
clashT : CanEqual q m => Term q d n -> Term q d n -> Term q d n -> m a
clashT ty s t = throwError $ ClashT !mode ty s t
2023-01-08 14:44:25 -05:00
private %inline
clashE : CanEqual q m => Elim q d n -> Elim q d n -> m a
2023-01-08 14:44:25 -05:00
clashE e f = throwError $ ClashE !mode e f
2023-02-10 15:40:44 -05:00
public export %inline
isType : (t : Term {}) -> Bool
isType (TYPE {}) = True
isType (Pi {}) = True
isType (Lam {}) = False
isType (Sig {}) = True
isType (Pair {}) = False
isType (Eq {}) = True
isType (DLam {}) = False
isType (E {}) = True
isType (CloT {}) = False
isType (DCloT {}) = 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
export %inline
ensureType : (t : Term q d n) -> m (So (isType t))
ensureType = ensure NotType isType
parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)}
mutual
2023-02-10 15:40:44 -05:00
-- [todo] remove cumulativity & subtyping, it's too much of a pain
-- mugen might be good
namespace Term
2023-02-10 15:40:44 -05:00
export covering %inline
compare0 : TContext q 0 n -> (ty, s, t : Term q 0 n) -> m ()
compare0 ctx ty s t = do
let Element ty nty = whnfD defs ty
Element s ns = whnfD defs s
Element t nt = whnfD defs t
tty <- ensureType ty
compare0' ctx ty s t
private %inline
toLamBody : Elim q d n -> Term q d (S n)
toLamBody e = E $ weakE e :@ BVT 0
private covering
compare0' : TContext q 0 n ->
(ty, s, t : Term q 0 n) ->
(0 nty : NotRedex defs ty) => (0 tty : So (isType ty)) =>
(0 ns : NotRedex defs s) => (0 nt : NotRedex defs t) =>
m ()
2023-02-10 15:40:44 -05:00
compare0' ctx (TYPE _) s t = compareType ctx s t
compare0' ctx ty@(Pi {arg, res, _}) s t = local {mode := Equal} $
let ctx' = ctx :< arg
eta : Elim q 0 ? -> ScopeTerm q 0 ? -> m ()
eta e (TUsed b) = compare0 ctx' res.term (toLamBody e) b
eta e (TUnused _) = clashT ty s t
in
case (s, t) of
(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) => ignore $ compare0 ctx e f
_ => throwError $ WrongType ty s t
compare0' ctx ty@(Sig {fst, snd, _}) s t = local {mode := Equal} $
-- no η (no fst/snd for π ≱ 0), so…
-- [todo] η for π ≥ 0 maybe
case (s, t) of
(Pair sFst sSnd, Pair tFst tSnd) => do
compare0 ctx fst sFst tFst
compare0 ctx (sub1 snd (sFst :# fst)) sSnd tSnd
_ => throwError $ WrongType ty s t
-- ✨ uip ✨
compare0' _ (Eq {}) _ _ = pure ()
compare0' ctx ty@(E _) s t = do
-- a neutral type can only be inhabited by neutral values
-- e.g. an abstract value in an abstract type, bound variables, …
E e <- pure s | _ => throwError $ WrongType ty s t
E f <- pure t | _ => throwError $ WrongType ty s t
ignore $ 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
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 (isType s)) =>
(0 nt : NotRedex defs t) => (0 tt : So (isType 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
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
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
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
E e => do
E f <- pure t | _ => err
-- no fanciness needed here cos anything other than a neutral
-- has been inlined by whnfD
ignore $ compare0 ctx e f
namespace Elim
2023-02-10 15:40:44 -05:00
export covering %inline
compare0 : TContext q 0 n -> (e, f : Elim q 0 n) -> m (Term q 0 n)
compare0 ctx e f =
let Element e ne = whnfD defs e
Element f nf = whnfD defs f
in
compare0' ctx e f
private
isSubSing : Term {} -> Bool
isSubSing (TYPE _) = False
isSubSing (Pi {res, _}) = isSubSing res.term
isSubSing (Lam {}) = False
isSubSing (Sig {fst, snd, _}) = isSubSing fst && isSubSing snd.term
isSubSing (Pair {}) = False
isSubSing (Eq {}) = True
isSubSing (DLam {}) = False
isSubSing (E e) = False
isSubSing (CloT tm th) = False
isSubSing (DCloT tm th) = False
private covering
compare0' : TContext q 0 n ->
(e, f : Elim q 0 n) ->
2023-02-10 15:40:44 -05:00
(0 ne : NotRedex defs e) => (0 nf : NotRedex defs f) =>
m (Term q 0 n)
compare0' _ e@(F x) f@(F y) = do
d <- lookupFree' defs x
let ty = d.type
-- [fixme] there is a better way to do this for sure
unless (isSubSing ty.get0 || x == y) $ clashE e f
pure ty.get
compare0' _ e@(F _) f = clashE e f
compare0' ctx e@(B i) f@(B j) = do
let ty = ctx !! i
-- [fixme] there is a better way to do this for sure
unless (isSubSing ty || i == j) $ clashE e f
pure ty
compare0' _ e@(B _) f = clashE e f
compare0' ctx (e :@ s) (f :@ t) = local {mode := Equal} $ do
Pi {arg, res, _} <- compare0 ctx e f
| ty => throwError $ ExpectedPi ty
compare0 ctx arg s t
pure $ sub1 res (s :# arg)
compare0' _ e@(_ :@ _) f = clashE e f
compare0' ctx (CasePair epi e _ eret _ _ ebody)
(CasePair fpi f _ fret _ _ fbody) =
local {mode := Equal} $ do
2023-02-10 15:40:44 -05:00
ty@(Sig {fst, snd, _}) <- compare0 ctx e f
| ty => throwError $ ExpectedSig ty
unless (epi == fpi) $ throwError $ ClashQ epi fpi
compareType (ctx :< ty) eret.term fret.term
compare0 (ctx :< fst :< snd.term) (substCasePairRet ty eret)
ebody.term fbody.term
pure $ sub1 eret e
compare0' _ e@(CasePair {}) f = clashE e f
compare0' ctx (e :% p) (f :% q) = local {mode := Equal} $ do
Eq {ty, _} <- compare0 ctx e f
| ty => throwError $ ExpectedEq ty
unless (p == q) $ throwError $ ClashD p q
pure $ dsub1 ty p
compare0' _ e@(_ :% _) f = clashE e f
compare0' ctx (s :# a) (t :# b) = do
compareType ctx a b
compare0 ctx a s t
pure b
compare0' _ e@(_ :# _) f = clashE e f
parameters {auto _ : (HasDefs' q _ m, HasErr q m, Eq q)}
(eq : DimEq d) (ctx : TContext q d n)
parameters (mode : EqMode)
namespace Term
2023-02-10 15:40:44 -05:00
export covering
compare : (ty, s, t : Term q d n) -> m ()
compare ty s t = do
defs <- ask
runReaderT {m} (MakeEnv {mode}) $
for_ (splits eq) $ \th =>
compare0 defs (map (/// th) ctx) (ty /// th) (s /// th) (t /// th)
2023-02-10 15:40:44 -05:00
export covering
compareType : (s, t : Term q d n) -> m ()
compareType s t = do
defs <- ask
runReaderT {m} (MakeEnv {mode}) $
for_ (splits eq) $ \th =>
compareType defs (map (/// th) ctx) (s /// th) (t /// th)
namespace Elim
2023-02-10 15:40:44 -05:00
-- can't return the type since it might be different in each dsubst ☹
export covering %inline
2023-02-10 15:40:44 -05:00
compare : (e, f : Elim q d n) -> m ()
compare e f = do
defs <- ask
runReaderT {m} (MakeEnv {mode}) $
for_ (splits eq) $ \th =>
ignore $ compare0 defs (map (/// th) ctx) (e /// th) (f /// th)
namespace Term
export covering %inline
2023-02-10 15:40:44 -05:00
equal, sub : (ty, s, t : Term q d n) -> m ()
equal = compare Equal
sub = compare Sub
export covering %inline
2023-02-10 15:40:44 -05:00
equalType, subtype : (s, t : Term q d n) -> m ()
equalType = compareType Equal
subtype = compareType Sub
namespace Elim
export covering %inline
2023-02-10 15:40:44 -05:00
equal, sub : (e, f : Elim q d n) -> m ()
equal = compare Equal
sub = compare Sub