grtt -> qtt
This commit is contained in:
parent
45825ebc17
commit
468c3a4c6a
7 changed files with 70 additions and 84 deletions
|
|
@ -1,6 +1,4 @@
|
|||
#  quantitative observational extensional(ish) type theory
|
||||
|
||||
hey what would happen if some idiot tried to weld qtt[^1] and xtt together?
|
||||
hey what would happen if some idiot tried to weld qtt and xtt together?
|
||||
let's find out together
|
||||
|
||||
[^1]: actually grtt but wtf is a grox
|
||||
|
|
|
|||
|
|
@ -43,10 +43,8 @@ parameters {auto _ : MonadThrow Error m}
|
|||
Sub => unless (k <= l) $ throw $ ClashU Sub k l
|
||||
compareTN' mode s@(TYPE _) t _ _ = clashT mode s t
|
||||
|
||||
compareTN' mode (Pi qtm1 qty1 _ arg1 res1)
|
||||
(Pi qtm2 qty2 _ arg2 res2) _ _ = do
|
||||
-- [todo] these should probably always be ==, right..?
|
||||
unless (qtm1 == qtm2) $ throw $ ClashQ qtm1 qtm2
|
||||
compareTN' mode (Pi qty1 _ arg1 res1) (Pi qty2 _ arg2 res2) _ _ = do
|
||||
-- [todo] this should probably always be ==, right..?
|
||||
unless (qty1 == qty2) $ throw $ ClashQ qty1 qty2
|
||||
compareT0 mode arg2 arg1 -- reversed for contravariant Sub
|
||||
compareTS0 mode res1 res2
|
||||
|
|
|
|||
|
|
@ -36,7 +36,7 @@ mutual
|
|||
TYPE : (l : Universe) -> Term d n
|
||||
|
||||
||| function type
|
||||
Pi : (qtm, qty : Qty) -> (x : Name) ->
|
||||
Pi : (qty : Qty) -> (x : Name) ->
|
||||
(arg : Term d n) -> (res : ScopeTerm d n) -> Term d n
|
||||
||| function term
|
||||
Lam : (x : Name) -> (body : ScopeTerm d n) -> Term d n
|
||||
|
|
@ -91,7 +91,7 @@ mutual
|
|||
|
||||
public export %inline
|
||||
Arr : Qty -> Term d n -> Term d n -> Term d n
|
||||
Arr pi a b = Pi {qtm = pi, qty = zero, x = "_", arg = a, res = TUnused b}
|
||||
Arr pi a b = Pi {qty = pi, x = "_", arg = a, res = TUnused b}
|
||||
|
||||
||| same as `F` but as a term
|
||||
public export %inline
|
||||
|
|
|
|||
|
|
@ -30,9 +30,9 @@ mutual
|
|||
PrettyHL (Term d n) where
|
||||
prettyM (TYPE l) =
|
||||
parensIfM App $ typeD <//> !(withPrec Arg $ prettyM l)
|
||||
prettyM (Pi qtm qty x s t) =
|
||||
prettyM (Pi qty x s t) =
|
||||
parensIfM Outer $ hang 2 $
|
||||
!(prettyBinder [qtm, qty] x s) <++> !arrowD
|
||||
!(prettyBinder [qty] x s) <++> !arrowD
|
||||
<//> !(under T x $ prettyM t)
|
||||
prettyM (Lam x t) =
|
||||
parensIfM Outer $
|
||||
|
|
|
|||
|
|
@ -64,8 +64,8 @@ mutual
|
|||
Term dfrom from -> NotCloTerm dto to
|
||||
pushSubstsTWith th ph (TYPE l) =
|
||||
ncloT $ TYPE l
|
||||
pushSubstsTWith th ph (Pi qtm qty x a body) =
|
||||
ncloT $ Pi qtm qty x (subs a th ph) (subs body th ph)
|
||||
pushSubstsTWith th ph (Pi qty x a body) =
|
||||
ncloT $ Pi qty x (subs a th ph) (subs body th ph)
|
||||
pushSubstsTWith th ph (Lam x body) =
|
||||
ncloT $ Lam x $ subs body th ph
|
||||
pushSubstsTWith th ph (E e) =
|
||||
|
|
@ -120,9 +120,9 @@ mutual
|
|||
Tighten (Term d) where
|
||||
tighten p (TYPE l) =
|
||||
pure $ TYPE l
|
||||
tighten p (Pi qtm qty x arg res) =
|
||||
Pi qtm qty x <$> tighten p arg
|
||||
<*> tighten p res
|
||||
tighten p (Pi qty x arg res) =
|
||||
Pi qty x <$> tighten p arg
|
||||
<*> tighten p res
|
||||
tighten p (Lam x body) =
|
||||
Lam x <$> tighten p body
|
||||
tighten p (E e) =
|
||||
|
|
@ -160,4 +160,3 @@ weakT t = t //. shift 1
|
|||
public export %inline
|
||||
weakE : Elim d n -> Elim d (S n)
|
||||
weakE t = t //. shift 1
|
||||
|
||||
|
|
|
|||
|
|
@ -16,11 +16,11 @@ expectTYPE s =
|
|||
|
||||
private covering %inline
|
||||
expectPi : MonadThrow Typing.Error m => Term d n ->
|
||||
m (Qty, Qty, Term d n, ScopeTerm d n)
|
||||
m (Qty, Term d n, ScopeTerm d n)
|
||||
expectPi ty =
|
||||
case (whnfT ty).fst of
|
||||
Pi qtm qty _ arg res => pure (qtm, qty, arg, res)
|
||||
_ => throw $ ExpectedPi ty
|
||||
Pi qty _ arg res => pure (qty, arg, res)
|
||||
_ => throw $ ExpectedPi ty
|
||||
|
||||
private %inline
|
||||
expectEqualQ : MonadThrow Equal.Error m =>
|
||||
|
|
@ -40,14 +40,14 @@ tail = {tctx $= tail, qctx $= tail}
|
|||
|
||||
private %inline
|
||||
weakI : InferResult d n -> InferResult d (S n)
|
||||
weakI = {type $= weakT, tmout $= (:< zero), tyout $= (:< zero)}
|
||||
weakI = {type $= weakT, qout $= (:< zero)}
|
||||
|
||||
private
|
||||
lookupBound : {n : Nat} -> Var n -> TyContext d n -> InferResult d n
|
||||
lookupBound VZ (MkTyContext {tctx = _ :< ty, qctx = _ :< tyout, _}) =
|
||||
InfRes {type = weakT ty, tmout = zero :< one, tyout = tyout :< zero}
|
||||
lookupBound (VS i) ctx =
|
||||
weakI $ lookupBound i (tail ctx)
|
||||
lookupBound : {n : Nat} -> Qty -> Var n -> TyContext d n -> InferResult d n
|
||||
lookupBound pi VZ (MkTyContext {tctx = _ :< ty, _}) =
|
||||
InfRes {type = weakT ty, qout = zero :< pi}
|
||||
lookupBound pi (VS i) ctx =
|
||||
weakI $ lookupBound pi i (tail ctx)
|
||||
|
||||
|
||||
mutual
|
||||
|
|
@ -55,88 +55,80 @@ mutual
|
|||
-- to either push them or parametrise the whole typechecker over ambient
|
||||
-- substitutions. both of them seem like the same amount of work for the
|
||||
-- computer but pushing is less work for the me
|
||||
--
|
||||
-- [todo] probably need to check that pi is 1 or 0 like atkey said
|
||||
|
||||
export covering %inline
|
||||
check : MonadThrows [Typing.Error, Equal.Error] m => {d, n : Nat} ->
|
||||
(ctx : TyContext d n) -> (subj : Term d n) -> (ty : Term d n) ->
|
||||
(ctx : TyContext d n) -> (pi : Qty) ->
|
||||
(subj : Term d n) -> (ty : Term d n) ->
|
||||
m (CheckResult n)
|
||||
check ctx subj ty = check' ctx (pushSubstsT subj) ty
|
||||
check ctx pi subj ty = check' ctx pi (pushSubstsT subj) ty
|
||||
|
||||
export covering %inline
|
||||
infer : MonadThrows [Typing.Error, Equal.Error] m => {d, n : Nat} ->
|
||||
(ctx : TyContext d n) -> (subj : Elim d n) ->
|
||||
(ctx : TyContext d n) -> (pi : Qty) -> (subj : Elim d n) ->
|
||||
m (InferResult d n)
|
||||
infer ctx subj = infer' ctx (pushSubstsE subj)
|
||||
infer ctx pi subj = infer' ctx pi (pushSubstsE subj)
|
||||
|
||||
|
||||
export covering
|
||||
check' : MonadThrows [Typing.Error, Equal.Error] m => {d, n : Nat} ->
|
||||
(ctx : TyContext d n) ->
|
||||
(ctx : TyContext d n) -> (pi : Qty) ->
|
||||
(subj : NotCloTerm d n) -> (ty : Term d n) ->
|
||||
m (CheckResult n)
|
||||
|
||||
check' ctx (Element (TYPE l) _) ty = do
|
||||
check' ctx pi (Element (TYPE l) _) ty = do
|
||||
l' <- expectTYPE ty
|
||||
expectEqualQ zero pi
|
||||
unless (l < l') $ throw $ BadUniverse l l'
|
||||
pure $ ChkRes {tmout = zero, tyout = zero}
|
||||
pure zero
|
||||
|
||||
-- [todo] factor this stuff out
|
||||
check' ctx (Element (Pi qtm qty x arg (TUsed res)) _) ty = do
|
||||
check' ctx pi (Element (Pi qty x arg res) _) ty = do
|
||||
l <- expectTYPE ty
|
||||
argty <- check ctx arg (TYPE l)
|
||||
resty <- check (extendTy arg argty.tmout ctx) res (TYPE l)
|
||||
res'tmout <- popQ qty resty.tmout
|
||||
pure $ ChkRes {tmout = argty.tmout + res'tmout, tyout = zero}
|
||||
check' ctx (Element (Pi qtm qty x arg (TUnused res)) _) ty = do
|
||||
ignore $ expectTYPE ty
|
||||
argty <- check ctx arg ty
|
||||
resty <- check ctx res ty
|
||||
expectEqualQ qty zero
|
||||
pure $ ChkRes {tmout = argty.tmout + resty.tmout, tyout = zero}
|
||||
expectEqualQ zero pi
|
||||
ignore $ check ctx zero arg (TYPE l)
|
||||
case res of
|
||||
TUsed res => ignore $ check (extendTy arg zero ctx) zero res (TYPE l)
|
||||
TUnused res => ignore $ check ctx zero res (TYPE l)
|
||||
pure zero
|
||||
|
||||
check' ctx (Element (Lam x body) _) ty = do
|
||||
(qtm, qty, arg, res) <- expectPi ty
|
||||
check' ctx pi (Element (Lam x body) _) ty = do
|
||||
(qty, arg, res) <- expectPi ty
|
||||
-- [todo] do this properly?
|
||||
let body = fromScopeTerm body; res = fromScopeTerm res
|
||||
argres <- check ctx arg (TYPE UAny)
|
||||
let ctx' = extendTy arg argres.tmout ctx
|
||||
bodyres <- check ctx' body res
|
||||
tmout <- popQ qtm bodyres.tmout
|
||||
tyout <- popQ qty bodyres.tyout
|
||||
pure $ ChkRes {tmout, tyout = argres.tmout + tyout}
|
||||
qout <- check (extendTy arg (pi * qty) ctx) pi body res
|
||||
popQ qty qout
|
||||
|
||||
check' ctx (Element (E e) _) ty = do
|
||||
infres <- infer ctx e
|
||||
tyres <- check ctx ty (TYPE UAny)
|
||||
check' ctx pi (Element (E e) _) ty = do
|
||||
infres <- infer ctx pi e
|
||||
ignore $ check ctx zero ty (TYPE UAny)
|
||||
infres.type `subT` ty
|
||||
pure $ ChkRes {tmout = infres.tmout, tyout = tyres.tmout}
|
||||
pure infres.qout
|
||||
|
||||
export covering
|
||||
infer' : MonadThrows [Typing.Error, Equal.Error] m => {d, n : Nat} ->
|
||||
(ctx : TyContext d n) -> (subj : NotCloElim d n) ->
|
||||
(ctx : TyContext d n) -> (pi : Qty) -> (subj : NotCloElim d n) ->
|
||||
m (InferResult d n)
|
||||
|
||||
infer' ctx (Element (F x) _) =
|
||||
infer' ctx pi (Element (F x) _) =
|
||||
-- [todo] check that global is erased ==> pi = zero
|
||||
case lookup x ctx.globals of
|
||||
Just g => pure $ InfRes {type = g.type, tmout = zero, tyout = zero}
|
||||
Just g => pure $ InfRes {type = g.type, qout = zero}
|
||||
Nothing => throw $ NotInScope x
|
||||
|
||||
infer' ctx (Element (B i) _) = pure $ lookupBound i ctx
|
||||
infer' ctx pi (Element (B i) _) =
|
||||
pure $ lookupBound pi i ctx
|
||||
|
||||
infer' ctx (Element (fun :@ arg) _) = do
|
||||
funres <- infer ctx fun
|
||||
(qtm, qty, argty, resty) <- expectPi funres.type
|
||||
let resty = fromScopeTerm resty
|
||||
argres <- check ctx arg argty
|
||||
let ctx' = extendTy argty argres.tyout ctx
|
||||
resres <- check ctx' resty (TYPE UAny)
|
||||
res'tyout <- popQ qty resres.tmout
|
||||
let type = resty //. (arg :# argty ::: id)
|
||||
pure $ InfRes {type,
|
||||
tmout = funres.tmout + qtm * argres.tmout,
|
||||
tyout = res'tyout + qty * argres.tmout}
|
||||
infer' ctx pi (Element (fun :@ arg) _) = do
|
||||
funres <- infer ctx pi fun
|
||||
(qty, argty, res) <- expectPi funres.type
|
||||
argout <- check ctx (pi * qty) arg argty
|
||||
pure $ InfRes {type = fromScopeTerm res //. ((arg :# argty) ::: id),
|
||||
qout = funres.qout + argout}
|
||||
|
||||
infer' ctx (Element (tm :# ty) _) = do
|
||||
ignore $ check ctx ty (TYPE UAny)
|
||||
res <- check ctx tm ty
|
||||
pure $ InfRes {type = ty, tmout = res.tmout, tyout = res.tyout}
|
||||
infer' ctx pi (Element (tm :# ty) _) = do
|
||||
ignore $ check ctx zero ty (TYPE UAny)
|
||||
qout <- check ctx pi tm ty
|
||||
pure $ InfRes {type = ty, qout}
|
||||
|
|
|
|||
|
|
@ -24,11 +24,11 @@ TContext d = Context (Term d)
|
|||
|
||||
public export
|
||||
QContext : Nat -> Type
|
||||
QContext = Triangle' Qty
|
||||
QContext = Context' Qty
|
||||
|
||||
public export
|
||||
QOutput : Nat -> Type
|
||||
QOutput = Context' Qty
|
||||
QOutput = QContext
|
||||
|
||||
|
||||
public export
|
||||
|
|
@ -60,8 +60,8 @@ namespace TContext
|
|||
|
||||
namespace TyContext
|
||||
export
|
||||
extendTy : Term d n -> QOutput n -> TyContext d n -> TyContext d (S n)
|
||||
extendTy s rhos = {tctx $= (:< s), qctx $= (:< rhos)}
|
||||
extendTy : Term d n -> Qty -> TyContext d n -> TyContext d (S n)
|
||||
extendTy s rho = {tctx $= (:< s), qctx $= (:< rho)}
|
||||
|
||||
export
|
||||
extendDim : TyContext d n -> TyContext (S d) n
|
||||
|
|
@ -87,15 +87,14 @@ namespace QOutput
|
|||
|
||||
|
||||
public export
|
||||
record CheckResult n where
|
||||
constructor ChkRes
|
||||
tmout, tyout : QOutput n
|
||||
CheckResult : Nat -> Type
|
||||
CheckResult = QOutput
|
||||
|
||||
public export
|
||||
record InferResult d n where
|
||||
constructor InfRes
|
||||
type : Term d n
|
||||
tmout, tyout : QOutput n
|
||||
qout : QOutput n
|
||||
|
||||
|
||||
public export
|
||||
|
|
|
|||
Loading…
Reference in a new issue