remove New from constructor name

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

Hide file tree

Showing 5 changed files with 12 additions and 12 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
@@ -89,8 +89,8 @@ checkPositivity noPositivityFlag mut = do
           markedPositive d = fromJust (find ((== d) . (^. inductiveName)) defs) ^. inductivePositive
       whenJust (nonEmpty (filter (not . markedPositive) neg)) $ \negTys ->
         throw $
-          ErrNonStrictlyPositiveNew
-            NonStrictlyPositiveNew
+          ErrNonStrictlyPositive
+            NonStrictlyPositive
               { _nonStrictlyPositiveNewOccurrences = negTys
               }
 

diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Error.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Error.hs
@@ -22,7 +22,7 @@ data TypeCheckerError
   | ErrTooManyArgumentsIndType WrongNumberArgumentsIndType
   | ErrTooFewArgumentsIndType WrongNumberArgumentsIndType
   | ErrInvalidPatternMatching InvalidPatternMatching
-  | ErrNonStrictlyPositiveNew NonStrictlyPositiveNew
+  | ErrNonStrictlyPositive NonStrictlyPositive
   | ErrUnsupportedTypeFunction UnsupportedTypeFunction
   | ErrInvalidInstanceType InvalidInstanceType
   | ErrInvalidCoercionType InvalidCoercionType
@@ -69,7 +69,7 @@ instance ToGenericError TypeCheckerError where
     ErrDefaultArgLoop e -> genericError e
     ErrBadScope e -> genericError e
     ErrInvalidConstructorArgType e -> genericError e
-    ErrNonStrictlyPositiveNew e -> genericError e
+    ErrNonStrictlyPositive e -> genericError e
 
 instance Show TypeCheckerError where
   show = \case
@@ -98,4 +98,4 @@ instance Show TypeCheckerError where
     ErrBuiltinNotDefined {} -> "ErrBuiltinNotDefined"
     ErrBadScope {} -> "ErrBadScope"
     ErrInvalidConstructorArgType {} -> "ErrInvalidConstructorArgType"
-    ErrNonStrictlyPositiveNew {} -> "ErrNonStrictlyPositiveNew"
+    ErrNonStrictlyPositive {} -> "ErrNonStrictlyPositive"
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
@@ -691,15 +691,15 @@ instance ToGenericError InvalidConstructorArgType where
               <> line
               <> ppCode opts' ty
 
-newtype NonStrictlyPositiveNew = NonStrictlyPositiveNew
+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
   }
 
-makeLenses ''NonStrictlyPositiveNew
+makeLenses ''NonStrictlyPositive
 
-instance ToGenericError NonStrictlyPositiveNew where
+instance ToGenericError NonStrictlyPositive where
   genericError e = ask >>= generr
     where
       generr opts =

diff --git a/test/Typecheck/Negative.hs b/test/Typecheck/Negative.hs
@@ -284,5 +284,5 @@ negPositivityTests =
     mk :: String -> Path Rel File -> NegTest
     mk testname testfile = negTest testname $(mkRelDir "Internal/Positivity") testfile $
       \case
-        ErrNonStrictlyPositiveNew NonStrictlyPositiveNew {} -> Nothing
+        ErrNonStrictlyPositive NonStrictlyPositive {} -> Nothing
         _ -> wrongError
diff --git a/test/Typecheck/NegativeNew.hs b/test/Typecheck/NegativeNew.hs
@@ -148,14 +148,14 @@ arityTests =
         _ -> wrongError,
     negTest "Evil: issue 2540" $(mkRelDir "Internal/Positivity") $(mkRelFile "Evil.juvix") $
       \case
-        ErrNonStrictlyPositiveNew {} -> Nothing
+        ErrNonStrictlyPositive {} -> Nothing
         _ -> wrongError,
     negTest "Evil: issue 2540 using Axiom" $(mkRelDir "Internal/Positivity") $(mkRelFile "EvilWithAxiom.juvix") $
       \case
-        ErrNonStrictlyPositiveNew {} -> Nothing
+        ErrNonStrictlyPositive {} -> Nothing
         _ -> wrongError,
     negTest "FreeT: issue 2540" $(mkRelDir "Internal/Positivity") $(mkRelFile "FreeT.juvix") $
       \case
-        ErrNonStrictlyPositiveNew {} -> Nothing
+        ErrNonStrictlyPositive {} -> Nothing
         _ -> wrongError
   ]