now the generation from template with meta-variables respects the dependent types

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)
+  restart g (\g -> generateForMetas (Identity g) pgf e dp)
-
-
-
--- 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
-    _ -> []
 
 
 ------------------------------------------------------------------------------
@@ -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

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