{-# LANGUAGE TypeSynonymInstances, PostfixOperators #-}
module Main where

import Control.Monad
import Prelude hiding ((+), (-), (*))

import Test.QuickCheck hiding (test, ok)

import Data.Regex.Antimirov hiding ( (<:), match )
import qualified Data.Regex.Antimirov as R

(<:) a b = (Just a) R.<: (Just b)
match r l_ = R.match (Just r) l_

test :: (RegexSubtyping sy, Show sy, Ord sy) => Regex sy -> ([[sy]], [[sy]]) -> IO ()
test r (pos, neg) = 
	let 
		fun = map (\g -> (match r g, g))
		(mPos, mNeg) = (fun pos, fun neg)
		errPos = filter (not . fst) mPos
		errNeg = filter fst mNeg
	in unless (null $ errPos ++ errNeg) (do
		putStr $ show r
	--	putStrLn $ show ndfa
		putStrLn $ show errPos ++ " " ++ show errNeg)
		
trick, t, p', p :: Regex Char
trick = (((l 'A')?)*)
t = l 'A' - l 'B'

p' = ((l 'A') ?) - ((l 'B') ?)
p = (p'*)

assert :: String -> Bool -> a -> a
assert s b r = if b then r else error s

instance RegexSubtyping ()

instance RegexSubtyping String

instance RegexSubtyping Char where
	literalSubtype _ '.' = True
	literalSubtype r s = r == s


data T = Element String (Regex T) | Any deriving (Ord, Eq, Show)

instance RegexSubtyping T where

	literalSubtype (Element n1 c1) (Element n2 c2) = n1 == n2 && c1 <: c2
	literalSubtype _ Any = True
	literalSubtype r s = r == s

compare' :: (RegexSubtyping sy, Show sy, Ord sy, Eq sy) => Regex sy -> Regex sy -> Maybe Ordering
compare' a1 a2 = case (a2 <: a1, a1 <: a2) of
	(False, False) -> Nothing
	(True, False) -> Just GT
	(False, True) -> Just LT
	(True, True) -> Just EQ

testCmp :: (RegexSubtyping sy, Ord sy, Show sy, Eq sy) => Maybe Ordering -> Regex sy -> Regex sy -> IO ()
testCmp o a1 a2 = let o' = compare' a1 a2 in do
	when (o /= o') (putStrLn $ "testCmp fail: " ++ show (a1, o, a2, o'))





main :: IO ()
main = do
	test t (["AB"], ["AC"])
	test ((l 'A' - ((l 'B')?) - l 'C')*) (["ACAC", "ABCAC"], ["ACC"])
	test trick (["", "A", "AAAAAA"], ["AC", "C", "AAAAC"])
	test (((l 'X') *) *) (["X"], ["A"])
	test (((l 'X') *) ?) (["XX", ""], ["A"])
	test p (["AB", "BA", "BBBB", ""], ["C"])
	let 
		t1 = (l 'A' - ((l 'B')*) - l 'C')
		r1 = (["ABC", "ABBBBBBC", "AC"], ["BC", "C", "AABC", "ABBBBBBBBBBBBBBCC"])
		t2 = ((l 'A' `Or` l 'B') - l 'C')
		r2 = (["AC", "BC"], ["ABC", "C"])
	test t1 r1
	test t2 r2
	test (t1 `Or` t2) (fst r1 ++ fst r2, [])
	test (t1 `Then` t2) (zipWith (++) (fst r1) (fst r2), [])
	test (t2 `Then` t1) (zipWith (++) (fst r2) (fst r1), [])
	test (Empty) ([""], ["A"])
	test (Literal 'A' `Or` (Literal 'A' `Then` Literal 'B')) (["AB", "A"], ["", "B", "AA"])
	test ((Literal 'A' `Then` Literal 'B') `Or` Literal 'A') (["AB", "A"], ["", "B", "AA"])
	test (Literal 'A' `Then` (Literal 'A' *)) (["AAAAAAAAAAAA"], ["", "B"])
--	test (Empty) (["Test the test"], [""])
	
	testCmp (Just GT) (Literal 'A' `Or` Literal 'B' `Or` Literal 'C') (Literal 'A' `Or` Literal 'B')
	testCmp (Just GT) ((Literal 'A' ?) `Then` (Literal 'B' ?)) (Literal 'A' `Or` Literal 'B')
	testCmp (Just EQ) Empty (Empty::Regex ())
	testCmp Nothing (Literal 'A') (Literal 'B') -- not equal, not gt not lt
	testCmp (Just LT) Empty (Literal 'A' *)
--	testCmp (Just EQ) (Literal "Test this test, too") Empty
	testCmp Nothing ((l 'C' ?) - l 'A') ((l 'A' ?) - l 'A')
	testCmp Nothing ((l 'C' *) # l 'A') (l 'C' - l 'A')

	testCmp (Just GT) (l 'C' - l '.') (l 'C' - l 'A')
	testCmp (Just GT) (l '.' - l '.') (l 'C' - l 'A')
	testCmp (Just GT) (l '.'  *) (l 'C' - l 'A')

	testCmp (Just LT) (l 'A') (l '.' ?)


	testCmp (Just EQ) (l 'a' - l 'b') (l 'a' - l 'b' # l 'a' - l 'b' # l 'a' - l 'b')
	testCmp (Just GT) ((l "first" *) - (l "second" *)) ((l "first" - l "second")?)


	testCmp (Just GT) (l Any *) (Then (l $ Element "e1" Empty) (l $ Element "e2" Empty))

	testCmp (Just GT) (l Any *) (Then (l $ Element "e1" Empty) (l $ Element "e2" Empty))

	testCmp (Just GT) (l $ Element "e1" (l Any)) (l $ Element "e1" (l $ Element "e2" Empty))
	testCmp (Just GT) (l $ Element "e1" ((l $ Element "e2" (l Any)) # Empty)) (l $ Element "e1" (Empty))


	testCmp (Just GT) ((l 'A' *) # (l 'B' *)) (l 'A')
	testCmp (Just GT) ((l 'A' *) # (l 'B' *)) (l 'B')
	testCmp (Just EQ) s_ s_
	testCmp (Just EQ)  te tf
	testCmp (Just LT) (l 'a' - l 'a' - l 'a') (l 'a' *)
	testCmp (Just EQ) ((l 'a' - l 'b') *) ((l 'a' - l 'b') *)
	testCmp Nothing ((l 'a' - l 'b') *) (((l 'a' - l 'b') *) - l 'c')

	quickCheck ((\e -> e <: e) :: Regex Char -> Bool)

	let f a b c = if a <: b && b <: c then a <: c else True
	quickCheck ((\a' -> let a = simplify a' in a <: a' && a' <: a) :: Regex Char -> Bool)
	quickCheck ((\a' b' c' -> let a = simplify a'; b = simplify b'; c = simplify c' in f a b c && f a c b && f b a c && f b c a && f c a b && f c b a) :: Regex Char -> Regex Char -> Regex Char -> Bool)

	testCmp (Just EQ) case1 case1
	testCmp (Just EQ) case2 case2
	testCmp (Just EQ) case3 case3
	testCmp (Just EQ)  case4 case4


te, tf :: Regex String
te = l "out" - ((l "in" - l "out")*)
tf = ((l "out" - l "in")*) - l "out"


case2, case3 :: Regex Char
case2 = ((Literal 'a' *) `Then` Literal 'c') `Then` ((Literal 'a' ?)*)


case3 = ((l 'b' # l 'c')*)
case4 = ((l 'b' - ((l 'a') *))*)

case1 :: Regex Char
case1 = Or ((Then (Or (Literal 'c') (Then (Literal 'b' *) Empty)) (Literal 'c'))) (Or Empty (Literal 'c')*)

s_ :: Regex Char
s_ = (l 'a' *)


instance (Arbitrary sy, Ord sy) => Arbitrary (Regex sy) where
	arbitrary = frequency [
		(2, liftM Star arbitrary),
		(7, liftM Literal arbitrary),
		(2, liftM2 Then arbitrary arbitrary),
		(2, liftM2 Or arbitrary arbitrary),
		(3, return Empty)]
	coarbitrary = undefined



instance Arbitrary Char where
	arbitrary = elements "abcd."
	coarbitrary = undefined