{-# OPTIONS -fglasgow-exts -fallow-undecidable-instances #-}

module Expr.Main where

import Base
import Representations
import Rewriting


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

data Exp = Const Int | Exp :+: Exp | Exp :*: Exp
  deriving Show

-- TODO: sanity checking
-- to . from = id
instance View Exp where
  type PF Exp = Sum (K Int) (Sum (Con (Prod Id Id)) (Con (Prod Id Id)))

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

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

instance Rewrite Exp

instance GMap (PF Exp) where
  fmapM = fmapM


-- --------------------------------------
-- Example rules
-- --------------------------------------
peepHole1 :: Rule1 Exp
peepHole1 x = x :+: Const 0 :~> x

peepHole2 :: Rule1 Exp
peepHole2 x = x :+: x :~> Const 2 :*: x

peepHole3 :: Rule2 Exp
peepHole3 x y = x :+: y :~> y :+: x

peepHole4 :: Rule2 Exp
peepHole4 x y = Const 2 :*: (x :+: y) :~> (Const 2 :*: x) :+: (Const 2 :*: y)

peepHole5 :: Rule3 Exp
peepHole5 x y z = x :*: (y :+: z) :~> (x :*: y) :+: (x :*: z) 

peepHole6 :: Rule0 Exp
peepHole6 = Const 1 :+: Const 1 :~> Const 2


-- --------------------------------------
-- Tests
-- --------------------------------------
test1, test2, test3, test4, test5, test6, test7, test8, test9, test10, test11 :: Maybe Exp

test1 = rewrite1 peepHole1 (Const 2 :+: Const 0)
  -- This rewrites to |Const 2|

test2 = rewrite1 peepHole1 (Const 2 :+: Const 3)

test3 = rewrite1 peepHole2 (Const 4 :+: Const 3)

test4 = rewrite1 peepHole2 (Const 4 :+: Const 4)

test5 = one (rewrite1 peepHole1) ((Const 4 :+: Const 0) :*: Const 2)

-- This does not work because the optimisation target is not
-- an immediate child.
test6 = one (rewrite1 peepHole1) (((Const 4 :+: Const 0) :*: Const 2) :+: Const 7)

-- This works well, because once applies the rule to the optimisation
-- target exactly once.
test7 = once (rewrite1 peepHole1) (((Const 4 :+: Const 0) :*: Const 2) :+: Const 7)

test8 = rewrite2 peepHole3 ((Const 1) :+: (Const 2))

test9 = rewrite2 peepHole4 ((Const 2) :*: ((Const 3) :+: (Const 4)))

test10 = rewrite3 peepHole5 ((Const 1) :*: ((Const 2) :+: (Const 3)))

test11 = rewrite0 peepHole6 (Const 1 :+: Const 1)

test12 :: [Maybe Exp]
test12 = let a = mkRule peepHole1
             b = mkRule peepHole2
             c = mkRule peepHole3
             d = mkRule peepHole4
             e = mkRule peepHole5
             f = mkRule peepHole6  
             rules = [a, b, c, d, e, f]
             tests = [ Const 2 :+: Const 0
                     , Const 4 :+: Const 3
                     , Const 1 :+: Const 2
                     , Const 2 :*: (Const 3 :+: Const 4)
                     , Const 1 :*: (Const 2 :+: Const 3)
                     , Const 1 :+: Const 1
                     ]  
         in  zipWith rewrite rules tests