{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE TypeFamilies       #-}
{-# LANGUAGE TypeOperators      #-}

module BadRules where

import Generics.Instant.Rewriting
import Generics.Instant

-- Test datatypes
data Term = Val Int | Add Term Term | Mul Term Term
  deriving (Show, Typeable, Eq)

data RecTerm = Branch Int RecTerm RecTerm
  deriving (Show, Typeable, Eq)

-- SPVIew instances
instance Representable Term where
  type Rep Term = Var Int :+: Rec Term :*: Rec Term :+: Rec Term :*: Rec Term

  from (Val i)   = L (Var i)
  from (Add x y) = R (L (Rec x :*: Rec y))
  from (Mul x y) = R (R (Rec x :*: Rec y))

  to (L (Var i))               = Val i
  to (R (L (Rec x :*: Rec y))) = Add x y
  to (R (R (Rec x :*: Rec y))) = Mul x y

instance Representable RecTerm where
  type Rep RecTerm = Var Int :*: Rec RecTerm :*: Rec RecTerm
  from (Branch i x y)            = Var i :*: Rec x :*: Rec y
  to (Var i :*: Rec x :*: Rec y) = Branch i x y

-- Rewritable instances
instance Rewritable Term
instance Rewritable RecTerm


-- Superfluous metavariable
-- Result: *** Exception: invalid rule
badApplication1 :: Rule Term
badApplication1 = synthesise badApplication1Template
    where badApplication1Template :: Term -> Term -> Term -> Template Term
          badApplication1Template x y z = Add x y +-> Add y x

-- Unbound metavariable in right-hand side
-- Result: *** Exception: user error (merging failure)
badApplication2 :: Rule Term
badApplication2 = synthesise badApplication2Template
    where badApplication2Template x y = Add x x +-> Add y x

-- Unbound metavariable in guard
-- Result: *** Exception: user error (merging failure)
badApplication3 :: Rule Term
badApplication3 = synthesise badApplication3Template
    where badApplication3Template x y = Add x x +-> Add y x // const True y


-- Metavariable has no possible finite values
-- Result: would loop, but it is rejected at the type level
{-
badApplication4 :: Rule RecTerm
badApplication4 = synthesise badApplication4Template
    where badApplication4Template i x y = Branch i x y +-> Branch i y x
-}

main = (map validate [badApplication1, badApplication2, badApplication3])