From 09da1013f9a14dfa672c8e1adea269fc337aa57c Mon Sep 17 00:00:00 2001 From: krasimir Date: Mon, 22 Feb 2010 15:50:41 +0000 Subject: [PATCH] refactor PGF.Expr and PGF.TypeCheck so that the evaluator always has access to the meta store --- src/runtime/haskell/PGF.hs | 2 +- src/runtime/haskell/PGF/Data.hs | 2 +- src/runtime/haskell/PGF/Expr.hs | 114 ++++++++++-------- src/runtime/haskell/PGF/TypeCheck.hs | 83 ++++++------- .../runtime/typecheck/typecheck.gfs.gold | 2 +- 5 files changed, 104 insertions(+), 99 deletions(-) diff --git a/src/runtime/haskell/PGF.hs b/src/runtime/haskell/PGF.hs index f8c6dfc8c..a2a2154bb 100644 --- a/src/runtime/haskell/PGF.hs +++ b/src/runtime/haskell/PGF.hs @@ -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 diff --git a/src/runtime/haskell/PGF/Data.hs b/src/runtime/haskell/PGF/Data.hs index a23958d82..fe768cd20 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, Env, Tree) +import PGF.Expr hiding (Value, Sig, Env, Tree, eval, apply, 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 5807c1815..7d88eb798 100644 --- a/src/runtime/haskell/PGF/Expr.hs +++ b/src/runtime/haskell/PGF/Expr.hs @@ -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 diff --git a/src/runtime/haskell/PGF/TypeCheck.hs b/src/runtime/haskell/PGF/TypeCheck.hs index 06459b991..85dbb3d3f 100644 --- a/src/runtime/haskell/PGF/TypeCheck.hs +++ b/src/runtime/haskell/PGF/TypeCheck.hs @@ -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)) diff --git a/testsuite/runtime/typecheck/typecheck.gfs.gold b/testsuite/runtime/typecheck/typecheck.gfs.gold index 9630aa3bf..bdc675587 100644 --- a/testsuite/runtime/typecheck/typecheck.gfs.gold +++ b/testsuite/runtime/typecheck/typecheck.gfs.gold @@ -13,7 +13,7 @@ Category unknown_cat is not in scope Cannot infer the type of expression \x -> x A function type is expected for the expression \x -> x instead of type Int Expression: append (succ (succ zero)) (succ zero) (vector (succ (succ zero))) (vector (succ zero)) -Type: Vector (plus (succ (succ zero)) (succ zero)) +Type: Vector (succ (succ (succ zero))) Expression: <\m, n -> vector (plus m n) : (m : Nat) -> (n : Nat) -> Vector (plus m n)> Type: (m : Nat) -> (n : Nat) -> Vector (plus m n)