native representation for HOAS in PMCFG and incremental type checking of the parse forest

1 files changed, 120 insertions, 57 deletions

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