support for proof search with high-order functions

1 files changed, 51 insertions, 60 deletions

diff --git a/src/runtime/haskell/PGF/Generate.hs b/src/runtime/haskell/PGF/Generate.hs
index 5ba822b3b..e79b6071f 100644
--- a/src/runtime/haskell/PGF/Generate.hs
+++ b/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
-  (fe,DTyp hypos _ es2) <- select cat dp
+prove dp scope (TTyp env1 (DTyp hypos1 cat es1)) = do
+  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
-    _                         -> return ()
-  (env2,args) <- mkEnv [] hypos
-  vs1 <- mapM (PGF.TypeCheck.eval env1) es1
+    Just 0 | not (null hypos2) -> mzero
+    _                          -> return ()
+  (env2,args) <- mkEnv scope' env2 hypos2
   vs2 <- mapM (PGF.TypeCheck.eval env2) es2
-  sequence_ [eqValue mzero suspend (scopeSize scope) v1 v2 | (v1,v2) <- zip vs1 vs2]
-  es <- mapM descend args
-  return (foldl EApp fe es)
+  sequence_ [eqValue mzero suspend (scopeSize scope') v1 v2 | (v1,v2) <- zip vs1 vs2]
+  es <- mapM (descend scope') args
+  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,[])
-    mkEnv env ((bt,x,ty):hypos) = do
+    abs []                e = e
+    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
-                          e <- case arg of
-                                 Right e  -> return e
-                                 Left tty -> prove dp' scope tty
-                          e <- case bt of
-                                 Implicit -> return (EImplArg e)
-                                 Explicit -> return e
-                          return e
+    descend scope (bt,arg) = do
+      let dp' = fmap (flip (-) 1) dp
+      e <- case arg of
+             Right e  -> return e
+             Left tty -> prove dp' scope tty
+      e <- case bt of
+             Implicit -> return (EImplArg 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
-    | cat == cidInt    = return (ELit (LInt 999),  DTyp [] cat [])
-    | cat == cidFloat  = return (ELit (LFlt 3.14), DTyp [] cat [])
-    | 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))
+  select cat scope dp = do
+    gens <- typeGenerators scope cat
+    TcM (\abstr s ms -> iter ms gens)
     where
-      iter abstr ms []           = Zero
-      iter abstr ms ((_,fn):fns) = Plus (select_helper fn abstr () ms) (iter abstr ms fns)
+      iter ms []              = Zero
+      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
-    | cat == cidInt    = TcM (\abstr (Identity g) ms ->
-                                  let (n,g') = maybe random (\d -> randomR ((-10)*d,10*d)) dp g
-                                  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))
+  select cat scope dp = do
+    gens <- typeGenerators scope cat
+    TcM (\abstr (Identity g) ms -> do_rand abstr g ms 1.0 gens)
     where
-      do_rand abstr g ms p []  = Zero
-      do_rand abstr g ms p fns = let (d,g')    = randomR (0.0,p) g
-                                     (g1,g2)   = split g'
-                                     (p',fn,fns') = hit d fns
-                                 in Plus (select_helper fn abstr (Identity g1) ms) (do_rand abstr g2 ms (p-p') fns')
-
-      hit :: Double -> [(Double,a)] -> (Double,a,[(Double,a)])
-      hit d (px@(p,x):xs)
-        | d < p     = (p,x,xs)
-        | otherwise = let (p',x',xs') = hit (d-p) xs
-                      in (p,x',px:xs')
-
-select_helper fn = unTcM $ do
-  ty <- lookupFunType fn
-  return (EFun fn,ty)
+      do_rand abstr g ms p []   = Zero
+      do_rand abstr g ms p gens = let (d,g')    = randomR (0.0,p) g
+                                      (g1,g2)   = split g'
+                                      (p',e_ty,gens') = hit d gens
+                                  in Plus (Ok (Identity g1) ms e_ty) (do_rand abstr g2 ms (p-p') gens')
+
+      hit :: Double -> [(Double,Expr,TType)] -> (Double,(Expr,TType),[(Double,Expr,TType)])
+      hit d (gen@(p,e,ty):gens)
+        | d < p     = (p,(e,ty),gens)
+        | otherwise = let (p',e_ty',gens') = hit (d-p) gens
+                      in (p',e_ty',gen:gens')