String Formatierung

[owestphal]

Teilweise entstehen auffällig große Lücken in (illegalen) Formeln:

[jvoigtlaender]

I'm wondering whether in some context the possibility of choosing "" in the last line here:

logic-tasks/src/Tasks/LegalProposition/PrintIllegal.hs

Lines 87 to 89 in 9b41859

	implementIllegal _ (Leaf _) _ = do
	operator <- elements (showOperatorNot : map showOperator allBinaryOperators)
	elements [operator,""]

might also lead to a situation with "too many spaces".

@nimec01, can you try to trace under what conditions that "" can be used and what an example tree and corresponding output would look like?

[nimec01]

I don't really get what you mean by "under what conditions that "" can be used", but here are some results from my tests.
I replaced "" with "_" to see where "" would be used. The generation of some LegalPropositionInst then lead to these formulae:

• _ ∧ ¬(B ∨ C)
• (C ∨ ¬E) ∧ (B ∧ _)
• (B ∧ ¬C) ∧ _
• (¬A ∨ ¬(C ∧ C)) ∨ _
• ¬((¬(_ ∧ A) ∧ C) ∧ B)

This shows me that there shouldn't be any problems regarding "too many spaces". This would only be the case if (C ∨ ¬E) ∧ (B ∧ ) was meant to be displayed as (C ∨ ¬E) ∧ (B ∧).

[jvoigtlaender]

I meant exactly what you did: Finding out which situations/call paths actually reach that one occurrence of "". Doing that by simply replacing it with "_" and using randomized generation was a clever way of tracing it. 😄

About the subject matter: Indeed I think it would be better to display (C ∨ ¬E) ∧ (B ∧) instead of (C ∨ ¬E) ∧ (B ∧ ). The latter seems too much of a "visual tell" as regards the "there's something missing here".

As to how to make that reduction happen: It's probably not worth it to refactor all the code and try to avoid generating that adjacent space there in the first place. Instead, the following strategy/hack should work:

• Leave your "_" instead of "" in.
• Wrap the single implementIllegal-call that exists (from ifUseIllegal) by something like replace " _" "" . replace "_ " "" (using Data.List.Extra.replace).

[nimec01]

ifUseIllegal :: Bool -> Bool -> SynTree BinOp Char -> String -> Gen String
ifUseIllegal useBug notFirstLayer synTree usedLiterals =
    let
      nodeNum = treeNodes synTree
      replace' a b = fmap (replace a b)
    in
      if not useBug
        then return (normalShow synTree)
        else frequency
          [ (1, replace' "_ " "" (replace' " _" "" (implementIllegal notFirstLayer synTree usedLiterals)))
          , (fromIntegral nodeNum - 1, subTreeIllegal notFirstLayer synTree usedLiterals)
          ]

This change should allow me to replace " _" with "". However, (C ∨ ¬E) ∧ (B ∧ _) remains the same.

If I go ahead and change " _" to "_" in line 10 then (C ∨ ¬E) ∧ (B ∧ _) will be changed to (C ∨ ¬E) ∧ (B ∧ ). I don't know why this is the case. Am I missing something?

[jvoigtlaender]

Sounds strange. Maybe some kind of side effect of using Unicode for displaying ∧? In the sense that Data.List.Extra.replace doesn't work correctly with the view of String as [Char] when the Chars are Unicode and hence not encoded/encodeable as "single ASCII bytes" or whatnot?

[nimec01]

I did some more testing and found out that you apparently cannot change a value encapsulated in a Gen.
It works fine when I run the replacements after these formulas have been generated (i.e. they are of type String instead of Gen String).

implementIllegal :: Bool -> SynTree BinOp Char -> String -> Gen String
implementIllegal notFirstLayer (Binary operator a b) usedLiterals =
    illegalShow notFirstLayer a b usedLiterals operator
implementIllegal _ (Not a) usedLiterals = do
    letter <- elements usedLiterals
    elements  $ map (++ (' ' : normalShow a)) ([letter] : map showOperator allBinaryOperators)
implementIllegal _ (Leaf _) _ = do
    operator <- elements (showOperatorNot : map showOperator allBinaryOperators)
    elements [operator,"_"]

generateLegalPropositionInst :: LegalPropositionConfig -> Gen LegalPropositionInst
generateLegalPropositionInst LegalPropositionConfig  {syntaxTreeConfig = SynTreeConfig {..}, ..} = do
    treeList <- vectorOf
        (fromIntegral formulas)
        (genSynTree (minNodes, maxNodes)
          maxDepth
          usedLiterals
          atLeastOccurring
          allowArrowOperators
          maxConsecutiveNegations
          minUniqueBinOperators
        )
      `suchThat` (not . similarExist)
    serialsOfWrong <- vectorOf (fromIntegral illegals) (choose (1, fromIntegral formulas) )`suchThat` listNoDuplicate
    serialsOfBracket <- vectorOf
        (fromIntegral bracketFormulas)
        (choose (1, fromIntegral formulas))
      `suchThat` (listNoDuplicate . (++ serialsOfWrong))
    pseudoFormulas <- genPseudoList serialsOfWrong serialsOfBracket treeList `suchThat` noSimilarFormulas
    return $ LegalPropositionInst
        { serialsOfWrong = fromList serialsOfWrong
        , pseudoFormulas = map replaceUnderscores pseudoFormulas
        , correctTrees = [ tree | (index, tree) <- zip [1..] treeList, index `notElem` serialsOfWrong ]
        , showSolution = printSolution
        , addText = extraText
        }
          where replaceUnderscores = DLE.replace "_ " "" . DLE.replace " _" ""

Betrachten Sie die folgenden aussagenlogischen (Pseudo-)Formeln:
>>>> <1. ¬¬((¬A ∧) ∧ B)
2. ¬((C ∨ A) ∧ =>)
3. ¬((A ∨ ¬¬C) ∨ B)
4. ¬¬((B ∨ A) ∧ E) ∨ (C)
5. ¬(¬¬C ∨ A) ∧ ¬B
> <<<<
[...]

The first formula here would have included a " _" right before the first closing bracket.

[jvoigtlaender]

I don't think the problem can be String vs. Gen String here.

Rather, my suggested place of adding the replacing to ifUseIllegal was "too close to the recursion base". At that point, the '_' hasn't yet had a chance to meet a ' '. That only happens when at non-leaf nodes the subformulas are combined. Hence, the replacing shouldn't happen at ifUseIllegal, but rather at illegalDisplay.

I'll comment further in #114.