From b0e110cf4f7c6e43d044f05fdedde3ffaabb9843 Mon Sep 17 00:00:00 2001 From: krasimir Date: Mon, 9 Aug 2010 10:10:08 +0000 Subject: native representation for HOAS in PMCFG and incremental type checking of the parse forest --- src/runtime/haskell/PGF/Forest.hs | 177 ++++++++++++++++++++++++++------------ 1 file changed, 120 insertions(+), 57 deletions(-) (limited to 'src/runtime/haskell/PGF/Forest.hs') diff --git a/src/runtime/haskell/PGF/Forest.hs b/src/runtime/haskell/PGF/Forest.hs index f814e3f4f..58f0209a8 100644 --- a/src/runtime/haskell/PGF/Forest.hs +++ b/src/runtime/haskell/PGF/Forest.hs @@ -14,12 +14,14 @@ module PGF.Forest( Forest(..) , BracketedString, showBracketedString, lengthBracketedString , linearizeWithBrackets + , getAbsTrees , foldForest ) where import PGF.CId import PGF.Data import PGF.Macros +import PGF.TypeCheck import Data.List import Data.Array.IArray import qualified Data.Set as Set @@ -34,7 +36,7 @@ data Forest { abstr :: Abstr , concr :: Concr , forest :: IntMap.IntMap (Set.Set Production) - , root :: [([Symbol],[FId])] + , root :: [([Symbol],[PArg])] } -------------------------------------------------------------------- @@ -51,29 +53,39 @@ linearizeWithBrackets = head . snd . untokn "" . bracketedTokn bracketedTokn :: Forest -> BracketedTokn bracketedTokn f@(Forest abs cnc forest root) = - case [computeSeq seq (map (render forest) args) | (seq,args) <- root] of + case [computeSeq isTrusted seq (map (render forest) args) | (seq,args) <- root] of ([bs@(Bracket_ _ _ _ _ _)]:_) -> bs (bss:_) -> Bracket_ wildCId 0 0 [] bss [] -> Bracket_ wildCId 0 0 [] [] where + isTrusted (_,fid) = IntSet.member fid trusted + trusted = foldl1 IntSet.intersection [IntSet.unions (map (trustedSpots IntSet.empty) args) | (_,args) <- root] - render forest fid = + render forest arg@(PArg hypos fid) = case IntMap.lookup fid forest >>= Set.maxView of - Just (p,set) -> descend (if Set.null set then forest else IntMap.insert fid set forest) p + Just (p,set) -> let (ct,es,(_,lin)) = descend (if Set.null set then forest else IntMap.insert fid set forest) p + in (ct,es,(map getVar hypos,lin)) Nothing -> error ("wrong forest id " ++ show fid) where descend forest (PApply funid args) = let (CncFun fun lins) = cncfuns cnc ! funid - Just (DTyp _ cat _,_,_) = Map.lookup fun (funs abs) - largs = map (render forest) args - ltable = listArray (bounds lins) - [computeSeq (elems (sequences cnc ! seqid)) largs | - seqid <- elems lins] - in (fid,cat,ltable) - descend forest (PCoerce fid) = render forest fid - descend forest (PConst cat _ ts) = (fid,cat,listArray (0,0) [[LeafKS ts]]) - - trustedSpots parents fid + cat = case isLindefCId fun of + Just cat -> cat + Nothing -> case Map.lookup fun (funs abs) of + Just (DTyp _ cat _,_,_) -> cat + largs = map (render forest) args + ltable = mkLinTable cnc isTrusted [] funid largs + in ((cat,fid),either (const []) id $ getAbsTrees f arg Nothing,ltable) + descend forest (PCoerce fid) = render forest (PArg [] fid) + descend forest (PConst cat e ts) = ((cat,fid),[e],([],listArray (0,0) [[LeafKS ts]])) + + getVar (fid,_) + | fid == fidVar = wildCId + | otherwise = x + where + (x:_) = [x | PConst _ (EFun x) _ <- maybe [] Set.toList (IntMap.lookup fid forest)] + + trustedSpots parents (PArg _ fid) | fid < totalCats cnc || -- forest ids from the grammar correspond to metavariables IntSet.member fid parents -- this avoids loops in the grammar = IntSet.empty @@ -85,65 +97,116 @@ bracketedTokn f@(Forest abs cnc forest root) = parents' = IntSet.insert fid parents descend (PApply funid args) = IntSet.unions (map (trustedSpots parents') args) - descend (PCoerce fid) = trustedSpots parents' fid + descend (PCoerce fid) = trustedSpots parents' (PArg [] fid) descend (PConst c e _) = IntSet.empty - computeSeq :: [Symbol] -> [(FId,CId,LinTable)] -> [BracketedTokn] - computeSeq seq args = concatMap compute seq - where - compute (SymCat d r) = getArg d r - compute (SymLit d r) = getArg d r - compute (SymKS ts) = [LeafKS ts] - compute (SymKP ts alts) = [LeafKP ts alts] - - getArg d r - | not (null arg_lin) && - IntSet.member fid trusted - = [Bracket_ cat fid r es arg_lin] - | otherwise = arg_lin - where - arg_lin = lin ! r - (fid,cat,lin) = args !! d - es = getAbsTrees f fid +isLindefCId id + | take l s == lindef = Just (mkCId (drop l s)) + | otherwise = Nothing + where + s = showCId id + lindef = "lindef " + l = length lindef -- | This function extracts the list of all completed parse trees -- that spans the whole input consumed so far. The trees are also -- limited by the category specified, which is usually -- the same as the startup category. -getAbsTrees :: Forest -> FId -> [Expr] -getAbsTrees (Forest abs cnc forest root) fid = - nubsort $ do (fvs,e) <- go Set.empty 0 (0,fid) - guard (Set.null fvs) - return e +getAbsTrees :: Forest -> PArg -> Maybe Type -> Either [(FId,TcError)] [Expr] +getAbsTrees (Forest abs cnc forest root) arg@(PArg _ fid) ty = + let (res,err) = unTcFM (do e <- go Set.empty emptyScope arg (fmap (TTyp []) ty) + e <- runTcM abs fid (refineExpr e) + runTcM abs fid (checkResolvedMetaStore emptyScope e) + return e) IntMap.empty + in if null res + then Left (nub err) + else Right (nubsort (map snd res)) where - go rec_ fcat' (d,fcat) - | fcat < totalCats cnc = return (Set.empty,EMeta (fcat'*10+d)) -- FIXME: here we assume that every rule has at most 10 arguments - | Set.member fcat rec_ = mzero - | otherwise = foldForest (\funid args trees -> + go rec_ scope_ (PArg hypos fid) mb_tty_ + | fid < totalCats cnc = case mb_tty of + Just tty -> do i <- runTcM abs fid (newMeta scope tty) + return (mkAbs (EMeta i)) + Nothing -> mzero + | Set.member fid rec_ = mzero + | otherwise = foldForest (\funid args trees -> do let CncFun fn lins = cncfuns cnc ! funid - args <- mapM (go (Set.insert fcat rec_) fcat) (zip [0..] args) - check_ho_fun fn args + case isLindefCId fn of + Just _ -> do arg <- go (Set.insert fid rec_) scope (head args) mb_tty + return (mkAbs arg) + Nothing -> do tty_fn <- runTcM abs fid (lookupFunType fn) + (e,tty0) <- foldM (\(e1,tty) arg -> goArg (Set.insert fid rec_) scope fid e1 arg tty) + (EFun fn,tty_fn) args + case mb_tty of + Just tty -> runTcM abs fid $ do + i <- newGuardedMeta e + eqType scope (scopeSize scope) i tty tty0 + Nothing -> return () + return (mkAbs e) `mplus` trees) - (\const _ trees -> - return (freeVar const,const) + (\const _ trees -> do + const <- runTcM abs fid $ + case mb_tty of + Just tty -> tcExpr scope const tty + Nothing -> fmap fst $ infExpr scope const + return (mkAbs const) `mplus` trees) - [] fcat forest + mzero fid forest + where + (scope,mkAbs,mb_tty) = updateScope hypos scope_ id mb_tty_ + + goArg rec_ scope fid e1 arg (TTyp delta (DTyp ((bt,x,ty):hs) c es)) = do + e2' <- go rec_ scope arg (Just (TTyp delta ty)) + let e2 = case bt of + Explicit -> e2' + Implicit -> EImplArg e2' + if x == wildCId + then return (EApp e1 e2,TTyp delta (DTyp hs c es)) + else do v2 <- runTcM abs fid (eval (scopeEnv scope) e2') + return (EApp e1 e2,TTyp (v2:delta) (DTyp hs c es)) + + updateScope [] scope mkAbs mb_tty = (scope,mkAbs,mb_tty) + updateScope ((fid,_):hypos) scope mkAbs mb_tty = + case mb_tty of + Just (TTyp delta (DTyp ((bt,y,ty):hs) c es)) -> + if y == wildCId + then updateScope hypos (addScopedVar x (TTyp delta ty) scope) + (mkAbs . EAbs bt x) + (Just (TTyp delta (DTyp hs c es))) + else updateScope hypos (addScopedVar x (TTyp delta ty) scope) + (mkAbs . EAbs bt x) + (Just (TTyp ((VGen (scopeSize scope) []):delta) (DTyp hs c es))) + Nothing -> (scope,mkAbs,Nothing) + where + (x:_) | fid == fidVar = [wildCId] + | otherwise = [x | PConst _ (EFun x) _ <- maybe [] Set.toList (IntMap.lookup fid forest)] + + +newtype TcFM a = TcFM {unTcFM :: MetaStore -> ([(MetaStore,a)],[(FId,TcError)])} + +instance Functor TcFM where + fmap f g = TcFM (\ms -> let (res_g,err_g) = unTcFM g ms + in ([(ms,f x) | (ms,x) <- res_g],err_g)) + +instance Monad TcFM where + return x = TcFM (\ms -> ([(ms,x)],[])) + f >>= g = TcFM (\ms -> case unTcFM f ms of + (res,err) -> let (res',err') = unzip [unTcFM (g x) ms | (ms,x) <- res] + in (concat res',concat (err:err'))) - check_ho_fun fun args - | fun == _V = return (head args) - | fun == _B = return (foldl1 Set.difference (map fst args), foldr (\x e -> EAbs Explicit (mkVar (snd x)) e) (snd (head args)) (tail args)) - | otherwise = return (Set.unions (map fst args),foldl (\e x -> EApp e (snd x)) (EFun fun) args) - - mkVar (EFun v) = v - mkVar (EMeta _) = wildCId - - freeVar (EFun v) = Set.singleton v - freeVar _ = Set.empty +instance MonadPlus TcFM where + mzero = TcFM (\ms -> ([],[])) + mplus f g = TcFM (\ms -> let (res_f,err_f) = unTcFM f ms + (res_g,err_g) = unTcFM g ms + in (res_f++res_g,err_f++err_g)) +runTcM :: Abstr -> FId -> TcM a -> TcFM a +runTcM abstr fid f = TcFM (\ms -> case unTcM f abstr ms of + Ok ms x -> ([(ms,x)],[] ) + Fail err -> ([], [(fid,err)])) -foldForest :: (FunId -> [FId] -> b -> b) -> (Expr -> [String] -> b -> b) -> b -> FId -> IntMap.IntMap (Set.Set Production) -> b +foldForest :: (FunId -> [PArg] -> b -> b) -> (Expr -> [String] -> b -> b) -> b -> FId -> IntMap.IntMap (Set.Set Production) -> b foldForest f g b fcat forest = case IntMap.lookup fcat forest of Nothing -> b -- cgit v1.2.3