in the middle of adapting CheckGrammar

5 files changed, 610 insertions, 134 deletions

diff --git a/src/GF/Devel/Compile/CheckGrammar.hs b/src/GF/Devel/Compile/CheckGrammar.hs
index 50367b85d..1c957ca71 100644
--- a/src/GF/Devel/Compile/CheckGrammar.hs
+++ b/src/GF/Devel/Compile/CheckGrammar.hs
@@ -34,7 +34,7 @@ import GF.Devel.Grammar.Judgements
 import GF.Devel.Grammar.Terms
 import GF.Devel.Grammar.MkJudgements
 import GF.Devel.Grammar.Macros
-import GF.Devel.Grammar.PrGrammar
+import GF.Devel.Grammar.PrGF
 import GF.Devel.Grammar.Lookup
 
 import GF.Infra.Ident
@@ -47,8 +47,8 @@ import GF.Infra.Ident
 
 --import GF.Grammar.LookAbs
 --import GF.Grammar.ReservedWords ----
---import GF.Grammar.PatternMatch
---import GF.Grammar.AppPredefined
+import GF.Grammar.PatternMatch (testOvershadow)
+import GF.Grammar.AppPredefined
 --import GF.Grammar.Lockfield (isLockLabel)
 
 import GF.Data.Operations
@@ -68,14 +68,14 @@ showCheckModule mos m = do
 
 checkModule :: GF -> SourceModule -> Check SourceModule
 checkModule gf0 (name,mo) = checkIn ("checking module" +++ prt name) $ do
-  let gf = gf0 {gfmodules = Map.insert name mo (gfmodules gf0)}
-  checkRestrictedInheritance gf (name, mo)
+  let gr = gf0 {gfmodules = Map.insert name mo (gfmodules gf0)}
+----  checkRestrictedInheritance gr (name, mo)
   mo1 <- case mtype mo of
     MTAbstract -> judgementOpModule (checkAbsInfo gr name) mo
-    MTResource -> judgementOpModule (checkResInfo gr name) mo
+    MTGrammar -> judgementOpModule (checkResInfo gr name) mo
 
     MTConcrete aname -> do
-      checkErr $ topoSortOpers $ allOperDependencies name js
+      checkErr $ topoSortOpers $ allOperDependencies name $ mjments mo
       abs <- checkErr $ lookupModule gr aname
       js1 <- checkCompleteGrammar abs mo
       judgementOpModule (checkCncInfo gr name (aname,abs)) js1
@@ -119,13 +119,13 @@ checkRestrictedInheritance mos (name,mo) = do
 
 
 -- | check if a term is typable
-justCheckLTerm :: SourceGrammar -> Term -> Err Term
+justCheckLTerm :: GF -> Term -> Err Term
 justCheckLTerm src t = do
   ((t',_),_) <- checkStart (inferLType src t)
   return t'
 
-checkAbsInfo :: GF -> Ident -> (Ident,JEntry) -> Check (Ident,JEntry)
-checkAbsInfo st m (c,info) = return (c,info) ----
+checkAbsInfo :: GF -> Ident -> Ident -> Judgement -> Check Judgement
+checkAbsInfo st m c info = return info ----
 
 {-
 checkAbsInfo st m (c,info) = do
@@ -178,70 +178,62 @@ checkAbsInfo st m (c,info) = do
      _ -> mkApp t [a]
 -}
 
-checkCompleteGrammar :: SourceAbs -> SourceCnc -> Check (BinTree Ident Info)
+
+checkCompleteGrammar :: Module -> Module -> Check Module
 checkCompleteGrammar abs cnc = do
-  let js = jments cnc
-  let fs = tree2list $ jments abs
-  foldM checkOne js fs
+  let js = mjments cnc
+  let fs = Map.assocs $ mjments abs
+  js' <- foldM checkOne js fs
+  return $ cnc {mjments = js'}
  where
-   checkOne js i@(c,info) = case info of
-     AbsFun (Yes _) _ -> case lookupIdent c js of
-       Ok _ -> return js
+   checkOne js i@(c, Left ju) = case jform ju of
+     JFun -> case Map.lookup c js of
+       Just (Left j) | jform ju == JLin -> return js
        _ -> do
          checkWarn $ "WARNING: no linearization of" +++ prt c
          return js
-     AbsCat (Yes _) _ -> case lookupIdent c js of
-       Ok (AnyInd _ _) -> return js
-       Ok (CncCat (Yes _) _ _) -> return js
-       Ok (CncCat _ mt mp) -> do
-         checkWarn $ 
-           "Warning: no linearization type for" +++ prt c ++ 
-           ", inserting default {s : Str}" 
-         return $ updateTree (c,CncCat (Yes defLinType) mt mp) js
-       _ -> do
+     JCat -> case Map.lookup c js of
+       Just (Left j) | jform ju == JLincat -> return js  
+       _ -> do        ---- TODO: other things to check here
          checkWarn $ 
            "Warning: no linearization type for" +++ prt c ++ 
            ", inserting default {s : Str}" 
-         return $ updateTree (c,CncCat (Yes defLinType) nope nope) js
+         return $ Map.insert c (cncCat defLinType) js
      _ -> return js
 
--- | General Principle: only Yes-values are checked. 
--- A May-value has always been checked in its origin module.
-checkResInfo :: SourceGrammar -> Ident -> (Ident,Info) -> Check (Ident,Info)
-checkResInfo gr mo (c,info) = do
-  checkReservedId c
-  case info of
-    ResOper pty pde -> chIn "operation" $ do
-      (pty', pde') <- case (pty,pde) of
-         (Yes ty, Yes de) -> do
-           ty'     <- check ty typeType >>= comp . fst
-           (de',_) <- check de ty'
-           return (Yes ty', Yes de')
-         (_, Yes de) -> do
-           (de',ty') <- infer de
-           return (Yes ty', Yes de')
-         (_,Nope) -> do
-           checkWarn "No definition given to oper"
-           return (pty,pde)
-         _ -> return (pty, pde) --- other cases are uninteresting
-      return (c, ResOper pty' pde')
-
+checkResInfo :: GF -> Ident -> Ident -> Judgement -> Check Judgement
+checkResInfo gr mo c info = do
+  ----  checkReservedId c
+  case jform info of
+    JOper -> chIn "operation" $ case (jtype info, jdef info) of
+      (_,Meta _) -> do
+        checkWarn "No definition given to oper"
+        return info
+      (Meta,de) -> do
+        (de',ty') <- infer de
+        return (resOper ty' de')
+      (ty, de) -> do
+        ty'     <- check ty typeType >>= comp . fst
+        (de',_) <- check de ty'
+        return (resOper ty' de')
+{- ----
     ResOverload tysts -> chIn "overloading" $ do
       tysts' <- mapM (uncurry $ flip check) tysts
       let tysts2 = [(y,x) | (x,y) <- tysts']
       --- this can only be a partial guarantee, since matching
       --- with value type is only possible if expected type is given
       checkUniq $ 
-        sort [t : map snd xs | (x,_) <- tysts2, Ok (xs,t) <- [typeFormCnc x]]
+        sort [t : map snd xs | (x,_) <- tysts2, let (xs,t) = prodForm x]
       return (c,ResOverload tysts2)
-
+-}
+{- ----
     ResParam (Yes (pcs,_)) -> chIn "parameter type" $ do
 ----      mapM ((mapM (computeLType gr . snd)) . snd) pcs
       mapM_ ((mapM_ (checkIfParType gr . snd)) . snd) pcs
       ts <- checkErr $ lookupParamValues gr mo c
       return (c,ResParam (Yes (pcs, Just ts)))
-
-    _ ->  return (c,info)
+-}
+    _ ->  return info
  where
    infer = inferLType gr
    check = checkLType gr
@@ -256,34 +248,37 @@ checkResInfo gr mo (c,info) = do
      _ -> return ()
 
 
-checkCncInfo :: SourceGrammar -> Ident -> (Ident,SourceAbs) -> 
-                (Ident,Info) -> Check (Ident,Info)
-checkCncInfo gr m (a,abs) (c,info) = do
-  checkReservedId c
-  case info of
-
-    CncFun _ (Yes trm) mpr -> chIn "linearization of" $ do
-      typ        <- checkErr $ lookupFunTypeSrc gr a c
+checkCncInfo :: GF -> Ident -> SourceModule -> 
+                Ident -> Judgement -> Check Judgement
+checkCncInfo gr cnc (a,abs) c info = do
+  ----  checkReservedId c
+  case jform info of
+    JFun -> chIn "linearization of" $ do
+      typ        <- checkErr $ lookupFunType gr a c
       cat0       <- checkErr $ valCat typ
-      (cont,val) <- linTypeOfType gr m typ         -- creates arg vars
-      (trm',_)   <- check trm (mkFunType (map snd cont) val)  -- erases arg vars
-      checkPrintname gr mpr
+      (cont,val) <- linTypeOfType gr cnc typ     -- creates arg vars
+      let lintyp = mkFunType (map snd cont) val
+      (trm',_)   <- check (jdef info) lintyp     -- erases arg vars
+      checkPrintname gr (jprintname info)
       cat        <- return $ snd cat0
-      return (c, CncFun (Just (cat,(cont,val))) (Yes trm') mpr)
+      return (info {jdef = trm'})
+      ---- return (c, CncFun (Just (cat,(cont,val))) (Yes trm') mpr)
                                                    -- cat for cf, typ for pe
 
-    CncCat (Yes typ) mdef mpr -> chIn "linearization type of" $ do
-      checkErr $ lookupCatContextSrc gr a c
-      typ'  <- checkIfLinType gr typ
+    JCat (Yes typ) mdef mpr -> chIn "linearization type of" $ do
+      checkErr $ lookupCatContext gr a c
+      typ'  <- checkIfLinType gr (jtype info)
+    {- ----
       mdef' <- case mdef of
         Yes def -> do
           (def',_) <- checkLType gr def (mkFunType [typeStr] typ)
           return $ Yes def'
         _ -> return mdef
-      checkPrintname gr mpr
-      return (c,CncCat (Yes typ') mdef' mpr)
+    -}
+      checkPrintname gr (jprintname info)
+      return (info {jtype = typ'})
 
-    _ -> checkResInfo gr m (c,info)
+    _ -> checkResInfo gr cnc c info
 
  where
    env = gr
@@ -292,7 +287,8 @@ checkCncInfo gr m (a,abs) (c,info) = do
    check = checkLType gr
    chIn cat = checkIn ("Happened in" +++ cat +++ prt c +++ ":")
 
-checkIfParType :: SourceGrammar -> Type -> Check ()
+
+checkIfParType :: GF -> Type -> Check ()
 checkIfParType st typ = checkCond ("Not parameter type" +++ prt typ) (isParType typ)
   where
    isParType ty = True ----
@@ -308,6 +304,7 @@ checkIfParType st typ = checkCond ("Not parameter type" +++ prt typ) (isParType
      _ -> False
 -}
 
+{- ----
 checkIfStrType :: SourceGrammar -> Type -> Check ()
 checkIfStrType st typ = case typ of
   Table arg val -> do
@@ -315,26 +312,17 @@ checkIfStrType st typ = case typ of
     checkIfStrType st val
   _ | typ == typeStr -> return ()
   _ -> prtFail "not a string type" typ
+-}
 
-
-checkIfLinType :: SourceGrammar -> Type -> Check Type
+checkIfLinType :: GF -> Type -> Check Type
 checkIfLinType st typ0 = do
   typ <- computeLType st typ0
   case typ of
-    RecType r -> do
-      let (lins,ihs) = partition (isLinLabel .fst) r
-      --- checkErr $ checkUnique $ map fst r
-      mapM_ checkInh ihs
-      mapM_ checkLin lins
+    RecType r -> return ()
     _ -> prtFail "a linearization type must be a record type instead of" typ
   return typ
 
- where
-   checkInh (label,typ) = checkIfParType st typ
-   checkLin (label,typ) = return () ---- checkIfStrType st typ
-
-
-computeLType :: SourceGrammar -> Type -> Check Type
+computeLType :: GF -> Type -> Check Type
 computeLType gr t = do
   g0 <- checkGetContext
   let g = [(x, Vr x) | (x,_) <- g0]
@@ -348,15 +336,15 @@ computeLType gr t = do
     Q (IC "Predef") (IC "Error")        -> return ty ---- shouldn't be needed
 
     Q m c | elem c [cPredef,cPredefAbs] -> return ty
-    Q m c | elem c [zIdent "Int"] -> 
+    Q m c | elem c [identC "Int"] -> 
       return $ defLinType
 ----      let ints k = App (Q (IC "Predef") (IC "Ints")) (EInt k) in
 ----      RecType [
 ----        (LIdent "last",ints 9),(LIdent "s", typeStr), (LIdent "size",ints 1)]
-    Q m c | elem c [zIdent "Float",zIdent "String"] -> return defLinType ----
+    Q m c | elem c [identC "Float",identC "String"] -> return defLinType ----
 
     Q m ident -> checkIn ("module" +++ prt m) $ do
-      ty' <- checkErr (lookupResDef gr m ident) 
+      ty' <- checkErr (lookupOperDef gr m ident) 
       if ty' == ty then return ty else comp ty' --- is this necessary to test?
 
     Vr ident  -> checkLookup ident -- never needed to compute!
@@ -388,41 +376,43 @@ computeLType gr t = do
       let fs' = sortBy (\x y -> compare (fst x) (fst y)) fs
       liftM RecType $ mapPairsM comp fs'
 
-    _ | ty == typeTok -> return typeStr
-    _ | isPredefConstant ty -> return ty
+----    _ | ty == typeStr -> return typeStr
+----    _ | isPredefConstant ty -> return ty
 
     _ -> composOp comp ty
 
-checkPrintname :: SourceGrammar -> Perh Term -> Check ()
-checkPrintname st (Yes t) = checkLType st t typeStr >> return ()
+checkPrintname :: GF -> Term -> Check ()
+---- checkPrintname st (Yes t) = checkLType st t typeStr >> return ()
 checkPrintname _ _ = return ()
 
+{- ----
 -- | for grammars obtained otherwise than by parsing ---- update!!
 checkReservedId :: Ident -> Check ()
 checkReservedId x = let c = prt x in
          if isResWord c 
             then checkWarn ("Warning: reserved word used as identifier:" +++ c)
             else return ()
+-}
 
 -- to normalize records and record types
 labelIndex :: Type -> Label -> Int
 labelIndex ty lab = case ty of
-  RecType ts -> maybe (error ("label index" +++ prt lab)) id $ lookup lab $ labs ts
+  RecType ts -> maybe (error ("label index"+++ prt lab)) id $ lookup lab $ labs ts
   _ -> error $ "label index" +++ prt ty
  where 
   labs ts = zip (map fst (sortBy (\ x y -> compare (fst x) (fst y)) ts)) [0..]
 
 -- the underlying algorithms
 
-inferLType :: SourceGrammar -> Term -> Check (Term, Type)
+inferLType :: GF -> Term -> Check (Term, Type)
 inferLType gr trm = case trm of
 
    Q m ident | isPredef m -> termWith trm $ checkErr (typPredefined ident)
 
    Q m ident -> checks [
-     termWith trm $ checkErr (lookupResType gr m ident) >>= comp
+     termWith trm $ checkErr (lookupOperType gr m ident) >>= comp
      ,
-     checkErr (lookupResDef gr m ident) >>= infer
+     checkErr (lookupOperDef gr m ident) >>= infer
      ,
 {-
      do
@@ -438,9 +428,9 @@ inferLType gr trm = case trm of
    QC m ident | isPredef m -> termWith trm $ checkErr (typPredefined ident)
 
    QC m ident -> checks [
-       termWith trm $ checkErr (lookupResType gr m ident) >>= comp
+       termWith trm $ checkErr (lookupOperType gr m ident) >>= comp
        ,
-       checkErr (lookupResDef gr m ident) >>= infer
+       checkErr (lookupOperDef gr m ident) >>= infer
        ,
        prtFail "cannot infer type of canonical constant" trm
        ]
@@ -532,23 +522,20 @@ inferLType gr trm = case trm of
      check2 (flip justCheck typeStr) C s1 s2 typeStr
 
    Glue s1 s2 -> 
-     check2 (flip justCheck typeStr) Glue s1 s2 typeStr ---- typeTok
+     check2 (flip justCheck typeStr) Glue s1 s2 typeStr
 
 ---- hack from Rename.identRenameTerm, to live with files with naming conflicts 18/6/2007
-   Strs (Cn (IC "#conflict") : ts) -> do
-     trace ("WARNING: unresolved constant, could be any of" +++ unwords (map prt ts)) (infer $ head ts)
+----   Strs (Cn (IC "#conflict") : ts) -> do
+----     trace ("WARNING: unresolved constant, could be any of" +++ unwords (map prt ts)) (infer $ head ts)
 --     checkWarn ("WARNING: unresolved constant, could be any of" +++ unwords (map prt ts))
 --     infer $ head ts
 
-   Strs ts -> do
-     ts' <- mapM (\t -> justCheck t typeStr) ts 
-     return (Strs ts', typeStrs)
 
    Alts (t,aa) -> do
      t'  <- justCheck t typeStr
      aa' <- flip mapM aa (\ (c,v) -> do
         c' <- justCheck c typeStr 
-        v' <- justCheck v typeStrs
+        v' <- justCheck v typeStr
         return (c',v'))
      return (Alts (t',aa'), typeStr)
 
@@ -633,7 +620,7 @@ inferLType gr trm = case trm of
      _ -> False
 
    inferPatt p = case p of
-     PP q c ps | q /= cPredef -> checkErr $ lookupResType gr q c >>= valTypeCnc
+     PP q c ps | q /= cPredef -> checkErr $ lookupOperType gr q c >>= snd . prodForm
      PAs _ p  -> inferPatt p
      PNeg p   -> inferPatt p
      PAlt p q -> checks [inferPatt p, inferPatt q]
@@ -644,9 +631,9 @@ inferLType gr trm = case trm of
 
 -- type inference: Nothing, type checking: Just t
 -- the latter permits matching with value type
-getOverload :: SourceGrammar -> Maybe Type -> Term -> Check (Maybe (Term,Type))
+getOverload :: GF -> Maybe Type -> Term -> Check (Maybe (Term,Type))
 getOverload env@gr mt t = case appForm t of
-     (f@(Q m c), ts) -> case lookupOverload gr m c of
+     (f@(Q m c), ts) -> case (return []) of ---- lookupOverload gr m c of
        Ok typs -> do
          ttys <- mapM infer ts
          v <- matchOverload f typs ttys
@@ -682,7 +669,7 @@ getOverload env@gr mt t = case appForm t of
 
    matchVal mt v = elem mt ([Nothing,Just v] ++ unlocked) where
      unlocked = case v of
-       RecType fs -> [Just $ RecType $ filter (not . isLockLabel . fst) fs]
+       RecType fs -> [Just $ RecType $ fs] ---- filter (not . isLockLabel . fst) fs]
        _ -> []
    ---- TODO: accept subtypes
    ---- TODO: use a trie
@@ -698,7 +685,7 @@ getOverload env@gr mt t = case appForm t of
      Prod _ _ _ -> False
      _ -> True
 
-checkLType :: SourceGrammar -> Term -> Type -> Check (Term, Type)
+checkLType :: GF -> Term -> Type -> Check (Term, Type)
 checkLType env trm typ0 = do
 
   typ <- comp typ0
@@ -862,8 +849,8 @@ pattContext :: LTEnv -> Type -> Patt -> Check Context
 pattContext env typ p = case p of
   PV x | not (isWildIdent x) -> return [(x,typ)]
   PP q c ps | q /= cPredef -> do ---- why this /=? AR 6/1/2006
-    t <- checkErr $ lookupResType cnc q c
-    (cont,v) <- checkErr $ typeFormCnc t
+    t <- checkErr $ lookupOperType cnc q c
+    let (cont,v) = prodForm t
     checkCond ("wrong number of arguments for constructor in" +++ prt p) 
               (length cont == length ps)
     checkEqLType env typ v (patt2term p)
@@ -912,7 +899,7 @@ pattContext env typ p = case p of
 
 -- auxiliaries
 
-type LTEnv = SourceGrammar
+type LTEnv = GF
 
 termWith :: Term -> Check Type -> Check (Term, Type)
 termWith t ct = do
@@ -1007,7 +994,7 @@ checkIfEqLType env t u trm = do
        let 
          ls = [l | (l,a) <- rs, 
                    not (any (\ (k,b) -> alpha g a b && l == k) ts)]
-         (locks,others) = partition isLockLabel ls
+         (locks,others) = partition (const False) ls ---- isLockLabel ls
        in case others of
          _:_ -> Bad $ "missing record fields" +++ unwords (map prt others)
          _ -> return locks
@@ -1019,15 +1006,19 @@ checkIfEqLType env t u trm = do
 
      _ -> Bad ""
 
-   sTypes = [typeStr, typeTok, typeString]
+   ---- to revise
+   allExtendsPlus _ n = [n]
+
+   sTypes = [typeStr, typeString]
    comp = computeLType env
 
 -- printing a type with a lock field lock_C as C
 prtType :: LTEnv -> Type -> String
 prtType env ty = case ty of
-  RecType fs -> case filter isLockLabel $ map fst fs of
-    [lock] -> (drop 5 $ prt lock) --- ++++ "Full form" +++ prt ty
-    _ -> prtt ty
+  RecType fs -> ---- case filter isLockLabel $ map fst fs of
+   ---- [lock] -> (drop 5 $ prt lock) --- ++++ "Full form" +++ prt ty
+   ---- _ -> 
+   prtt ty
   Prod x a b -> prtType env a +++ "->" +++ prtType env b
   _ -> prtt ty
  where
@@ -1036,7 +1027,7 @@ prtType env ty = case ty of
 
 
 -- | linearization types and defaults
-linTypeOfType :: SourceGrammar -> Ident -> Type -> Check (Context,Type)
+linTypeOfType :: GF -> Ident -> Type -> Check (Context,Type)
 linTypeOfType cnc m typ = do
   (cont,cat) <- checkErr $ typeSkeleton typ
   val  <- lookLin cat
@@ -1057,10 +1048,10 @@ linTypeOfType cnc m typ = do
 
 -- | dependency check, detecting circularities and returning topo-sorted list
 
-allOperDependencies :: Ident -> BinTree Ident Info -> [(Ident,[Ident])]
+allOperDependencies :: Ident -> Map.Map Ident JEntry -> [(Ident,[Ident])]
 allOperDependencies m = allDependencies (==m)
 
-allDependencies :: (Ident -> Bool) -> BinTree Ident Info -> [(Ident,[Ident])]
+allDependencies :: (Ident -> Bool) -> Map.Map Ident JEntry -> [(Ident,[Ident])]
 allDependencies ism b = 
   [(f, nub (concatMap opty (pts i))) | (f,i) <- tree2list b]
   where
@@ -1070,15 +1061,9 @@ allDependencies ism b =
       _ -> collectOp opersIn t
     opty (Yes ty) = opersIn ty
     opty _ = []
-    pts i = case i of
-      ResOper pty pt -> [pty,pt]
-      ResParam (Yes (ps,_)) -> [Yes 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
-      AbsCat (Yes co) _ -> [Yes ty | (_,ty) <- co]
-      _              -> []
-
+    pts i = [jtype i, jdef i]
+    ----  AbsFun pty ptr -> [pty] --- ptr is def, which can be mutual
+ 
 topoSortOpers :: [(Ident,[Ident])] -> Err [Ident]
 topoSortOpers st = do
   let eops = topoTest st
diff --git a/src/GF/Devel/Grammar/AppPredefined.hs b/src/GF/Devel/Grammar/AppPredefined.hs
new file mode 100644
index 000000000..6ff538148
--- /dev/null
+++ b/src/GF/Devel/Grammar/AppPredefined.hs
@@ -0,0 +1,163 @@
+----------------------------------------------------------------------
+-- |
+-- Module      : AppPredefined
+-- Maintainer  : AR
+-- Stability   : (stable)
+-- Portability : (portable)
+--
+-- > CVS $Date: 2005/10/06 14:21:34 $ 
+-- > CVS $Author: aarne $
+-- > CVS $Revision: 1.13 $
+--
+-- Predefined function type signatures and definitions.
+-----------------------------------------------------------------------------
+
+module GF.Devel.Grammar.AppPredefined (
+  isInPredefined, 
+  typPredefined, 
+  appPredefined
+  ) where
+
+import GF.Devel.Grammar.Terms
+import GF.Devel.Grammar.Macros
+import GF.Grammar.PrGF (prt,prt_,prtBad)
+import GF.Infra.Ident
+
+import GF.Data.Operations
+
+
+-- predefined function type signatures and definitions. AR 12/3/2003.
+
+isInPredefined :: Ident -> Bool
+isInPredefined = err (const True) (const False) . typPredefined
+
+typPredefined :: Ident -> Err Type
+typPredefined c@(IC f) = case f of
+  "Int"    -> return typePType
+  "Float"  -> return typePType
+  "Error"  -> return typeType
+  "Ints"   -> return $ mkFunType [cnPredef "Int"] typePType
+  "PBool"  -> return typePType
+  "error"  -> return $ mkFunType [typeStr] (cnPredef "Error")  -- non-can. of empty set
+  "PFalse" -> return $ cnPredef "PBool"
+  "PTrue"  -> return $ cnPredef "PBool"
+  "dp"     -> return $ mkFunType [cnPredef "Int",typeTok] typeTok
+  "drop"   -> return $ mkFunType [cnPredef "Int",typeTok] typeTok
+  "eqInt"  -> return $ mkFunType [cnPredef "Int",cnPredef "Int"] (cnPredef "PBool")
+  "lessInt"-> return $ mkFunType [cnPredef "Int",cnPredef "Int"] (cnPredef "PBool")
+  "eqStr"  -> return $ mkFunType [typeTok,typeTok] (cnPredef "PBool")
+  "length" -> return $ mkFunType [typeTok] (cnPredef "Int")
+  "occur"  -> return $ mkFunType [typeTok,typeTok] (cnPredef "PBool")
+  "occurs" -> return $ mkFunType [typeTok,typeTok] (cnPredef "PBool")
+  "plus"   -> return $ mkFunType [cnPredef "Int",cnPredef "Int"] (cnPredef "Int")
+----  "read"   -> (P : Type) -> Tok -> P
+  "show"   -> return $ mkProd -- (P : PType) -> P -> Tok
+    ([(zIdent "P",typePType),(wildIdent,Vr (zIdent "P"))],typeStr,[]) 
+  "toStr"  -> return $ mkProd -- (L : Type)  -> L -> Str
+    ([(zIdent "L",typeType),(wildIdent,Vr (zIdent "L"))],typeStr,[]) 
+  "mapStr" -> 
+    let ty = zIdent "L" in
+    return $ mkProd -- (L : Type)  -> (Str -> Str) -> L -> L
+    ([(ty,typeType),(wildIdent,mkFunType [typeStr] typeStr),(wildIdent,Vr ty)],Vr ty,[]) 
+  "take"   -> return $ mkFunType [cnPredef "Int",typeTok] typeTok
+  "tk"     -> return $ mkFunType [cnPredef "Int",typeTok] typeTok
+  _        -> prtBad "unknown in Predef:" c
+typPredefined c = prtBad "unknown in Predef:" c
+
+appPredefined :: Term -> Err (Term,Bool)
+appPredefined t = case t of
+
+  App f x0 -> do
+   (x,_) <- appPredefined x0
+   case f of
+    -- one-place functions
+    Q (IC "Predef") (IC f) -> case (f, x) of
+      ("length", K s) -> retb $ EInt $ toInteger $ length s
+      _ -> retb t ---- prtBad "cannot compute predefined" t
+
+    -- two-place functions
+    App (Q (IC "Predef") (IC f)) z0 -> do
+     (z,_) <- appPredefined z0
+     case (f, norm z, norm x) of
+      ("drop", EInt i, K s) -> retb $ K (drop (fi i) s)
+      ("take", EInt i, K s) -> retb $ K (take (fi i) s)
+      ("tk",   EInt i, K s) -> retb $ K (take (max 0 (length s - fi i)) s)
+      ("dp",   EInt i, K s) -> retb $ K (drop (max 0 (length s - fi i)) s)
+      ("eqStr",K s,    K t) -> retb $ if s == t then predefTrue else predefFalse
+      ("occur",K s,    K t) -> retb $ if substring s t then predefTrue else predefFalse
+      ("occurs",K s,   K t) -> retb $ if any (flip elem t) s then predefTrue else predefFalse
+      ("eqInt",EInt i, EInt j) -> retb $ if i==j then predefTrue else predefFalse
+      ("lessInt",EInt i, EInt j) -> retb $ if i<j then predefTrue else predefFalse
+      ("plus", EInt i, EInt j) -> retb $ EInt $ i+j
+      ("show", _, t) -> retb $ foldr C Empty $ map K $ words $ prt t
+      ("read", _, K s) -> retb $ str2tag s --- because of K, only works for atomic tags
+      ("toStr", _, t) -> trm2str t >>= retb
+
+      _ -> retb t ---- prtBad "cannot compute predefined" t
+
+    -- three-place functions
+    App (App (Q (IC "Predef") (IC f)) z0) y0 -> do
+     (y,_) <- appPredefined y0
+     (z,_) <- appPredefined z0
+     case (f, z, y, x) of
+      ("mapStr",ty,op,t) -> retf $ mapStr ty op t
+      _ -> retb t ---- prtBad "cannot compute predefined" t
+
+    _ -> retb t ---- prtBad "cannot compute predefined" t
+  _ -> retb t
+                  ---- should really check the absence of arg variables
+ where
+   retb t = return (t,True)  -- no further computing needed
+   retf t = return (t,False) -- must be computed further
+   norm t = case t of
+     Empty -> K []
+     _ -> t
+   fi = fromInteger
+
+-- read makes variables into constants
+
+str2tag :: String -> Term
+str2tag s = case s of
+----  '\'' : cs -> mkCn $ pTrm $ init cs
+  _ -> Cn $ IC s ---
+ where
+   mkCn t = case t of
+     Vr i -> Cn i
+     App c a -> App (mkCn c) (mkCn a)
+     _ -> t
+
+
+predefTrue = Q (IC "Predef") (IC "PTrue")
+predefFalse = Q (IC "Predef") (IC "PFalse")
+
+substring :: String -> String -> Bool
+substring s t = case (s,t) of
+  (c:cs, d:ds) -> (c == d && substring cs ds) || substring s ds
+  ([],_) -> True
+  _ -> False
+
+trm2str :: Term -> Err Term
+trm2str t = case t of
+  R ((_,(_,s)):_) -> trm2str s
+  T _ ((_,s):_)   -> trm2str s
+  TSh _ ((_,s):_) -> trm2str s
+  V _ (s:_)       -> trm2str s
+  C _ _         -> return $ t
+  K _           -> return $ t
+  S c _         -> trm2str c
+  Empty         -> return $ t
+  _ -> prtBad "cannot get Str from term" t
+
+-- simultaneous recursion on type and term: type arg is essential!
+-- But simplify the task by assuming records are type-annotated
+-- (this has been done in type checking)
+mapStr :: Type -> Term -> Term -> Term
+mapStr ty f t = case (ty,t) of
+  _ | elem ty [typeStr,typeTok] -> App f t
+  (_,        R ts)    -> R [(l,mapField v)   | (l,v) <- ts]
+  (Table a b,T ti cs) -> T ti [(p,mapStr b f v) | (p,v) <- cs]
+  _    -> t 
+ where
+   mapField (mty,te) = case mty of
+     Just ty -> (mty,mapStr ty f te)
+     _ -> (mty,te)
diff --git a/src/GF/Devel/Grammar/Lookup.hs b/src/GF/Devel/Grammar/Lookup.hs
index cb45b5406..3980577df 100644
--- a/src/GF/Devel/Grammar/Lookup.hs
+++ b/src/GF/Devel/Grammar/Lookup.hs
@@ -4,11 +4,13 @@ import GF.Devel.Grammar.Modules
 import GF.Devel.Grammar.Judgements
 import GF.Devel.Grammar.Macros
 import GF.Devel.Grammar.Terms
+import GF.Devel.Grammar.PrGF
 import GF.Infra.Ident
 
 import GF.Data.Operations
 
 import Data.Map
+import Data.List (sortBy) ----
 
 -- look up fields for a constant in a grammar
 
@@ -57,6 +59,22 @@ lookupParamValues gf m c = do
     V _ ts -> return ts
     _ -> raise "no parameter values"
 
+allParamValues :: GF -> Type -> Err [Term]
+allParamValues cnc ptyp = case ptyp of
+     App (Q (IC "Predef") (IC "Ints")) (EInt n) -> 
+       return [EInt i | i <- [0..n]]
+     QC p c -> lookupParamValues cnc p c
+     Q  p c -> lookupParamValues cnc p c ----
+     RecType r -> do
+       let (ls,tys) = unzip $ sortByFst r
+       tss <- mapM allPV tys
+       return [R (zipAssign ls ts) | ts <- combinations tss]
+     _ -> prtBad "cannot find parameter values for" ptyp
+  where
+    allPV = allParamValues cnc
+    -- to normalize records and record types
+    sortByFst = sortBy (\ x y -> compare (fst x) (fst y))
+
 -- infrastructure for lookup
     
 lookupModule :: GF -> Ident -> Err Module
diff --git a/src/GF/Devel/Grammar/Macros.hs b/src/GF/Devel/Grammar/Macros.hs
index 1b4ed1448..659ddb107 100644
--- a/src/GF/Devel/Grammar/Macros.hs
+++ b/src/GF/Devel/Grammar/Macros.hs
@@ -7,9 +7,12 @@ import GF.Infra.Ident
 
 import GF.Data.Operations
 
-import Data.Map
+import qualified Data.Map as Map
 import Control.Monad (liftM,liftM2)
 
+
+-- analyse types and terms
+
 contextOfType :: Type -> Context
 contextOfType ty = co where (co,_,_) = typeForm ty
 
@@ -30,9 +33,48 @@ appForm tr = (f,reverse xs) where
     App f a -> (f2,a:a2) where (f2,a2) = appForm f
     _ -> (t,[])
 
+valCat :: Type -> Err (Ident,Ident)
+valCat typ = case typeForm typ of
+  (_,Q m c,_) -> return (m,c)
+
+typeRawSkeleton :: Type -> Err ([(Int,Type)],Type)
+typeRawSkeleton typ = do
+  let (cont,typ) = prodForm typ
+  args <- mapM (typeRawSkeleton . snd) cont
+  return ([(length c, v) | (c,v) <- args], typ)
+
+type MCat = (Ident,Ident)
+
+sortMCat :: String -> MCat
+sortMCat s = (identC "_", identC s)
+
+--- hack for Editing.actCat in empty state
+errorCat :: MCat
+errorCat = (identC "?", identC "?")
+
+getMCat :: Term -> Err MCat
+getMCat t = case t of
+  Q  m c -> return (m,c)
+  QC m c -> return (m,c)
+  Sort s -> return $ sortMCat s
+  App f _ -> getMCat f
+  _ -> error $ "no qualified constant" +++ show t
+
+typeSkeleton :: Type -> Err ([(Int,MCat)],MCat)
+typeSkeleton typ = do
+  (cont,val) <- typeRawSkeleton typ
+  cont' <- mapPairsM getMCat cont
+  val'  <- getMCat val
+  return (cont',val')
+
+-- construct types and terms
+
 mkProd :: Context -> Type -> Type
 mkProd = flip (foldr (uncurry Prod))
 
+mkFunType :: [Type] -> Type -> Type
+mkFunType tt t = mkProd ([(wildIdent, ty) | ty <- tt]) t -- nondep prod
+
 mkApp :: Term -> [Term] -> Term
 mkApp = foldl App
 
@@ -43,6 +85,12 @@ mkCTable :: [Ident] -> Term -> Term
 mkCTable ids v = foldr ccase v ids where 
   ccase x t = T TRaw [(PV x,t)]
 
+appCons :: Ident -> [Term] -> Term
+appCons = mkApp . Con
+
+appc :: String -> [Term] -> Term
+appc = appCons . identC
+
 tuple2record :: [Term] -> [Assign]
 tuple2record ts = [assign (tupleLabel i) t | (i,t) <- zip [1..] ts]
 
@@ -67,9 +115,74 @@ mkDecl typ = (wildIdent, typ)
 mkLet :: [LocalDef] -> Term -> Term
 mkLet defs t = foldr Let t defs
 
+mkRecTypeN :: Int -> (Int -> Label) -> [Type] -> Type
+mkRecTypeN int lab typs = RecType [ (lab i, t) | (i,t) <- zip [int..] typs]
+
+mkRecType :: (Int -> Label) -> [Type] -> Type
+mkRecType = mkRecTypeN 0
+
+plusRecType :: Type -> Type -> Err Type
+plusRecType t1 t2 = case (t1, t2) of
+  (RecType r1, RecType r2) -> case
+    filter (`elem` (map fst r1)) (map fst r2) of
+      [] -> return (RecType (r1 ++ r2))
+      ls -> Bad $ "clashing labels" +++ unwords (map show ls)
+  _ -> Bad ("cannot add record types" +++ show t1 +++ "and" +++ show t2) 
+
+plusRecord :: Term -> Term -> Err Term
+plusRecord t1 t2 =
+ case (t1,t2) of
+   (R r1, R r2 ) -> return (R ([(l,v) | -- overshadowing of old fields
+                              (l,v) <- r1, not (elem l (map fst r2)) ] ++ r2))
+   (_,    FV rs) -> mapM (plusRecord t1) rs >>= return . FV
+   (FV rs,_    ) -> mapM (`plusRecord` t2) rs >>= return . FV
+   _ -> Bad ("cannot add records" +++ show t1 +++ "and" +++ show t2)
+
+zipAssign :: [Label] -> [Term] -> [Assign]
+zipAssign ls ts = [assign l t | (l,t) <- zip ls ts]
+
+-- type constants
+
 typeType :: Type
 typeType = Sort "Type"
 
+typePType :: Type
+typePType = Sort "PType"
+
+typeStr :: Type
+typeStr = Sort "Str"
+
+cPredef :: Ident
+cPredef = identC "Predef"
+
+cPredefAbs :: Ident
+cPredefAbs = identC "PredefAbs"
+
+typeString, typeFloat, typeInt :: Term
+typeInts :: Integer -> Term
+
+typeString = constPredefRes "String"
+typeInt = constPredefRes "Int"
+typeFloat = constPredefRes "Float"
+typeInts i = App (constPredefRes "Ints") (EInt i)
+
+isTypeInts :: Term -> Bool
+isTypeInts ty = case ty of
+  App c _ -> c == constPredefRes "Ints"
+  _ -> False
+
+constPredefRes :: String -> Term
+constPredefRes s = Q (IC "Predef") (identC s)
+
+isPredefConstant :: Term -> Bool
+isPredefConstant t = case t of
+  Q (IC "Predef") _ -> True
+  Q (IC "PredefAbs") _ -> True
+  _ -> False
+
+defLinType :: Type
+defLinType = RecType [(LIdent "s",  typeStr)]
+
 meta0 :: Term
 meta0 = Meta 0
 
@@ -93,12 +206,14 @@ termOpGF f g = do
 
 termOpModule :: Monad m => (Term -> m Term) -> Module -> m Module
 termOpModule f = judgementOpModule fj where
-  fj = either (liftM Left  . termOpJudgement f) (return . Right)
+  fj = termOpJudgement f
    
 judgementOpModule :: Monad m => (Judgement -> m Judgement) -> Module -> m Module
 judgementOpModule f m = do 
-  mjs <- mapMapM f (mjments m)
+  mjs <- mapMapM fj (mjments m)
   return m {mjments = mjs}
+ where
+  fj = either (liftM Left . f) (return . Right)
    
 termOpJudgement :: Monad m => (Term -> m Term) -> Judgement -> m Judgement
 termOpJudgement f j = do 
@@ -194,6 +309,28 @@ composOp co trm = case trm of
 
    _ -> return trm -- covers K, Vr, Cn, Sort
 
+
+---- should redefine using composOp
+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
+  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
+  _ -> [] -- covers K, Vr, Cn, Sort, Ready
+
 --- just aux to composOp?
 
 mapAssignM :: Monad m => (Term -> m c) -> [Assign] -> m [(Label,(Maybe c,c))]
@@ -207,9 +344,29 @@ changeTableType co i = case i of
     TWild ty  -> co ty >>= return . TWild
     _ -> return i
 
+
+patt2term :: Patt -> Term
+patt2term pt = case pt of
+  PV x      -> Vr x
+  PW        -> Vr wildIdent             --- not parsable, should not occur
+  PC c pp   -> mkApp (Con c) (map patt2term pp)
+  PP p c pp -> mkApp (QC p c) (map patt2term pp)
+  PR r      -> R [assign l (patt2term p) | (l,p) <- r] 
+  PT _ p    -> patt2term p
+  PInt i    -> EInt i
+  PFloat i  -> EFloat i
+  PString s -> K s 
+
+  PAs x p   -> appc "@" [Vr x, patt2term p]            --- an encoding
+  PSeq a b  -> appc "+" [(patt2term a), (patt2term b)] --- an encoding
+  PAlt a b  -> appc "|" [(patt2term a), (patt2term b)] --- an encoding
+  PRep a    -> appc "*" [(patt2term a)]                --- an encoding
+  PNeg a    -> appc "-" [(patt2term a)]                --- an encoding
+
+
 ---- given in lib?
 
-mapMapM :: (Monad m, Ord k) => (v -> m v) -> Map k v -> m (Map k v)
+mapMapM :: (Monad m, Ord k) => (v -> m v) -> Map.Map k v -> m (Map.Map k v)
 mapMapM f = 
-  liftM fromAscList . mapM (\ (x,y) -> liftM ((,) x) $ f y) . assocs 
+  liftM Map.fromAscList . mapM (\ (x,y) -> liftM ((,) x) $ f y) . Map.assocs 
 
diff --git a/src/GF/Devel/Grammar/PatternMatch.hs b/src/GF/Devel/Grammar/PatternMatch.hs
new file mode 100644
index 000000000..38c20fa98
--- /dev/null
+++ b/src/GF/Devel/Grammar/PatternMatch.hs
@@ -0,0 +1,153 @@
+----------------------------------------------------------------------
+-- |
+-- Module      : PatternMatch
+-- Maintainer  : AR
+-- Stability   : (stable)
+-- Portability : (portable)
+--
+-- > CVS $Date: 2005/10/12 12:38:29 $ 
+-- > CVS $Author: aarne $
+-- > CVS $Revision: 1.7 $
+--
+-- pattern matching for both concrete and abstract syntax. AR -- 16\/6\/2003
+-----------------------------------------------------------------------------
+
+module GF.Devel.Grammar.PatternMatch (matchPattern,
+		     testOvershadow, 
+		     findMatch
+		    ) where
+
+
+import GF.Grammar.Terms
+import GF.Grammar.Macros
+import GF.Grammar.PrGF
+import GF.Infra.Ident
+
+import GF.Data.Operations
+
+import Data.List
+import Control.Monad
+
+
+matchPattern :: [(Patt,Term)] -> Term -> Err (Term, Substitution)
+matchPattern pts term = 
+  if not (isInConstantForm term)
+    then prtBad "variables occur in" term
+  else 
+    errIn ("trying patterns" +++ unwords (intersperse "," (map (prt . fst) pts))) $
+    findMatch [([p],t) | (p,t) <- pts] [term]
+
+testOvershadow :: [Patt] -> [Term] -> Err [Patt]
+testOvershadow pts vs = do
+  let numpts = zip pts [0..]
+  let cases  = [(p,EInt i) | (p,i) <- numpts]
+  ts <- mapM (liftM fst . matchPattern cases) vs
+  return $ [p | (p,i) <- numpts, notElem i [i | EInt i <- ts] ]
+
+findMatch :: [([Patt],Term)] -> [Term] -> Err (Term, Substitution)
+findMatch cases terms = case cases of
+   [] -> Bad $"no applicable case for" +++ unwords (intersperse "," (map prt terms))
+   (patts,_):_ | length patts /= length terms -> 
+       Bad ("wrong number of args for patterns :" +++ 
+            unwords (map prt patts) +++ "cannot take" +++ unwords (map prt terms))
+   (patts,val):cc -> case mapM tryMatch (zip patts terms) of
+       Ok substs -> return (val, concat substs)
+       _         -> findMatch cc terms
+
+tryMatch :: (Patt, Term) -> Err [(Ident, Term)]
+tryMatch (p,t) = do 
+  t' <- termForm t
+  trym p t'
+ where
+  isInConstantFormt = True -- tested already
+  trym p t' =
+    case (p,t') of
+      (PVal _ i, (_,Val _ j,_)) 
+          | i == j -> return []
+          | otherwise -> Bad $ "no match of values"
+      (_,(x,Empty,y)) -> trym p (x,K [],y)   -- because "" = [""] = []
+      (PV IW, _) | isInConstantFormt -> return [] -- optimization with wildcard
+      (PV x,  _) | isInConstantFormt -> return [(x,t)]
+      (PString s, ([],K i,[])) | s==i -> return []
+      (PInt s, ([],EInt i,[])) | s==i -> return []
+      (PFloat s,([],EFloat i,[])) | s==i -> return [] --- rounding?
+      (PC p pp, ([], Con f, tt)) | 
+            p `eqStrIdent` f && length pp == length tt ->
+         do matches <- mapM tryMatch (zip pp tt)
+            return (concat matches)
+
+      (PP q p pp, ([], QC r f, tt)) | 
+            -- q `eqStrIdent` r &&  --- not for inherited AR 10/10/2005
+            p `eqStrIdent` f && length pp == length tt ->
+         do matches <- mapM tryMatch (zip pp tt)
+            return (concat matches)
+      ---- hack for AppPredef bug
+      (PP q p pp, ([], Q r f, tt)) | 
+            -- q `eqStrIdent` r && --- 
+            p `eqStrIdent` f && length pp == length tt ->
+         do matches <- mapM tryMatch (zip pp tt)
+            return (concat matches)
+
+      (PR r, ([],R r',[])) |
+            all (`elem` map fst r') (map fst r) ->
+         do matches <- mapM tryMatch 
+                            [(p,snd a) | (l,p) <- r, let Just a = lookup l r']
+            return (concat matches)
+      (PT _ p',_) -> trym p' t'
+      (_, ([],Alias _ _ d,[])) -> tryMatch (p,d)
+
+--      (PP (IC "Predef") (IC "CC") [p1,p2], ([],K s, [])) -> do
+
+      (PAs x p',_) -> do
+         subst <- trym p' t'
+         return $ (x,t) : subst
+
+      (PAlt p1 p2,_) -> checks [trym p1 t', trym p2 t']
+
+      (PNeg p',_) -> case tryMatch (p',t) of
+        Bad _ -> return []
+        _ -> prtBad "no match with negative pattern" p
+
+      (PSeq p1 p2, ([],K s, [])) -> do
+         let cuts = [splitAt n s | n <- [0 .. length s]] 
+         matches <- checks [mapM tryMatch [(p1,K s1),(p2,K s2)] | (s1,s2) <- cuts]
+         return (concat matches)
+
+      (PRep p1, ([],K s, [])) -> checks [
+         trym (foldr (const (PSeq p1)) (PString "") 
+           [1..n]) t' | n <- [0 .. length s]
+        ] >>
+        return []
+      _ -> prtBad "no match in case expr for" t
+  
+isInConstantForm :: Term -> Bool
+isInConstantForm trm = case trm of
+    Cn _     -> True
+    Con _    -> True
+    Q _ _    -> True
+    QC _ _   -> True
+    Abs _ _  -> True
+    App c a  -> isInConstantForm c && isInConstantForm a
+    R r      -> all (isInConstantForm . snd . snd) r
+    K _      -> True
+    Empty    -> True
+    Alias _ _ t -> isInConstantForm t
+    EInt _   -> True
+    _       -> False ---- isInArgVarForm trm
+
+varsOfPatt :: Patt -> [Ident]
+varsOfPatt p = case p of
+  PV x -> [x | not (isWildIdent x)]
+  PC _ ps -> concat $ map varsOfPatt ps
+  PP _ _ ps -> concat $ map varsOfPatt ps
+  PR r    -> concat $ map (varsOfPatt . snd) r
+  PT _ q -> varsOfPatt q
+  _ -> []
+
+-- | to search matching parameter combinations in tables
+isMatchingForms :: [Patt] -> [Term] -> Bool
+isMatchingForms ps ts = all match (zip ps ts') where
+  match (PC c cs, (Cn d, ds)) = c == d && isMatchingForms cs ds
+  match _ = True
+  ts' = map appForm ts
+