style

anoma · Sep 30, 2024 · 888045e · 888045e
1 parent 10269aa
commit 888045e
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 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
@@ -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
@@ -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 =