Syntax.hs

-- 
-- (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.