From 8a0db597989642ed11b2fad8d272bb2778587ac5 Mon Sep 17 00:00:00 2001
From: krasimir <krasimir@chalmers.se>
Date: Sat, 24 Oct 2009 17:42:02 +0000
Subject: split the abstract syntax specific and the concrete syntax specific
 modules in different subfolders in GF.Compile

---
 GF.cabal                                 |   9 +-
 src/GF/Compile/AbsCompute.hs             | 140 -------
 src/GF/Compile/Abstract/Compute.hs       | 139 +++++++
 src/GF/Compile/Abstract/TC.hs            | 294 +++++++++++++
 src/GF/Compile/Abstract/TypeCheck.hs     |  83 ++++
 src/GF/Compile/CheckGrammar.hs           | 684 +-----------------------------
 src/GF/Compile/Compute.hs                | 463 ---------------------
 src/GF/Compile/Concrete/AppPredefined.hs | 159 +++++++
 src/GF/Compile/Concrete/Compute.hs       | 463 +++++++++++++++++++++
 src/GF/Compile/Concrete/TypeCheck.hs     | 693 +++++++++++++++++++++++++++++++
 src/GF/Compile/GrammarToGFCC.hs          |   2 +-
 src/GF/Compile/Optimize.hs               |   2 +-
 src/GF/Compile/Rename.hs                 |   1 -
 src/GF/Compile/TC.hs                     | 294 -------------
 src/GF/Compile/TypeCheck.hs              |  83 ----
 src/GF/Grammar/AppPredefined.hs          | 159 -------
 src/GFI.hs                               |   2 +-
 17 files changed, 1842 insertions(+), 1828 deletions(-)
 delete mode 100644 src/GF/Compile/AbsCompute.hs
 create mode 100644 src/GF/Compile/Abstract/Compute.hs
 create mode 100644 src/GF/Compile/Abstract/TC.hs
 create mode 100644 src/GF/Compile/Abstract/TypeCheck.hs
 delete mode 100644 src/GF/Compile/Compute.hs
 create mode 100644 src/GF/Compile/Concrete/AppPredefined.hs
 create mode 100644 src/GF/Compile/Concrete/Compute.hs
 create mode 100644 src/GF/Compile/Concrete/TypeCheck.hs
 delete mode 100644 src/GF/Compile/TC.hs
 delete mode 100644 src/GF/Compile/TypeCheck.hs
 delete mode 100644 src/GF/Grammar/AppPredefined.hs

diff --git a/GF.cabal b/GF.cabal
index 3df470d39..4c605c0d2 100644
--- a/GF.cabal
+++ b/GF.cabal
@@ -132,13 +132,10 @@ executable gf
     GF.Grammar.MMacros
     GF.Grammar.Lookup
     GF.Grammar.Unify
-    GF.Grammar.AppPredefined 
     GF.Grammar.PatternMatch
     GF.Grammar.Printer
     GF.Grammar.Binary
     GF.Infra.CheckM
-    GF.Compile.TC
-    GF.Compile.TypeCheck
     GF.Compile.Update
     GF.Compile.CheckGrammar
     GF.Compile.Refresh
@@ -146,7 +143,11 @@ executable gf
     GF.Compile.Rename
     GF.Compile.ReadFiles
     GF.Compile.GrammarToGFCC
-    GF.Compile.Compute
+    GF.Compile.Concrete.Compute
+    GF.Compile.Concrete.AppPredefined
+    GF.Compile.Abstract.TC
+    GF.Compile.Abstract.TypeCheck
+    GF.Compile.Abstract.Compute
     GF.Compile.Optimize
     GF.Compile.OptimizeGF
     GF.Compile.OptimizeGFCC
diff --git a/src/GF/Compile/AbsCompute.hs b/src/GF/Compile/AbsCompute.hs
deleted file mode 100644
index bfc824d82..000000000
--- a/src/GF/Compile/AbsCompute.hs
+++ /dev/null
@@ -1,140 +0,0 @@
-----------------------------------------------------------------------
--- |
--- 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.Compile.AbsCompute (LookDef,
-		   compute, 
-		   computeAbsTerm, 
-		   computeAbsTermIn, 
-		   beta
-		  ) where
-
-import GF.Data.Operations
-
-import GF.Grammar
-import GF.Grammar.Lookup
-import GF.Compile.Compute
-
-import Debug.Trace
-import Data.List(intersperse)
-import Control.Monad (liftM, liftM2)
-import Text.PrettyPrint
-
--- for debugging
-tracd m t = t 
--- tracd = trace
-
-compute :: SourceGrammar -> Exp -> Err Exp
-compute = computeAbsTerm
-
-computeAbsTerm :: SourceGrammar -> 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 Int,Maybe [Equation])
-
-computeAbsTermIn :: LookDef -> [Ident] -> Exp -> Err Exp
-computeAbsTermIn lookd xs e = errIn (render (text "computing" <+> ppTerm Unqualified 0 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' = map snd yy ++ vv
-      aa'    <- mapM (compt vv') aa
-      case look f of
-        Just eqs -> tracd (text "\nmatching" <+> ppTerm Unqualified 0 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 (text "by Egs:" <+> ppTerm Unqualified 0 d') $ return $ mkAbs yy $ d'
-          _ -> tracd (text "no match" <+> ppTerm Unqualified 0 t') $ 
-               do
-            let v = mkApp f aa'
-            return $ mkAbs yy $ v
-        _ -> do
-          let t2 = mkAbs yy $ mkApp f aa'
-          tracd (text "not defined" <+> ppTerm Unqualified 0 t2) $ return t2
-
-  look t = case t of
-     (Q m f) -> case lookd m f of
-       Ok (_,md) -> md
-       _ -> Nothing
-     _ -> 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 b x a t      -> Prod b x (beta vv a) (beta (x:vv) t)
-  Abs b x t       -> Abs b x (beta (x:vv) t)
-  _               -> 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 $ render (text "no applicable case for" <+> hcat (punctuate comma (map (ppTerm Unqualified 0) terms)))
-  (patts,_):_ | length patts /= length terms -> 
-       Bad (render (text "wrong number of args for patterns :" <+> 
-                    hsep (map (ppPatt Unqualified 0) patts) <+> text "cannot take" <+> hsep (map (ppTerm Unqualified 0) terms)))
-  (patts,val):cc -> case mapM tryMatch (zip patts terms) of
-     Ok substs -> return (tracd (text "value" <+> ppTerm Unqualified 0 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
-    (PW,    _) | 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 (render (text "no match in pattern" <+> ppPatt Unqualified 0 p <+> text "for" <+> ppTerm Unqualified 0 t))
-
-  notMeta e = case e of
-    Meta _  -> False
-    App f a -> notMeta f &&  notMeta a  
-    Abs _ _ b -> notMeta b
-    _ -> True
-
-  prtm p g = 
-    ppPatt Unqualified 0 p <+> colon $$ hsep (punctuate semi [ppIdent x <+> char '=' <+> ppTerm Unqualified 0 y | (x,y) <- g])
diff --git a/src/GF/Compile/Abstract/Compute.hs b/src/GF/Compile/Abstract/Compute.hs
new file mode 100644
index 000000000..29cc73525
--- /dev/null
+++ b/src/GF/Compile/Abstract/Compute.hs
@@ -0,0 +1,139 @@
+----------------------------------------------------------------------
+-- |
+-- Module      : GF.Compile.Abstract.Compute
+-- 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.Compile.Abstract.Compute (LookDef,
+		   compute, 
+		   computeAbsTerm, 
+		   computeAbsTermIn, 
+		   beta
+		  ) where
+
+import GF.Data.Operations
+
+import GF.Grammar
+import GF.Grammar.Lookup
+
+import Debug.Trace
+import Data.List(intersperse)
+import Control.Monad (liftM, liftM2)
+import Text.PrettyPrint
+
+-- for debugging
+tracd m t = t 
+-- tracd = trace
+
+compute :: SourceGrammar -> Exp -> Err Exp
+compute = computeAbsTerm
+
+computeAbsTerm :: SourceGrammar -> 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 Int,Maybe [Equation])
+
+computeAbsTermIn :: LookDef -> [Ident] -> Exp -> Err Exp
+computeAbsTermIn lookd xs e = errIn (render (text "computing" <+> ppTerm Unqualified 0 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' = map snd yy ++ vv
+      aa'    <- mapM (compt vv') aa
+      case look f of
+        Just eqs -> tracd (text "\nmatching" <+> ppTerm Unqualified 0 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 (text "by Egs:" <+> ppTerm Unqualified 0 d') $ return $ mkAbs yy $ d'
+          _ -> tracd (text "no match" <+> ppTerm Unqualified 0 t') $ 
+               do
+            let v = mkApp f aa'
+            return $ mkAbs yy $ v
+        _ -> do
+          let t2 = mkAbs yy $ mkApp f aa'
+          tracd (text "not defined" <+> ppTerm Unqualified 0 t2) $ return t2
+
+  look t = case t of
+     (Q m f) -> case lookd m f of
+       Ok (_,md) -> md
+       _ -> Nothing
+     _ -> 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 b x a t      -> Prod b x (beta vv a) (beta (x:vv) t)
+  Abs b x t       -> Abs b x (beta (x:vv) t)
+  _               -> 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 $ render (text "no applicable case for" <+> hcat (punctuate comma (map (ppTerm Unqualified 0) terms)))
+  (patts,_):_ | length patts /= length terms -> 
+       Bad (render (text "wrong number of args for patterns :" <+> 
+                    hsep (map (ppPatt Unqualified 0) patts) <+> text "cannot take" <+> hsep (map (ppTerm Unqualified 0) terms)))
+  (patts,val):cc -> case mapM tryMatch (zip patts terms) of
+     Ok substs -> return (tracd (text "value" <+> ppTerm Unqualified 0 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
+    (PW,    _) | 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 (render (text "no match in pattern" <+> ppPatt Unqualified 0 p <+> text "for" <+> ppTerm Unqualified 0 t))
+
+  notMeta e = case e of
+    Meta _  -> False
+    App f a -> notMeta f &&  notMeta a  
+    Abs _ _ b -> notMeta b
+    _ -> True
+
+  prtm p g = 
+    ppPatt Unqualified 0 p <+> colon $$ hsep (punctuate semi [ppIdent x <+> char '=' <+> ppTerm Unqualified 0 y | (x,y) <- g])
diff --git a/src/GF/Compile/Abstract/TC.hs b/src/GF/Compile/Abstract/TC.hs
new file mode 100644
index 000000000..163301838
--- /dev/null
+++ b/src/GF/Compile/Abstract/TC.hs
@@ -0,0 +1,294 @@
+----------------------------------------------------------------------
+-- |
+-- 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.Compile.Abstract.TC (AExp(..),
+	   Theory,
+	   checkExp,
+	   inferExp,
+	   checkBranch,
+	   eqVal,
+	   whnf
+	  ) where
+
+import GF.Data.Operations
+import GF.Grammar
+import GF.Grammar.Predef
+
+import Control.Monad
+import Data.List (sortBy)
+import Data.Maybe
+import Text.PrettyPrint
+
+data AExp =
+     AVr   Ident Val 
+   | ACn   QIdent Val
+   | AType 
+   | AInt  Integer 
+   | AFloat Double
+   | AStr  String
+   | AMeta MetaId Val
+   | AApp  AExp AExp Val 
+   | AAbs  Ident Val AExp 
+   | AProd Ident AExp AExp 
+   | AEqs  [([Exp],AExp)] --- not used
+   | ARecType [ALabelling]
+   | AR    [AAssign]
+   | AP    AExp Label Val
+   | AData Val
+  deriving (Eq,Show)
+
+type ALabelling = (Label, AExp) 
+type AAssign = (Label, (Val, AExp))
+
+type Theory = QIdent -> Err Val
+
+lookupConst :: Theory -> QIdent -> Err Val
+lookupConst th f = th f
+
+lookupVar :: Env -> Ident -> Err Val
+lookupVar g x = maybe (Bad (render (text "unknown variable" <+> ppIdent 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)
+  RecType xs -> do xs <- mapM (\(l,e) -> eval env e >>= \e -> return (l,e)) xs
+                   return (VRecType xs)
+  _ -> 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,[])
+
+    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)
+      _ -> Bad (render (text "function type expected for" <+> ppTerm Unqualified 0 e <+> text "instead of" <+> ppValue Unqualified 0 typ))
+
+    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)
+
+    R xs -> 
+      case typ of
+        VRecType ys -> do case [l | (l,_) <- ys, isNothing (lookup l xs)] of
+                            [] -> return ()
+                            ls -> fail (render (text "no value given for label:" <+> fsep (punctuate comma (map ppLabel ls))))
+                          r <- mapM (checkAssign th tenv ys) xs
+                          let (xs,css) = unzip r
+                          return (AR xs, concat css)
+        _           -> Bad (render (text "record type expected for" <+> ppTerm Unqualified 0 e <+> text "instead of" <+> ppValue Unqualified 0 typ))
+
+    P r l -> do (r',cs) <- checkExp th tenv r (VRecType [(l,typ)])
+                return (AP r' l typ,cs)
+
+    _ -> 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 && isPredefCat c
+                     -> 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, [])
+   RecType xs -> do r <- mapM (checkLabelling th tenv) xs
+                    let (xs,css) = unzip r
+                    return (ARecType xs, vType, concat css)
+   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)
+      _ -> Bad (render (text "Prod expected for function" <+> ppTerm Unqualified 0 f <+> text "instead of" <+> ppValue Unqualified 0 typ))
+   _ -> Bad (render (text "cannot infer type of expression" <+> ppTerm Unqualified 0 e))
+
+checkLabelling :: Theory -> TCEnv -> Labelling -> Err (ALabelling, [(Val,Val)])
+checkLabelling th tenv (lbl,typ) = do
+  (atyp,cs) <- checkType th tenv typ
+  return ((lbl,atyp),cs)
+
+checkAssign :: Theory -> TCEnv -> [(Label,Val)] -> Assign -> Err (AAssign, [(Val,Val)])
+checkAssign th tenv@(k,rho,gamma) typs (lbl,(Just typ,exp)) = do
+  (atyp,cs1) <- checkType th tenv typ
+  val <- eval rho typ
+  cs2 <- case lookup lbl typs of
+           Nothing   -> return []
+           Just val0 -> eqVal k val val0
+  (aexp,cs3) <- checkExp th tenv exp val
+  return ((lbl,(val,aexp)),cs1++cs2++cs3)
+checkAssign th tenv@(k,rho,gamma) typs (lbl,(Nothing,exp)) = do
+  case lookup lbl typs of
+    Nothing  -> do (aexp,val,cs) <- inferExp th tenv exp
+                   return ((lbl,(val,aexp)),cs)
+    Just val -> do (aexp,cs) <- checkExp th tenv exp val
+                   return ((lbl,(val,aexp)),cs)
+
+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
+        _ -> Bad (render (text "Product expected for definiens" <+> ppTerm Unqualified 0 t <+> text "instead of" <+> ppValue Unqualified 0 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 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 (Q m c) xss : ps, j, g',k') 
+                    where (xss,j,g',k') = foldr p2t ([],i,g,k) xs
+     _ -> error $ render (text "undefined p2t case" <+> ppPatt Unqualified 0 p <+> text "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)
+         _ -> Bad (render (text "Prod expected for function" <+> ppTerm Unqualified 0 f <+> text "instead of" <+> ppValue Unqualified 0 typ))
+     _ -> Bad (render (text "cannot typecheck pattern" <+> ppTerm Unqualified 0 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/Compile/Abstract/TypeCheck.hs b/src/GF/Compile/Abstract/TypeCheck.hs
new file mode 100644
index 000000000..2632c54dd
--- /dev/null
+++ b/src/GF/Compile/Abstract/TypeCheck.hs
@@ -0,0 +1,83 @@
+----------------------------------------------------------------------
+-- |
+-- 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.Compile.Abstract.TypeCheck (-- * top-level type checking functions; TC should not be called directly.
+		  checkContext,
+		  checkTyp,
+		  checkDef,
+		  checkConstrs,
+		 ) where
+
+import GF.Data.Operations
+
+import GF.Infra.CheckM
+import GF.Grammar
+import GF.Grammar.Lookup
+import GF.Grammar.Unify
+import GF.Compile.Refresh
+import GF.Compile.Abstract.Compute
+import GF.Compile.Abstract.TC
+
+import Text.PrettyPrint
+import Control.Monad (foldM, liftM, liftM2)
+
+-- | invariant way of creating TCEnv from context
+initTCEnv gamma = 
+  (length gamma,[(x,VGen i x) | ((x,_),i) <- zip gamma [0..]], gamma) 
+
+-- interface to TC type checker
+
+type2val :: Type -> Val
+type2val = VClos []
+
+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
+
+justTypeCheck :: SourceGrammar -> Exp -> Val -> Err Constraints
+justTypeCheck gr e v = do
+  (_,constrs0) <- checkExp (grammar2theory gr) (initTCEnv []) e v
+  (constrs1,_) <- unifyVal constrs0
+  return $ filter notJustMeta constrs1
+
+notJustMeta (c,k) = case (c,k) of
+    (VClos g1 (Meta m1), VClos g2 (Meta m2)) -> False
+    _ -> True
+
+grammar2theory :: SourceGrammar -> 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
+
+checkContext :: SourceGrammar -> Context -> [Message]
+checkContext st = checkTyp st . cont2exp
+
+checkTyp :: SourceGrammar -> Type -> [Message]
+checkTyp gr typ = err (\x -> [text x]) ppConstrs $ justTypeCheck gr typ vType
+
+checkDef :: SourceGrammar -> Fun -> Type -> [Equation] -> [Message]
+checkDef gr (m,fun) typ eqs = err (\x -> [text x]) ppConstrs $ do
+  bcs <- mapM (\b -> checkBranch (grammar2theory gr) (initTCEnv []) b (type2val typ)) eqs
+  let (bs,css) = unzip bcs
+  (constrs,_) <- unifyVal (concat css)
+  return $ filter notJustMeta constrs
+
+checkConstrs :: SourceGrammar -> Cat -> [Ident] -> [String]
+checkConstrs gr cat _ = [] ---- check constructors!
diff --git a/src/GF/Compile/CheckGrammar.hs b/src/GF/Compile/CheckGrammar.hs
index e176cbb4a..520a7adbf 100644
--- a/src/GF/Compile/CheckGrammar.hs
+++ b/src/GF/Compile/CheckGrammar.hs
@@ -1,4 +1,3 @@
-{-# LANGUAGE PatternGuards #-}
 ----------------------------------------------------------------------
 -- |
 -- Module      : CheckGrammar
@@ -27,18 +26,14 @@ module GF.Compile.CheckGrammar (
 import GF.Infra.Ident
 import GF.Infra.Modules
 
-import GF.Compile.TypeCheck
+import GF.Compile.Abstract.TypeCheck
+import GF.Compile.Concrete.TypeCheck
 
-import GF.Compile.Refresh
+import GF.Grammar
 import GF.Grammar.Lexer
-import GF.Grammar.Grammar
-import GF.Grammar.Printer
 import GF.Grammar.Lookup
 import GF.Grammar.Predef
-import GF.Grammar.Macros
 import GF.Grammar.PatternMatch
-import GF.Grammar.AppPredefined
-import GF.Grammar.Lockfield (isLockLabel, lockRecType, unlockRecord)
 
 import GF.Data.Operations
 import GF.Infra.CheckM
@@ -263,54 +258,6 @@ checkCncInfo gr m mo (a,abs) c info = do
  where
    chIn cat = checkIn (text "Happened in" <+> text cat <+> ppIdent c <+> ppPosition mo c <> colon)
 
-computeLType :: SourceGrammar -> Context -> Type -> Check Type
-computeLType gr g0 t = comp (reverse [(b,x, Vr x) | (b,x,_) <- g0] ++ g0) t
- where
-  comp g ty = case ty of
-    _ | Just _ <- isTypeInts ty -> return ty ---- shouldn't be needed
-      | isPredefConstant ty     -> return ty ---- shouldn't be needed
-
-    Q m ident -> checkIn (text "module" <+> ppIdent m) $ do
-      ty' <- checkErr (lookupResDef gr m ident) 
-      if ty' == ty then return ty else comp g ty' --- is this necessary to test?
-
-    Vr ident  -> checkLookup ident g -- never needed to compute!
-
-    App f a -> do
-      f' <- comp g f
-      a' <- comp g a
-      case f' of
-        Abs b x t -> comp ((b,x,a'):g) t
-        _ -> return $ App f' a'
-
-    Prod bt x a b -> do
-      a' <- comp g a
-      b' <- comp ((bt,x,Vr x) : g) b
-      return $ Prod bt x a' b'
-
-    Abs bt x b -> do
-      b' <- comp ((bt,x,Vr x):g) b
-      return $ Abs bt x b'
-
-    ExtR r s -> do
-      r' <- comp g r
-      s' <- comp g s
-      case (r',s') of
-        (RecType rs, RecType ss) -> checkErr (plusRecType r' s') >>= comp g
-        _ -> return $ ExtR r' s'
-
-    RecType fs -> do
-      let fs' = sortRec fs
-      liftM RecType $ mapPairsM (comp g) fs'
-
-    ELincat c t -> do
-      t' <- comp g t
-      checkErr $ lockRecType c t' ---- locking to be removed AR 20/6/2009
-
-    _ | ty == typeTok -> return typeStr
-    _ | isPredefConstant ty -> return ty
-
-    _ -> composOp (comp g) ty
 
 checkPrintname :: SourceGrammar -> Maybe Term -> Check ()
 checkPrintname st (Just t) = checkLType st [] t typeStr >> return ()
@@ -322,627 +269,8 @@ checkReservedId x
   | isReservedWord (ident2bs x) = checkWarn (text "reserved word used as identifier:" <+> ppIdent x)
   | otherwise                   = return ()
 
--- the underlying algorithms
-
-inferLType :: SourceGrammar -> Context -> Term -> Check (Term, Type)
-inferLType gr g 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) >>= computeLType gr g
-     ,
-     checkErr (lookupResDef gr m ident) >>= inferLType gr g
-     ,
-     checkError (text "cannot infer type of constant" <+> ppTerm Unqualified 0 trm)
-     ]
-
-   QC m ident | isPredef m -> termWith trm $ checkErr (typPredefined ident)
-
-   QC m ident -> checks [
-       termWith trm $ checkErr (lookupResType gr m ident) >>= computeLType gr g
-       ,
-       checkErr (lookupResDef gr m ident) >>= inferLType gr g
-       ,
-       checkError (text "cannot infer type of canonical constant" <+> ppTerm Unqualified 0 trm)
-       ]
-
-   Val _ ty i -> termWith trm $ return ty
-
-   Vr ident -> termWith trm $ checkLookup ident g
-
-   Typed e t -> do
-     t' <- computeLType gr g t
-     checkLType gr g e t'
-     return (e,t')
-
-   App f a -> do
-     over <- getOverload gr g Nothing trm
-     case over of
-       Just trty -> return trty
-       _ -> do
-         (f',fty) <- inferLType gr g f
-         fty' <- computeLType gr g fty
-         case fty' of
-           Prod bt z arg val -> do 
-             a' <- justCheck g a arg
-             ty <- if isWildIdent z 
-                      then return val
-                      else substituteLType [(bt,z,a')] val
-             return (App f' a',ty) 
-           _ -> checkError (text "A function type is expected for" <+> ppTerm Unqualified 0 f <+> text "instead of type" <+> ppType fty)
-
-   S f x -> do
-     (f', fty) <- inferLType gr g f
-     case fty of
-       Table arg val -> do
-         x'<- justCheck g x arg
-         return (S f' x', val)
-       _ -> checkError (text "table lintype expected for the table in" $$ nest 2 (ppTerm Unqualified 0 trm))
-
-   P t i -> do
-     (t',ty) <- inferLType gr g t   --- ??
-     ty' <- computeLType gr g ty
-     let tr2 = P t' i
-     termWith tr2 $ case ty' of
-       RecType ts -> case lookup i ts of
-                       Nothing -> checkError (text "unknown label" <+> ppLabel i <+> text "in" $$ nest 2 (ppTerm Unqualified 0 ty'))
-                       Just x  -> return x
-       _          -> checkError (text "record type expected for:" <+> ppTerm Unqualified 0 t $$
-                                 text " instead of the inferred:" <+> ppTerm Unqualified 0 ty')
-   PI t i _ -> inferLType gr g $ P t i
-
-   R r -> do
-     let (ls,fs) = unzip r
-     fsts <- mapM inferM fs
-     let ts = [ty | (Just ty,_) <- fsts]
-     checkCond (text "cannot infer type of record" $$ nest 2 (ppTerm Unqualified 0 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
-     checkLType gr g trm (Table arg val)
-   T (TComp arg) pts -> do
-     (_,val) <- checks $ map (inferCase (Just arg)) pts
-     checkLType gr g 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 
-       [] -> checkError (text "cannot infer table type of" <+> ppTerm Unqualified 0 trm)
-----       PInt k : _ -> return $ Ints $ max [i | PInt i <- pts'] 
-       _  -> do 
-         (arg,val) <- checks $ map (inferCase Nothing) pts'
-         checkLType gr g trm (Table arg val)
-   V arg pts -> do
-     (_,val) <- checks $ map (inferLType gr g) pts
-     return (trm, Table arg val)
-
-   K s  -> do
-     if elem ' ' s
-        then do
-          let ss = foldr C Empty (map K (words s))  
-          ----- removed irritating warning AR 24/5/2008
-          ----- checkWarn ("token \"" ++ s ++ 
-          -----              "\" converted to token list" ++ prt ss)
-          return (ss, typeStr)
-        else return (trm, typeStr)
-
-   EInt i -> return (trm, typeInt)
-
-   EFloat i -> return (trm, typeFloat)
-
-   Empty -> return (trm, typeStr)
-
-   C s1 s2 -> 
-     check2 (flip (justCheck g) typeStr) C s1 s2 typeStr
-
-   Glue s1 s2 -> 
-     check2 (flip (justCheck g) typeStr) Glue s1 s2 typeStr ---- typeTok
-
----- hack from Rename.identRenameTerm, to live with files with naming conflicts 18/6/2007
-   Strs (Cn c : ts) | c == cConflict -> do
-     checkWarn (text "unresolved constant, could be any of" <+> hcat (map (ppTerm Unqualified 0) ts))
-     inferLType gr g (head ts)
-
-   Strs ts -> do
-     ts' <- mapM (\t -> justCheck g t typeStr) ts 
-     return (Strs ts', typeStrs)
-
-   Alts (t,aa) -> do
-     t'  <- justCheck g t typeStr
-     aa' <- flip mapM aa (\ (c,v) -> do
-        c' <- justCheck g c typeStr 
-        v' <- checks $ map (justCheck g v) [typeStrs, EPattType typeStr]
-        return (c',v'))
-     return (Alts (t',aa'), typeStr)
-
-   RecType r -> do
-     let (ls,ts) = unzip r
-     ts' <- mapM (flip (justCheck g) typeType) ts 
-     return (RecType (zip ls ts'), typeType)
-
-   ExtR r s -> do
-     (r',rT) <- inferLType gr g r 
-     rT'     <- computeLType gr g rT
-     (s',sT) <- inferLType gr g s
-     sT'     <- computeLType gr g 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'
-         checkLType gr g trm' rt ---- return (trm', rt)
-       _ | rT' == typeType && sT' == typeType -> return (trm', typeType)
-       _ -> checkError (text "records or record types expected in" <+> ppTerm Unqualified 0 trm)
-
-   Sort _     -> 
-     termWith trm $ return typeType
-
-   Prod bt x a b -> do
-     a' <- justCheck g a typeType
-     b' <- justCheck ((bt,x,a'):g) b typeType
-     return (Prod bt x a' b', typeType)
-
-   Table p t  -> do
-     p' <- justCheck g p typeType --- check p partype! 
-     t' <- justCheck g t typeType
-     return $ (Table p' t', typeType)
-
-   FV vs -> do
-     (_,ty) <- checks $ map (inferLType gr g) vs
----     checkIfComplexVariantType trm ty
-     checkLType gr g trm ty
-
-   EPattType ty -> do
-     ty' <- justCheck g ty typeType
-     return (EPattType ty',typeType)
-   EPatt p -> do
-     ty <- inferPatt p
-     return (trm, EPattType ty)
-
-   ELin c trm -> do
-     (trm',ty) <- inferLType gr g trm
-     ty' <- checkErr $ lockRecType c ty ---- lookup c; remove lock AR 20/6/2009
-     return $ (ELin c trm', ty') 
-
-   _ -> checkError (text "cannot infer lintype of" <+> ppTerm Unqualified 0 trm)
-
- where
-   isPredef m = elem m [cPredef,cPredefAbs]
-
-   justCheck g ty te = checkLType gr g ty te >>= return . fst
-
-   -- for record fields, which may be typed
-   inferM (mty, t) = do
-     (t', ty') <- case mty of
-       Just ty -> checkLType gr g ty t
-       _ -> inferLType gr g t
-     return (Just ty',t')
-
-   inferCase mty (patt,term) = do
-     arg  <- maybe (inferPatt patt) return mty
-     cont <- pattContext gr g arg patt
-     (_,val) <- inferLType gr (reverse cont ++ g) term
-     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
-     PChar -> True
-     PChars _ -> 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 $ liftM valTypeCnc (lookupResType gr q c)
-     PAs _ p  -> inferPatt p
-     PNeg p   -> inferPatt p
-     PAlt p q -> checks [inferPatt p, inferPatt q]
-     PSeq _ _ -> return $ typeStr
-     PRep _   -> return $ typeStr
-     PChar    -> return $ typeStr
-     PChars _ -> return $ typeStr
-     _ -> inferLType gr g (patt2term p) >>= return . snd
-
-
--- type inference: Nothing, type checking: Just t
--- the latter permits matching with value type
-getOverload :: SourceGrammar -> Context -> Maybe Type -> Term -> Check (Maybe (Term,Type))
-getOverload gr g mt ot = case appForm ot of
-     (f@(Q m c), ts) -> case lookupOverload gr m c of
-       Ok typs -> do
-         ttys <- mapM (inferLType gr g) ts
-         v <- matchOverload f typs ttys
-         return $ Just v
-       _ -> return Nothing
-     _ -> return Nothing
- where
-   matchOverload f typs ttys = do
-     let (tts,tys) = unzip ttys
-     let vfs = lookupOverloadInstance tys typs
-     let matches = [vf | vf@((v,_),_) <- vfs, matchVal mt v]
-
-     case ([vf | (vf,True) <- matches],[vf | (vf,False) <- matches]) of
-       ([(val,fun)],_) -> return (mkApp fun tts, val)
-       ([],[(val,fun)]) -> do
-         checkWarn (text "ignoring lock fields in resolving" <+> ppTerm Unqualified 0 ot) 
-         return (mkApp fun tts, val)
-       ([],[]) -> do
-         let showTypes ty = hsep (map ppType ty)
-         checkError $ text "no overload instance of" <+> ppTerm Unqualified 0 f $$
-                      text "for" $$
-                      nest 2 (showTypes tys) $$
-                      text "among" $$
-                      nest 2 (vcat [showTypes ty | (ty,_) <- typs]) $$
-                      maybe empty (\x -> text "with value type" <+> ppType x) mt
-
-       (vfs1,vfs2) -> case (noProds vfs1,noProds vfs2) of
-         ([(val,fun)],_) -> do
-           return (mkApp fun tts, val)
-         ([],[(val,fun)]) -> do
-           checkWarn (text "ignoring lock fields in resolving" <+> ppTerm Unqualified 0 ot) 
-           return (mkApp fun tts, val)
-
------ unsafely exclude irritating warning AR 24/5/2008
------           checkWarn $ "overloading of" +++ prt f +++ 
------             "resolved by excluding partial applications:" ++++
------             unlines [prtType env ty | (ty,_) <- vfs', not (noProd ty)]
-
-
-         _ -> checkError $ text "ambiguous overloading of" <+> ppTerm Unqualified 0 f <+>
-                           text "for" <+> hsep (map ppType tys) $$ 
-                           text "with alternatives" $$
-                           nest 2 (vcat [ppType ty | (ty,_) <- if null vfs1 then vfs2 else vfs2])
-
-   matchVal mt v = elem mt [Nothing,Just v,Just (unlocked v)]
-
-   unlocked v = case v of
-     RecType fs -> RecType $ filter (not . isLockLabel . fst) fs
-     _ -> v
-   ---- TODO: accept subtypes
-   ---- TODO: use a trie
-   lookupOverloadInstance tys typs = 
-     [((mkFunType rest val, t),isExact) | 
-       let lt = length tys,
-       (ty,(val,t)) <- typs, length ty >= lt,
-       let (pre,rest) = splitAt lt ty, 
-       let isExact = pre == tys,
-       isExact || map unlocked pre == map unlocked tys
-     ]
-
-   noProds vfs = [(v,f) | (v,f) <- vfs, noProd v]
-
-   noProd ty = case ty of
-     Prod _ _ _ _ -> False
-     _ -> True
-
-checkLType :: SourceGrammar -> Context -> Term -> Type -> Check (Term, Type)
-checkLType gr g trm typ0 = do
-
-  typ <- computeLType gr g typ0
-
-  case trm of
-
-    Abs bt x c -> do
-      case typ of
-        Prod bt' z a b -> do 
-          (c',b') <- if isWildIdent z
-                       then checkLType gr ((bt,x,a):g) c b
-                       else do b' <- checkIn (text "abs") $ substituteLType [(bt',z,Vr x)] b
-                               checkLType gr ((bt,x,a):g) c b'
-          return $ (Abs bt x c', Prod bt' x a b')
-        _ -> checkError $ text "function type expected instead of" <+> ppType typ
-
-    App f a -> do
-       over <- getOverload gr g (Just typ) trm
-       case over of
-         Just trty -> return trty
-         _ -> do
-          (trm',ty') <- inferLType gr g trm
-          termWith trm' $ checkEqLType gr g typ ty' trm'
-
-    Q _ _ -> do
-       over <- getOverload gr g (Just typ) trm
-       case over of
-         Just trty -> return trty
-         _ -> do
-          (trm',ty') <- inferLType gr g trm
-          termWith trm' $ checkEqLType gr g typ ty' trm'
-
-    T _ [] ->
-      checkError (text "found empty table in type" <+> ppTerm Unqualified 0 typ)
-    T _ cs -> case typ of 
-      Table arg val -> do 
-        case allParamValues gr arg of
-          Ok vs -> do
-            let ps0 = map fst cs
-            ps <- checkErr $ testOvershadow ps0 vs
-            if null ps 
-              then return () 
-              else checkWarn (text "patterns never reached:" $$
-                              nest 2 (vcat (map (ppPatt Unqualified 0) ps)))
-          _ -> return () -- happens with variable types
-        cs' <- mapM (checkCase arg val) cs
-        return (T (TTyped arg) cs', typ)
-      _ -> checkError $ text "table type expected for table instead of" $$ nest 2 (ppType 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
-
-       _ -> checkError (text "record type expected in type checking instead of" $$ nest 2 (ppTerm Unqualified 0 typ))
-
-    ExtR r s -> case typ of
-       _ | typ == typeType -> do
-         trm' <- computeLType gr g trm
-         case trm' of
-           RecType _ -> termWith trm $ return typeType
-           ExtR (Vr _) (RecType _) -> termWith trm $ return typeType 
-                                      -- ext t = t ** ...
-           _ -> checkError (text "invalid record type extension" <+> nest 2 (ppTerm Unqualified 0 trm))
-       RecType rr -> do
-         (r',ty,s') <- checks [
-            do (r',ty) <- inferLType gr g r
-               return (r',ty,s)
-           ,
-            do (s',ty) <- inferLType gr g s
-               return (s',ty,r)
-            ]
-         case ty of
-           RecType rr1 -> do
-                let (rr0,rr2) = recParts rr rr1
-                r2 <- justCheck g r' rr0
-                s2 <- justCheck g s' rr2
-                return $ (ExtR r2 s2, typ) 
-           _ -> checkError (text "record type expected in extension of" <+> ppTerm Unqualified 0 r $$
-                            text "but found" <+> ppTerm Unqualified 0 ty)
-
-       ExtR ty ex -> do
-         r' <- justCheck g r ty
-         s' <- justCheck g s ex
-         return $ (ExtR r' s', typ) --- is this all?
-
-       _ -> checkError (text "record extension not meaningful for" <+> ppTerm Unqualified 0 typ)
-
-    FV vs -> do
-      ttys <- mapM (flip (checkLType gr g) typ) vs
----      checkIfComplexVariantType trm typ
-      return (FV (map fst ttys), typ) --- typ' ?
-
-    S tab arg -> checks [ do
-      (tab',ty) <- inferLType gr g tab
-      ty'       <- computeLType gr g ty
-      case ty' of
-        Table p t -> do
-          (arg',val) <- checkLType gr g arg p
-          checkEqLType gr g typ t trm
-          return (S tab' arg', t)
-        _ -> checkError (text "table type expected for applied table instead of" <+> ppType ty')
-     , do
-      (arg',ty) <- inferLType gr g arg
-      ty'       <- computeLType gr g ty
-      (tab',_)  <- checkLType gr g tab (Table ty' typ)
-      return (S tab' arg', typ)
-      ]
-    Let (x,(mty,def)) body -> case mty of
-      Just ty -> do
-        (def',ty') <- checkLType gr g def ty
-        body' <- justCheck ((Explicit,x,ty'):g) body typ
-        return (Let (x,(Just ty',def')) body', typ)
-      _ -> do
-        (def',ty) <- inferLType gr g def  -- tries to infer type of local constant
-        checkLType gr g (Let (x,(Just ty,def')) body) typ
-
-    ELin c tr -> do
-      tr1 <- checkErr $ unlockRecord c tr
-      checkLType gr g tr1 typ
-
-    _ -> do
-      (trm',ty') <- inferLType gr g trm
-      termWith trm' $ checkEqLType gr g typ ty' trm'
- where
-   justCheck g ty te = checkLType gr g ty te >>= return . fst
-
-   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
-       checkEqLType gr g ty ty0 t
-       (t',ty') <- checkLType gr g t ty
-       return (l,(Just ty',t'))
-     Just (_,t) -> do
-       (t',ty') <- checkLType gr g t ty
-       return (l,(Just ty',t'))
-     _ -> checkError $ 
-            if isLockLabel l 
-              then let cat = drop 5 (showIdent (label2ident l))
-                   in ppTerm Unqualified 0 (R rms) <+> text "is not in the lincat of" <+> text cat <> 
-                      text "; try wrapping it with lin" <+> text cat
-              else text "cannot find value for label" <+> ppLabel l <+> text "in" <+> ppTerm Unqualified 0 (R rms)
-
-   checkCase arg val (p,t) = do
-     cont <- pattContext gr g arg p
-     t' <- justCheck (reverse cont ++ g) t val
-     return (p,t')
-
-pattContext :: SourceGrammar -> Context -> Type -> Patt -> Check Context
-pattContext env g typ p = case p of
-  PV x -> return [(Explicit,x,typ)]
-  PP q c ps | q /= cPredef -> do ---- why this /=? AR 6/1/2006
-    t <- checkErr $ lookupResType env q c
-    let (cont,v) = typeFormCnc t
-    checkCond (text "wrong number of arguments for constructor in" <+> ppPatt Unqualified 0 p) 
-              (length cont == length ps)
-    checkEqLType env g typ v (patt2term p)
-    mapM (\((_,_,ty),p) -> pattContext env g ty p) (zip cont ps) >>= return . concat
-  PR r -> do
-    typ' <- computeLType env g 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 g)) pts >>= return . concat
-      _ -> checkError (text "record type expected for pattern instead of" <+> ppTerm Unqualified 0 typ')
-  PT t p' -> do
-    checkEqLType env g typ t (patt2term p')
-    pattContext env g typ p'
-
-  PAs x p -> do
-    g' <- pattContext env g typ p
-    return ((Explicit,x,typ):g')
-
-  PAlt p' q -> do
-    g1 <- pattContext env g typ p'
-    g2 <- pattContext env g typ q
-    let pts = nub ([x | pt@(_,x,_) <- g1, notElem pt g2] ++ [x | pt@(_,x,_) <- g2, notElem pt g1])
-    checkCond 
-      (text "incompatible bindings of" <+>
-       fsep (map ppIdent pts) <+> 
-       text "in pattern alterantives" <+> ppPatt Unqualified 0 p) (null pts) 
-    return g1 -- must be g1 == g2
-  PSeq p q -> do
-    g1 <- pattContext env g typ p
-    g2 <- pattContext env g typ q
-    return $ g1 ++ g2
-  PRep p' -> noBind typeStr p'
-  PNeg p' -> noBind typ p'
-
-  _ -> return [] ---- check types!
- where 
-   noBind typ p' = do
-    co <- pattContext env g typ p'
-    if not (null co)
-      then checkWarn (text "no variable bound inside pattern" <+> ppPatt Unqualified 0 p) 
-           >> return []
-      else return []
-
 -- auxiliaries
 
-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 [(x,t) | (_,x,t) <- 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 :: SourceGrammar -> Context -> Type -> Type -> Term -> Check Type
-checkEqLType gr g t u trm = do
-  (b,t',u',s) <- checkIfEqLType gr g t u trm
-  case b of
-    True  -> return t'
-    False -> checkError $ text s <+> text "type of" <+> ppTerm Unqualified 0 trm $$
-                          text "expected:" <+> ppType t $$
-                          text "inferred:" <+> ppType u
-
-checkIfEqLType :: SourceGrammar -> Context -> Type -> Type -> Term -> Check (Bool,Type,Type,String)
-checkIfEqLType gr g t u trm = do
-  t' <- computeLType gr g t
-  u' <- computeLType gr g 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 $ text "missing lock field" <+> fsep (map ppLabel 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
-     (_,u) | u == typeError -> 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
-     (t,u) | Just m <- isTypeInts t, Just n <- isTypeInts t -> m >= n
-           | Just _ <- isTypeInts t, u == typeInt           -> True ---- check size!
-           | t == typeInt,           Just _ <- isTypeInts u -> True ---- why this ???? AR 11/12/2005
-
-     ---- this should be made in Rename
-     (Q  m a, Q  n b) | a == b -> elem m (allExtendsPlus gr n) 
-                               || elem n (allExtendsPlus gr m)
-                               || m == n --- for Predef
-     (QC m a, QC n b) | a == b -> elem m (allExtendsPlus gr n) 
-                               || elem n (allExtendsPlus gr m)
-     (QC m a, Q  n b) | a == b -> elem m (allExtendsPlus gr n) 
-                               || elem n (allExtendsPlus gr m)
-     (Q  m a, QC n b) | a == b -> elem m (allExtendsPlus gr n) 
-                               || elem n (allExtendsPlus gr 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 $ render (text "missing record fields:" <+> fsep (punctuate comma (map ppLabel 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]
-
--- printing a type with a lock field lock_C as C
-ppType :: Type -> Doc
-ppType ty =
-  case ty of
-    RecType fs   -> case filter isLockLabel $ map fst fs of
-                      [lock] -> text (drop 5 (showIdent (label2ident lock)))
-                      _      -> ppTerm Unqualified 0 ty
-    Prod _ x a b -> ppType a <+> text "->" <+> ppType b
-    _            -> ppTerm Unqualified 0 ty
-
 -- | linearization types and defaults
 linTypeOfType :: SourceGrammar -> Ident -> Type -> Check (Context,Type)
 linTypeOfType cnc m typ = do
@@ -998,9 +326,3 @@ topoSortOpers st = do
     return 
     (\ops -> Bad (render (text "circular definitions:" <+> fsep (map ppIdent (head ops)))))
     eops
-
-checkLookup :: Ident -> Context -> Check Type
-checkLookup x g =
-  case [ty | (b,y,ty) <- g, x == y] of
-    []     -> checkError (text "unknown variable" <+> ppIdent x)
-    (ty:_) -> return ty
diff --git a/src/GF/Compile/Compute.hs b/src/GF/Compile/Compute.hs
deleted file mode 100644
index f4bc61a5b..000000000
--- a/src/GF/Compile/Compute.hs
+++ /dev/null
@@ -1,463 +0,0 @@
-----------------------------------------------------------------------
--- |
--- 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.Compile.Compute (computeConcrete, computeTerm,computeConcreteRec) where
-
-import GF.Data.Operations
-import GF.Grammar.Grammar
-import GF.Infra.Ident
-import GF.Infra.Option
-import GF.Infra.Modules
-import GF.Data.Str
-import GF.Grammar.Printer
-import GF.Grammar.Predef
-import GF.Grammar.Macros
-import GF.Grammar.Lookup
-import GF.Compile.Refresh
-import GF.Grammar.PatternMatch
-import GF.Grammar.Lockfield (isLockLabel,unlockRecord) ----
-
-import GF.Grammar.AppPredefined
-
-import Data.List (nub,intersperse)
-import Control.Monad (liftM2, liftM)
-import Text.PrettyPrint
-
--- | 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 = comput True where
-
-   comput full g t = ---- errIn ("subterm" +++ prt t) $ --- for debugging 
-              case t of
-
-     Q p c | p == cPredef -> return t
-           | otherwise    -> look p c 
-
-     Vr x -> do
-       t' <- maybe (Bad (render (text "no value given to variable" <+> ppIdent x))) return $ lookup x g
-       case t' of 
-         _ | t == t' -> return t
-         _ -> comp g t'
-
-     -- Abs x@(IA _) b -> do 
-     Abs _ _ _ | full -> do 
-       let (xs,b1) = termFormCnc t   
-       b' <- comp ([(x,Vr x) | (_,x) <- xs] ++ g) b1
-       return $ mkAbs xs b'
-     --  b' <- comp (ext x (Vr x) g) b
-     --  return $ Abs x b'
-     Abs _ _ _ -> return t -- hnf
-
-     Let (x,(_,a)) b -> do
-       a' <- comp g a
-       comp (ext x a' g) b
-
-     Prod b x a t -> do
-       a' <- comp g a
-       t' <- comp (ext x (Vr x) g) t
-       return $ Prod b x a' t'
-
-     -- beta-convert
-     App f a -> case appForm t of
-      (h,as) | length as > 1 -> do
-        h' <- hnf g h
-        as' <- mapM (comp g) as
-        case h' of
-          _ | not (null [() | FV _ <- as']) -> compApp g (mkApp h' as')
-          c@(QC _ _) -> do
-            return $ mkApp c as'
-          Q mod f | mod == cPredef -> do     
-            (t',b) <- appPredefined (mkApp h' as')
-            if b then return t' else comp g t'
-
-          Abs _ _ _ -> do
-            let (xs,b) = termFormCnc h'
-            let g' = (zip (map snd xs) as') ++ g
-            let as2 = drop (length xs) as'
-            let xs2 = drop (length as') xs
-            b' <- comp g' (mkAbs xs2 b)
-            if null as2 then return b' else comp g (mkApp b' as2)
-
-          _ -> compApp g (mkApp h' as')
-      _ -> compApp 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 (Bad (render (text "no value for label" <+> ppLabel 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)
---- - } ---
-
-         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 v -> do
-       t' <- compTable g t
-       v' <- comp g v
-       t1 <- case t' of
-----           V (RecType fs) _         -> uncurrySelect g fs t' v'
-----           T (TComp (RecType fs)) _ -> uncurrySelect g fs t' v'
-           _ -> return $ S t' v'
-       compSelect g t1
-
-     -- 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
-
-         (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 (d,aa) -> do
-       d' <- comp g d
-       aa' <- mapM (compInAlts g) aa
-       returnC (Alts (d',aa'))
-
-     -- 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
-         (R rs, R ss) -> plusRecord r' s'
-         (RecType rs, RecType ss) -> plusRecType r' s'
-         _ -> return $ ExtR r' s'
-
-     ELin c r -> do
-       r' <- comp g r
-       unlockRecord c r'
-
-     T _ _ -> compTable g t
-     V _ _ -> compTable g t
-
-     -- otherwise go ahead
-     _ -> composOp (comp g) t >>= returnC
-
-    where
-
-     compApp g (App f a) = do
-       f' <- hnf 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'
-
-         (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'
-
-     hnf  = comput False
-     comp = comput True
-
-     look p c
-       | rec       = lookupResDef gr p c >>= comp []
-       | otherwise = lookupResDef gr p c
-
-     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
-
-     compPatternMacro p = case p of
-       PM m c -> case look m c of
-         Ok (EPatt p') -> compPatternMacro p'
-         _ -> Bad (render (text "pattern expected as value of" $$ nest 2 (ppPatt Unqualified 0 p)))
-       PAs x p -> do
-         p' <- compPatternMacro p
-         return $ PAs x p'
-       PAlt p q -> do
-         p' <- compPatternMacro p
-         q' <- compPatternMacro q
-         return $ PAlt p' q'
-       PSeq p q -> do
-         p' <- compPatternMacro p
-         q' <- compPatternMacro q
-         return $ PSeq p' q'
-       PRep p -> do
-         p' <- compPatternMacro p
-         return $ PRep p'
-       PNeg p -> do
-         p' <- compPatternMacro p
-         return $ PNeg p'
-       PR rs -> do
-         rs' <- mapPairsM compPatternMacro rs
-         return $ PR rs'
-
-       _ -> return p
-
-     compSelect g (S t' 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 _ [(PW,c)] -> comp g c           --- an optimization
-         T _ [(PT _ PW,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 -> case v' of
-           Val _ _ i -> comp g $ ts !! i
-           _ -> do
-             vs <- allParamValues gr ptyp
-             case lookupR v' (zip vs [0 .. length vs - 1]) of
-               Just i -> comp g $ ts !! i
-               _ -> return $ S t' v' -- if v' is not canonical
-         T _ cc -> do
-           let v2 = case v' of
-                 Val te _ _ -> te
-                 _ -> v'
-           case matchPattern cc v2 of
-             Ok (c,g') -> comp (g' ++ g) c
-             _ | isCan v2 -> Bad (render (text "missing case" <+> ppTerm Unqualified 0 v2 <+> text "in" <+> ppTerm Unqualified 0 t))
-             _ -> return $ S t' v' -- if v' is not canonical
-
-         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'
-
-     --- needed to match records with and without type information
-     ---- todo: eliminate linear search in a list of records!
-     lookupR v vs = case v of
-       R rs -> lookup ([(x,y) | (x,(_,y)) <- rs]) 
-                                [([(x,y) | (x,(_,y)) <- rs],v) | (R rs,v) <- vs]
-       _ -> lookup v vs
-
-     -- case-expand tables
-     -- if already expanded, don't expand again
-     compTable g t = case t of
-         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'
-         V ty cs -> do
-           ty' <- comp g ty
-           -- if there are no variables, don't even go inside
-           cs' <- if (null g) then return cs else mapM (comp g) cs
-           return $ V ty' cs'
-
-         T i cs -> do
-           pty0 <- getTableType i
-           ptyp <- comp g pty0
-           case allParamValues gr ptyp of
-             Ok vs0 -> do
-               let vs = vs0 ---- [Val v ptyp i | (v,i) <- zip vs0 [0..]]
-               ps0  <- mapM (compPatternMacro . fst) cs
-               cs'  <- mapM (compBranchOpt g) (zip ps0 (map snd cs))
-               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, just course of values
-               return $ T (TComp ptyp) (zip ps' ts)
-             _ -> do
-               ps0  <- mapM (compPatternMacro . fst) cs
-               cs'  <- mapM (compBranch g) (zip ps0 (map snd cs))
-
-----               cs' <- mapM (compBranch g) cs
-               return $ T i cs'  -- happens with variable types
-         _ -> comp g t
-
-     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
-
-     compInAlts g (v,c) = do
-       v' <- comp g v
-       c' <- comp g c
-       c2 <- case c' of
-         EPatt p -> liftM Strs $ getPatts p
-         _ -> return c'
-       return (v',c2)
-      where
-       getPatts p = case p of
-         PAlt a b  -> liftM2 (++) (getPatts a) (getPatts b)
-         PString s -> return [K s]
-         PSeq a b  -> do
-           as <- getPatts a
-           bs <- getPatts b
-           return [K (s ++ t) | K s <- as, K t <- bs]
-         _ -> fail (render (text "not valid pattern in pre expression" <+> ppPatt Unqualified 0 p))
-
-{- ----
-     uncurrySelect g fs t v = do
-       ts <- mapM (allParamValues gr . snd) fs
-       vs <- mapM (comp g) [P v r | r <- map fst fs]
-       return $ reorderSelect t fs ts vs
-
-     reorderSelect t fs pss vs = case (t,fs,pss,vs) of
-       (V _ ts, f:fs1, ps:pss1, v:vs1) -> 
-         S (V (snd f) 
-             [reorderSelect (V (RecType fs1) t) fs1 pss1 vs1 | 
-               t <- segments (length ts `div` length ps) ts]) v 
-       (T (TComp _) cs, f:fs1, ps:pss1, v:vs1) -> 
-         S (T (TComp (snd f)) 
-             [(p,reorderSelect (T (TComp (RecType fs1)) c) fs1 pss1 vs1) | 
-               (ep,c) <- zip ps (segments (length cs `div` length ps) cs),
-               let Ok p = term2patt ep]) v 
-       _ -> t
-
-     segments i xs = 
-       let (x0,xs1) = splitAt i xs in x0 : takeWhile (not . null) (segments i xs1)
--}
-
-
--- | argument variables cannot be glued
-checkNoArgVars :: Term -> Err Term
-checkNoArgVars t = case t of
-  Vr (IA _ _)    -> Bad $ glueErrorMsg $ ppTerm Unqualified 0 t 
-  Vr (IAV _ _ _) -> Bad $ glueErrorMsg $ ppTerm Unqualified 0 t 
-  _ -> composOp checkNoArgVars t
-
-glueErrorMsg s = 
-  render (text "Cannot glue (+) term with run-time variable" <+> s <> char '.' $$
-          text "Use Prelude.bind instead.")
-
-getArgType t = case t of
-  V ty _ -> return ty
-  T (TComp ty) _ -> return ty
-  _ -> Bad (render (text "cannot get argument type of table" $$ nest 2 (ppTerm Unqualified 0 t)))
diff --git a/src/GF/Compile/Concrete/AppPredefined.hs b/src/GF/Compile/Concrete/AppPredefined.hs
new file mode 100644
index 000000000..154d76821
--- /dev/null
+++ b/src/GF/Compile/Concrete/AppPredefined.hs
@@ -0,0 +1,159 @@
+----------------------------------------------------------------------
+-- |
+-- 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.Compile.Concrete.AppPredefined (isInPredefined, typPredefined, appPredefined
+		     ) where
+
+import GF.Infra.Ident
+import GF.Data.Operations
+import GF.Grammar.Predef
+import GF.Grammar.Grammar
+import GF.Grammar.Macros
+import GF.Grammar.Printer
+import qualified Data.ByteString.Char8 as BS
+import Text.PrettyPrint
+
+-- 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 f
+  | f == cInt       = return typePType
+  | f == cFloat     = return typePType
+  | f == cErrorType = return typeType
+  | f == cInts      = return $ mkFunType [typeInt] typePType
+  | f == cPBool     = return typePType
+  | f == cError     = return $ mkFunType [typeStr] typeError  -- non-can. of empty set
+  | f == cPFalse    = return $ typePBool
+  | f == cPTrue     = return $ typePBool
+  | f == cDp        = return $ mkFunType [typeInt,typeTok] typeTok
+  | f == cDrop      = return $ mkFunType [typeInt,typeTok] typeTok
+  | f == cEqInt     = return $ mkFunType [typeInt,typeInt] typePBool
+  | f == cLessInt   = return $ mkFunType [typeInt,typeInt] typePBool
+  | f == cEqStr     = return $ mkFunType [typeTok,typeTok] typePBool
+  | f == cLength    = return $ mkFunType [typeTok] typeInt
+  | f == cOccur     = return $ mkFunType [typeTok,typeTok] typePBool
+  | f == cOccurs    = return $ mkFunType [typeTok,typeTok] typePBool
+  | f == cPlus      = return $ mkFunType [typeInt,typeInt] (typeInt)
+----  "read"   -> (P : Type) -> Tok -> P
+  | f == cShow      = return $ mkProd -- (P : PType) -> P -> Tok
+    [(Explicit,varP,typePType),(Explicit,identW,Vr varP)] typeStr []
+  | f == cToStr     = return $ mkProd -- (L : Type)  -> L -> Str
+    [(Explicit,varL,typeType),(Explicit,identW,Vr varL)] typeStr []
+  | f == cMapStr    = return $ mkProd -- (L : Type)  -> (Str -> Str) -> L -> L
+    [(Explicit,varL,typeType),(Explicit,identW,mkFunType [typeStr] typeStr),(Explicit,identW,Vr varL)] (Vr varL) []
+  | f == cTake      = return $ mkFunType [typeInt,typeTok] typeTok
+  | f == cTk        = return $ mkFunType [typeInt,typeTok] typeTok
+  | otherwise       = Bad (render (text "unknown in Predef:" <+> ppIdent f))
+
+varL :: Ident
+varL = identC (BS.pack "L")
+
+varP :: Ident
+varP = identC (BS.pack "P")
+
+appPredefined :: Term -> Err (Term,Bool)
+appPredefined t = case t of
+  App f x0 -> do
+   (x,_) <- appPredefined x0
+   case f of
+    -- one-place functions
+    Q mod f | mod == cPredef ->
+      case x of
+        (K s) | f == cLength -> retb $ EInt $ toInteger $ length s
+        _                    -> retb t
+
+    -- two-place functions
+    App (Q mod f) z0 | mod == cPredef -> do
+     (z,_) <- appPredefined z0
+     case (norm z, norm x) of
+      (EInt i, K s)    | f == cDrop    -> retb $ K (drop (fi i) s)
+      (EInt i, K s)    | f == cTake    -> retb $ K (take (fi i) s)
+      (EInt i, K s)    | f == cTk      -> retb $ K (take (max 0 (length s - fi i)) s)
+      (EInt i, K s)    | f == cDp      -> retb $ K (drop (max 0 (length s - fi i)) s)
+      (K s,    K t)    | f == cEqStr   -> retb $ if s == t then predefTrue else predefFalse
+      (K s,    K t)    | f == cOccur   -> retb $ if substring s t then predefTrue else predefFalse
+      (K s,    K t)    | f == cOccurs  -> retb $ if any (flip elem t) s then predefTrue else predefFalse
+      (EInt i, EInt j) | f == cEqInt   -> retb $ if i==j then predefTrue else predefFalse
+      (EInt i, EInt j) | f == cLessInt -> retb $ if i<j  then predefTrue else predefFalse
+      (EInt i, EInt j) | f == cPlus    -> retb $ EInt $ i+j
+      (_,      t)      | f == cShow    -> retb $ foldr C Empty $ map K $ words $ render (ppTerm Unqualified 0 t)
+      (_,      K s)    | f == cRead    -> retb $ Cn (identC (BS.pack s)) --- because of K, only works for atomic tags
+      (_,      t)      | f == cToStr   -> trm2str t >>= retb
+      _ -> retb t ---- prtBad "cannot compute predefined" t
+
+    -- three-place functions
+    App (App (Q mod f) z0) y0 | mod == cPredef -> do
+     (y,_) <- appPredefined y0
+     (z,_) <- appPredefined z0
+     case (z, y, x) of
+      (ty,op,t) | f == cMapStr -> 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 (retc t,True)  -- no further computing needed
+   retf t = return (retc t,False) -- must be computed further
+   retc t = case t of
+     K [] -> t
+     K s  -> foldr1 C (map K (words s))
+     _    -> t
+   norm t = case t of
+     Empty -> K []
+     C u v -> case (norm u,norm v) of
+       (K x,K y) -> K (x +++ y)
+       _ -> t
+     _ -> t
+   fi = fromInteger
+
+-- read makes variables into constants
+
+predefTrue = Q cPredef cPTrue
+predefFalse = Q cPredef cPFalse
+
+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
+  _               -> Bad (render (text "cannot get Str from term" <+> ppTerm Unqualified 0 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/Compile/Concrete/Compute.hs b/src/GF/Compile/Concrete/Compute.hs
new file mode 100644
index 000000000..5a232a2a4
--- /dev/null
+++ b/src/GF/Compile/Concrete/Compute.hs
@@ -0,0 +1,463 @@
+----------------------------------------------------------------------
+-- |
+-- Module      : GF.Compile.Concrete.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.Compile.Concrete.Compute (computeConcrete, computeTerm,computeConcreteRec) where
+
+import GF.Data.Operations
+import GF.Grammar.Grammar
+import GF.Infra.Ident
+import GF.Infra.Option
+import GF.Infra.Modules
+import GF.Data.Str
+import GF.Grammar.Printer
+import GF.Grammar.Predef
+import GF.Grammar.Macros
+import GF.Grammar.Lookup
+import GF.Compile.Refresh
+import GF.Grammar.PatternMatch
+import GF.Grammar.Lockfield (isLockLabel,unlockRecord) ----
+
+import GF.Compile.Concrete.AppPredefined
+
+import Data.List (nub,intersperse)
+import Control.Monad (liftM2, liftM)
+import Text.PrettyPrint
+
+-- | 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 = comput True where
+
+   comput full g t = ---- errIn ("subterm" +++ prt t) $ --- for debugging 
+              case t of
+
+     Q p c | p == cPredef -> return t
+           | otherwise    -> look p c 
+
+     Vr x -> do
+       t' <- maybe (Bad (render (text "no value given to variable" <+> ppIdent x))) return $ lookup x g
+       case t' of 
+         _ | t == t' -> return t
+         _ -> comp g t'
+
+     -- Abs x@(IA _) b -> do 
+     Abs _ _ _ | full -> do 
+       let (xs,b1) = termFormCnc t   
+       b' <- comp ([(x,Vr x) | (_,x) <- xs] ++ g) b1
+       return $ mkAbs xs b'
+     --  b' <- comp (ext x (Vr x) g) b
+     --  return $ Abs x b'
+     Abs _ _ _ -> return t -- hnf
+
+     Let (x,(_,a)) b -> do
+       a' <- comp g a
+       comp (ext x a' g) b
+
+     Prod b x a t -> do
+       a' <- comp g a
+       t' <- comp (ext x (Vr x) g) t
+       return $ Prod b x a' t'
+
+     -- beta-convert
+     App f a -> case appForm t of
+      (h,as) | length as > 1 -> do
+        h' <- hnf g h
+        as' <- mapM (comp g) as
+        case h' of
+          _ | not (null [() | FV _ <- as']) -> compApp g (mkApp h' as')
+          c@(QC _ _) -> do
+            return $ mkApp c as'
+          Q mod f | mod == cPredef -> do     
+            (t',b) <- appPredefined (mkApp h' as')
+            if b then return t' else comp g t'
+
+          Abs _ _ _ -> do
+            let (xs,b) = termFormCnc h'
+            let g' = (zip (map snd xs) as') ++ g
+            let as2 = drop (length xs) as'
+            let xs2 = drop (length as') xs
+            b' <- comp g' (mkAbs xs2 b)
+            if null as2 then return b' else comp g (mkApp b' as2)
+
+          _ -> compApp g (mkApp h' as')
+      _ -> compApp 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 (Bad (render (text "no value for label" <+> ppLabel 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)
+--- - } ---
+
+         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 v -> do
+       t' <- compTable g t
+       v' <- comp g v
+       t1 <- case t' of
+----           V (RecType fs) _         -> uncurrySelect g fs t' v'
+----           T (TComp (RecType fs)) _ -> uncurrySelect g fs t' v'
+           _ -> return $ S t' v'
+       compSelect g t1
+
+     -- 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
+
+         (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 (d,aa) -> do
+       d' <- comp g d
+       aa' <- mapM (compInAlts g) aa
+       returnC (Alts (d',aa'))
+
+     -- 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
+         (R rs, R ss) -> plusRecord r' s'
+         (RecType rs, RecType ss) -> plusRecType r' s'
+         _ -> return $ ExtR r' s'
+
+     ELin c r -> do
+       r' <- comp g r
+       unlockRecord c r'
+
+     T _ _ -> compTable g t
+     V _ _ -> compTable g t
+
+     -- otherwise go ahead
+     _ -> composOp (comp g) t >>= returnC
+
+    where
+
+     compApp g (App f a) = do
+       f' <- hnf 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'
+
+         (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'
+
+     hnf  = comput False
+     comp = comput True
+
+     look p c
+       | rec       = lookupResDef gr p c >>= comp []
+       | otherwise = lookupResDef gr p c
+
+     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
+
+     compPatternMacro p = case p of
+       PM m c -> case look m c of
+         Ok (EPatt p') -> compPatternMacro p'
+         _ -> Bad (render (text "pattern expected as value of" $$ nest 2 (ppPatt Unqualified 0 p)))
+       PAs x p -> do
+         p' <- compPatternMacro p
+         return $ PAs x p'
+       PAlt p q -> do
+         p' <- compPatternMacro p
+         q' <- compPatternMacro q
+         return $ PAlt p' q'
+       PSeq p q -> do
+         p' <- compPatternMacro p
+         q' <- compPatternMacro q
+         return $ PSeq p' q'
+       PRep p -> do
+         p' <- compPatternMacro p
+         return $ PRep p'
+       PNeg p -> do
+         p' <- compPatternMacro p
+         return $ PNeg p'
+       PR rs -> do
+         rs' <- mapPairsM compPatternMacro rs
+         return $ PR rs'
+
+       _ -> return p
+
+     compSelect g (S t' 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 _ [(PW,c)] -> comp g c           --- an optimization
+         T _ [(PT _ PW,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 -> case v' of
+           Val _ _ i -> comp g $ ts !! i
+           _ -> do
+             vs <- allParamValues gr ptyp
+             case lookupR v' (zip vs [0 .. length vs - 1]) of
+               Just i -> comp g $ ts !! i
+               _ -> return $ S t' v' -- if v' is not canonical
+         T _ cc -> do
+           let v2 = case v' of
+                 Val te _ _ -> te
+                 _ -> v'
+           case matchPattern cc v2 of
+             Ok (c,g') -> comp (g' ++ g) c
+             _ | isCan v2 -> Bad (render (text "missing case" <+> ppTerm Unqualified 0 v2 <+> text "in" <+> ppTerm Unqualified 0 t))
+             _ -> return $ S t' v' -- if v' is not canonical
+
+         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'
+
+     --- needed to match records with and without type information
+     ---- todo: eliminate linear search in a list of records!
+     lookupR v vs = case v of
+       R rs -> lookup ([(x,y) | (x,(_,y)) <- rs]) 
+                                [([(x,y) | (x,(_,y)) <- rs],v) | (R rs,v) <- vs]
+       _ -> lookup v vs
+
+     -- case-expand tables
+     -- if already expanded, don't expand again
+     compTable g t = case t of
+         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'
+         V ty cs -> do
+           ty' <- comp g ty
+           -- if there are no variables, don't even go inside
+           cs' <- if (null g) then return cs else mapM (comp g) cs
+           return $ V ty' cs'
+
+         T i cs -> do
+           pty0 <- getTableType i
+           ptyp <- comp g pty0
+           case allParamValues gr ptyp of
+             Ok vs0 -> do
+               let vs = vs0 ---- [Val v ptyp i | (v,i) <- zip vs0 [0..]]
+               ps0  <- mapM (compPatternMacro . fst) cs
+               cs'  <- mapM (compBranchOpt g) (zip ps0 (map snd cs))
+               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, just course of values
+               return $ T (TComp ptyp) (zip ps' ts)
+             _ -> do
+               ps0  <- mapM (compPatternMacro . fst) cs
+               cs'  <- mapM (compBranch g) (zip ps0 (map snd cs))
+
+----               cs' <- mapM (compBranch g) cs
+               return $ T i cs'  -- happens with variable types
+         _ -> comp g t
+
+     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
+
+     compInAlts g (v,c) = do
+       v' <- comp g v
+       c' <- comp g c
+       c2 <- case c' of
+         EPatt p -> liftM Strs $ getPatts p
+         _ -> return c'
+       return (v',c2)
+      where
+       getPatts p = case p of
+         PAlt a b  -> liftM2 (++) (getPatts a) (getPatts b)
+         PString s -> return [K s]
+         PSeq a b  -> do
+           as <- getPatts a
+           bs <- getPatts b
+           return [K (s ++ t) | K s <- as, K t <- bs]
+         _ -> fail (render (text "not valid pattern in pre expression" <+> ppPatt Unqualified 0 p))
+
+{- ----
+     uncurrySelect g fs t v = do
+       ts <- mapM (allParamValues gr . snd) fs
+       vs <- mapM (comp g) [P v r | r <- map fst fs]
+       return $ reorderSelect t fs ts vs
+
+     reorderSelect t fs pss vs = case (t,fs,pss,vs) of
+       (V _ ts, f:fs1, ps:pss1, v:vs1) -> 
+         S (V (snd f) 
+             [reorderSelect (V (RecType fs1) t) fs1 pss1 vs1 | 
+               t <- segments (length ts `div` length ps) ts]) v 
+       (T (TComp _) cs, f:fs1, ps:pss1, v:vs1) -> 
+         S (T (TComp (snd f)) 
+             [(p,reorderSelect (T (TComp (RecType fs1)) c) fs1 pss1 vs1) | 
+               (ep,c) <- zip ps (segments (length cs `div` length ps) cs),
+               let Ok p = term2patt ep]) v 
+       _ -> t
+
+     segments i xs = 
+       let (x0,xs1) = splitAt i xs in x0 : takeWhile (not . null) (segments i xs1)
+-}
+
+
+-- | argument variables cannot be glued
+checkNoArgVars :: Term -> Err Term
+checkNoArgVars t = case t of
+  Vr (IA _ _)    -> Bad $ glueErrorMsg $ ppTerm Unqualified 0 t 
+  Vr (IAV _ _ _) -> Bad $ glueErrorMsg $ ppTerm Unqualified 0 t 
+  _ -> composOp checkNoArgVars t
+
+glueErrorMsg s = 
+  render (text "Cannot glue (+) term with run-time variable" <+> s <> char '.' $$
+          text "Use Prelude.bind instead.")
+
+getArgType t = case t of
+  V ty _ -> return ty
+  T (TComp ty) _ -> return ty
+  _ -> Bad (render (text "cannot get argument type of table" $$ nest 2 (ppTerm Unqualified 0 t)))
diff --git a/src/GF/Compile/Concrete/TypeCheck.hs b/src/GF/Compile/Concrete/TypeCheck.hs
new file mode 100644
index 000000000..e5d2a9160
--- /dev/null
+++ b/src/GF/Compile/Concrete/TypeCheck.hs
@@ -0,0 +1,693 @@
+{-# LANGUAGE PatternGuards #-}
+module GF.Compile.Concrete.TypeCheck( checkLType, inferLType, computeLType, ppType ) where
+
+import GF.Infra.CheckM
+import GF.Infra.Modules
+import GF.Data.Operations
+
+import GF.Grammar
+import GF.Grammar.Lookup
+import GF.Grammar.Predef
+import GF.Grammar.PatternMatch
+import GF.Grammar.Lockfield (isLockLabel, lockRecType, unlockRecord)
+import GF.Compile.Concrete.AppPredefined
+
+import Data.List
+import Control.Monad
+import Text.PrettyPrint
+
+computeLType :: SourceGrammar -> Context -> Type -> Check Type
+computeLType gr g0 t = comp (reverse [(b,x, Vr x) | (b,x,_) <- g0] ++ g0) t
+ where
+  comp g ty = case ty of
+    _ | Just _ <- isTypeInts ty -> return ty ---- shouldn't be needed
+      | isPredefConstant ty     -> return ty ---- shouldn't be needed
+
+    Q m ident -> checkIn (text "module" <+> ppIdent m) $ do
+      ty' <- checkErr (lookupResDef gr m ident) 
+      if ty' == ty then return ty else comp g ty' --- is this necessary to test?
+
+    Vr ident  -> checkLookup ident g -- never needed to compute!
+
+    App f a -> do
+      f' <- comp g f
+      a' <- comp g a
+      case f' of
+        Abs b x t -> comp ((b,x,a'):g) t
+        _ -> return $ App f' a'
+
+    Prod bt x a b -> do
+      a' <- comp g a
+      b' <- comp ((bt,x,Vr x) : g) b
+      return $ Prod bt x a' b'
+
+    Abs bt x b -> do
+      b' <- comp ((bt,x,Vr x):g) b
+      return $ Abs bt x b'
+
+    ExtR r s -> do
+      r' <- comp g r
+      s' <- comp g s
+      case (r',s') of
+        (RecType rs, RecType ss) -> checkErr (plusRecType r' s') >>= comp g
+        _ -> return $ ExtR r' s'
+
+    RecType fs -> do
+      let fs' = sortRec fs
+      liftM RecType $ mapPairsM (comp g) fs'
+
+    ELincat c t -> do
+      t' <- comp g t
+      checkErr $ lockRecType c t' ---- locking to be removed AR 20/6/2009
+
+    _ | ty == typeTok -> return typeStr
+    _ | isPredefConstant ty -> return ty
+
+    _ -> composOp (comp g) ty
+
+-- the underlying algorithms
+
+inferLType :: SourceGrammar -> Context -> Term -> Check (Term, Type)
+inferLType gr g 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) >>= computeLType gr g
+     ,
+     checkErr (lookupResDef gr m ident) >>= inferLType gr g
+     ,
+     checkError (text "cannot infer type of constant" <+> ppTerm Unqualified 0 trm)
+     ]
+
+   QC m ident | isPredef m -> termWith trm $ checkErr (typPredefined ident)
+
+   QC m ident -> checks [
+       termWith trm $ checkErr (lookupResType gr m ident) >>= computeLType gr g
+       ,
+       checkErr (lookupResDef gr m ident) >>= inferLType gr g
+       ,
+       checkError (text "cannot infer type of canonical constant" <+> ppTerm Unqualified 0 trm)
+       ]
+
+   Val _ ty i -> termWith trm $ return ty
+
+   Vr ident -> termWith trm $ checkLookup ident g
+
+   Typed e t -> do
+     t' <- computeLType gr g t
+     checkLType gr g e t'
+     return (e,t')
+
+   App f a -> do
+     over <- getOverload gr g Nothing trm
+     case over of
+       Just trty -> return trty
+       _ -> do
+         (f',fty) <- inferLType gr g f
+         fty' <- computeLType gr g fty
+         case fty' of
+           Prod bt z arg val -> do 
+             a' <- justCheck g a arg
+             ty <- if isWildIdent z 
+                      then return val
+                      else substituteLType [(bt,z,a')] val
+             return (App f' a',ty) 
+           _ -> checkError (text "A function type is expected for" <+> ppTerm Unqualified 0 f <+> text "instead of type" <+> ppType fty)
+
+   S f x -> do
+     (f', fty) <- inferLType gr g f
+     case fty of
+       Table arg val -> do
+         x'<- justCheck g x arg
+         return (S f' x', val)
+       _ -> checkError (text "table lintype expected for the table in" $$ nest 2 (ppTerm Unqualified 0 trm))
+
+   P t i -> do
+     (t',ty) <- inferLType gr g t   --- ??
+     ty' <- computeLType gr g ty
+     let tr2 = P t' i
+     termWith tr2 $ case ty' of
+       RecType ts -> case lookup i ts of
+                       Nothing -> checkError (text "unknown label" <+> ppLabel i <+> text "in" $$ nest 2 (ppTerm Unqualified 0 ty'))
+                       Just x  -> return x
+       _          -> checkError (text "record type expected for:" <+> ppTerm Unqualified 0 t $$
+                                 text " instead of the inferred:" <+> ppTerm Unqualified 0 ty')
+   PI t i _ -> inferLType gr g $ P t i
+
+   R r -> do
+     let (ls,fs) = unzip r
+     fsts <- mapM inferM fs
+     let ts = [ty | (Just ty,_) <- fsts]
+     checkCond (text "cannot infer type of record" $$ nest 2 (ppTerm Unqualified 0 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
+     checkLType gr g trm (Table arg val)
+   T (TComp arg) pts -> do
+     (_,val) <- checks $ map (inferCase (Just arg)) pts
+     checkLType gr g 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 
+       [] -> checkError (text "cannot infer table type of" <+> ppTerm Unqualified 0 trm)
+----       PInt k : _ -> return $ Ints $ max [i | PInt i <- pts'] 
+       _  -> do 
+         (arg,val) <- checks $ map (inferCase Nothing) pts'
+         checkLType gr g trm (Table arg val)
+   V arg pts -> do
+     (_,val) <- checks $ map (inferLType gr g) pts
+     return (trm, Table arg val)
+
+   K s  -> do
+     if elem ' ' s
+        then do
+          let ss = foldr C Empty (map K (words s))  
+          ----- removed irritating warning AR 24/5/2008
+          ----- checkWarn ("token \"" ++ s ++ 
+          -----              "\" converted to token list" ++ prt ss)
+          return (ss, typeStr)
+        else return (trm, typeStr)
+
+   EInt i -> return (trm, typeInt)
+
+   EFloat i -> return (trm, typeFloat)
+
+   Empty -> return (trm, typeStr)
+
+   C s1 s2 -> 
+     check2 (flip (justCheck g) typeStr) C s1 s2 typeStr
+
+   Glue s1 s2 -> 
+     check2 (flip (justCheck g) typeStr) Glue s1 s2 typeStr ---- typeTok
+
+---- hack from Rename.identRenameTerm, to live with files with naming conflicts 18/6/2007
+   Strs (Cn c : ts) | c == cConflict -> do
+     checkWarn (text "unresolved constant, could be any of" <+> hcat (map (ppTerm Unqualified 0) ts))
+     inferLType gr g (head ts)
+
+   Strs ts -> do
+     ts' <- mapM (\t -> justCheck g t typeStr) ts 
+     return (Strs ts', typeStrs)
+
+   Alts (t,aa) -> do
+     t'  <- justCheck g t typeStr
+     aa' <- flip mapM aa (\ (c,v) -> do
+        c' <- justCheck g c typeStr 
+        v' <- checks $ map (justCheck g v) [typeStrs, EPattType typeStr]
+        return (c',v'))
+     return (Alts (t',aa'), typeStr)
+
+   RecType r -> do
+     let (ls,ts) = unzip r
+     ts' <- mapM (flip (justCheck g) typeType) ts 
+     return (RecType (zip ls ts'), typeType)
+
+   ExtR r s -> do
+     (r',rT) <- inferLType gr g r 
+     rT'     <- computeLType gr g rT
+     (s',sT) <- inferLType gr g s
+     sT'     <- computeLType gr g 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'
+         checkLType gr g trm' rt ---- return (trm', rt)
+       _ | rT' == typeType && sT' == typeType -> return (trm', typeType)
+       _ -> checkError (text "records or record types expected in" <+> ppTerm Unqualified 0 trm)
+
+   Sort _     -> 
+     termWith trm $ return typeType
+
+   Prod bt x a b -> do
+     a' <- justCheck g a typeType
+     b' <- justCheck ((bt,x,a'):g) b typeType
+     return (Prod bt x a' b', typeType)
+
+   Table p t  -> do
+     p' <- justCheck g p typeType --- check p partype! 
+     t' <- justCheck g t typeType
+     return $ (Table p' t', typeType)
+
+   FV vs -> do
+     (_,ty) <- checks $ map (inferLType gr g) vs
+---     checkIfComplexVariantType trm ty
+     checkLType gr g trm ty
+
+   EPattType ty -> do
+     ty' <- justCheck g ty typeType
+     return (EPattType ty',typeType)
+   EPatt p -> do
+     ty <- inferPatt p
+     return (trm, EPattType ty)
+
+   ELin c trm -> do
+     (trm',ty) <- inferLType gr g trm
+     ty' <- checkErr $ lockRecType c ty ---- lookup c; remove lock AR 20/6/2009
+     return $ (ELin c trm', ty') 
+
+   _ -> checkError (text "cannot infer lintype of" <+> ppTerm Unqualified 0 trm)
+
+ where
+   isPredef m = elem m [cPredef,cPredefAbs]
+
+   justCheck g ty te = checkLType gr g ty te >>= return . fst
+
+   -- for record fields, which may be typed
+   inferM (mty, t) = do
+     (t', ty') <- case mty of
+       Just ty -> checkLType gr g ty t
+       _ -> inferLType gr g t
+     return (Just ty',t')
+
+   inferCase mty (patt,term) = do
+     arg  <- maybe (inferPatt patt) return mty
+     cont <- pattContext gr g arg patt
+     (_,val) <- inferLType gr (reverse cont ++ g) term
+     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
+     PChar -> True
+     PChars _ -> 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 $ liftM valTypeCnc (lookupResType gr q c)
+     PAs _ p  -> inferPatt p
+     PNeg p   -> inferPatt p
+     PAlt p q -> checks [inferPatt p, inferPatt q]
+     PSeq _ _ -> return $ typeStr
+     PRep _   -> return $ typeStr
+     PChar    -> return $ typeStr
+     PChars _ -> return $ typeStr
+     _ -> inferLType gr g (patt2term p) >>= return . snd
+
+
+-- type inference: Nothing, type checking: Just t
+-- the latter permits matching with value type
+getOverload :: SourceGrammar -> Context -> Maybe Type -> Term -> Check (Maybe (Term,Type))
+getOverload gr g mt ot = case appForm ot of
+     (f@(Q m c), ts) -> case lookupOverload gr m c of
+       Ok typs -> do
+         ttys <- mapM (inferLType gr g) ts
+         v <- matchOverload f typs ttys
+         return $ Just v
+       _ -> return Nothing
+     _ -> return Nothing
+ where
+   matchOverload f typs ttys = do
+     let (tts,tys) = unzip ttys
+     let vfs = lookupOverloadInstance tys typs
+     let matches = [vf | vf@((v,_),_) <- vfs, matchVal mt v]
+
+     case ([vf | (vf,True) <- matches],[vf | (vf,False) <- matches]) of
+       ([(val,fun)],_) -> return (mkApp fun tts, val)
+       ([],[(val,fun)]) -> do
+         checkWarn (text "ignoring lock fields in resolving" <+> ppTerm Unqualified 0 ot) 
+         return (mkApp fun tts, val)
+       ([],[]) -> do
+         let showTypes ty = hsep (map ppType ty)
+         checkError $ text "no overload instance of" <+> ppTerm Unqualified 0 f $$
+                      text "for" $$
+                      nest 2 (showTypes tys) $$
+                      text "among" $$
+                      nest 2 (vcat [showTypes ty | (ty,_) <- typs]) $$
+                      maybe empty (\x -> text "with value type" <+> ppType x) mt
+
+       (vfs1,vfs2) -> case (noProds vfs1,noProds vfs2) of
+         ([(val,fun)],_) -> do
+           return (mkApp fun tts, val)
+         ([],[(val,fun)]) -> do
+           checkWarn (text "ignoring lock fields in resolving" <+> ppTerm Unqualified 0 ot) 
+           return (mkApp fun tts, val)
+
+----- unsafely exclude irritating warning AR 24/5/2008
+-----           checkWarn $ "overloading of" +++ prt f +++ 
+-----             "resolved by excluding partial applications:" ++++
+-----             unlines [prtType env ty | (ty,_) <- vfs', not (noProd ty)]
+
+
+         _ -> checkError $ text "ambiguous overloading of" <+> ppTerm Unqualified 0 f <+>
+                           text "for" <+> hsep (map ppType tys) $$ 
+                           text "with alternatives" $$
+                           nest 2 (vcat [ppType ty | (ty,_) <- if null vfs1 then vfs2 else vfs2])
+
+   matchVal mt v = elem mt [Nothing,Just v,Just (unlocked v)]
+
+   unlocked v = case v of
+     RecType fs -> RecType $ filter (not . isLockLabel . fst) fs
+     _ -> v
+   ---- TODO: accept subtypes
+   ---- TODO: use a trie
+   lookupOverloadInstance tys typs = 
+     [((mkFunType rest val, t),isExact) | 
+       let lt = length tys,
+       (ty,(val,t)) <- typs, length ty >= lt,
+       let (pre,rest) = splitAt lt ty, 
+       let isExact = pre == tys,
+       isExact || map unlocked pre == map unlocked tys
+     ]
+
+   noProds vfs = [(v,f) | (v,f) <- vfs, noProd v]
+
+   noProd ty = case ty of
+     Prod _ _ _ _ -> False
+     _ -> True
+
+checkLType :: SourceGrammar -> Context -> Term -> Type -> Check (Term, Type)
+checkLType gr g trm typ0 = do
+
+  typ <- computeLType gr g typ0
+
+  case trm of
+
+    Abs bt x c -> do
+      case typ of
+        Prod bt' z a b -> do 
+          (c',b') <- if isWildIdent z
+                       then checkLType gr ((bt,x,a):g) c b
+                       else do b' <- checkIn (text "abs") $ substituteLType [(bt',z,Vr x)] b
+                               checkLType gr ((bt,x,a):g) c b'
+          return $ (Abs bt x c', Prod bt' x a b')
+        _ -> checkError $ text "function type expected instead of" <+> ppType typ
+
+    App f a -> do
+       over <- getOverload gr g (Just typ) trm
+       case over of
+         Just trty -> return trty
+         _ -> do
+          (trm',ty') <- inferLType gr g trm
+          termWith trm' $ checkEqLType gr g typ ty' trm'
+
+    Q _ _ -> do
+       over <- getOverload gr g (Just typ) trm
+       case over of
+         Just trty -> return trty
+         _ -> do
+          (trm',ty') <- inferLType gr g trm
+          termWith trm' $ checkEqLType gr g typ ty' trm'
+
+    T _ [] ->
+      checkError (text "found empty table in type" <+> ppTerm Unqualified 0 typ)
+    T _ cs -> case typ of 
+      Table arg val -> do 
+        case allParamValues gr arg of
+          Ok vs -> do
+            let ps0 = map fst cs
+            ps <- checkErr $ testOvershadow ps0 vs
+            if null ps 
+              then return () 
+              else checkWarn (text "patterns never reached:" $$
+                              nest 2 (vcat (map (ppPatt Unqualified 0) ps)))
+          _ -> return () -- happens with variable types
+        cs' <- mapM (checkCase arg val) cs
+        return (T (TTyped arg) cs', typ)
+      _ -> checkError $ text "table type expected for table instead of" $$ nest 2 (ppType 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
+
+       _ -> checkError (text "record type expected in type checking instead of" $$ nest 2 (ppTerm Unqualified 0 typ))
+
+    ExtR r s -> case typ of
+       _ | typ == typeType -> do
+         trm' <- computeLType gr g trm
+         case trm' of
+           RecType _ -> termWith trm $ return typeType
+           ExtR (Vr _) (RecType _) -> termWith trm $ return typeType 
+                                      -- ext t = t ** ...
+           _ -> checkError (text "invalid record type extension" <+> nest 2 (ppTerm Unqualified 0 trm))
+       RecType rr -> do
+         (r',ty,s') <- checks [
+            do (r',ty) <- inferLType gr g r
+               return (r',ty,s)
+           ,
+            do (s',ty) <- inferLType gr g s
+               return (s',ty,r)
+            ]
+         case ty of
+           RecType rr1 -> do
+                let (rr0,rr2) = recParts rr rr1
+                r2 <- justCheck g r' rr0
+                s2 <- justCheck g s' rr2
+                return $ (ExtR r2 s2, typ) 
+           _ -> checkError (text "record type expected in extension of" <+> ppTerm Unqualified 0 r $$
+                            text "but found" <+> ppTerm Unqualified 0 ty)
+
+       ExtR ty ex -> do
+         r' <- justCheck g r ty
+         s' <- justCheck g s ex
+         return $ (ExtR r' s', typ) --- is this all?
+
+       _ -> checkError (text "record extension not meaningful for" <+> ppTerm Unqualified 0 typ)
+
+    FV vs -> do
+      ttys <- mapM (flip (checkLType gr g) typ) vs
+---      checkIfComplexVariantType trm typ
+      return (FV (map fst ttys), typ) --- typ' ?
+
+    S tab arg -> checks [ do
+      (tab',ty) <- inferLType gr g tab
+      ty'       <- computeLType gr g ty
+      case ty' of
+        Table p t -> do
+          (arg',val) <- checkLType gr g arg p
+          checkEqLType gr g typ t trm
+          return (S tab' arg', t)
+        _ -> checkError (text "table type expected for applied table instead of" <+> ppType ty')
+     , do
+      (arg',ty) <- inferLType gr g arg
+      ty'       <- computeLType gr g ty
+      (tab',_)  <- checkLType gr g tab (Table ty' typ)
+      return (S tab' arg', typ)
+      ]
+    Let (x,(mty,def)) body -> case mty of
+      Just ty -> do
+        (def',ty') <- checkLType gr g def ty
+        body' <- justCheck ((Explicit,x,ty'):g) body typ
+        return (Let (x,(Just ty',def')) body', typ)
+      _ -> do
+        (def',ty) <- inferLType gr g def  -- tries to infer type of local constant
+        checkLType gr g (Let (x,(Just ty,def')) body) typ
+
+    ELin c tr -> do
+      tr1 <- checkErr $ unlockRecord c tr
+      checkLType gr g tr1 typ
+
+    _ -> do
+      (trm',ty') <- inferLType gr g trm
+      termWith trm' $ checkEqLType gr g typ ty' trm'
+ where
+   justCheck g ty te = checkLType gr g ty te >>= return . fst
+
+   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
+       checkEqLType gr g ty ty0 t
+       (t',ty') <- checkLType gr g t ty
+       return (l,(Just ty',t'))
+     Just (_,t) -> do
+       (t',ty') <- checkLType gr g t ty
+       return (l,(Just ty',t'))
+     _ -> checkError $ 
+            if isLockLabel l 
+              then let cat = drop 5 (showIdent (label2ident l))
+                   in ppTerm Unqualified 0 (R rms) <+> text "is not in the lincat of" <+> text cat <> 
+                      text "; try wrapping it with lin" <+> text cat
+              else text "cannot find value for label" <+> ppLabel l <+> text "in" <+> ppTerm Unqualified 0 (R rms)
+
+   checkCase arg val (p,t) = do
+     cont <- pattContext gr g arg p
+     t' <- justCheck (reverse cont ++ g) t val
+     return (p,t')
+
+pattContext :: SourceGrammar -> Context -> Type -> Patt -> Check Context
+pattContext env g typ p = case p of
+  PV x -> return [(Explicit,x,typ)]
+  PP q c ps | q /= cPredef -> do ---- why this /=? AR 6/1/2006
+    t <- checkErr $ lookupResType env q c
+    let (cont,v) = typeFormCnc t
+    checkCond (text "wrong number of arguments for constructor in" <+> ppPatt Unqualified 0 p) 
+              (length cont == length ps)
+    checkEqLType env g typ v (patt2term p)
+    mapM (\((_,_,ty),p) -> pattContext env g ty p) (zip cont ps) >>= return . concat
+  PR r -> do
+    typ' <- computeLType env g 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 g)) pts >>= return . concat
+      _ -> checkError (text "record type expected for pattern instead of" <+> ppTerm Unqualified 0 typ')
+  PT t p' -> do
+    checkEqLType env g typ t (patt2term p')
+    pattContext env g typ p'
+
+  PAs x p -> do
+    g' <- pattContext env g typ p
+    return ((Explicit,x,typ):g')
+
+  PAlt p' q -> do
+    g1 <- pattContext env g typ p'
+    g2 <- pattContext env g typ q
+    let pts = nub ([x | pt@(_,x,_) <- g1, notElem pt g2] ++ [x | pt@(_,x,_) <- g2, notElem pt g1])
+    checkCond 
+      (text "incompatible bindings of" <+>
+       fsep (map ppIdent pts) <+> 
+       text "in pattern alterantives" <+> ppPatt Unqualified 0 p) (null pts) 
+    return g1 -- must be g1 == g2
+  PSeq p q -> do
+    g1 <- pattContext env g typ p
+    g2 <- pattContext env g typ q
+    return $ g1 ++ g2
+  PRep p' -> noBind typeStr p'
+  PNeg p' -> noBind typ p'
+
+  _ -> return [] ---- check types!
+ where 
+   noBind typ p' = do
+    co <- pattContext env g typ p'
+    if not (null co)
+      then checkWarn (text "no variable bound inside pattern" <+> ppPatt Unqualified 0 p) 
+           >> return []
+      else return []
+
+checkEqLType :: SourceGrammar -> Context -> Type -> Type -> Term -> Check Type
+checkEqLType gr g t u trm = do
+  (b,t',u',s) <- checkIfEqLType gr g t u trm
+  case b of
+    True  -> return t'
+    False -> checkError $ text s <+> text "type of" <+> ppTerm Unqualified 0 trm $$
+                          text "expected:" <+> ppType t $$
+                          text "inferred:" <+> ppType u
+
+checkIfEqLType :: SourceGrammar -> Context -> Type -> Type -> Term -> Check (Bool,Type,Type,String)
+checkIfEqLType gr g t u trm = do
+  t' <- computeLType gr g t
+  u' <- computeLType gr g 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 $ text "missing lock field" <+> fsep (map ppLabel 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
+     (_,u) | u == typeError -> 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
+     (t,u) | Just m <- isTypeInts t, Just n <- isTypeInts t -> m >= n
+           | Just _ <- isTypeInts t, u == typeInt           -> True ---- check size!
+           | t == typeInt,           Just _ <- isTypeInts u -> True ---- why this ???? AR 11/12/2005
+
+     ---- this should be made in Rename
+     (Q  m a, Q  n b) | a == b -> elem m (allExtendsPlus gr n) 
+                               || elem n (allExtendsPlus gr m)
+                               || m == n --- for Predef
+     (QC m a, QC n b) | a == b -> elem m (allExtendsPlus gr n) 
+                               || elem n (allExtendsPlus gr m)
+     (QC m a, Q  n b) | a == b -> elem m (allExtendsPlus gr n) 
+                               || elem n (allExtendsPlus gr m)
+     (Q  m a, QC n b) | a == b -> elem m (allExtendsPlus gr n) 
+                               || elem n (allExtendsPlus gr 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 $ render (text "missing record fields:" <+> fsep (punctuate comma (map ppLabel 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]
+
+-- auxiliaries
+
+-- | 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 [(x,t) | (_,x,t) <- g]
+  _ -> composOp (substituteLType g) t
+
+termWith :: Term -> Check Type -> Check (Term, Type)
+termWith t ct = do
+  ty <- ct
+  return (t,ty)
+
+-- | 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)
+
+-- printing a type with a lock field lock_C as C
+ppType :: Type -> Doc
+ppType ty =
+  case ty of
+    RecType fs   -> case filter isLockLabel $ map fst fs of
+                      [lock] -> text (drop 5 (showIdent (label2ident lock)))
+                      _      -> ppTerm Unqualified 0 ty
+    Prod _ x a b -> ppType a <+> text "->" <+> ppType b
+    _            -> ppTerm Unqualified 0 ty
+
+checkLookup :: Ident -> Context -> Check Type
+checkLookup x g =
+  case [ty | (b,y,ty) <- g, x == y] of
+    []     -> checkError (text "unknown variable" <+> ppIdent x)
+    (ty:_) -> return ty
diff --git a/src/GF/Compile/GrammarToGFCC.hs b/src/GF/Compile/GrammarToGFCC.hs
index 9d0a45e41..2a31d2b75 100644
--- a/src/GF/Compile/GrammarToGFCC.hs
+++ b/src/GF/Compile/GrammarToGFCC.hs
@@ -16,7 +16,7 @@ import GF.Grammar.Grammar
 import qualified GF.Grammar.Lookup as Look
 import qualified GF.Grammar as A
 import qualified GF.Grammar.Macros as GM
-import qualified GF.Compile.Compute as Compute ---- 
+import qualified GF.Compile.Concrete.Compute as Compute ---- 
 import qualified GF.Infra.Modules as M
 import qualified GF.Infra.Option as O
 
diff --git a/src/GF/Compile/Optimize.hs b/src/GF/Compile/Optimize.hs
index cb0d6059a..c5b244903 100644
--- a/src/GF/Compile/Optimize.hs
+++ b/src/GF/Compile/Optimize.hs
@@ -23,7 +23,7 @@ import GF.Grammar.Macros
 import GF.Grammar.Lookup
 import GF.Grammar.Predef
 import GF.Compile.Refresh
-import GF.Compile.Compute
+import GF.Compile.Concrete.Compute
 import GF.Compile.BackOpt
 import GF.Compile.CheckGrammar
 import GF.Compile.Update
diff --git a/src/GF/Compile/Rename.hs b/src/GF/Compile/Rename.hs
index aea39e632..d037aaafc 100644
--- a/src/GF/Compile/Rename.hs
+++ b/src/GF/Compile/Rename.hs
@@ -35,7 +35,6 @@ import GF.Infra.Ident
 import GF.Infra.CheckM
 import GF.Grammar.Macros
 import GF.Grammar.Printer
-import GF.Grammar.AppPredefined
 import GF.Grammar.Lookup
 import GF.Grammar.Printer
 import GF.Data.Operations
diff --git a/src/GF/Compile/TC.hs b/src/GF/Compile/TC.hs
deleted file mode 100644
index c319cbd4a..000000000
--- a/src/GF/Compile/TC.hs
+++ /dev/null
@@ -1,294 +0,0 @@
-----------------------------------------------------------------------
--- |
--- 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.Compile.TC (AExp(..),
-	   Theory,
-	   checkExp,
-	   inferExp,
-	   checkBranch,
-	   eqVal,
-	   whnf
-	  ) where
-
-import GF.Data.Operations
-import GF.Grammar
-import GF.Grammar.Predef
-
-import Control.Monad
-import Data.List (sortBy)
-import Data.Maybe
-import Text.PrettyPrint
-
-data AExp =
-     AVr   Ident Val 
-   | ACn   QIdent Val
-   | AType 
-   | AInt  Integer 
-   | AFloat Double
-   | AStr  String
-   | AMeta MetaId Val
-   | AApp  AExp AExp Val 
-   | AAbs  Ident Val AExp 
-   | AProd Ident AExp AExp 
-   | AEqs  [([Exp],AExp)] --- not used
-   | ARecType [ALabelling]
-   | AR    [AAssign]
-   | AP    AExp Label Val
-   | AData Val
-  deriving (Eq,Show)
-
-type ALabelling = (Label, AExp) 
-type AAssign = (Label, (Val, AExp))
-
-type Theory = QIdent -> Err Val
-
-lookupConst :: Theory -> QIdent -> Err Val
-lookupConst th f = th f
-
-lookupVar :: Env -> Ident -> Err Val
-lookupVar g x = maybe (Bad (render (text "unknown variable" <+> ppIdent 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)
-  RecType xs -> do xs <- mapM (\(l,e) -> eval env e >>= \e -> return (l,e)) xs
-                   return (VRecType xs)
-  _ -> 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,[])
-
-    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)
-      _ -> Bad (render (text "function type expected for" <+> ppTerm Unqualified 0 e <+> text "instead of" <+> ppValue Unqualified 0 typ))
-
-    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)
-
-    R xs -> 
-      case typ of
-        VRecType ys -> do case [l | (l,_) <- ys, isNothing (lookup l xs)] of
-                            [] -> return ()
-                            ls -> fail (render (text "no value given for label:" <+> fsep (punctuate comma (map ppLabel ls))))
-                          r <- mapM (checkAssign th tenv ys) xs
-                          let (xs,css) = unzip r
-                          return (AR xs, concat css)
-        _           -> Bad (render (text "record type expected for" <+> ppTerm Unqualified 0 e <+> text "instead of" <+> ppValue Unqualified 0 typ))
-
-    P r l -> do (r',cs) <- checkExp th tenv r (VRecType [(l,typ)])
-                return (AP r' l typ,cs)
-
-    _ -> 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 && isPredefCat c
-                     -> 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, [])
-   RecType xs -> do r <- mapM (checkLabelling th tenv) xs
-                    let (xs,css) = unzip r
-                    return (ARecType xs, vType, concat css)
-   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)
-      _ -> Bad (render (text "Prod expected for function" <+> ppTerm Unqualified 0 f <+> text "instead of" <+> ppValue Unqualified 0 typ))
-   _ -> Bad (render (text "cannot infer type of expression" <+> ppTerm Unqualified 0 e))
-
-checkLabelling :: Theory -> TCEnv -> Labelling -> Err (ALabelling, [(Val,Val)])
-checkLabelling th tenv (lbl,typ) = do
-  (atyp,cs) <- checkType th tenv typ
-  return ((lbl,atyp),cs)
-
-checkAssign :: Theory -> TCEnv -> [(Label,Val)] -> Assign -> Err (AAssign, [(Val,Val)])
-checkAssign th tenv@(k,rho,gamma) typs (lbl,(Just typ,exp)) = do
-  (atyp,cs1) <- checkType th tenv typ
-  val <- eval rho typ
-  cs2 <- case lookup lbl typs of
-           Nothing   -> return []
-           Just val0 -> eqVal k val val0
-  (aexp,cs3) <- checkExp th tenv exp val
-  return ((lbl,(val,aexp)),cs1++cs2++cs3)
-checkAssign th tenv@(k,rho,gamma) typs (lbl,(Nothing,exp)) = do
-  case lookup lbl typs of
-    Nothing  -> do (aexp,val,cs) <- inferExp th tenv exp
-                   return ((lbl,(val,aexp)),cs)
-    Just val -> do (aexp,cs) <- checkExp th tenv exp val
-                   return ((lbl,(val,aexp)),cs)
-
-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
-        _ -> Bad (render (text "Product expected for definiens" <+> ppTerm Unqualified 0 t <+> text "instead of" <+> ppValue Unqualified 0 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 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 (Q m c) xss : ps, j, g',k') 
-                    where (xss,j,g',k') = foldr p2t ([],i,g,k) xs
-     _ -> error $ render (text "undefined p2t case" <+> ppPatt Unqualified 0 p <+> text "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)
-         _ -> Bad (render (text "Prod expected for function" <+> ppTerm Unqualified 0 f <+> text "instead of" <+> ppValue Unqualified 0 typ))
-     _ -> Bad (render (text "cannot typecheck pattern" <+> ppTerm Unqualified 0 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/Compile/TypeCheck.hs b/src/GF/Compile/TypeCheck.hs
deleted file mode 100644
index aefcf4d25..000000000
--- a/src/GF/Compile/TypeCheck.hs
+++ /dev/null
@@ -1,83 +0,0 @@
-----------------------------------------------------------------------
--- |
--- 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.Compile.TypeCheck (-- * top-level type checking functions; TC should not be called directly.
-		  checkContext,
-		  checkTyp,
-		  checkDef,
-		  checkConstrs,
-		 ) where
-
-import GF.Data.Operations
-
-import GF.Infra.CheckM
-import GF.Grammar
-import GF.Grammar.Lookup
-import GF.Grammar.Unify
-import GF.Compile.Refresh
-import GF.Compile.AbsCompute
-import GF.Compile.TC
-
-import Text.PrettyPrint
-import Control.Monad (foldM, liftM, liftM2)
-
--- | invariant way of creating TCEnv from context
-initTCEnv gamma = 
-  (length gamma,[(x,VGen i x) | ((x,_),i) <- zip gamma [0..]], gamma) 
-
--- interface to TC type checker
-
-type2val :: Type -> Val
-type2val = VClos []
-
-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
-
-justTypeCheck :: SourceGrammar -> Exp -> Val -> Err Constraints
-justTypeCheck gr e v = do
-  (_,constrs0) <- checkExp (grammar2theory gr) (initTCEnv []) e v
-  (constrs1,_) <- unifyVal constrs0
-  return $ filter notJustMeta constrs1
-
-notJustMeta (c,k) = case (c,k) of
-    (VClos g1 (Meta m1), VClos g2 (Meta m2)) -> False
-    _ -> True
-
-grammar2theory :: SourceGrammar -> 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
-
-checkContext :: SourceGrammar -> Context -> [Message]
-checkContext st = checkTyp st . cont2exp
-
-checkTyp :: SourceGrammar -> Type -> [Message]
-checkTyp gr typ = err (\x -> [text x]) ppConstrs $ justTypeCheck gr typ vType
-
-checkDef :: SourceGrammar -> Fun -> Type -> [Equation] -> [Message]
-checkDef gr (m,fun) typ eqs = err (\x -> [text x]) ppConstrs $ do
-  bcs <- mapM (\b -> checkBranch (grammar2theory gr) (initTCEnv []) b (type2val typ)) eqs
-  let (bs,css) = unzip bcs
-  (constrs,_) <- unifyVal (concat css)
-  return $ filter notJustMeta constrs
-
-checkConstrs :: SourceGrammar -> Cat -> [Ident] -> [String]
-checkConstrs gr cat _ = [] ---- check constructors!
diff --git a/src/GF/Grammar/AppPredefined.hs b/src/GF/Grammar/AppPredefined.hs
deleted file mode 100644
index ae7ffd2d3..000000000
--- a/src/GF/Grammar/AppPredefined.hs
+++ /dev/null
@@ -1,159 +0,0 @@
-----------------------------------------------------------------------
--- |
--- 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.Grammar.AppPredefined (isInPredefined, typPredefined, appPredefined
-		     ) where
-
-import GF.Infra.Ident
-import GF.Data.Operations
-import GF.Grammar.Predef
-import GF.Grammar.Grammar
-import GF.Grammar.Macros
-import GF.Grammar.Printer
-import qualified Data.ByteString.Char8 as BS
-import Text.PrettyPrint
-
--- 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 f
-  | f == cInt       = return typePType
-  | f == cFloat     = return typePType
-  | f == cErrorType = return typeType
-  | f == cInts      = return $ mkFunType [typeInt] typePType
-  | f == cPBool     = return typePType
-  | f == cError     = return $ mkFunType [typeStr] typeError  -- non-can. of empty set
-  | f == cPFalse    = return $ typePBool
-  | f == cPTrue     = return $ typePBool
-  | f == cDp        = return $ mkFunType [typeInt,typeTok] typeTok
-  | f == cDrop      = return $ mkFunType [typeInt,typeTok] typeTok
-  | f == cEqInt     = return $ mkFunType [typeInt,typeInt] typePBool
-  | f == cLessInt   = return $ mkFunType [typeInt,typeInt] typePBool
-  | f == cEqStr     = return $ mkFunType [typeTok,typeTok] typePBool
-  | f == cLength    = return $ mkFunType [typeTok] typeInt
-  | f == cOccur     = return $ mkFunType [typeTok,typeTok] typePBool
-  | f == cOccurs    = return $ mkFunType [typeTok,typeTok] typePBool
-  | f == cPlus      = return $ mkFunType [typeInt,typeInt] (typeInt)
-----  "read"   -> (P : Type) -> Tok -> P
-  | f == cShow      = return $ mkProd -- (P : PType) -> P -> Tok
-    [(Explicit,varP,typePType),(Explicit,identW,Vr varP)] typeStr []
-  | f == cToStr     = return $ mkProd -- (L : Type)  -> L -> Str
-    [(Explicit,varL,typeType),(Explicit,identW,Vr varL)] typeStr []
-  | f == cMapStr    = return $ mkProd -- (L : Type)  -> (Str -> Str) -> L -> L
-    [(Explicit,varL,typeType),(Explicit,identW,mkFunType [typeStr] typeStr),(Explicit,identW,Vr varL)] (Vr varL) []
-  | f == cTake      = return $ mkFunType [typeInt,typeTok] typeTok
-  | f == cTk        = return $ mkFunType [typeInt,typeTok] typeTok
-  | otherwise       = Bad (render (text "unknown in Predef:" <+> ppIdent f))
-
-varL :: Ident
-varL = identC (BS.pack "L")
-
-varP :: Ident
-varP = identC (BS.pack "P")
-
-appPredefined :: Term -> Err (Term,Bool)
-appPredefined t = case t of
-  App f x0 -> do
-   (x,_) <- appPredefined x0
-   case f of
-    -- one-place functions
-    Q mod f | mod == cPredef ->
-      case x of
-        (K s) | f == cLength -> retb $ EInt $ toInteger $ length s
-        _                    -> retb t
-
-    -- two-place functions
-    App (Q mod f) z0 | mod == cPredef -> do
-     (z,_) <- appPredefined z0
-     case (norm z, norm x) of
-      (EInt i, K s)    | f == cDrop    -> retb $ K (drop (fi i) s)
-      (EInt i, K s)    | f == cTake    -> retb $ K (take (fi i) s)
-      (EInt i, K s)    | f == cTk      -> retb $ K (take (max 0 (length s - fi i)) s)
-      (EInt i, K s)    | f == cDp      -> retb $ K (drop (max 0 (length s - fi i)) s)
-      (K s,    K t)    | f == cEqStr   -> retb $ if s == t then predefTrue else predefFalse
-      (K s,    K t)    | f == cOccur   -> retb $ if substring s t then predefTrue else predefFalse
-      (K s,    K t)    | f == cOccurs  -> retb $ if any (flip elem t) s then predefTrue else predefFalse
-      (EInt i, EInt j) | f == cEqInt   -> retb $ if i==j then predefTrue else predefFalse
-      (EInt i, EInt j) | f == cLessInt -> retb $ if i<j  then predefTrue else predefFalse
-      (EInt i, EInt j) | f == cPlus    -> retb $ EInt $ i+j
-      (_,      t)      | f == cShow    -> retb $ foldr C Empty $ map K $ words $ render (ppTerm Unqualified 0 t)
-      (_,      K s)    | f == cRead    -> retb $ Cn (identC (BS.pack s)) --- because of K, only works for atomic tags
-      (_,      t)      | f == cToStr   -> trm2str t >>= retb
-      _ -> retb t ---- prtBad "cannot compute predefined" t
-
-    -- three-place functions
-    App (App (Q mod f) z0) y0 | mod == cPredef -> do
-     (y,_) <- appPredefined y0
-     (z,_) <- appPredefined z0
-     case (z, y, x) of
-      (ty,op,t) | f == cMapStr -> 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 (retc t,True)  -- no further computing needed
-   retf t = return (retc t,False) -- must be computed further
-   retc t = case t of
-     K [] -> t
-     K s  -> foldr1 C (map K (words s))
-     _    -> t
-   norm t = case t of
-     Empty -> K []
-     C u v -> case (norm u,norm v) of
-       (K x,K y) -> K (x +++ y)
-       _ -> t
-     _ -> t
-   fi = fromInteger
-
--- read makes variables into constants
-
-predefTrue = Q cPredef cPTrue
-predefFalse = Q cPredef cPFalse
-
-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
-  _               -> Bad (render (text "cannot get Str from term" <+> ppTerm Unqualified 0 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/GFI.hs b/src/GFI.hs
index 727e91209..5c31fce41 100644
--- a/src/GFI.hs
+++ b/src/GFI.hs
@@ -11,7 +11,7 @@ import GF.Grammar hiding (Ident)
 import GF.Grammar.Parser (runP, pExp)
 import GF.Compile.Rename
 import GF.Compile.CheckGrammar
-import GF.Compile.Compute (computeConcrete)
+import GF.Compile.Concrete.Compute (computeConcrete)
 import GF.Infra.Dependencies
 import GF.Infra.CheckM
 import GF.Infra.UseIO
-- 
cgit v1.2.3