Hello! I’m trying to develop an analyrtic tableaux prover with Haskell and I want to test it with PBT using quickcheck.
I never used quickcheck and I have this data constructors:
data InputMetadata = InputMetadata
{ metadataLine :: Int
, metadataColumn :: Int
}
deriving (Show)
data Operator
= Not Char
| And Char
| Or Char
| Implies Char
| Equiv Char
| Prove Char
deriving (Show)
data Sign = T | F deriving (Show, Enum)
data TableauxInput
= TableauxAtom InputMetadata Text
| TableauxSign InputMetadata Sign
| TableauxOperator InputMetadata Operator
| TableauxWff InputMetadata [TableauxInput]
deriving (Show)
and this is my test file for now:
module Language.Tableaux.ParserSpec where
import Data.Text (singleton)
import Test.Hspec
import Test.Hspec.Parsec
import Test.Hspec.QuickCheck
import Test.QuickCheck
import Test.QuickCheck.Unicode
import Text.Parsec (parse)
import Language.Tableaux.Parser
instance Arbitrary Sign where
arbitrary = chooseEnum (T, F)
instance Arbitrary Operator where
arbitrary = intToOp <$> choose (1, 6)
instance Arbitrary TableauxInput where
arbitrary = intToTableaux <$> choose (1, 4)
main :: Spec
main = undefined
intToOp 1 = Not <$> elements "¬~!"
intToOp 2 = And <$> elements "∧&·"
intToOp 3 = Or <$> elements "∨+∥"
intToOp 4 = Implies <$> elements "⇒→⊃"
intToOp 5 = Equiv <$> elements "⇔≡↔"
intToOp 6 = Prove <$> elements "⊢"
intToTableaux 1 = TableauxAtom <$> inputMetadata <*> letter
intToTableaux 2 = TableauxSign <$> inputMetadata <*> arbitrary
intToTableaux 3 = TableauxOperator <$> inputMetadata <*> arbitrary
intToTableaux 4 = TableauxWff <$> inputMetadata <*> arbitrary
letter = frequency [(26, choose ('a', 'z'))]
inputMetadata = InputMetadata <$> arbitrary <*> arbitrary
however Iḿ having these errors:
/ParserSpec.hs:19:15: error:
• Couldn't match type ‘Gen Operator’ with ‘Operator’
Expected type: Gen Operator
Actual type: Gen (Gen Operator)
• In the expression: intToOp <$> choose (1, 6)
In an equation for ‘arbitrary’:
arbitrary = intToOp <$> choose (1, 6)
In the instance declaration for ‘Arbitrary Operator’
|
19 | arbitrary = intToOp <$> choose (1, 6)
| ^^^^^^^^^^^^^^^^^^^^^^^^^
/ParserSpec.hs:22:15: error:
• Couldn't match type ‘Gen TableauxInput’ with ‘TableauxInput’
Expected type: Gen TableauxInput
Actual type: Gen (Gen TableauxInput)
• In the expression: intToTableaux <$> choose (1, 4)
In an equation for ‘arbitrary’:
arbitrary = intToTableaux <$> choose (1, 4)
In the instance declaration for ‘Arbitrary TableauxInput’
|
22 | arbitrary = intToTableaux <$> choose (1, 4)
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^