rhi/quox
rhi/quox
1
0
Fork 0
Code Issues 15 Pull requests 1 Releases Wiki Activity

make typechecker actually pass the dimeq to subT

Browse source 
also erase some length arguments
This commit is contained in:
rhiannon morris 2023-01-09 19:03:21 +01:00
parent d8df40ab39
commit 84e524c978
3 changed files with 27 additions and 24 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
lib/Quox/Syntax/DimEq.idr
View file

@ -104,10 +104,10 @@ mutual
export %inline export %inline
setVar : (i, j : Var d) -> DimEq' d -> DimEq d setVar : (i, j : Var d) -> DimEq' d -> DimEq d
setVar i j eqs with (compareP i j) setVar i j eqs = case compareP i j of
_ | IsLT lt = setVar' i j lt eqs IsLT lt => setVar' i j lt eqs
setVar i i eqs | IsEQ = C eqs IsEQ => C eqs
_ | IsGT gt = setVar' j i gt eqs IsGT gt => setVar' j i gt eqs
export %inline export %inline

39
lib/Quox/Typechecker.idr
View file

@ -46,20 +46,23 @@ weakI : IsQty q => InferResult q d n -> InferResult q d (S n)
weakI = {type $= weakT, qout $= (:< zero)} weakI = {type $= weakT, qout $= (:< zero)}
private private
lookupBound : IsQty q => lookupBound : IsQty q => q -> Var n -> TyContext q d n -> InferResult q d n
{n : Nat} -> q -> Var n -> TyContext q d n -> InferResult q d n lookupBound pi VZ ctx@(MkTyContext {tctx = _ :< ty, _}) =
lookupBound pi VZ (MkTyContext {tctx = _ :< ty, _}) = InfRes {type = weakT ty, qout = zeroFor (tail ctx) :< pi}
InfRes {type = weakT ty, qout = zero :< pi}
lookupBound pi (VS i) ctx = lookupBound pi (VS i) ctx =
weakI $ lookupBound pi i (tail ctx) weakI $ lookupBound pi i (tail ctx)
private %inline private %inline
subjMult : IsQty q => (sg : SQty q) -> q -> SQty q subjMult : IsQty q => (sg : SQty q) -> q -> SQty q
subjMult (Element sg subj) qty = subjMult sg qty = if isYes $ isZero qty then szero else sg
if isYes (isZero sg) || isYes (isZero qty)
then Element zero zeroIsSubj
else Element sg subj export
makeDimEq : DContext d -> DimEq d
makeDimEq DNil = zeroEq
makeDimEq (DBind dctx) = makeDimEq dctx :<? Nothing
makeDimEq (DEq p q dctx) = set p q $ makeDimEq dctx
public export public export
@ -78,23 +81,20 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
-- computer but pushing is less work for the me -- computer but pushing is less work for the me
export covering %inline export covering %inline
check : {d, n : Nat} -> check : (ctx : TyContext q d n) -> (sg : SQty q) ->
(ctx : TyContext q d n) -> (sg : SQty q) ->
(subj : Term q d n) -> (ty : Term q d n) -> (subj : Term q d n) -> (ty : Term q d n) ->
m (CheckResult q n) m (CheckResult q n)
check ctx sg subj ty = check' ctx sg (pushSubstsT subj) ty check ctx sg subj ty = check' ctx sg (pushSubstsT subj) ty
export covering %inline export covering %inline
infer : {d, n : Nat} -> infer : (ctx : TyContext q d n) -> (sg : SQty q) ->
(ctx : TyContext q d n) -> (sg : SQty q) ->
(subj : Elim q d n) -> (subj : Elim q d n) ->
m (InferResult q d n) m (InferResult q d n)
infer ctx sg subj = infer' ctx sg (pushSubstsE subj) infer ctx sg subj = infer' ctx sg (pushSubstsE subj)
export covering export covering
check' : {d, n : Nat} -> check' : (ctx : TyContext q d n) -> (sg : SQty q) ->
(ctx : TyContext q d n) -> (sg : SQty q) ->
(subj : NotCloTerm q d n) -> (ty : Term q d n) -> (subj : NotCloTerm q d n) -> (ty : Term q d n) ->
m (CheckResult q n) m (CheckResult q n)
@ -102,7 +102,7 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
l' <- expectTYPE ty l' <- expectTYPE ty
expectEqualQ zero sg.fst expectEqualQ zero sg.fst
unless (l < l') $ throwError $ BadUniverse l l' unless (l < l') $ throwError $ BadUniverse l l'
pure zero pure $ zeroFor ctx
check' ctx sg (Element (Pi qty x arg res) _) ty = do check' ctx sg (Element (Pi qty x arg res) _) ty = do
l <- expectTYPE ty l <- expectTYPE ty
@ -113,7 +113,7 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
ignore $ check (extendTy arg zero ctx) szero res (TYPE l) ignore $ check (extendTy arg zero ctx) szero res (TYPE l)
TUnused res => TUnused res =>
ignore $ check ctx szero res (TYPE l) ignore $ check ctx szero res (TYPE l)
pure zero pure $ zeroFor ctx
check' ctx sg (Element (Lam x body) _) ty = do check' ctx sg (Element (Lam x body) _) ty = do
(qty, arg, res) <- expectPi ty (qty, arg, res) <- expectPi ty
@ -125,19 +125,18 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
check' ctx sg (Element (E e) _) ty = do check' ctx sg (Element (E e) _) ty = do
infres <- infer ctx sg e infres <- infer ctx sg e
ignore $ check ctx szero ty (TYPE UAny) ignore $ check ctx szero ty (TYPE UAny)
subT infres.type ty subTWith (makeDimEq ctx.dctx) infres.type ty
pure infres.qout pure infres.qout
export covering export covering
infer' : {d, n : Nat} -> infer' : (ctx : TyContext q d n) -> (sg : SQty q) ->
(ctx : TyContext q d n) -> (sg : SQty q) ->
(subj : NotCloElim q d n) -> (subj : NotCloElim q d n) ->
m (InferResult q d n) m (InferResult q d n)
infer' ctx sg (Element (F x) _) = do infer' ctx sg (Element (F x) _) = do
Just g <- asks $ lookup x | Nothing => throwError $ NotInScope x Just g <- asks $ lookup x | Nothing => throwError $ NotInScope x
when (isZero g) $ expectEqualQ sg.fst zero when (isZero g) $ expectEqualQ sg.fst zero
pure $ InfRes {type = g.type.get, qout = zero} pure $ InfRes {type = g.type.get, qout = zeroFor ctx}
infer' ctx sg (Element (B i) _) = infer' ctx sg (Element (B i) _) =
pure $ lookupBound sg.fst i ctx pure $ lookupBound sg.fst i ctx

4
lib/Quox/Typing.idr
View file

@ -81,6 +81,10 @@ namespace QOutput
zero : {n : Nat} -> QOutput q n zero : {n : Nat} -> QOutput q n
zero = pure zero zero = pure zero
export
zeroFor : TyContext q _ n -> QOutput q n
zeroFor ctx = const zero <$> ctx.qctx
public export public export
CheckResult : Type -> Nat -> Type CheckResult : Type -> Nat -> Type