---------------------------------------------------------------------- -- | -- 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.Abstract import GF.Compile.TypeCheck.Concrete(checkLType,inferLType) import GF.Compile.Compute.Concrete2(normalForm,Globals(..),stdPredef) 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 (foldM (checkInfo opts cwd sgr)) mo infoss -- 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)) -> mkCheck loc "the category" $ checkContext gr cont AbsFun (Just (L loc typ)) ma md moper -> do mkCheck loc "the type of function" $ checkTyp gr typ typ <- compAbsTyp [] typ -- to calculate let definitions case md of Just eqs -> mapM_ (\(L loc eq) -> mkCheck loc "the definition of function" $ checkDef gr (fst sm,c) typ eq) eqs Nothing -> return () update sm c (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" $ do (typ,_) <- checkLType g typ typeType typ <- normalForm g 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 g 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 g 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 g 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 (_,cat,cont,val),Just (L loc trm)) -> chIn loc "linearization of" $ do (trm,_) <- checkLType g trm (mkFunType (map (\(_,_,ty) -> ty) 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 g 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 g ty typeType normalForm g ty (de',_) <- chIn locd "operation" $ checkLType g de ty' return (Just (L loct ty'), Just (L locd de')) (Nothing , Just (L locd de)) -> do (de',ty') <- chIn locd "operation" $ inferLType g 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 g 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 g 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 g = Gl gr (stdPredef g) 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 g 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 () mkCheck loc cat ss = case ss of [] -> return sm _ -> 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 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)