content: ----------------------------------------------------------------------
  -- |
  -- 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 ((<>)) -- GHC 8.4.1 clash with Text.PrettyPrint
  
  import GF.Infra.Ident
  import GF.Infra.Option
  
  import GF.Compile.TypeCheck.Abstract
  import GF.Compile.TypeCheck.RConcrete
  import qualified GF.Compile.TypeCheck.ConcreteNew as CN
  import qualified GF.Compile.Compute.ConcreteNew as CN
  
  import GF.Grammar
  import GF.Grammar.Lexer
  import GF.Grammar.Lookup
  --import GF.Grammar.Predef
  --import GF.Grammar.PatternMatch
  
  import GF.Data.Operations
  import GF.Infra.CheckM
  
  import Data.List
  import qualified Data.Set as Set
  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
    infoss <- checkInModule cwd mi NoLoc empty $ topoSortJments2 mo
    foldM updateCheckInfos mo infoss
    where
      updateCheckInfos mo = fmap (foldl update mo) . parallelCheck . map check
        where check (i,info) = fmap ((,) i) (checkInfo opts cwd sgr mo i info)
      update mo@(m,mi) (i,info) = (m,mi{jments=updateTree (i,info) (jments mi)})
  
  -- 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 = modules sgr
     checkRem ((i,m),mi) = do
       let (incl,excl) = partition (isInherited mi) (map fst (tree2list (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 emptyBinTree (tree2list jsc)
  
    -- check that all abstract constants are in concrete; build default lin and lincats
    jsc <- foldM checkAbs jsc (tree2list 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 $ updateTree (c,CncFun ty (Just def) mn mf) js
                     Ok (CncFun ty Nothing    mn mf) ->
                       case mb_def of
                         Ok def -> return $ updateTree (c,CncFun ty (Just (L NoLoc def)) mn mf) js
                         Bad _  -> do noLinOf c
                                      return js
                     _ -> do
                       case mb_def of
                         Ok def -> do (cont,val) <- linTypeOfType gr cm ty
                                      let linty = (snd (valCat ty),cont,val)
                                      return $ updateTree (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 $ updateTree (c,CncCat (Just (L NoLoc defLinType)) md mr mp mpmcfg) js
           _ -> do
             checkWarn ("no linearization type for" <+> c <> ", inserting default {s : Str}")
             return $ updateTree (c,CncCat (Just (L NoLoc defLinType)) Nothing Nothing Nothing Nothing) js
         _ -> return js
       
     checkCnc js i@(c,info) =
       case info of
         CncFun _ d mn mf -> case lookupOrigInfo gr (am,c) of
                               Ok (_,AbsFun (Just (L _ ty)) _ _ _) -> 
                                          do (cont,val) <- linTypeOfType gr cm ty
                                             let linty = (snd (valCat ty),cont,val)
                                             return $ updateTree (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 _ -> return $ updateTree i js
                               _    -> do checkWarn ("category" <+> c <+> "is not in abstract")
                                          return js
         _                -> return $ updateTree i js
  
  
  -- | General Principle: only Just-values are checked. 
  -- A May-value has always been checked in its origin module.
  checkInfo :: Options -> FilePath -> SourceGrammar -> SourceModule -> Ident -> Info -> Check Info
  checkInfo opts cwd sgr (m,mo) c info = checkInModule cwd mo NoLoc empty $ do
    checkReservedId c
    case info of
      AbsCat (Just (L loc cont)) -> 
        mkCheck loc "the category" $ 
          checkContext gr cont
  
      AbsFun (Just (L loc typ0)) ma md moper -> do
        typ <- compAbsTyp [] typ0   -- to calculate let definitions
        mkCheck loc "the type of function" $
          checkTyp gr typ
        case md of
          Just eqs -> mapM_ (\(L loc eq) -> mkCheck loc "the definition of function" $
  	                                        checkDef gr (m,c) typ eq) eqs
          Nothing  -> return ()
        return (AbsFun (Just (L loc typ)) ma md moper)
  
      CncCat mty mdef mref mpr mpmcfg -> do
        mty  <- case mty of
                  Just (L loc typ) -> chIn loc "linearization type of" $ 
                                       (if False --flag optNewComp opts
                                          then do (typ,_) <- CN.checkLType (CN.resourceValues opts gr) typ typeType
                                                  typ  <- computeLType gr [] typ
                                                  return (Just (L loc typ))
                                          else do (typ,_) <- checkLType gr [] typ typeType
                                                  typ  <- computeLType gr [] 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 gr [] 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 gr [] 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 gr [] t typeStr
                         return (Just (L loc t))
                  _ -> return Nothing
        return (CncCat mty mdef mref mpr mpmcfg)
  
      CncFun mty mt mpr mpmcfg -> do
        mt <- case (mty,mt) of
                (Just (cat,cont,val),Just (L loc trm)) -> 
                    chIn loc "linearization of" $ do
                       (trm,_) <- checkLType gr [] trm (mkFunType (map (\(_,_,ty) -> ty) cont) val)  -- erases arg vars
                       return (Just (L loc trm))
                _ -> return mt
        mpr  <- case mpr of
                  (Just (L loc t)) -> 
                      chIn loc "print name of" $ do
                         (t,_) <- checkLType gr [] t typeStr
                         return (Just (L loc t))
                  _ -> return Nothing
        return (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" $
                           (if False --flag optNewComp opts
                              then CN.checkLType (CN.resourceValues opts gr) ty typeType >>= return . CN.normalForm (CN.resourceValues opts gr) (L loct c) . fst -- !!
                              else checkLType gr [] ty typeType >>= computeLType gr [] . fst)
             (de',_) <- chIn locd "operation" $
                           (if False -- flag optNewComp opts
                              then CN.checkLType (CN.resourceValues opts gr) de ty'
                              else checkLType gr [] de ty')
             return (Just (L loct ty'), Just (L locd de'))
           (Nothing         , Just (L locd de)) -> do
             (de',ty') <- chIn locd "operation" $
                            (if False -- flag optNewComp opts
                              then CN.inferLType (CN.resourceValues opts gr) de
                              else inferLType gr [] 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")
        return (ResOper pty' pde')
  
      ResOverload os tysts -> chIn NoLoc "overloading" $ do
        tysts' <- mapM (uncurry $ flip (\(L loc1 t) (L loc2 ty) -> checkLType gr [] t ty >>= \(t,ty) -> return (L loc1 t, L loc2 ty))) tysts  -- return explicit ones
        tysts0 <- lookupOverload gr (m,c)  -- check against inherited ones too
        tysts1 <- mapM (uncurry $ flip (checkLType gr [])) 
                    [(mkFunType args val,tr) | (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]
        return (ResOverload os [(y,x) | (x,y) <- tysts'])
  
      ResParam (Just (L loc pcs)) _ -> do
        ts <- chIn loc "parameter type" $ 
                liftM concat $ mapM mkPar pcs
        return (ResParam (Just (L loc pcs)) (Just ts))
  
      _ ->  return info
   where
     gr = prependModule sgr (m,mo)
     chIn loc cat = checkInModule cwd mo loc ("Happened in" <+> cat <+> c)
  
     mkPar (f,co) = do
         vs <- liftM combinations $ mapM (\(_,_,ty) -> allParamValues gr ty) co
         return $ map (mkApp (QC (m,f))) vs
  
     checkUniq xss = case xss of
       x:y:xs 
        | x == y    -> checkError $ "ambiguous for type" <+>
                                    ppType (mkFunType (tail x) (head x))  
        | otherwise -> checkUniq $ y:xs
       _ -> return ()
  
     mkCheck loc cat ss = case ss of
       [] -> return info
       _ -> chIn loc cat $ checkError (vcat ss)
  
     compAbsTyp g t = case t of
       Vr x -> maybe (checkError ("no value given to variable" <+> x)) return $ lookup x g
       Let (x,(_,a)) b -> do
         a' <- compAbsTyp g a
         compAbsTyp ((x, a'):g) b
       Prod b x a t -> do
         a' <- compAbsTyp g a
         t' <- compAbsTyp ((x,Vr x):g) t
         return $ Prod b x a' t'
       Abs _ _ _ -> return t
       _ -> composOp (compAbsTyp g) t  
  
  
  -- | for grammars obtained otherwise than by parsing ---- update!!
  checkReservedId :: Ident -> Check ()
  checkReservedId x =
    when (isReservedWord x) $
         checkWarn ("reserved word used as identifier:" <+> x)
  
  -- auxiliaries
  
  -- | linearization types and defaults
  linTypeOfType :: Grammar -> ModuleName -> Type -> Check (Context,Type)
  linTypeOfType cnc m typ = do
    let (cont,cat) = typeSkeleton typ
    val  <- lookLin cat
    args <- mapM mkLinArg (zip [0..] cont)
    return (args, val)
   where
     mkLinArg (i,(n,mc@(m,cat))) = do
       val  <- lookLin mc
       let vars = mkRecType varLabel $ replicate n typeStr
  	 symb = argIdent n cat i
       rec <- if n==0 then return val else
                         errIn (render ("extending" $$
                                        nest 2 vars $$
                                        "with" $$
                                        nest 2 val)) $
                               plusRecType vars val
       return (Explicit,symb,rec)
     lookLin (_,c) = checks [ --- rather: update with defLinType ?
        lookupLincat cnc m c >>= computeLType cnc []
       ,return defLinType
       ]
  