msyds/gf-core
1
0
Fork 0
forked from GitHub/gf-core
Code Pull Requests Activity

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

Browse Source
This commit is contained in:
krasimir
2010-10-11 09:59:57 +00:00
parent 9e484c7e8f
commit e7f6239bc6
2 changed files with 34 additions and 24 deletions
Download Patch File Download Diff File Expand all files Collapse all files

35
src/runtime/haskell/PGF/Generate.hs
View File

@@ -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

23
src/runtime/haskell/PGF/TypeCheck.hs
View File

@@ -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