{-# LANGUAGE GADTs, ExistentialQuantification #-}
-----------------------------------------------------------------------------
-- Copyright 2011, Open Universiteit Nederland. This file is distributed
-- under the terms of the GNU General Public License. For more information,
-- see the file "LICENSE.txt", which is included in the distribution.
-----------------------------------------------------------------------------
-- |
-- Maintainer  :  bastiaan.heeren@ou.nl
-- Stability   :  provisional
-- Portability :  portable (depends on ghc)
--
-- This module defines transformations. Given a term, a transformation returns a list of
-- results (often a singleton list or the empty list). A transformation can be parameterized
-- with one or more arguments. A rule is in essence just a transformation with a name (which
-- should be unique). Both transformations and rules can be lifted to work on more complex domains.
--
-----------------------------------------------------------------------------
module Common.Transformation
   ( -- * Transformations
     Transformation, makeTrans, makeTransList, makeRewriteTrans
     -- * Arguments
   , ArgDescr(..), defaultArgDescr, Argument(..), ArgValue(..), ArgValues
   , supply1, supply2, supply3
   , hasArguments, expectedArguments, getDescriptors, useArguments
     -- * Rules
   , Rule, isMinorRule, isMajorRule, isBuggyRule, isRewriteRule
   , finalRule, isFinalRule, ruleSiblings, rule, ruleList
   , makeRule, makeRuleList, makeSimpleRule, makeSimpleRuleList
   , idRule, checkRule, emptyRule, minorRule, buggyRule, doAfter
   , siblingOf, transformations, getRewriteRules
   , ruleRecognizer, useRecognizer, useSimpleRecognizer
     -- * Lifting
   , liftRule, liftTrans, liftRuleIn, liftTransIn
     -- * QuickCheck
   , testRule, propRuleSmart
   ) where

import Common.Classes
import Common.Id
import Common.Rewriting
import Common.Utils
import Common.View
import Control.Monad
import Data.Function
import Data.Maybe
import Test.QuickCheck

-----------------------------------------------------------
--- Transformations

-- | Abstract data type for representing transformations
data Transformation a
   = Function (a -> [a])
   | RewriteRule (RewriteRule a) (a -> [a])
   | forall b . Abstraction (ArgumentList b) (a -> Maybe b) (b -> Transformation a)
   | forall b c . LiftView (View a (b, c)) (Transformation b)
   | Recognizer (a -> a -> Maybe ArgValues) (Transformation a)

instance Apply Transformation where
   applyAll (Function f)        = f
   applyAll (RewriteRule _ f)   = f
   applyAll (Abstraction _ f g) = \a -> maybe [] (\b -> applyAll (g b) a) (f a)
   applyAll (LiftView v t)      = \a -> [ build v (b, c) | (b0, c) <- matchM v a, b <- applyAll t b0  ]
   applyAll (Recognizer _ t)    = applyAll t

-- | Turn a function (which returns its result in the Maybe monad) into a transformation
makeTrans :: (a -> Maybe a) -> Transformation a
makeTrans f = makeTransList (maybe [] return . f)

-- | Turn a function (which returns a list of results) into a transformation
makeTransList :: (a -> [a]) -> Transformation a
makeTransList = Function

-- | Turn a rewrite rule into a transformation
makeRewriteTrans :: RewriteRule a -> Transformation a
makeRewriteTrans r = RewriteRule r (rewriteM r)

-----------------------------------------------------------
--- Arguments

-- | A data type for describing an argument of a parameterized transformation
data ArgDescr a = ArgDescr
   { labelArgument    :: String               -- ^ Label that is shown to the user when asked to supply the argument
   , defaultArgument  :: Maybe a              -- ^ Default value that can be used
   , parseArgument    :: String -> Maybe a    -- ^ A parser
   , showArgument     :: a -> String          -- ^ A pretty-printer
   , termViewArgument :: View Term a          -- ^ Conversion to/from term
   , genArgument      :: Gen a                -- ^ An arbitrary argument generator
   }

-- | An argument descriptor, paired with a value
data ArgValue = forall a . ArgValue (ArgDescr a) a

-- | List of argument values
type ArgValues = [ArgValue]

instance Show ArgValue where
   show (ArgValue descr a) = showArgument descr a

instance Eq ArgValue where
   ArgValue d1 a1 == ArgValue d2 a2 =
      build (termViewArgument d1) a1 == build (termViewArgument d2) a2

-- | Constructor function for an argument descriptor that uses the Show and Read type classes
defaultArgDescr :: (Show a, Read a, IsTerm a, Arbitrary a) => String -> ArgDescr a
defaultArgDescr descr = ArgDescr descr Nothing readM show termView arbitrary

-- | A type class for types which have an argument descriptor
class Arbitrary a => Argument a where
   makeArgDescr :: String -> ArgDescr a   -- ^ The first argument is the label of the argument descriptor

instance Argument Int where
   makeArgDescr = defaultArgDescr

-- | Parameterization with one argument using the provided label
supply1 :: Argument x
                  => String -> (a -> Maybe x)
                  -> (x -> Transformation a) -> Transformation a
supply1 s f t =
   let args = Single (makeArgDescr s)
   in Abstraction args f t

-- | Parameterization with two arguments using the provided labels
supply2 :: (Argument x, Argument y)
                   => (String, String) -> (a -> Maybe (x, y))
                   -> (x -> y -> Transformation a) -> Transformation a
supply2 (s1, s2) f t =
   let args = Pair (Single (makeArgDescr s1)) (Single (makeArgDescr s2))
   in Abstraction args f (uncurry t)

-- | Parameterization with three arguments using the provided labels
supply3 :: (Argument x, Argument y, Argument z)
                  => (String, String, String) -> (a -> Maybe (x, y, z))
                  -> (x -> y -> z -> Transformation a) -> Transformation a
supply3 (s1, s2, s3) f t =
   let args = Pair (Single (makeArgDescr s1))
                   (Pair (Single (makeArgDescr s2)) (Single (makeArgDescr s3)))
       nest (a, b, c) = (a, (b, c))
   in Abstraction args (fmap nest . f) (\(a, (b, c)) -> t a b c)

-- | Checks whether a rule is parameterized
hasArguments :: Rule a -> Bool
hasArguments = not . null . getDescriptors

-- | Returns a list of argument descriptors
getDescriptors :: Rule a -> [Some ArgDescr]
getDescriptors r =
   case transformations r of
      [t] -> rec t
      _   -> []
 where
   rec :: Transformation a -> [Some ArgDescr]
   rec trans =
      case trans of
         Abstraction args _ _ -> someArguments args
         LiftView _ t   -> rec t
         Recognizer _ t -> rec t
         _ -> []

-- | Returns a list of pretty-printed expected arguments.
-- Nothing indicates that there are no such arguments (or the arguments
-- are not applicable for the current value)
expectedArguments :: Rule a -> a -> Maybe ArgValues
expectedArguments r =
   case transformations r of
      [t] -> rec t
      _   -> const Nothing
 where
    rec :: Transformation a -> a -> Maybe ArgValues
    rec trans a =
       case trans of
          Abstraction args f _ ->
             fmap (argumentValues args) (f a)
          LiftView v t -> do
             (b, _) <- match v a
             rec t b
          Recognizer _ t ->
             rec t a
          _ -> Nothing

-- | Transform a rule and use a list of pretty-printed arguments. Nothing indicates that the arguments are
-- invalid (not parsable), or that the wrong number of arguments was supplied
useArguments :: [String] -> Rule a -> Maybe (Rule a)
useArguments list r =
   case transformations r of
      [t] -> do new <- make t
                return r {transformations = [new]}
      _   -> Nothing
 where
   make :: Transformation a -> Maybe (Transformation a)
   make trans =
      case trans of
         Abstraction args _ g -> fmap g (parseArguments args list)
         LiftView v t         -> fmap (LiftView v) (make t)
         Recognizer f t       -> fmap (Recognizer f) (make t)
         _                    -> Nothing

-----------------------------------------------------------
--- Internal machinery for arguments

data ArgumentList a where
   Single :: ArgDescr a -> ArgumentList a
   Pair   :: ArgumentList a -> ArgumentList b -> ArgumentList (a, b)

parseArguments :: ArgumentList a -> [String] -> Maybe a
parseArguments (Single a) [x] = parseArgument a x
parseArguments (Pair a b) xs =
   let (ys, zs) = splitAt (numberOfArguments a) xs
   in liftM2 (,) (parseArguments a ys) (parseArguments b zs)
parseArguments _ _ = Nothing

someArguments :: ArgumentList a -> [Some ArgDescr]
someArguments (Single a) = [Some a]
someArguments (Pair a b) = someArguments a ++ someArguments b

argumentValues :: ArgumentList a -> a -> ArgValues
argumentValues (Single a) x      = [ArgValue a x]
argumentValues (Pair a b) (x, y) = argumentValues a x ++ argumentValues b y

numberOfArguments :: ArgumentList a -> Int
numberOfArguments = length . someArguments

-----------------------------------------------------------
--- Rules

-- | Abstract data type for representing rules
data Rule a = Rule
   { ruleId          :: Id  -- ^ Unique identifier of the rule
   , transformations :: [Transformation a]
   , afterwards      :: a -> a
   , isBuggyRule     :: Bool -- ^ Inspect whether or not the rule is buggy (unsound)
   , isMinorRule     :: Bool -- ^ Returns whether or not the rule is minor (i.e., an administrative step that is automatically performed by the system)
   , isFinalRule     :: Bool -- ^ Final (clean-up) step in derivation
   , ruleSiblings    :: [Id]
   }

instance Show (Rule a) where
   show = showId

instance Eq (Rule a) where
   r1 == r2 = ruleId r1 == ruleId r2

instance Ord (Rule a) where
   compare = compareId

instance Apply Rule where
   applyAll r a = do
      t <- transformations r
      b <- applyAll t a
      return (afterwards r b)

instance HasId (Rule a) where
   getId        = ruleId
   changeId f r = r { ruleId = f (ruleId r) }

instance (Arbitrary a, CoArbitrary a) => Arbitrary (Rule a) where
   arbitrary = liftM3 make arbitrary arbitrary arbitrary
    where
      make minor n f
         | minor     = minorRule $ makeSimpleRule n f
         | otherwise = makeSimpleRule (n :: Id) f

-- | Returns whether or not the rule is major (i.e., not minor)
isMajorRule :: Rule a -> Bool
isMajorRule = not . isMinorRule

isRewriteRule :: Rule a -> Bool
isRewriteRule = not . null . getRewriteRules

siblingOf :: HasId b => b -> Rule a -> Rule a
siblingOf sib r = r { ruleSiblings = getId sib : ruleSiblings r }

ruleList :: (IsId n, RuleBuilder f a) => n -> [f] -> Rule a
ruleList n = makeRuleList a . map (makeRewriteTrans . rewriteRule a)
 where a = newId n

rule :: (IsId n, RuleBuilder f a) => n -> f -> Rule a
rule n = makeRule a . makeRewriteTrans . rewriteRule a
 where a = newId n

-- | Turn a transformation into a rule: the first argument is the rule's name
makeRule :: IsId n => n -> Transformation a -> Rule a
makeRule n = makeRuleList n . return

-- | Turn a list of transformations into a single rule: the first argument is the rule's name
makeRuleList :: IsId n => n -> [Transformation a] -> Rule a
makeRuleList n ts = Rule (newId n) ts id False False False []

-- | Turn a function (which returns its result in the Maybe monad) into a rule: the first argument is the rule's name
makeSimpleRule :: IsId n => n -> (a -> Maybe a) -> Rule a
makeSimpleRule n = makeRule n . makeTrans

-- | Turn a function (which returns a list of results) into a rule: the first argument is the rule's name
makeSimpleRuleList :: IsId n => n -> (a -> [a]) -> Rule a
makeSimpleRuleList n = makeRule n . makeTransList

-- | A special (minor) rule that always returns the identity
idRule :: Rule a
idRule = minorRule $ makeSimpleRule "Identity" return

-- | A special (minor) rule that checks a predicate (and returns the identity
-- if the predicate holds)
checkRule :: (a -> Bool) -> Rule a
checkRule p = minorRule $ makeSimpleRule "Check" $ \a ->
   if p a then Just a else Nothing

-- | A special (minor) rule that is never applicable (i.e., this rule always fails)
emptyRule :: Rule a
emptyRule = minorRule $ makeSimpleRule "Empty" (const Nothing)

-- | Mark the rule as minor (by default, rules are not minor)
minorRule :: Rule a -> Rule a
minorRule r = r {isMinorRule = True}

-- | Mark the rule as buggy (by default, rules are supposed to be sound)
buggyRule :: Rule a -> Rule a
buggyRule r = r {isBuggyRule = True}

-- | Mark the rule as final (by default, false). Final rules are used as a
-- final step in the derivation, to get the term in the expected form
finalRule :: Rule a -> Rule a
finalRule r = r {isFinalRule = True}

-- | Perform the function after the rule has been fired
doAfter :: (a -> a) -> Rule a -> Rule a
doAfter f r = r {afterwards = f . afterwards r}

getRewriteRules :: Rule a -> [(Some RewriteRule, Bool)]
getRewriteRules r = concatMap f (transformations r)
 where
   f :: Transformation a -> [(Some RewriteRule, Bool)]
   f trans =
      case trans of
         RewriteRule rr _ -> [(Some rr, not $ isBuggyRule r)]
         LiftView _ t     -> f t
         _                -> []

ruleRecognizer :: (a -> a -> Bool) -> Rule a -> a -> a -> Maybe ArgValues
ruleRecognizer eq r a b = msum
   [ transRecognizer eq t a b | t <- transformations r ]

transRecognizer :: (a -> a -> Bool) -> Transformation a -> a -> a -> Maybe ArgValues
transRecognizer eq trans a b =
   case trans of
      Recognizer f t -> f a b `mplus` transRecognizer eq t a b
      LiftView v t   -> msum
         [ transRecognizer (eq `on` f) t av bv
         | (av, c) <- matchM v a
         , (bv, _) <- matchM v b
         , let f z = build v (z, c)
         ]
       `mplus`
         noArg (any (`eq` b) (applyAll trans a)) -- is this really needed?
      _ -> noArg $ any (`eq` b) (applyAll trans a)
 where
   noArg c = if c then Just [] else Nothing

useRecognizer :: (a -> a -> Maybe ArgValues) -> Transformation a -> Transformation a
useRecognizer = Recognizer

useSimpleRecognizer :: (a -> a -> Bool) -> Transformation a -> Transformation a
useSimpleRecognizer p = useRecognizer $ \x y -> guard (p x y) >> return []

-----------------------------------------------------------
--- Lifting

liftTrans :: View a b -> Transformation b -> Transformation a
liftTrans v = liftTransIn (v &&& identity)

liftTransIn :: View a (b, c) -> Transformation b -> Transformation a
liftTransIn = LiftView

liftRule :: View a b -> Rule b -> Rule a
liftRule v = liftRuleIn (v &&& identity)

liftRuleIn :: View a (b, c) -> Rule b -> Rule a
liftRuleIn v r = r
   { transformations = map (liftTransIn v) (transformations r)
   , afterwards      = simplifyWith (mapFirst (afterwards r)) v
   }

-----------------------------------------------------------
--- QuickCheck

-- | Check the soundness of a rule: the equality function is passed explicitly
testRule :: (Arbitrary a, Show a) => (a -> a -> Bool) -> Rule a -> IO ()
testRule eq r =
   quickCheck (propRule eq r arbitrary)

-- | Check the soundness of a rule and use a "smart generator" for this. The smart generator
-- behaves differently on transformations constructed with a (|-), and for these transformations,
-- the left-hand side patterns are used (meta variables are instantiated with random terms)
propRuleSmart :: Show a => (a -> a -> Bool) -> Rule a -> Gen a -> Property
propRuleSmart eq r = propRule eq r . smartGen r

propRule :: Show a => (a -> a -> Bool) -> Rule a -> Gen a -> Property
propRule eq r gen =
   forAll gen $ \a ->
   forAll (smartApplyRule r a) $ \ma ->
      isJust ma ==> (a `eq` fromJust ma)

smartGen :: Rule a -> Gen a -> Gen a
smartGen r gen = frequency [(2, gen), (1, smart)]
 where
   smart = gen >>= \a ->
      oneof (gen : mapMaybe (smartGenTrans a) (transformations r))

smartGenTrans :: a -> Transformation a -> Maybe (Gen a)
smartGenTrans a trans =
   case trans of
      RewriteRule r _ -> return (smartGenerator r)
      LiftView v t -> do
         (b, c) <- matchM v a
         gen    <- smartGenTrans b t
         return $ liftM (\n -> build v (n, c)) gen
      _ -> Nothing

smartApplyRule :: Rule a -> a -> Gen (Maybe a)
smartApplyRule r a = do
   xss <- mapM (`smartApplyTrans` a) (transformations r)
   case concat xss of
      [] -> return Nothing
      xs -> elements $ map Just xs

smartApplyTrans :: Transformation a -> a -> Gen [a]
smartApplyTrans trans a =
   case trans of
      Abstraction args _ g -> smartArgs args >>= \b -> smartApplyTrans (g b) a
      _ -> return (applyAll trans a)

smartArgs :: ArgumentList a -> Gen a
smartArgs (Single a) = genArgument a
smartArgs (Pair a b) = liftM2 (,) (smartArgs a) (smartArgs b)