---------------------------------------------------------------------- -- | -- 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, inferLType, allOperDependencies, topoSortOpers) where import GF.Infra.Ident import GF.Infra.Modules import GF.Compile.Abstract.TypeCheck import GF.Compile.Concrete.TypeCheck 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 Text.PrettyPrint -- | checking is performed in the dependency order of modules checkModule :: [SourceModule] -> SourceModule -> Check SourceModule checkModule ms (name,mo) = checkIn (text "checking module" <+> ppIdent name) $ do let js = jments mo checkRestrictedInheritance ms (name, mo) js' <- case mtype mo of MTAbstract -> checkMap (checkAbsInfo gr name mo) js MTResource -> checkMap (checkResInfo gr name mo) js MTConcrete a -> do checkErr $ topoSortOpers $ allOperDependencies name js abs <- checkErr $ lookupModule gr a js1 <- checkCompleteGrammar gr abs mo checkMap (checkCncInfo gr name mo (a,abs)) js1 MTInterface -> checkMap (checkResInfo gr name mo) js MTInstance a -> do checkMap (checkResInfo gr name mo) js return (name, replaceJudgements mo js') where gr = MGrammar $ (name,mo):ms -- check if restricted inheritance modules are still coherent -- i.e. that the defs of remaining names don't depend on omitted names checkRestrictedInheritance :: [SourceModule] -> SourceModule -> Check () checkRestrictedInheritance mos (name,mo) = do let irs = [ii | ii@(_,mi) <- extend 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 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 -> checkError (text "In inherited module" <+> ppIdent i <> text ", dependence of excluded constants:" $$ nest 2 (vcat [ppIdent f <+> text "on" <+> fsep (map ppIdent is) | (f,is) <- cs])) allDeps = concatMap (allDependencies (const True) . jments . snd) mos checkAbsInfo :: SourceGrammar -> Ident -> SourceModInfo -> Ident -> Info -> Check Info checkAbsInfo st m mo c info = do checkReservedId c case info of AbsCat (Just cont) _ -> mkCheck "category" $ checkContext st cont ---- also cstrs AbsFun (Just typ0) ma md -> do typ <- compAbsTyp [] typ0 -- to calculate let definitions mkCheck "type of function" $ checkTyp st typ case md of Just eqs -> mkCheck "definition of function" $ checkDef st (m,c) typ eqs Nothing -> return info return $ (AbsFun (Just typ) ma md) _ -> return info where mkCheck cat ss = case ss of [] -> return info _ -> checkError (vcat ss $$ text "in" <+> text cat <+> ppIdent c <+> ppPosition mo c) compAbsTyp g t = case t of Vr x -> maybe (checkError (text "no value given to variable" <+> ppIdent 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 checkCompleteGrammar :: SourceGrammar -> SourceModInfo -> SourceModInfo -> Check (BinTree Ident Info) checkCompleteGrammar gr abs cnc = do let jsa = jments abs let fsa = tree2list jsa let jsc = jments cnc let fsc = map fst $ filter (isCnc . snd) $ tree2list jsc -- remove those lincat and lin in concrete that are not in abstract let unkn = filter (not . flip isInBinTree jsa) fsc jsc1 <- if (null unkn) then return jsc else do checkWarn $ text "ignoring constants not in abstract:" <+> fsep (map ppIdent unkn) return $ filterBinTree (\f _ -> notElem f unkn) jsc -- check that all abstract constants are in concrete; build default lincats foldM checkOne jsc1 fsa where isCnc j = case j of CncFun _ _ _ -> True CncCat _ _ _ -> True _ -> False checkOne js i@(c,info) = case info of AbsFun (Just 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 (RecType [])) _ _ -> return (foldr (\_ -> Abs Explicit identW) (R []) cxt) _ -> Bad "no def lin" case lookupIdent c js of Ok (CncFun _ (Just _) _ ) -> return js Ok (CncFun cty Nothing pn) -> case mb_def of Ok def -> return $ updateTree (c,CncFun cty (Just def) pn) js Bad _ -> do checkWarn $ text "no linearization of" <+> ppIdent c return js _ -> do case mb_def of Ok def -> return $ updateTree (c,CncFun Nothing (Just def) Nothing) js Bad _ -> do checkWarn $ text "no linearization of" <+> ppIdent c return js AbsCat (Just _) _ -> case lookupIdent c js of Ok (AnyInd _ _) -> return js Ok (CncCat (Just _) _ _) -> return js Ok (CncCat _ mt mp) -> do checkWarn $ text "no linearization type for" <+> ppIdent c <> text ", inserting default {s : Str}" return $ updateTree (c,CncCat (Just defLinType) mt mp) js _ -> do checkWarn $ text "no linearization type for" <+> ppIdent c <> text ", inserting default {s : Str}" return $ updateTree (c,CncCat (Just defLinType) Nothing Nothing) js _ -> return js -- | General Principle: only Just-values are checked. -- A May-value has always been checked in its origin module. checkResInfo :: SourceGrammar -> Ident -> SourceModInfo -> Ident -> Info -> Check Info checkResInfo gr mo mm c info = do checkReservedId c case info of ResOper pty pde -> chIn "operation" $ do (pty', pde') <- case (pty,pde) of (Just ty, Just de) -> do ty' <- checkLType gr [] ty typeType >>= computeLType gr [] . fst (de',_) <- checkLType gr [] de ty' return (Just ty', Just de') (_ , Just de) -> do (de',ty') <- inferLType gr [] de return (Just ty', Just de') (_ , Nothing) -> do checkError (text "No definition given to the operation") return (ResOper pty' pde') ResOverload os tysts -> chIn "overloading" $ do tysts' <- mapM (uncurry $ flip (checkLType gr [])) tysts -- return explicit ones tysts0 <- checkErr $ lookupOverload gr mo 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 (pcs,_)) -> chIn "parameter type" $ do ts <- checkErr $ lookupParamValues gr mo c return (ResParam (Just (pcs, Just ts))) _ -> return info where chIn cat = checkIn (text "Happened in" <+> text cat <+> ppIdent c <+> ppPosition mm c <+> colon) checkUniq xss = case xss of x:y:xs | x == y -> checkError $ text "ambiguous for type" <+> ppType (mkFunType (tail x) (head x)) | otherwise -> checkUniq $ y:xs _ -> return () checkCncInfo :: SourceGrammar -> Ident -> SourceModInfo -> (Ident,SourceModInfo) -> Ident -> Info -> Check Info checkCncInfo gr m mo (a,abs) c info = do checkReservedId c case info of CncFun _ (Just trm) mpr -> chIn "linearization of" $ do typ <- checkErr $ lookupFunType gr a c let cat0 = valCat typ (cont,val) <- linTypeOfType gr m typ -- creates arg vars (trm',_) <- checkLType gr [] trm (mkFunType (map (\(_,_,ty) -> ty) cont) val) -- erases arg vars checkPrintname gr mpr cat <- return $ snd cat0 return (CncFun (Just (cat,(cont,val))) (Just trm') mpr) -- cat for cf, typ for pe CncCat (Just typ) mdef mpr -> chIn "linearization type of" $ do checkErr $ lookupCatContext gr a c typ' <- computeLType gr [] typ mdef' <- case mdef of Just def -> do (def',_) <- checkLType gr [] def (mkFunType [typeStr] typ) return $ Just def' _ -> return mdef checkPrintname gr mpr return (CncCat (Just typ') mdef' mpr) _ -> checkResInfo gr m mo c info where chIn cat = checkIn (text "Happened in" <+> text cat <+> ppIdent c <+> ppPosition mo c <> colon) checkPrintname :: SourceGrammar -> Maybe Term -> Check () checkPrintname st (Just t) = checkLType st [] t typeStr >> return () checkPrintname _ _ = return () -- | for grammars obtained otherwise than by parsing ---- update!! checkReservedId :: Ident -> Check () checkReservedId x | isReservedWord (ident2bs x) = checkWarn (text "reserved word used as identifier:" <+> ppIdent x) | otherwise = return () -- auxiliaries -- | linearization types and defaults linTypeOfType :: SourceGrammar -> Ident -> 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 checkErr $ errIn (render (text "extending" $$ nest 2 (ppTerm Unqualified 0 vars) $$ text "with" $$ nest 2 (ppTerm Unqualified 0 val))) $ plusRecType vars val return (Explicit,symb,rec) lookLin (_,c) = checks [ --- rather: update with defLinType ? checkErr (lookupLincat cnc m c) >>= computeLType cnc [] ,return defLinType ] -- | dependency check, detecting circularities and returning topo-sorted list allOperDependencies :: Ident -> BinTree Ident Info -> [(Ident,[Ident])] allOperDependencies m = allDependencies (==m) allDependencies :: (Ident -> Bool) -> BinTree Ident Info -> [(Ident,[Ident])] allDependencies ism b = [(f, nub (concatMap opty (pts i))) | (f,i) <- tree2list b] where opersIn t = case t of Q n c | ism n -> [c] QC n c | ism n -> [c] _ -> collectOp opersIn t opty (Just ty) = opersIn ty opty _ = [] pts i = case i of ResOper pty pt -> [pty,pt] ResParam (Just (ps,_)) -> [Just t | (_,cont) <- ps, (_,_,t) <- cont] CncCat pty _ _ -> [pty] CncFun _ pt _ -> [pt] ---- (Maybe (Ident,(Context,Type)) AbsFun pty _ ptr -> [pty] --- ptr is def, which can be mutual AbsCat (Just co) _ -> [Just ty | (_,_,ty) <- co] _ -> [] topoSortOpers :: [(Ident,[Ident])] -> Err [Ident] topoSortOpers st = do let eops = topoTest st either return (\ops -> Bad (render (text "circular definitions:" <+> fsep (map ppIdent (head ops))))) eops