----------------------------------------------------------------------
-- |
-- 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 -> Expr -> [Expr]
paraphrase PGF
pgf Expr
t = [Expr] -> [Expr]
forall a. Eq a => [a] -> [a]
nub (Int -> PGF -> Expr -> [Expr]
paraphraseN Int
2 PGF
pgf Expr
t)

paraphraseN :: Int -> PGF -> Expr -> [Expr]
paraphraseN :: Int -> PGF -> Expr -> [Expr]
paraphraseN Int
i PGF
pgf = (Tree -> Expr) -> [Tree] -> [Expr]
forall a b. (a -> b) -> [a] -> [b]
map Tree -> Expr
tree2expr ([Tree] -> [Expr]) -> (Expr -> [Tree]) -> Expr -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> PGF -> Tree -> [Tree]
paraphraseN' Int
i PGF
pgf (Tree -> [Tree]) -> (Expr -> Tree) -> Expr -> [Tree]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Tree
expr2tree

paraphraseN' :: Int -> PGF -> Tree -> [Tree]
paraphraseN' :: Int -> PGF -> Tree -> [Tree]
paraphraseN' Int
0 PGF
_ Tree
t = [Tree
t]
paraphraseN' Int
i PGF
pgf Tree
t = 
  Int -> Tree -> [Tree]
forall a. (Eq a, Num a) => a -> Tree -> [Tree]
step Int
i Tree
t [Tree] -> [Tree] -> [Tree]
forall a. [a] -> [a] -> [a]
++ [CId -> [Tree] -> Tree
Fun CId
g [Tree]
ts' | Fun CId
g [Tree]
ts <- Int -> Tree -> [Tree]
forall a. (Eq a, Num a) => a -> Tree -> [Tree]
step (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) Tree
t, [Tree]
ts' <- [[Tree]] -> [[Tree]]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence ((Tree -> [Tree]) -> [Tree] -> [[Tree]]
forall a b. (a -> b) -> [a] -> [b]
map Tree -> [Tree]
par [Tree]
ts)]
 where
  par :: Tree -> [Tree]
par = Int -> PGF -> Tree -> [Tree]
paraphraseN' (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) PGF
pgf 
  step :: a -> Tree -> [Tree]
step a
0 Tree
t = [Tree
t]
  step a
i Tree
t = let stept :: [Tree]
stept = a -> Tree -> [Tree]
step (a
ia -> a -> a
forall a. Num a => a -> a -> a
-a
1) Tree
t in [Tree]
stept [Tree] -> [Tree] -> [Tree]
forall a. [a] -> [a] -> [a]
++ [[Tree]] -> [Tree]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [Tree -> [Tree]
def Tree
u | Tree
u <- [Tree]
stept]
  def :: Tree -> [Tree]
def = PGF -> Tree -> [Tree]
fromDef PGF
pgf

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

  equsFrom :: CId -> [([Tree], Tree)]
equsFrom CId
f = [([Tree]
ps,Tree
d) | Just [(Tree, Tree)]
equs <- [CId -> [(CId, [(Tree, Tree)])] -> Maybe [(Tree, Tree)]
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup CId
f [(CId, [(Tree, Tree)])]
equss], (Fun CId
_ [Tree]
ps,Tree
d) <- [(Tree, Tree)]
equs]

  equsTo :: CId -> [([Tree], Tree)]
equsTo CId
f  = [([Tree], Tree)
c | (CId
_,[(Tree, Tree)]
equs) <- [(CId, [(Tree, Tree)])]
equss, ([Tree], Tree)
c <- CId -> [(Tree, Tree)] -> [([Tree], Tree)]
forall b. CId -> [(b, Tree)] -> [([Tree], b)]
casesTo CId
f [(Tree, Tree)]
equs]

  casesTo :: CId -> [(b, Tree)] -> [([Tree], b)]
casesTo CId
f [(b, Tree)]
equs = 
    [([Tree]
ps,b
p) | (b
p,d :: Tree
d@(Fun CId
g [Tree]
ps)) <- [(b, Tree)]
equs, CId
gCId -> CId -> Bool
forall a. Eq a => a -> a -> Bool
==CId
f, 
              Tree -> Bool
isClosed Tree
d Bool -> Bool -> Bool
|| ([(b, Tree)] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(b, Tree)]
equs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1 Bool -> Bool -> Bool
&& Tree -> Bool
isLinear Tree
d)]

  equss :: [(CId, [(Tree, Tree)])]
equss = [(CId
f,[(CId -> [Tree] -> Tree
Fun CId
f ((Patt -> Tree) -> [Patt] -> [Tree]
forall a b. (a -> b) -> [a] -> [b]
map Patt -> Tree
patt2tree [Patt]
ps), Expr -> Tree
expr2tree Expr
d) | (Equ [Patt]
ps Expr
d) <- [Equation]
eqs]) | 
                   (CId
f,(Type
_,Int
_,Just ([Equation]
eqs,[[Instr]]
_),Double
_)) <- Map CId (Type, Int, Maybe ([Equation], [[Instr]]), Double)
-> [(CId, (Type, Int, Maybe ([Equation], [[Instr]]), Double))]
forall k a. Map k a -> [(k, a)]
Map.assocs (Abstr -> Map CId (Type, Int, Maybe ([Equation], [[Instr]]), Double)
funs (PGF -> Abstr
abstract PGF
pgf)), Bool -> Bool
not ([Equation] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Equation]
eqs)]
  ---- AR 14/12/2010: (expr2tree d) fails unless we send the variable list from ps in eqs;
  ---- cf. PGF.Tree.expr2tree
  trequ :: p -> p -> p -> Bool
trequ p
s p
f p
e = Bool
True ----trace (s ++ ": " ++ show f ++ "  " ++ show e) True

subst :: Subst -> Tree -> Tree
subst :: Subst -> Tree -> Tree
subst Subst
g Tree
e = case Tree
e of
  Fun CId
f [Tree]
ts -> CId -> [Tree] -> Tree
Fun CId
f ((Tree -> Tree) -> [Tree] -> [Tree]
forall a b. (a -> b) -> [a] -> [b]
map Tree -> Tree
substg [Tree]
ts)
  Var CId
x -> Tree -> (Tree -> Tree) -> Maybe Tree -> Tree
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Tree
e Tree -> Tree
forall a. a -> a
id (Maybe Tree -> Tree) -> Maybe Tree -> Tree
forall a b. (a -> b) -> a -> b
$ CId -> Subst -> Maybe Tree
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup CId
x Subst
g
  Tree
_ -> Tree
e
 where
  substg :: Tree -> Tree
substg = Subst -> Tree -> Tree
subst Subst
g

type Subst = [(CId,Tree)]

-- this applies to pattern, hence don't need to consider abstractions
isClosed :: Tree -> Bool
isClosed :: Tree -> Bool
isClosed Tree
t = case Tree
t of
  Fun CId
_ [Tree]
ts -> (Tree -> Bool) -> [Tree] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Tree -> Bool
isClosed [Tree]
ts
  Var CId
_ -> Bool
False
  Tree
_ -> Bool
True

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


match :: [([Tree],Tree)] -> [Tree] -> [(Tree, Subst)]
match :: [([Tree], Tree)] -> [Tree] -> [(Tree, Subst)]
match [([Tree], Tree)]
cases [Tree]
terms = case [([Tree], Tree)]
cases of
  [] -> []
  ([Tree]
patts,Tree
_):[([Tree], Tree)]
_ | [Tree] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Tree]
patts Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= [Tree] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Tree]
terms -> []
  ([Tree]
patts,Tree
val):[([Tree], Tree)]
cc -> case ((Tree, Tree) -> Maybe Subst) -> [(Tree, Tree)] -> Maybe [Subst]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Tree, Tree) -> Maybe Subst
tryMatch ([Tree] -> [Tree] -> [(Tree, Tree)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Tree]
patts [Tree]
terms) of
     Just [Subst]
substs -> (Tree, Subst) -> [(Tree, Subst)]
forall (m :: * -> *) a. Monad m => a -> m a
return (Tree
val, [Subst] -> Subst
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [Subst]
substs)
     Maybe [Subst]
_           -> [([Tree], Tree)] -> [Tree] -> [(Tree, Subst)]
match [([Tree], Tree)]
cc [Tree]
terms
 where  
  tryMatch :: (Tree, Tree) -> Maybe Subst
tryMatch (Tree
p,Tree
t) = case (Tree
p, Tree
t) of
    (Var CId
x,     Tree
_) | Tree -> Bool
notMeta Tree
t  -> Subst -> Maybe Subst
forall (m :: * -> *) a. Monad m => a -> m a
return [(CId
x,Tree
t)]
    (Fun CId
p [Tree]
pp, Fun CId
f [Tree]
tt) | CId
p CId -> CId -> Bool
forall a. Eq a => a -> a -> Bool
== CId
f Bool -> Bool -> Bool
&& [Tree] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Tree]
pp Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Tree] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Tree]
tt -> do
         [Subst]
matches <- ((Tree, Tree) -> Maybe Subst) -> [(Tree, Tree)] -> Maybe [Subst]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Tree, Tree) -> Maybe Subst
tryMatch ([Tree] -> [Tree] -> [(Tree, Tree)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Tree]
pp [Tree]
tt)
         Subst -> Maybe Subst
forall (m :: * -> *) a. Monad m => a -> m a
return ([Subst] -> Subst
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [Subst]
matches)
    (Tree, Tree)
_ -> if Tree
pTree -> Tree -> Bool
forall a. Eq a => a -> a -> Bool
==Tree
t then Subst -> Maybe Subst
forall (m :: * -> *) a. Monad m => a -> m a
return [] else Maybe Subst
forall a. Maybe a
Nothing

  notMeta :: Tree -> Bool
notMeta Tree
e = case Tree
e of
    Meta Int
_   -> Bool
False
    Fun CId
f [Tree]
ts -> (Tree -> Bool) -> [Tree] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Tree -> Bool
notMeta [Tree]
ts  
    Tree
_ -> Bool
True

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