split the abstract syntax specific and the concrete syntax specific modules in different subfolders in GF.Compile

3 files changed, 1315 insertions, 0 deletions

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