From 9e76bcc76504fb0943c24702f52c6d92e8783dd6 Mon Sep 17 00:00:00 2001 From: rhiannon morris Date: Wed, 27 Apr 2022 22:57:56 +0200 Subject: [PATCH] check quantites of subject and global - subj qty must be 0 or 1 (atkey) - global must not be 0 if used at non-0 --- src/Quox/Syntax/Qty.idr | 11 +++++++ src/Quox/Typechecker.idr | 68 +++++++++++++++++++++++++--------------- src/Quox/Typing.idr | 4 ++- 3 files changed, 56 insertions(+), 27 deletions(-) diff --git a/src/Quox/Syntax/Qty.idr b/src/Quox/Syntax/Qty.idr index f27643f..cea9af9 100644 --- a/src/Quox/Syntax/Qty.idr +++ b/src/Quox/Syntax/Qty.idr @@ -70,3 +70,14 @@ IsQty Qty where zero = Zero; one = One (+) = plus; (*) = times (<=.) = compat + + +public export +data IsSubj : Qty -> Type where + SZero : IsSubj Zero + SOne : IsSubj One + +public export +data IsGlobal : Qty -> Type where + GZero : IsGlobal Zero + GAny : IsGlobal Any diff --git a/src/Quox/Typechecker.idr b/src/Quox/Typechecker.idr index 144127a..62ac62e 100644 --- a/src/Quox/Typechecker.idr +++ b/src/Quox/Typechecker.idr @@ -38,6 +38,12 @@ tail : TyContext d (S n) -> TyContext d n tail = {tctx $= tail, qctx $= tail} +private %inline +globalSubjQty : Global -> Qty +globalSubjQty (MkGlobal {qty = Zero, _}) = Zero +globalSubjQty (MkGlobal {qty = Any, _}) = One + + private %inline weakI : InferResult d n -> InferResult d (S n) weakI = {type $= weakT, qout $= (:< zero)} @@ -50,85 +56,95 @@ lookupBound pi (VS i) ctx = weakI $ lookupBound pi i (tail ctx) +private %inline +subjMult : Qty -> Qty -> Subset Qty IsSubj +subjMult sg qty = + if sg == Zero || qty == Zero + then Element Zero %search + else Element One %search + + mutual -- [todo] it seems like the options here for dealing with substitutions are -- 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) -> (pi : Qty) -> + (ctx : TyContext d n) -> (sg : Qty) -> {auto 0 sgs : IsSubj sg} -> (subj : Term d n) -> (ty : Term d n) -> m (CheckResult n) - check ctx pi subj ty = check' ctx pi (pushSubstsT subj) ty + check ctx sg subj ty = check' ctx sg (pushSubstsT subj) ty export covering %inline infer : MonadThrows [Typing.Error, Equal.Error] m => {d, n : Nat} -> - (ctx : TyContext d n) -> (pi : Qty) -> (subj : Elim d n) -> + (ctx : TyContext d n) -> (sg : Qty) -> {auto 0 sgs : IsSubj sg} -> + (subj : Elim d n) -> m (InferResult d n) - infer ctx pi subj = infer' ctx pi (pushSubstsE subj) + infer ctx sg subj = infer' ctx sg (pushSubstsE subj) export covering check' : MonadThrows [Typing.Error, Equal.Error] m => {d, n : Nat} -> - (ctx : TyContext d n) -> (pi : Qty) -> + (ctx : TyContext d n) -> (sg : Qty) -> {auto 0 sgs : IsSubj sg} -> (subj : NotCloTerm d n) -> (ty : Term d n) -> m (CheckResult n) - check' ctx pi (Element (TYPE l) _) ty = do + check' ctx sg (Element (TYPE l) _) ty = do l' <- expectTYPE ty - expectEqualQ zero pi + expectEqualQ zero sg unless (l < l') $ throw $ BadUniverse l l' pure zero -- [todo] factor this stuff out - check' ctx pi (Element (Pi qty x arg res) _) ty = do + check' ctx sg (Element (Pi qty x arg res) _) ty = do l <- expectTYPE ty - expectEqualQ zero pi + expectEqualQ zero sg 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 pi (Element (Lam x body) _) ty = do + check' ctx sg (Element (Lam x body) _) ty = do (qty, arg, res) <- expectPi ty -- [todo] do this properly? let body = fromScopeTerm body; res = fromScopeTerm res - qout <- check (extendTy arg (pi * qty) ctx) pi body res + qout <- check (extendTy arg (sg * qty) ctx) sg body res popQ qty qout - check' ctx pi (Element (E e) _) ty = do - infres <- infer ctx pi e + check' ctx sg (Element (E e) _) ty = do + infres <- infer ctx sg e ignore $ check ctx zero ty (TYPE UAny) infres.type `subT` ty pure infres.qout export covering infer' : MonadThrows [Typing.Error, Equal.Error] m => {d, n : Nat} -> - (ctx : TyContext d n) -> (pi : Qty) -> (subj : NotCloElim d n) -> + (ctx : TyContext d n) -> (sg : Qty) -> {auto 0 sgs : IsSubj sg} -> + (subj : NotCloElim d n) -> m (InferResult d n) - infer' ctx pi (Element (F x) _) = - -- [todo] check that global is erased ==> pi = zero + infer' ctx sg (Element (F x) _) = case lookup x ctx.globals of - Just g => pure $ InfRes {type = g.type, qout = zero} + Just g => do + expectEqualQ (globalSubjQty g) sg + pure $ InfRes {type = g.type, qout = zero} Nothing => throw $ NotInScope x - infer' ctx pi (Element (B i) _) = - pure $ lookupBound pi i ctx + infer' ctx sg (Element (B i) _) = + pure $ lookupBound sg i ctx - infer' ctx pi (Element (fun :@ arg) _) = do - funres <- infer ctx pi fun + infer' ctx sg (Element (fun :@ arg) _) = do + funres <- infer ctx sg fun (qty, argty, res) <- expectPi funres.type - argout <- check ctx (pi * qty) arg argty + let Element sg' _ = subjMult sg qty + argout <- check ctx sg' arg argty pure $ InfRes {type = fromScopeTerm res //. ((arg :# argty) ::: id), qout = funres.qout + argout} - infer' ctx pi (Element (tm :# ty) _) = do + infer' ctx sg (Element (tm :# ty) _) = do ignore $ check ctx zero ty (TYPE UAny) - qout <- check ctx pi tm ty + qout <- check ctx sg tm ty pure $ InfRes {type = ty, qout} diff --git a/src/Quox/Typing.idr b/src/Quox/Typing.idr index 0974914..30375d1 100644 --- a/src/Quox/Typing.idr +++ b/src/Quox/Typing.idr @@ -34,7 +34,9 @@ QOutput = QContext public export record Global where constructor MkGlobal - type, term : forall d, n. Term d n + qty : Qty + 0 qtyGlobal : IsGlobal qty + type, term : forall d, n. Term d n public export Globals : Type