{-# OPTIONS -fglasgow-exts #-}

module RuleTesting where

-- import System.Random
import Control.Applicative
import Test.QuickCheck

import Base
import Representations
import GArbitrary
import Rules
import Rewriting
import Data.Maybe (fromJust)

-- Generic creation of rules.

genRule1 :: (GArbitrary (PF a), PFView a) => (a -> Rule a) -> Int -> Gen (Rule a)
genRule1 r1 n = r1
  <$> garbitrary n

genRule2 :: (GArbitrary (PF a), PFView a) => (a -> a -> Rule a) -> Int -> Gen (Rule a)
genRule2 r2 n = (\a b -> r2 a b)
  <$> garbitrary n
  <*> garbitrary n

genRule3 :: (GArbitrary (PF a), PFView a) => (a -> a -> a -> Rule a) -> Int -> Gen (Rule a)
genRule3 r3 n = (\a b c -> r3 a b c)
  <$> garbitrary n
  <*> garbitrary n
  <*> garbitrary n

genLhsRule1 r n = lhsR <$> genRule1 r n 
genLhsRule2 r n = lhsR <$> genRule2 r n 
genLhsRule3 r n = lhsR <$> genRule3 r n 

genRhsRule1 r n = rhsR <$> genRule1 r n 
genRhsRule2 r n = rhsR <$> genRule2 r n 
genRhsRule3 r n = rhsR <$> genRule3 r n 

-- Interesting rule properties.

prop_rewrite1 ::
  (PFView a, LR (PF a), Crush (PF a), Zip (PF a), Eq a) =>
  Rule1 a -> a -> Bool
prop_rewrite1 r1 e = rewriteM (rule r1) l == Just r
  where l = lhsR $ r1 e
        r = rhsR $ r1 e

prop_rewrite2 ::
  (PFView a, LR (PF a), Crush (PF a), Zip (PF a), Eq a) =>
  Rule2 a -> a -> a -> Bool
prop_rewrite2 r2 e0 e1 = rewriteM (rule r2) l == Just r
  where l = lhsR $ r2 e0 e1
        r = rhsR $ r2 e0 e1

prop_rewrite3 ::
  (PFView a, LR (PF a), Crush (PF a), Zip (PF a), Eq a) =>
  Rule3 a -> a -> a -> a -> Bool
prop_rewrite3 r3 e0 e1 e2 = rewriteM (rule r3) l == Just r
  where l = lhsR $ r3 e0 e1 e2
        r = rhsR $ r3 e0 e1 e2


prop_semantics1 :: (Crush (PF a), PFView a, Zip (PF a), LR (PF a)) =>
                   (a -> a -> Bool) -> Rule1 a -> a -> Bool
prop_semantics1 f r e = f (fromJust $ rewriteM (rule r) l) l
  where l = lhsR $ r e

prop_semantics2 :: (Crush (PF a), PFView a, Zip (PF a), LR (PF a)) =>
                   (a -> a -> Bool) -> Rule2 a -> a -> a -> Bool
prop_semantics2 f r e0 e1 = f (fromJust $ rewriteM (rule r) l) l
  where l = lhsR $ r e0 e1

prop_semantics3 :: (Crush (PF a), PFView a, Zip (PF a), LR (PF a)) =>
                   (a -> a -> Bool) -> Rule3 a -> a -> a -> a -> Bool
prop_semantics3 f r e0 e1 e2 = f (fromJust $ rewriteM (rule r) l) l
  where l = lhsR $ r e0 e1 e2