----------------------------------------------------------------------
-- |
-- Module      : CheckGrammar
-- Maintainer  : AR
-- Stability   : (stable)
-- Portability : (portable)
--
-- > CVS $Date: 2005/11/11 23:24:33 $
-- > CVS $Author: aarne $
-- > CVS $Revision: 1.31 $
--
-- AR 4\/12\/1999 -- 1\/4\/2000 -- 8\/9\/2001 -- 15\/5\/2002 -- 27\/11\/2002 -- 18\/6\/2003
--
-- type checking also does the following modifications:
--
--  - types of operations and local constants are inferred and put in place
--
--  - both these types and linearization types are computed
--
--  - tables are type-annotated
-----------------------------------------------------------------------------

module GF.Compile.CheckGrammar(checkModule) where

import Prelude hiding ((<>))
import GF.Infra.Ident
import GF.Infra.Option

import GF.Compile.TypeCheck(checkLType,inferLType,checkContext,checkDef)
import GF.Compile.Compute(normalForm,Globals(..),noPredef,stdPredef)

import GF.Grammar
import GF.Grammar.Lexer
import GF.Grammar.Lookup
import GF.Grammar.Lockfield

import GF.Data.Operations
import GF.Infra.CheckM

import Data.List
import qualified Data.Set as Set
import qualified Data.Map as Map
import Control.Monad
import GF.Text.Pretty

-- | checking is performed in the dependency order of modules
checkModule :: Options -> FilePath -> SourceGrammar -> SourceModule -> Check SourceModule
checkModule opts cwd sgr mo@(m,mi) = do
  checkRestrictedInheritance cwd sgr mo
  mo <- case mtype mi of
          MTConcrete a -> do let gr = prependModule sgr mo
                             abs <- lookupModule gr a
                             checkCompleteGrammar opts cwd gr (a,abs) mo
          _            -> return mo
  infos <- checkInModule cwd mi NoLoc empty $ topoSortJments mo
  foldM (checkInfo opts cwd sgr) mo infos

-- check if restricted inheritance modules are still coherent
-- i.e. that the defs of remaining names don't depend on omitted names
checkRestrictedInheritance :: FilePath -> SourceGrammar -> SourceModule -> Check ()
checkRestrictedInheritance cwd sgr (name,mo) = checkInModule cwd mo NoLoc empty $ do
  let irs = [ii | ii@(_,mi) <- mextend mo, mi /= MIAll]  -- names with restr. inh.
  let mrs = [((i,m),mi) | (i,m) <- mos, Just mi <- [lookup i irs]]
                             -- the restr. modules themself, with restr. infos
  mapM_ checkRem mrs
 where
   mos = [mo | mo@(_,ModInfo{}) <- modules sgr]
   checkRem ((i,m),mi) = do
     let (incl,excl) = partition (isInherited mi) (Map.keys (jments m))
     let incld c   = Set.member c (Set.fromList incl)
     let illegal c = Set.member c (Set.fromList excl)
     let illegals = [(f,is) |
           (f,_,cs) <- allDeps, incld f, let is = filter illegal cs, not (null is)]
     case illegals of
       [] -> return ()
       cs -> checkWarn ("In inherited module" <+> i <> ", dependence of excluded constants:" $$
                         nest 2 (vcat [f <+> "on" <+> fsep is | (f,is) <- cs]))
   allDeps = concatMap (allDependencies (const True) . jments . snd) mos

checkCompleteGrammar :: Options -> FilePath -> Grammar -> Module -> Module -> Check Module
checkCompleteGrammar opts cwd gr (am,abs) (cm,cnc) = checkInModule cwd cnc NoLoc empty $ do
  let jsa = jments abs
  let jsc = jments cnc

  -- check that all concrete constants are in abstract; build types for all lin
  jsc <- foldM checkCnc Map.empty (Map.toList jsc)

  -- check that all abstract constants are in concrete; build default lin and lincats
  jsc <- foldM checkAbs jsc (Map.toList jsa)

  return (cm,cnc{jments=jsc})
  where
   checkAbs js i@(c,info) =
     case info of
       AbsFun (Just (L loc ty)) _
           -> do let mb_def = do
                       let (cxt,(_,i),_) = typeForm ty
                       info <- lookupIdent i js
                       info <- case info of
                                 (AnyInd _ m) -> do (m,info) <- lookupOrigInfo gr (m,i)
                                                    return info
                                 _            -> return info
                       case info of
                         CncCat (Just (L loc (RecType []))) _ _ _ _ -> return (foldr (\_ -> Abs Explicit identW) (R []) cxt)
                         _                                          -> Bad "no def lin"

                 case lookupIdent c js of
                   Ok (AnyInd _ _) -> return js
                   Ok (CncFun ty (Just def) mn mf) ->
                                 return $ Map.insert c (CncFun ty (Just def) mn mf) js
                   Ok (CncFun ty Nothing    mn mf) ->
                     case mb_def of
                       Ok def -> return $ Map.insert c (CncFun ty (Just (L NoLoc def)) mn mf) js
                       Bad _  -> do noLinOf c
                                    return js
                   _ -> do
                     case mb_def of
                       Ok def -> do linty <- linTypeOfType gr cm (L loc ty)
                                    return $ Map.insert c (CncFun (Just linty) (Just (L NoLoc def)) Nothing Nothing) js
                       Bad _  -> do noLinOf c
                                    return js
         where noLinOf c = checkWarn ("no linearization of" <+> c)
       AbsCat (Just _) -> case lookupIdent c js of
         Ok (AnyInd _ _) -> return js
         Ok (CncCat (Just _) _ _ _ _) -> return js
         Ok (CncCat Nothing md mr mp mpmcfg) -> do
           checkWarn ("no linearization type for" <+> c <> ", inserting default {s : Str}")
           return $ Map.insert c (CncCat (Just (L NoLoc defLinType)) md mr mp mpmcfg) js
         _ -> do
           checkWarn ("no linearization type for" <+> c <> ", inserting default {s : Str}")
           return $ Map.insert c (CncCat (Just (L NoLoc defLinType)) Nothing Nothing Nothing Nothing) js
       _ -> return js

   checkCnc js (c,info) =
     case info of
       CncFun _ d mn mf -> case lookupOrigInfo gr (am,c) of
                             Ok (_,AbsFun (Just (L loc ty)) _) ->
                                        do linty <- linTypeOfType gr cm (L loc ty)
                                           return $ Map.insert c (CncFun (Just linty) d mn mf) js
                             _       -> do checkWarn ("function" <+> c <+> "is not in abstract")
                                           return js
       CncCat {} ->
         case lookupOrigInfo gr (am,c) of
           Ok (_,AbsCat _) -> return $ Map.insert c info js
           {- -- This might be too pedantic:
           Ok (_,AbsFun {}) ->
                   checkError ("lincat:"<+>c<+>"is a fun, not a cat")
           -}
           _ -> do checkWarn ("category" <+> c <+> "is not in abstract")
                   return js

       _ -> return $ Map.insert c info js

checkInfo :: Options -> FilePath -> SourceGrammar -> SourceModule -> (Ident,Info) -> Check SourceModule
checkInfo opts cwd sgr sm (c,info) = checkInModule cwd (snd sm) NoLoc empty $ do
  checkReservedId c
  case info of
    AbsCat (Just (L loc cont)) ->
      chIn loc "the category" $ do
        cont <- checkContext ga cont
        update sm c (AbsCat (Just (L loc cont)))

    AbsFun (Just (L loc typ)) md -> do
      (typ,_) <- chIn loc "the type of function" $
                   checkLType ga typ typeType
      typ <- normalForm ga typ   -- to calculate let definitions
      sm <- update sm c (AbsFun (Just (L loc typ)) md)
      let gr' = prependModule sgr sm
          ga' = Gl gr' noPredef True
      md <- case md of
              Just (_,eqs) -> do eqs <- mapM (\(L loc eq) -> chIn loc "the definition of function" $
                                                            fmap (L loc) (checkDef ga (fst sm,c) typ eq)) eqs
                                 arity <-
                                    case [length ps | L _ (ps,_) <- eqs] of
                                      []                   -> return 0
                                      (arity : as) 
                                        | all (==arity) as -> return arity
                                      _ -> checkError ("The following equations have different arities" $$
                                                       nest 4 (vcat [ppQIdent Unqualified (fst sm,c) <+> hsep (map (ppPatt Unqualified 2) ps) | L _ (ps,_) <- eqs]))
                                 return (Just (arity,eqs))
              Nothing  -> return Nothing
      update sm c (AbsFun (Just (L loc typ)) md)

    CncCat mty mdef mref mpr mpmcfg -> do
      mty  <- case mty of
                Just (L loc typ) -> chIn loc "linearization type of" $ do
                                      (typ,_) <- checkLType gc typ typeType
                                      typ  <- normalForm gc typ
                                      return (Just (L loc typ))
                Nothing          -> return Nothing
      mdef <- case (mty,mdef) of
                (Just (L _ typ),Just (L loc def)) ->
                    chIn loc "default linearization of" $ do
                       (def,_) <- checkLType gc def (mkFunType [typeStr] typ)
                       return (Just (L loc def))
                _ -> return Nothing
      mref <- case (mty,mref) of
                (Just (L _ typ),Just (L loc ref)) ->
                    chIn loc "reference linearization of" $ do
                       (ref,_) <- checkLType gc ref (mkFunType [typ] typeStr)
                       return (Just (L loc ref))
                _ -> return Nothing
      mpr  <- case mpr of
                (Just (L loc t)) ->
                    chIn loc "print name of" $ do
                       (t,_) <- checkLType gc t typeStr
                       return (Just (L loc t))
                _ -> return Nothing
      update sm c (CncCat mty mdef mref mpr mpmcfg)

    CncFun mty mt mpr mpmcfg -> do
      mt <- case (mty,mt) of
              (Just (args,cat,cont,val),Just (L loc trm)) ->
                  chIn loc "linearization of" $ do
                     (trm,_) <- checkLType gc trm (mkFunType (zipWith (\cat (_,_,ty) -> lock cat ty) args cont) val)  -- erases arg vars
                     return (Just (L loc (etaExpand [] trm cont)))
              _ -> return mt
      mpr  <- case mpr of
                (Just (L loc t)) ->
                    chIn loc "print name of" $ do
                       (t,_) <- checkLType gc t typeStr
                       return (Just (L loc t))
                _ -> return Nothing
      update sm c (CncFun mty mt mpr mpmcfg)

    ResOper pty pde -> do
      (pty', pde') <- case (pty,pde) of
         (Just (L loct ty), Just (L locd de)) -> do
           ty'     <- chIn loct "operation" $ do
                         (ty,_) <- checkLType gc ty typeType
                         normalForm gc ty
           (de',_) <- chIn locd "operation" $
                         checkLType gc de ty'
           return (Just (L loct ty'), Just (L locd de'))
         (Nothing         , Just (L locd de)) -> do
           (de',ty') <- chIn locd "operation" $
                          inferLType gc de
           return (Just (L locd ty'), Just (L locd de'))
         (Just (L loct ty), Nothing) -> do
           chIn loct "operation" $
             checkError (pp "No definition given to the operation")
      update sm c (ResOper pty' pde')

    ResOverload os tysts -> chIn NoLoc "overloading" $ do
      tysts' <- mapM (uncurry $ flip (\(L loc1 t) (L loc2 ty) -> checkLType gc t ty >>= \(t,ty) -> return (L loc1 t, L loc2 ty))) tysts  -- return explicit ones
      tysts0 <- lookupOverload gr (fst sm,c)  -- check against inherited ones too
      tysts1 <- sequence
                  [checkLType gc tr (mkFunType args val) | (args,(val,tr)) <- tysts0]
      --- this can only be a partial guarantee, since matching
      --- with value type is only possible if expected type is given
      --checkUniq $
      --  sort [let (xs,t) = typeFormCnc x in t : map (\(b,x,t) -> t) xs | (_,x) <- tysts1]
      update sm c (ResOverload os [(y,x) | (x,y) <- tysts'])

    ResParam (Just (L loc pcs)) _ -> do
      (sm,cnt,ts,pcs) <- chIn loc "parameter type" $
                            mkParamValues sm c 0 [] pcs
      update sm c (ResParam (Just (L loc pcs)) (Just (ts,cnt)))

    _ ->  return sm
 where
   gr = prependModule sgr sm
   ga = Gl gr noPredef True
   gc = Gl gr (stdPredef gc) False
   chIn loc cat = checkInModule cwd (snd sm) loc ("Happened in" <+> cat <+> c)

   mkParamValues sm         c cnt ts []           = return (sm,cnt,[],[])
   mkParamValues sm@(mn,mi) c cnt ts ((p,co):pcs) = do
     co <- mapM (\(b,v,ty) -> normalForm gc ty >>= \ty -> return (b,v,ty)) co
     sm <- case lookupIdent p (jments mi) of
             Ok (ResValue (L loc _) _) -> update sm p (ResValue (L loc (mkProdSimple co (QC (mn,c)))) cnt)
             Bad msg                   -> checkError (pp msg)
     vs <- liftM sequence $ mapM (\(_,_,ty) -> allParamValues gr ty) co
     (sm,cnt,ts,pcs) <- mkParamValues sm c (cnt+length vs) ts pcs
     return (sm,cnt,map (mkApp (QC (mn,p))) vs ++ ts,(p,co):pcs)

   checkUniq xss = case xss of
     x:y:xs
      | x == y    -> checkError $ "ambiguous for type" <+>
                                  ppTerm Terse 0 (mkFunType (tail x) (head x))
      | otherwise -> checkUniq $ y:xs
     _ -> return ()

   etaExpand xs t            []               = t
   etaExpand xs (Abs bt x t) (_        :cont) = Abs bt x (etaExpand (x:xs) t              cont)
   etaExpand xs t            ((bt,_,ty):cont) = Abs bt x (etaExpand (x:xs) (App t (Vr x)) cont)
     where
       x = freeVar 1 xs

       freeVar i xs
         | elem x xs = freeVar (i+1) xs
         | otherwise = x
         where
           x = identS ("v"++show i)

   update (mn,mi) c info = return (mn,mi{jments=Map.insert c info (jments mi)})


-- | for grammars obtained otherwise than by parsing ---- update!!
checkReservedId :: Ident -> Check ()
checkReservedId x =
  when (isReservedWord GF x) $
       checkWarn ("reserved word used as identifier:" <+> x)

-- auxiliaries

-- | linearization types and defaults
linTypeOfType :: Grammar -> ModuleName -> L Type -> Check ([Ident],Ident,Context,Type)
linTypeOfType cnc m (L loc typ) = do
  let (ctxt,res_cat) = typeSkeleton typ
  val <- lookLin res_cat
  lin_args <- mapM mkLinArg (zip [1..] ctxt)
  let (args,arg_cats) = unzip lin_args
  return (arg_cats, snd res_cat, args, val)
 where
   mkLinArg (i,(n,mc@(m,cat))) = do
     val  <- lookLin mc
     let vars = mkRecType varLabel $ replicate n typeStr
     rec <- if n==0 then return val else
                       errIn (render ("extending" $$
                                      nest 2 vars $$
                                      "with" $$
                                      nest 2 val)) $
                             plusRecType vars val
     return ((Explicit,varX i,rec),cat)
   lookLin (_,c) = checks [ --- rather: update with defLinType ?
      lookupLincat cnc m c >>= normalForm g
     ,return defLinType
     ]
   g = Gl cnc (stdPredef g) False
