summaryrefslogtreecommitdiff
path: root/src/compiler/GF/Compile/CheckGrammar.hs
diff options
context:
space:
mode:
authorkrasimir <krasimir@chalmers.se>2009-12-13 18:50:29 +0000
committerkrasimir <krasimir@chalmers.se>2009-12-13 18:50:29 +0000
commitf85232947e74ee7ef8c7b0ad2338212e7e68f1be (patch)
tree667b886a5e3a4b026a63d4e3597f32497d824761 /src/compiler/GF/Compile/CheckGrammar.hs
parentd88a865faff59c98fc91556ff8700b10ee5f2df8 (diff)
reorganize the directories under src, and rescue the JavaScript interpreter from deprecated
Diffstat (limited to 'src/compiler/GF/Compile/CheckGrammar.hs')
-rw-r--r--src/compiler/GF/Compile/CheckGrammar.hs284
1 files changed, 284 insertions, 0 deletions
diff --git a/src/compiler/GF/Compile/CheckGrammar.hs b/src/compiler/GF/Compile/CheckGrammar.hs
new file mode 100644
index 000000000..f4765eb26
--- /dev/null
+++ b/src/compiler/GF/Compile/CheckGrammar.hs
@@ -0,0 +1,284 @@
+----------------------------------------------------------------------
+-- |
+-- 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.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 m@(name,mo) = checkIn (text "checking module" <+> ppIdent name) $ do
+ checkRestrictedInheritance ms m
+ m <- case mtype mo of
+ MTConcrete a -> do let gr = MGrammar (m:ms)
+ abs <- checkErr $ lookupModule gr a
+ checkCompleteGrammar gr (a,abs) m
+ _ -> return m
+ infos <- checkErr $ topoSortJments m
+ foldM updateCheckInfo m infos
+ where
+ updateCheckInfo (name,mo) (i,info) = do
+ info <- checkInfo ms (name,mo) i info
+ return (name,updateModule mo i info)
+
+-- 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
+
+checkCompleteGrammar :: SourceGrammar -> SourceModule -> SourceModule -> Check SourceModule
+checkCompleteGrammar gr (am,abs) (cm,cnc) = 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,replaceJudgements cnc jsc)
+ where
+ checkAbs 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 (AnyInd _ _) -> return js
+ Ok (CncFun ty (Just def) pn) ->
+ return $ updateTree (c,CncFun ty (Just def) pn) js
+ Ok (CncFun ty Nothing pn) ->
+ case mb_def of
+ Ok def -> return $ updateTree (c,CncFun ty (Just def) pn) js
+ Bad _ -> do checkWarn $ text "no linearization of" <+> ppIdent 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 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
+
+ checkCnc js i@(c,info) =
+ case info of
+ CncFun _ d pn -> case lookupOrigInfo gr am c of
+ Ok (_,AbsFun (Just ty) _ _) ->
+ do (cont,val) <- linTypeOfType gr cm ty
+ let linty = (snd (valCat ty),cont,val)
+ return $ updateTree (c,CncFun (Just linty) d pn) js
+ _ -> do checkWarn $ text "function" <+> ppIdent c <+> text "is not in abstract"
+ return js
+ CncCat _ _ _ -> case lookupOrigInfo gr am c of
+ Ok _ -> return $ updateTree i js
+ _ -> do checkWarn $ text "category" <+> ppIdent c <+> text "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 :: [SourceModule] -> SourceModule -> Ident -> Info -> Check Info
+checkInfo ms (m,mo) c info = do
+ checkReservedId c
+ case info of
+ AbsCat (Just cont) _ -> mkCheck "category" $
+ checkContext gr cont
+
+ AbsFun (Just typ0) ma md -> do
+ typ <- compAbsTyp [] typ0 -- to calculate let definitions
+ mkCheck "type of function" $
+ checkTyp gr typ
+ case md of
+ Just eqs -> mkCheck "definition of function" $
+ checkDef gr (m,c) typ eqs
+ Nothing -> return info
+ return (AbsFun (Just typ) ma md)
+
+ CncFun linty@(Just (cat,cont,val)) (Just trm) mpr -> chIn "linearization of" $ do
+ (trm',_) <- checkLType gr [] trm (mkFunType (map (\(_,_,ty) -> ty) cont) val) -- erases arg vars
+ mpr <- checkPrintname gr mpr
+ return (CncFun linty (Just trm') mpr)
+
+ CncCat (Just typ) mdef mpr -> chIn "linearization type of" $ do
+ (typ,_) <- checkLType gr [] typ typeType
+ typ <- computeLType gr [] typ
+ mdef <- case mdef of
+ Just def -> do
+ (def,_) <- checkLType gr [] def (mkFunType [typeStr] typ)
+ return $ Just def
+ _ -> return mdef
+ mpr <- checkPrintname gr mpr
+ return (CncCat (Just typ) mdef mpr)
+
+ 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 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 pcs) _ -> chIn "parameter type" $ do
+ ts <- checkErr $ liftM concat $ mapM mkPar pcs
+ return (ResParam (Just pcs) (Just ts))
+
+ _ -> return info
+ where
+ gr = MGrammar ((m,mo) : ms)
+ chIn cat = checkIn (text "Happened in" <+> text cat <+> ppIdent c <+> ppPosition mo c <> colon)
+
+ 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 $ text "ambiguous for type" <+>
+ ppType (mkFunType (tail x) (head x))
+ | otherwise -> checkUniq $ y:xs
+ _ -> return ()
+
+ 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
+
+
+checkPrintname :: SourceGrammar -> Maybe Term -> Check (Maybe Term)
+checkPrintname gr (Just t) = do (t,_) <- checkLType gr [] t typeStr
+ return (Just t)
+checkPrintname gr Nothing = return Nothing
+
+-- | 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
+ ]