Search code examples
haskellgeneratorquickcheck

quickCheck propositional logic generator


So I have this quickCheck propositional logic generator:

instance Arbitrary Form where
   arbitrary = genForm

genForm = sized genForm'
genForm' 0 = fmap Prop (choose (1,15))
genForm' n | n > 15 = genForm' (n `div` 2)
genForm' n | n > 0 =
          oneof [fmap Prop (choose (1,15)),
                 fmap Neg subform,
                 fmap Cnj subforms,
                 fmap Dsj subforms,
                 liftM2 Impl subform subform,
                 liftM2 Equiv subform subform]
          where subform = genForm' (n `div` 2)
                subforms = resize (n `div` 2) (vector (n `div` 2))

The datatype is defined as follows:

type Name = Int

data Form = Prop Name
          | Neg  Form
          | Cnj [Form]
          | Dsj [Form]
          | Impl Form Form
          | Equiv Form Form
          deriving (Eq,Ord)

The problem is this generator will generate in the form of: +[] (a disjunction of nothing). I don't want my operators to have no nested Prop member as it makes invalid propositional formulas. I want to make sure that there is no option to not have a Prop member at the end.

My thought is that this problem comes from the resize (div n 2). When n is even this will eventually hit 0 and not go further on generating and thus create a empty member. Removing the resize won't help because it then won't generate a ending 'tree'. So it seems to be needed but should be tweaked in some way.

But I'm not great at Haskell and I'm having difficulty debugging/reading the documentation.


Solution

  • Apply vector to a non-zero argument:

    subforms = resize (n `div` 2) (vector (1 + (n `div` 2)))
    

    Or use listOf1 arbitrary instead of vector

    subforms = resize (n `div` 2) (listOf1 arbitrary)
    

    From a follow-up comment:

    even need the generated amount to be at least >2

    Apply vector to a length >= 2:

    subforms = resize (n `div` 2) (vector (2 + (n `div` 2)))
    

    Or append two elements in front explicitly (using listOf to allow the length to also vary):

    subforms = resize (n `div` 2) (listOf2 arbitrary)
      where
        listOf2 :: Gen a -> Gen [a]
        listOf2 gen = liftA2 (:) gen (liftA2 (:) gen (listOf gen))
        -- 1. (listOf gen) to generate a list
        -- 2. Call gen twice to generate two more elements
        -- 3. Append everything together with `(:)`