Founding the newly structured GF2.0 cvs archive.

14 files changed, 2455 insertions, 0 deletions

diff --git a/src/GF/Compile/CheckGrammar.hs b/src/GF/Compile/CheckGrammar.hs
new file mode 100644
index 000000000..544214cb9
--- /dev/null
+++ b/src/GF/Compile/CheckGrammar.hs
@@ -0,0 +1,665 @@
+module CheckGrammar where
+
+import Grammar
+import Ident
+import Modules
+import Refresh ----
+
+import TypeCheck
+
+import PrGrammar
+import Lookup
+import LookAbs
+import Macros
+import ReservedWords ----
+import PatternMatch
+
+import Operations
+import CheckM
+
+import List
+import Monad
+
+-- 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
+
+showCheckModule :: [SourceModule] -> SourceModule -> Err ([SourceModule],String)
+showCheckModule mos m = do
+    (st,(_,msg)) <- checkStart $ checkModule mos m
+    return (st, unlines $ reverse msg)
+
+-- checking is performed in dependency order of modules
+
+checkModule :: [SourceModule] -> SourceModule -> Check [SourceModule]
+checkModule ms (name,mod) = checkIn ("checking module" +++ prt name) $ case mod of
+
+  ModMod mo@(Module mt fs me ops js) -> case mt of
+    MTAbstract -> do
+      js' <- mapMTree (checkAbsInfo gr name) js
+      return $ (name, ModMod (Module mt fs me ops js')) : ms
+
+    MTResource -> do
+      js' <- mapMTree (checkResInfo gr) js
+      return $ (name, ModMod (Module mt fs me ops js')) : ms
+
+    MTConcrete a -> do
+      ModMod abs <- checkErr $ lookupModule gr a
+      checkCompleteGrammar abs mo
+      js' <- mapMTree (checkCncInfo gr name (a,abs)) js
+      return $ (name, ModMod (Module mt fs me ops js')) : ms
+  _ -> return $ (name,mod) : ms
+ where
+   gr  = MGrammar $ (name,mod):ms
+
+checkAbsInfo :: SourceGrammar -> Ident -> (Ident,Info) -> Check (Ident,Info)
+checkAbsInfo st m (c,info) = do
+---- checkReservedId c
+ case info of
+   AbsCat (Yes cont) _ -> mkCheck "category" $ 
+     checkContext st cont ---- also cstrs
+   AbsFun (Yes typ) (Yes d) -> mkCheck "function" $ 
+     checkTyp st typ ----- ++ 
+     ----- checkEquation st (m,c) d  ---- also if there's no def!
+   _ -> return (c,info)
+ where
+   mkCheck cat ss = case ss of
+     [] -> return (c,info)
+     ["[]"] -> return (c,info) ----
+     _  -> checkErr $ prtBad (unlines ss ++++ "in" +++ cat) c
+
+checkCompleteGrammar :: SourceAbs -> SourceCnc -> Check ()
+checkCompleteGrammar abs cnc = mapM_ checkWarn $
+  checkComplete [f | (f, AbsFun (Yes _) _) <- abs'] cnc'
+   where
+     abs' = tree2list $ jments abs
+     cnc' = mapTree fst $ jments cnc
+     checkComplete sought given = foldr ckOne [] sought
+       where
+         ckOne f = if isInBinTree f given 
+                      then id
+                      else (("Warning: no linearization of" +++ prt f):)
+
+-- General Principle: only Yes-values are checked. 
+-- A May-value has always been checked in its origin module.
+
+checkResInfo :: SourceGrammar -> (Ident,Info) -> Check (Ident,Info)
+checkResInfo gr (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')
+         (Nope, Yes de) -> do
+           (de',ty') <- infer de
+           return (Yes ty', Yes de')
+         _ -> return (pty, pde) --- other cases are uninteresting
+      return (c, ResOper pty' pde')
+
+    ResParam (Yes pcs) -> chIn "parameter type" $ do
+      mapM_ ((mapM_ (checkIfParType gr . snd)) . snd) pcs
+      return (c,info)
+
+    _ ->  return (c,info)
+ where
+   infer = inferLType gr
+   check = checkLType gr
+   chIn cat = checkIn ("Happened in" +++ cat +++ prt c +++ ":")
+   comp = computeLType gr
+
+checkCncInfo :: SourceGrammar -> Ident -> (Ident,SourceAbs) -> 
+                (Ident,Info) -> Check (Ident,Info)
+checkCncInfo gr m (a,abs) (c,info) = do
+  checkReservedId c
+  case info of
+
+    CncFun _ (Yes trm) mpr -> chIn "linearization of" $ do
+      typ        <- checkErr $ lookupFunTypeSrc gr a c
+      cat0       <- checkErr $ valCat typ
+      (cont,val) <- linTypeOfType gr m typ         -- creates arg vars
+      (trm',_)   <- check trm (mkFunType (map snd cont) val)  -- erases arg vars
+      checkPrintname gr mpr
+      cat        <- return $ snd cat0
+      return (c, CncFun (Just (cat,(cont,val))) (Yes trm') mpr)
+                                                   -- cat for cf, typ for pe
+
+    CncCat (Yes typ) mdef mpr -> chIn "linearization type of" $ do
+      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)
+
+    _ -> return (c,info)
+
+ where
+   env = gr
+   infer = inferLType gr
+   comp = computeLType gr 
+   check = checkLType gr
+   chIn cat = checkIn ("Happened in" +++ cat +++ prt c +++ ":")
+
+checkIfParType :: SourceGrammar -> Type -> Check ()
+checkIfParType st typ = checkCond ("Not parameter type" +++ prt typ) (isParType typ)
+  where
+   isParType ty = True ----
+{- case ty of
+     Cn typ -> case lookupConcrete st typ of
+       Ok (CncParType _ _ _) -> True
+       Ok (CncOper _ ty' _) -> isParType ty'
+       _ -> False
+     Q p t -> case lookupInPackage st (p,t) of
+       Ok (CncParType _ _ _) -> True
+       _ -> False
+     RecType r -> all (isParType . snd) r
+     _ -> False
+-}
+
+checkIfStrType :: SourceGrammar -> Type -> Check ()
+checkIfStrType st typ = case typ of
+  Table arg val -> do
+    checkIfParType st arg 
+    checkIfStrType st val
+  _ | typ == typeStr -> return ()
+  _ -> prtFail "not a string type" typ
+
+
+checkIfLinType :: SourceGrammar -> Type -> Check Type
+checkIfLinType st typ0 = do
+  typ <- computeLType st typ0
+  case typ of
+    RecType r -> do
+      let (lins,ihs) = partition (isLinLabel .fst) r
+      --- checkErr $ checkUnique $ map fst r
+      mapM_ checkInh ihs
+      mapM_ checkLin lins
+    _ -> prtFail "a linearization type must be a record type instead of" typ
+  return typ
+
+ where
+   checkInh (label,typ) = checkIfParType st typ
+   checkLin (label,typ) = 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
+
+    Q m ident -> 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) -> return $ RecType (rs ++ ss)
+        _ -> return $ ExtR r' s'
+
+    _ | 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 ()
+
+-- the underlying algorithms
+
+inferLType :: SourceGrammar -> Term -> Check (Term, Type)
+inferLType gr trm = case trm of
+
+   Q m ident -> checks [
+     termWith trm $ checkErr (lookupResType gr m ident)
+     ,
+     checkErr (lookupResDef gr m ident) >>= infer
+     ,
+     prtFail "cannot infer type of constant" trm
+     ]
+
+   QC m ident -> checks [
+     termWith trm $ checkErr (lookupResType gr m ident)
+     ,
+     checkErr (lookupResDef gr m ident) >>= infer
+     ,
+     prtFail "cannot infer type of canonical constant" trm
+     ]
+
+   Vr ident -> termWith trm $ checkLookup ident
+
+   App f a -> 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) 
+       _ -> prtFail ("function type expected for" +++ prt f +++ "instead of") 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
+     termWith (P t' i) $ checkErr $ case ty' of
+       RecType ts -> maybeErr ("unknown label" +++ show i +++ "in" +++ show ty') $ 
+                     lookup i ts
+       _ -> prtBad ("record type expected for" +++ prt t +++ "instead of") ty'
+
+   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]
+     if null pts' 
+       then prtFail "cannot infer table type of" trm
+       else do 
+         (arg,val) <- checks $ map (inferCase Nothing) pts'
+         check trm (Table arg val)
+
+   K s  -> do
+     if elem ' ' s
+        then checkWarn ("Warning: space in token \"" ++ s ++ 
+                        "\". Lexical analysis may fail.")
+        else return ()
+     return (trm, typeTok)
+
+   EInt i -> return (trm, typeInt)
+
+   Empty -> return (trm, typeTok)
+
+   C s1 s2 -> 
+     check2 (flip justCheck typeStr) C s1 s2 typeStr
+
+   Glue s1 s2 -> 
+     check2 (flip justCheck typeStr) Glue s1 s2 typeStr ---- typeTok
+
+   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'
+     case (rT', sT') of
+       (RecType rs, RecType ss) -> return (trm', RecType (rs ++ ss))
+       _ | rT' == typeType && sT' == typeType -> return (trm', typeType)
+       _ -> prtFail "records or record types expected in" trm
+
+   Sort _     -> 
+     termWith trm $ return typeType
+
+   Prod x a b -> do
+     a' <- justCheck a typeType
+     b' <- checkInContext [(x,a')] $ justCheck b typeType
+     return (Prod x a' b', typeType)
+
+   Table p t  -> do
+     p' <- justCheck p typeType --- check p partype! 
+     t' <- justCheck t typeType
+     return $ (Table p' t', typeType)
+
+   FV vs -> do
+     (ty,_) <- checks $ map infer vs
+---     checkIfComplexVariantType trm ty
+     check trm ty
+
+   _ -> prtFail "cannot infer lintype of" trm
+
+ where
+   env = gr
+   infer = inferLType env
+   comp = computeLType env 
+
+   check = checkLType env
+   
+   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
+     _ -> False
+
+   inferPatt p = case p of
+     PP q c ps -> checkErr $ lookupResType gr q c >>= valTypeCnc
+     _ -> infer (patt2term p) >>= return . snd
+
+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')
+        _ -> prtFail "product expected instead of" typ
+
+    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)
+      _ -> prtFail "table type expected for table instead of" 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
+           _ -> prtFail "invalid record type extension" trm
+       RecType rr -> checks [
+         do (r',ty) <- infer r
+            case ty of
+              RecType rr1 -> do
+                s' <- justCheck s (minusRecType rr rr1)
+                return $ (ExtR r' s', typ) 
+              _ -> prtFail "record type expected in extension of" r
+         ,
+         do (s',ty) <- infer s
+            case ty of
+              RecType rr2 -> do 
+                r' <- justCheck r (minusRecType rr rr2)
+                return $ (ExtR r' s', typ) 
+              _ -> prtFail "record type expected in extension with" s
+         ]
+       _ -> 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 -> 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)
+        _ -> prtFail "table type expected for applied table instead of" ty'
+
+    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
+
+   minusRecType rr rr1 = RecType [(l,v) | (l,v) <- rr, notElem l (map fst rr1)]
+
+   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 -> return [(x,typ)]
+  PP q c ps -> do
+    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]]
+        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'
+
+  _ -> return [] ----
+ where 
+   cnc = env
+
+-- 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
+  t' <- comp t 
+  u' <- comp u
+  if alpha [] t' u' 
+     then return t'
+     else raise ("type of" +++ prt trm +++ 
+                ": expected" +++ prt t' ++ ", inferred" +++ prt u')
+ where
+   alpha g t u = case (t,u) of  --- quick hack version of TC.eqVal
+     (Prod x a b, Prod y c d) -> alpha g a c && alpha ((x,y):g) b d
+
+     ---- this should be made in Rename
+     (Q  m a, Q  n b) | a == b -> elem m (allExtends env n) 
+                               || elem n (allExtends env m)
+     (QC m a, QC n b) | a == b -> elem m (allExtends env n) 
+                               || elem n (allExtends env m)
+
+     (RecType rs, RecType ts) -> and [alpha g a b && l == k --- too strong req
+                                        | ((l,a),(k,b)) <- zip rs ts]
+                                  || -- if fails, try subtyping:
+                                 all (\ (l,a) -> 
+                                      any (\ (k,b) -> alpha g a b && l == k) ts) rs
+
+     (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) 
+
+   sTypes = [typeStr, typeTok, typeString]
+   comp = computeLType env
+
+-- linearization types and defaults
+
+linTypeOfType :: SourceGrammar -> Ident -> Type -> Check (Context,Type)
+linTypeOfType cnc m typ = do
+  (cont,cat) <- checkErr $ typeSkeleton typ
+  val  <- lookLin cat
+  args <- mapM mkLinArg (zip [0..] cont)
+  return (args, val)
+ where
+   mkLinArg (i,(n,mc@(m,cat))) = do
+     val  <- lookLin mc
+     let vars = mkRecType varLabel $ replicate n typeStr
+	 symb = argIdent n cat i
+     rec <- checkErr $ errIn ("extending" +++ prt vars +++ "with" +++ prt val) $
+            plusRecType vars val
+     return (symb,rec)
+   lookLin (_,c) = checks [ --- rather: update with defLinType ?
+      checkErr (lookupLincat cnc m c) >>= computeLType cnc
+     ,return defLinType
+     ]
+
+{-
+-- check if a type is complex in variants
+-- Not so useful as one might think, since variants of a complex type
+-- can be created indirectly: f (variants {True,False})
+
+checkIfComplexVariantType :: Term -> Type -> Check ()
+checkIfComplexVariantType e t = case t of
+  Prod _ _ _ -> cs
+  Table _ _  -> cs
+  RecType (_:_:_) -> cs
+  _ -> return ()
+ where
+   cs = case e of
+      FV (_:_) -> checkWarn $ "Warning:" +++ prt e +++ "has complex type" +++ prt t
+      _ -> return ()
+
+-}
diff --git a/src/GF/Compile/Compile.hs b/src/GF/Compile/Compile.hs
new file mode 100644
index 000000000..1e49946a6
--- /dev/null
+++ b/src/GF/Compile/Compile.hs
@@ -0,0 +1,207 @@
+module Compile where
+
+import Grammar
+import Ident
+import Option
+import PrGrammar
+import Update
+import Lookup
+import Modules
+import ModDeps
+import ReadFiles
+import ShellState
+import MkResource
+
+-- the main compiler passes
+import GetGrammar
+import Rename
+import Refresh
+import CheckGrammar
+import Optimize
+import GrammarToCanon
+import Share
+
+import qualified CanonToGrammar as CG
+
+import qualified GFC
+import qualified MkGFC
+import GetGFC
+
+import Operations
+import UseIO
+import Arch
+
+import Monad
+
+-- in batch mode: write code in a file
+
+batchCompile f = liftM fst $ compileModule defOpts emptyShellState f
+  where
+    defOpts = options [beVerbose, emitCode] 
+batchCompileOpt f = liftM fst $ compileModule defOpts emptyShellState f
+  where
+    defOpts = options [beVerbose, emitCode, optimizeCanon] 
+
+batchCompileOld f = compileOld defOpts f
+  where
+    defOpts = options [beVerbose, emitCode] 
+
+-- compile with one module as starting point
+
+compileModule :: Options -> ShellState -> FilePath -> 
+                 IOE (GFC.CanonGrammar, (SourceGrammar,[(FilePath,ModTime)]))
+compileModule opts st file = do
+  let ps   = pathListOpts opts
+  ioeIO $ print ps ----
+  let putp = putPointE opts
+  let rfs  = readFiles st
+  files <- getAllFiles ps rfs file
+  ioeIO $ print files ----
+  let names = map (fileBody . justFileName) files
+  ioeIO $ print names ----
+  let env0 = compileEnvShSt st names
+  (_,sgr,cgr) <- foldM (compileOne opts) env0 files
+  t <- ioeIO getNowTime
+  return $ (reverseModules cgr,       -- to preserve dependency order
+            (reverseModules sgr, --- keepResModules opts sgr, --- keep all so far
+             [(f,t) | f <- files]))   -- pass on the time of creation
+
+compileEnvShSt :: ShellState -> [ModName] -> CompileEnv
+compileEnvShSt st fs = (0,sgr,cgr) where
+  cgr = MGrammar [m | m@(i,_) <- modules (canModules st), notInc i]
+  sgr = MGrammar [m | m@(i,_) <- modules (srcModules st), notIns i]
+  notInc i = notElem (prt i) $ map fileBody fs
+  notIns i = notElem (prt i) $ map fileBody fs
+
+pathListOpts :: Options -> [InitPath]
+pathListOpts opts = maybe [""] pFilePaths $ getOptVal opts pathList
+
+reverseModules (MGrammar ms) = MGrammar $ reverse ms
+
+keepResModules :: Options -> SourceGrammar -> SourceGrammar
+keepResModules opts gr = 
+  if oElem retainOpers opts 
+    then MGrammar $ reverse [(i,mi) | (i,mi) <- modules gr, isResourceModule mi]
+    else emptyMGrammar
+
+
+-- the environment
+
+type CompileEnv = (Int,SourceGrammar, GFC.CanonGrammar)
+
+emptyCompileEnv :: CompileEnv
+emptyCompileEnv = (0,emptyMGrammar,emptyMGrammar)
+
+extendCompileEnvInt (_,MGrammar ss, MGrammar cs) (k,sm,cm) = 
+  return (k,MGrammar (sm:ss), MGrammar (cm:cs)) --- reverse later
+
+extendCompileEnv (k,s,c) (sm,cm) = extendCompileEnvInt (k,s,c) (k,sm,cm)
+
+compileOne :: Options -> CompileEnv -> FullPath -> IOE CompileEnv
+compileOne opts env file = do
+
+  let putp = putPointE opts
+  let gf   = fileSuffix file
+  let path = justInitPath file
+  let name = fileBody file
+
+  case gf of
+    -- for canonical gf, just read the file and update environment
+    "gfc" -> do
+       cm <- putp ("+ reading" +++ file) $ getCanonModule file
+       sm <- ioeErr $ CG.canon2sourceModule cm
+       extendCompileEnv env (sm, cm)
+
+    -- for compiled resource, parse and organize, then update environment
+    "gfr" -> do
+       sm0  <- putp ("| parsing" +++ file) $ getSourceModule file
+       let mos = case env of (_,gr,_) -> modules gr
+       sm <- {- putp "creating indirections" $ -} ioeErr $ extendModule mos sm0
+       let gfc = gfcFile name 
+       cm <- putp ("+ reading" +++ gfc) $ getCanonModule gfc
+       extendCompileEnv env (sm,cm)
+
+    -- for gf source, do full compilation
+    _ -> do
+       sm0 <- putp ("- parsing" +++ file) $ getSourceModule file
+       (k',sm)  <- makeSourceModule opts env sm0
+       cm  <- putp "  generating code... " $ generateModuleCode opts path sm
+       extendCompileEnvInt env (k',sm,cm)
+
+-- dispatch reused resource at early stage
+
+makeSourceModule :: Options -> CompileEnv -> SourceModule -> IOE (Int,SourceModule)
+makeSourceModule opts env@(k,gr,can) mo@(i,mi) = case mi of
+
+  ModMod m -> case mtype m of
+    MTReuse c -> do
+      sm <- ioeErr $ makeReuse gr i (extends m) c
+      let mo2 = (i, ModMod sm)
+          mos = modules gr
+      putp "  type checking reused" $ ioeErr $ showCheckModule mos mo2
+      return $ (k,mo2)
+    _ -> compileSourceModule opts env mo
+ where
+   putp = putPointE opts
+
+compileSourceModule :: Options -> CompileEnv -> SourceModule -> 
+                       IOE (Int,SourceModule)
+compileSourceModule opts env@(k,gr,can) mo@(i,mi) = do
+
+  let putp = putPointE opts
+      mos  = modules gr
+
+  mo2:_ <- putp "  renaming " $ ioeErr $ renameModule mos mo
+
+  (mo3:_,warnings) <- putp "  type checking" $ ioeErr $ showCheckModule mos mo2
+  putStrE warnings
+
+  (k',mo3r:_) <- ioeErr $ refreshModule (k,mos) mo3
+
+  mo4:_ <- putp "  optimizing" $ ioeErr $ evalModule mos mo3r
+
+  return (k',mo4)
+
+generateModuleCode :: Options -> InitPath -> SourceModule -> IOE GFC.CanonModule
+generateModuleCode opts path minfo@(name,info) = do
+  let pname = prefixPathName path (prt name)
+  minfo0     <- ioeErr $ redModInfo minfo
+  minfo'     <- return $ if optim 
+                then shareModule fullOpt minfo0   -- parametrization and sharing
+                else shareModule basicOpt minfo0  -- sharing only
+
+  -- for resource, also emit gfr
+  case info of
+    ModMod m | mtype m == MTResource && emit && nomulti -> do
+      let (file,out) = (gfrFile pname, prGrammar (MGrammar [minfo]))
+      ioeIO $ writeFile file out >> putStr ("  wrote file" +++ file)
+    _ -> return ()
+  (file,out) <- do
+      code <- return $ MkGFC.prCanonModInfo minfo'
+      return (gfcFile pname, code)
+  if emit && nomulti 
+     then ioeIO $ writeFile file out >> putStr ("  wrote file" +++ file)
+     else return ()
+  return minfo'
+ where 
+   nomulti = not $ oElem makeMulti opts
+   emit  = oElem emitCode opts
+   optim = oElem optimizeCanon opts
+
+-- for old GF: sort into modules, write files, compile as usual
+
+compileOld :: Options -> FilePath -> IOE GFC.CanonGrammar
+compileOld opts file = do
+  let putp = putPointE opts
+  grammar1 <- putp ("- parsing old gf" +++ file) $ getOldGrammar file
+  files <- mapM writeNewGF $ modules grammar1
+  (_,_,grammar) <- foldM (compileOne opts) emptyCompileEnv files
+  return grammar
+
+writeNewGF :: SourceModule -> IOE FilePath
+writeNewGF m@(i,_) = do
+  let file = gfFile $ prt i
+  ioeIO $ writeFile file $ prGrammar (MGrammar [m])
+  ioeIO $ putStrLn $ "wrote file" +++ file
+  return file
+
diff --git a/src/GF/Compile/Extend.hs b/src/GF/Compile/Extend.hs
new file mode 100644
index 000000000..66a632445
--- /dev/null
+++ b/src/GF/Compile/Extend.hs
@@ -0,0 +1,77 @@
+module Extend where
+
+import Grammar
+import Ident
+import PrGrammar
+import Modules
+import Update
+import Macros
+import Operations
+
+import Monad
+
+-- AR 14/5/2003
+
+-- The top-level function $extendModInfo$
+-- extends a module symbol table by indirections to the module it extends
+
+extendModInfo :: Ident -> SourceModInfo -> SourceModInfo -> Err SourceModInfo
+extendModInfo name old new = case (old,new) of
+  (ModMod m0, ModMod (Module mt fs _ ops js)) -> do
+    testErr (mtype m0 == mt) ("illegal extension type at module" +++ show name)
+    js' <- extendMod name (jments m0) js
+    return $ ModMod (Module mt fs Nothing ops js)
+
+-- this is what happens when extending a module: new information is inserted,
+-- and the process is interrupted if unification fails
+
+extendMod :: Ident -> BinTree (Ident,Info) -> BinTree (Ident,Info) -> 
+             Err (BinTree (Ident,Info))
+extendMod name old new = 
+  foldM (tryInsert (extendAnyInfo name) (indirInfo name)) new $ tree2list old
+
+indirInfo :: Ident -> Info -> Info
+indirInfo n info = AnyInd b n' where 
+  (b,n') = case info of
+    ResValue _ -> (True,n)
+    ResParam _ -> (True,n)
+    AnyInd b k -> (b,k)
+    _ -> (False,n) ---- canonical in Abs
+
+{- ----
+case info of
+  AbsFun pty ptr -> AbsFun (perhIndir n pty) (perhIndir n ptr)
+  ---- find a suitable indirection for cat info!
+
+  ResOper pty ptr -> ResOper (perhIndir n pty) (perhIndir n ptr)
+  ResParam pp -> ResParam (perhIndir n pp) 
+  _ -> info
+
+  CncCat pty ptr ppr -> CncCat (perhIndir n pty) (perhIndir n ptr) (perhIndir n ppr)
+  CncFun m ptr   ppr -> CncFun m (perhIndir n ptr)                 (perhIndir n ppr)
+-}
+
+perhIndir :: Ident -> Perh a -> Perh a
+perhIndir n p = case p of
+  Yes _ -> May n
+  _ -> p
+
+extendAnyInfo :: Ident -> Info -> Info -> Err Info
+extendAnyInfo n i j = case (i,j) of
+  (AbsCat mc1 mf1, AbsCat mc2 mf2) -> 
+    liftM2 AbsCat (updatePerhaps n mc1 mc2) (updatePerhaps n mf1 mf2) --- add cstrs
+  (AbsFun mt1 md1, AbsFun mt2 md2) -> 
+    liftM2 AbsFun (updatePerhaps n mt1 mt2) (updatePerhaps n md1 md2) --- add defs
+
+  (ResParam mt1, ResParam mt2) -> liftM ResParam $ updatePerhaps n mt1 mt2
+  (ResValue mt1, ResValue mt2) -> liftM ResValue $ updatePerhaps n mt1 mt2
+  (ResOper mt1 m1, ResOper mt2 m2) -> 
+    liftM2 ResOper (updatePerhaps n mt1 mt2) (updatePerhaps n m1 m2)
+
+  (CncCat mc1 mf1 mp1, CncCat mc2 mf2 mp2) -> 
+    liftM3 CncCat (updatePerhaps n mc1 mc2) 
+                  (updatePerhaps n mf1 mf2) (updatePerhaps n mp1 mp2)
+  (CncFun m mt1 md1, CncFun _ mt2 md2) -> 
+    liftM2 (CncFun m) (updatePerhaps n mt1 mt2) (updatePerhaps n md1 md2)
+
+  _ -> Bad $ "cannot unify information for" +++ show n
diff --git a/src/GF/Compile/GetGrammar.hs b/src/GF/Compile/GetGrammar.hs
new file mode 100644
index 000000000..fb3fbf5ad
--- /dev/null
+++ b/src/GF/Compile/GetGrammar.hs
@@ -0,0 +1,71 @@
+module GetGrammar where
+
+import Operations
+import qualified ErrM as E ----
+
+import UseIO
+import Grammar
+import Modules
+import PrGrammar
+import qualified AbsGF as A
+import SourceToGrammar
+---- import Macros
+---- import Rename
+import Option
+--- import Custom
+import ParGF
+
+import ReadFiles ----
+
+import List (nub)
+import Monad (foldM)
+
+-- this module builds the internal GF grammar that is sent to the type checker
+
+getSourceModule :: FilePath -> IOE SourceModule
+getSourceModule file = do
+  string    <- readFileIOE file
+  let tokens = myLexer string
+  mo1  <- ioeErr $ err2err $ pModDef tokens
+  ioeErr $ transModDef mo1
+
+
+-- for old GF format with includes
+
+getOldGrammar :: FilePath -> IOE SourceGrammar
+getOldGrammar file = do
+  defs <- parseOldGrammarFiles file
+  let g = A.OldGr A.NoIncl defs
+  ioeErr $ transOldGrammar g file
+
+parseOldGrammarFiles :: FilePath -> IOE [A.TopDef]
+parseOldGrammarFiles file = do
+   putStrE $ "reading grammar of old format" +++ file
+   (_, g) <- getImports "" ([],[]) file
+   return g  -- now we can throw away includes
+  where 
+   getImports oldInitPath (oldImps, oldG) f = do
+     (path,s) <- readFileLibraryIOE oldInitPath f
+     if not (elem path oldImps) 
+       then do
+         (imps,g) <- parseOldGrammar path
+         foldM (getImports (initFilePath path)) (path : oldImps, g ++ oldG) imps
+       else 
+         return (oldImps, oldG)
+
+parseOldGrammar :: FilePath -> IOE ([FilePath],[A.TopDef])
+parseOldGrammar file = do
+  putStrE $ "reading old file" +++ file
+  s <- ioeIO $ readFileIf file
+  A.OldGr incl topdefs <- ioeErr $ err2err $ pOldGrammar $ myLexer $ fixNewlines s
+  includes <- ioeErr $ transInclude incl
+  return (includes, topdefs)
+
+----
+
+err2err :: E.Err a -> Err a
+err2err (E.Ok v) = Ok v
+err2err (E.Bad s) = Bad s
+
+ioeEErr = ioeErr . err2err
+
diff --git a/src/GF/Compile/GrammarToCanon.hs b/src/GF/Compile/GrammarToCanon.hs
new file mode 100644
index 000000000..d5977b510
--- /dev/null
+++ b/src/GF/Compile/GrammarToCanon.hs
@@ -0,0 +1,224 @@
+module GrammarToCanon where
+
+import Operations
+import Zipper
+import Option
+import Grammar
+import Ident
+import PrGrammar
+import Modules
+import Macros
+import qualified AbsGFC as G
+import qualified GFC as C
+import MkGFC
+---- import Alias
+import qualified PrintGFC as P
+
+import Monad
+
+-- compilation of optimized grammars to canonical GF. AR 5/10/2001 -- 12/5/2003
+
+-- This is the top-level function printing a gfc file
+
+showGFC :: SourceGrammar -> String
+showGFC = err id id . liftM (P.printTree . grammar2canon) . redGrammar
+
+-- any grammar, first trying without dependent types
+
+-- abstract syntax without dependent types
+
+redGrammar :: SourceGrammar -> Err C.CanonGrammar
+redGrammar (MGrammar gr) = liftM MGrammar $ mapM redModInfo gr
+
+redModInfo :: (Ident, SourceModInfo) -> Err (Ident, C.CanonModInfo)
+redModInfo (c,info) = do
+  c'    <- redIdent c
+  info' <- case info of
+    ModMod m -> do
+      (e,os) <- redExtOpen m
+      flags <- mapM redFlag $ flags m 
+      (a,mt) <- case mtype m of
+         MTConcrete a -> do
+           a' <- redIdent a
+           return (a', MTConcrete a') 
+         MTAbstract -> return (c',MTAbstract) --- c' not needed
+         MTResource -> return (c',MTResource) --- c' not needed
+      defss <- mapM (redInfo a) $ tree2list $ jments m
+      defs  <- return $ sorted2tree $ concat defss  -- sorted, but reduced
+      return $ ModMod $ Module mt flags e os defs
+  return (c',info')
+ where
+   redExtOpen m = do
+     e' <- case extends m of
+       Just e -> liftM Just $ redIdent e
+       _ -> return Nothing
+     os' <- mapM (\ (OQualif _ i) -> liftM OSimple (redIdent i)) $ opens m
+     return (e',os')
+
+redInfo :: Ident -> (Ident,Info) -> Err [(Ident,C.Info)]
+redInfo am (c,info) = errIn ("translating definition of" +++ prt c) $ do
+  c' <- redIdent c 
+  case info of
+    AbsCat (Yes cont) pfs -> do
+      returns c' $ C.AbsCat cont [] ---- constrs
+    AbsFun (Yes typ) pdf -> do
+      returns c' $ C.AbsFun typ (Eqs []) ---- df
+
+    ResParam (Yes ps) -> do
+      ps' <- mapM redParam ps
+      returns c' $ C.ResPar ps'
+
+    CncCat pty ptr ppr -> case (pty,ptr) of
+      (Yes ty, Yes (Abs _ t)) -> do
+        ty'  <- redCType ty
+        trm' <- redCTerm t
+        ppr' <- return $ G.FV []  ---- redCTerm 
+        return [(c', C.CncCat ty' trm' ppr')]
+      _ -> prtBad "cannot reduce rule for" c
+      
+    CncFun mt ptr ppr -> case (mt,ptr) of
+      (Just (cat,_), Yes trm) -> do
+        cat' <- redIdent cat
+        (xx,body,_) <- termForm trm
+        xx'   <- mapM redArgvar xx
+        body' <- errIn (prt body) $ redCTerm body ---- debug
+        ppr'  <- return $ G.FV []  ---- redCTerm 
+        return [(c',C.CncFun (G.CIQ am cat') xx' body' ppr')]
+      _ -> prtBad ("cannot reduce rule" +++ show info +++ "for") c ---- debug
+
+    AnyInd s b -> do
+      b' <- redIdent b
+      returns c' $ C.AnyInd s b'
+
+    _ -> return [] --- retain some operations
+ where
+   returns f i = return [(f,i)]
+
+redQIdent :: QIdent -> Err G.CIdent
+redQIdent (m,c) = return $ G.CIQ m c
+
+redIdent :: Ident -> Err Ident
+redIdent x 
+  | isWildIdent x = return $ identC "h_" --- needed in declarations
+  | otherwise = return $ identC $ prt x ---
+
+redFlag :: Option -> Err G.Flag
+redFlag (Opt (f,[x])) = return $ G.Flg (identC f) (identC x)
+redFlag o = Bad $ "cannot reduce option" +++ prOpt o
+
+redDecl :: Decl -> Err G.Decl
+redDecl (x,a) = liftM2 G.Decl (redIdent x) (redType a)
+
+redType :: Type -> Err G.Exp
+redType = redTerm
+
+redTerm :: Type -> Err G.Exp
+redTerm t = return $ rtExp t
+
+-- resource
+
+redParam :: Param -> Err G.ParDef
+redParam (c,cont) = do
+  c'    <- redIdent c
+  cont' <- mapM (redCType . snd) cont
+  return $ G.ParD c' cont'
+
+redArgvar :: Ident -> Err G.ArgVar
+redArgvar x = case x of
+  IA (x,i)     -> return $ G.A  (identC x) (toInteger i)
+  IAV (x,b,i) -> return $ G.AB (identC x) (toInteger b) (toInteger i)
+  _ -> Bad $ "cannot reduce" +++ show x +++ "as argument variable"
+
+redLindef :: Term -> Err G.Term
+redLindef t = case t of
+  Abs x b -> redCTerm b ---
+  _ -> redCTerm t
+
+redCType :: Type -> Err G.CType
+redCType t = case t of
+  RecType lbs -> do
+    let (ls,ts) = unzip lbs
+        ls' = map redLabel ls
+    ts' <- mapM redCType ts
+    return $ G.RecType $ map (uncurry G.Lbg) $ zip ls' ts'
+  Table p v  -> liftM2 G.Table (redCType p) (redCType v)
+  Q m c    -> liftM G.Cn $ redQIdent (m,c)
+  QC m c   -> liftM G.Cn $ redQIdent (m,c)
+  Sort "Str" -> return $ G.TStr
+  _ -> prtBad "cannot reduce to canonical the type" t
+
+redCTerm :: Term -> Err G.Term
+redCTerm t = case t of
+  Vr x -> liftM G.Arg $ redArgvar x
+  App _ _ -> do  -- only constructor applications can remain
+    (_,c,xx) <- termForm t
+    xx' <- mapM redCTerm xx
+    case c of
+      QC p c -> liftM2 G.Con (redQIdent (p,c)) (return xx')
+      _ -> prtBad "expected constructor head instead of" c
+  Q p c  -> liftM G.I (redQIdent (p,c))
+  QC p c -> liftM2 G.Con (redQIdent (p,c)) (return [])
+  R rs     -> do
+    let (ls,tts) = unzip rs
+        ls' = map redLabel ls
+    ts <- mapM (redCTerm . snd) tts
+    return $ G.R $ map (uncurry G.Ass) $ zip ls' ts
+  P tr l -> do
+    tr' <- redCTerm tr
+    return $ G.P tr' (redLabel l)
+  T i cs     -> do
+    ty  <- getTableType i
+    ty' <- redCType ty
+    let (ps,ts) = unzip cs
+    ps' <- mapM redPatt ps
+    ts' <- mapM redCTerm ts
+    return $ G.T ty' $ map (uncurry G.Cas) $ zip (map singleton ps') ts'
+  S u v -> liftM2 G.S (redCTerm u) (redCTerm v)
+  K s   -> return $ G.K (G.KS s)
+  C u v -> liftM2 G.C (redCTerm u) (redCTerm v)
+  FV ts -> liftM G.FV $ mapM redCTerm ts
+---  Ready ss -> return $ G.Ready [redStr ss] --- obsolete
+
+  Alts (d,vs) -> do ---
+    d'  <- redCTermTok d
+    vs' <- mapM redVariant vs
+    return $ G.K $ G.KP d' vs'
+
+  Empty -> return $ G.E
+
+---  Strs ss -> return $ G.Strs [s | K s <- ss] ---
+
+---- Glue obsolete in canon, should not occur here
+  Glue x y -> redCTerm (C x y)
+
+  _ -> Bad ("cannot reduce term" +++ prt t)
+
+redPatt :: Patt -> Err G.Patt
+redPatt p = case p of
+  PP m c ps -> liftM2 G.PC (redQIdent (m,c)) (mapM redPatt ps) 
+  PR rs -> do
+    let (ls,tts) = unzip rs
+        ls' = map redLabel ls
+    ts <- mapM redPatt tts
+    return $ G.PR $  map (uncurry G.PAss) $ zip ls' ts
+  PT _ q -> redPatt q
+  _ -> prtBad "cannot reduce pattern" p
+
+redLabel :: Label -> G.Label
+redLabel (LIdent s) = G.L $ identC s
+redLabel (LVar i)   = G.LV $ toInteger i
+
+redVariant :: (Term, Term) -> Err G.Variant
+redVariant (v,c) = do
+  v' <- redCTermTok v
+  c' <- redCTermTok c
+  return $ G.Var v' c'
+
+redCTermTok :: Term -> Err [String]
+redCTermTok t = case t of
+  K s   -> return [s]
+  Empty -> return []
+  C a b -> liftM2 (++) (redCTermTok a) (redCTermTok b)
+  Strs ss -> return [s | K s <- ss] ---
+  _ -> prtBad "cannot get strings from term" t
+
diff --git a/src/GF/Compile/MkResource.hs b/src/GF/Compile/MkResource.hs
new file mode 100644
index 000000000..8b3a01793
--- /dev/null
+++ b/src/GF/Compile/MkResource.hs
@@ -0,0 +1,75 @@
+module MkResource where
+
+import Grammar
+import Ident
+import Modules
+import Macros
+import PrGrammar
+
+import Operations
+
+import Monad
+
+-- extracting resource r from abstract + concrete syntax
+-- AR 21/8/2002 -- 22/6/2003 for GF with modules
+
+makeReuse :: SourceGrammar -> Ident -> Maybe Ident -> Ident -> Err SourceRes
+makeReuse gr r me c = do
+  mc <- lookupModule gr c
+
+  flags <- return [] --- no flags are passed: they would not make sense
+
+  (ops,jms) <- case mc of 
+    ModMod m -> case mtype m of
+      MTConcrete a -> do
+        ma <- lookupModule gr a
+        jmsA <- case ma of 
+           ModMod m' -> return $ jments m'
+           _ -> prtBad "expected abstract to be the type of" a
+        liftM ((,) (opens m)) $ mkResDefs r a me (extends m) jmsA (jments m)
+      _ -> prtBad "expected concrete to be the type of" c
+    _ -> prtBad "expected concrete to be the type of" c
+
+  return $ Module MTResource flags me ops jms
+
+mkResDefs :: Ident -> Ident -> Maybe Ident -> Maybe Ident -> 
+             BinTree (Ident,Info) -> BinTree (Ident,Info) -> 
+             Err (BinTree (Ident,Info))
+mkResDefs r a mext maext abs cnc = mapMTree mkOne abs where
+
+  mkOne (f,info) = case info of
+      AbsCat _ _ -> do
+        typ <- err (const (return defLinType)) return $ look f
+        return (f, ResOper (Yes typeType) (Yes typ))
+      AbsFun (Yes typ0) _ -> do
+        trm <- look f
+        typ <- redirTyp typ0 --- if isHardType typ0 then compute typ0 else ...
+        return (f, ResOper (Yes typ) (Yes trm))
+      AnyInd b _ -> case mext of
+        Just ext -> return (f,AnyInd b ext)
+        _ -> prtBad "no indirection possible in" r
+
+  look f = do
+     info <- lookupTree prt f cnc
+     case info of
+       CncCat (Yes ty) _ _ -> return ty
+       CncCat _ _ _        -> return defLinType
+       CncFun _ (Yes tr) _ -> return tr
+       _ -> prtBad "not enough information to reuse" f
+
+  -- type constant qualifications changed from abstract to resource
+  redirTyp ty = case ty of
+    Q n c | n == a -> return $ Q r c
+    Q n c | Just n == maext -> case mext of
+      Just ext -> return $ Q ext c
+      _ -> prtBad "no indirection of type possible in" r
+    _ -> composOp redirTyp ty
+
+{-
+-- for nicer printing of type signatures: preserves synonyms if not HO/dep type
+
+isHardType t = case t of
+  Prod x a b -> not (isWildIdent x) || isHardType a || isHardType b
+  App _ _    -> True
+  _          -> False  
+-}
diff --git a/src/GF/Compile/ModDeps.hs b/src/GF/Compile/ModDeps.hs
new file mode 100644
index 000000000..2aa042a95
--- /dev/null
+++ b/src/GF/Compile/ModDeps.hs
@@ -0,0 +1,88 @@
+module ModDeps where
+
+import Grammar
+import Ident
+import Option
+import PrGrammar
+import Update
+import Lookup
+import Modules
+
+import Operations
+
+import Monad
+
+-- AR 13/5/2003
+
+-- 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]
+
+ where
+
+  test ms = testErr (all (`notElem` ns) ms)
+                    ("import names clashing with module names among" +++ 
+                       unwords (map prt ms))
+
+-- to decide what modules immediately depend on what, and check if the
+-- dependencies are appropriate
+
+type Dependencies = [(IdentM Ident,[IdentM Ident])]
+
+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 for-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 <- case es of
+      Just e -> liftM singleton $ lookupModuleType gr e
+      _ -> return []
+    testErr (all (compatMType ety) ests) "inappropriate extension module type" 
+    osts <- mapM (lookupModuleType gr . openedModule) os
+    testErr (all (==oty) osts) "inappropriate open module type"
+    let ab = case it of
+               IdentM _ (MTConcrete a) -> [IdentM a MTAbstract]
+               _ -> [] ---- 
+    return (it, ab ++
+                [IdentM e ety | Just e <- [es]] ++ 
+                [IdentM (openedModule o) oty | o <- os])
+
+  -- check for superficial compatibility, not submodule relation etc
+  compatMType mt0 mt = case (mt0,mt) of
+    (MTConcrete _, MTConcrete _) -> True
+    (MTResourceImpl _, MTResourceImpl _) -> True
+    (MTReuse _, MTReuse _) -> True
+    ---- some more
+    _ -> mt0 == mt
+
+  gr = MGrammar ms --- hack
diff --git a/src/GF/Compile/Optimize.hs b/src/GF/Compile/Optimize.hs
new file mode 100644
index 000000000..c901c3911
--- /dev/null
+++ b/src/GF/Compile/Optimize.hs
@@ -0,0 +1,171 @@
+module Optimize where
+
+import Grammar
+import Ident
+import Modules
+import PrGrammar
+import Macros
+import Lookup
+import Refresh
+import Compute
+import CheckGrammar
+import Update
+
+import Operations
+import CheckM
+
+import Monad
+import List
+
+-- partial evaluation of concrete syntax. AR 6/2001 -- 16/5/2003
+{-
+evalGrammar :: SourceGrammar -> Err SourceGrammar
+evalGrammar gr = do
+  gr2 <- refreshGrammar gr
+  mos <- foldM evalModule [] $ modules gr2
+  return $ MGrammar $ reverse mos 
+-}
+evalModule :: [(Ident,SourceModInfo)] -> (Ident,SourceModInfo) -> 
+               Err [(Ident,SourceModInfo)]
+evalModule ms mo@(name,mod) = case mod of
+
+  ModMod (Module mt fs me ops js) -> case mt of
+    MTResource -> do
+      let deps = allOperDependencies name js
+      ids <- topoSortOpers deps
+      MGrammar (mod' : _) <- foldM evalOp gr ids
+      return $ mod' : ms
+    MTConcrete a -> do
+      js' <- mapMTree (evalCncInfo gr0 name a) js
+      return $ (name, ModMod (Module mt fs me ops js')) : ms
+
+    _ -> return $ (name,mod):ms
+ where
+   gr0 = MGrammar $ ms
+   gr  = MGrammar $ (name,mod) : ms
+
+   evalOp g@(MGrammar ((_, ModMod m) : _)) i = do
+     info  <- lookupTree prt i $ jments m
+     info' <- evalResInfo 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 :: SourceGrammar -> (Ident,Info) -> Err Info
+evalResInfo gr (c,info) = case info of
+
+  ResOper pty pde -> eIn "operation" $ do
+    pde' <- case pde of
+       Yes de -> liftM yes $ comp de
+       _ -> return pde
+    return $ ResOper pty pde'
+
+  _ ->  return info
+ where
+   comp = computeConcrete gr
+   eIn cat = errIn ("Error optimizing" +++ cat +++ prt c +++ ":")
+
+
+evalCncInfo :: 
+  SourceGrammar -> Ident -> Ident -> (Ident,Info) -> Err (Ident,Info)
+evalCncInfo gr cnc abs (c,info) = case info of
+
+  CncCat ptyp pde ppr -> do
+
+    pde' <- case (ptyp,pde) of
+      (Yes typ, Yes de) -> 
+        liftM yes $ pEval ([(strVar, typeStr)], typ) de
+      (Yes typ, Nope)   -> 
+        liftM yes $ mkLinDefault gr typ >>= pEval ([(strVar, typeStr)],typ)
+      (May b, Nope) ->
+        return $ May b
+      _ -> return pde   -- indirection
+
+    ppr' <- return ppr ----
+
+    return (c, CncCat ptyp pde' ppr')
+
+  CncFun (mt@(Just (_,ty))) pde ppr -> eIn ("linearization in type" +++  
+                                             show ty +++ "of") $ do
+    pde' <- case pde of
+      Yes de -> do
+        liftM yes $ pEval ty de
+      _ -> return pde
+    ppr' <- case ppr of
+      Yes pr -> liftM yes $ comp pr
+      _ -> return ppr  
+    return $ (c, CncFun mt pde' ppr') -- only cat in type actually needed
+
+  _ ->  return (c,info)
+ where
+   comp = computeConcrete gr
+   pEval = partEval gr
+   eIn cat = errIn ("Error optimizing" +++ cat +++ prt c +++ ":")
+
+-- the main function for compiling linearizations
+
+partEval :: SourceGrammar -> (Context,Type) -> Term -> Err Term
+partEval gr (context, val) trm = do
+  let vars  = map fst context
+      args  = map Vr vars
+      subst = [(v, Vr v) | v <- vars]
+      trm1  = mkApp trm args
+  trm2 <- etaExpand val trm1 
+  trm3 <- comp subst trm2
+  return $ mkAbs vars trm3
+
+ where 
+
+   comp g t = {- refreshTerm t >>= -} computeTerm gr g t
+
+   etaExpand val t = recordExpand val t   --- >>= caseEx  -- done by comp
+
+-- 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
+
+allOperDependencies :: Ident -> BinTree (Ident,Info) -> [(Ident,[Ident])]
+allOperDependencies m b = 
+  [(f, nub (opty pty ++ opty pt)) | (f, ResOper pty pt) <- tree2list b]
+  where
+    opersIn t = case t of
+      Q n c | n == m -> [c]
+      _ -> collectOp opersIn t
+    opty (Yes ty) = opersIn ty
+    opty _ = []
+
+topoSortOpers :: [(Ident,[Ident])] -> Err [Ident]
+topoSortOpers st = do
+  let eops = topoTest st
+  either return (\ops -> Bad ("circular operations" +++ unwords (map prt (head ops)))) eops
+
+mkLinDefault :: SourceGrammar -> Type -> Err Term
+mkLinDefault gr typ = do
+  case unComputed typ of
+    RecType lts -> mapPairsM mkDefField lts >>= (return . Abs strVar . R . mkAssign)
+    _ -> prtBad "linearization type must be a record type, not" typ
+ where
+   mkDefField typ = case unComputed typ of
+     Table p t  -> do
+       t' <- mkDefField t
+       let T _ cs = mkWildCases t'
+       return $ T (TWild p) cs 
+     Sort "Str" -> return $ Vr strVar
+     QC q p     -> lookupFirstTag gr q p
+     RecType r  -> do
+       let (ls,ts) = unzip r
+       ts' <- mapM mkDefField ts
+       return $ R $ [assign l t | (l,t) <- zip ls ts']
+     _ -> prtBad "linearization type field cannot be" typ
+
diff --git a/src/GF/Compile/PGrammar.hs b/src/GF/Compile/PGrammar.hs
new file mode 100644
index 000000000..06d9fc72e
--- /dev/null
+++ b/src/GF/Compile/PGrammar.hs
@@ -0,0 +1,58 @@
+module PGrammar where
+
+---import LexGF
+import ParGF
+import SourceToGrammar
+import Grammar
+import Ident
+import qualified AbsGFC as A
+import qualified GFC as G
+import GetGrammar
+import Macros
+
+import Operations
+
+pTerm :: String -> Err Term
+pTerm s = do
+  e <- err2err $ pExp $ myLexer s
+  transExp e
+
+pTrm :: String -> Term
+pTrm = errVal (vr (zIdent "x")) . pTerm ---
+
+pTrms :: String -> [Term]
+pTrms = map pTrm . sep [] where
+  sep t cs = case cs of
+    ',' : cs2 -> reverse t : sep [] cs2
+    c   : cs2 -> sep (c:t) cs2
+    _         -> [reverse t]
+
+pTrm' :: String -> [Term]
+pTrm' = err (const []) singleton . pTerm
+
+pMeta :: String -> Integer
+pMeta _ = 0 ---
+
+pzIdent :: String -> Ident
+pzIdent = zIdent
+
+{-
+string2formsAndTerm :: String -> ([Term],Term)
+string2formsAndTerm s = case s of
+    '[':_:_ -> case span (/=']') s of  
+      (x,_:y) -> (pTrms (tail x), pTrm y)
+      _ -> ([],pTrm s)
+    _ -> ([], pTrm s)
+
+string2ident :: String -> Err Ident
+string2ident s = return $ case s of
+  c:'_':i -> identV (readIntArg i,[c]) ---
+  _ -> zIdent s
+
+-- reads the Haskell datatype
+readGrammar :: String -> Err GrammarST
+readGrammar s =  case [x | (x,t) <- reads s, ("","") <- lex t] of
+  [x] -> return x
+  []  -> Bad "no parse of Grammar"
+  _   -> Bad "ambiguous parse of Grammar"
+-}
diff --git a/src/GF/Compile/PrOld.hs b/src/GF/Compile/PrOld.hs
new file mode 100644
index 000000000..acce0ab67
--- /dev/null
+++ b/src/GF/Compile/PrOld.hs
@@ -0,0 +1,69 @@
+module PrOld where
+
+import PrGrammar
+import CanonToGrammar
+import qualified GFC
+import Grammar
+import Ident
+import Macros
+import Modules
+import qualified PrintGF as P
+import GrammarToSource
+
+import List
+import Operations
+import UseIO
+
+-- a hack to print gf2 into gf1 readable files
+-- Works only for canonical grammars, printed into GFC. Otherwise we would have
+-- problems with qualified names.
+--- printnames are not preserved, nor are lindefs
+
+printGrammarOld :: GFC.CanonGrammar -> String
+printGrammarOld gr = err id id $ do
+  as0 <- mapM canon2sourceModule [im | im@(_,ModMod m) <- modules gr, isModAbs m]
+  cs0 <- mapM canon2sourceModule 
+           [im | im@(_,ModMod m) <- modules gr, isModCnc m || isModRes m]
+  as1 <- return $ concatMap stripInfo $ concatMap (tree2list . js . snd) as0
+  cs1 <- return $ concatMap stripInfo $ concatMap (tree2list . js . snd) cs0
+  return $ unlines $ map prj $ srt as1 ++ srt cs1
+ where
+   js (ModMod m) = jments m
+   srt = sortBy (\ (i,_) (j,_) -> compare i j)
+   prj ii = P.printTree $ trAnyDef ii
+
+stripInfo :: (Ident,Info) -> [(Ident,Info)]
+stripInfo (c,i) = case i of
+  AbsCat   (Yes co) (Yes fs) -> rc $ AbsCat (Yes (stripContext co)) nope
+  AbsFun   (Yes ty) (Yes tr) -> rc $ AbsFun (Yes (stripTerm ty)) (Yes(stripTerm tr))
+  AbsFun   (Yes ty) _ -> rc $ AbsFun (Yes (stripTerm ty)) nope
+  ResParam (Yes ps)       -> rc $ ResParam (Yes [(c,stripContext co) | (c,co)<- ps])
+  CncCat   (Yes ty) _ _ -> rc $
+    CncCat (Yes (stripTerm ty)) nope nope
+  CncFun   _ (Yes tr) _ -> rc $ CncFun Nothing (Yes (stripTerm tr)) nope
+  _ -> []
+ where
+   rc j = [(c,j)]
+
+stripContext co = [(x, stripTerm t) | (x,t) <- co]
+
+stripTerm t = case t of
+  Q _ c -> Vr c
+  QC _ c -> Vr c
+  T ti cs -> T ti' [(stripPattern p, stripTerm c) | (p,c) <- cs] where
+               ti' = case ti of
+                  TTyped ty -> TTyped $ stripTerm ty
+                  TComp ty -> TComp $ stripTerm ty
+                  TWild ty -> TWild $ stripTerm ty
+                  _ -> ti
+  _ -> composSafeOp stripTerm t
+
+stripPattern p = case p of
+  PC c [] -> PV c
+  PP _ c [] -> PV c
+  PC c ps -> PC c (map stripPattern ps)
+  PP _ c ps -> PC c (map stripPattern ps)
+  PR lps -> PR [(l, stripPattern p) | (l,p) <- lps]
+  PT t p -> PT (stripTerm t) (stripPattern p)
+  _ -> p
+
diff --git a/src/GF/Compile/RemoveLiT.hs b/src/GF/Compile/RemoveLiT.hs
new file mode 100644
index 000000000..0e45be8c0
--- /dev/null
+++ b/src/GF/Compile/RemoveLiT.hs
@@ -0,0 +1,51 @@
+module RemoveLiT (removeLiT) where
+
+import Grammar
+import Ident
+import Modules
+import Macros
+import Lookup
+
+import Operations
+
+import Monad
+
+-- 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 procedule is uncertain, if T contains another Lin.
+
+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 (Module mt fs me ops js) -> do
+    js1 <- mapMTree (remlResInfo gr) js
+    let mod2 = ModMod $ Module mt fs me ops 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
+     _ -> zIdent "CNC" 
diff --git a/src/GF/Compile/Rename.hs b/src/GF/Compile/Rename.hs
new file mode 100644
index 000000000..1e45b5fcc
--- /dev/null
+++ b/src/GF/Compile/Rename.hs
@@ -0,0 +1,263 @@
+module Rename where
+
+import Grammar
+import Modules
+import Ident
+import Macros
+import PrGrammar
+import Lookup
+import Extend
+import Operations
+
+import Monad
+
+-- 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'.
+
+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 (Module mt fs me ops js) -> do
+    (_,mod1@(ModMod m)) <- extendModule ms (name,mod)
+    let js1 = jments m
+    status <- buildStatus (MGrammar ms) name mod1
+    js2    <- mapMTree (renameInfo status) js1
+    let mod2 = ModMod $ Module mt fs me (map forceQualif ops) js2
+    return $ (name,mod2) : ms
+
+extendModule :: [SourceModule] -> SourceModule -> Err SourceModule
+extendModule ms (name,mod) = case mod of
+  ModMod (Module mt fs me ops js0) -> do
+    js  <- case mt of
+{- --- building the {s : Str} lincat
+      MTConcrete a -> do
+        ModMod ma <- lookupModule (MGrammar ms) a
+        let cats = [c | (c,AbsCat _ _) <- tree2list $ jments ma]
+            jscs = [(c,CncCat (yes defLinType) nope nope) | c <- cats]
+        return $ updatesTreeNondestr jscs js0
+-}
+      _ -> return js0
+    js1 <- case me of
+      Just n -> do
+        m0 <- case lookup n ms of
+          Just (ModMod m) -> do
+            testErr (sameMType (mtype m) mt) 
+                    ("illegal extension type to module" +++ prt name)
+            return m
+          _ -> Bad $ "cannot find extended module" +++ prt n
+        extendMod n (jments m0) js
+      _ -> return js
+    return $ (name,ModMod (Module mt fs Nothing ops js1))
+
+
+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 = case t of
+  Vr c -> do
+    f <- lookupTreeMany prt opens c
+    return $ f c
+  Cn c -> do
+    f <- lookupTreeMany prt opens c
+    return $ f c
+  Q m' c -> do
+    m <- lookupErr m' qualifs
+    f <- lookupTree prt c m
+    return $ f c
+  QC m' c -> do
+    m <- lookupErr m' qualifs
+    f <- lookupTree prt c m
+    return $ f c
+  _ -> return t
+ where
+   opens   = act : [st  | (OSimple _,st) <- imps]
+   qualifs = [  (m, st) | (OQualif m _, st) <- imps]
+
+--- 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 (Con g)) | g == c -> 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 ops  = opens m
+    mods <- mapM (lookupModule gr . openedModule) ops
+    let sts = map modInfo2status $ zip ops mods    
+    return $ if isModCnc m
+      then (NT, sts) -- the module itself does not define any names
+      else (mo',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 = case i of
+  ModMod m -> mapTree (info2status (Just c)) (jments m)   -- qualify internal
+---  ModMod m -> mapTree (resInfo2status Nothing) (jments m)
+-- change Lookup.qualifAnnot if you change this
+
+forceQualif o = case o of
+  OSimple i   -> OQualif i i
+  OQualif _ i -> OQualif i i
+  
+renameInfo :: Status -> (Ident,Info) -> Err (Ident,Info)
+renameInfo status (i,info) = errIn ("renaming definition of" +++ prt i) $ 
+                                liftM ((,) i) $ case info of
+  AbsCat pco pfs -> liftM2 AbsCat (renPerh (renameContext status) pco)
+                                  (return pfs) ----
+  AbsFun pty ptr -> liftM2 AbsFun (ren pty) (ren ptr)
+
+  ResOper pty ptr -> liftM2 ResOper (ren pty) (ren ptr)
+  ResParam pp -> liftM ResParam (renPerh (mapM (renameParam status)) pp)
+  ResValue t  -> liftM ResValue (ren t)
+  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)
+    Vr x      
+      | elem x vs -> return trm
+      | otherwise -> renid trm
+    Cn _   -> renid trm
+    Con _  -> renid trm
+    Q _ _  -> renid trm
+    QC _ _ -> renid trm
+
+----    Eqs eqs -> Eqs (map (renameEquation consts vs) 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
+          _ -> liftM (flip P l) $ renid t                 -- const proj last
+
+    _ -> 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
+
+  PC c ps -> do
+    c' <- renameIdentTerm env $ Cn c
+    psvss <- mapM renp ps
+    let (ps',vs) = unzip psvss
+    return $ case c' of
+      QC p d -> (PP p d ps', concat vs)
+      _ -> (PC c ps', concat vs)
+
+----  PP p c ps -> (PP p c ps',concat vs') where (ps',vs') = unzip $ map renp ps
+
+  PV x -> case renid patt of
+    Ok p -> return (p,[])
+    _    -> 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') 
+
+  _ -> return (patt,[])
+
+ where 
+   renp  = renamePattern env
+   renid = renameIdentPatt 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
+
+{-
+renameEquation :: Status -> [Ident] -> Equation -> Equation
+renameEquation b vs (ps,t) = (ps',renameTerm b (concat vs' ++ vs) t) where
+  (ps',vs') = unzip $ map (renamePattern b vs) ps
+-}
+
diff --git a/src/GF/Compile/ShellState.hs b/src/GF/Compile/ShellState.hs
new file mode 100644
index 000000000..f24c3b87c
--- /dev/null
+++ b/src/GF/Compile/ShellState.hs
@@ -0,0 +1,338 @@
+module ShellState where
+
+import Operations
+import GFC
+import AbsGFC
+---import CMacros
+import Look
+import qualified Modules as M
+import qualified Grammar as G
+import qualified PrGrammar as P
+import CF
+import CFIdent
+import CanonToCF
+import Morphology
+import Option
+import Ident
+import Arch (ModTime)
+
+-- AR 11/11/2001 -- 17/6/2003 (for modules) ---- unfinished
+
+-- multilingual state with grammars and options
+data ShellState = ShSt {
+  abstract   :: Maybe Ident ,        -- pointer to actual abstract; nothing in empty st
+  concrete   :: Maybe Ident ,        -- pointer to primary concrete
+  concretes  :: [(Ident,Ident)],     -- list of all concretes
+  canModules :: CanonGrammar ,       -- the place where abstracts and concretes reside
+  srcModules :: G.SourceGrammar ,    -- the place of saved resource modules
+  cfs        :: [(Ident,CF)] ,       -- context-free grammars
+  morphos    :: [(Ident,Morpho)],    -- morphologies
+  gloptions  :: Options,             -- global options
+  readFiles  :: [(FilePath,ModTime)],-- files read
+  absCats    :: [(G.Cat,(G.Context,  -- cats, their contexts, 
+                  [(G.Fun,G.Type)],          -- functions to them,
+                  [((G.Fun,Int),G.Type)]))], -- functions on them
+  statistics :: [Statistics]         -- statistics on grammars
+  }                             
+
+data Statistics = 
+    StDepTypes Bool        -- whether there are dependent types      
+  | StBoundVars [G.Cat]    -- which categories have bound variables
+  ---                      -- etc
+   deriving (Eq,Ord)
+
+emptyShellState = ShSt {
+  abstract   = Nothing,
+  concrete   = Nothing,
+  concretes  = [],
+  canModules = M.emptyMGrammar,
+  srcModules = M.emptyMGrammar,
+  cfs        = [],
+  morphos    = [],
+  gloptions  = noOptions,
+  readFiles  = [],
+  absCats    = [],
+  statistics = []
+  }
+
+type Language = Ident
+language = identC
+prLanguage = prIdent
+
+-- grammar for one language in a state, comprising its abs and cnc
+
+data StateGrammar = StGr {
+  absId   :: Ident,
+  cncId   :: Ident,
+  grammar :: CanonGrammar,
+  cf      :: CF,
+  morpho  :: Morpho
+  }
+
+emptyStateGrammar = StGr {
+  absId   = identC "#EMPTY", ---
+  cncId   = identC "#EMPTY", ---
+  grammar = M.emptyMGrammar,
+  cf      = emptyCF,
+  morpho  = emptyMorpho
+  }
+
+-- analysing shell grammar into parts
+stateGrammarST = grammar
+stateCF        = cf
+stateMorpho    = morpho
+stateOptions _ = noOptions ----
+
+cncModuleIdST = stateGrammarST
+
+-- form a shell state from a canonical grammar
+
+grammar2shellState :: Options -> (CanonGrammar, G.SourceGrammar) -> Err ShellState 
+grammar2shellState opts (gr,sgr) = updateShellState opts emptyShellState (gr,(sgr,[]))
+
+-- update a shell state from a canonical grammar
+
+updateShellState :: Options -> ShellState -> 
+                    (CanonGrammar,(G.SourceGrammar,[(FilePath,ModTime)])) -> 
+                    Err ShellState 
+updateShellState opts sh (gr,(sgr,rts)) = do 
+  let cgr = M.updateMGrammar (canModules sh) gr
+      a' = ifNull Nothing (return . last) $ allAbstracts cgr
+  abstr0 <- case abstract sh of
+    Just a -> do
+      --- test that abstract is compatible
+      return $ Just a
+    _ -> return a'
+  let concrs = maybe [] (allConcretes cgr) abstr0
+      concr0 = ifNull Nothing (return . last) concrs
+      notInrts f = notElem f $ map fst rts
+  cfs <- mapM (canon2cf opts cgr) concrs --- would not need to update all...
+
+  let funs = [] ---- funRulesOf cgr
+  let cats = [] ---- allCatsOf cgr
+  let csi  = [] ----
+{-
+             [(c,(co,
+                  [(fun,typ) | (fun,typ) <- funs, compatType tc typ], 
+                  funsOnTypeFs compatType funs tc))
+                                              | (c,co) <- cats, let tc = cat2type c]
+-}
+  let deps = True ---- not $ null $ allDepCats cgr
+  let binds = [] ---- allCatsWithBind cgr 
+
+  return $ ShSt {
+    abstract   = abstr0, 
+    concrete   = concr0, 
+    concretes  = zip concrs concrs,
+    canModules = cgr,
+    srcModules = M.updateMGrammar (srcModules sh) sgr,
+    cfs        = zip concrs cfs,
+    morphos    = zip concrs (repeat emptyMorpho),
+    gloptions  = opts,                            ---- -- global options
+    readFiles  = [ft | ft@(f,_) <- readFiles sh, notInrts f] ++ rts,
+    absCats    = csi,
+    statistics = [StDepTypes deps,StBoundVars binds]
+    }            
+
+prShellStateInfo :: ShellState -> String
+prShellStateInfo sh = unlines [
+  "main abstract :    " +++ maybe "(none)" P.prt (abstract sh),
+  "main concrete :    " +++ maybe "(none)" P.prt (concrete sh),
+  "all concretes :    " +++ unwords (map (P.prt . fst) (concretes sh)),
+  "canonical modules :" +++ unwords (map (P.prt .fst) (M.modules (canModules sh))),
+  "source modules :   " +++ unwords (map (P.prt .fst) (M.modules (srcModules sh))),
+  "global options :   " +++ prOpts (gloptions sh)
+  ]
+
+
+-- form just one state grammar, if unique, from a canonical grammar
+
+grammar2stateGrammar :: Options -> CanonGrammar -> Err StateGrammar 
+grammar2stateGrammar opts gr = do 
+  st    <- grammar2shellState opts (gr,M.emptyMGrammar)
+  concr <- maybeErr "no concrete syntax" $ concrete st 
+  return $ stateGrammarOfLang st concr
+
+-- all abstract modules
+allAbstracts :: CanonGrammar -> [Ident]
+allAbstracts gr = [i | (i,M.ModMod m) <- M.modules gr, M.mtype m == M.MTAbstract]
+
+-- the last abstract in dependency order
+greatestAbstract :: CanonGrammar -> Maybe Ident
+greatestAbstract gr = case allAbstracts gr of
+  [] -> Nothing
+  a -> return $ last a
+
+-- all concretes for a given abstract
+allConcretes :: CanonGrammar -> Ident -> [Ident]
+allConcretes gr a = [i | (i,M.ModMod m) <- M.modules gr, M.mtype m== M.MTConcrete a]
+
+stateGrammarOfLang :: ShellState -> Language -> StateGrammar
+stateGrammarOfLang st l = StGr {
+  absId   = maybe (identC "Abs") id (abstract st), ---
+  cncId   = l,
+  grammar = canModules st, ---- only those needed for l
+  cf      = maybe emptyCF id (lookup l (cfs st)),
+  morpho  = maybe emptyMorpho id (lookup l (morphos st))
+  }
+
+grammarOfLang st = stateGrammarST . stateGrammarOfLang st
+cfOfLang st      = stateCF        . stateGrammarOfLang st
+morphoOfLang st  = stateMorpho    . stateGrammarOfLang st
+optionsOfLang st = stateOptions   . stateGrammarOfLang st
+
+-- the last introduced grammar, stored in options, is the default for operations
+
+firstStateGrammar :: ShellState -> StateGrammar
+firstStateGrammar st = errVal emptyStateGrammar $ do
+  concr <- maybeErr "no concrete syntax" $ concrete st 
+  return $ stateGrammarOfLang st concr
+
+mkStateGrammar :: ShellState -> Language -> StateGrammar
+mkStateGrammar = stateGrammarOfLang
+
+-- analysing shell state into parts
+globalOptions = gloptions
+allLanguages  = map fst . concretes
+
+allStateGrammars = map snd . allStateGrammarsWithNames
+
+allStateGrammarsWithNames st = [(c, mkStateGrammar st c) | (c,_) <- concretes st]
+
+allGrammarFileNames st = [prLanguage c ++ ".gf" | (c,_) <- concretes st] ---
+
+{-
+allActiveStateGrammarsWithNames (ShSt (ma,gs,_)) = 
+  [(l, mkStateGrammar a c) | (l,((_,True),c)) <- gs, Just a <- [ma]]
+
+
+
+allActiveGrammars = map snd . allActiveStateGrammarsWithNames
+
+allGrammarSTs = map stateGrammarST . allStateGrammars
+allCFs        = map stateCF        . allStateGrammars
+
+firstGrammarST  = stateGrammarST . firstStateGrammar
+firstAbstractST = abstractOf . firstGrammarST
+firstConcreteST = concreteOf . firstGrammarST
+-}
+-- command-line option -language=foo overrides the actual grammar in state
+grammarOfOptState :: Options -> ShellState -> StateGrammar
+grammarOfOptState opts st = 
+  maybe (firstStateGrammar st) (stateGrammarOfLang st . language) $ 
+                                               getOptVal opts useLanguage
+
+-- command-line option -cat=foo overrides the possible start cat of a grammar
+firstCatOpts :: Options -> StateGrammar -> CFCat
+firstCatOpts opts sgr = 
+  maybe (stateFirstCat sgr) (string2CFCat (P.prt (absId sgr))) $ 
+    getOptVal opts firstCat
+
+-- a grammar can have start category as option startcat=foo ; default is S 
+stateFirstCat sgr =
+  maybe (string2CFCat a "S") (string2CFCat a) $ 
+  getOptVal (stateOptions sgr) gStartCat
+ where 
+   a = P.prt (absId sgr)
+
+-- the first cat for random generation
+firstAbsCat :: Options -> StateGrammar -> G.QIdent
+firstAbsCat opts sgr = 
+  maybe (absId sgr, identC "S") (\c -> (absId sgr, identC c)) $ ----
+    getOptVal opts firstCat
+
+{-
+-- command-line option -cat=foo overrides the possible start cat of a grammar
+stateTransferFun :: StateGrammar -> Maybe Fun
+stateTransferFun sgr = getOptVal (stateOptions sgr) transferFun >>= return . zIdent
+
+stateConcrete = concreteOf . stateGrammarST
+stateAbstract = abstractOf . stateGrammarST
+
+maybeStateAbstract (ShSt (ma,_,_)) = ma
+hasStateAbstract = maybe False (const True) . maybeStateAbstract
+abstractOfState = maybe emptyAbstractST id . maybeStateAbstract
+
+stateIsWord sg = isKnownWord (stateMorpho sg)
+
+
+-- getting info on a language
+existLang :: ShellState -> Language -> Bool
+existLang st lang = elem lang (allLanguages st)
+
+stateConcreteOfLang :: ShellState -> Language -> StateConcrete
+stateConcreteOfLang (ShSt (_,gs,_)) lang = 
+  maybe emptyStateConcrete snd $ lookup lang gs
+
+fileOfLang :: ShellState -> Language -> FilePath
+fileOfLang (ShSt (_,gs,_)) lang = 
+  maybe nonExistingLangFile (fst .fst) $ lookup lang gs
+
+nonExistingLangFile = "NON-EXISTING LANGUAGE" ---
+
+
+allLangOptions st lang = unionOptions (optionsOfLang st lang) (globalOptions st)
+
+-- construct state
+
+stateGrammar st cf mo opts = StGr ((st,cf,mo),opts)
+
+initShellState ab fs gs opts = 
+  ShSt (Just ab, [(getLangName f, ((f,True),g)) | (f,g) <- zip fs gs], opts)
+emptyInitShellState opts     = ShSt (Nothing, [], opts)
+
+-- the second-last part of a file name is the default language name
+getLangName :: String -> Language
+getLangName file = language (if notElem '.' file then file else langname) where
+ elif     = reverse file
+ xiferp   = tail (dropWhile (/='.') elif)
+ langname = reverse (takeWhile (flip notElem "./") xiferp)
+
+-- option -language=foo overrides the default language name
+getLangNameOpt :: Options -> String -> Language
+getLangNameOpt opts file = 
+  maybe (getLangName file) language $ getOptVal opts useLanguage
+-}
+-- modify state
+
+type ShellStateOper = ShellState -> ShellState
+
+reinitShellState :: ShellStateOper
+reinitShellState = const emptyShellState
+
+{-
+languageOn  = languageOnOff True
+languageOff = languageOnOff False
+
+languageOnOff :: Bool -> Language -> ShellStateOper
+languageOnOff b lang (ShSt (ab,gs,os)) = ShSt (ab, gs', os) where
+  gs' = [if lang==l then (l,((f,b),g)) else i | i@(l,((f,_),g)) <- gs]
+
+updateLanguage :: FilePath -> (Language, StateConcrete) -> ShellStateOper
+updateLanguage file (lang,gr) (ShSt (ab,gs,os)) = 
+  ShSt (ab, updateAssoc (lang,((file,True),gr)) gs, os') where
+    os' = changeOptVal os useLanguage (prLanguage lang) -- actualizes the new lang
+
+initWithAbstract :: AbstractST -> ShellStateOper
+initWithAbstract ab st@(ShSt (ma,cs,os)) = 
+  maybe (ShSt (Just ab,cs,os)) (const st) ma
+
+removeLanguage :: Language -> ShellStateOper
+removeLanguage lang (ShSt (ab,gs,os)) = ShSt (ab,removeAssoc lang gs, os)
+-}
+changeOptions :: (Options -> Options) -> ShellStateOper
+changeOptions f (ShSt a c cs can src cfs ms os ff ts ss) = 
+  ShSt a c cs can src cfs ms (f os) ff ts ss
+
+changeModTimes :: [(FilePath,ModTime)] -> ShellStateOper
+changeModTimes mfs (ShSt a c cs can src cfs ms os ff ts ss) = 
+  ShSt a c cs can src cfs ms os ff' ts ss
+ where
+   ff' = mfs ++ [mf | mf@(f,_) <- ff, notElem f (map fst mfs)]
+
+addGlobalOptions :: Options -> ShellStateOper
+addGlobalOptions = changeOptions . addOptions
+
+removeGlobalOptions :: Options -> ShellStateOper
+removeGlobalOptions = changeOptions . removeOptions
+
diff --git a/src/GF/Compile/Update.hs b/src/GF/Compile/Update.hs
new file mode 100644
index 000000000..9bc16f03a
--- /dev/null
+++ b/src/GF/Compile/Update.hs
@@ -0,0 +1,98 @@
+module Update where
+
+import Ident
+import Grammar
+import PrGrammar
+import Modules
+
+import Operations
+
+import List
+import 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) (unifPerhaps 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
+
+  _ -> Bad $ "cannot unify information for" +++ show i
+
+--- 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 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"