----------------------------------------------------------------------
-- |
-- Module      : Paraphrase
-- Maintainer  : AR
-- Stability   : (stable)
-- Portability : (portable)
--
-- Generate parapharases with def definitions.
-----------------------------------------------------------------------------

module PGF.Paraphrase (
  paraphrase,
  paraphraseN
  ) where

import PGF.Data
import PGF.Tree
--import PGF.Macros (lookDef,isData)
--import PGF.CId

import Data.List (nub,sort,group)
import qualified Data.Map as Map

--import Debug.Trace ----

paraphrase :: PGF -> Expr -> [Expr]
paraphrase pgf t = nub (paraphraseN 2 pgf t)

paraphraseN :: Int -> PGF -> Expr -> [Expr]
paraphraseN i pgf = map tree2expr . paraphraseN' i pgf . expr2tree

paraphraseN' :: Int -> PGF -> Tree -> [Tree]
paraphraseN' 0 _ t = [t]
paraphraseN' i pgf t = 
  step i t ++ [Fun g ts' | Fun g ts <- step (i-1) t, ts' <- sequence (map par ts)]
 where
  par = paraphraseN' (i-1) pgf 
  step 0 t = [t]
  step i t = let stept = step (i-1) t in stept ++ concat [def u | u <- stept]
  def = fromDef pgf

fromDef :: PGF -> Tree -> [Tree]
fromDef pgf t@(Fun f ts) = defDown t ++ defUp t where
  defDown t = [subst g u | let equ = equsFrom f, (u,g) <- match equ ts, trequ "U" f equ]
  defUp   t = [subst g u | equ <- equsTo   f, (u,g) <- match [equ] ts, trequ "D" f equ]

  equsFrom f = [(ps,d) | Just equs <- [lookup f equss], (Fun _ ps,d) <- equs]

  equsTo f  = [c | (_,equs) <- equss, c <- casesTo f equs]

  casesTo f equs = 
    [(ps,p) | (p,d@(Fun g ps)) <- equs, g==f, 
              isClosed d || (length equs == 1 && isLinear d)]

  equss = [(f,[(Fun f (map patt2tree ps), expr2tree d) | (Equ ps d) <- eqs]) | 
                   (f,(_,_,Just (eqs,_),_)) <- Map.assocs (funs (abstract pgf)), not (null eqs)]
  ---- AR 14/12/2010: (expr2tree d) fails unless we send the variable list from ps in eqs;
  ---- cf. PGF.Tree.expr2tree
  trequ s f e = True ----trace (s ++ ": " ++ show f ++ "  " ++ show e) True

subst :: Subst -> Tree -> Tree
subst g e = case e of
  Fun f ts -> Fun f (map substg ts)
  Var x -> maybe e id $ lookup x g
  _ -> e
 where
  substg = subst g

type Subst = [(CId,Tree)]

-- this applies to pattern, hence don't need to consider abstractions
isClosed :: Tree -> Bool
isClosed t = case t of
  Fun _ ts -> all isClosed ts
  Var _ -> False
  _ -> True

-- this applies to pattern, hence don't need to consider abstractions
isLinear :: Tree -> Bool
isLinear = nodup . vars where
  vars t = case t of
    Fun _ ts -> concatMap vars ts
    Var x -> [x]
    _ -> []
  nodup = all ((<2) . length) . group . sort


match :: [([Tree],Tree)] -> [Tree] -> [(Tree, Subst)]
match cases terms = case cases of
  [] -> []
  (patts,_):_ | length patts /= length terms -> []
  (patts,val):cc -> case mapM tryMatch (zip patts terms) of
     Just substs -> return (val, concat substs)
     _           -> match cc terms
 where  
  tryMatch (p,t) = case (p, t) of
    (Var x,     _) | notMeta t  -> return [(x,t)]
    (Fun p pp, Fun f tt) | p == f && length pp == length tt -> do
         matches <- mapM tryMatch (zip pp tt)
         return (concat matches)
    _ -> if p==t then return [] else Nothing

  notMeta e = case e of
    Meta _   -> False
    Fun f ts -> all notMeta ts  
    _ -> True

-- | Converts a pattern to tree.
patt2tree :: Patt -> Tree
patt2tree (PApp f ps) = Fun f (map patt2tree ps)
patt2tree (PLit l)    = Lit l
patt2tree (PVar x)    = Var x
patt2tree PWild       = Meta 0