made Devel versions of Compute, CheckGrammar, Optimize, etc, to leave GF 2.8 untouched when experimenting

9 files changed, 2535 insertions, 6 deletions

diff --git a/src/GF/Devel/AbsCompute.hs b/src/GF/Devel/AbsCompute.hs
new file mode 100644
index 000000000..a55fbc83f
--- /dev/null
+++ b/src/GF/Devel/AbsCompute.hs
@@ -0,0 +1,145 @@
+----------------------------------------------------------------------
+-- |
+-- Module      : AbsCompute
+-- Maintainer  : AR
+-- Stability   : (stable)
+-- Portability : (portable)
+--
+-- > CVS $Date: 2005/10/02 20:50:19 $ 
+-- > CVS $Author: aarne $
+-- > CVS $Revision: 1.8 $
+--
+-- computation in abstract syntax w.r.t. explicit definitions.
+--
+-- old GF computation; to be updated
+-----------------------------------------------------------------------------
+
+module GF.Devel.AbsCompute (LookDef,
+		   compute, 
+		   computeAbsTerm, 
+		   computeAbsTermIn, 
+		   beta
+		  ) where
+
+import GF.Data.Operations
+
+import GF.Grammar.Abstract
+import GF.Grammar.PrGrammar
+import GF.Grammar.LookAbs
+import GF.Devel.Compute
+
+import Debug.Trace
+import Data.List(intersperse)
+import Control.Monad (liftM, liftM2)
+
+-- for debugging
+tracd m t = t 
+-- tracd = trace
+
+compute :: GFCGrammar -> Exp -> Err Exp
+compute = computeAbsTerm
+
+computeAbsTerm :: GFCGrammar -> 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 Term)
+
+computeAbsTermIn :: LookDef -> [Ident] -> Exp -> Err Exp
+computeAbsTermIn lookd xs e = errIn ("computing" +++ prt e) $ compt xs e where
+  compt vv t = case t of
+--    Prod x a b  -> liftM2 (Prod x) (compt vv a) (compt (x:vv) b)
+--    Abs x b     -> liftM  (Abs  x)              (compt (x:vv) b)
+    _ -> do
+      let t' = beta vv t
+      (yy,f,aa) <- termForm t'
+      let vv' = yy ++ vv
+      aa'    <- mapM (compt vv') aa
+      case look f of
+        Just (Eqs eqs) -> tracd ("\nmatching" +++ prt f) $ 
+                          case findMatch eqs aa' of
+          Ok (d,g) -> do
+            --- let (xs,ts) = unzip g
+            --- ts' <- alphaFreshAll vv' ts
+            let g' = g --- zip xs ts'
+            d' <- compt vv' $ substTerm vv' g' d
+            tracd ("by Egs:" +++ prt d') $ return $ mkAbs yy $ d'
+          _ -> tracd ("no match" +++ prt t') $ 
+               do
+            let v = mkApp f aa'
+            return $ mkAbs yy $ v
+        Just d -> tracd ("define" +++ prt t') $ do
+          da <- compt vv' $ mkApp d aa' 
+          return $ mkAbs yy $ da
+        _ -> do
+          let t2 = mkAbs yy $ mkApp f aa'
+          tracd ("not defined" +++ prt_ t2) $ return t2
+
+  look t = case t of
+     (Q m f) -> case lookd m f of
+       Ok (Just EData) -> Nothing  -- canonical --- should always be QC
+       Ok md -> md
+       _ -> Nothing
+     Eqs _ -> return t ---- for nested fn
+     _ -> Nothing
+
+beta :: [Ident] -> Exp -> Exp
+beta vv c = case c of
+  Let (x,(_,a)) b -> beta vv $ substTerm vv [(x,beta vv a)] (beta (x:vv) b) 
+  App f         a -> 
+    let (a',f') = (beta vv a, beta vv f) in 
+    case f' of
+      Abs x b -> beta vv $ substTerm vv [(x,a')] (beta (x:vv) b) 
+      _ ->               (if a'==a && f'==f then id else beta vv) $ App f' a'
+  Prod x a b      -> Prod x (beta vv a) (beta (x:vv) b)
+  Abs x b         -> Abs x (beta (x:vv) b)
+  _               -> c
+
+-- special version of pattern matching, to deal with comp under lambda
+
+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 (tracd ("value" +++ prt_ val) val, concat substs)
+     _         -> findMatch cc terms
+
+tryMatch :: (Patt, Term) -> Err [(Ident, Term)]
+tryMatch (p,t) = do 
+  t' <- termForm t
+  trym p t'
+ where
+
+  trym p t' = err (\s -> tracd s (Bad s)) (\t -> tracd (prtm p t) (return t)) $ ---- 
+              case (p,t') of
+    (PV IW, _) | notMeta t -> return [] -- optimization with wildcard
+    (PV x,  _) | notMeta t -> 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?
+    (PP q p pp, ([], QC r f, tt)) | 
+       p `eqStrIdent` f && length pp == length tt -> do
+         matches <- mapM tryMatch (zip pp tt)
+         return (concat matches)
+    (PP q p pp, ([], Q r f, tt)) | 
+       p `eqStrIdent` f && length pp == length tt -> do
+         matches <- mapM tryMatch (zip pp tt)
+         return (concat matches)
+    (PT _ p',_) -> trym p' t'
+    (_, ([],Alias _ _ d,[])) -> tryMatch (p,d)
+    (PAs x p',_) -> do
+       subst <- trym p' t'
+       return $ (x,t) : subst
+    _ -> Bad ("no match in pattern" +++ prt p +++ "for" +++ prt t)
+
+  notMeta e = case e of
+    Meta _  -> False
+    App f a -> notMeta f &&  notMeta a  
+    Abs _ b -> notMeta b
+    _ -> True
+
+  prtm p g = 
+    prt p +++ ":" ++++ unwords ["  " ++ prt_ x +++ "=" +++ prt_ y +++ ";" | (x,y) <- g]
diff --git a/src/GF/Devel/CheckGrammar.hs b/src/GF/Devel/CheckGrammar.hs
new file mode 100644
index 000000000..c3fde011d
--- /dev/null
+++ b/src/GF/Devel/CheckGrammar.hs
@@ -0,0 +1,1079 @@
+----------------------------------------------------------------------
+-- |
+-- Module      : CheckGrammar
+-- Maintainer  : AR
+-- Stability   : (stable)
+-- Portability : (portable)
+--
+-- > CVS $Date: 2005/11/11 23:24:33 $ 
+-- > CVS $Author: aarne $
+-- > CVS $Revision: 1.31 $
+--
+-- AR 4\/12\/1999 -- 1\/4\/2000 -- 8\/9\/2001 -- 15\/5\/2002 -- 27\/11\/2002 -- 18\/6\/2003
+--
+-- type checking also does the following modifications:
+--
+--  - types of operations and local constants are inferred and put in place
+--
+--  - both these types and linearization types are computed
+--
+--  - tables are type-annotated
+-----------------------------------------------------------------------------
+
+module GF.Devel.CheckGrammar (
+  showCheckModule, justCheckLTerm, allOperDependencies, topoSortOpers) where
+
+import GF.Grammar.Grammar
+import GF.Infra.Ident
+import GF.Infra.Modules
+import GF.Grammar.Refresh ----
+
+import GF.Devel.TypeCheck
+import GF.Grammar.Values (cPredefAbs) ---
+
+import GF.Grammar.PrGrammar
+import GF.Grammar.Lookup
+import GF.Grammar.LookAbs
+import GF.Grammar.Macros
+import GF.Grammar.ReservedWords ----
+import GF.Grammar.PatternMatch
+import GF.Grammar.AppPredefined
+import GF.Grammar.Lockfield (isLockLabel)
+
+import GF.Data.Operations
+import GF.Infra.CheckM
+
+import Data.List
+import qualified Data.Set as Set
+import qualified Data.Map as Map
+import Control.Monad
+import Debug.Trace ---
+
+
+showCheckModule :: [SourceModule] -> SourceModule -> Err ([SourceModule],String)
+showCheckModule mos m = do
+  (st,(_,msg)) <- checkStart $ checkModule mos m
+  return (st, unlines $ reverse msg)
+
+-- | checking is performed in the dependency order of modules
+checkModule :: [SourceModule] -> SourceModule -> Check [SourceModule]
+checkModule ms (name,mod) = checkIn ("checking module" +++ prt name) $ case mod of
+
+  ModMod mo@(Module mt st fs me ops js) -> do
+    checkRestrictedInheritance ms (name, mo)
+    js' <- case mt of
+      MTAbstract -> mapMTree (checkAbsInfo gr name) js
+
+      MTTransfer a b -> mapMTree (checkAbsInfo gr name) js
+
+      MTResource -> mapMTree (checkResInfo gr name) js
+
+      MTConcrete a -> do
+        checkErr $ topoSortOpers $ allOperDependencies name js
+        ModMod abs <- checkErr $ lookupModule gr a
+        js1 <- checkCompleteGrammar abs mo
+        mapMTree (checkCncInfo gr name (a,abs)) js1
+
+      MTInterface -> mapMTree (checkResInfo gr name) js
+
+      MTInstance a -> do
+        ModMod abs <- checkErr $ lookupModule gr a
+        -- checkCompleteInstance abs mo -- this is done in Rebuild
+        mapMTree (checkResInfo gr name) js
+
+    return $ (name, ModMod (Module mt st fs me ops js')) : ms
+
+  _ -> return $ (name,mod) : ms
+ where
+   gr  = MGrammar $ (name,mod):ms
+
+-- check if restricted inheritance modules are still coherent
+-- i.e. that the defs of remaining names don't depend on omitted names
+---checkRestrictedInheritance :: [SourceModule] -> SourceModule -> Check ()
+checkRestrictedInheritance mos (name,mo) = do
+  let irs = [ii | ii@(_,mi) <- extend mo, mi /= MIAll]  -- names with restr. inh.
+  let mrs = [((i,m),mi) | (i,ModMod m) <- mos, Just mi <- [lookup i irs]] 
+                             -- the restr. modules themself, with restr. infos
+  mapM_ checkRem mrs
+ where
+   checkRem ((i,m),mi) = do
+     let (incl,excl) = partition (isInherited mi) (map fst (tree2list (jments m)))
+     let incld c   = Set.member c (Set.fromList incl)
+     let illegal c = Set.member c (Set.fromList excl)
+     let illegals = [(f,is) | 
+           (f,cs) <- allDeps, incld f, let is = filter illegal cs, not (null is)]
+     case illegals of 
+       [] -> return ()
+       cs -> fail $ "In inherited module" +++ prt i ++
+               ", dependence of excluded constants:" ++++
+               unlines ["  " ++ prt f +++ "on" +++ unwords (map prt is) | 
+                              (f,is) <- cs]
+   allDeps = ---- transClosure $ Map.fromList $ 
+             concatMap (allDependencies (const True)) 
+                              [jments m | (_,ModMod m) <- mos]
+   transClosure ds = ds ---- TODO: check in deeper modules
+
+-- | check if a term is typable
+justCheckLTerm :: SourceGrammar -> Term -> Err Term
+justCheckLTerm src t = do
+  ((t',_),_) <- checkStart (inferLType src t)
+  return t'
+
+checkAbsInfo :: SourceGrammar -> Ident -> (Ident,Info) -> Check (Ident,Info)
+checkAbsInfo st m (c,info) = do
+---- checkReservedId c
+ case info of
+   AbsCat (Yes cont) _ -> mkCheck "category" $ 
+     checkContext st cont ---- also cstrs
+   AbsFun (Yes typ0) md -> do
+    typ <- compAbsTyp [] typ0   -- to calculate let definitions
+    mkCheck "type of function" $ checkTyp st typ 
+    md' <- case md of
+       Yes d -> do
+         let d' = elimTables d
+         mkCheckWarn "definition of function" $ checkEquation st (m,c) d'
+         return $ Yes d'
+       _ -> return md
+    return $ (c,AbsFun (Yes typ) md')
+   _ -> return (c,info)
+ where
+   mkCheck cat ss = case ss of
+     [] -> return (c,info)
+     ["[]"] -> return (c,info) ----
+     _  -> checkErr $ prtBad (unlines ss ++++ "in" +++ cat) c
+   ---- temporary solution when tc of defs is incomplete
+   mkCheckWarn cat ss = case ss of
+     [] -> return (c,info)
+     ["[]"] -> return (c,info) ----
+     _  -> checkWarn (unlines ss ++++ "in" +++ cat +++ prt c) >> return (c,info)
+   compAbsTyp g t = case t of
+     Vr x -> maybe (fail ("no value given to variable" +++ prt x)) return $ lookup x g
+     Let (x,(_,a)) b -> do
+       a' <- compAbsTyp g a
+       compAbsTyp ((x, a'):g) b
+     Prod x a b -> do
+       a' <- compAbsTyp g a
+       b' <- compAbsTyp ((x,Vr x):g) b
+       return $ Prod x a' b'
+     Abs _ _ -> return t
+     _ -> composOp (compAbsTyp g) t
+
+   elimTables e = case e of
+     S t a  -> elimSel (elimTables t) (elimTables a)
+     T _ cs -> Eqs [(elimPatt p, elimTables t) | (p,t) <- cs]
+     _ -> composSafeOp elimTables e
+   elimPatt p = case p of
+     PR lps -> map snd lps
+     _ -> [p]
+   elimSel t a = case a of
+     R fs -> mkApp t (map (snd . snd) fs)
+     _ -> mkApp t [a]
+
+checkCompleteGrammar :: SourceAbs -> SourceCnc -> Check (BinTree Ident Info)
+checkCompleteGrammar abs cnc = do
+  let js = jments cnc
+  let fs = tree2list $ jments abs
+  foldM checkOne js fs
+ where
+   checkOne js i@(c,info) = case info of
+     AbsFun (Yes _) _ -> case lookupIdent c js of
+       Ok _ -> 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
+         checkWarn $ 
+           "Warning: no linearization type for" +++ prt c ++ 
+           ", inserting default {s : Str}" 
+         return $ updateTree (c,CncCat (Yes defLinType) nope nope) 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')
+
+    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]]
+      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)
+ where
+   infer = inferLType gr
+   check = checkLType gr
+   chIn cat = checkIn ("Happened in" +++ cat +++ prt c +++ ":")
+   comp = computeLType gr
+
+   checkUniq xss = case xss of
+     x:y:xs 
+      | x == y -> raise $ "ambiguous for argument list" +++ 
+                         unwords (map (prtType gr) x)  
+      | otherwise -> checkUniq $ y:xs
+     _ -> 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
+      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
+      cat        <- return $ snd cat0
+      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
+      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)
+
+    _ -> checkResInfo gr m (c,info)
+
+ where
+   env = gr
+   infer = inferLType gr
+   comp = computeLType gr 
+   check = checkLType gr
+   chIn cat = checkIn ("Happened in" +++ cat +++ prt c +++ ":")
+
+checkIfParType :: SourceGrammar -> Type -> Check ()
+checkIfParType st typ = checkCond ("Not parameter type" +++ prt typ) (isParType typ)
+  where
+   isParType ty = True ----
+{- case ty of
+     Cn typ -> case lookupConcrete st typ of
+       Ok (CncParType _ _ _) -> True
+       Ok (CncOper _ ty' _) -> isParType ty'
+       _ -> False
+     Q p t -> case lookupInPackage st (p,t) of
+       Ok (CncParType _ _ _) -> True
+       _ -> False
+     RecType r -> all (isParType . snd) r
+     _ -> False
+-}
+
+checkIfStrType :: SourceGrammar -> Type -> Check ()
+checkIfStrType st typ = case typ of
+  Table arg val -> do
+    checkIfParType st arg 
+    checkIfStrType st val
+  _ | typ == typeStr -> return ()
+  _ -> prtFail "not a string type" typ
+
+
+checkIfLinType :: SourceGrammar -> 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
+    _ -> 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 gr t = do
+  g0 <- checkGetContext
+  let g = [(x, Vr x) | (x,_) <- g0]
+  checkInContext g $ comp t
+ where
+  comp ty = case ty of
+
+    App (Q (IC "Predef") (IC "Ints")) _ -> return ty ---- shouldn't be needed
+    Q (IC "Predef") (IC "Int")          -> return ty ---- shouldn't be needed
+    Q (IC "Predef") (IC "Float")        -> return ty ---- shouldn't be needed
+    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"] -> 
+      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 ident -> checkIn ("module" +++ prt m) $ do
+      ty' <- checkErr (lookupResDef 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!
+
+    App f a -> do
+      f' <- comp f
+      a' <- comp a
+      case f' of
+        Abs x b -> checkInContext [(x,a')] $ comp b
+        _ -> return $ App f' a'
+
+    Prod x a b -> do
+      a' <- comp a
+      b' <- checkInContext [(x,Vr x)] $ comp b
+      return $ Prod x a' b'
+
+    Abs x b -> do
+      b' <- checkInContext [(x,Vr x)] $ comp b
+      return $ Abs x b'
+
+    ExtR r s -> do
+      r' <- comp r
+      s' <- comp s
+      case (r',s') of
+        (RecType rs, RecType ss) -> checkErr (plusRecType r' s') >>= comp
+        _ -> return $ ExtR r' s'
+
+    RecType fs -> 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
+
+    _ -> composOp comp ty
+
+checkPrintname :: SourceGrammar -> Perh 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
+  _ -> 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 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
+     ,
+     checkErr (lookupResDef gr m ident) >>= infer
+     ,
+{-
+     do
+       over <- getOverload gr Nothing trm
+       case over of
+         Just trty -> return trty
+         _ -> prtFail "not overloaded" trm
+     ,
+-}
+     prtFail "cannot infer type of constant" trm
+     ]
+
+   QC m ident | isPredef m -> termWith trm $ checkErr (typPredefined ident)
+
+   QC m ident -> checks [
+       termWith trm $ checkErr (lookupResType gr m ident) >>= comp
+       ,
+       checkErr (lookupResDef gr m ident) >>= infer
+       ,
+       prtFail "cannot infer type of canonical constant" trm
+       ]
+
+   Val ty i -> termWith trm $ return ty
+
+   Vr ident -> termWith trm $ checkLookup ident
+
+   Typed e t -> do
+     t' <- comp t
+     check e t'
+     return (e,t')
+
+   App f a -> do
+     over <- getOverload gr Nothing trm
+     case over of
+       Just trty -> return trty
+       _ -> do
+         (f',fty) <- infer f
+         fty' <- comp fty
+         case fty' of
+           Prod z arg val -> do 
+             a' <- justCheck a arg
+             ty <- if isWildIdent z 
+                      then return val
+                      else substituteLType [(z,a')] val
+             return (App f' a',ty) 
+           _ -> raise ("function type expected for"+++ 
+                      prt f +++"instead of" +++ prtType env fty)
+
+   S f x -> do
+     (f', fty) <- infer f
+     case fty of
+       Table arg val -> do
+         x'<- justCheck x arg
+         return (S f' x', val)
+       _ -> prtFail "table lintype expected for the table in" trm
+
+   P t i -> do
+     (t',ty) <- infer t   --- ??
+     ty' <- comp ty
+-----     let tr2 = PI t' i (labelIndex ty' i)
+     let tr2 = P t' i
+     termWith tr2 $ checkErr $ case ty' of
+       RecType ts -> maybeErr ("unknown label" +++ prt i +++ "in" +++ prt ty') $ 
+                     lookup i ts
+       _ -> prtBad ("record type expected for" +++ prt t +++ "instead of") ty'
+   PI t i _ -> infer $ P t i
+
+   R r -> do
+     let (ls,fs) = unzip r
+     fsts <- mapM inferM fs
+     let ts = [ty | (Just ty,_) <- fsts]
+     checkCond ("cannot infer type of record"+++ prt trm) (length ts == length fsts)
+     return $ (R (zip ls fsts), RecType (zip ls ts))
+
+   T (TTyped arg) pts -> do
+     (_,val) <- checks $ map (inferCase (Just arg)) pts
+     check trm (Table arg val)
+   T (TComp arg) pts -> do
+     (_,val) <- checks $ map (inferCase (Just arg)) pts
+     check trm (Table arg val)
+   T ti pts -> do  -- tries to guess: good in oper type inference
+     let pts' = [pt | pt@(p,_) <- pts, isConstPatt p]
+     case pts' of 
+       [] -> prtFail "cannot infer table type of" trm
+----       PInt k : _ -> return $ Ints $ max [i | PInt i <- pts'] 
+       _  -> do 
+         (arg,val) <- checks $ map (inferCase Nothing) pts'
+         check trm (Table arg val)
+   V arg pts -> do
+     (_,val) <- checks $ map infer pts
+     return (trm, Table arg val)
+
+   K s  -> do
+     if elem ' ' s
+        then checkWarn ("WARNING: space in token \"" ++ s ++ 
+                        "\". Lexical analysis may fail.")
+        else return ()
+     return (trm, typeStr)
+
+   EInt i -> return (trm, typeInt)
+
+   EFloat i -> return (trm, typeFloat)
+
+   Empty -> return (trm, typeStr)
+
+   C s1 s2 -> 
+     check2 (flip justCheck typeStr) C s1 s2 typeStr
+
+   Glue s1 s2 -> 
+     check2 (flip justCheck typeStr) Glue s1 s2 typeStr ---- typeTok
+
+---- 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)
+--     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
+        return (c',v'))
+     return (Alts (t',aa'), typeStr)
+
+   RecType r -> do
+     let (ls,ts) = unzip r
+     ts' <- mapM (flip justCheck typeType) ts 
+     return (RecType (zip ls ts'), typeType)
+
+   ExtR r s -> do
+     (r',rT) <- infer r 
+     rT'     <- comp rT
+     (s',sT) <- infer s
+     sT'     <- comp sT
+
+     let trm' = ExtR r' s'
+     ---- trm'    <- checkErr $ plusRecord r' s'
+     case (rT', sT') of
+       (RecType rs, RecType ss) -> do
+         rt <- checkErr $ plusRecType rT' sT'
+         check trm' rt ---- return (trm', rt)
+       _ | rT' == typeType && sT' == typeType -> return (trm', typeType)
+       _ -> prtFail "records or record types expected in" trm
+
+   Sort _     -> 
+     termWith trm $ return typeType
+
+   Prod x a b -> do
+     a' <- justCheck a typeType
+     b' <- checkInContext [(x,a')] $ justCheck b typeType
+     return (Prod x a' b', typeType)
+
+   Table p t  -> do
+     p' <- justCheck p typeType --- check p partype! 
+     t' <- justCheck t typeType
+     return $ (Table p' t', typeType)
+
+   FV vs -> do
+     (_,ty) <- checks $ map infer vs
+---     checkIfComplexVariantType trm ty
+     check trm ty
+
+   _ -> prtFail "cannot infer lintype of" trm
+
+ where
+   env = gr
+   infer = inferLType env
+   comp = computeLType env 
+
+   check = checkLType env
+   
+   isPredef m = elem m [cPredef,cPredefAbs]
+
+   justCheck ty te = check ty te >>= return . fst
+
+   -- for record fields, which may be typed
+   inferM (mty, t) = do
+     (t', ty') <- case mty of
+       Just ty -> check ty t
+       _ -> infer t
+     return (Just ty',t')
+
+   inferCase mty (patt,term) = do
+     arg  <- maybe (inferPatt patt) return mty
+     cont <- pattContext env arg patt
+     i    <- checkUpdates cont
+     (_,val) <- infer term
+     checkResets i
+     return (arg,val)
+   isConstPatt p = case p of
+     PC _ ps -> True --- all isConstPatt ps
+     PP _ _ ps -> True --- all isConstPatt ps
+     PR ps -> all (isConstPatt . snd) ps
+     PT _ p -> isConstPatt p
+     PString _ -> True
+     PInt _ -> True
+     PFloat _ -> True
+     PSeq p q -> isConstPatt p && isConstPatt q
+     PAlt p q -> isConstPatt p && isConstPatt q
+     PRep p -> isConstPatt p
+     PNeg p -> isConstPatt p
+     PAs _ p -> isConstPatt p
+     _ -> False
+
+   inferPatt p = case p of
+     PP q c ps | q /= cPredef -> checkErr $ lookupResType gr q c >>= valTypeCnc
+     PAs _ p  -> inferPatt p
+     PNeg p   -> inferPatt p
+     PAlt p q -> checks [inferPatt p, inferPatt q]
+     PSeq _ _ -> return $ typeStr
+     PRep _   -> return $ typeStr
+     _ -> infer (patt2term p) >>= return . snd
+
+
+-- type inference: Nothing, type checking: Just t
+-- the latter permits matching with value type
+getOverload :: SourceGrammar -> 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
+       Ok typs -> do
+         ttys <- mapM infer ts
+         v <- matchOverload f typs ttys
+         return $ Just v
+       _ -> return Nothing
+     _ -> return Nothing
+ where
+   infer = inferLType env
+   matchOverload f typs ttys = do
+     let (tts,tys) = unzip ttys
+     let vfs = lookupOverloadInstance tys typs
+
+     case [vf | vf@(v,f) <- vfs, matchVal mt v] of
+       [(val,fun)] -> return (mkApp fun tts, val)
+       [] -> raise $ "no overload instance of" +++ prt f +++ 
+         "for" +++ unwords (map (prtType env) tys) +++ "among" ++++ 
+         unlines ["  " ++ unwords (map (prtType env) ty) | (ty,_) <- typs] ++
+         maybe [] (("with value type" +++) . prtType env) mt
+
+      ----  ++++ "DEBUG" +++ unwords (map show tys) +++ ";" 
+      ----  ++++ unlines (map (show . fst) typs) ----
+
+       vfs' -> case [(v,f) | (v,f) <- vfs', noProd v] of
+         [(val,fun)] -> do
+           checkWarn $ "WARNING: overloading of" +++ prt f +++ 
+             "resolved by excluding partial applications:" ++++
+             unlines [prtType env ty | (ty,_) <- vfs', not (noProd ty)]
+           return (mkApp fun tts, val)
+
+         _ -> raise $ "ambiguous overloading of" +++ prt f +++
+           "for" +++ unwords (map (prtType env) tys) ++++ "with alternatives" ++++ 
+           unlines [prtType env ty | (ty,_) <- vfs']
+
+   matchVal mt v = elem mt ([Nothing,Just v] ++ unlocked) where
+     unlocked = case v of
+       RecType fs -> [Just $ RecType $ filter (not . isLockLabel . fst) fs]
+       _ -> []
+   ---- TODO: accept subtypes
+   ---- TODO: use a trie
+   lookupOverloadInstance tys typs = 
+     [(mkFunType rest val, t) | 
+       let lt = length tys,
+       (ty,(val,t)) <- typs, length ty >= lt,
+       let (pre,rest) = splitAt lt ty, 
+       pre == tys
+     ]
+
+   noProd ty = case ty of
+     Prod _ _ _ -> False
+     _ -> True
+
+checkLType :: SourceGrammar -> Term -> Type -> Check (Term, Type)
+checkLType env trm typ0 = do
+
+  typ <- comp typ0
+
+  case trm of
+
+    Abs x c -> do
+      case typ of
+        Prod z a b -> do 
+          checkUpdate (x,a)
+          (c',b') <- if isWildIdent z
+                        then check c b
+                        else do
+                          b' <- checkIn "abs" $ substituteLType [(z,Vr x)] b
+                          check c b'
+          checkReset
+          return $ (Abs x c', Prod x a b')
+        _ -> raise $ "product expected instead of" +++ prtType env typ
+
+    App f a -> do
+       over <- getOverload env (Just typ) trm
+       case over of
+         Just trty -> return trty
+         _ -> do
+          (trm',ty') <- infer trm
+          termWith trm' $ checkEq typ ty' trm'
+
+    Q _ _ -> do
+       over <- getOverload env (Just typ) trm
+       case over of
+         Just trty -> return trty
+         _ -> do
+          (trm',ty') <- infer trm
+          termWith trm' $ checkEq typ ty' trm'
+
+    T _ [] ->
+      prtFail "found empty table in type" typ
+    T _ cs -> case typ of 
+      Table arg val -> do 
+        case allParamValues env arg of
+          Ok vs -> do
+            let ps0 = map fst cs
+            ps <- checkErr $ testOvershadow ps0 vs
+            if null ps 
+              then return () 
+              else checkWarn $ "WARNING: patterns never reached:" +++ 
+                               concat (intersperse ", " (map prt ps))
+
+          _ -> return () -- happens with variable types
+        cs' <- mapM (checkCase arg val) cs
+        return (T (TTyped arg) cs', typ)
+      _ -> raise $ "table type expected for table instead of" +++ prtType env typ
+
+    R r -> case typ of --- why needed? because inference may be too difficult
+       RecType rr -> do
+         let (ls,_) = unzip rr        -- labels of expected type
+         fsts <- mapM (checkM r) rr   -- check that they are found in the record
+         return $ (R fsts, typ)       -- normalize record
+
+       _ -> prtFail "record type expected in type checking instead of" typ
+
+    ExtR r s -> case typ of
+       _ | typ == typeType -> do
+         trm' <- comp trm
+         case trm' of
+           RecType _ -> termWith trm $ return typeType
+           ExtR (Vr _) (RecType _) -> termWith trm $ return typeType 
+                                      -- ext t = t ** ...
+           _ -> prtFail "invalid record type extension" trm
+       RecType rr -> do
+         (r',ty,s') <- checks [
+            do (r',ty) <- infer r
+               return (r',ty,s)
+           ,
+            do (s',ty) <- infer s
+               return (s',ty,r)
+            ]
+         case ty of
+           RecType rr1 -> do
+                let (rr0,rr2) = recParts rr rr1
+                r2 <- justCheck r' rr0
+                s2 <- justCheck s' rr2
+                return $ (ExtR r2 s2, typ) 
+           _ -> raise ("record type expected in extension of" +++ prt r +++ 
+                       "but found" +++ prt ty)
+
+       ExtR ty ex -> do
+         r' <- justCheck r ty
+         s' <- justCheck s ex
+         return $ (ExtR r' s', typ) --- is this all?
+
+       _ -> prtFail "record extension not meaningful for" typ
+
+    FV vs -> do
+      ttys <- mapM (flip check typ) vs
+---      checkIfComplexVariantType trm typ
+      return (FV (map fst ttys), typ) --- typ' ?
+
+    S tab arg -> checks [ do
+      (tab',ty) <- infer tab
+      ty'       <- comp ty
+      case ty' of
+        Table p t -> do
+          (arg',val) <- check arg p
+          checkEq typ t trm
+          return (S tab' arg', t)
+        _ -> raise $ "table type expected for applied table instead of" +++ 
+                   prtType env ty'
+     , do
+      (arg',ty) <- infer arg
+      ty'       <- comp ty
+      (tab',_)  <- check tab (Table ty' typ)
+      return (S tab' arg', typ)
+      ]
+    Let (x,(mty,def)) body -> case mty of
+      Just ty -> do
+        (def',ty') <- check def ty
+        checkUpdate (x,ty')
+        body' <- justCheck body typ
+        checkReset
+        return (Let (x,(Just ty',def')) body', typ)
+      _ -> do
+        (def',ty) <- infer def  -- tries to infer type of local constant
+        check (Let (x,(Just ty,def')) body) typ
+
+    _ -> do
+      (trm',ty') <- infer trm
+      termWith trm' $ checkEq typ ty' trm'
+ where
+   cnc = env
+   infer = inferLType env
+   comp = computeLType env 
+
+   check = checkLType env
+   
+   justCheck ty te = check ty te >>= return . fst
+
+   checkEq = checkEqLType env
+
+   recParts rr t = (RecType rr1,RecType rr2) where 
+     (rr1,rr2) = partition (flip elem (map fst t) . fst) rr 
+
+   checkM rms (l,ty) = case lookup l rms of
+     Just (Just ty0,t) -> do
+       checkEq ty ty0 t
+       (t',ty') <- check t ty
+       return (l,(Just ty',t'))
+     Just (_,t) -> do
+       (t',ty') <- check t ty
+       return (l,(Just ty',t'))
+     _ -> prtFail "cannot find value for label" l
+
+   checkCase arg val (p,t) = do
+     cont <- pattContext env arg p
+     i    <- checkUpdates cont
+     t'   <- justCheck t val
+     checkResets i
+     return (p,t')
+
+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
+    checkCond ("wrong number of arguments for constructor in" +++ prt p) 
+              (length cont == length ps)
+    checkEqLType env typ v (patt2term p)
+    mapM (uncurry (pattContext env)) (zip (map snd cont) ps) >>= return . concat
+  PR r -> do
+    typ' <- computeLType env typ
+    case typ' of
+      RecType t -> do
+        let pts = [(ty,tr) | (l,tr) <- r, Just ty <- [lookup l t]]
+        ----- checkWarn $ prt p ++++ show pts ----- debug
+        mapM (uncurry (pattContext env)) pts >>= return . concat
+      _ -> prtFail "record type expected for pattern instead of" typ'
+  PT t p' -> do
+    checkEqLType env typ t (patt2term p')
+    pattContext env typ p'
+
+  PAs x p -> do
+    g <- pattContext env typ p
+    return $ (x,typ):g
+
+  PAlt p' q -> do
+    g1 <- pattContext env typ p'
+    g2 <- pattContext env typ q
+    let pts = [pt | pt <- g1, notElem pt g2] ++ [pt | pt <- g2, notElem pt g1]
+    checkCond 
+      ("incompatible bindings of" +++ 
+       unwords (nub (map (prt . fst) pts))+++ 
+       "in pattern alterantives" +++ prt p) (null pts) 
+    return g1 -- must be g1 == g2
+  PSeq p q -> do
+    g1 <- pattContext env typ p
+    g2 <- pattContext env typ q
+    return $ g1 ++ g2
+  PRep p' -> noBind typeStr p'
+  PNeg p' -> noBind typ p'
+
+  _ -> return [] ---- check types!
+ where 
+   cnc = env
+   noBind typ p' = do
+    co <- pattContext env typ p'
+    if not (null co)
+      then checkWarn ("no variable bound inside pattern" +++ prt p) 
+           >> return []
+      else return []
+
+-- auxiliaries
+
+type LTEnv = SourceGrammar
+
+termWith :: Term -> Check Type -> Check (Term, Type)
+termWith t ct = do
+  ty <- ct
+  return (t,ty)
+
+-- | light-weight substitution for dep. types
+substituteLType :: Context -> Type -> Check Type
+substituteLType g t = case t of
+  Vr x -> return $ maybe t id $ lookup x g
+  _ -> composOp (substituteLType g) t
+
+-- | compositional check\/infer of binary operations
+check2 :: (Term -> Check Term) -> (Term -> Term -> Term) -> 
+          Term -> Term -> Type -> Check (Term,Type)
+check2 chk con a b t = do
+  a' <- chk a
+  b' <- chk b
+  return (con a' b', t)
+
+checkEqLType :: LTEnv -> Type -> Type -> Term -> Check Type
+checkEqLType env t u trm = do
+  (b,t',u',s) <- checkIfEqLType env t u trm
+  case b of
+    True  -> return t'
+    False -> raise $ s +++ "type of" +++ prt trm +++ 
+                        ": expected:" +++ prtType env t ++++ 
+                        "inferred:" +++ prtType env u
+
+checkIfEqLType :: LTEnv -> Type -> Type -> Term -> Check (Bool,Type,Type,String)
+checkIfEqLType env t u trm = do
+  t' <- comp t 
+  u' <- comp u
+  case t' == u' || alpha [] t' u' of
+    True -> return (True,t',u',[])
+    -- forgive missing lock fields by only generating a warning.
+    --- better: use a flag to forgive? (AR 31/1/2006)
+    _ -> case missingLock [] t' u' of
+      Ok lo -> do
+        checkWarn $ "WARNING: missing lock field" +++ unwords (map prt lo)
+        return (True,t',u',[])
+      Bad s -> return (False,t',u',s)
+
+  where
+
+   -- t is a subtype of u 
+   --- quick hack version of TC.eqVal
+   alpha g t u = case (t,u) of  
+
+     -- error (the empty type!) is subtype of any other type
+     (_,Q (IC "Predef") (IC "Error")) -> True
+
+     -- contravariance
+     (Prod x a b, Prod y c d) -> alpha g c a && alpha ((x,y):g) b d 
+                              
+     -- record subtyping
+     (RecType rs, RecType ts) -> all (\ (l,a) -> 
+                                   any (\ (k,b) -> alpha g a b && l == k) ts) rs
+     (ExtR r s, ExtR r' s') -> alpha g r r' && alpha g s s'
+     (ExtR r s, t) -> alpha g r t || alpha g s t
+
+     -- the following say that Ints n is a subset of Int and of Ints m >= n
+     (App (Q (IC "Predef") (IC "Ints")) (EInt n), 
+        App (Q (IC "Predef") (IC "Ints")) (EInt m)) -> m >= n
+     (App (Q (IC "Predef") (IC "Ints")) (EInt n), 
+        Q (IC "Predef") (IC "Int"))                 -> True ---- check size!
+     
+     (Q (IC "Predef") (IC "Int"),  ---- why this ???? AR 11/12/2005
+        App (Q (IC "Predef") (IC "Ints")) (EInt n)) -> True
+
+     ---- this should be made in Rename
+     (Q  m a, Q  n b) | a == b -> elem m (allExtendsPlus env n) 
+                               || elem n (allExtendsPlus env m)
+                               || m == n --- for Predef
+     (QC m a, QC n b) | a == b -> elem m (allExtendsPlus env n) 
+                               || elem n (allExtendsPlus env m)
+     (QC m a, Q  n b) | a == b -> elem m (allExtendsPlus env n) 
+                               || elem n (allExtendsPlus env m)
+     (Q  m a, QC n b) | a == b -> elem m (allExtendsPlus env n) 
+                               || elem n (allExtendsPlus env m)
+
+     (Table a b,  Table c d)  -> alpha g a c && alpha g b d
+     (Vr x,       Vr y)       -> x == y || elem (x,y) g || elem (y,x) g
+     _                        -> t == u 
+     --- the following should be one-way coercions only. AR 4/1/2001
+                                  || elem t sTypes && elem u sTypes
+                                  || (t == typeType && u == typePType) 
+                                  || (u == typeType && t == typePType) 
+
+   missingLock g t u = case (t,u) of  
+     (RecType rs, RecType ts) -> 
+       let 
+         ls = [l | (l,a) <- rs, 
+                   not (any (\ (k,b) -> alpha g a b && l == k) ts)]
+         (locks,others) = partition isLockLabel ls
+       in case others of
+         _:_ -> Bad $ "missing record fields" +++ unwords (map prt others)
+         _ -> return locks
+     -- contravariance
+     (Prod x a b, Prod y c d) -> do
+        ls1 <- missingLock g c a
+        ls2 <- missingLock g b d
+        return $ ls1 ++ ls2
+
+     _ -> Bad ""
+
+   sTypes = [typeStr, typeTok, 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
+  Prod x a b -> prtType env a +++ "->" +++ prtType env b
+  _ -> prtt ty
+ where
+   prtt t = prt t
+   ---- use computeLType gr to check if really equal to the cat with lock
+
+
+-- | linearization types and defaults
+linTypeOfType :: SourceGrammar -> Ident -> Type -> Check (Context,Type)
+linTypeOfType cnc m typ = do
+  (cont,cat) <- checkErr $ typeSkeleton typ
+  val  <- lookLin cat
+  args <- mapM mkLinArg (zip [0..] cont)
+  return (args, val)
+ where
+   mkLinArg (i,(n,mc@(m,cat))) = do
+     val  <- lookLin mc
+     let vars = mkRecType varLabel $ replicate n typeStr
+	 symb = argIdent n cat i
+     rec <- checkErr $ errIn ("extending" +++ prt vars +++ "with" +++ prt val) $
+            plusRecType vars val
+     return (symb,rec)
+   lookLin (_,c) = checks [ --- rather: update with defLinType ?
+      checkErr (lookupLincat cnc m c) >>= computeLType cnc
+     ,return defLinType
+     ]
+
+-- | dependency check, detecting circularities and returning topo-sorted list
+
+allOperDependencies :: Ident -> BinTree Ident Info -> [(Ident,[Ident])]
+allOperDependencies m = allDependencies (==m)
+
+allDependencies :: (Ident -> Bool) -> BinTree Ident Info -> [(Ident,[Ident])]
+allDependencies ism b = 
+  [(f, nub (concatMap opty (pts i))) | (f,i) <- tree2list b]
+  where
+    opersIn t = case t of
+      Q n c | ism n -> [c]
+      QC n c | ism n -> [c]
+      _ -> 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]
+      _              -> []
+
+topoSortOpers :: [(Ident,[Ident])] -> Err [Ident]
+topoSortOpers st = do
+  let eops = topoTest st
+  either 
+    return 
+    (\ops -> Bad ("circular definitions:" +++ unwords (map prt (head ops))))
+    eops
diff --git a/src/GF/Devel/Compile.hs b/src/GF/Devel/Compile.hs
index f5a16114f..1b6f2710e 100644
--- a/src/GF/Devel/Compile.hs
+++ b/src/GF/Devel/Compile.hs
@@ -6,9 +6,9 @@ import GF.Compile.Extend
 import GF.Compile.Rebuild
 import GF.Compile.Rename
 import GF.Grammar.Refresh
-import GF.Compile.CheckGrammar
-import GF.Compile.Optimize
-import GF.Compile.Evaluate ----
+import GF.Devel.CheckGrammar
+import GF.Devel.Optimize
+--import GF.Compile.Evaluate ----
 import GF.Devel.OptimizeGF
 --import GF.Canon.Share
 --import GF.Canon.Subexpressions (elimSubtermsMod,unSubelimModule)
@@ -166,7 +166,7 @@ compileSourceModule opts env@(k,gr) mo@(i,mi) = do
       (k',mo3r:_) <- putpp "  refreshing " $ ioeErr $ refreshModule (k,mos) mo3
       intermOut opts (iOpt "show_refresh") (prMod mo3r)
 
-      let eenv = emptyEEnv
+      let eenv = () --- emptyEEnv
       (mo4,eenv') <- 
         ---- if oElem "check_only" opts 
           putpp "  optimizing " $ ioeErr $ optimizeModule opts (mos,eenv) mo3r
diff --git a/src/GF/Devel/Compute.hs b/src/GF/Devel/Compute.hs
new file mode 100644
index 000000000..61efbd5c2
--- /dev/null
+++ b/src/GF/Devel/Compute.hs
@@ -0,0 +1,395 @@
+----------------------------------------------------------------------
+-- |
+-- Module      : Compute
+-- Maintainer  : AR
+-- Stability   : (stable)
+-- Portability : (portable)
+--
+-- > CVS $Date: 2005/11/01 15:39:12 $ 
+-- > CVS $Author: aarne $
+-- > CVS $Revision: 1.19 $
+--
+-- Computation of source terms. Used in compilation and in @cc@ command.
+-----------------------------------------------------------------------------
+
+module GF.Devel.Compute (computeConcrete, computeTerm,computeConcreteRec) where
+
+import GF.Data.Operations
+import GF.Grammar.Grammar
+import GF.Infra.Ident
+import GF.Infra.Option
+import GF.Data.Str
+import GF.Grammar.PrGrammar
+import GF.Infra.Modules
+import GF.Grammar.Macros
+import GF.Grammar.Lookup
+import GF.Grammar.Refresh
+import GF.Grammar.PatternMatch
+import GF.Grammar.Lockfield (isLockLabel) ----
+
+import GF.Grammar.AppPredefined
+
+import Data.List (nub,intersperse)
+import Control.Monad (liftM2, liftM)
+
+-- | computation of concrete syntax terms into normal form
+-- used mainly for partial evaluation
+computeConcrete :: SourceGrammar -> Term -> Err Term
+computeConcrete    g t = {- refreshTerm t >>= -} computeTerm g [] t
+computeConcreteRec g t = {- refreshTerm t >>= -} computeTermOpt True g [] t
+
+computeTerm :: SourceGrammar -> Substitution -> Term -> Err Term
+computeTerm = computeTermOpt False
+
+-- rec=True is used if it cannot be assumed that looked-up constants
+-- have already been computed (mainly with -optimize=noexpand in .gfr)
+
+computeTermOpt :: Bool -> SourceGrammar -> Substitution -> Term -> Err Term
+computeTermOpt rec gr = comp where
+
+   comp g t = ---- errIn ("subterm" +++ prt t) $ --- for debugging 
+              case t of
+
+     Q (IC "Predef") _ -> return t
+     Q p c -> look p c 
+
+     -- if computed do nothing
+     Computed t' -> return $ unComputed t'
+
+     Vr x -> do
+       t' <- maybe (prtBad ("no value given to variable") x) return $ lookup x g
+       case t' of 
+         _ | t == t' -> return t
+         _ -> comp g t'
+
+     Abs x b -> do 
+       b' <- comp (ext x (Vr x) g) b
+       return $ Abs x b'
+
+     Let (x,(_,a)) b -> do
+       a' <- comp g a
+       comp (ext x a' g) b
+
+     Prod x a b -> do
+       a' <- comp g a
+       b' <- comp (ext x (Vr x) g) b
+       return $ Prod x a' b'
+
+     -- beta-convert
+     App f a -> do
+       f' <- comp g f
+       a' <- comp g a
+       case (f',a') of
+         (Abs x b, FV as) -> 
+           mapM (\c -> comp (ext x c g) b) as >>= return . variants
+         (_, FV as)  -> mapM (\c -> comp g (App f' c)) as >>= return . variants
+         (FV fs, _)  -> mapM (\c -> comp g (App c a')) fs >>= return . variants
+         (Abs x b,_) -> comp (ext x a' g) b
+         (QC _ _,_)  -> returnC $ App f' a'
+
+         (Alias _ _ d, _) -> comp g (App d a')
+
+         (S (T i cs) e,_) -> prawitz g i (flip App a') cs e
+         (S (V i cs) e,_) -> prawitzV g i (flip App a') cs e
+
+	 _ -> do
+           (t',b) <- appPredefined (App f' a')
+           if b then return t' else comp g t'
+
+     P t l | isLockLabel l -> return $ R [] 
+     ---- a workaround 18/2/2005: take this away and find the reason
+     ---- why earlier compilation destroys the lock field
+
+
+     P t l  -> do
+       t' <- comp g t
+       case t' of
+         FV rs -> mapM (\c -> comp g (P c l)) rs >>= returnC . variants
+         R r   -> maybe (prtBad "no value for label" l) (comp g . snd) $ 
+                    lookup l $ reverse r 
+
+         ExtR a (R b) ->                 
+           case comp g (P (R b) l) of
+             Ok v -> return v
+             _ -> comp g (P a l)
+
+--- { - --- this is incorrect, since b can contain the proper value
+         ExtR (R a) b ->                 -- NOT POSSIBLE both a and b records!
+           case comp g (P (R a) l) of
+             Ok v -> return v
+             _ -> comp g (P b l)
+--- - } ---
+
+         Alias _ _ r -> comp g (P r l)
+
+         S (T i cs) e -> prawitz g i (flip P l) cs e
+         S (V i cs) e -> prawitzV g i (flip P l) cs e
+
+         _   -> returnC $ P t' l
+
+     PI t l i -> comp g $ P t l -----
+
+     S t@(T ti cc) v -> do
+       v'     <- comp g v
+       case v' of
+         FV vs -> do
+           ts' <- mapM (comp g . S t) vs
+           return $ variants ts' 
+         _ -> case ti of
+{-
+           TComp _  -> do
+             case term2patt v' of
+               Ok p' -> case lookup p' cc of
+                 Just u -> comp g u
+                 _ -> do
+                   t' <- comp g t
+                   return $ S t' v' -- if v' is not canonical
+               _ -> do
+                  t' <- comp g t
+                  return $ S t' v'
+-}
+           _ -> case matchPattern cc v' of
+             Ok (c,g') -> comp (g' ++ g) c
+             _ | isCan v' -> prtBad ("missing case" +++ prt v' +++ "in") t 
+             _ -> do
+               t' <- comp g t
+               return $ S t' v' -- if v' is not canonical
+
+
+     S t v -> do
+
+      t'     <- case t of
+---- why not? ResFin.Agr "has no values"
+----        T (TComp _) _ -> return t
+----        V _ _ -> return t
+        _ -> comp g t
+
+      v'     <- comp g v
+
+      case v' of
+       FV vs -> mapM (\c -> comp g (S t' c)) vs >>= returnC . variants        
+       _ -> case t' of
+         FV ccs -> mapM (\c -> comp g (S c v')) ccs >>= returnC . variants
+
+         T _ [(PV IW,c)] -> comp g c           --- an optimization
+         T _ [(PT _ (PV IW),c)] -> comp g c
+
+         T _ [(PV z,c)] -> comp (ext z v' g) c --- another optimization
+         T _ [(PT _ (PV z),c)] -> comp (ext z v' g) c
+
+         -- course-of-values table: look up by index, no pattern matching needed
+         V ptyp ts -> do
+           vs <- allParamValues gr ptyp
+           case lookup v' (zip vs [0 .. length vs - 1]) of
+             Just i -> comp g $ ts !! i
+-----             _ -> prtBad "selection" $ S t' v' -- debug
+             _ -> return $ S t' v' -- if v' is not canonical
+
+         T (TComp _) cs -> do
+           case term2patt v' of
+             Ok p' -> case lookup p' cs of
+               Just u -> comp g u
+               _ -> return $ S t' v' -- if v' is not canonical
+             _ -> return $ S t' v'
+
+         T _ cc -> case matchPattern cc v' of
+             Ok (c,g') -> comp (g' ++ g) c
+             _ | isCan v' -> prtBad ("missing case" +++ prt v' +++ "in") t 
+             _ -> return $ S t' v' -- if v' is not canonical
+
+         Alias _ _ d -> comp g (S d v')
+
+         S (T i cs) e -> prawitz g i (flip S v') cs e
+         S (V i cs) e -> prawitzV g i (flip S v') cs e
+         _    -> returnC $ S t' v'
+
+     -- normalize away empty tokens
+     K "" -> return Empty
+
+     -- glue if you can
+     Glue x0 y0 -> do
+       x <- comp g x0
+       y <- comp g y0
+       case (x,y) of
+         (FV ks,_)         -> do
+           kys <- mapM (comp g . flip Glue y) ks
+           return $ variants kys
+         (_,FV ks)         -> do
+           xks <- mapM (comp g . Glue x) ks
+           return $ variants xks
+
+         (Alias _ _ d, y)  -> comp g $ Glue d y
+         (x, Alias _ _ d)  -> comp g $ Glue x d
+
+         (S (T i cs) e, s) -> prawitz g i (flip Glue s) cs e
+         (s, S (T i cs) e) -> prawitz g i (Glue s) cs e
+         (S (V i cs) e, s) -> prawitzV g i (flip Glue s) cs e
+         (s, S (V i cs) e) -> prawitzV g i (Glue s) cs e
+         (_,Empty)         -> return x
+         (Empty,_)         -> return y
+         (K a, K b)        -> return $ K (a ++ b)
+         (_, Alts (d,vs)) -> do
+----         (K a, Alts (d,vs)) -> do
+            let glx = Glue x
+            comp g $ Alts (glx d, [(glx v,c) | (v,c) <- vs])
+         (Alts _, ka) -> checks [do
+            y' <- strsFromTerm ka
+----         (Alts _, K a) -> checks [do
+            x' <- strsFromTerm x -- this may fail when compiling opers
+            return $ variants [
+              foldr1 C (map K (str2strings (glueStr v u))) | v <- x', u <- y']
+----              foldr1 C (map K (str2strings (glueStr v (str a)))) | v <- x']
+           ,return $ Glue x y
+           ]
+         (C u v,_) -> comp g $ C u (Glue v y)
+
+         _ -> do
+           mapM_ checkNoArgVars [x,y]
+           r <- composOp (comp g) t
+           returnC r
+
+     Alts _ -> do
+       r <- composOp (comp g) t
+       returnC r
+
+     -- remove empty
+     C a b    -> do
+       a' <- comp g a
+       b' <- comp g b
+       case (a',b') of
+         (Alts _, K a) -> checks [do
+            as <- strsFromTerm a' -- this may fail when compiling opers
+            return $ variants [
+              foldr1 C (map K (str2strings (plusStr v (str a)))) | v <- as]
+            ,
+            return $ C a' b'
+           ]
+         (Empty,_) -> returnC b'
+         (_,Empty) -> returnC a'
+         _     -> returnC $ C a' b'
+
+     -- reduce free variation as much as you can
+     FV ts -> mapM (comp g) ts >>= returnC . variants
+
+     -- merge record extensions if you can
+     ExtR r s -> do
+       r' <- comp g r
+       s' <- comp g s
+       case (r',s') of
+         (Alias _ _ d, _)  -> comp g $ ExtR d s'
+         (_, Alias _ _ d)  -> comp g $ Glue r' d
+
+         (R rs, R ss) -> plusRecord r' s'
+         (RecType rs, RecType ss) -> plusRecType r' s'
+         _ -> return $ ExtR r' s'
+
+     -- case-expand tables
+     -- if already expanded, don't expand again
+     T i@(TComp ty) cs -> do
+       -- if there are no variables, don't even go inside
+       cs' <- if (null g) then return cs else mapPairsM (comp g) cs
+----       return $ V ty (map snd cs')
+       return $ T i cs'
+     --- this means some extra work; should implement TSh directly
+     TSh i cs -> comp g $ T i [(p,v) | (ps,v) <- cs, p <- ps] --- OBSOLETE
+
+     T i cs -> do
+       pty0 <- getTableType i
+       ptyp <- comp g pty0
+       case allParamValues gr ptyp of
+         Ok vs -> do
+
+           cs'  <- mapM (compBranchOpt g) cs  ---- why is this needed??
+           sts  <- mapM (matchPattern cs') vs 
+           ts   <- mapM (\ (c,g') -> comp (g' ++ g) c) sts
+           ps   <- mapM term2patt vs
+           let ps' = ps --- PT ptyp (head ps) : tail ps
+----           return $ V ptyp ts -- to save space ---- why doesn't this work??
+           return $ T (TComp ptyp) (zip ps' ts)
+         _ -> do
+           cs' <- mapM (compBranch g) cs
+           return $ T i cs'  -- happens with variable types
+
+     Alias c a d -> do --- OBSOLETE
+       d' <- comp g d
+       return $ Alias c a d'  -- alias only disappears in certain redexes
+
+     -- otherwise go ahead
+     _ -> composOp (comp g) t >>= returnC
+
+    where
+
+     look p c
+       | rec       = lookupResDef gr p c >>= comp []
+       | otherwise = lookupResDef gr p c
+
+{-
+     look p c = case lookupResDefKind gr p c of
+       Ok (t,_) | noExpand p || rec -> comp [] t
+       Ok (t,_) -> return t
+       Bad s -> raise s
+
+     noExpand p = errVal False $ do
+       mo <- lookupModMod gr p
+       return $ case getOptVal (iOpts (flags mo)) useOptimizer of
+         Just "noexpand" -> True
+         _ -> False
+-}
+
+     ext x a g = (x,a):g
+
+     returnC = return --- . computed
+
+     variants ts = case nub ts of
+       [t] -> t
+       ts  -> FV ts
+
+     isCan v = case v of
+       Con _    -> True
+       QC _ _   -> True
+       App f a  -> isCan f && isCan a
+       R rs     -> all (isCan . snd . snd) rs
+       _        -> False
+
+     compBranch g (p,v) = do
+       let g' = contP p ++ g
+       v' <- comp g' v
+       return (p,v')
+
+     compBranchOpt g c@(p,v) = case contP p of
+       [] -> return c
+       _ -> err (const (return c)) return $ compBranch g c
+
+     contP p = case p of
+       PV x -> [(x,Vr x)]
+       PC _ ps -> concatMap contP ps
+       PP _ _ ps -> concatMap contP ps
+       PT _ p -> contP p
+       PR rs -> concatMap (contP . snd) rs
+
+       PAs x p -> (x,Vr x) : contP p
+
+       PSeq p q -> concatMap contP [p,q]
+       PAlt p q -> concatMap contP [p,q]
+       PRep p   -> contP p
+       PNeg p   -> contP p
+
+       _ -> []
+
+     prawitz g i f cs e = do
+       cs' <- mapM (compBranch g) [(p, f v) | (p,v) <- cs]
+       return $ S (T i cs') e
+     prawitzV g i f cs e = do
+       cs' <- mapM (comp g) [(f v) | v <- cs]
+       return $ S (V i cs') e
+
+-- | argument variables cannot be glued
+checkNoArgVars :: Term -> Err Term
+checkNoArgVars t = case t of
+  Vr (IA _)  -> Bad $ glueErrorMsg $ prt t 
+  Vr (IAV _) -> Bad $ glueErrorMsg $ prt t 
+  _ -> composOp checkNoArgVars t
+
+glueErrorMsg s = 
+  "Cannot glue (+) term with run-time variable" +++ s ++ "." ++++
+  "Use Prelude.bind instead."
diff --git a/src/GF/Devel/GrammarToGFCC.hs b/src/GF/Devel/GrammarToGFCC.hs
index 647e4ae65..eabc07375 100644
--- a/src/GF/Devel/GrammarToGFCC.hs
+++ b/src/GF/Devel/GrammarToGFCC.hs
@@ -10,7 +10,7 @@ import qualified GF.GFCC.AbsGFCC as C
 import qualified GF.GFCC.DataGFCC as D
 import qualified GF.Grammar.Abstract as A
 import qualified GF.Grammar.Macros as GM
-import qualified GF.Grammar.Compute as Compute
+--import qualified GF.Grammar.Compute as Compute
 import qualified GF.Infra.Modules as M
 import qualified GF.Infra.Option as O
 
diff --git a/src/GF/Devel/Optimize.hs b/src/GF/Devel/Optimize.hs
new file mode 100644
index 000000000..4621e8f6c
--- /dev/null
+++ b/src/GF/Devel/Optimize.hs
@@ -0,0 +1,298 @@
+----------------------------------------------------------------------
+-- |
+-- Module      : Optimize
+-- Maintainer  : AR
+-- Stability   : (stable)
+-- Portability : (portable)
+--
+-- > CVS $Date: 2005/09/16 13:56:13 $ 
+-- > CVS $Author: aarne $
+-- > CVS $Revision: 1.18 $
+--
+-- Top-level partial evaluation for GF source modules.
+-----------------------------------------------------------------------------
+
+module GF.Devel.Optimize (optimizeModule) where
+
+import GF.Grammar.Grammar
+import GF.Infra.Ident
+import GF.Infra.Modules
+import GF.Grammar.PrGrammar
+import GF.Grammar.Macros
+import GF.Grammar.Lookup
+import GF.Grammar.Refresh
+import GF.Devel.Compute
+import GF.Compile.BackOpt
+import GF.Devel.CheckGrammar
+import GF.Compile.Update
+--import GF.Compile.Evaluate
+
+import GF.Data.Operations
+import GF.Infra.CheckM
+import GF.Infra.Option
+
+import Control.Monad
+import Data.List
+
+import Debug.Trace
+
+
+-- conditional trace
+
+prtIf :: (Print a) => Bool -> a -> a
+prtIf b t = if b then trace (" " ++ prt t) t else t
+
+-- experimental evaluation, option to import
+oEval = iOpt "eval"
+
+-- | partial evaluation of concrete syntax. AR 6\/2001 -- 16\/5\/2003 -- 5\/2\/2005.
+
+type EEnv = () --- not used
+
+-- only do this for resource: concrete is optimized in gfc form
+optimizeModule :: Options -> ([(Ident,SourceModInfo)],EEnv) -> 
+                  (Ident,SourceModInfo) -> Err ((Ident,SourceModInfo),EEnv)
+optimizeModule opts mse@(ms,eenv) mo@(_,mi) = case mi of
+  ModMod m0@(Module mt st fs me ops js) | 
+    st == MSComplete && isModRes m0 && not (oElem oEval oopts)-> do
+      (mo1,_) <- evalModule oopts mse mo
+      let 
+       mo2 = case optim of
+        "parametrize" -> shareModule paramOpt mo1  -- parametrization and sharing
+        "values"      -> shareModule valOpt mo1    -- tables as courses-of-values
+        "share"       -> shareModule shareOpt mo1  -- sharing of branches
+        "all"         -> shareModule allOpt mo1    -- first parametrize then values
+        "none"        -> mo1                       -- no optimization
+        _             -> mo1                       -- none; default for src
+      return (mo2,eenv)
+  _ -> evalModule oopts mse mo
+ where
+   oopts = addOptions opts (iOpts (flagsModule mo))
+   optim = maybe "all" id $ getOptVal oopts useOptimizer
+
+evalModule :: Options -> ([(Ident,SourceModInfo)],EEnv) -> (Ident,SourceModInfo) -> 
+               Err ((Ident,SourceModInfo),EEnv)
+evalModule oopts (ms,eenv) mo@(name,mod) = case mod of
+
+  ModMod m0@(Module mt st fs me ops js) | st == MSComplete -> case mt of
+    _ | isModRes m0 && not (oElem oEval oopts) -> do
+      let deps = allOperDependencies name js
+      ids <- topoSortOpers deps
+      MGrammar (mod' : _) <- foldM evalOp gr ids
+      return $ (mod',eenv)
+
+    MTConcrete a -> do
+      js' <- mapMTree (evalCncInfo oopts gr name a) js ---- <- gr0 6/12/2005
+      return $ ((name, ModMod (Module mt st fs me ops js')),eenv)
+
+    _ -> return $ ((name,mod),eenv)
+  _ -> return $ ((name,mod),eenv)
+ where
+   gr0 = MGrammar $ ms
+   gr  = MGrammar $ (name,mod) : ms
+
+   evalOp g@(MGrammar ((_, ModMod m) : _)) i = do
+     info  <- lookupTree prt i $ jments m
+     info' <- evalResInfo oopts gr (i,info)
+     return $ updateRes g name i info'
+
+-- | only operations need be compiled in a resource, and this is local to each
+-- definition since the module is traversed in topological order
+evalResInfo :: Options -> SourceGrammar -> (Ident,Info) -> Err Info
+evalResInfo oopts gr (c,info) = case info of
+
+  ResOper pty pde -> eIn "operation" $ do
+    pde' <- case pde of
+       Yes de | optres -> liftM yes $ comp de 
+       _ -> return pde
+    return $ ResOper pty pde'
+
+  _ ->  return info
+ where
+   comp = if optres then computeConcrete gr else computeConcreteRec gr
+   eIn cat = errIn ("Error optimizing" +++ cat +++ prt c +++ ":")
+   optim = maybe "all" id $ getOptVal oopts useOptimizer
+   optres = case optim of
+     "noexpand" -> False
+     _ -> True
+
+
+evalCncInfo :: 
+  Options -> SourceGrammar -> Ident -> Ident -> (Ident,Info) -> Err (Ident,Info)
+evalCncInfo opts gr cnc abs (c,info) = do
+
+ seq (prtIf (oElem beVerbose opts) c) $ return ()
+
+ errIn ("optimizing" +++ prt c) $ case info of
+
+  CncCat ptyp pde ppr -> do
+    pde' <- case (ptyp,pde) of
+      (Yes typ, Yes de) -> 
+        liftM yes $ pEval ([(strVar, typeStr)], typ) de
+      (Yes typ, Nope)   -> 
+        liftM yes $ mkLinDefault gr typ >>= partEval noOptions gr ([(strVar, typeStr)],typ)
+      (May b, Nope) ->
+        return $ May b
+      _ -> return pde   -- indirection
+
+    ppr' <- liftM yes $ evalPrintname gr c ppr (yes $ K $ prt c)
+
+    return (c, CncCat ptyp pde' ppr')
+
+  CncFun (mt@(Just (_,ty@(cont,val)))) pde ppr -> 
+       eIn ("linearization in type" +++ prt (mkProd (cont,val,[])) ++++ "of function") $ do
+    pde' <- case pde of
+      Yes de | notNewEval -> do
+        liftM yes $ pEval ty de
+
+      _ -> return pde
+    ppr' <-  liftM yes $ evalPrintname gr c ppr pde'
+    return $ (c, CncFun mt pde' ppr') -- only cat in type actually needed
+
+  _ ->  return (c,info)
+ where
+   pEval = partEval opts gr
+   eIn cat = errIn ("Error optimizing" +++ cat +++ prt c +++ ":")
+   notNewEval = not (oElem oEval opts)
+
+-- | the main function for compiling linearizations
+partEval :: Options -> SourceGrammar -> (Context,Type) -> Term -> Err Term
+partEval opts gr (context, val) trm = errIn ("parteval" +++ prt_ trm) $ do
+  let vars  = map fst context
+      args  = map Vr vars
+      subst = [(v, Vr v) | v <- vars]
+      trm1  = mkApp trm args
+  trm3 <- if globalTable 
+             then etaExpand subst trm1 >>= outCase subst
+             else etaExpand subst trm1
+  return $ mkAbs vars trm3
+
+ where 
+
+   globalTable = oElem showAll opts --- i -all
+
+   comp g t = {- refreshTerm t >>= -} computeTerm gr g t
+
+   etaExpand su t = do
+     t' <- comp su t 
+     case t' of
+       R _ | rightType t' -> comp su t' --- return t' wo noexpand...
+       _ -> recordExpand val t' >>= comp su
+   -- don't eta expand records of right length (correct by type checking)
+   rightType t = case (t,val) of
+     (R rs, RecType ts) -> length rs == length ts
+     _ -> False
+
+   outCase subst t = do
+     pts <- getParams context
+     let (args,ptyps) = unzip $ filter (flip occur t . fst) pts
+     if null args 
+       then return t 
+       else do 
+         let argtyp = RecType $ tuple2recordType ptyps
+         let pvars = map (Vr . zIdent . prt) args -- gets eliminated
+         patt <- term2patt $ R $ tuple2record $ pvars
+         let t' = replace (zip args pvars) t
+         t1 <- comp subst $ T (TTyped argtyp) [(patt, t')]
+         return $ S t1 $ R $ tuple2record args
+
+   --- notice: this assumes that all lin types follow the "old JFP style" 
+   getParams = liftM concat . mapM getParam 
+   getParam (argv,RecType rs) = return 
+     [(P (Vr argv) lab, ptyp) | (lab,ptyp) <- rs,  not (isLinLabel lab)] 
+   ---getParam (_,ty) | ty==typeStr = return [] --- in lindef 
+   getParam (av,ty) = 
+     Bad ("record type expected not" +++ prt ty +++ "for" +++ prt av) 
+     --- all lin types are rec types
+
+   replace :: [(Term,Term)] -> Term -> Term
+   replace reps trm = case trm of  
+     -- this is the important case
+     P _ _ -> maybe trm id $ lookup trm reps
+     _ -> composSafeOp (replace reps) trm
+
+   occur t trm = case trm of
+
+     -- this is the important case
+     P _ _   -> t == trm
+     S x y   -> occur t y || occur t x
+     App f x -> occur t x || occur t f
+     Abs _ f -> occur t f
+     R rs    -> any (occur t) (map (snd . snd) rs)
+     T _ cs  -> any (occur t) (map snd cs)
+     C x y   -> occur t x || occur t y
+     Glue x y -> occur t x || occur t y
+     ExtR x y -> occur t x || occur t y
+     FV ts   -> any (occur t) ts
+     V _ ts   -> any (occur t) ts
+     Let (_,(_,x)) y -> occur t x || occur t y
+     _ -> False
+
+
+-- here we must be careful not to reduce
+--   variants {{s = "Auto" ; g = N} ; {s = "Wagen" ; g = M}}
+--   {s  = variants {"Auto" ; "Wagen"} ; g  = variants {N ; M}} ;
+
+recordExpand :: Type -> Term -> Err Term
+recordExpand typ trm = case unComputed typ of
+  RecType tys -> case trm of
+    FV rs -> return $ FV [R [assign lab (P r lab) | (lab,_) <- tys] | r <- rs]
+    _ -> return $ R [assign lab (P trm lab) | (lab,_) <- tys]
+  _ -> return trm
+
+
+-- | auxiliaries for compiling the resource
+
+mkLinDefault :: SourceGrammar -> Type -> Err Term
+mkLinDefault gr typ = do
+  case unComputed typ of
+    RecType lts -> mapPairsM mkDefField lts >>= (return . Abs strVar . R . mkAssign)
+    _ -> prtBad "linearization type must be a record type, not" typ
+ where
+   mkDefField typ = case unComputed typ of
+     Table p t  -> do
+       t' <- mkDefField t
+       let T _ cs = mkWildCases t'
+       return $ T (TWild p) cs 
+     Sort "Str" -> return $ Vr strVar
+     QC q p     -> lookupFirstTag gr q p
+     RecType r  -> do
+       let (ls,ts) = unzip r
+       ts' <- mapM mkDefField ts
+       return $ R $ [assign l t | (l,t) <- zip ls ts']
+     _ | isTypeInts typ -> return $ EInt 0 -- exists in all as first val
+     _ -> prtBad "linearization type field cannot be" typ
+
+-- | Form the printname: if given, compute. If not, use the computed
+-- lin for functions, cat name for cats (dispatch made in evalCncDef above).
+--- We cannot use linearization at this stage, since we do not know the
+--- defaults we would need for question marks - and we're not yet in canon.
+evalPrintname :: SourceGrammar -> Ident -> MPr -> Perh Term -> Err Term
+evalPrintname gr c ppr lin =
+  case ppr of
+    Yes pr -> comp pr
+    _ -> case lin of
+      Yes t -> return $ K $ clean $ prt $ oneBranch t ---- stringFromTerm
+      _ -> return $ K $ prt c ----
+ where
+   comp = computeConcrete gr
+
+   oneBranch t = case t of
+     Abs _ b   -> oneBranch b
+     R   (r:_) -> oneBranch $ snd $ snd r
+     T _ (c:_) -> oneBranch $ snd c
+     V _ (c:_) -> oneBranch c
+     FV  (t:_) -> oneBranch t
+     C x y     -> C (oneBranch x) (oneBranch y)
+     S x _     -> oneBranch x
+     P x _     -> oneBranch x
+     Alts (d,_) -> oneBranch d
+     _ -> t
+
+  --- very unclean cleaner
+   clean s = case s of
+     '+':'+':' ':cs -> clean cs
+     '"':cs -> clean cs
+     c:cs -> c: clean cs
+     _ -> s
+
diff --git a/src/GF/Devel/OptimizeGF.hs b/src/GF/Devel/OptimizeGF.hs
index de05ed428..99e33941f 100644
--- a/src/GF/Devel/OptimizeGF.hs
+++ b/src/GF/Devel/OptimizeGF.hs
@@ -116,7 +116,9 @@ values :: Term -> Term
 values t = case t of
   T ty [(ps,t)]    -> T ty [(ps,values t)] -- don't destroy parametrization
   T (TComp ty)  cs -> V ty [values t | (_, t) <- cs]
-  T (TTyped ty) cs -> V ty [values t | (_, t) <- cs] ---- why are these left?
+  T (TTyped ty) cs -> V ty [values t | (_, t) <- cs] 
+        ---- why are these left?
+        ---- printing with GrammarToSource does not preserve the distinction
   _ -> C.composSafeOp values t
 
 
diff --git a/src/GF/Devel/TC.hs b/src/GF/Devel/TC.hs
new file mode 100644
index 000000000..5c439f671
--- /dev/null
+++ b/src/GF/Devel/TC.hs
@@ -0,0 +1,299 @@
+----------------------------------------------------------------------
+-- |
+-- Module      : TC
+-- Maintainer  : AR
+-- Stability   : (stable)
+-- Portability : (portable)
+--
+-- > CVS $Date: 2005/10/02 20:50:19 $ 
+-- > CVS $Author: aarne $
+-- > CVS $Revision: 1.11 $
+--
+-- Thierry Coquand's type checking algorithm that creates a trace
+-----------------------------------------------------------------------------
+
+module GF.Devel.TC (AExp(..),
+	   Theory,
+	   checkExp,
+	   inferExp,
+           checkEqs,
+	   eqVal,
+	   whnf
+	  ) where
+
+import GF.Data.Operations
+import GF.Grammar.Abstract
+import GF.Devel.AbsCompute
+
+import Control.Monad
+import Data.List (sortBy)
+
+data AExp =
+     AVr   Ident Val 
+   | ACn   QIdent Val
+   | AType 
+   | AInt  Integer 
+   | AFloat Double
+   | AStr  String
+   | AMeta MetaSymb Val
+   | AApp  AExp AExp Val 
+   | AAbs  Ident Val AExp 
+   | AProd Ident AExp AExp 
+   | AEqs  [([Exp],AExp)] --- not used
+   | AData Val
+  deriving (Eq,Show)
+
+type Theory = QIdent -> Err Val
+
+lookupConst :: Theory -> QIdent -> Err Val
+lookupConst th f = th f
+
+lookupVar :: Env -> Ident -> Err Val
+lookupVar g x = maybe (prtBad "unknown variable" x) return $ lookup x ((IW,uVal):g)
+-- wild card IW: no error produced, ?0 instead.
+
+type TCEnv = (Int,Env,Env)
+
+emptyTCEnv :: TCEnv
+emptyTCEnv = (0,[],[])
+
+whnf :: Val -> Err Val
+whnf v = ---- errIn ("whnf" +++ prt v) $ ---- debug
+         case v of
+  VApp u w -> do
+    u' <- whnf u 
+    w' <- whnf w
+    app u' w'
+  VClos env e -> eval env e
+  _ -> return v
+
+app :: Val -> Val -> Err Val
+app u v = case u of
+  VClos env (Abs x e) -> eval ((x,v):env) e
+  _ -> return $ VApp u v
+  
+eval :: Env -> Exp -> Err Val
+eval env e = ---- errIn ("eval" +++ prt e +++ "in" +++ prEnv env) $ 
+             case e of
+  Vr x    -> lookupVar env x
+  Q m c   -> return $ VCn (m,c)
+  QC m c  -> return $ VCn (m,c) ---- == Q ?
+  Sort c  -> return $ VType --- the only sort is Type
+  App f a -> join $ liftM2 app (eval env f) (eval env a)
+  _ -> return $ VClos env e
+
+eqVal :: Int -> Val -> Val -> Err [(Val,Val)]
+eqVal k u1 u2 = ---- errIn (prt u1 +++ "<>" +++ prBracket (show k) +++ prt u2) $ 
+                do
+  w1 <- whnf u1
+  w2 <- whnf u2 
+  let v = VGen k
+  case (w1,w2) of
+    (VApp f1 a1, VApp f2 a2) -> liftM2 (++) (eqVal k f1 f2) (eqVal k a1 a2)
+    (VClos env1 (Abs x1 e1), VClos env2 (Abs x2 e2)) ->
+      eqVal (k+1) (VClos ((x1,v x1):env1) e1) (VClos ((x2,v x1):env2) e2)
+    (VClos env1 (Prod x1 a1 e1), VClos env2 (Prod x2 a2 e2)) ->
+      liftM2 (++) 
+        (eqVal k     (VClos env1          a1) (VClos env2          a2))
+        (eqVal (k+1) (VClos ((x1,v x1):env1) e1) (VClos ((x2,v x1):env2) e2))
+    (VGen i _, VGen j _) -> return [(w1,w2) | i /= j]
+    (VCn (_, i), VCn (_,j)) -> return [(w1,w2) | i /= j] 
+    --- thus ignore qualifications; valid because inheritance cannot
+    --- be qualified. Simplifies annotation. AR 17/3/2005 
+    _ -> return [(w1,w2) | w1 /= w2]
+-- invariant: constraints are in whnf
+
+checkType :: Theory -> TCEnv -> Exp -> Err (AExp,[(Val,Val)])
+checkType th tenv e = checkExp th tenv e vType
+
+checkExp :: Theory -> TCEnv -> Exp -> Val -> Err (AExp, [(Val,Val)])
+checkExp th tenv@(k,rho,gamma) e ty = do
+  typ <- whnf ty
+  let v = VGen k
+  case e of
+    Meta m -> return $ (AMeta m typ,[])
+    EData -> return $ (AData typ,[])
+
+    Abs x t -> case typ of
+      VClos env (Prod y a b) -> do
+	a' <- whnf $ VClos env a ---
+	(t',cs) <- checkExp th 
+                           (k+1,(x,v x):rho, (x,a'):gamma) t (VClos ((y,v x):env) b)
+	return (AAbs x a' t', cs)
+      _ -> prtBad ("function type expected for" +++ prt e +++ "instead of") typ
+
+-- {- --- to get deprec when checkEqs works (15/9/2005)
+    Eqs es -> do
+      bcs <- mapM (\b -> checkBranch th tenv b typ) es
+      let (bs,css) = unzip bcs
+      return (AEqs bs, concat css) 
+-- - }
+    Prod x a b -> do
+      testErr (typ == vType) "expected Type"
+      (a',csa) <- checkType th tenv a
+      (b',csb) <- checkType th (k+1, (x,v x):rho, (x,VClos rho a):gamma) b
+      return (AProd x a' b', csa ++ csb)
+
+    _ -> checkInferExp th tenv e typ
+
+checkInferExp :: Theory -> TCEnv -> Exp -> Val -> Err (AExp, [(Val,Val)])
+checkInferExp th tenv@(k,_,_) e typ = do
+  (e',w,cs1) <- inferExp th tenv e
+  cs2 <- eqVal k w typ
+  return (e',cs1 ++ cs2)
+      
+inferExp :: Theory -> TCEnv -> Exp -> Err (AExp, Val, [(Val,Val)])
+inferExp th tenv@(k,rho,gamma) e = case e of
+   Vr x -> mkAnnot (AVr x) $ noConstr $ lookupVar gamma x
+   Q m c 
+    | m == cPredefAbs && (elem c (map identC ["Int","String","Float"])) ->
+                                       return (ACn (m,c) vType, vType, [])
+    | otherwise -> mkAnnot (ACn (m,c)) $ noConstr $ lookupConst th (m,c)
+   QC m c -> mkAnnot (ACn (m,c)) $ noConstr $ lookupConst th (m,c) ----
+   EInt i -> return (AInt i, valAbsInt, [])
+   EFloat i -> return (AFloat i, valAbsFloat, [])
+   K i -> return (AStr i, valAbsString, [])
+   Sort _ -> return (AType, vType, [])
+   App f t -> do
+    (f',w,csf) <- inferExp th tenv f 
+    typ <- whnf w
+    case typ of
+      VClos env (Prod x a b) -> do
+        (a',csa) <- checkExp th tenv t (VClos env a)
+	b' <- whnf $ VClos ((x,VClos rho t):env) b
+	return $ (AApp f' a' b', b', csf ++ csa)
+      _ -> prtBad ("Prod expected for function" +++ prt f +++ "instead of") typ
+   _ -> prtBad "cannot infer type of expression" e
+ where
+   predefAbs c s = case c of
+     IC "Int" -> return $ const $ Q cPredefAbs cInt
+     IC "Float" -> return $ const $ Q cPredefAbs cFloat
+     IC "String" -> return $ const $ Q cPredefAbs cString
+     _ -> Bad s
+
+checkEqs :: Theory -> TCEnv -> (Fun,Trm) -> Val -> Err [(Val,Val)]
+checkEqs th tenv@(k,rho,gamma) (fun@(m,f),def) val = case def of
+  Eqs es -> liftM concat $ mapM checkBranch es
+  _      -> liftM snd $ checkExp th tenv def val
+ where
+  checkBranch (ps,df) = 
+   let
+      (ps',_,vars) = foldr p2t ([],0,[]) ps
+      fps        = mkApp (Q m f) ps'
+   in errIn ("branch" +++ prt fps) $ do
+    (aexp, typ, cs1) <- inferExp th tenv fps
+    let
+      bds = binds vars aexp 
+      tenv' = (k, rho, bds ++ gamma) 
+    (_,cs2)  <- errIn (show bds) $ checkExp th tenv' df typ
+    return $ (cs1 ++ cs2)
+  p2t p (ps,i,g) = case p of
+     PW      -> (meta (MetaSymb i) : ps, i+1,        g) 
+     PV IW   -> (meta (MetaSymb i) : ps, i+1,        g) 
+     PV x    -> (meta (MetaSymb i) : ps, i+1,upd x i g)
+     PString s -> (            K s : ps, i,          g)
+     PInt n -> (EInt n : ps, i, g)
+     PFloat n -> (EFloat n : ps, i, g)
+     PP m c xs -> (mkApp (qq (m,c)) xss : ps, i', g') 
+                    where (xss,i',g') = foldr p2t ([],i,g) xs
+     _ -> error $ "undefined p2t case" +++ prt p +++ "in checkBranch"
+  upd x i g = (x,i) : g --- to annotate pattern variables: treat as metas
+  
+  -- notice: in vars, the sequence 0.. is sorted. In subst aexp, all
+  -- this occurs and nothing else.
+  binds vars aexp = [(x,v) | ((x,_),v) <- zip vars metas] where
+    metas = map snd $ sortBy (\ (x,_) (y,_) -> compare x y) $ subst aexp
+  subst aexp = case aexp of
+   AMeta (MetaSymb i) v -> [(i,v)]
+   AApp  c a _ -> subst c ++ subst a
+   _ -> [] -- never matter in patterns
+
+checkBranch :: Theory -> TCEnv -> Equation -> Val -> Err (([Exp],AExp),[(Val,Val)])
+checkBranch th tenv b@(ps,t) ty = errIn ("branch" +++ show b) $ 
+                                  chB tenv' ps' ty 
+ where 
+
+  (ps',_,rho2,k') = ps2ts k ps
+  tenv' = (k, rho2++rho, gamma) ---- k' ?
+  (k,rho,gamma) = tenv
+
+  chB tenv@(k,rho,gamma) ps ty = case ps of
+    p:ps2 -> do
+      typ <- whnf ty
+      case typ of
+        VClos env (Prod y a b) -> do
+	  a' <- whnf $ VClos env a
+          (p', sigma, binds, cs1) <- checkP tenv p y a'
+          let tenv' = (length binds, sigma ++ rho, binds ++ gamma)
+          ((ps',exp),cs2) <- chB tenv' ps2 (VClos ((y,p'):env) b)
+	  return ((p:ps',exp), cs1 ++ cs2) -- don't change the patt
+        _ -> prtBad ("Product expected for definiens" +++prt t +++ "instead of") typ
+    [] -> do
+      (e,cs) <- checkExp th tenv t ty
+      return (([],e),cs)
+  checkP env@(k,rho,gamma) t x a = do
+     (delta,cs) <- checkPatt th env t a
+     let sigma = [(x, VGen i x) | ((x,_),i) <- zip delta [k..]]
+     return (VClos sigma t, sigma, delta, cs)
+
+  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)
+     PFloat n -> (EFloat n : ps, i, g, k)
+     PP m c xs -> (mkApp (qq (m,c)) xss : ps, j, g',k') 
+                    where (xss,j,g',k') = foldr p2t ([],i,g,k) xs
+     _ -> error $ "undefined p2t case" +++ prt p +++ "in checkBranch"
+
+  upd x k g = (x, VGen k x) : g --- hack to recognize pattern variables
+
+
+checkPatt :: Theory -> TCEnv -> Exp -> Val -> Err (Binds,[(Val,Val)])
+checkPatt th tenv exp val = do
+  (aexp,_,cs) <- checkExpP tenv exp val
+  let binds = extrBinds aexp
+  return (binds,cs)
+ where
+   extrBinds aexp = case aexp of
+     AVr i v    -> [(i,v)]
+     AApp f a _ -> extrBinds f ++ extrBinds a
+     _ -> [] -- no other cases are possible
+
+--- ad hoc, to find types of variables
+   checkExpP tenv@(k,rho,gamma) exp val = case exp of
+     Meta m -> return $ (AMeta m val, val, [])
+     Vr x   -> return $ (AVr   x val, val, [])
+     EInt i -> return (AInt i, valAbsInt, [])
+     EFloat i -> return (AFloat i, valAbsFloat, [])
+     K s    -> return (AStr s, valAbsString, [])
+
+     Q m c  -> do
+       typ <- lookupConst th (m,c)
+       return $ (ACn (m,c) typ, typ, [])
+     QC m c  -> do
+       typ <- lookupConst th (m,c)
+       return $ (ACn (m,c) typ, typ, []) ----
+     App f t -> do
+       (f',w,csf) <- checkExpP tenv f val
+       typ <- whnf w
+       case typ of
+         VClos env (Prod x a b) -> do
+           (a',_,csa) <- checkExpP tenv t (VClos env a)
+	   b' <- whnf $ VClos ((x,VClos rho t):env) b
+	   return $ (AApp f' a' b', b', csf ++ csa)
+         _ -> prtBad ("Prod expected for function" +++ prt f +++ "instead of") typ
+     _ -> prtBad "cannot typecheck pattern" exp
+
+-- auxiliaries
+
+noConstr :: Err Val -> Err (Val,[(Val,Val)])
+noConstr er = er >>= (\v -> return (v,[]))
+
+mkAnnot :: (Val -> AExp) -> Err (Val,[(Val,Val)]) -> Err (AExp,Val,[(Val,Val)])
+mkAnnot a ti = do
+  (v,cs) <- ti
+  return (a v, v, cs)
+
diff --git a/src/GF/Devel/TypeCheck.hs b/src/GF/Devel/TypeCheck.hs
new file mode 100644
index 000000000..818b48a10
--- /dev/null
+++ b/src/GF/Devel/TypeCheck.hs
@@ -0,0 +1,311 @@
+----------------------------------------------------------------------
+-- |
+-- Module      : TypeCheck
+-- Maintainer  : AR
+-- Stability   : (stable)
+-- Portability : (portable)
+--
+-- > CVS $Date: 2005/09/15 16:22:02 $ 
+-- > CVS $Author: aarne $
+-- > CVS $Revision: 1.16 $
+--
+-- (Description of the module)
+-----------------------------------------------------------------------------
+
+module GF.Devel.TypeCheck (-- * top-level type checking functions; TC should not be called directly.
+		  annotate, annotateIn,
+		  justTypeCheck, checkIfValidExp,
+		  reduceConstraints, 
+		  splitConstraints,
+		  possibleConstraints,
+		  reduceConstraintsNode,
+		  performMetaSubstNode,
+		  -- * some top-level batch-mode checkers for the compiler
+		  justTypeCheckSrc,
+		  grammar2theorySrc,
+		  checkContext,
+		  checkTyp,
+		  checkEquation,
+		  checkConstrs,
+		  editAsTermCommand,
+		  exp2termCommand,
+		  exp2termlistCommand,
+		  tree2termlistCommand
+		 ) where
+
+import GF.Data.Operations
+import GF.Data.Zipper
+
+import GF.Grammar.Abstract
+import GF.Devel.AbsCompute
+import GF.Grammar.Refresh
+import GF.Grammar.LookAbs
+import qualified GF.Grammar.Lookup as Lookup ---
+
+import GF.Devel.TC
+
+import GF.Grammar.Unify ---
+
+import Control.Monad (foldM, liftM, liftM2)
+import Data.List (nub) ---
+
+-- top-level type checking functions; TC should not be called directly.
+
+annotate :: GFCGrammar -> Exp -> Err Tree
+annotate gr exp = annotateIn gr [] exp Nothing 
+
+-- | type check in empty context, return a list of constraints
+justTypeCheck :: GFCGrammar -> Exp -> Val -> Err Constraints
+justTypeCheck gr e v = do
+  (_,constrs0) <- checkExp (grammar2theory gr) (initTCEnv []) e v
+  constrs1     <- reduceConstraints (lookupAbsDef gr) 0 constrs0
+  return $ fst $ splitConstraints gr constrs1
+
+-- | type check in empty context, return the expression itself if valid
+checkIfValidExp :: GFCGrammar -> Exp -> Err Exp
+checkIfValidExp gr e = do
+  (_,_,constrs0) <- inferExp (grammar2theory gr) (initTCEnv []) e
+  constrs1       <- reduceConstraints (lookupAbsDef gr) 0 constrs0
+  ifNull (return e) (Bad  . unwords . prConstrs) constrs1
+
+annotateIn :: GFCGrammar -> Binds -> Exp -> Maybe Val -> Err Tree
+annotateIn gr gamma exp = maybe (infer exp) (check exp) where
+  infer e = do 
+    (a,_,cs) <- inferExp theory env e
+    aexp2treeC (a,cs)
+  check e v = do
+    (a,cs) <- checkExp theory env e v
+    aexp2treeC (a,cs)
+  env = initTCEnv gamma
+  theory = grammar2theory gr 
+  aexp2treeC (a,c) = do
+    c' <- reduceConstraints (lookupAbsDef gr) (length gamma) c
+    aexp2tree (a,c')
+
+-- | invariant way of creating TCEnv from context
+initTCEnv gamma = 
+  (length gamma,[(x,VGen i x) | ((x,_),i) <- zip gamma [0..]], gamma) 
+
+-- | process constraints after eqVal by computing by defs
+reduceConstraints :: LookDef -> Int -> Constraints -> Err Constraints
+reduceConstraints look i = liftM concat . mapM redOne where
+  redOne (u,v) = do
+    u' <- computeVal look u
+    v' <- computeVal look v
+    eqVal i u' v' 
+
+computeVal :: LookDef -> Val -> Err Val
+computeVal look v = case v of
+  VClos g@(_:_) e -> do
+    e' <- compt (map fst g) e          --- bindings of g in e?
+    whnf $ VClos g e'
+{- ----
+  _ -> do            ---- how to compute a Val, really??
+    e  <- val2exp v
+    e' <- compt [] e
+    whnf $ vClos e'
+-}
+  VApp f c -> liftM2 VApp (compv f) (compv c) >>= whnf
+  _ -> whnf v
+ where
+   compt = computeAbsTermIn look
+   compv = computeVal look
+
+-- | take apart constraints that have the form (? <> t), usable as solutions
+splitConstraints :: GFCGrammar -> Constraints -> (Constraints,MetaSubst)
+splitConstraints gr = splitConstraintsGen (lookupAbsDef gr)
+
+splitConstraintsSrc :: Grammar -> Constraints -> (Constraints,MetaSubst)
+splitConstraintsSrc gr = splitConstraintsGen (Lookup.lookupAbsDef gr)
+
+splitConstraintsGen :: LookDef -> Constraints -> (Constraints,MetaSubst)
+splitConstraintsGen look cs = csmsu where
+
+  csmsu       = (nub [(a,b) | (a,b) <- csf1,a /= b],msf1)
+  (csf1,msf1) = unif (csf,msf)  -- alternative: filter first
+  (csf,msf)   = foldr mkOne ([],[]) cs
+
+  csmsf     = foldr mkOne ([],msu) csu
+  (csu,msu) = unif (cs1,[])    -- alternative: unify first
+
+  cs1 = errVal cs $ reduceConstraints look 0 cs
+
+  mkOne (u,v) = case (u,v) of
+    (VClos g (Meta m), v) | null g -> sub m v
+    (v, VClos g (Meta m)) | null g -> sub m v
+    -- do nothing if meta has nonempty closure; null g || isConstVal v WAS WRONG
+    c -> con c
+  con c (cs,ms) = (c:cs,ms)
+  sub m v (cs,ms) = (cs,(m,v):ms)
+
+  unifo = id -- alternative: don't use unification
+
+  unif cm@(cs,ms) = errVal cm $ do --- alternative: use unification  
+    (cs',ms') <- unifyVal cs
+    return (cs', ms' ++ ms)
+
+performMetaSubstNode :: MetaSubst -> TrNode -> TrNode
+performMetaSubstNode subst n@(N (b,a,v,(c,m),s)) = let
+  v' = metaSubstVal v
+  b' = [(x,metaSubstVal v) | (x,v) <- b]
+  c' = [(u',v') | (u,v) <- c, 
+                  let (u',v') = (metaSubstVal u, metaSubstVal v), u' /= v']
+  in N (b',a,v',(c',m),s)
+ where
+   metaSubstVal u = errVal u $ whnf $ case u of
+     VApp  f a -> VApp  (metaSubstVal f) (metaSubstVal a)
+     VClos g e -> VClos [(x,metaSubstVal v) | (x,v) <- g] (metaSubstExp e)
+     _ -> u
+   metaSubstExp e = case e of
+     Meta m -> errVal e $ maybe (return e) val2expSafe $ lookup m subst
+     _ -> composSafeOp metaSubstExp e
+
+reduceConstraintsNode :: GFCGrammar -> TrNode -> TrNode
+reduceConstraintsNode gr = changeConstrs red where
+  red cs = errVal cs $ reduceConstraints (lookupAbsDef gr) 0 cs
+
+-- | weak heuristic to narrow down menus; not used for TC. 15\/11\/2001.
+-- the age-old method from GF 0.9
+possibleConstraints :: GFCGrammar -> Constraints -> Bool
+possibleConstraints gr = and . map (possibleConstraint gr)
+
+possibleConstraint :: GFCGrammar -> (Val,Val) -> Bool
+possibleConstraint gr (u,v) = errVal True $ do
+    u' <- val2exp u >>= compute gr
+    v' <- val2exp v >>= compute gr
+    return $ cts u' v'
+ where
+  cts t u = isUnknown t || isUnknown u || case (t,u) of
+    (Q m c,      Q n d)      -> c == d || notCan (m,c) || notCan (n,d)
+    (QC m c,     QC n d)     -> c == d
+    (App f a,    App g b)    -> cts f g && cts a b
+    (Abs x b,    Abs y c)    -> cts b c
+    (Prod x a f, Prod y b g) -> cts a b && cts f g
+    (_         , _)          -> False
+
+  isUnknown t = case t of
+    Vr _ -> True
+    Meta _ -> True
+    _ -> False
+
+  notCan = not . isPrimitiveFun gr
+
+-- interface to TC type checker
+
+type2val :: Type -> Val
+type2val = VClos []
+
+aexp2tree :: (AExp,[(Val,Val)]) -> Err Tree
+aexp2tree (aexp,cs) = do
+  (bi,at,vt,ts) <- treeForm aexp
+  ts' <- mapM aexp2tree [(t,[]) | t <- ts]
+  return $ Tr (N (bi,at,vt,(cs,[]),False),ts')
+ where
+  treeForm a = case a of
+     AAbs x v b  -> do
+       (bi, at, vt, args) <- treeForm b
+       v' <- whnf v ---- should not be needed...
+       return ((x,v') : bi, at, vt, args)
+     AApp c a v -> do
+       (_,at,_,args) <- treeForm c
+       v' <- whnf v ---- 
+       return ([],at,v',args ++ [a]) 
+     AVr x v -> do
+       v' <- whnf v ---- 
+       return ([],AtV x,v',[])
+     ACn c v -> do
+       v' <- whnf v ---- 
+       return ([],AtC c,v',[])
+     AInt i -> do
+       return ([],AtI i,valAbsInt,[])
+     AFloat i -> do
+       return ([],AtF i,valAbsFloat,[])
+     AStr s -> do
+       return ([],AtL s,valAbsString,[])
+     AMeta m v -> do
+       v' <- whnf v ---- 
+       return ([],AtM m,v',[])
+     _ -> Bad "illegal tree" -- AProd
+
+grammar2theory :: GFCGrammar -> Theory
+grammar2theory gr (m,f) = case lookupFunType gr m f of
+  Ok t -> return $ type2val t
+  Bad s -> case lookupCatContext gr m f of
+    Ok cont -> return $ cont2val cont
+    _ -> Bad s
+
+cont2exp :: Context -> Exp
+cont2exp c = mkProd (c, eType, []) -- to check a context
+
+cont2val :: Context -> Val
+cont2val = type2val . cont2exp
+
+-- some top-level batch-mode checkers for the compiler
+
+justTypeCheckSrc :: Grammar -> Exp -> Val -> Err Constraints
+justTypeCheckSrc gr e v = do
+  (_,constrs0) <- checkExp (grammar2theorySrc gr) (initTCEnv []) e v
+  return $ filter notJustMeta constrs0
+----  return $ fst $ splitConstraintsSrc gr constrs0
+---- this change was to force proper tc of abstract modules. 
+---- May not be quite right. AR 13/9/2005 
+
+notJustMeta (c,k) = case (c,k) of
+     (VClos g1 (Meta m1), VClos g2 (Meta m2)) -> False
+     _ -> True
+
+grammar2theorySrc :: Grammar -> Theory
+grammar2theorySrc gr (m,f) = case lookupFunTypeSrc gr m f of
+  Ok t -> return $ type2val t
+  Bad s -> case lookupCatContextSrc gr m f of
+    Ok cont -> return $ cont2val cont
+    _ -> Bad s
+
+checkContext :: Grammar -> Context -> [String]
+checkContext st = checkTyp st . cont2exp
+
+checkTyp :: Grammar -> Type -> [String]
+checkTyp gr typ = err singleton prConstrs $ justTypeCheckSrc gr typ vType
+
+checkEquation :: Grammar -> Fun -> Trm -> [String]
+checkEquation gr (m,fun) def = err singleton id $ do
+  typ  <- lookupFunTypeSrc gr m fun
+----  cs   <- checkEqs (grammar2theorySrc gr) (initTCEnv []) ((m,fun),def) (vClos typ)
+  cs   <- justTypeCheckSrc gr def (vClos typ)
+  let cs1 = filter notJustMeta cs ----- filter (not . possibleConstraint gr) cs ----
+  return $ ifNull [] (singleton . prConstraints) cs1
+
+checkConstrs :: Grammar -> Cat -> [Ident] -> [String]
+checkConstrs gr cat _ = [] ---- check constructors!
+
+
+
+
+
+ 
+{- ----
+err singleton concat . mapM checkOne where
+  checkOne con = do
+    typ   <- lookupFunType gr con
+    typ'  <- computeAbsTerm gr typ
+    vcat  <- valCat typ'
+    return $ if (cat == vcat) then [] else ["wrong type in constructor" +++ prt con]
+-}
+
+editAsTermCommand :: GFCGrammar -> (Loc TrNode -> Err (Loc TrNode)) -> Exp -> [Exp]
+editAsTermCommand gr c e = err (const []) singleton $ do
+  t  <- annotate gr $ refreshMetas [] e
+  t' <- c $ tree2loc t
+  return $ tree2exp $ loc2tree t'
+
+exp2termCommand :: GFCGrammar -> (Exp -> Err Exp) -> Tree -> Err Tree
+exp2termCommand gr f t = errIn ("modifying term" +++ prt t) $ do
+  let exp = tree2exp t
+  exp2 <- f exp
+  annotate gr exp2
+
+exp2termlistCommand :: GFCGrammar -> (Exp -> [Exp]) -> Tree -> [Tree]
+exp2termlistCommand gr f = err (const []) fst . mapErr (annotate gr) . f . tree2exp
+
+tree2termlistCommand :: GFCGrammar -> (Tree -> [Exp]) -> Tree -> [Tree]
+tree2termlistCommand gr f = err (const []) fst . mapErr (annotate gr) . f