----------------------------------------------------------------------
-- |
-- Module      : Macros
-- Maintainer  : AR
-- Stability   : (stable)
-- Portability : (portable)
--
-- > CVS $Date: 2005/11/11 16:38:00 $
-- > CVS $Author: bringert $
-- > CVS $Revision: 1.24 $
--
-- Macros for constructing and analysing source code terms.
--
-- operations on terms and types not involving lookup in or reference to grammars
--
-- AR 7\/12\/1999 - 9\/5\/2000 -- 4\/6\/2001
-----------------------------------------------------------------------------

module GF.Grammar.Macros where

import GF.Data.Operations
import GF.Data.Str
import GF.Infra.Ident
import GF.Grammar.Grammar
import GF.Grammar.Predef
import GF.Grammar.Printer

import Control.Monad.Identity(Identity(..))
import qualified Data.Traversable as T(mapM)
import qualified Data.Map as Map
import Control.Monad (liftM, liftM2, liftM3, forM)
import Data.List (nub)
import Data.Maybe (fromMaybe)
import Data.Monoid
import Data.Graph
import GF.Text.Pretty(render,(<+>),($$),hsep,fsep,vcat,nest)
import qualified Control.Monad.Fail as Fail

-- ** Functions for constructing and analysing source code terms.

typeForm :: Type -> (Context, Cat, [Term])
typeForm t =
  case t of
    Prod b x a t  ->
      let (x', cat, args) = typeForm t
      in ((b,x,a):x', cat, args)
    App c a ->
      let (_,  cat, args) = typeForm c
      in ([],cat,args ++ [a])
    Q  c -> ([],c,[])
    QC c -> ([],c,[])
    Sort c -> ([],(MN identW, c),[])
    _      -> error (render ("no normal form of type" <+> ppTerm Unqualified 0 t))

typeFormCnc :: Type -> (Context, Type)
typeFormCnc t =
  case t of
    Prod b x a t -> let (x', v) = typeFormCnc t
                    in ((b,x,a):x',v)
    _            -> ([],t)

valCat :: Type -> Cat
valCat typ =
  let (_,cat,_) = typeForm typ
  in cat

valType :: Type -> Type
valType typ =
  let (_,cat,xx) = typeForm typ --- not optimal to do in this way
  in mkApp (Q cat) xx

valTypeCnc :: Type -> Type
valTypeCnc typ = snd (typeFormCnc typ)

typeSkeleton :: Type -> ([(Int,Cat)],Cat)
typeSkeleton typ =
  let (ctxt,cat,_) = typeForm typ
  in ([(length c, v) | (b,x,t) <- ctxt, let (c,v) = typeSkeleton t], cat)

catSkeleton :: Type -> ([Cat],Cat)
catSkeleton typ =
  let (args,val) = typeSkeleton typ
  in (map snd args, val)

funsToAndFrom :: Type -> (Cat, [(Cat,[Int])])
funsToAndFrom t =
  let (cs,v) = catSkeleton t
      cis = zip cs [0..]
  in (v, [(c,[i | (c',i) <- cis, c' == c]) | c <- cs])

isRecursiveType :: Type -> Bool
isRecursiveType t =
  let (cc,c) = catSkeleton t -- thus recursivity on Cat level
  in any (== c) cc

isHigherOrderType :: Type -> Bool
isHigherOrderType t = fromErr True $ do  -- pessimistic choice
  co <- contextOfType t
  return $ not $ null [x | (_,x,Prod _ _ _ _) <- co]

contextOfType :: Monad m => Type -> m Context
contextOfType typ = case typ of
  Prod b x a t -> liftM ((b,x,a):) $ contextOfType t
  _            -> return []

termForm :: Monad m => Term -> m ([(BindType,Ident)], Term, [Term])
termForm t = case t of
   Abs b x t  ->
     do (x', fun, args) <- termForm t
        return ((b,x):x', fun, args)
   App c a ->
     do (_,fun, args) <- termForm c
        return ([],fun,args ++ [a])
   _       ->
     return ([],t,[])

termFormCnc :: Term -> ([(BindType,Ident)], Term)
termFormCnc t = case t of
   Abs b x t  -> ((b,x):xs, t') where (xs,t') = termFormCnc t
   _          -> ([],t)

appForm :: Term -> (Term, [Term])
appForm t = case t of
  App c a   -> (fun, args ++ [a]) where (fun, args) = appForm c
  Typed t _ -> appForm t
  _         -> (t,[])

mkProdSimple :: Context -> Term -> Term
mkProdSimple c t = mkProd c t []

mkProd :: Context -> Term -> [Term] -> Term
mkProd []           typ args = mkApp typ args
mkProd ((b,x,a):dd) typ args = Prod b x a (mkProd dd typ args)

mkTerm :: ([(BindType,Ident)], Term, [Term]) -> Term
mkTerm (xx,t,aa) = mkAbs xx (mkApp t aa)

mkApp :: Term -> [Term] -> Term
mkApp = foldl App

mkAbs :: [(BindType,Ident)] -> Term -> Term
mkAbs xx t = foldr (uncurry Abs) t xx

appCons :: Ident -> [Term] -> Term
appCons = mkApp . Cn

mkLet :: [LocalDef] -> Term -> Term
mkLet defs t = foldr Let t defs

mkLetUntyped :: Context -> Term -> Term
mkLetUntyped defs = mkLet [(x,(Nothing,t)) | (_,x,t) <- defs]

isVariable :: Term -> Bool
isVariable (Vr _ ) = True
isVariable _ = False

-- *** Assignment

assign :: Label -> Term -> Assign
assign l t = (l,(Nothing,t))

assignT :: Label -> Type -> Term -> Assign
assignT l a t = (l,(Just a,t))

unzipR :: [Assign] -> ([Label],[Term])
unzipR r = (ls, map snd ts) where (ls,ts) = unzip r

mkAssign :: [(Label,Term)] -> [Assign]
mkAssign lts = [assign l t | (l,t) <- lts]

projectRec :: Label -> [Assign] -> Term
projectRec l rs =
  case lookup l rs of
    Just (_,t) -> t
    Nothing    -> error (render ("no value for label" <+> l))

zipAssign :: [Label] -> [Term] -> [Assign]
zipAssign ls ts = [assign l t | (l,t) <- zip ls ts]

mapAssignM :: Monad m => (Term -> m c) -> [Assign] -> m [(Label,(Maybe c,c))]
mapAssignM f = mapM (\ (ls,tv) -> liftM ((,) ls) (g tv))
  where g (t,v) = liftM2 (,) (maybe (return Nothing) (liftM Just . f) t) (f v)

mapLabellingM :: Monad m => (Term -> m c) -> [Labelling] -> m [(Label,[Ident],c)]
mapLabellingM f = mapM (\(l,deps,t) -> f t >>= \t -> return (l,deps,t))

mapAttrs :: Monad m => (Term -> m c) -> [(Ident,Term)] -> m [(Ident,c)]
mapAttrs f []          = return []
mapAttrs f ((id,t):as) = do t  <- f t
                            as <- mapAttrs f as
                            return ((id,t):as)
-- *** Records

mkRecordN :: Int -> (Int -> Label) -> [Term] -> Term
mkRecordN int lab typs = R [ assign (lab i) t | (i,t) <- zip [int..] typs]

mkRecord :: (Int -> Label) -> [Term] -> Term
mkRecord = mkRecordN 0

mkRecTypeN :: Int -> (Int -> Label) -> [Type] -> Type
mkRecTypeN int lab typs = RecType [(lab i, [], t) | (i,t) <- zip [int..] typs]

mkRecType :: (Int -> Label) -> [Type] -> Type
mkRecType = mkRecTypeN 0

record2subst :: Term -> Err Substitution
record2subst t = case t of
  R fs -> return [(identC x, t) | (LIdent x,(_,t)) <- fs]
  _    -> Bad (render ("record expected, found" <+> ppTerm Unqualified 0 t))


-- *** Types

typeType, typePType, typeStr, typeTok, typeStrs :: Type

typeType  = Sort cType
typePType = Sort cPType
typeStr   = Sort cStr
typeTok   = Sort cTok
typeStrs  = Sort cStrs

typeString, typeFloat, typeInt :: Type
typeInts :: Integer -> Type
typePBool :: Type
typeError :: Type

typeString = cnPredef cString
typeInt = cnPredef cInt
typeFloat = cnPredef cFloat
typeInts i = App (cnPredef cInts) (EInt i)
typePBool = cnPredef cPBool
typeError = cnPredef cErrorType

isTypeInts :: Type -> Maybe Integer
isTypeInts (App c (EInt i)) | c == cnPredef cInts = Just i
isTypeInts _                                      = Nothing

-- *** Terms

isPredefConstant :: Term -> Bool
isPredefConstant t = case t of
  Q (mod,_) | mod == cPredef || mod == cPredefAbs -> True
  _                                               -> False

cnPredef :: Ident -> Term
cnPredef f = Q (cPredef,f)

mkSelects :: Term -> [Term] -> Term
mkSelects t tt = foldl S t tt

mkTable :: [Term] -> Term -> Term
mkTable tt t = foldr Table t tt

mkCTable :: [(BindType,Ident)] -> Term -> Term
mkCTable ids v = foldr ccase v ids where
  ccase (_,x) t = T TRaw [(PV x,t)]

mkHypo :: Term -> Hypo
mkHypo typ = (Explicit,identW, typ)

eqStrIdent :: Ident -> Ident -> Bool
eqStrIdent = (==)

tuple2record :: [Term] -> [Assign]
tuple2record ts = [assign (tupleLabel i) t | (i,t) <- zip [1..] ts]

tuple2recordType :: [Term] -> [Labelling]
tuple2recordType ts = [(tupleLabel i,[],t) | (i,t) <- zip [1..] ts]

tuple2recordPatt :: [Patt] -> [(Label,Patt)]
tuple2recordPatt ts = [(tupleLabel i, t) | (i,t) <- zip [1..] ts]

mkCases :: Ident -> Term -> Term
mkCases x t = T TRaw [(PV x, t)]

mkWildCases :: Term -> Term
mkWildCases = mkCases identW

mkFunType :: [Type] -> Type -> Type
mkFunType tt t = mkProd [(Explicit,identW, ty) | ty <- tt] t [] -- nondep prod

--plusRecType :: Type -> Type -> Err Type
plusRecType t1 t2 = case (t1, t2) of
  (RecType r1, RecType r2) -> case
    filter (`elem` [l | (l,_,_) <- r1]) [l | (l,_,_) <- r2] of
      [] -> return (RecType (r1 ++ r2))
      ls -> raise $ render ("clashing labels" <+> hsep ls)
  _ -> raise $ render ("cannot add record types" <+> ppTerm Unqualified 0 t1 <+> "and" <+> ppTerm Unqualified 0 t2)

--plusRecord :: Term -> Term -> Err Term
plusRecord t1 t2 =
 case (t1,t2) of
   (R r1, R r2 ) -> return (R ([(l,v) | -- overshadowing of old fields
                              (l,v) <- r1, not (elem l (map fst r2)) ] ++ r2))
   (_,    FV rs) -> mapM (plusRecord t1) rs >>= return . FV
   (FV rs,_    ) -> mapM (`plusRecord` t2) rs >>= return . FV
   _ -> raise $ render ("cannot add records" <+> ppTerm Unqualified 0 t1 <+> "and" <+> ppTerm Unqualified 0 t2)

-- | default linearization type
defLinType :: Type
defLinType = RecType [(theLinLabel, [], typeStr)]

-- | refreshing variables
mkFreshVar :: [Ident] -> Ident -> Ident
mkFreshVar olds x =
  case maximum ((-1) : map (varIndex' rx) olds) + 1 of
    0 -> x
    i -> identV rx i
  where
    rx = ident2raw x

-- | trying to preserve a given symbol
mkFreshVarX :: [Ident] -> Ident -> Ident
mkFreshVarX olds x = if (elem x olds) then (varX (maximum ((-1) : (map varIndex olds)) + 1)) else x

-- *** Almost compositional

-- | to define compositional term functions
composSafeOp :: (Term -> Term) -> Term -> Term
composSafeOp op = runIdentity . composOp (return . op)

-- | to define compositional term functions
composOp :: Monad m => (Term -> m Term) -> Term -> m Term
composOp co trm =
 case trm of
   App c a          -> liftM2 App (co c) (co a)
   Abs b x t        -> liftM (Abs b x) (co t)
   Prod b x a t     -> liftM2 (Prod b x) (co a) (co t)
   S c a            -> liftM2 S (co c) (co a)
   Table a c        -> liftM2 Table (co a) (co c)
   R r              -> liftM R (mapAssignM co r)
   RecType r        -> liftM RecType (mapLabellingM co r)
   P t i            -> liftM2 P (co t) (return i)
   ExtR a c         -> liftM2 ExtR (co a) (co c)
   Opts t os        -> liftM2 Opts (co t) (mapM (\(t1,t2) -> liftM2 (,) (maybe (return Nothing) (liftM Just . co) t1) (co t2)) os)
   T i cc           -> liftM2 (flip T) (mapPairsM co cc) (changeTableType co i)
   V ty vs          -> liftM2 V (co ty) (mapM co vs)
   Let (x,(mt,a)) b -> liftM3 let' (co a) (T.mapM co mt) (co b)
     where let' a' mt' b' = Let (x,(mt',a')) b'
   C s1 s2          -> liftM2 C (co s1) (co s2)
   Glue s1 s2       -> liftM2 Glue (co s1) (co s2)
   Alts t aa        -> liftM2 Alts (co t) (mapM (pairM co) aa)
   FV ts            -> liftM FV (mapM co ts)
   Strs tt          -> liftM Strs (mapM co tt)
   EPattType ty     -> liftM EPattType (co ty)
   ELincat c ty     -> liftM (ELincat c) (co ty)
   ELin c ty        -> liftM (ELin c) (co ty)
   ImplArg t        -> liftM ImplArg (co t)
   Markup t as cs   -> liftM2 (Markup t) (mapAttrs co as) (mapM (mapM co) cs)
   Reset ctl ct t qid->liftM2 (\mb_ct t->Reset ctl ct t qid) (maybe (pure Nothing) (fmap Just . co) ct) (co t)
   Typed t ty       -> liftM2 Typed (co t) (co ty)
   _ -> return trm -- covers K, Vr, Cn, Sort, EPatt

composSafePattOp op = runIdentity . composPattOp (return . op)

composPattOp :: Monad m => (Patt -> m Patt) -> Patt -> m Patt
composPattOp op patt =
  case patt of
    PC c ps         -> liftM  (PC c) (mapM op ps)
    PP qc ps        -> liftM  (PP qc) (mapM op ps)
    PR as           -> liftM  PR (mapPairsM op as)
    PT ty p         -> liftM  (PT ty) (op p)
    PAs x p         -> liftM  (PAs x) (op p)
    PImplArg p      -> liftM  PImplArg (op p)
    PNeg p          -> liftM  PNeg (op p)
    PAlt p1 p2      -> liftM2 PAlt (op p1) (op p2)
    PSeq _ _ p1 _ _ p2  -> liftM2 (\p1 p2 -> PSeq 0 Nothing p1 0 Nothing p2) (op p1) (op p2)
    PRep _ _ p      -> liftM  (PRep 0 Nothing) (op p)
    _               -> return patt -- covers cases without subpatterns

collectOp :: Monoid m => (Term -> m) -> Term -> m
collectOp co trm = case trm of
  App c a      -> co c <> co a
  Abs _ _ b    -> co b
  ImplArg t    -> co t
  Prod _ _ a b -> co a <> co b
  Typed a b    -> co a <> co b
  Example t _  -> co t
  S c a        -> co c <> co a
  Table a c    -> co a <> co c
  ExtR a c     -> co a <> co c
  Opts t os    -> co t <> mconcatMap (\(a,b) -> maybe mempty co a <> co b) os
  R r          -> mconcatMap (\(_,(mt,a)) -> maybe mempty co mt <> co a) r
  RecType r    -> mconcatMap (\(_,_,t) -> co t) r
  P t i        -> co t
  T _ cc       -> mconcatMap (co . snd) cc -- not from patterns --- nor from type annot
  V _ cc       -> mconcatMap co         cc --- nor from type annot
  Let (x,(mt,a)) b -> maybe mempty co mt <> co a <> co b
  C s1 s2      -> co s1 <> co s2
  Glue s1 s2   -> co s1 <> co s2
  EPattType t  -> co t
  Alts t aa    -> let (x,y) = unzip aa in co t <> mconcatMap co (x <> y)
  FV ts        -> mconcatMap co ts
  Strs tt      -> mconcatMap co tt
  ELincat _ t  -> co t
  ELin _ t     -> co t
  Markup t as cs -> mconcatMap (co.snd) as <> mconcatMap (co . unLoc) cs
  Reset _ ct t _-> maybe mempty co ct <> co t
  _            -> mempty -- covers K, Vr, Cn, Sort

mconcatMap f = mconcat . map f

collectPattOp :: (Patt -> [a]) -> Patt -> [a]
collectPattOp op patt =
  case patt of
    PC c ps         -> concatMap op ps
    PP qc ps        -> concatMap op ps
    PR as           -> concatMap (op.snd) as
    PT ty p         -> op p
    PAs x p         -> op p
    PImplArg p      -> op p
    PNeg p          -> op p
    PAlt p1 p2      -> op p1++op p2
    PSeq _ _ p1 _ _ p2 -> op p1++op p2
    PRep _ _ p      -> op p
    _               -> []     -- covers cases without subpatterns


-- *** Misc

-- | to get a string from a term that represents a sequence of terminals
strsFromTerm :: Term -> Err [Str]
strsFromTerm t = case t of
  K s   -> return [str s]
  Empty -> return [str []]
  C s t -> do
    s' <- strsFromTerm s
    t' <- strsFromTerm t
    return [plusStr x y | x <- s', y <- t']
  Glue s t -> do
    s' <- strsFromTerm s
    t' <- strsFromTerm t
    return [glueStr x y | x <- s', y <- t']
  Alts d vs -> do
    d0 <- strsFromTerm d
    v0 <- mapM (strsFromTerm . fst) vs
    c0 <- mapM (strsFromTerm . snd) vs
  --let vs' = zip v0 c0
    return [strTok (str2strings def) vars |
              def  <- d0,
              vars <- [[(str2strings v, map sstr c) | (v,c) <- zip vv c0] |
                                                          vv <- sequence v0]
           ]
  FV ts -> mapM strsFromTerm ts >>= return . concat
  Strs ts -> mapM strsFromTerm ts >>= return . concat
  _ -> raise (render ("cannot get Str from term" <+> ppTerm Unqualified 0 t))

changeTableType :: Monad m => (Type -> m Type) -> TInfo -> m TInfo
changeTableType co i = case i of
    TTyped ty -> co ty >>= return . TTyped
    TComp ty  -> co ty >>= return . TComp
    TWild ty  -> co ty >>= return . TWild
    _ -> return i

-- *** Dependencies

-- | dependency check, detecting circularities and returning topo-sorted list

allDependencies :: (ModuleName -> Bool) -> Map.Map Ident Info -> [(Ident,Info,[Ident])]
allDependencies ism b =
  [(f, i, nub (deps i)) | (f,i) <- Map.toList b]
  where
    opersIn t = case t of
      Q  (n,c) | ism n -> [c]
      QC (n,c) | ism n -> [c]
      EPatt _ _ p -> opersInPatt p
      T _ cs -> mconcatMap (\(p,t) -> opersInPatt p ++ opersIn t) cs
      _ -> collectOp opersIn t

    constrsIn t = case t of
      QC (n,c) | ism n -> [c]
      _ -> collectOp constrsIn t

    opersInPatt p = case p of
      PP (n,c) ps      -> (if ism n then (:)c else id)
                              (concatMap opersInPatt ps)
      PTilde t         -> opersIn t
      PM (n,c) | ism n -> [c]
      _ -> collectPattOp opersInPatt p

    opty (Just (L _ ty)) = opersIn ty
    opty _ = []

    deps i = case i of
      ResOper pty pt -> opty pty ++ opty pt
      ResOverload _ tyts -> concat [opersIn ty ++ opersIn tr | (L _ ty,L _ tr) <- tyts]
      ResParam (Just (L loc ps)) _ -> concat [opersIn  t | (_,cont) <- ps, (_,_,t) <- cont]
      CncCat pty _ _ _ _ -> opty pty
      CncFun _   pt _ _ -> opty pt
      AbsFun pty peqs -> opty pty ++ concat [concatMap opersInPatt ps++constrsIn t | L _ (ps,t) <- maybe [] snd peqs]
      AbsCat (Just (L loc co)) -> concat [opersIn ty | (_,_,ty) <- co]
      _              -> []

topoSortJments :: ErrorMonad m => SourceModule -> m [(Ident,Info)]
topoSortJments (m,mi) = do
  let sccs = stronglyConnComp (map toNode (allDependencies (==m) (jments mi)))
      cycles = [map fst jmts | CyclicSCC jmts <- sccs]
  case cycles of
    [] -> return [jmt | AcyclicSCC jmt <- sccs]
    _  -> raise (render ("circular definitions:" $$
                             nest 3 (vcat (map fsep cycles))))
  where
    toNode (id,info,deps) = ((id,info),id,deps)

mkStrs p = case p of
 PAlt a b -> do
   Strs as <- mkStrs a
   Strs bs <- mkStrs b
   return $ Strs $ as ++ bs
 PSeq _ _ a _ _ b ->
             do Strs as <- mkStrs a
                Strs bs <- mkStrs b
                return $ Strs $ [K (a++b) | K a <- as, K b <- bs]
 PString s -> return $ Strs [K s]
 PChars cs -> return $ Strs [K [c] | c <- cs]
 PV x -> return (Vr x) --- for macros; not yet complete
 PMacro x -> return (Vr x) --- for macros; not yet complete
 PM c -> return (Q c) --- for macros; not yet complete
 _ -> fail "no strs from pattern"
