{-# OPTIONS -fglasgow-exts #-}

module Expr where

import Control.Applicative hiding (Const)
import Test.QuickCheck
import Data.Maybe

import Base
import Representations
import GArbitrary
import Rewriting
import Rules
import Strategies
import RuleTesting

-- --------------------------------------
-- Types and conversion
-- --------------------------------------
infixl 7 :*:
infixl 6 :+:

data Expr = Const Int | Expr :+: Expr | Expr :*: Expr deriving (Show, Eq)

instance PFView Expr where
  type PF Expr = Sum (Con (K Int)) (Sum (Con (Prod Id Id)) (Con (Prod Id Id)))

  from (Const n)   = Inl (Con "Const" (K n))
  from (e1 :+: e2) = Inr (Inl (Con "(:+:)" $ Prod (Id e1) (Id e2)))
  from (e1 :*: e2) = Inr (Inr (Con "(:*:)" $ Prod (Id e1) (Id e2)))

  to (Inl (Con _ (K n)))                        = Const n
  to (Inr (Inl (Con _ (Prod (Id r1) (Id r2))))) = r1 :+: r2
  to (Inr (Inr (Con _ (Prod (Id r1) (Id r2))))) = r1 :*: r2

instance Arbitrary Expr where
  arbitrary = sized garbitrary
  coarbitrary = undefined

eval :: Expr -> Int
eval (Const x) = x
eval (x :+: y) = eval x + eval y
eval (x :*: y) = eval x * eval y

-- --------------------------------------
-- Testing.
-- --------------------------------------

prop_semantics1 :: Rule1 Expr -> Expr -> Bool
prop_semantics1 r e = (eval <$> Just l) == (eval <$> rewriteM (rule r) l)
  where l = lhsR $ r e

prop_semantics2 :: Rule2 Expr -> Expr -> Expr -> Bool
prop_semantics2 r e0 e1 = (eval <$> Just l) == (eval <$> rewriteM (rule r) l)
  where l = lhsR $ r e0 e1

prop_semantics3 :: Rule3 Expr -> Expr -> Expr -> Expr -> Bool
prop_semantics3 r e0 e1 e2 = (eval <$> Just l) == (eval <$> rewriteM (rule r) l)
  where l = lhsR $ r e0 e1 e2

-- --------------------------------------
-- Example rules
-- --------------------------------------
rule1 x = x :+: Const 0 :~> x
rule1'  = rule rule1

rule2 x = x :+: x :~> Const 2 :*: x
rule2'  = rule rule2

rule3 x y = x :+: y :~> y :+: x
rule3'    = rule rule3

rule4 x y = Const 2 :*: (x :+: y) :~> (Const 2 :*: x) :+: (Const 2 :*: y)
rule4'    = rule rule4

rule5 x y z = x :*: (y :+: z) :~> (x :*: y) :+: (x :*: z) 
rule5'      = rule rule5

rule6 = Const 1 :+: Const 1 :~> Const 2
rule6' = rule rule6

-- --------------------------------------
-- Tests
-- --------------------------------------
test1 :: Maybe Expr
test1 = rewriteM rule1' (Const 2 :+: Const 0)

test2 :: Maybe Expr
test2 = rewriteM rule1' (Const 2 :+: Const 3)

test3 :: Maybe Expr
test3 = rewriteM rule2' (Const 4 :+: Const 3)

test4 :: Maybe Expr
test4 = rewriteM rule2' (Const 4 :+: Const 4)

test5 :: Maybe Expr
test5 = one (rewriteM rule1') ((Const 4 :+: Const 0) :*: Const 2)

-- This does not work because the optimisation target is not
-- an immediate child.
test6 :: Maybe Expr
test6 = one (rewriteM rule1') (((Const 4 :+: Const 0) :*: Const 2) :+: Const 7)

-- This works well, because once applies the rule to the optimisation
-- target exactly once.
test7 :: Maybe Expr
test7 = once (rewriteM rule1') (((Const 4 :+: Const 0) :*: Const 2) :+: Const 7)

test8 :: Maybe Expr
test8 = rewriteM rule3' ((Const 1) :+: (Const 2))

test9 :: Maybe Expr
test9 = rewriteM rule4' ((Const 2) :*: ((Const 3) :+: (Const 4)))

test10 :: Maybe Expr
test10 = rewriteM rule5' ((Const 1) :*: ((Const 2) :+: (Const 3)))

test11 :: Maybe Expr
test11 = rewriteM rule6' (Const 1 :+: Const 1)

allTests :: [Maybe Expr]
allTests = [ test1
           , test2
           , test3
           , test4
           , test5
           , test6
           , test7
           , test8
           , test9
           , test10
           , test11
           ]


-- --------------------------------------
-- Running all the tests
-- --------------------------------------
-- This main function is defined to solve a bug in GHC
main :: IO ()
main = do let resultsPP         = zipWith resultPP [1..] allTests
              resultPP n result = "test" ++ show n ++ ": " ++ show result
          putStr (unlines resultsPP)