some work on evaluation with abstract expressions in PGF

src/GF/Command/Commands.hs

@@ -600,7 +600,7 @@ allCommands cod env@(pgf, mos) = Map.fromList [
      exec = \opts arg -> do
        case arg of
          [Fun id []] -> case Map.lookup id (funs (abstract pgf)) of
-                          Just (ty,eqs) -> return $ fromString $
+                          Just (ty,_,eqs) -> return $ fromString $
                                               render (text "fun" <+> text (prCId id) <+> colon <+> ppType 0 ty $$
                                                       if null eqs
                                                         then empty

src/GF/Compile/AbsCompute.hs

@@ -42,7 +42,7 @@ computeAbsTerm :: Grammar -> Exp -> Err Exp
 computeAbsTerm gr = computeAbsTermIn (lookupAbsDef gr) []
 
 -- | a hack to make compute work on source grammar as well
-type LookDef = Ident -> Ident -> Err (Maybe [Equation])
+type LookDef = Ident -> Ident -> Err (Maybe Int,Maybe [Equation])
 
 computeAbsTermIn :: LookDef -> [Ident] -> Exp -> Err Exp
 computeAbsTermIn lookd xs e = errIn ("computing" +++ prt e) $ compt xs e where
@@ -73,7 +73,7 @@ computeAbsTermIn lookd xs e = errIn ("computing" +++ prt e) $ compt xs e where
 
   look t = case t of
      (Q m f) -> case lookd m f of
-       Ok md -> md
+       Ok (_,md) -> md
        _ -> Nothing
      _ -> Nothing
 

src/GF/Compile/CheckGrammar.hs

@@ -123,7 +123,7 @@ checkAbsInfo st m mo (c,info) = do
  case info of
    AbsCat (Just cont) _ -> mkCheck "category" $ 
      checkContext st cont ---- also cstrs
-   AbsFun (Just typ0) md -> do
+   AbsFun (Just typ0) ma md -> do
      typ <- compAbsTyp [] typ0   -- to calculate let definitions
      mkCheck "type of function" $
        checkTyp st typ
@@ -131,7 +131,7 @@ checkAbsInfo st m mo (c,info) = do
        Just eqs -> mkCheck "definition of function" $
 	             checkDef st (m,c) typ eqs
        Nothing  -> return (c,info)
-     return $ (c,AbsFun (Just typ) md)
+     return $ (c,AbsFun (Just typ) ma md)
    _ -> return (c,info)
  where
    mkCheck cat ss = case ss of
@@ -181,28 +181,28 @@ checkCompleteGrammar gr abs cnc = do
      CncCat _ _ _ -> True
      _ -> False
    checkOne js i@(c,info) = case info of
-     AbsFun (Just ty) _ -> do let mb_def = do
+     AbsFun (Just ty) _ _ -> do let mb_def = do
-                                    (cxt,(_,i),_) <- typeForm ty
+                                      (cxt,(_,i),_) <- typeForm ty
-                                    info <- lookupIdent i js
+                                      info <- lookupIdent i js
-                                    info <- case info of
+                                      info <- case info of
-                                              (AnyInd _ m) -> do (m,info) <- lookupOrigInfo gr m i
+                                                (AnyInd _ m) -> do (m,info) <- lookupOrigInfo gr m i
-                                                                 return info
+                                                                   return info
-                                              _            -> return info
+                                                _            -> return info
-                                    case info of
+                                      case info of
-                                      CncCat (Just (RecType [])) _ _ -> return (foldr (\_ -> Abs identW) (R []) cxt)
+                                        CncCat (Just (RecType [])) _ _ -> return (foldr (\_ -> Abs identW) (R []) cxt)
-                                      _                              -> Bad "no def lin"
+                                        _                              -> Bad "no def lin"
-                              case lookupIdent c js of
+                                case lookupIdent c js of
-                                Ok (CncFun _   (Just _) _ ) -> return js
+                                  Ok (CncFun _   (Just _) _ ) -> return js
-                                Ok (CncFun cty Nothing  pn) ->
+                                  Ok (CncFun cty Nothing  pn) ->
-                                  case mb_def of
+                                    case mb_def of
-                                    Ok def -> return $ updateTree (c,CncFun cty (Just def) pn) js
+                                      Ok def -> return $ updateTree (c,CncFun cty (Just def) pn) js
-                                    Bad _  -> do checkWarn $ "no linearization of" +++ prt c
+                                      Bad _  -> do checkWarn $ "no linearization of" +++ prt c
-                                                 return js
+                                                   return js
-                                _ -> do
+                                  _ -> do
-                                  case mb_def of
+                                    case mb_def of
-                                    Ok def -> return $ updateTree (c,CncFun Nothing (Just def) Nothing) js
+                                      Ok def -> return $ updateTree (c,CncFun Nothing (Just def) Nothing) js
-                                    Bad _  -> do checkWarn $ "no linearization of" +++ prt c
+                                      Bad _  -> do checkWarn $ "no linearization of" +++ prt c
-                                                 return js
+                                                   return js
      AbsCat (Just _) _ -> case lookupIdent c js of
        Ok (AnyInd _ _) -> return js
        Ok (CncCat (Just _) _ _) -> return js
@@ -1115,7 +1115,7 @@ allDependencies ism b =
       ResParam (Just (ps,_)) -> [Just t | (_,cont) <- ps, (_,t) <- cont]
       CncCat pty _ _ -> [pty]
       CncFun _   pt _ -> [pt]  ---- (Maybe (Ident,(Context,Type))
-      AbsFun pty ptr -> [pty] --- ptr is def, which can be mutual
+      AbsFun pty _ ptr -> [pty] --- ptr is def, which can be mutual
       AbsCat (Just co) _ -> [Just ty | (_,ty) <- co]
       _              -> []
 

src/GF/Compile/GFCCtoHaskell.hs

@@ -201,7 +201,7 @@ hSkeleton gr =
    fns = groupBy valtypg (sortBy valtyps (map jty (Map.assocs (funs (abstract gr)))))
    valtyps (_, (_,x)) (_, (_,y)) = compare x y
    valtypg (_, (_,x)) (_, (_,y)) = x == y
-   jty (f,(ty,_)) = (f,catSkeleton ty)
+   jty (f,(ty,_,_)) = (f,catSkeleton ty)
 
 updateSkeleton :: OIdent -> HSkeleton -> (OIdent, [OIdent]) -> HSkeleton
 updateSkeleton cat skel rule =

src/GF/Compile/GFCCtoJS.hs

@@ -34,8 +34,8 @@ pgf2js pgf =
 abstract2js :: String -> Abstr -> JS.Expr
 abstract2js start ds = new "GFAbstract" [JS.EStr start, JS.EObj $ map absdef2js (Map.assocs (funs ds))]
 
-absdef2js :: (CId,(Type,[Equation])) -> JS.Property
+absdef2js :: (CId,(Type,Int,[Equation])) -> JS.Property
-absdef2js (f,(typ,_)) =
+absdef2js (f,(typ,_,_)) =
   let (args,cat) = M.catSkeleton typ in 
     JS.Prop (JS.IdentPropName (JS.Ident (prCId f))) (new "Type" [JS.EArray [JS.EStr (prCId x) | x <- args], JS.EStr (prCId cat)])
 

src/GF/Compile/GFCCtoProlog.hs

@@ -71,16 +71,16 @@ plCat (cat, hypos) = plFact "cat" (plTypeWithHypos typ)
           args = reverse [EVar x | (_,x) <- subst]
           typ = wildcardUnusedVars $ DTyp hypos' cat args
 
-plFun :: (CId, (Type, [Equation])) -> String
+plFun :: (CId, (Type, Int, [Equation])) -> String
-plFun (fun, (typ, _)) = plFact "fun" (plp fun : plTypeWithHypos typ')
+plFun (fun, (typ,_,_)) = plFact "fun" (plp fun : plTypeWithHypos typ')
     where typ' = wildcardUnusedVars $ snd $ alphaConvert emptyEnv typ
 
 plTypeWithHypos :: Type -> [String]
 plTypeWithHypos (DTyp hypos cat args) = [plTerm (plp cat) (map plp args), plp hypos]
 
-plFundef :: (CId, (Type, [Equation])) -> [String]
+plFundef :: (CId, (Type,Int,[Equation])) -> [String]
-plFundef (fun, (_, [])) = []
+plFundef (fun, (_,_,[])) = []
-plFundef (fun, (_, eqs)) = [plFact "def" [plp fun, plp fundef']]
+plFundef (fun, (_,_,eqs)) = [plFact "def" [plp fun, plp fundef']]
     where fundef' = snd $ alphaConvert emptyEnv eqs
 
 

src/GF/Compile/GenerateFCFG.hs

@@ -43,30 +43,30 @@ convertConcrete abs cnc = fixHoasFuns $ convert abs_defs' conc' cats'
              cats = lincats cnc
              (abs_defs',conc',cats') = expandHOAS abs_defs conc cats
 
-expandHOAS :: [(CId,(Type,[Equation]))] -> TermMap -> TermMap -> ([(CId,(Type,[Equation]))],TermMap,TermMap)
+expandHOAS :: [(CId,(Type,Int,[Equation]))] -> TermMap -> TermMap -> ([(CId,(Type,Int,[Equation]))],TermMap,TermMap)
 expandHOAS funs lins lincats = (funs' ++ hoFuns ++ varFuns, 
                                 Map.unions [lins, hoLins, varLins], 
                                 Map.unions [lincats, hoLincats, varLincat])
     where
       -- replace higher-order fun argument types with new categories
-      funs' = [(f,(fixType ty,e)) | (f,(ty,e)) <- funs]
+      funs' = [(f,(fixType ty,a,e)) | (f,(ty,a,e)) <- funs]
           where
             fixType :: Type -> Type
             fixType ty = let (ats,rt) = typeSkeleton ty in cftype (map catName ats) rt
 
       hoTypes :: [(Int,CId)]
-      hoTypes = sortNub [(n,c) | (_,(ty,_)) <- funs, (n,c) <- fst (typeSkeleton ty), n > 0]
+      hoTypes = sortNub [(n,c) | (_,(ty,_,_)) <- funs, (n,c) <- fst (typeSkeleton ty), n > 0]
       hoCats = sortNub (map snd hoTypes)
       -- for each Cat with N bindings, we add a new category _NCat
       -- each new category contains a single function __NCat : Cat -> _Var -> ... -> _Var -> _NCat
-      hoFuns = [(funName ty,(cftype (c : replicate n varCat) (catName ty),[])) | ty@(n,c) <- hoTypes]
+      hoFuns = [(funName ty,(cftype (c : replicate n varCat) (catName ty),0,[])) | ty@(n,c) <- hoTypes]
       -- lincats for the new categories
       hoLincats = Map.fromList [(catName ty, modifyRec (++ replicate n (S [])) (lincatOf c)) | ty@(n,c) <- hoTypes]
       -- linearizations of the new functions, lin __NCat v_0 ... v_n-1 x = { s1 = x.s1; ...; sk = x.sk; $0 = v_0.s ...
       hoLins = Map.fromList [ (funName ty, mkLin c n) | ty@(n,c) <- hoTypes]
           where mkLin c n = modifyRec (\fs -> [P (V 0) (C j) | j <- [0..length fs-1]] ++ [P (V i) (C 0) | i <- [1..n]]) (lincatOf c)
       -- for each Cat, we a add a fun _Var_Cat : _Var -> Cat
-      varFuns = [(varFunName cat, (cftype [varCat] cat,[])) | cat <- hoCats]
+      varFuns = [(varFunName cat, (cftype [varCat] cat,0,[])) | cat <- hoCats]
       -- linearizations of the _Var_Cat functions
       varLins = Map.fromList [(varFunName cat, R [P (V 0) (C 0)]) | cat <- hoCats]
       -- lincat for the _Var category
@@ -98,12 +98,12 @@ fixHoasFuns pinfo = pinfo{functions=mkArray [FFun (fixName n) prof lins | FFun n
                         | BS.pack "_Var_" `BS.isPrefixOf` n = wildCId
         fixName n = n
 
-convert :: [(CId,(Type,[Equation]))] -> TermMap -> TermMap -> ParserInfo
+convert :: [(CId,(Type,Int,[Equation]))] -> TermMap -> TermMap -> ParserInfo
 convert abs_defs cnc_defs cat_defs = getParserInfo (loop grammarEnv)
       where
         srules = [
           (XRule id args res (map findLinType args) (findLinType res) term) | 
-            (id, (ty,_)) <- abs_defs, let (args,res) = catSkeleton ty, 
+            (id, (ty,_,_)) <- abs_defs, let (args,res) = catSkeleton ty, 
             term <- maybeToList (Map.lookup id cnc_defs)]
         
         findLinType id = fromMaybe (error $ "No lincat for " ++ show id) (Map.lookup id cat_defs)

src/GF/Compile/GeneratePMCFG.hs

@@ -38,14 +38,14 @@ convertConcrete abs cnc = convert abs_defs conc cats
              conc = Map.union (opers cnc) (lins cnc) -- "union big+small most efficient"
              cats = lincats cnc
 
-convert :: [(CId,(Type,[Equation]))] -> TermMap -> TermMap -> ParserInfo
+convert :: [(CId,(Type,Int,[Equation]))] -> TermMap -> TermMap -> ParserInfo
 convert abs_defs cnc_defs cat_defs =
   let env = expandHOAS abs_defs cnc_defs cat_defs (emptyGrammarEnv cnc_defs cat_defs)
   in getParserInfo (List.foldl' (convertRule cnc_defs) env pfrules)
   where
     pfrules = [
       (PFRule id args (0,res) (map findLinType args) (findLinType (0,res)) term) | 
-        (id, (ty,_)) <- abs_defs, let (args,res) = typeSkeleton ty, 
+        (id, (ty,_,_)) <- abs_defs, let (args,res) = typeSkeleton ty, 
         term <- maybeToList (Map.lookup id cnc_defs)]
         
     findLinType (_,id) = fromMaybe (error $ "No lincat for " ++ show id) (Map.lookup id cat_defs)
@@ -320,11 +320,11 @@ expandHOAS abs_defs cnc_defs lincats env =
   foldl add_varFun (foldl (\env ncat -> add_hoFun (add_hoCat env ncat) ncat) env hoTypes) hoCats
   where
     hoTypes :: [(Int,CId)]
-    hoTypes = sortNub [(n,c) | (_,(ty,_)) <- abs_defs
+    hoTypes = sortNub [(n,c) | (_,(ty,_,_)) <- abs_defs
                              , (n,c) <- fst (typeSkeleton ty), n > 0]
 
     hoCats :: [CId]
-    hoCats = sortNub [c | (_,(ty,_)) <- abs_defs
+    hoCats = sortNub [c | (_,(ty,_,_)) <- abs_defs
                         , Hyp _ ty <- case ty of {DTyp hyps val _ -> hyps}
                         , c   <- fst (catSkeleton ty)]
   

src/GF/Compile/GrammarToGFCC.hs

@@ -71,16 +71,19 @@ canon2gfcc opts pars cgr@(M.MGrammar ((a,abm):cms)) =
 
   mkDef (Just eqs) = [C.Equ (map mkPatt ps) (mkExp e) | (ps,e) <- eqs]
   mkDef Nothing    = []
+  
+  mkArrity (Just a) = a
+  mkArrity Nothing  = 0
 
   -- concretes
-  lfuns = [(f', (mkType ty, mkDef pty)) | 
+  lfuns = [(f', (mkType ty, mkArrity ma, mkDef pty)) | 
-             (f,AbsFun (Just ty) pty) <- tree2list (M.jments abm), let f' = i2i f]
+             (f,AbsFun (Just ty) ma pty) <- tree2list (M.jments abm), let f' = i2i f]
   funs = Map.fromAscList lfuns
   lcats = [(i2i c, mkContext cont) |
                 (c,AbsCat (Just cont) _) <- tree2list (M.jments abm)]
   cats = Map.fromAscList lcats
   catfuns = Map.fromList 
-    [(cat,[f | (f, (C.DTyp _ c _,_)) <- lfuns, c==cat]) | (cat,_) <- lcats]
+    [(cat,[f | (f, (C.DTyp _ c _,_,_)) <- lfuns, c==cat]) | (cat,_) <- lcats]
 
   cncs  = Map.fromList [mkConcr lang (i2i lang) mo | (lang,mo) <- cms]
   mkConcr lang0 lang mo = 

src/GF/Compile/PGFPretty.hs

@@ -31,8 +31,8 @@ prCat :: CId -> [Hypo] -> Doc
 prCat c h | isLiteralCat c = empty
           | otherwise = text "cat" <+> text (prCId c)
 
-prFun :: CId -> (Type,[Equation]) -> Doc
+prFun :: CId -> (Type,Int,[Equation]) -> Doc
-prFun f (t,_) = text "fun" <+> text (prCId f) <+> text ":" <+> prType t
+prFun f (t,_,_) = text "fun" <+> text (prCId f) <+> text ":" <+> prType t
 
 prType :: Type -> Doc
 prType t = parens (hsep (punctuate (text ",") (map (text . prCId) cs))) <+> text "->" <+> text (prCId c)

src/GF/Compile/Rename.hs

@@ -116,7 +116,7 @@ renameIdentPatt env p = do
 
 info2status :: Maybe Ident -> (Ident,Info) -> StatusInfo
 info2status mq (c,i) = case i of
-  AbsFun _ Nothing -> maybe Con QC mq
+  AbsFun _ _ Nothing -> maybe Con QC mq
   ResValue _  -> maybe Con QC mq
   ResParam _  -> maybe Con QC mq
   AnyInd True m -> maybe Con (const (QC m)) mq
@@ -156,7 +156,7 @@ renameInfo mo status (i,info) = errIn
                                 liftM ((,) i) $ case info of
   AbsCat pco pfs -> liftM2 AbsCat (renPerh (renameContext status) pco)
                                   (renPerh (mapM rent) pfs)
-  AbsFun  pty ptr -> liftM2 AbsFun (ren pty) (renPerh (mapM (renameEquation status [])) ptr)
+  AbsFun  pty pa ptr -> liftM3 AbsFun (ren pty) (return pa) (renPerh (mapM (renameEquation status [])) ptr)
   ResOper pty ptr -> liftM2 ResOper (ren pty) (ren ptr)
   ResOverload os tysts -> 
     liftM (ResOverload os) (mapM (pairM rent) tysts)

src/GF/Compile/TC.hs

@@ -236,7 +236,6 @@ checkBranch th tenv b@(ps,t) ty = errIn ("branch" +++ show b) $
   ps2ts k = foldr p2t ([],0,[],k) 
   p2t p (ps,i,g,k) = case p of
      PW      -> (Meta (MetaSymb i) : ps, i+1,g,k) 
-     PV IW   -> (Meta (MetaSymb i) : ps, i+1,g,k) 
      PV x    -> (Vr x   : ps, i, upd x k g,k+1)
      PString s -> (K s : ps, i, g, k)
      PInt n -> (EInt n : ps, i, g, k)

src/GF/Compile/Update.hs

@@ -163,7 +163,7 @@ extendMod gr isCompl (name,cond) base old new = foldM try new $ Map.toList old
       (b,n') = case info of
         ResValue _ -> (True,n)
         ResParam _ -> (True,n)
-        AbsFun _ Nothing -> (True,n) 
+        AbsFun _ _ Nothing -> (True,n) 
         AnyInd b k -> (b,k)
         _ -> (False,n) ---- canonical in Abs
 
@@ -171,8 +171,8 @@ unifyAnyInfo :: Ident -> Info -> Info -> Err Info
 unifyAnyInfo m i j = case (i,j) of
   (AbsCat mc1 mf1, AbsCat mc2 mf2) -> 
     liftM2 AbsCat (unifMaybe mc1 mc2) (unifConstrs mf1 mf2) -- adding constrs
-  (AbsFun mt1 md1, AbsFun mt2 md2) -> 
+  (AbsFun mt1 ma1 md1, AbsFun mt2 ma2 md2) -> 
-    liftM2 AbsFun (unifMaybe mt1 mt2) (unifAbsDefs md1 md2) -- adding defs
+    liftM3 AbsFun (unifMaybe mt1 mt2) (unifAbsArrity ma1 ma2) (unifAbsDefs md1 md2) -- adding defs
 
   (ResParam mt1, ResParam mt2) -> liftM ResParam $ unifMaybe mt1 mt2
   (ResValue mt1, ResValue mt2) -> 
@@ -203,6 +203,14 @@ unifMaybe (Just p1) (Just p2)
   | p1==p2                    = return (Just p1)
   | otherwise                 = fail ""
 
+unifAbsArrity :: Maybe Int -> Maybe Int -> Err (Maybe Int)
+unifAbsArrity Nothing   Nothing   = return Nothing
+unifAbsArrity (Just a ) Nothing   = return (Just a )
+unifAbsArrity Nothing   (Just a ) = return (Just a )
+unifAbsArrity (Just a1) (Just a2)
+  | a1==a2                        = return (Just a1)
+  | otherwise                     = fail ""
+
 unifAbsDefs :: Maybe [Equation] -> Maybe [Equation] -> Err (Maybe [Equation])
 unifAbsDefs Nothing   Nothing   = return Nothing
 unifAbsDefs (Just _ ) Nothing   = fail ""

src/GF/Grammar/Binary.hs

@@ -90,7 +90,7 @@ instance Binary Options where
 
 instance Binary Info where
   put (AbsCat x y)     = putWord8 0 >> put (x,y)
-  put (AbsFun x y)     = putWord8 1 >> put (x,y)
+  put (AbsFun x y z)   = putWord8 1 >> put (x,y,z)
   put (ResParam x)     = putWord8 2 >> put x
   put (ResValue x)     = putWord8 3 >> put x
   put (ResOper x y)    = putWord8 4 >> put (x,y)
@@ -101,7 +101,7 @@ instance Binary Info where
   get = do tag <- getWord8
            case tag of
              0 -> get >>= \(x,y)   -> return (AbsCat x y)
-             1 -> get >>= \(x,y)   -> return (AbsFun x y)
+             1 -> get >>= \(x,y,z) -> return (AbsFun x y z)
              2 -> get >>= \x       -> return (ResParam x)
              3 -> get >>= \x       -> return (ResValue x)
              4 -> get >>= \(x,y)   -> return (ResOper x y)

src/GF/Grammar/Grammar.hs

@@ -41,7 +41,6 @@ module GF.Grammar.Grammar (SourceGrammar,
 		Param,
 		Altern,
 		Substitution,
-		wildPatt,
 		varLabel, tupleLabel, linLabel, theLinLabel,
 		ident2label, label2ident
 	       ) where
@@ -80,8 +79,8 @@ type PValues = [Term]
 -- and indirection to module (/INDIR/)
 data Info =
 -- judgements in abstract syntax
-   AbsCat   (Maybe Context) (Maybe [Term])   -- ^ (/ABS/) constructors; must be 'Id' or 'QId'
+   AbsCat   (Maybe Context) (Maybe [Term])               -- ^ (/ABS/) the second parameter is list of constructors - must be 'Id' or 'QId'
- | AbsFun   (Maybe Type) (Maybe [Equation])  -- ^ (/ABS/)
+ | AbsFun   (Maybe Type) (Maybe Int) (Maybe [Equation])  -- ^ (/ABS/) type, arrity and definition of function
 
 -- judgements in resource
  | ResParam (Maybe ([Param],Maybe PValues))  -- ^ (/RES/)
@@ -229,6 +228,3 @@ ident2label c = LIdent (ident2bs c)
 label2ident :: Label -> Ident
 label2ident (LIdent s) = identC s
 label2ident (LVar i)   = identC (BS.pack ('$':show i))
-
-wildPatt :: Patt
-wildPatt = PV identW

src/GF/Grammar/Lookup.hs

@@ -121,7 +121,7 @@ lookupResType gr m c = do
           mu <- lookupModule gr a
           info <- lookupIdentInfo mu c
           case info of
-            AbsFun (Just ty) _ -> return $ redirectTerm e ty 
+            AbsFun (Just ty) _ _ -> return $ redirectTerm e ty 
             AbsCat _ _ -> return typeType
             AnyInd _ n -> lookFun e m c n
             _ -> prtBad "cannot find type of reused function" c
@@ -227,14 +227,14 @@ qualifAnnotPar m t = case t of
   Con c -> QC m c
   _ -> composSafeOp (qualifAnnotPar m) t
 
-lookupAbsDef :: SourceGrammar -> Ident -> Ident -> Err (Maybe [Equation])
+lookupAbsDef :: SourceGrammar -> Ident -> Ident -> Err (Maybe Int,Maybe [Equation])
 lookupAbsDef gr m c = errIn ("looking up absdef of" +++ prt c) $ do
   mo <- lookupModule gr m
   info <- lookupIdentInfo mo c
   case info of
-    AbsFun _ (Just t) -> return (Just t)
+    AbsFun _ a d -> return (a,d)
-    AnyInd _ n        -> lookupAbsDef gr n c
+    AnyInd _ n   -> lookupAbsDef gr n c
-    _                 -> return Nothing
+    _            -> return (Nothing,Nothing)
 
 lookupLincat :: SourceGrammar -> Ident -> Ident -> Err Type
 lookupLincat gr m c | isPredefCat c = return defLinType --- ad hoc; not needed?
@@ -252,9 +252,9 @@ lookupFunType gr m c = do
   mo <- lookupModule gr m
   info <- lookupIdentInfo mo c
   case info of
-    AbsFun (Just t) _  -> return t
+    AbsFun (Just t) _ _  -> return t
-    AnyInd _ n         -> lookupFunType gr n c
+    AnyInd _ n           -> lookupFunType gr n c
-    _                  -> prtBad "cannot find type of" c
+    _                    -> prtBad "cannot find type of" c
 
 -- | this is needed at compile time
 lookupCatContext :: SourceGrammar -> Ident -> Ident -> Err Context
@@ -281,7 +281,7 @@ opersForType gr orig val =
       let cat = err error snd (valCat orig) in --- ignore module
       [(f,ty) |
         Ok a <- [abstractOfConcrete gr i >>= lookupModule gr],
-        (f, AbsFun (Just ty0) _) <- tree2list $ jments a,
+        (f, AbsFun (Just ty0) _ _) <- tree2list $ jments a,
         let ty = redirectTerm i ty0,
         Ok valt  <- [valCat ty],
         cat == snd valt ---

src/GF/Grammar/Macros.hs

@@ -414,7 +414,8 @@ linAsStr s = mkRecord linLabel [K s] -- default linearization {s = s}
 
 term2patt :: Term -> Err Patt
 term2patt trm = case termForm trm of
-  Ok ([], Vr x, []) -> return (PV x)
+  Ok ([], Vr x, []) | x == identW -> return PW
+                    | otherwise   -> return (PV x)
   Ok ([], Val te ty x, []) -> do
     te' <- term2patt te
     return (PVal te' ty x)

src/GF/Grammar/Parser.y

@@ -240,19 +240,19 @@ CatDef
 
 FunDef :: { [(Ident,SrcSpan,Info)] }
 FunDef
-  : Posn ListIdent ':' Exp Posn { [(fun, ($1,$5), AbsFun (Just $4) (Just [])) | fun <- $2] } 
+  : Posn ListIdent ':' Exp Posn { [(fun, ($1,$5), AbsFun (Just $4) Nothing (Just [])) | fun <- $2] } 
 
 DefDef :: { [(Ident,SrcSpan,Info)] }
 DefDef
-  : Posn ListName '=' Exp         Posn { [(f, ($1,$5),AbsFun Nothing (Just [([],$4)])) | f <- $2] }
+  : Posn ListName '=' Exp         Posn { [(f, ($1,$5),AbsFun Nothing (Just 0) (Just [([],$4)])) | f <- $2] }
-  | Posn Name ListPatt '=' Exp    Posn { [($2,($1,$6),AbsFun Nothing (Just [($3,$5)]))] }
+  | Posn Name ListPatt '=' Exp    Posn { [($2,($1,$6),AbsFun Nothing (Just (length $3)) (Just [($3,$5)]))] }
 
 DataDef :: { [(Ident,SrcSpan,Info)] }
 DataDef
   : Posn Ident '=' ListDataConstr Posn { ($2,   ($1,$5), AbsCat Nothing   (Just (map Cn $4))) :
-                                         [(fun, ($1,$5), AbsFun Nothing   Nothing) | fun <- $4] }
+                                         [(fun, ($1,$5), AbsFun Nothing   Nothing Nothing) | fun <- $4] }
   | Posn ListIdent ':' Exp Posn        { [(cat, ($1,$5), AbsCat Nothing   (Just (map Cn $2))) | Ok (_,cat) <- [valCat $4]] ++
-                                         [(fun, ($1,$5), AbsFun (Just $4) Nothing) | fun <- $2] }                                         
+                                         [(fun, ($1,$5), AbsFun (Just $4) Nothing Nothing) | fun <- $2] }                                         
 
 ParamDef :: { [(Ident,SrcSpan,Info)] }
 ParamDef
@@ -481,7 +481,7 @@ Patt2
   | '[' String ']'            { PChars $2 }
   | '#' Ident                 { PMacro $2 }
   | '#' Ident '.' Ident       { PM $2 $4 }
-  | '_'                       { wildPatt }
+  | '_'                       { PW }
   | Ident                     { PV $1 }
   | Ident '.' Ident           { PP $1 $3 [] }
   | Integer                   { PInt $1 }
@@ -609,8 +609,8 @@ listCatDef id pos cont size = [catd,nilfund,consfund]
     consId = mkConsId id
 
     catd     = (listId, pos, AbsCat (Just cont')   (Just [Cn baseId,Cn consId]))
-    nilfund  = (baseId, pos, AbsFun (Just niltyp)  Nothing)
+    nilfund  = (baseId, pos, AbsFun (Just niltyp)  Nothing Nothing)
-    consfund = (consId, pos, AbsFun (Just constyp) 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'
@@ -667,7 +667,7 @@ type SrcSpan = (Posn,Posn)
 checkInfoType MTAbstract       (id,pos,info) =
   case info of
     AbsCat _ _   -> return ()
-    AbsFun _ _   -> return ()
+    AbsFun _ _ _ -> return ()
     _            -> failLoc (fst pos) "illegal definition in abstract module" 
 checkInfoType MTResource       (id,pos,info) =
   case info of
@@ -701,7 +701,7 @@ checkInfoType (MTInstance _)   (id,pos,info) =
 checkInfoType (MTTransfer _ _) (id,pos,info) =
   case info of
     AbsCat _ _   -> return ()
-    AbsFun _ _   -> return ()
+    AbsFun _ _ _ -> return ()
     _            -> failLoc (fst pos) "illegal definition in transfer module" 
 
 

src/GF/Grammar/Printer.hs

@@ -79,7 +79,7 @@ ppJudgement q (id, AbsCat pcont pconstrs) =
   case pconstrs of
     Just costrs -> text "data" <+> ppIdent id <+> equals <+> fsep (intersperse (char '|') (map (ppTerm q 0) costrs)) <+> semi
     Nothing     -> empty
-ppJudgement q (id, AbsFun ptype pexp) =
+ppJudgement q (id, AbsFun ptype _ pexp) =
   (case ptype of
      Just typ   -> text "fun" <+> ppIdent id <+> colon <+> ppTerm q 0 typ <+> semi
      Nothing    -> empty) $$

src/GF/Source/CF.hs

@@ -105,7 +105,7 @@ cf2cat (_,(cat, items)) = map identS $ cat : [c | Left c <- items]
 cf2rule :: CFRule -> ((Ident,Info),(Ident,Info))
 cf2rule (fun, (cat, items)) = (def,ldef) where
   f     = identS fun
-  def   = (f, AbsFun (Just (mkProd (args', Cn (identS cat), []))) Nothing)
+  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]

src/GF/Source/GrammarToSource.hs

@@ -75,9 +75,9 @@ mkTopDefs ds = ds
 trAnyDef :: (Ident,Info) -> [P.TopDef]
 trAnyDef (i,info) = let i' = tri i in case info of
   AbsCat (Just co) pd -> [P.DefCat [P.SimpleCatDef i' (map trDecl co)]]
-  AbsFun (Just ty) Nothing    -> [P.DefFunData [P.FunDef [i'] (trt ty)]]
+  AbsFun (Just ty) _ Nothing    -> [P.DefFunData [P.FunDef [i'] (trt ty)]]
-  AbsFun (Just ty) (Just eqs) -> [P.DefFun [P.FunDef [i'] (trt ty)]] ++
+  AbsFun (Just ty) _ (Just eqs) -> [P.DefFun [P.FunDef [i'] (trt ty)]] ++
-                                 [P.DefDef [P.DPatt (mkName i') (map trp patts) (trt res)] | (patts,res) <- eqs]
+                                   [P.DefDef [P.DPatt (mkName i') (map trp patts) (trt res)] | (patts,res) <- eqs]
 
   ResOper pty ptr -> [P.DefOper [trDef i' pty ptr]]
   ResParam pp -> [P.DefPar [case pp of

src/GF/Source/SourceToGrammar.hs

@@ -585,7 +585,7 @@ transPatts p = case p of
 
 transPatt :: Patt -> Err G.Patt
 transPatt x = case x of
-  PW  -> return G.wildPatt
+  PW  -> return G.PW
   PV id  -> liftM G.PV $ transIdent id
   PC id patts  -> liftM2 G.PC (transIdent id) (mapM transPatt patts)
   PCon id  -> liftM2 G.PC (transIdent id) (return [])

src/PGF/Binary.hs

@@ -42,7 +42,7 @@ instance Binary Abstr where
   get = do aflags <- get
            funs <- get
            cats <- get
-           let catfuns = Map.mapWithKey (\cat _ -> [f | (f, (DTyp _ c _,_)) <- Map.toList funs, c==cat]) cats
+           let catfuns = Map.mapWithKey (\cat _ -> [f | (f, (DTyp _ c _,_,_)) <- Map.toList funs, c==cat]) cats
            return (Abstr{ aflags=aflags
                         , funs=funs, cats=cats
                         , catfuns=catfuns

src/PGF/Data.hs

@@ -24,7 +24,7 @@ data PGF = PGF {
 
 data Abstr = Abstr {
   aflags  :: Map.Map CId String,      -- value of a flag
-  funs    :: Map.Map CId (Type,[Equation]), -- type and def of a fun
+  funs    :: Map.Map CId (Type,Int,[Equation]), -- type, arrity and definition of function
   cats    :: Map.Map CId [Hypo],      -- context of a cat
   catfuns :: Map.Map CId [CId]        -- funs to a cat (redundant, for fast lookup)
   }

src/PGF/Expr.hs

@@ -11,9 +11,6 @@ module PGF.Expr(Tree(..), Literal(..),
 
                 -- helpers
                 pStr,pFactor,
-
-                -- refresh metavariables
-                newMetas
                ) where
 
 import PGF.CId
@@ -41,7 +38,7 @@ data Tree =
  | Var CId                          -- ^ variable
  | Fun CId [Tree]                   -- ^ function application
  | Lit Literal                      -- ^ literal
- | Meta Int                         -- ^ meta variable
+ | Meta {-# UNPACK #-} !Int         -- ^ meta variable
   deriving (Eq, Ord)
 
 -- | An expression represents a potentially unevaluated expression
@@ -52,7 +49,7 @@ data Expr =
    EAbs CId Expr                    -- ^ lambda abstraction
  | EApp Expr Expr                   -- ^ application
  | ELit Literal                     -- ^ literal
- | EMeta  Int                       -- ^ meta variable
+ | EMeta  {-# UNPACK #-} !Int       -- ^ meta variable
  | EVar   CId                       -- ^ variable or function reference
  | EPi CId Expr Expr                -- ^ dependent function type
   deriving (Eq,Ord)
@@ -219,7 +216,7 @@ expr2tree :: Funs -> Expr -> Tree
 expr2tree funs e = value2tree [] (eval funs Map.empty e)
   where
     value2tree xs (VApp f vs)               = case Map.lookup f funs of
-                                                Just (DTyp hyps _ _,_) -> -- eta conversion
+                                                Just (DTyp hyps _ _,_,_) -> -- eta conversion
                                                                           let a1  = length hyps    
                                                                               a2  = length vs
                                                                               a   = a1 - a2
@@ -228,11 +225,13 @@ expr2tree funs e = value2tree [] (eval funs Map.empty e)
                                                                           in ret (reverse xs'++xs)
                                                                                  (Fun f (map (value2tree []) vs++map Var xs'))
                                                 Nothing                -> error ("unknown variable "++prCId f)
-    value2tree xs (VGen i)                  = ret xs (Var (var i))
+    value2tree xs (VGen i vs)   | null vs   = ret xs (Var (var i))
-    value2tree xs (VMeta n)                 = ret xs (Meta n)
+                                | otherwise = error "variable of function type"
+    value2tree xs (VMeta n vs)  | null vs   = ret xs (Meta n)
+                                | otherwise = error "meta variable of function type"
     value2tree xs (VLit l)                  = ret xs (Lit l)
     value2tree xs (VClosure env (EAbs x e)) = let i = length xs
-                                              in value2tree (var i:xs) (eval funs (Map.insert x (VGen i) env) e)
+                                              in value2tree (var i:xs) (eval funs (Map.insert x (VGen i []) env) e)
 
     var i = mkCId ('v':show i)
 
@@ -242,73 +241,96 @@ expr2tree funs e = value2tree [] (eval funs Map.empty e)
 data Value
   = VApp CId [Value]
   | VLit Literal
-  | VMeta Int
+  | VMeta {-# UNPACK #-} !Int [Value]
-  | VGen Int
+  | VGen  {-# UNPACK #-} !Int [Value]
   | VClosure Env Expr
  deriving (Eq,Ord)
 
-type Funs = Map.Map CId (Type,[Equation]) -- type and def of a fun
+type Funs = Map.Map CId (Type,Int,[Equation]) -- type and def of a fun
 type Env  = Map.Map CId Value
 
 eval :: Funs -> Env -> Expr -> Value
 eval funs env (EVar x)     = case Map.lookup x env of
                                Just v  -> v
                                Nothing -> case Map.lookup x funs of
-                                            Just (_,eqs) -> case eqs of
+                                            Just (_,a,eqs) -> if a == 0
-                                                              Equ [] e : _ -> eval funs env e
+                                                                then case eqs of
-                                                              []           -> VApp x []                                                              
+                                                                       Equ [] e : _ -> eval funs env e
-                                            Nothing               -> error ("unknown variable "++prCId x)
+                                                                       _            -> VApp x []
+                                                                else VApp x []
+                                            Nothing        -> error ("unknown variable "++prCId x)
 eval funs env (EApp e1 e2) = apply funs env e1 [eval funs env e2]
 eval funs env (EAbs x e)   = VClosure env (EAbs x e)
-eval funs env (EMeta k)    = VMeta k
+eval funs env (EMeta k)    = VMeta k []
 eval funs env (ELit l)     = VLit l
 
 apply :: Funs -> Env -> Expr -> [Value] -> Value
 apply funs env e            []     = eval funs env e
 apply funs env (EVar x)     vs     = case Map.lookup x env of
                                        Just v  -> case (v,vs) of
+                                                    (VApp f  vs0            ,  vs) -> apply funs env (EVar f) (vs0++vs)
+                                                    (VLit _                 ,  vs) -> error "literal of function type"
+                                                    (VMeta i vs0            ,  vs) -> VMeta i (vs0++vs)
+                                                    (VGen  i vs0            ,  vs) -> VGen  i (vs0++vs)
                                                     (VClosure env (EAbs x e),v:vs) -> apply funs (Map.insert x v env) e vs
                                        Nothing -> case Map.lookup x funs of
-                                                    Just (_,eqs) -> case match eqs vs of
+                                                    Just (_,a,eqs) -> if a <= length vs
-                                                                      Just (e,vs,env) -> apply funs env e vs
+                                                                        then let (as,vs') = splitAt a vs
-                                                                      Nothing         -> VApp x vs
+                                                                             in case match eqs as of
-                                                    Nothing      -> error ("unknown variable "++prCId x)
+                                                                                  Match e env -> apply funs env e vs'
-apply funs env (EAbs x e)   (v:vs) = apply funs (Map.insert x v env) e vs
+                                                                                  Fail        -> VApp x vs
+                                                                                  Susp        -> VApp x vs
+                                                                        else VApp x vs
+                                                    Nothing        -> error ("unknown variable "++prCId x)
 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 (ELit l)     vs     = error "literal of function type"
 
-match :: [Equation] -> [Value] -> Maybe (Expr, [Value], Env)
+
-match eqs vs =
+-----------------------------------------------------
+-- Pattern matching
+-----------------------------------------------------
+
+data MatchRes
+  = Match Expr Env
+  | Susp
+  | Fail
+
+match :: [Equation] -> [Value] -> MatchRes
+match eqs as =
   case eqs of
-    []               -> Nothing
+    []               -> Fail
-    (Equ ps res):eqs -> let (as,vs') = splitAt (length ps) vs
+    (Equ ps res):eqs -> case tryMatches ps as res Map.empty of
-                        in case zipWithM tryMatch ps as of
+                          Fail -> match eqs as
-                             Just envs -> Just (res, vs', Map.unions envs)
+                          res  -> res
-                             Nothing   -> match eqs vs
   where
-    tryMatch p v = case (p, v) of
+    tryMatches []     []     res env = Match res env
-      (PVar x,    _         )           -> Just (Map.singleton x v)
+    tryMatches (p:ps) (a:as) res env = tryMatch p a env
-      (PApp f ps, VApp fe vs) | f == fe -> do envs <- zipWithM tryMatch ps vs
+      where
-                                              return (Map.unions envs)
+        tryMatch (PApp f1 ps1) (VApp f2 vs2) env | f1 == f2 = tryMatches (ps1++ps) (vs2++as) res env
-      (PLit l,    VLit le   ) | l == le -> Just Map.empty
+        tryMatch (PApp f1 ps1) (VMeta _ _  ) env            = Susp
-      _                                 -> Nothing
+        tryMatch (PApp f1 ps1) (VGen  _ _  ) env            = Susp
+        tryMatch (PLit l1    ) (VLit l2    ) env | l1 == l2 = tryMatches       ps        as  res env
+        tryMatch (PLit l1    ) (VMeta _ _  ) env            = Susp
+        tryMatch (PLit l1    ) (VGen  _ _  ) env            = Susp
+        tryMatch (PVar x     ) (v          ) env            = tryMatches       ps        as  res (Map.insert x v env)
+        tryMatch (PWild      ) (_          ) env            = tryMatches       ps        as  res env
+        tryMatch _             _             env            = Fail
+
+
+-----------------------------------------------------
+-- Equality checking
+-----------------------------------------------------
 
 eqValue :: Int -> Value -> Value -> [(Value,Value)]
 eqValue k v1 v2 =
   case (v1,v2) of
     (VApp f1 vs1, VApp f2 vs2) | f1 == f2  -> concat (zipWith (eqValue k) vs1 vs2)
     (VLit l1,     VLit l2    ) | l1 == l2  -> []
-    (VMeta i,     VMeta j    ) | i  == j   -> []
+    (VMeta i vs1, VMeta j vs2) | i  == j   -> concat (zipWith (eqValue k) vs1 vs2)
-    (VGen  i,     VGen  j    ) | i  == j   -> []
+    (VGen  i vs1, VGen  j vs2) | i  == j   -> concat (zipWith (eqValue k) vs1 vs2)
     (VClosure env1 (EAbs x1 e1), VClosure env2 (EAbs x2 e2)) ->
-      let v = VGen k
+      let v = VGen k []
       in eqValue (k+1) (VClosure (Map.insert x1 v env1) e1) (VClosure (Map.insert x2 v env2) e2)
     _                                      -> [(v1,v2)]
-
---- use composOp and state monad...
-newMetas :: Expr -> Expr
-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)

src/PGF/Macros.hs

@@ -35,17 +35,19 @@ lookPrintName pgf lang fun =
 
 lookType :: PGF -> CId -> Type
 lookType pgf f = 
-  fst $ lookMap (error $ "lookType " ++ show f) f (funs (abstract pgf))
+  case lookMap (error $ "lookType " ++ show f) f (funs (abstract pgf)) of
+    (ty,_,_) -> ty
 
 lookDef :: PGF -> CId -> [Equation]
 lookDef pgf f = 
-  snd $ lookMap (error $ "lookDef " ++ show f) f (funs (abstract pgf))
+  case lookMap (error $ "lookDef " ++ show f) f (funs (abstract pgf)) of
+    (_,a,eqs) -> eqs
 
 isData :: PGF -> CId -> Bool
 isData pgf f =
   case Map.lookup f (funs (abstract pgf)) of
-    Just (_,[]) -> True             -- the encoding of data constrs
+    Just (_,_,[]) -> True             -- the encoding of data constrs
-    _           -> False
+    _             -> False
 
 lookValCat :: PGF -> CId -> CId
 lookValCat pgf = valCat . lookType pgf
@@ -74,7 +76,7 @@ lookConcrFlag pgf lang f = Map.lookup f $ cflags $ lookConcr pgf lang
 
 functionsToCat :: PGF -> CId -> [(CId,Type)]
 functionsToCat pgf cat =
-  [(f,ty) | f <- fs, Just (ty,_) <- [Map.lookup f $ funs $ abstract pgf]]
+  [(f,ty) | f <- fs, Just (ty,_,_) <- [Map.lookup f $ funs $ abstract pgf]]
  where 
    fs = lookMap [] cat $ catfuns $ abstract pgf
 

src/PGF/Paraphrase.hs

@@ -50,7 +50,7 @@ fromDef pgf t@(Fun f ts) = defDown t ++ defUp t where
               isClosed d || (length equs == 1 && isLinear d)]
 
   equss = [(f,[(Fun f (map patt2tree ps), expr2tree (funs (abstract pgf)) d) | (Equ ps d) <- eqs]) | 
-                       (f,(_,eqs)) <- Map.assocs (funs (abstract pgf)), not (null eqs)]
+                       (f,(_,_,eqs)) <- Map.assocs (funs (abstract pgf)), not (null eqs)]
 
   trequ s f e = True ----trace (s ++ ": " ++ show f ++ "  " ++ show e) True
 

src/PGF/ShowLinearize.hs

@@ -99,7 +99,7 @@ markLinearize pgf lang t = concat $ take 1 $ linearizesMark pgf lang t
 collectWords :: PGF -> CId -> [(String, [(String,String)])]
 collectWords pgf lang = 
     concatMap collOne 
-      [(f,c,0) | (f,(DTyp [] c _,_)) <- Map.toList $ funs $ abstract pgf] 
+      [(f,c,0) | (f,(DTyp [] c _,_,_)) <- Map.toList $ funs $ abstract pgf] 
   where
     collOne (f,c,i) = 
       fromRec f [prCId c] (recLinearize pgf lang (Fun f (replicate i (Meta 888))))

src/PGF/TypeCheck.hs

@@ -61,7 +61,7 @@ infer pgf tenv@(k,rho,gamma) e = case e of
 
 checkExp :: PGF -> TCEnv -> Expr -> Value -> Err (Expr, [(Value,Value)])
 checkExp pgf tenv@(k,rho,gamma) e typ = do
-  let v = VGen k
+  let v = VGen k []
   case e of
     EMeta m -> return $ (e,[])
     EAbs x t -> case typ of
@@ -82,7 +82,7 @@ checkInferExp pgf tenv@(k,_,_) e typ = do
 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 . fst) $ 
+  _ -> maybe (Bad "var not found") (return . VClosure eempty . type2expr . (\(a,b,c) -> a)) $ 
          Map.lookup x (funs (abstract pgf))
 
 type2expr :: Type -> Expr
@@ -103,7 +103,7 @@ prValue = showExpr . value2expr
 
 value2expr v = case v of
   VApp f vs -> foldl EApp (EVar f) (map value2expr vs)
-  VMeta i -> EMeta i
+  VMeta i vs -> foldl EApp (EMeta i) (map value2expr vs)
   VClosure g e -> e ----
   VLit l -> ELit l
 
@@ -116,15 +116,15 @@ prConstraints cs = unwords
 splitConstraints :: [(Value,Value)] -> ([(Int,Expr)],[(Value,Value)])
 splitConstraints = mkSplit . partition isSubst . regroup . map reorder where
   reorder (v,w) = case w of
-    VMeta _ -> (w,v)
+    VMeta _ _ -> (w,v)
     _ -> (v,w)
 
   regroup = groupBy (\x y -> fst x == fst y) . sort
 
   isSubst cs@((v,u):_) = case v of
-    VMeta _ -> all ((==u) . snd) cs
+    VMeta _ _ -> all ((==u) . snd) cs
     _ -> False
-  mkSplit (ms,cs) = ([(i,value2expr v) | (VMeta i,v):_ <- ms], concat cs)
+  mkSplit (ms,cs) = ([(i,value2expr v) | (VMeta i _,v):_ <- ms], concat cs)
 
 metaSubst :: [(Int,Expr)] -> Expr -> Expr
 metaSubst vs exp = case exp of
@@ -136,3 +136,11 @@ metaSubst vs exp = case exp of
  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)

testsuite/update/ArrityCheck.gf

@@ -0,0 +1,5 @@
+abstract ArrityCheck = {
+  fun f : Int -> Int -> Int ;
+  def f 0 = \x -> x ;
+      f 1 1 = 0 ;
+}

testsuite/update/ArrityCheck.gfs

@@ -0,0 +1 @@
+i testsuite\update\ArrityCheck.gf

testsuite/update/ArrityCheck.gfs.gold

@@ -0,0 +1,8 @@
+
+
+
+
+C:\gf_2\testsuite\update\ArrityCheck.gf:6:1: cannot unify the informations
+
+    fun f : Int -> Int -> Int ;
+