hopefully complete and correct typechecker in PGF

5 files changed, 619 insertions, 353 deletions

diff --git a/src/PGF/Binary.hs b/src/PGF/Binary.hs
index bd896817f..87d61d1bc 100644
--- a/src/PGF/Binary.hs
+++ b/src/PGF/Binary.hs
@@ -104,20 +104,24 @@ instance Binary Term where
 instance Binary Expr where

   put (EAbs x exp)    = putWord8 0 >> put (x,exp)

   put (EApp e1 e2)    = putWord8 1 >> put (e1,e2)

-  put (EVar   x)      = putWord8 2 >> put x

-  put (ELit (LStr s)) = putWord8 3 >> put s

-  put (ELit (LFlt d)) = putWord8 4 >> put d

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

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

+  put (ELit (LStr s)) = putWord8 2 >> put s

+  put (ELit (LFlt d)) = putWord8 3 >> put d

+  put (ELit (LInt i)) = putWord8 4 >> put i

+  put (EMeta i)       = putWord8 5 >> put i

+  put (EFun  f)       = putWord8 6 >> put f

+  put (EVar  i)       = putWord8 7 >> put i

+  put (ETyped e ty)   = putWord8 8 >> put (e,ty)

   get = do tag <- getWord8

            case tag of

              0 -> liftM2 EAbs get get

              1 -> liftM2 EApp get get

-             2 -> liftM  EVar get

-             3 -> liftM  (ELit . LStr) get

-             4 -> liftM  (ELit . LFlt) get

-             5 -> liftM  (ELit . LInt) get

-             6 -> liftM  EMeta get

+             2 -> liftM  (ELit . LStr) get

+             3 -> liftM  (ELit . LFlt) get

+             4 -> liftM  (ELit . LInt) get

+             5 -> liftM  EMeta get

+             6 -> liftM  EFun get

+             7 -> liftM  EVar get

+             8 -> liftM2 ETyped get get

              _ -> decodingError

 

 instance Binary Patt where

diff --git a/src/PGF/Expr.hs b/src/PGF/Expr.hs
index c22fa8a08..62a97698a 100644
--- a/src/PGF/Expr.hs
+++ b/src/PGF/Expr.hs
@@ -7,12 +7,12 @@ module PGF.Expr(Tree(..), Literal(..),
                 tree2expr, expr2tree, normalForm,

 

                 -- needed in the typechecker

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

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

 

                 MetaId,

 

                 -- helpers

-                pStr,pFactor,

+                pStr,pFactor,freshName,ppMeta

                ) where

 

 import PGF.CId

@@ -20,16 +20,17 @@ import PGF.Type
 

 import Data.Char

 import Data.Maybe

+import Data.List as List

+import Data.Map as Map hiding (showTree)

 import Control.Monad

 import qualified Text.PrettyPrint as PP

 import qualified Text.ParserCombinators.ReadP as RP

-import qualified Data.Map as Map

 

 data Literal = 

    LStr String                      -- ^ string constant

  | LInt Integer                     -- ^ integer constant

  | LFlt Double                      -- ^ floating point constant

- deriving (Eq,Ord)

+ deriving (Eq,Ord,Show)

 

 type MetaId = Int

 

@@ -52,9 +53,10 @@ data Expr =
  | EApp Expr Expr                   -- ^ application

  | ELit Literal                     -- ^ literal

  | EMeta  {-# UNPACK #-} !MetaId    -- ^ meta variable

- | EVar   CId                       -- ^ variable or function reference

- | EPi CId Expr Expr                -- ^ dependent function type

-  deriving (Eq,Ord)

+ | EFun   CId                       -- ^ function or data constructor

+ | EVar   {-# UNPACK #-} !Int       -- ^ variable with de Bruijn index

+ | ETyped Expr Type

+  deriving (Eq,Ord,Show)

 

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

 data Patt =

@@ -94,12 +96,12 @@ readExpr s = case [x | (x,cs) <- RP.readP_to_S pExpr s, all isSpace cs] of
                [x] -> Just x

                _   -> Nothing

 

--- | renders expression as 'String'

-showExpr :: Expr -> String

-showExpr = PP.render . ppExpr 0

-

-instance Show Expr where

-    showsPrec i x = showString (PP.render (ppExpr i x))

+-- | renders expression as 'String'. The list

+-- of identifiers is the list of all free variables

+-- in the expression in order reverse to the order

+-- of binding.

+showExpr :: [CId] -> Expr -> String

+showExpr vars = PP.render . ppExpr 0 vars

 

 instance Read Expr where

     readsPrec _ = RP.readP_to_S pExpr

@@ -124,24 +126,31 @@ pTree isNested = RP.skipSpaces >> (pParen RP.<++ pAbs RP.<++ pApp RP.<++ fmap Li
                   return (Fun f ts)

 

 pExpr :: RP.ReadP Expr

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

+pExpr = pExpr0 >>= optTyped

   where

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

+

     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

+              e  <- pExpr0

               return (foldr EAbs e xs)

 

-pFactor =       fmap EVar  pCId

+    optTyped e = do RP.skipSpaces

+                    RP.char ':'

+                    RP.skipSpaces

+                    ty <- pType

+                    return (ETyped e ty)

+                 RP.<++

+                 return e 

+                 

+pFactor =       fmap EFun  pCId

         RP.<++  fmap ELit  pLit

         RP.<++  fmap EMeta pMeta

         RP.<++  RP.between (RP.char '(') (RP.char ')') pExpr

 

 pMeta = do RP.char '?'

-           cs <- RP.look

-           case cs of

-             (c:_) | isDigit c -> fmap read (RP.munch1 isDigit)

-             _                 -> return 0

+           return 0

 

 pLit :: RP.ReadP Literal

 pLit = pNum RP.<++ liftM LStr pStr

@@ -161,35 +170,37 @@ pStr = RP.char '"' >> (RP.manyTill (pEsc RP.<++ RP.get) (RP.char '"'))
 -----------------------------------------------------

 

 ppTree d (Abs xs t) = ppParens (d > 0) (PP.char '\\' PP.<>

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

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

                                         PP.text "->" PP.<+>

                                         ppTree 0 t)

 ppTree d (Fun f []) = PP.text (prCId f)

-ppTree d (Fun f ts) = ppParens (d > 0) (PP.text (prCId f) PP.<+> PP.hsep (map (ppTree 1) ts))

+ppTree d (Fun f ts) = ppParens (d > 0) (PP.text (prCId f) PP.<+> PP.hsep (List.map (ppTree 1) ts))

 ppTree d (Lit l)    = ppLit l

 ppTree d (Meta n)   = ppMeta 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.<+>

-                                             PP.text "->" PP.<+>

-                                             ppExpr 0 e1)

-                        where

-                          getVars (EAbs x e) = let (xs,e1) = getVars e in (x:xs,e1)

-                          getVars e          = ([],e)

-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)    = ppMeta n

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

-ppExpr d (EPi x e1 e2)= PP.parens (PP.text (prCId x) PP.<+> PP.colon PP.<+> ppExpr 0 e1) PP.<+> PP.text "->" PP.<+> ppExpr 0 e2

-

-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 '_'

+ppExpr :: Int -> [CId] -> Expr -> PP.Doc

+ppExpr d scope (EAbs x e)   = let (xs,e1) = getVars [x] e

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

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

+                                                   PP.text "->" PP.<+>

+                                                   ppExpr 1 (xs++scope) e1)

+                              where

+                                getVars xs (EAbs x e) = getVars (freshName x xs:xs) e

+                                getVars xs e          = (xs,e)

+ppExpr d scope (EApp e1 e2) = ppParens (d > 3) ((ppExpr 3 scope e1) PP.<+> (ppExpr 4 scope e2))

+ppExpr d scope (ELit l)     = ppLit l

+ppExpr d scope (EMeta n)    = ppMeta n

+ppExpr d scope (EFun f)     = PP.text (prCId f)

+ppExpr d scope (EVar i)     = PP.text (prCId (scope !! i))

+ppExpr d scope (ETyped e ty)= ppParens (d > 0) (ppExpr 0 scope e PP.<+> PP.colon PP.<+> ppType 0 scope ty)

+

+ppPatt d scope (PApp f ps) = let (scope',ds) = mapAccumL (ppPatt 2) scope ps

+                             in (scope',ppParens (not (List.null ps) && d > 1) (PP.text (prCId f) PP.<+> PP.hsep ds))

+ppPatt d scope (PLit l)    = (scope,ppLit l)

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

+ppPatt d scope PWild       = (scope,PP.char '_')

 

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

 ppLit (LInt n) = PP.integer n

@@ -203,6 +214,12 @@ ppMeta n
 ppParens True  = PP.parens

 ppParens False = id

 

+freshName :: CId -> [CId] -> CId

+freshName x xs = loop 1 x

+  where

+    loop i y

+      | elem y xs = loop (i+1) (mkCId (show x++"'"++show i))

+      | otherwise = y

 

 -----------------------------------------------------

 -- Conversion Expr <-> Tree

@@ -211,33 +228,38 @@ ppParens False = id
 -- | Converts a tree to expression. The conversion

 -- is always total, every tree is a valid expression.

 tree2expr :: Tree -> Expr

-tree2expr (Fun x ts) = foldl EApp (EVar x) (map tree2expr ts) 

-tree2expr (Lit l)    = ELit l

-tree2expr (Meta n)   = EMeta n

-tree2expr (Abs xs t) = foldr EAbs (tree2expr t) xs

-tree2expr (Var x)    = EVar x

+tree2expr = tree2expr []

+  where

+    tree2expr ys (Fun x ts) = foldl EApp (EFun x) (List.map (tree2expr ys) ts) 

+    tree2expr ys (Lit l)    = ELit l

+    tree2expr ys (Meta n)   = EMeta n

+    tree2expr ys (Abs xs t) = foldr EAbs (tree2expr (reverse xs++ys) t) xs

+    tree2expr ys (Var x)    = case List.lookup x (zip ys [0..]) of

+                                Just i  -> EVar i

+                                Nothing -> error "unknown variable"

 

 -- | Converts an expression to tree. The conversion is only partial.

 -- Variables and meta variables of function type and beta redexes are not allowed.

 expr2tree :: Expr -> Tree

 expr2tree e = abs [] [] e

   where

-    abs ys xs (EAbs x e) = abs ys (x:xs) e

-    abs ys xs e          = case xs of

-                             [] -> app ys [] e

-                             xs -> Abs (reverse xs) (app (xs++ys) [] e)

+    abs ys xs (EAbs x e)      = abs ys (x:xs) e

+    abs ys xs (ETyped e _)    = abs ys xs e

+    abs ys xs e               = case xs of

+                                  [] -> app ys [] e

+                                  xs -> Abs (reverse xs) (app (xs++ys) [] e)

 

-    app xs as (EApp e1 e2)   = app xs ((abs xs [] e2) : as) e1

+    app xs as (EApp e1 e2)    = app xs ((abs xs [] e2) : as) e1

     app xs as (ELit l)

-               | null as     = Lit l

-               | otherwise   = error "literal of function type encountered"

+               | List.null as = Lit l

+               | otherwise    = error "literal of function type encountered"

     app xs as (EMeta n)

-               | null as     = Meta n

-               | otherwise   = error "meta variables of function type are not allowed in trees"

-    app xs as (EAbs x e)     = error "beta redexes are not allowed in trees"

-    app xs as (EVar x)

-               | x `elem` xs = Var x

-               | otherwise   = Fun x as

+               | List.null as = Meta n

+               | otherwise    = error "meta variables of function type are not allowed in trees"

+    app xs as (EAbs x e)      = error "beta redexes are not allowed in trees"

+    app xs as (EVar i)        = Var (xs !! i)

+    app xs as (EFun f)        = Fun f as

+    app xs as (ETyped e _)    = app xs as e

 

 

 -----------------------------------------------------

@@ -245,109 +267,84 @@ expr2tree e = abs [] [] e
 -----------------------------------------------------

 

 -- | Compute an expression to normal form

-normalForm :: Funs -> Expr -> Expr

-normalForm funs e = value2expr 0 (eval funs Map.empty e)

+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 (EVar f)       (map (value2expr i) vs)

-    value2expr i (VGen j vs)               = foldl EApp (EVar (var j)) (map (value2expr i) vs)

-    value2expr i (VMeta j vs)              = foldl EApp (EMeta j)      (map (value2expr i) vs)

-    value2expr i (VSusp j vs k)            = value2expr i (k (VGen j vs))

+    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 (VLit l)                  = ELit l

-    value2expr i (VClosure env (EAbs x e)) = EAbs (var i) (value2expr (i+1) (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

+    value2expr i (VClosure env (EAbs x e)) = EAbs x (value2expr (i+1) (eval funs ((VGen i []):env) e))

 

 data Value

   = VApp CId [Value]

   | VLit Literal

-  | VMeta {-# UNPACK #-} !MetaId [Value]

-  | VGen  {-# UNPACK #-} !MetaId [Value]

-  | VSusp {-# UNPACK #-} !MetaId [Value] (Value -> Value)

+  | VMeta {-# UNPACK #-} !MetaId Env [Value]

+  | VSusp {-# UNPACK #-} !MetaId Env [Value] (Value -> Value)

+  | VGen  {-# UNPACK #-} !Int [Value]

   | VClosure Env Expr

 

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

-type Env  = Map.Map CId Value

+type Env  = [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 (_,a,eqs) -> if a == 0

-                                                                then case eqs of

-                                                                       Equ [] e : _ -> eval funs Map.empty e

-                                                                       _            -> VApp x []

-                                                                else VApp x []

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

+eval funs env (EVar i)     = env !! i

+eval funs env (EFun f)     = case Map.lookup f funs of

+                              Just (_,a,eqs) -> if a == 0

+                                                  then case eqs of

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

+                                                         _            -> VApp f []

+                                                  else VApp f []

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

 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 (EMeta i)    = VMeta i env []

 eval funs env (ELit l)     = VLit l

-eval funs env (EPi x e1 e2)= VClosure env (EPi x e1 e2)

+eval funs env (ETyped e _) = eval funs env e

 

 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  -> applyValue funs env v vs

-                                       Nothing -> case Map.lookup x funs of

-                                                    Just (_,a,eqs) -> if a <= length vs

-                                                                        then let (as,vs') = splitAt a vs

-                                                                             in match funs x eqs as vs'

-                                                                        else VApp x vs

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

+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,eqs) -> if a <= length vs

+                                                           then let (as,vs') = splitAt a vs

+                                                                in match funs f eqs as vs'

+                                                           else VApp f vs

+                                       Nothing      -> error ("unknown function "++prCId 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 (Map.insert x v env) e vs

-apply funs env (EMeta k)    vs     = VMeta k 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

 

-applyValue funs env (VApp f  vs0)             vs     = apply funs env (EVar f) (vs0++vs)

-applyValue funs env (VLit _)                  vs     = error "literal of function type"

-applyValue funs env (VMeta i vs0)             vs     = VMeta i (vs0++vs)

-applyValue funs env (VGen  i vs0)             vs     = VGen  i (vs0++vs)

-applyValue funs env (VSusp i vs0 k)           vs     = VSusp i vs0 (\v -> applyValue funs env (k v) vs)

-applyValue funs _   (VClosure env (EAbs x e)) (v:vs) = apply funs (Map.insert x v env) e vs

+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 (VClosure env (EAbs x e)) (v:vs) = apply funs (v:env) e vs

 

 -----------------------------------------------------

 -- Pattern matching

 -----------------------------------------------------

 

 match :: Funs -> CId -> [Equation] -> [Value] -> [Value] -> Value

-match funs f eqs as0 vs0 =

+match sig f eqs as0 vs0 =

   case eqs of

     []               -> VApp f (as0++vs0)

-    (Equ ps res):eqs -> tryMatches eqs ps as0 res Map.empty

+    (Equ ps res):eqs -> tryMatches eqs ps as0 res []

   where

-    tryMatches eqs []     []     res env = apply funs env res vs0

+    tryMatches eqs []     []     res env = apply sig env res vs0

     tryMatches eqs (p:ps) (a:as) res env = tryMatch p a env

       where

-        tryMatch (PVar x     ) (v           ) env            = tryMatches eqs  ps        as  res (Map.insert x v env)

-        tryMatch (PWild      ) (_           ) env            = tryMatches eqs  ps        as  res env

-        tryMatch (p          ) (VMeta i vs  ) env            = VSusp i vs (\v -> tryMatch p v env)

-        tryMatch (p          ) (VGen  i vs  ) env            = VApp f (as0++vs0)

-        tryMatch (p          ) (VSusp i vs k) env            = VSusp i vs (\v -> tryMatch p (k v) env)

-        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 _             _              env            = match funs f eqs as0 vs0

-

-

------------------------------------------------------

--- Equality checking

------------------------------------------------------

-

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

-eqValue funs k v1 v2 =

-  case (whnf v1,whnf v2) of

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

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

-    (VMeta i vs1, VMeta j vs2) | i  == j   -> concat (zipWith (eqValue funs k) vs1 vs2)

-    (VGen  i vs1, VGen  j vs2) | i  == j   -> concat (zipWith (eqValue funs k) vs1 vs2)

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

-      let v = VGen k []

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

-    _                                      -> [(v1,v2)]

-  where

-    whnf (VClosure env e) = eval funs env e   -- should be removed when the typechecker is improved

-    whnf v                = v

+        tryMatch (PVar x     ) (v                ) env            = tryMatches eqs  ps        as  res (v:env)

+        tryMatch (PWild      ) (_                ) env            = tryMatches eqs  ps        as  res env

+        tryMatch (p          ) (VMeta i envi vs  ) env            = VSusp i envi vs (\v -> tryMatch p v env)

+        tryMatch (p          ) (VGen  i vs       ) env            = VApp f (as0++vs0)

+        tryMatch (p          ) (VSusp i envi vs k) env            = VSusp i envi vs (\v -> tryMatch p (k v) env)

+        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 _             _                   env            = match sig f eqs as0 vs0

 

diff --git a/src/PGF/Expr.hs-boot b/src/PGF/Expr.hs-boot
index 0369be173..21f5f7ef1 100644
--- a/src/PGF/Expr.hs-boot
+++ b/src/PGF/Expr.hs-boot
@@ -1,13 +1,17 @@
 module PGF.Expr where

 

+import PGF.CId

 import qualified Text.PrettyPrint as PP

 import qualified Text.ParserCombinators.ReadP as RP

 

 data Expr

 

-instance Eq  Expr

-instance Ord Expr

+instance Eq   Expr

+instance Ord  Expr

+instance Show Expr

 

 pFactor :: RP.ReadP Expr

 

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

+ppExpr :: Int -> [CId] -> Expr -> PP.Doc

+

+freshName :: CId -> [CId] -> CId
\ No newline at end of file
diff --git a/src/PGF/Type.hs b/src/PGF/Type.hs
index a899e84c2..5ddad6ef0 100644
--- a/src/PGF/Type.hs
+++ b/src/PGF/Type.hs
@@ -5,22 +5,22 @@ module PGF.Type ( Type(..), Hypo(..),
 import PGF.CId

 import {-# SOURCE #-} PGF.Expr

 import Data.Char

+import Data.List

 import qualified Text.PrettyPrint as PP

 import qualified Text.ParserCombinators.ReadP as RP

 import Control.Monad

-import Debug.Trace

 

 -- | To read a type from a 'String', use 'read' or 'readType'.

 data Type =

    DTyp [Hypo] CId [Expr]

-  deriving (Eq,Ord)

+  deriving (Eq,Ord,Show)

 

 -- | 'Hypo' represents a hypothesis in a type i.e. in the type A -> B, A is the hypothesis

 data Hypo =

     Hyp      Type      -- ^ hypothesis without bound variable like in A -> B

   | HypV CId Type      -- ^ hypothesis with bound variable like in (x : A) -> B x

   | HypI CId Type      -- ^ hypothesis with bound implicit variable like in {x : A} -> B x

-  deriving (Eq,Ord)

+  deriving (Eq,Ord,Show)

 

 -- | Reads a 'Type' from a 'String'.

 readType :: String -> Maybe Type

@@ -28,15 +28,12 @@ readType s = case [x | (x,cs) <- RP.readP_to_S pType s, all isSpace cs] of
                [x] -> Just x

                _   -> Nothing

 

-instance Show Type where

-    showsPrec i x = showString (PP.render (ppType i x))

-

-instance Read Type where

-    readsPrec _ = RP.readP_to_S pType

-

--- | renders type as 'String'

-showType :: Type -> String

-showType = PP.render . ppType 0

+-- | renders type as 'String'. The list

+-- of identifiers is the list of all free variables

+-- in the expression in order reverse to the order

+-- of binding.

+showType :: [CId] -> Type -> String

+showType vars = PP.render . ppType 0 vars

 

 pType :: RP.ReadP Type

 pType = do

@@ -72,17 +69,19 @@ pType = do
       args <- RP.sepBy pFactor RP.skipSpaces

       return (cat, args)

 

-ppType :: Int -> Type -> PP.Doc

-ppType d (DTyp ctxt cat args)

-  | null ctxt = ppRes cat args

-  | otherwise = ppParens (d > 0) (foldr ppCtxt (ppRes cat args) ctxt)

+ppType :: Int -> [CId] -> Type -> PP.Doc

+ppType d scope (DTyp hyps cat args)

+  | null hyps = ppRes scope cat args

+  | otherwise = let (scope',hdocs) = mapAccumL ppHypo scope hyps

+                in ppParens (d > 0) (foldr (\hdoc doc -> hdoc PP.<+> PP.text "->" PP.<+> doc) (ppRes scope' cat args) hdocs)

   where

-    ppCtxt hyp doc = ppHypo hyp PP.<+> PP.text "->" PP.<+> doc

-    ppRes cat es = PP.text (prCId cat) PP.<+> PP.hsep (map (ppExpr 2) es)

+    ppRes scope cat es = PP.text (prCId cat) PP.<+> PP.hsep (map (ppExpr 4 scope) es)

 

-ppHypo (Hyp    typ) = ppType 1 typ

-ppHypo (HypV x typ) = PP.parens (PP.text (prCId x) PP.<+> PP.char ':' PP.<+> ppType 0 typ)

-ppHypo (HypI x typ) = PP.braces (PP.text (prCId x) PP.<+> PP.char ':' PP.<+> ppType 0 typ)

+ppHypo scope (Hyp    typ) = (  scope,ppType 1 scope typ)

+ppHypo scope (HypV x typ) = let y = freshName x scope

+                            in (y:scope,PP.parens (PP.text (prCId y) PP.<+> PP.char ':' PP.<+> ppType 0 scope typ))

+ppHypo scope (HypI x typ) = let y = freshName x scope

+                            in (y:scope,PP.braces (PP.text (prCId y) PP.<+> PP.char ':' PP.<+> ppType 0 scope typ))

 

 ppParens :: Bool -> PP.Doc -> PP.Doc

 ppParens True  = PP.parens

diff --git a/src/PGF/TypeCheck.hs b/src/PGF/TypeCheck.hs
index 3fba99302..ddccc2e70 100644
--- a/src/PGF/TypeCheck.hs
+++ b/src/PGF/TypeCheck.hs
@@ -1,201 +1,463 @@
 ----------------------------------------------------------------------
 -- |
--- Module      : TypeCheck
--- Maintainer  : AR
+-- Module      : PGF.TypeCheck
+-- Maintainer  : Krasimir Angelov
 -- Stability   : (stable)
 -- Portability : (portable)
 --
--- type checking in abstract syntax with dependent types.
+-- Type checking in abstract syntax with dependent types.
+-- The type checker also performs renaming and checking for unknown
+-- functions. The variable references are replaced by de Bruijn indices.
 --
--- modified from src GF TC
 -----------------------------------------------------------------------------
 
-module PGF.TypeCheck (
-		   typecheck
-		  ) where
+module PGF.TypeCheck (checkType, checkExpr, inferExpr,
+
+                      ppTcError, TcError(..)
+                     ) where
 
 import PGF.Data
-import PGF.Macros (lookDef,isData)
 import PGF.Expr
+import PGF.Macros (typeOfHypo)
 import PGF.CId
 
-import GF.Data.ErrM
-import qualified Data.Map as Map
-import Control.Monad (liftM2,foldM)
-import Data.List (partition,sort,groupBy)
-
-import Debug.Trace
-
-typecheck :: PGF -> Expr -> [Expr]
-typecheck pgf e = case inferExpr pgf (newMetas e) of
-  Ok e  -> [e]
-  Bad s -> trace s []
-
-inferExpr :: PGF -> Expr -> Err Expr
-inferExpr pgf e = case infer pgf emptyTCEnv e of
-  Ok (e,_,cs) -> let (ms,cs2) = splitConstraints pgf cs in case cs2 of
-    [] -> trace (prConstraints cs ++"\n"++ show ms) $ Ok (metaSubst ms e)
-    _  -> Bad ("Error in tree " ++ showExpr e ++ " :\n  " ++ prConstraints cs2)
-  Bad s -> Bad s
-
-infer :: PGF -> TCEnv -> Expr -> Err (Expr, Value, [(Value,Value)])
-infer pgf tenv@(k,rho,gamma) e = case e of
-   EVar x -> do
-     ty <- lookupEVar pgf tenv x
-     return (e,ty,[])
-
---   EInt i -> return (AInt i, valAbsInt, [])
---   EFloat i -> return (AFloat i, valAbsFloat, [])
---   K i -> return (AStr i, valAbsString, [])
-
-   EApp f t -> do
-    (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)
-	let b' = eval (getFunEnv (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 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
-	let a' = eval (getFunEnv (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)
-      _ -> Bad ("function type expected for " ++ show e)
-    _ -> checkInferExp pgf tenv e typ
-
-getFunEnv abs = Map.union (funs abs) (Map.map (\hypos -> (DTyp hypos cidType [],0,[])) (cats abs))
+import Data.Map as Map
+import Data.IntMap as IntMap
+import Data.Maybe as Maybe
+import Data.List as List
+import Control.Monad
+import Text.PrettyPrint
+
+-----------------------------------------------------
+-- The Scope
+-----------------------------------------------------
+
+data    TType = TTyp Env Type
+newtype Scope = Scope [(CId,TType)]
+
+emptyScope = Scope []
+
+addScopedVar :: CId -> TType -> Scope -> Scope
+addScopedVar x tty (Scope gamma) = Scope ((x,tty):gamma)
+
+-- | returns the type and the De Bruijn index of a local variable
+lookupVar :: CId -> Scope -> Maybe (Int,TType)
+lookupVar x (Scope gamma) = listToMaybe [(i,tty) | ((y,tty),i) <- zip gamma [0..], x == y]
+
+-- | returns the type and the name of a local variable
+getVar :: Int -> Scope -> (CId,TType)
+getVar i (Scope gamma) = gamma !! i
+
+scopeEnv :: Scope -> Env
+scopeEnv (Scope gamma) = let n = length gamma
+                         in [VGen (n-i-1) [] | i <- [0..n-1]]
+
+scopeVars :: Scope -> [CId]
+scopeVars (Scope gamma) = List.map fst gamma
+
+scopeSize :: Scope -> Int
+scopeSize (Scope gamma) = length gamma
+
+-----------------------------------------------------
+-- The Monad
+-----------------------------------------------------
+
+type MetaStore = IntMap MetaValue
+data MetaValue
+  = MUnbound Scope [Expr -> TcM ()]
+  | MBound   Expr
+  | MGuarded Expr  [Expr -> TcM ()] {-# UNPACK #-} !Int   -- the Int is the number of constraints that have to be solved 
+                                                          -- to unlock this meta variable
+
+newtype TcM a = TcM {unTcM :: Abstr -> MetaId -> MetaStore -> TcResult a}
+data TcResult a
+  = Ok {-# UNPACK #-} !MetaId MetaStore a
+  | Fail TcError
+
+instance Monad TcM where
+  return x = TcM (\abstr metaid ms -> Ok metaid ms x)
+  f >>= g  = TcM (\abstr metaid ms -> case unTcM f abstr metaid ms of
+                                        Ok metaid ms x   -> unTcM (g x) abstr metaid ms
+                                        Fail e           -> Fail e)
+
+instance Functor TcM where
+  fmap f x = TcM (\abstr metaid ms -> case unTcM x abstr metaid ms of
+                                        Ok metaid ms x   -> Ok metaid ms (f x)
+                                        Fail e           -> Fail e)
+
+lookupCatHyps :: CId -> TcM [Hypo]
+lookupCatHyps cat = TcM (\abstr metaid ms -> case Map.lookup cat (cats abstr) of
+                                               Just hyps -> Ok metaid ms hyps
+                                               Nothing   -> Fail (UnknownCat cat))
+
+lookupFunType :: CId -> TcM TType
+lookupFunType fun = TcM (\abstr metaid ms -> case Map.lookup fun (funs abstr) of
+                                               Just (ty,_,_) -> Ok metaid ms (TTyp [] ty)
+                                               Nothing       -> Fail (UnknownFun fun))
+
+newMeta :: Scope -> TcM MetaId
+newMeta scope = TcM (\abstr metaid ms -> Ok (metaid+1) (IntMap.insert metaid (MUnbound scope []) ms) metaid)
+
+newGuardedMeta :: Scope -> Expr -> TcM MetaId
+newGuardedMeta scope e = getFuns >>= \funs -> TcM (\abstr metaid ms -> Ok (metaid+1) (IntMap.insert metaid (MGuarded e [] 0) ms) metaid)
+
+getMeta :: MetaId -> TcM MetaValue
+getMeta i = TcM (\abstr metaid ms -> Ok metaid ms $! case IntMap.lookup i ms of
+                                                       Just mv  -> mv)
+setMeta :: MetaId -> MetaValue -> TcM ()
+setMeta i mv = TcM (\abstr metaid ms -> Ok metaid (IntMap.insert i mv ms) ())
+
+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)
+  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) ())
+
+    release = TcM (\abstr metaid ms -> case IntMap.lookup i ms of
+                                         Just (MGuarded e cs x) -> if x == 1
+                                                                     then unTcM (sequence_ [c e | c <- cs]) abstr metaid (IntMap.insert i (MGuarded e [] 0) ms)
+                                                                     else Ok metaid (IntMap.insert i (MGuarded e cs (x-1)) ms) ())
+
+-----------------------------------------------------
+-- Type errors
+-----------------------------------------------------
+
+data TcError
+  = UnknownCat      CId
+  | UnknownFun      CId
+  | WrongCatArgs    Scope Type CId  Int Int
+  | TypeMismatch    Scope Expr Type Type
+  | NotFunType      Scope Expr Type
+  | CannotInferType Scope Expr
+  | UnresolvedMetaVars Scope Expr [MetaId]
+
+ppTcError :: TcError -> Doc
+ppTcError (UnknownCat cat)                = text "Category" <+> text (prCId cat) <+> text "is not in scope"
+ppTcError (UnknownFun fun)                = text "Function" <+> text (prCId fun) <+> text "is not in scope"
+ppTcError (WrongCatArgs scope ty cat m n) =
+   text "Category" <+> text (prCId cat) <+> text "should have" <+> int m <+> text "argument(s), but has been given" <+> int n $$
+   text "In the type:" <+> ppType 0 (scopeVars scope) ty
+ppTcError (TypeMismatch scope e ty1 ty2)  = text "Couldn't match expected type" <+> ppType 0 (scopeVars scope) ty1 $$
+                                            text "       against inferred type" <+> ppType 0 (scopeVars scope) ty2 $$
+                                            text "In the expression:" <+> ppExpr 0 (scopeVars scope) e
+ppTcError (NotFunType scope e ty)         = text "A function type is expected for the expression" <+> ppExpr 0 (scopeVars scope) e <+> text "instead of type" <+> ppType 0 (scopeVars scope) ty
+ppTcError (CannotInferType scope e)       = text "Cannot infer the type of expression" <+> ppExpr 0 (scopeVars scope) e
+ppTcError (UnresolvedMetaVars scope e xs) = text "Meta variable(s)" <+> fsep (List.map ppMeta xs) <+> text "should be resolved" $$
+                                            text "in the expression:" <+> ppExpr 0 (scopeVars scope) e
+
+-----------------------------------------------------
+-- checkType
+-----------------------------------------------------
+
+checkType :: PGF -> Type -> Either TcError Type
+checkType pgf ty = 
+  case unTcM (tcType emptyScope ty >>= refineType) (abstract pgf) 0 IntMap.empty of
+    Ok _ ms ty  -> Right ty
+    Fail err    -> Left  err
+
+tcType :: Scope -> Type -> TcM Type
+tcType scope ty@(DTyp hyps cat es) = do
+  (scope,hyps) <- tcHypos scope hyps
+  c_hyps <- lookupCatHyps cat
+  let m = length es
+      n = length c_hyps
+  if m == n
+    then do (delta,es) <- tcHypoExprs scope [] (zip es c_hyps)
+            return (DTyp hyps cat es)
+    else tcError (WrongCatArgs scope ty cat n m)
+
+tcHypos :: Scope -> [Hypo] -> TcM (Scope,[Hypo])
+tcHypos scope []     = return (scope,[])
+tcHypos scope (h:hs) = do
+  (scope,h ) <- tcHypo  scope h
+  (scope,hs) <- tcHypos scope hs
+  return (scope,h:hs)
+
+tcHypo :: Scope -> Hypo -> TcM (Scope,Hypo)
+tcHypo scope (Hyp    ty) = do
+  ty <- tcType scope ty
+  return (scope,Hyp ty)
+tcHypo scope (HypV x ty) = do
+  ty <- tcType scope ty
+  return (addScopedVar x (TTyp (scopeEnv scope) ty) scope,HypV x ty)
+
+tcHypoExprs :: Scope -> Env -> [(Expr,Hypo)] -> TcM (Env,[Expr])
+tcHypoExprs scope delta []         = return (delta,[])
+tcHypoExprs scope delta ((e,h):xs) = do
+  (delta,e ) <- tcHypoExpr scope delta e h
+  (delta,es) <- tcHypoExprs scope delta xs
+  return (delta,e:es)
+
+tcHypoExpr :: Scope -> Env -> Expr -> Hypo -> TcM (Env,Expr)
+tcHypoExpr scope delta e (Hyp    ty) = do
+  e  <- tcExpr scope e (TTyp delta ty)
+  return (delta,e)
+tcHypoExpr scope delta e (HypV x ty) = do
+  e  <- tcExpr scope e (TTyp delta ty)
+  funs <- getFuns
+  return (eval funs (scopeEnv scope) e:delta,e)
+
+
+-----------------------------------------------------
+-- checkExpr
+-----------------------------------------------------
+
+checkExpr :: PGF -> Expr -> Type -> Either TcError Expr
+checkExpr pgf e ty =
+  case unTcM (do e <- tcExpr emptyScope e (TTyp [] ty)
+                 e <- refineExpr e
+                 checkResolvedMetaStore emptyScope e
+                 return e) (abstract pgf) 0 IntMap.empty of
+    Ok _ ms e  -> Right e
+    Fail err   -> Left err
+
+tcExpr :: Scope -> Expr -> TType -> TcM Expr
+tcExpr scope e0@(EAbs x e) tty =
+  case tty of
+    TTyp delta (DTyp (h:hs) c es) -> do e <- case h of
+                                               Hyp    ty -> tcExpr (addScopedVar x (TTyp delta ty) scope)
+                                                                   e (TTyp delta (DTyp hs c es))
+                                               HypV y ty -> tcExpr (addScopedVar x (TTyp delta ty) scope)
+                                                                   e (TTyp ((VGen (scopeSize scope) []):delta) (DTyp hs c es))
+                                        return (EAbs x e)
+    _                             -> do ty <- evalType (scopeSize scope) tty
+                                        tcError (NotFunType scope e0 ty)
+tcExpr scope (EMeta _) tty = do
+  i <- newMeta scope
+  return (EMeta i)
+tcExpr scope e0        tty = do
+  (e0,tty0) <- infExpr scope e0
+  i <- newGuardedMeta scope e0
+  eqType scope (scopeSize scope) i tty tty0
+  return (EMeta i)
+
+
+-----------------------------------------------------
+-- inferExpr
+-----------------------------------------------------
+
+inferExpr :: PGF -> Expr -> Either TcError (Expr,Type)
+inferExpr pgf e =
+  case unTcM (do (e,tty) <- infExpr emptyScope e
+                 e <- refineExpr e
+                 checkResolvedMetaStore emptyScope e
+                 ty <- evalType 0 tty
+                 return (e,ty)) (abstract pgf) 1 IntMap.empty of
+    Ok _ ms (e,ty) -> Right (e,ty)
+    Fail err       -> Left err
+
+infExpr :: Scope -> Expr -> TcM (Expr,TType)
+infExpr scope e0@(EApp e1 e2) = do
+  (e1,tty1) <- infExpr scope e1
+  case tty1 of
+    (TTyp delta1 (DTyp (h:hs) c es)) -> do (delta1,e2) <- tcHypoExpr scope delta1 e2 h
+                                           return (EApp e1 e2,TTyp delta1 (DTyp hs c es))
+    _                                -> do ty1 <- evalType (scopeSize scope) tty1
+                                           tcError (NotFunType scope e1 ty1)
+infExpr scope e0@(EFun x) = do
+  case lookupVar x scope of
+    Just (i,tty) -> return (EVar i,tty)
+    Nothing      -> do tty <- lookupFunType x
+                       return (e0,tty)
+infExpr scope e0@(EVar i) = do
+  return (e0,snd (getVar i scope))
+infExpr scope e0@(ELit l) = do
+  let cat = case l of
+              LStr _ -> mkCId "String"
+              LInt _ -> mkCId "Int"
+              LFlt _ -> mkCId "Float"
+  return (e0,TTyp [] (DTyp [] cat []))
+infExpr scope (ETyped e ty) = do
+  ty <- tcType scope ty
+  e  <- tcExpr scope e (TTyp (scopeEnv scope) ty)
+  return (ETyped e ty,TTyp (scopeEnv scope) ty)
+infExpr scope e = tcError (CannotInferType scope e)
+
+-----------------------------------------------------
+-- eqType
+-----------------------------------------------------
+
+eqType :: Scope -> Int -> MetaId -> TType -> TType -> TcM ()
+eqType scope k i0 tty1@(TTyp delta1 ty1@(DTyp hyps1 cat1 es1)) tty2@(TTyp delta2 ty2@(DTyp hyps2 cat2 es2))
+  | cat1 == cat2 = do (k,delta1,delta2) <- eqHyps k delta1 hyps1 delta2 hyps2
+                      sequence_ [eqExpr k delta1 e1 delta2 e2 | (e1,e2) <- zip es1 es2]
+  | otherwise    = raiseTypeMatchError
+  where
+    raiseTypeMatchError = do ty1 <- evalType k tty1
+                             ty2 <- evalType k tty2
+                             e   <- refineExpr (EMeta i0)
+                             tcError (TypeMismatch scope e ty1 ty2)
+
+    eqHyps :: Int -> Env -> [Hypo] -> Env -> [Hypo] -> TcM (Int,Env,Env)
+    eqHyps k delta1 []                 delta2 []                 =
+      return (k,delta1,delta2)
+    eqHyps k delta1 (Hyp    ty1 : h1s) delta2 (Hyp    ty2 : h2s) = do
+      eqType scope k i0 (TTyp delta1 ty1) (TTyp delta2 ty2)
+      (k,delta1,delta2) <- eqHyps k delta1 h1s delta2 h2s
+      return (k,delta1,delta2)
+    eqHyps k delta1 (HypV x ty1 : h1s) delta2 (HypV y ty2 : h2s) = do
+      eqType scope k i0 (TTyp delta1 ty1) (TTyp delta2 ty2)
+      (k,delta1,delta2) <- eqHyps (k+1) ((VGen k []):delta1) h1s ((VGen k []):delta2) h2s
+      return (k,delta1,delta2)
+    eqHyps k delta1               h1s  delta2               h2s  = raiseTypeMatchError
+
+    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)
+
+    eqValue :: Int -> Value -> Value -> TcM ()
+    eqValue k v1 v2 = do
+      v1 <- deRef v1
+      v2 <- deRef v2
+      eqValue' k v1 v2
+
+    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)
+                       | otherwise -> return v
+        MUnbound _ _               -> return v
+    deRef v = return v
+
+    eqValue' k (VSusp i env vs1 c)          v2                           = addConstraint i0 i env vs1 (\v1 -> eqValue k (c v1) v2)
+    eqValue' k v1                           (VSusp i env vs2 c)          = addConstraint i0 i env vs2 (\v2 -> eqValue k v1 (c v2))
+    eqValue' k (VMeta i env1 vs1)           (VMeta j env2 vs2) | i  == j = zipWithM_ (eqValue k) vs1 vs2
+    eqValue' k (VMeta i env1 vs1)           v2                           = do (MUnbound scopei cs) <- getMeta i
+                                                                              e2 <- mkLam i scopei env1 vs1 v2
+                                                                              sequence_ [c e2 | c <- cs]
+                                                                              setMeta i (MBound e2)
+    eqValue' k v1                           (VMeta i env2 vs2)           = do (MUnbound scopei cs) <- getMeta i
+                                                                              e1 <- mkLam i scopei env2 vs2 v1
+                                                                              sequence_ [c e1 | c <- cs]
+                                                                              setMeta i (MBound e1)
+    eqValue' k (VApp f1 vs1)                (VApp f2 vs2) | f1 == f2     = zipWithM_ (eqValue k) vs1 vs2
+    eqValue' k (VLit l1)                    (VLit l2    ) | l1 == l2     = return ()
+    eqValue' k (VGen  i vs1)                (VGen  j vs2) | i  == j      = zipWithM_ (eqValue k) vs1 vs2
+    eqValue' k (VClosure env1 (EAbs x1 e1)) (VClosure env2 (EAbs x2 e2)) = let v = VGen k []
+                                                                           in eqExpr (k+1) (v:env1) e1 (v:env2) e2
+    eqValue' k v1                           v2                           = raiseTypeMatchError
+
+    mkLam i scope env vs0 v = do
+      let k  = scopeSize scope
+          vs  = reverse (take k env) ++ vs0
+          xs  = nub [i | VGen i [] <- vs]
+      if length vs == length xs
+        then return ()
+        else raiseTypeMatchError
+      v <- occurCheck i k xs v
+      funs <- getFuns
+      return (addLam vs0 (value2expr funs (length xs) v))
+      where
+        addLam []     e = e
+        addLam (v:vs) e = EAbs var (addLam vs e)
+
+        var = mkCId "v"
+
+    occurCheck i0 k xs (VApp f vs)      = do vs <- mapM (occurCheck i0 k xs) vs
+                                             return (VApp f vs)
+    occurCheck i0 k xs (VLit l)         = return (VLit l)
+    occurCheck i0 k xs (VMeta i env vs) = do if i == i0
+                                               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)
+                                               MUnbound scopei _ | scopeSize scopei > k -> raiseTypeMatchError
+                                                                 | otherwise            -> do vs <- mapM (occurCheck i0 k xs) vs
+                                                                                              return (VMeta i env vs)
+    occurCheck i0 k xs (VSusp i env vs cnt) = do addConstraint i0 i env vs (\v -> occurCheck i0 k xs (cnt v) >> return ())
+                                                 return (VSusp i env vs cnt)
+    occurCheck i0 k xs (VGen  i vs)     = case List.findIndex (==i) xs of
+                                            Just i  -> do vs <- mapM (occurCheck i0 k xs) vs
+                                                          return (VGen i vs)
+                                            Nothing -> raiseTypeMatchError
+    occurCheck i0 k xs (VClosure env e) = do env <- mapM (occurCheck i0 k xs) env
+                                             return (VClosure env e)
+
+
+-----------------------------------------------------------
+-- check for meta variables that still have to be resolved
+-----------------------------------------------------------
+
+checkResolvedMetaStore :: Scope -> Expr -> TcM ()
+checkResolvedMetaStore scope e = TcM (\abstr metaid ms -> 
+  let xs = [i | (i,mv) <- IntMap.toList ms, not (isResolved mv)]
+  in if List.null xs
+       then Ok metaid ms ()
+       else Fail (UnresolvedMetaVars scope e xs))
+  where
+    isResolved (MUnbound _ [])   = True
+    isResolved (MGuarded  _ _ _) = True
+    isResolved (MBound    _)     = True
+    isResolved _                 = False
+
+-----------------------------------------------------
+-- evalType
+-----------------------------------------------------
+
+evalType :: Int -> TType -> TcM Type
+evalType k (TTyp delta ty) = do funs <- getFuns
+                                refineType (evalTy funs k delta ty)
   where
-    cidType = mkCId "Type"
-
-checkInferExp :: PGF -> TCEnv -> Expr -> Value -> Err (Expr, [(Value,Value)])
-checkInferExp pgf tenv@(k,_,_) e typ = do
-  (e',w,cs1) <- infer pgf tenv e
-  let cs2 = eqValue (getFunEnv (abstract pgf)) k w typ
-  return (e',cs1 ++ cs2)
-      
-lookupEVar :: PGF -> TCEnv -> CId -> Err Value
-lookupEVar pgf (_,g,_) x = case Map.lookup x g of
-  Just v -> return v
-  _ -> maybe (Bad "var not found") (return . VClosure eempty . type2expr . (\(a,b,c) -> a)) $ 
-         Map.lookup x (funs (abstract pgf))
-
-type2expr :: Type -> Expr
-type2expr (DTyp hyps cat es) = 
-  foldr (uncurry EPi) (foldl EApp (EVar cat) es) [toPair h | h <- hyps]
+    evalTy sig k delta (DTyp hyps cat es) = 
+      let ((k1,delta1),hyps1) = mapAccumL (evalHypo sig) (k,delta) hyps
+      in DTyp hyps1 cat (List.map (normalForm sig k1 delta1) es)
+    
+    evalHypo sig (k,delta) (Hyp    ty) = ((k,              delta),Hyp    (evalTy sig k delta ty))
+    evalHypo sig (k,delta) (HypV x ty) = ((k+1,(VGen k []):delta),HypV x (evalTy sig k delta ty))
+    evalHypo sig (k,delta) (HypI x ty) = ((k+1,(VGen k []):delta),HypI x (evalTy sig k delta ty))
+
+
+-----------------------------------------------------
+-- refinement
+-----------------------------------------------------
+
+refineExpr :: Expr -> TcM Expr
+refineExpr e = TcM (\abstr metaid ms -> Ok metaid ms (refineExpr_ ms e))
+
+refineExpr_ ms e = refine e
   where
-    toPair (Hyp    t) = (wildCId, type2expr t)
-    toPair (HypV x t) = (x,       type2expr t)
-
-type TCEnv = (Int,Env,Env)
-
-eempty = Map.empty
-eins = Map.insert
-
-emptyTCEnv :: TCEnv
-emptyTCEnv = (0,eempty,eempty)
-
-
--- this is not given in Expr
-prValue = showExpr . value2expr
-
-value2expr v = case v of
-  VApp f vs -> foldl EApp (EVar f) (map value2expr vs)
-  VMeta i vs -> foldl EApp (EMeta i) (map value2expr vs)
-  VClosure g e -> e ----
-  VLit l -> ELit l
-
-prConstraints :: [(Value,Value)] -> String
-prConstraints cs = unwords 
-  ["(" ++ prValue v ++ " <> " ++ prValue w ++ ")" | (v,w) <- cs]
-
--- work more on this: unification, compute,...
-
-{-
-splitConstraints :: PGF -> [(Value,Value)] -> ([(Int,Expr)],[(Value,Value)])
-splitConstraints pgf = mkSplit . partition isSubst . regroup . map reorder . map reduce where
-  reorder (v,w) = case w of
-    VMeta _ _ -> (w,v)
-    _ -> (v,w)
-
-  reduce (v,w) = (whnf v,whnf w)
-
-  whnf (VClosure env e) = eval (getFunEnv (abstract pgf)) env e   -- should be removed when the typechecker is improved
-  whnf v                = v
-
-  regroup = groupBy (\x y -> fst x == fst y) . sort
-
-  isSubst cs@((v,u):_) = case v of
-    VMeta _ _ -> all ((==u) . snd) cs
-    _ -> False
-  mkSplit (ms,cs) = ([(i,value2expr v) | (VMeta i _,v):_ <- ms], concat cs)
--}
-
-splitConstraints :: PGF -> [(Value,Value)] -> ([(Int,Expr)],[(Value,Value)])
-splitConstraints pgf = mkSplit . unifyAll [] . map reduce where
-  reduce (v,w) = (whnf v,whnf w)
-
-  whnf (VClosure env e) = eval (getFunEnv (abstract pgf)) env e -- should be removed when the typechecker is improved
-  whnf v                = v
-  mkSplit (ms,cs) = ([(i,value2expr v) | (i,v) <- ms], cs)
-
-  unifyAll g [] = (g, [])
-  unifyAll g ((a@(s, t)) : l) =
-    let (g1, c) = unifyAll g l
-    in case unify s t g1 of
-         Just g2  -> (g2, c)
-         _        -> (g1, a : c)
-
-  unify e1 e2 g = case (e1, e2) of 
-    (VMeta s _, t) -> do
-      let tg = substMetas g t
-      let sg = maybe e1 id (lookup s g)
-      if null (eqValue (funs (abstract pgf)) 0 sg e1) then extend s tg g else unify sg tg g 
-    (t, VMeta _ _) -> unify e2 e1 g
-    (VApp c as, VApp d bs) | c == d -> 
-       foldM (\ h (a,b) -> unify a b h) g (zip as bs)
-    _ -> Nothing
-
-  extend s t g = case t of
-    VMeta u _ | u == s -> return g  
-    _ | occCheck s t   -> Nothing
-    _                  -> return ((s, t) : g) 
-
-  substMetas subst trm = case trm of
-    VMeta s _ -> maybe trm id (lookup s subst)
-    VApp c vs -> VApp c (map (substMetas subst) vs)
-    _ -> trm
-
-  occCheck s u = case u of
-    VMeta t _ -> s == t
-    VApp c as -> any (occCheck s) as
-    _         -> False
-
-
-metaSubst :: [(Int,Expr)] -> Expr -> Expr
-metaSubst vs exp = case exp of
-  EApp u v  -> EApp (subst u) (subst v)
-  EMeta i   -> maybe exp id $ lookup i vs
-  EPi x a b -> EPi x (subst a) (subst b)
-  EAbs x b  -> EAbs x (subst b)
-  _ -> exp
- where
-  subst = metaSubst vs
-
---- use composOp and state monad...
-newMetas :: Expr -> Expr
-newMetas = fst . metas 0 where
-  metas i exp = case exp of
-    EAbs x e -> let (f,j) = metas i e in (EAbs x f, j)
-    EApp f a -> let (g,j) = metas i f ; (b,k) = metas j a in (EApp g b,k)
-    EMeta _  -> (EMeta i, i+1)
-    _        -> (exp,i)
+    refine (EAbs x e)    = EAbs x (refine e)
+    refine (EApp e1 e2)  = EApp (refine e1) (refine e2)
+    refine (ELit l)      = ELit l
+    refine (EMeta i)     = case IntMap.lookup i ms of
+                             Just (MBound   e    ) -> refine e
+                             Just (MGuarded e _ _) -> refine e
+                             _                     -> EMeta i
+    refine (EFun f)      = EFun f
+    refine (EVar i)      = EVar i
+    refine (ETyped e ty) = ETyped (refine e) (refineType_ ms ty)
+
+refineType :: Type -> TcM Type
+refineType ty = TcM (\abstr metaid ms -> Ok metaid ms (refineType_ ms ty))
+
+refineType_ ms (DTyp hyps cat es) = DTyp (List.map (refineHypo_ ms) hyps) cat (List.map (refineExpr_ ms) es)
+
+refineHypo_ ms (Hyp    ty) = Hyp    (refineType_ ms ty)
+refineHypo_ ms (HypV x ty) = HypV x (refineType_ ms ty)
+refineHypo_ ms (HypI x ty) = HypI x (refineType_ ms ty)
+
+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)          = 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 (VLit l)                  = ELit l
+value2expr sig i (VClosure env (EAbs x e)) = EAbs x (value2expr sig (i+1) (eval sig ((VGen i []):env) e))