From 4b6b3853a1209dd690e35dddf03f524429d0460d Mon Sep 17 00:00:00 2001 From: rhiannon morris Date: Thu, 24 Aug 2023 19:55:57 +0200 Subject: [PATCH] make uses of eff more consistent --- lib/Quox/Equal.idr | 80 +++++++++++++++++++--------------- lib/Quox/Parser/FromParser.idr | 2 +- lib/Quox/Typechecker.idr | 43 +++++++++--------- tests/Tests/Equal.idr | 8 ++-- tests/Tests/Typechecker.idr | 24 +++++----- 5 files changed, 81 insertions(+), 76 deletions(-) diff --git a/lib/Quox/Equal.idr b/lib/Quox/Equal.idr index c3e49dc..7010c23 100644 --- a/lib/Quox/Equal.idr +++ b/lib/Quox/Equal.idr @@ -13,15 +13,16 @@ EqModeState : Type -> Type EqModeState = State EqMode public export -Equal : Type -> Type -Equal = Eff [ErrorEff, DefsReader, NameGen] +Equal : List (Type -> Type) +Equal = [ErrorEff, DefsReader, NameGen] public export -Equal_ : Type -> Type -Equal_ = Eff [ErrorEff, NameGen, EqModeState] +EqualInner : List (Type -> Type) +EqualInner = [ErrorEff, NameGen, EqModeState] export -runEqualWith_ : EqMode -> NameSuf -> Equal_ a -> (Either Error a, NameSuf) +runEqualWith_ : EqMode -> NameSuf -> + Eff EqualInner a -> (Either Error a, NameSuf) runEqualWith_ mode suf act = extract $ runNameGenWith suf $ @@ -29,12 +30,13 @@ runEqualWith_ mode suf act = evalState mode act export -runEqual_ : EqMode -> Equal_ a -> Either Error a -runEqual_ mode act = fst $ runEqualWith_ mode 0 act +runEqualInner : EqMode -> Eff EqualInner a -> Either Error a +runEqualInner mode act = fst $ runEqualWith_ mode 0 act export -runEqualWith : NameSuf -> Definitions -> Equal a -> (Either Error a, NameSuf) +runEqualWith : NameSuf -> Definitions -> + Eff Equal a -> (Either Error a, NameSuf) runEqualWith suf defs act = extract $ runStateAt GEN suf $ @@ -42,7 +44,7 @@ runEqualWith suf defs act = runExcept act export -runEqual : Definitions -> Equal a -> Either Error a +runEqual : Definitions -> Eff Equal a -> Either Error a runEqual defs act = fst $ runEqualWith 0 defs act @@ -53,19 +55,19 @@ mode = get parameters (loc : Loc) (ctx : EqContext n) private %inline - clashT : Term 0 n -> Term 0 n -> Term 0 n -> Equal_ a + clashT : Term 0 n -> Term 0 n -> Term 0 n -> Eff EqualInner a clashT ty s t = throw $ ClashT loc ctx !mode ty s t private %inline - clashTy : Term 0 n -> Term 0 n -> Equal_ a + clashTy : Term 0 n -> Term 0 n -> Eff EqualInner a clashTy s t = throw $ ClashTy loc ctx !mode s t private %inline - clashE : Elim 0 n -> Elim 0 n -> Equal_ a + clashE : Elim 0 n -> Elim 0 n -> Eff EqualInner a clashE e f = throw $ ClashE loc ctx !mode e f private %inline - wrongType : Term 0 n -> Term 0 n -> Equal_ a + wrongType : Term 0 n -> Term 0 n -> Eff EqualInner a wrongType ty s = throw $ WrongType loc ctx ty s @@ -101,7 +103,8 @@ sameTyCon (E {}) _ = False ||| * an enum type is a subsingleton if it has zero or one tags. ||| * a box type is a subsingleton if its content is public export covering -isSubSing : {n : Nat} -> Definitions -> EqContext n -> Term 0 n -> Equal_ Bool +isSubSing : {n : Nat} -> Definitions -> EqContext n -> Term 0 n -> + Eff EqualInner Bool isSubSing defs ctx ty0 = do Element ty0 nc <- whnf defs ctx ty0.loc ty0 case ty0 of @@ -141,7 +144,7 @@ ensureTyCon loc ctx t = case nchoose $ isTyConE t of private covering computeElimTypeE : (defs : Definitions) -> EqContext n -> (e : Elim 0 n) -> (0 ne : NotRedex defs e) => - Equal_ (Term 0 n) + Eff EqualInner (Term 0 n) computeElimTypeE defs ectx e = let Val n = ectx.termLen in lift $ computeElimType defs (toWhnfContext ectx) e @@ -154,7 +157,7 @@ parameters (defs : Definitions) ||| ||| ⚠ **assumes that `s`, `t` have already been checked against `ty`**. ⚠ export covering %inline - compare0 : EqContext n -> (ty, s, t : Term 0 n) -> Equal_ () + compare0 : EqContext n -> (ty, s, t : Term 0 n) -> Eff EqualInner () compare0 ctx ty s t = wrapErr (WhileComparingT ctx !mode ty s t) $ do let Val n = ctx.termLen @@ -175,7 +178,7 @@ parameters (defs : Definitions) (ty, s, t : Term 0 n) -> (0 _ : NotRedex defs ty) => (0 _ : So (isTyConE ty)) => (0 _ : NotRedex defs s) => (0 _ : NotRedex defs t) => - Equal_ () + Eff EqualInner () compare0' ctx (TYPE {}) s t = compareType ctx s t compare0' ctx ty@(Pi {qty, arg, res, _}) s t {n} = local_ Equal $ @@ -201,7 +204,7 @@ parameters (defs : Definitions) ctx' : EqContext (S n) ctx' = extendTy qty res.name arg ctx - eta : Loc -> Elim 0 n -> ScopeTerm 0 n -> Equal_ () + eta : Loc -> Elim 0 n -> ScopeTerm 0 n -> Eff EqualInner () eta _ e (S _ (Y b)) = compare0 ctx' res.term (toLamBody e) b eta loc e (S _ (N _)) = clashT loc ctx ty s t @@ -297,7 +300,7 @@ parameters (defs : Definitions) ||| compares two types, using the current variance `mode` for universes. ||| fails if they are not types, even if they would happen to be equal. export covering %inline - compareType : EqContext n -> (s, t : Term 0 n) -> Equal_ () + compareType : EqContext n -> (s, t : Term 0 n) -> Eff EqualInner () compareType ctx s t = do let Val n = ctx.termLen Element s' _ <- whnf defs ctx s.loc s @@ -313,7 +316,7 @@ parameters (defs : Definitions) (0 _ : NotRedex defs s) => (0 _ : So (isTyConE s)) => (0 _ : NotRedex defs t) => (0 _ : So (isTyConE t)) => (0 _ : So (sameTyCon s t)) => - Equal_ () + Eff EqualInner () -- equality is the same as subtyping, except with the -- "≤" in the TYPE rule being replaced with "=" compareType' ctx a@(TYPE k {}) (TYPE l {}) = @@ -384,7 +387,7 @@ parameters (defs : Definitions) ||| ⚠ **assumes that they have both been typechecked, and have ||| equal types.** ⚠ export covering %inline - compare0 : EqContext n -> (e, f : Elim 0 n) -> Equal_ () + compare0 : EqContext n -> (e, f : Elim 0 n) -> Eff EqualInner () compare0 ctx e f = wrapErr (WhileComparingE ctx !mode e f) $ do let Val n = ctx.termLen @@ -397,7 +400,7 @@ parameters (defs : Definitions) compare0' : EqContext n -> (e, f : Elim 0 n) -> (0 ne : NotRedex defs e) -> (0 nf : NotRedex defs f) -> - Equal_ () + Eff EqualInner () compare0' ctx e@(F x u _) f@(F y v _) _ _ = unless (x == y && u == v) $ clashE e.loc ctx e f @@ -457,7 +460,8 @@ parameters (defs : Definitions) compare0 ctx (sub1 eret $ Ann (Tag t l.loc) ety l.loc) l r expectEqualQ eloc epi fpi where - lookupArm : Loc -> TagVal -> CaseEnumArms d n -> Equal_ (Term d n) + lookupArm : Loc -> TagVal -> CaseEnumArms d n -> + Eff EqualInner (Term d n) lookupArm loc t arms = case lookup t arms of Just arm => pure arm Nothing => throw $ TagNotIn loc t (fromList $ keys arms) @@ -570,7 +574,7 @@ parameters (defs : Definitions) (ret : Term 0 n) -> (u : Universe) -> (b1, b2 : Maybe (TypeCaseArmBody k 0 n)) -> (def : Term 0 n) -> - Equal_ () + Eff EqualInner () compareArm {b1 = Nothing, b2 = Nothing, _} = pure () compareArm ctx k ret u b1 b2 def = let def = SN def in @@ -580,7 +584,7 @@ parameters (defs : Definitions) compareArm_ : EqContext n -> (k : TyConKind) -> (ret : Term 0 n) -> (u : Universe) -> (b1, b2 : TypeCaseArmBody k 0 n) -> - Equal_ () + Eff EqualInner () compareArm_ ctx KTYPE ret u b1 b2 = compare0 ctx ret b1.term b2.term @@ -626,8 +630,8 @@ parameters (loc : Loc) (ctx : TyContext d n) parameters (mode : EqMode) private - fromEqual_ : Equal_ a -> Equal a - fromEqual_ act = lift $ evalState mode act + fromInner : Eff EqualInner a -> Eff Equal a + fromInner act = lift $ evalState mode act private eachFace : Applicative f => (EqContext n -> DSubst d 0 -> f ()) -> f () @@ -635,18 +639,22 @@ parameters (loc : Loc) (ctx : TyContext d n) for_ (splits loc ctx.dctx) $ \th => act (makeEqContext ctx th) th private - runCompare : (Definitions -> EqContext n -> DSubst d 0 -> Equal_ ()) -> - Equal () - runCompare act = fromEqual_ $ eachFace $ act !(askAt DEFS) + CompareAction : Nat -> Nat -> Type + CompareAction d n = + Definitions -> EqContext n -> DSubst d 0 -> Eff EqualInner () + + private + runCompare : CompareAction d n -> Eff Equal () + runCompare act = fromInner $ eachFace $ act !(askAt DEFS) namespace Term export covering - compare : (ty, s, t : Term d n) -> Equal () + compare : (ty, s, t : Term d n) -> Eff Equal () compare ty s t = runCompare $ \defs, ectx, th => compare0 defs ectx (ty // th) (s // th) (t // th) export covering - compareType : (s, t : Term d n) -> Equal () + compareType : (s, t : Term d n) -> Eff Equal () compareType s t = runCompare $ \defs, ectx, th => compareType defs ectx (s // th) (t // th) @@ -654,26 +662,26 @@ parameters (loc : Loc) (ctx : TyContext d n) ||| you don't have to pass the type in but the arguments must still be ||| of the same type!! export covering - compare : (e, f : Elim d n) -> Equal () + compare : (e, f : Elim d n) -> Eff Equal () compare e f = runCompare $ \defs, ectx, th => compare0 defs ectx (e // th) (f // th) namespace Term export covering %inline - equal, sub, super : (ty, s, t : Term d n) -> Equal () + equal, sub, super : (ty, s, t : Term d n) -> Eff Equal () equal = compare Equal sub = compare Sub super = compare Super export covering %inline - equalType, subtype, supertype : (s, t : Term d n) -> Equal () + equalType, subtype, supertype : (s, t : Term d n) -> Eff Equal () equalType = compareType Equal subtype = compareType Sub supertype = compareType Super namespace Elim export covering %inline - equal, sub, super : (e, f : Elim d n) -> Equal () + equal, sub, super : (e, f : Elim d n) -> Eff Equal () equal = compare Equal sub = compare Sub super = compare Super diff --git a/lib/Quox/Parser/FromParser.idr b/lib/Quox/Parser/FromParser.idr index 7ca26e5..c296d26 100644 --- a/lib/Quox/Parser/FromParser.idr +++ b/lib/Quox/Parser/FromParser.idr @@ -293,7 +293,7 @@ fromPBaseNameNS : PBaseName -> Eff [StateL NS Mods] Name fromPBaseNameNS name = pure $ addMods !(getAt NS) $ fromPBaseName name private -liftTC : TC a -> Eff FromParserPure a +liftTC : Eff TC a -> Eff FromParserPure a liftTC act = do res <- lift $ runExcept $ runReaderAt DEFS !(getAt DEFS) act rethrow $ mapFst WrapTypeError res diff --git a/lib/Quox/Typechecker.idr b/lib/Quox/Typechecker.idr index d5cb0e6..fa02277 100644 --- a/lib/Quox/Typechecker.idr +++ b/lib/Quox/Typechecker.idr @@ -13,25 +13,22 @@ import Quox.EffExtra public export -0 TCEff : List (Type -> Type) -TCEff = [ErrorEff, DefsReader, NameGen] - -public export -0 TC : Type -> Type -TC = Eff TCEff +0 TC : List (Type -> Type) +TC = [ErrorEff, DefsReader, NameGen] export -runTCWith : NameSuf -> Definitions -> TC a -> (Either Error a, NameSuf) +runTCWith : NameSuf -> Definitions -> Eff TC a -> (Either Error a, NameSuf) runTCWith = runEqualWith export -runTC : Definitions -> TC a -> Either Error a +runTC : Definitions -> Eff TC a -> Either Error a runTC = runEqual parameters (loc : Loc) export - popQs : Has ErrorEff fs => QContext s -> QOutput (s + n) -> Eff fs (QOutput n) + popQs : Has ErrorEff fs => QContext s -> QOutput (s + n) -> + Eff fs (QOutput n) popQs [<] qout = pure qout popQs (pis :< pi) (qout :< rh) = do expectCompatQ loc rh pi; popQs pis qout @@ -91,28 +88,28 @@ mutual ||| doing any further work. export covering %inline check : (ctx : TyContext d n) -> SQty -> Term d n -> Term d n -> - TC (CheckResult ctx.dctx n) + Eff TC (CheckResult ctx.dctx n) check ctx sg subj ty = ifConsistent ctx.dctx $ checkC ctx sg subj ty ||| "Ψ | Γ ⊢₀ s ⇐ A" ||| ||| `check0 ctx subj ty` checks a term (as `check`) in a zero context. export covering %inline - check0 : TyContext d n -> Term d n -> Term d n -> TC () + check0 : TyContext d n -> Term d n -> Term d n -> Eff TC () check0 ctx tm ty = ignore $ check ctx szero tm ty -- the output will always be 𝟎 because the subject quantity is 0 ||| `check`, assuming the dimension context is consistent export covering %inline checkC : (ctx : TyContext d n) -> SQty -> Term d n -> Term d n -> - TC (CheckResult' n) + Eff TC (CheckResult' n) checkC ctx sg subj ty = wrapErr (WhileChecking ctx sg.fst subj ty) $ checkCNoWrap ctx sg subj ty export covering %inline checkCNoWrap : (ctx : TyContext d n) -> SQty -> Term d n -> Term d n -> - TC (CheckResult' n) + Eff TC (CheckResult' n) checkCNoWrap ctx sg subj ty = let Element subj nc = pushSubsts subj in check' ctx sg subj ty @@ -122,16 +119,16 @@ mutual ||| `checkType ctx subj ty` checks a type (in a zero context). sometimes the ||| universe doesn't matter, only that a term is _a_ type, so it is optional. export covering %inline - checkType : TyContext d n -> Term d n -> Maybe Universe -> TC () + checkType : TyContext d n -> Term d n -> Maybe Universe -> Eff TC () checkType ctx subj l = ignore $ ifConsistent ctx.dctx $ checkTypeC ctx subj l export covering %inline - checkTypeC : TyContext d n -> Term d n -> Maybe Universe -> TC () + checkTypeC : TyContext d n -> Term d n -> Maybe Universe -> Eff TC () checkTypeC ctx subj l = wrapErr (WhileCheckingTy ctx subj l) $ checkTypeNoWrap ctx subj l export covering %inline - checkTypeNoWrap : TyContext d n -> Term d n -> Maybe Universe -> TC () + checkTypeNoWrap : TyContext d n -> Term d n -> Maybe Universe -> Eff TC () checkTypeNoWrap ctx subj l = let Element subj nc = pushSubsts subj in checkType' ctx subj l @@ -145,13 +142,13 @@ mutual ||| doing any further work. export covering %inline infer : (ctx : TyContext d n) -> SQty -> Elim d n -> - TC (InferResult ctx.dctx d n) + Eff TC (InferResult ctx.dctx d n) infer ctx sg subj = ifConsistent ctx.dctx $ inferC ctx sg subj ||| `infer`, assuming the dimension context is consistent export covering %inline inferC : (ctx : TyContext d n) -> SQty -> Elim d n -> - TC (InferResult' d n) + Eff TC (InferResult' d n) inferC ctx sg subj = wrapErr (WhileInferring ctx sg.fst subj) $ let Element subj nc = pushSubsts subj in @@ -161,7 +158,7 @@ mutual private covering toCheckType : TyContext d n -> SQty -> (subj : Term d n) -> (0 nc : NotClo subj) => Term d n -> - TC (CheckResult' n) + Eff TC (CheckResult' n) toCheckType ctx sg t ty = do u <- expectTYPE !(askAt DEFS) ctx ty.loc ty expectEqualQ t.loc Zero sg.fst @@ -171,7 +168,7 @@ mutual private covering check' : TyContext d n -> SQty -> (subj : Term d n) -> (0 nc : NotClo subj) => Term d n -> - TC (CheckResult' n) + Eff TC (CheckResult' n) check' ctx sg t@(TYPE {}) ty = toCheckType ctx sg t ty @@ -253,7 +250,7 @@ mutual private covering checkType' : TyContext d n -> (subj : Term d n) -> (0 nc : NotClo subj) => - Maybe Universe -> TC () + Maybe Universe -> Eff TC () checkType' ctx (TYPE k loc) u = do -- if 𝓀 < ℓ then Ψ | Γ ⊢₀ Type 𝓀 ⇐ Type ℓ @@ -320,7 +317,7 @@ mutual private covering checkTypeScope : TyContext d n -> Term d n -> - ScopeTerm d n -> Maybe Universe -> TC () + ScopeTerm d n -> Maybe Universe -> Eff TC () checkTypeScope ctx s (S _ (N body)) u = checkType ctx body u checkTypeScope ctx s (S [< x] (Y body)) u = checkType (extendTy Zero x s ctx) body u @@ -329,7 +326,7 @@ mutual private covering infer' : TyContext d n -> SQty -> (subj : Elim d n) -> (0 nc : NotClo subj) => - TC (InferResult' d n) + Eff TC (InferResult' d n) infer' ctx sg (F x u loc) = do -- if π·x : A {≔ s} in global context diff --git a/tests/Tests/Equal.idr b/tests/Tests/Equal.idr index 7756528..881320e 100644 --- a/tests/Tests/Equal.idr +++ b/tests/Tests/Equal.idr @@ -20,7 +20,7 @@ defGlobals = fromList ("eq-AB", ^mkPostulate gzero (^Eq0 (^TYPE 0) (^FT "A" 0) (^FT "B" 0))), ("two", ^mkDef gany (^Nat) (^Succ (^Succ (^Zero))))] -parameters (label : String) (act : Equal ()) +parameters (label : String) (act : Eff Equal ()) {default defGlobals globals : Definitions} testEq : Test testEq = test label $ runEqual globals act @@ -30,13 +30,13 @@ parameters (label : String) (act : Equal ()) parameters (ctx : TyContext d n) - subT, equalT : Term d n -> Term d n -> Term d n -> TC () + subT, equalT : Term d n -> Term d n -> Term d n -> Eff TC () subT ty s t = lift $ Term.sub noLoc ctx ty s t equalT ty s t = lift $ Term.equal noLoc ctx ty s t - equalTy : Term d n -> Term d n -> TC () + equalTy : Term d n -> Term d n -> Eff TC () equalTy s t = lift $ Term.equalType noLoc ctx s t - subE, equalE : Elim d n -> Elim d n -> TC () + subE, equalE : Elim d n -> Elim d n -> Eff TC () subE e f = lift $ Elim.sub noLoc ctx e f equalE e f = lift $ Elim.equal noLoc ctx e f diff --git a/tests/Tests/Typechecker.idr b/tests/Tests/Typechecker.idr index 248d415..b845e5b 100644 --- a/tests/Tests/Typechecker.idr +++ b/tests/Tests/Typechecker.idr @@ -30,10 +30,10 @@ ToInfo Error' where ("wanted", show good), ("wanted", show bad)] -0 M : Type -> Type -M = Eff [Except Error', DefsReader] +0 Test : List (Type -> Type) +Test = [Except Error', DefsReader] -inj : TC a -> M a +inj : Eff TC a -> Eff Test a inj act = rethrow $ mapFst TCError $ runTC !(askAt DEFS) act @@ -109,7 +109,7 @@ defGlobals = fromList ("fst", ^mkDef gany fstTy fstDef), ("snd", ^mkDef gany sndTy sndDef)] -parameters (label : String) (act : Lazy (M ())) +parameters (label : String) (act : Lazy (Eff Test ())) {default defGlobals globals : Definitions} testTC : Test testTC = test label {e = Error', a = ()} $ @@ -120,22 +120,22 @@ parameters (label : String) (act : Lazy (M ())) (extract $ runExcept $ runReaderAt DEFS globals act) $> "()" -inferredTypeEq : TyContext d n -> (exp, got : Term d n) -> M () +inferredTypeEq : TyContext d n -> (exp, got : Term d n) -> Eff Test () inferredTypeEq ctx exp got = wrapErr (const $ WrongInfer ctx.dnames ctx.tnames exp got) $ inj $ lift $ equalType noLoc ctx exp got -qoutEq : (exp, got : QOutput n) -> M () +qoutEq : (exp, got : QOutput n) -> Eff Test () qoutEq qout res = unless (qout == res) $ throw $ WrongQOut qout res -inferAs : TyContext d n -> (sg : SQty) -> Elim d n -> Term d n -> M () +inferAs : TyContext d n -> (sg : SQty) -> Elim d n -> Term d n -> Eff Test () inferAs ctx@(MkTyContext {dctx, _}) sg e ty = do case !(inj $ infer ctx sg e) of Just res => inferredTypeEq ctx ty res.type Nothing => pure () inferAsQ : TyContext d n -> (sg : SQty) -> - Elim d n -> Term d n -> QOutput n -> M () + Elim d n -> Term d n -> QOutput n -> Eff Test () inferAsQ ctx@(MkTyContext {dctx, _}) sg e ty qout = do case !(inj $ infer ctx sg e) of Just res => do @@ -143,20 +143,20 @@ inferAsQ ctx@(MkTyContext {dctx, _}) sg e ty qout = do qoutEq qout res.qout Nothing => pure () -infer_ : TyContext d n -> (sg : SQty) -> Elim d n -> M () +infer_ : TyContext d n -> (sg : SQty) -> Elim d n -> Eff Test () infer_ ctx sg e = ignore $ inj $ infer ctx sg e checkQ : TyContext d n -> SQty -> - Term d n -> Term d n -> QOutput n -> M () + Term d n -> Term d n -> QOutput n -> Eff Test () checkQ ctx@(MkTyContext {dctx, _}) sg s ty qout = do case !(inj $ check ctx sg s ty) of Just res => qoutEq qout res Nothing => pure () -check_ : TyContext d n -> SQty -> Term d n -> Term d n -> M () +check_ : TyContext d n -> SQty -> Term d n -> Term d n -> Eff Test () check_ ctx sg s ty = ignore $ inj $ check ctx sg s ty -checkType_ : TyContext d n -> Term d n -> Maybe Universe -> M () +checkType_ : TyContext d n -> Term d n -> Maybe Universe -> Eff Test () checkType_ ctx s u = inj $ checkType ctx s u