lazysmallcheck-0.1: benchmarks/RegExp.hs

(<==>) :: Bool -> Bool -> Bool
a <==> b = (a ==> b) && (b ==> a)

-- ---------------------

data Nat = Zer
         | Suc Nat
  deriving Show
--  deriving (Show,Data, Typeable)


instance Serial Nat where
  series = cons0 Zer \/ cons1 Suc

sub :: Nat -> Nat -> Nat
sub x y =
 case y of
  Zer -> x
  Suc y' -> case x of
   Zer -> Zer
   Suc x' -> sub x' y'

data Sym = N0
         | N1 Sym
 deriving (Eq, Show)
-- deriving (Eq, Show, Data, Typeable)

instance Serial Sym where
  series = cons0 N0 \/ cons1 N1

-- deriving Eq

data RE = Sym Sym
        | Or RE RE
        | Seq RE RE
        | And RE RE
        | Star RE
        | Empty
  deriving Show
--  deriving (Data, Typeable, Show)

{-
instance Serial RE where
  series =  cons0 Empty
         \/ cons1 Star
         \/ cons2 And
         \/ cons2 Seq
         \/ cons2 Or
         \/ cons1 Sym
-}

instance Serial RE where
  series = cons1 Sym
        \/ cons2 Or
        \/ cons2 Seq
        \/ cons2 And
        \/ cons1 Star
        \/ cons0 Empty



accepts :: RE -> [Sym] -> Bool
accepts re ss =
 case re of
  Sym n -> case ss of
   [] -> False
   (n':ss') -> n == n' && null ss'
  Or re1 re2 -> accepts re1 ss || accepts re2 ss
  Seq re1 re2 -> seqSplit re1 re2 [] ss
  And re1 re2 -> accepts re1 ss && accepts re2 ss
  Star re' -> case ss of
   [] -> True
   (s:ss') -> seqSplit re' re (s:[]) ss'
    -- accepts Empty ss || accepts (Seq re' re) ss
  Empty -> null ss

seqSplit :: RE -> RE -> [Sym] -> [Sym] -> Bool
seqSplit re1 re2 ss2 ss =
 seqSplit'' re1 re2 ss2 ss || seqSplit' re1 re2 ss2 ss

seqSplit'' :: RE -> RE -> [Sym] -> [Sym] -> Bool
seqSplit'' re1 re2 ss2 ss = accepts re1 ss2 && accepts re2 ss

seqSplit' :: RE -> RE -> [Sym] -> [Sym] -> Bool
seqSplit' re1 re2 ss2 ss =
 case ss of
  [] -> False
  (n:ss') ->
   seqSplit re1 re2 (ss2 ++ [n]) ss'

rep :: Nat -> RE -> RE
rep n re =
 case n of
  Zer -> Empty
  Suc n' -> Seq re (rep n' re)

repMax :: Nat -> RE -> RE
repMax n re =
 case n of
  Zer -> Empty
  Suc n' -> Or (rep n re) (repMax n' re)

repInt' :: Nat -> Nat -> RE -> RE
repInt' n k re =
 case k of
  Zer -> rep n re
  Suc k' -> Or (rep n re) (repInt' (Suc n) k' re)

repInt :: Nat -> Nat -> RE -> RE
repInt n k re = repInt' n (sub k n) re

-- ---------------------


-- main_1
prop_regex :: (Nat, Nat, RE, RE, [Sym]) -> Bool
prop_regex (n, k, p, q, s) =  r -- if r then True else True
  where
    r = (accepts (repInt n k (And p q)) s)
          <==> (accepts (And (repInt n k p) (repInt n k q)) s)
--(accepts (And (repInt n k p) (repInt n k q)) s) <==> (accepts (repInt n k (And p q)) s)

a_sol = (Zer, Suc (Suc Zer), Sym N0, Seq (Sym N0) (Sym N0), [N0, N0])