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

refactor GF.Infra.CheckM and use the CheckM monad in the renamer as well

Browse Source
This commit is contained in:
krasimir
2009-10-02 22:52:14 +00:00
parent f05088df54
commit 9b2c81436c
5 changed files with 251 additions and 330 deletions
Download Patch File Download Diff File Expand all files Collapse all files

6
src/GF/Compile.hs
View File

@@ -24,6 +24,7 @@ import GF.Infra.Ident
import GF.Infra.Option import GF.Infra.Option
import GF.Infra.Modules import GF.Infra.Modules
import GF.Infra.UseIO import GF.Infra.UseIO
import GF.Infra.CheckM
import GF.Data.Operations import GF.Data.Operations
@@ -205,10 +206,11 @@ compileSourceModule opts env@(k,gr,_) mo@(i,mi) = do
_ -> do _ -> do
let mos = modules gr let mos = modules gr
mo2:_ <- putpp " renaming " $ ioeErr $ renameModule mos mo1b (mo2,warnings) <- putpp " renaming " $ ioeErr $ runCheck (renameModule mos mo1b)
if null warnings then return () else puts warnings $ return ()
intermOut opts DumpRename (ppModule Qualified mo2) intermOut opts DumpRename (ppModule Qualified mo2)
(mo3:_,warnings) <- putpp " type checking" $ ioeErr $ showCheckModule mos mo2 (mo3,warnings) <- putpp " type checking" $ ioeErr $ runCheck (checkModule mos mo2)
if null warnings then return () else puts warnings $ return () if null warnings then return () else puts warnings $ return ()
intermOut opts DumpTypeCheck (ppModule Qualified mo3) intermOut opts DumpTypeCheck (ppModule Qualified mo3)

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

@@ -22,7 +22,7 @@
----------------------------------------------------------------------------- -----------------------------------------------------------------------------
module GF.Compile.CheckGrammar ( module GF.Compile.CheckGrammar (
showCheckModule, justCheckLTerm, allOperDependencies, topoSortOpers) where checkModule, inferLType, allOperDependencies, topoSortOpers) where
import GF.Infra.Ident import GF.Infra.Ident
import GF.Infra.Modules import GF.Infra.Modules
@@ -48,14 +48,8 @@ import qualified Data.Set as Set
import Control.Monad import Control.Monad
import Text.PrettyPrint import Text.PrettyPrint
showCheckModule :: [SourceModule] -> SourceModule -> Err ([SourceModule],String)
showCheckModule mos m =
case runCheck (checkModule mos m) of
Left msgs -> Bad ( render (vcat (reverse msgs)))
Right (st,_,msgs) -> Ok (st, render (vcat (reverse msgs)))
-- | 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 (name,mo) = checkIn (text "checking module" <+> ppIdent name) $ do
let js = jments mo let js = jments mo
checkRestrictedInheritance ms (name, mo) checkRestrictedInheritance ms (name, mo)
@@ -75,7 +69,7 @@ checkModule ms (name,mo) = checkIn (text "checking module" <+> ppIdent name) $ d
MTInstance a -> do MTInstance a -> do
checkMap (checkResInfo gr name mo) js checkMap (checkResInfo gr name mo) js
return $ (name, replaceJudgements mo js') : ms return (name, replaceJudgements mo js')
where where
gr = MGrammar $ (name,mo):ms gr = MGrammar $ (name,mo):ms
@@ -100,13 +94,6 @@ 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
-- | check if a term is typable
justCheckLTerm :: SourceGrammar -> Term -> Err Term
justCheckLTerm src t =
case runCheck (inferLType src t) of
Left msgs -> Bad ( render (vcat (reverse msgs)))
Right ((t',_),_,_) -> Ok t'
checkAbsInfo :: checkAbsInfo ::
SourceGrammar -> Ident -> SourceModInfo -> Ident -> Info -> Check Info SourceGrammar -> Ident -> SourceModInfo -> Ident -> Info -> Check Info
checkAbsInfo st m mo c info = do checkAbsInfo st m mo c info = do
@@ -206,20 +193,20 @@ checkResInfo gr mo mm c info = do
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
ty' <- check ty typeType >>= comp . fst ty' <- checkLType gr [] ty typeType >>= computeLType gr [] . fst
(de',_) <- check de ty' (de',_) <- checkLType gr [] de ty'
return (Just ty', Just de') return (Just ty', Just de')
(_ , Just de) -> do (_ , Just de) -> do
(de',ty') <- infer de (de',ty') <- inferLType gr [] de
return (Just ty', Just de') return (Just ty', Just de')
(_ , Nothing) -> do (_ , Nothing) -> do
checkError (text "No definition given to the operation") checkError (text "No definition given to the operation")
return (ResOper pty' pde') return (ResOper pty' pde')
ResOverload os tysts -> chIn "overloading" $ do ResOverload os tysts -> chIn "overloading" $ do
tysts' <- mapM (uncurry $ flip check) 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 mo c -- check against inherited ones too
tysts1 <- mapM (uncurry $ flip check) 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
--- with value type is only possible if expected type is given --- with value type is only possible if expected type is given
@@ -233,15 +220,12 @@ checkResInfo gr mo mm c info = do
_ -> return info _ -> return info
where where
infer = inferLType gr
check = checkLType gr
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 mm c <+> colon)
comp = computeLType gr
checkUniq xss = case xss of checkUniq xss = case xss of
x:y:xs x:y:xs
| x == y -> checkError $ text "ambiguous for type" <+> | x == y -> checkError $ text "ambiguous for type" <+>
ppType gr (mkFunType (tail x) (head x)) ppType (mkFunType (tail x) (head x))
| otherwise -> checkUniq $ y:xs | otherwise -> checkUniq $ y:xs
_ -> return () _ -> return ()
@@ -257,7 +241,7 @@ checkCncInfo gr m mo (a,abs) c info = do
typ <- checkErr $ lookupFunType gr a c typ <- checkErr $ lookupFunType gr a c
let cat0 = valCat typ let cat0 = valCat typ
(cont,val) <- linTypeOfType gr m typ -- creates arg vars (cont,val) <- linTypeOfType gr m typ -- creates arg vars
(trm',_) <- check trm (mkFunType (map (\(_,_,ty) -> ty) cont) val) -- erases arg vars (trm',_) <- checkLType gr [] trm (mkFunType (map (\(_,_,ty) -> ty) cont) val) -- erases arg vars
checkPrintname gr mpr checkPrintname gr mpr
cat <- return $ snd cat0 cat <- return $ snd cat0
return (CncFun (Just (cat,(cont,val))) (Just trm') mpr) return (CncFun (Just (cat,(cont,val))) (Just trm') mpr)
@@ -265,10 +249,10 @@ checkCncInfo gr m mo (a,abs) c info = do
CncCat (Just typ) mdef mpr -> chIn "linearization type of" $ do CncCat (Just typ) mdef mpr -> chIn "linearization type of" $ do
checkErr $ lookupCatContext gr a c checkErr $ lookupCatContext gr a c
typ' <- computeLType gr typ typ' <- computeLType gr [] typ
mdef' <- case mdef of mdef' <- case mdef of
Just def -> do Just def -> do
(def',_) <- checkLType gr def (mkFunType [typeStr] typ) (def',_) <- checkLType gr [] def (mkFunType [typeStr] typ)
return $ Just def' return $ Just def'
_ -> return mdef _ -> return mdef
checkPrintname gr mpr checkPrintname gr mpr
@@ -277,66 +261,59 @@ checkCncInfo gr m mo (a,abs) c info = do
_ -> checkResInfo gr m mo c info _ -> checkResInfo gr m mo c info
where where
env = gr
infer = inferLType gr
comp = computeLType gr
check = checkLType gr
chIn cat = checkIn (text "Happened in" <+> text cat <+> ppIdent c <+> ppPosition mo c <> colon) chIn cat = checkIn (text "Happened in" <+> text cat <+> ppIdent c <+> ppPosition mo c <> colon)
computeLType :: SourceGrammar -> Type -> Check Type computeLType :: SourceGrammar -> Context -> Type -> Check Type
computeLType gr t = do computeLType gr g0 t = comp (reverse [(b,x, Vr x) | (b,x,_) <- g0] ++ g0) t
g0 <- checkGetContext
let g = [(b,x, Vr x) | (b,x,_) <- g0]
checkInContext g $ comp t
where where
comp ty = case ty of comp g ty = case ty of
_ | Just _ <- isTypeInts ty -> return ty ---- shouldn't be needed _ | Just _ <- isTypeInts ty -> return ty ---- shouldn't be needed
| isPredefConstant ty -> return ty ---- shouldn't be needed | isPredefConstant ty -> return ty ---- shouldn't be needed
Q m ident -> checkIn (text "module" <+> ppIdent m) $ do Q m ident -> checkIn (text "module" <+> ppIdent m) $ do
ty' <- checkErr (lookupResDef gr m ident) ty' <- checkErr (lookupResDef gr m ident)
if ty' == ty then return ty else comp ty' --- is this necessary to test? if ty' == ty then return ty else comp g ty' --- is this necessary to test?
Vr ident -> checkLookup ident -- never needed to compute! Vr ident -> checkLookup ident g -- never needed to compute!
App f a -> do App f a -> do
f' <- comp f f' <- comp g f
a' <- comp a a' <- comp g a
case f' of case f' of
Abs b x t -> checkInContext [(b,x,a')] $ comp t Abs b x t -> comp ((b,x,a'):g) t
_ -> return $ App f' a' _ -> return $ App f' a'
Prod bt x a b -> do Prod bt x a b -> do
a' <- comp a a' <- comp g a
b' <- checkInContext [(bt,x,Vr x)] $ comp b b' <- comp ((bt,x,Vr x) : g) b
return $ Prod bt x a' b' return $ Prod bt x a' b'
Abs bt x b -> do Abs bt x b -> do
b' <- checkInContext [(bt,x,Vr x)] $ comp b b' <- comp ((bt,x,Vr x):g) b
return $ Abs bt x b' return $ Abs bt x b'
ExtR r s -> do ExtR r s -> do
r' <- comp r r' <- comp g r
s' <- comp s s' <- comp g s
case (r',s') of case (r',s') of
(RecType rs, RecType ss) -> checkErr (plusRecType r' s') >>= comp (RecType rs, RecType ss) -> checkErr (plusRecType r' s') >>= comp g
_ -> return $ ExtR r' s' _ -> return $ ExtR r' s'
RecType fs -> do RecType fs -> do
let fs' = sortRec fs let fs' = sortRec fs
liftM RecType $ mapPairsM comp fs' liftM RecType $ mapPairsM (comp g) fs'
ELincat c t -> do ELincat c t -> do
t' <- comp t t' <- comp g t
checkErr $ lockRecType c t' ---- locking to be removed AR 20/6/2009 checkErr $ lockRecType c t' ---- locking to be removed AR 20/6/2009
_ | ty == typeTok -> return typeStr _ | ty == typeTok -> return typeStr
_ | isPredefConstant ty -> return ty _ | isPredefConstant ty -> return ty
_ -> composOp comp ty _ -> composOp (comp g) ty
checkPrintname :: SourceGrammar -> Maybe Term -> Check () checkPrintname :: SourceGrammar -> Maybe Term -> Check ()
checkPrintname st (Just t) = checkLType st t typeStr >> return () checkPrintname st (Just t) = checkLType st [] t typeStr >> return ()
checkPrintname _ _ = return () checkPrintname _ _ = return ()
-- | for grammars obtained otherwise than by parsing ---- update!! -- | for grammars obtained otherwise than by parsing ---- update!!
@@ -347,15 +324,15 @@ checkReservedId x
-- the underlying algorithms -- the underlying algorithms
inferLType :: SourceGrammar -> Term -> Check (Term, Type) inferLType :: SourceGrammar -> Context -> Term -> Check (Term, Type)
inferLType gr trm = case trm of inferLType gr g trm = case trm of
Q m ident | isPredef m -> termWith trm $ checkErr (typPredefined ident) Q m ident | isPredef m -> termWith trm $ checkErr (typPredefined ident)
Q m ident -> checks [ Q m ident -> checks [
termWith trm $ checkErr (lookupResType gr m ident) >>= comp termWith trm $ checkErr (lookupResType gr m ident) >>= computeLType gr g
, ,
checkErr (lookupResDef gr m ident) >>= infer checkErr (lookupResDef gr m ident) >>= inferLType gr g
, ,
checkError (text "cannot infer type of constant" <+> ppTerm Unqualified 0 trm) checkError (text "cannot infer type of constant" <+> ppTerm Unqualified 0 trm)
] ]
@@ -363,49 +340,49 @@ inferLType gr trm = case trm of
QC m ident | isPredef m -> termWith trm $ checkErr (typPredefined ident) QC m ident | isPredef m -> termWith trm $ checkErr (typPredefined ident)
QC m ident -> checks [ QC m ident -> checks [
termWith trm $ checkErr (lookupResType gr m ident) >>= comp termWith trm $ checkErr (lookupResType gr m ident) >>= computeLType gr g
, ,
checkErr (lookupResDef gr m ident) >>= infer checkErr (lookupResDef gr m ident) >>= inferLType gr g
, ,
checkError (text "cannot infer type of canonical constant" <+> ppTerm Unqualified 0 trm) checkError (text "cannot infer type of canonical constant" <+> ppTerm Unqualified 0 trm)
] ]
Val _ ty i -> termWith trm $ return ty Val _ ty i -> termWith trm $ return ty
Vr ident -> termWith trm $ checkLookup ident Vr ident -> termWith trm $ checkLookup ident g
Typed e t -> do Typed e t -> do
t' <- comp t t' <- computeLType gr g t
check e t' checkLType gr g e t'
return (e,t') return (e,t')
App f a -> do App f a -> do
over <- getOverload gr Nothing trm over <- getOverload gr g Nothing trm
case over of case over of
Just trty -> return trty Just trty -> return trty
_ -> do _ -> do
(f',fty) <- infer f (f',fty) <- inferLType gr g f
fty' <- comp fty fty' <- computeLType gr g fty
case fty' of case fty' of
Prod bt z arg val -> do Prod bt z arg val -> do
a' <- justCheck a arg a' <- justCheck g a arg
ty <- if isWildIdent z ty <- if isWildIdent z
then return val then return val
else substituteLType [(bt,z,a')] val else substituteLType [(bt,z,a')] val
return (App f' a',ty) return (App f' a',ty)
_ -> checkError (text "A function type is expected for" <+> ppTerm Unqualified 0 f <+> text "instead of type" <+> ppType env fty) _ -> checkError (text "A function type is expected for" <+> ppTerm Unqualified 0 f <+> text "instead of type" <+> ppType fty)
S f x -> do S f x -> do
(f', fty) <- infer f (f', fty) <- inferLType gr g f
case fty of case fty of
Table arg val -> do Table arg val -> do
x'<- justCheck x arg x'<- justCheck g x arg
return (S f' x', val) return (S f' x', val)
_ -> checkError (text "table lintype expected for the table in" $$ nest 2 (ppTerm Unqualified 0 trm)) _ -> checkError (text "table lintype expected for the table in" $$ nest 2 (ppTerm Unqualified 0 trm))
P t i -> do P t i -> do
(t',ty) <- infer t --- ?? (t',ty) <- inferLType gr g t --- ??
ty' <- comp ty ty' <- computeLType gr g ty
let tr2 = P t' i let tr2 = P t' i
termWith tr2 $ case ty' of termWith tr2 $ case ty' of
RecType ts -> case lookup i ts of RecType ts -> case lookup i ts of
@@ -413,7 +390,7 @@ inferLType gr trm = case trm of
Just x -> return x Just x -> return x
_ -> checkError (text "record type expected for:" <+> ppTerm Unqualified 0 t $$ _ -> checkError (text "record type expected for:" <+> ppTerm Unqualified 0 t $$
text " instead of the inferred:" <+> ppTerm Unqualified 0 ty') text " instead of the inferred:" <+> ppTerm Unqualified 0 ty')
PI t i _ -> infer $ P t i PI t i _ -> inferLType gr g $ P t i
R r -> do R r -> do
let (ls,fs) = unzip r let (ls,fs) = unzip r
@@ -424,10 +401,10 @@ inferLType gr trm = case trm of
T (TTyped arg) pts -> do T (TTyped arg) pts -> do
(_,val) <- checks $ map (inferCase (Just arg)) pts (_,val) <- checks $ map (inferCase (Just arg)) pts
check trm (Table arg val) checkLType gr g trm (Table arg val)
T (TComp arg) pts -> do T (TComp arg) pts -> do
(_,val) <- checks $ map (inferCase (Just arg)) pts (_,val) <- checks $ map (inferCase (Just arg)) pts
check trm (Table arg val) checkLType gr g trm (Table arg val)
T ti pts -> do -- tries to guess: good in oper type inference T ti pts -> do -- tries to guess: good in oper type inference
let pts' = [pt | pt@(p,_) <- pts, isConstPatt p] let pts' = [pt | pt@(p,_) <- pts, isConstPatt p]
case pts' of case pts' of
@@ -435,9 +412,9 @@ inferLType gr trm = case trm of
---- PInt k : _ -> return $ Ints $ max [i | PInt i <- pts'] ---- PInt k : _ -> return $ Ints $ max [i | PInt i <- pts']
_ -> do _ -> do
(arg,val) <- checks $ map (inferCase Nothing) pts' (arg,val) <- checks $ map (inferCase Nothing) pts'
check trm (Table arg val) checkLType gr g trm (Table arg val)
V arg pts -> do V arg pts -> do
(_,val) <- checks $ map infer pts (_,val) <- checks $ map (inferLType gr g) pts
return (trm, Table arg val) return (trm, Table arg val)
K s -> do K s -> do
@@ -457,45 +434,45 @@ inferLType gr trm = case trm of
Empty -> return (trm, typeStr) Empty -> return (trm, typeStr)
C s1 s2 -> C s1 s2 ->
check2 (flip justCheck typeStr) C s1 s2 typeStr check2 (flip (justCheck g) typeStr) C s1 s2 typeStr
Glue s1 s2 -> Glue s1 s2 ->
check2 (flip justCheck typeStr) Glue s1 s2 typeStr ---- typeTok check2 (flip (justCheck g) typeStr) Glue s1 s2 typeStr ---- typeTok
---- hack from Rename.identRenameTerm, to live with files with naming conflicts 18/6/2007 ---- hack from Rename.identRenameTerm, to live with files with naming conflicts 18/6/2007
Strs (Cn c : ts) | c == cConflict -> do Strs (Cn c : ts) | c == cConflict -> do
checkWarn (text "unresolved constant, could be any of" <+> hcat (map (ppTerm Unqualified 0) ts)) checkWarn (text "unresolved constant, could be any of" <+> hcat (map (ppTerm Unqualified 0) ts))
infer (head ts) inferLType gr g (head ts)
Strs ts -> do Strs ts -> do
ts' <- mapM (\t -> justCheck t typeStr) ts ts' <- mapM (\t -> justCheck g t typeStr) ts
return (Strs ts', typeStrs) return (Strs ts', typeStrs)
Alts (t,aa) -> do Alts (t,aa) -> do
t' <- justCheck t typeStr t' <- justCheck g t typeStr
aa' <- flip mapM aa (\ (c,v) -> do aa' <- flip mapM aa (\ (c,v) -> do
c' <- justCheck c typeStr c' <- justCheck g c typeStr
v' <- checks $ map (justCheck v) [typeStrs, EPattType typeStr] v' <- checks $ map (justCheck g v) [typeStrs, EPattType typeStr]
return (c',v')) return (c',v'))
return (Alts (t',aa'), typeStr) return (Alts (t',aa'), typeStr)
RecType r -> do RecType r -> do
let (ls,ts) = unzip r let (ls,ts) = unzip r
ts' <- mapM (flip justCheck typeType) ts ts' <- mapM (flip (justCheck g) typeType) ts
return (RecType (zip ls ts'), typeType) return (RecType (zip ls ts'), typeType)
ExtR r s -> do ExtR r s -> do
(r',rT) <- infer r (r',rT) <- inferLType gr g r
rT' <- comp rT rT' <- computeLType gr g rT
(s',sT) <- infer s (s',sT) <- inferLType gr g s
sT' <- comp sT sT' <- computeLType gr g sT
let trm' = ExtR r' s' let trm' = ExtR r' s'
---- trm' <- checkErr $ plusRecord r' s' ---- trm' <- checkErr $ plusRecord r' s'
case (rT', sT') of case (rT', sT') of
(RecType rs, RecType ss) -> do (RecType rs, RecType ss) -> do
rt <- checkErr $ plusRecType rT' sT' rt <- checkErr $ plusRecType rT' sT'
check trm' rt ---- return (trm', rt) checkLType gr g trm' rt ---- return (trm', rt)
_ | rT' == typeType && sT' == typeType -> return (trm', typeType) _ | rT' == typeType && sT' == typeType -> return (trm', typeType)
_ -> checkError (text "records or record types expected in" <+> ppTerm Unqualified 0 trm) _ -> checkError (text "records or record types expected in" <+> ppTerm Unqualified 0 trm)
@@ -503,58 +480,50 @@ inferLType gr trm = case trm of
termWith trm $ return typeType termWith trm $ return typeType
Prod bt x a b -> do Prod bt x a b -> do
a' <- justCheck a typeType a' <- justCheck g a typeType
b' <- checkInContext [(bt,x,a')] $ justCheck b typeType b' <- justCheck ((bt,x,a'):g) b typeType
return (Prod bt x a' b', typeType) return (Prod bt x a' b', typeType)
Table p t -> do Table p t -> do
p' <- justCheck p typeType --- check p partype! p' <- justCheck g p typeType --- check p partype!
t' <- justCheck t typeType t' <- justCheck g t typeType
return $ (Table p' t', typeType) return $ (Table p' t', typeType)
FV vs -> do FV vs -> do
(_,ty) <- checks $ map infer vs (_,ty) <- checks $ map (inferLType gr g) vs
--- checkIfComplexVariantType trm ty --- checkIfComplexVariantType trm ty
check trm ty checkLType gr g trm ty
EPattType ty -> do EPattType ty -> do
ty' <- justCheck ty typeType ty' <- justCheck g ty typeType
return (EPattType ty',typeType) return (EPattType ty',typeType)
EPatt p -> do EPatt p -> do
ty <- inferPatt p ty <- inferPatt p
return (trm, EPattType ty) return (trm, EPattType ty)
ELin c trm -> do ELin c trm -> do
(trm',ty) <- infer trm (trm',ty) <- inferLType gr g trm
ty' <- checkErr $ lockRecType c ty ---- lookup c; remove lock AR 20/6/2009 ty' <- checkErr $ lockRecType c ty ---- lookup c; remove lock AR 20/6/2009
return $ (ELin c trm', ty') return $ (ELin c trm', ty')
_ -> checkError (text "cannot infer lintype of" <+> ppTerm Unqualified 0 trm) _ -> checkError (text "cannot infer lintype of" <+> ppTerm Unqualified 0 trm)
where where
env = gr
infer = inferLType env
comp = computeLType env
check = checkLType env
isPredef m = elem m [cPredef,cPredefAbs] isPredef m = elem m [cPredef,cPredefAbs]
justCheck ty te = check ty te >>= return . fst justCheck g ty te = checkLType gr g ty te >>= return . fst
-- for record fields, which may be typed -- for record fields, which may be typed
inferM (mty, t) = do inferM (mty, t) = do
(t', ty') <- case mty of (t', ty') <- case mty of
Just ty -> check ty t Just ty -> checkLType gr g ty t
_ -> infer t _ -> inferLType gr g t
return (Just ty',t') return (Just ty',t')
inferCase mty (patt,term) = do inferCase mty (patt,term) = do
arg <- maybe (inferPatt patt) return mty arg <- maybe (inferPatt patt) return mty
cont <- pattContext env arg patt cont <- pattContext gr g arg patt
i <- checkUpdates cont (_,val) <- inferLType gr (reverse cont ++ g) term
(_,val) <- infer term
checkResets i
return (arg,val) return (arg,val)
isConstPatt p = case p of isConstPatt p = case p of
PC _ ps -> True --- all isConstPatt ps PC _ ps -> True --- all isConstPatt ps
@@ -582,22 +551,21 @@ inferLType gr trm = case trm of
PRep _ -> return $ typeStr PRep _ -> return $ typeStr
PChar -> return $ typeStr PChar -> return $ typeStr
PChars _ -> return $ typeStr PChars _ -> return $ typeStr
_ -> infer (patt2term p) >>= return . snd _ -> inferLType gr g (patt2term p) >>= return . snd
-- type inference: Nothing, type checking: Just t -- type inference: Nothing, type checking: Just t
-- the latter permits matching with value type -- the latter permits matching with value type
getOverload :: SourceGrammar -> Maybe Type -> Term -> Check (Maybe (Term,Type)) getOverload :: SourceGrammar -> Context -> Maybe Type -> Term -> Check (Maybe (Term,Type))
getOverload env@gr mt ot = case appForm ot of getOverload gr g mt ot = case appForm ot of
(f@(Q m c), ts) -> case lookupOverload gr m c of (f@(Q m c), ts) -> case lookupOverload gr m c of
Ok typs -> do Ok typs -> do
ttys <- mapM infer ts ttys <- mapM (inferLType gr g) ts
v <- matchOverload f typs ttys v <- matchOverload f typs ttys
return $ Just v return $ Just v
_ -> return Nothing _ -> return Nothing
_ -> return Nothing _ -> return Nothing
where where
infer = inferLType env
matchOverload f typs ttys = do matchOverload f typs ttys = do
let (tts,tys) = unzip ttys let (tts,tys) = unzip ttys
let vfs = lookupOverloadInstance tys typs let vfs = lookupOverloadInstance tys typs
@@ -610,13 +578,13 @@ getOverload env@gr mt ot = case appForm ot of
return (mkApp fun tts, val) return (mkApp fun tts, val)
([],[]) -> do ([],[]) -> do
---- let prtType _ = prt -- to debug grammars ---- let prtType _ = prt -- to debug grammars
let showTypes ty = vcat (map (ppType env) ty) let showTypes ty = vcat (map ppType ty)
checkError $ text "no overload instance of" <+> ppTerm Unqualified 0 f $$ checkError $ text "no overload instance of" <+> ppTerm Unqualified 0 f $$
text "for" $$ text "for" $$
nest 2 (showTypes tys) $$ nest 2 (showTypes tys) $$
text "among" $$ text "among" $$
nest 2 (vcat [showTypes ty | (ty,_) <- typs]) $$ nest 2 (vcat [showTypes ty | (ty,_) <- typs]) $$
maybe empty (\x -> text "with value type" <+> ppType env x) mt maybe empty (\x -> text "with value type" <+> ppType x) mt
(vfs1,vfs2) -> case (noProds vfs1,noProds vfs2) of (vfs1,vfs2) -> case (noProds vfs1,noProds vfs2) of
([(val,fun)],_) -> do ([(val,fun)],_) -> do
@@ -632,9 +600,9 @@ getOverload env@gr mt ot = case appForm ot of
_ -> checkError $ text "ambiguous overloading of" <+> ppTerm Unqualified 0 f <+> _ -> checkError $ text "ambiguous overloading of" <+> ppTerm Unqualified 0 f <+>
text "for" <+> hsep (map (ppType env) tys) $$ text "for" <+> hsep (map ppType tys) $$
text "with alternatives" $$ text "with alternatives" $$
nest 2 (vcat [ppType env ty | (ty,_) <- if null vfs1 then vfs2 else vfs2]) nest 2 (vcat [ppType ty | (ty,_) <- if null vfs1 then vfs2 else vfs2])
matchVal mt v = elem mt [Nothing,Just v,Just (unlocked v)] matchVal mt v = elem mt [Nothing,Just v,Just (unlocked v)]
@@ -658,47 +626,44 @@ getOverload env@gr mt ot = case appForm ot of
Prod _ _ _ _ -> False Prod _ _ _ _ -> False
_ -> True _ -> True
checkLType :: SourceGrammar -> Term -> Type -> Check (Term, Type) checkLType :: SourceGrammar -> Context -> Term -> Type -> Check (Term, Type)
checkLType env trm typ0 = do checkLType gr g trm typ0 = do
typ <- comp typ0 typ <- computeLType gr g typ0
case trm of case trm of
Abs bt x c -> do Abs bt x c -> do
case typ of case typ of
Prod bt' z a b -> do Prod bt' z a b -> do
checkUpdate (bt,x,a)
(c',b') <- if isWildIdent z (c',b') <- if isWildIdent z
then check c b then checkLType gr ((bt,x,a):g) c b
else do else do b' <- checkIn (text "abs") $ substituteLType [(bt',z,Vr x)] b
b' <- checkIn (text "abs") $ substituteLType [(bt',z,Vr x)] b checkLType gr ((bt,x,a):g) c b'
check c b'
checkReset
return $ (Abs bt x c', Prod bt' x a b') return $ (Abs bt x c', Prod bt' x a b')
_ -> checkError $ text "function type expected instead of" <+> ppType env typ _ -> checkError $ text "function type expected instead of" <+> ppType typ
App f a -> do App f a -> do
over <- getOverload env (Just typ) trm over <- getOverload gr g (Just typ) trm
case over of case over of
Just trty -> return trty Just trty -> return trty
_ -> do _ -> do
(trm',ty') <- infer trm (trm',ty') <- inferLType gr g trm
termWith trm' $ checkEq typ ty' trm' termWith trm' $ checkEqLType gr g typ ty' trm'
Q _ _ -> do Q _ _ -> do
over <- getOverload env (Just typ) trm over <- getOverload gr g (Just typ) trm
case over of case over of
Just trty -> return trty Just trty -> return trty
_ -> do _ -> do
(trm',ty') <- infer trm (trm',ty') <- inferLType gr g trm
termWith trm' $ checkEq typ ty' trm' termWith trm' $ checkEqLType gr g typ ty' trm'
T _ [] -> T _ [] ->
checkError (text "found empty table in type" <+> ppTerm Unqualified 0 typ) checkError (text "found empty table in type" <+> ppTerm Unqualified 0 typ)
T _ cs -> case typ of T _ cs -> case typ of
Table arg val -> do Table arg val -> do
case allParamValues env arg of case allParamValues gr arg of
Ok vs -> do Ok vs -> do
let ps0 = map fst cs let ps0 = map fst cs
ps <- checkErr $ testOvershadow ps0 vs ps <- checkErr $ testOvershadow ps0 vs
@@ -709,7 +674,7 @@ checkLType env trm typ0 = do
_ -> return () -- happens with variable types _ -> return () -- happens with variable types
cs' <- mapM (checkCase arg val) cs cs' <- mapM (checkCase arg val) cs
return (T (TTyped arg) cs', typ) return (T (TTyped arg) cs', typ)
_ -> checkError $ text "table type expected for table instead of" $$ nest 2 (ppType env typ) _ -> checkError $ text "table type expected for table instead of" $$ nest 2 (ppType typ)
R r -> case typ of --- why needed? because inference may be too difficult R r -> case typ of --- why needed? because inference may be too difficult
RecType rr -> do RecType rr -> do
@@ -721,7 +686,7 @@ checkLType env trm typ0 = do
ExtR r s -> case typ of ExtR r s -> case typ of
_ | typ == typeType -> do _ | typ == typeType -> do
trm' <- comp trm trm' <- computeLType gr g trm
case trm' of case trm' of
RecType _ -> termWith trm $ return typeType RecType _ -> termWith trm $ return typeType
ExtR (Vr _) (RecType _) -> termWith trm $ return typeType ExtR (Vr _) (RecType _) -> termWith trm $ return typeType
@@ -729,87 +694,77 @@ checkLType env trm typ0 = do
_ -> checkError (text "invalid record type extension" <+> nest 2 (ppTerm Unqualified 0 trm)) _ -> checkError (text "invalid record type extension" <+> nest 2 (ppTerm Unqualified 0 trm))
RecType rr -> do RecType rr -> do
(r',ty,s') <- checks [ (r',ty,s') <- checks [
do (r',ty) <- infer r do (r',ty) <- inferLType gr g r
return (r',ty,s) return (r',ty,s)
, ,
do (s',ty) <- infer s do (s',ty) <- inferLType gr g s
return (s',ty,r) return (s',ty,r)
] ]
case ty of case ty of
RecType rr1 -> do RecType rr1 -> do
let (rr0,rr2) = recParts rr rr1 let (rr0,rr2) = recParts rr rr1
r2 <- justCheck r' rr0 r2 <- justCheck g r' rr0
s2 <- justCheck s' rr2 s2 <- justCheck g s' rr2
return $ (ExtR r2 s2, typ) return $ (ExtR r2 s2, typ)
_ -> checkError (text "record type expected in extension of" <+> ppTerm Unqualified 0 r $$ _ -> checkError (text "record type expected in extension of" <+> ppTerm Unqualified 0 r $$
text "but found" <+> ppTerm Unqualified 0 ty) text "but found" <+> ppTerm Unqualified 0 ty)
ExtR ty ex -> do ExtR ty ex -> do
r' <- justCheck r ty r' <- justCheck g r ty
s' <- justCheck s ex s' <- justCheck g s ex
return $ (ExtR r' s', typ) --- is this all? return $ (ExtR r' s', typ) --- is this all?
_ -> checkError (text "record extension not meaningful for" <+> ppTerm Unqualified 0 typ) _ -> checkError (text "record extension not meaningful for" <+> ppTerm Unqualified 0 typ)
FV vs -> do FV vs -> do
ttys <- mapM (flip check typ) vs ttys <- mapM (flip (checkLType gr g) typ) vs
--- checkIfComplexVariantType trm typ --- checkIfComplexVariantType trm typ
return (FV (map fst ttys), typ) --- typ' ? return (FV (map fst ttys), typ) --- typ' ?
S tab arg -> checks [ do S tab arg -> checks [ do
(tab',ty) <- infer tab (tab',ty) <- inferLType gr g tab
ty' <- comp ty ty' <- computeLType gr g ty
case ty' of case ty' of
Table p t -> do Table p t -> do
(arg',val) <- check arg p (arg',val) <- checkLType gr g arg p
checkEq typ t trm checkEqLType gr g typ t trm
return (S tab' arg', t) return (S tab' arg', t)
_ -> checkError (text "table type expected for applied table instead of" <+> ppType env ty') _ -> checkError (text "table type expected for applied table instead of" <+> ppType ty')
, do , do
(arg',ty) <- infer arg (arg',ty) <- inferLType gr g arg
ty' <- comp ty ty' <- computeLType gr g ty
(tab',_) <- check tab (Table ty' typ) (tab',_) <- checkLType gr g tab (Table ty' typ)
return (S tab' arg', typ) return (S tab' arg', typ)
] ]
Let (x,(mty,def)) body -> case mty of Let (x,(mty,def)) body -> case mty of
Just ty -> do Just ty -> do
(def',ty') <- check def ty (def',ty') <- checkLType gr g def ty
checkUpdate (Explicit,x,ty') body' <- justCheck ((Explicit,x,ty'):g) body typ
body' <- justCheck body typ
checkReset
return (Let (x,(Just ty',def')) body', typ) return (Let (x,(Just ty',def')) body', typ)
_ -> do _ -> do
(def',ty) <- infer def -- tries to infer type of local constant (def',ty) <- inferLType gr g def -- tries to infer type of local constant
check (Let (x,(Just ty,def')) body) typ checkLType gr g (Let (x,(Just ty,def')) body) typ
ELin c tr -> do ELin c tr -> do
tr1 <- checkErr $ unlockRecord c tr tr1 <- checkErr $ unlockRecord c tr
check tr1 typ checkLType gr g tr1 typ
_ -> do _ -> do
(trm',ty') <- infer trm (trm',ty') <- inferLType gr g trm
termWith trm' $ checkEq typ ty' trm' termWith trm' $ checkEqLType gr g typ ty' trm'
where where
cnc = env justCheck g ty te = checkLType gr g ty te >>= return . fst
infer = inferLType env
comp = computeLType env
check = checkLType env
justCheck ty te = check ty te >>= return . fst
checkEq = checkEqLType env
recParts rr t = (RecType rr1,RecType rr2) where recParts rr t = (RecType rr1,RecType rr2) where
(rr1,rr2) = partition (flip elem (map fst t) . fst) rr (rr1,rr2) = partition (flip elem (map fst t) . fst) rr
checkM rms (l,ty) = case lookup l rms of checkM rms (l,ty) = case lookup l rms of
Just (Just ty0,t) -> do Just (Just ty0,t) -> do
checkEq ty ty0 t checkEqLType gr g ty ty0 t
(t',ty') <- check t ty (t',ty') <- checkLType gr g t ty
return (l,(Just ty',t')) return (l,(Just ty',t'))
Just (_,t) -> do Just (_,t) -> do
(t',ty') <- check t ty (t',ty') <- checkLType gr g t ty
return (l,(Just ty',t')) return (l,(Just ty',t'))
_ -> checkError $ _ -> checkError $
if isLockLabel l if isLockLabel l
@@ -819,41 +774,39 @@ checkLType env trm typ0 = do
else text "cannot find value for label" <+> ppLabel l <+> text "in" <+> ppTerm Unqualified 0 (R rms) else text "cannot find value for label" <+> ppLabel l <+> text "in" <+> ppTerm Unqualified 0 (R rms)
checkCase arg val (p,t) = do checkCase arg val (p,t) = do
cont <- pattContext env arg p cont <- pattContext gr g arg p
i <- checkUpdates cont t' <- justCheck (reverse cont ++ g) t val
t' <- justCheck t val
checkResets i
return (p,t') return (p,t')
pattContext :: LTEnv -> Type -> Patt -> Check Context pattContext :: SourceGrammar -> Context -> Type -> Patt -> Check Context
pattContext env typ p = case p of pattContext env g typ p = case p of
PV x -> return [(Explicit,x,typ)] PV x -> return [(Explicit,x,typ)]
PP q c ps | q /= cPredef -> do ---- why this /=? AR 6/1/2006 PP q c ps | q /= cPredef -> do ---- why this /=? AR 6/1/2006
t <- checkErr $ lookupResType cnc q c t <- checkErr $ lookupResType env q c
let (cont,v) = typeFormCnc t let (cont,v) = typeFormCnc t
checkCond (text "wrong number of arguments for constructor in" <+> ppPatt Unqualified 0 p) checkCond (text "wrong number of arguments for constructor in" <+> ppPatt Unqualified 0 p)
(length cont == length ps) (length cont == length ps)
checkEqLType env typ v (patt2term p) checkEqLType env g typ v (patt2term p)
mapM (\((_,_,ty),p) -> pattContext env ty p) (zip cont ps) >>= return . concat mapM (\((_,_,ty),p) -> pattContext env g ty p) (zip cont ps) >>= return . concat
PR r -> do PR r -> do
typ' <- computeLType env typ typ' <- computeLType env g typ
case typ' of case typ' of
RecType t -> do RecType t -> do
let pts = [(ty,tr) | (l,tr) <- r, Just ty <- [lookup l t]] let pts = [(ty,tr) | (l,tr) <- r, Just ty <- [lookup l t]]
----- checkWarn $ prt p ++++ show pts ----- debug ----- checkWarn $ prt p ++++ show pts ----- debug
mapM (uncurry (pattContext env)) pts >>= return . concat mapM (uncurry (pattContext env g)) pts >>= return . concat
_ -> checkError (text "record type expected for pattern instead of" <+> ppTerm Unqualified 0 typ') _ -> checkError (text "record type expected for pattern instead of" <+> ppTerm Unqualified 0 typ')
PT t p' -> do PT t p' -> do
checkEqLType env typ t (patt2term p') checkEqLType env g typ t (patt2term p')
pattContext env typ p' pattContext env g typ p'
PAs x p -> do PAs x p -> do
g <- pattContext env typ p g' <- pattContext env g typ p
return $ (Explicit,x,typ):g return ((Explicit,x,typ):g')
PAlt p' q -> do PAlt p' q -> do
g1 <- pattContext env typ p' g1 <- pattContext env g typ p'
g2 <- pattContext env typ q g2 <- pattContext env g typ q
let pts = nub ([x | pt@(_,x,_) <- g1, notElem pt g2] ++ [x | pt@(_,x,_) <- g2, notElem pt g1]) let pts = nub ([x | pt@(_,x,_) <- g1, notElem pt g2] ++ [x | pt@(_,x,_) <- g2, notElem pt g1])
checkCond checkCond
(text "incompatible bindings of" <+> (text "incompatible bindings of" <+>
@@ -861,17 +814,16 @@ pattContext env typ p = case p of
text "in pattern alterantives" <+> ppPatt Unqualified 0 p) (null pts) text "in pattern alterantives" <+> ppPatt Unqualified 0 p) (null pts)
return g1 -- must be g1 == g2 return g1 -- must be g1 == g2
PSeq p q -> do PSeq p q -> do
g1 <- pattContext env typ p g1 <- pattContext env g typ p
g2 <- pattContext env typ q g2 <- pattContext env g typ q
return $ g1 ++ g2 return $ g1 ++ g2
PRep p' -> noBind typeStr p' PRep p' -> noBind typeStr p'
PNeg p' -> noBind typ p' PNeg p' -> noBind typ p'
_ -> return [] ---- check types! _ -> return [] ---- check types!
where where
cnc = env
noBind typ p' = do noBind typ p' = do
co <- pattContext env typ p' co <- pattContext env g typ p'
if not (null co) if not (null co)
then checkWarn (text "no variable bound inside pattern" <+> ppPatt Unqualified 0 p) then checkWarn (text "no variable bound inside pattern" <+> ppPatt Unqualified 0 p)
>> return [] >> return []
@@ -879,8 +831,6 @@ pattContext env typ p = case p of
-- auxiliaries -- auxiliaries
type LTEnv = SourceGrammar
termWith :: Term -> Check Type -> Check (Term, Type) termWith :: Term -> Check Type -> Check (Term, Type)
termWith t ct = do termWith t ct = do
ty <- ct ty <- ct
@@ -900,19 +850,19 @@ check2 chk con a b t = do
b' <- chk b b' <- chk b
return (con a' b', t) return (con a' b', t)
checkEqLType :: LTEnv -> Type -> Type -> Term -> Check Type checkEqLType :: SourceGrammar -> Context -> Type -> Type -> Term -> Check Type
checkEqLType env t u trm = do checkEqLType gr g t u trm = do
(b,t',u',s) <- checkIfEqLType env t u trm (b,t',u',s) <- checkIfEqLType gr g t u trm
case b of case b of
True -> return t' True -> return t'
False -> checkError $ text s <+> text "type of" <+> ppTerm Unqualified 0 trm $$ False -> checkError $ text s <+> text "type of" <+> ppTerm Unqualified 0 trm $$
text "expected:" <+> ppType env t $$ text "expected:" <+> ppType t $$
text "inferred:" <+> ppType env u text "inferred:" <+> ppType u
checkIfEqLType :: LTEnv -> Type -> Type -> Term -> Check (Bool,Type,Type,String) checkIfEqLType :: SourceGrammar -> Context -> Type -> Type -> Term -> Check (Bool,Type,Type,String)
checkIfEqLType env t u trm = do checkIfEqLType gr g t u trm = do
t' <- comp t t' <- computeLType gr g t
u' <- comp u u' <- computeLType gr g u
case t' == u' || alpha [] t' u' of case t' == u' || alpha [] t' u' of
True -> return (True,t',u',[]) True -> return (True,t',u',[])
-- forgive missing lock fields by only generating a warning. -- forgive missing lock fields by only generating a warning.
@@ -947,15 +897,15 @@ checkIfEqLType env t u trm = do
| t == typeInt, Just _ <- isTypeInts u -> True ---- why this ???? AR 11/12/2005 | t == typeInt, Just _ <- isTypeInts u -> True ---- why this ???? AR 11/12/2005
---- this should be made in Rename ---- this should be made in Rename
(Q m a, Q n b) | a == b -> elem m (allExtendsPlus env n) (Q m a, Q n b) | a == b -> elem m (allExtendsPlus gr n)
|| elem n (allExtendsPlus env m) || elem n (allExtendsPlus gr m)
|| m == n --- for Predef || m == n --- for Predef
(QC m a, QC n b) | a == b -> elem m (allExtendsPlus env n) (QC m a, QC n b) | a == b -> elem m (allExtendsPlus gr n)
|| elem n (allExtendsPlus env m) || elem n (allExtendsPlus gr m)
(QC m a, Q n b) | a == b -> elem m (allExtendsPlus env n) (QC m a, Q n b) | a == b -> elem m (allExtendsPlus gr n)
|| elem n (allExtendsPlus env m) || elem n (allExtendsPlus gr m)
(Q m a, QC n b) | a == b -> elem m (allExtendsPlus env n) (Q m a, QC n b) | a == b -> elem m (allExtendsPlus gr n)
|| elem n (allExtendsPlus env m) || elem n (allExtendsPlus gr m)
(Table a b, Table c d) -> alpha g a c && alpha g b d (Table a b, Table c d) -> alpha g a c && alpha g b d
(Vr x, Vr y) -> x == y || elem (x,y) g || elem (y,x) g (Vr x, Vr y) -> x == y || elem (x,y) g || elem (y,x) g
@@ -983,16 +933,15 @@ checkIfEqLType env t u trm = do
_ -> Bad "" _ -> Bad ""
sTypes = [typeStr, typeTok, typeString] sTypes = [typeStr, typeTok, typeString]
comp = computeLType env
-- printing a type with a lock field lock_C as C -- printing a type with a lock field lock_C as C
ppType :: LTEnv -> Type -> Doc ppType :: Type -> Doc
ppType env ty = ppType ty =
case ty of case ty of
RecType fs -> case filter isLockLabel $ map fst fs of RecType fs -> case filter isLockLabel $ map fst fs of
[lock] -> text (drop 5 (showIdent (label2ident lock))) [lock] -> text (drop 5 (showIdent (label2ident lock)))
_ -> ppTerm Unqualified 0 ty _ -> ppTerm Unqualified 0 ty
Prod _ x a b -> ppType env a <+> text "->" <+> ppType env b Prod _ x a b -> ppType a <+> text "->" <+> ppType b
_ -> ppTerm Unqualified 0 ty _ -> ppTerm Unqualified 0 ty
-- | linearization types and defaults -- | linearization types and defaults
@@ -1015,7 +964,7 @@ linTypeOfType cnc m typ = do
plusRecType vars val plusRecType vars val
return (Explicit,symb,rec) return (Explicit,symb,rec)
lookLin (_,c) = checks [ --- rather: update with defLinType ? lookLin (_,c) = checks [ --- rather: update with defLinType ?
checkErr (lookupLincat cnc m c) >>= computeLType cnc checkErr (lookupLincat cnc m c) >>= computeLType cnc []
,return defLinType ,return defLinType
] ]
@@ -1050,3 +999,9 @@ topoSortOpers st = do
return return
(\ops -> Bad (render (text "circular definitions:" <+> fsep (map ppIdent (head ops))))) (\ops -> Bad (render (text "circular definitions:" <+> fsep (map ppIdent (head ops)))))
eops eops
checkLookup :: Ident -> Context -> Check Type
checkLookup x g =
case [ty | (b,y,ty) <- g, x == y] of
[] -> checkError (text "unknown variable" <+> ppIdent x)
(ty:_) -> return ty

110
src/GF/Compile/Rename.hs
View File

@@ -22,7 +22,7 @@
-- Hence we can proceed by @fold@ing "from left to right". -- Hence we can proceed by @fold@ing "from left to right".
----------------------------------------------------------------------------- -----------------------------------------------------------------------------
module GF.Compile.Rename (renameGrammar, module GF.Compile.Rename (
renameSourceTerm, renameSourceTerm,
renameModule renameModule
) where ) where
@@ -32,6 +32,7 @@ import GF.Grammar.Values
import GF.Grammar.Predef import GF.Grammar.Predef
import GF.Infra.Modules import GF.Infra.Modules
import GF.Infra.Ident import GF.Infra.Ident
import GF.Infra.CheckM
import GF.Grammar.Macros import GF.Grammar.Macros
import GF.Grammar.Printer import GF.Grammar.Printer
import GF.Grammar.AppPredefined import GF.Grammar.AppPredefined
@@ -41,25 +42,21 @@ import GF.Data.Operations
import Control.Monad import Control.Monad
import Data.List (nub) import Data.List (nub)
import Debug.Trace (trace)
import Text.PrettyPrint import Text.PrettyPrint
renameGrammar :: SourceGrammar -> Err SourceGrammar
renameGrammar g = liftM (MGrammar . reverse) $ foldM renameModule [] (modules g)
-- | this gives top-level access to renaming term input in the cc command -- | this gives top-level access to renaming term input in the cc command
renameSourceTerm :: SourceGrammar -> Ident -> Term -> Err Term renameSourceTerm :: SourceGrammar -> Ident -> Term -> Check Term
renameSourceTerm g m t = do renameSourceTerm g m t = do
mo <- lookupModule g m mo <- checkErr $ lookupModule g m
status <- buildStatus g m mo status <- buildStatus g m mo
renameTerm status [] t renameTerm status [] t
renameModule :: [SourceModule] -> SourceModule -> Err [SourceModule] renameModule :: [SourceModule] -> SourceModule -> Check SourceModule
renameModule ms (name,mo) = errIn ("renaming module" +++ showIdent name) $ do renameModule ms (name,mo) = checkIn (text "renaming module" <+> ppIdent name) $ do
let js1 = jments mo let js1 = jments mo
status <- buildStatus (MGrammar ms) name mo status <- buildStatus (MGrammar ms) name mo
js2 <- mapsErrTree (renameInfo mo status) js1 js2 <- checkMap (renameInfo mo status) js1
return $ (name, mo {opens = map forceQualif (opens mo), jments = js2}) : ms return (name, mo {opens = map forceQualif (opens mo), jments = js2})
type Status = (StatusTree, [(OpenSpec Ident, StatusTree)]) type Status = (StatusTree, [(OpenSpec Ident, StatusTree)])
@@ -67,20 +64,20 @@ type StatusTree = BinTree Ident StatusInfo
type StatusInfo = Ident -> Term type StatusInfo = Ident -> Term
renameIdentTerm :: Status -> Term -> Err Term renameIdentTerm :: Status -> Term -> Check Term
renameIdentTerm env@(act,imps) t = renameIdentTerm env@(act,imps) t =
errIn (render (text "atomic term" <+> ppTerm Unqualified 0 t $$ text "given" <+> hsep (punctuate comma (map (ppIdent . fst) qualifs)))) $ checkIn (text "atomic term" <+> ppTerm Qualified 0 t $$ text "given" <+> hsep (punctuate comma (map (ppIdent . fst) qualifs))) $
case t of case t of
Vr c -> ident predefAbs c Vr c -> ident predefAbs c
Cn c -> ident (\_ s -> Bad s) c Cn c -> ident (\_ s -> checkError s) c
Q m' c | m' == cPredef {- && isInPredefined c -} -> return t Q m' c | m' == cPredef {- && isInPredefined c -} -> return t
Q m' c -> do Q m' c -> do
m <- lookupErr m' qualifs m <- checkErr (lookupErr m' qualifs)
f <- lookupTree showIdent c m f <- lookupTree showIdent c m
return $ f c return $ f c
QC m' c | m' == cPredef {- && isInPredefined c -} -> return t QC m' c | m' == cPredef {- && isInPredefined c -} -> return t
QC m' c -> do QC m' c -> do
m <- lookupErr m' qualifs m <- checkErr (lookupErr m' qualifs)
f <- lookupTree showIdent c m f <- lookupTree showIdent c m
return $ f c return $ f c
_ -> return t _ -> return t
@@ -92,28 +89,21 @@ renameIdentTerm env@(act,imps) t =
-- this facility is mainly for BWC with GF1: you need not import PredefAbs -- this facility is mainly for BWC with GF1: you need not import PredefAbs
predefAbs c s predefAbs c s
| isPredefCat c = return $ Q cPredefAbs c | isPredefCat c = return $ Q cPredefAbs c
| otherwise = Bad s | otherwise = checkError s
ident alt c = case lookupTree showIdent c act of ident alt c = case lookupTree showIdent c act of
Ok f -> return $ f c Ok f -> return $ f c
_ -> case lookupTreeManyAll showIdent opens c of _ -> case lookupTreeManyAll showIdent opens c of
[f] -> return $ f c [f] -> return $ f c
[] -> alt c (render (text "constant not found:" <+> ppIdent c)) [] -> alt c (text "constant not found:" <+> ppIdent c)
fs -> case nub [f c | f <- fs] of fs -> case nub [f c | f <- fs] of
[tr] -> return tr [tr] -> return tr
ts@(t:_) -> trace (render (text "Warning: conflict" <+> hsep (punctuate comma (map (ppTerm Qualified 0) ts)))) (return t) ts@(t:_) -> do checkWarn (text "conflict" <+> hsep (punctuate comma (map (ppTerm Qualified 0) ts)))
return t
-- a warning will be generated in CheckGrammar, and the head returned -- a warning will be generated in CheckGrammar, and the head returned
-- in next V: -- in next V:
-- Bad $ "conflicting imports:" +++ unwords (map prt ts) -- Bad $ "conflicting imports:" +++ unwords (map prt ts)
--- | would it make sense to optimize this by inlining?
renameIdentPatt :: Status -> Patt -> Err Patt
renameIdentPatt env p = do
let t = patt2term p
t' <- renameIdentTerm env t
term2patt t'
info2status :: Maybe Ident -> (Ident,Info) -> StatusInfo info2status :: Maybe Ident -> (Ident,Info) -> StatusInfo
info2status mq (c,i) = case i of info2status mq (c,i) = case i of
AbsFun _ _ Nothing -> maybe Con QC mq AbsFun _ _ Nothing -> maybe Con QC mq
@@ -128,11 +118,11 @@ tree2status o = case o of
OSimple i -> mapTree (info2status (Just i)) OSimple i -> mapTree (info2status (Just i))
OQualif i j -> mapTree (info2status (Just j)) OQualif i j -> mapTree (info2status (Just j))
buildStatus :: SourceGrammar -> Ident -> SourceModInfo -> Err Status buildStatus :: SourceGrammar -> Ident -> SourceModInfo -> Check Status
buildStatus gr c mo = let mo' = self2status c mo in do buildStatus gr c mo = let mo' = self2status c mo in do
let gr1 = MGrammar ((c,mo) : modules gr) let gr1 = MGrammar ((c,mo) : modules gr)
ops = [OSimple e | e <- allExtends gr1 c] ++ opens mo ops = [OSimple e | e <- allExtends gr1 c] ++ opens mo
mods <- mapM (lookupModule gr1 . openedModule) ops mods <- checkErr $ mapM (lookupModule gr1 . openedModule) ops
let sts = map modInfo2status $ zip ops mods let sts = map modInfo2status $ zip ops mods
return $ if isModCnc mo return $ if isModCnc mo
then (emptyBinTree, reverse sts) -- the module itself does not define any names then (emptyBinTree, reverse sts) -- the module itself does not define any names
@@ -148,10 +138,10 @@ forceQualif o = case o of
OSimple i -> OQualif i i OSimple i -> OQualif i i
OQualif _ i -> OQualif i i OQualif _ i -> OQualif i i
renameInfo :: SourceModInfo -> Status -> (Ident,Info) -> Err (Ident,Info) renameInfo :: SourceModInfo -> Status -> Ident -> Info -> Check Info
renameInfo mo status (i,info) = errIn renameInfo mo status i info = checkIn
(render (text "renaming definition of" <+> ppIdent i <+> ppPosition mo i)) $ (text "renaming definition of" <+> ppIdent i <+> ppPosition mo i) $
liftM ((,) i) $ case info of case info of
AbsCat pco pfs -> liftM2 AbsCat (renPerh (renameContext status) pco) AbsCat pco pfs -> liftM2 AbsCat (renPerh (renameContext status) pco)
(renPerh (mapM rent) pfs) (renPerh (mapM rent) pfs)
AbsFun pty pa ptr -> liftM3 AbsFun (ren pty) (return pa) (renPerh (mapM (renameEquation status [])) ptr) AbsFun pty pa ptr -> liftM3 AbsFun (ren pty) (return pa) (renPerh (mapM (renameEquation status [])) ptr)
@@ -175,7 +165,7 @@ renameInfo mo status (i,info) = errIn
renPerh ren (Just t) = liftM Just $ ren t renPerh ren (Just t) = liftM Just $ ren t
renPerh ren Nothing = return Nothing renPerh ren Nothing = return Nothing
renameTerm :: Status -> [Ident] -> Term -> Err Term renameTerm :: Status -> [Ident] -> Term -> Check Term
renameTerm env vars = ren vars where renameTerm env vars = ren vars where
ren vs trm = case trm of ren vs trm = case trm of
Abs b x t -> liftM (Abs b x) (ren (x:vs) t) Abs b x t -> liftM (Abs b x) (ren (x:vs) t)
@@ -202,13 +192,13 @@ renameTerm env vars = ren vars where
b' <- ren (x:vs) b b' <- ren (x:vs) b
return $ Let (x,(m',a')) b' return $ Let (x,(m',a')) b'
P t@(Vr r) l -- for constant t we know it is projection P t@(Vr r) l -- Here we have $r.l$ and this is ambiguous it could be either
| elem r vs -> return trm -- var proj first -- record projection from variable or constant $r$ or qualified expression with module $r$
| otherwise -> case renid (Q r (label2ident l)) of -- qualif second | elem r vs -> return trm -- try var proj first ..
Ok t -> return t | otherwise -> checks [ renid (Q r (label2ident l)) -- .. and qualified expression second.
_ -> case liftM (flip P l) $ renid t of , renid t >>= \t -> return (P t l) -- try as a constant at the end
Ok t -> return t -- const proj last , checkError (text "unknown qualified constant" <+> ppTerm Unqualified 0 trm)
_ -> Bad (render (text "unknown qualified constant" <+> ppTerm Qualified 0 trm)) ]
EPatt p -> do EPatt p -> do
(p',_) <- renpatt p (p',_) <- renpatt p
@@ -224,40 +214,42 @@ renameTerm env vars = ren vars where
renpatt = renamePattern env renpatt = renamePattern env
-- | vars not needed in env, since patterns always overshadow old vars -- | vars not needed in env, since patterns always overshadow old vars
renamePattern :: Status -> Patt -> Err (Patt,[Ident]) renamePattern :: Status -> Patt -> Check (Patt,[Ident])
renamePattern env patt = case patt of renamePattern env patt = case patt of
PMacro c -> do PMacro c -> do
c' <- renid $ Vr c c' <- renid $ Vr c
case c' of case c' of
Q p d -> renp $ PM p d Q p d -> renp $ PM p d
_ -> Bad (render (text "unresolved pattern" <+> ppPatt Unqualified 0 patt)) _ -> checkError (text "unresolved pattern" <+> ppPatt Unqualified 0 patt)
PC c ps -> do PC c ps -> do
c' <- renid $ Cn c c' <- renid $ Cn c
case c' of case c' of
QC m c -> renp $ PP m c ps QC m c -> do psvss <- mapM renp ps
Q _ _ -> Bad $ render (text "data constructor expected but" <+> ppTerm Qualified 0 c' <+> text "is found instead") let (ps,vs) = unzip psvss
_ -> Bad $ render (text "unresolved data constructor" <+> ppTerm Qualified 0 c') return (PP m c ps, concat vs)
Q _ _ -> checkError (text "data constructor expected but" <+> ppTerm Qualified 0 c' <+> text "is found instead")
_ -> checkError (text "unresolved data constructor" <+> ppTerm Qualified 0 c')
PP p c ps -> do PP p c ps -> do
(QC p' c') <- renid (QC p c)
(p', c') <- case renid (QC p c) of
Ok (QC p' c') -> return (p',c')
_ -> return (p,c) --- temporarily, for bw compat
psvss <- mapM renp ps psvss <- mapM renp ps
let (ps',vs) = unzip psvss let (ps',vs) = unzip psvss
return (PP p' c' ps', concat vs) return (PP p' c' ps', concat vs)
PM p c -> do PM p c -> do
(p', c') <- case renid (Q p c) of x <- renid (Q p c)
Ok (Q p' c') -> return (p',c') (p',c') <- case x of
_ -> Bad (render (text "not a pattern macro" <+> ppPatt Unqualified 0 patt)) (Q p' c') -> return (p',c')
_ -> checkError (text "not a pattern macro" <+> ppPatt Qualified 0 patt)
return (PM p' c', []) return (PM p' c', [])
PV x -> do case renid (Vr x) of PV x -> checks [ renid (Vr x) >>= \t' -> case t' of
Ok (QC m c) -> return (PP m c [],[]) QC m c -> return (PP m c [],[])
_ -> return (patt, [x]) _ -> checkError (text "not a constructor")
, return (patt, [x])
]
PR r -> do PR r -> do
let (ls,ps) = unzip r let (ls,ps) = unzip r
@@ -293,12 +285,12 @@ renamePattern env patt = case patt of
renp = renamePattern env renp = renamePattern env
renid = renameIdentTerm env renid = renameIdentTerm env
renameParam :: Status -> (Ident, Context) -> Err (Ident, Context) renameParam :: Status -> (Ident, Context) -> Check (Ident, Context)
renameParam env (c,co) = do renameParam env (c,co) = do
co' <- renameContext env co co' <- renameContext env co
return (c,co') return (c,co')
renameContext :: Status -> Context -> Err Context renameContext :: Status -> Context -> Check Context
renameContext b = renc [] where renameContext b = renc [] where
renc vs cont = case cont of renc vs cont = case cont of
(bt,x,t) : xts (bt,x,t) : xts
@@ -315,7 +307,7 @@ renameContext b = renc [] where
ren = renameTerm b ren = renameTerm b
-- | vars not needed in env, since patterns always overshadow old vars -- | vars not needed in env, since patterns always overshadow old vars
renameEquation :: Status -> [Ident] -> Equation -> Err Equation renameEquation :: Status -> [Ident] -> Equation -> Check Equation
renameEquation b vs (ps,t) = do renameEquation b vs (ps,t) = do
(ps',vs') <- liftM unzip $ mapM (renamePattern b) ps (ps',vs') <- liftM unzip $ mapM (renamePattern b) ps
t' <- renameTerm b (concat vs' ++ vs) t t' <- renameTerm b (concat vs' ++ vs) t

10
src/GF/Grammar/API.hs
View File

@@ -8,6 +8,7 @@ module GF.Grammar.API (
) where ) where
import GF.Infra.Ident import GF.Infra.Ident
import GF.Infra.CheckM
import GF.Infra.Modules (greatestResource) import GF.Infra.Modules (greatestResource)
import GF.Compile.GetGrammar import GF.Compile.GetGrammar
import GF.Grammar.Macros import GF.Grammar.Macros
@@ -16,7 +17,7 @@ import GF.Grammar.Printer
import GF.Grammar.Grammar import GF.Grammar.Grammar
import GF.Compile.Rename (renameSourceTerm) import GF.Compile.Rename (renameSourceTerm)
import GF.Compile.CheckGrammar (justCheckLTerm) import GF.Compile.CheckGrammar (inferLType)
import GF.Compile.Compute (computeConcrete) import GF.Compile.Compute (computeConcrete)
import GF.Data.Operations import GF.Data.Operations
@@ -36,9 +37,10 @@ checkTerm gr t = do
checkTermAny gr mo t checkTermAny gr mo t
checkTermAny :: Grammar -> Ident -> Term -> Err Term checkTermAny :: Grammar -> Ident -> Term -> Err Term
checkTermAny gr m t = do checkTermAny gr m t = (fmap fst . runCheck) $ do
t1 <- renameSourceTerm gr m t t <- renameSourceTerm gr m t
justCheckLTerm gr t1 (t,_) <- inferLType gr [] t
return t
computeTerm :: Grammar -> Term -> Err Term computeTerm :: Grammar -> Term -> Err Term
computeTerm = computeConcrete computeTerm = computeConcrete

62
src/GF/Infra/CheckM.hs
View File

@@ -14,9 +14,8 @@
module GF.Infra.CheckM module GF.Infra.CheckM
(Check, Message, runCheck, (Check, Message, runCheck,
checkError, checkCond, checkWarn, checkUpdate, checkInContext, checkError, checkCond, checkWarn,
checkUpdates, checkReset, checkResets, checkGetContext, checkErr, checkIn, checkMap
checkLookup, checkErr, checkIn, checkMap
) where ) where
import GF.Data.Operations import GF.Data.Operations
@@ -29,21 +28,21 @@ import Text.PrettyPrint
type Message = Doc type Message = Doc
data CheckResult a data CheckResult a
= Fail [Message] = Fail [Message]
| Success a Context [Message] | Success a [Message]
newtype Check a = Check {unCheck :: Context -> [Message] -> CheckResult a} newtype Check a = Check {unCheck :: Context -> [Message] -> CheckResult a}
instance Monad Check where instance Monad Check where
return x = Check (\ctxt msgs -> Success x ctxt msgs) return x = Check (\ctxt msgs -> Success x msgs)
f >>= g = Check (\ctxt msgs -> case unCheck f ctxt msgs of f >>= g = Check (\ctxt msgs -> case unCheck f ctxt msgs of
Success x ctxt msgs -> unCheck (g x) ctxt msgs Success x msgs -> unCheck (g x) ctxt msgs
Fail msgs -> Fail msgs) Fail msgs -> Fail msgs)
instance ErrorMonad Check where instance ErrorMonad Check where
raise s = checkError (text s) raise s = checkError (text s)
handle f h = Check (\ctxt msgs -> case unCheck f ctxt msgs of handle f h = Check (\ctxt msgs -> case unCheck f ctxt msgs of
Success x ctxt msgs -> Success x ctxt msgs Success x msgs -> Success x msgs
Fail (msg:msgs) -> unCheck (h (render msg)) ctxt msgs) Fail (msg:msgs) -> unCheck (h (render msg)) ctxt msgs)
checkError :: Message -> Check a checkError :: Message -> Check a
checkError msg = Check (\ctxt msgs -> Fail (msg : msgs)) checkError msg = Check (\ctxt msgs -> Fail (msg : msgs))
@@ -53,42 +52,13 @@ checkCond s b = if b then return () else checkError s
-- | warnings should be reversed in the end -- | warnings should be reversed in the end
checkWarn :: Message -> Check () checkWarn :: Message -> Check ()
checkWarn msg = Check (\ctxt msgs -> Success () ctxt ((text "Warning:" <+> msg) : msgs)) checkWarn msg = Check (\ctxt msgs -> Success () ((text "Warning:" <+> msg) : msgs))
checkUpdate :: Hypo -> Check () runCheck :: Check a -> Err (a,String)
checkUpdate d = Check (\ctxt msgs -> Success () (d:ctxt) msgs)
checkInContext :: [Hypo] -> Check r -> Check r
checkInContext g ch = do
i <- checkUpdates g
r <- ch
checkResets i
return r
checkUpdates :: [Hypo] -> Check Int
checkUpdates ds = mapM checkUpdate ds >> return (length ds)
checkReset :: Check ()
checkReset = checkResets 1
checkResets :: Int -> Check ()
checkResets i = Check (\ctxt msgs -> Success () (drop i ctxt) msgs)
checkGetContext :: Check Context
checkGetContext = Check (\ctxt msgs -> Success ctxt ctxt msgs)
checkLookup :: Ident -> Check Type
checkLookup x = do
co <- checkGetContext
case [ty | (b,y,ty) <- co, x == y] of
[] -> checkError (text "unknown variable" <+> ppIdent x)
(ty:_) -> return ty
runCheck :: Check a -> Either [Message] (a,Context,[Message])
runCheck c = runCheck c =
case unCheck c [] [] of case unCheck c [] [] of
Fail msgs -> Left msgs Fail msgs -> Bad ( render (vcat (reverse msgs)))
Success v ctxt msgs -> Right (v,ctxt,msgs) Success v msgs -> Ok (v, render (vcat (reverse msgs)))
checkMap :: (Ord a) => (a -> b -> Check b) -> Map.Map a b -> Check (Map.Map a b) checkMap :: (Ord a) => (a -> b -> Check b) -> Map.Map a b -> Check (Map.Map a b)
checkMap f map = do xs <- mapM (\(k,v) -> do v <- f k v checkMap f map = do xs <- mapM (\(k,v) -> do v <- f k v
@@ -102,6 +72,6 @@ checkErr (Bad err) = checkError (text err)
checkIn :: Doc -> Check a -> Check a checkIn :: Doc -> Check a -> Check a
checkIn msg c = Check $ \ctxt msgs -> checkIn msg c = Check $ \ctxt msgs ->
case unCheck c ctxt [] of case unCheck c ctxt [] of
Fail msgs' -> Fail ((msg $$ nest 3 (vcat (reverse msgs'))) : msgs) Fail msgs' -> Fail ((msg $$ nest 3 (vcat (reverse msgs'))) : msgs)
Success v ctxt' msgs' | null msgs' -> Success v ctxt' msgs Success v msgs' | null msgs' -> Success v msgs
| otherwise -> Success v ctxt' ((msg $$ nest 3 (vcat (reverse msgs'))) : msgs) | otherwise -> Success v ((msg $$ nest 3 (vcat (reverse msgs'))) : msgs)