module QC_combinators where

import qualified Prelude as P (not)
import Prelude hiding (not)
import qualified QuickCheck as QC
import ShowFunctions
--import System(getEnv)
import Maybe(fromMaybe)

import Generators(generators)


-- the type of formulas
data F              = Prop QC.Property | Bool Bool

instance QC.Testable F where
  property (Bool p) = QC.property p
  property (Prop p) = p

-- predicates
type Pred a         = a -> F


(/\), (\/), (==>)   :: F -> F -> F
not                 :: F -> F
forAll, exists      :: (Show a, QC.Arbitrary a) => String -> (a -> F) -> F
true,false          :: F

(!)                 :: (a -> Bool) -> Pred a
lfp,gfp             :: (Pred a -> Pred a) -> Pred a
(===)               :: Eq a => a -> a -> F

(-=>)               :: (Show a, QC.Arbitrary a) => Pred a -> Pred b -> Pred (a -> b)

(%:)                :: Pred a -> Pred [a] -> Pred [a]




Bool p /\ Bool q    = Bool (p && q)
_ /\ _              = noNest

Bool p \/ Bool q    = Bool (p || q) 
_ \/ _              = noNest

not (Bool p)        = Bool (P.not p)
not _               = noNest

---
pNot p  = lift1 not p
(^/\) p q = liftPropOp (/\) p q
(^\/) p q = liftPropOp (\/) p q
(^==>) p q = liftPropOp (==>) p q
-- (^<==>) = liftPropOp (<==>)

class LiftProp p where
  lift1 :: (F->F)->p->p
  liftPropOp :: (F->F->F)->p->p->p

instance LiftProp F where
  lift1 = id
  liftPropOp = id

instance LiftProp p => LiftProp (a->p) where
  lift1 f p x = lift1 f (p x)
  liftPropOp op p q x = liftPropOp op (p x) (q x)

--liftPropOp op p q x = p x `op` q x -- The S combinator, missing from Prelude!

---

forAll x f          = Prop (QC.forAll (genFor x) f)

exists              = noExists        -- does not exist :-)

true                = Bool True

false               = Bool False

Bool p ==> q        = Prop (p QC.==> q)
p ==> q             = not p \/ q

x === y             = Bool (x == y)

(p -=> q) f         = forAll "x" $ \x -> p x ==> q (f x)        -- how to control this x

(!) p               = Bool . p


(p %: q) (x:xs)     = p x /\ q xs
(p %: q) _          = false


noNest              = error "nested quantifers are not supported"
noExists            = error "existential quantifiers are not supported"


-- TODO: parametrize on 50
-- lfp f x             = foldr (\/) false $ take 50 $ map ($ x) $ iterate f (const false)
-- gfp f x             = foldr (/\) true  $ take 50 $ map ($ x) $ iterate f (const true)


lfp f               = iterate f (const false) !! 50
--lfp f               = f (lfp f)
gfp f x             = foldr1 (/\) $ take 50 $ map ($ x) $ iterate f (const true)


genFor x            = fromMaybe QC.arbitrary (lookup x generators)


--testToFile fileName f = ...

testToStdout maxTest maxFail verbose =
    QC.check config{QC.configMaxTest=maxTest,QC.configMaxFail=maxFail}
  where 
    config = if verbose then qcVerbose else qcConfig

-- Copied from QuickCheck since they aren't exported:
qcConfig = QC.Config
  { QC.configMaxTest = 100
  , QC.configMaxFail = 1000
  , QC.configSize    = (+ 3) . (`div` 2)
  , QC.configEvery   = \n args -> let s = show n in s ++ [ '\b' | _ <- s ]
  }
         
qcVerbose = qcConfig
  { QC.configEvery = \n args -> show n ++ ":\n" ++ unlines args
  }