---------------------------------------------------------------------- -- | -- 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 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 ]