rename Negative -> NonStrictlyPositive

anoma · Sep 30, 2024 · 10c7a1d · 10c7a1d
1 parent 7a8f7ba
commit 10c7a1d
Show file tree

Hide file tree

Showing 3 changed files with 13 additions and 14 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
@@ -40,7 +40,7 @@ emptyBuilder =
 
 functionSidePolarity :: FunctionSide -> Polarity
 functionSidePolarity = \case
-  FunctionLeft -> PolarityNegative
+  FunctionLeft -> PolarityNonStrictlyPositive
   FunctionRight -> PolarityStrictlyPositive
 
 checkPositivity ::
@@ -96,7 +96,7 @@ checkPositivity noPositivityFlag mut = do
 
 -- NOTE we conservatively assume that axioms have all variables in negative positions
 axiomPolarity :: Polarity
-axiomPolarity = PolarityNegative
+axiomPolarity = PolarityNonStrictlyPositive
 
 -- | Returns the list of non-strictly positive types
 checkStrictlyPositive ::
@@ -134,15 +134,15 @@ checkStrictlyPositive tbl mutual =
       [Occurrences] ->
       Sem r' ()
     goApp (side, lhs) occ = local (functionSidePolarity side <>) $ case lhs of
-      AppVar {} -> local (const PolarityNegative) (mapM_ go occ)
+      AppVar {} -> local (const PolarityNonStrictlyPositive) (mapM_ go occ)
       AppAxiom {} -> local (<> axiomPolarity) (mapM_ go occ)
       AppInductive d -> do
         ctx <- ask
         let pols = getPolarities d
         case ctx of
           PolarityUnused -> impossible
           PolarityStrictlyPositive -> return ()
-          PolarityNegative -> when (isMutual d) (output d)
+          PolarityNonStrictlyPositive -> when (isMutual d) (output d)
         mapM_ (uncurry goArg) (zipExact pols occ)
       where
         getPolarities :: InductiveName -> [Polarity]
@@ -154,7 +154,7 @@ checkStrictlyPositive tbl mutual =
 localPolarity :: (Members '[Reader Polarity] r) => Polarity -> Sem r () -> Sem r ()
 localPolarity p = case p of
   PolarityUnused -> const (return ())
-  PolarityNegative -> local (p <>)
+  PolarityNonStrictlyPositive -> local (p <>)
   PolarityStrictlyPositive -> local (p <>)
 
 computePolarities :: PolarityTable -> NonEmpty InductiveDef -> Occurrences -> HashMap InductiveParam Polarity
@@ -214,8 +214,8 @@ computePolarities tab defs topOccurrences =
 
         increaseMinimum :: Blocking -> Maybe Blocking
         increaseMinimum = case newPol of
-          PolarityNegative -> const Nothing
-          PolarityStrictlyPositive -> Just . set blockingUnblockerMinimum PolarityNegative
+          PolarityNonStrictlyPositive -> const Nothing
+          PolarityStrictlyPositive -> Just . set blockingUnblockerMinimum PolarityNonStrictlyPositive
           PolarityUnused -> impossible
 
         isTriggered :: Blocking -> Bool
@@ -239,7 +239,7 @@ computePolarities tab defs topOccurrences =
     goAxiomArgs os = local (const axiomPolarity) (mapM_ go os)
 
     goVarArgs :: (Members '[State Builder, Reader Polarity] r) => [Occurrences] -> Sem r ()
-    goVarArgs os = local (const PolarityNegative) (mapM_ go os)
+    goVarArgs os = local (const PolarityNonStrictlyPositive) (mapM_ go os)
 
     block ::
       (Members '[State Builder, Reader Polarity] r) =>
@@ -272,6 +272,6 @@ computePolarities tab defs topOccurrences =
               Just pol -> case pol of
                 PolarityUnused -> impossible
                 PolarityStrictlyPositive -> do
-                  block PolarityNegative p o
+                  block PolarityNonStrictlyPositive p o
                   localPolarity PolarityStrictlyPositive (go o)
-                PolarityNegative -> localPolarity PolarityNegative (go o)
+                PolarityNonStrictlyPositive -> localPolarity PolarityNonStrictlyPositive (go o)
diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs
@@ -253,7 +253,7 @@ checkTopMutualBlock (MutualBlock ds) =
     <$> runInferenceDefs
       ( do
           ls <- mapM checkMutualStatement ds
-          checkBlockPositivity (MutualBlock ls) -- TODO uncomment
+          checkBlockPositivity (MutualBlock ls)
           return ls
       )
 

diff --git a/src/Juvix/Data/Polarity.hs b/src/Juvix/Data/Polarity.hs
@@ -8,8 +8,7 @@ import Juvix.Prelude.Pretty
 data Polarity
   = PolarityUnused
   | PolarityStrictlyPositive
-  | -- TODO rename PolarityNegative to PolarityNotStrictlyPositive
-    PolarityNegative
+  | PolarityNonStrictlyPositive
   deriving stock (Ord, Enum, Bounded, Eq, Generic, Data, Show)
 
 instance Hashable Polarity
@@ -26,6 +25,6 @@ instance Monoid Polarity where
 
 instance Pretty Polarity where
   pretty = \case
-    PolarityNegative -> "negative"
+    PolarityNonStrictlyPositive -> "non-strictly-positive"
     PolarityStrictlyPositive -> "strictly-positive"
     PolarityUnused -> "unused"