GitHub/gf-core
1
0
Fork 1
mirror of https://github.com/GrammaticalFramework/gf-core.git synced 2026-04-23 19:42:50 -06:00
Code Issues Packages Projects Releases Wiki Activity

small refactoring in GF.Compile.CheckGrammar

Browse Source
This commit is contained in:
krasimir
2009-10-25 15:20:44 +00:00
parent 116912647b
commit d63be8ac72
4 changed files with 80 additions and 109 deletions
Download Patch File Download Diff File Expand all files Collapse all files

175
src/GF/Compile/CheckGrammar.hs
View File

@@ -45,28 +45,17 @@ import Text.PrettyPrint
-- | checking is performed in the dependency order of modules -- | checking is performed in the dependency order of modules
checkModule :: [SourceModule] -> SourceModule -> Check SourceModule checkModule :: [SourceModule] -> SourceModule -> Check SourceModule
checkModule ms (name,mo) = checkIn (text "checking module" <+> ppIdent name) $ do checkModule ms m@(name,mo) = checkIn (text "checking module" <+> ppIdent name) $ do
let js = jments mo checkRestrictedInheritance ms m
checkRestrictedInheritance ms (name, mo) js <- case mtype mo of
js' <- case mtype mo of MTConcrete a -> do checkErr $ topoSortOpers $ allOperDependencies name (jments mo)
MTAbstract -> checkMap (checkAbsInfo gr name mo) js abs <- checkErr $ lookupModule gr a
checkCompleteGrammar gr (a,abs) m
MTResource -> checkMap (checkResInfo gr name mo) js _ -> return (jments mo)
js <- checkMap (checkInfo gr m) js
MTConcrete a -> do return (name, replaceJudgements mo js)
checkErr $ topoSortOpers $ allOperDependencies name js where
abs <- checkErr $ lookupModule gr a gr = MGrammar $ (name,mo):ms
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 -- check if restricted inheritance modules are still coherent
-- i.e. that the defs of remaining names don't depend on omitted names -- i.e. that the defs of remaining names don't depend on omitted names
@@ -89,42 +78,8 @@ checkRestrictedInheritance mos (name,mo) = do
nest 2 (vcat [ppIdent f <+> text "on" <+> fsep (map ppIdent is) | (f,is) <- cs])) nest 2 (vcat [ppIdent f <+> text "on" <+> fsep (map ppIdent is) | (f,is) <- cs]))
allDeps = concatMap (allDependencies (const True) . jments . snd) mos allDeps = concatMap (allDependencies (const True) . jments . snd) mos
checkAbsInfo :: checkCompleteGrammar :: SourceGrammar -> SourceModule -> SourceModule -> Check (BinTree Ident Info)
SourceGrammar -> Ident -> SourceModInfo -> Ident -> Info -> Check Info checkCompleteGrammar gr (am,abs) (cm,cnc) = do
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 jsa = jments abs
let fsa = tree2list jsa let fsa = tree2list jsa
let jsc = jments cnc let jsc = jments cnc
@@ -154,16 +109,21 @@ checkCompleteGrammar gr abs cnc = do
case info of case info of
CncCat (Just (RecType [])) _ _ -> return (foldr (\_ -> Abs Explicit identW) (R []) cxt) CncCat (Just (RecType [])) _ _ -> return (foldr (\_ -> Abs Explicit identW) (R []) cxt)
_ -> Bad "no def lin" _ -> Bad "no def lin"
(cont,val) <- linTypeOfType gr cm ty
let linty = (snd (valCat ty),cont,val)
case lookupIdent c js of case lookupIdent c js of
Ok (CncFun _ (Just _) _ ) -> return js Ok (CncFun _ (Just def) pn) ->
Ok (CncFun cty Nothing pn) -> return $ updateTree (c,CncFun (Just linty) (Just def) pn) js
Ok (CncFun _ Nothing pn) ->
case mb_def of case mb_def of
Ok def -> return $ updateTree (c,CncFun cty (Just def) pn) js Ok def -> return $ updateTree (c,CncFun (Just linty) (Just def) pn) js
Bad _ -> do checkWarn $ text "no linearization of" <+> ppIdent c Bad _ -> do checkWarn $ text "no linearization of" <+> ppIdent c
return js return js
_ -> do _ -> do
case mb_def of case mb_def of
Ok def -> return $ updateTree (c,CncFun Nothing (Just def) Nothing) js Ok def -> return $ updateTree (c,CncFun (Just linty) (Just def) Nothing) js
Bad _ -> do checkWarn $ text "no linearization of" <+> ppIdent c Bad _ -> do checkWarn $ text "no linearization of" <+> ppIdent c
return js return js
AbsCat (Just _) _ -> case lookupIdent c js of AbsCat (Just _) _ -> case lookupIdent c js of
@@ -181,10 +141,38 @@ checkCompleteGrammar gr abs cnc = do
-- | General Principle: only Just-values are checked. -- | General Principle: only Just-values are checked.
-- A May-value has always been checked in its origin module. -- A May-value has always been checked in its origin module.
checkResInfo :: SourceGrammar -> Ident -> SourceModInfo -> Ident -> Info -> Check Info checkInfo :: SourceGrammar -> SourceModule -> Ident -> Info -> Check Info
checkResInfo gr mo mm c info = do checkInfo gr (m,mo) c info = do
checkReservedId c checkReservedId c
case info of 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' <- 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 ResOper pty pde -> chIn "operation" $ do
(pty', pde') <- case (pty,pde) of (pty', pde') <- case (pty,pde) of
(Just ty, Just de) -> do (Just ty, Just de) -> do
@@ -200,7 +188,7 @@ checkResInfo gr mo mm c info = do
ResOverload os tysts -> chIn "overloading" $ do ResOverload os tysts -> chIn "overloading" $ do
tysts' <- mapM (uncurry $ flip (checkLType gr [])) tysts -- return explicit ones tysts' <- mapM (uncurry $ flip (checkLType gr [])) tysts -- return explicit ones
tysts0 <- checkErr $ lookupOverload gr mo c -- check against inherited ones too tysts0 <- checkErr $ lookupOverload gr m c -- check against inherited ones too
tysts1 <- mapM (uncurry $ flip (checkLType gr [])) tysts1 <- mapM (uncurry $ flip (checkLType gr []))
[(mkFunType args val,tr) | (args,(val,tr)) <- tysts0] [(mkFunType args val,tr) | (args,(val,tr)) <- tysts0]
--- this can only be a partial guarantee, since matching --- this can only be a partial guarantee, since matching
@@ -210,12 +198,12 @@ checkResInfo gr mo mm c info = do
return (ResOverload os [(y,x) | (x,y) <- tysts']) return (ResOverload os [(y,x) | (x,y) <- tysts'])
ResParam (Just (pcs,_)) -> chIn "parameter type" $ do ResParam (Just (pcs,_)) -> chIn "parameter type" $ do
ts <- checkErr $ lookupParamValues gr mo c ts <- checkErr $ lookupParamValues gr m c
return (ResParam (Just (pcs, Just ts))) return (ResParam (Just (pcs, Just ts)))
_ -> return info _ -> return info
where where
chIn cat = checkIn (text "Happened in" <+> text cat <+> ppIdent c <+> ppPosition mm c <+> colon) chIn cat = checkIn (text "Happened in" <+> text cat <+> ppIdent c <+> ppPosition mo c <> colon)
checkUniq xss = case xss of checkUniq xss = case xss of
x:y:xs x:y:xs
@@ -224,44 +212,27 @@ checkResInfo gr mo mm c info = do
| otherwise -> checkUniq $ y:xs | otherwise -> checkUniq $ y:xs
_ -> return () _ -> return ()
mkCheck cat ss = case ss of
[] -> return info
_ -> checkError (vcat ss $$ text "in" <+> text cat <+> ppIdent c <+> ppPosition mo c)
checkCncInfo :: SourceGrammar -> Ident -> SourceModInfo -> compAbsTyp g t = case t of
(Ident,SourceModInfo) -> Vr x -> maybe (checkError (text "no value given to variable" <+> ppIdent x)) return $ lookup x g
Ident -> Info -> Check Info Let (x,(_,a)) b -> do
checkCncInfo gr m mo (a,abs) c info = do a' <- compAbsTyp g a
checkReservedId c compAbsTyp ((x, a'):g) b
case info of Prod b x a t -> do
a' <- compAbsTyp g a
CncFun _ (Just trm) mpr -> chIn "linearization of" $ do t' <- compAbsTyp ((x,Vr x):g) t
typ <- checkErr $ lookupFunType gr a c return $ Prod b x a' t'
let cat0 = valCat typ Abs _ _ _ -> return t
(cont,val) <- linTypeOfType gr m typ -- creates arg vars _ -> composOp (compAbsTyp g) t
(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 :: SourceGrammar -> Maybe Term -> Check (Maybe Term)
checkPrintname st (Just t) = checkLType st [] t typeStr >> return () checkPrintname gr (Just t) = do (t,_) <- checkLType gr [] t typeStr
checkPrintname _ _ = return () return (Just t)
checkPrintname gr Nothing = return Nothing
-- | for grammars obtained otherwise than by parsing ---- update!! -- | for grammars obtained otherwise than by parsing ---- update!!
checkReservedId :: Ident -> Check () checkReservedId :: Ident -> Check ()

4
src/GF/Compile/Optimize.hs
View File

@@ -104,10 +104,10 @@ evalCncInfo opts gr cnc abs (c,info) = do
return (CncCat ptyp pde' ppr') return (CncCat ptyp pde' ppr')
CncFun (mt@(Just (_,ty@(cont,val)))) pde ppr -> --trace (prt c) $ CncFun (mt@(Just (_,cont,val))) pde ppr -> --trace (prt c) $
eIn (text "linearization in type" <+> ppTerm Unqualified 0 (mkProd cont val []) $$ text "of function") $ do eIn (text "linearization in type" <+> ppTerm Unqualified 0 (mkProd cont val []) $$ text "of function") $ do
pde' <- case pde of pde' <- case pde of
Just de -> liftM Just $ pEval ty de Just de -> liftM Just $ pEval (cont,val) de
Nothing -> return pde Nothing -> return pde
ppr' <- liftM Just $ evalPrintname gr c ppr pde' ppr' <- liftM Just $ evalPrintname gr c ppr pde'
return $ CncFun mt pde' ppr' -- only cat in type actually needed return $ CncFun mt pde' ppr' -- only cat in type actually needed

4
src/GF/Grammar/Grammar.hs
View File

@@ -91,8 +91,8 @@ data Info =
| ResOverload [Ident] [(Type,Term)] -- ^ (/RES/) idents: modules inherited | ResOverload [Ident] [(Type,Term)] -- ^ (/RES/) idents: modules inherited
-- judgements in concrete syntax -- judgements in concrete syntax
| CncCat (Maybe Type) (Maybe Term) (Maybe Term) -- ^ (/CNC/) lindef ini'zed, | CncCat (Maybe Type) (Maybe Term) (Maybe Term) -- ^ (/CNC/) lindef ini'zed,
| CncFun (Maybe (Ident,(Context,Type))) (Maybe Term) (Maybe Term) -- ^ (/CNC/) type info added at 'TC' | CncFun (Maybe (Ident,Context,Type)) (Maybe Term) (Maybe Term) -- ^ (/CNC/) type info added at 'TC'
-- indirection to module Ident -- indirection to module Ident
| AnyInd Bool Ident -- ^ (/INDIR/) the 'Bool' says if canonical | AnyInd Bool Ident -- ^ (/INDIR/) the 'Bool' says if canonical

6
src/GF/Grammar/Lookup.hs
View File

@@ -90,8 +90,8 @@ lookupResDefKind gr m c
CncCat (Just ty) _ _ -> liftM (flip (,) 1) $ lock c ty CncCat (Just ty) _ _ -> liftM (flip (,) 1) $ lock c ty
CncCat _ _ _ -> liftM (flip (,) 1) $ lock c defLinType CncCat _ _ _ -> liftM (flip (,) 1) $ lock c defLinType
CncFun (Just (cat,_)) (Just tr) _ -> liftM (flip (,) 1) $ unlock cat tr CncFun (Just (cat,_,_)) (Just tr) _ -> liftM (flip (,) 1) $ unlock cat tr
CncFun _ (Just tr) _ -> liftM (flip (,) 1) (return tr) ---- $ unlock c tr CncFun _ (Just tr) _ -> liftM (flip (,) 1) (return tr) ---- $ unlock c tr
AnyInd _ n -> look False n c AnyInd _ n -> look False n c
ResParam _ -> return (QC m c,2) ResParam _ -> return (QC m c,2)
@@ -109,7 +109,7 @@ lookupResType gr m c = do
-- used in reused concrete -- used in reused concrete
CncCat _ _ _ -> return typeType CncCat _ _ _ -> return typeType
CncFun (Just (cat,(cont@(_:_),val))) _ _ -> do CncFun (Just (cat,cont@(_:_),val)) _ _ -> do
val' <- lock cat val val' <- lock cat val
return $ mkProd cont val' [] return $ mkProd cont val' []
CncFun _ _ _ -> lookFunType m m c CncFun _ _ _ -> lookFunType m m c