changed names of resource-1.3; added a note on homepage on release

23 files changed, 5834 insertions, 0 deletions

diff --git a/src/GF/Compile/BackOpt.hs b/src/GF/Compile/BackOpt.hs
new file mode 100644
index 000000000..8667023c0
--- /dev/null
+++ b/src/GF/Compile/BackOpt.hs
@@ -0,0 +1,105 @@
+----------------------------------------------------------------------
+-- |
+-- Module      : BackOpt
+-- Maintainer  : AR
+-- Stability   : (stable)
+-- Portability : (portable)
+--
+-- > CVS $Date: 2005/04/21 16:21:33 $ 
+-- > CVS $Author: bringert $
+-- > CVS $Revision: 1.6 $
+--
+-- Optimizations on GF source code: sharing, parametrization, value sets.
+--
+-- optimization: sharing branches in tables. AR 25\/4\/2003.
+-- following advice of Josef Svenningsson
+-----------------------------------------------------------------------------
+
+module GF.Compile.BackOpt (shareModule, OptSpec) where
+
+import GF.Grammar.Grammar
+import GF.Infra.Ident
+import GF.Infra.Option
+import qualified GF.Grammar.Macros as C
+import GF.Grammar.PrGrammar (prt)
+import GF.Data.Operations
+import Data.List
+import qualified GF.Infra.Modules as M
+import qualified Data.ByteString.Char8 as BS
+
+import Data.Set (Set)
+import qualified Data.Set as Set
+
+type OptSpec = Set Optimization
+
+shareModule :: OptSpec -> (Ident, SourceModInfo) -> (Ident, SourceModInfo)
+shareModule opt (i,m) = case m of
+  M.ModMod mo -> 
+    (i,M.ModMod (M.replaceJudgements mo (mapTree (shareInfo opt) (M.jments mo))))
+  _ -> (i,m)
+
+shareInfo opt (c, CncCat ty (Yes t) m) = (c,CncCat ty (Yes (shareOptim opt c t)) m)
+shareInfo opt (c, CncFun kxs (Yes t) m) = (c,CncFun kxs (Yes (shareOptim opt c t)) m)
+shareInfo opt (c, ResOper ty (Yes t)) = (c,ResOper ty (Yes (shareOptim opt c t)))
+shareInfo _ i = i
+
+-- the function putting together optimizations
+shareOptim :: OptSpec -> Ident -> Term -> Term
+shareOptim opt c =   (if OptValues      `Set.member` opt then values     else id)
+                   . (if OptParametrize `Set.member` opt then factor c 0 else id)
+
+-- do even more: factor parametric branches
+
+factor :: Ident -> Int -> Term -> Term
+factor c i t = case t of
+  T _ [_] -> t
+  T _ []  -> t
+  T (TComp ty) cs -> 
+    T (TTyped ty) $ factors i [(p, factor c (i+1) v) | (p, v) <- cs]
+  _ -> C.composSafeOp (factor c i) t
+ where
+
+   factors i psvs =   -- we know psvs has at least 2 elements
+     let p   = qqIdent c i
+         vs' = map (mkFun p) psvs
+     in if   allEqs vs'
+        then mkCase p vs' 
+        else psvs
+
+   mkFun p (patt, val) = replace (C.patt2term patt) (Vr p) val
+
+   allEqs (v:vs) = all (==v) vs
+
+   mkCase p (v:_) = [(PV p, v)]
+
+--- we hope this will be fresh and don't check... in GFC would be safe
+
+qqIdent c i = identC (BS.pack ("q_" ++ prt c ++ "__" ++ show i))
+
+
+--  we need to replace subterms
+
+replace :: Term -> Term -> Term -> Term
+replace old new trm = case trm of
+  
+  -- these are the important cases, since they can correspond to patterns  
+  QC _ _   | trm == old -> new
+  App t ts | trm == old -> new
+  App t ts              -> App (repl t) (repl ts)
+  R _ | isRec && trm == old -> new
+  _ -> C.composSafeOp repl trm
+ where
+   repl = replace old new
+   isRec = case trm of
+     R _ -> True
+     _ -> False
+
+-- It is very important that this is performed only after case
+-- expansion since otherwise the order and number of values can
+-- be incorrect. Guaranteed by the TComp flag.
+
+values :: Term -> Term
+values t = case t of
+  T ty [(ps,t)]   -> T ty [(ps,values t)] -- don't destroy parametrization
+  T (TComp ty) cs -> V ty [values t | (_, t) <- cs]
+  _ -> C.composSafeOp values t
diff --git a/src/GF/Compile/CheckGrammar.hs b/src/GF/Compile/CheckGrammar.hs
new file mode 100644
index 000000000..0a8361d36
--- /dev/null
+++ b/src/GF/Compile/CheckGrammar.hs
@@ -0,0 +1,1105 @@
+{-# LANGUAGE PatternGuards #-}
+----------------------------------------------------------------------
+-- |
+-- Module      : CheckGrammar
+-- Maintainer  : AR
+-- Stability   : (stable)
+-- Portability : (portable)
+--
+-- > CVS $Date: 2005/11/11 23:24:33 $ 
+-- > CVS $Author: aarne $
+-- > CVS $Revision: 1.31 $
+--
+-- AR 4\/12\/1999 -- 1\/4\/2000 -- 8\/9\/2001 -- 15\/5\/2002 -- 27\/11\/2002 -- 18\/6\/2003
+--
+-- type checking also does the following modifications:
+--
+--  - types of operations and local constants are inferred and put in place
+--
+--  - both these types and linearization types are computed
+--
+--  - tables are type-annotated
+-----------------------------------------------------------------------------
+
+module GF.Compile.CheckGrammar (
+  showCheckModule, justCheckLTerm, allOperDependencies, topoSortOpers) where
+
+import GF.Infra.Ident
+import GF.Infra.Modules
+
+import GF.Compile.TypeCheck
+
+import GF.Compile.Refresh
+import GF.Grammar.Grammar
+import GF.Grammar.PrGrammar
+import GF.Grammar.Lookup
+import GF.Grammar.LookAbs
+import GF.Grammar.Predef
+import GF.Grammar.Macros
+import GF.Grammar.ReservedWords
+import GF.Grammar.PatternMatch
+import GF.Grammar.AppPredefined
+import GF.Grammar.Lockfield (isLockLabel)
+
+import GF.Data.Operations
+import GF.Infra.CheckM
+
+import Data.List
+import qualified Data.Set as Set
+import qualified Data.Map as Map
+import Control.Monad
+import Debug.Trace ---
+
+
+showCheckModule :: [SourceModule] -> SourceModule -> Err ([SourceModule],String)
+showCheckModule mos m = do
+  (st,(_,msg)) <- checkStart $ checkModule mos m
+  return (st, unlines $ reverse msg)
+
+mapsCheckTree :: 
+  (Ord a) => ((a,b) -> Check (a,c)) -> BinTree a b -> Check (BinTree a c)
+mapsCheckTree f = checkErr . mapsErrTree (\t -> checkStart (f t) >>= return . fst)
+
+
+-- | checking is performed in the dependency order of modules
+checkModule :: [SourceModule] -> SourceModule -> Check [SourceModule]
+checkModule ms (name,mod) = checkIn ("checking module" +++ prt name) $ case mod of
+
+  ModMod mo -> do
+    let js = jments mo
+    checkRestrictedInheritance ms (name, mo)
+    js' <- case mtype mo of
+      MTAbstract -> mapsCheckTree (checkAbsInfo gr name mo) js
+
+      MTTransfer a b -> mapsCheckTree (checkAbsInfo gr name mo) js
+
+      MTResource -> mapsCheckTree (checkResInfo gr name mo) js
+
+      MTConcrete a -> do
+        checkErr $ topoSortOpers $ allOperDependencies name js
+        ModMod abs <- checkErr $ lookupModule gr a
+        js1 <- checkCompleteGrammar abs mo
+        mapsCheckTree (checkCncInfo gr name mo (a,abs)) js1
+
+      MTInterface -> mapsCheckTree (checkResInfo gr name mo) js
+
+      MTInstance a -> do
+        ModMod abs <- checkErr $ lookupModule gr a
+        -- checkCompleteInstance abs mo -- this is done in Rebuild
+        mapsCheckTree (checkResInfo gr name mo) js
+
+    return $ (name, ModMod (replaceJudgements mo js')) : ms
+
+  _ -> return $ (name,mod) : ms
+ where
+   gr  = MGrammar $ (name,mod):ms
+
+-- check if restricted inheritance modules are still coherent
+-- i.e. that the defs of remaining names don't depend on omitted names
+---checkRestrictedInheritance :: [SourceModule] -> SourceModule -> Check ()
+checkRestrictedInheritance mos (name,mo) = do
+  let irs = [ii | ii@(_,mi) <- extend mo, mi /= MIAll]  -- names with restr. inh.
+  let mrs = [((i,m),mi) | (i,ModMod m) <- mos, Just mi <- [lookup i irs]] 
+                             -- the restr. modules themself, with restr. infos
+  mapM_ checkRem mrs
+ where
+   checkRem ((i,m),mi) = do
+     let (incl,excl) = partition (isInherited mi) (map fst (tree2list (jments m)))
+     let incld c   = Set.member c (Set.fromList incl)
+     let illegal c = Set.member c (Set.fromList excl)
+     let illegals = [(f,is) | 
+           (f,cs) <- allDeps, incld f, let is = filter illegal cs, not (null is)]
+     case illegals of 
+       [] -> return ()
+       cs -> fail $ "In inherited module" +++ prt i ++
+               ", dependence of excluded constants:" ++++
+               unlines ["  " ++ prt f +++ "on" +++ unwords (map prt is) | 
+                              (f,is) <- cs]
+   allDeps = ---- transClosure $ Map.fromList $ 
+             concatMap (allDependencies (const True)) 
+                              [jments m | (_,ModMod m) <- mos]
+   transClosure ds = ds ---- TODO: check in deeper modules
+
+-- | check if a term is typable
+justCheckLTerm :: SourceGrammar -> Term -> Err Term
+justCheckLTerm src t = do
+  ((t',_),_) <- checkStart (inferLType src t)
+  return t'
+
+checkAbsInfo :: 
+  SourceGrammar -> Ident -> Module Ident Info -> (Ident,Info) -> Check (Ident,Info)
+checkAbsInfo st m mo (c,info) = do
+---- checkReservedId c
+ case info of
+   AbsCat (Yes cont) _ -> mkCheck "category" $ 
+     checkContext st cont ---- also cstrs
+   AbsFun (Yes typ0) md -> do
+    typ <- compAbsTyp [] typ0   -- to calculate let definitions
+    mkCheck "type of function" $ checkTyp st typ 
+    md' <- case md of
+       Yes d -> do
+         let d' = elimTables d
+         mkCheckWarn "definition of function" $ checkEquation st (m,c) d'
+         return $ Yes d'
+       _ -> return md
+    return $ (c,AbsFun (Yes typ) md')
+   _ -> return (c,info)
+ where
+   mkCheck cat ss = case ss of
+     [] -> return (c,info)
+     ["[]"] -> return (c,info) ----
+     _  -> checkErr $ Bad (unlines ss ++++ "in" +++ cat +++ prt c +++ pos c)
+   ---- temporary solution when tc of defs is incomplete
+   mkCheckWarn cat ss = case ss of
+     [] -> return (c,info)
+     ["[]"] -> return (c,info) ----
+     _  -> do
+       checkWarn (unlines ss ++++ "in" +++ cat +++ prt c +++ pos c)
+       return (c,info)
+
+   pos c = showPosition mo c
+
+   compAbsTyp g t = case t of
+     Vr x -> maybe (fail ("no value given to variable" +++ prt x)) return $ lookup x g
+     Let (x,(_,a)) b -> do
+       a' <- compAbsTyp g a
+       compAbsTyp ((x, a'):g) b
+     Prod x a b -> do
+       a' <- compAbsTyp g a
+       b' <- compAbsTyp ((x,Vr x):g) b
+       return $ Prod x a' b'
+     Abs _ _ -> return t
+     _ -> composOp (compAbsTyp g) t
+
+   elimTables e = case e of
+     S t a  -> elimSel (elimTables t) (elimTables a)
+     T _ cs -> Eqs [(elimPatt p, elimTables t) | (p,t) <- cs]
+     _ -> composSafeOp elimTables e
+   elimPatt p = case p of
+     PR lps -> map snd lps
+     _ -> [p]
+   elimSel t a = case a of
+     R fs -> mkApp t (map (snd . snd) fs)
+     _ -> mkApp t [a]
+
+checkCompleteGrammar :: SourceAbs -> SourceCnc -> Check (BinTree Ident Info)
+checkCompleteGrammar abs cnc = do
+  let js = jments cnc
+  let fs = tree2list $ jments abs
+  foldM checkOne js fs
+ where
+   checkOne js i@(c,info) = case info of
+     AbsFun (Yes _) _ -> case lookupIdent c js of
+       Ok _ -> return js
+       _ -> do
+         checkWarn $ "WARNING: no linearization of" +++ prt c
+         return js
+     AbsCat (Yes _) _ -> case lookupIdent c js of
+       Ok (AnyInd _ _) -> return js
+       Ok (CncCat (Yes _) _ _) -> return js
+       Ok (CncCat _ mt mp) -> do
+         checkWarn $ 
+           "Warning: no linearization type for" +++ prt c ++ 
+           ", inserting default {s : Str}" 
+         return $ updateTree (c,CncCat (Yes defLinType) mt mp) js
+       _ -> do
+         checkWarn $ 
+           "Warning: no linearization type for" +++ prt c ++ 
+           ", inserting default {s : Str}" 
+         return $ updateTree (c,CncCat (Yes defLinType) nope nope) js
+     _ -> return js
+
+-- | General Principle: only Yes-values are checked. 
+-- A May-value has always been checked in its origin module.
+checkResInfo :: 
+  SourceGrammar -> Ident -> Module Ident Info -> (Ident,Info) -> Check (Ident,Info)
+checkResInfo gr mo mm (c,info) = do
+  checkReservedId c
+  case info of
+    ResOper pty pde -> chIn "operation" $ do
+      (pty', pde') <- case (pty,pde) of
+         (Yes ty, Yes de) -> do
+           ty'     <- check ty typeType >>= comp . fst
+           (de',_) <- check de ty'
+           return (Yes ty', Yes de')
+         (_, Yes de) -> do
+           (de',ty') <- infer de
+           return (Yes ty', Yes de')
+         (_,Nope) -> do
+           checkWarn "No definition given to oper"
+           return (pty,pde)
+         _ -> return (pty, pde) --- other cases are uninteresting
+      return (c, ResOper pty' pde')
+
+    ResOverload os tysts -> chIn "overloading" $ do
+      tysts' <- mapM (uncurry $ flip check) tysts  -- return explicit ones
+      tysts0 <- checkErr $ lookupOverload gr mo c  -- check against inherited ones too
+      tysts1 <- mapM (uncurry $ flip check) 
+                  [(mkFunType args val,tr) | (args,(val,tr)) <- tysts0]
+      let tysts2 = [(y,x) | (x,y) <- tysts1]
+      --- this can only be a partial guarantee, since matching
+      --- with value type is only possible if expected type is given
+      checkUniq $ 
+        sort [t : map snd xs | (x,_) <- tysts2, Ok (xs,t) <- [typeFormCnc x]]
+      return (c,ResOverload os [(y,x) | (x,y) <- tysts'])
+
+    ResParam (Yes (pcs,_)) -> chIn "parameter type" $ do
+----      mapM ((mapM (computeLType gr . snd)) . snd) pcs
+      mapM_ ((mapM_ (checkIfParType gr . snd)) . snd) pcs
+      ts <- checkErr $ lookupParamValues gr mo c
+      return (c,ResParam (Yes (pcs, Just ts)))
+
+    _ ->  return (c,info)
+ where
+   infer = inferLType gr
+   check = checkLType gr
+   chIn cat = checkIn ("Happened in" +++ cat +++ prt c +++ pos c +++ ":")
+   comp = computeLType gr
+   pos c = showPosition mm c
+
+   checkUniq xss = case xss of
+     x:y:xs 
+      | x == y -> raise $ "ambiguous for type" +++ 
+                           prtType gr (mkFunType (tail x) (head x))  
+      | otherwise -> checkUniq $ y:xs
+     _ -> return ()
+
+
+checkCncInfo :: SourceGrammar -> Ident -> Module Ident Info -> 
+                (Ident,SourceAbs) -> 
+                (Ident,Info) -> Check (Ident,Info)
+checkCncInfo gr m mo (a,abs) (c,info) = do
+  checkReservedId c
+  case info of
+
+    CncFun _ (Yes trm) mpr -> chIn "linearization of" $ do
+      typ        <- checkErr $ lookupFunType gr a c
+      cat0       <- checkErr $ valCat typ
+      (cont,val) <- linTypeOfType gr m typ         -- creates arg vars
+      (trm',_)   <- check trm (mkFunType (map snd cont) val)  -- erases arg vars
+      checkPrintname gr mpr
+      cat        <- return $ snd cat0
+      return (c, CncFun (Just (cat,(cont,val))) (Yes trm') mpr)
+                                                   -- cat for cf, typ for pe
+
+    CncCat (Yes typ) mdef mpr -> chIn "linearization type of" $ do
+      checkErr $ lookupCatContext gr a c
+      typ'  <- checkIfLinType gr typ
+      mdef' <- case mdef of
+        Yes def -> do
+          (def',_) <- checkLType gr def (mkFunType [typeStr] typ)
+          return $ Yes def'
+        _ -> return mdef
+      checkPrintname gr mpr
+      return (c,CncCat (Yes typ') mdef' mpr)
+
+    _ -> checkResInfo gr m mo (c,info)
+
+ where
+   env = gr
+   infer = inferLType gr
+   comp = computeLType gr 
+   check = checkLType gr
+   chIn cat = checkIn ("Happened in" +++ cat +++ prt c +++ pos c +++ ":")
+   pos c = showPosition mo c
+
+checkIfParType :: SourceGrammar -> Type -> Check ()
+checkIfParType st typ = checkCond ("Not parameter type" +++ prt typ) (isParType typ)
+  where
+   isParType ty = True ----
+{- case ty of
+     Cn typ -> case lookupConcrete st typ of
+       Ok (CncParType _ _ _) -> True
+       Ok (CncOper _ ty' _) -> isParType ty'
+       _ -> False
+     Q p t -> case lookupInPackage st (p,t) of
+       Ok (CncParType _ _ _) -> True
+       _ -> False
+     RecType r -> all (isParType . snd) r
+     _ -> False
+-}
+
+checkIfStrType :: SourceGrammar -> Type -> Check ()
+checkIfStrType st typ = case typ of
+  Table arg val -> do
+    checkIfParType st arg 
+    checkIfStrType st val
+  _ | typ == typeStr -> return ()
+  _ -> prtFail "not a string type" typ
+
+
+checkIfLinType :: SourceGrammar -> Type -> Check Type
+checkIfLinType st typ0 = do
+  typ <- computeLType st typ0
+{- ---- should check that not fun type
+  case typ of
+    RecType r -> do
+      let (lins,ihs) = partition (isLinLabel .fst) r
+      --- checkErr $ checkUnique $ map fst r
+      mapM_ checkInh ihs
+      mapM_ checkLin lins
+    _ -> prtFail "a linearization type cannot be" typ
+-}
+  return typ
+
+ where
+   checkInh (label,typ) = checkIfParType st typ
+   checkLin (label,typ) = return () ---- checkIfStrType st typ
+
+
+computeLType :: SourceGrammar -> Type -> Check Type
+computeLType gr t = do
+  g0 <- checkGetContext
+  let g = [(x, Vr x) | (x,_) <- g0]
+  checkInContext g $ comp t
+ where
+  comp ty = case ty of
+    _ | Just _ <- isTypeInts ty -> return ty ---- shouldn't be needed
+      | isPredefConstant ty     -> return ty ---- shouldn't be needed
+
+    Q m ident -> checkIn ("module" +++ prt m) $ do
+      ty' <- checkErr (lookupResDef gr m ident) 
+      if ty' == ty then return ty else comp ty' --- is this necessary to test?
+
+    Vr ident  -> checkLookup ident -- never needed to compute!
+
+    App f a -> do
+      f' <- comp f
+      a' <- comp a
+      case f' of
+        Abs x b -> checkInContext [(x,a')] $ comp b
+        _ -> return $ App f' a'
+
+    Prod x a b -> do
+      a' <- comp a
+      b' <- checkInContext [(x,Vr x)] $ comp b
+      return $ Prod x a' b'
+
+    Abs x b -> do
+      b' <- checkInContext [(x,Vr x)] $ comp b
+      return $ Abs x b'
+
+    ExtR r s -> do
+      r' <- comp r
+      s' <- comp s
+      case (r',s') of
+        (RecType rs, RecType ss) -> checkErr (plusRecType r' s') >>= comp
+        _ -> return $ ExtR r' s'
+
+    RecType fs -> do
+      let fs' = sortRec fs
+      liftM RecType $ mapPairsM comp fs'
+
+    _ | ty == typeTok -> return typeStr
+    _ | isPredefConstant ty -> return ty
+
+    _ -> composOp comp ty
+
+checkPrintname :: SourceGrammar -> Perh Term -> Check ()
+checkPrintname st (Yes t) = checkLType st t typeStr >> return ()
+checkPrintname _ _ = return ()
+
+-- | for grammars obtained otherwise than by parsing ---- update!!
+checkReservedId :: Ident -> Check ()
+checkReservedId x = let c = prt x in
+         if isResWord c 
+            then checkWarn ("Warning: reserved word used as identifier:" +++ c)
+            else return ()
+
+-- to normalize records and record types
+labelIndex :: Type -> Label -> Int
+labelIndex ty lab = case ty of
+  RecType ts -> maybe (error ("label index" +++ prt lab)) id $ lookup lab $ labs ts
+  _ -> error $ "label index" +++ prt ty
+ where 
+  labs ts = zip (map fst (sortRec ts)) [0..]
+
+-- the underlying algorithms
+
+inferLType :: SourceGrammar -> Term -> Check (Term, Type)
+inferLType gr trm = case trm of
+
+   Q m ident | isPredef m -> termWith trm $ checkErr (typPredefined ident)
+
+   Q m ident -> checks [
+     termWith trm $ checkErr (lookupResType gr m ident) >>= comp
+     ,
+     checkErr (lookupResDef gr m ident) >>= infer
+     ,
+     prtFail "cannot infer type of constant" trm
+     ]
+
+   QC m ident | isPredef m -> termWith trm $ checkErr (typPredefined ident)
+
+   QC m ident -> checks [
+       termWith trm $ checkErr (lookupResType gr m ident) >>= comp
+       ,
+       checkErr (lookupResDef gr m ident) >>= infer
+       ,
+       prtFail "cannot infer type of canonical constant" trm
+       ]
+
+   Val ty i -> termWith trm $ return ty
+
+   Vr ident -> termWith trm $ checkLookup ident
+
+   Typed e t -> do
+     t' <- comp t
+     check e t'
+     return (e,t')
+
+   App f a -> do
+     over <- getOverload gr Nothing trm
+     case over of
+       Just trty -> return trty
+       _ -> do
+         (f',fty) <- infer f
+         fty' <- comp fty
+         case fty' of
+           Prod z arg val -> do 
+             a' <- justCheck a arg
+             ty <- if isWildIdent z 
+                      then return val
+                      else substituteLType [(z,a')] val
+             return (App f' a',ty) 
+           _ -> raise ("function type expected for"+++ 
+                      prt f +++"instead of" +++ prtType env fty)
+
+   S f x -> do
+     (f', fty) <- infer f
+     case fty of
+       Table arg val -> do
+         x'<- justCheck x arg
+         return (S f' x', val)
+       _ -> prtFail "table lintype expected for the table in" trm
+
+   P t i -> do
+     (t',ty) <- infer t   --- ??
+     ty' <- comp ty
+-----     let tr2 = PI t' i (labelIndex ty' i)
+     let tr2 = P t' i
+     termWith tr2 $ checkErr $ case ty' of
+       RecType ts -> maybeErr ("unknown label" +++ prt i +++ "in" +++ prt ty') $ 
+                     lookup i ts
+       _ -> prtBad ("record type expected for" +++ prt t +++ "instead of") ty'
+   PI t i _ -> infer $ P t i
+
+   R r -> do
+     let (ls,fs) = unzip r
+     fsts <- mapM inferM fs
+     let ts = [ty | (Just ty,_) <- fsts]
+     checkCond ("cannot infer type of record"+++ prt trm) (length ts == length fsts)
+     return $ (R (zip ls fsts), RecType (zip ls ts))
+
+   T (TTyped arg) pts -> do
+     (_,val) <- checks $ map (inferCase (Just arg)) pts
+     check trm (Table arg val)
+   T (TComp arg) pts -> do
+     (_,val) <- checks $ map (inferCase (Just arg)) pts
+     check trm (Table arg val)
+   T ti pts -> do  -- tries to guess: good in oper type inference
+     let pts' = [pt | pt@(p,_) <- pts, isConstPatt p]
+     case pts' of 
+       [] -> prtFail "cannot infer table type of" trm
+----       PInt k : _ -> return $ Ints $ max [i | PInt i <- pts'] 
+       _  -> do 
+         (arg,val) <- checks $ map (inferCase Nothing) pts'
+         check trm (Table arg val)
+   V arg pts -> do
+     (_,val) <- checks $ map infer pts
+     return (trm, Table arg val)
+
+   K s  -> do
+     if elem ' ' s
+        then do
+          let ss = foldr C Empty (map K (words s))  
+          ----- removed irritating warning AR 24/5/2008
+          ----- checkWarn ("WARNING: 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 typeStr) C s1 s2 typeStr
+
+   Glue s1 s2 -> 
+     check2 (flip justCheck typeStr) Glue s1 s2 typeStr ---- typeTok
+
+---- hack from Rename.identRenameTerm, to live with files with naming conflicts 18/6/2007
+   Strs (Cn c : ts) | c == cConflict -> do
+     trace ("WARNING: unresolved constant, could be any of" +++ unwords (map prt ts)) (infer $ head ts)
+--     checkWarn ("WARNING: unresolved constant, could be any of" +++ unwords (map prt ts))
+--     infer $ head ts
+
+   Strs ts -> do
+     ts' <- mapM (\t -> justCheck t typeStr) ts 
+     return (Strs ts', typeStrs)
+
+   Alts (t,aa) -> do
+     t'  <- justCheck t typeStr
+     aa' <- flip mapM aa (\ (c,v) -> do
+        c' <- justCheck c typeStr 
+        v' <- justCheck v typeStrs
+        return (c',v'))
+     return (Alts (t',aa'), typeStr)
+
+   RecType r -> do
+     let (ls,ts) = unzip r
+     ts' <- mapM (flip justCheck typeType) ts 
+     return (RecType (zip ls ts'), typeType)
+
+   ExtR r s -> do
+     (r',rT) <- infer r 
+     rT'     <- comp rT
+     (s',sT) <- infer s
+     sT'     <- comp sT
+
+     let trm' = ExtR r' s'
+     ---- trm'    <- checkErr $ plusRecord r' s'
+     case (rT', sT') of
+       (RecType rs, RecType ss) -> do
+         rt <- checkErr $ plusRecType rT' sT'
+         check trm' rt ---- return (trm', rt)
+       _ | rT' == typeType && sT' == typeType -> return (trm', typeType)
+       _ -> prtFail "records or record types expected in" trm
+
+   Sort _     -> 
+     termWith trm $ return typeType
+
+   Prod x a b -> do
+     a' <- justCheck a typeType
+     b' <- checkInContext [(x,a')] $ justCheck b typeType
+     return (Prod x a' b', typeType)
+
+   Table p t  -> do
+     p' <- justCheck p typeType --- check p partype! 
+     t' <- justCheck t typeType
+     return $ (Table p' t', typeType)
+
+   FV vs -> do
+     (_,ty) <- checks $ map infer vs
+---     checkIfComplexVariantType trm ty
+     check trm ty
+
+   EPattType ty -> do
+     ty' <- justCheck ty typeType
+     return (ty',typeType)
+   EPatt p -> do
+     ty <- inferPatt p
+     return (trm, EPattType ty)
+
+   _ -> prtFail "cannot infer lintype of" trm
+
+ where
+   env = gr
+   infer = inferLType env
+   comp = computeLType env 
+
+   check = checkLType env
+   
+   isPredef m = elem m [cPredef,cPredefAbs]
+
+   justCheck ty te = check ty te >>= return . fst
+
+   -- for record fields, which may be typed
+   inferM (mty, t) = do
+     (t', ty') <- case mty of
+       Just ty -> check ty t
+       _ -> infer t
+     return (Just ty',t')
+
+   inferCase mty (patt,term) = do
+     arg  <- maybe (inferPatt patt) return mty
+     cont <- pattContext env arg patt
+     i    <- checkUpdates cont
+     (_,val) <- infer term
+     checkResets i
+     return (arg,val)
+   isConstPatt p = case p of
+     PC _ ps -> True --- all isConstPatt ps
+     PP _ _ ps -> True --- all isConstPatt ps
+     PR ps -> all (isConstPatt . snd) ps
+     PT _ p -> isConstPatt p
+     PString _ -> True
+     PInt _ -> True
+     PFloat _ -> True
+     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 $ lookupResType gr q c >>= valTypeCnc
+     PAs _ p  -> inferPatt p
+     PNeg p   -> inferPatt p
+     PAlt p q -> checks [inferPatt p, inferPatt q]
+     PSeq _ _ -> return $ typeStr
+     PRep _   -> return $ typeStr
+     PChar    -> return $ typeStr
+     PChars _ -> return $ typeStr
+     _ -> infer (patt2term p) >>= return . snd
+
+
+-- type inference: Nothing, type checking: Just t
+-- the latter permits matching with value type
+getOverload :: SourceGrammar -> Maybe Type -> Term -> Check (Maybe (Term,Type))
+getOverload env@gr mt ot = case appForm ot of
+     (f@(Q m c), ts) -> case lookupOverload gr m c of
+       Ok typs -> do
+         ttys <- mapM infer ts
+         v <- matchOverload f typs ttys
+         return $ Just v
+       _ -> return Nothing
+     _ -> return Nothing
+ where
+   infer = inferLType env
+   matchOverload f typs ttys = do
+     let (tts,tys) = unzip ttys
+     let vfs = lookupOverloadInstance tys typs
+     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 ("ignoring lock fields in resolving" +++ prt ot) 
+         return (mkApp fun tts, val)
+       ([],[]) -> do
+         raise $ "no overload instance of" +++ prt f +++ 
+           "for" +++ unwords (map (prtType env) tys) +++ "among" ++++ 
+           unlines ["  " ++ unwords (map (prtType env) ty) | (ty,_) <- typs] ++
+           maybe [] (("with value type" +++) . prtType env) mt
+
+       (vfs1,vfs2) -> case (noProds vfs1,noProds vfs2) of
+         ([(val,fun)],_) -> do
+           return (mkApp fun tts, val)
+         ([],[(val,fun)]) -> do
+           checkWarn ("ignoring lock fields in resolving" +++ prt ot) 
+           return (mkApp fun tts, val)
+
+----- unsafely exclude irritating warning AR 24/5/2008
+-----           checkWarn $ "WARNING: overloading of" +++ prt f +++ 
+-----             "resolved by excluding partial applications:" ++++
+-----             unlines [prtType env ty | (ty,_) <- vfs', not (noProd ty)]
+
+
+         _ -> raise $ "ambiguous overloading of" +++ prt f +++
+             "for" +++ unwords (map (prtType env) tys) ++++ "with alternatives" ++++ 
+             unlines [prtType env 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 -> Term -> Type -> Check (Term, Type)
+checkLType env trm typ0 = do
+
+  typ <- comp typ0
+
+  case trm of
+
+    Abs x c -> do
+      case typ of
+        Prod z a b -> do 
+          checkUpdate (x,a)
+          (c',b') <- if isWildIdent z
+                        then check c b
+                        else do
+                          b' <- checkIn "abs" $ substituteLType [(z,Vr x)] b
+                          check c b'
+          checkReset
+          return $ (Abs x c', Prod x a b')
+        _ -> raise $ "product expected instead of" +++ prtType env typ
+
+    App f a -> do
+       over <- getOverload env (Just typ) trm
+       case over of
+         Just trty -> return trty
+         _ -> do
+          (trm',ty') <- infer trm
+          termWith trm' $ checkEq typ ty' trm'
+
+    Q _ _ -> do
+       over <- getOverload env (Just typ) trm
+       case over of
+         Just trty -> return trty
+         _ -> do
+          (trm',ty') <- infer trm
+          termWith trm' $ checkEq typ ty' trm'
+
+    T _ [] ->
+      prtFail "found empty table in type" typ
+    T _ cs -> case typ of 
+      Table arg val -> do 
+        case allParamValues env arg of
+          Ok vs -> do
+            let ps0 = map fst cs
+            ps <- checkErr $ testOvershadow ps0 vs
+            if null ps 
+              then return () 
+              else checkWarn $ "WARNING: patterns never reached:" +++ 
+                               concat (intersperse ", " (map prt ps))
+
+          _ -> return () -- happens with variable types
+        cs' <- mapM (checkCase arg val) cs
+        return (T (TTyped arg) cs', typ)
+      _ -> raise $ "table type expected for table instead of" +++ prtType env typ
+
+    R r -> case typ of --- why needed? because inference may be too difficult
+       RecType rr -> do
+         let (ls,_) = unzip rr        -- labels of expected type
+         fsts <- mapM (checkM r) rr   -- check that they are found in the record
+         return $ (R fsts, typ)       -- normalize record
+
+       _ -> prtFail "record type expected in type checking instead of" typ
+
+    ExtR r s -> case typ of
+       _ | typ == typeType -> do
+         trm' <- comp trm
+         case trm' of
+           RecType _ -> termWith trm $ return typeType
+           ExtR (Vr _) (RecType _) -> termWith trm $ return typeType 
+                                      -- ext t = t ** ...
+           _ -> prtFail "invalid record type extension" trm
+       RecType rr -> do
+         (r',ty,s') <- checks [
+            do (r',ty) <- infer r
+               return (r',ty,s)
+           ,
+            do (s',ty) <- infer s
+               return (s',ty,r)
+            ]
+         case ty of
+           RecType rr1 -> do
+                let (rr0,rr2) = recParts rr rr1
+                r2 <- justCheck r' rr0
+                s2 <- justCheck s' rr2
+                return $ (ExtR r2 s2, typ) 
+           _ -> raise ("record type expected in extension of" +++ prt r +++ 
+                       "but found" +++ prt ty)
+
+       ExtR ty ex -> do
+         r' <- justCheck r ty
+         s' <- justCheck s ex
+         return $ (ExtR r' s', typ) --- is this all?
+
+       _ -> prtFail "record extension not meaningful for" typ
+
+    FV vs -> do
+      ttys <- mapM (flip check typ) vs
+---      checkIfComplexVariantType trm typ
+      return (FV (map fst ttys), typ) --- typ' ?
+
+    S tab arg -> checks [ do
+      (tab',ty) <- infer tab
+      ty'       <- comp ty
+      case ty' of
+        Table p t -> do
+          (arg',val) <- check arg p
+          checkEq typ t trm
+          return (S tab' arg', t)
+        _ -> raise $ "table type expected for applied table instead of" +++ 
+                   prtType env ty'
+     , do
+      (arg',ty) <- infer arg
+      ty'       <- comp ty
+      (tab',_)  <- check tab (Table ty' typ)
+      return (S tab' arg', typ)
+      ]
+    Let (x,(mty,def)) body -> case mty of
+      Just ty -> do
+        (def',ty') <- check def ty
+        checkUpdate (x,ty')
+        body' <- justCheck body typ
+        checkReset
+        return (Let (x,(Just ty',def')) body', typ)
+      _ -> do
+        (def',ty) <- infer def  -- tries to infer type of local constant
+        check (Let (x,(Just ty,def')) body) typ
+
+    _ -> do
+      (trm',ty') <- infer trm
+      termWith trm' $ checkEq typ ty' trm'
+ where
+   cnc = env
+   infer = inferLType env
+   comp = computeLType env 
+
+   check = checkLType env
+   
+   justCheck ty te = check ty te >>= return . fst
+
+   checkEq = checkEqLType env
+
+   recParts rr t = (RecType rr1,RecType rr2) where 
+     (rr1,rr2) = partition (flip elem (map fst t) . fst) rr 
+
+   checkM rms (l,ty) = case lookup l rms of
+     Just (Just ty0,t) -> do
+       checkEq ty ty0 t
+       (t',ty') <- check t ty
+       return (l,(Just ty',t'))
+     Just (_,t) -> do
+       (t',ty') <- check t ty
+       return (l,(Just ty',t'))
+     _ -> prtFail "cannot find value for label" l
+
+   checkCase arg val (p,t) = do
+     cont <- pattContext env arg p
+     i    <- checkUpdates cont
+     t'   <- justCheck t val
+     checkResets i
+     return (p,t')
+
+pattContext :: LTEnv -> Type -> Patt -> Check Context
+pattContext env typ p = case p of
+  PV x | not (isWildIdent x) -> return [(x,typ)]
+  PP q c ps | q /= cPredef -> do ---- why this /=? AR 6/1/2006
+    t <- checkErr $ lookupResType cnc q c
+    (cont,v) <- checkErr $ typeFormCnc t
+    checkCond ("wrong number of arguments for constructor in" +++ prt p) 
+              (length cont == length ps)
+    checkEqLType env typ v (patt2term p)
+    mapM (uncurry (pattContext env)) (zip (map snd cont) ps) >>= return . concat
+  PR r -> do
+    typ' <- computeLType env typ
+    case typ' of
+      RecType t -> do
+        let pts = [(ty,tr) | (l,tr) <- r, Just ty <- [lookup l t]]
+        ----- checkWarn $ prt p ++++ show pts ----- debug
+        mapM (uncurry (pattContext env)) pts >>= return . concat
+      _ -> prtFail "record type expected for pattern instead of" typ'
+  PT t p' -> do
+    checkEqLType env typ t (patt2term p')
+    pattContext env typ p'
+
+  PAs x p -> do
+    g <- pattContext env typ p
+    return $ (x,typ):g
+
+  PAlt p' q -> do
+    g1 <- pattContext env typ p'
+    g2 <- pattContext env typ q
+    let pts = [pt | pt <- g1, notElem pt g2] ++ [pt | pt <- g2, notElem pt g1]
+    checkCond 
+      ("incompatible bindings of" +++ 
+       unwords (nub (map (prt . fst) pts))+++ 
+       "in pattern alterantives" +++ prt p) (null pts) 
+    return g1 -- must be g1 == g2
+  PSeq p q -> do
+    g1 <- pattContext env typ p
+    g2 <- pattContext env typ q
+    return $ g1 ++ g2
+  PRep p' -> noBind typeStr p'
+  PNeg p' -> noBind typ p'
+
+  _ -> return [] ---- check types!
+ where 
+   cnc = env
+   noBind typ p' = do
+    co <- pattContext env typ p'
+    if not (null co)
+      then checkWarn ("no variable bound inside pattern" +++ prt p) 
+           >> return []
+      else return []
+
+-- auxiliaries
+
+type LTEnv = SourceGrammar
+
+termWith :: Term -> Check Type -> Check (Term, Type)
+termWith t ct = do
+  ty <- ct
+  return (t,ty)
+
+-- | light-weight substitution for dep. types
+substituteLType :: Context -> Type -> Check Type
+substituteLType g t = case t of
+  Vr x -> return $ maybe t id $ lookup x g
+  _ -> composOp (substituteLType g) t
+
+-- | compositional check\/infer of binary operations
+check2 :: (Term -> Check Term) -> (Term -> Term -> Term) -> 
+          Term -> Term -> Type -> Check (Term,Type)
+check2 chk con a b t = do
+  a' <- chk a
+  b' <- chk b
+  return (con a' b', t)
+
+checkEqLType :: LTEnv -> Type -> Type -> Term -> Check Type
+checkEqLType env t u trm = do
+  (b,t',u',s) <- checkIfEqLType env t u trm
+  case b of
+    True  -> return t'
+    False -> raise $ s +++ "type of" +++ prt trm +++ 
+                        ": expected:" +++ prtType env t ++++ 
+                        "inferred:" +++ prtType env u
+
+checkIfEqLType :: LTEnv -> Type -> Type -> Term -> Check (Bool,Type,Type,String)
+checkIfEqLType env t u trm = do
+  t' <- comp t 
+  u' <- comp u
+  case t' == u' || alpha [] t' u' of
+    True -> return (True,t',u',[])
+    -- forgive missing lock fields by only generating a warning.
+    --- better: use a flag to forgive? (AR 31/1/2006)
+    _ -> case missingLock [] t' u' of
+      Ok lo -> do
+        checkWarn $ "WARNING: missing lock field" +++ unwords (map prt lo)
+        return (True,t',u',[])
+      Bad s -> return (False,t',u',s)
+
+  where
+
+   -- t is a subtype of u 
+   --- quick hack version of TC.eqVal
+   alpha g t u = case (t,u) of  
+
+     -- error (the empty type!) is subtype of any other type
+     (_,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 env n) 
+                               || elem n (allExtendsPlus env m)
+                               || m == n --- for Predef
+     (QC m a, QC n b) | a == b -> elem m (allExtendsPlus env n) 
+                               || elem n (allExtendsPlus env m)
+     (QC m a, Q  n b) | a == b -> elem m (allExtendsPlus env n) 
+                               || elem n (allExtendsPlus env m)
+     (Q  m a, QC n b) | a == b -> elem m (allExtendsPlus env n) 
+                               || elem n (allExtendsPlus env m)
+
+     (Table a b,  Table c d)  -> alpha g a c && alpha g b d
+     (Vr x,       Vr y)       -> x == y || elem (x,y) g || elem (y,x) g
+     _                        -> t == u 
+     --- the following should be one-way coercions only. AR 4/1/2001
+                                  || elem t sTypes && elem u sTypes
+                                  || (t == typeType && u == typePType) 
+                                  || (u == typeType && t == typePType) 
+
+   missingLock g t u = case (t,u) of  
+     (RecType rs, RecType ts) -> 
+       let 
+         ls = [l | (l,a) <- rs, 
+                   not (any (\ (k,b) -> alpha g a b && l == k) ts)]
+         (locks,others) = partition isLockLabel ls
+       in case others of
+         _:_ -> Bad $ "missing record fields" +++ unwords (map prt others)
+         _ -> return locks
+     -- contravariance
+     (Prod x a b, Prod y c d) -> do
+        ls1 <- missingLock g c a
+        ls2 <- missingLock g b d
+        return $ ls1 ++ ls2
+
+     _ -> Bad ""
+
+   sTypes = [typeStr, typeTok, typeString]
+   comp = computeLType env
+
+-- printing a type with a lock field lock_C as C
+prtType :: LTEnv -> Type -> String
+prtType env ty = case ty of
+  RecType fs -> case filter isLockLabel $ map fst fs of
+    [lock] -> (drop 5 $ prt lock) --- ++++ "Full form" +++ prt ty
+    _ -> prtt ty
+  Prod x a b -> prtType env a +++ "->" +++ prtType env b
+  _ -> prtt ty
+ where
+   prtt t = prt t
+   ---- use computeLType gr to check if really equal to the cat with lock
+
+
+-- | linearization types and defaults
+linTypeOfType :: SourceGrammar -> Ident -> Type -> Check (Context,Type)
+linTypeOfType cnc m typ = do
+  (cont,cat) <- checkErr $ typeSkeleton typ
+  val  <- lookLin cat
+  args <- mapM mkLinArg (zip [0..] cont)
+  return (args, val)
+ where
+   mkLinArg (i,(n,mc@(m,cat))) = do
+     val  <- lookLin mc
+     let vars = mkRecType varLabel $ replicate n typeStr
+	 symb = argIdent n cat i
+     rec <- if n==0 then return val else
+            checkErr $ errIn ("extending" +++ prt vars +++ "with" +++ prt val) $
+            plusRecType vars val
+     return (symb,rec)
+   lookLin (_,c) = checks [ --- rather: update with defLinType ?
+      checkErr (lookupLincat cnc m c) >>= computeLType cnc
+     ,return defLinType
+     ]
+
+-- | dependency check, detecting circularities and returning topo-sorted list
+
+allOperDependencies :: Ident -> BinTree Ident Info -> [(Ident,[Ident])]
+allOperDependencies m = allDependencies (==m)
+
+allDependencies :: (Ident -> Bool) -> BinTree Ident Info -> [(Ident,[Ident])]
+allDependencies ism b = 
+  [(f, nub (concatMap opty (pts i))) | (f,i) <- tree2list b]
+  where
+    opersIn t = case t of
+      Q n c | ism n -> [c]
+      QC n c | ism n -> [c]
+      _ -> collectOp opersIn t
+    opty (Yes ty) = opersIn ty
+    opty _ = []
+    pts i = case i of
+      ResOper pty pt -> [pty,pt]
+      ResParam (Yes (ps,_)) -> [Yes t | (_,cont) <- ps, (_,t) <- cont]
+      CncCat pty _ _ -> [pty]
+      CncFun _   pt _ -> [pt]  ---- (Maybe (Ident,(Context,Type))
+      AbsFun pty ptr -> [pty] --- ptr is def, which can be mutual
+      AbsCat (Yes co) _ -> [Yes ty | (_,ty) <- co]
+      _              -> []
+
+topoSortOpers :: [(Ident,[Ident])] -> Err [Ident]
+topoSortOpers st = do
+  let eops = topoTest st
+  either 
+    return 
+    (\ops -> Bad ("circular definitions:" +++ unwords (map prt (head ops))))
+    eops
diff --git a/src/GF/Compile/Compute.hs b/src/GF/Compile/Compute.hs
new file mode 100644
index 000000000..f35e7c6a9
--- /dev/null
+++ b/src/GF/Compile/Compute.hs
@@ -0,0 +1,429 @@
+----------------------------------------------------------------------
+-- |
+-- 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.Data.Str
+import GF.Grammar.PrGrammar
+import GF.Infra.Modules
+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) ----
+
+import GF.Grammar.AppPredefined
+
+import Data.List (nub,intersperse)
+import Control.Monad (liftM2, liftM)
+
+-- | computation of concrete syntax terms into normal form
+-- used mainly for partial evaluation
+computeConcrete :: SourceGrammar -> Term -> Err Term
+computeConcrete    g t = {- refreshTerm t >>= -} computeTerm g [] t
+computeConcreteRec g t = {- refreshTerm t >>= -} computeTermOpt True g [] t
+
+computeTerm :: SourceGrammar -> Substitution -> Term -> Err Term
+computeTerm = computeTermOpt False
+
+-- rec=True is used if it cannot be assumed that looked-up constants
+-- have already been computed (mainly with -optimize=noexpand in .gfr)
+
+computeTermOpt :: Bool -> SourceGrammar -> Substitution -> Term -> Err Term
+computeTermOpt rec gr = 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 
+
+     -- if computed do nothing
+     Computed t' -> return $ unComputed t'
+
+     Vr x -> do
+       t' <- maybe (prtBad ("no value given to variable") x) return $ lookup x g
+       case t' of 
+         _ | t == t' -> return t
+         _ -> comp g t'
+
+     -- Abs x@(IA _) b -> do 
+     Abs x b | 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 x a b -> do
+       a' <- comp g a
+       b' <- comp (ext x (Vr x) g) b
+       return $ Prod x a' b'
+
+     -- beta-convert
+     App f a -> 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 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 (prtBad "no value for label" l) (comp g . snd) $ 
+                    lookup l $ reverse r 
+
+         ExtR a (R b) ->                 
+           case comp g (P (R b) l) of
+             Ok v -> return v
+             _ -> comp g (P a l)
+
+--- { - --- this is incorrect, since b can contain the proper value
+         ExtR (R a) b ->                 -- NOT POSSIBLE both a and b records!
+           case comp g (P (R a) l) of
+             Ok v -> return v
+             _ -> comp g (P b l)
+--- - } ---
+
+         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 _ -> do
+       r <- composOp (comp g) t
+       returnC r
+
+     -- remove empty
+     C a b    -> do
+       a' <- comp g a
+       b' <- comp g b
+       case (a',b') of
+         (Alts _, K a) -> checks [do
+            as <- strsFromTerm a' -- this may fail when compiling opers
+            return $ variants [
+              foldr1 C (map K (str2strings (plusStr v (str a)))) | v <- as]
+            ,
+            return $ C a' b'
+           ]
+         (Empty,_) -> returnC b'
+         (_,Empty) -> returnC a'
+         _     -> returnC $ C a' b'
+
+     -- reduce free variation as much as you can
+     FV ts -> mapM (comp g) ts >>= returnC . variants
+
+     -- merge record extensions if you can
+     ExtR r s -> do
+       r' <- comp g r
+       s' <- comp g s
+       case (r',s') of
+         (R rs, R ss) -> plusRecord r' s'
+         (RecType rs, RecType ss) -> plusRecType r' s'
+         _ -> return $ ExtR r' s'
+
+     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'
+         _ -> prtBad "pattern expected as value of" p ---- should be in CheckGr
+       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 _ [(PV IW,c)] -> comp g c           --- an optimization
+         T _ [(PT _ (PV IW),c)] -> comp g c
+
+         T _ [(PV z,c)] -> comp (ext z v' g) c --- another optimization
+         T _ [(PT _ (PV z),c)] -> comp (ext z v' g) c
+
+         -- course-of-values table: look up by index, no pattern matching needed
+         V ptyp ts -> do
+           vs <- allParamValues gr ptyp
+           case lookup v' (zip vs [0 .. length vs - 1]) of
+             Just i -> comp g $ ts !! i
+             _ -> return $ S t' v' -- if v' is not canonical
+         T _ cc -> case matchPattern cc v' of
+             Ok (c,g') -> comp (g' ++ g) c
+             _ | isCan v' -> prtBad ("missing case" +++ prt v' +++ "in") t 
+             _ -> return $ S t' v' -- if v' is not canonical
+
+         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'
+
+     -- 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 vs -> do
+
+               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
+               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
+
+{- ----
+     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 $ prt t 
+  Vr (IAV _ _ _) -> Bad $ glueErrorMsg $ prt t 
+  _ -> composOp checkNoArgVars t
+
+glueErrorMsg s = 
+  "Cannot glue (+) term with run-time variable" +++ s ++ "." ++++
+  "Use Prelude.bind instead."
+
+getArgType t = case t of
+  V ty _ -> return ty
+  T (TComp ty) _ -> return ty
+  _ -> prtBad "cannot get argument type of table" t
+
+
+
diff --git a/src/GF/Compile/Export.hs b/src/GF/Compile/Export.hs
new file mode 100644
index 000000000..9e9a99e99
--- /dev/null
+++ b/src/GF/Compile/Export.hs
@@ -0,0 +1,61 @@
+module GF.Compile.Export where
+
+import PGF.CId
+import PGF.Data (PGF(..))
+import PGF.Raw.Print (printTree)
+import PGF.Raw.Convert (fromPGF)
+import GF.Compile.GFCCtoHaskell
+import GF.Compile.GFCCtoJS
+import GF.Infra.Option
+import GF.Speech.CFG
+import GF.Speech.PGFToCFG
+import GF.Speech.SRGS_XML
+import GF.Speech.JSGF
+import GF.Speech.GSL
+import GF.Speech.VoiceXML
+import GF.Speech.SLF
+import GF.Speech.PrRegExp
+import GF.Text.UTF8
+
+import Data.Maybe
+import System.FilePath
+
+-- top-level access to code generation
+
+exportPGF :: Options
+          -> OutputFormat 
+          -> PGF 
+          -> [(FilePath,String)] -- ^ List of recommended file names and contents.
+exportPGF opts fmt pgf = 
+    case fmt of
+      FmtPGF          -> multi "pgf" printPGF
+      FmtJavaScript   -> multi "js"  pgf2js
+      FmtHaskell      -> multi "hs"  (grammar2haskell name)
+      FmtHaskell_GADT -> multi "hs"  (grammar2haskellGADT name)
+      FmtBNF          -> single "bnf"   bnfPrinter
+      FmtSRGS_XML     -> single "grxml" (srgsXmlPrinter sisr)
+      FmtJSGF         -> single "jsgf"  (jsgfPrinter sisr)
+      FmtGSL          -> single "gsl"   gslPrinter
+      FmtVoiceXML     -> single "vxml"  grammar2vxml
+      FmtSLF          -> single ".slf"  slfPrinter
+      FmtRegExp       -> single ".rexp" regexpPrinter
+      FmtFA           -> single ".dot"  slfGraphvizPrinter
+ where
+   name = fromMaybe (prCId (absname pgf)) (moduleFlag optName opts)
+   sisr = flag optSISR opts
+
+   multi :: String -> (PGF -> String) -> [(FilePath,String)]
+   multi ext pr = [(name <.> ext, pr pgf)]
+
+   single :: String -> (PGF -> CId -> String) -> [(FilePath,String)]
+   single ext pr = [(prCId cnc <.> ext, pr pgf cnc) | cnc <- cncnames pgf]
+
+-- | Get the name of the concrete syntax to generate output from.
+-- FIXME: there should be an option to change this.
+outputConcr :: PGF -> CId
+outputConcr pgf = case cncnames pgf of
+                    []     -> error "No concrete syntax."
+                    cnc:_  -> cnc
+
+printPGF :: PGF -> String
+printPGF = encodeUTF8 . printTree . fromPGF
diff --git a/src/GF/Compile/Extend.hs b/src/GF/Compile/Extend.hs
new file mode 100644
index 000000000..8344a1696
--- /dev/null
+++ b/src/GF/Compile/Extend.hs
@@ -0,0 +1,138 @@
+----------------------------------------------------------------------
+-- |
+-- Module      : Extend
+-- Maintainer  : AR
+-- Stability   : (stable)
+-- Portability : (portable)
+--
+-- > CVS $Date: 2005/05/30 21:08:14 $ 
+-- > CVS $Author: aarne $
+-- > CVS $Revision: 1.18 $
+--
+-- AR 14\/5\/2003 -- 11\/11
+--
+-- The top-level function 'extendModule'
+-- extends a module symbol table by indirections to the module it extends
+-----------------------------------------------------------------------------
+
+module GF.Compile.Extend (extendModule, extendMod
+	      ) where
+
+import GF.Grammar.Grammar
+import GF.Infra.Ident
+import GF.Grammar.PrGrammar
+import GF.Infra.Modules
+import GF.Compile.Update
+import GF.Grammar.Macros
+import GF.Data.Operations
+
+import Control.Monad
+
+extendModule :: [SourceModule] -> SourceModule -> Err SourceModule
+extendModule ms (name,mod) = case mod of
+
+  ---- Just to allow inheritance in incomplete concrete (which are not
+  ---- compiled anyway), extensions are not built for them.
+  ---- Should be replaced by real control. AR 4/2/2005
+  ModMod m | mstatus m == MSIncomplete && isModCnc m -> return (name,mod)
+
+  ModMod m -> do
+    mod' <- foldM extOne m (extend m) 
+    return (name,ModMod mod') 
+ where
+   extOne mo (n,cond) = do
+        (m0,isCompl) <- do
+          m <- lookupModMod  (MGrammar ms) n
+
+          -- test that the module types match, and find out if the old is complete
+          testErr (sameMType (mtype m) (mtype mo)) 
+                    ("illegal extension type to module" +++ prt name)
+          return (m, isCompleteModule m)
+
+        -- build extension in a way depending on whether the old module is complete
+        js1 <- extendMod isCompl (n, isInherited cond) name (jments m0) (jments mo)
+
+        -- if incomplete, throw away extension information
+        let es  = extend mo
+        let es' = if isCompl then es else (filter ((/=n) . fst) es) 
+        return $ mo {extend = es', jments = js1}
+
+-- | When extending a complete module: new information is inserted,
+-- and the process is interrupted if unification fails.
+-- If the extended module is incomplete, its judgements are just copied.
+extendMod :: Bool -> (Ident,Ident -> Bool) -> Ident -> 
+             BinTree Ident Info -> BinTree Ident Info -> 
+             Err (BinTree Ident Info)
+extendMod isCompl (name,cond) base old new = foldM try new $ tree2list old where
+  try t i@(c,_) | not (cond c) = return t
+  try t i@(c,_) = errIn ("constant" +++ prt c) $
+                  tryInsert (extendAnyInfo isCompl name base) indirIf t i
+  indirIf = if isCompl then indirInfo name else id
+
+indirInfo :: Ident -> Info -> Info
+indirInfo n info = AnyInd b n' where 
+  (b,n') = case info of
+    ResValue _ -> (True,n)
+    ResParam _ -> (True,n)
+    AbsFun _ (Yes EData) -> (True,n) 
+    AnyInd b k -> (b,k)
+    _ -> (False,n) ---- canonical in Abs
+
+perhIndir :: Ident -> Perh a -> Perh a
+perhIndir n p = case p of
+  Yes _ -> May n
+  _ -> p
+
+extendAnyInfo :: Bool -> Ident -> Ident -> Info -> Info -> Err Info
+extendAnyInfo isc n o i j = 
+ errIn ("building extension for" +++ prt n +++ "in" +++ prt o) $ case (i,j) of
+  (AbsCat mc1 mf1, AbsCat mc2 mf2) -> 
+    liftM2 AbsCat (updn isc n mc1 mc2) (updn isc n mf1 mf2) --- add cstrs
+  (AbsFun mt1 md1, AbsFun mt2 md2) -> 
+    liftM2 AbsFun (updn isc n mt1 mt2) (updn isc n md1 md2) --- add defs
+  (ResParam mt1, ResParam mt2) -> 
+    liftM ResParam $ updn isc n mt1 mt2
+  (ResValue mt1, ResValue mt2) -> 
+    liftM ResValue $ updn isc n mt1 mt2
+  (_, ResOverload ms t) | elem n ms ->
+    return $ ResOverload ms t
+  (ResOper mt1 m1, ResOper mt2 m2) ->           ---- extendResOper n mt1 m1 mt2 m2 
+    liftM2 ResOper (updn isc n mt1 mt2) (updn isc n m1 m2)
+  (CncCat mc1 mf1 mp1, CncCat mc2 mf2 mp2) -> 
+    liftM3 CncCat (updn isc n mc1 mc2) (updn isc n mf1 mf2) (updn isc n mp1 mp2)
+  (CncFun m mt1 md1, CncFun _ mt2 md2) -> 
+    liftM2 (CncFun m) (updn isc n mt1 mt2) (updn isc n md1 md2)
+
+----  (AnyInd _ _, ResOper _ _) -> return j ----
+
+  (AnyInd b1 m1, AnyInd b2 m2) -> do
+    testErr (b1 == b2) "inconsistent indirection status"
+---- commented out as work-around for a spurious problem in
+---- TestResourceFre; should look at building of completion. 17/11/2004 
+    testErr (m1 == m2) $ 
+      "different sources of indirection: " +++ show m1 +++ show m2
+    return i
+
+  _ -> Bad $ "cannot unify information in" ++++ show i ++++ "and" ++++ show j
+
+--- where
+   
+updn isc n = if isc  then (updatePerhaps n) else (updatePerhapsHard n)
+updc isc n = if True then (updatePerhaps n) else (updatePerhapsHard n)
+
+
+
+{- ---- no more needed: this is done in Rebuild
+-- opers declared in an interface and defined in an instance are a special case
+
+extendResOper n mt1 m1 mt2 m2 = case (m1,m2) of
+  (Nope,_) -> return $ ResOper (strip mt1) m2
+  _ -> liftM2 ResOper (updatePerhaps n mt1 mt2) (updatePerhaps n m1 m2)
+ where
+   strip (Yes t) = Yes $ strp t
+   strip m = m
+   strp t = case t of
+     Q _ c  -> Vr c
+     QC _ c -> Vr c
+     _ -> composSafeOp strp t
+-}
diff --git a/src/GF/Compile/GFCCtoHaskell.hs b/src/GF/Compile/GFCCtoHaskell.hs
new file mode 100644
index 000000000..59db9c364
--- /dev/null
+++ b/src/GF/Compile/GFCCtoHaskell.hs
@@ -0,0 +1,213 @@
+----------------------------------------------------------------------
+-- |
+-- Module      : GFCCtoHaskell
+-- Maintainer  : Aarne Ranta
+-- Stability   : (stable)
+-- Portability : (portable)
+--
+-- > CVS $Date: 2005/06/17 12:39:07 $ 
+-- > CVS $Author: bringert $
+-- > CVS $Revision: 1.8 $
+--
+-- to write a GF abstract grammar into a Haskell module with translations from
+-- data objects into GF trees. Example: GSyntax for Agda.
+-- AR 11/11/1999 -- 7/12/2000 -- 18/5/2004
+-----------------------------------------------------------------------------
+
+module GF.Compile.GFCCtoHaskell (grammar2haskell, grammar2haskellGADT) where
+
+import PGF.CId
+import PGF.Data
+import PGF.Macros
+
+import GF.Data.Operations
+import GF.Text.UTF8
+
+import Data.List --(isPrefixOf, find, intersperse)
+import qualified Data.Map as Map
+
+-- | the main function
+grammar2haskell :: String  -- ^ Module name.
+                -> PGF
+                -> String
+grammar2haskell name gr = encodeUTF8 $ foldr (++++) [] $  
+  haskPreamble name ++ [datatypes gr', gfinstances gr']
+    where gr' = hSkeleton gr
+
+grammar2haskellGADT :: String -> PGF -> String
+grammar2haskellGADT name gr = encodeUTF8 $ foldr (++++) [] $  
+  ["{-# OPTIONS_GHC -fglasgow-exts #-}"] ++ 
+  haskPreamble name ++ [datatypesGADT gr', gfinstances gr']
+    where gr' = hSkeleton gr
+
+-- | by this you can prefix all identifiers with stg; the default is 'G'
+gId :: OIdent -> OIdent 
+gId i = 'G':i
+
+haskPreamble name =
+ [
+  "module " ++ name ++ " where",
+  "",
+  "import PGF",
+  "----------------------------------------------------",
+  "-- automatic translation from GF to Haskell",
+  "----------------------------------------------------",
+  "", 
+  "class Gf a where",
+  "  gf :: a -> Tree",
+  "  fg :: Tree -> a",
+  "",
+  predefInst "GString" "String"  "Lit (LStr s)",
+  "",
+  predefInst "GInt"    "Integer" "Lit (LInt s)",
+  "",
+  predefInst "GFloat"  "Double"  "Lit (LFlt s)",
+  "",
+  "----------------------------------------------------",
+  "-- below this line machine-generated",
+  "----------------------------------------------------",
+  ""
+ ]
+
+predefInst gtyp typ patt = 
+  "newtype" +++ gtyp +++ "=" +++ gtyp +++ typ +++ " deriving Show" +++++
+  "instance Gf" +++ gtyp +++ "where" ++++
+  "  gf (" ++ gtyp +++ "s) =" +++ patt ++++
+  "  fg t =" ++++
+  "    case t of" ++++
+  "     " +++ patt +++ " ->" +++ gtyp +++ "s" ++++
+  "      _ -> error (\"no" +++ gtyp +++ "\" ++ show t)"
+
+type OIdent = String
+
+type HSkeleton = [(OIdent, [(OIdent, [OIdent])])]
+
+datatypes, gfinstances :: (String,HSkeleton) -> String
+datatypes   = (foldr (+++++) "") . (filter (/="")) . (map hDatatype) . snd
+gfinstances (m,g) = (foldr (+++++) "") $ (filter (/="")) $ (map (gfInstance m)) g
+
+hDatatype  :: (OIdent, [(OIdent, [OIdent])]) -> String
+gfInstance :: String -> (OIdent, [(OIdent, [OIdent])]) -> String
+
+hDatatype ("Cn",_) = "" ---
+hDatatype (cat,[]) = ""
+hDatatype (cat,rules) | isListCat (cat,rules) = 
+ "newtype" +++ gId cat +++ "=" +++ gId cat +++ "[" ++ gId (elemCat cat) ++ "]" 
+  +++ "deriving Show"
+hDatatype (cat,rules) =
+ "data" +++ gId cat +++ "=" ++
+ (if length rules == 1 then "" else "\n  ") +++
+ foldr1 (\x y -> x ++ "\n |" +++ y) 
+        [gId f +++ foldr (+++) "" (map gId xx) | (f,xx) <- rules] ++++
+ "  deriving Show"
+
+-- GADT version of data types
+datatypesGADT :: (String,HSkeleton) -> String
+datatypesGADT (_,skel) = 
+    unlines (concatMap hCatTypeGADT skel)
+    +++++
+    "data Tree :: * -> * where" ++++ unlines (concatMap (map ("  "++) . hDatatypeGADT) skel)
+
+hCatTypeGADT :: (OIdent, [(OIdent, [OIdent])]) -> [String]
+hCatTypeGADT (cat,rules)
+    = ["type"+++gId cat+++"="+++"Tree"+++gId cat++"_",
+       "data"+++gId cat++"_"]
+
+hDatatypeGADT :: (OIdent, [(OIdent, [OIdent])]) -> [String]
+hDatatypeGADT (cat, rules) 
+    | isListCat (cat,rules) = [gId cat+++"::"+++"["++gId (elemCat cat)++"]" +++ "->" +++ t]
+    | otherwise =
+        [ gId f +++ "::" +++ concatMap (\a -> gId a +++ "-> ") args ++ t | (f,args) <- rules ]
+  where t = "Tree" +++ gId cat ++ "_"
+
+gfInstance m crs = hInstance m crs ++++ fInstance m crs
+
+----hInstance m ("Cn",_) = "" --- seems to belong to an old applic. AR 18/5/2004
+hInstance m (cat,[]) = "" 
+hInstance m (cat,rules) 
+ | isListCat (cat,rules) =
+  "instance Gf" +++ gId cat +++ "where" ++++
+     "  gf (" ++ gId cat +++ "[" ++ concat (intersperse "," baseVars) ++ "])" 
+           +++ "=" +++ mkRHS ("Base"++ec) baseVars ++++
+     "  gf (" ++ gId cat +++ "(x:xs)) = " 
+           ++ mkRHS ("Cons"++ec) ["x",prParenth (gId cat+++"xs")] 
+-- no show for GADTs
+--     ++++ " gf (" ++ gId cat +++ "xs) = error (\"Bad " ++ cat ++ " value: \" ++ show xs)" 
+ | otherwise =
+  "instance Gf" +++ gId cat +++ "where\n" ++
+  unlines [mkInst f xx | (f,xx) <- rules]
+ where
+   ec = elemCat cat
+   baseVars = mkVars (baseSize (cat,rules))
+   mkInst f xx = let xx' = mkVars (length xx) in "  gf " ++
+     (if length xx == 0 then gId f else prParenth (gId f +++ foldr1 (+++) xx')) +++
+     "=" +++ mkRHS f xx'
+   mkVars n = ["x" ++ show i | i <- [1..n]]
+   mkRHS f vars = "Fun (mkCId \"" ++ f ++ "\")" +++ 
+		   "[" ++ prTList ", " ["gf" +++ x | x <- vars] ++ "]"
+
+
+----fInstance m ("Cn",_) = "" ---
+fInstance m (cat,[]) = ""
+fInstance m (cat,rules) =
+  "  fg t =" ++++
+  "    case t of" ++++
+  unlines [mkInst f xx | (f,xx) <- rules] ++++
+  "      _ -> error (\"no" +++ cat ++ " \" ++ show t)"
+   where
+    mkInst f xx =
+     "      Fun i " ++
+     "[" ++ prTList "," xx' ++ "]" +++
+     "| i == mkCId \"" ++ f ++ "\" ->" +++ mkRHS f xx'
+       where xx' = ["x" ++ show i | (_,i) <- zip xx [1..]]
+	     mkRHS f vars 
+		 | isListCat (cat,rules) =
+		     if "Base" `isPrefixOf` f then
+			gId cat +++ "[" ++ prTList ", " [ "fg" +++ x | x <- vars ] ++ "]"
+		      else
+                       let (i,t) = (init vars,last vars)
+                        in "let" +++ gId cat +++ "xs = fg " ++ t +++ "in" +++ 
+                          gId cat +++ prParenth (prTList ":" (["fg"+++v | v <- i] ++ ["xs"]))
+		 | otherwise = 
+		     gId f +++  
+		     prTList " " [prParenth ("fg" +++ x) | x <- vars]
+
+
+--type HSkeleton = [(OIdent, [(OIdent, [OIdent])])]
+hSkeleton :: PGF -> (String,HSkeleton)
+hSkeleton gr = 
+  (prCId (absname gr), 
+   [(prCId c, [(prCId f, map prCId cs) | (f, (cs,_)) <- fs]) | 
+                                        fs@((_, (_,c)):_) <- fns]
+  )
+ where
+   fns = groupBy valtypg (sortBy valtyps (map jty (Map.assocs (funs (abstract gr)))))
+   valtyps (_, (_,x)) (_, (_,y)) = compare x y
+   valtypg (_, (_,x)) (_, (_,y)) = x == y
+   jty (f,(ty,_)) = (f,catSkeleton ty)
+
+updateSkeleton :: OIdent -> HSkeleton -> (OIdent, [OIdent]) -> HSkeleton
+updateSkeleton cat skel rule =
+ case skel of
+   (cat0,rules):rr | cat0 == cat -> (cat0, rule:rules) : rr
+   (cat0,rules):rr               -> (cat0, rules) : updateSkeleton cat rr rule
+
+isListCat :: (OIdent, [(OIdent, [OIdent])]) -> Bool
+isListCat (cat,rules) = "List" `isPrefixOf` cat && length rules == 2
+		    && ("Base"++c) `elem` fs && ("Cons"++c) `elem` fs
+    where c = elemCat cat
+	  fs = map fst rules
+
+-- | Gets the element category of a list category.
+elemCat :: OIdent -> OIdent
+elemCat = drop 4
+
+isBaseFun :: OIdent -> Bool
+isBaseFun f = "Base" `isPrefixOf` f
+
+isConsFun :: OIdent -> Bool
+isConsFun f = "Cons" `isPrefixOf` f
+
+baseSize :: (OIdent, [(OIdent, [OIdent])]) -> Int
+baseSize (_,rules) = length bs
+    where Just (_,bs) = find (("Base" `isPrefixOf`) . fst) rules
diff --git a/src/GF/Compile/GFCCtoJS.hs b/src/GF/Compile/GFCCtoJS.hs
new file mode 100644
index 000000000..8259e7385
--- /dev/null
+++ b/src/GF/Compile/GFCCtoJS.hs
@@ -0,0 +1,117 @@
+module GF.Compile.GFCCtoJS (pgf2js) where
+
+import PGF.CId
+import PGF.Data
+import qualified PGF.Macros as M
+import qualified GF.JavaScript.AbsJS as JS
+import qualified GF.JavaScript.PrintJS as JS
+
+import GF.Text.UTF8
+import GF.Data.ErrM
+import GF.Infra.Option
+
+import Control.Monad (mplus)
+import Data.Array (Array)
+import qualified Data.Array as Array
+import Data.Maybe (fromMaybe)
+import qualified Data.Map as Map
+
+pgf2js :: PGF -> String
+pgf2js pgf =
+  encodeUTF8 $ JS.printTree $ JS.Program [JS.ElStmt $ JS.SDeclOrExpr $ JS.Decl [JS.DInit (JS.Ident n) grammar]]
+ where
+   n  = prCId $ absname pgf
+   as = abstract pgf
+   cs = Map.assocs (concretes pgf)
+   start = M.lookStartCat pgf
+   grammar = new "GFGrammar" [js_abstract, js_concrete]
+   js_abstract = abstract2js start as
+   js_concrete = JS.EObj $ map (concrete2js start n) cs
+
+abstract2js :: String -> Abstr -> JS.Expr
+abstract2js start ds = new "GFAbstract" [JS.EStr start, JS.EObj $ map absdef2js (Map.assocs (funs ds))]
+
+absdef2js :: (CId,(Type,Expr)) -> JS.Property
+absdef2js (f,(typ,_)) =
+  let (args,cat) = M.catSkeleton typ in 
+    JS.Prop (JS.IdentPropName (JS.Ident (prCId f))) (new "Type" [JS.EArray [JS.EStr (prCId x) | x <- args], JS.EStr (prCId cat)])
+
+concrete2js :: String -> String -> (CId,Concr) -> JS.Property
+concrete2js start n (c, cnc) =
+    JS.Prop l (new "GFConcrete" ([(JS.EObj $ ((map (cncdef2js n (prCId c)) ds) ++ litslins))] ++
+                                 maybe [] (parser2js start) (parser cnc)))
+  where 
+   l  = JS.IdentPropName (JS.Ident (prCId c))
+   ds = concatMap Map.assocs [lins cnc, opers cnc, lindefs cnc]
+   litslins = [JS.Prop (JS.StringPropName    "Int") (JS.EFun [children] [JS.SReturn $ new "Arr" [JS.EIndex (JS.EVar children) (JS.EInt 0)]]), 
+               JS.Prop (JS.StringPropName  "Float") (JS.EFun [children] [JS.SReturn $ new "Arr" [JS.EIndex (JS.EVar children) (JS.EInt 0)]]),
+               JS.Prop (JS.StringPropName "String") (JS.EFun [children] [JS.SReturn $ new "Arr" [JS.EIndex (JS.EVar children) (JS.EInt 0)]])]
+
+
+cncdef2js :: String -> String -> (CId,Term) -> JS.Property
+cncdef2js n l (f, t) = JS.Prop (JS.IdentPropName (JS.Ident (prCId f))) (JS.EFun [children] [JS.SReturn (term2js n l t)])
+
+term2js :: String -> String -> Term -> JS.Expr
+term2js n l t = f t
+  where 
+  f t = 
+    case t of
+      R xs           -> new "Arr" (map f xs)
+      P x y          -> JS.ECall (JS.EMember (f x) (JS.Ident "sel")) [f y]
+      S xs           -> mkSeq (map f xs)
+      K t            -> tokn2js t
+      V i            -> JS.EIndex (JS.EVar children) (JS.EInt i)
+      C i            -> new "Int" [JS.EInt i]
+      F f            -> JS.ECall (JS.EMember (JS.EIndex (JS.EMember (JS.EVar $ JS.Ident n) (JS.Ident "concretes")) (JS.EStr l)) (JS.Ident "rule")) [JS.EStr (prCId f), JS.EVar children]
+      FV xs          -> new "Variants" (map f xs)
+      W str x        -> new "Suffix" [JS.EStr str, f x]
+      TM _           -> new "Meta" []
+
+tokn2js :: Tokn -> JS.Expr
+tokn2js (KS s) = mkStr s
+tokn2js (KP ss vs) = mkSeq (map mkStr ss) -- FIXME
+
+mkStr :: String -> JS.Expr
+mkStr s = new "Str" [JS.EStr s]
+
+mkSeq :: [JS.Expr] -> JS.Expr
+mkSeq [x] = x
+mkSeq xs = new "Seq" xs
+
+argIdent :: Integer -> JS.Ident
+argIdent n = JS.Ident ("x" ++ show n)
+
+children :: JS.Ident
+children = JS.Ident "cs"
+
+-- Parser
+parser2js :: String -> ParserInfo -> [JS.Expr]
+parser2js start p  = [new "Parser" [JS.EStr start,
+                                    JS.EArray $ map frule2js (Array.elems (allRules p)),
+                                    JS.EObj $ map cats (Map.assocs (startupCats p))]]
+  where 
+    cats (c,is) = JS.Prop (JS.IdentPropName (JS.Ident (prCId c))) (JS.EArray (map JS.EInt is))
+
+frule2js :: FRule -> JS.Expr
+frule2js (FRule f ps args res lins) = new "Rule" [JS.EInt res, name2js (f,ps), JS.EArray (map JS.EInt args), lins2js lins]
+
+name2js :: (CId,[Profile]) -> JS.Expr
+name2js (f,ps) | f == wildCId = fromProfile (head ps)
+               | otherwise    = new "FunApp" $ [JS.EStr $ prCId f, JS.EArray (map fromProfile ps)]
+  where
+    fromProfile :: Profile -> JS.Expr
+    fromProfile []   = new "MetaVar" []
+    fromProfile [x]  = daughter x
+    fromProfile args = new "Unify" [JS.EArray (map daughter args)]
+
+    daughter i = new "Arg" [JS.EInt i]
+
+lins2js :: Array FIndex (Array FPointPos FSymbol) -> JS.Expr
+lins2js ls = JS.EArray [ JS.EArray [ sym2js s | s <- Array.elems l] | l <- Array.elems ls]
+
+sym2js :: FSymbol -> JS.Expr
+sym2js (FSymCat l n) = new "ArgProj" [JS.EInt n, JS.EInt l]
+sym2js (FSymTok t) = new "Terminal" [JS.EStr t]
+
+new :: String -> [JS.Expr] -> JS.Expr
+new f xs = JS.ENew (JS.Ident f) xs
diff --git a/src/GF/Compile/GenerateFCFG.hs b/src/GF/Compile/GenerateFCFG.hs
new file mode 100644
index 000000000..c2854ef3d
--- /dev/null
+++ b/src/GF/Compile/GenerateFCFG.hs
@@ -0,0 +1,526 @@
+----------------------------------------------------------------------
+-- |
+-- Maintainer  : Krasimir Angelov
+-- Stability   : (stable)
+-- Portability : (portable)
+--
+-- Converting SimpleGFC grammars to fast nonerasing MCFG grammar.
+--
+-- the resulting grammars might be /very large/
+--
+-- the conversion is only equivalent if the GFC grammar has a context-free backbone.
+-----------------------------------------------------------------------------
+
+
+module GF.Compile.GenerateFCFG
+    (convertConcrete) where
+
+import PGF.CId
+import PGF.Data
+import PGF.Macros --hiding (prt)
+import PGF.Parsing.FCFG.Utilities
+
+import GF.Data.BacktrackM
+import GF.Data.SortedList
+import GF.Data.Utilities (updateNthM, sortNub)
+
+import qualified Data.Map as Map
+import qualified Data.Set as Set
+import qualified Data.List as List
+import qualified Data.ByteString.Char8 as BS
+import Data.Array
+import Data.Maybe
+import Control.Monad
+
+----------------------------------------------------------------------
+-- main conversion function
+
+convertConcrete :: Abstr -> Concr -> FGrammar
+convertConcrete abs cnc = fixHoasFuns $ convert abs_defs' conc' cats'
+       where abs_defs = Map.assocs (funs abs)
+             conc = Map.union (opers cnc) (lins cnc) -- "union big+small most efficient"
+             cats = lincats cnc
+             (abs_defs',conc',cats') = expandHOAS abs_defs conc cats
+
+expandHOAS :: [(CId,(Type,Expr))] -> TermMap -> TermMap -> ([(CId,(Type,Expr))],TermMap,TermMap)
+expandHOAS funs lins lincats = (funs' ++ hoFuns ++ varFuns, 
+                                Map.unions [lins, hoLins, varLins], 
+                                Map.unions [lincats, hoLincats, varLincat])
+    where
+      -- replace higher-order fun argument types with new categories
+      funs' = [(f,(fixType ty,e)) | (f,(ty,e)) <- funs]
+          where
+            fixType :: Type -> Type
+            fixType ty = let (ats,rt) = typeSkeleton ty in cftype (map catName ats) rt
+
+      hoTypes :: [(Int,CId)]
+      hoTypes = sortNub [(n,c) | (_,(ty,_)) <- funs, (n,c) <- fst (typeSkeleton ty), n > 0]
+      hoCats = sortNub (map snd hoTypes)
+      -- for each Cat with N bindings, we add a new category _NCat
+      -- each new category contains a single function __NCat : Cat -> _Var -> ... -> _Var -> _NCat
+      hoFuns = [(funName ty,(cftype (c : replicate n varCat) (catName ty),EEq [])) | ty@(n,c) <- hoTypes]
+      -- lincats for the new categories
+      hoLincats = Map.fromList [(catName ty, modifyRec (++ replicate n (S [])) (lincatOf c)) | ty@(n,c) <- hoTypes]
+      -- linearizations of the new functions, lin __NCat v_0 ... v_n-1 x = { s1 = x.s1; ...; sk = x.sk; $0 = v_0.s ...
+      hoLins = Map.fromList [ (funName ty, mkLin c n) | ty@(n,c) <- hoTypes]
+          where mkLin c n = modifyRec (\fs -> [P (V 0) (C j) | j <- [0..length fs-1]] ++ [P (V i) (C 0) | i <- [1..n]]) (lincatOf c)
+      -- for each Cat, we a add a fun _Var_Cat : _Var -> Cat
+      varFuns = [(varFunName cat, (cftype [varCat] cat,EEq [])) | cat <- hoCats]
+      -- linearizations of the _Var_Cat functions
+      varLins = Map.fromList [(varFunName cat, R [P (V 0) (C 0)]) | cat <- hoCats]
+      -- lincat for the _Var category
+      varLincat = Map.singleton varCat (R [S []])
+
+      lincatOf c = fromMaybe (error $ "No lincat for " ++ prCId c) $ Map.lookup c lincats
+
+      modifyRec :: ([Term] -> [Term]) -> Term -> Term
+      modifyRec f (R xs) = R (f xs)
+      modifyRec _ t = error $ "Not a record: " ++ show t
+
+      varCat = mkCId "_Var"
+
+      catName :: (Int,CId) -> CId
+      catName (0,c) = c
+      catName (n,c) = mkCId ("_" ++ show n ++ prCId c)
+
+      funName :: (Int,CId) -> CId
+      funName (n,c) = mkCId ("__" ++ show n ++ prCId c)
+
+      varFunName :: CId -> CId
+      varFunName c = mkCId ("_Var_" ++ prCId c)
+
+-- replaces __NCat with _B and _Var_Cat with _.
+-- the temporary names are just there to avoid name collisions.
+fixHoasFuns :: FGrammar -> FGrammar
+fixHoasFuns (rs, cs) = ([FRule (fixName n) ps args cat lins | FRule n ps args cat lins <- rs], cs)
+  where fixName (CId n) | BS.pack "__"    `BS.isPrefixOf` n = (mkCId "_B")
+                        | BS.pack "_Var_" `BS.isPrefixOf` n = wildCId
+        fixName n = n
+
+convert :: [(CId,(Type,Expr))] -> TermMap -> TermMap -> FGrammar
+convert abs_defs cnc_defs cat_defs = getFGrammar (loop frulesEnv)
+      where
+        srules = [
+          (XRule id args res (map findLinType args) (findLinType res) term) | 
+            (id, (ty,_)) <- abs_defs, let (args,res) = catSkeleton ty, 
+            term <- Map.lookup id cnc_defs]
+        
+        findLinType id = fromMaybe (error $ "No lincat for " ++ show id) (Map.lookup id cat_defs)
+
+        (xrulesMap,frulesEnv) = List.foldl' helper (Map.empty,emptyFRulesEnv) srules
+           where
+	     helper (xrulesMap,frulesEnv) rule@(XRule id abs_args abs_res cnc_args cnc_res term) = 
+	       let xrulesMap' = Map.insertWith (++) abs_res [rule] xrulesMap
+	           frulesEnv' = List.foldl' (\env selector -> convertRule cnc_defs selector rule env)
+	                                    frulesEnv
+	                                    (mkSingletonSelectors cnc_defs cnc_res)
+               in xrulesMap' `seq` frulesEnv' `seq` (xrulesMap',frulesEnv')
+
+        loop frulesEnv =
+          let (todo, frulesEnv') = takeToDoRules xrulesMap frulesEnv
+          in case todo of
+               [] -> frulesEnv'
+               _  -> loop $! List.foldl' (\env (srules,selector) -> 
+                             List.foldl' (\env srule             -> convertRule cnc_defs selector srule env) env srules) frulesEnv' todo
+
+convertRule :: TermMap -> TermSelector -> XRule -> FRulesEnv -> FRulesEnv
+convertRule cnc_defs selector (XRule fun args cat ctypes ctype term) frulesEnv =
+  foldBM addRule
+         frulesEnv
+         (convertTerm cnc_defs selector term [([],[])])
+         (protoFCat cat, map (\scat -> (protoFCat scat,[])) args, ctype, ctypes)
+  where
+    addRule linRec (newCat', newArgs', _, _) env0 =
+      let (env1, newCat)          = genFCatHead env0 newCat'
+          (env2, newArgs,idxArgs) = foldr (\((xcat@(PFCat cat rcs tcs),xpaths),ctype,idx) (env,args,all_args) ->
+                                       let xargs          = xcat:[PFCat cat [path] tcs | path <- reverse xpaths]
+                                           (env1, xargs1) = List.mapAccumL (genFCatArg cnc_defs ctype) env xargs
+                                       in case xcat of
+                                            PFCat _ [] _ -> (env ,        args,                       all_args)
+                                            _            -> (env1,xargs1++args,(idx,zip xargs1 xargs):all_args)) (env1,[],[]) (zip3 newArgs' ctypes [0..])
+
+          newLinRec = listArray (0,length linRec-1) [translateLin idxArgs path linRec | path <- case newCat' of {PFCat _ rcs _ -> rcs}]
+
+          (_,newProfile) = List.mapAccumL accumProf 0 newArgs'
+            where
+              accumProf nr (PFCat _ [] _,_     ) = (nr,       []          )
+              accumProf nr (_           ,xpaths) = (nr+cnt+1, [nr..nr+cnt])
+                where cnt = length xpaths
+
+          rule = FRule fun newProfile newArgs newCat newLinRec
+      in addFRule env2 rule
+
+translateLin idxArgs lbl' []                    = array (0,-1) []
+translateLin idxArgs lbl' ((lbl,syms) : lins)
+  | lbl' == lbl = listArray (0,length syms-1) (map instSym syms)
+  | otherwise   = translateLin idxArgs lbl' lins
+  where
+    instSym = either (\(lbl, nr, xnr) -> instCat lbl nr xnr 0 idxArgs) FSymTok
+    instCat lbl nr xnr nr' ((idx,xargs):idxArgs)
+      | nr == idx = let (fcat, PFCat _ rcs _) = xargs !! xnr
+                    in FSymCat (index lbl rcs 0) (nr'+xnr)
+      | otherwise = instCat lbl nr xnr (nr'+length xargs) idxArgs
+
+    index lbl' (lbl:lbls) idx
+      | lbl' == lbl = idx
+      | otherwise   = index lbl' lbls $! (idx+1)
+
+
+----------------------------------------------------------------------
+-- term conversion
+
+type CnvMonad a = BacktrackM Env a
+
+type FPath   = [FIndex]
+type Env     = (ProtoFCat, [(ProtoFCat,[FPath])], Term, [Term])
+type LinRec  = [(FPath, [Either (FPath, FIndex, Int) FToken])]
+
+type TermMap = Map.Map CId Term
+
+convertTerm :: TermMap -> TermSelector -> Term -> LinRec -> CnvMonad LinRec
+convertTerm cnc_defs selector (V nr)       ((lbl_path,lin) : lins) = convertArg selector nr []    lbl_path lin lins
+convertTerm cnc_defs selector (C nr)       ((lbl_path,lin) : lins) = convertCon selector nr       lbl_path lin lins
+convertTerm cnc_defs selector (R record)   ((lbl_path,lin) : lins) = convertRec cnc_defs selector 0 record lbl_path lin lins
+
+convertTerm cnc_defs selector (P term sel)                   lins  = do nr <- evalTerm cnc_defs [] sel
+                                                                        convertTerm cnc_defs (TuplePrj nr selector) term lins
+convertTerm cnc_defs selector (FV vars)                      lins  = do term <- member vars
+                                                                        convertTerm cnc_defs selector term lins
+convertTerm cnc_defs selector (S ts)       ((lbl_path,lin) : lins) = do projectHead lbl_path
+                                                                        foldM (\lins t -> convertTerm cnc_defs selector t lins) ((lbl_path,lin) : lins) (reverse ts)
+convertTerm cnc_defs selector (K (KS str)) ((lbl_path,lin) : lins) = 
+  do projectHead lbl_path
+     return ((lbl_path,Right str : lin) : lins)
+convertTerm cnc_defs selector (K (KP strs vars))((lbl_path,lin) : lins) = 
+  do projectHead lbl_path
+     toks <- member (strs:[strs' | Alt strs' _ <- vars])
+     return ((lbl_path, map Right toks ++ lin) : lins)
+convertTerm cnc_defs selector (F id)                         lins  = do term <- Map.lookup id cnc_defs
+                                                                        convertTerm cnc_defs selector term lins
+convertTerm cnc_defs selector (W s t)     ((lbl_path,lin) : lins) = do
+  ss <- case t of
+    R ss -> return ss
+    F f -> do
+      t <- Map.lookup f cnc_defs 
+      case t of
+        R ss -> return ss
+  convertRec cnc_defs selector 0 [K (KS (s ++ s1)) | K (KS s1) <- ss] lbl_path lin lins
+convertTerm cnc_defs selector x lins  = error ("convertTerm ("++show x++")")
+
+
+convertArg (TupleSel record)  nr path lbl_path lin lins =
+  foldM (\lins (lbl,  selector) -> convertArg selector nr (lbl:path)  (lbl:lbl_path) lin lins) lins record
+convertArg (TuplePrj lbl selector) nr path lbl_path lin lins = 
+  convertArg selector nr (lbl:path) lbl_path lin lins
+convertArg (ConSel indices) nr path lbl_path lin lins = do
+  index <- member indices
+  restrictHead lbl_path index
+  restrictArg nr path index
+  return lins
+convertArg StrSel nr path lbl_path lin lins = do
+  projectHead lbl_path
+  xnr <- projectArg nr path
+  return ((lbl_path, Left (path, nr, xnr) : lin) : lins)
+
+convertCon (ConSel indices) index lbl_path lin lins = do
+  guard (index `elem` indices)
+  restrictHead lbl_path index
+  return lins
+convertCon x _ _ _ _ = error $ "SimpleToFCFG,convertCon: " ++ show x
+
+convertRec cnc_defs selector                   index []           lbl_path lin lins = return lins
+convertRec cnc_defs selector@(TupleSel fields) index (val:record) lbl_path lin lins = select fields
+  where
+    select []                          = convertRec cnc_defs selector (index+1) record lbl_path lin lins
+    select ((index',sub_sel) : fields)
+      | index == index'                = do lins <- convertTerm cnc_defs sub_sel val ((index:lbl_path,lin) : lins)
+                                            convertRec cnc_defs selector (index+1) record lbl_path lin lins
+      | otherwise                      = select fields
+convertRec cnc_defs (TuplePrj index' sub_sel) index record lbl_path lin lins = do
+  convertTerm cnc_defs sub_sel (record !! (index'-index)) ((lbl_path,lin) : lins)
+
+
+------------------------------------------------------------
+-- eval a term to ground terms
+
+evalTerm :: TermMap -> FPath -> Term -> CnvMonad FIndex
+evalTerm cnc_defs path (V nr)       = do term <- readArgCType nr
+                                         unifyPType nr (reverse path) (selectTerm path term)
+evalTerm cnc_defs path (C nr)       = return nr
+evalTerm cnc_defs path (R record)   = case path of
+                                        (index:path) -> evalTerm cnc_defs path (record !! index)
+evalTerm cnc_defs path (P term sel) = do index <- evalTerm cnc_defs [] sel
+                                         evalTerm cnc_defs (index:path) term
+evalTerm cnc_defs path (FV terms)   = member terms >>= evalTerm cnc_defs path
+evalTerm cnc_defs path (F id)       = do term <- Map.lookup id cnc_defs
+                                         evalTerm cnc_defs path term
+evalTerm cnc_defs path x = error ("evalTerm ("++show x++")")
+
+unifyPType :: FIndex -> FPath -> Term -> CnvMonad FIndex
+unifyPType nr path (C max_index) =
+    do (_, args, _, _) <- readState
+       let (PFCat _ _ tcs,_) = args !! nr
+       case lookup path tcs of
+         Just index -> return index
+         Nothing    -> do index <- member [0..max_index]
+		          restrictArg nr path index
+		          return index
+unifyPType nr path t = error $ "unifyPType " ++ show t ---- AR 2/10/2007
+
+selectTerm :: FPath -> Term -> Term
+selectTerm []           term        = term
+selectTerm (index:path) (R  record) = selectTerm path (record !! index)
+
+
+----------------------------------------------------------------------
+-- FRulesEnv
+
+data FRulesEnv = FRulesEnv {-# UNPACK #-} !Int FCatSet [FRule]
+type FCatSet   = Map.Map CId (Map.Map [FPath] (Map.Map [(FPath,FIndex)] (Either FCat FCat)))
+
+data ProtoFCat = PFCat CId [FPath] [(FPath,FIndex)]
+
+protoFCat :: CId -> ProtoFCat
+protoFCat cat = PFCat cat [] []
+
+emptyFRulesEnv = FRulesEnv 0 (ins fcatString (mkCId "String") [[0]] [] $
+                              ins fcatInt    (mkCId "Int")    [[0]] [] $
+                              ins fcatFloat  (mkCId "Float")  [[0]] [] $
+                              ins fcatVar    (mkCId "_Var")   [[0]] [] $
+                              Map.empty) []
+  where
+    ins fcat cat rcs tcs fcatSet =
+      Map.insertWith (\_ -> Map.insertWith (\_ -> Map.insert tcs right_fcat) rcs tmap_s) cat rmap_s fcatSet
+      where
+        right_fcat = Right fcat
+        tmap_s = Map.singleton tcs right_fcat
+        rmap_s = Map.singleton rcs tmap_s
+
+addFRule :: FRulesEnv -> FRule -> FRulesEnv
+addFRule (FRulesEnv last_id fcatSet rules) rule = FRulesEnv last_id fcatSet (rule:rules)
+
+getFGrammar :: FRulesEnv -> FGrammar
+getFGrammar (FRulesEnv last_id fcatSet rules) = (rules, Map.map getFCatList fcatSet)
+  where
+    getFCatList rcs = Map.fold (\tcs lst -> Map.fold (\x lst -> either id id x : lst) lst tcs) [] rcs
+
+genFCatHead :: FRulesEnv -> ProtoFCat -> (FRulesEnv, FCat)
+genFCatHead env@(FRulesEnv last_id fcatSet rules) (PFCat cat rcs tcs) =
+  case Map.lookup cat fcatSet >>= Map.lookup rcs >>= Map.lookup tcs of
+    Just (Left  fcat) -> (FRulesEnv last_id (ins fcat) rules, fcat)
+    Just (Right fcat) -> (env, fcat)
+    Nothing           -> let fcat = last_id+1
+                         in (FRulesEnv fcat (ins fcat) rules, fcat)
+  where
+    ins fcat = Map.insertWith (\_ -> Map.insertWith (\_ -> Map.insert tcs right_fcat) rcs tmap_s) cat rmap_s fcatSet
+      where
+        right_fcat = Right fcat
+        tmap_s = Map.singleton tcs right_fcat
+        rmap_s = Map.singleton rcs tmap_s
+
+genFCatArg :: TermMap -> Term -> FRulesEnv -> ProtoFCat -> (FRulesEnv, FCat)
+genFCatArg cnc_defs ctype env@(FRulesEnv last_id fcatSet rules) (PFCat cat rcs tcs) =
+  case Map.lookup cat fcatSet >>= Map.lookup rcs of
+    Just tmap -> case Map.lookup tcs tmap of
+                   Just (Left  fcat) -> (env,   fcat)
+                   Just (Right fcat) -> (env,   fcat)
+                   Nothing           -> ins tmap
+    Nothing   -> ins Map.empty
+  where
+    ins tmap =
+      let fcat = last_id+1
+          (either_fcat,last_id1,tmap1,rules1)
+                  = foldBM (\tcs st (either_fcat,last_id,tmap,rules) ->
+                                   let (last_id1,tmap1,fcat_arg) = addArg tcs last_id tmap
+                                       rule = FRule wildCId [[0]] [fcat_arg] fcat
+                                                    (listArray (0,length rcs-1) [listArray (0,0) [FSymCat lbl 0] | lbl <- [0..length rcs-1]])
+                                   in if st
+                                        then (Right fcat, last_id1,tmap1,rule:rules)
+                                        else (either_fcat,last_id, tmap,      rules))
+                           (Left fcat,fcat,Map.insert tcs either_fcat tmap,rules)
+                           (gen_tcs ctype [] [])
+                           False
+          rmap1 = Map.singleton rcs tmap1
+      in (FRulesEnv last_id1 (Map.insertWith (\_ -> Map.insert rcs tmap1) cat rmap1 fcatSet) rules1, fcat)
+      where
+        addArg tcs last_id tmap =
+	  case Map.lookup tcs tmap of
+	    Just (Left  fcat) -> (last_id, tmap, fcat)
+	    Just (Right fcat) -> (last_id, tmap, fcat)
+	    Nothing           -> let fcat = last_id+1
+                                 in (fcat, Map.insert tcs (Left fcat) tmap, fcat)
+
+    gen_tcs :: Term -> FPath -> [(FPath,FIndex)] -> BacktrackM Bool [(FPath,FIndex)]
+    gen_tcs (R record)    path acc = foldM (\acc (label,ctype) -> gen_tcs ctype (label:path) acc) acc (zip [0..] record)
+    gen_tcs (S _)         path acc = return acc
+    gen_tcs (C max_index) path acc =
+      case List.lookup path tcs of
+        Just index -> return $! addConstraint path index acc
+        Nothing    -> do writeState True
+                         index <- member [0..max_index]
+                         return $! addConstraint path index acc
+      where
+        addConstraint path0 index0 (c@(path,index) : cs)
+	  | path0 > path = c:addConstraint path0 index0 cs
+        addConstraint path0 index0 cs  = (path0,index0) : cs
+    gen_tcs (F id)        path acc = case Map.lookup id cnc_defs of
+                                        Just term -> gen_tcs term path acc
+                                        Nothing   -> error ("unknown identifier: "++prCId id)
+
+
+
+------------------------------------------------------------
+-- TODO queue organization
+
+type XRulesMap = Map.Map CId [XRule]
+data XRule     = XRule CId     {- function -}
+                       [CId]   {- argument types -}
+                       CId     {- result   type  -}
+                       [Term]  {- argument lin-types representation -}
+                       Term    {- result   lin-type  representation -}
+                       Term    {- body -}
+
+takeToDoRules :: XRulesMap -> FRulesEnv -> ([([XRule], TermSelector)], FRulesEnv)
+takeToDoRules xrulesMap (FRulesEnv last_id fcatSet rules) = (todo,FRulesEnv last_id fcatSet' rules)
+  where
+    (todo,fcatSet') =
+          Map.mapAccumWithKey (\todo cat rmap ->
+                let (todo1,rmap1) = Map.mapAccumWithKey (\todo rcs tmap -> 
+                                          let (tcss,tmap') = Map.mapAccumWithKey (\tcss tcs either_xcat ->
+                                                                   case either_xcat of
+                                                                     Left  xcat -> (tcs:tcss,Right xcat)
+                                                                     Right xcat -> (    tcss,either_xcat)) [] tmap
+                                          in case tcss of
+                                               [] -> (                               todo,tmap )
+                                               _  -> ((srules,mkSelector rcs tcss) : todo,tmap')) todo rmap
+                    mb_srules   = Map.lookup cat xrulesMap
+                    Just srules = mb_srules
+
+                in case mb_srules of
+                     Just srules -> (todo1,rmap1)
+                     Nothing     -> (todo ,rmap1)) [] fcatSet
+
+
+------------------------------------------------------------
+-- The TermSelector
+
+data TermSelector
+  = TupleSel [(FIndex, TermSelector)]
+  | TuplePrj   FIndex  TermSelector
+  | ConSel   [FIndex]
+  | StrSel
+  deriving Show
+
+mkSingletonSelectors :: TermMap 
+                     -> Term               -- ^ Type representation term
+                     -> [TermSelector]     -- ^ list of selectors containing just one string field
+mkSingletonSelectors cnc_defs term = sels0
+  where
+    (sels0,tcss0) = loop [] ([],[]) term
+
+    loop path st          (R record) = List.foldl' (\st (index,term) -> loop (index:path) st term) st (zip [0..] record)
+    loop path (sels,tcss) (C i)      = (                          sels,map ((,) path) [0..i] : tcss)
+    loop path (sels,tcss) (S _)      = (mkSelector [path] tcss0 : sels,                        tcss)
+    loop path (sels,tcss) (F id)     = case Map.lookup id cnc_defs of
+                                         Just term -> loop path (sels,tcss) term
+                                         Nothing   -> error ("unknown identifier: "++prCId id)
+
+mkSelector :: [FPath] -> [[(FPath,FIndex)]] -> TermSelector
+mkSelector rcs tcss =
+  List.foldl' addRestriction (case xs of
+                                (path:xs) -> List.foldl' addProjection (path2selector StrSel path) xs) ys
+  where
+    xs = [ reverse path       |               path       <- rcs]
+    ys = [(reverse path,term) | tcs <- tcss, (path,term) <- tcs]
+    
+    addRestriction :: TermSelector -> (FPath,FIndex) -> TermSelector
+    addRestriction (ConSel indices)  ([]          ,n_index) = ConSel (add indices)
+      where
+        add []                      = [n_index]
+        add (index':indices)
+          | n_index == index'       = index':    indices
+          | otherwise               = index':add indices
+    addRestriction (TupleSel fields) (index : path,n_index) = TupleSel (add fields)
+      where
+        add []                      = [(index,path2selector (ConSel [n_index]) path)]
+        add (field@(index',sub_sel):fields)
+          | index == index'         = (index',addRestriction sub_sel (path,n_index)):fields
+          | otherwise               = field : add fields
+
+    addProjection :: TermSelector -> FPath -> TermSelector
+    addProjection StrSel            []             = StrSel
+    addProjection (TupleSel fields) (index : path) = TupleSel (add fields)
+      where
+        add []                      = [(index,path2selector StrSel path)]
+        add (field@(index',sub_sel):fields)
+          | index == index'         = (index',addProjection sub_sel path):fields
+          | otherwise               = field : add fields
+    
+    path2selector base []             = base
+    path2selector base (index : path) = TupleSel [(index,path2selector base path)]
+
+------------------------------------------------------------
+-- updating the MCF rule
+
+readArgCType :: FIndex -> CnvMonad Term
+readArgCType nr = do (_, _, _, ctypes) <- readState
+		     return (ctypes !! nr)
+
+restrictArg :: FIndex -> FPath -> FIndex -> CnvMonad ()
+restrictArg nr path index = do
+  (head, args, ctype, ctypes) <- readState 
+  args' <- updateNthM (\(xcat,xs) -> do xcat <- restrictProtoFCat path index xcat
+                                        return (xcat,xs)                         ) nr args
+  writeState (head, args', ctype, ctypes)
+
+projectArg :: FIndex -> FPath -> CnvMonad Int
+projectArg nr path = do
+  (head, args, ctype, ctypes) <- readState
+  (xnr,args') <- updateArgs nr args
+  writeState (head, args', ctype, ctypes)
+  return xnr
+  where
+    updateArgs :: FIndex -> [(ProtoFCat,[FPath])] -> CnvMonad (Int,[(ProtoFCat,[FPath])])
+    updateArgs 0 ((a@(PFCat _ rcs _),xpaths) : as)
+      | path `elem` rcs = return (length xpaths+1,(a,path:xpaths):as)
+      | otherwise       = do a <- projectProtoFCat path a
+                             return (0,(a,xpaths):as)
+    updateArgs n (a : as) = do
+      (xnr,as) <- updateArgs (n-1) as
+      return (xnr,a:as)
+
+readHeadCType :: CnvMonad Term
+readHeadCType = do (_, _, ctype, _) <- readState
+		   return ctype
+
+restrictHead :: FPath -> FIndex -> CnvMonad ()
+restrictHead path term
+    = do (head, args, ctype, ctypes) <- readState
+	 head' <- restrictProtoFCat path term head
+	 writeState (head', args, ctype, ctypes)
+
+projectHead :: FPath -> CnvMonad ()
+projectHead path
+    = do (head, args, ctype, ctypes) <- readState
+	 head' <- projectProtoFCat path head
+	 writeState (head', args, ctype, ctypes)
+
+restrictProtoFCat :: FPath -> FIndex -> ProtoFCat -> CnvMonad ProtoFCat
+restrictProtoFCat path0 index0 (PFCat cat rcs tcs) = do
+  tcs <- addConstraint tcs
+  return (PFCat cat rcs tcs)
+  where
+    addConstraint (c@(path,index) : cs)
+        | path0 >  path = liftM (c:) (addConstraint cs)
+        | path0 == path = guard (index0 == index) >>
+                          return (c : cs)
+    addConstraint cs    = return ((path0,index0) : cs)
+
+projectProtoFCat :: FPath -> ProtoFCat -> CnvMonad ProtoFCat
+projectProtoFCat path0 (PFCat cat rcs tcs) = do
+  return (PFCat cat (addConstraint rcs) tcs)
+  where
+    addConstraint (path : rcs)
+        | path0 >  path = path  : addConstraint rcs
+        | path0 == path = path  : rcs
+    addConstraint rcs   = path0 : rcs
diff --git a/src/GF/Compile/GeneratePMCFG.hs b/src/GF/Compile/GeneratePMCFG.hs
new file mode 100644
index 000000000..e0343e8d6
--- /dev/null
+++ b/src/GF/Compile/GeneratePMCFG.hs
@@ -0,0 +1,356 @@
+{-# OPTIONS -fbang-patterns #-}
+----------------------------------------------------------------------
+-- |
+-- Maintainer  : Krasimir Angelov
+-- Stability   : (stable)
+-- Portability : (portable)
+--
+-- Converting SimpleGFC grammars to fast nonerasing MCFG grammar.
+--
+-- the resulting grammars might be /very large/
+--
+-- the conversion is only equivalent if the GFC grammar has a context-free backbone.
+-----------------------------------------------------------------------------
+
+
+module GF.Compile.GeneratePMCFG
+    (convertConcrete) where
+
+import PGF.CId
+import PGF.Data
+import PGF.Macros --hiding (prt)
+import PGF.Parsing.FCFG.Utilities
+
+import GF.Data.BacktrackM
+import GF.Data.SortedList
+import GF.Data.Utilities (updateNthM, sortNub)
+
+import qualified Data.Map as Map
+import qualified Data.Set as Set
+import qualified Data.List as List
+import qualified Data.ByteString.Char8 as BS
+import Data.Array
+import Data.Maybe
+import Control.Monad
+import Debug.Trace
+
+----------------------------------------------------------------------
+-- main conversion function
+
+convertConcrete :: Abstr -> Concr -> FGrammar
+convertConcrete abs cnc = fixHoasFuns $ convert abs_defs' conc' cats'
+       where abs_defs = Map.assocs (funs abs)
+             conc = Map.union (opers cnc) (lins cnc) -- "union big+small most efficient"
+             cats = lincats cnc
+             (abs_defs',conc',cats') = expandHOAS abs_defs conc cats
+
+expandHOAS :: [(CId,(Type,Expr))] -> TermMap -> TermMap -> ([(CId,(Type,Expr))],TermMap,TermMap)
+expandHOAS funs lins lincats = (funs' ++ hoFuns ++ varFuns, 
+                                Map.unions [lins, hoLins, varLins], 
+                                Map.unions [lincats, hoLincats, varLincat])
+    where
+      -- replace higher-order fun argument types with new categories
+      funs' = [(f,(fixType ty,e)) | (f,(ty,e)) <- funs]
+          where
+            fixType :: Type -> Type
+            fixType ty = let (ats,rt) = typeSkeleton ty in cftype (map catName ats) rt
+
+      hoTypes :: [(Int,CId)]
+      hoTypes = sortNub [(n,c) | (_,(ty,_)) <- funs, (n,c) <- fst (typeSkeleton ty), n > 0]
+      hoCats = sortNub (map snd hoTypes)
+      -- for each Cat with N bindings, we add a new category _NCat
+      -- each new category contains a single function __NCat : Cat -> _Var -> ... -> _Var -> _NCat
+      hoFuns = [(funName ty,(cftype (c : replicate n varCat) (catName ty),EEq [])) | ty@(n,c) <- hoTypes]
+      -- lincats for the new categories
+      hoLincats = Map.fromList [(catName ty, modifyRec (++ replicate n (S [])) (lincatOf c)) | ty@(n,c) <- hoTypes]
+      -- linearizations of the new functions, lin __NCat v_0 ... v_n-1 x = { s1 = x.s1; ...; sk = x.sk; $0 = v_0.s ...
+      hoLins = Map.fromList [ (funName ty, mkLin c n) | ty@(n,c) <- hoTypes]
+          where mkLin c n = modifyRec (\fs -> [P (V 0) (C j) | j <- [0..length fs-1]] ++ [P (V i) (C 0) | i <- [1..n]]) (lincatOf c)
+      -- for each Cat, we a add a fun _Var_Cat : _Var -> Cat
+      varFuns = [(varFunName cat, (cftype [varCat] cat,EEq [])) | cat <- hoCats]
+      -- linearizations of the _Var_Cat functions
+      varLins = Map.fromList [(varFunName cat, R [P (V 0) (C 0)]) | cat <- hoCats]
+      -- lincat for the _Var category
+      varLincat = Map.singleton varCat (R [S []])
+
+      lincatOf c = fromMaybe (error $ "No lincat for " ++ prCId c) $ Map.lookup c lincats
+
+      modifyRec :: ([Term] -> [Term]) -> Term -> Term
+      modifyRec f (R xs) = R (f xs)
+      modifyRec _ t = error $ "Not a record: " ++ show t
+
+      varCat = mkCId "_Var"
+
+      catName :: (Int,CId) -> CId
+      catName (0,c) = c
+      catName (n,c) = mkCId ("_" ++ show n ++ prCId c)
+
+      funName :: (Int,CId) -> CId
+      funName (n,c) = mkCId ("__" ++ show n ++ prCId c)
+
+      varFunName :: CId -> CId
+      varFunName c = mkCId ("_Var_" ++ prCId c)
+
+-- replaces __NCat with _B and _Var_Cat with _.
+-- the temporary names are just there to avoid name collisions.
+fixHoasFuns :: FGrammar -> FGrammar
+fixHoasFuns (!rs, !cs) = ([FRule (fixName n) ps args cat lins | FRule n ps args cat lins <- rs], cs)
+  where fixName (CId n) | BS.pack "__"    `BS.isPrefixOf` n = (mkCId "_B")
+                        | BS.pack "_Var_" `BS.isPrefixOf` n = wildCId
+        fixName n = n
+
+convert :: [(CId,(Type,Expr))] -> TermMap -> TermMap -> FGrammar
+convert abs_defs cnc_defs cat_defs = getFGrammar (List.foldl' (convertRule cnc_defs) emptyFRulesEnv srules)
+  where
+    srules = [
+      (XRule id args res (map findLinType args) (findLinType res) term) | 
+        (id, (ty,_)) <- abs_defs, let (args,res) = catSkeleton ty, 
+        term <- Map.lookup id cnc_defs]
+        
+    findLinType id = fromMaybe (error $ "No lincat for " ++ show id) (Map.lookup id cat_defs)
+
+
+convertRule :: TermMap -> FRulesEnv -> XRule -> FRulesEnv
+convertRule cnc_defs frulesEnv (XRule fun args cat ctypes ctype term) =
+  foldBM addRule
+         frulesEnv
+         (convertTerm cnc_defs [] ctype term [([],[])])
+         (protoFCat cnc_defs cat ctype, zipWith (protoFCat cnc_defs) args ctypes)
+  where
+    addRule linRec (newCat', newArgs') env0 =
+      let (env1, newCat)  = genFCatHead env0 newCat'
+          (env2, newArgs) = List.mapAccumL (genFCatArg cnc_defs) env1 newArgs'
+
+          newLinRec = mkArray (map (mkArray . snd) linRec)
+          mkArray lst = listArray (0,length lst-1) lst
+
+          rule = FRule fun [] newArgs newCat newLinRec
+      in addFRule env2 rule
+
+----------------------------------------------------------------------
+-- term conversion
+
+type CnvMonad a = BacktrackM Env a
+
+type FPath     = [FIndex]
+data ProtoFCat = PFCat CId [FPath] [(FPath,FIndex)] Term
+type Env       = (ProtoFCat, [ProtoFCat])
+type LinRec    = [(FPath, [FSymbol])]
+data XRule     = XRule CId     {- function -}
+                       [CId]   {- argument types -}
+                       CId     {- result   type  -}
+                       [Term]  {- argument lin-types representation -}
+                       Term    {- result   lin-type  representation -}
+                       Term    {- body -}
+
+protoFCat :: TermMap -> CId -> Term -> ProtoFCat
+protoFCat cnc_defs cat ctype = PFCat cat (getRCS cnc_defs ctype) [] ctype
+
+type TermMap = Map.Map CId Term
+
+convertTerm :: TermMap -> FPath -> Term -> Term -> LinRec -> CnvMonad LinRec
+convertTerm cnc_defs sel ctype (V nr)       ((lbl_path,lin) : lins) = convertArg ctype nr (reverse sel) lbl_path lin lins
+convertTerm cnc_defs sel ctype (C nr)       ((lbl_path,lin) : lins) = convertCon ctype nr (reverse sel) lbl_path lin lins
+convertTerm cnc_defs sel ctype (R record)   ((lbl_path,lin) : lins) = convertRec cnc_defs sel ctype record lbl_path lin lins
+convertTerm cnc_defs sel ctype (P term p)                     lins  = do nr <- evalTerm cnc_defs [] p
+                                                                         convertTerm cnc_defs (nr:sel) ctype term lins
+convertTerm cnc_defs sel ctype (FV vars)                      lins  = do term <- member vars
+                                                                         convertTerm cnc_defs sel ctype term lins
+convertTerm cnc_defs sel ctype (S ts)       ((lbl_path,lin) : lins) = foldM (\lins t -> convertTerm cnc_defs sel ctype t lins) ((lbl_path,lin) : lins) (reverse ts)
+convertTerm cnc_defs sel ctype (K (KS str)) ((lbl_path,lin) : lins) = return ((lbl_path,FSymTok str : lin) : lins)
+convertTerm cnc_defs sel ctype (K (KP strs vars))((lbl_path,lin) : lins) = 
+  do toks <- member (strs:[strs' | Alt strs' _ <- vars])
+     return ((lbl_path, map FSymTok toks ++ lin) : lins)
+convertTerm cnc_defs sel ctype (F id)                         lins  = do term <- Map.lookup id cnc_defs
+                                                                         convertTerm cnc_defs sel ctype term lins
+convertTerm cnc_defs sel ctype (W s t)     ((lbl_path,lin) : lins) = do
+  ss <- case t of
+    R ss -> return ss
+    F f -> do
+      t <- Map.lookup f cnc_defs 
+      case t of
+        R ss -> return ss
+  convertRec cnc_defs sel ctype [K (KS (s ++ s1)) | K (KS s1) <- ss] lbl_path lin lins
+convertTerm cnc_defs sel ctype x lins  = error ("convertTerm ("++show x++")")
+
+
+convertArg (R record) nr path lbl_path lin lins =
+  foldM (\lins (lbl, ctype) -> convertArg ctype nr (lbl:path) (lbl:lbl_path) lin lins) lins (zip [0..] record)
+convertArg (C max) nr path lbl_path lin lins = do
+  index <- member [0..max]
+  restrictHead lbl_path index
+  restrictArg nr path index
+  return lins
+convertArg (S _) nr path lbl_path lin lins = do
+  (_, args) <- readState
+  let PFCat cat rcs tcs _ = args !! nr
+  return ((lbl_path, FSymCat (index path rcs 0) nr : lin) : lins)
+  where
+    index lbl' (lbl:lbls) idx
+      | lbl' == lbl = idx
+      | otherwise   = index lbl' lbls $! (idx+1)
+
+
+convertCon (C max) index [] lbl_path lin lins = do
+  guard (index <= max)
+  restrictHead lbl_path index
+  return lins
+convertCon x _ _ _ _ _ = error $ "SimpleToFCFG,convertCon: " ++ show x
+
+convertRec cnc_defs [] (R ctypes) record lbl_path lin lins =
+  foldM (\lins (index,ctype,val) -> convertTerm cnc_defs [] ctype val ((index:lbl_path,lin) : lins))
+        lins
+        (zip3 [0..] ctypes record)
+convertRec cnc_defs (index:sub_sel) ctype record lbl_path lin lins = do
+  convertTerm cnc_defs sub_sel ctype (record !! index) ((lbl_path,lin) : lins)
+
+
+------------------------------------------------------------
+-- eval a term to ground terms
+
+evalTerm :: TermMap -> FPath -> Term -> CnvMonad FIndex
+evalTerm cnc_defs path (V nr)       = do (_, args) <- readState
+		                         let PFCat _ _ _ ctype = args !! nr
+                                         unifyPType nr (reverse path) (selectTerm path ctype)
+evalTerm cnc_defs path (C nr)       = return nr
+evalTerm cnc_defs path (R record)   = case path of
+                                        (index:path) -> evalTerm cnc_defs path (record !! index)
+evalTerm cnc_defs path (P term sel) = do index <- evalTerm cnc_defs [] sel
+                                         evalTerm cnc_defs (index:path) term
+evalTerm cnc_defs path (FV terms)   = member terms >>= evalTerm cnc_defs path
+evalTerm cnc_defs path (F id)       = do term <- Map.lookup id cnc_defs
+                                         evalTerm cnc_defs path term
+evalTerm cnc_defs path x = error ("evalTerm ("++show x++")")
+
+unifyPType :: FIndex -> FPath -> Term -> CnvMonad FIndex
+unifyPType nr path (C max_index) =
+    do (_, args) <- readState
+       let PFCat _ _ tcs _ = args !! nr
+       case lookup path tcs of
+         Just index -> return index
+         Nothing    -> do index <- member [0..max_index]
+		          restrictArg nr path index
+		          return index
+unifyPType nr path t = error $ "unifyPType " ++ show t ---- AR 2/10/2007
+
+selectTerm :: FPath -> Term -> Term
+selectTerm []           term        = term
+selectTerm (index:path) (R  record) = selectTerm path (record !! index)
+
+
+----------------------------------------------------------------------
+-- FRulesEnv
+
+data FRulesEnv = FRulesEnv {-# UNPACK #-} !Int FCatSet [FRule]
+type FCatSet   = Map.Map CId (Map.Map [(FPath,FIndex)] FCat)
+
+emptyFRulesEnv = FRulesEnv 0 (ins fcatString (mkCId "String") [] $
+                              ins fcatInt    (mkCId "Int")    [] $
+                              ins fcatFloat  (mkCId "Float")  [] $
+                              ins fcatVar    (mkCId "_Var")   [] $
+                              Map.empty) []
+  where
+    ins fcat cat tcs fcatSet =
+      Map.insertWith (\_ -> Map.insert tcs fcat) cat tmap_s fcatSet
+      where
+        tmap_s = Map.singleton tcs fcat
+
+addFRule :: FRulesEnv -> FRule -> FRulesEnv
+addFRule (FRulesEnv last_id fcatSet rules) rule = FRulesEnv last_id fcatSet (rule:rules)
+
+getFGrammar :: FRulesEnv -> FGrammar
+getFGrammar (FRulesEnv last_id fcatSet rules) = (rules, Map.map Map.elems fcatSet)
+
+genFCatHead :: FRulesEnv -> ProtoFCat -> (FRulesEnv, FCat)
+genFCatHead env@(FRulesEnv last_id fcatSet rules) (PFCat cat rcs tcs _) =
+  case Map.lookup cat fcatSet >>= Map.lookup tcs of
+    Just fcat -> (env, fcat)
+    Nothing   -> let fcat = last_id+1
+                 in (FRulesEnv fcat (ins fcat) rules, fcat)
+  where
+    ins fcat = Map.insertWith (\_ -> Map.insert tcs fcat) cat tmap_s fcatSet
+      where
+        tmap_s = Map.singleton tcs fcat
+
+genFCatArg :: TermMap -> FRulesEnv -> ProtoFCat -> (FRulesEnv, FCat)
+genFCatArg cnc_defs env@(FRulesEnv last_id fcatSet rules) (PFCat cat rcs tcs ctype) =
+  case Map.lookup cat fcatSet of
+    Just tmap -> case Map.lookup tcs tmap of
+                   Just fcat -> (env, fcat)
+                   Nothing   -> ins tmap
+    Nothing   -> ins Map.empty
+  where
+    ins tmap =
+      let fcat = last_id+1
+          (last_id1,tmap1,rules1)
+                  = foldBM (\tcs st (last_id,tmap,rules) ->
+                                   let (last_id1,tmap1,fcat_arg) = addArg tcs last_id tmap
+                                       rule = FRule wildCId [[0]] [fcat_arg] fcat
+                                                    (listArray (0,length rcs-1) [listArray (0,0) [FSymCat lbl 0] | lbl <- [0..length rcs-1]])
+                                   in if st
+                                        then (last_id1,tmap1,rule:rules)
+                                        else (last_id, tmap,      rules))
+                           (fcat,Map.insert tcs fcat tmap,rules)
+                           (gen_tcs ctype [] [])
+                           False
+      in (FRulesEnv last_id1 (Map.insert cat tmap1 fcatSet) rules1, fcat)
+      where
+        addArg tcs last_id tmap =
+	  case Map.lookup tcs tmap of
+	    Just fcat -> (last_id, tmap, fcat)
+	    Nothing   -> let fcat = last_id+1
+                         in (fcat, Map.insert tcs fcat tmap, fcat)
+
+    gen_tcs :: Term -> FPath -> [(FPath,FIndex)] -> BacktrackM Bool [(FPath,FIndex)]
+    gen_tcs (R record)    path acc = foldM (\acc (label,ctype) -> gen_tcs ctype (label:path) acc) acc (zip [0..] record)
+    gen_tcs (S _)         path acc = return acc
+    gen_tcs (C max_index) path acc =
+      case List.lookup path tcs of
+        Just index -> return $! addConstraint path index acc
+        Nothing    -> do writeState True
+                         index <- member [0..max_index]
+                         return $! addConstraint path index acc
+      where
+        addConstraint path0 index0 (c@(path,index) : cs)
+	  | path0 > path = c:addConstraint path0 index0 cs
+        addConstraint path0 index0 cs  = (path0,index0) : cs
+    gen_tcs (F id)        path acc = case Map.lookup id cnc_defs of
+                                        Just term -> gen_tcs term path acc
+                                        Nothing   -> error ("unknown identifier: "++prCId id)
+
+
+getRCS :: TermMap -> Term -> [FPath]
+getRCS cnc_defs = loop [] []
+  where
+    loop path rcs (R record) = List.foldl' (\rcs (index,term) -> loop (index:path) rcs term) rcs (zip [0..] record)
+    loop path rcs (C i)      = rcs
+    loop path rcs (S _)      = path:rcs
+    loop path rcs (F id)     = case Map.lookup id cnc_defs of
+                                 Just term -> loop path rcs term
+                                 Nothing   -> error ("unknown identifier: "++show id)
+
+------------------------------------------------------------
+-- updating the MCF rule
+
+restrictArg :: FIndex -> FPath -> FIndex -> CnvMonad ()
+restrictArg nr path index = do
+  (head, args) <- readState 
+  args' <- updateNthM (restrictProtoFCat path index) nr args
+  writeState (head, args')
+
+restrictHead :: FPath -> FIndex -> CnvMonad ()
+restrictHead path term
+    = do (head, args) <- readState
+	 head' <- restrictProtoFCat path term head
+	 writeState (head', args)
+
+restrictProtoFCat :: FPath -> FIndex -> ProtoFCat -> CnvMonad ProtoFCat
+restrictProtoFCat path0 index0 (PFCat cat rcs tcs ctype) = do
+  tcs <- addConstraint tcs
+  return (PFCat cat rcs tcs ctype)
+  where
+    addConstraint (c@(path,index) : cs)
+        | path0 >  path = liftM (c:) (addConstraint cs)
+        | path0 == path = guard (index0 == index) >>
+                          return (c : cs)
+    addConstraint cs    = return ((path0,index0) : cs)
diff --git a/src/GF/Compile/GetGrammar.hs b/src/GF/Compile/GetGrammar.hs
new file mode 100644
index 000000000..a8eb8b749
--- /dev/null
+++ b/src/GF/Compile/GetGrammar.hs
@@ -0,0 +1,55 @@
+----------------------------------------------------------------------
+-- |
+-- Module      : GetGrammar
+-- Maintainer  : AR
+-- Stability   : (stable)
+-- Portability : (portable)
+--
+-- > CVS $Date: 2005/11/15 17:56:13 $ 
+-- > CVS $Author: aarne $
+-- > CVS $Revision: 1.16 $
+--
+-- this module builds the internal GF grammar that is sent to the type checker
+-----------------------------------------------------------------------------
+
+module GF.Compile.GetGrammar where
+
+import GF.Data.Operations
+import qualified GF.Source.ErrM as E
+
+import GF.Infra.UseIO
+import GF.Infra.Modules
+import GF.Grammar.Grammar
+import qualified GF.Source.AbsGF as A
+import GF.Source.SourceToGrammar
+---- import Macros
+---- import Rename
+import GF.Infra.Option
+--- import Custom
+import GF.Source.ParGF
+import qualified GF.Source.LexGF as L
+
+import GF.Compile.ReadFiles
+
+import Data.Char (toUpper)
+import Data.List (nub)
+import qualified Data.ByteString.Char8 as BS
+import Control.Monad (foldM)
+import System.Cmd (system)
+
+getSourceModule :: Options -> FilePath -> IOE SourceModule
+getSourceModule opts file0 = do
+  file <- foldM runPreprocessor file0 (moduleFlag optPreprocessors opts)
+  string    <- readFileIOE file
+  let tokens = myLexer string
+  mo1  <- ioeErr $ pModDef tokens
+  ioeErr $ transModDef mo1
+
+-- FIXME: should use System.IO.openTempFile
+runPreprocessor :: FilePath -> String -> IOE FilePath
+runPreprocessor file0 p =
+    do let tmp = "_gf_preproc.tmp"
+           cmd = p +++ file0 ++ ">" ++ tmp
+       ioeIO $ system cmd
+       -- ioeIO $ putStrLn $ "preproc" +++ cmd
+       return tmp
diff --git a/src/GF/Compile/GrammarToGFCC.hs b/src/GF/Compile/GrammarToGFCC.hs
new file mode 100644
index 000000000..d14a914f1
--- /dev/null
+++ b/src/GF/Compile/GrammarToGFCC.hs
@@ -0,0 +1,561 @@
+{-# LANGUAGE PatternGuards #-}
+module GF.Compile.GrammarToGFCC (prGrammar2gfcc,mkCanon2gfcc,addParsers) where
+
+import GF.Compile.Export
+import GF.Compile.OptimizeGF (unshareModule)
+import qualified GF.Compile.GenerateFCFG  as FCFG
+import qualified GF.Compile.GeneratePMCFG as PMCFG
+
+import PGF.CId
+import PGF.BuildParser (buildParserInfo)
+import qualified PGF.Macros as CM
+import qualified PGF.Data as C
+import qualified PGF.Data as D
+import GF.Grammar.Predef
+import GF.Grammar.PrGrammar
+import GF.Grammar.Grammar
+import qualified GF.Grammar.Lookup as Look
+import qualified GF.Grammar.Abstract as A
+import qualified GF.Grammar.Macros as GM
+import qualified GF.Compile.Compute as Compute ---- 
+import qualified GF.Infra.Modules as M
+import qualified GF.Infra.Option as O
+
+import GF.Infra.Ident
+import GF.Infra.Option
+import GF.Data.Operations
+import GF.Text.UTF8
+
+import Data.List
+import Data.Char (isDigit,isSpace)
+import qualified Data.Map as Map
+import qualified Data.ByteString.Char8 as BS
+import Debug.Trace ----
+
+-- when developing, swap commenting
+
+--traceD s t = trace s t 
+traceD s t = t 
+
+
+-- the main function: generate PGF from GF.
+
+prGrammar2gfcc :: Options -> String -> SourceGrammar -> (String,String)
+prGrammar2gfcc opts cnc gr = (abs,printPGF gc) where
+  (abs,gc) = mkCanon2gfcc opts cnc gr 
+
+mkCanon2gfcc :: Options -> String -> SourceGrammar -> (String,D.PGF)
+mkCanon2gfcc opts cnc gr = 
+  (prIdent abs, (canon2gfcc opts pars . reorder abs . canon2canon abs) gr)
+  where
+    abs = err error id $ M.abstractOfConcrete gr (identC (BS.pack cnc))
+    pars = mkParamLincat gr
+
+-- Adds parsers for all concretes
+addParsers :: D.PGF -> D.PGF
+addParsers pgf = pgf { D.concretes = Map.map conv (D.concretes pgf) }
+  where
+    conv cnc = cnc { D.parser = Just (buildParserInfo fcfg) }
+      where
+        fcfg
+          | Map.lookup (mkCId "erasing") (D.cflags cnc) == Just "on" = PMCFG.convertConcrete (D.abstract pgf) cnc
+          | otherwise                                                = FCFG.convertConcrete  (D.abstract pgf) cnc
+    
+
+-- Generate PGF from GFCM.
+-- this assumes a grammar translated by canon2canon
+
+canon2gfcc :: Options -> (Ident -> Ident -> C.Term) -> SourceGrammar -> D.PGF
+canon2gfcc opts pars cgr@(M.MGrammar ((a,M.ModMod abm):cms)) = 
+  (if dump opts DumpCanon then trace (prGrammar cgr) else id) $
+     D.PGF an cns gflags abs cncs 
+ where
+  -- abstract
+  an  = (i2i a)
+  cns = map (i2i . fst) cms
+  abs = D.Abstr aflags funs cats catfuns
+  gflags = Map.empty
+  aflags = Map.fromList [(mkCId f,x) | (f,x) <- moduleOptionsGFO (M.flags abm)]
+  mkDef pty = case pty of
+    Yes t -> mkExp t
+    _ -> CM.primNotion
+
+  -- concretes
+  lfuns = [(f', (mkType ty, mkDef pty)) | 
+             (f,AbsFun (Yes ty) pty) <- tree2list (M.jments abm), let f' = i2i f]
+  funs = Map.fromAscList lfuns
+  lcats = [(i2i c, mkContext cont) |
+                (c,AbsCat (Yes cont) _) <- tree2list (M.jments abm)]
+  cats = Map.fromAscList lcats
+  catfuns = Map.fromList 
+    [(cat,[f | (f, (C.DTyp _ c _,_)) <- lfuns, c==cat]) | (cat,_) <- lcats]
+
+  cncs  = Map.fromList [mkConcr lang (i2i lang) mo | (lang,M.ModMod mo) <- cms]
+  mkConcr lang0 lang mo = 
+      (lang,D.Concr flags lins opers lincats lindefs printnames params fcfg)
+    where
+      js = tree2list (M.jments mo)
+      flags   = Map.fromList [(mkCId f,x) | (f,x) <- moduleOptionsGFO (M.flags mo)]
+      opers   = Map.fromAscList [] -- opers will be created as optimization
+      utf     = if moduleFlag optEncoding (moduleOptions (M.flags mo)) == UTF_8
+                  then D.convertStringsInTerm decodeUTF8 else id
+      lins    = Map.fromAscList 
+        [(i2i f, utf (mkTerm tr))  | (f,CncFun _ (Yes tr) _) <- js]
+      lincats = Map.fromAscList 
+        [(i2i c, mkCType ty) | (c,CncCat (Yes ty) _ _) <- js]
+      lindefs = Map.fromAscList 
+        [(i2i c, mkTerm tr)  | (c,CncCat _ (Yes tr) _) <- js]
+      printnames = Map.union 
+        (Map.fromAscList [(i2i f, mkTerm tr) | (f,CncFun _ _ (Yes tr)) <- js])
+        (Map.fromAscList [(i2i f, mkTerm tr) | (f,CncCat _ _ (Yes tr)) <- js])
+      params = Map.fromAscList 
+        [(i2i c, pars lang0 c) | (c,CncCat (Yes ty) _ _) <- js]
+      fcfg = Nothing
+
+i2i :: Ident -> CId
+i2i = CId . ident2bs
+
+mkType :: A.Type -> C.Type
+mkType t = case GM.typeForm t of
+  Ok (hyps,(_,cat),args) -> C.DTyp (mkContext hyps) (i2i cat) (map mkExp args)
+
+mkExp :: A.Term -> C.Expr
+mkExp t = case t of
+  A.Eqs eqs -> C.EEq [C.Equ (map mkPatt ps) (mkExp e) | (ps,e) <- eqs]
+  _ -> case GM.termForm t of
+    Ok (xs,c,args) -> mkAbs xs (mkApp c (map mkExp args))
+  where
+    mkAbs xs t = foldr (C.EAbs . i2i) t xs
+    mkApp c args = case c of
+      Q _ c    -> foldl C.EApp (C.EVar (i2i c)) args
+      QC _ c   -> foldl C.EApp (C.EVar (i2i c)) args
+      Vr x     -> C.EVar (i2i x)
+      EInt i   -> C.ELit (C.LInt i)
+      EFloat f -> C.ELit (C.LFlt f)
+      K s      -> C.ELit (C.LStr s)
+      Meta (MetaSymb i) -> C.EMeta i
+      _        -> C.EMeta 0
+    mkPatt p = case p of
+      A.PP _ c ps -> foldl C.EApp (C.EVar (i2i c)) (map mkPatt ps)
+      A.PV x      -> C.EVar (i2i x)
+      A.PW        -> C.EVar wildCId
+      A.PInt i    -> C.ELit (C.LInt i)
+
+mkContext :: A.Context -> [C.Hypo]
+mkContext hyps = [C.Hyp (i2i x) (mkType ty) | (x,ty) <- hyps]
+
+mkTerm :: Term -> C.Term
+mkTerm tr = case tr of
+  Vr (IA _ i) -> C.V i
+  Vr (IAV _ _ i) -> C.V i
+  Vr (IC s) | isDigit (BS.last s) -> 
+    C.V ((read . BS.unpack . snd . BS.spanEnd isDigit) s)
+    ---- from gf parser of gfc
+  EInt i      -> C.C $ fromInteger i
+  R rs     -> C.R [mkTerm t | (_, (_,t)) <- rs]
+  P t l    -> C.P (mkTerm t) (C.C (mkLab l))
+  TSh _ _    -> error $ show tr
+  T _ cs   -> C.R [mkTerm t | (_,t) <- cs] ------
+  V _ cs   -> C.R [mkTerm t | t <- cs]
+  S t p    -> C.P (mkTerm t) (mkTerm p)
+  C s t    -> C.S $ concatMap flats [mkTerm x | x <- [s,t]]
+  FV ts    -> C.FV [mkTerm t | t <- ts]
+  K s      -> C.K (C.KS s)
+-----  K (KP ss _) -> C.K (C.KP ss []) ---- TODO: prefix variants
+  Empty    -> C.S []
+  App _ _  -> prtTrace tr $ C.C 66661          ---- for debugging
+  Abs _ t  -> mkTerm t ---- only on toplevel
+  Alts (td,tvs) -> 
+    C.K (C.KP (strings td) [C.Alt (strings u) (strings v) | (u,v) <- tvs])
+  _ -> prtTrace tr $ C.S [C.K (C.KS (A.prt tr +++ "66662"))] ---- for debugging
+ where
+   mkLab (LIdent l) = case BS.unpack l of
+     '_':ds -> (read ds) :: Int
+     _ -> prtTrace tr $ 66663
+   strings t = case t of
+     K s -> [s]
+     C u v -> strings u ++ strings v
+     Strs ss -> concatMap strings ss
+     _ -> prtTrace tr $ ["66660"]
+   flats t = case t of
+     C.S ts -> concatMap flats ts
+     _ -> [t]
+
+-- encoding PGF-internal lincats as terms
+mkCType :: Type -> C.Term
+mkCType t = case t of
+  EInt i      -> C.C $ fromInteger i
+  RecType rs  -> C.R [mkCType t | (_, t) <- rs]
+  Table pt vt -> case pt of
+    EInt i -> C.R $ replicate (1 + fromInteger i) $ mkCType vt
+    RecType rs -> mkCType $ foldr Table vt (map snd rs) 
+  Sort s | s == cStr -> C.S [] --- Str only
+  _ | Just i <- GM.isTypeInts t -> C.C $ fromInteger i
+  _ -> error  $ "mkCType " ++ show t
+
+-- encoding showable lincats (as in source gf) as terms
+mkParamLincat :: SourceGrammar -> Ident -> Ident -> C.Term
+mkParamLincat sgr lang cat = errVal (C.R [C.S []]) $ do 
+  typ <- Look.lookupLincat sgr lang cat
+  mkPType typ
+ where
+  mkPType typ = case typ of
+    RecType lts -> do
+      ts <- mapM (mkPType . snd) lts
+      return $ C.R [ C.P (kks $ prt_ l) t | ((l,_),t) <- zip lts ts]
+    Table (RecType lts) v -> do
+      ps <- mapM (mkPType . snd) lts
+      v' <- mkPType v
+      return $ foldr (\p v -> C.S [p,v]) v' ps
+    Table p v -> do
+      p' <- mkPType p
+      v' <- mkPType v
+      return $ C.S [p',v']
+    Sort s | s == cStr -> return $ C.S []
+    _ -> return $ 
+      C.FV $ map (kks . filter showable . prt_) $ 
+             errVal [] $ Look.allParamValues sgr typ
+  showable c = not (isSpace c) ---- || (c == ' ')  -- to eliminate \n in records
+  kks = C.K . C.KS
+
+-- return just one module per language
+
+reorder :: Ident -> SourceGrammar -> SourceGrammar
+reorder abs cg = M.MGrammar $ 
+    (abs, M.ModMod $ 
+          M.Module M.MTAbstract M.MSComplete aflags [] [] adefs poss):
+      [(c, M.ModMod $ 
+          M.Module (M.MTConcrete abs) M.MSComplete fs [] [] (sorted2tree js) poss) 
+            | (c,(fs,js)) <- cncs] 
+     where
+       poss = emptyBinTree -- positions no longer needed
+       mos = M.allModMod cg
+       adefs = sorted2tree $ sortIds $
+                 predefADefs ++ Look.allOrigInfos cg abs
+       predefADefs = 
+         [(c, AbsCat (Yes []) Nope) | c <- [cFloat,cInt,cString]]
+       aflags = 
+         concatModuleOptions [M.flags mo | (_,mo) <- M.allModMod cg, M.isModAbs mo]
+
+       cncs = sortIds [(lang, concr lang) | lang <- M.allConcretes cg abs]
+       concr la = (flags, 
+                   sortIds (predefCDefs ++ jments)) where 
+         jments = Look.allOrigInfos cg la
+         flags  = concatModuleOptions 
+                    [M.flags mo | 
+                     (i,mo) <- mos, M.isModCnc mo, 
+                     Just r <- [lookup i (M.allExtendSpecs cg la)]]
+
+         predefCDefs = 
+           [(c, CncCat (Yes GM.defLinType) Nope Nope) | c <- [cInt,cFloat,cString]]
+
+       sortIds = sortBy (\ (f,_) (g,_) -> compare f g) 
+
+
+-- one grammar per language - needed for symtab generation
+repartition :: Ident -> SourceGrammar -> [SourceGrammar]
+repartition abs cg = [M.partOfGrammar cg (lang,mo) | 
+  let mos = M.allModMod cg,
+  lang <- M.allConcretes cg abs,
+  let mo = errVal 
+       (error ("no module found for " ++ A.prt lang)) $ M.lookupModule cg lang
+  ]
+ 
+
+-- translate tables and records to arrays, parameters and labels to indices
+
+canon2canon :: Ident -> SourceGrammar -> SourceGrammar
+canon2canon abs = 
+   recollect . map cl2cl . repartition abs . purgeGrammar abs 
+ where
+  recollect = M.MGrammar . nubBy (\ (i,_) (j,_) -> i==j) . concatMap M.modules
+  cl2cl = M.MGrammar . js2js . map (c2c p2p) . M.modules
+    
+  js2js ms = map (c2c (j2j (M.MGrammar ms))) ms
+
+  c2c f2 (c,m) = case m of
+      M.ModMod mo ->
+        (c, M.ModMod $ M.replaceJudgements mo $ mapTree f2 (M.jments mo))
+      _ -> (c,m)    
+  j2j cg (f,j) = case j of
+      CncFun x (Yes tr) z -> (f,CncFun x (Yes ({-trace ("+ " ++ prt f)-} (t2t tr))) z)
+      CncCat (Yes ty) (Yes x) y -> (f,CncCat (Yes (ty2ty ty)) (Yes (t2t x)) y)
+      _ -> (f,j)
+   where
+      t2t = term2term cg pv
+      ty2ty = type2type cg pv
+      pv@(labels,untyps,typs) = trs $ paramValues cg
+
+    -- flatten record arguments of param constructors
+  p2p (f,j) = case j of
+      ResParam (Yes (ps,v)) -> 
+        (f,ResParam (Yes ([(c,concatMap unRec cont) | (c,cont) <- ps],Nothing)))
+      _ -> (f,j)
+  unRec (x,ty) = case ty of
+      RecType fs -> [ity | (_,typ) <- fs, ity <- unRec (identW,typ)] 
+      _ -> [(x,ty)]
+
+----
+  trs v = traceD (tr v) v
+
+  tr (labels,untyps,typs) =
+     ("LABELS:" ++++
+       unlines [A.prt c ++ "." ++ unwords (map A.prt l) +++ "=" +++ show i  | 
+       ((c,l),i) <- Map.toList labels]) ++++
+     ("UNTYPS:" ++++ unlines [A.prt t +++ "=" +++ show i | 
+       (t,i) <- Map.toList untyps]) ++++
+     ("TYPS:" ++++ unlines [A.prt t +++ "=" +++ show (Map.assocs i) | 
+       (t,i) <- Map.toList typs])
+----
+
+purgeGrammar :: Ident -> SourceGrammar -> SourceGrammar
+purgeGrammar abstr gr = 
+  (M.MGrammar . list . map unopt . filter complete . purge . M.modules) gr 
+ where
+  list ms = traceD ("MODULES" +++ unwords (map (prt . fst) ms)) ms
+  purge = nubBy (\x y -> fst x == fst y) . filter (flip elem needed . fst)
+  needed = nub $ concatMap (requiredCanModules isSingle gr) acncs
+  acncs = abstr : M.allConcretes gr abstr
+  isSingle = True
+  complete (i,M.ModMod m) = M.isCompleteModule m --- not . isIncompleteCanon
+  unopt = unshareModule gr -- subexp elim undone when compiled
+
+type ParamEnv =
+  (Map.Map (Ident,[Label]) (Type,Integer), -- numbered labels
+   Map.Map Term Integer,                   -- untyped terms to values
+   Map.Map Type (Map.Map Term Integer))    -- types to their terms to values
+
+--- gathers those param types that are actually used in lincats and lin terms
+paramValues :: SourceGrammar -> ParamEnv
+paramValues cgr = (labels,untyps,typs) where
+  partyps = nub $ 
+            --- [App (Q (IC "Predef") (IC "Ints")) (EInt i) | i <- [1,9]] ---linTypeInt 
+            [ty | 
+              (_,(_,CncCat (Yes ty0) _ _)) <- jments,
+              ty  <- typsFrom ty0
+            ] ++ [
+             Q m ty | 
+              (m,(ty,ResParam _)) <- jments
+            ] ++ [ty | 
+              (_,(_,CncFun _ (Yes tr) _)) <- jments,
+              ty  <- err (const []) snd $ appSTM (typsFromTrm tr) []
+            ]
+  params = [(ty, errVal (traceD ("UNKNOWN PARAM TYPE" +++ show ty) []) $ 
+                                         Look.allParamValues cgr ty) | ty <- partyps]
+  typsFrom ty = unlockTy ty : case ty of
+    Table p t  -> typsFrom p ++ typsFrom t
+    RecType ls -> concat [typsFrom t | (_, t) <- ls]
+    _ -> []
+ 
+  typsFromTrm :: Term -> STM [Type] Term
+  typsFromTrm tr = case tr of
+    R fs -> mapM_ (typsFromField . snd) fs >> return tr 
+      where
+        typsFromField (mty, t) = case mty of
+          Just x -> updateSTM (x:) >> typsFromTrm t
+          _ -> typsFromTrm t
+    V ty ts -> updateSTM (ty:) >> mapM_ typsFromTrm ts >> return tr
+    T (TTyped ty) cs -> 
+      updateSTM (ty:) >> mapM_ typsFromTrm [t | (_, t) <- cs] >> return tr
+    T (TComp ty) cs -> 
+      updateSTM (ty:) >> mapM_ typsFromTrm [t | (_, t) <- cs] >> return tr
+    _ -> GM.composOp typsFromTrm tr
+
+  jments = 
+    [(m,j) | (m,mo) <- M.allModMod cgr, j <- tree2list $ M.jments mo]
+  typs = 
+    Map.fromList [(ci,Map.fromList (zip vs [0..])) | (ci,vs) <- params]
+  untyps = 
+    Map.fromList $ concatMap Map.toList [typ | (_,typ) <- Map.toList typs]
+  lincats = 
+    [(cat,[f | let RecType fs = GM.defLinType, f <- fs]) | cat <- [cInt,cFloat, cString]] ++
+    reverse ---- TODO: really those lincats that are reached
+            ---- reverse is enough to expel overshadowed ones... 
+      [(cat,ls) | (_,(cat,CncCat (Yes ty) _ _)) <- jments, 
+                  RecType ls <- [unlockTy ty]]
+  labels = Map.fromList $ concat 
+    [((cat,[lab]),(typ,i)): 
+      [((cat,[LVar v]),(typ,toInteger (mx + v))) | v <- [0,1]] ++ ---- 1 or 2 vars 
+      [((cat,[lab,lab2]),(ty,j)) | 
+        rs <- getRec typ, ((lab2, ty),j) <- zip rs [0..]] 
+      | 
+        (cat,ls) <- lincats, ((lab, typ),i) <- zip ls [0..], let mx = length ls]
+    -- go to tables recursively
+    ---- TODO: even go to deeper records
+   where
+     getRec typ = case typ of
+       RecType rs -> [rs] ---- [unlockTyp rs]  -- (sort (unlockTyp ls))
+       Table _ t  -> getRec t
+       _ -> []
+
+type2type :: SourceGrammar -> ParamEnv -> Type -> Type
+type2type cgr env@(labels,untyps,typs) ty = case ty of
+  RecType rs ->
+    RecType [(mkLab i, t2t t) | (i,(l, t)) <- zip [0..] (unlockTyp rs)]
+  Table pt vt -> Table (t2t pt) (t2t vt)
+  QC _ _ -> look ty
+  _ -> ty
+ where
+   t2t = type2type cgr env
+   look ty = EInt $ (+ (-1)) $ toInteger $ case Map.lookup ty typs of
+     Just vs -> length $ Map.assocs vs
+     _ -> trace ("unknown partype " ++ show ty) 66669
+
+term2term :: SourceGrammar -> ParamEnv -> Term -> Term
+term2term cgr env@(labels,untyps,typs) tr = case tr of
+  App _ _ -> mkValCase (unrec tr)
+  QC  _ _ -> mkValCase tr 
+  R rs    -> R [(mkLab i, (Nothing, t2t t)) | 
+                 (i,(l,(_,t))) <- zip [0..] (GM.sortRec (unlock rs))]
+  P  t l   -> r2r tr
+  PI t l i -> EInt $ toInteger i
+
+  T (TWild _) _ -> error $ "wild" +++ prt tr
+  T (TComp  ty) cs  -> t2t $ V ty $ map snd cs ---- should be elim'ed in tc
+  T (TTyped ty) cs  -> t2t $ V ty $ map snd cs ---- should be elim'ed in tc
+  V ty ts  -> mkCurry $ V ty [t2t t | t <- ts]
+  S t p    -> mkCurrySel (t2t t) (t2t p)
+
+  _ -> GM.composSafeOp t2t tr
+ where
+   t2t = term2term cgr env
+
+   unrec t = case t of
+     App f (R fs) -> GM.mkApp (unrec f) [unrec u | (_,(_,u)) <- fs]
+     _ -> GM.composSafeOp unrec t
+
+   mkValCase tr = case appSTM (doVar tr) [] of
+     Ok (tr', st@(_:_)) -> t2t $ comp $ foldr mkCase tr' st
+     _ -> valNum $ comp tr
+
+   --- this is mainly needed for parameter record projections
+   ---- was: 
+   comp t = errVal t $ Compute.computeConcreteRec cgr t
+   compt t = case t of
+     T (TComp typ) ts  -> comp $ V typ (map (comp . snd) ts)  ---- should...
+     T (TTyped typ) ts -> comp $ V typ (map (comp . snd) ts)  ---- should
+     V typ ts -> V typ (map comp ts)
+     S tb (FV ts) -> FV $ map (comp . S tb) ts
+     S tb@(V typ ts) v0 -> err error id $ do
+       let v = comp v0 
+       let mv1 = Map.lookup v untyps
+       case mv1 of 
+         Just v1 -> return $ (comp . (ts !!) . fromInteger) v1 
+         _ -> return (S (comp tb) v) 
+                  
+     R r -> R [(l,(ty,comp t)) | (l,(ty,t)) <- r]
+     P (R r) l -> maybe t (comp . snd) $ lookup l r
+     _ -> GM.composSafeOp comp t
+
+   doVar :: Term -> STM [((Type,[Term]),(Term,Term))] Term
+   doVar tr = case getLab tr of
+     Ok (cat, lab) -> do
+       k <- readSTM >>= return . length
+       let tr' = Vr $ identC $ (BS.pack (show k)) -----
+
+       let tyvs = case Map.lookup (cat,lab) labels of
+             Just (ty,_) -> case Map.lookup ty typs of
+               Just vs -> (ty,[t | 
+                            (t,_) <- sortBy (\x y -> compare (snd x) (snd y)) 
+                                            (Map.assocs vs)])
+               _ -> error $ "doVar1" +++ A.prt ty
+             _ -> error $ "doVar2" +++ A.prt tr +++ show (cat,lab) ---- debug
+       updateSTM ((tyvs, (tr', tr)):) 
+       return tr'
+     _ -> GM.composOp doVar tr
+
+   r2r tr@(P (S (V ty ts) v) l) = t2t $ S (V ty [comp (P t l) | t <- ts]) v
+
+   r2r tr@(P p _) = case getLab tr of
+     Ok (cat,labs) -> P (t2t p) . mkLab $ 
+          maybe (prtTrace tr $ 66664) snd $ 
+            Map.lookup (cat,labs) labels
+     _ -> K ((A.prt tr +++ prtTrace tr "66665"))
+
+   -- this goes recursively into tables (ignored) and records (accumulated)
+   getLab tr = case tr of
+     Vr (IA cat _) -> return (identC cat,[])
+     Vr (IAV cat _ _) -> return (identC cat,[])
+     Vr (IC s) -> return (identC cat,[]) where
+       cat = BS.takeWhile (/='_') s ---- also to match IAVs; no _ in a cat tolerated
+             ---- init (reverse (dropWhile (/='_') (reverse s))) ---- from gf parser
+----     Vr _ -> error $ "getLab " ++ show tr
+     P p lab2 -> do
+       (cat,labs) <- getLab p
+       return (cat,labs++[lab2]) 
+     S p _ -> getLab p
+     _ -> Bad "getLab"
+
+
+   mkCase ((ty,vs),(x,p)) tr = 
+     S (V ty [mkBranch x v tr | v <- vs]) p
+   mkBranch x t tr = case tr of
+     _ | tr == x -> t
+     _ -> GM.composSafeOp (mkBranch x t) tr     
+
+   valNum tr = maybe (valNumFV $ tryFV tr) EInt $ Map.lookup tr untyps
+    where
+      tryFV tr = case GM.appForm tr of
+        (c@(QC _ _), ts) -> [GM.mkApp c ts' | ts' <- combinations (map tryFV ts)]
+        (FV ts,_) -> ts
+        _ -> [tr]
+      valNumFV ts = case ts of
+        [tr] -> error ("valNum" +++ prt tr) ----- prtTrace tr $ K "66667"
+        _ -> FV $ map valNum ts
+
+   mkCurry trm = case trm of
+     V (RecType [(_,ty)]) ts -> V ty ts 
+     V (RecType ((_,ty):ltys)) ts -> 
+       V ty [mkCurry (V (RecType ltys) cs) | 
+         cs <- chop (product (map (lengthtyp . snd) ltys)) ts] 
+     _ -> trm
+   lengthtyp ty = case Map.lookup ty typs of
+     Just m -> length (Map.assocs m)
+     _ -> error $ "length of type " ++ show ty
+   chop i xs = case splitAt i xs of 
+     (xs1,[])  -> [xs1]
+     (xs1,xs2) -> xs1:chop i xs2
+
+
+   mkCurrySel t p = S t p -- done properly in CheckGFCC
+
+
+mkLab k = LIdent (BS.pack ("_" ++ show k))
+
+-- remove lock fields; in fact, any empty records and record types
+unlock = filter notlock where
+  notlock (l,(_, t)) = case t of --- need not look at l
+     R [] -> False
+     RecType [] -> False
+     _ -> True
+
+unlockTyp = filter notlock
+  
+notlock (l, t) = case t of --- need not look at l
+     RecType [] -> False
+     _ -> True
+
+unlockTy ty = case ty of
+  RecType ls -> RecType $ GM.sortRec [(l, unlockTy t) | (l,t) <- ls, notlock (l,t)]
+  _ -> GM.composSafeOp unlockTy ty
+
+
+prtTrace tr n = 
+  trace ("-- INTERNAL COMPILER ERROR" +++ A.prt tr ++++ show n) n
+prTrace  tr n = trace ("-- OBSERVE" +++ A.prt tr +++ show n +++ show tr) n
+
+
+-- | this function finds out what modules are really needed in the canonical gr.
+-- its argument is typically a concrete module name
+requiredCanModules :: (Ord i, Show i) => Bool -> M.MGrammar i a -> i -> [i]
+requiredCanModules isSingle gr c = nub $ filter notReuse ops ++ exts where
+  exts = M.allExtends gr c
+  ops  = if isSingle 
+         then map fst (M.modules gr) 
+         else iterFix (concatMap more) $ exts
+  more i = errVal [] $ do
+    m <- M.lookupModMod gr i
+    return $ M.extends m ++ [o | o <- map M.openedModule (M.opens m)]
+  notReuse i = errVal True $ do
+    m <- M.lookupModMod gr i
+    return $ M.isModRes m -- to exclude reused Cnc and Abs from required
diff --git a/src/GF/Compile/ModDeps.hs b/src/GF/Compile/ModDeps.hs
new file mode 100644
index 000000000..b5b1b798c
--- /dev/null
+++ b/src/GF/Compile/ModDeps.hs
@@ -0,0 +1,153 @@
+----------------------------------------------------------------------
+-- |
+-- Module      : ModDeps
+-- Maintainer  : AR
+-- Stability   : (stable)
+-- Portability : (portable)
+--
+-- > CVS $Date: 2005/11/11 23:24:34 $ 
+-- > CVS $Author: aarne $
+-- > CVS $Revision: 1.14 $
+--
+-- Check correctness of module dependencies. Incomplete.
+--
+-- AR 13\/5\/2003
+-----------------------------------------------------------------------------
+
+module GF.Compile.ModDeps (mkSourceGrammar,
+		moduleDeps,
+		openInterfaces,
+		requiredCanModules
+	       ) where
+
+import GF.Grammar.Grammar
+import GF.Infra.Ident
+import GF.Infra.Option
+import GF.Grammar.PrGrammar
+import GF.Compile.Update
+import GF.Grammar.Lookup
+import GF.Infra.Modules
+
+import GF.Data.Operations
+
+import Control.Monad
+import Data.List
+
+-- | to check uniqueness of module names and import names, the
+-- appropriateness of import and extend types,
+-- to build a dependency graph of modules, and to sort them topologically
+mkSourceGrammar :: [(Ident,SourceModInfo)] -> Err SourceGrammar
+mkSourceGrammar ms = do
+  let ns = map fst ms
+  checkUniqueErr ns
+  mapM (checkUniqueImportNames ns . snd) ms
+  deps    <- moduleDeps ms
+  deplist <- either 
+               return 
+               (\ms -> Bad $ "circular modules" +++ unwords (map show ms)) $ 
+               topoTest deps
+  return $ MGrammar [(m, maybe undefined id $ lookup m ms)  | IdentM m _ <- deplist]
+
+checkUniqueErr ::  (Show i, Eq i) => [i] -> Err ()
+checkUniqueErr ms = do
+  let msg = checkUnique ms
+  if null msg then return () else Bad $ unlines msg
+
+-- | check that import names don't clash with module names
+checkUniqueImportNames :: [Ident] -> SourceModInfo -> Err ()
+checkUniqueImportNames ns mo = case mo of
+  ModMod m -> test [n | OQualif _ n v <- opens m, n /= v]
+  _ -> return () --- Bad $ "bug: ModDeps does not treat" +++ show mo
+ where
+
+  test ms = testErr (all (`notElem` ns) ms)
+                    ("import names clashing with module names among" +++ 
+                       unwords (map prt ms))
+
+type Dependencies = [(IdentM Ident,[IdentM Ident])]
+
+-- | to decide what modules immediately depend on what, and check if the
+-- dependencies are appropriate
+moduleDeps :: [(Ident,SourceModInfo)] -> Err Dependencies
+moduleDeps ms = mapM deps ms where
+  deps (c,mi) = errIn ("checking dependencies of module" +++ prt c) $ case mi of
+    ModMod m -> case mtype m of
+      MTConcrete a -> do
+        aty <- lookupModuleType gr a
+        testErr (aty == MTAbstract) "the of-module is not an abstract syntax" 
+        chDep (IdentM c (MTConcrete a)) 
+              (extends m) (MTConcrete a) (opens m) MTResource
+      t -> chDep (IdentM c t) (extends m) t (opens m) t
+
+  chDep it es ety os oty = do
+    ests <- mapM (lookupModuleType gr) es
+    testErr (all (compatMType ety) ests) "inappropriate extension module type" 
+----    osts <- mapM (lookupModuleType gr . openedModule) os
+----    testErr (all (compatOType oty) osts) "inappropriate open module type"
+    let ab = case it of
+               IdentM _ (MTConcrete a) -> [IdentM a MTAbstract]
+               _ -> [] ---- 
+    return (it, ab ++
+                [IdentM e ety | e <- es] ++ 
+                [IdentM (openedModule o) oty | o <- os])
+
+  -- check for superficial compatibility, not submodule relation etc: what can be extended
+  compatMType mt0 mt = case (mt0,mt) of
+    (MTResource,   MTConcrete _) -> True
+    (MTInstance _, MTConcrete _) -> True
+    (MTInterface,  MTAbstract)   -> True
+    (MTConcrete _, MTConcrete _) -> True
+    (MTInstance _, MTInstance _) -> True
+    (MTReuse _, MTReuse _) -> True
+    (MTInstance _, MTResource) -> True
+    (MTResource, MTInstance _) -> True
+    ---- some more?
+    _ -> mt0 == mt
+  -- in the same way; this defines what can be opened
+  compatOType mt0 mt = case mt0 of
+    MTAbstract     -> mt == MTAbstract
+    MTTransfer _ _ -> mt == MTAbstract
+    _ -> case mt of
+      MTResource -> True
+      MTReuse _ -> True
+      MTInterface -> True
+      MTInstance _ -> True
+      _ -> False      
+
+  gr = MGrammar ms --- hack
+
+openInterfaces :: Dependencies -> Ident -> Err [Ident]
+openInterfaces ds m = do
+  let deps = [(i,ds) | (IdentM i _,ds) <- ds]
+  let more (c,_) = [(i,mt) | Just is <- [lookup c deps], IdentM i mt <- is]
+  let mods = iterFix (concatMap more) (more (m,undefined))
+  return $ [i | (i,MTInterface) <- mods]
+
+-- | this function finds out what modules are really needed in the canonical gr.
+-- its argument is typically a concrete module name
+requiredCanModules :: (Ord i, Show i) => Bool -> MGrammar i a -> i -> [i]
+requiredCanModules isSingle gr c = nub $ filter notReuse ops ++ exts where
+  exts = allExtends gr c
+  ops  = if isSingle 
+         then map fst (modules gr) 
+         else iterFix (concatMap more) $ exts
+  more i = errVal [] $ do
+    m <- lookupModMod gr i
+    return $ extends m ++ [o | o <- map openedModule (opens m)]
+  notReuse i = errVal True $ do
+    m <- lookupModMod gr i
+    return $ isModRes m -- to exclude reused Cnc and Abs from required
+
+
+{-
+-- to test
+exampleDeps = [
+  (ir "Nat",[ii "Gen", ir "Adj"]),
+  (ir "Adj",[ii "Num", ii "Gen", ir "Nou"]),
+  (ir "Nou",[ii "Cas"])
+  ]
+
+ii s = IdentM (IC s) MTInterface
+ir s = IdentM (IC s) MTResource
+-}
+
diff --git a/src/GF/Compile/Optimize.hs b/src/GF/Compile/Optimize.hs
new file mode 100644
index 000000000..83cbeb57a
--- /dev/null
+++ b/src/GF/Compile/Optimize.hs
@@ -0,0 +1,235 @@
+{-# LANGUAGE PatternGuards #-}
+----------------------------------------------------------------------
+-- |
+-- Module      : Optimize
+-- Maintainer  : AR
+-- Stability   : (stable)
+-- Portability : (portable)
+--
+-- > CVS $Date: 2005/09/16 13:56:13 $ 
+-- > CVS $Author: aarne $
+-- > CVS $Revision: 1.18 $
+--
+-- Top-level partial evaluation for GF source modules.
+-----------------------------------------------------------------------------
+
+module GF.Compile.Optimize (optimizeModule) where
+
+import GF.Grammar.Grammar
+import GF.Infra.Ident
+import GF.Infra.Modules
+import GF.Grammar.PrGrammar
+import GF.Grammar.Macros
+import GF.Grammar.Lookup
+import GF.Grammar.Predef
+import GF.Compile.Refresh
+import GF.Compile.Compute
+import GF.Compile.BackOpt
+import GF.Compile.CheckGrammar
+import GF.Compile.Update
+
+import GF.Data.Operations
+import GF.Infra.CheckM
+import GF.Infra.Option
+
+import Control.Monad
+import Data.List
+import qualified Data.Set as Set
+
+import Debug.Trace
+
+
+-- conditional trace
+
+prtIf :: (Print a) => Bool -> a -> a
+prtIf b t = if b then trace (" " ++ prt t) t else t
+
+-- | partial evaluation of concrete syntax. AR 6\/2001 -- 16\/5\/2003 -- 5\/2\/2005.
+
+type EEnv = () --- not used
+
+-- only do this for resource: concrete is optimized in gfc form
+optimizeModule :: Options -> ([(Ident,SourceModInfo)],EEnv) -> 
+                  (Ident,SourceModInfo) -> Err ((Ident,SourceModInfo),EEnv)
+optimizeModule opts mse@(ms,eenv) mo@(_,mi) = case mi of
+  ModMod m0 | mstatus m0 == MSComplete && isModRes m0 -> do
+      (mo1,_) <- evalModule oopts mse mo
+      let mo2 = shareModule optim mo1
+      return (mo2,eenv)
+  _ -> evalModule oopts mse mo
+ where
+   oopts = addOptions opts (moduleOptions (flagsModule mo))
+   optim = moduleFlag optOptimizations oopts
+
+evalModule :: Options -> ([(Ident,SourceModInfo)],EEnv) -> (Ident,SourceModInfo) -> 
+               Err ((Ident,SourceModInfo),EEnv)
+evalModule oopts (ms,eenv) mo@(name,mod) = case mod of
+
+  ModMod m0 | mstatus m0 == MSComplete -> case mtype m0 of
+    _ | isModRes m0 -> do
+      let deps = allOperDependencies name (jments m0)
+      ids <- topoSortOpers deps
+      MGrammar (mod' : _) <- foldM evalOp gr ids
+      return $ (mod',eenv)
+
+    MTConcrete a -> do
+      js' <- mapMTree (evalCncInfo oopts gr name a) (jments m0)
+      return $ ((name, ModMod (replaceJudgements m0 js')),eenv)
+
+    _ -> return $ ((name,mod),eenv)
+  _ -> return $ ((name,mod),eenv)
+ where
+   gr0 = MGrammar $ ms
+   gr  = MGrammar $ (name,mod) : ms
+
+   evalOp g@(MGrammar ((_, ModMod m) : _)) i = do
+     info  <- lookupTree prt i $ jments m
+     info' <- evalResInfo oopts gr (i,info)
+     return $ updateRes g name i info'
+
+-- | only operations need be compiled in a resource, and this is local to each
+-- definition since the module is traversed in topological order
+evalResInfo :: Options -> SourceGrammar -> (Ident,Info) -> Err Info
+evalResInfo oopts gr (c,info) = case info of
+
+  ResOper pty pde -> eIn "operation" $ do
+    pde' <- case pde of
+       Yes de | optres -> liftM yes $ comp de 
+       _ -> return pde
+    return $ ResOper pty pde'
+
+  _ ->  return info
+ where
+   comp = if optres then computeConcrete gr else computeConcreteRec gr
+   eIn cat = errIn ("Error optimizing" +++ cat +++ prt c +++ ":")
+   optim = moduleFlag optOptimizations oopts
+   optres = OptExpand `Set.member` optim
+
+
+evalCncInfo :: 
+  Options -> SourceGrammar -> Ident -> Ident -> (Ident,Info) -> Err (Ident,Info)
+evalCncInfo opts gr cnc abs (c,info) = do
+
+ seq (prtIf (verbAtLeast opts Verbose) c) $ return ()
+
+ errIn ("optimizing" +++ prt c) $ case info of
+
+  CncCat ptyp pde ppr -> do
+    pde' <- case (ptyp,pde) of
+      (Yes typ, Yes de) -> 
+        liftM yes $ pEval ([(varStr, typeStr)], typ) de
+      (Yes typ, Nope)   -> 
+        liftM yes $ mkLinDefault gr typ >>= partEval noOptions gr ([(varStr, typeStr)],typ)
+      (May b, Nope) ->
+        return $ May b
+      _ -> return pde   -- indirection
+
+    ppr' <- liftM yes $ evalPrintname gr c ppr (yes $ K $ prt c)
+
+    return (c, CncCat ptyp pde' ppr')
+
+  CncFun (mt@(Just (_,ty@(cont,val)))) pde ppr -> --trace (prt c) $
+       eIn ("linearization in type" +++ prt (mkProd (cont,val,[])) ++++ "of function") $ do
+    pde' <- case pde of
+      Yes de -> do
+        liftM yes $ pEval ty de
+
+      _ -> return pde
+    ppr' <-  liftM yes $ evalPrintname gr c ppr pde'
+    return $ (c, CncFun mt pde' ppr') -- only cat in type actually needed
+
+  _ ->  return (c,info)
+ where
+   pEval = partEval opts gr
+   eIn cat = errIn ("Error optimizing" +++ cat +++ prt c +++ ":")
+
+-- | the main function for compiling linearizations
+partEval :: Options -> SourceGrammar -> (Context,Type) -> Term -> Err Term
+partEval opts gr (context, val) trm = errIn ("parteval" +++ prt_ trm) $ do
+  let vars  = map fst context
+      args  = map Vr vars
+      subst = [(v, Vr v) | v <- vars]
+      trm1 = mkApp trm args
+  trm2 <- computeTerm gr subst trm1
+  trm3 <- if rightType trm2
+            then computeTerm gr subst trm2
+            else recordExpand val trm2 >>= computeTerm gr subst
+  return $ mkAbs vars trm3
+  where
+    -- don't eta expand records of right length (correct by type checking)
+    rightType (R rs) = case val of
+                         RecType ts -> length rs == length ts
+                         _          -> False
+    rightType _      = False
+
+
+
+
+-- here we must be careful not to reduce
+--   variants {{s = "Auto" ; g = N} ; {s = "Wagen" ; g = M}}
+--   {s  = variants {"Auto" ; "Wagen"} ; g  = variants {N ; M}} ;
+
+recordExpand :: Type -> Term -> Err Term
+recordExpand typ trm = case unComputed typ of
+  RecType tys -> case trm of
+    FV rs -> return $ FV [R [assign lab (P r lab) | (lab,_) <- tys] | r <- rs]
+    _ -> return $ R [assign lab (P trm lab) | (lab,_) <- tys]
+  _ -> return trm
+
+
+-- | auxiliaries for compiling the resource
+
+mkLinDefault :: SourceGrammar -> Type -> Err Term
+mkLinDefault gr typ = do
+  case unComputed typ of
+    RecType lts -> mapPairsM mkDefField lts >>= (return . Abs varStr . R . mkAssign)
+    _ -> liftM (Abs varStr) $ mkDefField typ
+----    _ -> prtBad "linearization type must be a record type, not" typ
+ where
+   mkDefField typ = case unComputed typ of
+     Table p t  -> do
+       t' <- mkDefField t
+       let T _ cs = mkWildCases t'
+       return $ T (TWild p) cs 
+     Sort s | s == cStr -> return $ Vr varStr
+     QC q p             -> lookupFirstTag gr q p
+     RecType r  -> do
+       let (ls,ts) = unzip r
+       ts' <- mapM mkDefField ts
+       return $ R $ [assign l t | (l,t) <- zip ls ts']
+     _ | Just _ <- isTypeInts typ -> return $ EInt 0 -- exists in all as first val
+     _ -> prtBad "linearization type field cannot be" typ
+
+-- | Form the printname: if given, compute. If not, use the computed
+-- lin for functions, cat name for cats (dispatch made in evalCncDef above).
+--- We cannot use linearization at this stage, since we do not know the
+--- defaults we would need for question marks - and we're not yet in canon.
+evalPrintname :: SourceGrammar -> Ident -> MPr -> Perh Term -> Err Term
+evalPrintname gr c ppr lin =
+  case ppr of
+    Yes pr -> comp pr
+    _ -> case lin of
+      Yes t -> return $ K $ clean $ prt $ oneBranch t ---- stringFromTerm
+      _ -> return $ K $ prt c ----
+ where
+   comp = computeConcrete gr
+
+   oneBranch t = case t of
+     Abs _ b   -> oneBranch b
+     R   (r:_) -> oneBranch $ snd $ snd r
+     T _ (c:_) -> oneBranch $ snd c
+     V _ (c:_) -> oneBranch c
+     FV  (t:_) -> oneBranch t
+     C x y     -> C (oneBranch x) (oneBranch y)
+     S x _     -> oneBranch x
+     P x _     -> oneBranch x
+     Alts (d,_) -> oneBranch d
+     _ -> t
+
+  --- very unclean cleaner
+   clean s = case s of
+     '+':'+':' ':cs -> clean cs
+     '"':cs -> clean cs
+     c:cs -> c: clean cs
+     _ -> s
+
diff --git a/src/GF/Compile/OptimizeGF.hs b/src/GF/Compile/OptimizeGF.hs
new file mode 100644
index 000000000..41b828aa3
--- /dev/null
+++ b/src/GF/Compile/OptimizeGF.hs
@@ -0,0 +1,277 @@
+----------------------------------------------------------------------
+-- |
+-- Module      : OptimizeGF
+-- Maintainer  : AR
+-- Stability   : (stable)
+-- Portability : (portable)
+--
+-- > CVS $Date: 2005/04/21 16:21:33 $ 
+-- > CVS $Author: bringert $
+-- > CVS $Revision: 1.6 $
+--
+-- Optimizations on GF source code: sharing, parametrization, value sets.
+--
+-- optimization: sharing branches in tables. AR 25\/4\/2003.
+-- following advice of Josef Svenningsson
+-----------------------------------------------------------------------------
+
+module GF.Compile.OptimizeGF (
+  optModule,unshareModule,unsubexpModule,unoptModule,subexpModule,shareModule
+  ) where 
+
+import GF.Grammar.Grammar
+import GF.Grammar.Lookup
+import GF.Infra.Ident
+import qualified GF.Grammar.Macros as C
+import GF.Grammar.PrGrammar (prt)
+import qualified GF.Infra.Modules as M
+import GF.Data.Operations
+
+import Control.Monad
+import Data.Map (Map)
+import qualified Data.Map as Map
+import qualified Data.ByteString.Char8 as BS
+import Data.List
+
+optModule :: (Ident, SourceModInfo) -> (Ident, SourceModInfo)
+optModule = subexpModule . shareModule
+
+shareModule = processModule optim
+
+unoptModule :: SourceGrammar -> (Ident, SourceModInfo) -> (Ident, SourceModInfo)
+unoptModule gr = unshareModule gr . unsubexpModule
+
+unshareModule :: SourceGrammar -> (Ident, SourceModInfo) -> (Ident, SourceModInfo)
+unshareModule gr = processModule (const (unoptim gr))
+
+processModule :: 
+  (Ident -> Term -> Term) -> (Ident, SourceModInfo) -> (Ident, SourceModInfo)
+processModule opt (i,m) = case m of
+  M.ModMod mo -> 
+    (i,M.ModMod (M.replaceJudgements mo (mapTree (shareInfo opt) (M.jments mo))))
+  _ -> (i,m)
+
+shareInfo opt (c, CncCat ty (Yes t) m) = (c,CncCat ty (Yes (opt c t)) m)
+shareInfo opt (c, CncFun kxs (Yes t) m) = (c,CncFun kxs (Yes (opt c t)) m)
+shareInfo opt (c, ResOper ty (Yes t)) = (c,ResOper ty (Yes (opt c t)))
+shareInfo _ i = i
+
+-- the function putting together optimizations
+optim :: Ident -> Term -> Term
+optim c = values . factor c 0
+
+-- we need no counter to create new variable names, since variables are 
+-- local to tables (only true in GFC) ---
+
+-- factor parametric branches
+
+factor :: Ident -> Int -> Term -> Term
+factor c i t = case t of
+  T _ [_] -> t
+  T _ []  -> t
+  T (TComp ty) cs -> 
+    T (TTyped ty) $ factors i [(p, factor c (i+1) v) | (p, v) <- cs]
+  _ -> C.composSafeOp (factor c i) t
+ where
+
+   factors i psvs =   -- we know psvs has at least 2 elements
+     let p   = qqIdent c i
+         vs' = map (mkFun p) psvs
+     in if   allEqs vs'
+        then mkCase p vs' 
+        else psvs
+
+   mkFun p (patt, val) = replace (C.patt2term patt) (Vr p) val
+
+   allEqs (v:vs) = all (==v) vs
+
+   mkCase p (v:_) = [(PV p, v)]
+
+--- we hope this will be fresh and don't check... in GFC would be safe
+
+qqIdent c i = identC (BS.pack ("q_" ++ prt c ++ "__" ++ show i))
+
+
+--  we need to replace subterms
+
+replace :: Term -> Term -> Term -> Term
+replace old new trm = case trm of
+  
+  -- these are the important cases, since they can correspond to patterns  
+  QC _ _   | trm == old -> new
+  App t ts | trm == old -> new
+  App t ts              -> App (repl t) (repl ts)
+  R _ | isRec && trm == old -> new
+  _ -> C.composSafeOp repl trm
+ where
+   repl = replace old new
+   isRec = case trm of
+     R _ -> True
+     _ -> False
+
+-- It is very important that this is performed only after case
+-- expansion since otherwise the order and number of values can
+-- be incorrect. Guaranteed by the TComp flag.
+
+values :: Term -> Term
+values t = case t of
+  T ty [(ps,t)]    -> T ty [(ps,values t)] -- don't destroy parametrization
+  T (TComp ty)  cs -> V ty [values t | (_, t) <- cs]
+  T (TTyped ty) cs -> V ty [values t | (_, t) <- cs] 
+        ---- why are these left?
+        ---- printing with GrammarToSource does not preserve the distinction
+  _ -> C.composSafeOp values t
+
+
+-- to undo the effect of factorization
+
+unoptim :: SourceGrammar -> Term -> Term
+unoptim gr = unfactor gr
+
+unfactor :: SourceGrammar -> Term -> Term
+unfactor gr t = case t of
+  T (TTyped ty) [(PV x,u)] -> V ty [restore x v (unfac u) | v <- vals ty]
+  _ -> C.composSafeOp unfac t
+ where
+   unfac = unfactor gr
+   vals  = err error id . allParamValues gr
+   restore x u t = case t of
+     Vr y | y == x -> u
+     _ -> C.composSafeOp (restore x u) t
+
+
+----------------------------------------------------------------------
+
+{-
+This module implements a simple common subexpression elimination
+ for gfc grammars, to factor out shared subterms in lin rules.
+It works in three phases: 
+
+  (1) collectSubterms collects recursively all subterms of forms table and (P x..y)
+      from lin definitions (experience shows that only these forms
+      tend to get shared) and counts how many times they occur
+  (2) addSubexpConsts takes those subterms t that occur more than once
+      and creates definitions of form "oper A''n = t" where n is a
+      fresh number; notice that we assume no ids of this form are in
+      scope otherwise
+  (3) elimSubtermsMod goes through lins and the created opers by replacing largest
+      possible subterms by the newly created identifiers
+
+The optimization is invoked in gf by the flag i -subs.
+
+If an application does not support GFC opers, the effect of this
+optimization can be undone by the function unSubelimCanon.
+
+The function unSubelimCanon can be used to diagnostisize how much
+cse is possible in the grammar. It is used by the flag pg -printer=subs.
+
+-}
+
+subexpModule :: SourceModule -> SourceModule
+subexpModule (n,m) = errVal (n,m) $ case m of
+  M.ModMod mo -> do
+    let ljs = tree2list (M.jments mo)
+    (tree,_) <- appSTM (getSubtermsMod n ljs) (Map.empty,0)
+    js2 <- liftM buildTree $ addSubexpConsts n tree $ ljs
+    return (n,M.ModMod (M.replaceJudgements mo js2))
+  _ -> return (n,m)
+
+unsubexpModule :: SourceModule -> SourceModule
+unsubexpModule sm@(i,m) = case m of
+    M.ModMod mo | hasSub ljs ->
+      (i, M.ModMod (M.replaceJudgements mo
+                     (rebuild (map unparInfo ljs)))) 
+                        where ljs = tree2list (M.jments mo)
+    _ -> (i,m)
+  where
+    -- perform this iff the module has opers
+    hasSub ljs = not $ null [c | (c,ResOper _ _) <- ljs]
+    unparInfo (c,info) = case info of
+      CncFun xs (Yes t) m -> [(c, CncFun xs (Yes (unparTerm t)) m)]
+      ResOper (Yes (EInt 8)) _ -> [] -- subexp-generated opers
+      ResOper pty (Yes t) -> [(c, ResOper pty (Yes (unparTerm t)))]
+      _ -> [(c,info)]
+    unparTerm t = case t of
+      Q m c | isOperIdent c -> --- name convention of subexp opers
+        errVal t $ liftM unparTerm $ lookupResDef gr m c 
+      _ -> C.composSafeOp unparTerm t
+    gr = M.MGrammar [sm] 
+    rebuild = buildTree . concat
+
+-- implementation
+
+type TermList = Map Term (Int,Int) -- number of occs, id
+type TermM a = STM (TermList,Int) a
+
+addSubexpConsts :: 
+  Ident -> Map Term (Int,Int) -> [(Ident,Info)] -> Err [(Ident,Info)]
+addSubexpConsts mo tree lins = do
+  let opers = [oper id trm | (trm,(_,id)) <- list]
+  mapM mkOne $ opers ++ lins
+ where
+
+   mkOne (f,def) = case def of
+     CncFun xs (Yes trm) pn -> do
+       trm' <- recomp f trm
+       return (f,CncFun xs (Yes trm') pn)
+     ResOper ty (Yes trm) -> do
+       trm' <- recomp f trm
+       return (f,ResOper ty (Yes trm'))
+     _ -> return (f,def)
+   recomp f t = case Map.lookup t tree of
+     Just (_,id) | operIdent id /= f -> return $ Q mo (operIdent id)
+     _ -> C.composOp (recomp f) t
+
+   list = Map.toList tree
+
+   oper id trm = (operIdent id, ResOper (Yes (EInt 8)) (Yes trm)) 
+   --- impossible type encoding generated opers
+
+getSubtermsMod :: Ident -> [(Ident,Info)] -> TermM (Map Term (Int,Int))
+getSubtermsMod mo js = do
+  mapM (getInfo (collectSubterms mo)) js
+  (tree0,_) <- readSTM
+  return $ Map.filter (\ (nu,_) -> nu > 1) tree0
+ where
+   getInfo get fi@(f,i) = case i of
+     CncFun xs (Yes trm) pn -> do
+       get trm
+       return $ fi
+     ResOper ty (Yes trm) -> do
+       get trm
+       return $ fi
+     _ -> return fi
+
+collectSubterms :: Ident -> Term -> TermM Term
+collectSubterms mo t = case t of
+  App f a -> do
+    collect f
+    collect a
+    add t 
+  T ty cs -> do
+    let (_,ts) = unzip cs
+    mapM collect ts
+    add t
+  V ty ts -> do
+    mapM collect ts
+    add t
+----  K (KP _ _)  -> add t
+  _ -> C.composOp (collectSubterms mo) t
+ where
+   collect = collectSubterms mo
+   add t = do
+     (ts,i) <- readSTM
+     let 
+       ((count,id),next) = case Map.lookup t ts of
+         Just (nu,id) -> ((nu+1,id), i)
+         _ ->            ((1,   i ), i+1)
+     writeSTM (Map.insert t (count,id) ts, next)
+     return t --- only because of composOp
+
+operIdent :: Int -> Ident
+operIdent i = identC (operPrefix `BS.append` (BS.pack (show i))) ---
+
+isOperIdent :: Ident -> Bool
+isOperIdent id = BS.isPrefixOf operPrefix (ident2bs id)
+
+operPrefix = BS.pack ("A''")
diff --git a/src/GF/Compile/OptimizeGFCC.hs b/src/GF/Compile/OptimizeGFCC.hs
new file mode 100644
index 000000000..c73d5bbcb
--- /dev/null
+++ b/src/GF/Compile/OptimizeGFCC.hs
@@ -0,0 +1,124 @@
+module GF.Compile.OptimizeGFCC where
+
+import PGF.CId
+import PGF.Data
+
+import GF.Data.Operations
+
+import Data.List
+import qualified Data.Map as Map
+
+
+-- back-end optimization: 
+-- suffix analysis followed by common subexpression elimination
+
+optPGF :: PGF -> PGF
+optPGF = cseOptimize . suffixOptimize
+
+suffixOptimize :: PGF -> PGF
+suffixOptimize pgf = pgf {
+  concretes = Map.map opt (concretes pgf)
+  }
+ where 
+  opt cnc = cnc {
+    lins = Map.map optTerm (lins cnc),
+    lindefs = Map.map optTerm (lindefs cnc),
+    printnames = Map.map optTerm (printnames cnc)
+  }
+
+cseOptimize :: PGF -> PGF
+cseOptimize pgf = pgf {
+  concretes = Map.map subex (concretes pgf)
+  }
+
+-- analyse word form lists into prefix + suffixes
+-- suffix sets can later be shared by subex elim
+
+optTerm :: Term -> Term  
+optTerm tr = case tr of
+    R ts@(_:_:_) | all isK ts -> mkSuff $ optToks [s | K (KS s) <- ts]
+    R ts  -> R $ map optTerm ts
+    P t v -> P (optTerm t) v
+    _ -> tr
+ where
+  optToks ss = prf : suffs where
+    prf = pref (head ss) (tail ss)
+    suffs = map (drop (length prf)) ss
+    pref cand ss = case ss of
+      s1:ss2 -> if isPrefixOf cand s1 then pref cand ss2 else pref (init cand) ss
+      _ -> cand
+  isK t = case t of
+    K (KS _) -> True
+    _ -> False
+  mkSuff ("":ws) = R (map (K . KS) ws)
+  mkSuff (p:ws) = W p (R (map (K . KS) ws))
+
+
+-- common subexpression elimination
+
+---subex :: [(CId,Term)] -> [(CId,Term)]
+subex :: Concr -> Concr
+subex cnc = err error id $ do
+  (tree,_) <- appSTM (getSubtermsMod cnc) (Map.empty,0)
+  return $ addSubexpConsts tree cnc
+
+type TermList = Map.Map Term (Int,Int) -- number of occs, id
+type TermM a = STM (TermList,Int) a
+
+addSubexpConsts :: TermList -> Concr -> Concr
+addSubexpConsts tree cnc = cnc {
+  opers = Map.fromList [(f,recomp f trm) | (f,trm) <- ops],
+  lins  = rec lins,
+  lindefs = rec lindefs,
+  printnames = rec printnames
+  }
+ where
+   ops = [(fid id, trm) | (trm,(_,id)) <- Map.assocs tree]
+   mkOne (f,trm) = (f, recomp f trm)
+   recomp f t = case Map.lookup t tree of
+     Just (_,id) | fid id /= f -> F $ fid id -- not to replace oper itself
+     _ -> case t of
+       R ts   -> R $ map (recomp f) ts
+       S ts   -> S $ map (recomp f) ts
+       W s t  -> W s (recomp f t)
+       P t p  -> P (recomp f t) (recomp f p)
+       _ -> t
+   fid n = mkCId $ "_" ++ show n
+   rec field = Map.fromAscList [(f,recomp f trm) | (f,trm) <- Map.assocs (field cnc)]
+
+
+getSubtermsMod :: Concr -> TermM TermList
+getSubtermsMod cnc = do
+  mapM getSubterms (Map.assocs (lins cnc))
+  mapM getSubterms (Map.assocs (lindefs cnc))
+  mapM getSubterms (Map.assocs (printnames cnc))
+  (tree0,_) <- readSTM
+  return $ Map.filter (\ (nu,_) -> nu > 1) tree0
+ where
+   getSubterms (f,trm) = collectSubterms trm >> return ()
+
+collectSubterms :: Term -> TermM ()
+collectSubterms t = case t of
+  R ts -> do
+    mapM collectSubterms ts
+    add t
+  S ts -> do
+    mapM collectSubterms ts
+    add t
+  W s u -> do
+    collectSubterms u
+    add t
+  P p u -> do
+    collectSubterms p
+    collectSubterms u
+    add t
+  _ -> return ()
+ where
+   add t = do
+     (ts,i) <- readSTM
+     let 
+       ((count,id),next) = case Map.lookup t ts of
+         Just (nu,id) -> ((nu+1,id), i)
+         _ ->            ((1,   i ), i+1)
+     writeSTM (Map.insert t (count,id) ts, next)
+
diff --git a/src/GF/Compile/ReadFiles.hs b/src/GF/Compile/ReadFiles.hs
new file mode 100644
index 000000000..cd2faec15
--- /dev/null
+++ b/src/GF/Compile/ReadFiles.hs
@@ -0,0 +1,195 @@
+----------------------------------------------------------------------
+-- |
+-- Module      : ReadFiles
+-- Maintainer  : AR
+-- Stability   : (stable)
+-- Portability : (portable)
+--
+-- > CVS $Date: 2005/11/11 23:24:34 $ 
+-- > CVS $Author: aarne $
+-- > CVS $Revision: 1.26 $
+--
+-- Decide what files to read as function of dependencies and time stamps.
+--
+-- make analysis for GF grammar modules. AR 11\/6\/2003--24\/2\/2004
+--
+-- to find all files that have to be read, put them in dependency order, and
+-- decide which files need recompilation. Name @file.gf@ is returned for them,
+-- and @file.gfo@ otherwise.
+-----------------------------------------------------------------------------
+
+module GF.Compile.ReadFiles 
+           ( getAllFiles,ModName,ModEnv,importsOfModule,
+             gfoFile,gfFile,isGFO,
+             getOptionsFromFile) where
+
+import GF.Infra.UseIO
+import GF.Infra.Option
+import GF.Data.Operations
+import GF.Source.AbsGF hiding (FileName)
+import GF.Source.LexGF
+import GF.Source.ParGF
+
+import Control.Monad
+import Data.Char
+import Data.List
+import qualified Data.ByteString.Char8 as BS
+import qualified Data.Map as Map
+import System.Time
+import System.Directory
+import System.FilePath
+
+type ModName = String
+type ModEnv  = Map.Map ModName (ClockTime,[ModName])
+
+
+-- | Returns a list of all files to be compiled in topological order i.e.
+-- the low level (leaf) modules are first.
+getAllFiles :: Options -> [InitPath] -> ModEnv -> FileName -> IOE [FullPath]
+getAllFiles opts ps env file = do
+  -- read module headers from all files recursively
+  ds <- liftM reverse $ get [] [] (justModuleName file)
+  ioeIO $ putIfVerb opts $ "all modules:" +++ show [name | (name,_,_,_,_) <- ds]
+  return $ paths ds
+  where
+    -- construct list of paths to read
+    paths cs = [mk (p </> f) | (f,st,_,_,p) <- cs, mk <- mkFile st]
+      where
+        mkFile CSComp = [gfFile ]
+        mkFile CSRead = [gfoFile]
+        mkFile _      = []
+
+    -- | traverses the dependency graph and returns a topologicaly sorted
+    -- list of ModuleInfo. An error is raised if there is circular dependency
+    get :: [ModName]          -- ^ keeps the current path in the dependency graph to avoid cycles
+        -> [ModuleInfo]       -- ^ a list of already traversed modules
+        -> ModName            -- ^ the current module
+        -> IOE [ModuleInfo]   -- ^ the final 
+    get trc ds name
+      | name `elem` trc = ioeErr $ Bad $ "circular modules" +++ unwords trc
+      | (not . null) [n | (n,_,_,_,_) <- ds, name == n]     --- file already read
+                        = return ds
+      | otherwise       = do
+           (name,st0,t0,imps,p) <- findModule name
+           ds <- foldM (get (name:trc)) ds imps
+           let (st,t) | (not . null) [f | (f,CSComp,_,_,_) <- ds, elem f imps]
+                                  = (CSComp,Nothing)
+                      | otherwise = (st0,t0)
+           return ((name,st,t,imps,p):ds)
+
+    -- searches for module in the search path and if it is found
+    -- returns 'ModuleInfo'. It fails if there is no such module
+    findModule :: ModName -> IOE ModuleInfo
+    findModule name = do
+      (file,gfTime,gfoTime) <- do
+          mb_gfFile <- ioeIO $ getFilePathMsg "" ps (gfFile name)
+          case mb_gfFile of
+            Just gfFile -> do gfTime  <- ioeIO $ getModificationTime gfFile
+                              mb_gfoTime <- ioeIO $ catch (liftM Just $ getModificationTime (replaceExtension gfFile "gfo"))
+                                                        (\_->return Nothing)
+                              return (gfFile, Just gfTime, mb_gfoTime)
+            Nothing     -> do mb_gfoFile <- ioeIO $ getFilePathMsg "" ps (gfoFile name)
+                              case mb_gfoFile of
+                                Just gfoFile -> do gfoTime <- ioeIO $ getModificationTime gfoFile
+                                                   return (gfoFile, Nothing, Just gfoTime)
+                                Nothing      -> ioeErr $ Bad ("File " ++ gfFile name ++ " does not exist.")
+
+
+      let mb_envmod = Map.lookup name env
+          (st,t) = selectFormat opts (fmap fst mb_envmod) gfTime gfoTime
+
+      imps <- if st == CSEnv
+                then return (maybe [] snd mb_envmod)
+                else do s <- ioeIO $ BS.readFile file
+                        (mname,imps) <- ioeErr ((liftM importsOfModule . pModHeader . myLexer) s)
+                        ioeErr $ testErr  (mname == name)
+                                          ("module name" +++ mname +++ "differs from file name" +++ name)
+                        return imps
+
+      return (name,st,t,imps,dropFileName file)
+
+
+isGFO :: FilePath -> Bool
+isGFO = (== ".gfo") . takeExtensions
+
+gfoFile :: FilePath -> FilePath
+gfoFile f = addExtension f "gfo"
+
+gfFile :: FilePath -> FilePath
+gfFile f = addExtension f "gf"
+
+
+-- From the given Options and the time stamps computes
+-- whether the module have to be computed, read from .gfo or
+-- the environment version have to be used
+selectFormat :: Options -> Maybe ClockTime -> Maybe ClockTime -> Maybe ClockTime -> (CompStatus,Maybe ClockTime)
+selectFormat opts mtenv mtgf mtgfo =
+  case (mtenv,mtgfo,mtgf) of
+    (_,_,Just tgf)         | fromSrc  -> (CSComp,Nothing)
+    (Just tenv,_,_)        | fromComp -> (CSEnv, Just tenv)
+    (_,Just tgfo,_)        | fromComp -> (CSRead,Just tgfo)
+    (Just tenv,_,Just tgf) | tenv > tgf -> (CSEnv, Just tenv)
+    (_,Just tgfo,Just tgf) | tgfo > tgf -> (CSRead,Just tgfo)
+    (Just tenv,_,Nothing) -> (CSEnv,Just tenv) -- source does not exist
+    (_,_,        Nothing) -> (CSRead,Nothing)  -- source does not exist
+    _ -> (CSComp,Nothing)
+  where
+    fromComp = flag optRecomp opts == NeverRecomp
+    fromSrc  = flag optRecomp opts == AlwaysRecomp
+
+
+-- internal module dep information
+
+
+data CompStatus =
+   CSComp -- compile: read gf
+ | CSRead -- read gfo
+ | CSEnv  -- gfo is in env
+  deriving Eq
+
+type ModuleInfo = (ModName,CompStatus,Maybe ClockTime,[ModName],InitPath)
+
+ 
+importsOfModule :: ModDef -> (ModName,[ModName])
+importsOfModule (MModule _ typ body) = modType typ (modBody body [])
+  where
+    modType (MTAbstract  m)      xs = (modName m,xs)
+    modType (MTResource m)       xs = (modName m,xs)
+    modType (MTInterface m)      xs = (modName m,xs)
+    modType (MTConcrete m m2)    xs = (modName m,modName m2:xs)
+    modType (MTInstance m m2)    xs = (modName m,modName m2:xs)
+    modType (MTTransfer m o1 o2) xs = (modName m,open o1 (open o2 xs))
+
+    modBody (MBody e o _)            xs = extend e (opens o xs)
+    modBody (MNoBody is)             xs = foldr include xs is
+    modBody (MWith i os)             xs = include i (foldr open xs os)
+    modBody (MWithBody i os o _)     xs = include i (foldr open (opens o xs) os)
+    modBody (MWithE is i os)         xs = foldr include (include i (foldr open xs os)) is
+    modBody (MWithEBody is i os o _) xs = foldr include (include i (foldr open (opens o xs) os)) is
+    modBody (MReuse m)               xs = modName m:xs
+    modBody (MUnion is)              xs = foldr include xs is
+
+    include (IAll   m)   xs = modName m:xs
+    include (ISome  m _) xs = modName m:xs
+    include (IMinus m _) xs = modName m:xs
+
+    open (OName n)     xs = modName n:xs
+    open (OQualQO _ n) xs = modName n:xs
+    open (OQual _ _ n) xs = modName n:xs
+
+    extend NoExt    xs = xs
+    extend (Ext is) xs = foldr include xs is
+
+    opens NoOpens     xs = xs
+    opens (OpenIn os) xs = foldr open xs os
+
+    modName (PIdent (_,s)) = BS.unpack s
+
+
+-- | options can be passed to the compiler by comments in @--#@, in the main file
+getOptionsFromFile :: FilePath -> IOE Options
+getOptionsFromFile file = do
+  s <- ioeIO $ readFileIfStrict file
+  let ls = filter (BS.isPrefixOf (BS.pack "--#")) $ BS.lines s
+      fs = map (BS.unpack . BS.unwords . BS.words . BS.drop 3) ls
+  ioeErr $ liftM moduleOptions $ parseModuleOptions fs
diff --git a/src/GF/Compile/Rebuild.hs b/src/GF/Compile/Rebuild.hs
new file mode 100644
index 000000000..ec9076e1c
--- /dev/null
+++ b/src/GF/Compile/Rebuild.hs
@@ -0,0 +1,104 @@
+----------------------------------------------------------------------
+-- |
+-- Module      : Rebuild
+-- Maintainer  : AR
+-- Stability   : (stable)
+-- Portability : (portable)
+--
+-- > CVS $Date: 2005/05/30 21:08:14 $ 
+-- > CVS $Author: aarne $
+-- > CVS $Revision: 1.14 $
+--
+-- Rebuild a source module from incomplete and its with-instance.
+-----------------------------------------------------------------------------
+
+module GF.Compile.Rebuild (rebuildModule) where
+
+import GF.Grammar.Grammar
+import GF.Compile.ModDeps
+import GF.Grammar.PrGrammar
+import GF.Grammar.Lookup
+import GF.Compile.Extend
+import GF.Grammar.Macros
+
+import GF.Infra.Ident
+import GF.Infra.Modules
+import GF.Infra.Option
+import GF.Data.Operations
+
+import Data.List (nub)
+
+-- | rebuilding instance + interface, and "with" modules, prior to renaming. 
+-- AR 24/10/2003
+rebuildModule :: [SourceModule] -> SourceModule -> Err SourceModule
+rebuildModule ms mo@(i,mi) = do
+  let gr = MGrammar ms
+----  deps <- moduleDeps ms
+----  is   <- openInterfaces deps i
+  let is = [] ---- the method above is buggy: try "i -src" for two grs. AR 8/3/2005
+  mi'  <- case mi of
+
+    -- add the information given in interface into an instance module
+    ModMod m -> do
+      testErr (null is || mstatus m == MSIncomplete) 
+              ("module" +++ prt i +++ 
+               "has open interfaces and must therefore be declared incomplete") 
+      case mtype m of
+        MTInstance i0 -> do
+          m1 <- lookupModMod gr i0
+          testErr (isModRes m1) ("interface expected instead of" +++ prt i0)
+          m' <- do
+            js' <- extendMod False (i0,const True) i (jments m1) (jments m)
+            --- to avoid double inclusions, in instance I of I0 = J0 ** ...
+            case extends m of
+              [] -> return $ replaceJudgements m js'
+              j0s -> do 
+                m0s <- mapM (lookupModMod gr) j0s
+                let notInM0 c _  = all (not . isInBinTree c . jments) m0s
+                let js2 = filterBinTree notInM0 js'
+                return $ (replaceJudgements m js2) 
+                  {positions = 
+                    buildTree (tree2list (positions m1) ++ 
+                               tree2list (positions m))}
+          return $ ModMod m'
+        _ -> return mi
+
+    -- add the instance opens to an incomplete module "with" instances
+    --      ModWith mt stat ext me ops -> do
+    ModWith (Module mt stat fs_ me ops_ js_ ps_) (ext,incl) ops -> do
+      let insts = [(inf,inst) | OQualif _ inf inst <- ops]
+      let infs  = map fst insts
+      let stat' = ifNull MSComplete (const MSIncomplete)
+                    [i | i <- is, notElem i infs]
+      testErr (stat' == MSComplete || stat == MSIncomplete) 
+              ("module" +++ prt i +++ "remains incomplete")
+      Module mt0 _ fs me' ops0 js ps0 <- lookupModMod gr ext
+      let ops1 = nub $
+                   ops_ ++ -- N.B. js has been name-resolved already
+                   ops ++ [o | o <- ops0, notElem (openedModule o) infs]
+                       ++ [oQualif i i | i <- map snd insts] ----
+                       ++ [oSimple i   | i <- map snd insts] ----
+
+      --- check if me is incomplete
+      let fs1 = addModuleOptions fs fs_                           -- new flags have priority
+      let js0 = [ci | ci@(c,_) <- tree2list js, isInherited incl c]
+      let js1 = buildTree (tree2list js_ ++ js0)
+      let ps1 = buildTree (tree2list ps_ ++ tree2list ps0)
+      return $ ModMod $ Module mt0 stat' fs1 me ops1 js1 ps1 
+                          ---- (mapTree (qualifInstanceInfo insts) js) -- not needed
+
+    _ -> return mi
+  return (i,mi')
+
+checkCompleteInstance :: SourceRes -> SourceRes -> Err ()
+checkCompleteInstance abs cnc = ifNull (return ()) (Bad . unlines) $
+  checkComplete [f | (f, ResOper (Yes _) _) <- abs'] cnc'
+   where
+     abs' = tree2list $ jments abs
+     cnc' = jments cnc
+     checkComplete sought given = foldr ckOne [] sought
+       where
+         ckOne f = if isInBinTree f given 
+                      then id
+                      else (("Error: no definition given to" +++ prt f):)
+
diff --git a/src/GF/Compile/Refresh.hs b/src/GF/Compile/Refresh.hs
new file mode 100644
index 000000000..39fb57db0
--- /dev/null
+++ b/src/GF/Compile/Refresh.hs
@@ -0,0 +1,133 @@
+----------------------------------------------------------------------
+-- |
+-- Module      : Refresh
+-- Maintainer  : AR
+-- Stability   : (stable)
+-- Portability : (portable)
+--
+-- > CVS $Date: 2005/04/21 16:22:27 $ 
+-- > CVS $Author: bringert $
+-- > CVS $Revision: 1.6 $
+--
+-- (Description of the module)
+-----------------------------------------------------------------------------
+
+module GF.Compile.Refresh (refreshTerm, refreshTermN,
+		refreshModule
+	       ) where
+
+import GF.Data.Operations
+import GF.Grammar.Grammar
+import GF.Infra.Ident
+import GF.Infra.Modules
+import GF.Grammar.Macros
+import Control.Monad
+
+refreshTerm :: Term -> Err Term
+refreshTerm = refreshTermN 0
+
+refreshTermN :: Int -> Term -> Err Term
+refreshTermN i e = liftM snd $ refreshTermKN i e
+
+refreshTermKN :: Int -> Term -> Err (Int,Term)
+refreshTermKN i e = liftM (\ (t,(_,i)) -> (i,t)) $ 
+                    appSTM (refresh e) (initIdStateN i)
+
+refresh :: Term -> STM IdState Term
+refresh e = case e of
+
+  Vr x    -> liftM  Vr  (lookVar x)
+  Abs x b -> liftM2 Abs (refVarPlus x)  (refresh b)
+
+  Prod x a b -> do
+    a'  <- refresh a
+    x'  <- refVar  x
+    b'  <- refresh b
+    return $ Prod x' a' b'
+
+  Let (x,(mt,a)) b -> do
+    a'  <- refresh a
+    mt' <- case mt of
+             Just t -> refresh t >>= (return . Just) 
+             _ -> return mt
+    x'  <- refVar x
+    b'  <- refresh b
+    return (Let (x',(mt',a')) b')
+
+  R r  -> liftM R $ refreshRecord r
+
+  ExtR r s -> liftM2 ExtR (refresh r)  (refresh s)
+  
+  T i cc -> liftM2 T (refreshTInfo i) (mapM refreshCase cc)
+
+  _ -> composOp refresh e
+
+refreshCase :: (Patt,Term) -> STM IdState (Patt,Term)
+refreshCase (p,t) = liftM2 (,) (refreshPatt p) (refresh t)
+
+refreshPatt p = case p of
+  PV x    -> liftM PV     (refVar x)
+  PC c ps -> liftM (PC c) (mapM refreshPatt ps)
+  PP q c ps -> liftM (PP q c) (mapM refreshPatt ps)
+  PR r    -> liftM PR     (mapPairsM refreshPatt r)
+  PT t p' -> liftM2 PT    (refresh t) (refreshPatt p')
+
+  PAs x p'   -> liftM2 PAs     (refVar x) (refreshPatt p')
+
+  PSeq p' q' -> liftM2 PSeq    (refreshPatt p') (refreshPatt q')
+  PAlt p' q' -> liftM2 PAlt    (refreshPatt p') (refreshPatt q')
+  PRep p'    -> liftM  PRep    (refreshPatt p')
+  PNeg p'    -> liftM  PNeg    (refreshPatt p')
+
+  _ -> return p
+
+refreshRecord r = case r of
+  [] -> return r
+  (x,(mt,a)):b -> do
+    a'  <- refresh a
+    mt' <- case mt of
+             Just t -> refresh t >>= (return . Just) 
+             _ -> return mt
+    b'  <- refreshRecord b
+    return $ (x,(mt',a')) : b'
+
+refreshTInfo i = case i of
+  TTyped t -> liftM TTyped $ refresh t
+  TComp t -> liftM TComp $ refresh t
+  TWild t -> liftM TWild $ refresh t
+  _ -> return i
+
+-- for abstract syntax
+
+refreshEquation :: Equation -> Err ([Patt],Term)
+refreshEquation pst = err Bad (return . fst) (appSTM (refr pst) initIdState) where
+  refr (ps,t) = liftM2 (,) (mapM refreshPatt ps) (refresh t)
+
+-- for concrete and resource in grammar, before optimizing
+
+refreshGrammar :: SourceGrammar -> Err SourceGrammar
+refreshGrammar = liftM (MGrammar . snd) . foldM refreshModule (0,[]) . modules
+
+refreshModule :: (Int,[SourceModule]) -> SourceModule -> Err (Int,[SourceModule])
+refreshModule (k,ms) mi@(i,m) = case m of
+    ModMod mo | (isModCnc mo || isModRes mo) -> do
+      (k',js') <- foldM refreshRes (k,[]) $ tree2list $ jments mo
+      return (k', (i, ModMod(replaceJudgements mo (buildTree js'))) : ms)
+    _ -> return (k, mi:ms)
+ where
+  refreshRes (k,cs) ci@(c,info) = case info of
+    ResOper ptyp (Yes trm) -> do   ---- refresh ptyp
+      (k',trm') <- refreshTermKN k trm
+      return $ (k', (c, ResOper ptyp (Yes trm')):cs)
+    ResOverload os tyts -> do
+      (k',tyts') <- liftM (\ (t,(_,i)) -> (i,t)) $ 
+                    appSTM (mapPairsM refresh tyts) (initIdStateN k)
+      return $ (k', (c, ResOverload os tyts'):cs)
+    CncCat mt (Yes trm) pn -> do   ---- refresh mt, pn
+      (k',trm') <- refreshTermKN k trm
+      return $ (k', (c, CncCat mt (Yes trm') pn):cs)
+    CncFun mt (Yes trm) pn -> do   ---- refresh pn
+      (k',trm') <- refreshTermKN k trm
+      return $ (k', (c, CncFun mt (Yes trm') pn):cs)
+    _ -> return (k, ci:cs)
+
diff --git a/src/GF/Compile/RemoveLiT.hs b/src/GF/Compile/RemoveLiT.hs
new file mode 100644
index 000000000..d06b80400
--- /dev/null
+++ b/src/GF/Compile/RemoveLiT.hs
@@ -0,0 +1,64 @@
+----------------------------------------------------------------------
+-- |
+-- Module      : RemoveLiT
+-- Maintainer  : AR
+-- Stability   : (stable)
+-- Portability : (portable)
+--
+-- > CVS $Date: 2005/04/21 16:21:45 $ 
+-- > CVS $Author: bringert $
+-- > CVS $Revision: 1.6 $
+--
+-- remove obsolete (Lin C) expressions before doing anything else. AR 21/6/2003
+--
+-- What the program does is replace the occurrences of Lin C with the actual
+-- definition T given in lincat C = T ; with {s : Str} if no lincat is found.
+-- The procedure is uncertain, if T contains another Lin.
+-----------------------------------------------------------------------------
+
+module GF.Compile.RemoveLiT (removeLiT) where
+
+import GF.Grammar.Grammar
+import GF.Infra.Ident
+import GF.Infra.Modules
+import GF.Grammar.Macros
+import GF.Grammar.Lookup
+import GF.Grammar.Predef
+
+import GF.Data.Operations
+
+import Control.Monad
+
+removeLiT :: SourceGrammar -> Err SourceGrammar
+removeLiT gr = liftM MGrammar $ mapM (remlModule gr) (modules gr)
+
+remlModule :: SourceGrammar -> (Ident,SourceModInfo) -> Err (Ident,SourceModInfo)
+remlModule gr mi@(name,mod) = case mod of
+  ModMod mo -> do
+    js1 <- mapMTree (remlResInfo gr) (jments mo)
+    let mod2 = ModMod $ mo {jments = js1}
+    return $ (name,mod2)
+  _ -> return mi
+
+remlResInfo :: SourceGrammar -> (Ident,Info) -> Err (Ident,Info)
+remlResInfo gr mi@(i,info) = case info of
+  ResOper pty ptr    -> liftM ((,) i) $ liftM2 ResOper (ren pty) (ren ptr)
+  CncCat pty ptr ppr -> liftM ((,) i) $ liftM3 CncCat (ren pty) (ren ptr) (ren ppr)
+  CncFun mt  ptr ppr -> liftM ((,) i) $ liftM2 (CncFun mt)      (ren ptr) (ren ppr)
+  _ -> return mi
+ where 
+   ren = remlPerh gr
+
+remlPerh gr pt = case pt of
+  Yes t -> liftM Yes $ remlTerm gr t
+  _ -> return pt
+
+remlTerm :: SourceGrammar -> Term -> Err Term
+remlTerm gr trm = case trm of
+  LiT c -> look c >>= remlTerm gr
+  _ -> composOp (remlTerm gr) trm
+ where
+   look c = err (const $ return defLinType) return $ lookupLincat gr m c
+   m = case [cnc | (cnc,ModMod m) <- modules gr, isModCnc m] of
+     cnc:_ -> cnc   -- actually there is always exactly one
+     _ -> cCNC
diff --git a/src/GF/Compile/Rename.hs b/src/GF/Compile/Rename.hs
new file mode 100644
index 000000000..7b4d09277
--- /dev/null
+++ b/src/GF/Compile/Rename.hs
@@ -0,0 +1,338 @@
+----------------------------------------------------------------------
+-- |
+-- Module      : Rename
+-- Maintainer  : AR
+-- Stability   : (stable)
+-- Portability : (portable)
+--
+-- > CVS $Date: 2005/05/30 18:39:44 $ 
+-- > CVS $Author: aarne $
+-- > CVS $Revision: 1.19 $
+--
+-- AR 14\/5\/2003
+-- The top-level function 'renameGrammar' does several things:
+--
+--   - extends each module symbol table by indirections to extended module
+--
+--   - changes unqualified and as-qualified imports to absolutely qualified
+--
+--   - goes through the definitions and resolves names
+--
+-- Dependency analysis between modules has been performed before this pass.
+-- Hence we can proceed by @fold@ing "from left to right".
+-----------------------------------------------------------------------------
+
+module GF.Compile.Rename (renameGrammar,
+	       renameSourceTerm,
+	       renameModule
+	      ) where
+
+import GF.Grammar.Grammar
+import GF.Grammar.Values
+import GF.Grammar.Predef
+import GF.Infra.Modules
+import GF.Infra.Ident
+import GF.Grammar.Macros
+import GF.Grammar.PrGrammar
+import GF.Grammar.AppPredefined
+import GF.Grammar.Lookup
+import GF.Compile.Extend
+import GF.Data.Operations
+
+import Control.Monad
+import Data.List (nub)
+import Debug.Trace (trace)
+
+renameGrammar :: SourceGrammar -> Err SourceGrammar
+renameGrammar g = liftM (MGrammar . reverse) $ foldM renameModule [] (modules g)
+
+-- | this gives top-level access to renaming term input in the cc command
+renameSourceTerm :: SourceGrammar -> Ident -> Term -> Err Term
+renameSourceTerm g m t = do
+  mo     <- lookupErr m (modules g)
+  status <- buildStatus g m mo
+  renameTerm status [] t
+
+renameModule :: [SourceModule] -> SourceModule -> Err [SourceModule]
+renameModule ms (name,mod) = errIn ("renaming module" +++ prt name) $ case mod of
+  ModMod mo -> do
+    let js1 = jments mo
+    status <- buildStatus (MGrammar ms) name mod
+    js2    <- mapsErrTree (renameInfo mo status) js1
+    let mod2 = ModMod $ mo {opens = map forceQualif (opens mo), jments = js2}
+    return $ (name,mod2) : ms
+
+type Status = (StatusTree, [(OpenSpec Ident, StatusTree)])
+
+type StatusTree = BinTree Ident StatusInfo
+
+type StatusInfo = Ident -> Term
+
+renameIdentTerm :: Status -> Term -> Err Term
+renameIdentTerm env@(act,imps) t = 
+ errIn ("atomic term" +++ prt t +++ "given" +++ unwords (map (prt . fst) qualifs)) $
+   case t of
+  Vr c -> ident predefAbs c
+  Cn c -> ident (\_ s -> Bad s) c
+  Q m' c | m' == cPredef {- && isInPredefined c -} -> return t
+  Q m' c -> do
+    m <- lookupErr m' qualifs
+    f <- lookupTree prt c m
+    return $ f c
+  QC m' c | m' == cPredef {- && isInPredefined c -} -> return t
+  QC m' c -> do
+    m <- lookupErr m' qualifs
+    f <- lookupTree prt c m
+    return $ f c
+  _ -> return t
+ where
+   opens  = [st  | (OSimple _ _,st) <- imps]
+   qualifs = [(m, st) | (OQualif _ m _, st) <- imps] ++ 
+             [(m, st) | (OSimple _ m, st) <- imps] -- qualif is always possible
+
+   -- this facility is mainly for BWC with GF1: you need not import PredefAbs
+   predefAbs c s
+     | isPredefCat c = return $ Q cPredefAbs c
+     | otherwise     = Bad s
+
+   ident alt c = case lookupTree prt c act of
+      Ok f -> return $ f c
+      _ -> case lookupTreeManyAll prt opens c of
+        [f] -> return $ f c
+        []  -> alt c ("constant not found:" +++ prt c) 
+        fs -> case nub [f c | f <- fs]  of
+          [tr] -> return tr
+          ts@(t:_) -> trace ("WARNING: conflict" +++ unwords (map prt ts)) (return t)
+            -- a warning will be generated in CheckGrammar, and the head returned
+            -- in next V: 
+            -- Bad $ "conflicting imports:" +++ unwords (map prt ts) 
+
+
+--- | would it make sense to optimize this by inlining?
+renameIdentPatt :: Status -> Patt -> Err Patt
+renameIdentPatt env p = do
+  let t = patt2term p
+  t' <- renameIdentTerm env t
+  term2patt t'
+
+info2status :: Maybe Ident -> (Ident,Info) -> (Ident,StatusInfo)
+info2status mq (c,i) = (c, case i of
+  AbsFun _ (Yes EData) -> maybe Con QC mq
+  ResValue _  -> maybe Con QC mq
+  ResParam _  -> maybe Con QC mq
+  AnyInd True m -> maybe Con (const (QC m)) mq
+  AnyInd False m -> maybe Cn (const (Q m)) mq
+  _           -> maybe Cn  Q mq
+  )
+
+tree2status :: OpenSpec Ident -> BinTree Ident Info -> BinTree Ident StatusInfo
+tree2status o = case o of
+  OSimple _ i   -> mapTree (info2status (Just i))
+  OQualif _ i j -> mapTree (info2status (Just j))
+
+buildStatus :: SourceGrammar -> Ident -> SourceModInfo -> Err Status
+buildStatus gr c mo = let mo' = self2status c mo in case mo of
+  ModMod m -> do
+    let gr1 = MGrammar $ (c,mo) : modules gr 
+        ops = [OSimple OQNormal e | e <- allExtends gr1 c] ++ allOpens m
+    mods <- mapM (lookupModule gr1 . openedModule) ops
+    let sts = map modInfo2status $ zip ops mods    
+    return $ if isModCnc m
+      then (emptyBinTree, reverse sts) -- the module itself does not define any names
+      else (mo',reverse sts) -- so the empty ident is not needed
+
+modInfo2status :: (OpenSpec Ident,SourceModInfo) -> (OpenSpec Ident, StatusTree)
+modInfo2status (o,i) = (o,case i of
+  ModMod m -> tree2status o (jments m)
+  )
+
+self2status :: Ident -> SourceModInfo -> StatusTree
+self2status c i = mapTree (info2status (Just c)) js where   -- qualify internal
+  js = case i of
+    ModMod m 
+      | isModTrans m -> sorted2tree $ filter noTrans $ tree2list $ jments m 
+      | otherwise -> jments m
+  noTrans (_,d) = case d of  -- to enable other than transfer js in transfer module 
+    AbsTrans _ -> False
+    _ -> True
+
+forceQualif o = case o of
+  OSimple q i   -> OQualif q i i
+  OQualif q _ i -> OQualif q i i
+  
+renameInfo :: Module Ident Info -> Status -> (Ident,Info) -> Err (Ident,Info)
+renameInfo mo status (i,info) = errIn 
+    ("renaming definition of" +++ prt i +++ showPosition mo i) $ 
+                                liftM ((,) i) $ case info of
+  AbsCat pco pfs -> liftM2 AbsCat (renPerh (renameContext status) pco)
+                                  (renPerh (mapM rent) pfs)
+  AbsFun pty ptr -> liftM2 AbsFun (ren pty) (ren ptr)
+  AbsTrans f -> liftM AbsTrans (rent f)
+
+  ResOper pty ptr -> liftM2 ResOper (ren pty) (ren ptr)
+  ResOverload os tysts -> 
+    liftM (ResOverload os) (mapM (pairM rent) tysts)
+
+  ResParam (Yes (pp,m)) -> do
+    pp' <- mapM (renameParam status) pp
+    return $ ResParam $ Yes (pp',m)
+  ResValue (Yes (t,m)) -> do
+    t' <- rent t
+    return $ ResValue $ Yes (t',m)
+  CncCat pty ptr ppr -> liftM3 CncCat (ren pty) (ren ptr) (ren ppr)
+  CncFun mt  ptr ppr -> liftM2 (CncFun mt)      (ren ptr) (ren ppr)
+  _ -> return info
+ where 
+   ren = renPerh rent
+   rent = renameTerm status []
+
+renPerh ren pt = case pt of
+  Yes t -> liftM Yes $ ren t
+  _ -> return pt
+
+renameTerm :: Status -> [Ident] -> Term -> Err Term
+renameTerm env vars = ren vars where
+  ren vs trm = case trm of
+    Abs x b    -> liftM  (Abs x) (ren (x:vs) b)
+    Prod x a b -> liftM2 (Prod x) (ren vs a) (ren (x:vs) b)
+    Typed a b  -> liftM2 Typed (ren vs a) (ren vs b)
+    Vr x      
+      | elem x vs -> return trm
+      | otherwise -> renid trm
+    Cn _   -> renid trm
+    Con _  -> renid trm
+    Q _ _  -> renid trm
+    QC _ _ -> renid trm
+    Eqs eqs -> liftM Eqs $ mapM (renameEquation env vars) eqs
+    T i cs -> do
+      i' <- case i of
+        TTyped ty -> liftM TTyped $ ren vs ty -- the only annotation in source
+        _ -> return i
+      liftM (T i') $ mapM (renCase vs) cs  
+
+    Let (x,(m,a)) b -> do
+      m' <- case m of
+        Just ty -> liftM Just $ ren vs ty
+        _ -> return m
+      a' <- ren vs a
+      b' <- ren (x:vs) b
+      return $ Let (x,(m',a')) b'
+
+    P t@(Vr r) l                     -- for constant t we know it is projection
+      | elem r vs -> return trm                           -- var proj first
+      | otherwise -> case renid (Q r (label2ident l)) of  -- qualif   second
+          Ok t -> return t
+          _ -> case liftM (flip P l) $ renid t of
+            Ok t -> return t                              -- const proj last
+            _ -> prtBad "unknown qualified constant" trm
+
+    EPatt p -> do
+      (p',_) <- renpatt p
+      return $ EPatt p'
+
+    _ -> composOp (ren vs) trm
+
+  renid = renameIdentTerm env
+  renCase vs (p,t) = do
+    (p',vs') <- renpatt p
+    t' <- ren (vs' ++ vs) t
+    return (p',t')
+  renpatt = renamePattern env
+
+-- | vars not needed in env, since patterns always overshadow old vars
+renamePattern :: Status -> Patt -> Err (Patt,[Ident])
+renamePattern env patt = case patt of
+
+  PMacro c -> do
+    c' <- renid $ Vr c
+    case c' of
+      Q p d -> renp $ PM p d
+      _ -> prtBad "unresolved pattern" patt
+
+  PC c ps -> do
+    c' <- renameIdentTerm env $ Cn c
+    case c' of
+      QC p d -> renp $ PP p d ps
+--      Q  p d -> renp $ PP p d ps --- why this? AR 15/3/2008
+      _ -> prtBad "unresolved pattern" c' ---- (PC c ps', concat vs)
+
+  PP p c ps -> do
+
+    (p', c') <- case renameIdentTerm env (QC p c) of
+      Ok (QC p' c') -> return (p',c')
+      _ -> return (p,c) --- temporarily, for bw compat
+    psvss <- mapM renp ps
+    let (ps',vs) = unzip psvss
+    return (PP p' c' ps', concat vs)
+
+  PM p c -> do
+    (p', c') <- case renameIdentTerm env (Q p c) of
+      Ok (Q p' c') -> return (p',c')
+      _ -> prtBad "not a pattern macro" patt
+    return (PM p' c', [])
+
+  PV x -> case renid (Vr x) of
+    Ok (QC m c) -> return (PP m c [],[])
+    _    -> return (patt, [x])
+
+  PR r -> do
+    let (ls,ps) = unzip r
+    psvss <- mapM renp ps
+    let (ps',vs') = unzip psvss
+    return (PR (zip ls ps'), concat vs') 
+
+  PAlt p q -> do
+    (p',vs) <- renp p
+    (q',ws) <- renp q
+    return (PAlt p' q', vs ++ ws)
+
+  PSeq p q -> do
+    (p',vs) <- renp p
+    (q',ws) <- renp q
+    return (PSeq p' q', vs ++ ws)
+
+  PRep p -> do
+    (p',vs) <- renp p
+    return (PRep p', vs)
+
+  PNeg p -> do
+    (p',vs) <- renp p
+    return (PNeg p', vs)
+
+  PAs x p -> do
+    (p',vs) <- renp p
+    return (PAs x p', x:vs)
+
+  _ -> return (patt,[])
+
+ where 
+   renp  = renamePattern env
+   renid = renameIdentTerm env
+
+renameParam :: Status -> (Ident, Context) -> Err (Ident, Context)
+renameParam env (c,co) = do
+  co' <- renameContext env co
+  return (c,co')
+
+renameContext :: Status -> Context -> Err Context
+renameContext b = renc [] where
+  renc vs cont = case cont of
+    (x,t) : xts 
+      | isWildIdent x -> do
+          t'   <- ren vs t
+          xts' <- renc vs xts
+          return $ (x,t') : xts'
+      | otherwise -> do
+          t'   <- ren vs t
+          let vs' = x:vs
+          xts' <- renc vs' xts
+          return $ (x,t') : xts'
+    _ -> return cont
+  ren = renameTerm b
+
+-- | vars not needed in env, since patterns always overshadow old vars
+renameEquation :: Status -> [Ident] -> Equation -> Err Equation
+renameEquation b vs (ps,t) = do
+  (ps',vs') <- liftM unzip $ mapM (renamePattern b) ps
+  t'        <- renameTerm b (concat vs' ++ vs) t
+  return (ps',t')
diff --git a/src/GF/Compile/TC.hs b/src/GF/Compile/TC.hs
new file mode 100644
index 000000000..c0c8a83ae
--- /dev/null
+++ b/src/GF/Compile/TC.hs
@@ -0,0 +1,292 @@
+----------------------------------------------------------------------
+-- |
+-- 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,
+           checkEqs,
+	   eqVal,
+	   whnf
+	  ) where
+
+import GF.Data.Operations
+import GF.Grammar.Predef
+import GF.Grammar.Abstract
+
+import Control.Monad
+import Data.List (sortBy)
+
+data AExp =
+     AVr   Ident Val 
+   | ACn   QIdent Val
+   | AType 
+   | AInt  Integer 
+   | AFloat Double
+   | AStr  String
+   | AMeta MetaSymb Val
+   | AApp  AExp AExp Val 
+   | AAbs  Ident Val AExp 
+   | AProd Ident AExp AExp 
+   | AEqs  [([Exp],AExp)] --- not used
+   | AData Val
+  deriving (Eq,Show)
+
+type Theory = QIdent -> Err Val
+
+lookupConst :: Theory -> QIdent -> Err Val
+lookupConst th f = th f
+
+lookupVar :: Env -> Ident -> Err Val
+lookupVar g x = maybe (prtBad "unknown variable" x) return $ lookup x ((IW,uVal):g)
+-- wild card IW: no error produced, ?0 instead.
+
+type TCEnv = (Int,Env,Env)
+
+emptyTCEnv :: TCEnv
+emptyTCEnv = (0,[],[])
+
+whnf :: Val -> Err Val
+whnf v = ---- errIn ("whnf" +++ prt v) $ ---- debug
+         case v of
+  VApp u w -> do
+    u' <- whnf u 
+    w' <- whnf w
+    app u' w'
+  VClos env e -> eval env e
+  _ -> return v
+
+app :: Val -> Val -> Err Val
+app u v = case u of
+  VClos env (Abs x e) -> eval ((x,v):env) e
+  _ -> return $ VApp u v
+  
+eval :: Env -> Exp -> Err Val
+eval env e = ---- errIn ("eval" +++ prt e +++ "in" +++ prEnv env) $ 
+             case e of
+  Vr x    -> lookupVar env x
+  Q m c   -> return $ VCn (m,c)
+  QC m c  -> return $ VCn (m,c) ---- == Q ?
+  Sort c  -> return $ VType --- the only sort is Type
+  App f a -> join $ liftM2 app (eval env f) (eval env a)
+  _ -> return $ VClos env e
+
+eqVal :: Int -> Val -> Val -> Err [(Val,Val)]
+eqVal k u1 u2 = ---- errIn (prt u1 +++ "<>" +++ prBracket (show k) +++ prt u2) $ 
+                do
+  w1 <- whnf u1
+  w2 <- whnf u2 
+  let v = VGen k
+  case (w1,w2) of
+    (VApp f1 a1, VApp f2 a2) -> liftM2 (++) (eqVal k f1 f2) (eqVal k a1 a2)
+    (VClos env1 (Abs x1 e1), VClos env2 (Abs x2 e2)) ->
+      eqVal (k+1) (VClos ((x1,v x1):env1) e1) (VClos ((x2,v x1):env2) e2)
+    (VClos env1 (Prod x1 a1 e1), VClos env2 (Prod x2 a2 e2)) ->
+      liftM2 (++) 
+        (eqVal k     (VClos env1          a1) (VClos env2          a2))
+        (eqVal (k+1) (VClos ((x1,v x1):env1) e1) (VClos ((x2,v x1):env2) e2))
+    (VGen i _, VGen j _) -> return [(w1,w2) | i /= j]
+    (VCn (_, i), VCn (_,j)) -> return [(w1,w2) | i /= j] 
+    --- thus ignore qualifications; valid because inheritance cannot
+    --- be qualified. Simplifies annotation. AR 17/3/2005 
+    _ -> return [(w1,w2) | w1 /= w2]
+-- invariant: constraints are in whnf
+
+checkType :: Theory -> TCEnv -> Exp -> Err (AExp,[(Val,Val)])
+checkType th tenv e = checkExp th tenv e vType
+
+checkExp :: Theory -> TCEnv -> Exp -> Val -> Err (AExp, [(Val,Val)])
+checkExp th tenv@(k,rho,gamma) e ty = do
+  typ <- whnf ty
+  let v = VGen k
+  case e of
+    Meta m -> return $ (AMeta m typ,[])
+    EData -> return $ (AData typ,[])
+
+    Abs x t -> case typ of
+      VClos env (Prod y a b) -> do
+	a' <- whnf $ VClos env a ---
+	(t',cs) <- checkExp th 
+                           (k+1,(x,v x):rho, (x,a'):gamma) t (VClos ((y,v x):env) b)
+	return (AAbs x a' t', cs)
+      _ -> prtBad ("function type expected for" +++ prt e +++ "instead of") typ
+
+-- {- --- to get deprec when checkEqs works (15/9/2005)
+    Eqs es -> do
+      bcs <- mapM (\b -> checkBranch th tenv b typ) es
+      let (bs,css) = unzip bcs
+      return (AEqs bs, concat css) 
+-- - }
+    Prod x a b -> do
+      testErr (typ == vType) "expected Type"
+      (a',csa) <- checkType th tenv a
+      (b',csb) <- checkType th (k+1, (x,v x):rho, (x,VClos rho a):gamma) b
+      return (AProd x a' b', csa ++ csb)
+
+    _ -> checkInferExp th tenv e typ
+
+checkInferExp :: Theory -> TCEnv -> Exp -> Val -> Err (AExp, [(Val,Val)])
+checkInferExp th tenv@(k,_,_) e typ = do
+  (e',w,cs1) <- inferExp th tenv e
+  cs2 <- eqVal k w typ
+  return (e',cs1 ++ cs2)
+      
+inferExp :: Theory -> TCEnv -> Exp -> Err (AExp, Val, [(Val,Val)])
+inferExp th tenv@(k,rho,gamma) e = case e of
+   Vr x -> mkAnnot (AVr x) $ noConstr $ lookupVar gamma x
+   Q m c | m == cPredefAbs && 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, [])
+   App f t -> do
+    (f',w,csf) <- inferExp th tenv f 
+    typ <- whnf w
+    case typ of
+      VClos env (Prod x a b) -> do
+        (a',csa) <- checkExp th tenv t (VClos env a)
+	b' <- whnf $ VClos ((x,VClos rho t):env) b
+	return $ (AApp f' a' b', b', csf ++ csa)
+      _ -> prtBad ("Prod expected for function" +++ prt f +++ "instead of") typ
+   _ -> prtBad "cannot infer type of expression" e
+
+checkEqs :: Theory -> TCEnv -> (Fun,Trm) -> Val -> Err [(Val,Val)]
+checkEqs th tenv@(k,rho,gamma) (fun@(m,f),def) val = case def of
+  Eqs es -> liftM concat $ mapM checkBranch es
+  _      -> liftM snd $ checkExp th tenv def val
+ where
+  checkBranch (ps,df) = 
+   let
+      (ps',_,vars) = foldr p2t ([],0,[]) ps
+      fps        = mkApp (Q m f) ps'
+   in errIn ("branch" +++ prt fps) $ do
+    (aexp, typ, cs1) <- inferExp th tenv fps
+    let
+      bds = binds vars aexp 
+      tenv' = (k, rho, bds ++ gamma) 
+    (_,cs2)  <- errIn (show bds) $ checkExp th tenv' df typ
+    return $ (cs1 ++ cs2)
+  p2t p (ps,i,g) = case p of
+     PW      -> (Meta (MetaSymb i) : ps, i+1,        g) 
+     PV IW   -> (Meta (MetaSymb i) : ps, i+1,        g) 
+     PV x    -> (Meta (MetaSymb i) : ps, i+1,upd x i g)
+     PString s -> (            K s : ps, i,          g)
+     PInt n -> (EInt n : ps, i, g)
+     PFloat n -> (EFloat n : ps, i, g)
+     PP m c xs -> (mkApp (qq (m,c)) xss : ps, i', g') 
+                    where (xss,i',g') = foldr p2t ([],i,g) xs
+     _ -> error $ "undefined p2t case" +++ prt p +++ "in checkBranch"
+  upd x i g = (x,i) : g --- to annotate pattern variables: treat as metas
+  
+  -- notice: in vars, the sequence 0.. is sorted. In subst aexp, all
+  -- this occurs and nothing else.
+  binds vars aexp = [(x,v) | ((x,_),v) <- zip vars metas] where
+    metas = map snd $ sortBy (\ (x,_) (y,_) -> compare x y) $ subst aexp
+  subst aexp = case aexp of
+   AMeta (MetaSymb i) v -> [(i,v)]
+   AApp  c a _ -> subst c ++ subst a
+   _ -> [] -- never matter in patterns
+
+checkBranch :: Theory -> TCEnv -> Equation -> Val -> Err (([Exp],AExp),[(Val,Val)])
+checkBranch th tenv b@(ps,t) ty = errIn ("branch" +++ show b) $ 
+                                  chB tenv' ps' ty 
+ where 
+
+  (ps',_,rho2,k') = ps2ts k ps
+  tenv' = (k, rho2++rho, gamma) ---- k' ?
+  (k,rho,gamma) = tenv
+
+  chB tenv@(k,rho,gamma) ps ty = case ps of
+    p:ps2 -> do
+      typ <- whnf ty
+      case typ of
+        VClos env (Prod y a b) -> do
+	  a' <- whnf $ VClos env a
+          (p', sigma, binds, cs1) <- checkP tenv p y a'
+          let tenv' = (length binds, sigma ++ rho, binds ++ gamma)
+          ((ps',exp),cs2) <- chB tenv' ps2 (VClos ((y,p'):env) b)
+	  return ((p:ps',exp), cs1 ++ cs2) -- don't change the patt
+        _ -> prtBad ("Product expected for definiens" +++prt t +++ "instead of") typ
+    [] -> do
+      (e,cs) <- checkExp th tenv t ty
+      return (([],e),cs)
+  checkP env@(k,rho,gamma) t x a = do
+     (delta,cs) <- checkPatt th env t a
+     let sigma = [(x, VGen i x) | ((x,_),i) <- zip delta [k..]]
+     return (VClos sigma t, sigma, delta, cs)
+
+  ps2ts k = foldr p2t ([],0,[],k) 
+  p2t p (ps,i,g,k) = case p of
+     PW      -> (Meta (MetaSymb i) : ps, i+1,g,k) 
+     PV IW   -> (Meta (MetaSymb i) : ps, i+1,g,k) 
+     PV x    -> (Vr x   : ps, i, upd x k g,k+1)
+     PString s -> (K s : ps, i, g, k)
+     PInt n -> (EInt n : ps, i, g, k)
+     PFloat n -> (EFloat n : ps, i, g, k)
+     PP m c xs -> (mkApp (qq (m,c)) xss : ps, j, g',k') 
+                    where (xss,j,g',k') = foldr p2t ([],i,g,k) xs
+     _ -> error $ "undefined p2t case" +++ prt p +++ "in checkBranch"
+
+  upd x k g = (x, VGen k x) : g --- hack to recognize pattern variables
+
+
+checkPatt :: Theory -> TCEnv -> Exp -> Val -> Err (Binds,[(Val,Val)])
+checkPatt th tenv exp val = do
+  (aexp,_,cs) <- checkExpP tenv exp val
+  let binds = extrBinds aexp
+  return (binds,cs)
+ where
+   extrBinds aexp = case aexp of
+     AVr i v    -> [(i,v)]
+     AApp f a _ -> extrBinds f ++ extrBinds a
+     _ -> [] -- no other cases are possible
+
+--- ad hoc, to find types of variables
+   checkExpP tenv@(k,rho,gamma) exp val = case exp of
+     Meta m -> return $ (AMeta m val, val, [])
+     Vr x   -> return $ (AVr   x val, val, [])
+     EInt i -> return (AInt i, valAbsInt, [])
+     EFloat i -> return (AFloat i, valAbsFloat, [])
+     K s    -> return (AStr s, valAbsString, [])
+
+     Q m c  -> do
+       typ <- lookupConst th (m,c)
+       return $ (ACn (m,c) typ, typ, [])
+     QC m c  -> do
+       typ <- lookupConst th (m,c)
+       return $ (ACn (m,c) typ, typ, []) ----
+     App f t -> do
+       (f',w,csf) <- checkExpP tenv f val
+       typ <- whnf w
+       case typ of
+         VClos env (Prod x a b) -> do
+           (a',_,csa) <- checkExpP tenv t (VClos env a)
+	   b' <- whnf $ VClos ((x,VClos rho t):env) b
+	   return $ (AApp f' a' b', b', csf ++ csa)
+         _ -> prtBad ("Prod expected for function" +++ prt f +++ "instead of") typ
+     _ -> prtBad "cannot typecheck pattern" exp
+
+-- auxiliaries
+
+noConstr :: Err Val -> Err (Val,[(Val,Val)])
+noConstr er = er >>= (\v -> return (v,[]))
+
+mkAnnot :: (Val -> AExp) -> Err (Val,[(Val,Val)]) -> Err (AExp,Val,[(Val,Val)])
+mkAnnot a ti = do
+  (v,cs) <- ti
+  return (a v, v, cs)
+
diff --git a/src/GF/Compile/TypeCheck.hs b/src/GF/Compile/TypeCheck.hs
new file mode 100644
index 000000000..2d58a33ee
--- /dev/null
+++ b/src/GF/Compile/TypeCheck.hs
@@ -0,0 +1,118 @@
+----------------------------------------------------------------------
+-- |
+-- 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,
+		  checkEquation,
+		  checkConstrs,
+		 ) where
+
+import GF.Data.Operations
+import GF.Data.Zipper
+
+import GF.Grammar.Abstract
+import GF.Compile.Refresh
+import GF.Grammar.LookAbs
+import qualified GF.Grammar.Lookup as Lookup ---
+import GF.Grammar.Unify ---
+
+import GF.Compile.TC
+
+import Control.Monad (foldM, liftM, liftM2)
+import Data.List (nub) ---
+
+-- | 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 []
+
+aexp2tree :: (AExp,[(Val,Val)]) -> Err Tree
+aexp2tree (aexp,cs) = do
+  (bi,at,vt,ts) <- treeForm aexp
+  ts' <- mapM aexp2tree [(t,[]) | t <- ts]
+  return $ Tr (N (bi,at,vt,(cs,[]),False),ts')
+ where
+  treeForm a = case a of
+     AAbs x v b  -> do
+       (bi, at, vt, args) <- treeForm b
+       v' <- whnf v ---- should not be needed...
+       return ((x,v') : bi, at, vt, args)
+     AApp c a v -> do
+       (_,at,_,args) <- treeForm c
+       v' <- whnf v ---- 
+       return ([],at,v',args ++ [a]) 
+     AVr x v -> do
+       v' <- whnf v ---- 
+       return ([],AtV x,v',[])
+     ACn c v -> do
+       v' <- whnf v ---- 
+       return ([],AtC c,v',[])
+     AInt i -> do
+       return ([],AtI i,valAbsInt,[])
+     AFloat i -> do
+       return ([],AtF i,valAbsFloat,[])
+     AStr s -> do
+       return ([],AtL s,valAbsString,[])
+     AMeta m v -> do
+       v' <- whnf v ---- 
+       return ([],AtM m,v',[])
+     _ -> Bad "illegal tree" -- AProd
+
+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 :: Grammar -> Exp -> Val -> Err Constraints
+justTypeCheck gr e v = do
+  (_,constrs0) <- checkExp (grammar2theory gr) (initTCEnv []) e v
+  return $ filter notJustMeta constrs0
+----  return $ fst $ splitConstraintsSrc gr constrs0
+---- this change was to force proper tc of abstract modules. 
+---- May not be quite right. AR 13/9/2005 
+
+notJustMeta (c,k) = case (c,k) of
+     (VClos g1 (Meta m1), VClos g2 (Meta m2)) -> False
+     _ -> True
+
+grammar2theory :: Grammar -> 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 :: Grammar -> Context -> [String]
+checkContext st = checkTyp st . cont2exp
+
+checkTyp :: Grammar -> Type -> [String]
+checkTyp gr typ = err singleton prConstrs $ justTypeCheck gr typ vType
+
+checkEquation :: Grammar -> Fun -> Trm -> [String]
+checkEquation gr (m,fun) def = err singleton id $ do
+  typ  <- lookupFunType gr m fun
+  cs   <- justTypeCheck gr def (vClos typ)
+  let cs1 = filter notJustMeta cs
+  return $ ifNull [] (singleton . prConstraints) cs1
+
+checkConstrs :: Grammar -> Cat -> [Ident] -> [String]
+checkConstrs gr cat _ = [] ---- check constructors!
diff --git a/src/GF/Compile/Update.hs b/src/GF/Compile/Update.hs
new file mode 100644
index 000000000..82d7a609e
--- /dev/null
+++ b/src/GF/Compile/Update.hs
@@ -0,0 +1,135 @@
+----------------------------------------------------------------------
+-- |
+-- Module      : Update
+-- Maintainer  : AR
+-- Stability   : (stable)
+-- Portability : (portable)
+--
+-- > CVS $Date: 2005/05/30 18:39:44 $ 
+-- > CVS $Author: aarne $
+-- > CVS $Revision: 1.8 $
+--
+-- (Description of the module)
+-----------------------------------------------------------------------------
+
+module GF.Compile.Update (updateRes, buildAnyTree, combineAnyInfos, unifyAnyInfo,
+	       -- * these auxiliaries should be somewhere else 
+	       -- since they don't use the info types
+	       groupInfos, sortInfos, combineInfos, unifyInfos,
+	       tryInsert, unifAbsDefs, unifConstrs
+	      ) where
+
+import GF.Infra.Ident
+import GF.Grammar.Grammar
+import GF.Grammar.PrGrammar
+import GF.Infra.Modules
+
+import GF.Data.Operations
+
+import Data.List
+import Control.Monad
+
+-- | update a resource module by adding a new or changing an old definition
+updateRes :: SourceGrammar -> Ident -> Ident -> Info -> SourceGrammar
+updateRes gr@(MGrammar ms) m i info = MGrammar $ map upd ms where
+  upd (n,mod) 
+    | n /= m = (n,mod)
+    | n == m = case mod of
+       ModMod r -> (m,ModMod $ updateModule r i info)
+       _ -> (n,mod) --- no error msg
+
+-- | combine a list of definitions into a balanced binary search tree
+buildAnyTree :: [(Ident,Info)] -> Err (BinTree Ident Info)
+buildAnyTree ias = do
+  ias' <- combineAnyInfos ias
+  return $ buildTree ias'
+
+
+-- | unifying information for abstract, resource, and concrete
+combineAnyInfos :: [(Ident,Info)] -> Err [(Ident,Info)]
+combineAnyInfos = combineInfos unifyAnyInfo
+
+unifyAnyInfo :: Ident -> Info -> Info -> Err Info
+unifyAnyInfo c i j = errIn ("combining information for" +++ prt c) $ case (i,j) of
+  (AbsCat mc1 mf1, AbsCat mc2 mf2) -> 
+    liftM2 AbsCat (unifPerhaps mc1 mc2) (unifConstrs mf1 mf2) -- adding constrs
+  (AbsFun mt1 md1, AbsFun mt2 md2) -> 
+    liftM2 AbsFun (unifPerhaps mt1 mt2) (unifAbsDefs md1 md2) -- adding defs
+
+  (ResParam mt1, ResParam mt2) -> liftM ResParam $ unifPerhaps mt1 mt2
+  (ResOper mt1 m1, ResOper mt2 m2) -> 
+    liftM2 ResOper (unifPerhaps mt1 mt2) (unifPerhaps m1 m2)
+
+  (CncCat mc1 mf1 mp1, CncCat mc2 mf2 mp2) -> 
+    liftM3 CncCat (unifPerhaps mc1 mc2) (unifPerhaps mf1 mf2) (unifPerhaps mp1 mp2)
+  (CncFun m mt1 md1, CncFun _ mt2 md2) -> 
+    liftM2 (CncFun m) (unifPerhaps mt1 mt2) (unifPerhaps md1 md2) ---- adding defs
+-- for bw compatibility with unspecified printnames in old GF
+  (CncFun Nothing Nope (Yes pr),_) -> 
+    unifyAnyInfo c (CncCat Nope Nope (Yes pr)) j 
+  (_,CncFun Nothing Nope (Yes pr)) -> 
+    unifyAnyInfo c i (CncCat Nope Nope (Yes pr)) 
+
+  _ -> Bad $ "cannot unify informations in" ++++ show i ++++ "and" ++++ show j
+
+--- these auxiliaries should be somewhere else since they don't use the info types
+
+groupInfos :: Eq a => [(a,b)] -> [[(a,b)]]
+groupInfos = groupBy (\i j -> fst i == fst j)
+
+sortInfos :: Ord a => [(a,b)] -> [(a,b)]
+sortInfos = sortBy (\i j -> compare (fst i) (fst j))
+
+combineInfos :: Ord a => (a -> b -> b -> Err b) -> [(a,b)] -> Err [(a,b)]
+combineInfos f ris = do
+  let riss = groupInfos $ sortInfos ris
+  mapM (unifyInfos f) riss
+
+unifyInfos :: (a -> b -> b -> Err b) -> [(a,b)] -> Err (a,b)
+unifyInfos _ [] = Bad "empty info list"
+unifyInfos unif ris = do
+  let c = fst $ head ris
+  let infos = map snd ris
+  let ([i],is) = splitAt 1 infos 
+  info <- foldM (unif c) i is
+  return (c,info)
+
+
+tryInsert :: Ord a => (b -> b -> Err b) -> (b -> b) ->
+             BinTree a b -> (a,b) -> Err (BinTree a b)
+tryInsert unif indir tree z@(x, info) = case justLookupTree x tree of
+  Ok info0 -> do
+    info1 <- unif info info0
+    return $ updateTree (x,info1) tree 
+  _ -> return $ updateTree (x,indir info) tree
+
+{- ----
+case tree of
+ NT -> return $ BT (x, indir info) NT NT
+ BT c@(a,info0) left right 
+   | x < a  -> do
+       left' <- tryInsert unif indir left z    
+       return $ BT c left' right 
+   | x > a  -> do
+       right' <- tryInsert unif indir right z    
+       return $ BT c left right' 
+   | x == a -> do
+       info' <- unif info info0
+       return $ BT (x,info') left right
+-}
+
+--- addToMaybeList m c = maybe (return c) (\old -> return (c ++ old)) m
+
+unifAbsDefs :: Perh Term -> Perh Term -> Err (Perh Term)
+unifAbsDefs p1 p2 = case (p1,p2) of
+  (Nope, _)  -> return p2
+  (_, Nope)  -> return p1
+  (Yes (Eqs bs), Yes (Eqs ds)) -> return $ yes $ Eqs $ bs ++ ds --- order!
+  _ -> Bad "update conflict for definitions"
+
+unifConstrs :: Perh [Term] -> Perh [Term] -> Err (Perh [Term])
+unifConstrs p1 p2 = case (p1,p2) of
+  (Nope, _)  -> return p2
+  (_, Nope)  -> return p1
+  (Yes bs, Yes ds) -> return $ yes $ bs ++ ds
+  _ -> Bad "update conflict for constructors"