From dbe00fd0ebf99f64a9be882ab0756e0d7f535316 Mon Sep 17 00:00:00 2001 From: "kr.angelov" Date: Tue, 30 Aug 2011 11:24:59 +0000 Subject: [PATCH] bugfixes in the typechecker and the tree generator --- src/runtime/haskell/PGF/Data.hs | 2 +- src/runtime/haskell/PGF/Expr.hs | 2 +- src/runtime/haskell/PGF/Generate.hs | 4 +--- src/runtime/haskell/PGF/TypeCheck.hs | 13 ++++++++++++- 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)