change the data types and the syntax in PGF to match the new syntax for implict arguments

14 files changed, 168 insertions, 198 deletions

diff --git a/src/GF/Command/Interpreter.hs b/src/GF/Command/Interpreter.hs
index 17ff6aa29..ff84da8a3 100644
--- a/src/GF/Command/Interpreter.hs
+++ b/src/GF/Command/Interpreter.hs
@@ -74,7 +74,7 @@ appCommand xs c@(Command i os arg) = case arg of
   _       -> c
  where
   app e = case e of
-    EAbs x e   -> EAbs x (app e)
+    EAbs b x e -> EAbs b x (app e)
     EApp e1 e2 -> EApp (app e1) (app e2)
     ELit l     -> ELit l
     EMeta i    -> xs !! i
diff --git a/src/GF/Command/TreeOperations.hs b/src/GF/Command/TreeOperations.hs
index 73cef05b2..941f03782 100644
--- a/src/GF/Command/TreeOperations.hs
+++ b/src/GF/Command/TreeOperations.hs
@@ -27,6 +27,6 @@ allTreeOps pgf = [
 smallest :: [Expr] -> [Expr]
 smallest = sortBy (\t u -> compare (size t) (size u)) where
   size t = case t of
-    EAbs _ e -> size e + 1
+    EAbs _ _ e -> size e + 1
     EApp e1 e2 -> size e1 + size e2 + 1
     _ -> 1
diff --git a/src/GF/Compile/GFCCtoProlog.hs b/src/GF/Compile/GFCCtoProlog.hs
index a31fe4b84..702d4afe5 100644
--- a/src/GF/Compile/GFCCtoProlog.hs
+++ b/src/GF/Compile/GFCCtoProlog.hs
@@ -19,7 +19,7 @@ import GF.Text.UTF8
 
 import qualified Data.Map as Map
 import Data.Char (isAlphaNum, isAsciiLower, isAsciiUpper, ord)
-import Data.List (isPrefixOf)
+import Data.List (isPrefixOf,mapAccumL)
 
 grammar2prolog, grammar2prolog_abs :: PGF -> String
 -- Most prologs have problems with UTF8 encodings, so we skip that:
@@ -67,7 +67,7 @@ plAbstract (name, Abstr aflags funs cats _catfuns) =
 
 plCat :: (CId, [Hypo]) -> String
 plCat (cat, hypos) = plFact "cat" (plTypeWithHypos typ) 
-    where ((_,subst), hypos') = alphaConvert emptyEnv hypos
+    where ((_,subst), hypos') = mapAccumL alphaConvertHypo emptyEnv hypos
           args = reverse [EFun x | (_,x) <- subst]
           typ = DTyp hypos' cat args
 
@@ -76,7 +76,7 @@ plFun (fun, (typ,_,_)) = plFact "fun" (plp fun : plTypeWithHypos typ')
     where typ' = snd $ alphaConvert emptyEnv typ
 
 plTypeWithHypos :: Type -> [String]
-plTypeWithHypos (DTyp hypos cat args) = [plTerm (plp cat) (map plp args), plp hypos]
+plTypeWithHypos (DTyp hypos cat args) = [plTerm (plp cat) (map plp args), plList (map (\(_,x,ty) -> plOper ":" (plp x) (plp ty)) hypos)]
 
 plFundef :: (CId, (Type,Int,[Equation])) -> [String]
 plFundef (fun, (_,_,[])) = []
@@ -110,17 +110,12 @@ plConcrete (cncname, Concr cflags lins opers lincats lindefs
 
 instance PLPrint Type where
     plp (DTyp hypos cat args) | null hypos = result
-                              | otherwise  = plOper " -> " (plp hypos) result
+                              | otherwise  = plOper " -> " (plList (map (\(_,x,ty) -> plOper ":" (plp x) (plp ty)) hypos)) result
         where result = plTerm (plp cat) (map plp args)
 
-instance PLPrint Hypo where
-    plp (Hyp      typ) = plOper ":" (plp wildCId) (plp typ)
-    plp (HypI var typ) = plOper ":" (plp var) (plp typ)
-    plp (HypV var typ) = plOper ":" (plp var) (plp typ)
-
 instance PLPrint Expr where
     plp (EFun x)    = plp x
-    plp (EAbs x e)  = plOper "^" (plp x) (plp e)
+    plp (EAbs _ x e)= plOper "^" (plp x) (plp e)
     plp (EApp e e') = plOper " * " (plp e) (plp e')
     plp (ELit lit)  = plp lit
     plp (EMeta n)   = "Meta_" ++ show n
@@ -259,21 +254,15 @@ instance AlphaConvert a => AlphaConvert [a] where
 instance AlphaConvert Type where
     alphaConvert env@(_,subst) (DTyp hypos cat args) 
         = ((ctr,subst), DTyp hypos' cat args')
-        where (env',   hypos') = alphaConvert env hypos
+        where (env',   hypos') = mapAccumL alphaConvertHypo env hypos
               ((ctr,_), args') = alphaConvert env' args
 
-instance AlphaConvert Hypo where
-    alphaConvert env (Hyp typ) = ((ctr+1,subst), Hyp typ')
-        where ((ctr,subst), typ') = alphaConvert env typ
-    alphaConvert env (HypI x typ) = ((ctr+1,(x,x'):subst), HypI x' typ')
-        where ((ctr,subst), typ') = alphaConvert env typ
-              x' = createLogicalVariable ctr
-    alphaConvert env (HypV x typ) = ((ctr+1,(x,x'):subst), HypV x' typ')
-        where ((ctr,subst), typ') = alphaConvert env typ
-              x' = createLogicalVariable ctr
+alphaConvertHypo env (b,x,typ) = ((ctr+1,(x,x'):subst), (b,x',typ'))
+    where ((ctr,subst), typ') = alphaConvert env typ
+          x' = createLogicalVariable ctr
 
 instance AlphaConvert Expr where
-    alphaConvert (ctr,subst) (EAbs x e) = ((ctr',subst), EAbs x' e')
+    alphaConvert (ctr,subst) (EAbs b x e) = ((ctr',subst), EAbs b x' e')
         where ((ctr',_), e') = alphaConvert (ctr+1,(x,x'):subst) e
               x' = createLogicalVariable ctr
     alphaConvert env (EApp e1 e2) = (env'', EApp e1' e2')
diff --git a/src/GF/Compile/GrammarToGFCC.hs b/src/GF/Compile/GrammarToGFCC.hs
index b285faa81..a2b03ab63 100644
--- a/src/GF/Compile/GrammarToGFCC.hs
+++ b/src/GF/Compile/GrammarToGFCC.hs
@@ -129,7 +129,7 @@ mkExp :: [Ident] -> A.Term -> C.Expr
 mkExp scope t = case GM.termForm t of
     Ok (xs,c,args) -> mkAbs xs (mkApp (reverse xs++scope) c (map (mkExp scope) args))
   where
-    mkAbs xs t = foldr (C.EAbs . i2i) t xs
+    mkAbs xs t = foldr (C.EAbs C.Explicit . i2i) t xs
     mkApp scope c args = case c of
       Q _ c    -> foldl C.EApp (C.EFun (i2i c)) args
       QC _ c   -> foldl C.EApp (C.EFun (i2i c)) args
@@ -156,8 +156,8 @@ mkPatt scope p =
 mkContext :: [Ident] -> A.Context -> ([Ident],[C.Hypo])
 mkContext scope hyps = mapAccumL (\scope (x,ty) -> let ty' = mkType scope ty
                                                    in if x == identW
-                                                        then (  scope,C.Hyp          ty')
-                                                        else (x:scope,C.HypV (i2i x) ty')) scope hyps 
+                                                        then (  scope,(C.Explicit,i2i x,ty'))
+                                                        else (x:scope,(C.Explicit,i2i x,ty'))) scope hyps 
 
 mkTerm :: Term -> C.Term
 mkTerm tr = case tr of
diff --git a/src/PGF/Binary.hs b/src/PGF/Binary.hs
index 87d61d1bc..e4ed98424 100644
--- a/src/PGF/Binary.hs
+++ b/src/PGF/Binary.hs
@@ -102,7 +102,7 @@ instance Binary Term where
              _  -> decodingError

 

 instance Binary Expr where

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

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

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

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

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

@@ -113,7 +113,7 @@ instance Binary Expr where
   put (ETyped e ty)   = putWord8 8 >> put (e,ty)

   get = do tag <- getWord8

            case tag of

-             0 -> liftM2 EAbs get get

+             0 -> liftM3 EAbs get get get

              1 -> liftM2 EApp get get

              2 -> liftM  (ELit . LStr) get

              3 -> liftM  (ELit . LFlt) get

@@ -149,15 +149,14 @@ instance Binary Type where
   put (DTyp hypos cat exps) = put (hypos,cat,exps)

   get = liftM3 DTyp get get get

 

-instance Binary Hypo where

-  put (Hyp    t) = putWord8 0 >> put t

-  put (HypV v t) = putWord8 1 >> put (v,t)

-  put (HypI v t) = putWord8 2 >> put (v,t)

+instance Binary BindType where

+  put Explicit = putWord8 0

+  put Implicit = putWord8 1

   get = do tag <- getWord8

            case tag of

-             0 -> liftM  Hyp  get 

-             1 -> liftM2 HypV get get

-             2 -> liftM2 HypI get get

+             0 -> return Explicit

+             1 -> return Implicit

+             _ -> decodingError

 

 instance Binary FFun where

   put (FFun fun prof lins) = put (fun,prof,lins)

diff --git a/src/PGF/Expr.hs b/src/PGF/Expr.hs
index d3a5992bb..8a30a0988 100644
--- a/src/PGF/Expr.hs
+++ b/src/PGF/Expr.hs
@@ -1,5 +1,5 @@
-module PGF.Expr(Tree, Expr(..), Literal(..), Patt(..), Equation(..),

-                readExpr, showExpr, pExpr, ppExpr, ppPatt,

+module PGF.Expr(Tree, BindType(..), Expr(..), Literal(..), Patt(..), Equation(..),

+                readExpr, showExpr, pExpr, pBinds, ppExpr, ppPatt,

 

                 mkApp,    unApp,

                 mkStr,    unStr,

@@ -36,6 +36,11 @@ data Literal =
 

 type MetaId = Int

 

+data BindType = 

+    Explicit

+  | Implicit

+  deriving (Eq,Ord,Show)

+

 -- | Tree is the abstract syntax representation of a given sentence

 -- in some concrete syntax. Technically 'Tree' is a type synonym

 -- of 'Expr'.

@@ -45,7 +50,7 @@ type Tree = Expr
 -- both parameter of a dependent type or an abstract syntax tree for

 -- for some sentence.

 data Expr =

-   EAbs CId Expr                    -- ^ lambda abstraction

+   EAbs BindType CId Expr           -- ^ lambda abstraction

  | EApp Expr Expr                   -- ^ application

  | ELit Literal                     -- ^ literal

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

@@ -131,10 +136,24 @@ 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 ','))

+    pAbs = do xs <- RP.between (RP.char '\\') (RP.skipSpaces >> RP.string "->") pBinds

               e  <- pExpr

-              return (foldr EAbs e xs)

-                 

+              return (foldr (\(b,x) e -> EAbs b x e) e xs)

+

+pBinds :: RP.ReadP [(BindType,CId)]

+pBinds = do xss <- RP.sepBy1 (RP.skipSpaces >> pBind) (RP.skipSpaces >> RP.char ',')

+            return (concat xss)

+  where

+    pCIdOrWild = pCId `mplus` (RP.char '_' >> return wildCId)

+

+    pBind = 

+      do x <- pCIdOrWild

+         return [(Explicit,x)]

+      `mplus`

+      RP.between (RP.char '{')

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

+                 (RP.sepBy1 (RP.skipSpaces >> pCIdOrWild >>= \id -> return (Implicit,id)) (RP.skipSpaces >> RP.char ','))

+

 pFactor =       fmap EFun  pCId

         RP.<++  fmap ELit  pLit

         RP.<++  fmap EMeta pMeta

@@ -170,14 +189,14 @@ pStr = RP.char '"' >> (RP.manyTill (pEsc RP.<++ RP.get) (RP.char '"'))
 -----------------------------------------------------

 

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

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

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

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

-                                                   PP.hsep (PP.punctuate PP.comma (List.map ppCId (reverse xs))) PP.<+>

+                                                   PP.hsep (PP.punctuate PP.comma (reverse (List.zipWith ppBind bs 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)

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

+                                getVars bs xs e            = (bs,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

@@ -192,6 +211,9 @@ ppPatt d scope (PLit l)    = (scope,ppLit l)
 ppPatt d scope (PVar f)    = (f:scope,ppCId f)

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

 

+ppBind Explicit x = ppCId x

+ppBind Implicit x = PP.braces (ppCId x)

+

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

 ppLit (LInt n) = PP.integer n

 ppLit (LFlt d) = PP.double d

@@ -205,10 +227,12 @@ ppParens True  = PP.parens
 ppParens False = id

 

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

-freshName x xs = loop 1 x

+freshName x xs0 = loop 1 x

   where

+    xs = wildCId : xs0

+

     loop i y

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

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

       | otherwise = y

 

 

@@ -220,12 +244,12 @@ freshName x xs = loop 1 x
 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 (VLit l)                  = ELit l

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

+    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 b x e)) = EAbs b x (value2expr (i+1) (eval funs ((VGen i []):env) e))

 

 data Value

   = VApp CId [Value]

@@ -248,7 +272,7 @@ eval funs env (EFun f)     = case Map.lookup f funs of
                                                   else 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 x e)   = VClosure env (EAbs x e)

+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

@@ -263,18 +287,18 @@ apply funs env (EFun f)     vs     = case Map.lookup f funs of
                                                            else 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 (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 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

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

 

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

 -- Pattern matching

diff --git a/src/PGF/Expr.hs-boot b/src/PGF/Expr.hs-boot
index 533feea75..075f7f44b 100644
--- a/src/PGF/Expr.hs-boot
+++ b/src/PGF/Expr.hs-boot
@@ -10,7 +10,16 @@ instance Eq   Expr
 instance Ord  Expr

 instance Show Expr

 

+

+data BindType = Explicit | Implicit

+

+instance Eq   BindType

+instance Ord  BindType

+instance Show BindType

+

+

 pFactor :: RP.ReadP Expr

+pBinds  :: RP.ReadP [(BindType,CId)]

 

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

 

diff --git a/src/PGF/Linearize.hs b/src/PGF/Linearize.hs
index 418ed9d5a..f733c8cb1 100644
--- a/src/PGF/Linearize.hs
+++ b/src/PGF/Linearize.hs
@@ -59,8 +59,8 @@ linTree :: PGF -> CId -> Expr -> Term
 linTree pgf lang = lin . expr2tree
   where
     lin (Abs xs  e )   = case lin e of
-                             R ts -> R $ ts     ++ (Data.List.map (kks . showCId) xs)
-                             TM s -> R $ (TM s)  : (Data.List.map (kks . showCId) xs)
+                             R ts -> R $ ts     ++ (Data.List.map (kks . showCId . snd) xs)
+                             TM s -> R $ (TM s)  : (Data.List.map (kks . showCId . snd) xs)
     lin (Fun fun es)   = let argVariants = mapM (liftVariants . lin) es
                           in variants [compute pgf lang args $ look fun | args <- argVariants]
     lin (Lit (LStr s)) = R [kks (show s)] -- quoted
@@ -130,8 +130,8 @@ linTreeMark :: PGF -> CId -> Expr -> Term
 linTreeMark pgf lang = lin [] . expr2tree
   where
     lin p (Abs xs  e )   = case lin p e of
-                             R ts -> R $ ts     ++ (Data.List.map (kks . showCId) xs)
-                             TM s -> R $ (TM s)  : (Data.List.map (kks . showCId) xs)
+                             R ts -> R $ ts     ++ (Data.List.map (kks . showCId . snd) xs)
+                             TM s -> R $ (TM s)  : (Data.List.map (kks . showCId . snd) xs)
     lin p (Fun fun es)   = let argVariants = 
                                 mapM (\ (i,e) -> liftVariants $ lin (sub p i) e) (zip [0..] es)
                           in variants [mark p $ compute pgf lang args $ look fun | args <- argVariants]
diff --git a/src/PGF/Macros.hs b/src/PGF/Macros.hs
index 05980d823..604f3c35d 100644
--- a/src/PGF/Macros.hs
+++ b/src/PGF/Macros.hs
@@ -100,17 +100,15 @@ restrictPGF cond pgf = pgf {
   abstr = abstract pgf
 
 depth :: Expr -> Int
-depth (EAbs _  t)  = depth t
+depth (EAbs _ _ t) = depth t
 depth (EApp e1 e2) = max (depth e1) (depth e2) + 1
 depth _            = 1
 
 cftype :: [CId] -> CId -> Type
-cftype args val = DTyp [Hyp (cftype [] arg) | arg <- args] val []
+cftype args val = DTyp [(Explicit,wildCId,cftype [] arg) | arg <- args] val []
 
 typeOfHypo :: Hypo -> Type
-typeOfHypo (Hyp    ty) = ty
-typeOfHypo (HypV _ ty) = ty
-typeOfHypo (HypI _ ty) = ty
+typeOfHypo (_,_,ty) = ty
 
 catSkeleton :: Type -> ([CId],CId)
 catSkeleton ty = case ty of
diff --git a/src/PGF/Parsing/FCFG/Incremental.hs b/src/PGF/Parsing/FCFG/Incremental.hs
index cae0ad80f..6ae18e3bf 100644
--- a/src/PGF/Parsing/FCFG/Incremental.hs
+++ b/src/PGF/Parsing/FCFG/Incremental.hs
@@ -134,7 +134,7 @@ extractTrees (State pgf pinfo chart items) ty@(DTyp _ start _) =
 

     check_ho_fun fun args

       | fun == _V = return (head args)

-      | fun == _B = return (foldl1 Set.difference (map fst args), foldr (\x e -> EAbs (mkVar (snd x)) e) (snd (head args)) (tail args))

+      | fun == _B = return (foldl1 Set.difference (map fst args), foldr (\x e -> EAbs Explicit (mkVar (snd x)) e) (snd (head args)) (tail args))

       | otherwise = return (Set.unions (map fst args),foldl (\e x -> EApp e (snd x)) (EFun fun) args)

     

     mkVar (EFun  v) = v

diff --git a/src/PGF/Tree.hs b/src/PGF/Tree.hs
index c2d2f33f5..cf01b4470 100644
--- a/src/PGF/Tree.hs
+++ b/src/PGF/Tree.hs
@@ -1,6 +1,5 @@
 module PGF.Tree 
          ( Tree(..),
-           readTree, showTree, pTree, ppTree,
            tree2expr, expr2tree
          ) where
 
@@ -18,54 +17,13 @@ import qualified Text.ParserCombinators.ReadP as RP
 -- allow unapplied lambda abstractions. The tree is used directly 
 -- from the linearizer and is produced directly from the parser.
 data Tree = 
-   Abs [CId] Tree                   -- ^ lambda abstraction. The list of variables is non-empty
+   Abs [(BindType,CId)] Tree        -- ^ lambda abstraction. The list of variables is non-empty
  | Var CId                          -- ^ variable
  | Fun CId [Tree]                   -- ^ function application
  | Lit Literal                      -- ^ literal
  | Meta {-# UNPACK #-} !MetaId      -- ^ meta variable
   deriving (Eq, Ord)
 
--- | parses 'String' as an expression
-readTree :: String -> Maybe Tree
-readTree s = case [x | (x,cs) <- RP.readP_to_S (pTree False) s, all isSpace cs] of
-               [x] -> Just x
-               _   -> Nothing
-
--- | renders expression as 'String'
-showTree :: Tree -> String
-showTree = PP.render . ppTree 0
-
-instance Show Tree where
-    showsPrec i x = showString (PP.render (ppTree i x))
-
-instance Read Tree where
-    readsPrec _ = RP.readP_to_S (pTree False)
-
-pTrees :: RP.ReadP [Tree]
-pTrees = liftM2 (:) (pTree True) pTrees RP.<++ (RP.skipSpaces >> return [])
-
-pTree :: Bool -> RP.ReadP Tree
-pTree isNested = RP.skipSpaces >> (pParen RP.<++ pAbs RP.<++ pApp RP.<++ fmap Lit pLit RP.<++ fmap Meta pMeta)
-  where 
-        pParen = RP.between (RP.char '(') (RP.char ')') (pTree False)
-        pAbs = do xs <- RP.between (RP.char '\\') (RP.skipSpaces >> RP.string "->") (RP.sepBy1 (RP.skipSpaces >> pCId) (RP.skipSpaces >> RP.char ','))
-                  t  <- pTree False
-                  return (Abs xs t)
-        pApp = do f  <- pCId
-                  ts <- (if isNested then return [] else pTrees)
-                  return (Fun f ts)
-
-ppTree d (Abs xs t) = ppParens (d > 0) (PP.char '\\' PP.<>
-                                        PP.hsep (PP.punctuate PP.comma (List.map ppCId xs)) PP.<+>
-                                        PP.text "->" PP.<+>
-                                        ppTree 0 t)
-ppTree d (Fun f []) = ppCId f
-ppTree d (Fun f ts) = ppParens (d > 0) (ppCId 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)   = ppCId id
-
-
 -----------------------------------------------------
 -- Conversion Expr <-> Tree
 -----------------------------------------------------
@@ -78,7 +36,7 @@ tree2expr = tree2expr []
     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 (Abs xs t) = foldr (\(b,x) e -> EAbs b x e) (tree2expr (List.map snd (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"
@@ -88,11 +46,11 @@ tree2expr = tree2expr []
 expr2tree :: Expr -> Tree
 expr2tree e = abs [] [] e
   where
-    abs ys xs (EAbs x e)      = abs ys (x:xs) e
+    abs ys xs (EAbs b x e)    = abs ys ((b,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)
+                                  xs -> Abs (reverse xs) (app (map snd xs++ys) [] e)
 
     app xs as (EApp e1 e2)    = app xs ((abs xs [] e2) : as) e1
     app xs as (ELit l)
@@ -101,7 +59,7 @@ expr2tree e = abs [] [] e
     app xs as (EMeta n)
                | 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 (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
diff --git a/src/PGF/Type.hs b/src/PGF/Type.hs
index dbd52343b..2b6862bbf 100644
--- a/src/PGF/Type.hs
+++ b/src/PGF/Type.hs
@@ -1,4 +1,4 @@
-module PGF.Type ( Type(..), Hypo(..),

+module PGF.Type ( Type(..), Hypo,

                   readType, showType,

                   pType, ppType, ppHypo ) where

 

@@ -16,11 +16,7 @@ data Type =
   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,Show)

+type Hypo = (BindType,CId,Type)

 

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

 readType :: String -> Maybe Type

@@ -45,23 +41,23 @@ pType = do
   where

     pHypo =

       do (cat,args) <- pAtom

-         return [Hyp (DTyp [] cat args)]

+         return [(Explicit,wildCId,DTyp [] cat args)]

       RP.<++

       (RP.between (RP.char '(') (RP.char ')') $ do

-         hyp <- RP.option (\ty -> [Hyp ty]) $ do

-                     vs <- RP.sepBy (RP.skipSpaces >> pCId) (RP.skipSpaces >> RP.char ',')

+         xs <- RP.option [(Explicit,wildCId)] $ do

+                     xs <- pBinds

                      RP.skipSpaces

                      RP.char ':'

-                     return (\ty -> [HypV v ty | v <- vs])

+                     return xs

          ty <- pType

-         return (hyp ty))

+         return [(b,v,ty) | (b,v) <- xs])

       RP.<++

       (RP.between (RP.char '{') (RP.char '}') $ do

          vs <- RP.sepBy1 (RP.skipSpaces >> pCId) (RP.skipSpaces >> RP.char ',')

          RP.skipSpaces

          RP.char ':'

          ty <- pType

-         return [HypI v ty | v <- vs])

+         return [(Implicit,v,ty) | v <- vs])

 

     pAtom = do

       cat <- pCId

@@ -77,8 +73,11 @@ ppType d scope (DTyp hyps cat args)
   where

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

 

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

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

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

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

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

+ppHypo scope (Explicit,x,typ) = if x == wildCId

+                                  then (scope,ppType 1 scope typ)

+                                  else let y = freshName x scope

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

+ppHypo scope (Implicit,x,typ) = if x == wildCId

+                                  then (scope,PP.parens (PP.braces (ppCId x) PP.<+> PP.char ':' PP.<+> ppType 0 scope typ))

+                                  else let y = freshName x scope

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

diff --git a/src/PGF/TypeCheck.hs b/src/PGF/TypeCheck.hs
index 2683588d4..bbd3ae126 100644
--- a/src/PGF/TypeCheck.hs
+++ b/src/PGF/TypeCheck.hs
@@ -200,12 +200,11 @@ tcHypos scope (h:hs) = do
   return (scope,h:hs)
 
 tcHypo :: Scope -> Hypo -> TcM (Scope,Hypo)
-tcHypo scope (Hyp    ty) = do
+tcHypo scope (b,x,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)
+  if x == wildCId
+    then return (scope,(b,x,ty))
+    else return (addScopedVar x (TTyp (scopeEnv scope) ty) scope,(b,x,ty))
 
 tcHypoExprs :: Scope -> Env -> [(Expr,Hypo)] -> TcM (Env,[Expr])
 tcHypoExprs scope delta []         = return (delta,[])
@@ -215,13 +214,12 @@ tcHypoExprs scope delta ((e,h):xs) = do
   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)
+tcHypoExpr scope delta e (b,x,ty) = do
+     e  <- tcExpr scope e (TTyp delta ty)
+     funs <- getFuns
+     if x == wildCId
+       then return (                             delta,e)
+       else return (eval funs (scopeEnv scope) e:delta,e)
 
 
 -----------------------------------------------------
@@ -239,16 +237,16 @@ checkExpr pgf e ty =
     Fail err   -> Left err
 
 tcExpr :: Scope -> Expr -> TType -> TcM Expr
-tcExpr scope e0@(EAbs x e) tty =
+tcExpr scope e0@(EAbs b 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 (scopeVars scope) e0 ty)
+    TTyp delta (DTyp ((_,y,ty):hs) c es) -> do e <- if y == wildCId
+                                                      then tcExpr (addScopedVar x (TTyp delta ty) scope)
+                                                                  e (TTyp delta (DTyp hs c es))
+                                                      else tcExpr (addScopedVar x (TTyp delta ty) scope)
+                                                                  e (TTyp ((VGen (scopeSize scope) []):delta) (DTyp hs c es))
+                                               return (EAbs b x e)
+    _                                    -> do ty <- evalType (scopeSize scope) tty
+                                               tcError (NotFunType (scopeVars scope) e0 ty)
 tcExpr scope (EMeta _) tty = do
   i <- newMeta scope
   return (EMeta i)
@@ -322,14 +320,13 @@ eqType scope k i0 tty1@(TTyp delta1 ty1@(DTyp hyps1 cat1 es1)) tty2@(TTyp delta2
     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
+    eqHyps k delta1 ((_,x,ty1) : h1s) delta2 ((_,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)
+      if x == wildCId && y == wildCId
+        then eqHyps k delta1 h1s delta2 h2s
+        else if x /= wildCId && y /= wildCId
+               then eqHyps (k+1) ((VGen k []):delta1) h1s ((VGen k []):delta2) h2s
+               else raiseTypeMatchError
     eqHyps k delta1               h1s  delta2               h2s  = raiseTypeMatchError
 
     eqExpr :: Int -> Env -> Expr -> Env -> Expr -> TcM ()
@@ -353,23 +350,23 @@ eqType scope k i0 tty1@(TTyp delta1 ty1@(DTyp hyps1 cat1 es1)) tty2@(TTyp delta2
         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
-                                                                              setMeta i (MBound e2)
-                                                                              sequence_ [c e2 | c <- cs]
-    eqValue' k v1                           (VMeta i env2 vs2)           = do (MUnbound scopei cs) <- getMeta i
-                                                                              e1 <- mkLam i scopei env2 vs2 v1
-                                                                              setMeta i (MBound e1)
-                                                                              sequence_ [c e1 | c <- cs]
-    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
+    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
+                                                                                  setMeta i (MBound e2)
+                                                                                  sequence_ [c e2 | c <- cs]
+    eqValue' k v1                             (VMeta i env2 vs2)             = do (MUnbound scopei cs) <- getMeta i
+                                                                                  e1 <- mkLam i scopei env2 vs2 v1
+                                                                                  setMeta i (MBound e1)
+                                                                                  sequence_ [c e1 | c <- cs]
+    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
@@ -383,7 +380,7 @@ eqType scope k i0 tty1@(TTyp delta1 ty1@(DTyp hyps1 cat1 es1)) tty2@(TTyp delta2
       return (addLam vs0 (value2expr funs (length xs) v))
       where
         addLam []     e = e
-        addLam (v:vs) e = EAbs var (addLam vs e)
+        addLam (v:vs) e = EAbs Explicit var (addLam vs e)
 
         var = mkCId "v"
 
@@ -439,9 +436,10 @@ evalType k (TTyp delta ty) = do funs <- getFuns
       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))
+    evalHypo sig (k,delta) (b,x,ty) =
+      if x == wildCId
+        then ((k,              delta),(b,x,evalTy sig k delta ty))
+        else ((k+1,(VGen k []):delta),(b,x,evalTy sig k delta ty))
 
 
 -----------------------------------------------------
@@ -453,7 +451,7 @@ refineExpr e = TcM (\abstr metaid ms -> Ok metaid ms (refineExpr_ ms e))
 
 refineExpr_ ms e = refine e
   where
-    refine (EAbs x e)    = EAbs x (refine e)
+    refine (EAbs b x e)  = EAbs b 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
@@ -467,15 +465,11 @@ refineExpr_ ms e = refine e
 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)
+refineType_ ms (DTyp hyps cat es) = DTyp [(b,x,refineType_ ms ty) | (b,x,ty) <- hyps] cat (List.map (refineExpr_ ms) es)
 
-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))
+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 b x e)) = EAbs b x (value2expr sig (i+1) (eval sig ((VGen i []):env) e))
diff --git a/testsuite/runtime/typecheck/typecheck.gfs.gold b/testsuite/runtime/typecheck/typecheck.gfs.gold
index 5e27e1482..a43a0c216 100644
--- a/testsuite/runtime/typecheck/typecheck.gfs.gold
+++ b/testsuite/runtime/typecheck/typecheck.gfs.gold
@@ -30,7 +30,7 @@ In the expression: mkMorph (\x -> succ zero)
 Expression: <append zero (succ zero) : Vector zero -> Vector (succ zero) -> Vector (succ zero)>


 Type:       Vector zero -> Vector (succ zero) -> Vector (succ zero)


 


-Expression: <\n, v1, n'1, v2 -> append n n'1 v1 v2 : (n : Nat) -> Vector n -> (m : Nat) -> Vector m -> Vector (plus n m)>


+Expression: <\n, v1, n1, v2 -> append n n1 v1 v2 : (n : Nat) -> Vector n -> (m : Nat) -> Vector m -> Vector (plus n m)>


 Type:       (n : Nat) -> Vector n -> (m : Nat) -> Vector m -> Vector (plus n m)


 


 Category EQ is not in scope