module Quox.Equal import public Quox.Syntax import public Quox.Definition import public Quox.Typing import public Control.Monad.Either import public Control.Monad.Reader import Data.Maybe private %inline ClashE : EqMode -> Term q d n -> Elim q d n -> Elim q d n -> Error q ClashE mode ty = ClashT mode ty `on` E public export record Env where constructor MakeEnv mode : EqMode public export 0 HasEnv : (Type -> Type) -> Type HasEnv = MonadReader Env public export 0 CanEqual : (q : Type) -> (Type -> Type) -> Type CanEqual q m = (HasErr q m, HasEnv m) private %inline mode : HasEnv m => m EqMode mode = asks mode private %inline 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 private %inline clashE : CanEqual q m => Elim q d n -> Elim q d n -> m a clashE e f = throwError $ ClashE !mode e f 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 -- [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 () 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 () 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 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) -> (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 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 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) 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 -- can't return the type since it might be different in each dsubst ☹ export covering %inline 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 equal, sub : (ty, s, t : Term q d n) -> m () equal = compare Equal sub = compare Sub export covering %inline equalType, subtype : (s, t : Term q d n) -> m () equalType = compareType Equal subtype = compareType Sub namespace Elim export covering %inline equal, sub : (e, f : Elim q d n) -> m () equal = compare Equal sub = compare Sub