mirror of
https://github.com/GrammaticalFramework/gf-core.git
synced 2026-05-10 11:42:51 -06:00
partial check of dependencies with restricted inheritance
This commit is contained in:
@@ -44,20 +44,23 @@ import GF.Data.Operations
|
|||||||
import GF.Infra.CheckM
|
import GF.Infra.CheckM
|
||||||
|
|
||||||
import Data.List
|
import Data.List
|
||||||
|
import qualified Data.Set as Set
|
||||||
|
import qualified Data.Map as Map
|
||||||
import Control.Monad
|
import Control.Monad
|
||||||
import Debug.Trace ---
|
import Debug.Trace ---
|
||||||
|
|
||||||
|
|
||||||
showCheckModule :: [SourceModule] -> SourceModule -> Err ([SourceModule],String)
|
showCheckModule :: [SourceModule] -> 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 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,mod) = checkIn ("checking module" +++ prt name) $ case mod of
|
checkModule ms (name,mod) = checkIn ("checking module" +++ prt name) $ case mod of
|
||||||
|
|
||||||
ModMod mo@(Module mt st fs me ops js) -> do
|
ModMod mo@(Module mt st fs me ops js) -> do
|
||||||
|
checkRestrictedInheritance ms (name, mo)
|
||||||
js' <- case mt of
|
js' <- case mt of
|
||||||
MTAbstract -> mapMTree (checkAbsInfo gr name) js
|
MTAbstract -> mapMTree (checkAbsInfo gr name) js
|
||||||
|
|
||||||
@@ -84,6 +87,32 @@ checkModule ms (name,mod) = checkIn ("checking module" +++ prt name) $ case mod
|
|||||||
where
|
where
|
||||||
gr = MGrammar $ (name,mod):ms
|
gr = MGrammar $ (name,mod):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,ModMod 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 -> fail $ "In inherited module" +++ prt i ++
|
||||||
|
", dependence of excluded constants:" ++++
|
||||||
|
unlines [" " ++ prt f +++ "on" +++ unwords (map prt is) |
|
||||||
|
(f,is) <- cs]
|
||||||
|
allDeps = ---- transClosure $ Map.fromList $
|
||||||
|
concatMap (allDependencies (const True))
|
||||||
|
[jments m | (_,ModMod m) <- mos]
|
||||||
|
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
|
||||||
justCheckLTerm src t = do
|
justCheckLTerm src t = do
|
||||||
@@ -1020,20 +1049,26 @@ linTypeOfType cnc m typ = do
|
|||||||
-- | dependency check, detecting circularities and returning topo-sorted list
|
-- | dependency check, detecting circularities and returning topo-sorted list
|
||||||
|
|
||||||
allOperDependencies :: Ident -> BinTree Ident Info -> [(Ident,[Ident])]
|
allOperDependencies :: Ident -> BinTree Ident Info -> [(Ident,[Ident])]
|
||||||
allOperDependencies m b =
|
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]
|
[(f, nub (concatMap opty (pts i))) | (f,i) <- tree2list b]
|
||||||
where
|
where
|
||||||
opersIn t = case t of
|
opersIn t = case t of
|
||||||
Q n c | n == m -> [c]
|
Q n c | ism n -> [c]
|
||||||
QC n c | n == m -> [c]
|
QC n c | ism n -> [c]
|
||||||
_ -> collectOp opersIn t
|
_ -> collectOp opersIn t
|
||||||
opty (Yes ty) = opersIn ty
|
opty (Yes ty) = opersIn ty
|
||||||
opty _ = []
|
opty _ = []
|
||||||
pts i = case i of
|
pts i = case i of
|
||||||
ResOper pty pt -> [pty,pt]
|
ResOper pty pt -> [pty,pt]
|
||||||
ResParam (Yes (ps,_)) -> [Yes t | (_,cont) <- ps, (_,t) <- cont]
|
ResParam (Yes (ps,_)) -> [Yes t | (_,cont) <- ps, (_,t) <- cont]
|
||||||
CncFun _ pt _ -> [pt] ---- (Maybe (Ident,(Context,Type))
|
CncCat pty _ _ -> [pty]
|
||||||
_ -> [] ---- ResParam
|
CncFun _ pt _ -> [pt] ---- (Maybe (Ident,(Context,Type))
|
||||||
|
AbsFun pty ptr -> [pty] --- ptr is def, which can be mutual
|
||||||
|
AbsCat (Yes co) _ -> [Yes ty | (_,ty) <- co]
|
||||||
|
_ -> []
|
||||||
|
|
||||||
topoSortOpers :: [(Ident,[Ident])] -> Err [Ident]
|
topoSortOpers :: [(Ident,[Ident])] -> Err [Ident]
|
||||||
topoSortOpers st = do
|
topoSortOpers st = do
|
||||||
|
|||||||
Reference in New Issue
Block a user