summaryrefslogtreecommitdiff
path: root/src/runtime/haskell
diff options
context:
space:
mode:
Diffstat (limited to 'src/runtime/haskell')
-rw-r--r--src/runtime/haskell/PGF/Forest.hs28
-rw-r--r--src/runtime/haskell/PGF/Generate.hs37
-rw-r--r--src/runtime/haskell/PGF/TypeCheck.hs120
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]
-
-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
+ [e | (_,ms,e) <- snd $ runTcM (abstract pgf)
+ (prove dp emptyScope (TTyp [] ty) >>= checkResolvedMetaStore emptyScope)
+ sel emptyMetaStore]
-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
+
+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
- isResolved (MUnbound _ _ []) = True
- isResolved (MGuarded _ _ _) = True
- isResolved (MBound _) = True
- isResolved _ = False
+ 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
generated by cgit v1.2.3 (git 2.39.1) at 2026-05-20 09:35:32 +0000