refactor the PGF.Expr type and the evaluation of abstract expressions

9 files changed, 157 insertions, 218 deletions

diff --git a/src/PGF/AbsCompute.hs b/src/PGF/AbsCompute.hs
deleted file mode 100644
index 0997ca952..000000000
--- a/src/PGF/AbsCompute.hs
+++ /dev/null
@@ -1,106 +0,0 @@
-----------------------------------------------------------------------
--- |
--- Module      : AbsCompute
--- Maintainer  : AR
--- Stability   : (stable)
--- Portability : (portable)
---
--- computation in abstract syntax with def definitions.
---
--- modified from src GF computation
------------------------------------------------------------------------------
-
-module PGF.AbsCompute (
-		   compute
-		  ) where
-
-import PGF.Data
-import PGF.Macros (lookDef,isData)
-import PGF.Expr
-import PGF.CId
-
-compute :: PGF -> Tree -> Tree
-compute pgf = computeAbsTermIn pgf []
-
-computeAbsTermIn :: PGF -> [CId] -> Tree -> Tree
-computeAbsTermIn pgf vv = expr2tree . compt vv . tree2expr where
-  compt vv t = 
-      let 
-        t'        = beta vv t
-        (yy,f,aa) = exprForm t'
-        vv'       = yy ++ vv
-        aa'       = map (compt vv') aa
-      in 
-      mkAbs yy $ case look f of
-        Left (EEq eqs) -> case match eqs aa' of
-          Just (d,g) -> compt vv' $ subst vv' g d
-          _ -> mkApp f aa'
-        Left (EMeta _) -> mkApp f aa' -- canonical or primitive
-        Left d -> compt vv' $ mkApp d aa'
-        _ -> mkApp f aa' -- literal
-  look f = case f of
-    EVar c -> Left $ lookDef pgf c
-    _ -> Right f
-  match = findMatch pgf
-
-beta :: [CId] -> Expr -> Expr
-beta vv c = case c of
-  EApp f a -> 
-    let (a',f') = (beta vv a, beta vv f) in 
-    case f' of
-      EAbs x b -> beta vv $ subst vv [(x,a')] (beta (x:vv) b) 
-      _        -> (if a'==a && f'==f then id else beta vv) $ EApp f' a'
-  EAbs x b     -> EAbs x (beta (x:vv) b)
-  _            -> c
-
-
-subst :: [CId] -> Subst -> Expr -> Expr
-subst xs g e = case e of
-  EAbs x b -> EAbs x (subst (x:xs) g e) ---- TODO: refresh variables
-  EApp f a -> EApp (substg f) (substg a)
-  EVar x -> maybe e id $ lookup x g
-  _ -> e
- where
-  substg = subst xs g
-
-type Subst = [(CId,Expr)]
-type Patt = Expr
-
-
-exprForm :: Expr -> ([CId],Expr,[Expr])
-exprForm exp = upd ([],exp,[]) where
-  upd (xs,f,es) = case f of
-    EAbs x b -> upd (x:xs,b,es)
-    EApp c a -> upd (xs,c,a:es)
-    _        -> (reverse xs,f,es)
-
-mkAbs xs b = foldr EAbs b xs
-mkApp f es = foldl EApp f es
-
--- special version of pattern matching, to deal with comp under lambda
-
-findMatch :: PGF -> [Equation] -> [Expr] -> Maybe (Expr, Subst)
-findMatch pgf cases terms = case cases of
-  [] -> Nothing
-  (Equ patts _):_ | length patts /= length terms -> Nothing 
-  (Equ patts val):cc -> case mapM tryMatch (zip patts terms) of
-     Just substs -> return (val, concat substs)
-     _           -> findMatch pgf cc terms
- where
-  
-  tryMatch (p,t) = case (exprForm p, exprForm t) of
-    (([],EVar c,[]),_) | constructor c -> if p==t then return [] else Nothing
-    (([],EVar x,[]),_) | notMeta t     -> return [(x,t)]
-    (([],p, pp), ([], f, tt)) | p == f && length pp == length tt -> do
-         matches <- mapM tryMatch (zip pp tt)
-         return (concat matches)
-    _ -> if p==t then return [] else Nothing
-
-  notMeta e = case e of
-    EMeta _  -> False
-    EApp f a -> notMeta f &&  notMeta a  
-    EAbs _ b -> notMeta b
-    _ -> True
-
-  constructor = isData pgf
-
diff --git a/src/PGF/Binary.hs b/src/PGF/Binary.hs
index 9df9be146..2a96f0c91 100644
--- a/src/PGF/Binary.hs
+++ b/src/PGF/Binary.hs
@@ -109,7 +109,6 @@ instance Binary Expr where
   put (ELit (LFlt d)) = putWord8 4 >> put d

   put (ELit (LInt i)) = putWord8 5 >> put i

   put (EMeta i)       = putWord8 6 >> put i

-  put (EEq eqs)       = putWord8 7 >> put eqs

   get = do tag <- getWord8

            case tag of

              0 -> liftM2 EAbs get get

@@ -119,9 +118,25 @@ instance Binary Expr where
              4 -> liftM  (ELit . LFlt) get

              5 -> liftM  (ELit . LInt) get

              6 -> liftM  EMeta get

-             7 -> liftM  EEq get

              _ -> decodingError

-             

+

+instance Binary Patt where

+  put (PApp f ps)     = putWord8 0 >> put (f,ps)

+  put (PVar   x)      = putWord8 1 >> put x

+  put PWild           = putWord8 2

+  put (PLit (LStr s)) = putWord8 3 >> put s

+  put (PLit (LFlt d)) = putWord8 4 >> put d

+  put (PLit (LInt i)) = putWord8 5 >> put i

+  get = do tag <- getWord8

+           case tag of

+             0 -> liftM2 PApp get get

+             1 -> liftM  PVar get

+             2 -> return PWild

+             3 -> liftM  (PLit . LStr) get

+             4 -> liftM  (PLit . LFlt) get

+             5 -> liftM  (PLit . LInt) get

+             _ -> decodingError

+

 instance Binary Equation where

   put (Equ ps e) = put (ps,e)

   get = liftM2 Equ get get

diff --git a/src/PGF/Data.hs b/src/PGF/Data.hs
index 5aba8cdfa..58952dc7d 100644
--- a/src/PGF/Data.hs
+++ b/src/PGF/Data.hs
@@ -24,7 +24,7 @@ data PGF = PGF {
 
 data Abstr = Abstr {
   aflags  :: Map.Map CId String,      -- value of a flag
-  funs    :: Map.Map CId (Type,Expr), -- type and def of a fun
+  funs    :: Map.Map CId (Type,[Equation]), -- type and def of a fun
   cats    :: Map.Map CId [Hypo],      -- context of a cat
   catfuns :: Map.Map CId [CId]        -- funs to a cat (redundant, for fast lookup)
   }
diff --git a/src/PGF/Expr.hs b/src/PGF/Expr.hs
index eee489100..79c88303d 100644
--- a/src/PGF/Expr.hs
+++ b/src/PGF/Expr.hs
@@ -1,13 +1,13 @@
 module PGF.Expr(Tree(..), Literal(..),                

                 readTree, showTree, pTree, ppTree,

 

-                Expr(..), Equation(..),

-                readExpr, showExpr, pExpr, ppExpr,

+                Expr(..), Patt(..), Equation(..),

+                readExpr, showExpr, pExpr, ppExpr, ppPatt,

 

                 tree2expr, expr2tree,

 

                 -- needed in the typechecker

-                Value(..), Env, eval, apply,

+                Value(..), Env, eval, apply, eqValue,

 

                 -- helpers

                 pStr,pFactor,

@@ -17,6 +17,7 @@ module PGF.Expr(Tree(..), Literal(..),
                ) where

 

 import PGF.CId

+import PGF.Type

 

 import Data.Char

 import Data.Maybe

@@ -29,7 +30,7 @@ data Literal =
    LStr String                      -- ^ string constant

  | LInt Integer                     -- ^ integer constant

  | LFlt Double                      -- ^ floating point constant

- deriving (Eq,Ord,Show)

+ deriving (Eq,Ord)

 

 -- | The tree is an evaluated expression in the abstract syntax

 -- of the grammar. The type is especially restricted to not

@@ -53,17 +54,24 @@ data Expr =
  | ELit Literal                     -- ^ literal

  | EMeta  Int                       -- ^ meta variable

  | EVar   CId                       -- ^ variable or function reference

- | EEq [Equation]                   -- ^ lambda function defined as a set of equations with pattern matching

  | EPi CId Expr Expr                -- ^ dependent function type

   deriving (Eq,Ord)

 

+-- | The pattern is used to define equations in the abstract syntax of the grammar.

+data Patt =

+   PApp CId [Patt]                  -- ^ application. The identifier should be constructor i.e. defined with 'data'

+ | PLit Literal                     -- ^ literal

+ | PVar CId                         -- ^ variable

+ | PWild                            -- ^ wildcard

+  deriving (Eq,Ord)

+

 -- | The equation is used to define lambda function as a sequence

 -- of equations with pattern matching. The list of 'Expr' represents

 -- the patterns and the second 'Expr' is the function body for this

 -- equation.

 data Equation =

-   Equ [Expr] Expr

-  deriving (Eq,Ord,Show)

+   Equ [Patt] Expr

+  deriving (Eq,Ord)

 

 -- | parses 'String' as an expression

 readTree :: String -> Maybe Tree

@@ -120,24 +128,13 @@ pTree isNested = RP.skipSpaces >> (pParen RP.<++ pAbs RP.<++ pApp RP.<++ fmap Li
                    return (Meta n)

 

 pExpr :: RP.ReadP Expr

-pExpr = RP.skipSpaces >> (pAbs RP.<++ pTerm RP.<++ pEqs)

+pExpr = RP.skipSpaces >> (pAbs RP.<++ pTerm)

   where

     pTerm   =       fmap (foldl1 EApp) (RP.sepBy1 pFactor RP.skipSpaces)

 

     pAbs = do xs <- RP.between (RP.char '\\') (RP.skipSpaces >> RP.string "->") (RP.sepBy1 (RP.skipSpaces >> pCId) (RP.skipSpaces >> RP.char ','))

               e  <- pExpr

               return (foldr EAbs e xs)

-               

-    pEqs = fmap EEq $

-           RP.between (RP.skipSpaces >> RP.char '{')

-                      (RP.skipSpaces >> RP.char '}')

-                      (RP.sepBy1 (RP.skipSpaces >> pEq) 

-                                 (RP.skipSpaces >> RP.string ";"))

-

-    pEq = do pats <- (RP.sepBy1 pExpr RP.skipSpaces)

-             RP.skipSpaces >> RP.string "=>"

-             e <- pExpr

-             return (Equ pats e)

 

 pFactor =       fmap EVar pCId

         RP.<++  fmap ELit pLit

@@ -176,6 +173,7 @@ ppTree d (Meta n)   = PP.char '?' PP.<> PP.int n
 ppTree d (Var id)   = PP.text (prCId id)

 

 

+ppExpr :: Int -> Expr -> PP.Doc

 ppExpr d (EAbs x e)   = let (xs,e1) = getVars (EAbs x e)

                         in ppParens (d > 0) (PP.char '\\' PP.<>

                                              PP.hsep (PP.punctuate PP.comma (map (PP.text . prCId) xs)) PP.<+>

@@ -188,9 +186,11 @@ ppExpr d (EApp e1 e2) = ppParens (d > 1) ((ppExpr 1 e1) PP.<+> (ppExpr 2 e2))
 ppExpr d (ELit l)     = ppLit l

 ppExpr d (EMeta n)    = PP.char '?' PP.<+> PP.int n

 ppExpr d (EVar f)     = PP.text (prCId f)

-ppExpr d (EEq eqs)    = PP.braces (PP.sep (PP.punctuate PP.semi (map ppEquation eqs)))

 

-ppEquation (Equ pats e) = PP.hsep (map (ppExpr 2) pats) PP.<+> PP.text "=>" PP.<+> ppExpr 0 e

+ppPatt d (PApp f ps) = ppParens (d > 1) (PP.text (prCId f) PP.<+> PP.hsep (map (ppPatt 2) ps))

+ppPatt d (PLit l)    = ppLit l

+ppPatt d (PVar f)    = PP.text (prCId f)

+ppPatt d PWild       = PP.char '_'

 

 ppLit (LStr s) = PP.text (show s)

 ppLit (LInt n) = PP.integer n

@@ -212,46 +212,97 @@ tree2expr (Meta n)   = EMeta n
 tree2expr (Abs xs t) = foldr EAbs (tree2expr t) xs

 tree2expr (Var x)    = EVar x

 

--- | Converts an expression to tree. If the expression

--- contains unevaluated applications they will be applied.

-expr2tree :: Expr -> Tree

-expr2tree e = value2tree (eval Map.empty e) [] []

+-- | Converts an expression to tree. The expression

+-- is first reduced to beta-eta-alfa normal form and

+-- after that converted to tree.

+expr2tree :: Funs -> Expr -> Tree

+expr2tree funs e = value2tree [] (eval funs Map.empty e)

   where

-    value2tree (VApp v1 v2)              xs ts = value2tree v1 xs (value2tree v2 [] []:ts)

-    value2tree (VVar x)                  xs ts = ret xs (fun xs x ts)

-    value2tree (VMeta n)                 xs [] = ret xs (Meta n)

-    value2tree (VLit l)                  xs [] = ret xs (Lit l)

-    value2tree (VClosure env (EAbs x e)) xs [] = value2tree (eval (Map.insert x (VVar x) env) e) (x:xs) []

-    

-    fun xs x ts

-      | x `elem` xs = Var x

-      | otherwise   = Fun x ts

+    value2tree xs (VApp f vs)               = case Map.lookup f funs of

+                                                Just (DTyp hyps _ _,_) -> -- eta conversion

+                                                                          let a1  = length hyps    

+                                                                              a2  = length vs

+                                                                              a   = a1 - a2

+                                                                              i   = length xs

+                                                                              xs' = [var i | i <- [i..i+a-1]]

+                                                                          in ret (reverse xs'++xs)

+                                                                                 (Fun f (map (value2tree []) vs++map Var xs'))

+                                                Nothing                -> error ("unknown variable "++prCId f)

+    value2tree xs (VGen i)                  = ret xs (Var (var i))

+    value2tree xs (VMeta n)                 = ret xs (Meta n)

+    value2tree xs (VLit l)                  = ret xs (Lit l)

+    value2tree xs (VClosure env (EAbs x e)) = let i = length xs

+                                              in value2tree (var i:xs) (eval funs (Map.insert x (VGen i) env) e)

+

+    var i = mkCId ('v':show i)

 

     ret [] t = t

     ret xs t = Abs (reverse xs) t

 

 data Value

-  = VGen Int

-  | VApp Value Value

-  | VVar CId

-  | VMeta Int 

+  = VApp CId [Value]

   | VLit Literal

+  | VMeta Int

+  | VGen Int

   | VClosure Env Expr

- deriving (Show,Eq,Ord)

-

-type Env = Map.Map CId Value

-

-eval :: Env -> Expr -> Value

-eval env (EVar x)     = fromMaybe (VVar x) (Map.lookup x env)

-eval env (EApp e1 e2) = apply (eval env e1) (eval env e2)

-eval env (EAbs x e)   = VClosure env (EAbs x e)

-eval env (EMeta k)    = VMeta k

-eval env (ELit l)     = VLit l

-eval env e            = VClosure env e

-

-apply :: Value -> Value -> Value

-apply (VClosure env (EAbs x e)) v = eval (Map.insert x v env) e

-apply v0                        v = VApp v0 v

+ deriving (Eq,Ord)

+

+type Funs = Map.Map CId (Type,[Equation]) -- type and def of a fun

+type Env  = Map.Map CId Value

+

+eval :: Funs -> Env -> Expr -> Value

+eval funs env (EVar x)     = case Map.lookup x env of

+                               Just v  -> v

+                               Nothing -> case Map.lookup x funs of

+                                            Just (_,eqs) -> case eqs of

+                                                              Equ [] e : _ -> eval funs env e

+                                                              []           -> VApp x []                                                              

+                                            Nothing               -> error ("unknown variable "++prCId x)

+eval funs env (EApp e1 e2) = apply funs env e1 [eval funs env e2]

+eval funs env (EAbs x e)   = VClosure env (EAbs x e)

+eval funs env (EMeta k)    = VMeta k

+eval funs env (ELit l)     = VLit l

+

+apply :: Funs -> Env -> Expr -> [Value] -> Value

+apply funs env e            []     = eval funs env e

+apply funs env (EVar x)     vs     = case Map.lookup x env of

+                                       Just v  -> case (v,vs) of

+                                                    (VClosure env (EAbs x e),v:vs) -> apply funs (Map.insert x v env) e vs

+                                       Nothing -> case Map.lookup x funs of

+                                                    Just (_,eqs) -> case match eqs vs of

+                                                                      Just (e,vs,env) -> apply funs env e vs

+                                                                      Nothing         -> VApp x vs

+                                                    Nothing      -> error ("unknown variable "++prCId x)

+apply funs env (EAbs x e)   (v:vs) = apply funs (Map.insert x v env) e vs

+apply funs env (EApp e1 e2) vs     = apply funs env e1 (eval funs env e2 : vs)

+

+match :: [Equation] -> [Value] -> Maybe (Expr, [Value], Env)

+match eqs vs =

+  case eqs of

+    []               -> Nothing

+    (Equ ps res):eqs -> let (as,vs') = splitAt (length ps) vs

+                        in case zipWithM tryMatch ps as of

+                             Just envs -> Just (res, vs', Map.unions envs)

+                             Nothing   -> match eqs vs

+  where

+    tryMatch p v = case (p, v) of

+      (PVar x,    _         )           -> Just (Map.singleton x v)

+      (PApp f ps, VApp fe vs) | f == fe -> do envs <- zipWithM tryMatch ps vs

+                                              return (Map.unions envs)

+      (PLit l,    VLit le   ) | l == le -> Just Map.empty

+      _                                 -> Nothing

+

+eqValue :: Int -> Value -> Value -> [(Value,Value)]

+eqValue k v1 v2 =

+  case (v1,v2) of

+    (VApp f1 vs1, VApp f2 vs2) | f1 == f2  -> concat (zipWith (eqValue k) vs1 vs2)

+    (VLit l1,     VLit l2    ) | l1 == l2  -> []

+    (VMeta i,     VMeta j    ) | i  == j   -> []

+    (VGen  i,     VGen  j    ) | i  == j   -> []

+    (VClosure env1 (EAbs x1 e1), VClosure env2 (EAbs x2 e2)) ->

+      let v = VGen k

+      in eqValue (k+1) (VClosure (Map.insert x1 v env1) e1) (VClosure (Map.insert x2 v env2) e2)

+    _                                      -> [(v1,v2)]

 

 --- use composOp and state monad...

 newMetas :: Expr -> Expr

diff --git a/src/PGF/Expr.hs-boot b/src/PGF/Expr.hs-boot
new file mode 100644
index 000000000..0369be173
--- /dev/null
+++ b/src/PGF/Expr.hs-boot
@@ -0,0 +1,13 @@
+module PGF.Expr where

+

+import qualified Text.PrettyPrint as PP

+import qualified Text.ParserCombinators.ReadP as RP

+

+data Expr

+

+instance Eq  Expr

+instance Ord Expr

+

+pFactor :: RP.ReadP Expr

+

+ppExpr :: Int -> Expr -> PP.Doc

diff --git a/src/PGF/Macros.hs b/src/PGF/Macros.hs
index 22b96df92..462fa9cba 100644
--- a/src/PGF/Macros.hs
+++ b/src/PGF/Macros.hs
@@ -37,14 +37,15 @@ lookType :: PGF -> CId -> Type
 lookType pgf f = 
   fst $ lookMap (error $ "lookType " ++ show f) f (funs (abstract pgf))
 
-lookDef :: PGF -> CId -> Expr
+lookDef :: PGF -> CId -> [Equation]
 lookDef pgf f = 
   snd $ lookMap (error $ "lookDef " ++ show f) f (funs (abstract pgf))
 
 isData :: PGF -> CId -> Bool
-isData pgf f = case Map.lookup f (funs (abstract pgf)) of
-  Just (_,EMeta 0) -> True ---- the encoding of data constrs
-  _ -> False
+isData pgf f =
+  case Map.lookup f (funs (abstract pgf)) of
+    Just (_,[]) -> True             -- the encoding of data constrs
+    _           -> False
 
 lookValCat :: PGF -> CId -> CId
 lookValCat pgf = valCat . lookType pgf
@@ -120,9 +121,6 @@ contextLength :: Type -> Int
 contextLength ty = case ty of
   DTyp hyps _ _ -> length hyps
 
-primNotion :: Expr
-primNotion = EEq []
-
 term0 :: CId -> Term
 term0 = TM . prCId
 
diff --git a/src/PGF/Paraphrase.hs b/src/PGF/Paraphrase.hs
index 9e0123605..ff718a785 100644
--- a/src/PGF/Paraphrase.hs
+++ b/src/PGF/Paraphrase.hs
@@ -49,13 +49,8 @@ fromDef pgf t@(Fun f ts) = defDown t ++ defUp t where
     [(ps,p) | (p,d@(Fun g ps)) <- equs, g==f, 
               isClosed d || (length equs == 1 && isLinear d)]
 
-  equss = [(f,[(Fun f (map expr2tree ps), expr2tree d) | (Equ ps d) <- eqs]) | 
-                       (f,(_,d)) <- Map.assocs (funs (abstract pgf)), eqs <- defs d]
-
-  defs d = case d of
-    EEq eqs -> [eqs]
-    EMeta _ -> []
-    _      -> [[Equ [] d]]
+  equss = [(f,[(Fun f (map patt2tree ps), expr2tree (funs (abstract pgf)) d) | (Equ ps d) <- eqs]) | 
+                       (f,(_,eqs)) <- Map.assocs (funs (abstract pgf)), not (null eqs)]
 
   trequ s f e = True ----trace (s ++ ": " ++ show f ++ "  " ++ show e) True
 
@@ -86,8 +81,6 @@ isLinear = nodup . vars where
   nodup = all ((<2) . length) . group . sort
 
 
--- special version of AbsCompute.findMatch, working on Tree
-
 match :: [([Tree],Tree)] -> [Tree] -> [(Tree, Subst)]
 match cases terms = case cases of
   [] -> []
@@ -108,3 +101,9 @@ match cases terms = case cases of
     Fun f ts -> all notMeta ts  
     _ -> True
 
+-- | Converts a pattern to tree.
+patt2tree :: Patt -> Tree
+patt2tree (PApp f ps) = Fun f (map patt2tree ps)
+patt2tree (PLit l)    = Lit l
+patt2tree (PVar x)    = Var x
+patt2tree PWild       = Meta 0
diff --git a/src/PGF/Type.hs b/src/PGF/Type.hs
index 8c513ffd4..5b77c8085 100644
--- a/src/PGF/Type.hs
+++ b/src/PGF/Type.hs
@@ -3,7 +3,7 @@ module PGF.Type ( Type(..), Hypo(..),
                   pType, ppType, ppHypo ) where

 

 import PGF.CId

-import PGF.Expr

+import {-# SOURCE #-} PGF.Expr

 import Data.Char

 import qualified Text.PrettyPrint as PP

 import qualified Text.ParserCombinators.ReadP as RP

diff --git a/src/PGF/TypeCheck.hs b/src/PGF/TypeCheck.hs
index 1a2ba334a..7a7a5ccc0 100644
--- a/src/PGF/TypeCheck.hs
+++ b/src/PGF/TypeCheck.hs
@@ -17,7 +17,6 @@ module PGF.TypeCheck (
 import PGF.Data
 import PGF.Macros (lookDef,isData)
 import PGF.Expr
-import PGF.AbsCompute
 import PGF.CId
 
 import GF.Data.ErrM
@@ -29,7 +28,7 @@ import Debug.Trace
 
 typecheck :: PGF -> Tree -> [Tree]
 typecheck pgf t = case inferExpr pgf (newMetas (tree2expr t)) of
-  Ok t  -> [expr2tree t]
+  Ok t  -> [expr2tree (funs (abstract pgf)) t]
   Bad s -> trace s []
 
 inferExpr :: PGF -> Expr -> Err Expr
@@ -50,26 +49,24 @@ infer pgf tenv@(k,rho,gamma) e = case e of
 --   K i -> return (AStr i, valAbsString, [])
 
    EApp f t -> do
-    (f',w,csf) <- infer pgf tenv f 
-    typ <- whnf w
+    (f',typ,csf) <- infer pgf tenv f 
     case typ of
       VClosure env (EPi x a b) -> do
         (a',csa) <- checkExp pgf tenv t (VClosure env a)
-	b' <- whnf $ VClosure (eins x (VClosure rho t) env) b
+	let b' = eval (funs (abstract pgf)) (eins x (VClosure rho t) env) b
 	return $ (EApp f' a', b', csf ++ csa)
       _ -> Bad ("function type expected for function " ++ show f)
    _ -> Bad ("cannot infer type of expression" ++ show e)
 
 
 checkExp :: PGF -> TCEnv -> Expr -> Value -> Err (Expr, [(Value,Value)])
-checkExp pgf tenv@(k,rho,gamma) e ty = do
-  typ <- whnf ty
+checkExp pgf tenv@(k,rho,gamma) e typ = do
   let v = VGen k
   case e of
     EMeta m -> return $ (e,[])
     EAbs x t -> case typ of
       VClosure env (EPi y a b) -> do
-	a' <- whnf $ VClosure env a
+	let a' = eval (funs (abstract pgf)) env a
 	(t',cs) <- checkExp pgf (k+1,eins x v rho, eins x a' gamma) t 
                             (VClosure (eins y v env) b)
 	return (EAbs x t', cs)
@@ -79,7 +76,7 @@ checkExp pgf tenv@(k,rho,gamma) e ty = do
 checkInferExp :: PGF -> TCEnv -> Expr -> Value -> Err (Expr, [(Value,Value)])
 checkInferExp pgf tenv@(k,_,_) e typ = do
   (e',w,cs1) <- infer pgf tenv e
-  cs2 <- eqValue k w typ
+  let cs2 = eqValue k w typ
   return (e',cs1 ++ cs2)
       
 lookupEVar :: PGF -> TCEnv -> CId -> Err Value
@@ -100,40 +97,12 @@ eins = Map.insert
 emptyTCEnv :: TCEnv
 emptyTCEnv = (0,eempty,eempty)
 
-whnf :: Value -> Err Value
-whnf v = case v of
-  VApp u w -> do
-    u' <- whnf u 
-    w' <- whnf w
-    return $ apply u' w'
-  VClosure env e -> return $ eval env e
-  _ -> return v
-
-eqValue :: Int -> Value -> Value -> Err [(Value,Value)]
-eqValue k u1 u2 = do
-  w1 <- whnf u1
-  w2 <- whnf u2 
-  let v = VGen k
-  case (w1,w2) of
-    (VApp f1 a1, VApp f2 a2) -> liftM2 (++) (eqValue k f1 f2) (eqValue k a1 a2)
-    (VClosure env1 (EAbs x1 e1), VClosure env2 (EAbs x2 e2)) ->
-      eqValue (k+1) (VClosure (eins x1 v env1) e1) (VClosure (eins x2 v env2) e2)
-    (VClosure env1 (EPi x1 a1 b1), VClosure env2 (EPi x2 a2 b2)) ->
-      liftM2 (++) 
-        (eqValue k     (VClosure env1 a1) (VClosure env2 a2))
-        (eqValue (k+1) (VClosure (eins x1 v env1) b1) (VClosure (eins x2 v env2) b2))
-    (VGen i, VGen j) -> return [(w1,w2) | i /= j]
-    (VVar i, VVar j) -> return [(w1,w2) | i /= j] 
-    _ -> return [(w1,w2) | w1 /= w2]
--- invariant: constraints are in whnf
-
 
 -- this is not given in Expr
 prValue = showExpr . value2expr
 
 value2expr v = case v of
-  VApp v u -> EApp (value2expr v) (value2expr u)
-  VVar x -> EVar x
+  VApp f vs -> foldl EApp (EVar f) (map value2expr vs)
   VMeta i -> EMeta i
   VClosure g e -> e ----
   VLit l -> ELit l