diff --git a/src/LogicTasks/Semantics/Prolog.hs b/src/LogicTasks/Semantics/Prolog.hs index 33ef2c0a..4a75da33 100644 --- a/src/LogicTasks/Semantics/Prolog.hs +++ b/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." diff --git a/test/PrologSpec.hs b/test/PrologSpec.hs index 16320adb..2538b9b4 100644 --- a/test/PrologSpec.hs +++ b/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