Closed owestphal closed 8 months ago
I'm wondering whether in some context the possibility of choosing ""
in the last line here: https://github.com/fmidue/logic-tasks/blob/9b4185921c716268b7e74f5d02fcb7693d1e3d3c/src/Tasks/LegalProposition/PrintIllegal.hs#L87-L89 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?
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 ∧)
.
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. :smile:
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:
"_"
instead of ""
in.implementIllegal
-call that exists (from ifUseIllegal
) by something like replace " _" "" . replace "_ " ""
(using Data.List.Extra.replace
). 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?
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 Char
s are Unicode and hence not encoded/encodeable as "single ASCII bytes" or whatnot?
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.
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.
Teilweise entstehen auffällig große Lücken in (illegalen) Formeln: