From fe30e3274872db43e96ed9db467e51f12f53effb Mon Sep 17 00:00:00 2001 From: aarne Date: Thu, 6 Dec 2007 17:29:19 +0000 Subject: [PATCH] in the middle of adapting CheckGrammar --- src/GF/Devel/Compile/CheckGrammar.hs | 243 ++++++++++++-------------- src/GF/Devel/Grammar/AppPredefined.hs | 163 +++++++++++++++++ src/GF/Devel/Grammar/Lookup.hs | 18 ++ src/GF/Devel/Grammar/Macros.hs | 167 +++++++++++++++++- src/GF/Devel/Grammar/PatternMatch.hs | 153 ++++++++++++++++ 5 files changed, 610 insertions(+), 134 deletions(-) create mode 100644 src/GF/Devel/Grammar/AppPredefined.hs create mode 100644 src/GF/Devel/Grammar/PatternMatch.hs diff --git a/src/GF/Devel/Compile/CheckGrammar.hs b/src/GF/Devel/Compile/CheckGrammar.hs index 50367b85d..1c957ca71 100644 --- a/src/GF/Devel/Compile/CheckGrammar.hs +++ b/src/GF/Devel/Compile/CheckGrammar.hs @@ -34,7 +34,7 @@ import GF.Devel.Grammar.Judgements import GF.Devel.Grammar.Terms import GF.Devel.Grammar.MkJudgements import GF.Devel.Grammar.Macros -import GF.Devel.Grammar.PrGrammar +import GF.Devel.Grammar.PrGF import GF.Devel.Grammar.Lookup import GF.Infra.Ident @@ -47,8 +47,8 @@ import GF.Infra.Ident --import GF.Grammar.LookAbs --import GF.Grammar.ReservedWords ---- ---import GF.Grammar.PatternMatch ---import GF.Grammar.AppPredefined +import GF.Grammar.PatternMatch (testOvershadow) +import GF.Grammar.AppPredefined --import GF.Grammar.Lockfield (isLockLabel) import GF.Data.Operations @@ -68,14 +68,14 @@ showCheckModule mos m = do checkModule :: GF -> SourceModule -> Check SourceModule checkModule gf0 (name,mo) = checkIn ("checking module" +++ prt name) $ do - let gf = gf0 {gfmodules = Map.insert name mo (gfmodules gf0)} - checkRestrictedInheritance gf (name, mo) + let gr = gf0 {gfmodules = Map.insert name mo (gfmodules gf0)} +---- checkRestrictedInheritance gr (name, mo) mo1 <- case mtype mo of MTAbstract -> judgementOpModule (checkAbsInfo gr name) mo - MTResource -> judgementOpModule (checkResInfo gr name) mo + MTGrammar -> judgementOpModule (checkResInfo gr name) mo MTConcrete aname -> do - checkErr $ topoSortOpers $ allOperDependencies name js + checkErr $ topoSortOpers $ allOperDependencies name $ mjments mo abs <- checkErr $ lookupModule gr aname js1 <- checkCompleteGrammar abs mo judgementOpModule (checkCncInfo gr name (aname,abs)) js1 @@ -119,13 +119,13 @@ checkRestrictedInheritance mos (name,mo) = do -- | check if a term is typable -justCheckLTerm :: SourceGrammar -> Term -> Err Term +justCheckLTerm :: GF -> Term -> Err Term justCheckLTerm src t = do ((t',_),_) <- checkStart (inferLType src t) return t' -checkAbsInfo :: GF -> Ident -> (Ident,JEntry) -> Check (Ident,JEntry) -checkAbsInfo st m (c,info) = return (c,info) ---- +checkAbsInfo :: GF -> Ident -> Ident -> Judgement -> Check Judgement +checkAbsInfo st m c info = return info ---- {- checkAbsInfo st m (c,info) = do @@ -178,70 +178,62 @@ checkAbsInfo st m (c,info) = do _ -> mkApp t [a] -} -checkCompleteGrammar :: SourceAbs -> SourceCnc -> Check (BinTree Ident Info) + +checkCompleteGrammar :: Module -> Module -> Check Module checkCompleteGrammar abs cnc = do - let js = jments cnc - let fs = tree2list $ jments abs - foldM checkOne js fs + let js = mjments cnc + let fs = Map.assocs $ mjments abs + js' <- foldM checkOne js fs + return $ cnc {mjments = js'} where - checkOne js i@(c,info) = case info of - AbsFun (Yes _) _ -> case lookupIdent c js of - Ok _ -> return js + checkOne js i@(c, Left ju) = case jform ju of + JFun -> case Map.lookup c js of + Just (Left j) | jform ju == JLin -> return js _ -> do checkWarn $ "WARNING: no linearization of" +++ prt c return js - AbsCat (Yes _) _ -> case lookupIdent c js of - Ok (AnyInd _ _) -> return js - Ok (CncCat (Yes _) _ _) -> return js - Ok (CncCat _ mt mp) -> do + JCat -> case Map.lookup c js of + Just (Left j) | jform ju == JLincat -> return js + _ -> do ---- TODO: other things to check here checkWarn $ "Warning: no linearization type for" +++ prt c ++ ", inserting default {s : Str}" - return $ updateTree (c,CncCat (Yes defLinType) mt mp) js - _ -> do - checkWarn $ - "Warning: no linearization type for" +++ prt c ++ - ", inserting default {s : Str}" - return $ updateTree (c,CncCat (Yes defLinType) nope nope) js + return $ Map.insert c (cncCat defLinType) js _ -> return js --- | General Principle: only Yes-values are checked. --- A May-value has always been checked in its origin module. -checkResInfo :: SourceGrammar -> Ident -> (Ident,Info) -> Check (Ident,Info) -checkResInfo gr mo (c,info) = do - checkReservedId c - case info of - ResOper pty pde -> chIn "operation" $ do - (pty', pde') <- case (pty,pde) of - (Yes ty, Yes de) -> do - ty' <- check ty typeType >>= comp . fst - (de',_) <- check de ty' - return (Yes ty', Yes de') - (_, Yes de) -> do - (de',ty') <- infer de - return (Yes ty', Yes de') - (_,Nope) -> do - checkWarn "No definition given to oper" - return (pty,pde) - _ -> return (pty, pde) --- other cases are uninteresting - return (c, ResOper pty' pde') - +checkResInfo :: GF -> Ident -> Ident -> Judgement -> Check Judgement +checkResInfo gr mo c info = do + ---- checkReservedId c + case jform info of + JOper -> chIn "operation" $ case (jtype info, jdef info) of + (_,Meta _) -> do + checkWarn "No definition given to oper" + return info + (Meta,de) -> do + (de',ty') <- infer de + return (resOper ty' de') + (ty, de) -> do + ty' <- check ty typeType >>= comp . fst + (de',_) <- check de ty' + return (resOper ty' de') +{- ---- ResOverload tysts -> chIn "overloading" $ do tysts' <- mapM (uncurry $ flip check) tysts let tysts2 = [(y,x) | (x,y) <- tysts'] --- this can only be a partial guarantee, since matching --- with value type is only possible if expected type is given checkUniq $ - sort [t : map snd xs | (x,_) <- tysts2, Ok (xs,t) <- [typeFormCnc x]] + sort [t : map snd xs | (x,_) <- tysts2, let (xs,t) = prodForm x] return (c,ResOverload tysts2) - +-} +{- ---- ResParam (Yes (pcs,_)) -> chIn "parameter type" $ do ---- mapM ((mapM (computeLType gr . snd)) . snd) pcs mapM_ ((mapM_ (checkIfParType gr . snd)) . snd) pcs ts <- checkErr $ lookupParamValues gr mo c return (c,ResParam (Yes (pcs, Just ts))) - - _ -> return (c,info) +-} + _ -> return info where infer = inferLType gr check = checkLType gr @@ -256,34 +248,37 @@ checkResInfo gr mo (c,info) = do _ -> return () -checkCncInfo :: SourceGrammar -> Ident -> (Ident,SourceAbs) -> - (Ident,Info) -> Check (Ident,Info) -checkCncInfo gr m (a,abs) (c,info) = do - checkReservedId c - case info of - - CncFun _ (Yes trm) mpr -> chIn "linearization of" $ do - typ <- checkErr $ lookupFunTypeSrc gr a c +checkCncInfo :: GF -> Ident -> SourceModule -> + Ident -> Judgement -> Check Judgement +checkCncInfo gr cnc (a,abs) c info = do + ---- checkReservedId c + case jform info of + JFun -> chIn "linearization of" $ do + typ <- checkErr $ lookupFunType gr a c cat0 <- checkErr $ valCat typ - (cont,val) <- linTypeOfType gr m typ -- creates arg vars - (trm',_) <- check trm (mkFunType (map snd cont) val) -- erases arg vars - checkPrintname gr mpr + (cont,val) <- linTypeOfType gr cnc typ -- creates arg vars + let lintyp = mkFunType (map snd cont) val + (trm',_) <- check (jdef info) lintyp -- erases arg vars + checkPrintname gr (jprintname info) cat <- return $ snd cat0 - return (c, CncFun (Just (cat,(cont,val))) (Yes trm') mpr) + return (info {jdef = trm'}) + ---- return (c, CncFun (Just (cat,(cont,val))) (Yes trm') mpr) -- cat for cf, typ for pe - CncCat (Yes typ) mdef mpr -> chIn "linearization type of" $ do - checkErr $ lookupCatContextSrc gr a c - typ' <- checkIfLinType gr typ + JCat (Yes typ) mdef mpr -> chIn "linearization type of" $ do + checkErr $ lookupCatContext gr a c + typ' <- checkIfLinType gr (jtype info) + {- ---- mdef' <- case mdef of Yes def -> do (def',_) <- checkLType gr def (mkFunType [typeStr] typ) return $ Yes def' _ -> return mdef - checkPrintname gr mpr - return (c,CncCat (Yes typ') mdef' mpr) + -} + checkPrintname gr (jprintname info) + return (info {jtype = typ'}) - _ -> checkResInfo gr m (c,info) + _ -> checkResInfo gr cnc c info where env = gr @@ -292,7 +287,8 @@ checkCncInfo gr m (a,abs) (c,info) = do check = checkLType gr chIn cat = checkIn ("Happened in" +++ cat +++ prt c +++ ":") -checkIfParType :: SourceGrammar -> Type -> Check () + +checkIfParType :: GF -> Type -> Check () checkIfParType st typ = checkCond ("Not parameter type" +++ prt typ) (isParType typ) where isParType ty = True ---- @@ -308,6 +304,7 @@ checkIfParType st typ = checkCond ("Not parameter type" +++ prt typ) (isParType _ -> False -} +{- ---- checkIfStrType :: SourceGrammar -> Type -> Check () checkIfStrType st typ = case typ of Table arg val -> do @@ -315,26 +312,17 @@ checkIfStrType st typ = case typ of checkIfStrType st val _ | typ == typeStr -> return () _ -> prtFail "not a string type" typ +-} - -checkIfLinType :: SourceGrammar -> Type -> Check Type +checkIfLinType :: GF -> Type -> Check Type checkIfLinType st typ0 = do typ <- computeLType st typ0 case typ of - RecType r -> do - let (lins,ihs) = partition (isLinLabel .fst) r - --- checkErr $ checkUnique $ map fst r - mapM_ checkInh ihs - mapM_ checkLin lins + RecType r -> return () _ -> prtFail "a linearization type must be a record type instead of" typ return typ - where - checkInh (label,typ) = checkIfParType st typ - checkLin (label,typ) = return () ---- checkIfStrType st typ - - -computeLType :: SourceGrammar -> Type -> Check Type +computeLType :: GF -> Type -> Check Type computeLType gr t = do g0 <- checkGetContext let g = [(x, Vr x) | (x,_) <- g0] @@ -348,15 +336,15 @@ computeLType gr t = do Q (IC "Predef") (IC "Error") -> return ty ---- shouldn't be needed Q m c | elem c [cPredef,cPredefAbs] -> return ty - Q m c | elem c [zIdent "Int"] -> + Q m c | elem c [identC "Int"] -> return $ defLinType ---- let ints k = App (Q (IC "Predef") (IC "Ints")) (EInt k) in ---- RecType [ ---- (LIdent "last",ints 9),(LIdent "s", typeStr), (LIdent "size",ints 1)] - Q m c | elem c [zIdent "Float",zIdent "String"] -> return defLinType ---- + Q m c | elem c [identC "Float",identC "String"] -> return defLinType ---- Q m ident -> checkIn ("module" +++ prt m) $ do - ty' <- checkErr (lookupResDef gr m ident) + ty' <- checkErr (lookupOperDef gr m ident) if ty' == ty then return ty else comp ty' --- is this necessary to test? Vr ident -> checkLookup ident -- never needed to compute! @@ -388,41 +376,43 @@ computeLType gr t = do let fs' = sortBy (\x y -> compare (fst x) (fst y)) fs liftM RecType $ mapPairsM comp fs' - _ | ty == typeTok -> return typeStr - _ | isPredefConstant ty -> return ty +---- _ | ty == typeStr -> return typeStr +---- _ | isPredefConstant ty -> return ty _ -> composOp comp ty -checkPrintname :: SourceGrammar -> Perh Term -> Check () -checkPrintname st (Yes t) = checkLType st t typeStr >> return () +checkPrintname :: GF -> Term -> Check () +---- checkPrintname st (Yes t) = checkLType st t typeStr >> return () checkPrintname _ _ = return () +{- ---- -- | for grammars obtained otherwise than by parsing ---- update!! checkReservedId :: Ident -> Check () checkReservedId x = let c = prt x in if isResWord c then checkWarn ("Warning: reserved word used as identifier:" +++ c) else return () +-} -- to normalize records and record types labelIndex :: Type -> Label -> Int labelIndex ty lab = case ty of - RecType ts -> maybe (error ("label index" +++ prt lab)) id $ lookup lab $ labs ts + RecType ts -> maybe (error ("label index"+++ prt lab)) id $ lookup lab $ labs ts _ -> error $ "label index" +++ prt ty where labs ts = zip (map fst (sortBy (\ x y -> compare (fst x) (fst y)) ts)) [0..] -- the underlying algorithms -inferLType :: SourceGrammar -> Term -> Check (Term, Type) +inferLType :: GF -> Term -> Check (Term, Type) inferLType gr trm = case trm of Q m ident | isPredef m -> termWith trm $ checkErr (typPredefined ident) Q m ident -> checks [ - termWith trm $ checkErr (lookupResType gr m ident) >>= comp + termWith trm $ checkErr (lookupOperType gr m ident) >>= comp , - checkErr (lookupResDef gr m ident) >>= infer + checkErr (lookupOperDef gr m ident) >>= infer , {- do @@ -438,9 +428,9 @@ inferLType gr trm = case trm of QC m ident | isPredef m -> termWith trm $ checkErr (typPredefined ident) QC m ident -> checks [ - termWith trm $ checkErr (lookupResType gr m ident) >>= comp + termWith trm $ checkErr (lookupOperType gr m ident) >>= comp , - checkErr (lookupResDef gr m ident) >>= infer + checkErr (lookupOperDef gr m ident) >>= infer , prtFail "cannot infer type of canonical constant" trm ] @@ -532,23 +522,20 @@ inferLType gr trm = case trm of check2 (flip justCheck typeStr) C s1 s2 typeStr Glue s1 s2 -> - check2 (flip justCheck typeStr) Glue s1 s2 typeStr ---- typeTok + check2 (flip justCheck typeStr) Glue s1 s2 typeStr ---- hack from Rename.identRenameTerm, to live with files with naming conflicts 18/6/2007 - Strs (Cn (IC "#conflict") : ts) -> do - trace ("WARNING: unresolved constant, could be any of" +++ unwords (map prt ts)) (infer $ head ts) +---- Strs (Cn (IC "#conflict") : ts) -> do +---- trace ("WARNING: unresolved constant, could be any of" +++ unwords (map prt ts)) (infer $ head ts) -- checkWarn ("WARNING: unresolved constant, could be any of" +++ unwords (map prt ts)) -- infer $ head ts - Strs ts -> do - ts' <- mapM (\t -> justCheck t typeStr) ts - return (Strs ts', typeStrs) Alts (t,aa) -> do t' <- justCheck t typeStr aa' <- flip mapM aa (\ (c,v) -> do c' <- justCheck c typeStr - v' <- justCheck v typeStrs + v' <- justCheck v typeStr return (c',v')) return (Alts (t',aa'), typeStr) @@ -633,7 +620,7 @@ inferLType gr trm = case trm of _ -> False inferPatt p = case p of - PP q c ps | q /= cPredef -> checkErr $ lookupResType gr q c >>= valTypeCnc + PP q c ps | q /= cPredef -> checkErr $ lookupOperType gr q c >>= snd . prodForm PAs _ p -> inferPatt p PNeg p -> inferPatt p PAlt p q -> checks [inferPatt p, inferPatt q] @@ -644,9 +631,9 @@ inferLType gr trm = case trm of -- type inference: Nothing, type checking: Just t -- the latter permits matching with value type -getOverload :: SourceGrammar -> Maybe Type -> Term -> Check (Maybe (Term,Type)) +getOverload :: GF -> Maybe Type -> Term -> Check (Maybe (Term,Type)) getOverload env@gr mt t = case appForm t of - (f@(Q m c), ts) -> case lookupOverload gr m c of + (f@(Q m c), ts) -> case (return []) of ---- lookupOverload gr m c of Ok typs -> do ttys <- mapM infer ts v <- matchOverload f typs ttys @@ -682,7 +669,7 @@ getOverload env@gr mt t = case appForm t of matchVal mt v = elem mt ([Nothing,Just v] ++ unlocked) where unlocked = case v of - RecType fs -> [Just $ RecType $ filter (not . isLockLabel . fst) fs] + RecType fs -> [Just $ RecType $ fs] ---- filter (not . isLockLabel . fst) fs] _ -> [] ---- TODO: accept subtypes ---- TODO: use a trie @@ -698,7 +685,7 @@ getOverload env@gr mt t = case appForm t of Prod _ _ _ -> False _ -> True -checkLType :: SourceGrammar -> Term -> Type -> Check (Term, Type) +checkLType :: GF -> Term -> Type -> Check (Term, Type) checkLType env trm typ0 = do typ <- comp typ0 @@ -862,8 +849,8 @@ pattContext :: LTEnv -> Type -> Patt -> Check Context pattContext env typ p = case p of PV x | not (isWildIdent x) -> return [(x,typ)] PP q c ps | q /= cPredef -> do ---- why this /=? AR 6/1/2006 - t <- checkErr $ lookupResType cnc q c - (cont,v) <- checkErr $ typeFormCnc t + t <- checkErr $ lookupOperType cnc q c + let (cont,v) = prodForm t checkCond ("wrong number of arguments for constructor in" +++ prt p) (length cont == length ps) checkEqLType env typ v (patt2term p) @@ -912,7 +899,7 @@ pattContext env typ p = case p of -- auxiliaries -type LTEnv = SourceGrammar +type LTEnv = GF termWith :: Term -> Check Type -> Check (Term, Type) termWith t ct = do @@ -1007,7 +994,7 @@ checkIfEqLType env t u trm = do let ls = [l | (l,a) <- rs, not (any (\ (k,b) -> alpha g a b && l == k) ts)] - (locks,others) = partition isLockLabel ls + (locks,others) = partition (const False) ls ---- isLockLabel ls in case others of _:_ -> Bad $ "missing record fields" +++ unwords (map prt others) _ -> return locks @@ -1019,15 +1006,19 @@ checkIfEqLType env t u trm = do _ -> Bad "" - sTypes = [typeStr, typeTok, typeString] + ---- to revise + allExtendsPlus _ n = [n] + + sTypes = [typeStr, typeString] comp = computeLType env -- printing a type with a lock field lock_C as C prtType :: LTEnv -> Type -> String prtType env ty = case ty of - RecType fs -> case filter isLockLabel $ map fst fs of - [lock] -> (drop 5 $ prt lock) --- ++++ "Full form" +++ prt ty - _ -> prtt ty + RecType fs -> ---- case filter isLockLabel $ map fst fs of + ---- [lock] -> (drop 5 $ prt lock) --- ++++ "Full form" +++ prt ty + ---- _ -> + prtt ty Prod x a b -> prtType env a +++ "->" +++ prtType env b _ -> prtt ty where @@ -1036,7 +1027,7 @@ prtType env ty = case ty of -- | linearization types and defaults -linTypeOfType :: SourceGrammar -> Ident -> Type -> Check (Context,Type) +linTypeOfType :: GF -> Ident -> Type -> Check (Context,Type) linTypeOfType cnc m typ = do (cont,cat) <- checkErr $ typeSkeleton typ val <- lookLin cat @@ -1057,10 +1048,10 @@ linTypeOfType cnc m typ = do -- | dependency check, detecting circularities and returning topo-sorted list -allOperDependencies :: Ident -> BinTree Ident Info -> [(Ident,[Ident])] +allOperDependencies :: Ident -> Map.Map Ident JEntry -> [(Ident,[Ident])] allOperDependencies m = allDependencies (==m) -allDependencies :: (Ident -> Bool) -> BinTree Ident Info -> [(Ident,[Ident])] +allDependencies :: (Ident -> Bool) -> Map.Map Ident JEntry -> [(Ident,[Ident])] allDependencies ism b = [(f, nub (concatMap opty (pts i))) | (f,i) <- tree2list b] where @@ -1070,15 +1061,9 @@ allDependencies ism b = _ -> collectOp opersIn t opty (Yes ty) = opersIn ty opty _ = [] - pts i = case i of - ResOper pty pt -> [pty,pt] - ResParam (Yes (ps,_)) -> [Yes t | (_,cont) <- ps, (_,t) <- cont] - CncCat pty _ _ -> [pty] - CncFun _ pt _ -> [pt] ---- (Maybe (Ident,(Context,Type)) - AbsFun pty ptr -> [pty] --- ptr is def, which can be mutual - AbsCat (Yes co) _ -> [Yes ty | (_,ty) <- co] - _ -> [] - + pts i = [jtype i, jdef i] + ---- AbsFun pty ptr -> [pty] --- ptr is def, which can be mutual + topoSortOpers :: [(Ident,[Ident])] -> Err [Ident] topoSortOpers st = do let eops = topoTest st diff --git a/src/GF/Devel/Grammar/AppPredefined.hs b/src/GF/Devel/Grammar/AppPredefined.hs new file mode 100644 index 000000000..6ff538148 --- /dev/null +++ b/src/GF/Devel/Grammar/AppPredefined.hs @@ -0,0 +1,163 @@ +---------------------------------------------------------------------- +-- | +-- Module : AppPredefined +-- Maintainer : AR +-- Stability : (stable) +-- Portability : (portable) +-- +-- > CVS $Date: 2005/10/06 14:21:34 $ +-- > CVS $Author: aarne $ +-- > CVS $Revision: 1.13 $ +-- +-- Predefined function type signatures and definitions. +----------------------------------------------------------------------------- + +module GF.Devel.Grammar.AppPredefined ( + isInPredefined, + typPredefined, + appPredefined + ) where + +import GF.Devel.Grammar.Terms +import GF.Devel.Grammar.Macros +import GF.Grammar.PrGF (prt,prt_,prtBad) +import GF.Infra.Ident + +import GF.Data.Operations + + +-- predefined function type signatures and definitions. AR 12/3/2003. + +isInPredefined :: Ident -> Bool +isInPredefined = err (const True) (const False) . typPredefined + +typPredefined :: Ident -> Err Type +typPredefined c@(IC f) = case f of + "Int" -> return typePType + "Float" -> return typePType + "Error" -> return typeType + "Ints" -> return $ mkFunType [cnPredef "Int"] typePType + "PBool" -> return typePType + "error" -> return $ mkFunType [typeStr] (cnPredef "Error") -- non-can. of empty set + "PFalse" -> return $ cnPredef "PBool" + "PTrue" -> return $ cnPredef "PBool" + "dp" -> return $ mkFunType [cnPredef "Int",typeTok] typeTok + "drop" -> return $ mkFunType [cnPredef "Int",typeTok] typeTok + "eqInt" -> return $ mkFunType [cnPredef "Int",cnPredef "Int"] (cnPredef "PBool") + "lessInt"-> return $ mkFunType [cnPredef "Int",cnPredef "Int"] (cnPredef "PBool") + "eqStr" -> return $ mkFunType [typeTok,typeTok] (cnPredef "PBool") + "length" -> return $ mkFunType [typeTok] (cnPredef "Int") + "occur" -> return $ mkFunType [typeTok,typeTok] (cnPredef "PBool") + "occurs" -> return $ mkFunType [typeTok,typeTok] (cnPredef "PBool") + "plus" -> return $ mkFunType [cnPredef "Int",cnPredef "Int"] (cnPredef "Int") +---- "read" -> (P : Type) -> Tok -> P + "show" -> return $ mkProd -- (P : PType) -> P -> Tok + ([(zIdent "P",typePType),(wildIdent,Vr (zIdent "P"))],typeStr,[]) + "toStr" -> return $ mkProd -- (L : Type) -> L -> Str + ([(zIdent "L",typeType),(wildIdent,Vr (zIdent "L"))],typeStr,[]) + "mapStr" -> + let ty = zIdent "L" in + return $ mkProd -- (L : Type) -> (Str -> Str) -> L -> L + ([(ty,typeType),(wildIdent,mkFunType [typeStr] typeStr),(wildIdent,Vr ty)],Vr ty,[]) + "take" -> return $ mkFunType [cnPredef "Int",typeTok] typeTok + "tk" -> return $ mkFunType [cnPredef "Int",typeTok] typeTok + _ -> prtBad "unknown in Predef:" c +typPredefined c = prtBad "unknown in Predef:" c + +appPredefined :: Term -> Err (Term,Bool) +appPredefined t = case t of + + App f x0 -> do + (x,_) <- appPredefined x0 + case f of + -- one-place functions + Q (IC "Predef") (IC f) -> case (f, x) of + ("length", K s) -> retb $ EInt $ toInteger $ length s + _ -> retb t ---- prtBad "cannot compute predefined" t + + -- two-place functions + App (Q (IC "Predef") (IC f)) z0 -> do + (z,_) <- appPredefined z0 + case (f, norm z, norm x) of + ("drop", EInt i, K s) -> retb $ K (drop (fi i) s) + ("take", EInt i, K s) -> retb $ K (take (fi i) s) + ("tk", EInt i, K s) -> retb $ K (take (max 0 (length s - fi i)) s) + ("dp", EInt i, K s) -> retb $ K (drop (max 0 (length s - fi i)) s) + ("eqStr",K s, K t) -> retb $ if s == t then predefTrue else predefFalse + ("occur",K s, K t) -> retb $ if substring s t then predefTrue else predefFalse + ("occurs",K s, K t) -> retb $ if any (flip elem t) s then predefTrue else predefFalse + ("eqInt",EInt i, EInt j) -> retb $ if i==j then predefTrue else predefFalse + ("lessInt",EInt i, EInt j) -> retb $ if i retb $ EInt $ i+j + ("show", _, t) -> retb $ foldr C Empty $ map K $ words $ prt t + ("read", _, K s) -> retb $ str2tag s --- because of K, only works for atomic tags + ("toStr", _, t) -> trm2str t >>= retb + + _ -> retb t ---- prtBad "cannot compute predefined" t + + -- three-place functions + App (App (Q (IC "Predef") (IC f)) z0) y0 -> do + (y,_) <- appPredefined y0 + (z,_) <- appPredefined z0 + case (f, z, y, x) of + ("mapStr",ty,op,t) -> retf $ mapStr ty op t + _ -> retb t ---- prtBad "cannot compute predefined" t + + _ -> retb t ---- prtBad "cannot compute predefined" t + _ -> retb t + ---- should really check the absence of arg variables + where + retb t = return (t,True) -- no further computing needed + retf t = return (t,False) -- must be computed further + norm t = case t of + Empty -> K [] + _ -> t + fi = fromInteger + +-- read makes variables into constants + +str2tag :: String -> Term +str2tag s = case s of +---- '\'' : cs -> mkCn $ pTrm $ init cs + _ -> Cn $ IC s --- + where + mkCn t = case t of + Vr i -> Cn i + App c a -> App (mkCn c) (mkCn a) + _ -> t + + +predefTrue = Q (IC "Predef") (IC "PTrue") +predefFalse = Q (IC "Predef") (IC "PFalse") + +substring :: String -> String -> Bool +substring s t = case (s,t) of + (c:cs, d:ds) -> (c == d && substring cs ds) || substring s ds + ([],_) -> True + _ -> False + +trm2str :: Term -> Err Term +trm2str t = case t of + R ((_,(_,s)):_) -> trm2str s + T _ ((_,s):_) -> trm2str s + TSh _ ((_,s):_) -> trm2str s + V _ (s:_) -> trm2str s + C _ _ -> return $ t + K _ -> return $ t + S c _ -> trm2str c + Empty -> return $ t + _ -> prtBad "cannot get Str from term" t + +-- simultaneous recursion on type and term: type arg is essential! +-- But simplify the task by assuming records are type-annotated +-- (this has been done in type checking) +mapStr :: Type -> Term -> Term -> Term +mapStr ty f t = case (ty,t) of + _ | elem ty [typeStr,typeTok] -> App f t + (_, R ts) -> R [(l,mapField v) | (l,v) <- ts] + (Table a b,T ti cs) -> T ti [(p,mapStr b f v) | (p,v) <- cs] + _ -> t + where + mapField (mty,te) = case mty of + Just ty -> (mty,mapStr ty f te) + _ -> (mty,te) diff --git a/src/GF/Devel/Grammar/Lookup.hs b/src/GF/Devel/Grammar/Lookup.hs index cb45b5406..3980577df 100644 --- a/src/GF/Devel/Grammar/Lookup.hs +++ b/src/GF/Devel/Grammar/Lookup.hs @@ -4,11 +4,13 @@ import GF.Devel.Grammar.Modules import GF.Devel.Grammar.Judgements import GF.Devel.Grammar.Macros import GF.Devel.Grammar.Terms +import GF.Devel.Grammar.PrGF import GF.Infra.Ident import GF.Data.Operations import Data.Map +import Data.List (sortBy) ---- -- look up fields for a constant in a grammar @@ -57,6 +59,22 @@ lookupParamValues gf m c = do V _ ts -> return ts _ -> raise "no parameter values" +allParamValues :: GF -> Type -> Err [Term] +allParamValues cnc ptyp = case ptyp of + App (Q (IC "Predef") (IC "Ints")) (EInt n) -> + return [EInt i | i <- [0..n]] + QC p c -> lookupParamValues cnc p c + Q p c -> lookupParamValues cnc p c ---- + RecType r -> do + let (ls,tys) = unzip $ sortByFst r + tss <- mapM allPV tys + return [R (zipAssign ls ts) | ts <- combinations tss] + _ -> prtBad "cannot find parameter values for" ptyp + where + allPV = allParamValues cnc + -- to normalize records and record types + sortByFst = sortBy (\ x y -> compare (fst x) (fst y)) + -- infrastructure for lookup lookupModule :: GF -> Ident -> Err Module diff --git a/src/GF/Devel/Grammar/Macros.hs b/src/GF/Devel/Grammar/Macros.hs index 1b4ed1448..659ddb107 100644 --- a/src/GF/Devel/Grammar/Macros.hs +++ b/src/GF/Devel/Grammar/Macros.hs @@ -7,9 +7,12 @@ import GF.Infra.Ident import GF.Data.Operations -import Data.Map +import qualified Data.Map as Map import Control.Monad (liftM,liftM2) + +-- analyse types and terms + contextOfType :: Type -> Context contextOfType ty = co where (co,_,_) = typeForm ty @@ -30,9 +33,48 @@ appForm tr = (f,reverse xs) where App f a -> (f2,a:a2) where (f2,a2) = appForm f _ -> (t,[]) +valCat :: Type -> Err (Ident,Ident) +valCat typ = case typeForm typ of + (_,Q m c,_) -> return (m,c) + +typeRawSkeleton :: Type -> Err ([(Int,Type)],Type) +typeRawSkeleton typ = do + let (cont,typ) = prodForm typ + args <- mapM (typeRawSkeleton . snd) cont + return ([(length c, v) | (c,v) <- args], typ) + +type MCat = (Ident,Ident) + +sortMCat :: String -> MCat +sortMCat s = (identC "_", identC s) + +--- hack for Editing.actCat in empty state +errorCat :: MCat +errorCat = (identC "?", identC "?") + +getMCat :: Term -> Err MCat +getMCat t = case t of + Q m c -> return (m,c) + QC m c -> return (m,c) + Sort s -> return $ sortMCat s + App f _ -> getMCat f + _ -> error $ "no qualified constant" +++ show t + +typeSkeleton :: Type -> Err ([(Int,MCat)],MCat) +typeSkeleton typ = do + (cont,val) <- typeRawSkeleton typ + cont' <- mapPairsM getMCat cont + val' <- getMCat val + return (cont',val') + +-- construct types and terms + mkProd :: Context -> Type -> Type mkProd = flip (foldr (uncurry Prod)) +mkFunType :: [Type] -> Type -> Type +mkFunType tt t = mkProd ([(wildIdent, ty) | ty <- tt]) t -- nondep prod + mkApp :: Term -> [Term] -> Term mkApp = foldl App @@ -43,6 +85,12 @@ mkCTable :: [Ident] -> Term -> Term mkCTable ids v = foldr ccase v ids where ccase x t = T TRaw [(PV x,t)] +appCons :: Ident -> [Term] -> Term +appCons = mkApp . Con + +appc :: String -> [Term] -> Term +appc = appCons . identC + tuple2record :: [Term] -> [Assign] tuple2record ts = [assign (tupleLabel i) t | (i,t) <- zip [1..] ts] @@ -67,9 +115,74 @@ mkDecl typ = (wildIdent, typ) mkLet :: [LocalDef] -> Term -> Term mkLet defs t = foldr Let t defs +mkRecTypeN :: Int -> (Int -> Label) -> [Type] -> Type +mkRecTypeN int lab typs = RecType [ (lab i, t) | (i,t) <- zip [int..] typs] + +mkRecType :: (Int -> Label) -> [Type] -> Type +mkRecType = mkRecTypeN 0 + +plusRecType :: Type -> Type -> Err Type +plusRecType t1 t2 = case (t1, t2) of + (RecType r1, RecType r2) -> case + filter (`elem` (map fst r1)) (map fst r2) of + [] -> return (RecType (r1 ++ r2)) + ls -> Bad $ "clashing labels" +++ unwords (map show ls) + _ -> Bad ("cannot add record types" +++ show t1 +++ "and" +++ show t2) + +plusRecord :: Term -> Term -> Err Term +plusRecord t1 t2 = + case (t1,t2) of + (R r1, R r2 ) -> return (R ([(l,v) | -- overshadowing of old fields + (l,v) <- r1, not (elem l (map fst r2)) ] ++ r2)) + (_, FV rs) -> mapM (plusRecord t1) rs >>= return . FV + (FV rs,_ ) -> mapM (`plusRecord` t2) rs >>= return . FV + _ -> Bad ("cannot add records" +++ show t1 +++ "and" +++ show t2) + +zipAssign :: [Label] -> [Term] -> [Assign] +zipAssign ls ts = [assign l t | (l,t) <- zip ls ts] + +-- type constants + typeType :: Type typeType = Sort "Type" +typePType :: Type +typePType = Sort "PType" + +typeStr :: Type +typeStr = Sort "Str" + +cPredef :: Ident +cPredef = identC "Predef" + +cPredefAbs :: Ident +cPredefAbs = identC "PredefAbs" + +typeString, typeFloat, typeInt :: Term +typeInts :: Integer -> Term + +typeString = constPredefRes "String" +typeInt = constPredefRes "Int" +typeFloat = constPredefRes "Float" +typeInts i = App (constPredefRes "Ints") (EInt i) + +isTypeInts :: Term -> Bool +isTypeInts ty = case ty of + App c _ -> c == constPredefRes "Ints" + _ -> False + +constPredefRes :: String -> Term +constPredefRes s = Q (IC "Predef") (identC s) + +isPredefConstant :: Term -> Bool +isPredefConstant t = case t of + Q (IC "Predef") _ -> True + Q (IC "PredefAbs") _ -> True + _ -> False + +defLinType :: Type +defLinType = RecType [(LIdent "s", typeStr)] + meta0 :: Term meta0 = Meta 0 @@ -93,12 +206,14 @@ termOpGF f g = do termOpModule :: Monad m => (Term -> m Term) -> Module -> m Module termOpModule f = judgementOpModule fj where - fj = either (liftM Left . termOpJudgement f) (return . Right) + fj = termOpJudgement f judgementOpModule :: Monad m => (Judgement -> m Judgement) -> Module -> m Module judgementOpModule f m = do - mjs <- mapMapM f (mjments m) + mjs <- mapMapM fj (mjments m) return m {mjments = mjs} + where + fj = either (liftM Left . f) (return . Right) termOpJudgement :: Monad m => (Term -> m Term) -> Judgement -> m Judgement termOpJudgement f j = do @@ -194,6 +309,28 @@ composOp co trm = case trm of _ -> return trm -- covers K, Vr, Cn, Sort + +---- should redefine using composOp +collectOp :: (Term -> [a]) -> Term -> [a] +collectOp co trm = case trm of + App c a -> co c ++ co a + Abs _ b -> co b + Prod _ a b -> co a ++ co b + S c a -> co c ++ co a + Table a c -> co a ++ co c + ExtR a c -> co a ++ co c + R r -> concatMap (\ (_,(mt,a)) -> maybe [] co mt ++ co a) r + RecType r -> concatMap (co . snd) r + P t i -> co t + T _ cc -> concatMap (co . snd) cc -- not from patterns --- nor from type annot + V _ cc -> concatMap co cc --- nor from type annot + Let (x,(mt,a)) b -> maybe [] co mt ++ co a ++ co b + C s1 s2 -> co s1 ++ co s2 + Glue s1 s2 -> co s1 ++ co s2 + Alts (t,aa) -> let (x,y) = unzip aa in co t ++ concatMap co (x ++ y) + FV ts -> concatMap co ts + _ -> [] -- covers K, Vr, Cn, Sort, Ready + --- just aux to composOp? mapAssignM :: Monad m => (Term -> m c) -> [Assign] -> m [(Label,(Maybe c,c))] @@ -207,9 +344,29 @@ changeTableType co i = case i of TWild ty -> co ty >>= return . TWild _ -> return i + +patt2term :: Patt -> Term +patt2term pt = case pt of + PV x -> Vr x + PW -> Vr wildIdent --- not parsable, should not occur + PC c pp -> mkApp (Con c) (map patt2term pp) + PP p c pp -> mkApp (QC p c) (map patt2term pp) + PR r -> R [assign l (patt2term p) | (l,p) <- r] + PT _ p -> patt2term p + PInt i -> EInt i + PFloat i -> EFloat i + PString s -> K s + + PAs x p -> appc "@" [Vr x, patt2term p] --- an encoding + PSeq a b -> appc "+" [(patt2term a), (patt2term b)] --- an encoding + PAlt a b -> appc "|" [(patt2term a), (patt2term b)] --- an encoding + PRep a -> appc "*" [(patt2term a)] --- an encoding + PNeg a -> appc "-" [(patt2term a)] --- an encoding + + ---- given in lib? -mapMapM :: (Monad m, Ord k) => (v -> m v) -> Map k v -> m (Map k v) +mapMapM :: (Monad m, Ord k) => (v -> m v) -> Map.Map k v -> m (Map.Map k v) mapMapM f = - liftM fromAscList . mapM (\ (x,y) -> liftM ((,) x) $ f y) . assocs + liftM Map.fromAscList . mapM (\ (x,y) -> liftM ((,) x) $ f y) . Map.assocs diff --git a/src/GF/Devel/Grammar/PatternMatch.hs b/src/GF/Devel/Grammar/PatternMatch.hs new file mode 100644 index 000000000..38c20fa98 --- /dev/null +++ b/src/GF/Devel/Grammar/PatternMatch.hs @@ -0,0 +1,153 @@ +---------------------------------------------------------------------- +-- | +-- Module : PatternMatch +-- Maintainer : AR +-- Stability : (stable) +-- Portability : (portable) +-- +-- > CVS $Date: 2005/10/12 12:38:29 $ +-- > CVS $Author: aarne $ +-- > CVS $Revision: 1.7 $ +-- +-- pattern matching for both concrete and abstract syntax. AR -- 16\/6\/2003 +----------------------------------------------------------------------------- + +module GF.Devel.Grammar.PatternMatch (matchPattern, + testOvershadow, + findMatch + ) where + + +import GF.Grammar.Terms +import GF.Grammar.Macros +import GF.Grammar.PrGF +import GF.Infra.Ident + +import GF.Data.Operations + +import Data.List +import Control.Monad + + +matchPattern :: [(Patt,Term)] -> Term -> Err (Term, Substitution) +matchPattern pts term = + if not (isInConstantForm term) + then prtBad "variables occur in" term + else + errIn ("trying patterns" +++ unwords (intersperse "," (map (prt . fst) pts))) $ + findMatch [([p],t) | (p,t) <- pts] [term] + +testOvershadow :: [Patt] -> [Term] -> Err [Patt] +testOvershadow pts vs = do + let numpts = zip pts [0..] + let cases = [(p,EInt i) | (p,i) <- numpts] + ts <- mapM (liftM fst . matchPattern cases) vs + return $ [p | (p,i) <- numpts, notElem i [i | EInt i <- ts] ] + +findMatch :: [([Patt],Term)] -> [Term] -> Err (Term, Substitution) +findMatch cases terms = case cases of + [] -> Bad $"no applicable case for" +++ unwords (intersperse "," (map prt terms)) + (patts,_):_ | length patts /= length terms -> + Bad ("wrong number of args for patterns :" +++ + unwords (map prt patts) +++ "cannot take" +++ unwords (map prt terms)) + (patts,val):cc -> case mapM tryMatch (zip patts terms) of + Ok substs -> return (val, concat substs) + _ -> findMatch cc terms + +tryMatch :: (Patt, Term) -> Err [(Ident, Term)] +tryMatch (p,t) = do + t' <- termForm t + trym p t' + where + isInConstantFormt = True -- tested already + trym p t' = + case (p,t') of + (PVal _ i, (_,Val _ j,_)) + | i == j -> return [] + | otherwise -> Bad $ "no match of values" + (_,(x,Empty,y)) -> trym p (x,K [],y) -- because "" = [""] = [] + (PV IW, _) | isInConstantFormt -> return [] -- optimization with wildcard + (PV x, _) | isInConstantFormt -> return [(x,t)] + (PString s, ([],K i,[])) | s==i -> return [] + (PInt s, ([],EInt i,[])) | s==i -> return [] + (PFloat s,([],EFloat i,[])) | s==i -> return [] --- rounding? + (PC p pp, ([], Con f, tt)) | + p `eqStrIdent` f && length pp == length tt -> + do matches <- mapM tryMatch (zip pp tt) + return (concat matches) + + (PP q p pp, ([], QC r f, tt)) | + -- q `eqStrIdent` r && --- not for inherited AR 10/10/2005 + p `eqStrIdent` f && length pp == length tt -> + do matches <- mapM tryMatch (zip pp tt) + return (concat matches) + ---- hack for AppPredef bug + (PP q p pp, ([], Q r f, tt)) | + -- q `eqStrIdent` r && --- + p `eqStrIdent` f && length pp == length tt -> + do matches <- mapM tryMatch (zip pp tt) + return (concat matches) + + (PR r, ([],R r',[])) | + all (`elem` map fst r') (map fst r) -> + do matches <- mapM tryMatch + [(p,snd a) | (l,p) <- r, let Just a = lookup l r'] + return (concat matches) + (PT _ p',_) -> trym p' t' + (_, ([],Alias _ _ d,[])) -> tryMatch (p,d) + +-- (PP (IC "Predef") (IC "CC") [p1,p2], ([],K s, [])) -> do + + (PAs x p',_) -> do + subst <- trym p' t' + return $ (x,t) : subst + + (PAlt p1 p2,_) -> checks [trym p1 t', trym p2 t'] + + (PNeg p',_) -> case tryMatch (p',t) of + Bad _ -> return [] + _ -> prtBad "no match with negative pattern" p + + (PSeq p1 p2, ([],K s, [])) -> do + let cuts = [splitAt n s | n <- [0 .. length s]] + matches <- checks [mapM tryMatch [(p1,K s1),(p2,K s2)] | (s1,s2) <- cuts] + return (concat matches) + + (PRep p1, ([],K s, [])) -> checks [ + trym (foldr (const (PSeq p1)) (PString "") + [1..n]) t' | n <- [0 .. length s] + ] >> + return [] + _ -> prtBad "no match in case expr for" t + +isInConstantForm :: Term -> Bool +isInConstantForm trm = case trm of + Cn _ -> True + Con _ -> True + Q _ _ -> True + QC _ _ -> True + Abs _ _ -> True + App c a -> isInConstantForm c && isInConstantForm a + R r -> all (isInConstantForm . snd . snd) r + K _ -> True + Empty -> True + Alias _ _ t -> isInConstantForm t + EInt _ -> True + _ -> False ---- isInArgVarForm trm + +varsOfPatt :: Patt -> [Ident] +varsOfPatt p = case p of + PV x -> [x | not (isWildIdent x)] + PC _ ps -> concat $ map varsOfPatt ps + PP _ _ ps -> concat $ map varsOfPatt ps + PR r -> concat $ map (varsOfPatt . snd) r + PT _ q -> varsOfPatt q + _ -> [] + +-- | to search matching parameter combinations in tables +isMatchingForms :: [Patt] -> [Term] -> Bool +isMatchingForms ps ts = all match (zip ps ts') where + match (PC c cs, (Cn d, ds)) = c == d && isMatchingForms cs ds + match _ = True + ts' = map appForm ts +