msyds/gf-core
1
0
Fork 0
forked from GitHub/gf-core
Code Pull Requests Activity

refactor PGF.Expr and PGF.TypeCheck so that the evaluator always has access to the meta store

Browse Source
This commit is contained in:
krasimir
2010-02-22 15:50:41 +00:00
parent 415375f35c
commit 5d2b204246
5 changed files with 104 additions and 99 deletions
Download Patch File Download Diff File Expand all files Collapse all files

2
src/runtime/haskell/PGF.hs
View File

@@ -293,7 +293,7 @@ complete pgf from typ input =
-- | Converts an expression to normal form
compute :: PGF -> Expr -> Expr
compute pgf = PGF.Data.normalForm (funs (abstract pgf)) 0 []
compute pgf = PGF.Data.normalForm (funs (abstract pgf),const Nothing) 0 []
browse :: PGF -> CId -> Maybe (String,[CId],[CId])
browse pgf id = fmap (\def -> (def,producers,consumers)) definition

2
src/runtime/haskell/PGF/Data.hs
View File

@@ -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, Env, Tree)
import PGF.Expr hiding (Value, Sig, Env, Tree, eval, apply, value2expr)
import PGF.Type
import qualified Data.Map as Map

114
src/runtime/haskell/PGF/Expr.hs
View File

@@ -10,7 +10,7 @@ module PGF.Expr(Tree, BindType(..), Expr(..), Literal(..), Patt(..), Equation(..
normalForm,
-- needed in the typechecker
Value(..), Env, Funs, eval, apply,
Value(..), Env, Sig, eval, apply, value2expr,
MetaId,
@@ -262,17 +262,19 @@ freshName x xs0 = loop 1 x
-----------------------------------------------------
-- | Compute an expression to normal form
normalForm :: Funs -> Int -> Env -> Expr -> Expr
normalForm funs k env e = value2expr k (eval funs env e)
where
value2expr i (VApp f vs) = foldl EApp (EFun f) (List.map (value2expr i) vs)
value2expr i (VGen j vs) = foldl EApp (EVar (i-j-1)) (List.map (value2expr i) vs)
value2expr i (VMeta j env vs) = foldl EApp (EMeta j) (List.map (value2expr i) vs)
value2expr i (VSusp j env vs k) = value2expr i (k (VGen j vs))
value2expr i (VConst f vs) = foldl EApp (EFun f) (List.map (value2expr i) vs)
value2expr i (VLit l) = ELit l
value2expr i (VClosure env (EAbs b x e)) = EAbs b x (value2expr (i+1) (eval funs ((VGen i []):env) e))
value2expr i (VImplArg v) = EImplArg (value2expr i v)
normalForm :: Sig -> Int -> Env -> Expr -> Expr
normalForm sig k env e = value2expr sig k (eval sig env e)
value2expr sig i (VApp f vs) = foldl EApp (EFun f) (List.map (value2expr sig i) vs)
value2expr sig i (VGen j vs) = foldl EApp (EVar (i-j-1)) (List.map (value2expr sig i) vs)
value2expr sig i (VMeta j env vs) = case snd sig j of
Just e -> value2expr sig i (apply sig env e vs)
Nothing -> foldl EApp (EMeta j) (List.map (value2expr sig i) vs)
value2expr sig i (VSusp j env vs k) = value2expr sig i (k (VGen j vs))
value2expr sig i (VConst f vs) = foldl EApp (EFun f) (List.map (value2expr sig i) vs)
value2expr sig i (VLit l) = ELit l
value2expr sig i (VClosure env (EAbs b x e)) = EAbs b x (value2expr sig (i+1) (eval sig ((VGen i []):env) e))
value2expr sig i (VImplArg v) = EImplArg (value2expr sig i v)
data Value
= VApp CId [Value]
@@ -284,65 +286,71 @@ data Value
| VClosure Env Expr
| VImplArg Value
type Funs = Map.Map CId (Type,Int,Maybe [Equation]) -- type and def of a fun
type Env = [Value]
type Sig = ( Map.Map CId (Type,Int,Maybe [Equation]) -- type and def of a fun
, Int -> Maybe Expr -- lookup for metavariables
)
type Env = [Value]
eval :: Funs -> Env -> Expr -> Value
eval funs env (EVar i) = env !! i
eval funs env (EFun f) = case Map.lookup f funs of
eval :: Sig -> Env -> Expr -> Value
eval sig env (EVar i) = env !! i
eval sig env (EFun f) = case Map.lookup f (fst sig) of
Just (_,a,meqs) -> case meqs of
Just eqs -> if a == 0
then case eqs of
Equ [] e : _ -> eval funs [] e
Equ [] e : _ -> eval sig [] e
_ -> VConst f []
else VApp f []
Nothing -> VApp f []
Nothing -> error ("unknown function "++showCId f)
eval funs env (EApp e1 e2) = apply funs env e1 [eval funs env e2]
eval funs env (EAbs b x e) = VClosure env (EAbs b x e)
eval funs env (EMeta i) = VMeta i env []
eval funs env (ELit l) = VLit l
eval funs env (ETyped e _) = eval funs env e
eval funs env (EImplArg e) = VImplArg (eval funs env e)
eval sig env (EApp e1 e2) = apply sig env e1 [eval sig env e2]
eval sig env (EAbs b x e) = VClosure env (EAbs b x e)
eval sig env (EMeta i) = case snd sig i of
Just e -> eval sig env e
Nothing -> VMeta i env []
eval sig env (ELit l) = VLit l
eval sig env (ETyped e _) = eval sig env e
eval sig env (EImplArg e) = VImplArg (eval sig env e)
apply :: Funs -> Env -> Expr -> [Value] -> Value
apply funs env e [] = eval funs env e
apply funs env (EVar i) vs = applyValue funs (env !! i) vs
apply funs env (EFun f) vs = case Map.lookup f funs of
Just (_,a,meqs) -> case meqs of
Just eqs -> if a <= length vs
then match funs f eqs vs
else VApp f vs
Nothing -> VApp f vs
Nothing -> error ("unknown function "++showCId f)
apply funs env (EApp e1 e2) vs = apply funs env e1 (eval funs env e2 : vs)
apply funs env (EAbs _ x e) (v:vs) = apply funs (v:env) e vs
apply funs env (EMeta i) vs = VMeta i env vs
apply funs env (ELit l) vs = error "literal of function type"
apply funs env (ETyped e _) vs = apply funs env e vs
apply funs env (EImplArg _) vs = error "implicit argument in function position"
apply :: Sig -> Env -> Expr -> [Value] -> Value
apply sig env e [] = eval sig env e
apply sig env (EVar i) vs = applyValue sig (env !! i) vs
apply sig env (EFun f) vs = case Map.lookup f (fst sig) of
Just (_,a,meqs) -> case meqs of
Just eqs -> if a <= length vs
then match sig f eqs vs
else VApp f vs
Nothing -> VApp f vs
Nothing -> error ("unknown function "++showCId f)
apply sig env (EApp e1 e2) vs = apply sig env e1 (eval sig env e2 : vs)
apply sig env (EAbs _ x e) (v:vs) = apply sig (v:env) e vs
apply sig env (EMeta i) vs = case snd sig i of
Just e -> apply sig env e vs
Nothing -> VMeta i env vs
apply sig env (ELit l) vs = error "literal of function type"
apply sig env (ETyped e _) vs = apply sig env e vs
apply sig env (EImplArg _) vs = error "implicit argument in function position"
applyValue funs v [] = v
applyValue funs (VApp f vs0) vs = apply funs [] (EFun f) (vs0++vs)
applyValue funs (VLit _) vs = error "literal of function type"
applyValue funs (VMeta i env vs0) vs = VMeta i env (vs0++vs)
applyValue funs (VGen i vs0) vs = VGen i (vs0++vs)
applyValue funs (VSusp i env vs0 k) vs = VSusp i env vs0 (\v -> applyValue funs (k v) vs)
applyValue funs (VConst f vs0) vs = VConst f (vs0++vs)
applyValue funs (VClosure env (EAbs b x e)) (v:vs) = apply funs (v:env) e vs
applyValue funs (VImplArg _) vs = error "implicit argument in function position"
applyValue sig v [] = v
applyValue sig (VApp f vs0) vs = apply sig [] (EFun f) (vs0++vs)
applyValue sig (VLit _) vs = error "literal of function type"
applyValue sig (VMeta i env vs0) vs = VMeta i env (vs0++vs)
applyValue sig (VGen i vs0) vs = VGen i (vs0++vs)
applyValue sig (VSusp i env vs0 k) vs = VSusp i env vs0 (\v -> applyValue sig (k v) vs)
applyValue sig (VConst f vs0) vs = VConst f (vs0++vs)
applyValue sig (VClosure env (EAbs b x e)) (v:vs) = apply sig (v:env) e vs
applyValue sig (VImplArg _) vs = error "implicit argument in function position"
-----------------------------------------------------
-- Pattern matching
-----------------------------------------------------
match :: Funs -> CId -> [Equation] -> [Value] -> Value
match funs f eqs as0 =
match :: Sig -> CId -> [Equation] -> [Value] -> Value
match sig f eqs as0 =
case eqs of
[] -> VConst f as0
(Equ ps res):eqs -> tryMatches eqs ps as0 res []
where
tryMatches eqs [] as res env = apply funs env res as
tryMatches eqs [] as res env = apply sig env res as
tryMatches eqs (p:ps) (a:as) res env = tryMatch p a env
where
tryMatch (PVar x ) (v ) env = tryMatches eqs ps as res (v:env)
@@ -354,5 +362,5 @@ match funs f eqs as0 =
tryMatch (PApp f1 ps1) (VApp f2 vs2 ) env | f1 == f2 = tryMatches eqs (ps1++ps) (vs2++as) res env
tryMatch (PLit l1 ) (VLit l2 ) env | l1 == l2 = tryMatches eqs ps as res env
tryMatch (PImplArg p ) (VImplArg v ) env = tryMatch p v env
tryMatch _ _ env = match funs f eqs as0
tryMatch _ _ env = match sig f eqs as0

83
src/runtime/haskell/PGF/TypeCheck.hs
View File

@@ -17,7 +17,8 @@ module PGF.TypeCheck (checkType, checkExpr, inferExpr,
) where
import PGF.Data
import PGF.Expr
import PGF.Expr hiding (eval, apply, value2expr)
import qualified PGF.Expr as Expr
import PGF.Macros (typeOfHypo)
import PGF.CId
@@ -107,21 +108,25 @@ getMeta i = TcM (\abstr metaid ms -> Ok metaid ms $! case IntMap.lookup i ms of
setMeta :: MetaId -> MetaValue -> TcM ()
setMeta i mv = TcM (\abstr metaid ms -> Ok metaid (IntMap.insert i mv ms) ())
lookupMeta ms i =
case IntMap.lookup i ms of
Just (MBound t) -> Just t
Just (MGuarded t _ x) | x == 0 -> Just t
| otherwise -> Nothing
Just (MUnbound _ _) -> Nothing
Nothing -> Nothing
tcError :: TcError -> TcM a
tcError e = TcM (\abstr metaid ms -> Fail e)
getFuns :: TcM Funs
getFuns = TcM (\abstr metaid ms -> Ok metaid ms (funs abstr))
addConstraint :: MetaId -> MetaId -> Env -> [Value] -> (Value -> TcM ()) -> TcM ()
addConstraint i j env vs c = do
funs <- getFuns
mv <- getMeta j
case mv of
MUnbound scope cs -> addRef >> setMeta j (MUnbound scope ((\e -> release >> c (apply funs env e vs)) : cs))
MBound e -> c (apply funs env e vs)
MGuarded e cs x | x == 0 -> c (apply funs env e vs)
| otherwise -> addRef >> setMeta j (MGuarded e ((\e -> release >> c (apply funs env e vs)) : cs) x)
MUnbound scope cs -> addRef >> setMeta j (MUnbound scope ((\e -> release >> apply env e vs >>= c) : cs))
MBound e -> apply env e vs >>= c
MGuarded e cs x | x == 0 -> apply env e vs >>= c
| otherwise -> addRef >> setMeta j (MGuarded e ((\e -> release >> apply env e vs >>= c) : cs) x)
where
addRef = TcM (\abstr metaid ms -> case IntMap.lookup i ms of
Just (MGuarded e cs x) -> Ok metaid (IntMap.insert i (MGuarded e cs (x+1)) ms) ())
@@ -210,10 +215,10 @@ tcCatArgs scope [] delta [] ty0 n m = return (del
tcCatArgs scope (EImplArg e:es) delta ((Explicit,x,ty):hs) ty0 n m = tcError (UnexpectedImplArg (scopeVars scope) e)
tcCatArgs scope (EImplArg e:es) delta ((Implicit,x,ty):hs) ty0 n m = do
e <- tcExpr scope e (TTyp delta ty)
funs <- getFuns
(delta,es) <- if x == wildCId
then tcCatArgs scope es delta hs ty0 n m
else tcCatArgs scope es (eval funs (scopeEnv scope) e:delta) hs ty0 n m
then tcCatArgs scope es delta hs ty0 n m
else do v <- eval (scopeEnv scope) e
tcCatArgs scope es (v:delta) hs ty0 n m
return (delta,EImplArg e:es)
tcCatArgs scope es delta ((Implicit,x,ty):hs) ty0 n m = do
i <- newMeta scope
@@ -223,10 +228,10 @@ tcCatArgs scope es delta ((Implicit,x,ty):hs) ty0 n m = do
return (delta,EImplArg (EMeta i) : es)
tcCatArgs scope (e:es) delta ((Explicit,x,ty):hs) ty0 n m = do
e <- tcExpr scope e (TTyp delta ty)
funs <- getFuns
(delta,es) <- if x == wildCId
then tcCatArgs scope es delta hs ty0 n m
else tcCatArgs scope es (eval funs (scopeEnv scope) e:delta) hs ty0 n m
else do v <- eval (scopeEnv scope) e
tcCatArgs scope es (v:delta) hs ty0 n m
return (delta,e:es)
tcCatArgs scope _ delta _ ty0@(DTyp _ cat _) n m = do
tcError (WrongCatArgs (scopeVars scope) ty0 cat n m)
@@ -334,16 +339,16 @@ tcArg scope e1 e2 delta ty0@(DTyp [] c es) = do
tcArg scope e1 (EImplArg e2) delta ty0@(DTyp ((Explicit,x,ty):hs) c es) = tcError (UnexpectedImplArg (scopeVars scope) e2)
tcArg scope e1 (EImplArg e2) delta ty0@(DTyp ((Implicit,x,ty):hs) c es) = do
e2 <- tcExpr scope e2 (TTyp delta ty)
funs <- getFuns
if x == wildCId
then return (EApp e1 (EImplArg e2), delta,DTyp hs c es)
else return (EApp e1 (EImplArg e2),eval funs (scopeEnv scope) e2:delta,DTyp hs c es)
else do v2 <- eval (scopeEnv scope) e2
return (EApp e1 (EImplArg e2),v2:delta,DTyp hs c es)
tcArg scope e1 e2 delta ty0@(DTyp ((Explicit,x,ty):hs) c es) = do
e2 <- tcExpr scope e2 (TTyp delta ty)
funs <- getFuns
if x == wildCId
then return (EApp e1 e2, delta,DTyp hs c es)
else return (EApp e1 e2,eval funs (scopeEnv scope) e2:delta,DTyp hs c es)
then return (EApp e1 e2,delta,DTyp hs c es)
else do v2 <- eval (scopeEnv scope) e2
return (EApp e1 e2,v2:delta,DTyp hs c es)
tcArg scope e1 e2 delta ty0@(DTyp ((Implicit,x,ty):hs) c es) = do
i <- newMeta scope
if x == wildCId
@@ -379,8 +384,9 @@ eqType scope k i0 tty1@(TTyp delta1 ty1@(DTyp hyps1 cat1 es1)) tty2@(TTyp delta2
eqExpr :: Int -> Env -> Expr -> Env -> Expr -> TcM ()
eqExpr k env1 e1 env2 e2 = do
funs <- getFuns
eqValue k (eval funs env1 e1) (eval funs env2 e2)
v1 <- eval env1 e1
v2 <- eval env2 e2
eqValue k v1 v2
eqValue :: Int -> Value -> Value -> TcM ()
eqValue k v1 v2 = do
@@ -390,10 +396,9 @@ eqType scope k i0 tty1@(TTyp delta1 ty1@(DTyp hyps1 cat1 es1)) tty2@(TTyp delta2
deRef v@(VMeta i env vs) = do
mv <- getMeta i
funs <- getFuns
case mv of
MBound e -> deRef (apply funs env e vs)
MGuarded e _ x | x == 0 -> deRef (apply funs env e vs)
MBound e -> apply env e vs
MGuarded e _ x | x == 0 -> apply env e vs
| otherwise -> return v
MUnbound _ _ -> return v
deRef v = return v
@@ -440,10 +445,9 @@ eqType scope k i0 tty1@(TTyp delta1 ty1@(DTyp hyps1 cat1 es1)) tty2@(TTyp delta2
then raiseTypeMatchError
else return ()
mv <- getMeta i
funs <- getFuns
case mv of
MBound e -> occurCheck i0 k xs (apply funs env e vs)
MGuarded e _ _ -> occurCheck i0 k xs (apply funs env e vs)
MBound e -> apply env e vs >>= occurCheck i0 k xs
MGuarded e _ _ -> apply env e vs >>= occurCheck i0 k xs
MUnbound scopei _ | scopeSize scopei > k -> raiseTypeMatchError
| otherwise -> do vs <- mapM (occurCheck i0 k xs) vs
return (VMeta i env vs)
@@ -480,12 +484,11 @@ checkResolvedMetaStore scope e = TcM (\abstr metaid ms ->
-----------------------------------------------------
evalType :: Int -> TType -> TcM Type
evalType k (TTyp delta ty) = do funs <- getFuns
evalTy funs k delta ty
evalType k (TTyp delta ty) = evalTy funs k delta ty
where
evalTy sig k delta (DTyp hyps cat es) = do
(k,delta,hyps) <- evalHypos sig k delta hyps
es <- mapM (value2expr k . eval sig delta) es
es <- mapM (\e -> eval delta e >>= value2expr k) es
return (DTyp hyps cat es)
evalHypos sig k delta [] = return (k,delta,[])
@@ -523,17 +526,11 @@ refineType ty = TcM (\abstr metaid ms -> Ok metaid ms (refineType_ ms ty))
refineType_ ms (DTyp hyps cat es) = DTyp [(b,x,refineType_ ms ty) | (b,x,ty) <- hyps] cat (List.map (refineExpr_ ms) es)
eval :: Env -> Expr -> TcM Value
eval env e = TcM (\abstr metaid ms -> Ok metaid ms (Expr.eval (funs abstr,lookupMeta ms) env e))
apply :: Env -> Expr -> [Value] -> TcM Value
apply env e vs = TcM (\abstr metaid ms -> Ok metaid ms (Expr.apply (funs abstr,lookupMeta ms) env e vs))
value2expr :: Int -> Value -> TcM Expr
value2expr i v = TcM (\abstr metaid ms -> Ok metaid ms (value2expr ms (funs abstr) i v))
where
value2expr ms sig i (VApp f vs) = foldl EApp (EFun f) (List.map (value2expr ms sig i) vs)
value2expr ms sig i (VGen j vs) = foldl EApp (EVar (i-j-1)) (List.map (value2expr ms sig i) vs)
value2expr ms sig i (VConst f vs) = foldl EApp (EFun f) (List.map (value2expr ms sig i) vs)
value2expr ms sig i (VMeta j env vs) = case IntMap.lookup j ms of
Just (MBound e ) -> value2expr ms sig i (apply sig env e vs)
Just (MGuarded e _ _) -> value2expr ms sig i (apply sig env e vs)
_ -> foldl EApp (EMeta j) (List.map (value2expr ms sig i) vs)
value2expr ms sig i (VSusp j env vs k) = value2expr ms sig i (k (VGen j vs))
value2expr ms sig i (VLit l) = ELit l
value2expr ms sig i (VClosure env (EAbs b x e)) = EAbs b x (value2expr ms sig (i+1) (eval sig ((VGen i []):env) e))
value2expr ms sig i (VImplArg v) = EImplArg (value2expr ms sig i v)
value2expr i v = TcM (\abstr metaid ms -> Ok metaid ms (Expr.value2expr (funs abstr,lookupMeta ms) i v))

2
testsuite/runtime/typecheck/typecheck.gfs.gold
View File

@@ -13,7 +13,7 @@ Category unknown_cat is not in scope
Couldn't match expected type Int -> Int
against inferred type Int
In the expression: 1
unknown category of function identifier unknown_fun