mirror of
https://github.com/GrammaticalFramework/gf-core.git
synced 2026-04-09 04:59:31 -06:00
bugfixes in the typechecker and the tree generator
This commit is contained in:
@@ -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
|
||||
|
||||
@@ -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,
|
||||
|
||||
|
||||
@@ -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)
|
||||
|
||||
@@ -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)
|
||||
|
||||
Reference in New Issue
Block a user