From eb8f4974b438b443b7e5a251d40455d130be95cf Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Mon, 30 Sep 2024 12:19:36 +0200 Subject: [PATCH] style --- .../FromInternal/Analysis/Positivity/Checker.hs | 11 +++++------ .../FromInternal/Analysis/TypeChecking/Error/Types.hs | 4 ++-- 2 files changed, 7 insertions(+), 8 deletions(-) diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/Checker.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/Checker.hs index c6a94302dd..923b88530b 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/Checker.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/Checker.hs @@ -91,7 +91,7 @@ checkPositivity noPositivityFlag mut = do throw $ ErrNonStrictlyPositive NonStrictlyPositive - { _nonStrictlyPositiveNewOccurrences = negTys + { _nonStrictlyPositiveOccurrences = negTys } -- NOTE we conservatively assume that axioms have all variables in negative positions @@ -196,10 +196,9 @@ computePolarities tab defs topOccurrences = where addPolarity :: InductiveParam -> Polarity -> Sem r () addPolarity var p = do - modif <- ask - let new :: Polarity = p <> modif - modify (over (builderPolarities . at var) (Just . maybe new (new <>))) - unblock var new + newPol <- (p <>) <$> ask + modify (over (builderPolarities . at var) (Just . maybe newPol (newPol <>))) + unblock var newPol unblock :: forall r. (Members '[State Builder] r) => InductiveParam -> Polarity -> Sem r () unblock p newPol = unblockGo @@ -236,7 +235,7 @@ computePolarities tab defs topOccurrences = AppInductive a -> goInductive a os goAxiomArgs :: (Members '[State Builder, Reader Polarity] r) => [Occurrences] -> Sem r () - goAxiomArgs os = local (const axiomPolarity) (mapM_ go os) + goAxiomArgs os = local (<> axiomPolarity) (mapM_ go os) goVarArgs :: (Members '[State Builder, Reader Polarity] r) => [Occurrences] -> Sem r () goVarArgs os = local (const PolarityNonStrictlyPositive) (mapM_ go os) diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Error/Types.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Error/Types.hs index d1dc75ec8c..e42e6835c8 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Error/Types.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Error/Types.hs @@ -694,7 +694,7 @@ instance ToGenericError InvalidConstructorArgType where newtype NonStrictlyPositive = NonStrictlyPositive { -- This list contains occurrences of the inductive types in non-strictly -- positive positions. Thus it may contain repeated names - _nonStrictlyPositiveNewOccurrences :: NonEmpty InductiveName + _nonStrictlyPositiveOccurrences :: NonEmpty InductiveName } makeLenses ''NonStrictlyPositive @@ -711,7 +711,7 @@ instance ToGenericError NonStrictlyPositive where } where opts' = fromGenericOptions opts - occs :: NonEmpty InductiveName = e ^. nonStrictlyPositiveNewOccurrences + occs :: NonEmpty InductiveName = e ^. nonStrictlyPositiveOccurrences tys = nubHashableNonEmpty occs i = getLoc (tys ^. _head1) msg :: Doc Ann =