-- 
-- (C) Susumu Katayama
--
module MagicHaskeller.Analytical.Syntax where

import Control.Monad -- hiding (guard)
import Data.List(nub)

import qualified MagicHaskeller.Types as Types

--
-- Datatypes
--

data IOPair  = IOP { numUniIDs :: Int  -- ^ number of variables quantified with forall
                   , inputs    :: [Expr] -- ^ input example for each argument. The last argument comes first.
                   , output    :: Expr}
             deriving (Show,Eq)

type TBS = [Bool]                 -- ^ the to-be-sought list
data Expr    = E Int -- ^ existential variable. When doing analytical synthesis, there is no functional variable. 
             | U Int -- ^ universal variable. When doing analytical synthesis, there is no functional variable. 
                     --   IntではなくTH.Nameを直接使った方がよい？
             | C {sz :: Int, ctor :: Types.Typed Constr, fields :: [Expr]}
               deriving (Eq, Show)
type Constr  = Int
normalizeMkIOP :: [Expr] -> Expr -> IOPair
normalizeMkIOP ins out = let varIDs = nub $ concatMap vr (out : ins)
                             tup    = zip varIDs [0..]
                         in mapIOP (mapU (\tv -> case lookup tv tup of Just n  -> n)) IOP{numUniIDs = length varIDs, inputs = ins, output = out}
vr (U i)    = [i]
vr (C _ _ es) = concatMap vr es
mapU f (U i) = U $ f i
mapU f (C sz c xs) = C sz c $ map (mapU f) xs

maybeCtor :: Expr -> Maybe (Types.Typed Constr)
maybeCtor (C _ c _) = Just c
maybeCtor _       = Nothing

hasExistential (E _) = True
hasExistential (U _) = False
hasExistential (C _ _ es) = any hasExistential es

visibles tbs ins = [ i | (True,i) <- zip tbs ins ]

--
-- unification
--

type Subst = [(Int,Expr)]


unify (C _ i xs) (C _ j ys) | Types.typee i == Types.typee j = unifyList xs ys
                            | otherwise = mzero
unify e        f        | e==f      = return []
unify (E i)    e        = bind i e
unify e        (E i)    = bind i e
unify _        _        = mzero

unifyList []     []     = return []
unifyList (x:xs) (y:ys) = do s1 <- unify x y
                             s2 <- unifyList (map (apply s1) xs) (map (apply s1) ys)
                             return $ s2 `plusSubst` s1
unifyList _      _      = error "Partial application to a constructor." -- Can this happen?

bind i e | i `occursIn` e = mzero           -- I think permitting infinite data would break the unification algorithm.
         | otherwise      = return [(i,e)]

-- | 'apply' applies a substitution which replaces existential variables to an expression.
apply subst v@(E i)  = maybe v id $ lookup i subst
apply subst v@(U _)  = v
apply subst (C _ i xs) = cap i (map (apply subst) xs) -- 遅いかね

i `occursIn` (E j)    = i==j
i `occursIn` (U _)    = False
i `occursIn` (C _ _ xs) = any (i `occursIn`) xs


plusSubst :: Subst -> Subst -> Subst
s0 `plusSubst` s1 = [(u, apply s0 t) | (u,t) <- s1] ++ s0

emptySubst = []


fresh f e@(E _)      = e
fresh f (U i)    = E $ f i
fresh f (C s c xs) = C s c (map (fresh f) xs)
-- | fusion of @apply s@ and @fresh f@
apfresh s e@(E _)      = e -- NB: this RHS is incorrect if apfresh is used for UniT (because s may include a replacement of e).
apfresh s (U i) = maybe (E i) id $ lookup i s
apfresh s (C _sz c xs) = cap c (map (apfresh s) xs)
mapE f e@(U _)    = e
mapE f (E i)      = E $ f i
mapE f (C s c xs) = C s c (map (mapE f) xs)


-- Note that numUniIDs will not be touched.
applyIOPs s iops = map (applyIOP s) iops
applyIOP s iop = mapIOP (apply s) iop
mapIOP f (IOP bvs ins out) = IOP bvs (map f ins) (f out)
mapTypee f (x Types.::: t) = f x Types.::: t


--
-- termination
--

newtype TermStat = TS {unTS :: [Bool]} deriving Show

initTS :: TermStat
initTS = TS $ replicate (length termCrit) True
updateTS :: [Expr] -> [Expr] -> TermStat -> TermStat
updateTS bkis is (TS bs) = TS $ zipWith (&&) bs [ bkis < is | (<) <- termCrit ]
evalTS :: TermStat -> Bool
evalTS (TS bs) = or bs

-- termination criteria. Enumerate anything that come to your mind. (Should this be an option?)
termCrit :: [[Expr]->[Expr]->Bool]
-- termCrit = [fullyLex, aWise, revFullyLex, revAWise ] -- , linear
--termCrit = [aWise,revAWise]
termCrit = [aWise]

fullyLex, revFullyLex, aWise, revAWise, linear :: [Expr]->[Expr]->Bool
fullyLex   = lessRevListsLex cmpExprs
revFullyLex= lessListsLex cmpExprs
aWise      = lessRevListsLex cmpExprSzs
revAWise   = lessListsLex cmpExprSzs
-- linear is really slow, so is not recommended.
linear ls rs = sum (map size ls) < sum (map size rs)
-- でも，caseでぶった切ったあとのすべての引数を比較しているから遅いのであって，一番最初の段階の引数だけで比較すれば速いのでは？
-- でも，Ackermann's functionで考えると，やっぱそれではダメっぽい．

revArgs :: ([Expr]->[Expr]->Bool) -> [Expr]->[Expr]->Bool
revArgs cmp ls rs = cmp (reverse ls) (reverse rs)

lessRevListsLex cmp  = revArgs (lessListsLex cmp)
lessListsLex cmp []       _        = False -- In general, input arguments of BKs should be shorter, and we have to compare only this length.
lessListsLex cmp (e0:es0) (e1:es1) = case cmp e0 e1 of LT -> True
                                                       EQ -> lessListsLex cmp es0 es1
                                                       GT -> False
cmpExprss []       []       = EQ
cmpExprss []       _        = LT
cmpExprss _        []       = GT
cmpExprss (e0:es0) (e1:es1) = case cmpExprs e0 e1 of EQ -> cmpExprss es0 es1
                                                     c  -> c
cmpExprs (C _ _ fs) (C _ _ gs) = cmpExprss fs gs
cmpExprs _          (C _ _ _)  = LT
cmpExprs (C _ _ _)  _          = GT
cmpExprs _          _          = EQ

cmpExprSzs e0 e1 = compare (size e0) (size e1)
size (C sz _ fs) = sz
size _        = 1 -- questionable?
cap con fs = C (1 + sum (map size fs)) con fs

-- Q: Are existential variables always smaller than constructor applications? A: No, I'm afraid.
-- If we want to make sure the termination, we can always return GT when questionable;
-- if we want to save all questionable expressions, we can always return LT when questionable.