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.Concrete(computeLType,checkLType,inferLType,ppType)
  import qualified GF.Compile.TypeCheck.ConcreteNew as CN(checkLType,inferLType)
  import qualified GF.Compile.Compute.Concrete as CN(normalForm,resourceValues)
  
  import GF.Grammar
  import GF.Grammar.Lexer
  import GF.Grammar.Lookup
  
  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
    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=Map.insert 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.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 (cont,val) <- linTypeOfType gr cm ty
                                      let linty = (snd (valCat ty),cont,val)
                                      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 _ ty)) _ _ _) ->
                                          do (cont,val) <- linTypeOfType gr cm ty
                                             let linty = (snd (valCat ty),cont,val)
                                             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
  
  
  -- | 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 sequence $ 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
       ]
  