From e7f6239bc6118d3872f67392665198f5f0c2c273 Mon Sep 17 00:00:00 2001 From: krasimir Date: Mon, 11 Oct 2010 09:59:57 +0000 Subject: [PATCH] now the generation from template with meta-variables respects the dependent types --- src/runtime/haskell/PGF/Generate.hs | 35 ++++++++++++---------------- src/runtime/haskell/PGF/TypeCheck.hs | 23 ++++++++++++++---- 2 files changed, 34 insertions(+), 24 deletions(-) diff --git a/src/runtime/haskell/PGF/Generate.hs b/src/runtime/haskell/PGF/Generate.hs index 86cfaa47b..3fabbb2f4 100644 --- a/src/runtime/haskell/PGF/Generate.hs +++ b/src/runtime/haskell/PGF/Generate.hs @@ -38,7 +38,7 @@ 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 False pgf (\ty -> generateAllDepth pgf ty dp) e +generateFromDepth pgf e dp = generateForMetas () pgf e dp -- | Generates an infinite list of random abstract syntax expressions. -- This is usefull for tree bank generation which after that can be used @@ -58,24 +58,7 @@ 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 True pgf (\ty -> generate (Identity g) pgf ty dp) e) - - - --- generic algorithm for filling holes in a generator --- for random, should be breadth-first, since otherwise first metas always get the same --- value when a list is generated -generateForMetas :: Bool -> PGF -> (Type -> [Expr]) -> Expr -> [Expr] -generateForMetas breadth pgf gen exp = case exp of - EApp f (EMeta _) -> [EApp g a | g <- gener f, a <- genArg g] - EApp f x | breadth -> [EApp g a | (g,a) <- zip (gener f) (gener x)] - EApp f x -> [EApp g a | g <- gener f, a <- gener x] - _ -> if breadth then repeat exp else [exp] - where - gener = generateForMetas breadth pgf gen - genArg f = case inferExpr pgf f of - Right (_,DTyp ((_,_,ty):_) _ _) -> gen ty - _ -> [] + restart g (\g -> generateForMetas (Identity g) pgf e dp) ------------------------------------------------------------------------------ @@ -84,7 +67,19 @@ generateForMetas breadth pgf gen exp = case exp of generate :: Selector sel => sel -> PGF -> Type -> Maybe Int -> [Expr] generate sel pgf ty dp = [value2expr (funs (abstract pgf),lookupMeta ms) 0 v | - (ms,v) <- runGenM (prove (abstract pgf) emptyScope (TTyp [] ty) dp) sel IntMap.empty] + (ms,v) <- runGenM (prove (abstract pgf) emptyScope (TTyp [] ty) dp) sel emptyMetaStore] + +generateForMetas :: Selector sel => sel -> PGF -> Expr -> Maybe Int -> [Expr] +generateForMetas sel pgf e dp = + case unTcM (infExpr emptyScope e) abs emptyMetaStore of + Ok ms (e,_) -> let gen = do fillinVariables (runTcM abs) $ \scope tty -> do + v <- prove abs scope tty dp + return (value2expr (funs abs,lookupMeta ms) 0 v) + runTcM abs (refineExpr e) + in [e | (ms,e) <- runGenM gen sel ms] + Fail _ -> [] + where + abs = abstract pgf prove :: Selector sel => Abstr -> Scope -> TType -> Maybe Int -> GenM sel MetaStore Value prove abs scope tty@(TTyp env (DTyp [] cat es)) dp = do diff --git a/src/runtime/haskell/PGF/TypeCheck.hs b/src/runtime/haskell/PGF/TypeCheck.hs index d95e50c5e..10938a639 100644 --- a/src/runtime/haskell/PGF/TypeCheck.hs +++ b/src/runtime/haskell/PGF/TypeCheck.hs @@ -1,3 +1,5 @@ +{-# LANGUAGE FlexibleContexts, RankNTypes #-} + ---------------------------------------------------------------------- -- | -- Module : PGF.TypeCheck @@ -16,7 +18,7 @@ module PGF.TypeCheck ( checkType, checkExpr, inferExpr , ppTcError, TcError(..) -- internals needed for the typechecking of forests - , MetaStore, newMeta, newGuardedMeta + , MetaStore, emptyMetaStore, newMeta, newGuardedMeta, fillinVariables , Scope, emptyScope, scopeSize, scopeEnv, addScopedVar , TcM(..), TcResult(..), TType(..), tcError , tcExpr, infExpr, eqType @@ -104,6 +106,9 @@ lookupFunType fun = TcM (\abstr ms -> case Map.lookup fun (funs abstr) of Just (ty,_,_,_) -> Ok ms (TTyp [] ty) Nothing -> Fail (UnknownFun fun)) +emptyMetaStore :: MetaStore +emptyMetaStore = IntMap.empty + newMeta :: Scope -> TType -> TcM MetaId newMeta scope tty = TcM (\abstr ms -> let metaid = IntMap.size ms + 1 in Ok (IntMap.insert metaid (MUnbound scope tty []) ms) metaid) @@ -126,6 +131,16 @@ lookupMeta ms i = Just (MUnbound _ _ _) -> Nothing Nothing -> Nothing +fillinVariables :: Monad m => (forall a . TcM a -> m a) -> (Scope -> TType -> m Expr) -> m () +fillinVariables runTcM f = do + fvs <- runTcM (TcM (\abstr ms -> Ok 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 + runTcM $ do setMeta i (MBound e) + sequence_ [c e | c <- cs] + fillinVariables runTcM f + tcError :: TcError -> TcM a tcError e = TcM (\abstr ms -> Fail e) @@ -198,7 +213,7 @@ ppTcError (UnsolvableGoal xs metaid ty)= text "The goal:" <+> ppMeta metaid <+> -- syntax of the grammar. checkType :: PGF -> Type -> Either TcError Type checkType pgf ty = - case unTcM (tcType emptyScope ty >>= refineType) (abstract pgf) IntMap.empty of + case unTcM (tcType emptyScope ty >>= refineType) (abstract pgf) emptyMetaStore of Ok ms ty -> Right ty Fail err -> Left err @@ -260,7 +275,7 @@ checkExpr pgf e ty = case unTcM (do e <- tcExpr emptyScope e (TTyp [] ty) e <- refineExpr e checkResolvedMetaStore emptyScope e - return e) (abstract pgf) IntMap.empty of + return e) (abstract pgf) emptyMetaStore of Ok ms e -> Right e Fail err -> Left err @@ -316,7 +331,7 @@ inferExpr pgf e = e <- refineExpr e checkResolvedMetaStore emptyScope e ty <- evalType 0 tty - return (e,ty)) (abstract pgf) IntMap.empty of + return (e,ty)) (abstract pgf) emptyMetaStore of Ok ms (e,ty) -> Right (e,ty) Fail err -> Left err