syntax for implicit arguments in GF

11 files changed, 210 insertions, 244 deletions

diff --git a/src/GF/Grammar/AppPredefined.hs b/src/GF/Grammar/AppPredefined.hs
index 248445c0c..9e5b0d83a 100644
--- a/src/GF/Grammar/AppPredefined.hs
+++ b/src/GF/Grammar/AppPredefined.hs
@@ -50,11 +50,11 @@ typPredefined f
   | f == cPlus      = return $ mkFunType [typeInt,typeInt] (typeInt)
 ----  "read"   -> (P : Type) -> Tok -> P
   | f == cShow      = return $ mkProd -- (P : PType) -> P -> Tok
-    ([(varP,typePType),(identW,Vr varP)],typeStr,[]) 
+    ([(Explicit,varP,typePType),(Explicit,identW,Vr varP)],typeStr,[]) 
   | f == cToStr     = return $ mkProd -- (L : Type)  -> L -> Str
-    ([(varL,typeType),(identW,Vr varL)],typeStr,[]) 
+    ([(Explicit,varL,typeType),(Explicit,identW,Vr varL)],typeStr,[]) 
   | f == cMapStr    = return $ mkProd -- (L : Type)  -> (Str -> Str) -> L -> L
-    ([(varL,typeType),(identW,mkFunType [typeStr] typeStr),(identW,Vr varL)],Vr varL,[])
+    ([(Explicit,varL,typeType),(Explicit,identW,mkFunType [typeStr] typeStr),(Explicit,identW,Vr varL)],Vr varL,[])
   | f == cTake      = return $ mkFunType [typeInt,typeTok] typeTok
   | f == cTk        = return $ mkFunType [typeInt,typeTok] typeTok
   | otherwise       = Bad (render (text "unknown in Predef:" <+> ppIdent f))
diff --git a/src/GF/Grammar/Binary.hs b/src/GF/Grammar/Binary.hs
index 31e4ea222..e22e1dc87 100644
--- a/src/GF/Grammar/Binary.hs
+++ b/src/GF/Grammar/Binary.hs
@@ -109,6 +109,15 @@ instance Binary Info where
              8 -> get >>= \(x,y)   -> return (AnyInd x y)

              _ -> decodingError

 

+instance Binary BindType where

+  put Explicit = putWord8 0

+  put Implicit = putWord8 1

+  get = do tag <- getWord8

+           case tag of

+             0 -> return Explicit

+             1 -> return Implicit

+             _ -> decodingError

+

 instance Binary Term where

   put (Vr x)        = putWord8 0  >> put x

   put (Cn x)        = putWord8 1  >> put x

@@ -119,9 +128,9 @@ instance Binary Term where
   put (K x)         = putWord8 7  >> put x

   put (Empty)       = putWord8 8

   put (App x y)     = putWord8 9  >> put (x,y)

-  put (Abs x y)     = putWord8 10 >> put (x,y)

+  put (Abs x y z)   = putWord8 10 >> put (x,y,z)

   put (Meta x)      = putWord8 11 >> put x

-  put (Prod x y z)  = putWord8 12 >> put (x,y,z)

+  put (Prod w x y z)= putWord8 12 >> put (w,x,y,z)

   put (Typed x y)   = putWord8 14 >> put (x,y)

   put (Example x y) = putWord8 15 >> put (x,y)

   put (RecType x)   = putWord8 16 >> put x

@@ -159,9 +168,9 @@ instance Binary Term where
              7  -> get >>= \x       -> return (K x)

              8  ->                     return (Empty)

              9  -> get >>= \(x,y)   -> return (App x y)

-             10 -> get >>= \(x,y)   -> return (Abs x y)

+             10 -> get >>= \(x,y,z) -> return (Abs x y z)

              11 -> get >>= \x       -> return (Meta x)

-             12 -> get >>= \(x,y,z) -> return (Prod x y z)

+             12 -> get >>= \(w,x,y,z)->return (Prod w x y z)

              14 -> get >>= \(x,y)   -> return (Typed x y)

              15 -> get >>= \(x,y)   -> return (Example x y)

              16 -> get >>= \x       -> return (RecType x)

diff --git a/src/GF/Grammar/CF.hs b/src/GF/Grammar/CF.hs
index 5d88916cd..2a94bbfdb 100644
--- a/src/GF/Grammar/CF.hs
+++ b/src/GF/Grammar/CF.hs
@@ -112,8 +112,8 @@ cf2rule (fun, (cat, items)) = (def,ldef) where
   f     = identS fun
   def   = (f, AbsFun (Just (mkProd (args', Cn (identS cat), []))) Nothing Nothing)
   args0 = zip (map (identS . ("x" ++) . show) [0..]) items
-  args  = [(v, Cn (identS c)) | (v, Left c) <- args0]
-  args' = [(identS "_", Cn (identS c)) | (_, Left c) <- args0]
+  args  = [((Explicit,v), Cn (identS c)) | (v, Left c) <- args0]
+  args' = [(Explicit,identS "_", Cn (identS c)) | (_, Left c) <- args0]
   ldef  = (f, CncFun 
                Nothing 
                (Just (mkAbs (map fst args) 
diff --git a/src/GF/Grammar/Grammar.hs b/src/GF/Grammar/Grammar.hs
index 8cfc397af..d7af03f22 100644
--- a/src/GF/Grammar/Grammar.hs
+++ b/src/GF/Grammar/Grammar.hs
@@ -15,35 +15,36 @@
 -----------------------------------------------------------------------------
 
 module GF.Grammar.Grammar (SourceGrammar,
-                emptySourceGrammar,                
-		SourceModInfo,
-		SourceModule,
-                mapSourceModule,
-		Info(..),
-                PValues,
-		Type,
-		Cat,
-		Fun,
-		QIdent,
-		Term(..),
-		Patt(..),
-		TInfo(..),
-		Label(..),
-		MetaId,
-		Hypo,
-		Context,
-		Equation,
-		Labelling,
-		Assign,
-		Case,
-		Cases,
-		LocalDef,
-		Param,
-		Altern,
-		Substitution,
-		varLabel, tupleLabel, linLabel, theLinLabel,
-		ident2label, label2ident
-	       ) where
+        emptySourceGrammar,                
+        SourceModInfo,
+        SourceModule,
+        mapSourceModule,
+        Info(..),
+        PValues,
+        Type,
+        Cat,
+        Fun,
+        QIdent,
+        BindType(..),
+        Term(..),
+        Patt(..),
+        TInfo(..),
+        Label(..),
+        MetaId,
+        Hypo,
+        Context,
+        Equation,
+        Labelling,
+        Assign,
+        Case,
+        Cases,
+        LocalDef,
+        Param,
+        Altern,
+        Substitution,
+        varLabel, tupleLabel, linLabel, theLinLabel,
+        ident2label, label2ident
+        ) where
 
 import GF.Infra.Ident
 import GF.Infra.Option ---
@@ -103,57 +104,62 @@ type Fun  = QIdent
 
 type QIdent = (Ident,Ident)
 
+data BindType = 
+    Explicit
+  | Implicit
+  deriving (Eq,Ord,Show)
+
 data Term =
-   Vr Ident             -- ^ variable
- | Cn Ident             -- ^ constant
- | Con Ident            -- ^ constructor
- | Sort Ident           -- ^ basic type
- | EInt Integer         -- ^ integer literal
- | EFloat Double        -- ^ floating point literal
- | K String             -- ^ string literal or token: @\"foo\"@
- | Empty                -- ^ the empty string @[]@
-
- | App Term Term        -- ^ application: @f a@
- | Abs Ident Term       -- ^ abstraction: @\x -> b@
+   Vr Ident                      -- ^ variable
+ | Cn Ident                      -- ^ constant
+ | Con Ident                     -- ^ constructor
+ | Sort Ident                    -- ^ basic type
+ | EInt Integer                  -- ^ integer literal
+ | EFloat Double                 -- ^ floating point literal
+ | K String                      -- ^ string literal or token: @\"foo\"@
+ | Empty                         -- ^ the empty string @[]@
+
+ | App Term Term                 -- ^ application: @f a@
+ | Abs BindType Ident Term       -- ^ abstraction: @\x -> b@
  | Meta {-# UNPACK #-} !MetaId   -- ^ metavariable: @?i@ (only parsable: ? = ?0)
- | Prod Ident Term Term -- ^ function type: @(x : A) -> B@
- | Typed Term Term      -- ^ type-annotated term
+ | Prod BindType Ident Term Term -- ^ function type: @(x : A) -> B@, @A -> B@, @({x} : A) -> B@
+ | Typed Term Term               -- ^ type-annotated term
 --
 -- /below this, the constructors are only for concrete syntax/
- | Example Term String  -- ^ example-based term: @in M.C "foo"
- | RecType [Labelling]  -- ^ record type: @{ p : A ; ...}@
- | R [Assign]           -- ^ record:      @{ p = a ; ...}@
- | P Term Label         -- ^ projection:  @r.p@
- | PI Term Label Int    -- ^ index-annotated projection
- | ExtR Term Term       -- ^ extension:   @R ** {x : A}@ (both types and terms)
+ | Example Term String           -- ^ example-based term: @in M.C "foo"
+ | RecType [Labelling]           -- ^ record type: @{ p : A ; ...}@
+ | R [Assign]                    -- ^ record:      @{ p = a ; ...}@
+ | P Term Label                  -- ^ projection:  @r.p@
+ | PI Term Label Int             -- ^ index-annotated projection
+ | ExtR Term Term                -- ^ extension:   @R ** {x : A}@ (both types and terms)
  
- | Table Term Term      -- ^ table type:  @P => A@
- | T TInfo [Case]       -- ^ table:       @table {p => c ; ...}@
- | TSh TInfo [Cases]    -- ^ table with disjunctive patters (only back end opt)
- | V Type [Term]        -- ^ table given as course of values: @table T [c1 ; ... ; cn]@
- | S Term Term          -- ^ selection:   @t ! p@
- | Val Term Type Int    -- ^ parameter value number: @T # i#
+ | Table Term Term               -- ^ table type:  @P => A@
+ | T TInfo [Case]                -- ^ table:       @table {p => c ; ...}@
+ | TSh TInfo [Cases]             -- ^ table with disjunctive patters (only back end opt)
+ | V Type [Term]                 -- ^ table given as course of values: @table T [c1 ; ... ; cn]@
+ | S Term Term                   -- ^ selection:   @t ! p@
+ | Val Term Type Int             -- ^ parameter value number: @T # i#
 
- | Let LocalDef Term    -- ^ local definition: @let {t : T = a} in b@
+ | Let LocalDef Term             -- ^ local definition: @let {t : T = a} in b@
 
- | Alias Ident Type Term  -- ^ constant and its definition, used in inlining
+ | Alias Ident Type Term         -- ^ constant and its definition, used in inlining
 
- | Q  Ident Ident        -- ^ qualified constant from a package
- | QC Ident Ident        -- ^ qualified constructor from a package
+ | Q  Ident Ident                -- ^ qualified constant from a package
+ | QC Ident Ident                -- ^ qualified constructor from a package
 
- | C Term Term    -- ^ concatenation: @s ++ t@
- | Glue Term Term -- ^ agglutination: @s + t@
+ | C Term Term                   -- ^ concatenation: @s ++ t@
+ | Glue Term Term                -- ^ agglutination: @s + t@
 
- | EPatt Patt     -- ^ pattern (in macro definition): # p
- | EPattType Term -- ^ pattern type: pattern T
+ | EPatt Patt                    -- ^ pattern (in macro definition): # p
+ | EPattType Term                -- ^ pattern type: pattern T
 
- | ELincat Ident Term -- ^ boxed linearization type of Ident
- | ELin Ident Term    -- ^ boxed linearization of type Ident
+ | ELincat Ident Term            -- ^ boxed linearization type of Ident
+ | ELin Ident Term               -- ^ boxed linearization of type Ident
 
- | FV [Term]      -- ^ alternatives in free variation: @variants { s ; ... }@
+ | FV [Term]                     -- ^ alternatives in free variation: @variants { s ; ... }@
 
- | Alts (Term, [(Term, Term)]) -- ^ alternatives by prefix: @pre {t ; s\/c ; ...}@
- | Strs [Term]                 -- ^ conditioning prefix strings: @strs {s ; ...}@
+ | Alts (Term, [(Term, Term)])   -- ^ alternatives by prefix: @pre {t ; s\/c ; ...}@
+ | Strs [Term]                   -- ^ conditioning prefix strings: @strs {s ; ...}@
 
   deriving (Show, Eq, Ord)
 
@@ -200,8 +206,8 @@ data Label =
 
 type MetaId = Int
 
-type Hypo     = (Ident,Term)  -- (x:A)  (_:A)  A
-type Context  = [Hypo]        -- (x:A)(y:B)   (x,y:A)   (_,_:A)
+type Hypo     = (BindType,Ident,Term)   -- (x:A)  (_:A)  A  ({x}:A)
+type Context  = [Hypo]                  -- (x:A)(y:B)   (x,y:A)   (_,_:A)
 type Equation = ([Patt],Term) 
 
 type Labelling = (Label, Term) 
diff --git a/src/GF/Grammar/Lookup.hs b/src/GF/Grammar/Lookup.hs
index c0cbbe962..a85f54c90 100644
--- a/src/GF/Grammar/Lookup.hs
+++ b/src/GF/Grammar/Lookup.hs
@@ -137,7 +137,7 @@ lookupOverload gr m c = do
     case info of
       ResOverload os tysts -> do
             tss <- mapM (\x -> lookupOverload gr x c) os
-            return $ [(map snd args,(val,tr)) | 
+            return $ [(map (\(b,x,t) -> t) args,(val,tr)) | 
                       (ty,tr) <- tysts, Ok (args,val) <- [typeFormCnc ty]] ++ 
                      concat tss
 
@@ -173,7 +173,7 @@ lookupParamValues gr m c = do
     _ -> liftM concat $ mapM mkPar ps
  where
    mkPar (f,co) = do
-     vs <- liftM combinations $ mapM (\ (_,ty) -> allParamValues gr ty) co
+     vs <- liftM combinations $ mapM (\(_,_,ty) -> allParamValues gr ty) co
      return $ map (mkApp (QC m f)) vs
 
 lookupFirstTag :: SourceGrammar -> Ident -> Ident -> Err Term
diff --git a/src/GF/Grammar/MMacros.hs b/src/GF/Grammar/MMacros.hs
index 0a6c721ed..a0852421d 100644
--- a/src/GF/Grammar/MMacros.hs
+++ b/src/GF/Grammar/MMacros.hs
@@ -143,10 +143,10 @@ substTerm  :: [Ident] -> Substitution -> Term -> Term
 substTerm ss g c = case c of
   Vr x        -> maybe c id $ lookup x g
   App f a     -> App (substTerm ss g f) (substTerm ss g a)
-  Abs x b     -> let y = mkFreshVarX ss x in 
-                   Abs y (substTerm (y:ss) ((x, Vr y):g) b)
-  Prod x a b  -> let y = mkFreshVarX ss x in 
-                   Prod y (substTerm ss g a) (substTerm (y:ss) ((x,Vr y):g) b)
+  Abs b x t   -> let y = mkFreshVarX ss x in 
+                   Abs b y (substTerm (y:ss) ((x, Vr y):g) t)
+  Prod b x a t  -> let y = mkFreshVarX ss x in 
+                   Prod b y (substTerm ss g a) (substTerm (y:ss) ((x,Vr y):g) t)
   _           -> c
 
 metaSubstExp :: MetaSubst -> [(MetaId,Exp)]
@@ -204,64 +204,16 @@ mkProdVal :: Binds -> Val -> Err Val ---
 mkProdVal bs v = do 
   bs' <- mapPairsM val2exp bs
   v'  <- val2exp v
-  return $ vClos $ foldr (uncurry Prod) v' bs'
+  return $ vClos $ foldr (uncurry (Prod Explicit)) v' bs'
 
 freeVarsExp :: Exp -> [Ident]
 freeVarsExp e = case e of
   Vr x -> [x]
   App f c -> freeVarsExp f ++ freeVarsExp c
-  Abs x b -> filter (/=x) (freeVarsExp b)
-  Prod x a b -> freeVarsExp a ++ filter (/=x) (freeVarsExp b)
+  Abs _ x b -> filter (/=x) (freeVarsExp b)
+  Prod _ x a b -> freeVarsExp a ++ filter (/=x) (freeVarsExp b)
   _ -> [] --- thus applies to abstract syntax only
 
-ident2string :: Ident -> String
-ident2string = showIdent
-{-
-tree :: (TrNode,[Tree]) -> Tree
-tree = Tr
-
-eqCat :: Cat -> Cat -> Bool
-eqCat = (==)
-
-addBinds :: Binds -> Tree -> Tree
-addBinds b (Tr (N (b0,at,t,c,x),ts)) = Tr (N (b ++ b0,at,t,c,x),ts)
-
-bodyTree :: Tree -> Tree
-bodyTree (Tr (N (_,a,t,c,x),ts)) = Tr (N ([],a,t,c,x),ts)
--}
-
-ref2exp :: [Var] -> Type -> Ref -> Err Exp
-ref2exp bounds typ ref = do
-  cont <- contextOfType typ
-  xx0  <- mapM (typeSkeleton . snd) cont
-  let (xxs,cs) = unzip [(length hs, c) | (hs,c) <- xx0]
-      args     = [mkAbs xs mExp | i <- xxs, let xs = mkFreshVars i bounds]
-  return $ mkApp ref args
-  -- no refreshment of metas
-  
--- | invariant: only 'Con' or 'Var'
-type Ref = Exp 
-
-fun2wrap :: [Var] -> ((Fun,Int),Type) -> Exp -> Err Exp
-fun2wrap oldvars ((fun,i),typ) exp = do
-  cont <- contextOfType typ
-  args <- mapM mkArg (zip [0..] (map snd cont))
-  return $ mkApp (qq fun) args
- where
-  mkArg (n,c) = do
-    cont <- contextOfType c
-    let vars = mkFreshVars (length cont) oldvars
-    return $ mkAbs vars $ if n==i then exp else mExp
-
--- | weak heuristics: sameness of value category
-compatType :: Val -> Type -> Bool
-compatType v t = errVal True $ do
-  cat1 <- val2cat v
-  cat2 <- valCat t
-  return $ cat1 == cat2
-
----
-
 mkJustProd :: Context -> Term -> Term
 mkJustProd cont typ = mkProd (cont,typ,[])
 
@@ -283,8 +235,8 @@ identVar _ = Bad "not a variable"
 qualifTerm :: Ident -> Term -> Term
 qualifTerm m  = qualif [] where
   qualif xs t = case t of
-    Abs x b -> let x' = chV x in Abs x' $ qualif (x':xs) b
-    Prod x a b -> Prod x (qualif xs a) $ qualif (x:xs) b
+    Abs b x t -> let x' = chV x in Abs b x' $ qualif (x':xs) t
+    Prod b x a t -> Prod b x (qualif xs a) $ qualif (x:xs) t
     Vr x -> let x' = chV x in if (elem x' xs) then (Vr x') else (Q m x) 
     Cn c  -> Q m c
     Con c -> QC m c
@@ -300,8 +252,8 @@ string2var s = case BS.unpack s of
 reindexTerm :: Term -> Term
 reindexTerm = qualif (0,[]) where
   qualif dg@(d,g) t = case t of
-    Abs x b    -> let x' = ind x d in Abs x' $ qualif (d+1, (x,x'):g) b
-    Prod x a b -> let x' = ind x d in Prod x' (qualif dg a) $ qualif (d+1, (x,x'):g) b
+    Abs b x t    -> let x' = ind x d in Abs b x' $ qualif (d+1, (x,x'):g) t
+    Prod b x a t -> let x' = ind x d in Prod b x' (qualif dg a) $ qualif (d+1, (x,x'):g) t
     Vr x       -> Vr $ look x g
     _ -> composSafeOp (qualif dg) t
   look x  = maybe x id . lookup x --- if x is not in scope it is unchanged
diff --git a/src/GF/Grammar/Macros.hs b/src/GF/Grammar/Macros.hs
index 84a217b26..289531331 100644
--- a/src/GF/Grammar/Macros.hs
+++ b/src/GF/Grammar/Macros.hs
@@ -33,16 +33,16 @@ import Text.PrettyPrint
 
 firstTypeForm :: Type -> Err (Context, Type)
 firstTypeForm t = case t of
-  Prod x a b  -> do
-    (x', val) <- firstTypeForm b 
-    return ((x,a):x',val)
+  Prod b x a t  -> do
+    (x', val) <- firstTypeForm t
+    return ((b,x,a):x',val)
   _ -> return ([],t)
 
 qTypeForm :: Type -> Err (Context, Cat, [Term])
 qTypeForm t = case t of
-  Prod x a b  -> do
-    (x', cat, args) <- qTypeForm b 
-    return ((x,a):x', cat, args)
+  Prod b x a t  -> do
+    (x', cat, args) <- qTypeForm t
+    return ((b,x,a):x', cat, args)
   App c a -> do
     (_,cat, args) <- qTypeForm c
     return ([],cat,args ++ [a])
@@ -61,9 +61,9 @@ typeForm = qTypeForm ---- no need to distinguish any more
 
 typeFormCnc :: Type -> Err (Context, Type)
 typeFormCnc t = case t of
-  Prod x a b  -> do
-    (x', v) <- typeFormCnc b 
-    return ((x,a):x',v)
+  Prod b x a t  -> do
+    (x', v) <- typeFormCnc t
+    return ((b,x,a):x',v)
   _ -> return ([],t)
 
 valCat :: Type -> Err Cat
@@ -84,7 +84,7 @@ valTypeCnc typ =
 typeRawSkeleton :: Type -> Err ([(Int,Type)],Type)
 typeRawSkeleton typ =
   do (cont,typ) <- typeFormCnc typ
-     args <- mapM (typeRawSkeleton . snd) cont
+     args <- mapM (\(b,x,t) -> typeRawSkeleton t) cont
      return ([(length c, v) | (c,v) <- args], typ)
 
 type MCat = (Ident,Ident)
@@ -117,9 +117,9 @@ funsToAndFrom t = errVal undefined $ do ---
 
 typeFormConcrete :: Type -> Err (Context, Type)
 typeFormConcrete t = case t of
-  Prod x a b  -> do 
-    (x', typ) <- typeFormConcrete b 
-    return ((x,a):x', typ)
+  Prod b x a t  -> do 
+    (x', typ) <- typeFormConcrete t
+    return ((b,x,a):x', typ)
   _       -> return ([],t)
 
 isRecursiveType :: Type -> Bool
@@ -130,54 +130,49 @@ isRecursiveType t = errVal False $ do
 isHigherOrderType :: Type -> Bool
 isHigherOrderType t = errVal True $ do  -- pessimistic choice
   co <- contextOfType t
-  return $ not $ null [x | (x,Prod _ _ _) <- co]
+  return $ not $ null [x | (_,x,Prod _ _ _ _) <- co]
 
 contextOfType :: Type -> Err Context
 contextOfType typ = case typ of
-  Prod x a b -> liftM ((x,a):) $ contextOfType b
-  _ -> return [] 
+  Prod b x a t -> liftM ((b,x,a):) $ contextOfType t
+  _            -> return [] 
 
-termForm :: Term -> Err ([(Ident)], Term, [Term])
+termForm :: Term -> Err ([(BindType,Ident)], Term, [Term])
 termForm t = case t of
-   Abs x b  ->
-     do (x', fun, args) <- termForm b 
-        return (x:x', fun, args)
+   Abs b x t  ->
+     do (x', fun, args) <- termForm t
+        return ((b,x):x', fun, args)
    App c a ->
      do (_,fun, args) <- termForm c
         return ([],fun,args ++ [a]) 
    _       -> 
      return ([],t,[])
 
-termFormCnc :: Term -> ([(Ident)], Term)
+termFormCnc :: Term -> ([(BindType,Ident)], Term)
 termFormCnc t = case t of
-   Abs x b  -> (x:xs, t') where (xs,t') = termFormCnc b 
-   _        -> ([],t)
+   Abs b x t  -> ((b,x):xs, t') where (xs,t') = termFormCnc t
+   _          -> ([],t)
 
 appForm :: Term -> (Term, [Term])
 appForm t = case t of
   App c a -> (fun, args ++ [a]) where (fun, args) = appForm c
   _       -> (t,[])
 
-varsOfType :: Type -> [Ident]
-varsOfType t = case t of
-  Prod x _ b -> x : varsOfType b
-  _ -> []
-
 mkProdSimple :: Context -> Term -> Term
 mkProdSimple c t = mkProd (c,t,[])
 
 mkProd :: (Context, Term, [Term]) -> Term
-mkProd ([],typ,args) = mkApp typ args
-mkProd ((x,a):dd, typ, args) = Prod x a (mkProd (dd, typ, args))
+mkProd ([],         typ, args) = mkApp typ args
+mkProd ((b,x,a):dd, typ, args) = Prod b x a (mkProd (dd, typ, args))
 
-mkTerm :: ([(Ident)], Term, [Term]) -> Term
+mkTerm :: ([(BindType,Ident)], Term, [Term]) -> Term
 mkTerm (xx,t,aa) = mkAbs xx (mkApp t aa)
 
 mkApp :: Term -> [Term] -> Term
 mkApp = foldl App
 
-mkAbs :: [Ident] -> Term -> Term
-mkAbs xx t = foldr Abs t xx
+mkAbs :: [(BindType,Ident)] -> Term -> Term
+mkAbs xx t = foldr (uncurry Abs) t xx
 
 appCons :: Ident -> [Term] -> Term
 appCons = mkApp . Cn
@@ -186,7 +181,7 @@ mkLet :: [LocalDef] -> Term -> Term
 mkLet defs t = foldr Let t defs
 
 mkLetUntyped :: Context -> Term -> Term
-mkLetUntyped defs = mkLet [(x,(Nothing,t)) | (x,t) <- defs]
+mkLetUntyped defs = mkLet [(x,(Nothing,t)) | (_,x,t) <- defs]
 
 isVariable :: Term -> Bool
 isVariable (Vr _ ) = True
@@ -272,12 +267,12 @@ mkSelects t tt = foldl S t tt
 mkTable :: [Term] -> Term -> Term
 mkTable tt t = foldr Table t tt
 
-mkCTable :: [Ident] -> Term -> Term
+mkCTable :: [(BindType,Ident)] -> Term -> Term
 mkCTable ids v = foldr ccase v ids where 
-  ccase x t = T TRaw [(PV x,t)]
+  ccase (_,x) t = T TRaw [(PV x,t)]
 
 mkHypo :: Term -> Hypo
-mkHypo typ = (identW, typ)
+mkHypo typ = (Explicit,identW, typ)
 
 eqStrIdent :: Ident -> Ident -> Bool
 eqStrIdent = (==)
@@ -298,7 +293,7 @@ mkWildCases :: Term -> Term
 mkWildCases = mkCases identW
 
 mkFunType :: [Type] -> Type -> Type
-mkFunType tt t = mkProd ([(identW, ty) | ty <- tt], t, []) -- nondep prod
+mkFunType tt t = mkProd ([(Explicit,identW, ty) | ty <- tt], t, []) -- nondep prod
 
 plusRecType :: Type -> Type -> Err Type
 plusRecType t1 t2 = case (t1, t2) of
@@ -510,13 +505,13 @@ composOp co trm =
      do c' <- co c
         a' <- co a
         return (App c' a')
-   Abs x b ->
-     do b' <- co b
-        return (Abs x b')
-   Prod x a b -> 
+   Abs b x t ->
+     do t' <- co t
+        return (Abs b x t')
+   Prod b x a t -> 
      do a' <- co a
-        b' <- co b
-        return (Prod x a' b')
+        t' <- co t
+        return (Prod b x a' t')
    S c a -> 
      do c' <- co c
         a' <- co a
@@ -618,25 +613,25 @@ changeTableType co i = case i of
 
 collectOp :: (Term -> [a]) -> Term -> [a]
 collectOp co trm = case trm of
-  App c a    -> co c ++ co a 
-  Abs _ b    -> co b
-  Prod _ a b -> co a ++ co b 
-  S c a      -> co c ++ co a
-  Table a c  -> co a ++ co c
-  ExtR a c   -> co a ++ co c
-  R r        -> concatMap (\ (_,(mt,a)) -> maybe [] co mt ++ co a) r 
-  RecType r  -> concatMap (co . snd) r 
-  P t i      -> co t
-  T _ cc     -> concatMap (co . snd) cc -- not from patterns --- nor from type annot
-  TSh _ cc   -> concatMap (co . snd) cc -- not from patterns --- nor from type annot
-  V _ cc     -> concatMap co         cc --- nor from type annot
+  App c a      -> co c ++ co a 
+  Abs _ _ b    -> co b
+  Prod _ _ a b -> co a ++ co b 
+  S c a        -> co c ++ co a
+  Table a c    -> co a ++ co c
+  ExtR a c     -> co a ++ co c
+  R r          -> concatMap (\ (_,(mt,a)) -> maybe [] co mt ++ co a) r 
+  RecType r    -> concatMap (co . snd) r 
+  P t i        -> co t
+  T _ cc       -> concatMap (co . snd) cc -- not from patterns --- nor from type annot
+  TSh _ cc     -> concatMap (co . snd) cc -- not from patterns --- nor from type annot
+  V _ cc       -> concatMap co         cc --- nor from type annot
   Let (x,(mt,a)) b -> maybe [] co mt ++ co a ++ co b
-  C s1 s2    -> co s1 ++ co s2 
-  Glue s1 s2 -> co s1 ++ co s2 
-  Alts (t,aa) -> let (x,y) = unzip aa in co t ++ concatMap co (x ++ y)
-  FV ts      -> concatMap co ts
-  Strs tt    -> concatMap co tt
-  _ -> [] -- covers K, Vr, Cn, Sort
+  C s1 s2      -> co s1 ++ co s2 
+  Glue s1 s2   -> co s1 ++ co s2 
+  Alts (t,aa)  -> let (x,y) = unzip aa in co t ++ concatMap co (x ++ y)
+  FV ts        -> concatMap co ts
+  Strs tt      -> concatMap co tt
+  _            -> [] -- covers K, Vr, Cn, Sort
 
 -- | to find the word items in a term
 wordsInTerm :: Term -> [String]
@@ -653,12 +648,6 @@ noExist = FV []
 defaultLinType :: Type
 defaultLinType = mkRecType linLabel [typeStr]
 
--- | from GF1, 20\/9\/2003
-isInOneType :: Type -> Bool
-isInOneType t = case t of
-  Prod _ a b -> a == b
-  _ -> False
-
 -- normalize records and record types; put s first
 
 sortRec :: [(Label,a)] -> [(Label,a)]
diff --git a/src/GF/Grammar/Parser.y b/src/GF/Grammar/Parser.y
index 76458209c..a6d9ca455 100644
--- a/src/GF/Grammar/Parser.y
+++ b/src/GF/Grammar/Parser.y
@@ -344,6 +344,11 @@ ListIdent
   : Ident               { [$1]    } 
   | Ident ',' ListIdent { $1 : $3 }
 
+ListIdent2 :: { [Ident] }
+ListIdent2 
+  : Ident               { [$1]    } 
+  | Ident ListIdent2    { $1 : $2 }
+
 Name :: { Ident }
 Name
   : Ident         { $1          } 
@@ -492,11 +497,6 @@ Patt2
   | '<' ListPattTupleComp '>' { (PR . tuple2recordPatt) $2 }
   | '(' Patt ')'              { $2 }
 
-Arg :: { Ident }
-Arg 
-  : '_'                       { identW }
-  | Ident                     { $1     }
-
 PattAss :: { [(Label,Patt)] }
 PattAss
   : ListIdent '=' Patt { [(LIdent (ident2bs i),$3) | i <- $1] } 
@@ -525,25 +525,32 @@ ListPatt
   : Patt2          { [$1]    } 
   | Patt2 ListPatt { $1 : $2 }
 
-ListArg :: { [Ident] }
+Arg :: { [(BindType,Ident)] }
+Arg 
+  : Ident               { [(Explicit,$1    )]      }
+  | '_'                 { [(Explicit,identW)]      }
+  | '{' ListIdent2 '}'  { [(Implicit,v) | v <- $2] }
+  
+ListArg :: { [(BindType,Ident)] }
 ListArg
-  : Arg         { [$1]    } 
-  | Arg ListArg { $1 : $2 }
+  : Arg                 { $1       } 
+  | Arg ListArg         { $1 ++ $2 }
 
-Bind :: { Ident }
+Bind :: { [(BindType,Ident)] }
 Bind
-  : Ident  { $1     } 
-  | '_'    { identW }
+  : Ident               { [(Explicit,$1    )]      } 
+  | '_'                 { [(Explicit,identW)]      }
+  | '{' ListIdent '}'   { [(Implicit,v) | v <- $2] }
 
-ListBind :: { [Ident] }
+ListBind :: { [(BindType,Ident)] }
 ListBind
-  : Bind              { [$1]    }
-  | Bind ',' ListBind { $1 : $3 }
+  : Bind                { $1       }
+  | Bind ',' ListBind   { $1 ++ $3 }
 
 Decl :: { [Hypo] }
 Decl
-  : '(' ListBind ':' Exp ')' { [(x,$4) | x <- $2] } 
-  | Exp4                     { [mkHypo $1]        }
+  : '(' ListBind ':' Exp ')' { [(b,x,$4) | (b,x) <- $2] } 
+  | Exp4                     { [mkHypo $1]              }
 
 ListTupleComp :: { [Term] }
 ListTupleComp
@@ -577,8 +584,8 @@ ListAltern
 
 DDecl :: { [Hypo] }
 DDecl
-  : '(' ListBind ':' Exp ')' { [(x,$4) | x <- $2] } 
-  | Exp6                     { [mkHypo $1]        }
+  : '(' ListBind ':' Exp ')' { [(b,x,$4) | (b,x) <- $2] } 
+  | Exp6                     { [mkHypo $1]              }
 
 ListDDecl :: { [Hypo] }
 ListDDecl
@@ -603,6 +610,7 @@ mkBaseId = prefixId (BS.pack "Base")
 prefixId :: BS.ByteString -> Ident -> Ident
 prefixId pref id = identC (BS.append pref (ident2bs id))
 
+listCatDef :: Ident -> SrcSpan -> Context -> Int -> [(Ident,SrcSpan,Info)]
 listCatDef id pos cont size = [catd,nilfund,consfund]
   where
     listId = mkListId id
@@ -613,8 +621,8 @@ listCatDef id pos cont size = [catd,nilfund,consfund]
     nilfund  = (baseId, pos, AbsFun (Just niltyp)  Nothing Nothing)
     consfund = (consId, pos, AbsFun (Just constyp) Nothing Nothing)
 
-    cont' = [(mkId x i,ty) | (i,(x,ty)) <- zip [0..] cont]
-    xs = map (Vr . fst) cont'
+    cont' = [(b,mkId x i,ty) | (i,(b,x,ty)) <- zip [0..] cont]
+    xs = map (\(b,x,t) -> Vr x) cont'
     cd = mkHypo (mkApp (Vr id) xs)
     lc = mkApp (Vr listId) xs
 
diff --git a/src/GF/Grammar/PatternMatch.hs b/src/GF/Grammar/PatternMatch.hs
index 0fb23f531..828a2e365 100644
--- a/src/GF/Grammar/PatternMatch.hs
+++ b/src/GF/Grammar/PatternMatch.hs
@@ -146,7 +146,7 @@ isInConstantForm trm = case trm of
     Con _    -> True
     Q _ _    -> True
     QC _ _   -> True
-    Abs _ _  -> True
+    Abs _ _ _ -> True
     C c a    -> isInConstantForm c && isInConstantForm a
     App c a  -> isInConstantForm c && isInConstantForm a
     R r      -> all (isInConstantForm . snd . snd) r
diff --git a/src/GF/Grammar/Printer.hs b/src/GF/Grammar/Printer.hs
index 6a09548cd..e0edadbec 100644
--- a/src/GF/Grammar/Printer.hs
+++ b/src/GF/Grammar/Printer.hs
@@ -116,16 +116,16 @@ ppJudgement q (id, CncCat  ptype pexp pprn) =
      Nothing  -> empty)

 ppJudgement q (id, CncFun  ptype pdef pprn) =

   (case pdef of

-     Just e  -> let (vs,e') = getAbs e

-              in text "lin" <+> ppIdent id <+> hsep (map ppIdent vs) <+> equals <+> ppTerm q 0 e' <+> semi

+     Just e  -> let (xs,e') = getAbs e

+              in text "lin" <+> ppIdent id <+> hsep (map ppBind xs) <+> equals <+> ppTerm q 0 e' <+> semi

      Nothing -> empty) $$

   (case pprn of

      Just prn -> text "printname" <+> text "fun" <+> ppIdent id <+> equals <+> ppTerm q 0 prn <+> semi

      Nothing  -> empty)

 ppJudgement q (id, AnyInd cann mid) = text "ind" <+> ppIdent id <+> equals <+> (if cann then text "canonical" else empty) <+> ppIdent mid <+> semi

 

-ppTerm q d (Abs v e)   = let (vs,e') = getAbs e

-                         in prec d 0 (char '\\' <> commaPunct ppIdent (v:vs) <+> text "->" <+> ppTerm q 0 e')

+ppTerm q d (Abs b v e)   = let (xs,e') = getAbs (Abs b v e)

+                           in prec d 0 (char '\\' <> commaPunct ppBind xs <+> text "->" <+> ppTerm q 0 e')

 ppTerm q d (T TRaw xs) = case getCTable (T TRaw xs) of

                            ([],_) -> text "table" <+> lbrace $$

 	  		             nest 2 (vcat (punctuate semi (map (ppCase q) xs))) $$

@@ -140,9 +140,9 @@ ppTerm q d (T (TComp  t) xs) = text "table" <+> ppTerm q 0 t <+> lbrace $$
 ppTerm q d (T (TWild  t) xs) = text "table" <+> ppTerm q 0 t <+> lbrace $$

 			       nest 2 (vcat (punctuate semi (map (ppCase q) xs))) $$

 			       rbrace

-ppTerm q d (Prod x a b)= if x == identW

-                           then prec d 0 (ppTerm q 4 a <+> text "->" <+> ppTerm q 0 b)

-                           else prec d 0 (parens (ppIdent x <+> colon <+> ppTerm q 0 a) <+> text "->" <+> ppTerm q 0 b)

+ppTerm q d (Prod bt x a b)= if x == identW && bt == Explicit

+                              then prec d 0 (ppTerm q 4 a <+> text "->" <+> ppTerm q 0 b)

+                              else prec d 0 (parens (ppBind (bt,x) <+> colon <+> ppTerm q 0 a) <+> text "->" <+> ppTerm q 0 b)

 ppTerm q d (Table kt vt)=prec d 0 (ppTerm q 3 kt <+> text "=>" <+> ppTerm q 0 vt)

 ppTerm q d (Let l e)    = let (ls,e') = getLet e

                           in prec d 0 (text "let" <+> vcat (map (ppLocDef q) (l:ls)) $$ text "in" <+> ppTerm q 0 e')

@@ -246,11 +246,11 @@ ppEnv e = hcat (map (\(x,t) -> braces (ppIdent x <> text ":=" <> ppValue Unquali
 

 str s = doubleQuotes (text s)

 

-ppDecl q (id,typ)

+ppDecl q (_,id,typ)

   | id == identW = ppTerm q 4 typ

   | otherwise    = parens (ppIdent id <+> colon <+> ppTerm q 0 typ)

 

-ppDDecl q (id,typ)

+ppDDecl q (_,id,typ)

   | id == identW = ppTerm q 6 typ

   | otherwise    = parens (ppIdent id <+> colon <+> ppTerm q 0 typ)

 

@@ -272,6 +272,8 @@ ppLocDef q (id, (mbt, e)) =
   ppIdent id <+>

   (case mbt of {Just t -> colon  <+> ppTerm q 0 t; Nothing -> empty} <+> equals <+> ppTerm q 0 e) <+> semi

 

+ppBind (Explicit,v) = ppIdent v

+ppBind (Implicit,v) = braces (ppIdent v)

 

 ppAltern q (x,y) = ppTerm q 0 x <+> char '/' <+> ppTerm q 0 y

 

@@ -283,10 +285,10 @@ prec d1 d2 doc
   | d1 > d2   = parens doc

   | otherwise = doc

 

-getAbs :: Term -> ([Ident], Term)

-getAbs (Abs v e) = let (vs,e') = getAbs e

-                   in (v:vs,e')

-getAbs e         = ([],e)

+getAbs :: Term -> ([(BindType,Ident)], Term)

+getAbs (Abs bt v e) = let (xs,e') = getAbs e

+                      in ((bt,v):xs,e')

+getAbs e            = ([],e)

 

 getCTable :: Term -> ([Ident], Term)

 getCTable (T TRaw [(PV v,e)]) = let (vs,e') = getCTable e

diff --git a/src/GF/Grammar/Unify.hs b/src/GF/Grammar/Unify.hs
index 8ac5351e1..9bb49cfe2 100644
--- a/src/GF/Grammar/Unify.hs
+++ b/src/GF/Grammar/Unify.hs
@@ -60,8 +60,8 @@ unify e1 e2 g =
   (Q _ a, Q _ b) | (a == b)      -> return g ---- qualif?
   (QC _ a, QC _ b) | (a == b)    -> return g ----
   (Vr x, Vr y) | (x == y)        -> return g 
-  (Abs x b, Abs y c)               -> do let c' = substTerm [x] [(y,Vr x)] c 
-                                         unify b c' g
+  (Abs _ x b, Abs _ y c)         -> do let c' = substTerm [x] [(y,Vr x)] c 
+                                       unify b c' g
   (App c a, App d b)            -> case unify c d g of 
                                      Ok g1 -> unify a b g1 
                                      _     -> Bad (render (text "fail unify" <+> ppTerm Unqualified 0 e1))
@@ -92,6 +92,6 @@ occCheck :: MetaId -> Term -> Bool
 occCheck s u = case u of
     Meta v  -> s == v
     App c a -> occCheck s c || occCheck s a
-    Abs x b -> occCheck s b
+    Abs _ x b -> occCheck s b
     _       -> False