From 896ae3238c833c68869918952adfa5f62a7f792d Mon Sep 17 00:00:00 2001
From: nimec01 <24428341+nimec01@users.noreply.github.com>
Date: Fri, 31 Jan 2025 14:59:15 +0100
Subject: [PATCH 1/5] rename Literal constructors

---
 src/Config.hs                      | 30 ++++++++++++-------------
 src/Formula/Parsing.hs             | 31 ++++++++++++-------------
 src/Formula/Printing.hs            |  4 ++--
 src/Formula/Resolution.hs          | 10 ++++-----
 src/Formula/Types.hs               | 36 +++++++++++++++---------------
 src/Formula/Util.hs                |  2 +-
 src/LogicTasks/Debug.hs            |  4 ++--
 src/LogicTasks/Semantics/Max.hs    |  4 ++--
 src/LogicTasks/Semantics/Min.hs    |  4 ++--
 src/LogicTasks/Semantics/Prolog.hs |  4 ++--
 src/LogicTasks/Semantics/Step.hs   |  2 +-
 src/Trees/Formula.hs               |  8 +++----
 src/Trees/Helpers.hs               |  4 ++--
 test/FormulaSpec.hs                |  4 ++--
 test/ParsingSpec.hs                |  4 ++--
 test/ResolutionSpec.hs             | 14 ++++++------
 16 files changed, 83 insertions(+), 82 deletions(-)

diff --git a/src/Config.hs b/src/Config.hs
index e6920273..f61878d2 100644
--- a/src/Config.hs
+++ b/src/Config.hs
@@ -71,7 +71,7 @@ data PickInst = PickInst {
 
 dPickInst :: PickInst
 dPickInst =  PickInst
-          { formulas = [InstCnf $ mkCnf [mkClause [Literal 'A', Not 'B']], InstCnf $ mkCnf [mkClause [Not 'A', Literal 'B']]]
+          { formulas = [InstCnf $ mkCnf [mkClause [Pos 'A', Neg 'B']], InstCnf $ mkCnf [mkClause [Neg 'A', Pos 'B']]]
           , correct = 1
           , showSolution = False
           , addText = Nothing
@@ -89,7 +89,7 @@ data MaxInst = MaxInst {
 
 dMaxInst :: MaxInst
 dMaxInst =  MaxInst
-          { cnf = mkCnf [mkClause [Literal 'A', Not 'B']]
+          { cnf = mkCnf [mkClause [Pos 'A', Neg 'B']]
           , showSolution = False
           , addText = Nothing
           , unicodeAllowed = False
@@ -108,7 +108,7 @@ data MinInst = MinInst {
 
 dMinInst :: MinInst
 dMinInst =  MinInst
-          { dnf = mkDnf [mkCon [Literal 'A', Not 'B']]
+          { dnf = mkDnf [mkCon [Pos 'A', Neg 'B']]
           , showSolution = False
           , addText = Nothing
           , unicodeAllowed = False
@@ -127,7 +127,7 @@ data FillInst = FillInst {
 
 dFillInst :: FillInst
 dFillInst =  FillInst
-          { formula = InstCnf $ mkCnf [mkClause [Literal 'A', Not 'B']]
+          { formula = InstCnf $ mkCnf [mkClause [Pos 'A', Neg 'B']]
           , missing = [1,4]
           , missingValues = [True, True]
           , showSolution = False
@@ -146,7 +146,7 @@ data DecideInst = DecideInst {
 
 dDecideInst :: DecideInst
 dDecideInst =  DecideInst
-          { formula = InstCnf $ mkCnf [mkClause [Literal 'A', Not 'B']]
+          { formula = InstCnf $ mkCnf [mkClause [Pos 'A', Neg 'B']]
           , changed = [1,4]
           , showSolution = False
           , addText = Nothing
@@ -167,9 +167,9 @@ data StepInst = StepInst {
 
 dStepInst :: StepInst
 dStepInst =  StepInst
-          { clause1 = mkClause [Not 'A', Not 'C', Literal 'B']
-          , clause2 = mkClause [Literal 'A', Not 'C']
-          , solution = (Literal 'A', mkClause [Not 'C', Literal 'B'])
+          { clause1 = mkClause [Neg 'A', Neg 'C', Pos 'B']
+          , clause2 = mkClause [Pos 'A', Neg 'C']
+          , solution = (Pos 'A', mkClause [Neg 'C', Pos 'B'])
           , usesSetNotation = False
           , showSolution = False
           , addText = Nothing
@@ -191,13 +191,13 @@ data ResolutionInst = ResolutionInst {
 
 dResInst :: ResolutionInst
 dResInst = let
-            nAnCpB = mkClause [Not 'A', Not 'C', Literal 'B']
-            pAnC = mkClause [Literal 'A', Not 'C']
-            pC = mkClause [Literal 'C']
-            nB = mkClause [Not 'B']
-            pA = mkClause [Literal 'A']
-            nC = mkClause [Not 'C']
-            nCpB = mkClause [Not 'C', Literal 'B']
+            nAnCpB = mkClause [Neg 'A', Neg 'C', Pos 'B']
+            pAnC = mkClause [Pos 'A', Neg 'C']
+            pC = mkClause [Pos 'C']
+            nB = mkClause [Neg 'B']
+            pA = mkClause [Pos 'A']
+            nC = mkClause [Neg 'C']
+            nCpB = mkClause [Neg 'C', Pos 'B']
               in ResolutionInst
                 { clauses =
                     [ nAnCpB
diff --git a/src/Formula/Parsing.hs b/src/Formula/Parsing.hs
index 29e0aefa..1ac65470 100644
--- a/src/Formula/Parsing.hs
+++ b/src/Formula/Parsing.hs
@@ -17,7 +17,8 @@ module Formula.Parsing (
 import Config
 import Formula.Util
 import ParsingHelpers (caseInsensitive, lexeme, tokenSymbol)
-import Formula.Types
+import Formula.Types hiding (Literal(..))
+import qualified Formula.Types as Lit (Literal(..))
 
 import Control.Monad (void)
 import Data.Map (fromList)
@@ -174,8 +175,8 @@ instance Parse TruthValue where
 
 
 
-instance Parse Literal
-instance FromGrammar Literal where
+instance Parse Lit.Literal
+instance FromGrammar Lit.Literal where
   topLevelSpec = LevelSpec
     { allowOr = False
     , allowAnd = False
@@ -188,8 +189,8 @@ instance FromGrammar Literal where
     , nextLevelSpec = Nothing
     }
 
-  fromGrammar (WithPrecedence (NoArrows (NoOrs (NoAnds (OfAtom (Atom x)))))) = Just $ Literal x
-  fromGrammar (WithPrecedence (NoArrows (NoOrs (NoAnds (NegAtom (Atom x)))))) = Just $ Not x
+  fromGrammar (WithPrecedence (NoArrows (NoOrs (NoAnds (OfAtom (Atom x)))))) = Just $ Lit.Pos x
+  fromGrammar (WithPrecedence (NoArrows (NoOrs (NoAnds (NegAtom (Atom x)))))) = Just $ Lit.Neg x
   fromGrammar _ = Nothing
 
 clauseSetParser :: Parser Clause
@@ -222,9 +223,9 @@ instance FromGrammar Clause where
   fromGrammar (WithPrecedence TopLevelBackImpl) = Nothing
   fromGrammar (WithPrecedence (NoArrows f)) =  mkClause <$> foldlOrs phi (Just []) f
     where
-      phi :: Maybe [Literal] -> Ands -> Maybe [Literal]
-      phi xs (NoAnds (OfAtom (Atom x))) = (Literal x :) <$> xs
-      phi xs (NoAnds ((NegAtom (Atom x)))) = (Not x :) <$> xs
+      phi :: Maybe [Lit.Literal] -> Ands -> Maybe [Lit.Literal]
+      phi xs (NoAnds (OfAtom (Atom x))) = (Lit.Pos x :) <$> xs
+      phi xs (NoAnds ((NegAtom (Atom x)))) = (Lit.Neg x :) <$> xs
       phi _ (NoAnds (Neg{})) = Nothing
       phi _ (NoAnds (OfNested{})) = Nothing
       phi _ Ands{} = Nothing
@@ -247,9 +248,9 @@ instance FromGrammar Con where
   fromGrammar OfNoFixity{} = Nothing
   fromGrammar (WithPrecedence (NoArrows (OfAnds f))) = mkCon <$> foldlAnds phi (Just []) f
     where
-      phi :: Maybe [Literal] -> Neg -> Maybe [Literal]
-      phi xs (OfAtom (Atom x)) = (Literal x :) <$> xs
-      phi xs (NegAtom (Atom x)) = (Not x :) <$> xs
+      phi :: Maybe [Lit.Literal] -> Neg -> Maybe [Lit.Literal]
+      phi xs (OfAtom (Atom x)) = (Lit.Pos x :) <$> xs
+      phi xs (NegAtom (Atom x)) = (Lit.Neg x :) <$> xs
       phi _ Neg{} = Nothing
       phi _ OfNested{} = Nothing
   fromGrammar _ = Nothing
@@ -269,8 +270,8 @@ instance FromGrammar Cnf where
       go (WithPrecedence TopLevelBackImpl) = Nothing
       phi :: Maybe [Clause] -> Neg -> Maybe [Clause]
       phi xs (OfNested (Nested f)) = (:) <$> fromGrammar f  <*> xs
-      phi xs (OfAtom (Atom x)) = (mkClause [Literal x] :) <$> xs
-      phi xs (NegAtom (Atom x)) = (mkClause [Not x] :) <$> xs
+      phi xs (OfAtom (Atom x)) = (mkClause [Lit.Pos x] :) <$> xs
+      phi xs (NegAtom (Atom x)) = (mkClause [Lit.Neg x] :) <$> xs
       phi _ Neg{} = Nothing
 
 instance Parse Dnf
@@ -285,8 +286,8 @@ instance FromGrammar Dnf where
     where
       phi :: Maybe [Con] -> Ands -> Maybe [Con]
       phi xs (NoAnds (OfNested (Nested x))) = (:) <$> fromGrammar x <*> xs
-      phi xs (NoAnds (OfAtom (Atom x))) = (mkCon [Literal x] :) <$> xs
-      phi xs (NoAnds (NegAtom (Atom x))) = (mkCon [Not x] :) <$> xs
+      phi xs (NoAnds (OfAtom (Atom x))) = (mkCon [Lit.Pos x] :) <$> xs
+      phi xs (NoAnds (NegAtom (Atom x))) = (mkCon [Lit.Neg x] :) <$> xs
       phi _ (NoAnds Neg{}) = Nothing
       phi _ (Ands{}) = Nothing
 
diff --git a/src/Formula/Printing.hs b/src/Formula/Printing.hs
index 35da7620..e3ba8e50 100644
--- a/src/Formula/Printing.hs
+++ b/src/Formula/Printing.hs
@@ -51,8 +51,8 @@ instance Pretty ResStep where
 
 
 instance Pretty Literal where
-   pretty (Literal x) = char x
-   pretty (Not x) = myText ['¬', x]
+   pretty (Pos x) = char x
+   pretty (Neg x) = myText ['¬', x]
 
 
 
diff --git a/src/Formula/Resolution.hs b/src/Formula/Resolution.hs
index d20c3aca..35bf4d2e 100644
--- a/src/Formula/Resolution.hs
+++ b/src/Formula/Resolution.hs
@@ -100,8 +100,8 @@ genRes (minLen,maxLen) steps lits = do
               then do
                 chosenChar <- elements xs
                 let
-                  pos = Set.singleton $ Literal chosenChar
-                  neg = Set.singleton $ Not chosenChar
+                  pos = Set.singleton $ Pos chosenChar
+                  neg = Set.singleton $ Neg chosenChar
                   startSet = Set.fromList [pos,neg]
                 buildClauses xs (startSet,[Res (Left (toClause pos),Left (toClause neg), (toClause empty,Nothing))]) 0
               else do
@@ -111,7 +111,7 @@ genRes (minLen,maxLen) steps lits = do
                 chosenClause <- setElements (if Set.null underMin then underMax else underMin)
                 let
                   chooseableLits = filter (\lit ->
-                    Literal lit `Set.notMember` chosenClause && Not lit `Set.notMember` chosenClause) xs
+                    Pos lit `Set.notMember` chosenClause && Neg lit `Set.notMember` chosenClause) xs
                 if null chooseableLits
                     then buildClauses xs (ys,rs) (runs+1)
                     else do
@@ -124,10 +124,10 @@ genRes (minLen,maxLen) steps lits = do
                                 else choose (1,2)
                       chosenChar <- elements chooseableLits
                       if choice == 1
-                        then checkValidAndInsert (Literal chosenChar) chosenClause rs clauseSize 0
+                        then checkValidAndInsert (Pos chosenChar) chosenClause rs clauseSize 0
                         else do
                           firstAmount <- choose (1, clauseSize-1)
-                          chosenSign <- elements [Literal chosenChar, Not chosenChar]
+                          chosenSign <- elements [Pos chosenChar, Neg chosenChar]
                           checkValidAndInsert chosenSign chosenClause rs firstAmount firstAmount
       where
         checkValidAndInsert :: Literal -> Set Literal -> [ResStep] -> Int -> Int -> Gen (Set (Set Literal),[ResStep])
diff --git a/src/Formula/Types.hs b/src/Formula/Types.hs
index 4f5cb6b8..4abfb3ea 100644
--- a/src/Formula/Types.hs
+++ b/src/Formula/Types.hs
@@ -82,8 +82,8 @@ queryClause = HornClause Query
 
 -- | A datatype representing a literal
 data Literal
-    = Literal { letter :: Char} -- ^ positive sign
-    | Not { letter :: Char} -- ^ negative sign
+    = Pos { letter :: Char} -- ^ positive sign
+    | Neg { letter :: Char} -- ^ negative sign
     deriving
       ( Eq -- ^ derived
       , Typeable -- ^ derived
@@ -93,37 +93,37 @@ data Literal
 
 -- | order literals alphabetically first, then prefer a positive sign
 instance Ord Literal where
-   compare (Not x) (Literal y) = if x == y then LT else compare x y
-   compare (Literal x) (Not y) = if x == y then GT else compare x y
+   compare (Neg x) (Pos y) = if x == y then LT else compare x y
+   compare (Pos x) (Neg y) = if x == y then GT else compare x y
    compare l1 l2 = compare (letter l1) (letter l2)
 
 
--- | '¬' denotes a negative sign
+-- | '¬' deNeges a negative sign
 instance Show Literal where
-   show (Literal x) = [x]
-   show (Not x) = ['¬', x]
+   show (Pos x) = [x]
+   show (Neg x) = ['¬', x]
 
 
 instance Read Literal where
-   readsPrec _ ('¬':x:rest) = [(Not x, rest) | x `elem` ['A' .. 'Z']]
-   readsPrec _ (x:rest) = [(Literal x, rest) | x `elem` ['A' .. 'Z']]
+   readsPrec _ ('¬':x:rest) = [(Neg x, rest) | x `elem` ['A' .. 'Z']]
+   readsPrec _ (x:rest) = [(Pos x, rest) | x `elem` ['A' .. 'Z']]
    readsPrec _ _ = []
 
 
 instance Formula Literal where
    literals lit = [lit]
 
-   atomics (Not x) = [Literal x]
+   atomics (Neg x) = [Pos x]
    atomics lit = [lit]
 
    amount _ = 1
 
-   evaluate xs (Not y) = not <$> evaluate xs (Literal y)
+   evaluate xs (Neg y) = not <$> evaluate xs (Pos y)
    evaluate xs z = lookup z xs
 
 instance ToSAT Literal where
-  convert (Literal c) = Sat.Var c
-  convert (Not c) = Sat.Not (Sat.Var c)
+  convert (Pos c) = Sat.Var c
+  convert (Neg c) = Sat.Not (Sat.Var c)
 
 instance Arbitrary Literal where
    arbitrary = genLiteral ['A'..'Z']
@@ -135,13 +135,13 @@ genLiteral :: [Char] -> Gen Literal
 genLiteral [] = error "Cannot construct literal from empty list."
 genLiteral lits = do
    rChar <- elements lits
-   elements [Literal rChar, Not rChar]
+   elements [Pos rChar, Neg rChar]
 
 
 -- | Reverses the sign of the literal
 opposite :: Literal -> Literal
-opposite (Literal l) = Not l
-opposite (Not l) = Literal l
+opposite (Pos l) = Neg l
+opposite (Neg l) = Pos l
 
 
 ------------------------------------------------------------
@@ -278,7 +278,7 @@ genCnf :: (Int,Int) -> (Int,Int) -> [Char] -> Bool -> Gen Cnf
 genCnf (minNum,maxNum) (minLen,maxLen) lits enforceUsingAllLiterals = do
     (num, nLits) <- genForNF (minNum,maxNum) (minLen,maxLen) lits
     cnf <- generateClauses nLits empty num
-      `suchThat` \xs -> not enforceUsingAllLiterals || all ((`elem` concatMap atomics (Set.toList xs)) . Literal) nLits
+      `suchThat` \xs -> not enforceUsingAllLiterals || all ((`elem` concatMap atomics (Set.toList xs)) . Pos) nLits
     pure (Cnf cnf)
   where
     generateClauses :: [Char] -> Set Clause -> Int -> Gen (Set Clause)
@@ -424,7 +424,7 @@ genDnf :: (Int,Int) -> (Int,Int) -> [Char] -> Bool -> Gen Dnf
 genDnf (minNum,maxNum) (minLen,maxLen) lits enforceUsingAllLiterals = do
     (num, nLits) <- genForNF (minNum,maxNum) (minLen,maxLen) lits
     dnf <- generateCons nLits empty num
-      `suchThat` \xs -> not enforceUsingAllLiterals || all ((`elem` concatMap atomics (Set.toList xs)) . Literal) nLits
+      `suchThat` \xs -> not enforceUsingAllLiterals || all ((`elem` concatMap atomics (Set.toList xs)) . Pos) nLits
     pure (Dnf dnf)
   where
     generateCons :: [Char] -> Set Con -> Int -> Gen (Set Con)
diff --git a/src/Formula/Util.hs b/src/Formula/Util.hs
index 3cbbf862..0b7d6dfc 100644
--- a/src/Formula/Util.hs
+++ b/src/Formula/Util.hs
@@ -34,7 +34,7 @@ import Formula.Types
 
 -- | Is the input a positive literal?
 isPositive :: Literal -> Bool
-isPositive (Not _) = False
+isPositive (Neg _) = False
 isPositive _ = True
 
 ---------------------------------------------------------------------------------------------------
diff --git a/src/LogicTasks/Debug.hs b/src/LogicTasks/Debug.hs
index 0e84ed83..7d32570b 100644
--- a/src/LogicTasks/Debug.hs
+++ b/src/LogicTasks/Debug.hs
@@ -55,10 +55,10 @@ analyseCnfGenerator gen = quickCheckWith stdArgs{maxSuccess=1000} $ forAll gen $
   tabulate "clause lengths" (map (show . size . literalSet) . toList $ clauseSet cnf) $
   tabulate "number of clauses" (pure . show . size $ clauseSet cnf) $
   tabulate "trivial clauses (containing both X and not X)" (map (show . isTrivial) . toList $ clauseSet cnf) $
-  tabulate "usage of atomic formulas" (pure . nubSort . map (\case (Literal x) -> x ; (Not x) -> x) $ literals cnf)
+  tabulate "usage of atomic formulas" (pure . nubSort . map (\case (Pos x) -> x ; (Neg x) -> x) $ literals cnf)
     True
 
 isTrivial :: Clause -> Bool
 isTrivial x =
   let (pos,neg) = partition isPositive $ toList $ literalSet x
-  in any (\case (Literal a) -> Not a `elem` neg; _ -> error "impossible") pos
+  in any (\case (Pos a) -> Neg a `elem` neg; _ -> error "impossible") pos
diff --git a/src/LogicTasks/Semantics/Max.hs b/src/LogicTasks/Semantics/Max.hs
index 17bd1d01..dd035d7a 100644
--- a/src/LogicTasks/Semantics/Max.hs
+++ b/src/LogicTasks/Semantics/Max.hs
@@ -64,7 +64,7 @@ description MaxInst{..} = do
   -- jscpd:ignore-start
   paragraph $ indent $ do
     translate $ do
-      let formulaStr = show $ mkCnf [mkClause [Literal 'A', Not 'B'], mkClause [Not 'C', Not 'D']]
+      let formulaStr = show $ mkCnf [mkClause [Pos 'A', Neg 'B'], mkClause [Neg 'C', Neg 'D']]
       german $ unwords ["Ein Lösungsversuch für Formel", formulaStr, "könnte beispielsweise so aussehen: "]
       english $ unwords ["A solution attempt for the formula", formulaStr, "could look like this: "]
     translatedCode $ flip localise $ translations exampleCode
@@ -104,7 +104,7 @@ verifyQuiz MinMaxConfig{..} = do
 
 
 start :: Cnf
-start = mkCnf [mkClause [Literal 'A']]
+start = mkCnf [mkClause [Pos 'A']]
 
 
 
diff --git a/src/LogicTasks/Semantics/Min.hs b/src/LogicTasks/Semantics/Min.hs
index 6458c217..7068f7a5 100644
--- a/src/LogicTasks/Semantics/Min.hs
+++ b/src/LogicTasks/Semantics/Min.hs
@@ -62,7 +62,7 @@ description MinInst{..} = do
 
   paragraph $ indent $ do
     translate $ do
-      let formulaStr = show $ mkDnf [mkCon [Literal 'A', Not 'B'], mkCon [Not 'C', Not 'D']]
+      let formulaStr = show $ mkDnf [mkCon [Pos 'A', Neg 'B'], mkCon [Neg 'C', Neg 'D']]
       german $ unwords ["Ein Lösungsversuch für Formel", formulaStr, "könnte beispielsweise so aussehen: "]
       english $ unwords ["A solution attempt for the formula", formulaStr, "could look like this: "]
     translatedCode $ flip localise $ translations exampleCode
@@ -96,7 +96,7 @@ verifyQuiz = Max.verifyQuiz
 
 
 start :: Dnf
-start = mkDnf [mkCon [Literal 'A']]
+start = mkDnf [mkCon [Pos 'A']]
 
 partialGrade :: OutputCapable m => MinInst -> Delayed Dnf -> LangM m
 partialGrade inst = (partialGrade' inst `withDelayed` parser) displayParseError
diff --git a/src/LogicTasks/Semantics/Prolog.hs b/src/LogicTasks/Semantics/Prolog.hs
index b0442204..5bd5764a 100644
--- a/src/LogicTasks/Semantics/Prolog.hs
+++ b/src/LogicTasks/Semantics/Prolog.hs
@@ -250,9 +250,9 @@ transform (pc1,pc2) = (clause1, clause2, applyPol)
 
     polLookup p = (p,lit)
       where lit = case lookup p mapping of
-                    Just l1  -> Literal l1
+                    Just l1  -> Pos l1
                     Nothing  -> case lookup (flipPol p) mapping of
-                                  Just l2 -> Not l2
+                                  Just l2 -> Neg l2
                                   Nothing -> error "each literal should have a mapping."
 
     applyPol = map polLookup allPredicates
diff --git a/src/LogicTasks/Semantics/Step.hs b/src/LogicTasks/Semantics/Step.hs
index 2a105c33..32e550cc 100644
--- a/src/LogicTasks/Semantics/Step.hs
+++ b/src/LogicTasks/Semantics/Step.hs
@@ -238,7 +238,7 @@ completeGrade' StepInst{..} sol =
 genResStepClause :: Int -> Int -> [Char] -> Gen (Clause, Literal, [Literal])
 genResStepClause minClauseLength maxClauseLength usedLiterals = do
     rChar <- elements usedLiterals
-    resolveLit <- elements [Literal rChar, Not rChar]
+    resolveLit <- elements [Pos rChar, Neg rChar]
     let
       restLits = delete rChar usedLiterals
     minLen1 <- elements [minClauseLength-1..maxClauseLength-1]
diff --git a/src/Trees/Formula.hs b/src/Trees/Formula.hs
index 67297169..ee7da915 100644
--- a/src/Trees/Formula.hs
+++ b/src/Trees/Formula.hs
@@ -10,17 +10,17 @@ import Data.List.Extra (nubSort)
 import Trees.Helpers (collectLeaves, treeNodes)
 
 instance Formula (SynTree BinOp Char) where
-  literals (Leaf x) = [F.Literal x]
-  literals (Not (Leaf x)) = [F.Not x]
+  literals (Leaf x) = [F.Pos x]
+  literals (Not (Leaf x)) = [F.Neg x]
   literals (Not x) = literals x
   literals (Binary _ l r) = nubSort $ literals l ++ literals r
 
   atomics :: SynTree BinOp Char -> [F.Literal]
-  atomics = map F.Literal . nubSort . collectLeaves
+  atomics = map F.Pos . nubSort . collectLeaves
 
   amount = fromIntegral . treeNodes
 
-  evaluate allocation (Leaf x) = snd <$> find (\(k,_) -> F.Literal x == k) allocation
+  evaluate allocation (Leaf x) = snd <$> find (\(k,_) -> F.Pos x == k) allocation
   evaluate allocation (Not x) = not <$> evaluate allocation x
   evaluate allocation (Binary op l r) = applyMaybe (
     case op of
diff --git a/src/Trees/Helpers.hs b/src/Trees/Helpers.hs
index d0247760..bedc869c 100644
--- a/src/Trees/Helpers.hs
+++ b/src/Trees/Helpers.hs
@@ -148,8 +148,8 @@ conToSynTree :: SetFormulaDnf.Con -> SynTree BinOp Char
 conToSynTree = foldr1 (Binary And) . map literalToSynTree . toList . SetFormulaDnf.literalSet
 
 literalToSynTree :: SetFormula.Literal -> SynTree o Char
-literalToSynTree (SetFormula.Literal a) = Leaf a
-literalToSynTree (SetFormula.Not a) = Not (Leaf a)
+literalToSynTree (SetFormula.Pos a) = Leaf a
+literalToSynTree (SetFormula.Neg a) = Not (Leaf a)
 
 
 numOfOps :: SynTree o c -> Integer
diff --git a/test/FormulaSpec.hs b/test/FormulaSpec.hs
index 5a90b536..d24b01a6 100644
--- a/test/FormulaSpec.hs
+++ b/test/FormulaSpec.hs
@@ -84,7 +84,7 @@ spec = do
     it "should generate a random cnf formula containing all given atoms - or else an invariant assumed in LogicTasks.Util.usesAllAtoms becomes wrong" $ -- editorconfig-checker-disable-line
       forAll validBoundsCnf $ \((lowerNum,upperNum),(lowerLen,upperLen),chars) ->
         forAll (genCnf (lowerNum,upperNum) (lowerLen,upperLen) chars True) $ \cnf' ->
-          all (\c -> Literal c `elem` atomics cnf') chars
+          all (\c -> Pos c `elem` atomics cnf') chars
 
   describe "genDnf" $ do
     it "should return the empty disjunction when called with the empty list" $
@@ -106,4 +106,4 @@ spec = do
     it "should generate a random dnf formula containing all given atoms - or else an invariant assumed in LogicTasks.Util.usesAllAtoms becomes wrong" $ -- editorconfig-checker-disable-line
       forAll validBoundsCnf $ \((lowerNum,upperNum),(lowerLen,upperLen),chars) ->
         forAll (genDnf (lowerNum,upperNum) (lowerLen,upperLen) chars True) $ \dnf' ->
-          all (\c -> Literal c `elem` atomics dnf') chars
+          all (\c -> Pos c `elem` atomics dnf') chars
diff --git a/test/ParsingSpec.hs b/test/ParsingSpec.hs
index a98585ed..4696f61b 100644
--- a/test/ParsingSpec.hs
+++ b/test/ParsingSpec.hs
@@ -5,7 +5,7 @@ import Data.Either (isLeft, isRight)
 import Test.Hspec ( describe, it, Spec)
 
 import LogicTasks.Parsing (Parse(parser))
-import LogicTasks.Formula (Cnf, Dnf, mkDnf, mkCon, Literal (Literal, Not))
+import LogicTasks.Formula (Cnf, Dnf, mkDnf, mkCon, Literal (..))
 import Trees.Parsing (formulaParse)
 
 import Text.Parsec (parse)
@@ -48,7 +48,7 @@ spec = do
     it "correctly parses the pretty representation of a PickInst (cnf)" $
       either (const False) (== dPickInst) $ parse (parser @PickInst) "" $ show $ pretty dPickInst
     it "correctly parses the pretty representation of a PickInst (dnf)" $
-      let pickInst = dPickInst { formulas = [InstDnf (mkDnf [mkCon [Literal 'A', Not 'B']])] } in
+      let pickInst = dPickInst { formulas = [InstDnf (mkDnf [mkCon [Pos 'A', Neg 'B']])] } in
         either (const False) (== pickInst) $ parse (parser @PickInst) "" $ show $ pretty pickInst
     it "correctly parses the pretty representation of a PickInst (arbitrary)" $
       let pickInst = dPickInst { formulas = [InstArbitrary (TT.Binary TT.And (TT.Leaf 'A') (TT.Not (TT.Leaf 'B')))] } in
diff --git a/test/ResolutionSpec.hs b/test/ResolutionSpec.hs
index 7cfde447..e9ea601f 100644
--- a/test/ResolutionSpec.hs
+++ b/test/ResolutionSpec.hs
@@ -4,7 +4,7 @@ module ResolutionSpec where
 import Test.Hspec
 import Formula.Resolution (applySteps)
 import Data.Maybe (isJust, fromJust, isNothing)
-import Formula.Types (Clause(Clause), Literal (Literal,Not))
+import Formula.Types (Clause(Clause), Literal (..))
 import qualified Data.Set
 import Config (ResolutionConfig (..), BaseConfig (..), dResConf, ResolutionInst(solution))
 import Test.QuickCheck (Gen, choose, suchThat, forAll)
@@ -15,19 +15,19 @@ import Control.OutputCapable.Blocks.Generic (evalLangM)
 import FillSpec (validBoundsBase)
 
 justA :: Clause
-justA = Clause (Data.Set.fromList [Literal 'A'])
+justA = Clause (Data.Set.fromList [Pos 'A'])
 
 notAnotB :: Clause
-notAnotB = Clause (Data.Set.fromList [Not 'A', Not 'B'])
+notAnotB = Clause (Data.Set.fromList [Neg 'A', Neg 'B'])
 
 notAjustB :: Clause
-notAjustB = Clause (Data.Set.fromList [Not 'A', Literal 'B'])
+notAjustB = Clause (Data.Set.fromList [Neg 'A', Pos 'B'])
 
 notB :: Clause
-notB = Clause (Data.Set.fromList [Not 'B'])
+notB = Clause (Data.Set.fromList [Neg 'B'])
 
 justB :: Clause
-justB = Clause (Data.Set.fromList [Literal 'B'])
+justB = Clause (Data.Set.fromList [Pos 'B'])
 
 emptyClause :: Clause
 emptyClause = Clause Data.Set.empty
@@ -54,7 +54,7 @@ spec = do
     it "should return a Just value if there are no clauses" $
       isJust $ applySteps [] []
     it "should return the original list of clauses if there are no steps to apply" $ do
-      let clauses = [Clause (Data.Set.fromList [Literal 'A'])]
+      let clauses = [Clause (Data.Set.fromList [Pos 'A'])]
       fromJust (applySteps clauses []) == clauses
     it "should return the correct list of clauses if the steps are able to be applied" $ do
       let clauses = [justA, notAnotB, notAjustB]

From e57f1cd58cbc39c649fd50618ebbc192997be86b Mon Sep 17 00:00:00 2001
From: nimec01 <24428341+nimec01@users.noreply.github.com>
Date: Fri, 31 Jan 2025 15:59:15 +0100
Subject: [PATCH 2/5] change type of  + turn some 'literal' to 'atomic'

---
 src/Formula/Resolution.hs          |  2 +-
 src/Formula/Table.hs               | 11 ++++----
 src/Formula/Types.hs               | 42 +++++++++++++++---------------
 src/LogicTasks/Semantics/Decide.hs |  4 +--
 src/LogicTasks/Semantics/Fill.hs   |  4 +--
 src/LogicTasks/Semantics/Max.hs    | 36 ++++++++++++-------------
 src/LogicTasks/Semantics/Pick.hs   |  4 +--
 src/Trees/Formula.hs               |  6 ++---
 test/FormulaSpec.hs                |  4 +--
 9 files changed, 56 insertions(+), 57 deletions(-)

diff --git a/src/Formula/Resolution.hs b/src/Formula/Resolution.hs
index 35bf4d2e..b26d289e 100644
--- a/src/Formula/Resolution.hs
+++ b/src/Formula/Resolution.hs
@@ -53,7 +53,7 @@ resolvableWith c1 c2
     | length possible == 1 = Just (head possible)
     | otherwise = Nothing
   where
-    lits = atomics c1
+    lits = map Pos $ atomics c1 -- TODO: Should `literals` be used here?
     possible = filter (isJust . resolve c1 c2) lits
 
 
diff --git a/src/Formula/Table.hs b/src/Formula/Table.hs
index 58b60493..aab3154f 100644
--- a/src/Formula/Table.hs
+++ b/src/Formula/Table.hs
@@ -2,7 +2,7 @@
 module Formula.Table
        (
          readEntries
-       , readLiterals
+       , readAtomics
        , flipAt
        , gapsAt
        ) where
@@ -20,13 +20,14 @@ import qualified Data.Set as Set (fromList)
 readEntries :: Table -> [Maybe Bool]
 readEntries = getEntries
 
-readLiterals :: Table -> Set Literal
-readLiterals = Set.fromList . getLiterals
+-- Used in Autotool
+readAtomics :: Table -> Set Char
+readAtomics = Set.fromList . getAtomics
 
 
 
 gapsAt :: Table -> [Int] -> Table
-gapsAt table gaps = Table (getLiterals table) newEntries
+gapsAt table gaps = Table (getAtomics table) newEntries
   where
     entries = getEntries table
     newEntries = [ if x+1 `elem` gaps then Nothing else entries !! x
@@ -38,7 +39,7 @@ gapsAt table gaps = Table (getLiterals table) newEntries
 
 
 flipAt :: Table -> [Int] -> Table
-flipAt table indices = Table (getLiterals table) newEntries
+flipAt table indices = Table (getAtomics table) newEntries
   where
     entries = getEntries table
     newEntries = [ let value = entries !! x in
diff --git a/src/Formula/Types.hs b/src/Formula/Types.hs
index 4abfb3ea..2a7c493c 100644
--- a/src/Formula/Types.hs
+++ b/src/Formula/Types.hs
@@ -58,7 +58,7 @@ newtype TruthValue = TruthValue {truth :: Bool}
 
 class Formula a where
     literals :: a -> [Literal]
-    atomics :: a -> [Literal]
+    atomics :: a -> [Char]
     amount :: a -> Int
     evaluate :: Allocation -> a -> Maybe Bool
 
@@ -113,13 +113,13 @@ instance Read Literal where
 instance Formula Literal where
    literals lit = [lit]
 
-   atomics (Neg x) = [Pos x]
-   atomics lit = [lit]
+   atomics (Pos x) = [x]
+   atomics (Neg x) = [x]
 
    amount _ = 1
 
    evaluate xs (Neg y) = not <$> evaluate xs (Pos y)
-   evaluate xs z = lookup z xs
+   evaluate xs (Pos c) = lookup c xs
 
 instance ToSAT Literal where
   convert (Pos c) = Sat.Var c
@@ -204,7 +204,7 @@ genClause (minLength,maxLength) lits = do
 
 
 -- | A shorthand representing an allocation.
-type Allocation = [(Literal, Bool)]
+type Allocation = [(Char, Bool)]
 
 
 --------------------------------------------------------------
@@ -278,7 +278,7 @@ genCnf :: (Int,Int) -> (Int,Int) -> [Char] -> Bool -> Gen Cnf
 genCnf (minNum,maxNum) (minLen,maxLen) lits enforceUsingAllLiterals = do
     (num, nLits) <- genForNF (minNum,maxNum) (minLen,maxLen) lits
     cnf <- generateClauses nLits empty num
-      `suchThat` \xs -> not enforceUsingAllLiterals || all ((`elem` concatMap atomics (Set.toList xs)) . Pos) nLits
+      `suchThat` \xs -> not enforceUsingAllLiterals || all (`elem` concatMap atomics (Set.toList xs)) nLits
     pure (Cnf cnf)
   where
     generateClauses :: [Char] -> Set Clause -> Int -> Gen (Set Clause)
@@ -424,7 +424,7 @@ genDnf :: (Int,Int) -> (Int,Int) -> [Char] -> Bool -> Gen Dnf
 genDnf (minNum,maxNum) (minLen,maxLen) lits enforceUsingAllLiterals = do
     (num, nLits) <- genForNF (minNum,maxNum) (minLen,maxLen) lits
     dnf <- generateCons nLits empty num
-      `suchThat` \xs -> not enforceUsingAllLiterals || all ((`elem` concatMap atomics (Set.toList xs)) . Pos) nLits
+      `suchThat` \xs -> not enforceUsingAllLiterals || all (`elem` concatMap atomics (Set.toList xs)) nLits
     pure (Dnf dnf)
   where
     generateCons :: [Char] -> Set Con -> Int -> Gen (Set Con)
@@ -439,7 +439,7 @@ genDnf (minNum,maxNum) (minLen,maxLen) lits enforceUsingAllLiterals = do
 
 -- | A datatype representing a truth table
 data Table = Table
-    { getLiterals :: [Literal]
+    { getAtomics :: [Char]
     , getEntries :: [Maybe Bool]
     } deriving (Ord,Typeable,Generic)
 
@@ -457,18 +457,18 @@ instance Show Table where
                      ]
       where
         hLine = map (\c -> if c /= '|' then '-' else c) header
-        lits = getLiterals t
+        atoms = getAtomics t
 
         formatLine :: Show a => [a] -> Maybe Bool -> String
         formatLine [] _ = []
         formatLine x y =
             foldr ((\a b -> a ++ " | " ++ b) . show) (maybe "-" (show . fromEnum) y) x ++ "\n"
 
-        header = concat [show x ++ " | " | x <- lits] ++ [availableLetter $ getLiterals t]
+        header = concat [x : " | " | x <- atoms] ++ [availableLetter atoms]
         rows = concat [formatLine x y | (x,y) <- unformattedRows]
           where
 
-            unformattedRows = zip (transpose $ comb (length lits) 1) $ getEntries t
+            unformattedRows = zip (transpose $ comb (length atoms) 1) $ getEntries t
               where
                 comb :: Int -> Int -> [[Int]]
                 comb 0 _ = []
@@ -492,31 +492,31 @@ instance Arbitrary Table where
             pure (getTable (cnf :: Cnf))
 
 
--- | Returns all possible allocations for the list of literals.
-possibleAllocations :: [Literal] -> [Allocation]
-possibleAllocations lits = transpose (allCombinations lits 1)
+-- | Returns all possible allocations for the list of atomics.
+possibleAllocations :: [Char] -> [Allocation]
+possibleAllocations atoms = transpose (allCombinations atoms 1)
   where
-    allCombinations :: [Literal] -> Int ->  [Allocation]
+    allCombinations :: [Char] -> Int ->  [Allocation]
     allCombinations [] _ = []
     allCombinations (x:xs) n =
       concat (replicate n $ pairs False ++ pairs True) : allCombinations xs (n*2)
       where
         num = 2^ length xs
-        pairs :: a -> [(Literal,a)]
+        pairs :: a -> [(Char,a)]
         pairs a = replicate num (x,a)
 
 
 
 -- | Constructs a truth table for the given formula
 getTable :: Formula a => a -> Table
-getTable f = Table lits values
+getTable f = Table atoms values
   where
-    lits = atomics f
-    values = map (`evaluate` f) $ possibleAllocations lits
+    atoms = atomics f
+    values = map (`evaluate` f) $ possibleAllocations atoms
 
 
-availableLetter :: [Literal] -> Char
-availableLetter xs = head $ (['F'..'Z'] ++ "*") \\ map letter xs
+availableLetter :: [Char] -> Char
+availableLetter xs = head $ (['F'..'Z'] ++ "*") \\ xs
 
 
 -------------------------------------------------------------------
diff --git a/src/LogicTasks/Semantics/Decide.hs b/src/LogicTasks/Semantics/Decide.hs
index 0f9e9188..94bf773e 100644
--- a/src/LogicTasks/Semantics/Decide.hs
+++ b/src/LogicTasks/Semantics/Decide.hs
@@ -31,7 +31,7 @@ import Test.QuickCheck (Gen, suchThat)
 
 import Config (DecideConfig(..), DecideInst(..), FormulaConfig (..), FormulaInst (..))
 import Formula.Table (flipAt, readEntries)
-import Formula.Types (atomics, availableLetter, getTable, literals)
+import Formula.Types (atomics, availableLetter, getTable)
 import Util (isOutside, remove, withRatio, checkTruthValueRangeAndFormulaConf)
 import LogicTasks.Helpers (extra)
 import Control.Monad (when)
@@ -89,7 +89,7 @@ description withDropdowns DecideInst{..} = do
     translate $ do
       english "Consider the following formula:"
       german "Betrachten Sie die folgende Formel:"
-    indent $ code $ availableLetter (literals formula) : " = " ++ displayFormula formula
+    indent $ code $ availableLetter (atomics formula) : " = " ++ displayFormula formula
     pure ()
   paragraph $ do
     translate $ do
diff --git a/src/LogicTasks/Semantics/Fill.hs b/src/LogicTasks/Semantics/Fill.hs
index 68900c90..0044286e 100644
--- a/src/LogicTasks/Semantics/Fill.hs
+++ b/src/LogicTasks/Semantics/Fill.hs
@@ -26,7 +26,7 @@ import Test.QuickCheck(Gen, suchThat)
 
 import Config ( FillConfig(..), FillInst(..), FormulaInst (..), FormulaConfig (..))
 import Formula.Table (gapsAt, readEntries)
-import Formula.Types (TruthValue, availableLetter, atomics, getTable, literals, truth)
+import Formula.Types (TruthValue, availableLetter, atomics, getTable, truth)
 import Util (isOutside, pairwiseCheck, preventWithHint, remove, withRatio, tryGen, checkTruthValueRangeAndFormulaConf)
 import LogicTasks.Helpers (extra)
 import Trees.Generate (genSynTree)
@@ -74,7 +74,7 @@ description inputHelp FillInst{..} = do
     translate $ do
       german  "Betrachten Sie die folgende Formel:"
       english "Consider the following formula:"
-    indent $ code $ availableLetter (literals formula) : " = " ++ displayFormula formula
+    indent $ code $ availableLetter (atomics formula) : " = " ++ displayFormula formula
     pure ()
   paragraph $ do
     translate $ do
diff --git a/src/LogicTasks/Semantics/Max.hs b/src/LogicTasks/Semantics/Max.hs
index dd035d7a..ba4d7562 100644
--- a/src/LogicTasks/Semantics/Max.hs
+++ b/src/LogicTasks/Semantics/Max.hs
@@ -108,32 +108,32 @@ start = mkCnf [mkClause [Pos 'A']]
 
 
 
-partialMinMax :: (OutputCapable m, Formula f) => [Literal] -> f -> f -> Bool -> Bool -> LangM m
-partialMinMax correctLits correct solution allValidTerms isMaxTermTask = do
-  preventWithHint (not $ null extraLiterals)
+partialMinMax :: (OutputCapable m, Formula f) => [Char] -> f -> f -> Bool -> Bool -> LangM m
+partialMinMax correctAtoms correct solution allValidTerms isMaxTermTask = do
+  preventWithHint (not $ null extraAtoms)
     (translate $ do
-      german "Angegebene Literale kommen in Aufgabe vor?"
-      english "Given literals are used in task?"
+      german "Angegebene atomare Formeln kommen in Aufgabe vor?"
+      english "Given atomic formulas are used in task?"
     )
 
     (paragraph $ do
       translate $ do
-        german "Es sind unbekannte Literale enthalten. Diese Literale kommen in der korrekten Lösung nicht vor: "
-        english "Your submission contains unknown literals. These do not appear in a correct solution: "
-      itemizeM $ map (text . show) extraLiterals
+        german "Es sind unbekannte atomare Formeln enthalten. Diese atomaren Formeln kommen in der korrekten Lösung nicht vor: "
+        english "Your submission contains unknown atomic formulas. These do not appear in a correct solution: "
+      itemizeM $ map (text . show) extraAtoms
       pure ()
     )
 
   preventWithHint (not $ null missing)
     (translate $ do
-      german "Alle Literale kommen vor?"
-      english "All literals are contained in solution?"
+      german "Alle atomaren Formeln kommen vor?"
+      english "All atomic formulas are contained in solution?"
     )
 
     (paragraph $ do
       translate $ do
-        german "Es fehlen Literale. Fügen Sie diese Literale der Abgabe hinzu: "
-        english "Some literals are missing. Add these literals to your submission: "
+        german "Es fehlen atomare Formeln. Fügen Sie diese atomaren Formeln der Abgabe hinzu: "
+        english "Some atomic formulas are missing. Add these atomic formulas to your submission: "
       itemizeM $ map (text . show) missing
       pure ()
     )
@@ -175,9 +175,9 @@ partialMinMax correctLits correct solution allValidTerms isMaxTermTask = do
     )
   pure ()
  where
-    solLits = atomics solution
-    extraLiterals = solLits \\ correctLits
-    missing = correctLits \\ solLits
+    solAtoms = atomics solution
+    extraAtoms = solAtoms \\ correctAtoms
+    missing = correctAtoms \\ solAtoms
     table = getTable correct
     corrLen = length $ filter (== Just False) (readEntries table)
     solLen = amount solution
@@ -190,10 +190,10 @@ partialGrade :: OutputCapable m => MaxInst -> Delayed Cnf -> LangM m
 partialGrade inst = (partialGrade' inst `withDelayed` parser) displayParseError
 
 partialGrade' :: OutputCapable m => MaxInst -> Cnf -> LangM m
-partialGrade' MaxInst{..} sol = partialMinMax corLits cnf sol allMaxTerms True
+partialGrade' MaxInst{..} sol = partialMinMax corAtoms cnf sol allMaxTerms True
   where
-    corLits = atomics cnf
-    allMaxTerms = not $ all (\c -> amount c == length corLits) $ getClauses sol
+    corAtoms = atomics cnf
+    allMaxTerms = not $ all (\c -> amount c == length corAtoms) $ getClauses sol
 
 
 
diff --git a/src/LogicTasks/Semantics/Pick.hs b/src/LogicTasks/Semantics/Pick.hs
index c85a2969..ec469267 100644
--- a/src/LogicTasks/Semantics/Pick.hs
+++ b/src/LogicTasks/Semantics/Pick.hs
@@ -24,7 +24,7 @@ import Test.QuickCheck (Gen, suchThat, elements)
 
 import Config (Number(..), PickConfig(..), PickInst(..), FormulaConfig (..), FormulaInst (..), BaseConfig (..), NormalFormConfig(..))
 import Formula.Util (isSemanticEqual)
-import Formula.Types (availableLetter, getTable, literals)
+import Formula.Types (availableLetter, getTable, Formula (atomics))
 import Formula.Printing (showIndexedList)
 import LogicTasks.Helpers (extra)
 import Data.Maybe (fromJust, fromMaybe)
@@ -67,7 +67,7 @@ description inputHelp PickInst{..} = do
       translate $ do
         german "Betrachten Sie die folgende Formel:"
         english "Consider the following formula:"
-      indent $ code $ availableLetter (literals correctFormula) : " = " ++ displayFormula correctFormula
+      indent $ code $ availableLetter (atomics correctFormula) : " = " ++ displayFormula correctFormula
       pure ()
     paragraph $ do
       translate $ do
diff --git a/src/Trees/Formula.hs b/src/Trees/Formula.hs
index ee7da915..1ad85280 100644
--- a/src/Trees/Formula.hs
+++ b/src/Trees/Formula.hs
@@ -1,6 +1,5 @@
 {-# LANGUAGE FlexibleInstances #-}
 {-# OPTIONS_GHC -Wno-orphans #-}
-{-# LANGUAGE InstanceSigs #-}
 module Trees.Formula where
 import Formula.Types (Formula(..))
 import Trees.Types (SynTree(..), BinOp(..))
@@ -15,12 +14,11 @@ instance Formula (SynTree BinOp Char) where
   literals (Not x) = literals x
   literals (Binary _ l r) = nubSort $ literals l ++ literals r
 
-  atomics :: SynTree BinOp Char -> [F.Literal]
-  atomics = map F.Pos . nubSort . collectLeaves
+  atomics = nubSort . collectLeaves
 
   amount = fromIntegral . treeNodes
 
-  evaluate allocation (Leaf x) = snd <$> find (\(k,_) -> F.Pos x == k) allocation
+  evaluate allocation (Leaf x) = snd <$> find (\(k,_) -> x == k) allocation
   evaluate allocation (Not x) = not <$> evaluate allocation x
   evaluate allocation (Binary op l r) = applyMaybe (
     case op of
diff --git a/test/FormulaSpec.hs b/test/FormulaSpec.hs
index d24b01a6..b821d312 100644
--- a/test/FormulaSpec.hs
+++ b/test/FormulaSpec.hs
@@ -84,7 +84,7 @@ spec = do
     it "should generate a random cnf formula containing all given atoms - or else an invariant assumed in LogicTasks.Util.usesAllAtoms becomes wrong" $ -- editorconfig-checker-disable-line
       forAll validBoundsCnf $ \((lowerNum,upperNum),(lowerLen,upperLen),chars) ->
         forAll (genCnf (lowerNum,upperNum) (lowerLen,upperLen) chars True) $ \cnf' ->
-          all (\c -> Pos c `elem` atomics cnf') chars
+          all (\c -> c `elem` atomics cnf') chars
 
   describe "genDnf" $ do
     it "should return the empty disjunction when called with the empty list" $
@@ -106,4 +106,4 @@ spec = do
     it "should generate a random dnf formula containing all given atoms - or else an invariant assumed in LogicTasks.Util.usesAllAtoms becomes wrong" $ -- editorconfig-checker-disable-line
       forAll validBoundsCnf $ \((lowerNum,upperNum),(lowerLen,upperLen),chars) ->
         forAll (genDnf (lowerNum,upperNum) (lowerLen,upperLen) chars True) $ \dnf' ->
-          all (\c -> Pos c `elem` atomics dnf') chars
+          all (\c -> c `elem` atomics dnf') chars

From af0c5a331db0297ee505e26589703338f3465418 Mon Sep 17 00:00:00 2001
From: nimec01 <24428341+nimec01@users.noreply.github.com>
Date: Fri, 31 Jan 2025 16:20:48 +0100
Subject: [PATCH 3/5] fix accidental replacement

---
 src/Formula/Types.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Formula/Types.hs b/src/Formula/Types.hs
index 2a7c493c..6857ab6c 100644
--- a/src/Formula/Types.hs
+++ b/src/Formula/Types.hs
@@ -98,7 +98,7 @@ instance Ord Literal where
    compare l1 l2 = compare (letter l1) (letter l2)
 
 
--- | '¬' deNeges a negative sign
+-- | '¬' denotes a negative sign
 instance Show Literal where
    show (Pos x) = [x]
    show (Neg x) = ['¬', x]

From ab2f72d5d85fa0e3c3ebbeedd22cf8c014698e16 Mon Sep 17 00:00:00 2001
From: nimec01 <24428341+nimec01@users.noreply.github.com>
Date: Tue, 11 Feb 2025 14:23:56 +0100
Subject: [PATCH 4/5] apply changes after merge

---
 src/Formula/Util.hs | 17 ++++++-----------
 1 file changed, 6 insertions(+), 11 deletions(-)

diff --git a/src/Formula/Util.hs b/src/Formula/Util.hs
index 57284355..766320c2 100644
--- a/src/Formula/Util.hs
+++ b/src/Formula/Util.hs
@@ -39,11 +39,6 @@ isPositive :: Literal -> Bool
 isPositive (Neg _) = False
 isPositive _ = True
 
--- | Return the used char in an atom. Can be removed after #248 was merged.
-atomicChar :: Literal -> Char
-atomicChar (Literal c) = c
-atomicChar _ = error "this should not happen"
-
 ---------------------------------------------------------------------------------------------------
 
 -- | Builds a clause containing the given literals.
@@ -101,16 +96,16 @@ hasEmptyCon (Dnf set) = Con Set.empty `Set.member` set
 ---------------------------------------------------------------------------------------------------
 
 replaceLiteral :: Char -> Literal -> Literal
-replaceLiteral c l@(Literal a)
-  | a == c = Not c
+replaceLiteral c l@(Pos a)
+  | a == c = Neg c
   | otherwise = l
-replaceLiteral c l@(Not a)
-  | a == c = Literal c
+replaceLiteral c l@(Neg a)
+  | a == c = Pos c
   | otherwise = l
 
 cnfDependsOnAllAtomics :: Cnf -> Bool
 cnfDependsOnAllAtomics cnf = not $ any (\c -> isSemanticEqual cnf (replaceAtomInCnf c cnf) ) atoms
-  where atoms = map atomicChar $ atomics cnf
+  where atoms = atomics cnf
 
         replaceAtomInCnf c (Cnf clauses) = Cnf $ Set.map (replaceAtomInClause c) clauses
 
@@ -119,7 +114,7 @@ cnfDependsOnAllAtomics cnf = not $ any (\c -> isSemanticEqual cnf (replaceAtomIn
 
 dnfDependsOnAllAtomics :: Dnf -> Bool
 dnfDependsOnAllAtomics dnf = not $ any (\c -> isSemanticEqual dnf (replaceAtomInDnf c dnf) ) atoms
-  where atoms = map atomicChar $ atomics dnf
+  where atoms = atomics dnf
 
         replaceAtomInDnf c (Dnf cons) = Dnf $ Set.map (replaceAtomInCon c) cons
 

From 3005941e4eb2a9e005439b35558efdf515db0eb0 Mon Sep 17 00:00:00 2001
From: nimec01 <24428341+nimec01@users.noreply.github.com>
Date: Tue, 11 Feb 2025 14:27:44 +0100
Subject: [PATCH 5/5] change constructor names

---
 src/Config.hs                      | 30 ++++++++++++-------------
 src/Formula/Parsing.hs             | 31 +++++++++++++------------
 src/Formula/Printing.hs            |  4 ++--
 src/Formula/Resolution.hs          | 12 +++++-----
 src/Formula/Types.hs               | 36 +++++++++++++++---------------
 src/Formula/Util.hs                | 10 ++++-----
 src/LogicTasks/Debug.hs            |  6 ++---
 src/LogicTasks/Semantics/Max.hs    |  4 ++--
 src/LogicTasks/Semantics/Min.hs    |  4 ++--
 src/LogicTasks/Semantics/Prolog.hs |  4 ++--
 src/LogicTasks/Semantics/Step.hs   |  2 +-
 src/Trees/Formula.hs               |  7 +++---
 src/Trees/Helpers.hs               |  4 ++--
 test/ParsingSpec.hs                |  2 +-
 test/ResolutionSpec.hs             | 12 +++++-----
 15 files changed, 83 insertions(+), 85 deletions(-)

diff --git a/src/Config.hs b/src/Config.hs
index 027739d1..2cabf719 100644
--- a/src/Config.hs
+++ b/src/Config.hs
@@ -71,7 +71,7 @@ data PickInst = PickInst {
 
 dPickInst :: PickInst
 dPickInst =  PickInst
-          { formulas = [InstCnf $ mkCnf [mkClause [Pos 'A', Neg 'B']], InstCnf $ mkCnf [mkClause [Neg 'A', Pos 'B']]]
+          { formulas = [InstCnf $ mkCnf [mkClause [Positive 'A', Negative 'B']], InstCnf $ mkCnf [mkClause [Negative 'A', Positive 'B']]]
           , correct = 1
           , showSolution = False
           , addText = Nothing
@@ -89,7 +89,7 @@ data MaxInst = MaxInst {
 
 dMaxInst :: MaxInst
 dMaxInst =  MaxInst
-          { cnf = mkCnf [mkClause [Pos 'A', Neg 'B']]
+          { cnf = mkCnf [mkClause [Positive 'A', Negative 'B']]
           , showSolution = False
           , addText = Nothing
           , unicodeAllowed = False
@@ -108,7 +108,7 @@ data MinInst = MinInst {
 
 dMinInst :: MinInst
 dMinInst =  MinInst
-          { dnf = mkDnf [mkCon [Pos 'A', Neg 'B']]
+          { dnf = mkDnf [mkCon [Positive 'A', Negative 'B']]
           , showSolution = False
           , addText = Nothing
           , unicodeAllowed = False
@@ -127,7 +127,7 @@ data FillInst = FillInst {
 
 dFillInst :: FillInst
 dFillInst =  FillInst
-          { formula = InstCnf $ mkCnf [mkClause [Pos 'A', Neg 'B']]
+          { formula = InstCnf $ mkCnf [mkClause [Positive 'A', Negative 'B']]
           , missing = [1,4]
           , missingValues = [True, True]
           , showSolution = False
@@ -146,7 +146,7 @@ data DecideInst = DecideInst {
 
 dDecideInst :: DecideInst
 dDecideInst =  DecideInst
-          { formula = InstCnf $ mkCnf [mkClause [Pos 'A', Neg 'B']]
+          { formula = InstCnf $ mkCnf [mkClause [Positive 'A', Negative 'B']]
           , changed = [1,4]
           , showSolution = False
           , addText = Nothing
@@ -167,9 +167,9 @@ data StepInst = StepInst {
 
 dStepInst :: StepInst
 dStepInst =  StepInst
-          { clause1 = mkClause [Neg 'A', Neg 'C', Pos 'B']
-          , clause2 = mkClause [Pos 'A', Neg 'C']
-          , solution = (Pos 'A', mkClause [Neg 'C', Pos 'B'])
+          { clause1 = mkClause [Negative 'A', Negative 'C', Positive 'B']
+          , clause2 = mkClause [Positive 'A', Negative 'C']
+          , solution = (Positive 'A', mkClause [Negative 'C', Positive 'B'])
           , usesSetNotation = False
           , showSolution = False
           , addText = Nothing
@@ -191,13 +191,13 @@ data ResolutionInst = ResolutionInst {
 
 dResInst :: ResolutionInst
 dResInst = let
-            nAnCpB = mkClause [Neg 'A', Neg 'C', Pos 'B']
-            pAnC = mkClause [Pos 'A', Neg 'C']
-            pC = mkClause [Pos 'C']
-            nB = mkClause [Neg 'B']
-            pA = mkClause [Pos 'A']
-            nC = mkClause [Neg 'C']
-            nCpB = mkClause [Neg 'C', Pos 'B']
+            nAnCpB = mkClause [Negative 'A', Negative 'C', Positive 'B']
+            pAnC = mkClause [Positive 'A', Negative 'C']
+            pC = mkClause [Positive 'C']
+            nB = mkClause [Negative 'B']
+            pA = mkClause [Positive 'A']
+            nC = mkClause [Negative 'C']
+            nCpB = mkClause [Negative 'C', Positive 'B']
               in ResolutionInst
                 { clauses =
                     [ nAnCpB
diff --git a/src/Formula/Parsing.hs b/src/Formula/Parsing.hs
index 6a2def83..76de1df2 100644
--- a/src/Formula/Parsing.hs
+++ b/src/Formula/Parsing.hs
@@ -16,8 +16,7 @@ module Formula.Parsing (
 import Config
 import Formula.Util
 import ParsingHelpers (caseInsensitive, lexeme, tokenSymbol)
-import Formula.Types hiding (Literal(..))
-import qualified Formula.Types as Lit (Literal(..))
+import Formula.Types
 
 import Control.Monad (void)
 import Data.Map (fromList)
@@ -170,8 +169,8 @@ instance Parse TruthValue where
 
 
 
-instance Parse Lit.Literal
-instance FromGrammar Lit.Literal where
+instance Parse Literal
+instance FromGrammar Literal where
   topLevelSpec = LevelSpec
     { allowOr = False
     , allowAnd = False
@@ -184,8 +183,8 @@ instance FromGrammar Lit.Literal where
     , nextLevelSpec = Nothing
     }
 
-  fromGrammar (WithPrecedence (NoArrows (NoOrs (NoAnds (OfAtom (Atom x)))))) = Just $ Lit.Pos x
-  fromGrammar (WithPrecedence (NoArrows (NoOrs (NoAnds (NegAtom (Atom x)))))) = Just $ Lit.Neg x
+  fromGrammar (WithPrecedence (NoArrows (NoOrs (NoAnds (OfAtom (Atom x)))))) = Just $ Positive x
+  fromGrammar (WithPrecedence (NoArrows (NoOrs (NoAnds (NegAtom (Atom x)))))) = Just $ Negative x
   fromGrammar _ = Nothing
 
 clauseSetParser :: Parser Clause
@@ -218,9 +217,9 @@ instance FromGrammar Clause where
   fromGrammar (WithPrecedence TopLevelBackImpl) = Nothing
   fromGrammar (WithPrecedence (NoArrows f)) =  mkClause <$> foldlOrs phi (Just []) f
     where
-      phi :: Maybe [Lit.Literal] -> Ands -> Maybe [Lit.Literal]
-      phi xs (NoAnds (OfAtom (Atom x))) = (Lit.Pos x :) <$> xs
-      phi xs (NoAnds ((NegAtom (Atom x)))) = (Lit.Neg x :) <$> xs
+      phi :: Maybe [Literal] -> Ands -> Maybe [Literal]
+      phi xs (NoAnds (OfAtom (Atom x))) = (Positive x :) <$> xs
+      phi xs (NoAnds ((NegAtom (Atom x)))) = (Negative x :) <$> xs
       phi _ (NoAnds (Neg{})) = Nothing
       phi _ (NoAnds (OfNested{})) = Nothing
       phi _ Ands{} = Nothing
@@ -243,9 +242,9 @@ instance FromGrammar Con where
   fromGrammar OfNoFixity{} = Nothing
   fromGrammar (WithPrecedence (NoArrows (OfAnds f))) = mkCon <$> foldlAnds phi (Just []) f
     where
-      phi :: Maybe [Lit.Literal] -> Neg -> Maybe [Lit.Literal]
-      phi xs (OfAtom (Atom x)) = (Lit.Pos x :) <$> xs
-      phi xs (NegAtom (Atom x)) = (Lit.Neg x :) <$> xs
+      phi :: Maybe [Literal] -> Neg -> Maybe [Literal]
+      phi xs (OfAtom (Atom x)) = (Positive x :) <$> xs
+      phi xs (NegAtom (Atom x)) = (Negative x :) <$> xs
       phi _ Neg{} = Nothing
       phi _ OfNested{} = Nothing
   fromGrammar _ = Nothing
@@ -265,8 +264,8 @@ instance FromGrammar Cnf where
       go (WithPrecedence TopLevelBackImpl) = Nothing
       phi :: Maybe [Clause] -> Neg -> Maybe [Clause]
       phi xs (OfNested (Nested f)) = (:) <$> fromGrammar f  <*> xs
-      phi xs (OfAtom (Atom x)) = (mkClause [Lit.Pos x] :) <$> xs
-      phi xs (NegAtom (Atom x)) = (mkClause [Lit.Neg x] :) <$> xs
+      phi xs (OfAtom (Atom x)) = (mkClause [Positive x] :) <$> xs
+      phi xs (NegAtom (Atom x)) = (mkClause [Negative x] :) <$> xs
       phi _ Neg{} = Nothing
 
 instance Parse Dnf
@@ -281,8 +280,8 @@ instance FromGrammar Dnf where
     where
       phi :: Maybe [Con] -> Ands -> Maybe [Con]
       phi xs (NoAnds (OfNested (Nested x))) = (:) <$> fromGrammar x <*> xs
-      phi xs (NoAnds (OfAtom (Atom x))) = (mkCon [Lit.Pos x] :) <$> xs
-      phi xs (NoAnds (NegAtom (Atom x))) = (mkCon [Lit.Neg x] :) <$> xs
+      phi xs (NoAnds (OfAtom (Atom x))) = (mkCon [Positive x] :) <$> xs
+      phi xs (NoAnds (NegAtom (Atom x))) = (mkCon [Negative x] :) <$> xs
       phi _ (NoAnds Neg{}) = Nothing
       phi _ (Ands{}) = Nothing
 
diff --git a/src/Formula/Printing.hs b/src/Formula/Printing.hs
index e3ba8e50..c169712b 100644
--- a/src/Formula/Printing.hs
+++ b/src/Formula/Printing.hs
@@ -51,8 +51,8 @@ instance Pretty ResStep where
 
 
 instance Pretty Literal where
-   pretty (Pos x) = char x
-   pretty (Neg x) = myText ['¬', x]
+   pretty (Positive x) = char x
+   pretty (Negative x) = myText ['¬', x]
 
 
 
diff --git a/src/Formula/Resolution.hs b/src/Formula/Resolution.hs
index b26d289e..027086e8 100644
--- a/src/Formula/Resolution.hs
+++ b/src/Formula/Resolution.hs
@@ -53,7 +53,7 @@ resolvableWith c1 c2
     | length possible == 1 = Just (head possible)
     | otherwise = Nothing
   where
-    lits = map Pos $ atomics c1 -- TODO: Should `literals` be used here?
+    lits = map Positive $ atomics c1 -- TODO: Should `literals` be used here?
     possible = filter (isJust . resolve c1 c2) lits
 
 
@@ -100,8 +100,8 @@ genRes (minLen,maxLen) steps lits = do
               then do
                 chosenChar <- elements xs
                 let
-                  pos = Set.singleton $ Pos chosenChar
-                  neg = Set.singleton $ Neg chosenChar
+                  pos = Set.singleton $ Positive chosenChar
+                  neg = Set.singleton $ Negative chosenChar
                   startSet = Set.fromList [pos,neg]
                 buildClauses xs (startSet,[Res (Left (toClause pos),Left (toClause neg), (toClause empty,Nothing))]) 0
               else do
@@ -111,7 +111,7 @@ genRes (minLen,maxLen) steps lits = do
                 chosenClause <- setElements (if Set.null underMin then underMax else underMin)
                 let
                   chooseableLits = filter (\lit ->
-                    Pos lit `Set.notMember` chosenClause && Neg lit `Set.notMember` chosenClause) xs
+                    Positive lit `Set.notMember` chosenClause && Negative lit `Set.notMember` chosenClause) xs
                 if null chooseableLits
                     then buildClauses xs (ys,rs) (runs+1)
                     else do
@@ -124,10 +124,10 @@ genRes (minLen,maxLen) steps lits = do
                                 else choose (1,2)
                       chosenChar <- elements chooseableLits
                       if choice == 1
-                        then checkValidAndInsert (Pos chosenChar) chosenClause rs clauseSize 0
+                        then checkValidAndInsert (Positive chosenChar) chosenClause rs clauseSize 0
                         else do
                           firstAmount <- choose (1, clauseSize-1)
-                          chosenSign <- elements [Pos chosenChar, Neg chosenChar]
+                          chosenSign <- elements [Positive chosenChar, Negative chosenChar]
                           checkValidAndInsert chosenSign chosenClause rs firstAmount firstAmount
       where
         checkValidAndInsert :: Literal -> Set Literal -> [ResStep] -> Int -> Int -> Gen (Set (Set Literal),[ResStep])
diff --git a/src/Formula/Types.hs b/src/Formula/Types.hs
index 6857ab6c..6bc39e64 100644
--- a/src/Formula/Types.hs
+++ b/src/Formula/Types.hs
@@ -46,7 +46,7 @@ import Data.List(intercalate, delete, nub, transpose, (\\))
 import Data.Set (Set,empty)
 import Data.Typeable
 import GHC.Generics
-import Test.QuickCheck
+import Test.QuickCheck hiding (Positive,Negative)
 import Numeric.SpecFunctions as Math (choose)
 
 newtype ResStep = Res {trip :: (Either Clause Int, Either Clause Int, (Clause, Maybe Int))} deriving Show
@@ -82,8 +82,8 @@ queryClause = HornClause Query
 
 -- | A datatype representing a literal
 data Literal
-    = Pos { letter :: Char} -- ^ positive sign
-    | Neg { letter :: Char} -- ^ negative sign
+    = Positive { letter :: Char} -- ^ positive sign
+    | Negative { letter :: Char} -- ^ negative sign
     deriving
       ( Eq -- ^ derived
       , Typeable -- ^ derived
@@ -93,37 +93,37 @@ data Literal
 
 -- | order literals alphabetically first, then prefer a positive sign
 instance Ord Literal where
-   compare (Neg x) (Pos y) = if x == y then LT else compare x y
-   compare (Pos x) (Neg y) = if x == y then GT else compare x y
+   compare (Negative x) (Positive y) = if x == y then LT else compare x y
+   compare (Positive x) (Negative y) = if x == y then GT else compare x y
    compare l1 l2 = compare (letter l1) (letter l2)
 
 
 -- | '¬' denotes a negative sign
 instance Show Literal where
-   show (Pos x) = [x]
-   show (Neg x) = ['¬', x]
+   show (Positive x) = [x]
+   show (Negative x) = ['¬', x]
 
 
 instance Read Literal where
-   readsPrec _ ('¬':x:rest) = [(Neg x, rest) | x `elem` ['A' .. 'Z']]
-   readsPrec _ (x:rest) = [(Pos x, rest) | x `elem` ['A' .. 'Z']]
+   readsPrec _ ('¬':x:rest) = [(Negative x, rest) | x `elem` ['A' .. 'Z']]
+   readsPrec _ (x:rest) = [(Positive x, rest) | x `elem` ['A' .. 'Z']]
    readsPrec _ _ = []
 
 
 instance Formula Literal where
    literals lit = [lit]
 
-   atomics (Pos x) = [x]
-   atomics (Neg x) = [x]
+   atomics (Positive x) = [x]
+   atomics (Negative x) = [x]
 
    amount _ = 1
 
-   evaluate xs (Neg y) = not <$> evaluate xs (Pos y)
-   evaluate xs (Pos c) = lookup c xs
+   evaluate xs (Negative y) = not <$> evaluate xs (Positive y)
+   evaluate xs (Positive c) = lookup c xs
 
 instance ToSAT Literal where
-  convert (Pos c) = Sat.Var c
-  convert (Neg c) = Sat.Not (Sat.Var c)
+  convert (Positive c) = Sat.Var c
+  convert (Negative c) = Sat.Not (Sat.Var c)
 
 instance Arbitrary Literal where
    arbitrary = genLiteral ['A'..'Z']
@@ -135,13 +135,13 @@ genLiteral :: [Char] -> Gen Literal
 genLiteral [] = error "Cannot construct literal from empty list."
 genLiteral lits = do
    rChar <- elements lits
-   elements [Pos rChar, Neg rChar]
+   elements [Positive rChar, Negative rChar]
 
 
 -- | Reverses the sign of the literal
 opposite :: Literal -> Literal
-opposite (Pos l) = Neg l
-opposite (Neg l) = Pos l
+opposite (Positive l) = Negative l
+opposite (Negative l) = Positive l
 
 
 ------------------------------------------------------------
diff --git a/src/Formula/Util.hs b/src/Formula/Util.hs
index 766320c2..f5794f16 100644
--- a/src/Formula/Util.hs
+++ b/src/Formula/Util.hs
@@ -36,7 +36,7 @@ import Formula.Types
 
 -- | Is the input a positive literal?
 isPositive :: Literal -> Bool
-isPositive (Neg _) = False
+isPositive (Negative _) = False
 isPositive _ = True
 
 ---------------------------------------------------------------------------------------------------
@@ -96,11 +96,11 @@ hasEmptyCon (Dnf set) = Con Set.empty `Set.member` set
 ---------------------------------------------------------------------------------------------------
 
 replaceLiteral :: Char -> Literal -> Literal
-replaceLiteral c l@(Pos a)
-  | a == c = Neg c
+replaceLiteral c l@(Positive a)
+  | a == c = Negative c
   | otherwise = l
-replaceLiteral c l@(Neg a)
-  | a == c = Pos c
+replaceLiteral c l@(Negative a)
+  | a == c = Positive c
   | otherwise = l
 
 cnfDependsOnAllAtomics :: Cnf -> Bool
diff --git a/src/LogicTasks/Debug.hs b/src/LogicTasks/Debug.hs
index 7d32570b..c9cec194 100644
--- a/src/LogicTasks/Debug.hs
+++ b/src/LogicTasks/Debug.hs
@@ -10,7 +10,7 @@ module LogicTasks.Debug (
   Display(..), Language (..),
   ) where
 
-import Test.QuickCheck
+import Test.QuickCheck hiding (Positive, Negative)
 import Control.OutputCapable.Blocks.Generic
 import Control.OutputCapable.Blocks
 import Text.Parsec
@@ -55,10 +55,10 @@ analyseCnfGenerator gen = quickCheckWith stdArgs{maxSuccess=1000} $ forAll gen $
   tabulate "clause lengths" (map (show . size . literalSet) . toList $ clauseSet cnf) $
   tabulate "number of clauses" (pure . show . size $ clauseSet cnf) $
   tabulate "trivial clauses (containing both X and not X)" (map (show . isTrivial) . toList $ clauseSet cnf) $
-  tabulate "usage of atomic formulas" (pure . nubSort . map (\case (Pos x) -> x ; (Neg x) -> x) $ literals cnf)
+  tabulate "usage of atomic formulas" (pure . nubSort . map (\case (Positive x) -> x ; (Negative x) -> x) $ literals cnf)
     True
 
 isTrivial :: Clause -> Bool
 isTrivial x =
   let (pos,neg) = partition isPositive $ toList $ literalSet x
-  in any (\case (Pos a) -> Neg a `elem` neg; _ -> error "impossible") pos
+  in any (\case (Positive a) -> Negative a `elem` neg; _ -> error "impossible") pos
diff --git a/src/LogicTasks/Semantics/Max.hs b/src/LogicTasks/Semantics/Max.hs
index fba32500..792a85d9 100644
--- a/src/LogicTasks/Semantics/Max.hs
+++ b/src/LogicTasks/Semantics/Max.hs
@@ -64,7 +64,7 @@ description MaxInst{..} = do
   -- jscpd:ignore-start
   paragraph $ indent $ do
     translate $ do
-      let formulaStr = show $ mkCnf [mkClause [Pos 'A', Neg 'B'], mkClause [Neg 'C', Neg 'D']]
+      let formulaStr = show $ mkCnf [mkClause [Positive 'A', Negative 'B'], mkClause [Negative 'C', Negative 'D']]
       german $ unwords ["Ein Lösungsversuch für Formel", formulaStr, "könnte beispielsweise so aussehen: "]
       english $ unwords ["A solution attempt for the formula", formulaStr, "could look like this: "]
     translatedCode $ flip localise $ translations exampleCode
@@ -104,7 +104,7 @@ verifyQuiz MinMaxConfig{..} = do
 
 
 start :: Cnf
-start = mkCnf [mkClause [Pos 'A']]
+start = mkCnf [mkClause [Positive 'A']]
 
 
 
diff --git a/src/LogicTasks/Semantics/Min.hs b/src/LogicTasks/Semantics/Min.hs
index b2fd2bfe..ffb42e53 100644
--- a/src/LogicTasks/Semantics/Min.hs
+++ b/src/LogicTasks/Semantics/Min.hs
@@ -62,7 +62,7 @@ description MinInst{..} = do
 
   paragraph $ indent $ do
     translate $ do
-      let formulaStr = show $ mkDnf [mkCon [Pos 'A', Neg 'B'], mkCon [Neg 'C', Neg 'D']]
+      let formulaStr = show $ mkDnf [mkCon [Positive 'A', Negative 'B'], mkCon [Negative 'C', Negative 'D']]
       german $ unwords ["Ein Lösungsversuch für Formel", formulaStr, "könnte beispielsweise so aussehen: "]
       english $ unwords ["A solution attempt for the formula", formulaStr, "could look like this: "]
     translatedCode $ flip localise $ translations exampleCode
@@ -96,7 +96,7 @@ verifyQuiz = Max.verifyQuiz
 
 
 start :: Dnf
-start = mkDnf [mkCon [Pos 'A']]
+start = mkDnf [mkCon [Positive 'A']]
 
 partialGrade :: OutputCapable m => MinInst -> Delayed Dnf -> LangM m
 partialGrade inst = (partialGrade' inst `withDelayed` parser) displayParseError
diff --git a/src/LogicTasks/Semantics/Prolog.hs b/src/LogicTasks/Semantics/Prolog.hs
index 3b096f5b..33ef2c0a 100644
--- a/src/LogicTasks/Semantics/Prolog.hs
+++ b/src/LogicTasks/Semantics/Prolog.hs
@@ -250,9 +250,9 @@ transform (pc1,pc2) = (clause1, clause2, applyPol)
 
     polLookup p = (p,lit)
       where lit = case lookup p mapping of
-                    Just l1  -> Pos l1
+                    Just l1  -> Positive l1
                     Nothing  -> case lookup (flipPol p) mapping of
-                                  Just l2 -> Neg l2
+                                  Just l2 -> Negative l2
                                   Nothing -> error "each literal should have a mapping."
 
     applyPol = map polLookup allPredicates
diff --git a/src/LogicTasks/Semantics/Step.hs b/src/LogicTasks/Semantics/Step.hs
index 4c5e5445..d0122589 100644
--- a/src/LogicTasks/Semantics/Step.hs
+++ b/src/LogicTasks/Semantics/Step.hs
@@ -238,7 +238,7 @@ completeGrade' StepInst{..} sol =
 genResStepClause :: Int -> Int -> [Char] -> Gen (Clause, Literal, [Literal])
 genResStepClause minClauseLength maxClauseLength usedAtoms = do
     rChar <- elements usedAtoms
-    resolveLit <- elements [Pos rChar, Neg rChar]
+    resolveLit <- elements [Positive rChar, Negative rChar]
     let
       restLits = delete rChar usedAtoms
     minLen1 <- elements [minClauseLength-1..maxClauseLength-1]
diff --git a/src/Trees/Formula.hs b/src/Trees/Formula.hs
index 72ed7e98..1e90705b 100644
--- a/src/Trees/Formula.hs
+++ b/src/Trees/Formula.hs
@@ -1,16 +1,15 @@
 {-# LANGUAGE FlexibleInstances #-}
 {-# OPTIONS_GHC -Wno-orphans #-}
 module Trees.Formula where
-import Formula.Types (Formula(..))
+import Formula.Types (Formula(..), Literal(..))
 import Trees.Types (SynTree(..), BinOp(..))
-import qualified Formula.Types as F (Literal(..))
 import Data.List (find)
 import Data.List.Extra (nubSort)
 import Trees.Helpers (collectLeaves, treeNodes)
 
 instance Formula (SynTree BinOp Char) where
-  literals (Leaf x) = [F.Pos x]
-  literals (Not (Leaf x)) = [F.Neg x]
+  literals (Leaf x) = [Positive x]
+  literals (Not (Leaf x)) = [Negative x]
   literals (Not x) = literals x
   literals (Binary _ l r) = nubSort $ literals l ++ literals r
 
diff --git a/src/Trees/Helpers.hs b/src/Trees/Helpers.hs
index bd59e634..6f0100e6 100644
--- a/src/Trees/Helpers.hs
+++ b/src/Trees/Helpers.hs
@@ -150,8 +150,8 @@ conToSynTree :: SetFormulaDnf.Con -> SynTree BinOp Char
 conToSynTree = foldr1 (Binary And) . map literalToSynTree . toList . SetFormulaDnf.literalSet
 
 literalToSynTree :: SetFormula.Literal -> SynTree o Char
-literalToSynTree (SetFormula.Pos a) = Leaf a
-literalToSynTree (SetFormula.Neg a) = Not (Leaf a)
+literalToSynTree (SetFormula.Positive a) = Leaf a
+literalToSynTree (SetFormula.Negative a) = Not (Leaf a)
 
 
 numOfOps :: SynTree o c -> Integer
diff --git a/test/ParsingSpec.hs b/test/ParsingSpec.hs
index 4696f61b..4c4025c9 100644
--- a/test/ParsingSpec.hs
+++ b/test/ParsingSpec.hs
@@ -48,7 +48,7 @@ spec = do
     it "correctly parses the pretty representation of a PickInst (cnf)" $
       either (const False) (== dPickInst) $ parse (parser @PickInst) "" $ show $ pretty dPickInst
     it "correctly parses the pretty representation of a PickInst (dnf)" $
-      let pickInst = dPickInst { formulas = [InstDnf (mkDnf [mkCon [Pos 'A', Neg 'B']])] } in
+      let pickInst = dPickInst { formulas = [InstDnf (mkDnf [mkCon [Positive 'A', Negative 'B']])] } in
         either (const False) (== pickInst) $ parse (parser @PickInst) "" $ show $ pretty pickInst
     it "correctly parses the pretty representation of a PickInst (arbitrary)" $
       let pickInst = dPickInst { formulas = [InstArbitrary (TT.Binary TT.And (TT.Leaf 'A') (TT.Not (TT.Leaf 'B')))] } in
diff --git a/test/ResolutionSpec.hs b/test/ResolutionSpec.hs
index 4996d4c2..b0221f5d 100644
--- a/test/ResolutionSpec.hs
+++ b/test/ResolutionSpec.hs
@@ -15,19 +15,19 @@ import Control.OutputCapable.Blocks.Generic (evalLangM)
 import FillSpec (validBoundsBase)
 
 justA :: Clause
-justA = Clause (Data.Set.fromList [Pos 'A'])
+justA = Clause (Data.Set.fromList [Positive 'A'])
 
 notAnotB :: Clause
-notAnotB = Clause (Data.Set.fromList [Neg 'A', Neg 'B'])
+notAnotB = Clause (Data.Set.fromList [Negative 'A', Negative 'B'])
 
 notAjustB :: Clause
-notAjustB = Clause (Data.Set.fromList [Neg 'A', Pos 'B'])
+notAjustB = Clause (Data.Set.fromList [Negative 'A', Positive 'B'])
 
 notB :: Clause
-notB = Clause (Data.Set.fromList [Neg 'B'])
+notB = Clause (Data.Set.fromList [Negative 'B'])
 
 justB :: Clause
-justB = Clause (Data.Set.fromList [Pos 'B'])
+justB = Clause (Data.Set.fromList [Positive 'B'])
 
 emptyClause :: Clause
 emptyClause = Clause Data.Set.empty
@@ -54,7 +54,7 @@ spec = do
     it "should return a Just value if there are no clauses" $
       isJust $ applySteps [] []
     it "should return the original list of clauses if there are no steps to apply" $ do
-      let clauses = [Clause (Data.Set.fromList [Pos 'A'])]
+      let clauses = [Clause (Data.Set.fromList [Positive 'A'])]
       fromJust (applySteps clauses []) == clauses
     it "should return the correct list of clauses if the steps are able to be applied" $ do
       let clauses = [justA, notAnotB, notAjustB]