bugfixes in the typechecker and the tree generator

4 files changed, 15 insertions, 6 deletions

diff --git a/src/runtime/haskell/PGF/Data.hs b/src/runtime/haskell/PGF/Data.hs
index e97b8701e..f382601a8 100644
--- a/src/runtime/haskell/PGF/Data.hs
+++ b/src/runtime/haskell/PGF/Data.hs
@@ -1,7 +1,7 @@
 module PGF.Data (module PGF.Data, module PGF.Expr, module PGF.Type) where
 
 import PGF.CId
-import PGF.Expr hiding (Value, Sig, Env, Tree, eval, apply, value2expr)
+import PGF.Expr hiding (Value, Sig, Env, Tree, eval, apply, applyValue, value2expr)
 import PGF.Type
 
 import qualified Data.Map as Map
diff --git a/src/runtime/haskell/PGF/Expr.hs b/src/runtime/haskell/PGF/Expr.hs
index ffc135d96..456518555 100644
--- a/src/runtime/haskell/PGF/Expr.hs
+++ b/src/runtime/haskell/PGF/Expr.hs
@@ -11,7 +11,7 @@ module PGF.Expr(Tree, BindType(..), Expr(..), Literal(..), Patt(..), Equation(..
                 normalForm,

 

                 -- needed in the typechecker

-                Value(..), Env, Sig, eval, apply, value2expr,

+                Value(..), Env, Sig, eval, apply, applyValue, value2expr,

 

                 MetaId,

 

diff --git a/src/runtime/haskell/PGF/Generate.hs b/src/runtime/haskell/PGF/Generate.hs
index 408dcc590..33021066e 100644
--- a/src/runtime/haskell/PGF/Generate.hs
+++ b/src/runtime/haskell/PGF/Generate.hs
@@ -99,9 +99,7 @@ prove dp scope (TTyp env1 (DTyp hypos1 cat es1)) = do
       mv <- getMeta i
       case mv of
         MBound e -> c e
-        MUnbound _ scope tty cs -> do e <- prove dp scope tty
-                                      setMeta i (MBound e)
-                                      sequence_ [c e | c <- (c:cs)]
+        MUnbound x scope tty cs -> setMeta i (MUnbound x scope tty (c:cs))
 
     abs []                e = e
     abs ((bt,x,ty):hypos) e = EAbs bt x (abs hypos e)
diff --git a/src/runtime/haskell/PGF/TypeCheck.hs b/src/runtime/haskell/PGF/TypeCheck.hs
index bc8304a2b..ac9f5b792 100644
--- a/src/runtime/haskell/PGF/TypeCheck.hs
+++ b/src/runtime/haskell/PGF/TypeCheck.hs
@@ -28,7 +28,7 @@ module PGF.TypeCheck ( checkType, checkExpr, inferExpr
                      ) where
 
 import PGF.Data
-import PGF.Expr hiding (eval, apply, value2expr)
+import PGF.Expr hiding (eval, apply, applyValue, value2expr)
 import qualified PGF.Expr as Expr
 import PGF.Macros (typeOfHypo, cidInt, cidFloat, cidString)
 import PGF.CId
@@ -498,6 +498,14 @@ eqValue fail suspend k v1 v2 = do
     eqValue' k (VGen  i vs1)                  (VGen  j vs2)   | i  == j      = zipWithM_ (eqValue fail suspend k) vs1 vs2
     eqValue' k (VClosure env1 (EAbs _ x1 e1)) (VClosure env2 (EAbs _ x2 e2)) = let v = VGen k []
                                                                                in eqExpr fail suspend (k+1) (v:env1) e1 (v:env2) e2
+    eqValue' k (VClosure env1 (EAbs _ x1 e1)) v2                             = let v = VGen k []
+                                                                               in do v1 <- eval (v:env1) e1
+                                                                                     v2 <- applyValue v2 [v]
+                                                                                     eqValue fail suspend (k+1) v1 v2
+    eqValue' k v1                             (VClosure env2 (EAbs _ x2 e2)) = let v = VGen k []
+                                                                               in do v1 <- applyValue v1 [v]
+                                                                                     v2 <- eval (v:env2) e2
+                                                                                     eqValue fail suspend (k+1) v1 v2
     eqValue' k v1                             v2                             = fail
 
     bind i scope cs env vs0 v = do
@@ -649,5 +657,8 @@ eval env e = TcM (\abstr k h ms -> k (Expr.eval (funs abstr,lookupMeta ms) env e
 apply :: Env -> Expr -> [Value] -> TcM s Value
 apply env e vs = TcM (\abstr k h ms -> k (Expr.apply (funs abstr,lookupMeta ms) env e vs) ms)
 
+applyValue :: Value -> [Value] -> TcM s Value
+applyValue v vs = TcM (\abstr k h ms -> k (Expr.applyValue (funs abstr,lookupMeta ms) v vs) ms)
+
 value2expr :: Int -> Value -> TcM s Expr
 value2expr i v = TcM (\abstr k h ms -> k (Expr.value2expr (funs abstr,lookupMeta ms) i v) ms)