logic-tasks/src/Tasks/LegalNormalForm/Quiz.hs at master · fmidue/logic-tasks · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE TupleSections #-}

module Tasks.LegalNormalForm.Quiz
  ( generateLegalCNFInst,
    generateLegalDNFInst,
  )
where

import Auxiliary (listNoDuplicate)
import Config (BaseConfig (..), NormalFormConfig (..))
import Data.List ((\\))
import Formula.Types (genCnf, genDnf)
import Tasks.LegalNormalForm.Config (LegalNormalFormConfig (..), LegalNormalFormInst (..), ErrorReason, TreeInfo(..))
import Tasks.LegalNormalForm.GenerateIllegal (genIllegalCnfSynTree, genIllegalDnfSynTree)
import Test.QuickCheck (Gen, chooseInt, elements, suchThat, vectorOf)
import Trees.Helpers (cnfToSynTree, dnfToSynTree)
import Trees.Print (simplestDisplay)
import Trees.Types (BinOp (..), SynTree (..))
import Data.Bifunctor (Bifunctor(second))

generateLegalCNFInst :: LegalNormalFormConfig -> Gen LegalNormalFormInst
generateLegalCNFInst = generateLegalNormalFormInst genCnf cnfToSynTree genIllegalCnfSynTree

generateLegalDNFInst :: LegalNormalFormConfig -> Gen LegalNormalFormInst
generateLegalDNFInst = generateLegalNormalFormInst genDnf dnfToSynTree genIllegalDnfSynTree

generateLegalNormalFormInst ::
  ((Int, Int) -> (Int, Int) -> [Char] -> Bool -> Gen a) ->
  (a -> SynTree BinOp Char) ->
  ((Int,Int) -> (Int,Int) -> [Char] -> Bool -> Gen (SynTree BinOp Char, ErrorReason)) ->
  LegalNormalFormConfig ->
  Gen LegalNormalFormInst
generateLegalNormalFormInst gen toSynTree genIllegal config@LegalNormalFormConfig {..} = do
  serialsOfWrong <- vectorOf illegals (chooseInt (1, formulas)) `suchThat` listNoDuplicate
  let serial1 = [1 .. formulas] \\ serialsOfWrong
  serialsOfJustOneClause <- vectorOf (if includeFormWithJustOneClause then 1 else 0) (elements serial1)
  let serial2 = serial1 \\ serialsOfJustOneClause
  serialsOfJustOneLiteralPerClause <-
    vectorOf
      (if includeFormWithJustOneLiteralPerClause then 1 else 0)
      (elements serial2)
  treeList <-
    genSynTreeList
      serialsOfWrong
      serialsOfJustOneClause
      serialsOfJustOneLiteralPerClause
      [1 .. formulas]
      config
      gen
      toSynTree
      genIllegal
      `suchThat` (listNoDuplicate . map ((simplestDisplay . fmap (const '_')) . fst))
  return $
    LegalNormalFormInst
      { formulaInfos = zipWith (curry (\(i,(sd,info)) -> (i, info, simplestDisplay sd))) [1..] treeList ,
        showSolution = printDetailedSolution,
        addText = extraText
      }

genSynTreeList ::
  [Int] ->
  [Int] ->
  [Int] ->
  [Int] ->
  LegalNormalFormConfig ->
  ((Int, Int) -> (Int, Int) -> [Char] -> Bool -> Gen a) ->
  (a -> SynTree BinOp Char) ->
  ((Int,Int) -> (Int,Int) -> [Char] -> Bool -> Gen (SynTree BinOp Char, ErrorReason)) ->
  Gen [(SynTree BinOp Char, TreeInfo)]
genSynTreeList
  serialsOfWrong
  serialsOfJustOneClause
  serialsOfJustOneLiteralPerClause
  formulasList
  config@LegalNormalFormConfig {..}
  gen
  toSynTree
  genIllegal =
    mapM
      ( \serial ->
          genSynTreeWithSerial
            serialsOfWrong
            serialsOfJustOneClause
            serialsOfJustOneLiteralPerClause
            config
            serial
            gen
            toSynTree
            genIllegal
            `suchThat` (checkSize minStringSize maxStringSize . fst)
      )
      formulasList

genSynTreeWithSerial ::
  [Int] ->
  [Int] ->
  [Int] ->
  LegalNormalFormConfig ->
  Int ->
  ((Int, Int) -> (Int, Int) -> [Char] -> Bool -> Gen a) ->
  (a -> SynTree BinOp Char) ->
  ((Int,Int) -> (Int,Int) -> [Char] -> Bool -> Gen (SynTree BinOp Char, ErrorReason)) ->
  Gen (SynTree BinOp Char, TreeInfo)
genSynTreeWithSerial
  serialsOfWrong
  serialsOfJustOneClause
  serialsOfJustOneLiteralPerClause
  LegalNormalFormConfig {normalFormConfig = NormalFormConfig {baseConf = BaseConfig {..}, ..}, ..}
  serial
  gen
  toSynTree
  genIllegal
    | serial `elem` serialsOfWrong =
        second Erroneous <$> genIllegal
          (minClauseAmount, maxClauseAmount)
          (minClauseLength, maxClauseLength)
          usedAtoms
          allowArrowOperators
    | serial `elem` serialsOfJustOneClause =
        (,CorrectSingleClause) . toSynTree
          <$> gen (1, 1) (minClauseLength, maxClauseLength) usedAtoms False
    | serial `elem` serialsOfJustOneLiteralPerClause =
        (,CorrectAtomicClauses) . toSynTree
          <$> gen (minClauseAmount, maxClauseAmount) (1, 1) usedAtoms False
    | otherwise =
        (,Correct) . toSynTree
          <$> gen
            (minClauseAmount, maxClauseAmount)
            (minClauseLength, maxClauseLength)
            usedAtoms
            False

checkSize :: Int -> Int -> SynTree BinOp Char -> Bool
checkSize minStringSize maxStringSize synTree =
  let stringLength = length (simplestDisplay synTree)
   in stringLength <= maxStringSize && stringLength >= minStringSize