From 702b4aad3b7862c445a22a05de9fef6e3f44576c Mon Sep 17 00:00:00 2001 From: krasimir Date: Mon, 18 Oct 2010 15:55:14 +0000 Subject: [PATCH] now we use the GF reasoner to fillin meta variables in the abstract trees generated from the parser --- src/runtime/haskell/PGF/Forest.hs | 28 +++---- src/runtime/haskell/PGF/Generate.hs | 37 ++++----- src/runtime/haskell/PGF/TypeCheck.hs | 120 +++++++++++++++++---------- 3 files changed, 103 insertions(+), 82 deletions(-) diff --git a/src/runtime/haskell/PGF/Forest.hs b/src/runtime/haskell/PGF/Forest.hs index 54204cabb..97cfbfa21 100644 --- a/src/runtime/haskell/PGF/Forest.hs +++ b/src/runtime/haskell/PGF/Forest.hs @@ -24,6 +24,7 @@ import PGF.CId import PGF.Data import PGF.Macros import PGF.TypeCheck +import PGF.Generate import Data.List import Data.Array.IArray import qualified Data.Set as Set @@ -118,9 +119,7 @@ isLindefCId id getAbsTrees :: Forest -> PArg -> Maybe Type -> Either [(FId,TcError)] [Expr] getAbsTrees (Forest abs cnc forest root) arg@(PArg _ fid) ty = let (err,res) = runTcM abs (do e <- go Set.empty emptyScope (fmap (TTyp []) ty) arg - e <- refineExpr e - checkResolvedMetaStore emptyScope e - return e) fid IntMap.empty + generateForForest (prove (Just 20)) e) fid IntMap.empty in if null res then Left (nub err) else Right (nubsort [e | (_,_,e) <- res]) @@ -131,10 +130,12 @@ getAbsTrees (Forest abs cnc forest root) arg@(PArg _ fid) ty = return (mkAbs (EMeta i)) Nothing -> mzero | Set.member fid rec_ = mzero - | otherwise = foldForest (\funid args trees -> + | otherwise = do fid0 <- get + put fid + x <- foldForest (\funid args trees -> do let CncFun fn lins = cncfuns cnc ! funid case isLindefCId fn of - Just _ -> do arg <- bracket (go (Set.insert fid rec_) scope mb_tty) arg + Just _ -> do arg <- go (Set.insert fid rec_) scope mb_tty arg return (mkAbs arg) Nothing -> do ty_fn <- lookupFunType fn (e,tty0) <- foldM (\(e1,tty) arg -> goArg (Set.insert fid rec_) scope fid e1 arg tty) @@ -146,19 +147,22 @@ getAbsTrees (Forest abs cnc forest root) arg@(PArg _ fid) ty = return (mkAbs e) `mplus` trees) - (\const _ trees -> do + (\const _ trees -> do const <- case mb_tty of Just tty -> tcExpr scope const tty Nothing -> fmap fst $ infExpr scope const return (mkAbs const) `mplus` trees) - mzero fid forest + mzero fid forest + put fid0 + return x + 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' <- bracket (go rec_ scope (Just (TTyp delta ty))) arg + e2' <- go rec_ scope (Just (TTyp delta ty)) arg let e2 = case bt of Explicit -> e2' Implicit -> EImplArg e2' @@ -182,14 +186,6 @@ getAbsTrees (Forest abs cnc forest root) arg@(PArg _ fid) ty = where (x:_) | fid == fidVar = [wildCId] | otherwise = [x | PConst _ (EFun x) _ <- maybe [] Set.toList (IntMap.lookup fid forest)] - - bracket f arg@(PArg _ fid) = do - fid0 <- get - put fid - x <- f arg - put fid0 - return x - foldForest :: (FunId -> [PArg] -> b -> b) -> (Expr -> [String] -> b -> b) -> b -> FId -> IntMap.IntMap (Set.Set Production) -> b foldForest f g b fcat forest = diff --git a/src/runtime/haskell/PGF/Generate.hs b/src/runtime/haskell/PGF/Generate.hs index cbd3d23ab..fcbf405a2 100644 --- a/src/runtime/haskell/PGF/Generate.hs +++ b/src/runtime/haskell/PGF/Generate.hs @@ -3,6 +3,7 @@ module PGF.Generate , generateFrom, generateFromDepth , generateRandom, generateRandomDepth , generateRandomFrom, generateRandomFromDepth + , prove ) where import PGF.CId @@ -43,7 +44,10 @@ generateFrom pgf ex = generateFromDepth pgf ex Nothing -- | A variant of 'generateFrom' which also takes as argument -- the upper limit of the depth of the generated subexpressions. generateFromDepth :: PGF -> Expr -> Maybe Int -> [Expr] -generateFromDepth pgf e dp = generateForMetas () pgf e dp +generateFromDepth pgf e dp = + [e | (_,_,e) <- snd $ runTcM (abstract pgf) + (generateForMetas (prove dp) e) + () emptyMetaStore] -- | Generates an infinite list of random abstract syntax expressions. -- This is usefull for tree bank generation which after that can be used @@ -63,7 +67,9 @@ generateRandomFrom g pgf e = generateRandomFromDepth g pgf e Nothing -- | Random generation based on template with a limitation in the depth. generateRandomFromDepth :: RandomGen g => g -> PGF -> Expr -> Maybe Int -> [Expr] generateRandomFromDepth g pgf e dp = - restart g (\g -> generateForMetas (Identity g) pgf e dp) + restart g (\g -> [e | (_,ms,e) <- snd $ runTcM (abstract pgf) + (generateForMetas (prove dp) e) + (Identity g) emptyMetaStore]) ------------------------------------------------------------------------------ @@ -71,21 +77,12 @@ generateRandomFromDepth g pgf e dp = generate :: Selector sel => sel -> PGF -> Type -> Maybe Int -> [Expr] generate sel pgf ty dp = - [e | (_,ms,e) <- snd $ runTcM (abstract pgf) (prove emptyScope (TTyp [] ty) dp >>= refineExpr) sel emptyMetaStore] + [e | (_,ms,e) <- snd $ runTcM (abstract pgf) + (prove dp emptyScope (TTyp [] ty) >>= checkResolvedMetaStore emptyScope) + sel emptyMetaStore] -generateForMetas :: Selector sel => sel -> PGF -> Expr -> Maybe Int -> [Expr] -generateForMetas sel pgf e dp = - case unTcM (infExpr emptyScope e) abs sel emptyMetaStore of - Ok sel ms (e,_) -> let gen = do fillinVariables $ \scope tty -> do - prove scope tty dp - refineExpr e - in [e | (_,ms,e) <- snd $ runTcM abs gen sel ms] - Fail _ _ -> [] - where - abs = abstract pgf - -prove :: Selector sel => Scope -> TType -> Maybe Int -> TcM sel Expr -prove scope (TTyp env1 (DTyp [] cat es1)) dp = do +prove :: Selector sel => Maybe Int -> Scope -> TType -> TcM sel Expr +prove dp scope (TTyp env1 (DTyp [] cat es1)) = do (fe,DTyp hypos _ es2) <- select cat dp if fe == EFun (mkCId "plus") then mzero else return () case dp of @@ -102,9 +99,9 @@ prove scope (TTyp env1 (DTyp [] cat es1)) dp = do mv <- getMeta i case mv of MBound e -> c e - MUnbound scope tty cs -> do e <- prove scope tty dp - setMeta i (MBound e) - sequence_ [c e | c <- (c:cs)] + MUnbound _ scope tty cs -> do e <- prove dp scope tty + setMeta i (MBound e) + sequence_ [c e | c <- (c:cs)] mkEnv env [] = return (env,[]) mkEnv env ((bt,x,ty):hypos) = do @@ -118,7 +115,7 @@ prove scope (TTyp env1 (DTyp [] cat es1)) dp = do descend (bt,arg) = do let dp' = fmap (flip (-) 1) dp e <- case arg of Right e -> return e - Left tty -> prove scope tty dp' + Left tty -> prove dp' scope tty e <- case bt of Implicit -> return (EImplArg e) Explicit -> return e diff --git a/src/runtime/haskell/PGF/TypeCheck.hs b/src/runtime/haskell/PGF/TypeCheck.hs index 843326e4c..c4da14926 100644 --- a/src/runtime/haskell/PGF/TypeCheck.hs +++ b/src/runtime/haskell/PGF/TypeCheck.hs @@ -18,12 +18,13 @@ module PGF.TypeCheck ( checkType, checkExpr, inferExpr , ppTcError, TcError(..) -- internals needed for the typechecking of forests - , MetaStore, emptyMetaStore, newMeta, newGuardedMeta, fillinVariables, getMeta, setMeta, MetaValue(..) + , MetaStore, emptyMetaStore, newMeta, newGuardedMeta + , getMeta, setMeta, lookupMeta, MetaValue(..) , Scope, emptyScope, scopeSize, scopeEnv, addScopedVar , TcM(..), TcResult(..), runTcM, TType(..), Selector(..) , tcExpr, infExpr, eqType, eqValue , lookupFunType, eval - , refineExpr, checkResolvedMetaStore, lookupMeta + , generateForMetas, generateForForest, checkResolvedMetaStore ) where import PGF.Data @@ -78,7 +79,7 @@ scopeSize (Scope gamma) = length gamma type MetaStore s = IntMap (MetaValue s) data MetaValue s - = MUnbound Scope TType [Expr -> TcM s ()] + = MUnbound s Scope TType [Expr -> TcM s ()] | MBound Expr | MGuarded Expr [Expr -> TcM s ()] {-# UNPACK #-} !Int -- the Int is the number of constraints that have to be solved -- to unlock this meta variable @@ -152,7 +153,7 @@ emptyMetaStore = IntMap.empty newMeta :: Scope -> TType -> TcM s MetaId newMeta scope tty = TcM (\abstr s ms -> let metaid = IntMap.size ms + 1 - in Ok s (IntMap.insert metaid (MUnbound scope tty []) ms) metaid) + in Ok s (IntMap.insert metaid (MUnbound s scope tty []) ms) metaid) newGuardedMeta :: Expr -> TcM s MetaId newGuardedMeta e = TcM (\abstr s ms -> let metaid = IntMap.size ms + 1 @@ -170,24 +171,14 @@ lookupMeta ms i = Just (MBound t) -> Just t Just (MGuarded t _ x) | x == 0 -> Just t | otherwise -> Nothing - Just (MUnbound _ _ _) -> Nothing + Just (MUnbound _ _ _ _) -> Nothing Nothing -> Nothing -fillinVariables :: (Scope -> TType -> TcM s Expr) -> TcM s () -fillinVariables f = do - fvs <- TcM (\abstr s ms -> Ok s ms [(i,scope,tty,cs) | (i,MUnbound scope tty cs) <- IntMap.toList ms]) - case fvs of - [] -> return () - (i,scope,tty,cs):_ -> do e <- f scope tty - setMeta i (MBound e) - sequence_ [c e | c <- cs] - fillinVariables f - addConstraint :: MetaId -> MetaId -> (Expr -> TcM s ()) -> TcM s () addConstraint i j c = do mv <- getMeta j case mv of - MUnbound scope tty cs -> addRef >> setMeta j (MUnbound scope tty ((\e -> release >> c e) : cs)) + MUnbound s scope tty cs -> addRef >> setMeta j (MUnbound s scope tty ((\e -> release >> c e) : cs)) MBound e -> c e MGuarded e cs x | x == 0 -> c e | otherwise -> addRef >> setMeta j (MGuarded e ((\e -> release >> c e) : cs) x) @@ -312,9 +303,7 @@ tcCatArgs scope _ delta _ ty0@(DTyp _ cat _) n m = do checkExpr :: PGF -> Expr -> Type -> Either TcError Expr checkExpr pgf e ty = case unTcM (do e <- tcExpr emptyScope e (TTyp [] ty) - e <- refineExpr e - checkResolvedMetaStore emptyScope e - return e) (abstract pgf) () emptyMetaStore of + checkResolvedMetaStore emptyScope e) (abstract pgf) () emptyMetaStore of Ok _ ms e -> Right e Fail _ err -> Left err @@ -367,8 +356,7 @@ tcExpr scope e0 tty = do inferExpr :: PGF -> Expr -> Either TcError (Expr,Type) inferExpr pgf e = case unTcM (do (e,tty) <- infExpr emptyScope e - e <- refineExpr e - checkResolvedMetaStore emptyScope e + e <- checkResolvedMetaStore emptyScope e ty <- evalType 0 tty return (e,ty)) (abstract pgf) () emptyMetaStore of Ok _ ms (e,ty) -> Right (e,ty) @@ -468,7 +456,7 @@ eqValue fail suspend k v1 v2 = do MBound e -> apply env e vs MGuarded e _ x | x == 0 -> apply env e vs | otherwise -> return v - MUnbound _ _ _ -> return v + MUnbound _ _ _ _ -> return v deRef v = return v eqValue' k (VSusp i env vs1 c) v2 = suspend i (\e -> apply env e vs1 >>= \v1 -> eqValue fail suspend k (c v1) v2) @@ -476,16 +464,16 @@ eqValue fail suspend k v1 v2 = do eqValue' k (VMeta i env1 vs1) (VMeta j env2 vs2) | i == j = zipWithM_ (eqValue fail suspend k) vs1 vs2 eqValue' k (VMeta i env1 vs1) v2 = do mv <- getMeta i case mv of - MUnbound scopei _ cs -> do e2 <- mkLam i scopei env1 vs1 v2 - setMeta i (MBound e2) - sequence_ [c e2 | c <- cs] - MGuarded e cs x -> setMeta i (MGuarded e ((\e -> apply env1 e vs1 >>= \v1 -> eqValue' k v1 v2) : cs) x) + MUnbound _ scopei _ cs -> do e2 <- mkLam i scopei env1 vs1 v2 + setMeta i (MBound e2) + sequence_ [c e2 | c <- cs] + MGuarded e cs x -> setMeta i (MGuarded e ((\e -> apply env1 e vs1 >>= \v1 -> eqValue' k v1 v2) : cs) x) eqValue' k v1 (VMeta i env2 vs2) = do mv <- getMeta i case mv of - MUnbound scopei _ cs -> do e1 <- mkLam i scopei env2 vs2 v1 - setMeta i (MBound e1) - sequence_ [c e1 | c <- cs] - MGuarded e cs x -> setMeta i (MGuarded e ((\e -> apply env2 e vs2 >>= \v2 -> eqValue' k v1 v2) : cs) x) + MUnbound _ scopei _ cs -> do e1 <- mkLam i scopei env2 vs2 v1 + setMeta i (MBound e1) + sequence_ [c e1 | c <- cs] + MGuarded e cs x -> setMeta i (MGuarded e ((\e -> apply env2 e vs2 >>= \v2 -> eqValue' k v1 v2) : cs) x) eqValue' k (VApp f1 vs1) (VApp f2 vs2) | f1 == f2 = zipWithM_ (eqValue fail suspend k) vs1 vs2 eqValue' k (VConst f1 vs1) (VConst f2 vs2) | f1 == f2 = zipWithM_ (eqValue fail suspend k) vs1 vs2 eqValue' k (VLit l1) (VLit l2 ) | l1 == l2 = return () @@ -518,11 +506,11 @@ eqValue fail suspend k v1 v2 = do else return () mv <- getMeta i case mv of - MBound e -> apply env e vs >>= occurCheck i0 k xs - MGuarded e _ _ -> apply env e vs >>= occurCheck i0 k xs - MUnbound scopei _ _ | scopeSize scopei > k -> fail - | otherwise -> do vs <- mapM (occurCheck i0 k xs) vs - return (VMeta i env vs) + MBound e -> apply env e vs >>= occurCheck i0 k xs + MGuarded e _ _ -> apply env e vs >>= occurCheck i0 k xs + MUnbound _ scopei _ _ | scopeSize scopei > k -> fail + | otherwise -> do vs <- mapM (occurCheck i0 k xs) vs + return (VMeta i env vs) occurCheck i0 k xs (VSusp i env vs cnt) = do suspend i (\e -> apply env e vs >>= \v -> occurCheck i0 k xs (cnt v) >> return ()) return (VSusp i env vs cnt) occurCheck i0 k xs (VGen i vs) = case List.findIndex (==i) xs of @@ -536,20 +524,60 @@ eqValue fail suspend k v1 v2 = do ----------------------------------------------------------- --- check for meta variables that still have to be resolved +-- three ways of dealing with meta variables that +-- still have to be resolved ----------------------------------------------------------- -checkResolvedMetaStore :: Scope -> Expr -> TcM s () -checkResolvedMetaStore scope e = TcM (\abstr s ms -> - let xs = [i | (i,mv) <- IntMap.toList ms, not (isResolved mv)] - in if List.null xs - then Ok s ms () - else Fail s (UnresolvedMetaVars (scopeVars scope) e xs)) +checkResolvedMetaStore :: Scope -> Expr -> TcM s Expr +checkResolvedMetaStore scope e = do + e <- refineExpr e + TcM (\abstr s ms -> + let xs = [i | (i,mv) <- IntMap.toList ms, not (isResolved mv)] + in if List.null xs + then Ok s ms () + else Fail s (UnresolvedMetaVars (scopeVars scope) e xs)) + return e where - isResolved (MUnbound _ _ []) = True - isResolved (MGuarded _ _ _) = True - isResolved (MBound _) = True - isResolved _ = False + isResolved (MUnbound _ _ _ []) = True + isResolved (MGuarded _ _ _) = True + isResolved (MBound _) = True + isResolved _ = False + +generateForMetas :: Selector s => (Scope -> TType -> TcM s Expr) -> Expr -> TcM s Expr +generateForMetas prove e = do + infExpr emptyScope e + fillinVariables + refineExpr e + return e + where + fillinVariables = do + fvs <- TcM (\abstr s ms -> Ok s ms [(i,s,scope,tty,cs) | (i,MUnbound s scope tty cs) <- IntMap.toList ms]) + case fvs of + [] -> return () + (i,_,scope,tty,cs):_ -> do e <- prove scope tty + setMeta i (MBound e) + sequence_ [c e | c <- cs] + fillinVariables + +generateForForest :: (Scope -> TType -> TcM FId Expr) -> Expr -> TcM FId Expr +generateForForest prove e = do + fillinVariables + refineExpr e + return e + where + fillinVariables = do + fvs <- TcM (\abstr s ms -> Ok s ms [(i,s,scope,tty,cs) | (i,MUnbound s scope tty cs) <- IntMap.toList ms]) + case fvs of + [] -> return () + (i,s,scope,tty,cs):_ -> TcM (\abstr s0 ms -> + case snd $ runTcM abstr (prove scope tty) s ms of + [] -> unTcM (do ty <- evalType (scopeSize scope) tty + throwError (UnsolvableGoal (scopeVars scope) s ty) + ) abstr s ms + ((_,ms,e):_) -> unTcM (do setMeta i (MBound e) + sequence_ [c e | c <- cs] + fillinVariables + ) abstr s ms) ----------------------------------------------------- -- evalType