mirror of
https://github.com/GrammaticalFramework/gf-core.git
synced 2026-04-23 11:42:49 -06:00
CheckGrammar is now using the printer in GF.Grammar.Printer. Fixed bug that was hiding the warnings
This commit is contained in:
@@ -21,7 +21,6 @@ import GF.Grammar.Grammar
|
|||||||
import GF.Infra.Ident
|
import GF.Infra.Ident
|
||||||
import GF.Infra.Option
|
import GF.Infra.Option
|
||||||
import qualified GF.Grammar.Macros as C
|
import qualified GF.Grammar.Macros as C
|
||||||
import GF.Grammar.PrGrammar (prt)
|
|
||||||
import GF.Data.Operations
|
import GF.Data.Operations
|
||||||
import Data.List
|
import Data.List
|
||||||
import qualified GF.Infra.Modules as M
|
import qualified GF.Infra.Modules as M
|
||||||
@@ -72,7 +71,7 @@ factor c i t = case t of
|
|||||||
|
|
||||||
--- we hope this will be fresh and don't check... in GFC would be safe
|
--- we hope this will be fresh and don't check... in GFC would be safe
|
||||||
|
|
||||||
qqIdent c i = identC (BS.pack ("q_" ++ prt c ++ "__" ++ show i))
|
qqIdent c i = identC (BS.pack ("q_" ++ showIdent c ++ "__" ++ show i))
|
||||||
|
|
||||||
|
|
||||||
-- we need to replace subterms
|
-- we need to replace subterms
|
||||||
|
|||||||
@@ -32,7 +32,7 @@ import GF.Compile.TypeCheck
|
|||||||
import GF.Compile.Refresh
|
import GF.Compile.Refresh
|
||||||
import GF.Grammar.Lexer
|
import GF.Grammar.Lexer
|
||||||
import GF.Grammar.Grammar
|
import GF.Grammar.Grammar
|
||||||
import GF.Grammar.PrGrammar
|
import GF.Grammar.Printer
|
||||||
import GF.Grammar.Lookup
|
import GF.Grammar.Lookup
|
||||||
import GF.Grammar.Predef
|
import GF.Grammar.Predef
|
||||||
import GF.Grammar.Macros
|
import GF.Grammar.Macros
|
||||||
@@ -45,43 +45,37 @@ import GF.Infra.CheckM
|
|||||||
|
|
||||||
import Data.List
|
import Data.List
|
||||||
import qualified Data.Set as Set
|
import qualified Data.Set as Set
|
||||||
import qualified Data.Map as Map
|
|
||||||
import Control.Monad
|
import Control.Monad
|
||||||
import Debug.Trace ---
|
import Text.PrettyPrint
|
||||||
|
|
||||||
|
|
||||||
showCheckModule :: [SourceModule] -> SourceModule -> Err ([SourceModule],String)
|
showCheckModule :: [SourceModule] -> SourceModule -> Err ([SourceModule],String)
|
||||||
showCheckModule mos m = do
|
showCheckModule mos m =
|
||||||
(st,(_,msg)) <- checkStart $ checkModule mos m
|
case runCheck (checkModule mos m) of
|
||||||
return (st, unlines $ reverse msg)
|
Left msgs -> Bad ( render (vcat (reverse msgs)))
|
||||||
|
Right (st,_,msgs) -> Ok (st, render (vcat (reverse msgs)))
|
||||||
mapsCheckTree ::
|
|
||||||
(Ord a) => ((a,b) -> Check (a,c)) -> BinTree a b -> Check (BinTree a c)
|
|
||||||
mapsCheckTree f = checkErr . mapsErrTree (\t -> checkStart (f t) >>= return . fst)
|
|
||||||
|
|
||||||
|
|
||||||
-- | 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 ("checking module" +++ prt 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)
|
||||||
js' <- case mtype mo of
|
js' <- case mtype mo of
|
||||||
MTAbstract -> mapsCheckTree (checkAbsInfo gr name mo) js
|
MTAbstract -> checkMap (checkAbsInfo gr name mo) js
|
||||||
|
|
||||||
MTTransfer a b -> mapsCheckTree (checkAbsInfo gr name mo) js
|
MTTransfer a b -> checkMap (checkAbsInfo gr name mo) js
|
||||||
|
|
||||||
MTResource -> mapsCheckTree (checkResInfo gr name mo) js
|
MTResource -> checkMap (checkResInfo gr name mo) js
|
||||||
|
|
||||||
MTConcrete a -> do
|
MTConcrete a -> do
|
||||||
checkErr $ topoSortOpers $ allOperDependencies name js
|
checkErr $ topoSortOpers $ allOperDependencies name js
|
||||||
abs <- checkErr $ lookupModule gr a
|
abs <- checkErr $ lookupModule gr a
|
||||||
js1 <- checkCompleteGrammar gr abs mo
|
js1 <- checkCompleteGrammar gr abs mo
|
||||||
mapsCheckTree (checkCncInfo gr name mo (a,abs)) js1
|
checkMap (checkCncInfo gr name mo (a,abs)) js1
|
||||||
|
|
||||||
MTInterface -> mapsCheckTree (checkResInfo gr name mo) js
|
MTInterface -> checkMap (checkResInfo gr name mo) js
|
||||||
|
|
||||||
MTInstance a -> do
|
MTInstance a -> do
|
||||||
mapsCheckTree (checkResInfo gr name mo) js
|
checkMap (checkResInfo gr name mo) js
|
||||||
|
|
||||||
return $ (name, replaceJudgements mo js') : ms
|
return $ (name, replaceJudgements mo js') : ms
|
||||||
where
|
where
|
||||||
@@ -104,22 +98,21 @@ checkRestrictedInheritance mos (name,mo) = do
|
|||||||
(f,cs) <- allDeps, incld f, let is = filter illegal cs, not (null is)]
|
(f,cs) <- allDeps, incld f, let is = filter illegal cs, not (null is)]
|
||||||
case illegals of
|
case illegals of
|
||||||
[] -> return ()
|
[] -> return ()
|
||||||
cs -> fail $ "In inherited module" +++ prt i ++
|
cs -> checkError (text "In inherited module" <+> ppIdent i <> text ", dependence of excluded constants:" $$
|
||||||
", dependence of excluded constants:" ++++
|
nest 2 (vcat [ppIdent f <+> text "on" <+> fsep (map ppIdent is) | (f,is) <- cs]))
|
||||||
unlines [" " ++ prt f +++ "on" +++ unwords (map prt 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
|
-- | check if a term is typable
|
||||||
justCheckLTerm :: SourceGrammar -> Term -> Err Term
|
justCheckLTerm :: SourceGrammar -> Term -> Err Term
|
||||||
justCheckLTerm src t = do
|
justCheckLTerm src t =
|
||||||
((t',_),_) <- checkStart (inferLType src t)
|
case runCheck (inferLType src t) of
|
||||||
return t'
|
Left msgs -> Bad ( render (vcat (reverse msgs)))
|
||||||
|
Right ((t',_),_,_) -> Ok t'
|
||||||
|
|
||||||
checkAbsInfo ::
|
checkAbsInfo ::
|
||||||
SourceGrammar -> Ident -> SourceModInfo -> (Ident,Info) -> Check (Ident,Info)
|
SourceGrammar -> Ident -> SourceModInfo -> Ident -> Info -> Check Info
|
||||||
checkAbsInfo st m mo (c,info) = do
|
checkAbsInfo st m mo c info = do
|
||||||
---- checkReservedId c
|
checkReservedId c
|
||||||
case info of
|
case info of
|
||||||
AbsCat (Just cont) _ -> mkCheck "category" $
|
AbsCat (Just cont) _ -> mkCheck "category" $
|
||||||
checkContext st cont ---- also cstrs
|
checkContext st cont ---- also cstrs
|
||||||
@@ -130,25 +123,16 @@ checkAbsInfo st m mo (c,info) = do
|
|||||||
case md of
|
case md of
|
||||||
Just eqs -> mkCheck "definition of function" $
|
Just eqs -> mkCheck "definition of function" $
|
||||||
checkDef st (m,c) typ eqs
|
checkDef st (m,c) typ eqs
|
||||||
Nothing -> return (c,info)
|
Nothing -> return info
|
||||||
return $ (c,AbsFun (Just typ) ma md)
|
return $ (AbsFun (Just typ) ma md)
|
||||||
_ -> return (c,info)
|
_ -> return info
|
||||||
where
|
where
|
||||||
mkCheck cat ss = case ss of
|
mkCheck cat ss = case ss of
|
||||||
[] -> return (c,info)
|
[] -> return info
|
||||||
_ -> checkErr $ Bad (unlines ss ++++ "in" +++ cat +++ prt c +++ pos c)
|
_ -> checkError (vcat (map text ss) $$ text "in" <+> text cat <+> ppIdent c <+> ppPosition mo c)
|
||||||
---- temporary solution when tc of defs is incomplete
|
|
||||||
mkCheckWarn cat ss = case ss of
|
|
||||||
[] -> return (c,info)
|
|
||||||
["[]"] -> return (c,info) ----
|
|
||||||
_ -> do
|
|
||||||
checkWarn (unlines ss ++++ "in" +++ cat +++ prt c +++ pos c)
|
|
||||||
return (c,info)
|
|
||||||
|
|
||||||
pos c = showPosition mo c
|
|
||||||
|
|
||||||
compAbsTyp g t = case t of
|
compAbsTyp g t = case t of
|
||||||
Vr x -> maybe (fail ("no value given to variable" +++ prt x)) return $ lookup x g
|
Vr x -> maybe (checkError (text "no value given to variable" <+> ppIdent x)) return $ lookup x g
|
||||||
Let (x,(_,a)) b -> do
|
Let (x,(_,a)) b -> do
|
||||||
a' <- compAbsTyp g a
|
a' <- compAbsTyp g a
|
||||||
compAbsTyp ((x, a'):g) b
|
compAbsTyp ((x, a'):g) b
|
||||||
@@ -169,8 +153,7 @@ checkCompleteGrammar gr abs cnc = do
|
|||||||
-- remove those lincat and lin in concrete that are not in abstract
|
-- remove those lincat and lin in concrete that are not in abstract
|
||||||
let unkn = filter (not . flip isInBinTree jsa) fsc
|
let unkn = filter (not . flip isInBinTree jsa) fsc
|
||||||
jsc1 <- if (null unkn) then return jsc else do
|
jsc1 <- if (null unkn) then return jsc else do
|
||||||
checkWarn $ "ignoring constants not in abstract:" +++
|
checkWarn $ text "ignoring constants not in abstract:" <+> fsep (map ppIdent unkn)
|
||||||
unwords (map prt unkn)
|
|
||||||
return $ filterBinTree (\f _ -> notElem f unkn) jsc
|
return $ filterBinTree (\f _ -> notElem f unkn) jsc
|
||||||
|
|
||||||
-- check that all abstract constants are in concrete; build default lincats
|
-- check that all abstract constants are in concrete; build default lincats
|
||||||
@@ -196,32 +179,30 @@ checkCompleteGrammar gr abs cnc = do
|
|||||||
Ok (CncFun cty Nothing pn) ->
|
Ok (CncFun cty 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 cty (Just def) pn) js
|
||||||
Bad _ -> do checkWarn $ "no linearization of" +++ prt 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 Nothing (Just def) Nothing) js
|
||||||
Bad _ -> do checkWarn $ "no linearization of" +++ prt 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
|
||||||
Ok (AnyInd _ _) -> return js
|
Ok (AnyInd _ _) -> return js
|
||||||
Ok (CncCat (Just _) _ _) -> return js
|
Ok (CncCat (Just _) _ _) -> return js
|
||||||
Ok (CncCat _ mt mp) -> do
|
Ok (CncCat _ mt mp) -> do
|
||||||
checkWarn $
|
checkWarn $
|
||||||
"no linearization type for" +++ prt c ++
|
text "no linearization type for" <+> ppIdent c <> text ", inserting default {s : Str}"
|
||||||
", inserting default {s : Str}"
|
|
||||||
return $ updateTree (c,CncCat (Just defLinType) mt mp) js
|
return $ updateTree (c,CncCat (Just defLinType) mt mp) js
|
||||||
_ -> do
|
_ -> do
|
||||||
checkWarn $
|
checkWarn $
|
||||||
"no linearization type for" +++ prt c ++
|
text "no linearization type for" <+> ppIdent c <> text ", inserting default {s : Str}"
|
||||||
", inserting default {s : Str}"
|
|
||||||
return $ updateTree (c,CncCat (Just defLinType) Nothing Nothing) js
|
return $ updateTree (c,CncCat (Just defLinType) Nothing Nothing) js
|
||||||
_ -> return js
|
_ -> return js
|
||||||
|
|
||||||
-- | 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 (Ident,Info)
|
checkResInfo :: SourceGrammar -> Ident -> SourceModInfo -> Ident -> Info -> Check Info
|
||||||
checkResInfo gr mo mm (c,info) = do
|
checkResInfo gr mo mm c info = do
|
||||||
checkReservedId c
|
checkReservedId c
|
||||||
case info of
|
case info of
|
||||||
ResOper pty pde -> chIn "operation" $ do
|
ResOper pty pde -> chIn "operation" $ do
|
||||||
@@ -234,47 +215,43 @@ checkResInfo gr mo mm (c,info) = do
|
|||||||
(de',ty') <- infer de
|
(de',ty') <- infer de
|
||||||
return (Just ty', Just de')
|
return (Just ty', Just de')
|
||||||
(_ , Nothing) -> do
|
(_ , Nothing) -> do
|
||||||
raise "No definition given to oper"
|
checkError (text "No definition given to the operation")
|
||||||
return (c, 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 check) 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 check)
|
||||||
[(mkFunType args val,tr) | (args,(val,tr)) <- tysts0]
|
[(mkFunType args val,tr) | (args,(val,tr)) <- tysts0]
|
||||||
let tysts2 = [(y,x) | (x,y) <- tysts1]
|
|
||||||
--- 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
|
||||||
checkUniq $
|
checkUniq $
|
||||||
sort [t : map snd xs | (x,_) <- tysts2, Ok (xs,t) <- [typeFormCnc x]]
|
sort [t : map snd xs | (_,x) <- tysts1, Ok (xs,t) <- [typeFormCnc x]]
|
||||||
return (c,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
|
||||||
---- mapM ((mapM (computeLType gr . snd)) . snd) pcs
|
|
||||||
mapM_ ((mapM_ (checkIfParType gr . snd)) . snd) pcs
|
|
||||||
ts <- checkErr $ lookupParamValues gr mo c
|
ts <- checkErr $ lookupParamValues gr mo c
|
||||||
return (c,ResParam (Just (pcs, Just ts)))
|
return (ResParam (Just (pcs, Just ts)))
|
||||||
|
|
||||||
_ -> return (c,info)
|
_ -> return info
|
||||||
where
|
where
|
||||||
infer = inferLType gr
|
infer = inferLType gr
|
||||||
check = checkLType gr
|
check = checkLType gr
|
||||||
chIn cat = checkIn ("Happened in" +++ cat +++ prt c +++ pos c +++ ":")
|
chIn cat = checkIn (text "Happened in" <+> text cat <+> ppIdent c <+> ppPosition mm c <+> colon)
|
||||||
comp = computeLType gr
|
comp = computeLType gr
|
||||||
pos c = showPosition mm c
|
|
||||||
|
|
||||||
checkUniq xss = case xss of
|
checkUniq xss = case xss of
|
||||||
x:y:xs
|
x:y:xs
|
||||||
| x == y -> raise $ "ambiguous for type" +++
|
| x == y -> checkError $ text "ambiguous for type" <+>
|
||||||
prtType gr (mkFunType (tail x) (head x))
|
ppType gr (mkFunType (tail x) (head x))
|
||||||
| otherwise -> checkUniq $ y:xs
|
| otherwise -> checkUniq $ y:xs
|
||||||
_ -> return ()
|
_ -> return ()
|
||||||
|
|
||||||
|
|
||||||
checkCncInfo :: SourceGrammar -> Ident -> SourceModInfo ->
|
checkCncInfo :: SourceGrammar -> Ident -> SourceModInfo ->
|
||||||
(Ident,SourceModInfo) ->
|
(Ident,SourceModInfo) ->
|
||||||
(Ident,Info) -> Check (Ident,Info)
|
Ident -> Info -> Check Info
|
||||||
checkCncInfo gr m mo (a,abs) (c,info) = do
|
checkCncInfo gr m mo (a,abs) c info = do
|
||||||
checkReservedId c
|
checkReservedId c
|
||||||
case info of
|
case info of
|
||||||
|
|
||||||
@@ -285,73 +262,28 @@ checkCncInfo gr m mo (a,abs) (c,info) = do
|
|||||||
(trm',_) <- check trm (mkFunType (map snd cont) val) -- erases arg vars
|
(trm',_) <- check trm (mkFunType (map snd cont) val) -- erases arg vars
|
||||||
checkPrintname gr mpr
|
checkPrintname gr mpr
|
||||||
cat <- return $ snd cat0
|
cat <- return $ snd cat0
|
||||||
return (c, CncFun (Just (cat,(cont,val))) (Just trm') mpr)
|
return (CncFun (Just (cat,(cont,val))) (Just trm') mpr)
|
||||||
-- cat for cf, typ for pe
|
-- cat for cf, typ for pe
|
||||||
|
|
||||||
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' <- checkIfLinType 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
|
||||||
return (c,CncCat (Just typ') mdef' mpr)
|
return (CncCat (Just typ') mdef' mpr)
|
||||||
|
|
||||||
_ -> checkResInfo gr m mo (c,info)
|
_ -> checkResInfo gr m mo c info
|
||||||
|
|
||||||
where
|
where
|
||||||
env = gr
|
env = gr
|
||||||
infer = inferLType gr
|
infer = inferLType gr
|
||||||
comp = computeLType gr
|
comp = computeLType gr
|
||||||
check = checkLType gr
|
check = checkLType gr
|
||||||
chIn cat = checkIn ("Happened in" +++ cat +++ prt c +++ pos c +++ ":")
|
chIn cat = checkIn (text "Happened in" <+> text cat <+> ppIdent c <+> ppPosition mo c <> colon)
|
||||||
pos c = showPosition mo c
|
|
||||||
|
|
||||||
checkIfParType :: SourceGrammar -> Type -> Check ()
|
|
||||||
checkIfParType st typ = checkCond ("Not parameter type" +++ prt typ) (isParType typ)
|
|
||||||
where
|
|
||||||
isParType ty = True ----
|
|
||||||
{- case ty of
|
|
||||||
Cn typ -> case lookupConcrete st typ of
|
|
||||||
Ok (CncParType _ _ _) -> True
|
|
||||||
Ok (CncOper _ ty' _) -> isParType ty'
|
|
||||||
_ -> False
|
|
||||||
Q p t -> case lookupInPackage st (p,t) of
|
|
||||||
Ok (CncParType _ _ _) -> True
|
|
||||||
_ -> False
|
|
||||||
RecType r -> all (isParType . snd) r
|
|
||||||
_ -> False
|
|
||||||
-}
|
|
||||||
|
|
||||||
checkIfStrType :: SourceGrammar -> Type -> Check ()
|
|
||||||
checkIfStrType st typ = case typ of
|
|
||||||
Table arg val -> do
|
|
||||||
checkIfParType st arg
|
|
||||||
checkIfStrType st val
|
|
||||||
_ | typ == typeStr -> return ()
|
|
||||||
_ -> prtFail "not a string type" typ
|
|
||||||
|
|
||||||
|
|
||||||
checkIfLinType :: SourceGrammar -> Type -> Check Type
|
|
||||||
checkIfLinType st typ0 = do
|
|
||||||
typ <- computeLType st typ0
|
|
||||||
{- ---- should check that not fun type
|
|
||||||
case typ of
|
|
||||||
RecType r -> do
|
|
||||||
let (lins,ihs) = partition (isLinLabel .fst) r
|
|
||||||
--- checkErr $ checkUnique $ map fst r
|
|
||||||
mapM_ checkInh ihs
|
|
||||||
mapM_ checkLin lins
|
|
||||||
_ -> prtFail "a linearization type cannot be" typ
|
|
||||||
-}
|
|
||||||
return typ
|
|
||||||
|
|
||||||
where
|
|
||||||
checkInh (label,typ) = checkIfParType st typ
|
|
||||||
checkLin (label,typ) = return () ---- checkIfStrType st typ
|
|
||||||
|
|
||||||
|
|
||||||
computeLType :: SourceGrammar -> Type -> Check Type
|
computeLType :: SourceGrammar -> Type -> Check Type
|
||||||
computeLType gr t = do
|
computeLType gr t = do
|
||||||
@@ -363,7 +295,7 @@ computeLType gr t = do
|
|||||||
_ | 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 ("module" +++ prt 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 ty' --- is this necessary to test?
|
||||||
|
|
||||||
@@ -412,17 +344,9 @@ checkPrintname _ _ = return ()
|
|||||||
-- | for grammars obtained otherwise than by parsing ---- update!!
|
-- | for grammars obtained otherwise than by parsing ---- update!!
|
||||||
checkReservedId :: Ident -> Check ()
|
checkReservedId :: Ident -> Check ()
|
||||||
checkReservedId x
|
checkReservedId x
|
||||||
| isReservedWord (ident2bs x) = checkWarn ("reserved word used as identifier:" +++ prt x)
|
| isReservedWord (ident2bs x) = checkWarn (text "reserved word used as identifier:" <+> ppIdent x)
|
||||||
| otherwise = return ()
|
| otherwise = return ()
|
||||||
|
|
||||||
-- to normalize records and record types
|
|
||||||
labelIndex :: Type -> Label -> Int
|
|
||||||
labelIndex ty lab = case ty of
|
|
||||||
RecType ts -> maybe (error ("label index" +++ prt lab)) id $ lookup lab $ labs ts
|
|
||||||
_ -> error $ "label index" +++ prt ty
|
|
||||||
where
|
|
||||||
labs ts = zip (map fst (sortRec ts)) [0..]
|
|
||||||
|
|
||||||
-- the underlying algorithms
|
-- the underlying algorithms
|
||||||
|
|
||||||
inferLType :: SourceGrammar -> Term -> Check (Term, Type)
|
inferLType :: SourceGrammar -> Term -> Check (Term, Type)
|
||||||
@@ -435,7 +359,7 @@ inferLType gr trm = case trm of
|
|||||||
,
|
,
|
||||||
checkErr (lookupResDef gr m ident) >>= infer
|
checkErr (lookupResDef gr m ident) >>= infer
|
||||||
,
|
,
|
||||||
prtFail "cannot infer type of constant" trm
|
checkError (text "cannot infer type of constant" <+> ppTerm Unqualified 0 trm)
|
||||||
]
|
]
|
||||||
|
|
||||||
QC m ident | isPredef m -> termWith trm $ checkErr (typPredefined ident)
|
QC m ident | isPredef m -> termWith trm $ checkErr (typPredefined ident)
|
||||||
@@ -445,7 +369,7 @@ inferLType gr trm = case trm of
|
|||||||
,
|
,
|
||||||
checkErr (lookupResDef gr m ident) >>= infer
|
checkErr (lookupResDef gr m ident) >>= infer
|
||||||
,
|
,
|
||||||
prtFail "cannot infer type of canonical constant" 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
|
||||||
@@ -471,8 +395,7 @@ inferLType gr trm = case trm of
|
|||||||
then return val
|
then return val
|
||||||
else substituteLType [(z,a')] val
|
else substituteLType [(z,a')] val
|
||||||
return (App f' a',ty)
|
return (App f' a',ty)
|
||||||
_ -> raise ("function type expected for"+++
|
_ -> checkError (text "A function type is expected for" <+> ppTerm Unqualified 0 f <+> text "instead of type" <+> ppType env fty)
|
||||||
prt f +++"instead of" +++ prtType env fty)
|
|
||||||
|
|
||||||
S f x -> do
|
S f x -> do
|
||||||
(f', fty) <- infer f
|
(f', fty) <- infer f
|
||||||
@@ -480,24 +403,25 @@ inferLType gr trm = case trm of
|
|||||||
Table arg val -> do
|
Table arg val -> do
|
||||||
x'<- justCheck x arg
|
x'<- justCheck x arg
|
||||||
return (S f' x', val)
|
return (S f' x', val)
|
||||||
_ -> prtFail "table lintype expected for the table in" 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) <- infer t --- ??
|
||||||
ty' <- comp ty
|
ty' <- comp ty
|
||||||
----- let tr2 = PI t' i (labelIndex ty' i)
|
|
||||||
let tr2 = P t' i
|
let tr2 = P t' i
|
||||||
termWith tr2 $ checkErr $ case ty' of
|
termWith tr2 $ case ty' of
|
||||||
RecType ts -> maybeErr ("unknown label" +++ prt i +++ "in" +++ prt ty') $
|
RecType ts -> case lookup i ts of
|
||||||
lookup i ts
|
Nothing -> checkError (text "unknown label" <+> ppLabel i <+> text "in" $$ nest 2 (ppTerm Unqualified 0 ty'))
|
||||||
_ -> prtBad ("record type expected for" +++ prt t +++ "instead of") ty'
|
Just x -> return x
|
||||||
|
_ -> checkError (text "record type expected for:" <+> ppTerm Unqualified 0 t $$
|
||||||
|
text " instead of the inferred:" <+> ppTerm Unqualified 0 ty')
|
||||||
PI t i _ -> infer $ P t i
|
PI t i _ -> infer $ P t i
|
||||||
|
|
||||||
R r -> do
|
R r -> do
|
||||||
let (ls,fs) = unzip r
|
let (ls,fs) = unzip r
|
||||||
fsts <- mapM inferM fs
|
fsts <- mapM inferM fs
|
||||||
let ts = [ty | (Just ty,_) <- fsts]
|
let ts = [ty | (Just ty,_) <- fsts]
|
||||||
checkCond ("cannot infer type of record"+++ prt trm) (length ts == length fsts)
|
checkCond (text "cannot infer type of record" $$ nest 2 (ppTerm Unqualified 0 trm)) (length ts == length fsts)
|
||||||
return $ (R (zip ls fsts), RecType (zip ls ts))
|
return $ (R (zip ls fsts), RecType (zip ls ts))
|
||||||
|
|
||||||
T (TTyped arg) pts -> do
|
T (TTyped arg) pts -> do
|
||||||
@@ -509,7 +433,7 @@ inferLType gr trm = case trm of
|
|||||||
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
|
||||||
[] -> prtFail "cannot infer table type of" trm
|
[] -> checkError (text "cannot infer table type of" <+> ppTerm Unqualified 0 trm)
|
||||||
---- 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'
|
||||||
@@ -542,9 +466,8 @@ inferLType gr trm = case trm of
|
|||||||
|
|
||||||
---- 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
|
||||||
trace ("WARNING: unresolved constant, could be any of" +++ unwords (map prt ts)) (infer $ head ts)
|
checkWarn (text "unresolved constant, could be any of" <+> hcat (map (ppTerm Unqualified 0) ts))
|
||||||
-- checkWarn ("unresolved constant, could be any of" +++ unwords (map prt ts))
|
infer (head ts)
|
||||||
-- infer $ head ts
|
|
||||||
|
|
||||||
Strs ts -> do
|
Strs ts -> do
|
||||||
ts' <- mapM (\t -> justCheck t typeStr) ts
|
ts' <- mapM (\t -> justCheck t typeStr) ts
|
||||||
@@ -576,7 +499,7 @@ inferLType gr trm = case trm of
|
|||||||
rt <- checkErr $ plusRecType rT' sT'
|
rt <- checkErr $ plusRecType rT' sT'
|
||||||
check trm' rt ---- return (trm', rt)
|
check trm' rt ---- return (trm', rt)
|
||||||
_ | rT' == typeType && sT' == typeType -> return (trm', typeType)
|
_ | rT' == typeType && sT' == typeType -> return (trm', typeType)
|
||||||
_ -> prtFail "records or record types expected in" trm
|
_ -> checkError (text "records or record types expected in" <+> ppTerm Unqualified 0 trm)
|
||||||
|
|
||||||
Sort _ ->
|
Sort _ ->
|
||||||
termWith trm $ return typeType
|
termWith trm $ return typeType
|
||||||
@@ -608,7 +531,7 @@ inferLType gr trm = case trm of
|
|||||||
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')
|
||||||
|
|
||||||
_ -> prtFail "cannot infer lintype of" trm
|
_ -> checkError (text "cannot infer lintype of" <+> ppTerm Unqualified 0 trm)
|
||||||
|
|
||||||
where
|
where
|
||||||
env = gr
|
env = gr
|
||||||
@@ -685,28 +608,23 @@ getOverload env@gr mt ot = case appForm ot of
|
|||||||
case ([vf | (vf,True) <- matches],[vf | (vf,False) <- matches]) of
|
case ([vf | (vf,True) <- matches],[vf | (vf,False) <- matches]) of
|
||||||
([(val,fun)],_) -> return (mkApp fun tts, val)
|
([(val,fun)],_) -> return (mkApp fun tts, val)
|
||||||
([],[(val,fun)]) -> do
|
([],[(val,fun)]) -> do
|
||||||
checkWarn ("ignoring lock fields in resolving" +++ prt ot)
|
checkWarn (text "ignoring lock fields in resolving" <+> ppTerm Unqualified 0 ot)
|
||||||
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 sought = unwords (map (prtType env) tys)
|
let showTypes ty = vcat (map (ppType env) ty)
|
||||||
let showTypes ty = case unwords (map (prtType env) ty) of
|
checkError $ text "no overload instance of" <+> ppTerm Unqualified 0 f $$
|
||||||
s | s == sought ->
|
text "for" $$
|
||||||
s +++ " -- i.e." +++ unwords (map prt ty) ++++
|
nest 2 (showTypes tys) $$
|
||||||
" where we sought" +++ unwords (map prt tys)
|
text "among" $$
|
||||||
s -> s
|
nest 2 (vcat [showTypes ty | (ty,_) <- typs]) $$
|
||||||
raise $ "no overload instance of" +++ prt f +++
|
maybe empty (\x -> text "with value type" <+> ppType env x) mt
|
||||||
"for" +++
|
|
||||||
sought +++
|
|
||||||
"among" ++++
|
|
||||||
unlines [" " ++ showTypes ty | (ty,_) <- typs] ++
|
|
||||||
maybe [] (("with value type" +++) . prtType env) mt
|
|
||||||
|
|
||||||
(vfs1,vfs2) -> case (noProds vfs1,noProds vfs2) of
|
(vfs1,vfs2) -> case (noProds vfs1,noProds vfs2) of
|
||||||
([(val,fun)],_) -> do
|
([(val,fun)],_) -> do
|
||||||
return (mkApp fun tts, val)
|
return (mkApp fun tts, val)
|
||||||
([],[(val,fun)]) -> do
|
([],[(val,fun)]) -> do
|
||||||
checkWarn ("ignoring lock fields in resolving" +++ prt ot)
|
checkWarn (text "ignoring lock fields in resolving" <+> ppTerm Unqualified 0 ot)
|
||||||
return (mkApp fun tts, val)
|
return (mkApp fun tts, val)
|
||||||
|
|
||||||
----- unsafely exclude irritating warning AR 24/5/2008
|
----- unsafely exclude irritating warning AR 24/5/2008
|
||||||
@@ -715,9 +633,10 @@ getOverload env@gr mt ot = case appForm ot of
|
|||||||
----- unlines [prtType env ty | (ty,_) <- vfs', not (noProd ty)]
|
----- unlines [prtType env ty | (ty,_) <- vfs', not (noProd ty)]
|
||||||
|
|
||||||
|
|
||||||
_ -> raise $ "ambiguous overloading of" +++ prt f +++
|
_ -> checkError $ text "ambiguous overloading of" <+> ppTerm Unqualified 0 f <+>
|
||||||
"for" +++ unwords (map (prtType env) tys) ++++ "with alternatives" ++++
|
text "for" <+> hsep (map (ppType env) tys) $$
|
||||||
unlines [prtType env ty | (ty,_) <- if (null vfs1) then vfs2 else vfs2]
|
text "with alternatives" $$
|
||||||
|
nest 2 (vcat [ppType env 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)]
|
||||||
|
|
||||||
@@ -755,11 +674,11 @@ checkLType env trm typ0 = do
|
|||||||
(c',b') <- if isWildIdent z
|
(c',b') <- if isWildIdent z
|
||||||
then check c b
|
then check c b
|
||||||
else do
|
else do
|
||||||
b' <- checkIn "abs" $ substituteLType [(z,Vr x)] b
|
b' <- checkIn (text "abs") $ substituteLType [(z,Vr x)] b
|
||||||
check c b'
|
check c b'
|
||||||
checkReset
|
checkReset
|
||||||
return $ (Abs x c', Prod x a b')
|
return $ (Abs x c', Prod x a b')
|
||||||
_ -> raise $ "function type expected instead of" +++ prtType env typ
|
_ -> checkError $ text "function type expected instead of" <+> ppType env typ
|
||||||
|
|
||||||
App f a -> do
|
App f a -> do
|
||||||
over <- getOverload env (Just typ) trm
|
over <- getOverload env (Just typ) trm
|
||||||
@@ -778,7 +697,7 @@ checkLType env trm typ0 = do
|
|||||||
termWith trm' $ checkEq typ ty' trm'
|
termWith trm' $ checkEq typ ty' trm'
|
||||||
|
|
||||||
T _ [] ->
|
T _ [] ->
|
||||||
prtFail "found empty table in type" 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 env arg of
|
||||||
@@ -787,20 +706,12 @@ checkLType env trm typ0 = do
|
|||||||
ps <- checkErr $ testOvershadow ps0 vs
|
ps <- checkErr $ testOvershadow ps0 vs
|
||||||
if null ps
|
if null ps
|
||||||
then return ()
|
then return ()
|
||||||
---- use this if you want to see where the error is
|
else checkWarn (text "patterns never reached:" $$
|
||||||
-- else raise $ "patterns never reached:" +++
|
nest 2 (vcat (map (ppPatt Unqualified 0) ps)))
|
||||||
-- concat (intersperse ", " (map prt ps))
|
|
||||||
---- else use this
|
|
||||||
else trace ("WARNING: patterns never reached:" +++
|
|
||||||
concat (intersperse ", " (map prt ps))) (return ())
|
|
||||||
---- AR 6/4/2009: this would be the best but checkWarn doesn't show because of laziness (?)
|
|
||||||
---- else checkWarn $ "patterns never reached:" +++
|
|
||||||
---- concat (intersperse ", " (map prt ps))
|
|
||||||
|
|
||||||
_ -> 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)
|
||||||
_ -> raise $ "table type expected for table instead of" +++ prtType env typ
|
_ -> checkError $ text "table type expected for table instead of" $$ nest 2 (ppType env 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
|
||||||
@@ -808,7 +719,7 @@ checkLType env trm typ0 = do
|
|||||||
fsts <- mapM (checkM r) rr -- check that they are found in the record
|
fsts <- mapM (checkM r) rr -- check that they are found in the record
|
||||||
return $ (R fsts, typ) -- normalize record
|
return $ (R fsts, typ) -- normalize record
|
||||||
|
|
||||||
_ -> prtFail "record type expected in type checking instead of" typ
|
_ -> checkError (text "record type expected in type checking instead of" $$ nest 2 (ppTerm Unqualified 0 typ))
|
||||||
|
|
||||||
ExtR r s -> case typ of
|
ExtR r s -> case typ of
|
||||||
_ | typ == typeType -> do
|
_ | typ == typeType -> do
|
||||||
@@ -817,7 +728,7 @@ checkLType env trm typ0 = do
|
|||||||
RecType _ -> termWith trm $ return typeType
|
RecType _ -> termWith trm $ return typeType
|
||||||
ExtR (Vr _) (RecType _) -> termWith trm $ return typeType
|
ExtR (Vr _) (RecType _) -> termWith trm $ return typeType
|
||||||
-- ext t = t ** ...
|
-- ext t = t ** ...
|
||||||
_ -> prtFail "invalid record type extension" 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) <- infer r
|
||||||
@@ -832,15 +743,15 @@ checkLType env trm typ0 = do
|
|||||||
r2 <- justCheck r' rr0
|
r2 <- justCheck r' rr0
|
||||||
s2 <- justCheck s' rr2
|
s2 <- justCheck s' rr2
|
||||||
return $ (ExtR r2 s2, typ)
|
return $ (ExtR r2 s2, typ)
|
||||||
_ -> raise ("record type expected in extension of" +++ prt r +++
|
_ -> checkError (text "record type expected in extension of" <+> ppTerm Unqualified 0 r $$
|
||||||
"but found" +++ prt ty)
|
text "but found" <+> ppTerm Unqualified 0 ty)
|
||||||
|
|
||||||
ExtR ty ex -> do
|
ExtR ty ex -> do
|
||||||
r' <- justCheck r ty
|
r' <- justCheck r ty
|
||||||
s' <- justCheck s ex
|
s' <- justCheck s ex
|
||||||
return $ (ExtR r' s', typ) --- is this all?
|
return $ (ExtR r' s', typ) --- is this all?
|
||||||
|
|
||||||
_ -> prtFail "record extension not meaningful for" 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 check typ) vs
|
||||||
@@ -855,8 +766,7 @@ checkLType env trm typ0 = do
|
|||||||
(arg',val) <- check arg p
|
(arg',val) <- check arg p
|
||||||
checkEq typ t trm
|
checkEq typ t trm
|
||||||
return (S tab' arg', t)
|
return (S tab' arg', t)
|
||||||
_ -> raise $ "table type expected for applied table instead of" +++
|
_ -> checkError (text "table type expected for applied table instead of" <+> ppType env ty')
|
||||||
prtType env ty'
|
|
||||||
, do
|
, do
|
||||||
(arg',ty) <- infer arg
|
(arg',ty) <- infer arg
|
||||||
ty' <- comp ty
|
ty' <- comp ty
|
||||||
@@ -903,14 +813,12 @@ checkLType env trm typ0 = do
|
|||||||
Just (_,t) -> do
|
Just (_,t) -> do
|
||||||
(t',ty') <- check t ty
|
(t',ty') <- check t ty
|
||||||
return (l,(Just ty',t'))
|
return (l,(Just ty',t'))
|
||||||
_ -> raise $
|
_ -> checkError $
|
||||||
if isLockLabel l
|
if isLockLabel l
|
||||||
then
|
then let cat = drop 5 (showIdent (label2ident l))
|
||||||
let cat = drop 5 (prt l) in
|
in ppTerm Unqualified 0 (R rms) <+> text "is not in the lincat of" <+> text cat <>
|
||||||
prt_ (R rms) +++ "is not in the lincat of" +++ cat ++
|
text "; try wrapping it with lin" <+> text cat
|
||||||
"; try wrapping it with lin " ++ cat
|
else text "cannot find value for label" <+> ppLabel l <+> text "in" <+> ppTerm Unqualified 0 (R rms)
|
||||||
else
|
|
||||||
"cannot find value for label" +++ prt l +++ "in" +++ prt_ (R rms)
|
|
||||||
|
|
||||||
checkCase arg val (p,t) = do
|
checkCase arg val (p,t) = do
|
||||||
cont <- pattContext env arg p
|
cont <- pattContext env arg p
|
||||||
@@ -925,7 +833,7 @@ pattContext env typ p = case p of
|
|||||||
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 cnc q c
|
||||||
(cont,v) <- checkErr $ typeFormCnc t
|
(cont,v) <- checkErr $ typeFormCnc t
|
||||||
checkCond ("wrong number of arguments for constructor in" +++ prt 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 typ v (patt2term p)
|
||||||
mapM (uncurry (pattContext env)) (zip (map snd cont) ps) >>= return . concat
|
mapM (uncurry (pattContext env)) (zip (map snd cont) ps) >>= return . concat
|
||||||
@@ -936,7 +844,7 @@ pattContext env typ p = case p of
|
|||||||
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)) pts >>= return . concat
|
||||||
_ -> prtFail "record type expected for pattern instead of" 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 typ t (patt2term p')
|
||||||
pattContext env typ p'
|
pattContext env typ p'
|
||||||
@@ -948,11 +856,11 @@ pattContext env typ p = case p of
|
|||||||
PAlt p' q -> do
|
PAlt p' q -> do
|
||||||
g1 <- pattContext env typ p'
|
g1 <- pattContext env typ p'
|
||||||
g2 <- pattContext env typ q
|
g2 <- pattContext env typ q
|
||||||
let pts = [pt | pt <- g1, notElem pt g2] ++ [pt | pt <- g2, notElem pt g1]
|
let pts = nub ([fst pt | pt <- g1, notElem pt g2] ++ [fst pt | pt <- g2, notElem pt g1])
|
||||||
checkCond
|
checkCond
|
||||||
("incompatible bindings of" +++
|
(text "incompatible bindings of" <+>
|
||||||
unwords (nub (map (prt . fst) pts))+++
|
fsep (map ppIdent pts) <+>
|
||||||
"in pattern alterantives" +++ prt 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 typ p
|
||||||
@@ -967,7 +875,7 @@ pattContext env typ p = case p of
|
|||||||
noBind typ p' = do
|
noBind typ p' = do
|
||||||
co <- pattContext env typ p'
|
co <- pattContext env typ p'
|
||||||
if not (null co)
|
if not (null co)
|
||||||
then checkWarn ("no variable bound inside pattern" +++ prt p)
|
then checkWarn (text "no variable bound inside pattern" <+> ppPatt Unqualified 0 p)
|
||||||
>> return []
|
>> return []
|
||||||
else return []
|
else return []
|
||||||
|
|
||||||
@@ -999,9 +907,9 @@ checkEqLType env t u trm = do
|
|||||||
(b,t',u',s) <- checkIfEqLType env t u trm
|
(b,t',u',s) <- checkIfEqLType env t u trm
|
||||||
case b of
|
case b of
|
||||||
True -> return t'
|
True -> return t'
|
||||||
False -> raise $ s +++ "type of" +++ prt trm +++
|
False -> checkError $ text s <+> text "type of" <+> ppTerm Unqualified 0 trm $$
|
||||||
": expected:" +++ prtType env t ++++
|
text "expected:" <+> ppType env t $$
|
||||||
"inferred:" +++ prtType env u
|
text "inferred:" <+> ppType env u
|
||||||
|
|
||||||
checkIfEqLType :: LTEnv -> Type -> Type -> Term -> Check (Bool,Type,Type,String)
|
checkIfEqLType :: LTEnv -> Type -> Type -> Term -> Check (Bool,Type,Type,String)
|
||||||
checkIfEqLType env t u trm = do
|
checkIfEqLType env t u trm = do
|
||||||
@@ -1013,7 +921,7 @@ checkIfEqLType env t u trm = do
|
|||||||
--- better: use a flag to forgive? (AR 31/1/2006)
|
--- better: use a flag to forgive? (AR 31/1/2006)
|
||||||
_ -> case missingLock [] t' u' of
|
_ -> case missingLock [] t' u' of
|
||||||
Ok lo -> do
|
Ok lo -> do
|
||||||
checkWarn $ "missing lock field" +++ unwords (map prt lo)
|
checkWarn $ text "missing lock field" <+> fsep (map ppLabel lo)
|
||||||
return (True,t',u',[])
|
return (True,t',u',[])
|
||||||
Bad s -> return (False,t',u',s)
|
Bad s -> return (False,t',u',s)
|
||||||
|
|
||||||
@@ -1066,7 +974,7 @@ checkIfEqLType env t u trm = do
|
|||||||
not (any (\ (k,b) -> alpha g a b && l == k) ts)]
|
not (any (\ (k,b) -> alpha g a b && l == k) ts)]
|
||||||
(locks,others) = partition isLockLabel ls
|
(locks,others) = partition isLockLabel ls
|
||||||
in case others of
|
in case others of
|
||||||
_:_ -> Bad $ "missing record fields" +++ unwords (map prt others)
|
_:_ -> Bad $ render (text "missing record fields:" <+> fsep (punctuate comma (map ppLabel others))
|
||||||
_ -> return locks
|
_ -> return locks
|
||||||
-- contravariance
|
-- contravariance
|
||||||
(Prod x a b, Prod y c d) -> do
|
(Prod x a b, Prod y c d) -> do
|
||||||
@@ -1079,24 +987,15 @@ checkIfEqLType env t u trm = do
|
|||||||
sTypes = [typeStr, typeTok, typeString]
|
sTypes = [typeStr, typeTok, typeString]
|
||||||
comp = computeLType env
|
comp = computeLType env
|
||||||
|
|
||||||
-- if prtType is misleading, print the full type
|
|
||||||
prtTypeF :: LTEnv -> Type -> Type -> String
|
|
||||||
prtTypeF env exp ty =
|
|
||||||
let pty = prtType env ty
|
|
||||||
in if pty == prtType env exp then prt ty else pty
|
|
||||||
|
|
||||||
-- printing a type with a lock field lock_C as C
|
-- printing a type with a lock field lock_C as C
|
||||||
prtType :: LTEnv -> Type -> String
|
ppType :: LTEnv -> Type -> Doc
|
||||||
prtType env ty = case ty of
|
ppType env ty =
|
||||||
RecType fs -> case filter isLockLabel $ map fst fs of
|
case ty of
|
||||||
[lock] -> (drop 5 $ prt lock) --- ++++ "Full form" +++ prt ty
|
RecType fs -> case filter isLockLabel $ map fst fs of
|
||||||
_ -> prtt ty
|
[lock] -> text (drop 5 (showIdent (label2ident lock)))
|
||||||
Prod x a b -> prtType env a +++ "->" +++ prtType env b
|
_ -> ppTerm Unqualified 0 ty
|
||||||
_ -> prtt ty
|
Prod x a b -> ppType env a <+> text "->" <+> ppType env b
|
||||||
where
|
_ -> ppTerm Unqualified 0 ty
|
||||||
prtt t = prt t
|
|
||||||
---- use computeLType gr to check if really equal to the cat with lock
|
|
||||||
|
|
||||||
|
|
||||||
-- | linearization types and defaults
|
-- | linearization types and defaults
|
||||||
linTypeOfType :: SourceGrammar -> Ident -> Type -> Check (Context,Type)
|
linTypeOfType :: SourceGrammar -> Ident -> Type -> Check (Context,Type)
|
||||||
@@ -1111,8 +1010,11 @@ linTypeOfType cnc m typ = do
|
|||||||
let vars = mkRecType varLabel $ replicate n typeStr
|
let vars = mkRecType varLabel $ replicate n typeStr
|
||||||
symb = argIdent n cat i
|
symb = argIdent n cat i
|
||||||
rec <- if n==0 then return val else
|
rec <- if n==0 then return val else
|
||||||
checkErr $ errIn ("extending" +++ prt vars +++ "with" +++ prt val) $
|
checkErr $ errIn (render (text "extending" $$
|
||||||
plusRecType vars val
|
nest 2 (ppTerm Unqualified 0 vars) $$
|
||||||
|
text "with" $$
|
||||||
|
nest 2 (ppTerm Unqualified 0 val))) $
|
||||||
|
plusRecType vars val
|
||||||
return (symb,rec)
|
return (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
|
||||||
@@ -1148,5 +1050,5 @@ topoSortOpers st = do
|
|||||||
let eops = topoTest st
|
let eops = topoTest st
|
||||||
either
|
either
|
||||||
return
|
return
|
||||||
(\ops -> Bad ("circular definitions:" +++ unwords (map prt (head ops))))
|
(\ops -> Bad (render (text "circular definitions:" <+> fsep (map ppIdent (head ops)))))
|
||||||
eops
|
eops
|
||||||
|
|||||||
@@ -38,7 +38,7 @@ traceD s t = t
|
|||||||
-- the main function: generate PGF from GF.
|
-- the main function: generate PGF from GF.
|
||||||
mkCanon2gfcc :: Options -> String -> SourceGrammar -> (String,D.PGF)
|
mkCanon2gfcc :: Options -> String -> SourceGrammar -> (String,D.PGF)
|
||||||
mkCanon2gfcc opts cnc gr =
|
mkCanon2gfcc opts cnc gr =
|
||||||
(prIdent abs, (canon2gfcc opts pars . reorder abs . canon2canon opts abs) gr)
|
(showIdent abs, (canon2gfcc opts pars . reorder abs . canon2canon opts abs) gr)
|
||||||
where
|
where
|
||||||
abs = err (const c) id $ M.abstractOfConcrete gr c where c = identC (BS.pack cnc)
|
abs = err (const c) id $ M.abstractOfConcrete gr c where c = identC (BS.pack cnc)
|
||||||
pars = mkParamLincat gr
|
pars = mkParamLincat gr
|
||||||
|
|||||||
@@ -198,7 +198,7 @@ importsOfModule (m,mi) = (modName m,depModInfo mi [])
|
|||||||
|
|
||||||
depInst (m,n) xs = modName m:modName n:xs
|
depInst (m,n) xs = modName m:modName n:xs
|
||||||
|
|
||||||
modName = prIdent
|
modName = showIdent
|
||||||
|
|
||||||
-- | options can be passed to the compiler by comments in @--#@, in the main file
|
-- | options can be passed to the compiler by comments in @--#@, in the main file
|
||||||
getOptionsFromFile :: FilePath -> IOE Options
|
getOptionsFromFile :: FilePath -> IOE Options
|
||||||
|
|||||||
@@ -58,7 +58,7 @@ extendModule gr (name,m)
|
|||||||
|
|
||||||
-- test that the module types match, and find out if the old is complete
|
-- test that the module types match, and find out if the old is complete
|
||||||
testErr (sameMType (mtype m) (mtype mo))
|
testErr (sameMType (mtype m) (mtype mo))
|
||||||
("illegal extension type to module" +++ prIdent name)
|
("illegal extension type to module" +++ showIdent name)
|
||||||
|
|
||||||
let isCompl = isCompleteModule m0
|
let isCompl = isCompleteModule m0
|
||||||
|
|
||||||
@@ -86,12 +86,12 @@ rebuildModule gr mo@(i,mi@(ModInfo mt stat fs_ me mw ops_ med_ js_ ps_)) = do
|
|||||||
-- add the information given in interface into an instance module
|
-- add the information given in interface into an instance module
|
||||||
Nothing -> do
|
Nothing -> do
|
||||||
testErr (null is || mstatus mi == MSIncomplete)
|
testErr (null is || mstatus mi == MSIncomplete)
|
||||||
("module" +++ prIdent i +++
|
("module" +++ showIdent i +++
|
||||||
"has open interfaces and must therefore be declared incomplete")
|
"has open interfaces and must therefore be declared incomplete")
|
||||||
case mt of
|
case mt of
|
||||||
MTInstance i0 -> do
|
MTInstance i0 -> do
|
||||||
m1 <- lookupModule gr i0
|
m1 <- lookupModule gr i0
|
||||||
testErr (isModRes m1) ("interface expected instead of" +++ prIdent i0)
|
testErr (isModRes m1) ("interface expected instead of" +++ showIdent i0)
|
||||||
js' <- extendMod gr False (i0,const True) i (jments m1) (jments mi)
|
js' <- extendMod gr False (i0,const True) i (jments m1) (jments mi)
|
||||||
--- to avoid double inclusions, in instance I of I0 = J0 ** ...
|
--- to avoid double inclusions, in instance I of I0 = J0 ** ...
|
||||||
case extends mi of
|
case extends mi of
|
||||||
@@ -110,7 +110,7 @@ rebuildModule gr mo@(i,mi@(ModInfo mt stat fs_ me mw ops_ med_ js_ ps_)) = do
|
|||||||
let stat' = ifNull MSComplete (const MSIncomplete)
|
let stat' = ifNull MSComplete (const MSIncomplete)
|
||||||
[i | i <- is, notElem i infs]
|
[i | i <- is, notElem i infs]
|
||||||
testErr (stat' == MSComplete || stat == MSIncomplete)
|
testErr (stat' == MSComplete || stat == MSIncomplete)
|
||||||
("module" +++ prIdent i +++ "remains incomplete")
|
("module" +++ showIdent i +++ "remains incomplete")
|
||||||
ModInfo mt0 _ fs me' _ ops0 _ js ps0 <- lookupModule gr ext
|
ModInfo mt0 _ fs me' _ ops0 _ js ps0 <- lookupModule gr ext
|
||||||
let ops1 = nub $
|
let ops1 = nub $
|
||||||
ops_ ++ -- N.B. js has been name-resolved already
|
ops_ ++ -- N.B. js has been name-resolved already
|
||||||
|
|||||||
@@ -54,16 +54,16 @@ unlock c = unlockRecord c -- return
|
|||||||
-- to look up a constant etc in a search tree --- why here? AR 29/5/2008
|
-- to look up a constant etc in a search tree --- why here? AR 29/5/2008
|
||||||
lookupIdent :: Ident -> BinTree Ident b -> Err b
|
lookupIdent :: Ident -> BinTree Ident b -> Err b
|
||||||
lookupIdent c t =
|
lookupIdent c t =
|
||||||
case lookupTree prIdent c t of
|
case lookupTree showIdent c t of
|
||||||
Ok v -> return v
|
Ok v -> return v
|
||||||
Bad _ -> Bad ("unknown identifier" +++ prIdent c)
|
Bad _ -> Bad ("unknown identifier" +++ showIdent c)
|
||||||
|
|
||||||
lookupIdentInfo :: ModInfo Ident a -> Ident -> Err a
|
lookupIdentInfo :: ModInfo Ident a -> Ident -> Err a
|
||||||
lookupIdentInfo mo i = lookupIdent i (jments mo)
|
lookupIdentInfo mo i = lookupIdent i (jments mo)
|
||||||
|
|
||||||
lookupIdentInfoIn :: ModInfo Ident a -> Ident -> Ident -> Err a
|
lookupIdentInfoIn :: ModInfo Ident a -> Ident -> Ident -> Err a
|
||||||
lookupIdentInfoIn mo m i =
|
lookupIdentInfoIn mo m i =
|
||||||
err (\s -> Bad (s +++ "in module" +++ prIdent m)) return $ lookupIdentInfo mo i
|
err (\s -> Bad (s +++ "in module" +++ showIdent m)) return $ lookupIdentInfo mo i
|
||||||
|
|
||||||
lookupResDef :: SourceGrammar -> Ident -> Ident -> Err Term
|
lookupResDef :: SourceGrammar -> Ident -> Ident -> Err Term
|
||||||
lookupResDef gr m c = liftM fst $ lookupResDefKind gr m c
|
lookupResDef gr m c = liftM fst $ lookupResDefKind gr m c
|
||||||
|
|||||||
@@ -214,7 +214,7 @@ freeVarsExp e = case e of
|
|||||||
_ -> [] --- thus applies to abstract syntax only
|
_ -> [] --- thus applies to abstract syntax only
|
||||||
|
|
||||||
ident2string :: Ident -> String
|
ident2string :: Ident -> String
|
||||||
ident2string = prIdent
|
ident2string = showIdent
|
||||||
{-
|
{-
|
||||||
tree :: (TrNode,[Tree]) -> Tree
|
tree :: (TrNode,[Tree]) -> Tree
|
||||||
tree = Tr
|
tree = Tr
|
||||||
|
|||||||
@@ -350,10 +350,10 @@ float2term = EFloat
|
|||||||
|
|
||||||
-- | create a terminal from identifier
|
-- | create a terminal from identifier
|
||||||
ident2terminal :: Ident -> Term
|
ident2terminal :: Ident -> Term
|
||||||
ident2terminal = K . prIdent
|
ident2terminal = K . showIdent
|
||||||
|
|
||||||
symbolOfIdent :: Ident -> String
|
symbolOfIdent :: Ident -> String
|
||||||
symbolOfIdent = prIdent
|
symbolOfIdent = showIdent
|
||||||
|
|
||||||
symid :: Ident -> String
|
symid :: Ident -> String
|
||||||
symid = symbolOfIdent
|
symid = symbolOfIdent
|
||||||
|
|||||||
@@ -753,7 +753,7 @@ happyReduction_3 (happy_x_4 `HappyStk`
|
|||||||
Ok x -> return x
|
Ok x -> return x
|
||||||
Bad msg -> fail msg
|
Bad msg -> fail msg
|
||||||
let poss = buildTree [(i,(fname,mkSrcSpan p)) | (i,p,_) <- jments]
|
let poss = buildTree [(i,(fname,mkSrcSpan p)) | (i,p,_) <- jments]
|
||||||
fname = prIdent id ++ ".gf"
|
fname = showIdent id ++ ".gf"
|
||||||
|
|
||||||
mkSrcSpan :: (Posn, Posn) -> (Int,Int)
|
mkSrcSpan :: (Posn, Posn) -> (Int,Int)
|
||||||
mkSrcSpan (Pn l1 _, Pn l2 _) = (l1,l2)
|
mkSrcSpan (Pn l1 _, Pn l2 _) = (l1,l2)
|
||||||
|
|||||||
@@ -117,7 +117,7 @@ ModDef
|
|||||||
Ok x -> return x
|
Ok x -> return x
|
||||||
Bad msg -> fail msg
|
Bad msg -> fail msg
|
||||||
let poss = buildTree [(i,(fname,mkSrcSpan p)) | (i,p,_) <- jments]
|
let poss = buildTree [(i,(fname,mkSrcSpan p)) | (i,p,_) <- jments]
|
||||||
fname = prIdent id ++ ".gf"
|
fname = showIdent id ++ ".gf"
|
||||||
|
|
||||||
mkSrcSpan :: (Posn, Posn) -> (Int,Int)
|
mkSrcSpan :: (Posn, Posn) -> (Int,Int)
|
||||||
mkSrcSpan (Pn l1 _, Pn l2 _) = (l1,l2)
|
mkSrcSpan (Pn l1 _, Pn l2 _) = (l1,l2)
|
||||||
@@ -278,7 +278,7 @@ TermDef
|
|||||||
|
|
||||||
FlagDef :: { Options }
|
FlagDef :: { Options }
|
||||||
FlagDef
|
FlagDef
|
||||||
: Posn Ident '=' Ident Posn {% case parseModuleOptions ["--" ++ prIdent $2 ++ "=" ++ prIdent $4] of
|
: Posn Ident '=' Ident Posn {% case parseModuleOptions ["--" ++ showIdent $2 ++ "=" ++ showIdent $4] of
|
||||||
Ok x -> return x
|
Ok x -> return x
|
||||||
Bad msg -> failLoc $1 msg }
|
Bad msg -> failLoc $1 msg }
|
||||||
|
|
||||||
@@ -626,7 +626,7 @@ listCatDef id pos cont size = [catd,nilfund,consfund]
|
|||||||
mkId x i = if isWildIdent x then (varX i) else x
|
mkId x i = if isWildIdent x then (varX i) else x
|
||||||
|
|
||||||
tryLoc (c,mty,Just e) = return (c,(mty,e))
|
tryLoc (c,mty,Just e) = return (c,(mty,e))
|
||||||
tryLoc (c,_ ,_ ) = fail ("local definition of" +++ prIdent c +++ "without value")
|
tryLoc (c,_ ,_ ) = fail ("local definition of" +++ showIdent c +++ "without value")
|
||||||
|
|
||||||
mkR [] = return $ RecType [] --- empty record always interpreted as record type
|
mkR [] = return $ RecType [] --- empty record always interpreted as record type
|
||||||
mkR fs@(f:_) =
|
mkR fs@(f:_) =
|
||||||
@@ -635,10 +635,10 @@ mkR fs@(f:_) =
|
|||||||
_ -> mapM tryR fs >>= return . R
|
_ -> mapM tryR fs >>= return . R
|
||||||
where
|
where
|
||||||
tryRT (lab,Just ty,Nothing) = return (ident2label lab,ty)
|
tryRT (lab,Just ty,Nothing) = return (ident2label lab,ty)
|
||||||
tryRT (lab,_ ,_ ) = fail $ "illegal record type field" +++ prIdent lab --- manifest fields ?!
|
tryRT (lab,_ ,_ ) = fail $ "illegal record type field" +++ showIdent lab --- manifest fields ?!
|
||||||
|
|
||||||
tryR (lab,mty,Just t) = return (ident2label lab,(mty,t))
|
tryR (lab,mty,Just t) = return (ident2label lab,(mty,t))
|
||||||
tryR (lab,_ ,_ ) = fail $ "illegal record field" +++ prIdent lab
|
tryR (lab,_ ,_ ) = fail $ "illegal record field" +++ showIdent lab
|
||||||
|
|
||||||
mkOverload pdt pdf@(Just df) =
|
mkOverload pdt pdf@(Just df) =
|
||||||
case appForm df of
|
case appForm df of
|
||||||
@@ -660,8 +660,8 @@ mkOverload pdt pdf = [ResOper pdt pdf]
|
|||||||
|
|
||||||
isOverloading t =
|
isOverloading t =
|
||||||
case t of
|
case t of
|
||||||
Vr keyw | prIdent keyw == "overload" -> True -- overload is a "soft keyword"
|
Vr keyw | showIdent keyw == "overload" -> True -- overload is a "soft keyword"
|
||||||
_ -> False
|
_ -> False
|
||||||
|
|
||||||
|
|
||||||
type SrcSpan = (Posn,Posn)
|
type SrcSpan = (Posn,Posn)
|
||||||
|
|||||||
@@ -235,7 +235,7 @@ ppDDecl q (id,typ)
|
|||||||
| id == identW = ppTerm q 6 typ
|
| id == identW = ppTerm q 6 typ
|
||||||
| otherwise = parens (ppIdent id <+> colon <+> ppTerm q 0 typ)
|
| otherwise = parens (ppIdent id <+> colon <+> ppTerm q 0 typ)
|
||||||
|
|
||||||
ppIdent = text . prIdent
|
ppIdent = text . showIdent
|
||||||
|
|
||||||
ppQIdent q m id =
|
ppQIdent q m id =
|
||||||
case q of
|
case q of
|
||||||
|
|||||||
@@ -12,33 +12,51 @@
|
|||||||
-- (Description of the module)
|
-- (Description of the module)
|
||||||
-----------------------------------------------------------------------------
|
-----------------------------------------------------------------------------
|
||||||
|
|
||||||
module GF.Infra.CheckM (Check,
|
module GF.Infra.CheckM
|
||||||
|
(Check, Message, runCheck,
|
||||||
checkError, checkCond, checkWarn, checkUpdate, checkInContext,
|
checkError, checkCond, checkWarn, checkUpdate, checkInContext,
|
||||||
checkUpdates, checkReset, checkResets, checkGetContext,
|
checkUpdates, checkReset, checkResets, checkGetContext,
|
||||||
checkLookup, checkStart, checkErr, checkVal, checkIn,
|
checkLookup, checkErr, checkIn, checkMap
|
||||||
prtFail
|
|
||||||
) where
|
) where
|
||||||
|
|
||||||
import GF.Data.Operations
|
import GF.Data.Operations
|
||||||
import GF.Grammar.Grammar
|
|
||||||
import GF.Infra.Ident
|
import GF.Infra.Ident
|
||||||
import GF.Grammar.PrGrammar
|
import GF.Grammar.Grammar
|
||||||
|
import GF.Grammar.Printer
|
||||||
|
|
||||||
-- | the strings are non-fatal warnings
|
import qualified Data.Map as Map
|
||||||
type Check a = STM (Context,[String]) a
|
import Text.PrettyPrint
|
||||||
|
|
||||||
checkError :: String -> Check a
|
type Message = Doc
|
||||||
checkError = raise
|
data CheckResult a
|
||||||
|
= Fail [Message]
|
||||||
|
| Success a Context [Message]
|
||||||
|
newtype Check a = Check {unCheck :: Context -> [Message] -> CheckResult a}
|
||||||
|
|
||||||
checkCond :: String -> Bool -> Check ()
|
instance Monad Check where
|
||||||
|
return x = Check (\ctxt msgs -> Success x ctxt msgs)
|
||||||
|
f >>= g = Check (\ctxt msgs -> case unCheck f ctxt msgs of
|
||||||
|
Success x ctxt msgs -> unCheck (g x) ctxt msgs
|
||||||
|
Fail msgs -> Fail msgs)
|
||||||
|
|
||||||
|
instance ErrorMonad Check where
|
||||||
|
raise s = checkError (text s)
|
||||||
|
handle f h = Check (\ctxt msgs -> case unCheck f ctxt msgs of
|
||||||
|
Success x ctxt msgs -> Success x ctxt msgs
|
||||||
|
Fail (msg:msgs) -> unCheck (h (render msg)) ctxt msgs)
|
||||||
|
|
||||||
|
checkError :: Message -> Check a
|
||||||
|
checkError msg = Check (\ctxt msgs -> Fail (msg : msgs))
|
||||||
|
|
||||||
|
checkCond :: Message -> Bool -> Check ()
|
||||||
checkCond s b = if b then return () else checkError s
|
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 :: String -> Check ()
|
checkWarn :: Message -> Check ()
|
||||||
checkWarn s = updateSTM (\ (cont,msg) -> (cont, ("Warning: "++s):msg))
|
checkWarn msg = Check (\ctxt msgs -> Success () ctxt ((text "Warning:" <+> msg) : msgs))
|
||||||
|
|
||||||
checkUpdate :: Decl -> Check ()
|
checkUpdate :: Decl -> Check ()
|
||||||
checkUpdate d = updateSTM (\ (cont,msg) -> (d:cont, msg))
|
checkUpdate d = Check (\ctxt msgs -> Success () (d:ctxt) msgs)
|
||||||
|
|
||||||
checkInContext :: [Decl] -> Check r -> Check r
|
checkInContext :: [Decl] -> Check r -> Check r
|
||||||
checkInContext g ch = do
|
checkInContext g ch = do
|
||||||
@@ -54,36 +72,36 @@ checkReset :: Check ()
|
|||||||
checkReset = checkResets 1
|
checkReset = checkResets 1
|
||||||
|
|
||||||
checkResets :: Int -> Check ()
|
checkResets :: Int -> Check ()
|
||||||
checkResets i = updateSTM (\ (cont,msg) -> (drop i cont, msg))
|
checkResets i = Check (\ctxt msgs -> Success () (drop i ctxt) msgs)
|
||||||
|
|
||||||
checkGetContext :: Check Context
|
checkGetContext :: Check Context
|
||||||
checkGetContext = do
|
checkGetContext = Check (\ctxt msgs -> Success ctxt ctxt msgs)
|
||||||
(co,_) <- readSTM
|
|
||||||
return co
|
|
||||||
|
|
||||||
checkLookup :: Ident -> Check Type
|
checkLookup :: Ident -> Check Type
|
||||||
checkLookup x = do
|
checkLookup x = do
|
||||||
co <- checkGetContext
|
co <- checkGetContext
|
||||||
checkErr $ maybe (prtBad "unknown variable" x) return $ lookup x co
|
case lookup x co of
|
||||||
|
Nothing -> checkError (text "unknown variable" <+> ppIdent x)
|
||||||
|
Just ty -> return ty
|
||||||
|
|
||||||
checkStart :: Check a -> Err (a,(Context,[String]))
|
runCheck :: Check a -> Either [Message] (a,Context,[Message])
|
||||||
checkStart c = appSTM c ([],[])
|
runCheck c =
|
||||||
|
case unCheck c [] [] of
|
||||||
|
Fail msgs -> Left msgs
|
||||||
|
Success v ctxt msgs -> Right (v,ctxt,msgs)
|
||||||
|
|
||||||
|
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
|
||||||
|
return (k,v)) (Map.toList map)
|
||||||
|
return (Map.fromAscList xs)
|
||||||
|
|
||||||
checkErr :: Err a -> Check a
|
checkErr :: Err a -> Check a
|
||||||
checkErr e = stm (\s -> do
|
checkErr (Ok x) = return x
|
||||||
v <- e
|
checkErr (Bad err) = checkError (text err)
|
||||||
return (v,s)
|
|
||||||
)
|
|
||||||
|
|
||||||
checkVal :: a -> Check a
|
checkIn :: Doc -> Check a -> Check a
|
||||||
checkVal v = return v
|
checkIn msg c = Check $ \ctxt msgs ->
|
||||||
|
case unCheck c ctxt [] of
|
||||||
prtFail :: Print a => String -> a -> Check b
|
Fail msgs' -> Fail ((msg $$ nest 3 (vcat (reverse msgs'))) : msgs)
|
||||||
prtFail s t = checkErr $ prtBad s t
|
Success v ctxt' msgs' | null msgs' -> Success v ctxt' msgs
|
||||||
|
| otherwise -> Success v ctxt' ((msg $$ nest 3 (vcat (reverse msgs'))) : msgs)
|
||||||
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
|
|
||||||
|
|||||||
@@ -18,16 +18,16 @@ prDepGraph deps = unlines $ [
|
|||||||
"}"
|
"}"
|
||||||
]
|
]
|
||||||
where
|
where
|
||||||
mkNode (i,dep) = unwords [prIdent i, "[",nodeAttr (modtype dep),"]"]
|
mkNode (i,dep) = unwords [showIdent i, "[",nodeAttr (modtype dep),"]"]
|
||||||
nodeAttr ty = case ty of
|
nodeAttr ty = case ty of
|
||||||
MTAbstract -> "style = \"solid\", shape = \"box\""
|
MTAbstract -> "style = \"solid\", shape = \"box\""
|
||||||
MTConcrete _ -> "style = \"solid\", shape = \"ellipse\""
|
MTConcrete _ -> "style = \"solid\", shape = \"ellipse\""
|
||||||
_ -> "style = \"dashed\", shape = \"ellipse\""
|
_ -> "style = \"dashed\", shape = \"ellipse\""
|
||||||
mkArrows (i,dep) =
|
mkArrows (i,dep) =
|
||||||
[unwords [prIdent i,"->",prIdent j,"[",arrowAttr "of","]"] | j <- ofs dep] ++
|
[unwords [showIdent i,"->",showIdent j,"[",arrowAttr "of","]"] | j <- ofs dep] ++
|
||||||
[unwords [prIdent i,"->",prIdent j,"[",arrowAttr "ex","]"] | j <- extendeds dep] ++
|
[unwords [showIdent i,"->",showIdent j,"[",arrowAttr "ex","]"] | j <- extendeds dep] ++
|
||||||
[unwords [prIdent i,"->",prIdent j,"[",arrowAttr "op","]"] | j <- openeds dep] ++
|
[unwords [showIdent i,"->",showIdent j,"[",arrowAttr "op","]"] | j <- openeds dep] ++
|
||||||
[unwords [prIdent i,"->",prIdent j,"[",arrowAttr "ed","]"] | j <- extrads dep]
|
[unwords [showIdent i,"->",showIdent j,"[",arrowAttr "ed","]"] | j <- extrads dep]
|
||||||
arrowAttr s = case s of
|
arrowAttr s = case s of
|
||||||
"of" -> "style = \"solid\", arrowhead = \"empty\""
|
"of" -> "style = \"solid\", arrowhead = \"empty\""
|
||||||
"ex" -> "style = \"solid\""
|
"ex" -> "style = \"solid\""
|
||||||
|
|||||||
@@ -13,7 +13,7 @@
|
|||||||
-----------------------------------------------------------------------------
|
-----------------------------------------------------------------------------
|
||||||
|
|
||||||
module GF.Infra.Ident (-- * Identifiers
|
module GF.Infra.Ident (-- * Identifiers
|
||||||
Ident(..), ident2bs, prIdent,
|
Ident(..), ident2bs, showIdent,
|
||||||
identC, identV, identA, identAV, identW,
|
identC, identV, identA, identAV, identW,
|
||||||
argIdent, varStr, varX, isWildIdent, varIndex,
|
argIdent, varStr, varX, isWildIdent, varIndex,
|
||||||
-- * refreshing identifiers
|
-- * refreshing identifiers
|
||||||
@@ -48,8 +48,8 @@ ident2bs i = case i of
|
|||||||
IAV s b j -> BS.append s (BS.pack ('_':show b ++ '_':show j))
|
IAV s b j -> BS.append s (BS.pack ('_':show b ++ '_':show j))
|
||||||
IW -> BS.pack "_"
|
IW -> BS.pack "_"
|
||||||
|
|
||||||
prIdent :: Ident -> String
|
showIdent :: Ident -> String
|
||||||
prIdent i = BS.unpack $! ident2bs i
|
showIdent i = BS.unpack $! ident2bs i
|
||||||
|
|
||||||
identC :: BS.ByteString -> Ident
|
identC :: BS.ByteString -> Ident
|
||||||
identV :: BS.ByteString -> Int -> Ident
|
identV :: BS.ByteString -> Int -> Ident
|
||||||
|
|||||||
@@ -33,7 +33,7 @@ module GF.Infra.Modules (
|
|||||||
IdentM(..),
|
IdentM(..),
|
||||||
abstractOfConcrete, abstractModOfConcrete,
|
abstractOfConcrete, abstractModOfConcrete,
|
||||||
lookupModule, lookupModuleType, lookupInfo,
|
lookupModule, lookupModuleType, lookupInfo,
|
||||||
lookupPosition, showPosition,
|
lookupPosition, showPosition, ppPosition,
|
||||||
isModAbs, isModRes, isModCnc, isModTrans,
|
isModAbs, isModRes, isModCnc, isModTrans,
|
||||||
sameMType, isCompilableModule, isCompleteModule,
|
sameMType, isCompilableModule, isCompleteModule,
|
||||||
allAbstracts, greatestAbstract, allResources,
|
allAbstracts, greatestAbstract, allResources,
|
||||||
@@ -45,7 +45,7 @@ import GF.Infra.Option
|
|||||||
import GF.Data.Operations
|
import GF.Data.Operations
|
||||||
|
|
||||||
import Data.List
|
import Data.List
|
||||||
|
import Text.PrettyPrint
|
||||||
|
|
||||||
-- AR 29/4/2003
|
-- AR 29/4/2003
|
||||||
|
|
||||||
@@ -274,6 +274,12 @@ showPosition mo i = case lookupPosition mo i of
|
|||||||
Ok (f,(b,e)) -> "in" +++ f ++ ", lines" +++ show b ++ "-" ++ show e
|
Ok (f,(b,e)) -> "in" +++ f ++ ", lines" +++ show b ++ "-" ++ show e
|
||||||
_ -> ""
|
_ -> ""
|
||||||
|
|
||||||
|
ppPosition :: (Show i, Ord i) => ModInfo i a -> i -> Doc
|
||||||
|
ppPosition mo i = case lookupPosition mo i of
|
||||||
|
Ok (f,(b,e)) | b == e -> text "in" <+> text f <> text ", line" <+> int b
|
||||||
|
| otherwise -> text "in" <+> text f <> text ", lines" <+> int b <> text "-" <> int e
|
||||||
|
_ -> empty
|
||||||
|
|
||||||
isModAbs :: ModInfo i a -> Bool
|
isModAbs :: ModInfo i a -> Bool
|
||||||
isModAbs m = case mtype m of
|
isModAbs m = case mtype m of
|
||||||
MTAbstract -> True
|
MTAbstract -> True
|
||||||
|
|||||||
@@ -205,7 +205,7 @@ buildPosTree m = buildTree . mkPoss . filter ((>0) . snd) where
|
|||||||
(i,p):rest@((_,q):_) -> (i,(name,(p,max p (q-1)))) : mkPoss rest
|
(i,p):rest@((_,q):_) -> (i,(name,(p,max p (q-1)))) : mkPoss rest
|
||||||
(i,p):[] -> (i,(name,(p,p+100))) : [] --- don't know last line
|
(i,p):[] -> (i,(name,(p,p+100))) : [] --- don't know last line
|
||||||
_ -> []
|
_ -> []
|
||||||
name = prIdent m ++ ".gf" ----
|
name = showIdent m ++ ".gf" ----
|
||||||
|
|
||||||
transAbsDef :: TopDef -> Err (Either [(Ident, Int, G.Info)] GO.Options)
|
transAbsDef :: TopDef -> Err (Either [(Ident, Int, G.Info)] GO.Options)
|
||||||
transAbsDef x = case x of
|
transAbsDef x = case x of
|
||||||
|
|||||||
@@ -226,16 +226,16 @@ string s = "'" ++ concatMap esc s ++ "'"
|
|||||||
--
|
--
|
||||||
|
|
||||||
isListCat :: (CId, [(CId, [CId])]) -> Bool
|
isListCat :: (CId, [(CId, [CId])]) -> Bool
|
||||||
isListCat (cat,rules) = "List" `isPrefixOf` prIdent cat && length rules == 2
|
isListCat (cat,rules) = "List" `isPrefixOf` showIdent cat && length rules == 2
|
||||||
&& ("Base"++c) `elem` fs && ("Cons"++c) `elem` fs
|
&& ("Base"++c) `elem` fs && ("Cons"++c) `elem` fs
|
||||||
where c = drop 4 (prIdent cat)
|
where c = drop 4 (showIdent cat)
|
||||||
fs = map (prIdent . fst) rules
|
fs = map (showIdent . fst) rules
|
||||||
|
|
||||||
isBaseFun :: CId -> Bool
|
isBaseFun :: CId -> Bool
|
||||||
isBaseFun f = "Base" `isPrefixOf` prIdent f
|
isBaseFun f = "Base" `isPrefixOf` showIdent f
|
||||||
|
|
||||||
isConsFun :: CId -> Bool
|
isConsFun :: CId -> Bool
|
||||||
isConsFun f = "Cons" `isPrefixOf` prIdent f
|
isConsFun f = "Cons" `isPrefixOf` showIdent f
|
||||||
|
|
||||||
baseSize :: (CId, [(CId, [CId])]) -> Int
|
baseSize :: (CId, [(CId, [CId])]) -> Int
|
||||||
baseSize (_,rules) = length bs
|
baseSize (_,rules) = length bs
|
||||||
|
|||||||
Reference in New Issue
Block a user