{-# LANGUAGE RankNTypes, ExistentialQuantification #-}
-----------------------------------------------------------------------------
-- Copyright 2019, Ideas project team. This file is distributed under the
-- terms of the Apache License 2.0. For more information, see the files
-- "LICENSE.txt" and "NOTICE.txt", which are included in the distribution.
-----------------------------------------------------------------------------
-- |
-- Maintainer  :  bastiaan.heeren@ou.nl
-- Stability   :  provisional
-- Portability :  portable (depends on ghc)
--
-- Representation of a strategy as a cyclic tree with explicit fixed-points.
-- The nodes in the tree are named strategy combinators. The leafs are rules.
--
-----------------------------------------------------------------------------

module Ideas.Common.Strategy.StrategyTree
   ( -- * StrategyTree type synonym
     StrategyTree, Leaf(..), treeToProcess, mapRulesInTree
     -- * Declarations (named combinators)
   , Decl, Combinator, associative, isAssociative, combinator
   ,  (.=.), applyDecl
     -- * Dynamic strategies
   , Dynamic, makeDynamic, dynamicToTerm, dynamicTree, dynamicFromTerm
     -- * Arities
   , Arity(..), Nullary(..), Unary(..), Binary(..), Nary(..)
   ) where

import Control.Monad
import Data.Function
import Data.Maybe
import Ideas.Common.Classes
import Ideas.Common.Id
import Ideas.Common.Rewriting.Term (Term, IsTerm(..))
import Ideas.Common.Rule
import Ideas.Common.Strategy.Choice
import Ideas.Common.Strategy.CyclicTree
import Ideas.Common.Strategy.Process
import Ideas.Common.Strategy.Sequence
import Ideas.Common.Strategy.Symbol
import Ideas.Common.View

infix 1 .=.

------------------------------------------------------------------------------

type StrategyTree a = CyclicTree (Decl Nary) (Leaf a)

data Leaf a = LeafRule (Rule a)
            | LeafDyn  (Dynamic a)

instance Show (Leaf a) where
   show = showId

instance Eq (Leaf a) where
   x == y = getId x == getId y

instance HasId (Leaf a) where
   getId      (LeafRule r) = getId r
   getId      (LeafDyn d)  = getId d
   changeId f (LeafRule r) = LeafRule (changeId f r)
   changeId f (LeafDyn d)  = LeafDyn (changeId f d)

instance AtomicSymbol (Leaf a) where
   atomicOpen  = LeafRule atomicOpen
   atomicClose = LeafRule atomicClose

instance LabelSymbol (Leaf a) where
   isEnterSymbol (LeafRule r) = isEnterSymbol r
   isEnterSymbol (LeafDyn _)  = False

instance Minor (Leaf a) where
   isMinor    (LeafRule r)   = isMinor r
   isMinor    (LeafDyn _)    = False
   setMinor b (LeafRule r)   = LeafRule (setMinor b r)
   setMinor _ lf@(LeafDyn _) = lf

instance Apply Leaf where
   applyAll (LeafRule r) a    = applyAll r a
   applyAll (LeafDyn d) a = applyAll d a

instance LiftView Leaf where
   liftViewIn v (LeafRule r) = LeafRule (liftViewIn v r)
   liftViewIn v (LeafDyn d)  = LeafDyn  (liftViewIn v d)

treeToProcess :: StrategyTree a -> Process (Leaf a)
treeToProcess = foldUnwind emptyAlg
   { fNode  = fromNary . combinator
   , fLeaf  = single
   , fLabel = \l p -> LeafRule (enterRule l) ~> p .*. (LeafRule (exitRule l) ~> done)
   }

mapRulesInTree :: (Rule a -> Rule a) -> StrategyTree a -> StrategyTree a
mapRulesInTree f = inTree
 where
   inTree = fmap inLeaf

   inLeaf (LeafRule r) = LeafRule (f r)
   inLeaf (LeafDyn d)  = LeafDyn (inDyn d)

   inDyn d = d { dynamicFromTerm = fmap inTree . dynamicFromTerm d }

applyDecl :: Arity f => Decl f -> f (StrategyTree a)
applyDecl d = toArity (node (d {combinator = op}) . make)
 where
   op = Nary $ fromMaybe empty . listify (combinator d)

   make | isAssociative d = concatMap collect
        | otherwise       = id

   collect a  =
      case isNode a of
         Just (da, as) | getId da == getId d -> as
         _ -> [a]

------------------------------------------------------------------------------

data Dynamic a = Dyn
   { dynamicId       :: Id
   , dynamicToTerm   :: a -> Maybe Term
   , dynamicFromTerm :: Term -> Maybe (StrategyTree a)
   }

instance HasId (Dynamic a) where
   getId = dynamicId
   changeId f d = d { dynamicId = changeId f (dynamicId d) }

instance Apply Dynamic where
   applyAll d a = maybe [] ((`runProcess` a) . treeToProcess) (dynamicTree d a)

instance LiftView Dynamic where
   liftViewIn v d = d
      { dynamicToTerm   = fmap fst . match v >=> dynamicToTerm d
      , dynamicFromTerm = fmap (fmap (liftViewIn v)) . dynamicFromTerm d
      }

makeDynamic :: (IsId n, IsTerm a) => n -> (a -> StrategyTree a) -> Dynamic a
makeDynamic n f = Dyn (newId n) (Just . toTerm) (fmap f . fromTerm)

dynamicTree :: Dynamic a -> a -> Maybe (StrategyTree a)
dynamicTree d = dynamicToTerm d >=> dynamicFromTerm d

------------------------------------------------------------------------------

type Combinator f = forall a . f (Process (Leaf a))

data Decl f = C
   { declId        :: Id
   , combinator    :: Combinator f
   , isAssociative :: Bool
   }

instance Show (Decl f) where
   show = showId

instance Eq (Decl f) where
   (==) = (==) `on` getId

instance HasId (Decl f) where
   getId = declId
   changeId f d = d { declId = f (declId d) }

(.=.) :: IsId n => n -> Combinator f -> Decl f
n .=. f = C (newId n) f False

associative :: Decl f -> Decl f
associative c = c {isAssociative = True}

------------------------------------------------------------------------------

class Arity f where
   listify :: f a -> [a] -> Maybe a
   toArity :: ([a] -> a) -> f a
   liftIso :: Isomorphism a b -> f a -> f b

newtype Nullary a = Nullary { fromNullary :: a }
newtype Unary   a = Unary   { fromUnary   :: a -> a }
newtype Binary  a = Binary  { fromBinary  :: a -> a -> a }
newtype Nary    a = Nary    { fromNary    :: [a] -> a }

instance Arity Nullary where
   listify (Nullary a) [] = Just a
   listify _ _ = Nothing
   toArity f = Nullary (f [])
   liftIso p (Nullary a) = Nullary (from p a)

instance Arity Unary where
   listify (Unary f) [x] = Just (f x)
   listify _ _ = Nothing
   toArity f = Unary (\x -> f [x])
   liftIso p (Unary f) = Unary (from p . f . to p)

instance Arity Binary where
   listify (Binary f) [x, y] = Just (f x y)
   listify _ _ = Nothing
   toArity f = Binary (\x y -> f [x, y])
   liftIso p (Binary f) = Binary (\x y -> from p (f (to p x) (to p y)))

instance Arity Nary where
   listify (Nary f) = Just . f
   toArity = Nary
   liftIso p (Nary f) = Nary (from p . f . map (to p))