Testen mit zufälligen Konfigurationen bei Prolog

src/LogicTasks/Semantics/Prolog.hs

@@ -21,7 +21,7 @@ import Data.Tuple (swap)
 import Test.QuickCheck (Gen, suchThat)
 
 import Config (PrologConfig(..), PrologInst(..))
-import Formula.Types (Clause, Literal(..), PrologLiteral(..), PrologClause(..), literals, opposite, ClauseShape (HornClause), HornShape (Fact, Query), terms)
+import Formula.Types (Clause, Literal(..), PrologLiteral(..), PrologClause(..), literals, opposite, ClauseShape (HornClause), HornShape (Fact, Query), terms, factClause, procedureClause)
 import Formula.Util (flipPol, isEmptyClause, isPositive, mkPrologClause, transformProlog)
 import Formula.Resolution (resolvable, resolve)
 import LogicTasks.Semantics.Step (genResStepClause)
@@ -148,6 +148,19 @@ verifyQuiz PrologConfig{..}
           german "Es wurden keine Literale angegeben."
           english "You did not specify which literals should be used."
 
+    | factClause `elem` [firstClauseShape, secondClauseShape] && minClauseLength > 1 =
+         refuse $ indent $ translate $ do
+           german "Die Klauselform 'Fakt' hat immer Länge 1. "
+           german "Das 'minClauseLength'-Parameter muss verringert werden."
+           english "A 'fact' clause always has length 1. "
+           english "Adjust the 'minClauseLength' parameter accordingly."
+     | procedureClause `elem` [firstClauseShape, secondClauseShape] && maxClauseLength < 2 =
+         refuse $ indent $ translate $ do
+           german "Die Klauselform 'Regel' hat mindestens Länge 2. "
+           german "Das 'maxClauseLength'-Parameter muss erhöht werden."
+           english "A 'procedure' clause always has at least length 2. "
+           english "Adjust the 'maxClauseLength' parameter accordingly."
+
     | (firstClauseShape `elem` [HornClause Fact, HornClause Query]) && firstClauseShape == secondClauseShape =
         refuse $ indent $ translate $ do
           german "Mit diesen Klauselformen ist keine Resolution möglich."

test/PrologSpec.hs

@@ -1,4 +1,5 @@
 {-# LANGUAGE RecordWildCards #-}
+{-# LANGUAGE NamedFieldPuns #-}
 module PrologSpec where
 import Test.Hspec
 import LogicTasks.Semantics.Prolog (genPrologInst, verifyQuiz, description, verifyStatic, partialGrade', completeGrade')
@@ -7,27 +8,83 @@ import Formula.Helpers (hasTheClauseShape)
 import Test.QuickCheck
 import Control.OutputCapable.Blocks (LangM)
 import TestHelpers (doesNotRefuse)
+import Formula.Types (PrologLiteral (..), ClauseShape (..), HornShape (..))
+import Data.List (singleton)
 
 
+validBoundsClauseShape :: Gen ClauseShape
+validBoundsClauseShape = oneof
+  [ pure AnyClause
+  , pure $ HornClause AnyHornClause
+  , pure $ HornClause Fact
+  , pure $ HornClause Procedure
+  , pure $ HornClause Query
+  ]
+
+validBoundsPrologLiteral :: Gen PrologLiteral
+validBoundsPrologLiteral = do
+  polarity <- elements [True, False]
+  name <- singleton <$> elements "fghijklmn" -- no-spell-check
+  constantAmount <- choose (1,5)
+  constants <- vectorOf constantAmount (singleton <$> elements "abcdeuvwxyz") -- no-spell-check
+
+  return $ PrologLiteral
+    { polarity
+    , name
+    , constants
+    }
+
+
+validBoundsPrologConfig :: Gen PrologConfig
+validBoundsPrologConfig = do
+  minClauseLength <- choose (1, 5)
+  maxClauseLength <- choose (minClauseLength, 5)
+  predicateAmount <- choose (minClauseLength, maxClauseLength)
+  usedPredicates <- vectorOf predicateAmount validBoundsPrologLiteral
+  let clauseShape = validBoundsClauseShape `suchThat` shapeSuitsClauseBounds (minClauseLength, maxClauseLength)
+  (firstClauseShape, secondClauseShape) <- ((,) <$> clauseShape <*> clauseShape)
+    `suchThat` \(f,s) -> not ((f `elem` [HornClause Fact, HornClause Query]) && f == s)
+
+  return $ PrologConfig
+    { minClauseLength
+    , maxClauseLength
+    , usedPredicates
+    , extraText = Nothing
+    , printSolution = True
+    , firstClauseShape
+    , secondClauseShape
+    , useSetNotation = False
+    }
+  where
+    shapeSuitsClauseBounds (minB, _) (HornClause Fact) = minB == 1
+    shapeSuitsClauseBounds (_, maxB) (HornClause Procedure) = maxB >= 2
+    shapeSuitsClauseBounds _ _ = True
 
 spec :: Spec
 spec = do
   describe "config" $ do
     it "default config should pass config check" $
       doesNotRefuse (verifyQuiz dPrologConf :: LangM Maybe)
+    it "validBoundsPrologConfig should pass config check" $
+      forAll validBoundsPrologConfig $ \config ->
+          doesNotRefuse (verifyQuiz config :: LangM Maybe)
   describe "description" $ do
     it "should not reject" $
-      forAll (genPrologInst dPrologConf) $ \inst ->
-        doesNotRefuse (description inst :: LangM Maybe)
+      forAll validBoundsPrologConfig $ \config ->
+        forAll (genPrologInst config) $ \inst ->
+          doesNotRefuse (description inst :: LangM Maybe)
   describe "genPrologInst" $ do
     it "should pass verifyStatic" $
-      forAll (genPrologInst dPrologConf) $ \inst ->
-        doesNotRefuse (verifyStatic inst :: LangM Maybe)
+      forAll validBoundsPrologConfig $ \config ->
+        forAll (genPrologInst config) $ \inst ->
+          doesNotRefuse (verifyStatic inst :: LangM Maybe)
     it "should pass grading with correct answer" $
-      forAll (genPrologInst dPrologConf) $ \inst ->
-        doesNotRefuse (partialGrade' inst (solution inst) :: LangM Maybe) &&
-        doesNotRefuse (completeGrade' inst (solution inst) :: LangM Maybe)
+      forAll validBoundsPrologConfig $ \config ->
+        forAll (genPrologInst config) $ \inst ->
+          doesNotRefuse (partialGrade' inst (solution inst) :: LangM Maybe) &&
+          doesNotRefuse (completeGrade' inst (solution inst) :: LangM Maybe)
     it "should only generate PrologInst with horn clauses by default" $
-      forAll (genPrologInst dPrologConf) $ \PrologInst {..} ->
-        hasTheClauseShape (firstClauseShape dPrologConf) literals1
-          && hasTheClauseShape (secondClauseShape dPrologConf) literals2
+      forAll validBoundsPrologConfig $ \config ->
+        forAll (genPrologInst config) $ \PrologInst{..} ->
+          hasTheClauseShape (firstClauseShape dPrologConf) literals1
+            && hasTheClauseShape (secondClauseShape dPrologConf) literals2