From 3bdf5978757dfb9e66ed9ddae58642c386253454 Mon Sep 17 00:00:00 2001 From: Craig Roy Date: Wed, 27 Nov 2024 12:22:36 +0000 Subject: [PATCH] Apply lints --- brat/Brat/Checker.hs | 4 ++-- brat/Brat/Checker/Helpers.hs | 4 ++-- brat/Brat/Checker/Monad.hs | 2 +- brat/Brat/Checker/SolveHoles.hs | 14 ++++++++------ brat/Brat/Eval.hs | 4 +--- brat/Control/Monad/Freer.hs | 2 +- 6 files changed, 15 insertions(+), 15 deletions(-) diff --git a/brat/Brat/Checker.hs b/brat/Brat/Checker.hs index 21541b8..40983c9 100644 --- a/brat/Brat/Checker.hs +++ b/brat/Brat/Checker.hs @@ -660,7 +660,7 @@ check' (Of n e) ((), unders) = case ?my of (elems, unders, rightUnders) <- getVecs len unders pure ((tgt, el):elems, (tgt, ty):unders, rightUnders) getVecs _ unders = pure ([], [], unders) -check' Hope ((), ((tgt, ty):unders)) = case (?my, ty) of +check' Hope ((), (tgt, ty):unders) = case (?my, ty) of (Braty, Left _k) -> do fc <- req AskFC req (ANewHope (toEnd tgt, fc)) @@ -731,7 +731,7 @@ checkBody fnName body cty = do NoLhs tm -> pure (tm, (fcOf tm, fcOf tm)) Clauses (c :| cs) -> do fc <- req AskFC - pure $ (WC fc (Lambda c cs), (bimap fcOf fcOf c)) + pure (WC fc (Lambda c cs), bimap fcOf fcOf c) Undefined -> err (InternalError "Checking undefined clause") ((src, _), _) <- makeBox (fnName ++ ".box") cty $ \conns@(_, unders) -> do (((), ()), leftovers) <- check tm conns diff --git a/brat/Brat/Checker/Helpers.hs b/brat/Brat/Checker/Helpers.hs index 182cc08..882a787 100644 --- a/brat/Brat/Checker/Helpers.hs +++ b/brat/Brat/Checker/Helpers.hs @@ -380,10 +380,10 @@ valueToBinder Braty = Right valueToBinder Kerny = id defineSrc :: Src -> Val Z -> Checking () -defineSrc src v = defineEnd (ExEnd (end src)) v +defineSrc src = defineEnd (ExEnd (end src)) defineTgt :: Tgt -> Val Z -> Checking () -defineTgt tgt v = defineEnd (InEnd (end tgt)) v +defineTgt tgt = defineEnd (InEnd (end tgt)) declareSrc :: Src -> Modey m -> BinderType m -> Checking () declareSrc src my ty = req (Declare (ExEnd (end src)) my ty) diff --git a/brat/Brat/Checker/Monad.hs b/brat/Brat/Checker/Monad.hs index b2b1a1d..b42fe61 100644 --- a/brat/Brat/Checker/Monad.hs +++ b/brat/Brat/Checker/Monad.hs @@ -282,7 +282,7 @@ handler (Req s k) ctx g RemoveHope e -> let hset = hopeSet ctx in if M.member e hset then handler (k ()) (ctx { hopeSet = M.delete e hset }) g - else (Left (dumbErr (InternalError ("Trying to remove hole not in set: " ++ show e)))) + else Left (dumbErr (InternalError ("Trying to remove hole not in set: " ++ show e))) howStuck :: Val n -> Stuck howStuck (VApp (VPar e) _) = AwaitingAny (S.singleton e) diff --git a/brat/Brat/Checker/SolveHoles.hs b/brat/Brat/Checker/SolveHoles.hs index 5928690..168b00b 100644 --- a/brat/Brat/Checker/SolveHoles.hs +++ b/brat/Brat/Checker/SolveHoles.hs @@ -15,7 +15,8 @@ import Bwd import Hasochism import Util (zipSameLength) -import Data.Foldable (traverse_) +import Data.Bifunctor (second) +import Data.Foldable (sequenceA, traverse_) import Data.Functor import qualified Data.Map as M import Data.Type.Equality (TestEquality(..), (:~:)(..)) @@ -106,11 +107,12 @@ typeEqRow :: Modey m -> Ro m lv top0 -> Ro m lv top1 -> Either ErrorMsg (Some ((Ny :* Stack Z TypeKind :* Stack Z Sem) -- The new stack of kinds and fresh level - :* (((:~:) top0) :* ((:~:) top1))) -- Proofs both input rows have same length (quantified over by Some) + :* ((:~:) top0 :* (:~:) top1)) -- Proofs both input rows have same length (quantified over by Some) ,[Checking ()] -- subproblems to run in parallel ) typeEqRow _ _ stuff R0 R0 = pure (Some (stuff :* (Refl :* Refl)), []) -typeEqRow m tm stuff (RPr (_,ty1) ro1) (RPr (_,ty2) ro2) = typeEqRow m tm stuff ro1 ro2 <&> \(res, probs) -> (res, (typeEq tm stuff (kindForMode m) ty1 ty2):probs) +typeEqRow m tm stuff (RPr (_,ty1) ro1) (RPr (_,ty2) ro2) = typeEqRow m tm stuff ro1 ro2 <&> second + ((:) (typeEq tm stuff (kindForMode m) ty1 ty2)) typeEqRow m tm (ny :* kz :* semz) (REx (_,k1) ro1) (REx (_,k2) ro2) | k1 == k2 = typeEqRow m tm (Sy ny :* (kz :<< k1) :* (semz :<< semLvl ny)) ro1 ro2 typeEqRow _ _ _ _ _ = Left $ TypeErr "Mismatched rows" @@ -144,13 +146,13 @@ typeEqRigid tm lvkz (TypeFor m []) (VCon c args) (VCon c' args') | c == c' = typeEqRigid tm lvkz (Star []) (VFun m0 (ins0 :->> outs0)) (VFun m1 (ins1 :->> outs1)) | Just Refl <- testEquality m0 m1 = do probs :: [Checking ()] <- throwLeft $ typeEqRow m0 tm lvkz ins0 ins1 >>= \case -- this is in Either ErrorMsg (Some (lvkz :* (Refl :* Refl)), ps1) -> typeEqRow m0 tm lvkz outs0 outs1 <&> (ps1++) . snd - traverse_ id probs -- uses Applicative (unlike sequence_ which uses Monad), hence parallelized + sequenceA_ probs -- uses Applicative (unlike sequence_ which uses Monad), hence parallelized typeEqRigid tm lvkz (TypeFor _ []) (VSum m0 rs0) (VSum m1 rs1) | Just Refl <- testEquality m0 m1 = case zipSameLength rs0 rs1 of Nothing -> typeErr "Mismatched sum lengths" - Just rs -> traverse eqVariant rs >>= (traverse_ id . concat) + Just rs -> traverse eqVariant rs >>= (sequenceA_ . concat) where - eqVariant (Some r0, Some r1) = throwLeft $ (snd <$> typeEqRow m0 tm lvkz r0 r1) + eqVariant (Some r0, Some r1) = throwLeft (snd <$> typeEqRow m0 tm lvkz r0 r1) typeEqRigid tm _ _ v0 v1 = err $ TypeMismatch tm (show v0) (show v1) wire :: (Src, Val Z, Tgt) -> Checking () diff --git a/brat/Brat/Eval.hs b/brat/Brat/Eval.hs index bc991ec..f9ae33d 100644 --- a/brat/Brat/Eval.hs +++ b/brat/Brat/Eval.hs @@ -302,9 +302,7 @@ eqTests tm lvkz = go -- We can have bogus failures here because we're not normalising under lambdas -- N.B. the value argument is normalised. doesntOccur :: End -> Val n -> Either ErrorMsg () -doesntOccur e (VNum nv) = case getNumVar nv of - Just e' -> collision e e' - _ -> pure () +doesntOccur e (VNum nv) = traverse_ (collision e) (getNumVar nv) where getNumVar :: NumVal (VVar n) -> Maybe End getNumVar (NumValue _ (StrictMonoFun (StrictMono _ mono))) = case mono of diff --git a/brat/Control/Monad/Freer.hs b/brat/Control/Monad/Freer.hs index 34e3573..2fb2405 100644 --- a/brat/Control/Monad/Freer.hs +++ b/brat/Control/Monad/Freer.hs @@ -21,7 +21,7 @@ updateEnd (News m) e = case M.lookup e m of -- The RHS of the operation is the newer news -- Invariant: The domains of these Newses are disjoint instance Semigroup News where - (News m1) <> n2@(News m2) = News (m2 `M.union` (M.map (/// n2) m1)) + (News m1) <> n2@(News m2) = News (m2 `M.union` M.map (/// n2) m1) instance Monoid News where mempty = News M.empty