Formula type refactoring

[nimec01]

Closes #248

This also includes the change from "literals" to "atomics" at the Table type (there might be an overlap with #239 here).
Some tasks need to be adapted on the Autotool-side after this gets merged.

One thing I'm not sure about is the usage of atomics here: https://github.com/nimec01/logic-tasks/blob/e57f1cd58cbc39c649fd50618ebbc192997be86b/src/Formula/Resolution.hs#L50-L57

There also might be more renaming to consider since there are still name overlaps in UniversalParser, Formula.Types (and potentially Trees.Types).

Example: Neg-Constructor of Literal and Neg-Constructor of Neg (at UniversalParser)

[jvoigtlaender]

The merge of master above includes #239, so maybe this part of the initial comment above is now obsolete:

there might be an overlap with #239 here

[nimec01]

Example: Neg-Constructor of Literal and Neg-Constructor of Neg (at UniversalParser)

This exact case could also be resolved by changing the new constructor names to:

data Literal
    = Positive { letter :: Char} -- ^ positive sign
    | Negative { letter :: Char} -- ^ negative sign

instead of

data Literal
    = Pos { letter :: Char} -- ^ positive sign
    | Neg { letter :: Char} -- ^ negative sign

[jvoigtlaender]

Does this also still warrant some action here?

logic-tasks/src/Formula/Util.hs

Lines 42 to 45 in b453da2

	-- | 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"

[jvoigtlaender]

And yes, Positive and Negative seems fine.

[jvoigtlaender]

About this part:

One thing I'm not sure about is the usage of atomics here: https://github.com/nimec01/logic-tasks/blob/e57f1cd58cbc39c649fd50618ebbc192997be86b/src/Formula/Resolution.hs#L50-L57

Where does the uncertainty come from? That piece of code seems to be semantically equivalent to what it was before. Do you suspect there was a semantic error so far?

[jvoigtlaender]

What appears from looking through the code here is also that there seem to be further cases in the code where "literal" vs. "atom" is confused, not caught by #239 (maybe because the code search there was for "literal" rather than also possible variations of it).

For example, in here:

logic-tasks/src/LogicTasks/Semantics/Min.hs

Lines 104 to 108 in e7a0424

	partialGrade' :: OutputCapable m => MinInst -> Dnf -> LangM m
	partialGrade' MinInst{..} sol = Max.partialMinMax corLits dnf sol allMinTerms False
	where
	corLits = atomics dnf
	allMinTerms = not $ all (\c -> amount c == length corLits) $ getConjunctions sol

I guess corLits should be correctAtoms.

And here:

logic-tasks/src/Formula/Types.hs

Lines 597 to 607 in e7a0424

	genForNF :: (Int,Int) -> (Int,Int) -> [Char] -> Gen (Int, [Char])
	genForNF (minNum,maxNum) (minLen,maxLen) lits
	| null nLits || invalidLen || invalidNum = pure (0, [])
	| otherwise = do
	num <- chooseInt (minNum, min maxNum upperBound)
	pure (num, nLits)
	where
	nLits = nub lits
	invalidLen = minLen <= 0 || minLen > maxLen || minLen > length nLits
	invalidNum = minNum <= 0 || minNum > maxNum || minNum > upperBound
	upperBound = lengthBound (length nLits) maxLen

(and also in uses of this function) the "lits" are really "atoms"?

[nimec01]

About this part:

One thing I'm not sure about is the usage of atomics here: https://github.com/nimec01/logic-tasks/blob/e57f1cd58cbc39c649fd50618ebbc192997be86b/src/Formula/Resolution.hs#L50-L57

Where does the uncertainty come from? That piece of code seems to be semantically equivalent to what it was before. Do you suspect there was a semantic error so far?

I was wondering if a simple literals call would work here. Thelits variable could then of course include elements using the Negative constructor, but would this be a problem? (I have not really looked into the code behind the Resolution task)

[nimec01]

What appears from looking through the code here is also that there seem to be further cases in the code where "literal" vs. "atom" is confused, not caught by #239 (maybe because the code search there was for "literal" rather than also possible variations of it).

For example, in here:

logic-tasks/src/LogicTasks/Semantics/Min.hs

Lines 104 to 108 in e7a0424

	partialGrade' :: OutputCapable m => MinInst -> Dnf -> LangM m
	partialGrade' MinInst{..} sol = Max.partialMinMax corLits dnf sol allMinTerms False
	where
	corLits = atomics dnf
	allMinTerms = not $ all (\c -> amount c == length corLits) $ getConjunctions sol

I guess corLits should be correctAtoms.
And here:

logic-tasks/src/Formula/Types.hs

Lines 597 to 607 in e7a0424

	genForNF :: (Int,Int) -> (Int,Int) -> [Char] -> Gen (Int, [Char])
	genForNF (minNum,maxNum) (minLen,maxLen) lits
	| null nLits || invalidLen || invalidNum = pure (0, [])
	| otherwise = do
	num <- chooseInt (minNum, min maxNum upperBound)
	pure (num, nLits)
	where
	nLits = nub lits
	invalidLen = minLen <= 0 || minLen > maxLen || minLen > length nLits
	invalidNum = minNum <= 0 || minNum > maxNum || minNum > upperBound
	upperBound = lengthBound (length nLits) maxLen

(and also in uses of this function) the "lits" are really "atoms"?

I will address this in a separate pull request.

[jvoigtlaender]

Thelits variable could then of course include elements using the Negative constructor, but would this be a problem? (I have not really looked into the code behind the Resolution task)

I'll merge this PR here, then open a separate issue related to that point. There is actually a subtlety about the implementation of resolution I was not aware of before.