msyds/gf-core
1
0
Fork 0
forked from GitHub/gf-core
Code Pull Requests Activity

new type checker type checks

Browse Source
This commit is contained in:
aarne
2007-12-06 21:43:21 +00:00
parent 35f585b352
commit 5d1ad0badc
7 changed files with 160 additions and 59 deletions
Download Patch File Download Diff File Expand all files Collapse all files

90
src/GF/Devel/CheckM.hs Normal file
View File

@@ -0,0 +1,90 @@
----------------------------------------------------------------------
-- |
-- Module : CheckM
-- Maintainer : (Maintainer)
-- Stability : (stable)
-- Portability : (portable)
--
-- > CVS $Date: 2005/04/21 16:22:33 $
-- > CVS $Author: bringert $
-- > CVS $Revision: 1.5 $
--
-- (Description of the module)
-----------------------------------------------------------------------------
module GF.Devel.CheckM (Check,
checkError, checkCond, checkWarn, checkUpdate, checkInContext,
checkUpdates, checkReset, checkResets, checkGetContext,
checkLookup, checkStart, checkErr, checkVal, checkIn,
prtFail
) where
import GF.Data.Operations
import GF.Devel.Grammar.Modules
import GF.Devel.Grammar.Terms
import GF.Infra.Ident
import GF.Devel.Grammar.PrGF
-- | the strings are non-fatal warnings
type Check a = STM (Context,[String]) a
checkError :: String -> Check a
checkError = raise
checkCond :: String -> Bool -> Check ()
checkCond s b = if b then return () else checkError s
-- | warnings should be reversed in the end
checkWarn :: String -> Check ()
checkWarn s = updateSTM (\ (cont,msg) -> (cont, s:msg))
checkUpdate :: Decl -> Check ()
checkUpdate d = updateSTM (\ (cont,msg) -> (d:cont, msg))
checkInContext :: [Decl] -> Check r -> Check r
checkInContext g ch = do
i <- checkUpdates g
r <- ch
checkResets i
return r
checkUpdates :: [Decl] -> Check Int
checkUpdates ds = mapM checkUpdate ds >> return (length ds)
checkReset :: Check ()
checkReset = checkResets 1
checkResets :: Int -> Check ()
checkResets i = updateSTM (\ (cont,msg) -> (drop i cont, msg))
checkGetContext :: Check Context
checkGetContext = do
(co,_) <- readSTM
return co
checkLookup :: Ident -> Check Type
checkLookup x = do
co <- checkGetContext
checkErr $ maybe (prtBad "unknown variable" x) return $ lookup x co
checkStart :: Check a -> Err (a,(Context,[String]))
checkStart c = appSTM c ([],[])
checkErr :: Err a -> Check a
checkErr e = stm (\s -> do
v <- e
return (v,s)
)
checkVal :: a -> Check a
checkVal v = return v
prtFail :: Print a => String -> a -> Check b
prtFail s t = checkErr $ prtBad s t
checkIn :: String -> Check a -> Check a
checkIn msg c = stm $ \s@(g,ws) -> case appSTM c s of
Bad e -> Bad $ msg ++++ e
Ok (v,(g',ws')) -> Ok (v,(g',ws2)) where
new = take (length ws' - length ws) ws'
ws2 = [msg ++++ w | w <- new] ++ ws

35
src/GF/Devel/Compile/CheckGrammar.hs
View File

@@ -47,12 +47,13 @@ import GF.Infra.Ident
--import GF.Grammar.LookAbs
--import GF.Grammar.ReservedWords ----
import GF.Grammar.PatternMatch (testOvershadow)
import GF.Grammar.AppPredefined
import GF.Devel.Grammar.PatternMatch (testOvershadow)
import GF.Devel.Grammar.AppPredefined
--import GF.Grammar.Lockfield (isLockLabel)
import GF.Devel.CheckM
import GF.Data.Operations
import GF.Infra.CheckM
import Data.List
import qualified Data.Set as Set
@@ -77,8 +78,8 @@ checkModule gf0 (name,mo) = checkIn ("checking module" +++ prt name) $ do
MTConcrete aname -> do
checkErr $ topoSortOpers $ allOperDependencies name $ mjments mo
abs <- checkErr $ lookupModule gr aname
js1 <- checkCompleteGrammar abs mo
judgementOpModule (checkCncInfo gr name (aname,abs)) js1
mo1 <- checkCompleteGrammar abs mo
entryOpModule (checkCncInfo gr name (aname,abs)) mo1
MTInterface -> judgementOpModule (checkResInfo gr name) mo
@@ -124,8 +125,8 @@ justCheckLTerm src t = do
((t',_),_) <- checkStart (inferLType src t)
return t'
checkAbsInfo :: GF -> Ident -> Ident -> Judgement -> Check Judgement
checkAbsInfo st m c info = return info ----
checkAbsInfo :: GF -> Ident -> Judgement -> Check Judgement
checkAbsInfo st m info = return info ----
{-
checkAbsInfo st m (c,info) = do
@@ -198,18 +199,18 @@ checkCompleteGrammar abs cnc = do
checkWarn $
"Warning: no linearization type for" +++ prt c ++
", inserting default {s : Str}"
return $ Map.insert c (cncCat defLinType) js
return $ Map.insert c (Left (cncCat defLinType)) js
_ -> return js
checkResInfo :: GF -> Ident -> Ident -> Judgement -> Check Judgement
checkResInfo gr mo c info = do
checkResInfo :: GF -> Ident -> Judgement -> Check Judgement
checkResInfo gr mo info = do
---- checkReservedId c
case jform info of
JOper -> chIn "operation" $ case (jtype info, jdef info) of
(_,Meta _) -> do
checkWarn "No definition given to oper"
return info
(Meta,de) -> do
(Meta _,de) -> do
(de',ty') <- infer de
return (resOper ty' de')
(ty, de) -> do
@@ -237,7 +238,7 @@ checkResInfo gr mo c info = do
where
infer = inferLType gr
check = checkLType gr
chIn cat = checkIn ("Happened in" +++ cat +++ prt c +++ ":")
chIn cat = checkIn ("Happened in" +++ cat) ---- +++ prt c +++ ":")
comp = computeLType gr
checkUniq xss = case xss of
@@ -265,7 +266,7 @@ checkCncInfo gr cnc (a,abs) c info = do
---- return (c, CncFun (Just (cat,(cont,val))) (Yes trm') mpr)
-- cat for cf, typ for pe
JCat (Yes typ) mdef mpr -> chIn "linearization type of" $ do
JCat -> chIn "linearization type of" $ do
checkErr $ lookupCatContext gr a c
typ' <- checkIfLinType gr (jtype info)
{- ----
@@ -278,7 +279,7 @@ checkCncInfo gr cnc (a,abs) c info = do
checkPrintname gr (jprintname info)
return (info {jtype = typ'})
_ -> checkResInfo gr cnc c info
_ -> checkResInfo gr cnc info
where
env = gr
@@ -620,7 +621,7 @@ inferLType gr trm = case trm of
_ -> False
inferPatt p = case p of
PP q c ps | q /= cPredef -> checkErr $ lookupOperType gr q c >>= snd . prodForm
PP q c ps | q /= cPredef -> checkErr $ lookupOperType gr q c >>= return . snd . prodForm
PAs _ p -> inferPatt p
PNeg p -> inferPatt p
PAlt p q -> checks [inferPatt p, inferPatt q]
@@ -1053,14 +1054,12 @@ allOperDependencies m = allDependencies (==m)
allDependencies :: (Ident -> Bool) -> Map.Map Ident JEntry -> [(Ident,[Ident])]
allDependencies ism b =
[(f, nub (concatMap opty (pts i))) | (f,i) <- tree2list b]
[(f, nub (concatMap opersIn (pts i))) | (f,Left i) <- Map.assocs b]
where
opersIn t = case t of
Q n c | ism n -> [c]
QC n c | ism n -> [c]
_ -> collectOp opersIn t
opty (Yes ty) = opersIn ty
opty _ = []
pts i = [jtype i, jdef i]
---- AbsFun pty ptr -> [pty] --- ptr is def, which can be mutual

5
src/GF/Devel/Compile/Compile.hs
View File

@@ -4,10 +4,9 @@ module GF.Devel.Compile.Compile (batchCompile) where
import GF.Devel.Compile.GetGrammar
import GF.Devel.Compile.Extend
import GF.Devel.Compile.Rename
import GF.Devel.Compile.CheckGrammar
----import GF.Grammar.Refresh
----import GF.Devel.CheckGrammar
----import GF.Devel.Optimize
--import GF.Compile.Evaluate ----
----import GF.Devel.OptimizeGF
import GF.Devel.Grammar.Terms
@@ -157,7 +156,7 @@ compileSourceModule opts env@(k,gr) mo@(i,mi) = do
if null warnings then return () else putp warnings $ return ()
intermOut opts (iOpt "show_typecheck") (prMod moc)
return (k,moc) ----
return (k,mor) ----
{- ----

40
src/GF/Devel/Grammar/AppPredefined.hs
View File

@@ -20,7 +20,7 @@ module GF.Devel.Grammar.AppPredefined (
import GF.Devel.Grammar.Terms
import GF.Devel.Grammar.Macros
import GF.Grammar.PrGF (prt,prt_,prtBad)
import GF.Devel.Grammar.PrGF (prt,prt_,prtBad)
import GF.Infra.Ident
import GF.Data.Operations
@@ -41,29 +41,32 @@ typPredefined c@(IC f) = case f of
"error" -> return $ mkFunType [typeStr] (cnPredef "Error") -- non-can. of empty set
"PFalse" -> return $ cnPredef "PBool"
"PTrue" -> return $ cnPredef "PBool"
"dp" -> return $ mkFunType [cnPredef "Int",typeTok] typeTok
"drop" -> return $ mkFunType [cnPredef "Int",typeTok] typeTok
"dp" -> return $ mkFunType [cnPredef "Int",typeStr] typeStr
"drop" -> return $ mkFunType [cnPredef "Int",typeStr] typeStr
"eqInt" -> return $ mkFunType [cnPredef "Int",cnPredef "Int"] (cnPredef "PBool")
"lessInt"-> return $ mkFunType [cnPredef "Int",cnPredef "Int"] (cnPredef "PBool")
"eqStr" -> return $ mkFunType [typeTok,typeTok] (cnPredef "PBool")
"length" -> return $ mkFunType [typeTok] (cnPredef "Int")
"occur" -> return $ mkFunType [typeTok,typeTok] (cnPredef "PBool")
"occurs" -> return $ mkFunType [typeTok,typeTok] (cnPredef "PBool")
"eqStr" -> return $ mkFunType [typeStr,typeStr] (cnPredef "PBool")
"length" -> return $ mkFunType [typeStr] (cnPredef "Int")
"occur" -> return $ mkFunType [typeStr,typeStr] (cnPredef "PBool")
"occurs" -> return $ mkFunType [typeStr,typeStr] (cnPredef "PBool")
"plus" -> return $ mkFunType [cnPredef "Int",cnPredef "Int"] (cnPredef "Int")
---- "read" -> (P : Type) -> Tok -> P
"show" -> return $ mkProd -- (P : PType) -> P -> Tok
([(zIdent "P",typePType),(wildIdent,Vr (zIdent "P"))],typeStr,[])
"toStr" -> return $ mkProd -- (L : Type) -> L -> Str
([(zIdent "L",typeType),(wildIdent,Vr (zIdent "L"))],typeStr,[])
"show" -> return $ mkProds -- (P : PType) -> P -> Tok
([(identC "P",typePType),(wildIdent,Vr (identC "P"))],typeStr,[])
"toStr" -> return $ mkProds -- (L : Type) -> L -> Str
([(identC "L",typeType),(wildIdent,Vr (identC "L"))],typeStr,[])
"mapStr" ->
let ty = zIdent "L" in
return $ mkProd -- (L : Type) -> (Str -> Str) -> L -> L
let ty = identC "L" in
return $ mkProds -- (L : Type) -> (Str -> Str) -> L -> L
([(ty,typeType),(wildIdent,mkFunType [typeStr] typeStr),(wildIdent,Vr ty)],Vr ty,[])
"take" -> return $ mkFunType [cnPredef "Int",typeTok] typeTok
"tk" -> return $ mkFunType [cnPredef "Int",typeTok] typeTok
"take" -> return $ mkFunType [cnPredef "Int",typeStr] typeStr
"tk" -> return $ mkFunType [cnPredef "Int",typeStr] typeStr
_ -> prtBad "unknown in Predef:" c
typPredefined c = prtBad "unknown in Predef:" c
mkProds (cont,t,xx) = foldr (uncurry Prod) (mkApp t xx) cont
appPredefined :: Term -> Err (Term,Bool)
appPredefined t = case t of
@@ -119,10 +122,10 @@ appPredefined t = case t of
str2tag :: String -> Term
str2tag s = case s of
---- '\'' : cs -> mkCn $ pTrm $ init cs
_ -> Cn $ IC s ---
_ -> Con $ IC s ---
where
mkCn t = case t of
Vr i -> Cn i
Vr i -> Con i
App c a -> App (mkCn c) (mkCn a)
_ -> t
@@ -140,7 +143,6 @@ trm2str :: Term -> Err Term
trm2str t = case t of
R ((_,(_,s)):_) -> trm2str s
T _ ((_,s):_) -> trm2str s
TSh _ ((_,s):_) -> trm2str s
V _ (s:_) -> trm2str s
C _ _ -> return $ t
K _ -> return $ t
@@ -153,7 +155,7 @@ trm2str t = case t of
-- (this has been done in type checking)
mapStr :: Type -> Term -> Term -> Term
mapStr ty f t = case (ty,t) of
_ | elem ty [typeStr,typeTok] -> App f t
_ | elem ty [typeStr,typeStr] -> App f t
(_, R ts) -> R [(l,mapField v) | (l,v) <- ts]
(Table a b,T ti cs) -> T ti [(p,mapStr b f v) | (p,v) <- cs]
_ -> t

22
src/GF/Devel/Grammar/Macros.hs
View File

@@ -21,11 +21,22 @@ typeForm t = (co,f,a) where
(co,t2) = prodForm t
(f,a) = appForm t2
termForm :: Term -> ([Ident],Term,[Term])
termForm t = (co,f,a) where
(co,t2) = absForm t
(f,a) = appForm t2
prodForm :: Type -> (Context,Term)
prodForm t = case t of
Prod x ty val -> ((x,ty):co,t2) where (co,t2) = prodForm val
_ -> ([],t)
absForm :: Term -> ([Ident],Term)
absForm t = case t of
Abs x val -> (x:co,t2) where (co,t2) = absForm val
_ -> ([],t)
appForm :: Term -> (Term,[Term])
appForm tr = (f,reverse xs) where
(f,xs) = apps tr
@@ -171,6 +182,8 @@ isTypeInts ty = case ty of
App c _ -> c == constPredefRes "Ints"
_ -> False
cnPredef = constPredefRes
constPredefRes :: String -> Term
constPredefRes s = Q (IC "Predef") (identC s)
@@ -214,6 +227,15 @@ judgementOpModule f m = do
return m {mjments = mjs}
where
fj = either (liftM Left . f) (return . Right)
entryOpModule :: Monad m =>
(Ident -> Judgement -> m Judgement) -> Module -> m Module
entryOpModule f m = do
mjs <- liftM Map.fromAscList $ mapm $ Map.assocs $ mjments m
return $ m {mjments = mjs}
where
mapm = mapM (\ (i,j) -> liftM ((,) i) (fe i j))
fe i j = either (liftM Left . f i) (return . Right) j
termOpJudgement :: Monad m => (Term -> m Term) -> Judgement -> m Judgement
termOpJudgement f j = do

25
src/GF/Devel/Grammar/PatternMatch.hs
View File

@@ -18,9 +18,9 @@ module GF.Devel.Grammar.PatternMatch (matchPattern,
) where
import GF.Grammar.Terms
import GF.Grammar.Macros
import GF.Grammar.PrGF
import GF.Devel.Grammar.Terms
import GF.Devel.Grammar.Macros
import GF.Devel.Grammar.PrGF
import GF.Infra.Ident
import GF.Data.Operations
@@ -56,15 +56,12 @@ findMatch cases terms = case cases of
tryMatch :: (Patt, Term) -> Err [(Ident, Term)]
tryMatch (p,t) = do
t' <- termForm t
let t' = termForm t
trym p t'
where
isInConstantFormt = True -- tested already
trym p t' =
case (p,t') of
(PVal _ i, (_,Val _ j,_))
| i == j -> return []
| otherwise -> Bad $ "no match of values"
(_,(x,Empty,y)) -> trym p (x,K [],y) -- because "" = [""] = []
(PV IW, _) | isInConstantFormt -> return [] -- optimization with wildcard
(PV x, _) | isInConstantFormt -> return [(x,t)]
@@ -94,7 +91,6 @@ tryMatch (p,t) = do
[(p,snd a) | (l,p) <- r, let Just a = lookup l r']
return (concat matches)
(PT _ p',_) -> trym p' t'
(_, ([],Alias _ _ d,[])) -> tryMatch (p,d)
-- (PP (IC "Predef") (IC "CC") [p1,p2], ([],K s, [])) -> do
@@ -119,10 +115,11 @@ tryMatch (p,t) = do
] >>
return []
_ -> prtBad "no match in case expr for" t
eqStrIdent = (==) ----
isInConstantForm :: Term -> Bool
isInConstantForm trm = case trm of
Cn _ -> True
Con _ -> True
Q _ _ -> True
QC _ _ -> True
@@ -131,7 +128,6 @@ isInConstantForm trm = case trm of
R r -> all (isInConstantForm . snd . snd) r
K _ -> True
Empty -> True
Alias _ _ t -> isInConstantForm t
EInt _ -> True
_ -> False ---- isInArgVarForm trm
@@ -144,10 +140,3 @@ varsOfPatt p = case p of
PT _ q -> varsOfPatt q
_ -> []
-- | to search matching parameter combinations in tables
isMatchingForms :: [Patt] -> [Term] -> Bool
isMatchingForms ps ts = all match (zip ps ts') where
match (PC c cs, (Cn d, ds)) = c == d && isMatchingForms cs ds
match _ = True
ts' = map appForm ts

2
src/GF/Devel/Grammar/PrGF.hs
View File

@@ -82,13 +82,13 @@ instance Print Term where
instance Print Ident where
prt = cprintTree . tri
{- ----
instance Print Patt where
prt = P.printTree . trp
instance Print Label where
prt = P.printTree . trLabel
{-
instance Print MetaSymb where
prt (MetaSymb i) = "?" ++ show i