mirror of
https://github.com/GrammaticalFramework/gf-core.git
synced 2026-04-23 11:42:49 -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
|
module PGF.Data (module PGF.Data, module PGF.Expr, module PGF.Type) where
|
||||||
|
|
||||||
import PGF.CId
|
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 PGF.Type
|
||||||
|
|
||||||
import qualified Data.Map as Map
|
import qualified Data.Map as Map
|
||||||
|
|||||||
@@ -11,7 +11,7 @@ module PGF.Expr(Tree, BindType(..), Expr(..), Literal(..), Patt(..), Equation(..
|
|||||||
normalForm,
|
normalForm,
|
||||||
|
|
||||||
-- needed in the typechecker
|
-- needed in the typechecker
|
||||||
Value(..), Env, Sig, eval, apply, value2expr,
|
Value(..), Env, Sig, eval, apply, applyValue, value2expr,
|
||||||
|
|
||||||
MetaId,
|
MetaId,
|
||||||
|
|
||||||
|
|||||||
@@ -99,9 +99,7 @@ prove dp scope (TTyp env1 (DTyp hypos1 cat es1)) = do
|
|||||||
mv <- getMeta i
|
mv <- getMeta i
|
||||||
case mv of
|
case mv of
|
||||||
MBound e -> c e
|
MBound e -> c e
|
||||||
MUnbound _ scope tty cs -> do e <- prove dp scope tty
|
MUnbound x scope tty cs -> setMeta i (MUnbound x scope tty (c:cs))
|
||||||
setMeta i (MBound e)
|
|
||||||
sequence_ [c e | c <- (c:cs)]
|
|
||||||
|
|
||||||
abs [] e = e
|
abs [] e = e
|
||||||
abs ((bt,x,ty):hypos) e = EAbs bt x (abs hypos e)
|
abs ((bt,x,ty):hypos) e = EAbs bt x (abs hypos e)
|
||||||
|
|||||||
@@ -28,7 +28,7 @@ module PGF.TypeCheck ( checkType, checkExpr, inferExpr
|
|||||||
) where
|
) where
|
||||||
|
|
||||||
import PGF.Data
|
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 qualified PGF.Expr as Expr
|
||||||
import PGF.Macros (typeOfHypo, cidInt, cidFloat, cidString)
|
import PGF.Macros (typeOfHypo, cidInt, cidFloat, cidString)
|
||||||
import PGF.CId
|
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 (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 []
|
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
|
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
|
eqValue' k v1 v2 = fail
|
||||||
|
|
||||||
bind i scope cs env vs0 v = do
|
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 -> 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)
|
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 :: Int -> Value -> TcM s Expr
|
||||||
value2expr i v = TcM (\abstr k h ms -> k (Expr.value2expr (funs abstr,lookupMeta ms) i v) ms)
|
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