mirror of
https://github.com/GrammaticalFramework/gf-core.git
synced 2026-04-23 11:42:49 -06:00
started grammar checking with new internal format
This commit is contained in:
@@ -23,23 +23,32 @@
|
|||||||
-----------------------------------------------------------------------------
|
-----------------------------------------------------------------------------
|
||||||
|
|
||||||
module GF.Devel.Compile.CheckGrammar (
|
module GF.Devel.Compile.CheckGrammar (
|
||||||
showCheckModule, justCheckLTerm, allOperDependencies, topoSortOpers) where
|
showCheckModule,
|
||||||
|
justCheckLTerm,
|
||||||
|
allOperDependencies,
|
||||||
|
topoSortOpers
|
||||||
|
) where
|
||||||
|
|
||||||
|
import GF.Devel.Grammar.Modules
|
||||||
|
import GF.Devel.Grammar.Judgements
|
||||||
|
import GF.Devel.Grammar.Terms
|
||||||
|
import GF.Devel.Grammar.MkJudgements
|
||||||
|
import GF.Devel.Grammar.Macros
|
||||||
|
import GF.Devel.Grammar.PrGrammar
|
||||||
|
import GF.Devel.Grammar.Lookup
|
||||||
|
|
||||||
import GF.Grammar.Grammar
|
|
||||||
import GF.Infra.Ident
|
import GF.Infra.Ident
|
||||||
import GF.Infra.Modules
|
|
||||||
import GF.Grammar.Refresh ----
|
|
||||||
|
|
||||||
import GF.Grammar.TypeCheck
|
--import GF.Grammar.Refresh ----
|
||||||
import GF.Grammar.Values (cPredefAbs) ---
|
|
||||||
|
--import GF.Grammar.TypeCheck
|
||||||
|
--import GF.Grammar.Values (cPredefAbs) ---
|
||||||
|
|
||||||
|
|
||||||
import GF.Grammar.PrGrammar
|
|
||||||
import GF.Grammar.Lookup
|
|
||||||
--import GF.Grammar.LookAbs
|
--import GF.Grammar.LookAbs
|
||||||
import GF.Grammar.Macros
|
--import GF.Grammar.ReservedWords ----
|
||||||
import GF.Grammar.ReservedWords ----
|
--import GF.Grammar.PatternMatch
|
||||||
import GF.Grammar.PatternMatch
|
--import GF.Grammar.AppPredefined
|
||||||
import GF.Grammar.AppPredefined
|
|
||||||
--import GF.Grammar.Lockfield (isLockLabel)
|
--import GF.Grammar.Lockfield (isLockLabel)
|
||||||
|
|
||||||
import GF.Data.Operations
|
import GF.Data.Operations
|
||||||
@@ -52,43 +61,35 @@ import Control.Monad
|
|||||||
import Debug.Trace ---
|
import Debug.Trace ---
|
||||||
|
|
||||||
|
|
||||||
showCheckModule :: [SourceModule] -> SourceModule -> Err ([SourceModule],String)
|
showCheckModule :: GF -> SourceModule -> Err (SourceModule,String)
|
||||||
showCheckModule mos m = do
|
showCheckModule mos m = do
|
||||||
(st,(_,msg)) <- checkStart $ checkModule mos m
|
(st,(_,msg)) <- checkStart $ checkModule mos m
|
||||||
return (st, unlines $ reverse msg)
|
return (st, unlines $ reverse msg)
|
||||||
|
|
||||||
-- | checking is performed in the dependency order of modules
|
checkModule :: GF -> SourceModule -> Check SourceModule
|
||||||
checkModule :: [SourceModule] -> SourceModule -> Check [SourceModule]
|
checkModule gf0 (name,mo) = checkIn ("checking module" +++ prt name) $ do
|
||||||
checkModule ms (name,mod) = checkIn ("checking module" +++ prt name) $ case mod of
|
let gf = gf0 {gfmodules = Map.insert name mo (gfmodules gf0)}
|
||||||
|
checkRestrictedInheritance gf (name, mo)
|
||||||
|
mo1 <- case mtype mo of
|
||||||
|
MTAbstract -> judgementOpModule (checkAbsInfo gr name) mo
|
||||||
|
MTResource -> judgementOpModule (checkResInfo gr name) mo
|
||||||
|
|
||||||
ModMod mo@(Module mt st fs me ops js) -> do
|
MTConcrete aname -> do
|
||||||
checkRestrictedInheritance ms (name, mo)
|
checkErr $ topoSortOpers $ allOperDependencies name js
|
||||||
js' <- case mt of
|
abs <- checkErr $ lookupModule gr aname
|
||||||
MTAbstract -> mapMTree (checkAbsInfo gr name) js
|
js1 <- checkCompleteGrammar abs mo
|
||||||
|
judgementOpModule (checkCncInfo gr name (aname,abs)) js1
|
||||||
|
|
||||||
MTTransfer a b -> mapMTree (checkAbsInfo gr name) js
|
MTInterface -> judgementOpModule (checkResInfo gr name) mo
|
||||||
|
|
||||||
MTResource -> mapMTree (checkResInfo gr name) js
|
MTInstance iname -> do
|
||||||
|
intf <- checkErr $ lookupModule gr iname
|
||||||
|
-- checkCompleteInstance abs mo -- this is done in Rebuild
|
||||||
|
judgementOpModule (checkResInfo gr name) mo
|
||||||
|
|
||||||
MTConcrete a -> do
|
return $ (name, mo1)
|
||||||
checkErr $ topoSortOpers $ allOperDependencies name js
|
|
||||||
ModMod abs <- checkErr $ lookupModule gr a
|
|
||||||
js1 <- checkCompleteGrammar abs mo
|
|
||||||
mapMTree (checkCncInfo gr name (a,abs)) js1
|
|
||||||
|
|
||||||
MTInterface -> mapMTree (checkResInfo gr name) js
|
|
||||||
|
|
||||||
MTInstance a -> do
|
|
||||||
ModMod abs <- checkErr $ lookupModule gr a
|
|
||||||
-- checkCompleteInstance abs mo -- this is done in Rebuild
|
|
||||||
mapMTree (checkResInfo gr name) js
|
|
||||||
|
|
||||||
return $ (name, ModMod (Module mt st fs me ops js')) : ms
|
|
||||||
|
|
||||||
_ -> return $ (name,mod) : ms
|
|
||||||
where
|
|
||||||
gr = MGrammar $ (name,mod):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
|
||||||
---checkRestrictedInheritance :: [SourceModule] -> SourceModule -> Check ()
|
---checkRestrictedInheritance :: [SourceModule] -> SourceModule -> Check ()
|
||||||
@@ -114,6 +115,8 @@ checkRestrictedInheritance mos (name,mo) = do
|
|||||||
concatMap (allDependencies (const True))
|
concatMap (allDependencies (const True))
|
||||||
[jments m | (_,ModMod m) <- mos]
|
[jments m | (_,ModMod m) <- mos]
|
||||||
transClosure ds = ds ---- TODO: check in deeper modules
|
transClosure ds = ds ---- TODO: check in deeper modules
|
||||||
|
-}
|
||||||
|
|
||||||
|
|
||||||
-- | check if a term is typable
|
-- | check if a term is typable
|
||||||
justCheckLTerm :: SourceGrammar -> Term -> Err Term
|
justCheckLTerm :: SourceGrammar -> Term -> Err Term
|
||||||
@@ -121,7 +124,10 @@ justCheckLTerm src t = do
|
|||||||
((t',_),_) <- checkStart (inferLType src t)
|
((t',_),_) <- checkStart (inferLType src t)
|
||||||
return t'
|
return t'
|
||||||
|
|
||||||
checkAbsInfo :: SourceGrammar -> Ident -> (Ident,Info) -> Check (Ident,Info)
|
checkAbsInfo :: GF -> Ident -> (Ident,JEntry) -> Check (Ident,JEntry)
|
||||||
|
checkAbsInfo st m (c,info) = return (c,info) ----
|
||||||
|
|
||||||
|
{-
|
||||||
checkAbsInfo st m (c,info) = do
|
checkAbsInfo st m (c,info) = do
|
||||||
---- checkReservedId c
|
---- checkReservedId c
|
||||||
case info of
|
case info of
|
||||||
@@ -170,6 +176,7 @@ checkAbsInfo st m (c,info) = do
|
|||||||
elimSel t a = case a of
|
elimSel t a = case a of
|
||||||
R fs -> mkApp t (map (snd . snd) fs)
|
R fs -> mkApp t (map (snd . snd) fs)
|
||||||
_ -> mkApp t [a]
|
_ -> mkApp t [a]
|
||||||
|
-}
|
||||||
|
|
||||||
checkCompleteGrammar :: SourceAbs -> SourceCnc -> Check (BinTree Ident Info)
|
checkCompleteGrammar :: SourceAbs -> SourceCnc -> Check (BinTree Ident Info)
|
||||||
checkCompleteGrammar abs cnc = do
|
checkCompleteGrammar abs cnc = do
|
||||||
|
|||||||
@@ -147,14 +147,18 @@ compileSourceModule opts env@(k,gr) mo@(i,mi) = do
|
|||||||
putpp = putPointEsil opts
|
putpp = putPointEsil opts
|
||||||
|
|
||||||
|
|
||||||
mor <- ioeErr $ renameModule gr mo
|
moe <- ioeErr $ extendModule gr mo
|
||||||
intermOut opts (iOpt "show_rename") (prMod mor)
|
|
||||||
|
|
||||||
moe <- ioeErr $ extendModule gr mor
|
|
||||||
intermOut opts (iOpt "show_extend") (prMod moe)
|
intermOut opts (iOpt "show_extend") (prMod moe)
|
||||||
|
|
||||||
|
mor <- ioeErr $ renameModule gr moe
|
||||||
|
intermOut opts (iOpt "show_rename") (prMod mor)
|
||||||
|
|
||||||
|
(moc,warnings) <- putpp " type checking" $ ioeErr $ showCheckModule gr mor
|
||||||
|
if null warnings then return () else putp warnings $ return ()
|
||||||
|
intermOut opts (iOpt "show_typecheck") (prMod moc)
|
||||||
|
|
||||||
|
return (k,moc) ----
|
||||||
|
|
||||||
return (k,moe) ----
|
|
||||||
|
|
||||||
{- ----
|
{- ----
|
||||||
mo1 <- ioeErr $ rebuildModule mos mo
|
mo1 <- ioeErr $ rebuildModule mos mo
|
||||||
|
|||||||
@@ -109,9 +109,9 @@ rebuildModule gr mo@(i,mi) = case mtype mi of
|
|||||||
|
|
||||||
-- copy interface contents to instance
|
-- copy interface contents to instance
|
||||||
MTInstance i0 -> do
|
MTInstance i0 -> do
|
||||||
m1 <- lookupModule gr i0
|
m0 <- lookupModule gr i0
|
||||||
testErr (isInterface m1) ("not an interface:" +++ prt i0)
|
testErr (isInterface m0) ("not an interface:" +++ prt i0)
|
||||||
js1 <- extendMod False i0 (const True) i (mjments m1) (mjments mi)
|
js1 <- extendMod False i0 (const True) i (mjments m0) (mjments mi)
|
||||||
|
|
||||||
--- to avoid double inclusions, in instance J of I0 = J0 ** ...
|
--- to avoid double inclusions, in instance J of I0 = J0 ** ...
|
||||||
case mextends mi of
|
case mextends mi of
|
||||||
@@ -120,7 +120,9 @@ rebuildModule gr mo@(i,mi) = case mtype mi of
|
|||||||
mes <- mapM (lookupModule gr . fst) es ---- restricted?? 12/2007
|
mes <- mapM (lookupModule gr . fst) es ---- restricted?? 12/2007
|
||||||
let notInExts c _ = all (notMember c . mjments) mes
|
let notInExts c _ = all (notMember c . mjments) mes
|
||||||
let js2 = filterWithKey notInExts js1
|
let js2 = filterWithKey notInExts js1
|
||||||
return $ (i,mi {mjments = js2})
|
return $ (i,mi {
|
||||||
|
mjments = js2
|
||||||
|
})
|
||||||
|
|
||||||
-- copy functor contents to instantiation, and also add opens
|
-- copy functor contents to instantiation, and also add opens
|
||||||
_ -> case minstances mi of
|
_ -> case minstances mi of
|
||||||
|
|||||||
@@ -92,11 +92,13 @@ termOpGF f g = do
|
|||||||
fm = termOpModule f
|
fm = termOpModule f
|
||||||
|
|
||||||
termOpModule :: Monad m => (Term -> m Term) -> Module -> m Module
|
termOpModule :: Monad m => (Term -> m Term) -> Module -> m Module
|
||||||
termOpModule f m = do
|
termOpModule f = judgementOpModule fj where
|
||||||
mjs <- mapMapM fj (mjments m)
|
fj = either (liftM Left . termOpJudgement f) (return . Right)
|
||||||
|
|
||||||
|
judgementOpModule :: Monad m => (Judgement -> m Judgement) -> Module -> m Module
|
||||||
|
judgementOpModule f m = do
|
||||||
|
mjs <- mapMapM f (mjments m)
|
||||||
return m {mjments = mjs}
|
return m {mjments = mjs}
|
||||||
where
|
|
||||||
fj = either (liftM Left . termOpJudgement f) (return . Right)
|
|
||||||
|
|
||||||
termOpJudgement :: Monad m => (Term -> m Term) -> Judgement -> m Judgement
|
termOpJudgement :: Monad m => (Term -> m Term) -> Judgement -> m Judgement
|
||||||
termOpJudgement f j = do
|
termOpJudgement f j = do
|
||||||
|
|||||||
Reference in New Issue
Block a user