TestGen.hs

-- |This module uses "Test.Quickcheck" to test the PolyFix package by generating randomly 100 different types
-- running ExFind with that type and then simplifying the generated free theorem
-- to a antilogy of the kind \"() = _|_\" or \"0 = _|_\".
module Language.Haskell.FreeTheorems.Variations.CounterExamples.Test.TestGen where
import Test.QuickCheck
import Language.Haskell.FreeTheorems.Variations.CounterExamples.ExFind (testTerm,testSimple,getComplete)
import Language.Haskell.FreeTheorems.Variations.CounterExamples.Common.AlgCommon (showTyp)
import Language.Haskell.FreeTheorems.Variations.CounterExamples.Parser.ParseType(Typ(..), TypVar(..))
import Data.List (sort,nub)
import Control.Monad (liftM, liftM2)
import Debug.Trace

-- *Generation of example types

-- |TypVar generator
instance Arbitrary TypVar where
--  arbitrary = oneof [UnpointedVar arbitrary, PointedVar arbitrary]
  arbitrary = oneof [return (TypVar 1), return (TypVar 2), return(TypVar 3), return(TypVar 4), return (TypVar 5), return (TypVar 6)]

-- |recursive type generator
instance Arbitrary Typ where
  arbitrary = quantify (sized typ')
    where typ' 0 = frequency [(1, return Int), (1, return TNat), (12, liftM TVar arbitrary)]
          typ' n | n>0 =
               frequency [(1, liftM TVar arbitrary), (2,liftM2 Arrow subtyp1 subtyp1), (1,liftM List subtyp2), 
			  (1,return Int),(1,return TNat),(1,return TBrace),(1,return TBool), (1,liftM2 TPair subtyp1 subtyp1),
			  (1,liftM2 TEither subtyp1 subtyp1), (1,liftM TMaybe subtyp2)]
	    where subtyp1 = typ' (n `div` 2)
		  subtyp2 = typ' (n-1)
          quantify t = do {tau <- t;
			   return (addquantifiers tau (usedvars tau []))
			  }
	  usedvars tau vars = case tau of
                                TVar (TypVar i) -> (i:vars)
                                Arrow t1 t2     -> (usedvars t1 []) ++ (usedvars t2 []) ++ vars
                                List t1         -> (usedvars t1 []) ++ vars
				Int             -> vars
				TNat            -> vars
			        TBool           -> vars
                                TBrace          -> vars
				TPair t1 t2     -> (usedvars t1 []) ++ (usedvars t2 []) ++ vars
				TEither t1 t2   -> (usedvars t1 []) ++ (usedvars t2 []) ++ vars
                                TMaybe t1       -> (usedvars t1 []) ++ vars
--				_               -> vars
	  addquantifiers tau l =  case reverse.sort.nub $ l of
				    []   -> tau
                                    x:xs -> if x < 4 
					    then addquantifiers (AllStar (TypVar x) tau) xs
					    else addquantifiers (All (TypVar x) tau) xs


-- *test properties

prop_Test typ = trace (showTyp typ) True

prop_PrintTerms typ = trace 
		  (if findsTerm 
		   then "YES:" ++ showTyp typ ++ "\n\n" 
		   else "" --NO: " ++ showTyp typ ++ "\n\n"
		  ) True
    where findsTerm = if (testTerm typ) == Nothing then False else True

prop_HowManyTerms typ =
   classify (findsTerm)  "Term" $
   classify (not findsTerm) "No Term" $
   True
 where findsTerm = if (testTerm typ) == Nothing then False else True

prop_SimpleResult = testSimple
    
-- *test functions

mainTest = quickCheck prop_SimpleResult
howMany  = quickCheck prop_HowManyTerms
genCheck = quickCheck prop_Test
getTerms = quickCheck prop_PrintTerms