nick8325 / quickspec

Equational laws for free
BSD 3-Clause "New" or "Revised" License
247 stars 24 forks source link

QS duplicates laws #49

Open isovector opened 4 years ago

isovector commented 4 years ago

I'm not sure what's happening, but QS will spit out the following laws:

 49. negative (both x (choose x y)) = negative x
 50. negative (both x (choose x y)) = negative x
 51. negative (both x (choose x y)) = negative x
 52. negative (both x (choose x y)) = negative x
 53. negative (both x (choose x y)) = negative x
 54. negative (both x (choose x y)) = negative x

however, uncommenting the following parts of the signature prevent this from occurring:

  -- -- UNCOMMENT ME
  -- , con "failMatch" $ failMatch @Bool3
  -- , con "optional"  $ optional  @Bool3

???

isovector commented 4 years ago

repro:

{-# LANGUAGE DeriveDataTypeable                   #-}
{-# LANGUAGE DeriveGeneric                        #-}
{-# LANGUAGE FlexibleInstances                    #-}
{-# LANGUAGE MultiParamTypeClasses                #-}
{-# LANGUAGE NumDecimals                          #-}
{-# LANGUAGE PatternSynonyms                      #-}
{-# LANGUAGE ScopedTypeVariables                  #-}
{-# LANGUAGE TupleSections                        #-}
{-# LANGUAGE TypeApplications                     #-}
{-# LANGUAGE TypeSynonymInstances                 #-}
{-# OPTIONS_GHC -Wall                             #-}
{-# OPTIONS_GHC -fno-warn-incomplete-uni-patterns #-}

module Lib where

import           Control.Arrow
import           Control.Monad
import           Data.Bool
import           Data.Data
import           Data.Either
import           Data.List
import           Data.Ord
import           Data.Tuple
import           GHC.Generics
import           QuickSpec
import qualified Test.QuickCheck as QC
import           Test.QuickCheck hiding (oneof, choose, Negative (..))

data Regex a
  = Char a
  | Empty
  | AnyChar
  | Fail
  | Cat (Regex a) (Regex a)
  | Choose (Regex a) (Regex a)
  | Optional (Regex a)
  | Star (Regex a)
  | Lookahead (Regex a)
  | Both (Regex a) (Regex a)
  | Negative (Regex a)
  deriving (Eq, Ord, Show, Data, Generic)

both :: Regex a -> Regex a -> Regex a
both = Both

negative :: Regex a -> Regex a
negative = Negative

lookahead :: Regex a -> Regex a
lookahead = Lookahead

char :: a -> Regex a
char = Char

anyChar :: Regex a
anyChar = AnyChar

emptyStr :: Regex a
emptyStr = Empty

failMatch :: Regex a
failMatch = Fail

cat :: Regex a -> Regex a -> Regex a
cat (Cat x y) z = Cat x (cat y z)
cat x y = Cat x y

cats :: [Regex a] -> Regex a
cats = foldr cat emptyStr

choose :: Eq a => Regex a -> Regex a -> Regex a
choose (Cat x y) (Cat x' z)
  | x == x' = cat x (choose y z)
choose Fail x = x
choose x Fail = x
choose x y
  | x == y    = x
  | otherwise = Choose x y

oneof :: Eq a => [Regex a] -> Regex a
oneof = foldr choose failMatch

optional :: Regex a -> Regex a
optional (Star x) = Star x
optional (Optional x) = Optional x
optional Empty = emptyStr
optional x = Optional x

star :: Eq a => Regex a -> Regex a
star (Star x) = Star x
star (Optional x) = star x
star (Choose x (Star y)) = star (choose x y)
star (Choose (Star x) y) = star (choose x y)
star Fail = emptyStr
star Empty = optional Empty
star x = Star x

digit :: Regex Char
digit = oneof (map char ['0' .. '9'])

number :: Regex Char
number =
  cats
    [ digit
    , star digit
    , optional (
        cats
          [ char '.'
          , digit
          , star digit
          , optional (char 'f')
          ]
      )
    ]

consume :: (Show a, Eq a) => Regex a -> [a] -> [[a]]
consume (Both r1 r2) s = do
  m1 <- consume r1 s
  m2 <- consume r2 s
  let [small, large] = sortBy (comparing length) [m1, m2]
  guard $ small `isSuffixOf` large
  pure small
consume (Negative r) s =
  case null $ consume r s of
    True  -> [s]
    False -> []
consume (Lookahead r) s = s <$ consume r s
consume Empty s             = [s]
consume AnyChar (_ : cs) = [cs]
consume AnyChar [] = []
consume (Char c) (c' : cs) = bool [] [cs] $ c == c'
consume (Char _) [] = []
consume Fail _              = []
consume (Cat r1 r2) str     = do
  str' <- consume r1 str
  consume r2 str'
consume (Choose r1 r2) str  = consume r1 str ++ consume r2 str
consume (Optional r) str    = str : consume r str
consume (Star _) []      = [[]]
consume s@(Star r) str      = str : do
  -- traceM $ show str
  str' <- consume r str
  if str /= str'
     then consume s str'
     else []

match :: (Show a, Eq a) => Regex a -> [a] -> Bool
match r s = not . null $ consume r s

------------------------------------------------------------------------------
-- | quickcheck

instance (Eq a, Arbitrary a) => Arbitrary (Regex a) where
  arbitrary = subtermFrequency
    [ (Cheap, char <$> arbitrary)
    , (Cheap, pure emptyStr)
    , (Cheap, pure failMatch)
    , (Expensive 2, cat      <$> smallerArbitrary 2 <*> smallerArbitrary 2)
    , (Expensive 2, choose   <$> smallerArbitrary 2 <*> smallerArbitrary 2)
    , (Expensive 4, star     <$> smallerArbitrary 2)
    , (Expensive 3, optional <$> smallerArbitrary 2)
    , (Expensive 2, lookahead <$> smallerArbitrary 2)
    , (Expensive 2, negative <$> smallerArbitrary 2)
    , (Expensive 4, both     <$> smallerArbitrary 2 <*> smallerArbitrary 2)
    ]
  shrink = genericShrink

smallerArbitrary :: Arbitrary a => Int -> Gen a
smallerArbitrary n = smallerGen n arbitrary

smallerGen :: Int -> Gen a -> Gen a
smallerGen n = scale (`div` n)

data Freq
  = Cheap
  | Expensive Int

splitFreq :: x -> Freq -> Either x Int
splitFreq x Cheap = Left x
splitFreq _ (Expensive x) = Right x

subtermFrequency :: [(Freq, Gen a)] -> Gen a
subtermFrequency qs =
  let (cheaps, exps) =
        partitionEithers
          $ fmap (\x -> sequence . swap $ first (splitFreq $ snd x) x) qs
   in QC.oneof
        [ QC.oneof cheaps
        , sized $ \size ->
            QC.frequency $
              (fmap (first (div size)) $ fmap swap exps) ++ fmap (1,) cheaps
        ]

------------------------------------------------------------------------------
-- | quickspec

instance (Show a, Arbitrary a, Ord a) => Observe [a] [[a]] (Regex a) where
  observe s r = nub $ sort $ consume r s

sig :: [Sig]
sig =
  [ withMaxTermSize 7
  , withMaxTests 1000
  , withMaxTestSize 10
  , defaultTo $ Proxy @Bool3

  , con "char"      $ char      @Bool3
  , con "emptyStr"  $ emptyStr  @Bool3
  , con "cat"       $ cat       @Bool3
  , con "choose"    $ choose    @Bool3
  , con "star"      $ star      @Bool3
  , con "negative"  $ negative @Bool3
  , con "lookahead"  $ lookahead @Bool3
  , con "both"  $ both @Bool3

  -- -- UNCOMMENT ME
  -- , con "failMatch" $ failMatch @Bool3
  -- , con "optional"  $ optional  @Bool3

  , monoTypeObserve $ Proxy @(Regex Bool3)
  , monoType $ Proxy @[Bool3]
  , monoType $ Proxy @Bool3
  ]

data Bool3 = True3 | False3 | Tri3 deriving (Eq, Ord, Show, Data)

instance Arbitrary Bool3 where
  arbitrary = elements [True3, False3, Tri3]

main :: IO ()
main = quickSpec sig