forked from GitHub/gf-core
Perhaps -> Maybe refactoring and better error message for conflicts during module update
This commit is contained in:
2
GF.cabal
2
GF.cabal
@@ -670,7 +670,6 @@ executable gf
|
|||||||
GF.Compile.CheckGrammar
|
GF.Compile.CheckGrammar
|
||||||
GF.Compile.Refresh
|
GF.Compile.Refresh
|
||||||
GF.Compile.BackOpt
|
GF.Compile.BackOpt
|
||||||
GF.Compile.Extend
|
|
||||||
GF.Compile.Rename
|
GF.Compile.Rename
|
||||||
GF.Compile.ReadFiles
|
GF.Compile.ReadFiles
|
||||||
GF.Compile.GrammarToGFCC
|
GF.Compile.GrammarToGFCC
|
||||||
@@ -679,7 +678,6 @@ executable gf
|
|||||||
GF.Compile.OptimizeGF
|
GF.Compile.OptimizeGF
|
||||||
GF.Compile.OptimizeGFCC
|
GF.Compile.OptimizeGFCC
|
||||||
GF.Compile.ModDeps
|
GF.Compile.ModDeps
|
||||||
GF.Compile.Rebuild
|
|
||||||
GF.Source.SourceToGrammar
|
GF.Source.SourceToGrammar
|
||||||
GF.Compile.GetGrammar
|
GF.Compile.GetGrammar
|
||||||
GF.Compile
|
GF.Compile
|
||||||
|
|||||||
@@ -33,7 +33,7 @@ importGrammar pgf0 opts files =
|
|||||||
res <- appIOE $ compileToPGF opts files
|
res <- appIOE $ compileToPGF opts files
|
||||||
case res of
|
case res of
|
||||||
Ok pgf2 -> do return $ unionPGF pgf0 pgf2
|
Ok pgf2 -> do return $ unionPGF pgf0 pgf2
|
||||||
Bad msg -> do putStrLn msg
|
Bad msg -> do putStrLn ('\n':'\n':msg)
|
||||||
return pgf0
|
return pgf0
|
||||||
".pgf" -> do
|
".pgf" -> do
|
||||||
pgf2 <- mapM readPGF files >>= return . foldl1 unionPGF
|
pgf2 <- mapM readPGF files >>= return . foldl1 unionPGF
|
||||||
|
|||||||
@@ -2,8 +2,6 @@ module GF.Compile (batchCompile, link, compileToPGF, compileSourceGrammar) where
|
|||||||
|
|
||||||
-- the main compiler passes
|
-- the main compiler passes
|
||||||
import GF.Compile.GetGrammar
|
import GF.Compile.GetGrammar
|
||||||
import GF.Compile.Extend
|
|
||||||
import GF.Compile.Rebuild
|
|
||||||
import GF.Compile.Rename
|
import GF.Compile.Rename
|
||||||
import GF.Compile.CheckGrammar
|
import GF.Compile.CheckGrammar
|
||||||
import GF.Compile.Optimize
|
import GF.Compile.Optimize
|
||||||
|
|||||||
@@ -36,9 +36,9 @@ shareModule :: OptSpec -> SourceModule -> SourceModule
|
|||||||
shareModule opt (i,mo) = (i,M.replaceJudgements mo (mapTree (shareInfo opt) (M.jments mo)))
|
shareModule opt (i,mo) = (i,M.replaceJudgements mo (mapTree (shareInfo opt) (M.jments mo)))
|
||||||
|
|
||||||
shareInfo :: OptSpec -> (Ident, Info) -> Info
|
shareInfo :: OptSpec -> (Ident, Info) -> Info
|
||||||
shareInfo opt (c, CncCat ty (Yes t) m) = CncCat ty (Yes (shareOptim opt c t)) m
|
shareInfo opt (c, CncCat ty (Just t) m) = CncCat ty (Just (shareOptim opt c t)) m
|
||||||
shareInfo opt (c, CncFun kxs (Yes t) m) = CncFun kxs (Yes (shareOptim opt c t)) m
|
shareInfo opt (c, CncFun kxs (Just t) m) = CncFun kxs (Just (shareOptim opt c t)) m
|
||||||
shareInfo opt (c, ResOper ty (Yes t)) = ResOper ty (Yes (shareOptim opt c t))
|
shareInfo opt (c, ResOper ty (Just t)) = ResOper ty (Just (shareOptim opt c t))
|
||||||
shareInfo _ (_,i) = i
|
shareInfo _ (_,i) = i
|
||||||
|
|
||||||
-- the function putting together optimizations
|
-- the function putting together optimizations
|
||||||
|
|||||||
@@ -121,19 +121,19 @@ checkAbsInfo ::
|
|||||||
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 (Yes cont) _ -> mkCheck "category" $
|
AbsCat (Just cont) _ -> mkCheck "category" $
|
||||||
checkContext st cont ---- also cstrs
|
checkContext st cont ---- also cstrs
|
||||||
AbsFun (Yes typ0) md -> do
|
AbsFun (Just typ0) md -> do
|
||||||
typ <- compAbsTyp [] typ0 -- to calculate let definitions
|
typ <- compAbsTyp [] typ0 -- to calculate let definitions
|
||||||
mkCheck "type of function" $ checkTyp st typ
|
mkCheck "type of function" $ checkTyp st typ
|
||||||
md' <- case md of
|
md' <- case md of
|
||||||
Yes d -> do
|
Just d -> do
|
||||||
let d' = elimTables d
|
let d' = elimTables d
|
||||||
---- mkCheckWarn "definition of function" $ checkEquation st (m,c) d'
|
---- mkCheckWarn "definition of function" $ checkEquation st (m,c) d'
|
||||||
mkCheck "definition of function" $ checkEquation st (m,c) d'
|
mkCheck "definition of function" $ checkEquation st (m,c) d'
|
||||||
return $ Yes d'
|
return $ Just d'
|
||||||
_ -> return md
|
_ -> return md
|
||||||
return $ (c,AbsFun (Yes typ) md')
|
return $ (c,AbsFun (Just typ) md')
|
||||||
_ -> return (c,info)
|
_ -> return (c,info)
|
||||||
where
|
where
|
||||||
mkCheck cat ss = case ss of
|
mkCheck cat ss = case ss of
|
||||||
@@ -195,27 +195,27 @@ checkCompleteGrammar abs cnc = do
|
|||||||
CncCat _ _ _ -> True
|
CncCat _ _ _ -> True
|
||||||
_ -> False
|
_ -> False
|
||||||
checkOne js i@(c,info) = case info of
|
checkOne js i@(c,info) = case info of
|
||||||
AbsFun (Yes _) _ -> case lookupIdent c js of
|
AbsFun (Just _) _ -> case lookupIdent c js of
|
||||||
Ok _ -> return js
|
Ok _ -> return js
|
||||||
_ -> do
|
_ -> do
|
||||||
checkWarn $ "WARNING: no linearization of" +++ prt c
|
checkWarn $ "WARNING: no linearization of" +++ prt c
|
||||||
return js
|
return js
|
||||||
AbsCat (Yes _) _ -> case lookupIdent c js of
|
AbsCat (Just _) _ -> case lookupIdent c js of
|
||||||
Ok (AnyInd _ _) -> return js
|
Ok (AnyInd _ _) -> return js
|
||||||
Ok (CncCat (Yes _) _ _) -> return js
|
Ok (CncCat (Just _) _ _) -> return js
|
||||||
Ok (CncCat _ mt mp) -> do
|
Ok (CncCat _ mt mp) -> do
|
||||||
checkWarn $
|
checkWarn $
|
||||||
"Warning: no linearization type for" +++ prt c ++
|
"Warning: no linearization type for" +++ prt c ++
|
||||||
", inserting default {s : Str}"
|
", inserting default {s : Str}"
|
||||||
return $ updateTree (c,CncCat (Yes defLinType) mt mp) js
|
return $ updateTree (c,CncCat (Just defLinType) mt mp) js
|
||||||
_ -> do
|
_ -> do
|
||||||
checkWarn $
|
checkWarn $
|
||||||
"Warning: no linearization type for" +++ prt c ++
|
"Warning: no linearization type for" +++ prt c ++
|
||||||
", inserting default {s : Str}"
|
", inserting default {s : Str}"
|
||||||
return $ updateTree (c,CncCat (Yes defLinType) nope nope) js
|
return $ updateTree (c,CncCat (Just defLinType) Nothing Nothing) js
|
||||||
_ -> return js
|
_ -> return js
|
||||||
|
|
||||||
-- | General Principle: only Yes-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 (Ident,Info)
|
||||||
checkResInfo gr mo mm (c,info) = do
|
checkResInfo gr mo mm (c,info) = do
|
||||||
@@ -223,17 +223,15 @@ checkResInfo gr mo mm (c,info) = do
|
|||||||
case info of
|
case info of
|
||||||
ResOper pty pde -> chIn "operation" $ do
|
ResOper pty pde -> chIn "operation" $ do
|
||||||
(pty', pde') <- case (pty,pde) of
|
(pty', pde') <- case (pty,pde) of
|
||||||
(Yes ty, Yes de) -> do
|
(Just ty, Just de) -> do
|
||||||
ty' <- check ty typeType >>= comp . fst
|
ty' <- check ty typeType >>= comp . fst
|
||||||
(de',_) <- check de ty'
|
(de',_) <- check de ty'
|
||||||
return (Yes ty', Yes de')
|
return (Just ty', Just de')
|
||||||
(_, Yes de) -> do
|
(_ , Just de) -> do
|
||||||
(de',ty') <- infer de
|
(de',ty') <- infer de
|
||||||
return (Yes ty', Yes de')
|
return (Just ty', Just de')
|
||||||
(_,Nope) -> do
|
(_ , Nothing) -> do
|
||||||
raise "No definition given to oper"
|
raise "No definition given to oper"
|
||||||
--return (pty,pde)
|
|
||||||
_ -> return (pty, pde) --- other cases are uninteresting
|
|
||||||
return (c, ResOper pty' pde')
|
return (c, ResOper pty' pde')
|
||||||
|
|
||||||
ResOverload os tysts -> chIn "overloading" $ do
|
ResOverload os tysts -> chIn "overloading" $ do
|
||||||
@@ -248,11 +246,11 @@ checkResInfo gr mo mm (c,info) = do
|
|||||||
sort [t : map snd xs | (x,_) <- tysts2, Ok (xs,t) <- [typeFormCnc x]]
|
sort [t : map snd xs | (x,_) <- tysts2, Ok (xs,t) <- [typeFormCnc x]]
|
||||||
return (c,ResOverload os [(y,x) | (x,y) <- tysts'])
|
return (c,ResOverload os [(y,x) | (x,y) <- tysts'])
|
||||||
|
|
||||||
ResParam (Yes (pcs,_)) -> chIn "parameter type" $ do
|
ResParam (Just (pcs,_)) -> chIn "parameter type" $ do
|
||||||
---- mapM ((mapM (computeLType gr . snd)) . snd) pcs
|
---- mapM ((mapM (computeLType gr . snd)) . snd) pcs
|
||||||
mapM_ ((mapM_ (checkIfParType 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 (Yes (pcs, Just ts)))
|
return (c,ResParam (Just (pcs, Just ts)))
|
||||||
|
|
||||||
_ -> return (c,info)
|
_ -> return (c,info)
|
||||||
where
|
where
|
||||||
@@ -277,26 +275,26 @@ checkCncInfo gr m mo (a,abs) (c,info) = do
|
|||||||
checkReservedId c
|
checkReservedId c
|
||||||
case info of
|
case info of
|
||||||
|
|
||||||
CncFun _ (Yes trm) mpr -> chIn "linearization of" $ do
|
CncFun _ (Just trm) mpr -> chIn "linearization of" $ do
|
||||||
typ <- checkErr $ lookupFunType gr a c
|
typ <- checkErr $ lookupFunType gr a c
|
||||||
cat0 <- checkErr $ valCat typ
|
cat0 <- checkErr $ 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 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))) (Yes trm') mpr)
|
return (c, CncFun (Just (cat,(cont,val))) (Just trm') mpr)
|
||||||
-- cat for cf, typ for pe
|
-- cat for cf, typ for pe
|
||||||
|
|
||||||
CncCat (Yes 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' <- checkIfLinType gr typ
|
||||||
mdef' <- case mdef of
|
mdef' <- case mdef of
|
||||||
Yes def -> do
|
Just def -> do
|
||||||
(def',_) <- checkLType gr def (mkFunType [typeStr] typ)
|
(def',_) <- checkLType gr def (mkFunType [typeStr] typ)
|
||||||
return $ Yes def'
|
return $ Just def'
|
||||||
_ -> return mdef
|
_ -> return mdef
|
||||||
checkPrintname gr mpr
|
checkPrintname gr mpr
|
||||||
return (c,CncCat (Yes typ') mdef' mpr)
|
return (c,CncCat (Just typ') mdef' mpr)
|
||||||
|
|
||||||
_ -> checkResInfo gr m mo (c,info)
|
_ -> checkResInfo gr m mo (c,info)
|
||||||
|
|
||||||
@@ -400,9 +398,9 @@ computeLType gr t = do
|
|||||||
|
|
||||||
_ -> composOp comp ty
|
_ -> composOp comp ty
|
||||||
|
|
||||||
checkPrintname :: SourceGrammar -> Perh Term -> Check ()
|
checkPrintname :: SourceGrammar -> Maybe Term -> Check ()
|
||||||
checkPrintname st (Yes 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!!
|
||||||
checkReservedId :: Ident -> Check ()
|
checkReservedId :: Ident -> Check ()
|
||||||
@@ -1105,15 +1103,15 @@ allDependencies ism b =
|
|||||||
Q n c | ism n -> [c]
|
Q n c | ism n -> [c]
|
||||||
QC n c | ism n -> [c]
|
QC n c | ism n -> [c]
|
||||||
_ -> collectOp opersIn t
|
_ -> collectOp opersIn t
|
||||||
opty (Yes ty) = opersIn ty
|
opty (Just ty) = opersIn ty
|
||||||
opty _ = []
|
opty _ = []
|
||||||
pts i = case i of
|
pts i = case i of
|
||||||
ResOper pty pt -> [pty,pt]
|
ResOper pty pt -> [pty,pt]
|
||||||
ResParam (Yes (ps,_)) -> [Yes t | (_,cont) <- ps, (_,t) <- cont]
|
ResParam (Just (ps,_)) -> [Just t | (_,cont) <- ps, (_,t) <- cont]
|
||||||
CncCat pty _ _ -> [pty]
|
CncCat pty _ _ -> [pty]
|
||||||
CncFun _ pt _ -> [pt] ---- (Maybe (Ident,(Context,Type))
|
CncFun _ pt _ -> [pt] ---- (Maybe (Ident,(Context,Type))
|
||||||
AbsFun pty ptr -> [pty] --- ptr is def, which can be mutual
|
AbsFun pty ptr -> [pty] --- ptr is def, which can be mutual
|
||||||
AbsCat (Yes co) _ -> [Yes ty | (_,ty) <- co]
|
AbsCat (Just co) _ -> [Just ty | (_,ty) <- co]
|
||||||
_ -> []
|
_ -> []
|
||||||
|
|
||||||
topoSortOpers :: [(Ident,[Ident])] -> Err [Ident]
|
topoSortOpers :: [(Ident,[Ident])] -> Err [Ident]
|
||||||
|
|||||||
@@ -24,10 +24,10 @@ codeSourceModule :: (String -> String) -> SourceModule -> SourceModule
|
|||||||
codeSourceModule co (id,mo) = (id,replaceJudgements mo (mapTree codj (jments mo)))
|
codeSourceModule co (id,mo) = (id,replaceJudgements mo (mapTree codj (jments mo)))
|
||||||
where
|
where
|
||||||
codj (c,info) = case info of
|
codj (c,info) = case info of
|
||||||
ResOper pty pt -> ResOper (mapP codt pty) (mapP codt pt)
|
ResOper pty pt -> ResOper (fmap codt pty) (fmap codt pt)
|
||||||
ResOverload es tyts -> ResOverload es [(codt ty,codt t) | (ty,t) <- tyts]
|
ResOverload es tyts -> ResOverload es [(codt ty,codt t) | (ty,t) <- tyts]
|
||||||
CncCat pty pt mpr -> CncCat pty (mapP codt pt) (mapP codt mpr)
|
CncCat pty pt mpr -> CncCat pty (fmap codt pt) (fmap codt mpr)
|
||||||
CncFun mty pt mpr -> CncFun mty (mapP codt pt) (mapP codt mpr)
|
CncFun mty pt mpr -> CncFun mty (fmap codt pt) (fmap codt mpr)
|
||||||
_ -> info
|
_ -> info
|
||||||
codt t = case t of
|
codt t = case t of
|
||||||
K s -> K (co s)
|
K s -> K (co s)
|
||||||
|
|||||||
@@ -1,140 +0,0 @@
|
|||||||
----------------------------------------------------------------------
|
|
||||||
-- |
|
|
||||||
-- Module : Extend
|
|
||||||
-- Maintainer : AR
|
|
||||||
-- Stability : (stable)
|
|
||||||
-- Portability : (portable)
|
|
||||||
--
|
|
||||||
-- > CVS $Date: 2005/05/30 21:08:14 $
|
|
||||||
-- > CVS $Author: aarne $
|
|
||||||
-- > CVS $Revision: 1.18 $
|
|
||||||
--
|
|
||||||
-- AR 14\/5\/2003 -- 11\/11
|
|
||||||
--
|
|
||||||
-- The top-level function 'extendModule'
|
|
||||||
-- extends a module symbol table by indirections to the module it extends
|
|
||||||
-----------------------------------------------------------------------------
|
|
||||||
|
|
||||||
module GF.Compile.Extend (extendModule, extendMod
|
|
||||||
) where
|
|
||||||
|
|
||||||
import GF.Grammar.Grammar
|
|
||||||
import GF.Infra.Ident
|
|
||||||
import GF.Grammar.PrGrammar
|
|
||||||
import GF.Infra.Modules
|
|
||||||
import GF.Compile.Update
|
|
||||||
import GF.Grammar.Macros
|
|
||||||
import GF.Data.Operations
|
|
||||||
|
|
||||||
import Control.Monad
|
|
||||||
import Data.List(nub)
|
|
||||||
|
|
||||||
extendModule :: [SourceModule] -> SourceModule -> Err SourceModule
|
|
||||||
extendModule ms (name,m)
|
|
||||||
---- Just to allow inheritance in incomplete concrete (which are not
|
|
||||||
---- compiled anyway), extensions are not built for them.
|
|
||||||
---- Should be replaced by real control. AR 4/2/2005
|
|
||||||
| mstatus m == MSIncomplete && isModCnc m = return (name,m)
|
|
||||||
| otherwise = do m' <- foldM extOne m (extend m)
|
|
||||||
return (name,m')
|
|
||||||
where
|
|
||||||
extOne mo (n,cond) = do
|
|
||||||
m0 <- lookupModule (MGrammar ms) n
|
|
||||||
|
|
||||||
-- test that the module types match, and find out if the old is complete
|
|
||||||
testErr (sameMType (mtype m) (mtype mo))
|
|
||||||
("illegal extension type to module" +++ prt name)
|
|
||||||
|
|
||||||
let isCompl = isCompleteModule m0
|
|
||||||
|
|
||||||
-- build extension in a way depending on whether the old module is complete
|
|
||||||
js1 <- extendMod isCompl (n, isInherited cond) name (jments m0) (jments mo)
|
|
||||||
|
|
||||||
-- if incomplete, throw away extension information
|
|
||||||
return $
|
|
||||||
if isCompl
|
|
||||||
then mo {jments = js1}
|
|
||||||
else mo {extend = filter ((/=n) . fst) (extend mo)
|
|
||||||
,mexdeps= nub (n : mexdeps mo)
|
|
||||||
,jments = js1
|
|
||||||
}
|
|
||||||
|
|
||||||
-- | When extending a complete module: new information is inserted,
|
|
||||||
-- and the process is interrupted if unification fails.
|
|
||||||
-- If the extended module is incomplete, its judgements are just copied.
|
|
||||||
extendMod :: Bool -> (Ident,Ident -> Bool) -> Ident ->
|
|
||||||
BinTree Ident Info -> BinTree Ident Info ->
|
|
||||||
Err (BinTree Ident Info)
|
|
||||||
extendMod isCompl (name,cond) base old new = foldM try new $ tree2list old where
|
|
||||||
try t i@(c,_) | not (cond c) = return t
|
|
||||||
try t i@(c,_) = errIn ("constant" +++ prt c) $
|
|
||||||
tryInsert (extendAnyInfo isCompl name base) indirIf t i
|
|
||||||
indirIf = if isCompl then indirInfo name else id
|
|
||||||
|
|
||||||
indirInfo :: Ident -> Info -> Info
|
|
||||||
indirInfo n info = AnyInd b n' where
|
|
||||||
(b,n') = case info of
|
|
||||||
ResValue _ -> (True,n)
|
|
||||||
ResParam _ -> (True,n)
|
|
||||||
AbsFun _ (Yes EData) -> (True,n)
|
|
||||||
AnyInd b k -> (b,k)
|
|
||||||
_ -> (False,n) ---- canonical in Abs
|
|
||||||
|
|
||||||
perhIndir :: Ident -> Perh a -> Perh a
|
|
||||||
perhIndir n p = case p of
|
|
||||||
Yes _ -> May n
|
|
||||||
_ -> p
|
|
||||||
|
|
||||||
extendAnyInfo :: Bool -> Ident -> Ident -> Info -> Info -> Err Info
|
|
||||||
extendAnyInfo isc n o i j =
|
|
||||||
errIn ("building extension for" +++ prt n +++ "in" +++ prt o) $ case (i,j) of
|
|
||||||
(AbsCat mc1 mf1, AbsCat mc2 mf2) ->
|
|
||||||
liftM2 AbsCat (updn isc n mc1 mc2) (updn isc n mf1 mf2) --- add cstrs
|
|
||||||
(AbsFun mt1 md1, AbsFun mt2 md2) ->
|
|
||||||
liftM2 AbsFun (updn isc n mt1 mt2) (updn isc n md1 md2) --- add defs
|
|
||||||
(ResParam mt1, ResParam mt2) ->
|
|
||||||
liftM ResParam $ updn isc n mt1 mt2
|
|
||||||
(ResValue mt1, ResValue mt2) ->
|
|
||||||
liftM ResValue $ updn isc n mt1 mt2
|
|
||||||
(_, ResOverload ms t) | elem n ms ->
|
|
||||||
return $ ResOverload ms t
|
|
||||||
(ResOper mt1 m1, ResOper mt2 m2) -> ---- extendResOper n mt1 m1 mt2 m2
|
|
||||||
liftM2 ResOper (updn isc n mt1 mt2) (updn isc n m1 m2)
|
|
||||||
(CncCat mc1 mf1 mp1, CncCat mc2 mf2 mp2) ->
|
|
||||||
liftM3 CncCat (updn isc n mc1 mc2) (updn isc n mf1 mf2) (updn isc n mp1 mp2)
|
|
||||||
(CncFun m mt1 md1, CncFun _ mt2 md2) ->
|
|
||||||
liftM2 (CncFun m) (updn isc n mt1 mt2) (updn isc n md1 md2)
|
|
||||||
|
|
||||||
---- (AnyInd _ _, ResOper _ _) -> return j ----
|
|
||||||
|
|
||||||
(AnyInd b1 m1, AnyInd b2 m2) -> do
|
|
||||||
testErr (b1 == b2) "inconsistent indirection status"
|
|
||||||
---- commented out as work-around for a spurious problem in
|
|
||||||
---- TestResourceFre; should look at building of completion. 17/11/2004
|
|
||||||
testErr (m1 == m2) $
|
|
||||||
"different sources of indirection: " +++ show m1 +++ show m2
|
|
||||||
return i
|
|
||||||
|
|
||||||
_ -> Bad $ "cannot unify information in" ++++ show i ++++ "and" ++++ show j
|
|
||||||
|
|
||||||
--- where
|
|
||||||
|
|
||||||
updn isc n = if isc then (updatePerhaps n) else (updatePerhapsHard n)
|
|
||||||
updc isc n = if True then (updatePerhaps n) else (updatePerhapsHard n)
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
{- ---- no more needed: this is done in Rebuild
|
|
||||||
-- opers declared in an interface and defined in an instance are a special case
|
|
||||||
|
|
||||||
extendResOper n mt1 m1 mt2 m2 = case (m1,m2) of
|
|
||||||
(Nope,_) -> return $ ResOper (strip mt1) m2
|
|
||||||
_ -> liftM2 ResOper (updatePerhaps n mt1 mt2) (updatePerhaps n m1 m2)
|
|
||||||
where
|
|
||||||
strip (Yes t) = Yes $ strp t
|
|
||||||
strip m = m
|
|
||||||
strp t = case t of
|
|
||||||
Q _ c -> Vr c
|
|
||||||
QC _ c -> Vr c
|
|
||||||
_ -> composSafeOp strp t
|
|
||||||
-}
|
|
||||||
@@ -69,15 +69,15 @@ canon2gfcc opts pars cgr@(M.MGrammar ((a,abm):cms)) =
|
|||||||
gflags = Map.empty
|
gflags = Map.empty
|
||||||
aflags = Map.fromList [(mkCId f,x) | (f,x) <- optionsPGF (M.flags abm)]
|
aflags = Map.fromList [(mkCId f,x) | (f,x) <- optionsPGF (M.flags abm)]
|
||||||
mkDef pty = case pty of
|
mkDef pty = case pty of
|
||||||
Yes t -> mkExp t
|
Just t -> mkExp t
|
||||||
_ -> CM.primNotion
|
_ -> CM.primNotion
|
||||||
|
|
||||||
-- concretes
|
-- concretes
|
||||||
lfuns = [(f', (mkType ty, mkDef pty)) |
|
lfuns = [(f', (mkType ty, mkDef pty)) |
|
||||||
(f,AbsFun (Yes ty) pty) <- tree2list (M.jments abm), let f' = i2i f]
|
(f,AbsFun (Just ty) pty) <- tree2list (M.jments abm), let f' = i2i f]
|
||||||
funs = Map.fromAscList lfuns
|
funs = Map.fromAscList lfuns
|
||||||
lcats = [(i2i c, mkContext cont) |
|
lcats = [(i2i c, mkContext cont) |
|
||||||
(c,AbsCat (Yes cont) _) <- tree2list (M.jments abm)]
|
(c,AbsCat (Just cont) _) <- tree2list (M.jments abm)]
|
||||||
cats = Map.fromAscList lcats
|
cats = Map.fromAscList lcats
|
||||||
catfuns = Map.fromList
|
catfuns = Map.fromList
|
||||||
[(cat,[f | (f, (C.DTyp _ c _,_)) <- lfuns, c==cat]) | (cat,_) <- lcats]
|
[(cat,[f | (f, (C.DTyp _ c _,_)) <- lfuns, c==cat]) | (cat,_) <- lcats]
|
||||||
@@ -95,18 +95,18 @@ canon2gfcc opts pars cgr@(M.MGrammar ((a,abm):cms)) =
|
|||||||
---- then (trace "decode" D.convertStringsInTerm decodeUTF8) else id
|
---- then (trace "decode" D.convertStringsInTerm decodeUTF8) else id
|
||||||
umkTerm = utf . mkTerm
|
umkTerm = utf . mkTerm
|
||||||
lins = Map.fromAscList
|
lins = Map.fromAscList
|
||||||
[(f', umkTerm tr) | (f,CncFun _ (Yes tr) _) <- js,
|
[(f', umkTerm tr) | (f,CncFun _ (Just tr) _) <- js,
|
||||||
let f' = i2i f, exists f'] -- eliminating lins without fun
|
let f' = i2i f, exists f'] -- eliminating lins without fun
|
||||||
-- needed even here because of restricted inheritance
|
-- needed even here because of restricted inheritance
|
||||||
lincats = Map.fromAscList
|
lincats = Map.fromAscList
|
||||||
[(i2i c, mkCType ty) | (c,CncCat (Yes ty) _ _) <- js]
|
[(i2i c, mkCType ty) | (c,CncCat (Just ty) _ _) <- js]
|
||||||
lindefs = Map.fromAscList
|
lindefs = Map.fromAscList
|
||||||
[(i2i c, umkTerm tr) | (c,CncCat _ (Yes tr) _) <- js]
|
[(i2i c, umkTerm tr) | (c,CncCat _ (Just tr) _) <- js]
|
||||||
printnames = Map.union
|
printnames = Map.union
|
||||||
(Map.fromAscList [(i2i f, umkTerm tr) | (f,CncFun _ _ (Yes tr)) <- js])
|
(Map.fromAscList [(i2i f, umkTerm tr) | (f,CncFun _ _ (Just tr)) <- js])
|
||||||
(Map.fromAscList [(i2i f, umkTerm tr) | (f,CncCat _ _ (Yes tr)) <- js])
|
(Map.fromAscList [(i2i f, umkTerm tr) | (f,CncCat _ _ (Just tr)) <- js])
|
||||||
params = Map.fromAscList
|
params = Map.fromAscList
|
||||||
[(i2i c, pars lang0 c) | (c,CncCat (Yes ty) _ _) <- js]
|
[(i2i c, pars lang0 c) | (c,CncCat (Just ty) _ _) <- js]
|
||||||
fcfg = Nothing
|
fcfg = Nothing
|
||||||
|
|
||||||
exists f = Map.member f funs
|
exists f = Map.member f funs
|
||||||
@@ -232,7 +232,7 @@ reorder abs cg = M.MGrammar $
|
|||||||
adefs = sorted2tree $ sortIds $
|
adefs = sorted2tree $ sortIds $
|
||||||
predefADefs ++ Look.allOrigInfos cg abs
|
predefADefs ++ Look.allOrigInfos cg abs
|
||||||
predefADefs =
|
predefADefs =
|
||||||
[(c, AbsCat (Yes []) Nope) | c <- [cFloat,cInt,cString]]
|
[(c, AbsCat (Just []) Nothing) | c <- [cFloat,cInt,cString]]
|
||||||
aflags =
|
aflags =
|
||||||
concatOptions [M.flags mo | (_,mo) <- M.modules cg, M.isModAbs mo]
|
concatOptions [M.flags mo | (_,mo) <- M.modules cg, M.isModAbs mo]
|
||||||
|
|
||||||
@@ -246,7 +246,7 @@ reorder abs cg = M.MGrammar $
|
|||||||
Just r <- [lookup i (M.allExtendSpecs cg la)]]
|
Just r <- [lookup i (M.allExtendSpecs cg la)]]
|
||||||
|
|
||||||
predefCDefs =
|
predefCDefs =
|
||||||
[(c, CncCat (Yes GM.defLinType) Nope Nope) | c <- [cInt,cFloat,cString]]
|
[(c, CncCat (Just GM.defLinType) Nothing Nothing) | c <- [cInt,cFloat,cString]]
|
||||||
|
|
||||||
sortIds = sortBy (\ (f,_) (g,_) -> compare f g)
|
sortIds = sortBy (\ (f,_) (g,_) -> compare f g)
|
||||||
|
|
||||||
@@ -279,8 +279,8 @@ canon2canon opts abs cg0 =
|
|||||||
j2j cg (f,j) =
|
j2j cg (f,j) =
|
||||||
let debug = if verbAtLeast opts Verbose then trace ("+ " ++ prt f) else id in
|
let debug = if verbAtLeast opts Verbose then trace ("+ " ++ prt f) else id in
|
||||||
case j of
|
case j of
|
||||||
CncFun x (Yes tr) z -> CncFun x (Yes (debug (t2t tr))) z
|
CncFun x (Just tr) z -> CncFun x (Just (debug (t2t tr))) z
|
||||||
CncCat (Yes ty) (Yes x) y -> CncCat (Yes (ty2ty ty)) (Yes (t2t x)) y
|
CncCat (Just ty) (Just x) y -> CncCat (Just (ty2ty ty)) (Just (t2t x)) y
|
||||||
_ -> j
|
_ -> j
|
||||||
where
|
where
|
||||||
cg1 = cg
|
cg1 = cg
|
||||||
@@ -290,8 +290,8 @@ canon2canon opts abs cg0 =
|
|||||||
|
|
||||||
-- flatten record arguments of param constructors
|
-- flatten record arguments of param constructors
|
||||||
p2p (f,j) = case j of
|
p2p (f,j) = case j of
|
||||||
ResParam (Yes (ps,v)) ->
|
ResParam (Just (ps,v)) ->
|
||||||
ResParam (Yes ([(c,concatMap unRec cont) | (c,cont) <- ps],Nothing))
|
ResParam (Just ([(c,concatMap unRec cont) | (c,cont) <- ps],Nothing))
|
||||||
_ -> j
|
_ -> j
|
||||||
unRec (x,ty) = case ty of
|
unRec (x,ty) = case ty of
|
||||||
RecType fs -> [ity | (_,typ) <- fs, ity <- unRec (identW,typ)]
|
RecType fs -> [ity | (_,typ) <- fs, ity <- unRec (identW,typ)]
|
||||||
@@ -333,13 +333,13 @@ paramValues cgr = (labels,untyps,typs) where
|
|||||||
partyps = nub $
|
partyps = nub $
|
||||||
--- [App (Q (IC "Predef") (IC "Ints")) (EInt i) | i <- [1,9]] ---linTypeInt
|
--- [App (Q (IC "Predef") (IC "Ints")) (EInt i) | i <- [1,9]] ---linTypeInt
|
||||||
[ty |
|
[ty |
|
||||||
(_,(_,CncCat (Yes ty0) _ _)) <- jments,
|
(_,(_,CncCat (Just ty0) _ _)) <- jments,
|
||||||
ty <- typsFrom ty0
|
ty <- typsFrom ty0
|
||||||
] ++ [
|
] ++ [
|
||||||
Q m ty |
|
Q m ty |
|
||||||
(m,(ty,ResParam _)) <- jments
|
(m,(ty,ResParam _)) <- jments
|
||||||
] ++ [ty |
|
] ++ [ty |
|
||||||
(_,(_,CncFun _ (Yes tr) _)) <- jments,
|
(_,(_,CncFun _ (Just tr) _)) <- jments,
|
||||||
ty <- err (const []) snd $ appSTM (typsFromTrm tr) []
|
ty <- err (const []) snd $ appSTM (typsFromTrm tr) []
|
||||||
]
|
]
|
||||||
params = [(ty, errVal (traceD ("UNKNOWN PARAM TYPE" +++ show ty) []) $
|
params = [(ty, errVal (traceD ("UNKNOWN PARAM TYPE" +++ show ty) []) $
|
||||||
@@ -381,7 +381,7 @@ paramValues cgr = (labels,untyps,typs) where
|
|||||||
[(cat,[f | let RecType fs = GM.defLinType, f <- fs]) | cat <- [cInt,cFloat, cString]] ++
|
[(cat,[f | let RecType fs = GM.defLinType, f <- fs]) | cat <- [cInt,cFloat, cString]] ++
|
||||||
reverse ---- TODO: really those lincats that are reached
|
reverse ---- TODO: really those lincats that are reached
|
||||||
---- reverse is enough to expel overshadowed ones...
|
---- reverse is enough to expel overshadowed ones...
|
||||||
[(cat,ls) | (_,(cat,CncCat (Yes ty) _ _)) <- jments,
|
[(cat,ls) | (_,(cat,CncCat (Just ty) _ _)) <- jments,
|
||||||
RecType ls <- [unlockTy ty]]
|
RecType ls <- [unlockTy ty]]
|
||||||
labels = Map.fromList $ concat
|
labels = Map.fromList $ concat
|
||||||
[((cat,[lab]),(typ,i)):
|
[((cat,[lab]),(typ,i)):
|
||||||
|
|||||||
@@ -85,6 +85,13 @@ evalModule oopts (ms,eenv) mo@(name,m0)
|
|||||||
info' <- evalResInfo oopts gr (i,info)
|
info' <- evalResInfo oopts gr (i,info)
|
||||||
return $ updateRes g name i info'
|
return $ updateRes g name i info'
|
||||||
|
|
||||||
|
-- | update a resource module by adding a new or changing an old definition
|
||||||
|
updateRes :: SourceGrammar -> Ident -> Ident -> Info -> SourceGrammar
|
||||||
|
updateRes gr@(MGrammar ms) m i info = MGrammar $ map upd ms where
|
||||||
|
upd (n,mo)
|
||||||
|
| n /= m = (n,mo)
|
||||||
|
| n == m = (n,updateModule mo i info)
|
||||||
|
|
||||||
-- | only operations need be compiled in a resource, and this is local to each
|
-- | only operations need be compiled in a resource, and this is local to each
|
||||||
-- definition since the module is traversed in topological order
|
-- definition since the module is traversed in topological order
|
||||||
evalResInfo :: Options -> SourceGrammar -> (Ident,Info) -> Err Info
|
evalResInfo :: Options -> SourceGrammar -> (Ident,Info) -> Err Info
|
||||||
@@ -92,8 +99,8 @@ evalResInfo oopts gr (c,info) = case info of
|
|||||||
|
|
||||||
ResOper pty pde -> eIn "operation" $ do
|
ResOper pty pde -> eIn "operation" $ do
|
||||||
pde' <- case pde of
|
pde' <- case pde of
|
||||||
Yes de | optres -> liftM yes $ comp de
|
Just de | optres -> liftM Just $ comp de
|
||||||
_ -> return pde
|
_ -> return pde
|
||||||
return $ ResOper pty pde'
|
return $ ResOper pty pde'
|
||||||
|
|
||||||
_ -> return info
|
_ -> return info
|
||||||
@@ -114,26 +121,22 @@ evalCncInfo opts gr cnc abs (c,info) = do
|
|||||||
|
|
||||||
CncCat ptyp pde ppr -> do
|
CncCat ptyp pde ppr -> do
|
||||||
pde' <- case (ptyp,pde) of
|
pde' <- case (ptyp,pde) of
|
||||||
(Yes typ, Yes de) ->
|
(Just typ, Just de) ->
|
||||||
liftM yes $ pEval ([(varStr, typeStr)], typ) de
|
liftM Just $ pEval ([(varStr, typeStr)], typ) de
|
||||||
(Yes typ, Nope) ->
|
(Just typ, Nothing) ->
|
||||||
liftM yes $ mkLinDefault gr typ >>= partEval noOptions gr ([(varStr, typeStr)],typ)
|
liftM Just $ mkLinDefault gr typ >>= partEval noOptions gr ([(varStr, typeStr)],typ)
|
||||||
(May b, Nope) ->
|
|
||||||
return $ May b
|
|
||||||
_ -> return pde -- indirection
|
_ -> return pde -- indirection
|
||||||
|
|
||||||
ppr' <- liftM yes $ evalPrintname gr c ppr (yes $ K $ prt c)
|
ppr' <- liftM Just $ evalPrintname gr c ppr (Just $ K $ prt c)
|
||||||
|
|
||||||
return (CncCat ptyp pde' ppr')
|
return (CncCat ptyp pde' ppr')
|
||||||
|
|
||||||
CncFun (mt@(Just (_,ty@(cont,val)))) pde ppr -> --trace (prt c) $
|
CncFun (mt@(Just (_,ty@(cont,val)))) pde ppr -> --trace (prt c) $
|
||||||
eIn ("linearization in type" +++ prt (mkProd (cont,val,[])) ++++ "of function") $ do
|
eIn ("linearization in type" +++ prt (mkProd (cont,val,[])) ++++ "of function") $ do
|
||||||
pde' <- case pde of
|
pde' <- case pde of
|
||||||
Yes de -> do
|
Just de -> liftM Just $ pEval ty de
|
||||||
liftM yes $ pEval ty de
|
Nothing -> return pde
|
||||||
|
ppr' <- liftM Just $ evalPrintname gr c ppr pde'
|
||||||
_ -> return pde
|
|
||||||
ppr' <- liftM yes $ evalPrintname gr c ppr pde'
|
|
||||||
return $ CncFun mt pde' ppr' -- only cat in type actually needed
|
return $ CncFun mt pde' ppr' -- only cat in type actually needed
|
||||||
|
|
||||||
_ -> return info
|
_ -> return info
|
||||||
@@ -202,13 +205,13 @@ mkLinDefault gr typ = do
|
|||||||
-- lin for functions, cat name for cats (dispatch made in evalCncDef above).
|
-- lin for functions, cat name for cats (dispatch made in evalCncDef above).
|
||||||
--- We cannot use linearization at this stage, since we do not know the
|
--- We cannot use linearization at this stage, since we do not know the
|
||||||
--- defaults we would need for question marks - and we're not yet in canon.
|
--- defaults we would need for question marks - and we're not yet in canon.
|
||||||
evalPrintname :: SourceGrammar -> Ident -> MPr -> Perh Term -> Err Term
|
evalPrintname :: SourceGrammar -> Ident -> Maybe Term -> Maybe Term -> Err Term
|
||||||
evalPrintname gr c ppr lin =
|
evalPrintname gr c ppr lin =
|
||||||
case ppr of
|
case ppr of
|
||||||
Yes pr -> comp pr
|
Just pr -> comp pr
|
||||||
_ -> case lin of
|
Nothing -> case lin of
|
||||||
Yes t -> return $ K $ clean $ prt $ oneBranch t ---- stringFromTerm
|
Just t -> return $ K $ clean $ prt $ oneBranch t ---- stringFromTerm
|
||||||
_ -> return $ K $ prt c ----
|
Nothing -> return $ K $ prt c ----
|
||||||
where
|
where
|
||||||
comp = computeConcrete gr
|
comp = computeConcrete gr
|
||||||
|
|
||||||
|
|||||||
@@ -48,9 +48,9 @@ processModule :: (Ident -> Term -> Term) -> SourceModule -> SourceModule
|
|||||||
processModule opt (i,mo) = (i,M.replaceJudgements mo (mapTree (shareInfo opt) (M.jments mo)))
|
processModule opt (i,mo) = (i,M.replaceJudgements mo (mapTree (shareInfo opt) (M.jments mo)))
|
||||||
|
|
||||||
shareInfo :: (Ident -> Term -> Term) -> (Ident,Info) -> Info
|
shareInfo :: (Ident -> Term -> Term) -> (Ident,Info) -> Info
|
||||||
shareInfo opt (c, CncCat ty (Yes t) m) = CncCat ty (Yes (opt c t)) m
|
shareInfo opt (c, CncCat ty (Just t) m) = CncCat ty (Just (opt c t)) m
|
||||||
shareInfo opt (c, CncFun kxs (Yes t) m) = CncFun kxs (Yes (opt c t)) m
|
shareInfo opt (c, CncFun kxs (Just t) m) = CncFun kxs (Just (opt c t)) m
|
||||||
shareInfo opt (c, ResOper ty (Yes t)) = ResOper ty (Yes (opt c t))
|
shareInfo opt (c, ResOper ty (Just t)) = ResOper ty (Just (opt c t))
|
||||||
shareInfo _ (_,i) = i
|
shareInfo _ (_,i) = i
|
||||||
|
|
||||||
-- the function putting together optimizations
|
-- the function putting together optimizations
|
||||||
@@ -181,9 +181,9 @@ unsubexpModule sm@(i,mo)
|
|||||||
-- perform this iff the module has opers
|
-- perform this iff the module has opers
|
||||||
hasSub ljs = not $ null [c | (c,ResOper _ _) <- ljs]
|
hasSub ljs = not $ null [c | (c,ResOper _ _) <- ljs]
|
||||||
unparInfo (c,info) = case info of
|
unparInfo (c,info) = case info of
|
||||||
CncFun xs (Yes t) m -> [(c, CncFun xs (Yes (unparTerm t)) m)]
|
CncFun xs (Just t) m -> [(c, CncFun xs (Just (unparTerm t)) m)]
|
||||||
ResOper (Yes (EInt 8)) _ -> [] -- subexp-generated opers
|
ResOper (Just (EInt 8)) _ -> [] -- subexp-generated opers
|
||||||
ResOper pty (Yes t) -> [(c, ResOper pty (Yes (unparTerm t)))]
|
ResOper pty (Just t) -> [(c, ResOper pty (Just (unparTerm t)))]
|
||||||
_ -> [(c,info)]
|
_ -> [(c,info)]
|
||||||
unparTerm t = case t of
|
unparTerm t = case t of
|
||||||
Q m c | isOperIdent c -> --- name convention of subexp opers
|
Q m c | isOperIdent c -> --- name convention of subexp opers
|
||||||
@@ -205,12 +205,12 @@ addSubexpConsts mo tree lins = do
|
|||||||
where
|
where
|
||||||
|
|
||||||
mkOne (f,def) = case def of
|
mkOne (f,def) = case def of
|
||||||
CncFun xs (Yes trm) pn -> do
|
CncFun xs (Just trm) pn -> do
|
||||||
trm' <- recomp f trm
|
trm' <- recomp f trm
|
||||||
return (f,CncFun xs (Yes trm') pn)
|
return (f,CncFun xs (Just trm') pn)
|
||||||
ResOper ty (Yes trm) -> do
|
ResOper ty (Just trm) -> do
|
||||||
trm' <- recomp f trm
|
trm' <- recomp f trm
|
||||||
return (f,ResOper ty (Yes trm'))
|
return (f,ResOper ty (Just trm'))
|
||||||
_ -> return (f,def)
|
_ -> return (f,def)
|
||||||
recomp f t = case Map.lookup t tree of
|
recomp f t = case Map.lookup t tree of
|
||||||
Just (_,id) | operIdent id /= f -> return $ Q mo (operIdent id)
|
Just (_,id) | operIdent id /= f -> return $ Q mo (operIdent id)
|
||||||
@@ -218,7 +218,7 @@ addSubexpConsts mo tree lins = do
|
|||||||
|
|
||||||
list = Map.toList tree
|
list = Map.toList tree
|
||||||
|
|
||||||
oper id trm = (operIdent id, ResOper (Yes (EInt 8)) (Yes trm))
|
oper id trm = (operIdent id, ResOper (Just (EInt 8)) (Just trm))
|
||||||
--- impossible type encoding generated opers
|
--- impossible type encoding generated opers
|
||||||
|
|
||||||
getSubtermsMod :: Ident -> [(Ident,Info)] -> TermM (Map Term (Int,Int))
|
getSubtermsMod :: Ident -> [(Ident,Info)] -> TermM (Map Term (Int,Int))
|
||||||
@@ -228,10 +228,10 @@ getSubtermsMod mo js = do
|
|||||||
return $ Map.filter (\ (nu,_) -> nu > 1) tree0
|
return $ Map.filter (\ (nu,_) -> nu > 1) tree0
|
||||||
where
|
where
|
||||||
getInfo get fi@(f,i) = case i of
|
getInfo get fi@(f,i) = case i of
|
||||||
CncFun xs (Yes trm) pn -> do
|
CncFun xs (Just trm) pn -> do
|
||||||
get trm
|
get trm
|
||||||
return $ fi
|
return $ fi
|
||||||
ResOper ty (Yes trm) -> do
|
ResOper ty (Just trm) -> do
|
||||||
get trm
|
get trm
|
||||||
return $ fi
|
return $ fi
|
||||||
_ -> return fi
|
_ -> return fi
|
||||||
|
|||||||
@@ -1,101 +0,0 @@
|
|||||||
----------------------------------------------------------------------
|
|
||||||
-- |
|
|
||||||
-- Module : Rebuild
|
|
||||||
-- Maintainer : AR
|
|
||||||
-- Stability : (stable)
|
|
||||||
-- Portability : (portable)
|
|
||||||
--
|
|
||||||
-- > CVS $Date: 2005/05/30 21:08:14 $
|
|
||||||
-- > CVS $Author: aarne $
|
|
||||||
-- > CVS $Revision: 1.14 $
|
|
||||||
--
|
|
||||||
-- Rebuild a source module from incomplete and its with-instance.
|
|
||||||
-----------------------------------------------------------------------------
|
|
||||||
|
|
||||||
module GF.Compile.Rebuild (rebuildModule) where
|
|
||||||
|
|
||||||
import GF.Grammar.Grammar
|
|
||||||
import GF.Compile.ModDeps
|
|
||||||
import GF.Grammar.PrGrammar
|
|
||||||
import GF.Grammar.Lookup
|
|
||||||
import GF.Compile.Extend
|
|
||||||
import GF.Grammar.Macros
|
|
||||||
|
|
||||||
import GF.Infra.Ident
|
|
||||||
import GF.Infra.Modules
|
|
||||||
import GF.Infra.Option
|
|
||||||
import GF.Data.Operations
|
|
||||||
|
|
||||||
import Data.List (nub)
|
|
||||||
import Data.Maybe (isNothing)
|
|
||||||
|
|
||||||
-- | rebuilding instance + interface, and "with" modules, prior to renaming.
|
|
||||||
-- AR 24/10/2003
|
|
||||||
rebuildModule :: [SourceModule] -> SourceModule -> Err SourceModule
|
|
||||||
rebuildModule ms mo@(i,mi@(ModInfo mt stat fs_ me mw ops_ med_ js_ ps_)) = do
|
|
||||||
let gr = MGrammar ms
|
|
||||||
---- deps <- moduleDeps ms
|
|
||||||
---- is <- openInterfaces deps i
|
|
||||||
let is = [] ---- the method above is buggy: try "i -src" for two grs. AR 8/3/2005
|
|
||||||
mi' <- case mw of
|
|
||||||
|
|
||||||
-- add the information given in interface into an instance module
|
|
||||||
Nothing -> do
|
|
||||||
testErr (null is || mstatus mi == MSIncomplete)
|
|
||||||
("module" +++ prt i +++
|
|
||||||
"has open interfaces and must therefore be declared incomplete")
|
|
||||||
case mt of
|
|
||||||
MTInstance i0 -> do
|
|
||||||
m1 <- lookupModule gr i0
|
|
||||||
testErr (isModRes m1) ("interface expected instead of" +++ prt i0)
|
|
||||||
js' <- extendMod False (i0,const True) i (jments m1) (jments mi)
|
|
||||||
--- to avoid double inclusions, in instance I of I0 = J0 ** ...
|
|
||||||
case extends mi of
|
|
||||||
[] -> return $ replaceJudgements mi js'
|
|
||||||
j0s -> do
|
|
||||||
m0s <- mapM (lookupModule gr) j0s
|
|
||||||
let notInM0 c _ = all (not . isInBinTree c . jments) m0s
|
|
||||||
let js2 = filterBinTree notInM0 js'
|
|
||||||
return $ (replaceJudgements mi js2)
|
|
||||||
{positions =
|
|
||||||
buildTree (tree2list (positions m1) ++
|
|
||||||
tree2list (positions mi))}
|
|
||||||
_ -> return mi
|
|
||||||
|
|
||||||
-- add the instance opens to an incomplete module "with" instances
|
|
||||||
Just (ext,incl,ops) -> do
|
|
||||||
let (infs,insts) = unzip ops
|
|
||||||
let stat' = ifNull MSComplete (const MSIncomplete)
|
|
||||||
[i | i <- is, notElem i infs]
|
|
||||||
testErr (stat' == MSComplete || stat == MSIncomplete)
|
|
||||||
("module" +++ prt i +++ "remains incomplete")
|
|
||||||
ModInfo mt0 _ fs me' _ ops0 _ js ps0 <- lookupModule gr ext
|
|
||||||
let ops1 = nub $
|
|
||||||
ops_ ++ -- N.B. js has been name-resolved already
|
|
||||||
[OQualif i j | (i,j) <- ops] ++
|
|
||||||
[o | o <- ops0, notElem (openedModule o) infs] ++
|
|
||||||
[OQualif i i | i <- insts] ++
|
|
||||||
[OSimple i | i <- insts]
|
|
||||||
|
|
||||||
--- check if me is incomplete
|
|
||||||
let fs1 = fs `addOptions` fs_ -- new flags have priority
|
|
||||||
let js0 = [ci | ci@(c,_) <- tree2list js, isInherited incl c]
|
|
||||||
let js1 = buildTree (tree2list js_ ++ js0)
|
|
||||||
let ps1 = buildTree (tree2list ps_ ++ tree2list ps0)
|
|
||||||
let med1= nub (ext : infs ++ insts ++ med_)
|
|
||||||
return $ ModInfo mt0 stat' fs1 me Nothing ops1 med1 js1 ps1
|
|
||||||
|
|
||||||
return (i,mi')
|
|
||||||
|
|
||||||
checkCompleteInstance :: SourceModInfo -> SourceModInfo -> Err ()
|
|
||||||
checkCompleteInstance abs cnc = ifNull (return ()) (Bad . unlines) $
|
|
||||||
checkComplete [f | (f, ResOper (Yes _) _) <- abs'] cnc'
|
|
||||||
where
|
|
||||||
abs' = tree2list $ jments abs
|
|
||||||
cnc' = jments cnc
|
|
||||||
checkComplete sought given = foldr ckOne [] sought
|
|
||||||
where
|
|
||||||
ckOne f = if isInBinTree f given
|
|
||||||
then id
|
|
||||||
else (("Error: no definition given to" +++ prt f):)
|
|
||||||
|
|
||||||
@@ -116,18 +116,18 @@ refreshModule (k,ms) mi@(i,mo)
|
|||||||
| otherwise = return (k, mi:ms)
|
| otherwise = return (k, mi:ms)
|
||||||
where
|
where
|
||||||
refreshRes (k,cs) ci@(c,info) = case info of
|
refreshRes (k,cs) ci@(c,info) = case info of
|
||||||
ResOper ptyp (Yes trm) -> do ---- refresh ptyp
|
ResOper ptyp (Just trm) -> do ---- refresh ptyp
|
||||||
(k',trm') <- refreshTermKN k trm
|
(k',trm') <- refreshTermKN k trm
|
||||||
return $ (k', (c, ResOper ptyp (Yes trm')):cs)
|
return $ (k', (c, ResOper ptyp (Just trm')):cs)
|
||||||
ResOverload os tyts -> do
|
ResOverload os tyts -> do
|
||||||
(k',tyts') <- liftM (\ (t,(_,i)) -> (i,t)) $
|
(k',tyts') <- liftM (\ (t,(_,i)) -> (i,t)) $
|
||||||
appSTM (mapPairsM refresh tyts) (initIdStateN k)
|
appSTM (mapPairsM refresh tyts) (initIdStateN k)
|
||||||
return $ (k', (c, ResOverload os tyts'):cs)
|
return $ (k', (c, ResOverload os tyts'):cs)
|
||||||
CncCat mt (Yes trm) pn -> do ---- refresh mt, pn
|
CncCat mt (Just trm) pn -> do ---- refresh mt, pn
|
||||||
(k',trm') <- refreshTermKN k trm
|
(k',trm') <- refreshTermKN k trm
|
||||||
return $ (k', (c, CncCat mt (Yes trm') pn):cs)
|
return $ (k', (c, CncCat mt (Just trm') pn):cs)
|
||||||
CncFun mt (Yes trm) pn -> do ---- refresh pn
|
CncFun mt (Just trm) pn -> do ---- refresh pn
|
||||||
(k',trm') <- refreshTermKN k trm
|
(k',trm') <- refreshTermKN k trm
|
||||||
return $ (k', (c, CncFun mt (Yes trm') pn):cs)
|
return $ (k', (c, CncFun mt (Just trm') pn):cs)
|
||||||
_ -> return (k, ci:cs)
|
_ -> return (k, ci:cs)
|
||||||
|
|
||||||
|
|||||||
@@ -36,7 +36,6 @@ import GF.Grammar.Macros
|
|||||||
import GF.Grammar.PrGrammar
|
import GF.Grammar.PrGrammar
|
||||||
import GF.Grammar.AppPredefined
|
import GF.Grammar.AppPredefined
|
||||||
import GF.Grammar.Lookup
|
import GF.Grammar.Lookup
|
||||||
import GF.Compile.Extend
|
|
||||||
import GF.Data.Operations
|
import GF.Data.Operations
|
||||||
|
|
||||||
import Control.Monad
|
import Control.Monad
|
||||||
@@ -115,7 +114,7 @@ renameIdentPatt env p = do
|
|||||||
|
|
||||||
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 _ (Yes EData) -> maybe Con QC mq
|
AbsFun _ (Just EData) -> maybe Con QC mq
|
||||||
ResValue _ -> maybe Con QC mq
|
ResValue _ -> maybe Con QC mq
|
||||||
ResParam _ -> maybe Con QC mq
|
ResParam _ -> maybe Con QC mq
|
||||||
AnyInd True m -> maybe Con (const (QC m)) mq
|
AnyInd True m -> maybe Con (const (QC m)) mq
|
||||||
@@ -161,12 +160,12 @@ renameInfo mo status (i,info) = errIn
|
|||||||
ResOverload os tysts ->
|
ResOverload os tysts ->
|
||||||
liftM (ResOverload os) (mapM (pairM rent) tysts)
|
liftM (ResOverload os) (mapM (pairM rent) tysts)
|
||||||
|
|
||||||
ResParam (Yes (pp,m)) -> do
|
ResParam (Just (pp,m)) -> do
|
||||||
pp' <- mapM (renameParam status) pp
|
pp' <- mapM (renameParam status) pp
|
||||||
return $ ResParam $ Yes (pp',m)
|
return $ ResParam $ Just (pp',m)
|
||||||
ResValue (Yes (t,m)) -> do
|
ResValue (Just (t,m)) -> do
|
||||||
t' <- rent t
|
t' <- rent t
|
||||||
return $ ResValue $ Yes (t',m)
|
return $ ResValue $ Just (t',m)
|
||||||
CncCat pty ptr ppr -> liftM3 CncCat (ren pty) (ren ptr) (ren ppr)
|
CncCat pty ptr ppr -> liftM3 CncCat (ren pty) (ren ptr) (ren ppr)
|
||||||
CncFun mt ptr ppr -> liftM2 (CncFun mt) (ren ptr) (ren ppr)
|
CncFun mt ptr ppr -> liftM2 (CncFun mt) (ren ptr) (ren ppr)
|
||||||
_ -> return info
|
_ -> return info
|
||||||
@@ -174,9 +173,8 @@ renameInfo mo status (i,info) = errIn
|
|||||||
ren = renPerh rent
|
ren = renPerh rent
|
||||||
rent = renameTerm status []
|
rent = renameTerm status []
|
||||||
|
|
||||||
renPerh ren pt = case pt of
|
renPerh ren (Just t) = liftM Just $ ren t
|
||||||
Yes t -> liftM Yes $ ren t
|
renPerh ren Nothing = return Nothing
|
||||||
_ -> return pt
|
|
||||||
|
|
||||||
renameTerm :: Status -> [Ident] -> Term -> Err Term
|
renameTerm :: Status -> [Ident] -> Term -> Err Term
|
||||||
renameTerm env vars = ren vars where
|
renameTerm env vars = ren vars where
|
||||||
|
|||||||
@@ -12,122 +12,200 @@
|
|||||||
-- (Description of the module)
|
-- (Description of the module)
|
||||||
-----------------------------------------------------------------------------
|
-----------------------------------------------------------------------------
|
||||||
|
|
||||||
module GF.Compile.Update (updateRes, buildAnyTree, combineAnyInfos, unifyAnyInfo,
|
module GF.Compile.Update (buildAnyTree, extendModule, rebuildModule) where
|
||||||
-- * these auxiliaries should be somewhere else
|
|
||||||
-- since they don't use the info types
|
|
||||||
groupInfos, sortInfos, combineInfos, unifyInfos,
|
|
||||||
tryInsert, unifAbsDefs, unifConstrs
|
|
||||||
) where
|
|
||||||
|
|
||||||
import GF.Infra.Ident
|
import GF.Infra.Ident
|
||||||
import GF.Grammar.Grammar
|
import GF.Grammar.Grammar
|
||||||
import GF.Grammar.PrGrammar
|
import GF.Grammar.Printer
|
||||||
import GF.Infra.Modules
|
import GF.Infra.Modules
|
||||||
|
import GF.Infra.Option
|
||||||
|
|
||||||
import GF.Data.Operations
|
import GF.Data.Operations
|
||||||
|
|
||||||
import Data.List
|
import Data.List
|
||||||
|
import qualified Data.Map as Map
|
||||||
import Control.Monad
|
import Control.Monad
|
||||||
|
import Text.PrettyPrint
|
||||||
-- | update a resource module by adding a new or changing an old definition
|
|
||||||
updateRes :: SourceGrammar -> Ident -> Ident -> Info -> SourceGrammar
|
|
||||||
updateRes gr@(MGrammar ms) m i info = MGrammar $ map upd ms where
|
|
||||||
upd (n,mo)
|
|
||||||
| n /= m = (n,mo)
|
|
||||||
| n == m = (n,updateModule mo i info)
|
|
||||||
|
|
||||||
-- | combine a list of definitions into a balanced binary search tree
|
-- | combine a list of definitions into a balanced binary search tree
|
||||||
buildAnyTree :: [(Ident,Info)] -> Err (BinTree Ident Info)
|
buildAnyTree :: Ident -> [(Ident,Info)] -> Err (BinTree Ident Info)
|
||||||
buildAnyTree ias = do
|
buildAnyTree m = go Map.empty
|
||||||
ias' <- combineAnyInfos ias
|
where
|
||||||
return $ buildTree ias'
|
go map [] = return map
|
||||||
|
go map ((c,j):is) = do
|
||||||
|
case Map.lookup c map of
|
||||||
|
Just i -> case unifyAnyInfo c i j of
|
||||||
|
Ok k -> go (Map.insert c k map) is
|
||||||
|
Bad _ -> fail $ render (text "cannot unify the informations" $$
|
||||||
|
nest 4 (ppJudgement (c,i)) $$
|
||||||
|
text "and" $+$
|
||||||
|
nest 4 (ppJudgement (c,j)) $$
|
||||||
|
text "in module" <+> ppIdent m)
|
||||||
|
Nothing -> go (Map.insert c j map) is
|
||||||
|
|
||||||
|
extendModule :: [SourceModule] -> SourceModule -> Err SourceModule
|
||||||
|
extendModule ms (name,m)
|
||||||
|
---- Just to allow inheritance in incomplete concrete (which are not
|
||||||
|
---- compiled anyway), extensions are not built for them.
|
||||||
|
---- Should be replaced by real control. AR 4/2/2005
|
||||||
|
| mstatus m == MSIncomplete && isModCnc m = return (name,m)
|
||||||
|
| otherwise = do m' <- foldM extOne m (extend m)
|
||||||
|
return (name,m')
|
||||||
|
where
|
||||||
|
extOne mo (n,cond) = do
|
||||||
|
m0 <- lookupModule (MGrammar ms) n
|
||||||
|
|
||||||
-- | unifying information for abstract, resource, and concrete
|
-- test that the module types match, and find out if the old is complete
|
||||||
combineAnyInfos :: [(Ident,Info)] -> Err [(Ident,Info)]
|
testErr (sameMType (mtype m) (mtype mo))
|
||||||
combineAnyInfos = combineInfos unifyAnyInfo
|
("illegal extension type to module" +++ prIdent name)
|
||||||
|
|
||||||
|
let isCompl = isCompleteModule m0
|
||||||
|
|
||||||
|
-- build extension in a way depending on whether the old module is complete
|
||||||
|
js1 <- extendMod isCompl (n, isInherited cond) name (jments m0) (jments mo)
|
||||||
|
|
||||||
|
-- if incomplete, throw away extension information
|
||||||
|
return $
|
||||||
|
if isCompl
|
||||||
|
then mo {jments = js1}
|
||||||
|
else mo {extend = filter ((/=n) . fst) (extend mo)
|
||||||
|
,mexdeps= nub (n : mexdeps mo)
|
||||||
|
,jments = js1
|
||||||
|
}
|
||||||
|
|
||||||
|
-- | rebuilding instance + interface, and "with" modules, prior to renaming.
|
||||||
|
-- AR 24/10/2003
|
||||||
|
rebuildModule :: [SourceModule] -> SourceModule -> Err SourceModule
|
||||||
|
rebuildModule ms mo@(i,mi@(ModInfo mt stat fs_ me mw ops_ med_ js_ ps_)) = do
|
||||||
|
let gr = MGrammar ms
|
||||||
|
---- deps <- moduleDeps ms
|
||||||
|
---- is <- openInterfaces deps i
|
||||||
|
let is = [] ---- the method above is buggy: try "i -src" for two grs. AR 8/3/2005
|
||||||
|
mi' <- case mw of
|
||||||
|
|
||||||
|
-- add the information given in interface into an instance module
|
||||||
|
Nothing -> do
|
||||||
|
testErr (null is || mstatus mi == MSIncomplete)
|
||||||
|
("module" +++ prIdent i +++
|
||||||
|
"has open interfaces and must therefore be declared incomplete")
|
||||||
|
case mt of
|
||||||
|
MTInstance i0 -> do
|
||||||
|
m1 <- lookupModule gr i0
|
||||||
|
testErr (isModRes m1) ("interface expected instead of" +++ prIdent i0)
|
||||||
|
js' <- extendMod False (i0,const True) i (jments m1) (jments mi)
|
||||||
|
--- to avoid double inclusions, in instance I of I0 = J0 ** ...
|
||||||
|
case extends mi of
|
||||||
|
[] -> return $ replaceJudgements mi js'
|
||||||
|
j0s -> do
|
||||||
|
m0s <- mapM (lookupModule gr) j0s
|
||||||
|
let notInM0 c _ = all (not . isInBinTree c . jments) m0s
|
||||||
|
let js2 = filterBinTree notInM0 js'
|
||||||
|
return $ (replaceJudgements mi js2)
|
||||||
|
{positions = Map.union (positions m1) (positions mi)}
|
||||||
|
_ -> return mi
|
||||||
|
|
||||||
|
-- add the instance opens to an incomplete module "with" instances
|
||||||
|
Just (ext,incl,ops) -> do
|
||||||
|
let (infs,insts) = unzip ops
|
||||||
|
let stat' = ifNull MSComplete (const MSIncomplete)
|
||||||
|
[i | i <- is, notElem i infs]
|
||||||
|
testErr (stat' == MSComplete || stat == MSIncomplete)
|
||||||
|
("module" +++ prIdent i +++ "remains incomplete")
|
||||||
|
ModInfo mt0 _ fs me' _ ops0 _ js ps0 <- lookupModule gr ext
|
||||||
|
let ops1 = nub $
|
||||||
|
ops_ ++ -- N.B. js has been name-resolved already
|
||||||
|
[OQualif i j | (i,j) <- ops] ++
|
||||||
|
[o | o <- ops0, notElem (openedModule o) infs] ++
|
||||||
|
[OQualif i i | i <- insts] ++
|
||||||
|
[OSimple i | i <- insts]
|
||||||
|
|
||||||
|
--- check if me is incomplete
|
||||||
|
let fs1 = fs `addOptions` fs_ -- new flags have priority
|
||||||
|
let js0 = [ci | ci@(c,_) <- tree2list js, isInherited incl c]
|
||||||
|
let js1 = buildTree (tree2list js_ ++ js0)
|
||||||
|
let ps1 = Map.union ps_ ps0
|
||||||
|
let med1= nub (ext : infs ++ insts ++ med_)
|
||||||
|
return $ ModInfo mt0 stat' fs1 me Nothing ops1 med1 js1 ps1
|
||||||
|
|
||||||
|
return (i,mi')
|
||||||
|
|
||||||
|
-- | When extending a complete module: new information is inserted,
|
||||||
|
-- and the process is interrupted if unification fails.
|
||||||
|
-- If the extended module is incomplete, its judgements are just copied.
|
||||||
|
extendMod :: Bool -> (Ident,Ident -> Bool) -> Ident ->
|
||||||
|
BinTree Ident Info -> BinTree Ident Info ->
|
||||||
|
Err (BinTree Ident Info)
|
||||||
|
extendMod isCompl (name,cond) base old new = foldM try new $ Map.toList old
|
||||||
|
where
|
||||||
|
try new (c,i)
|
||||||
|
| not (cond c) = return new
|
||||||
|
| otherwise = case Map.lookup c new of
|
||||||
|
Just j -> case unifyAnyInfo c i j of
|
||||||
|
Ok k -> return $ updateTree (c,k) new
|
||||||
|
Bad _ -> fail $ render (text "cannot unify the information" $$
|
||||||
|
nest 4 (ppJudgement (c,i)) $$
|
||||||
|
text "in module" <+> ppIdent name <+> text "with" $$
|
||||||
|
nest 4 (ppJudgement (c,j)) $$
|
||||||
|
text "in module" <+> ppIdent base)
|
||||||
|
Nothing -> if isCompl
|
||||||
|
then return $ updateTree (c,indirInfo name i) new
|
||||||
|
else return $ updateTree (c,i) new
|
||||||
|
|
||||||
|
indirInfo :: Ident -> Info -> Info
|
||||||
|
indirInfo n info = AnyInd b n' where
|
||||||
|
(b,n') = case info of
|
||||||
|
ResValue _ -> (True,n)
|
||||||
|
ResParam _ -> (True,n)
|
||||||
|
AbsFun _ (Just EData) -> (True,n)
|
||||||
|
AnyInd b k -> (b,k)
|
||||||
|
_ -> (False,n) ---- canonical in Abs
|
||||||
|
|
||||||
unifyAnyInfo :: Ident -> Info -> Info -> Err Info
|
unifyAnyInfo :: Ident -> Info -> Info -> Err Info
|
||||||
unifyAnyInfo c i j = errIn ("combining information for" +++ prt c) $ case (i,j) of
|
unifyAnyInfo c i j = case (i,j) of
|
||||||
(AbsCat mc1 mf1, AbsCat mc2 mf2) ->
|
(AbsCat mc1 mf1, AbsCat mc2 mf2) ->
|
||||||
liftM2 AbsCat (unifPerhaps mc1 mc2) (unifConstrs mf1 mf2) -- adding constrs
|
liftM2 AbsCat (unifMaybe mc1 mc2) (unifConstrs mf1 mf2) -- adding constrs
|
||||||
(AbsFun mt1 md1, AbsFun mt2 md2) ->
|
(AbsFun mt1 md1, AbsFun mt2 md2) ->
|
||||||
liftM2 AbsFun (unifPerhaps mt1 mt2) (unifAbsDefs md1 md2) -- adding defs
|
liftM2 AbsFun (unifMaybe mt1 mt2) (unifAbsDefs md1 md2) -- adding defs
|
||||||
|
|
||||||
(ResParam mt1, ResParam mt2) -> liftM ResParam $ unifPerhaps mt1 mt2
|
(ResParam mt1, ResParam mt2) -> liftM ResParam $ unifMaybe mt1 mt2
|
||||||
|
(ResValue mt1, ResValue mt2) ->
|
||||||
|
liftM ResValue $ unifMaybe mt1 mt2
|
||||||
|
(_, ResOverload ms t) | elem c ms ->
|
||||||
|
return $ ResOverload ms t
|
||||||
(ResOper mt1 m1, ResOper mt2 m2) ->
|
(ResOper mt1 m1, ResOper mt2 m2) ->
|
||||||
liftM2 ResOper (unifPerhaps mt1 mt2) (unifPerhaps m1 m2)
|
liftM2 ResOper (unifMaybe mt1 mt2) (unifMaybe m1 m2)
|
||||||
|
|
||||||
(CncCat mc1 mf1 mp1, CncCat mc2 mf2 mp2) ->
|
(CncCat mc1 mf1 mp1, CncCat mc2 mf2 mp2) ->
|
||||||
liftM3 CncCat (unifPerhaps mc1 mc2) (unifPerhaps mf1 mf2) (unifPerhaps mp1 mp2)
|
liftM3 CncCat (unifMaybe mc1 mc2) (unifMaybe mf1 mf2) (unifMaybe mp1 mp2)
|
||||||
(CncFun m mt1 md1, CncFun _ mt2 md2) ->
|
(CncFun m mt1 md1, CncFun _ mt2 md2) ->
|
||||||
liftM2 (CncFun m) (unifPerhaps mt1 mt2) (unifPerhaps md1 md2) ---- adding defs
|
liftM2 (CncFun m) (unifMaybe mt1 mt2) (unifMaybe md1 md2) ---- adding defs
|
||||||
-- for bw compatibility with unspecified printnames in old GF
|
|
||||||
(CncFun Nothing Nope (Yes pr),_) ->
|
|
||||||
unifyAnyInfo c (CncCat Nope Nope (Yes pr)) j
|
|
||||||
(_,CncFun Nothing Nope (Yes pr)) ->
|
|
||||||
unifyAnyInfo c i (CncCat Nope Nope (Yes pr))
|
|
||||||
|
|
||||||
_ -> Bad $ "cannot unify informations in" ++++ show i ++++ "and" ++++ show j
|
(AnyInd b1 m1, AnyInd b2 m2) -> do
|
||||||
|
testErr (b1 == b2) $ "indirection status"
|
||||||
|
testErr (m1 == m2) $ "different sources of indirection"
|
||||||
|
return i
|
||||||
|
|
||||||
--- these auxiliaries should be somewhere else since they don't use the info types
|
_ -> fail "informations"
|
||||||
|
|
||||||
groupInfos :: Eq a => [(a,b)] -> [[(a,b)]]
|
-- | this is what happens when matching two values in the same module
|
||||||
groupInfos = groupBy (\i j -> fst i == fst j)
|
unifMaybe :: Eq a => Maybe a -> Maybe a -> Err (Maybe a)
|
||||||
|
unifMaybe Nothing Nothing = return Nothing
|
||||||
|
unifMaybe (Just p1) Nothing = return (Just p1)
|
||||||
|
unifMaybe Nothing (Just p2) = return (Just p2)
|
||||||
|
unifMaybe (Just p1) (Just p2)
|
||||||
|
| p1==p2 = return (Just p1)
|
||||||
|
| otherwise = fail ""
|
||||||
|
|
||||||
sortInfos :: Ord a => [(a,b)] -> [(a,b)]
|
unifAbsDefs :: Maybe Term -> Maybe Term -> Err (Maybe Term)
|
||||||
sortInfos = sortBy (\i j -> compare (fst i) (fst j))
|
|
||||||
|
|
||||||
combineInfos :: Ord a => (a -> b -> b -> Err b) -> [(a,b)] -> Err [(a,b)]
|
|
||||||
combineInfos f ris = do
|
|
||||||
let riss = groupInfos $ sortInfos ris
|
|
||||||
mapM (unifyInfos f) riss
|
|
||||||
|
|
||||||
unifyInfos :: (a -> b -> b -> Err b) -> [(a,b)] -> Err (a,b)
|
|
||||||
unifyInfos _ [] = Bad "empty info list"
|
|
||||||
unifyInfos unif ris = do
|
|
||||||
let c = fst $ head ris
|
|
||||||
let infos = map snd ris
|
|
||||||
let ([i],is) = splitAt 1 infos
|
|
||||||
info <- foldM (unif c) i is
|
|
||||||
return (c,info)
|
|
||||||
|
|
||||||
|
|
||||||
tryInsert :: Ord a => (b -> b -> Err b) -> (b -> b) ->
|
|
||||||
BinTree a b -> (a,b) -> Err (BinTree a b)
|
|
||||||
tryInsert unif indir tree z@(x, info) = case justLookupTree x tree of
|
|
||||||
Ok info0 -> do
|
|
||||||
info1 <- unif info info0
|
|
||||||
return $ updateTree (x,info1) tree
|
|
||||||
_ -> return $ updateTree (x,indir info) tree
|
|
||||||
|
|
||||||
{- ----
|
|
||||||
case tree of
|
|
||||||
NT -> return $ BT (x, indir info) NT NT
|
|
||||||
BT c@(a,info0) left right
|
|
||||||
| x < a -> do
|
|
||||||
left' <- tryInsert unif indir left z
|
|
||||||
return $ BT c left' right
|
|
||||||
| x > a -> do
|
|
||||||
right' <- tryInsert unif indir right z
|
|
||||||
return $ BT c left right'
|
|
||||||
| x == a -> do
|
|
||||||
info' <- unif info info0
|
|
||||||
return $ BT (x,info') left right
|
|
||||||
-}
|
|
||||||
|
|
||||||
--- addToMaybeList m c = maybe (return c) (\old -> return (c ++ old)) m
|
|
||||||
|
|
||||||
unifAbsDefs :: Perh Term -> Perh Term -> Err (Perh Term)
|
|
||||||
unifAbsDefs p1 p2 = case (p1,p2) of
|
unifAbsDefs p1 p2 = case (p1,p2) of
|
||||||
(Nope, _) -> return p2
|
(Nothing, _) -> return p2
|
||||||
(_, Nope) -> return p1
|
(_, Nothing) -> return p1
|
||||||
(Yes (Eqs bs), Yes (Eqs ds)) -> return $ yes $ Eqs $ bs ++ ds --- order!
|
(Just (Eqs bs), Just (Eqs ds))
|
||||||
_ -> Bad "update conflict for definitions"
|
-> return $ Just $ Eqs $ bs ++ ds --- order!
|
||||||
|
_ -> fail "definitions"
|
||||||
|
|
||||||
unifConstrs :: Perh [Term] -> Perh [Term] -> Err (Perh [Term])
|
unifConstrs :: Maybe [Term] -> Maybe [Term] -> Err (Maybe [Term])
|
||||||
unifConstrs p1 p2 = case (p1,p2) of
|
unifConstrs p1 p2 = case (p1,p2) of
|
||||||
(Nope, _) -> return p2
|
(Nothing, _) -> return p2
|
||||||
(_, Nope) -> return p1
|
(_, Nothing) -> return p1
|
||||||
(Yes bs, Yes ds) -> return $ yes $ bs ++ ds
|
(Just bs, Just ds) -> return $ Just $ bs ++ ds
|
||||||
_ -> Bad "update conflict for constructors"
|
|
||||||
|
|||||||
@@ -26,11 +26,6 @@ module GF.Data.Operations (-- * misc functions
|
|||||||
-- ** checking
|
-- ** checking
|
||||||
checkUnique,
|
checkUnique,
|
||||||
|
|
||||||
-- * a three-valued maybe type to express indirections
|
|
||||||
Perhaps(..), yes, may, nope,
|
|
||||||
mapP,
|
|
||||||
unifPerhaps, updatePerhaps, updatePerhapsHard,
|
|
||||||
|
|
||||||
-- * binary search trees; now with FiniteMap
|
-- * binary search trees; now with FiniteMap
|
||||||
BinTree, emptyBinTree, isInBinTree, justLookupTree,
|
BinTree, emptyBinTree, isInBinTree, justLookupTree,
|
||||||
lookupTree, lookupTreeMany, lookupTreeManyAll, updateTree,
|
lookupTree, lookupTreeMany, lookupTreeManyAll, updateTree,
|
||||||
@@ -127,51 +122,6 @@ checkUnique ss = ["overloaded" +++ show s | s <- nub overloads] where
|
|||||||
overloads = filter overloaded ss
|
overloads = filter overloaded ss
|
||||||
overloaded s = length (filter (==s) ss) > 1
|
overloaded s = length (filter (==s) ss) > 1
|
||||||
|
|
||||||
-- | a three-valued maybe type to express indirections
|
|
||||||
data Perhaps a b = Yes a | May b | Nope deriving (Show,Read,Eq,Ord)
|
|
||||||
|
|
||||||
yes :: a -> Perhaps a b
|
|
||||||
yes = Yes
|
|
||||||
|
|
||||||
may :: b -> Perhaps a b
|
|
||||||
may = May
|
|
||||||
|
|
||||||
nope :: Perhaps a b
|
|
||||||
nope = Nope
|
|
||||||
|
|
||||||
mapP :: (a -> c) -> Perhaps a b -> Perhaps c b
|
|
||||||
mapP f p = case p of
|
|
||||||
Yes a -> Yes (f a)
|
|
||||||
May b -> May b
|
|
||||||
Nope -> Nope
|
|
||||||
|
|
||||||
-- | this is what happens when matching two values in the same module
|
|
||||||
unifPerhaps :: (Eq a, Eq b, Show a, Show b) =>
|
|
||||||
Perhaps a b -> Perhaps a b -> Err (Perhaps a b)
|
|
||||||
unifPerhaps p1 p2 = case (p1,p2) of
|
|
||||||
(Nope, _) -> return p2
|
|
||||||
(_, Nope) -> return p1
|
|
||||||
_ -> if p1==p2 then return p1
|
|
||||||
else Bad ("update conflict between" ++++ show p1 ++++ show p2)
|
|
||||||
|
|
||||||
-- | this is what happens when updating a module extension
|
|
||||||
updatePerhaps :: (Eq a,Eq b, Show a, Show b) =>
|
|
||||||
b -> Perhaps a b -> Perhaps a b -> Err (Perhaps a b)
|
|
||||||
updatePerhaps old p1 p2 = case (p1,p2) of
|
|
||||||
(Yes a, Nope) -> return $ may old
|
|
||||||
(May older,Nope) -> return $ may older
|
|
||||||
(_, May a) -> Bad "strange indirection"
|
|
||||||
_ -> unifPerhaps p1 p2
|
|
||||||
|
|
||||||
-- | here the value is copied instead of referred to; used for oper types
|
|
||||||
updatePerhapsHard :: (Eq a, Eq b, Show a, Show b) => b ->
|
|
||||||
Perhaps a b -> Perhaps a b -> Err (Perhaps a b)
|
|
||||||
updatePerhapsHard old p1 p2 = case (p1,p2) of
|
|
||||||
(Yes a, Nope) -> return $ yes a
|
|
||||||
(May older,Nope) -> return $ may older
|
|
||||||
(_, May a) -> Bad "strange indirection"
|
|
||||||
_ -> unifPerhaps p1 p2
|
|
||||||
|
|
||||||
-- binary search trees
|
-- binary search trees
|
||||||
|
|
||||||
type BinTree a b = Map a b
|
type BinTree a b = Map a b
|
||||||
|
|||||||
@@ -228,16 +228,6 @@ instance Binary Patt where
|
|||||||
17 -> get >>= \x -> return (PMacro x)
|
17 -> get >>= \x -> return (PMacro x)
|
||||||
18 -> get >>= \(x,y) -> return (PM x y)
|
18 -> get >>= \(x,y) -> return (PM x y)
|
||||||
|
|
||||||
instance (Binary a, Binary b) => Binary (Perhaps a b) where
|
|
||||||
put (Yes x) = putWord8 0 >> put x
|
|
||||||
put (May y) = putWord8 1 >> put y
|
|
||||||
put Nope = putWord8 2
|
|
||||||
get = do tag <- getWord8
|
|
||||||
case tag of
|
|
||||||
0 -> fmap Yes get
|
|
||||||
1 -> fmap May get
|
|
||||||
2 -> return Nope
|
|
||||||
|
|
||||||
instance Binary TInfo where
|
instance Binary TInfo where
|
||||||
put TRaw = putWord8 0
|
put TRaw = putWord8 0
|
||||||
put (TTyped t) = putWord8 1 >> put t
|
put (TTyped t) = putWord8 1 >> put t
|
||||||
|
|||||||
@@ -21,8 +21,6 @@ module GF.Grammar.Grammar (SourceGrammar,
|
|||||||
mapSourceModule,
|
mapSourceModule,
|
||||||
Info(..),
|
Info(..),
|
||||||
PValues,
|
PValues,
|
||||||
Perh,
|
|
||||||
MPr,
|
|
||||||
Type,
|
Type,
|
||||||
Cat,
|
Cat,
|
||||||
Fun,
|
Fun,
|
||||||
@@ -82,30 +80,24 @@ type PValues = [Term]
|
|||||||
-- and indirection to module (/INDIR/)
|
-- and indirection to module (/INDIR/)
|
||||||
data Info =
|
data Info =
|
||||||
-- judgements in abstract syntax
|
-- judgements in abstract syntax
|
||||||
AbsCat (Perh Context) (Perh [Term]) -- ^ (/ABS/) constructors; must be 'Id' or 'QId'
|
AbsCat (Maybe Context) (Maybe [Term]) -- ^ (/ABS/) constructors; must be 'Id' or 'QId'
|
||||||
| AbsFun (Perh Type) (Perh Term) -- ^ (/ABS/) 'Yes f' = canonical
|
| AbsFun (Maybe Type) (Maybe Term) -- ^ (/ABS/) 'Yes f' = canonical
|
||||||
|
|
||||||
-- judgements in resource
|
-- judgements in resource
|
||||||
| ResParam (Perh ([Param],Maybe PValues)) -- ^ (/RES/)
|
| ResParam (Maybe ([Param],Maybe PValues)) -- ^ (/RES/)
|
||||||
| ResValue (Perh (Type,Maybe Int)) -- ^ (/RES/) to mark parameter constructors for lookup
|
| ResValue (Maybe (Type,Maybe Int)) -- ^ (/RES/) to mark parameter constructors for lookup
|
||||||
| ResOper (Perh Type) (Perh Term) -- ^ (/RES/)
|
| ResOper (Maybe Type) (Maybe Term) -- ^ (/RES/)
|
||||||
|
|
||||||
| ResOverload [Ident] [(Type,Term)] -- ^ (/RES/) idents: modules inherited
|
| ResOverload [Ident] [(Type,Term)] -- ^ (/RES/) idents: modules inherited
|
||||||
|
|
||||||
-- judgements in concrete syntax
|
-- judgements in concrete syntax
|
||||||
| CncCat (Perh Type) (Perh Term) MPr -- ^ (/CNC/) lindef ini'zed,
|
| CncCat (Maybe Type) (Maybe Term) (Maybe Term) -- ^ (/CNC/) lindef ini'zed,
|
||||||
| CncFun (Maybe (Ident,(Context,Type))) (Perh Term) MPr -- (/CNC/) type info added at 'TC'
|
| CncFun (Maybe (Ident,(Context,Type))) (Maybe Term) (Maybe Term) -- ^ (/CNC/) type info added at 'TC'
|
||||||
|
|
||||||
-- indirection to module Ident
|
-- indirection to module Ident
|
||||||
| AnyInd Bool Ident -- ^ (/INDIR/) the 'Bool' says if canonical
|
| AnyInd Bool Ident -- ^ (/INDIR/) the 'Bool' says if canonical
|
||||||
deriving (Read, Show)
|
deriving (Read, Show)
|
||||||
|
|
||||||
-- | to express indirection to other module
|
|
||||||
type Perh a = Perhaps a Ident
|
|
||||||
|
|
||||||
-- | printname
|
|
||||||
type MPr = Perhaps Term Ident
|
|
||||||
|
|
||||||
type Type = Term
|
type Type = Term
|
||||||
type Cat = QIdent
|
type Cat = QIdent
|
||||||
type Fun = QIdent
|
type Fun = QIdent
|
||||||
|
|||||||
@@ -78,15 +78,15 @@ lookupResDefKind gr m c
|
|||||||
mo <- lookupModule gr m
|
mo <- lookupModule gr m
|
||||||
info <- lookupIdentInfoIn mo m c
|
info <- lookupIdentInfoIn mo m c
|
||||||
case info of
|
case info of
|
||||||
ResOper _ (Yes t) -> return (qualifAnnot m t, 0)
|
ResOper _ (Just t) -> return (qualifAnnot m t, 0)
|
||||||
ResOper _ Nope -> return (Q m c, 0) ---- if isTop then lookExt m c
|
ResOper _ Nothing -> return (Q m c, 0) ---- if isTop then lookExt m c
|
||||||
---- else prtBad "cannot find in exts" c
|
---- else prtBad "cannot find in exts" c
|
||||||
|
|
||||||
CncCat (Yes ty) _ _ -> liftM (flip (,) 1) $ lock c ty
|
CncCat (Just ty) _ _ -> liftM (flip (,) 1) $ lock c ty
|
||||||
CncCat _ _ _ -> liftM (flip (,) 1) $ lock c defLinType
|
CncCat _ _ _ -> liftM (flip (,) 1) $ lock c defLinType
|
||||||
CncFun (Just (cat,_)) (Yes tr) _ -> liftM (flip (,) 1) $ unlock cat tr
|
|
||||||
|
|
||||||
CncFun _ (Yes tr) _ -> liftM (flip (,) 1) (return tr) ---- $ unlock c tr
|
CncFun (Just (cat,_)) (Just tr) _ -> liftM (flip (,) 1) $ unlock cat tr
|
||||||
|
CncFun _ (Just tr) _ -> liftM (flip (,) 1) (return tr) ---- $ unlock c tr
|
||||||
|
|
||||||
AnyInd _ n -> look False n c
|
AnyInd _ n -> look False n c
|
||||||
ResParam _ -> return (QC m c,2)
|
ResParam _ -> return (QC m c,2)
|
||||||
@@ -100,8 +100,7 @@ lookupResType gr m c = do
|
|||||||
mo <- lookupModule gr m
|
mo <- lookupModule gr m
|
||||||
info <- lookupIdentInfo mo c
|
info <- lookupIdentInfo mo c
|
||||||
case info of
|
case info of
|
||||||
ResOper (Yes t) _ -> return $ qualifAnnot m t
|
ResOper (Just t) _ -> return $ qualifAnnot m t
|
||||||
ResOper (May n) _ -> lookupResType gr n c
|
|
||||||
|
|
||||||
-- used in reused concrete
|
-- used in reused concrete
|
||||||
CncCat _ _ _ -> return typeType
|
CncCat _ _ _ -> return typeType
|
||||||
@@ -111,7 +110,7 @@ lookupResType gr m c = do
|
|||||||
CncFun _ _ _ -> lookFunType m m c
|
CncFun _ _ _ -> lookFunType m m c
|
||||||
AnyInd _ n -> lookupResType gr n c
|
AnyInd _ n -> lookupResType gr n c
|
||||||
ResParam _ -> return $ typePType
|
ResParam _ -> return $ typePType
|
||||||
ResValue (Yes (t,_)) -> return $ qualifAnnotPar m t
|
ResValue (Just (t,_)) -> return $ qualifAnnotPar m t
|
||||||
_ -> Bad $ prt c +++ "has no type defined in resource" +++ prt m
|
_ -> Bad $ prt c +++ "has no type defined in resource" +++ prt m
|
||||||
where
|
where
|
||||||
lookFunType e m c = do
|
lookFunType e m c = do
|
||||||
@@ -121,7 +120,7 @@ lookupResType gr m c = do
|
|||||||
mu <- lookupModule gr a
|
mu <- lookupModule gr a
|
||||||
info <- lookupIdentInfo mu c
|
info <- lookupIdentInfo mu c
|
||||||
case info of
|
case info of
|
||||||
AbsFun (Yes ty) _ -> return $ redirectTerm e ty
|
AbsFun (Just ty) _ -> return $ redirectTerm e ty
|
||||||
AbsCat _ _ -> return typeType
|
AbsCat _ _ -> return typeType
|
||||||
AnyInd _ n -> lookFun e m c n
|
AnyInd _ n -> lookFun e m c n
|
||||||
_ -> prtBad "cannot find type of reused function" c
|
_ -> prtBad "cannot find type of reused function" c
|
||||||
@@ -154,9 +153,9 @@ lookupParams gr = look True where
|
|||||||
mo <- lookupModule gr m
|
mo <- lookupModule gr m
|
||||||
info <- lookupIdentInfo mo c
|
info <- lookupIdentInfo mo c
|
||||||
case info of
|
case info of
|
||||||
ResParam (Yes psm) -> return psm
|
ResParam (Just psm) -> return psm
|
||||||
AnyInd _ n -> look False n c
|
AnyInd _ n -> look False n c
|
||||||
_ -> Bad $ prt c +++ "has no parameters defined in resource" +++ prt m
|
_ -> Bad $ prt c +++ "has no parameters defined in resource" +++ prt m
|
||||||
lookExt m c =
|
lookExt m c =
|
||||||
checks [look False n c | n <- allExtensions gr m]
|
checks [look False n c | n <- allExtensions gr m]
|
||||||
|
|
||||||
@@ -231,9 +230,9 @@ lookupAbsDef gr m c = errIn ("looking up absdef of" +++ prt c) $ do
|
|||||||
mo <- lookupModule gr m
|
mo <- lookupModule gr m
|
||||||
info <- lookupIdentInfo mo c
|
info <- lookupIdentInfo mo c
|
||||||
case info of
|
case info of
|
||||||
AbsFun _ (Yes t) -> return (Just t)
|
AbsFun _ (Just t) -> return (Just t)
|
||||||
AnyInd _ n -> lookupAbsDef gr n c
|
AnyInd _ n -> lookupAbsDef gr n c
|
||||||
_ -> return Nothing
|
_ -> return Nothing
|
||||||
|
|
||||||
lookupLincat :: SourceGrammar -> Ident -> Ident -> Err Type
|
lookupLincat :: SourceGrammar -> Ident -> Ident -> Err Type
|
||||||
lookupLincat gr m c | isPredefCat c = return defLinType --- ad hoc; not needed?
|
lookupLincat gr m c | isPredefCat c = return defLinType --- ad hoc; not needed?
|
||||||
@@ -241,9 +240,9 @@ lookupLincat gr m c = do
|
|||||||
mo <- lookupModule gr m
|
mo <- lookupModule gr m
|
||||||
info <- lookupIdentInfo mo c
|
info <- lookupIdentInfo mo c
|
||||||
case info of
|
case info of
|
||||||
CncCat (Yes t) _ _ -> return t
|
CncCat (Just t) _ _ -> return t
|
||||||
AnyInd _ n -> lookupLincat gr n c
|
AnyInd _ n -> lookupLincat gr n c
|
||||||
_ -> Bad $ prt c +++ "has no linearization type in" +++ prt m
|
_ -> Bad $ prt c +++ "has no linearization type in" +++ prt m
|
||||||
|
|
||||||
-- | this is needed at compile time
|
-- | this is needed at compile time
|
||||||
lookupFunType :: SourceGrammar -> Ident -> Ident -> Err Type
|
lookupFunType :: SourceGrammar -> Ident -> Ident -> Err Type
|
||||||
@@ -251,9 +250,9 @@ lookupFunType gr m c = do
|
|||||||
mo <- lookupModule gr m
|
mo <- lookupModule gr m
|
||||||
info <- lookupIdentInfo mo c
|
info <- lookupIdentInfo mo c
|
||||||
case info of
|
case info of
|
||||||
AbsFun (Yes t) _ -> return t
|
AbsFun (Just t) _ -> return t
|
||||||
AnyInd _ n -> lookupFunType gr n c
|
AnyInd _ n -> lookupFunType gr n c
|
||||||
_ -> prtBad "cannot find type of" c
|
_ -> prtBad "cannot find type of" c
|
||||||
|
|
||||||
-- | this is needed at compile time
|
-- | this is needed at compile time
|
||||||
lookupCatContext :: SourceGrammar -> Ident -> Ident -> Err Context
|
lookupCatContext :: SourceGrammar -> Ident -> Ident -> Err Context
|
||||||
@@ -261,9 +260,9 @@ lookupCatContext gr m c = do
|
|||||||
mo <- lookupModule gr m
|
mo <- lookupModule gr m
|
||||||
info <- lookupIdentInfo mo c
|
info <- lookupIdentInfo mo c
|
||||||
case info of
|
case info of
|
||||||
AbsCat (Yes co) _ -> return co
|
AbsCat (Just co) _ -> return co
|
||||||
AnyInd _ n -> lookupCatContext gr n c
|
AnyInd _ n -> lookupCatContext gr n c
|
||||||
_ -> prtBad "unknown category" c
|
_ -> prtBad "unknown category" c
|
||||||
|
|
||||||
-- The first type argument is uncomputed, usually a category symbol.
|
-- The first type argument is uncomputed, usually a category symbol.
|
||||||
-- This is a hack to find implicit (= reused) opers.
|
-- This is a hack to find implicit (= reused) opers.
|
||||||
@@ -273,14 +272,14 @@ opersForType gr orig val =
|
|||||||
[((i,f),ty) | (i,m) <- modules gr, (f,ty) <- opers i m val] where
|
[((i,f),ty) | (i,m) <- modules gr, (f,ty) <- opers i m val] where
|
||||||
opers i m val =
|
opers i m val =
|
||||||
[(f,ty) |
|
[(f,ty) |
|
||||||
(f,ResOper (Yes ty) _) <- tree2list $ jments m,
|
(f,ResOper (Just ty) _) <- tree2list $ jments m,
|
||||||
Ok valt <- [valTypeCnc ty],
|
Ok valt <- [valTypeCnc ty],
|
||||||
elem valt [val,orig]
|
elem valt [val,orig]
|
||||||
] ++
|
] ++
|
||||||
let cat = err error snd (valCat orig) in --- ignore module
|
let cat = err error snd (valCat orig) in --- ignore module
|
||||||
[(f,ty) |
|
[(f,ty) |
|
||||||
Ok a <- [abstractOfConcrete gr i >>= lookupModule gr],
|
Ok a <- [abstractOfConcrete gr i >>= lookupModule gr],
|
||||||
(f, AbsFun (Yes ty0) _) <- tree2list $ jments a,
|
(f, AbsFun (Just ty0) _) <- tree2list $ jments a,
|
||||||
let ty = redirectTerm i ty0,
|
let ty = redirectTerm i ty0,
|
||||||
Ok valt <- [valCat ty],
|
Ok valt <- [valCat ty],
|
||||||
cat == snd valt ---
|
cat == snd valt ---
|
||||||
|
|||||||
@@ -21,15 +21,8 @@
|
|||||||
|
|
||||||
module GF.Grammar.PrGrammar (Print(..),
|
module GF.Grammar.PrGrammar (Print(..),
|
||||||
prtBad,
|
prtBad,
|
||||||
prGrammar, prModule,
|
prGrammar,
|
||||||
prContext, prParam,
|
|
||||||
prQIdent, prQIdent_,
|
|
||||||
prRefinement, prTermOpt,
|
|
||||||
-- prt_Tree, prMarkedTree, prTree,
|
|
||||||
-- tree2string, prprTree,
|
|
||||||
prConstrs, prConstraints,
|
prConstrs, prConstraints,
|
||||||
-- prMetaSubst, prEnv, prMSubst,
|
|
||||||
prExp, prOperSignature,
|
|
||||||
prTermTabular
|
prTermTabular
|
||||||
) where
|
) where
|
||||||
|
|
||||||
|
|||||||
@@ -69,30 +69,30 @@ ppOptions opts =
|
|||||||
ppJudgement (id, AbsCat pcont pconstrs) =
|
ppJudgement (id, AbsCat pcont pconstrs) =
|
||||||
text "cat" <+> ppIdent id <+>
|
text "cat" <+> ppIdent id <+>
|
||||||
(case pcont of
|
(case pcont of
|
||||||
Yes cont -> hsep (map ppDecl cont)
|
Just cont -> hsep (map ppDecl cont)
|
||||||
_ -> empty) <+> semi $$
|
Nothing -> empty) <+> semi $$
|
||||||
case pconstrs of
|
case pconstrs of
|
||||||
Yes costrs -> text "data" <+> ppIdent id <+> equals <+> fsep (intersperse (char '|') (map (ppTerm 0) costrs)) <+> semi
|
Just costrs -> text "data" <+> ppIdent id <+> equals <+> fsep (intersperse (char '|') (map (ppTerm 0) costrs)) <+> semi
|
||||||
_ -> empty
|
Nothing -> empty
|
||||||
ppJudgement (id, AbsFun ptype pexp) =
|
ppJudgement (id, AbsFun ptype pexp) =
|
||||||
(case ptype of
|
(case ptype of
|
||||||
Yes typ -> text "fun" <+> ppIdent id <+> colon <+> ppTerm 0 typ <+> semi
|
Just typ -> text "fun" <+> ppIdent id <+> colon <+> ppTerm 0 typ <+> semi
|
||||||
_ -> empty) $$
|
Nothing -> empty) $$
|
||||||
(case pexp of
|
(case pexp of
|
||||||
Yes EData -> empty
|
Just EData -> empty
|
||||||
Yes (Eqs [(ps,e)]) -> text "def" <+> ppIdent id <+> hcat (map (ppPatt 2) ps) <+> equals <+> ppTerm 0 e <+> semi
|
Just (Eqs [(ps,e)]) -> text "def" <+> ppIdent id <+> hcat (map (ppPatt 2) ps) <+> equals <+> ppTerm 0 e <+> semi
|
||||||
Yes exp -> text "def" <+> ppIdent id <+> equals <+> ppTerm 0 exp <+> semi
|
Just exp -> text "def" <+> ppIdent id <+> equals <+> ppTerm 0 exp <+> semi
|
||||||
_ -> empty)
|
Nothing -> empty)
|
||||||
ppJudgement (id, ResParam pparams) =
|
ppJudgement (id, ResParam pparams) =
|
||||||
text "param" <+> ppIdent id <+>
|
text "param" <+> ppIdent id <+>
|
||||||
(case pparams of
|
(case pparams of
|
||||||
Yes (ps,_) -> equals <+> fsep (intersperse (char '|') (map ppParam ps))
|
Just (ps,_) -> equals <+> fsep (intersperse (char '|') (map ppParam ps))
|
||||||
_ -> empty) <+> semi
|
_ -> empty) <+> semi
|
||||||
ppJudgement (id, ResValue pvalue) = empty
|
ppJudgement (id, ResValue pvalue) = empty
|
||||||
ppJudgement (id, ResOper ptype pexp) =
|
ppJudgement (id, ResOper ptype pexp) =
|
||||||
text "oper" <+> ppIdent id <+>
|
text "oper" <+> ppIdent id <+>
|
||||||
(case ptype of {Yes t -> colon <+> ppTerm 0 t; _ -> empty} $$
|
(case ptype of {Just t -> colon <+> ppTerm 0 t; Nothing -> empty} $$
|
||||||
case pexp of {Yes e -> equals <+> ppTerm 0 e; _ -> empty}) <+> semi
|
case pexp of {Just e -> equals <+> ppTerm 0 e; Nothing -> empty}) <+> semi
|
||||||
ppJudgement (id, ResOverload ids defs) =
|
ppJudgement (id, ResOverload ids defs) =
|
||||||
text "oper" <+> ppIdent id <+> equals <+>
|
text "oper" <+> ppIdent id <+> equals <+>
|
||||||
(text "overload" <+> lbrace $$
|
(text "overload" <+> lbrace $$
|
||||||
@@ -100,22 +100,22 @@ ppJudgement (id, ResOverload ids defs) =
|
|||||||
rbrace) <+> semi
|
rbrace) <+> semi
|
||||||
ppJudgement (id, CncCat ptype pexp pprn) =
|
ppJudgement (id, CncCat ptype pexp pprn) =
|
||||||
(case ptype of
|
(case ptype of
|
||||||
Yes typ -> text "lincat" <+> ppIdent id <+> equals <+> ppTerm 0 typ <+> semi
|
Just typ -> text "lincat" <+> ppIdent id <+> equals <+> ppTerm 0 typ <+> semi
|
||||||
_ -> empty) $$
|
Nothing -> empty) $$
|
||||||
(case pexp of
|
(case pexp of
|
||||||
Yes exp -> text "lindef" <+> ppIdent id <+> equals <+> ppTerm 0 exp <+> semi
|
Just exp -> text "lindef" <+> ppIdent id <+> equals <+> ppTerm 0 exp <+> semi
|
||||||
_ -> empty) $$
|
Nothing -> empty) $$
|
||||||
(case pprn of
|
(case pprn of
|
||||||
Yes prn -> text "printname" <+> text "cat" <+> ppIdent id <+> equals <+> ppTerm 0 prn <+> semi
|
Just prn -> text "printname" <+> text "cat" <+> ppIdent id <+> equals <+> ppTerm 0 prn <+> semi
|
||||||
_ -> empty)
|
Nothing -> empty)
|
||||||
ppJudgement (id, CncFun ptype pdef pprn) =
|
ppJudgement (id, CncFun ptype pdef pprn) =
|
||||||
(case pdef of
|
(case pdef of
|
||||||
Yes e -> let (vs,e') = getAbs e
|
Just e -> let (vs,e') = getAbs e
|
||||||
in text "lin" <+> ppIdent id <+> hsep (map ppIdent vs) <+> equals <+> ppTerm 0 e' <+> semi
|
in text "lin" <+> ppIdent id <+> hsep (map ppIdent vs) <+> equals <+> ppTerm 0 e' <+> semi
|
||||||
_ -> empty) $$
|
Nothing -> empty) $$
|
||||||
(case pprn of
|
(case pprn of
|
||||||
Yes prn -> text "printname" <+> text "fun" <+> ppIdent id <+> equals <+> ppTerm 0 prn <+> semi
|
Just prn -> text "printname" <+> text "fun" <+> ppIdent id <+> equals <+> ppTerm 0 prn <+> semi
|
||||||
_ -> empty)
|
Nothing -> empty)
|
||||||
ppJudgement (id, AnyInd cann mid) = text "ind" <+> ppIdent id <+> equals <+> (if cann then text "canonical" else empty) <+> ppIdent mid
|
ppJudgement (id, AnyInd cann mid) = text "ind" <+> ppIdent id <+> equals <+> (if cann then text "canonical" else empty) <+> ppIdent mid
|
||||||
|
|
||||||
ppTerm d (Abs v e) = let (vs,e') = getAbs e
|
ppTerm d (Abs v e) = let (vs,e') = getAbs e
|
||||||
|
|||||||
@@ -94,9 +94,9 @@ cf2grammar :: CF -> (BinTree Ident Info, BinTree Ident Info)
|
|||||||
cf2grammar rules = (buildTree abs, buildTree conc) where
|
cf2grammar rules = (buildTree abs, buildTree conc) where
|
||||||
abs = cats ++ funs
|
abs = cats ++ funs
|
||||||
conc = lincats ++ lins
|
conc = lincats ++ lins
|
||||||
cats = [(cat, AbsCat (yes []) (yes [])) |
|
cats = [(cat, AbsCat (Just []) (Just [])) |
|
||||||
cat <- nub (concat (map cf2cat rules))] ----notPredef cat
|
cat <- nub (concat (map cf2cat rules))] ----notPredef cat
|
||||||
lincats = [(cat, CncCat (yes defLinType) nope nope) | (cat,AbsCat _ _) <- cats]
|
lincats = [(cat, CncCat (Just defLinType) Nothing Nothing) | (cat,AbsCat _ _) <- cats]
|
||||||
(funs,lins) = unzip (map cf2rule rules)
|
(funs,lins) = unzip (map cf2rule rules)
|
||||||
|
|
||||||
cf2cat :: CFRule -> [Ident]
|
cf2cat :: CFRule -> [Ident]
|
||||||
@@ -105,15 +105,15 @@ cf2cat (_,(cat, items)) = map identS $ cat : [c | Left c <- items]
|
|||||||
cf2rule :: CFRule -> ((Ident,Info),(Ident,Info))
|
cf2rule :: CFRule -> ((Ident,Info),(Ident,Info))
|
||||||
cf2rule (fun, (cat, items)) = (def,ldef) where
|
cf2rule (fun, (cat, items)) = (def,ldef) where
|
||||||
f = identS fun
|
f = identS fun
|
||||||
def = (f, AbsFun (yes (mkProd (args', Cn (identS cat), []))) nope)
|
def = (f, AbsFun (Just (mkProd (args', Cn (identS cat), []))) Nothing)
|
||||||
args0 = zip (map (identS . ("x" ++) . show) [0..]) items
|
args0 = zip (map (identS . ("x" ++) . show) [0..]) items
|
||||||
args = [(v, Cn (identS c)) | (v, Left c) <- args0]
|
args = [(v, Cn (identS c)) | (v, Left c) <- args0]
|
||||||
args' = [(identS "_", Cn (identS c)) | (_, Left c) <- args0]
|
args' = [(identS "_", Cn (identS c)) | (_, Left c) <- args0]
|
||||||
ldef = (f, CncFun
|
ldef = (f, CncFun
|
||||||
Nothing
|
Nothing
|
||||||
(yes (mkAbs (map fst args)
|
(Just (mkAbs (map fst args)
|
||||||
(mkRecord (const theLinLabel) [foldconcat (map mkIt args0)])))
|
(mkRecord (const theLinLabel) [foldconcat (map mkIt args0)])))
|
||||||
nope)
|
Nothing)
|
||||||
mkIt (v, Left _) = P (Vr v) theLinLabel
|
mkIt (v, Left _) = P (Vr v) theLinLabel
|
||||||
mkIt (_, Right a) = K a
|
mkIt (_, Right a) = K a
|
||||||
foldconcat [] = K ""
|
foldconcat [] = K ""
|
||||||
|
|||||||
@@ -74,18 +74,16 @@ mkTopDefs ds = ds
|
|||||||
|
|
||||||
trAnyDef :: (Ident,Info) -> [P.TopDef]
|
trAnyDef :: (Ident,Info) -> [P.TopDef]
|
||||||
trAnyDef (i,info) = let i' = tri i in case info of
|
trAnyDef (i,info) = let i' = tri i in case info of
|
||||||
AbsCat (Yes co) pd -> [P.DefCat [P.SimpleCatDef i' (map trDecl co)]]
|
AbsCat (Just co) pd -> [P.DefCat [P.SimpleCatDef i' (map trDecl co)]]
|
||||||
AbsFun (Yes ty) (Yes EData) -> [P.DefFunData [P.FunDef [i'] (trt ty)]]
|
AbsFun (Just ty) (Just EData) -> [P.DefFunData [P.FunDef [i'] (trt ty)]]
|
||||||
AbsFun (Yes ty) pt -> [P.DefFun [P.FunDef [i'] (trt ty)]] ++ case pt of
|
AbsFun (Just ty) pt -> [P.DefFun [P.FunDef [i'] (trt ty)]] ++ case pt of
|
||||||
Yes t -> [P.DefDef [P.DDef [mkName i'] (trt t)]]
|
Just t -> [P.DefDef [P.DDef [mkName i'] (trt t)]]
|
||||||
_ -> []
|
Nothing -> []
|
||||||
AbsFun (May b) _ -> [P.DefFun [P.FunDef [i'] (P.EIndir (tri b))]]
|
|
||||||
|
|
||||||
ResOper pty ptr -> [P.DefOper [trDef i' pty ptr]]
|
ResOper pty ptr -> [P.DefOper [trDef i' pty ptr]]
|
||||||
ResParam pp -> [P.DefPar [case pp of
|
ResParam pp -> [P.DefPar [case pp of
|
||||||
Yes (ps,_) -> P.ParDefDir i' [P.ParConstr (tri c) (map trDecl co) | (c,co) <- ps]
|
Just (ps,_) -> P.ParDefDir i' [P.ParConstr (tri c) (map trDecl co) | (c,co) <- ps]
|
||||||
May b -> P.ParDefIndir i' $ tri b
|
Nothing -> P.ParDefAbs i']]
|
||||||
_ -> P.ParDefAbs i']]
|
|
||||||
|
|
||||||
ResOverload os tysts ->
|
ResOverload os tysts ->
|
||||||
[P.DefOper [P.DDef [mkName i'] (
|
[P.DefOper [P.DDef [mkName i'] (
|
||||||
@@ -94,34 +92,23 @@ trAnyDef (i,info) = let i' = tri i in case info of
|
|||||||
(map (P.EIdent . tri) os ++
|
(map (P.EIdent . tri) os ++
|
||||||
[P.ERecord [P.LDFull [i'] (trt ty) (trt fu) | (ty,fu) <- tysts]]))]]
|
[P.ERecord [P.LDFull [i'] (trt ty) (trt fu) | (ty,fu) <- tysts]]))]]
|
||||||
|
|
||||||
CncCat (Yes ty) Nope _ ->
|
CncCat (Just ty) Nothing _ ->
|
||||||
[P.DefLincat [P.PrintDef [mkName i'] (trt ty)]]
|
[P.DefLincat [P.PrintDef [mkName i'] (trt ty)]]
|
||||||
CncCat pty ptr ppr ->
|
CncCat pty ptr ppr ->
|
||||||
[P.DefLindef [trDef i' pty ptr]] ++
|
[P.DefLindef [trDef i' pty ptr]] ++
|
||||||
[P.DefPrintCat [P.PrintDef [mkName i'] (trt pr)] | Yes pr <- [ppr]]
|
[P.DefPrintCat [P.PrintDef [mkName i'] (trt pr)] | Just pr <- [ppr]]
|
||||||
CncFun _ ptr ppr ->
|
CncFun _ ptr ppr ->
|
||||||
[P.DefLin [trDef i' nope ptr]] ++
|
[P.DefLin [trDef i' Nothing ptr]] ++
|
||||||
[P.DefPrintFun [P.PrintDef [mkName i'] (trt pr)] | Yes pr <- [ppr]]
|
[P.DefPrintFun [P.PrintDef [mkName i'] (trt pr)] | Just pr <- [ppr]]
|
||||||
{-
|
|
||||||
---- encoding of AnyInd without changing syntax. AR 20/9/2007
|
|
||||||
AnyInd s b ->
|
|
||||||
[P.DefOper [P.DDef [mkName i]
|
|
||||||
(P.EApp (P.EInt (if s then 1 else 0)) (P.EIdent (tri b)))]]
|
|
||||||
-}
|
|
||||||
_ -> []
|
_ -> []
|
||||||
|
|
||||||
|
|
||||||
trDef :: P.PIdent -> Perh Type -> Perh Term -> P.Def
|
trDef :: P.PIdent -> Maybe Type -> Maybe Term -> P.Def
|
||||||
trDef i pty ptr = case (pty,ptr) of
|
trDef i pty ptr = case (pty,ptr) of
|
||||||
(Nope, Nope) -> P.DDef [mkName i] (P.EMeta) ---
|
(Nothing, Nothing) -> P.DDef [mkName i] (P.EMeta) ---
|
||||||
(_, Nope) -> P.DDecl [mkName i] (trPerh pty)
|
(_, Nothing) -> P.DDecl [mkName i] (maybe P.EMeta trt pty)
|
||||||
(Nope, _ ) -> P.DDef [mkName i] (trPerh ptr)
|
(Nothing, _ ) -> P.DDef [mkName i] (maybe P.EMeta trt ptr)
|
||||||
(_, _ ) -> P.DFull [mkName i] (trPerh pty) (trPerh ptr)
|
(_, _ ) -> P.DFull [mkName i] (maybe P.EMeta trt pty) (maybe P.EMeta trt ptr)
|
||||||
|
|
||||||
trPerh p = case p of
|
|
||||||
Yes t -> trt t
|
|
||||||
May b -> P.EIndir $ tri b
|
|
||||||
_ -> P.EMeta ---
|
|
||||||
|
|
||||||
trFlags :: Options -> [P.TopDef]
|
trFlags :: Options -> [P.TopDef]
|
||||||
trFlags = map trFlag . optionsGFO
|
trFlags = map trFlag . optionsGFO
|
||||||
|
|||||||
@@ -107,7 +107,7 @@ transModDef x = case x of
|
|||||||
opens' <- transOpens opens
|
opens' <- transOpens opens
|
||||||
defs0 <- mapM trDef $ getTopDefs defs
|
defs0 <- mapM trDef $ getTopDefs defs
|
||||||
poss0 <- return [(i,p) | Left ds <- defs0, (i,p,_) <- ds]
|
poss0 <- return [(i,p) | Left ds <- defs0, (i,p,_) <- ds]
|
||||||
defs' <- U.buildAnyTree [(i,d) | Left ds <- defs0, (i,_,d) <- ds]
|
defs' <- U.buildAnyTree id' [(i,d) | Left ds <- defs0, (i,_,d) <- ds]
|
||||||
flags' <- return $ concatOptions [o | Right o <- defs0]
|
flags' <- return $ concatOptions [o | Right o <- defs0]
|
||||||
let poss1 = buildPosTree id' poss0
|
let poss1 = buildPosTree id' poss0
|
||||||
return (id', GM.ModInfo mtyp' mstat' flags' extends' Nothing opens' [] defs' poss1)
|
return (id', GM.ModInfo mtyp' mstat' flags' extends' Nothing opens' [] defs' poss1)
|
||||||
@@ -122,7 +122,7 @@ transModDef x = case x of
|
|||||||
opens' <- transOpens opens
|
opens' <- transOpens opens
|
||||||
defs0 <- mapM trDef $ getTopDefs defs
|
defs0 <- mapM trDef $ getTopDefs defs
|
||||||
poss0 <- return [(i,p) | Left ds <- defs0, (i,p,_) <- ds]
|
poss0 <- return [(i,p) | Left ds <- defs0, (i,p,_) <- ds]
|
||||||
defs' <- U.buildAnyTree [(i,d) | Left ds <- defs0, (i,_,d) <- ds]
|
defs' <- U.buildAnyTree id' [(i,d) | Left ds <- defs0, (i,_,d) <- ds]
|
||||||
flags' <- return $ concatOptions [o | Right o <- defs0]
|
flags' <- return $ concatOptions [o | Right o <- defs0]
|
||||||
let poss1 = buildPosTree id' poss0
|
let poss1 = buildPosTree id' poss0
|
||||||
return (id', GM.ModInfo mtyp' mstat' flags' extends' (Just (fst m',snd m',insts')) opens' [] defs' poss1)
|
return (id', GM.ModInfo mtyp' mstat' flags' extends' (Just (fst m',snd m',insts')) opens' [] defs' poss1)
|
||||||
@@ -212,23 +212,23 @@ transAbsDef x = case x of
|
|||||||
DefCat catdefs -> liftM (Left . concat) $ mapM transCatDef catdefs
|
DefCat catdefs -> liftM (Left . concat) $ mapM transCatDef catdefs
|
||||||
DefFun fundefs -> do
|
DefFun fundefs -> do
|
||||||
fundefs' <- mapM transFunDef fundefs
|
fundefs' <- mapM transFunDef fundefs
|
||||||
returnl [(fun, nopos, G.AbsFun (yes typ) nope) | (funs,typ) <- fundefs', fun <- funs]
|
returnl [(fun, nopos, G.AbsFun (Just typ) Nothing) | (funs,typ) <- fundefs', fun <- funs]
|
||||||
DefFunData fundefs -> do
|
DefFunData fundefs -> do
|
||||||
fundefs' <- mapM transFunDef fundefs
|
fundefs' <- mapM transFunDef fundefs
|
||||||
returnl $
|
returnl $
|
||||||
[(cat, nopos, G.AbsCat nope (yes [G.Cn fun])) | (funs,typ) <- fundefs',
|
[(cat, nopos, G.AbsCat Nothing (Just [G.Cn fun])) | (funs,typ) <- fundefs',
|
||||||
fun <- funs,
|
fun <- funs,
|
||||||
Ok (_,cat) <- [M.valCat typ]
|
Ok (_,cat) <- [M.valCat typ]
|
||||||
] ++
|
] ++
|
||||||
[(fun, nopos, G.AbsFun (yes typ) (yes G.EData)) | (funs,typ) <- fundefs', fun <- funs]
|
[(fun, nopos, G.AbsFun (Just typ) (Just G.EData)) | (funs,typ) <- fundefs', fun <- funs]
|
||||||
DefDef defs -> do
|
DefDef defs -> do
|
||||||
defs' <- liftM concat $ mapM getDefsGen defs
|
defs' <- liftM concat $ mapM getDefsGen defs
|
||||||
returnl [(c, nopos, G.AbsFun nope pe) | ((c,p),(_,pe)) <- defs']
|
returnl [(c, nopos, G.AbsFun Nothing pe) | ((c,p),(_,pe)) <- defs']
|
||||||
DefData ds -> do
|
DefData ds -> do
|
||||||
ds' <- mapM transDataDef ds
|
ds' <- mapM transDataDef ds
|
||||||
returnl $
|
returnl $
|
||||||
[(c, nopos, G.AbsCat nope (yes ps)) | (c,ps) <- ds'] ++
|
[(c, nopos, G.AbsCat Nothing (Just ps)) | (c,ps) <- ds'] ++
|
||||||
[(f, nopos, G.AbsFun nope (yes G.EData)) | (_,fs) <- ds', tf <- fs, f <- funs tf]
|
[(f, nopos, G.AbsFun Nothing (Just G.EData)) | (_,fs) <- ds', tf <- fs, f <- funs tf]
|
||||||
DefFlag defs -> liftM (Right . concatOptions) $ mapM transFlagDef defs
|
DefFlag defs -> liftM (Right . concatOptions) $ mapM transFlagDef defs
|
||||||
_ -> Bad $ "illegal definition in abstract module:" ++++ printTree x
|
_ -> Bad $ "illegal definition in abstract module:" ++++ printTree x
|
||||||
where
|
where
|
||||||
@@ -262,24 +262,24 @@ transCatDef x = case x of
|
|||||||
cat i pos ddecls = do
|
cat i pos ddecls = do
|
||||||
-- i <- transIdent id
|
-- i <- transIdent id
|
||||||
cont <- liftM concat $ mapM transDDecl ddecls
|
cont <- liftM concat $ mapM transDDecl ddecls
|
||||||
return (i, pos, G.AbsCat (yes cont) nope)
|
return (i, pos, G.AbsCat (Just cont) Nothing)
|
||||||
listCat id ddecls size = do
|
listCat id ddecls size = do
|
||||||
(id',pos) <- getIdentPos id
|
(id',pos) <- getIdentPos id
|
||||||
let
|
let
|
||||||
li = mkListId id'
|
li = mkListId id'
|
||||||
baseId = mkBaseId id'
|
baseId = mkBaseId id'
|
||||||
consId = mkConsId id'
|
consId = mkConsId id'
|
||||||
catd0@(c,p,G.AbsCat (Yes cont0) _) <- cat li pos ddecls
|
catd0@(c,p,G.AbsCat (Just cont0) _) <- cat li pos ddecls
|
||||||
let
|
let
|
||||||
catd = (c,pos,G.AbsCat (Yes cont0) (Yes [G.Cn baseId,G.Cn consId]))
|
catd = (c,pos,G.AbsCat (Just cont0) (Just [G.Cn baseId,G.Cn consId]))
|
||||||
cont = [(mkId x i,ty) | (i,(x,ty)) <- zip [0..] cont0]
|
cont = [(mkId x i,ty) | (i,(x,ty)) <- zip [0..] cont0]
|
||||||
xs = map (G.Vr . fst) cont
|
xs = map (G.Vr . fst) cont
|
||||||
cd = M.mkDecl (M.mkApp (G.Vr id') xs)
|
cd = M.mkDecl (M.mkApp (G.Vr id') xs)
|
||||||
lc = M.mkApp (G.Vr li) xs
|
lc = M.mkApp (G.Vr li) xs
|
||||||
niltyp = M.mkProdSimple (cont ++ genericReplicate size cd) lc
|
niltyp = M.mkProdSimple (cont ++ genericReplicate size cd) lc
|
||||||
nilfund = (baseId, nopos, G.AbsFun (yes niltyp) (yes G.EData))
|
nilfund = (baseId, nopos, G.AbsFun (Just niltyp) (Just G.EData))
|
||||||
constyp = M.mkProdSimple (cont ++ [cd, M.mkDecl lc]) lc
|
constyp = M.mkProdSimple (cont ++ [cd, M.mkDecl lc]) lc
|
||||||
consfund = (consId, nopos, G.AbsFun (yes constyp) (yes G.EData))
|
consfund = (consId, nopos, G.AbsFun (Just constyp) (Just G.EData))
|
||||||
return [catd,nilfund,consfund]
|
return [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
|
||||||
|
|
||||||
@@ -300,10 +300,10 @@ transResDef x = case x of
|
|||||||
DefPar pardefs -> do
|
DefPar pardefs -> do
|
||||||
pardefs' <- mapM transParDef pardefs
|
pardefs' <- mapM transParDef pardefs
|
||||||
returnl $ [(p, nopos, G.ResParam (if null pars
|
returnl $ [(p, nopos, G.ResParam (if null pars
|
||||||
then nope -- abstract param type
|
then Nothing -- abstract param type
|
||||||
else (yes (pars,Nothing))))
|
else (Just (pars,Nothing))))
|
||||||
| (p,pars) <- pardefs']
|
| (p,pars) <- pardefs']
|
||||||
++ [(f, nopos, G.ResValue (yes (M.mkProdSimple co (G.Cn p),Nothing))) |
|
++ [(f, nopos, G.ResValue (Just (M.mkProdSimple co (G.Cn p),Nothing))) |
|
||||||
(p,pars) <- pardefs', (f,co) <- pars]
|
(p,pars) <- pardefs', (f,co) <- pars]
|
||||||
|
|
||||||
DefOper defs -> do
|
DefOper defs -> do
|
||||||
@@ -319,7 +319,7 @@ transResDef x = case x of
|
|||||||
_ -> Bad $ "illegal definition form in resource" +++ printTree x
|
_ -> Bad $ "illegal definition form in resource" +++ printTree x
|
||||||
where
|
where
|
||||||
mkOverload op@(c,p,j) = case j of
|
mkOverload op@(c,p,j) = case j of
|
||||||
G.ResOper _ (Yes df) -> case M.appForm df of
|
G.ResOper _ (Just df) -> case M.appForm df of
|
||||||
(keyw, ts@(_:_)) | isOverloading keyw -> case last ts of
|
(keyw, ts@(_:_)) | isOverloading keyw -> case last ts of
|
||||||
G.R fs ->
|
G.R fs ->
|
||||||
[(c,p,G.ResOverload [m | G.Vr m <- ts] [(ty,fu) | (_,(Just ty,fu)) <- fs])]
|
[(c,p,G.ResOverload [m | G.Vr m <- ts] [(ty,fu) | (_,(Just ty,fu)) <- fs])]
|
||||||
@@ -327,7 +327,7 @@ transResDef x = case x of
|
|||||||
_ -> [op]
|
_ -> [op]
|
||||||
|
|
||||||
-- to enable separare type signature --- not type-checked
|
-- to enable separare type signature --- not type-checked
|
||||||
G.ResOper (Yes df) _ -> case M.appForm df of
|
G.ResOper (Just df) _ -> case M.appForm df of
|
||||||
(keyw, ts@(_:_)) | isOverloading keyw -> case last ts of
|
(keyw, ts@(_:_)) | isOverloading keyw -> case last ts of
|
||||||
G.RecType _ -> []
|
G.RecType _ -> []
|
||||||
_ -> [op]
|
_ -> [op]
|
||||||
@@ -349,27 +349,27 @@ transCncDef :: TopDef -> Err (Either [(Ident, Int, G.Info)] GO.Options)
|
|||||||
transCncDef x = case x of
|
transCncDef x = case x of
|
||||||
DefLincat defs -> do
|
DefLincat defs -> do
|
||||||
defs' <- liftM concat $ mapM transPrintDef defs
|
defs' <- liftM concat $ mapM transPrintDef defs
|
||||||
returnl [(f, nopos, G.CncCat (yes t) nope nope) | (f,t) <- defs']
|
returnl [(f, nopos, G.CncCat (Just t) Nothing Nothing) | (f,t) <- defs']
|
||||||
DefLindef defs -> do
|
DefLindef defs -> do
|
||||||
defs' <- liftM concat $ mapM getDefs defs
|
defs' <- liftM concat $ mapM getDefs defs
|
||||||
returnl [(f, p, G.CncCat pt pe nope) | ((f,p),(pt,pe)) <- defs']
|
returnl [(f, p, G.CncCat pt pe Nothing) | ((f,p),(pt,pe)) <- defs']
|
||||||
DefLin defs -> do
|
DefLin defs -> do
|
||||||
defs' <- liftM concat $ mapM getDefs defs
|
defs' <- liftM concat $ mapM getDefs defs
|
||||||
returnl [(f, p, G.CncFun Nothing pe nope) | ((f,p),(_,pe)) <- defs']
|
returnl [(f, p, G.CncFun Nothing pe Nothing) | ((f,p),(_,pe)) <- defs']
|
||||||
DefPrintCat defs -> do
|
DefPrintCat defs -> do
|
||||||
defs' <- liftM concat $ mapM transPrintDef defs
|
defs' <- liftM concat $ mapM transPrintDef defs
|
||||||
returnl [(f, nopos, G.CncCat nope nope (yes e)) | (f,e) <- defs']
|
returnl [(f, nopos, G.CncCat Nothing Nothing (Just e)) | (f,e) <- defs']
|
||||||
DefPrintFun defs -> do
|
DefPrintFun defs -> do
|
||||||
defs' <- liftM concat $ mapM transPrintDef defs
|
defs' <- liftM concat $ mapM transPrintDef defs
|
||||||
returnl [(f, nopos, G.CncFun Nothing nope (yes e)) | (f,e) <- defs']
|
returnl [(f, nopos, G.CncFun Nothing Nothing (Just e)) | (f,e) <- defs']
|
||||||
DefPrintOld defs -> do --- a guess, for backward compatibility
|
DefPrintOld defs -> do --- a guess, for backward compatibility
|
||||||
defs' <- liftM concat $ mapM transPrintDef defs
|
defs' <- liftM concat $ mapM transPrintDef defs
|
||||||
returnl [(f, nopos, G.CncFun Nothing nope (yes e)) | (f,e) <- defs']
|
returnl [(f, nopos, G.CncFun Nothing Nothing (Just e)) | (f,e) <- defs']
|
||||||
DefFlag defs -> liftM (Right . concatOptions) $ mapM transFlagDef defs
|
DefFlag defs -> liftM (Right . concatOptions) $ mapM transFlagDef defs
|
||||||
DefPattern defs -> do
|
DefPattern defs -> do
|
||||||
defs' <- liftM concat $ mapM getDefs defs
|
defs' <- liftM concat $ mapM getDefs defs
|
||||||
let defs2 = [(f, termInPattern t) | (f,(_,Yes t)) <- defs']
|
let defs2 = [(f, termInPattern t) | (f,(_,Just t)) <- defs']
|
||||||
returnl [(f, p, G.CncFun Nothing (yes t) nope) | ((f,p),t) <- defs2]
|
returnl [(f, p, G.CncFun Nothing (Just t) Nothing) | ((f,p),t) <- defs2]
|
||||||
|
|
||||||
_ -> errIn ("illegal definition in concrete syntax:") $ transResDef x
|
_ -> errIn ("illegal definition in concrete syntax:") $ transResDef x
|
||||||
|
|
||||||
@@ -379,35 +379,35 @@ transPrintDef x = case x of
|
|||||||
(ids,e) <- liftM2 (,) (mapM transName ids) (transExp exp)
|
(ids,e) <- liftM2 (,) (mapM transName ids) (transExp exp)
|
||||||
return $ [(i,e) | i <- ids]
|
return $ [(i,e) | i <- ids]
|
||||||
|
|
||||||
getDefsGen :: Def -> Err [((Ident, Int),(G.Perh G.Type, G.Perh G.Term))]
|
getDefsGen :: Def -> Err [((Ident, Int),(Maybe G.Type, Maybe G.Term))]
|
||||||
getDefsGen d = case d of
|
getDefsGen d = case d of
|
||||||
DDecl ids t -> do
|
DDecl ids t -> do
|
||||||
ids' <- mapM transNamePos ids
|
ids' <- mapM transNamePos ids
|
||||||
t' <- transExp t
|
t' <- transExp t
|
||||||
return [(i,(yes t', nope)) | i <- ids']
|
return [(i,(Just t', Nothing)) | i <- ids']
|
||||||
DDef ids e -> do
|
DDef ids e -> do
|
||||||
ids' <- mapM transNamePos ids
|
ids' <- mapM transNamePos ids
|
||||||
e' <- transExp e
|
e' <- transExp e
|
||||||
return [(i,(nope, yes e')) | i <- ids']
|
return [(i,(Nothing, Just e')) | i <- ids']
|
||||||
DFull ids t e -> do
|
DFull ids t e -> do
|
||||||
ids' <- mapM transNamePos ids
|
ids' <- mapM transNamePos ids
|
||||||
t' <- transExp t
|
t' <- transExp t
|
||||||
e' <- transExp e
|
e' <- transExp e
|
||||||
return [(i,(yes t', yes e')) | i <- ids']
|
return [(i,(Just t', Just e')) | i <- ids']
|
||||||
DPatt id patts e -> do
|
DPatt id patts e -> do
|
||||||
id' <- transNamePos id
|
id' <- transNamePos id
|
||||||
ps' <- mapM transPatt patts
|
ps' <- mapM transPatt patts
|
||||||
e' <- transExp e
|
e' <- transExp e
|
||||||
return [(id',(nope, yes (G.Eqs [(ps',e')])))]
|
return [(id',(Nothing, Just (G.Eqs [(ps',e')])))]
|
||||||
|
|
||||||
-- | sometimes you need this special case, e.g. in linearization rules
|
-- | sometimes you need this special case, e.g. in linearization rules
|
||||||
getDefs :: Def -> Err [((Ident,Int), (G.Perh G.Type, G.Perh G.Term))]
|
getDefs :: Def -> Err [((Ident,Int), (Maybe G.Type, Maybe G.Term))]
|
||||||
getDefs d = case d of
|
getDefs d = case d of
|
||||||
DPatt id patts e -> do
|
DPatt id patts e -> do
|
||||||
id' <- transNamePos id
|
id' <- transNamePos id
|
||||||
xs <- mapM tryMakeVar patts
|
xs <- mapM tryMakeVar patts
|
||||||
e' <- transExp e
|
e' <- transExp e
|
||||||
return [(id',(nope, yes (M.mkAbs xs e')))]
|
return [(id',(Nothing, Just (M.mkAbs xs e')))]
|
||||||
_ -> getDefsGen d
|
_ -> getDefsGen d
|
||||||
|
|
||||||
-- | accepts a pattern that is either a variable or a wild card
|
-- | accepts a pattern that is either a variable or a wild card
|
||||||
|
|||||||
Reference in New Issue
Block a user