support for proof search with high-order functions

src/runtime/haskell/PGF/Forest.hs

@@ -203,13 +203,9 @@ foldForest f g b fcat forest =
 
 instance Selector FId where
   splitSelector s = (s,s)
-  select cat dp = TcM (\abstr s ms -> case Map.lookup cat (cats abstr) of
+  select cat scope dp = do
-                                        Just (_,fns) -> iter abstr s ms fns
+    gens <- typeGenerators scope cat
-                                        Nothing      -> Fail s (UnknownCat cat))
+    TcM (\abstr s ms -> iter s ms gens)
     where
-      iter abstr s ms []           = Zero
+      iter s ms []              = Zero
-      iter abstr s ms ((_,fn):fns) = Plus (select_helper fn abstr s ms) (iter abstr s ms fns)
+      iter s ms ((_,e,tty):fns) = Plus (Ok s ms (e,tty)) (iter s ms fns)
-
-select_helper fn = unTcM $ do
-  ty <- lookupFunType fn
-  return (EFun fn,ty)

src/runtime/haskell/PGF/Generate.hs

@@ -82,18 +82,19 @@ generate sel pgf ty dp =
                                 sel emptyMetaStore]
 
 prove :: Selector sel => Maybe Int -> Scope -> TType -> TcM sel Expr
-prove dp scope (TTyp env1 (DTyp [] cat es1)) = do
+prove dp scope (TTyp env1 (DTyp hypos1 cat es1)) = do
-  (fe,DTyp hypos _ es2) <- select cat dp
+  vs1 <- mapM (PGF.TypeCheck.eval env1) es1
+  let scope' = exScope scope env1 hypos1
+  (fe,TTyp env2 (DTyp hypos2 _ es2)) <- select cat scope' dp
   if fe == EFun (mkCId "plus") then mzero else return ()
   case dp of
-    Just 0 | not (null hypos) -> mzero
+    Just 0 | not (null hypos2) -> mzero
-    _                         -> return ()
+    _                          -> return ()
-  (env2,args) <- mkEnv [] hypos
+  (env2,args) <- mkEnv scope' env2 hypos2
-  vs1 <- mapM (PGF.TypeCheck.eval env1) es1
   vs2 <- mapM (PGF.TypeCheck.eval env2) es2
-  sequence_ [eqValue mzero suspend (scopeSize scope) v1 v2 | (v1,v2) <- zip vs1 vs2]
+  sequence_ [eqValue mzero suspend (scopeSize scope') v1 v2 | (v1,v2) <- zip vs1 vs2]
-  es <- mapM descend args
+  es <- mapM (descend scope') args
-  return (foldl EApp fe es)
+  return (abs hypos1 (foldl EApp fe es))
   where
     suspend i c = do
       mv <- getMeta i
@@ -103,23 +104,33 @@ prove dp scope (TTyp env1 (DTyp [] cat es1)) = do
                                       setMeta i (MBound e)
                                       sequence_ [c e | c <- (c:cs)]
 
-    mkEnv env []                = return (env,[])
+    abs []                e = e
-    mkEnv env ((bt,x,ty):hypos) = do
+    abs ((bt,x,ty):hypos) e = EAbs bt x (abs hypos e)
+
+    exScope scope env []                = scope
+    exScope scope env ((bt,x,ty):hypos) = 
+       let env' | x /= wildCId = VGen (scopeSize scope) [] : env
+                | otherwise    = env
+       in exScope (addScopedVar x (TTyp env ty) scope) env' hypos
+
+    mkEnv scope env []                = return (env,[])
+    mkEnv scope env ((bt,x,ty):hypos) = do
       (env,arg) <- if x /= wildCId
                     then do i <- newMeta scope (TTyp env ty)
                             return (VMeta i (scopeEnv scope) [] : env,Right (EMeta i))
                     else return (env,Left (TTyp env ty))
-      (env,args) <- mkEnv env hypos
+      (env,args) <- mkEnv scope env hypos
       return (env,(bt,arg):args)
 
-    descend (bt,arg) = do let dp' = fmap (flip (-) 1) dp
+    descend scope (bt,arg) = do
-                          e <- case arg of
+      let dp' = fmap (flip (-) 1) dp
-                                 Right e  -> return e
+      e <- case arg of
-                                 Left tty -> prove dp' scope tty
+             Right e  -> return e
-                          e <- case bt of
+             Left tty -> prove dp' scope tty
-                                 Implicit -> return (EImplArg e)
+      e <- case bt of
-                                 Explicit -> return e
+             Implicit -> return (EImplArg e)
-                          return e
+             Explicit -> return e
+      return e
 
 
 -- Helper function for random generation. After every
@@ -137,50 +148,30 @@ restart g f =
 
 instance Selector () where
   splitSelector s = (s,s)
-  select cat dp
+  select cat scope dp = do
-    | cat == cidInt    = return (ELit (LInt 999),  DTyp [] cat [])
+    gens <- typeGenerators scope cat
-    | cat == cidFloat  = return (ELit (LFlt 3.14), DTyp [] cat [])
+    TcM (\abstr s ms -> iter ms gens)
-    | cat == cidString = return (ELit (LStr "Foo"),DTyp [] cat [])
-    | otherwise        = TcM (\abstr s ms -> case Map.lookup cat (cats abstr) of
-                                               Just (_,fns) -> iter abstr ms fns
-                                               Nothing      -> Fail s (UnknownCat cat))
     where
-      iter abstr ms []           = Zero
+      iter ms []              = Zero
-      iter abstr ms ((_,fn):fns) = Plus (select_helper fn abstr () ms) (iter abstr ms fns)
+      iter ms ((_,e,tty):fns) = Plus (Ok () ms (e,tty)) (iter ms fns)
+
 
 instance RandomGen g => Selector (Identity g) where
   splitSelector (Identity g) = let (g1,g2) = split g
                                in (Identity g1, Identity g2)
 
-  select cat dp
+  select cat scope dp = do
-    | cat == cidInt    = TcM (\abstr (Identity g) ms ->
+    gens <- typeGenerators scope cat
-                                  let (n,g') = maybe random (\d -> randomR ((-10)*d,10*d)) dp g
+    TcM (\abstr (Identity g) ms -> do_rand abstr g ms 1.0 gens)
-                                  in Ok (Identity g) ms (ELit (LInt n),DTyp [] cat []))
-    | cat == cidFloat  = TcM (\abstr (Identity g) ms ->
-                                  let (d,g') = maybe random (\d' -> let d = fromIntegral d'
-                                                                    in randomR ((-pi)*d,pi*d)) dp g
-                                  in Ok (Identity g) ms (ELit (LFlt d),DTyp [] cat []))
-    | cat == cidString = TcM (\abstr (Identity g) ms ->
-                                  let (g1,g2) = split g
-                                      s = take (fromMaybe 10 dp) (randomRs ('A','Z') g1)
-                                  in Ok (Identity g2) ms (ELit (LStr s),DTyp [] cat []))
-    | otherwise        = TcM (\abstr (Identity g) ms ->
-                                  case Map.lookup cat (cats abstr) of
-                                    Just (_,fns) -> do_rand abstr g ms 1.0 fns
-                                    Nothing      -> Fail (Identity g) (UnknownCat cat))
     where
-      do_rand abstr g ms p []  = Zero
+      do_rand abstr g ms p []   = Zero
-      do_rand abstr g ms p fns = let (d,g')    = randomR (0.0,p) g
+      do_rand abstr g ms p gens = let (d,g')    = randomR (0.0,p) g
-                                     (g1,g2)   = split g'
+                                      (g1,g2)   = split g'
-                                     (p',fn,fns') = hit d fns
+                                      (p',e_ty,gens') = hit d gens
-                                 in Plus (select_helper fn abstr (Identity g1) ms) (do_rand abstr g2 ms (p-p') fns')
+                                  in Plus (Ok (Identity g1) ms e_ty) (do_rand abstr g2 ms (p-p') gens')
 
-      hit :: Double -> [(Double,a)] -> (Double,a,[(Double,a)])
+      hit :: Double -> [(Double,Expr,TType)] -> (Double,(Expr,TType),[(Double,Expr,TType)])
-      hit d (px@(p,x):xs)
+      hit d (gen@(p,e,ty):gens)
-        | d < p     = (p,x,xs)
+        | d < p     = (p,(e,ty),gens)
-        | otherwise = let (p',x',xs') = hit (d-p) xs
+        | otherwise = let (p',e_ty',gens') = hit (d-p) gens
-                      in (p,x',px:xs')
+                      in (p',e_ty',gen:gens')
-
-select_helper fn = unTcM $ do
-  ty <- lookupFunType fn
-  return (EFun fn,ty)

src/runtime/haskell/PGF/TypeCheck.hs

@@ -23,14 +23,14 @@ module PGF.TypeCheck ( checkType, checkExpr, inferExpr
                      , Scope, emptyScope, scopeSize, scopeEnv, addScopedVar
                      , TcM(..), TcResult(..), runTcM, TType(..), Selector(..)
                      , tcExpr, infExpr, eqType, eqValue
-                     , lookupFunType, eval
+                     , lookupFunType, typeGenerators, eval
                      , generateForMetas, generateForForest, checkResolvedMetaStore
                      ) where
 
 import PGF.Data
 import PGF.Expr hiding (eval, apply, value2expr)
 import qualified PGF.Expr as Expr
-import PGF.Macros (typeOfHypo)
+import PGF.Macros (typeOfHypo, cidInt, cidFloat, cidString)
 import PGF.CId
 
 import Data.Map as Map
@@ -93,7 +93,7 @@ data TcResult s a
 
 class Selector s where
   splitSelector :: s -> (s,s)
-  select        :: CId -> Maybe Int -> TcM s (Expr,Type)
+  select        :: CId -> Scope -> Maybe Int -> TcM s (Expr,TType)
 
 instance Monad (TcM s) where
   return x = TcM (\abstr s ms -> Ok s ms x)
@@ -148,6 +148,31 @@ lookupFunType fun = TcM (\abstr s ms -> case Map.lookup fun (funs abstr) of
                                           Just (ty,_,_,_) -> Ok s ms ty
                                           Nothing         -> Fail s (UnknownFun fun))
 
+typeGenerators :: Scope -> CId -> TcM s [(Double,Expr,TType)]
+typeGenerators scope cat = fmap normalize (liftM2 (++) x y)
+  where
+    x = return
+           [(0.25,EVar i,tty) | (i,(_,tty@(TTyp _ (DTyp _ cat' _)))) <- zip [0..] gamma
+                              , cat == cat']
+         where
+           Scope gamma = scope
+
+    y | cat == cidInt    = return [(1.0,ELit (LInt 999),  TTyp [] (DTyp [] cat []))]
+      | cat == cidFloat  = return [(1.0,ELit (LFlt 3.14), TTyp [] (DTyp [] cat []))]
+      | cat == cidString = return [(1.0,ELit (LStr "Foo"),TTyp [] (DTyp [] cat []))]
+      | otherwise        = TcM (\abstr s ms ->
+                                    case Map.lookup cat (cats abstr) of
+                                      Just (_,fns) -> unTcM (mapM helper fns) abstr s ms
+                                      Nothing      -> Fail s (UnknownCat cat))
+
+    helper (p,fn) = do
+      ty <- lookupFunType fn
+      return (p,EFun fn,TTyp [] ty)
+      
+    normalize gens = [(p/s,e,tty) | (p,e,tty) <- gens]
+      where
+        s = sum [p | (p,_,_) <- gens]
+
 emptyMetaStore :: MetaStore s
 emptyMetaStore = IntMap.empty