module Quox.Typechecker import public Quox.Syntax import public Quox.Typing import public Quox.Equal import public Control.Monad.Either import Decidable.Decidable import Data.SnocVect %default total public export 0 CanTC' : (q : Type) -> (q -> Type) -> (Type -> Type) -> Type CanTC' q isGlobal m = (HasErr q m, MonadReader (Definitions' q isGlobal) m) public export 0 CanTC : (q : Type) -> IsQty q => (Type -> Type) -> Type CanTC q = CanTC' q IsGlobal private covering %inline expectTYPE : CanTC' q _ m => Term q d n -> m Universe expectTYPE s = case whnfD !ask s of Element (TYPE l) _ => pure l _ => throwError $ ExpectedTYPE s private covering %inline expectPi : CanTC' q _ m => Term q d n -> m (q, Term q d n, ScopeTerm q d n) expectPi ty = case whnfD !ask ty of Element (Pi qty _ arg res) _ => pure (qty, arg, res) _ => throwError $ ExpectedPi ty private covering %inline expectSig : CanTC' q _ m => Term q d n -> m (Term q d n, ScopeTerm q d n) expectSig ty = case whnfD !ask ty of Element (Sig _ arg res) _ => pure (arg, res) _ => throwError $ ExpectedSig ty private covering %inline expectEq : CanTC' q _ m => Term q d n -> m (DScopeTerm q d n, Term q d n, Term q d n) expectEq ty = case whnfD !ask ty of Element (Eq _ ty l r) _ => pure (ty, l, r) _ => throwError $ ExpectedEq ty private popQs : HasErr q m => IsQty q => SnocVect s q -> QOutput q (s + n) -> m (QOutput q n) popQs [<] qctx = pure qctx popQs (pis :< pi) (qctx :< rh) = do expectCompatQ rh pi; popQs pis qctx private %inline popQ : HasErr q m => IsQty q => q -> QOutput q (S n) -> m (QOutput q n) popQ pi = popQs [< pi] private %inline tail : TyContext q d (S n) -> TyContext q d n tail = {tctx $= tail, qctx $= tail} private %inline weakI : IsQty q => InferResult q d n -> InferResult q d (S n) weakI = {type $= weakT, qout $= (:< zero)} private lookupBound : IsQty q => q -> Var n -> TyContext q d n -> InferResult q d n lookupBound pi VZ (MkTyContext {tctx = tctx :< ty, _}) = InfRes {type = weakT ty, qout = (zero <$ tctx) :< pi} lookupBound pi (VS i) ctx = weakI $ lookupBound pi i (tail ctx) private lookupFree : CanTC' q g m => Name -> m (Definition' q g) lookupFree x = lookupFree' !ask x private %inline subjMult : IsQty q => (sg : SQty q) -> q -> SQty q subjMult sg qty = if isYes $ isZero qty then szero else sg export makeDimEq : DContext d -> DimEq d makeDimEq DNil = zeroEq makeDimEq (DBind dctx) = makeDimEq dctx : SQty q -> Term q d n -> Term q d n -> m (CheckResult q n) check ctx sg subj ty = let Element subj nc = pushSubsts subj in check' ctx sg subj nc ty ||| `check0 ctx subj ty` checks a term in a zero context. export covering %inline check0 : TyContext q d n -> Term q d n -> Term q d n -> m (CheckResult q n) check0 ctx = check (zeroed ctx) szero ||| `infer ctx sg subj` infers the type of `subj` in the context `ctx`, ||| and returns its type and the bound variables it used. export covering %inline infer : TyContext q d n -> SQty q -> Elim q d n -> m (InferResult q d n) infer ctx sg subj = let Element subj nc = pushSubsts subj in infer' ctx sg subj nc export covering check' : TyContext q d n -> SQty q -> (subj : Term q d n) -> (0 nc : NotClo subj) -> Term q d n -> m (CheckResult q n) check' ctx sg (TYPE l) _ ty = do -- if ℓ < ℓ' then Ψ | Γ ⊢ Type ℓ · 0 ⇐ Type ℓ' ⊳ 𝟎 l' <- expectTYPE ty expectEqualQ zero sg.fst unless (l < l') $ throwError $ BadUniverse l l' pure $ zeroFor ctx check' ctx sg (Pi qty _ arg res) _ ty = do l <- expectTYPE ty expectEqualQ zero sg.fst -- if Ψ | Γ ⊢ A · 0 ⇐ Type ℓ ⊳ 𝟎 ignore $ check0 ctx arg (TYPE l) -- if Ψ | Γ, x · 0 : A ⊢ B · 0 ⇐ Type ℓ ⊳ 𝟎 case res of TUsed res => ignore $ check0 (extendTy arg zero ctx) res (TYPE l) TUnused res => ignore $ check0 ctx res (TYPE l) -- then Ψ | Γ ⊢ (x : A) → B · 0 ⇐ Type ℓ ⊳ 𝟎 pure $ zeroFor ctx check' ctx sg (Lam _ body) _ ty = do (qty, arg, res) <- expectPi ty -- if Ψ | Γ, x · πσ : A ⊢ t · σ ⇐ B ⊳ Σ, x · σπ qout <- check (extendTy arg (sg.fst * qty) ctx) sg body.term res.term -- then Ψ | Γ ⊢ λx. t · σ ⇐ (x · π : A) → B ⊳ Σ popQ (sg.fst * qty) qout check' ctx sg (Sig _ fst snd) _ ty = do l <- expectTYPE ty expectEqualQ zero sg.fst -- if Ψ | Γ ⊢ A · 0 ⇐ Type ℓ ⊳ 𝟎 ignore $ check0 ctx fst (TYPE l) -- if Ψ | Γ, x · 0 : A ⊢ B · 0 ⇐ Type ℓ ⊳ 𝟎 case snd of TUsed snd => ignore $ check0 (extendTy fst zero ctx) snd (TYPE l) TUnused snd => ignore $ check0 ctx snd (TYPE l) -- then Ψ | Γ ⊢ (x : A) × B · 0 ⇐ Type ℓ ⊳ 𝟎 pure $ zeroFor ctx check' ctx sg (Pair fst snd) _ ty = do (tfst, tsnd) <- expectSig ty -- if Ψ | Γ ⊢ s · σ ⇐ A ⊳ Σ₁ qfst <- check ctx sg fst tfst let tsnd = sub1 tsnd (fst :# tfst) -- if Ψ | Γ ⊢ t · σ ⇐ B[s] ⊳ Σ₂ qsnd <- check ctx sg snd tsnd -- then Ψ | Γ ⊢ (s, t) · σ ⇐ (x : A) × B ⊳ Σ₁ + Σ₂ pure $ qfst + qsnd check' ctx sg (Eq i t l r) _ ty = do u <- expectTYPE ty expectEqualQ zero sg.fst -- if Ψ, i | Γ ⊢ A · 0 ⇐ Type ℓ ⊳ 𝟎 case t of DUsed t => ignore $ check0 (extendDim ctx) t (TYPE u) DUnused t => ignore $ check0 ctx t (TYPE u) -- if Ψ | Γ ⊢ l · 0 ⇐ A‹0› ⊳ 𝟎 ignore $ check0 ctx t.zero l -- if Ψ | Γ ⊢ r · 0 ⇐ A‹1› ⊳ 𝟎 ignore $ check0 ctx t.one r -- then Ψ | Γ ⊢ Eq [i ⇒ A] l r ⇐ Type ℓ ⊳ 𝟎 pure $ zeroFor ctx check' ctx sg (DLam i body) _ ty = do (ty, l, r) <- expectEq ty -- if Ψ, i | Γ ⊢ t · σ ⇐ A ⊳ Σ qout <- check (extendDim ctx) sg body.term ty.term let eqs = makeDimEq ctx.dctx -- if Ψ ⊢ t‹0› = l equal eqs ctx.tctx ty.zero body.zero l -- if Ψ ⊢ t‹1› = r equal eqs ctx.tctx ty.one body.one r -- then Ψ | Γ ⊢ (λᴰi ⇒ t) · σ ⇐ Eq [i ⇒ A] l r ⊳ Σ pure qout check' ctx sg (E e) _ ty = do -- if Ψ | Γ ⊢ e · σ ⇒ A' ⊳ Σ infres <- infer ctx sg e -- if Ψ ⊢ A' <: A subtype (makeDimEq ctx.dctx) ctx.tctx infres.type ty -- then Ψ | Γ ⊢ e · σ ⇐ A ⊳ Σ pure infres.qout export covering infer' : TyContext q d n -> SQty q -> (subj : Elim q d n) -> (0 nc : NotClo subj) -> m (InferResult q d n) infer' ctx sg (F x) _ = do -- if x · π : A {≔ s} in global context g <- lookupFree x -- if σ ≤ π expectCompatQ sg.fst g.qty -- then Ψ | Γ ⊢ x ⇒ A ⊳ 𝟎 pure $ InfRes {type = g.type.get, qout = zeroFor ctx} infer' ctx sg (B i) _ = -- if x : A ∈ Γ -- then Ψ | Γ ⊢ x · σ ⇒ A ⊳ (𝟎, σ · x, 𝟎) pure $ lookupBound sg.fst i ctx infer' ctx sg (fun :@ arg) _ = do -- if Ψ | Γ ⊢ f · σ ⇒ (x · π : A) → B ⊳ Σ₁ funres <- infer ctx sg fun (qty, argty, res) <- expectPi funres.type -- if Ψ | Γ ⊢ s · σ∧π ⇐ A ⊳ Σ₂ -- (0∧π = σ∧0 = 0; σ∧π = σ otherwise) argout <- check ctx (subjMult sg qty) arg argty -- then Ψ | Γ ⊢ f s · σ ⇒ B[s] ⊳ Σ₁ + Σ₂ pure $ InfRes { type = sub1 res $ arg :# argty, qout = funres.qout + argout } infer' ctx sg (CasePair pi pair _ ret _ _ body) _ = do -- if 1 ≤ π expectCompatQ one pi -- if Ψ | Γ ⊢ pair · 1 ⇒ (x : A) × B ⊳ Σ₁ pairres <- infer ctx sone pair ignore $ check0 (extendTy pairres.type zero ctx) ret.term (TYPE UAny) (tfst, tsnd) <- expectSig pairres.type -- if Ψ | Γ, x · π : A, y · π : B ⊢ σ body ⇐ ret[(x, y)] -- ⊳ Σ₂, x · π₁, y · π₂ -- if π₁, π₂ ≤ π let bodyctx = extendTyN [< (tfst, pi), (tsnd.term, pi)] ctx bodyty = substCasePairRet pairres.type ret bodyout <- check bodyctx sg body.term bodyty >>= popQs [< pi, pi] -- then Ψ | Γ ⊢ σ case ⋯ ⇒ ret[pair] ⊳ πΣ₁ + Σ₂ pure $ InfRes { type = sub1 ret pair, qout = pi * pairres.qout + bodyout } infer' ctx sg (fun :% dim) _ = do -- if Ψ | Γ ⊢ f · σ ⇒ Eq [i ⇒ A] l r ⊳ Σ InfRes {type, qout} <- infer ctx sg fun (ty, _, _) <- expectEq type -- then Ψ | Γ ⊢ f p · σ ⇒ A‹p› ⊳ Σ pure $ InfRes {type = dsub1 ty dim, qout} infer' ctx sg (term :# type) _ = do -- if Ψ | Γ ⊢ A · 0 ⇐ Type ℓ ⊳ 𝟎 ignore $ check0 ctx type (TYPE UAny) -- if Ψ | Γ ⊢ s · σ ⇐ A ⊳ Σ qout <- check ctx sg term type -- then Ψ | Γ ⊢ (s ∷ A) · σ ⇒ A ⊳ Σ pure $ InfRes {type, qout}