reorganize the modules in GF.Compile.*

src/compiler/GF/Compile/Compute/Abstract.hs

@@ -0,0 +1,138 @@
+----------------------------------------------------------------------
+-- |
+-- Module      : GF.Compile.Abstract.Compute
+-- Maintainer  : AR
+-- Stability   : (stable)
+-- Portability : (portable)
+--
+-- > CVS $Date: 2005/10/02 20:50:19 $ 
+-- > CVS $Author: aarne $
+-- > CVS $Revision: 1.8 $
+--
+-- computation in abstract syntax w.r.t. explicit definitions.
+--
+-- old GF computation; to be updated
+-----------------------------------------------------------------------------
+
+module GF.Compile.Compute.Abstract (LookDef,
+		   compute, 
+		   computeAbsTerm, 
+		   computeAbsTermIn, 
+		   beta
+		  ) where
+
+import GF.Data.Operations
+
+import GF.Grammar
+import GF.Grammar.Lookup
+
+import Debug.Trace
+import Data.List(intersperse)
+import Control.Monad (liftM, liftM2)
+import Text.PrettyPrint
+
+-- for debugging
+tracd m t = t 
+-- tracd = trace
+
+compute :: SourceGrammar -> Exp -> Err Exp
+compute = computeAbsTerm
+
+computeAbsTerm :: SourceGrammar -> Exp -> Err Exp
+computeAbsTerm gr = computeAbsTermIn (lookupAbsDef gr) []
+
+-- | a hack to make compute work on source grammar as well
+type LookDef = Ident -> Ident -> Err (Maybe Int,Maybe [Equation])
+
+computeAbsTermIn :: LookDef -> [Ident] -> Exp -> Err Exp
+computeAbsTermIn lookd xs e = errIn (render (text "computing" <+> ppTerm Unqualified 0 e)) $ compt xs e where
+  compt vv t = case t of
+--    Prod x a b  -> liftM2 (Prod x) (compt vv a) (compt (x:vv) b)
+--    Abs x b     -> liftM  (Abs  x)              (compt (x:vv) b)
+    _ -> do
+      let t' = beta vv t
+      (yy,f,aa) <- termForm t'
+      let vv' = map snd yy ++ vv
+      aa'    <- mapM (compt vv') aa
+      case look f of
+        Just eqs -> tracd (text "\nmatching" <+> ppTerm Unqualified 0 f) $ 
+                          case findMatch eqs aa' of
+          Ok (d,g) -> do
+            --- let (xs,ts) = unzip g
+            --- ts' <- alphaFreshAll vv' ts
+            let g' = g --- zip xs ts'
+            d' <- compt vv' $ substTerm vv' g' d
+            tracd (text "by Egs:" <+> ppTerm Unqualified 0 d') $ return $ mkAbs yy $ d'
+          _ -> tracd (text "no match" <+> ppTerm Unqualified 0 t') $ 
+               do
+            let v = mkApp f aa'
+            return $ mkAbs yy $ v
+        _ -> do
+          let t2 = mkAbs yy $ mkApp f aa'
+          tracd (text "not defined" <+> ppTerm Unqualified 0 t2) $ return t2
+
+  look t = case t of
+     (Q (m,f)) -> case lookd m f of
+       Ok (_,md) -> md
+       _ -> Nothing
+     _ -> Nothing
+
+beta :: [Ident] -> Exp -> Exp
+beta vv c = case c of
+  Let (x,(_,a)) b -> beta vv $ substTerm vv [(x,beta vv a)] (beta (x:vv) b) 
+  App f         a -> 
+    let (a',f') = (beta vv a, beta vv f) in 
+    case f' of
+      Abs _ x b -> beta vv $ substTerm vv [(x,a')] (beta (x:vv) b) 
+      _ ->               (if a'==a && f'==f then id else beta vv) $ App f' a'
+  Prod b x a t      -> Prod b x (beta vv a) (beta (x:vv) t)
+  Abs b x t       -> Abs b x (beta (x:vv) t)
+  _               -> c
+
+-- special version of pattern matching, to deal with comp under lambda
+
+findMatch :: [([Patt],Term)] -> [Term] -> Err (Term, Substitution)
+findMatch cases terms = case cases of
+  [] -> Bad $ render (text "no applicable case for" <+> hcat (punctuate comma (map (ppTerm Unqualified 0) terms)))
+  (patts,_):_ | length patts /= length terms -> 
+       Bad (render (text "wrong number of args for patterns :" <+> 
+                    hsep (map (ppPatt Unqualified 0) patts) <+> text "cannot take" <+> hsep (map (ppTerm Unqualified 0) terms)))
+  (patts,val):cc -> case mapM tryMatch (zip patts terms) of
+     Ok substs -> return (tracd (text "value" <+> ppTerm Unqualified 0 val) val, concat substs)
+     _         -> findMatch cc terms
+
+tryMatch :: (Patt, Term) -> Err [(Ident, Term)]
+tryMatch (p,t) = do 
+  t' <- termForm t
+  trym p t'
+ where
+
+  trym p t' = err (\s -> tracd s (Bad s)) (\t -> tracd (prtm p t) (return t)) $ ---- 
+              case (p,t') of
+    (PW,    _) | notMeta t -> return [] -- optimization with wildcard
+    (PV x,  _) | notMeta t -> return [(x,t)]
+    (PString s, ([],K i,[])) | s==i -> return []
+    (PInt s, ([],EInt i,[])) | s==i -> return []
+    (PFloat s,([],EFloat i,[])) | s==i -> return [] --- rounding?
+    (PP (q,p) pp, ([], QC (r,f), tt)) | 
+       p `eqStrIdent` f && length pp == length tt -> do
+         matches <- mapM tryMatch (zip pp tt)
+         return (concat matches)
+    (PP (q,p) pp, ([], Q (r,f), tt)) | 
+       p `eqStrIdent` f && length pp == length tt -> do
+         matches <- mapM tryMatch (zip pp tt)
+         return (concat matches)
+    (PT _ p',_) -> trym p' t'
+    (PAs x p',_) -> do
+       subst <- trym p' t'
+       return $ (x,t) : subst
+    _ -> Bad (render (text "no match in pattern" <+> ppPatt Unqualified 0 p <+> text "for" <+> ppTerm Unqualified 0 t))
+
+  notMeta e = case e of
+    Meta _  -> False
+    App f a -> notMeta f &&  notMeta a  
+    Abs _ _ b -> notMeta b
+    _ -> True
+
+  prtm p g = 
+    ppPatt Unqualified 0 p <+> colon $$ hsep (punctuate semi [ppIdent x <+> char '=' <+> ppTerm Unqualified 0 y | (x,y) <- g])

src/compiler/GF/Compile/Compute/AppPredefined.hs

@@ -0,0 +1,157 @@
+----------------------------------------------------------------------
+-- |
+-- Module      : AppPredefined
+-- Maintainer  : AR
+-- Stability   : (stable)
+-- Portability : (portable)
+--
+-- > CVS $Date: 2005/10/06 14:21:34 $ 
+-- > CVS $Author: aarne $
+-- > CVS $Revision: 1.13 $
+--
+-- Predefined function type signatures and definitions.
+-----------------------------------------------------------------------------
+
+module GF.Compile.Compute.AppPredefined (isInPredefined, typPredefined, appPredefined
+		     ) where
+
+import GF.Infra.Ident
+import GF.Data.Operations
+import GF.Grammar.Predef
+import GF.Grammar.Grammar
+import GF.Grammar.Macros
+import GF.Grammar.Printer
+import qualified Data.ByteString.Char8 as BS
+import Text.PrettyPrint
+
+-- predefined function type signatures and definitions. AR 12/3/2003.
+
+isInPredefined :: Ident -> Bool
+isInPredefined = err (const True) (const False) . typPredefined
+
+typPredefined :: Ident -> Err Type
+typPredefined f
+  | f == cInt       = return typePType
+  | f == cFloat     = return typePType
+  | f == cErrorType = return typeType
+  | f == cInts      = return $ mkFunType [typeInt] typePType
+  | f == cPBool     = return typePType
+  | f == cError     = return $ mkFunType [typeStr] typeError  -- non-can. of empty set
+  | f == cPFalse    = return $ typePBool
+  | f == cPTrue     = return $ typePBool
+  | f == cDp        = return $ mkFunType [typeInt,typeTok] typeTok
+  | f == cDrop      = return $ mkFunType [typeInt,typeTok] typeTok
+  | f == cEqInt     = return $ mkFunType [typeInt,typeInt] typePBool
+  | f == cLessInt   = return $ mkFunType [typeInt,typeInt] typePBool
+  | f == cEqStr     = return $ mkFunType [typeTok,typeTok] typePBool
+  | f == cLength    = return $ mkFunType [typeTok] typeInt
+  | f == cOccur     = return $ mkFunType [typeTok,typeTok] typePBool
+  | f == cOccurs    = return $ mkFunType [typeTok,typeTok] typePBool
+  | f == cPlus      = return $ mkFunType [typeInt,typeInt] (typeInt)
+----  "read"   -> (P : Type) -> Tok -> P
+  | f == cShow      = return $ mkProd -- (P : PType) -> P -> Tok
+    [(Explicit,varP,typePType),(Explicit,identW,Vr varP)] typeStr []
+  | f == cToStr     = return $ mkProd -- (L : Type)  -> L -> Str
+    [(Explicit,varL,typeType),(Explicit,identW,Vr varL)] typeStr []
+  | f == cMapStr    = return $ mkProd -- (L : Type)  -> (Str -> Str) -> L -> L
+    [(Explicit,varL,typeType),(Explicit,identW,mkFunType [typeStr] typeStr),(Explicit,identW,Vr varL)] (Vr varL) []
+  | f == cTake      = return $ mkFunType [typeInt,typeTok] typeTok
+  | f == cTk        = return $ mkFunType [typeInt,typeTok] typeTok
+  | otherwise       = Bad (render (text "unknown in Predef:" <+> ppIdent f))
+
+varL :: Ident
+varL = identC (BS.pack "L")
+
+varP :: Ident
+varP = identC (BS.pack "P")
+
+appPredefined :: Term -> Err (Term,Bool)
+appPredefined t = case t of
+  App f x0 -> do
+   (x,_) <- appPredefined x0
+   case f of
+    -- one-place functions
+    Q (mod,f) | mod == cPredef ->
+      case x of
+        (K s) | f == cLength -> retb $ EInt $ length s
+        _                    -> retb t
+
+    -- two-place functions
+    App (Q (mod,f)) z0 | mod == cPredef -> do
+     (z,_) <- appPredefined z0
+     case (norm z, norm x) of
+      (EInt i, K s)    | f == cDrop    -> retb $ K (drop i s)
+      (EInt i, K s)    | f == cTake    -> retb $ K (take i s)
+      (EInt i, K s)    | f == cTk      -> retb $ K (take (max 0 (length s - i)) s)
+      (EInt i, K s)    | f == cDp      -> retb $ K (drop (max 0 (length s - i)) s)
+      (K s,    K t)    | f == cEqStr   -> retb $ if s == t then predefTrue else predefFalse
+      (K s,    K t)    | f == cOccur   -> retb $ if substring s t then predefTrue else predefFalse
+      (K s,    K t)    | f == cOccurs  -> retb $ if any (flip elem t) s then predefTrue else predefFalse
+      (EInt i, EInt j) | f == cEqInt   -> retb $ if i==j then predefTrue else predefFalse
+      (EInt i, EInt j) | f == cLessInt -> retb $ if i<j  then predefTrue else predefFalse
+      (EInt i, EInt j) | f == cPlus    -> retb $ EInt $ i+j
+      (_,      t)      | f == cShow    -> retb $ foldr C Empty $ map K $ words $ render (ppTerm Unqualified 0 t)
+      (_,      K s)    | f == cRead    -> retb $ Cn (identC (BS.pack s)) --- because of K, only works for atomic tags
+      (_,      t)      | f == cToStr   -> trm2str t >>= retb
+      _ -> retb t ---- prtBad "cannot compute predefined" t
+
+    -- three-place functions
+    App (App (Q (mod,f)) z0) y0 | mod == cPredef -> do
+     (y,_) <- appPredefined y0
+     (z,_) <- appPredefined z0
+     case (z, y, x) of
+       (ty,op,t) | f == cMapStr -> retf $ mapStr ty op t
+       _ -> retb t ---- prtBad "cannot compute predefined" t
+
+    _ -> retb t ---- prtBad "cannot compute predefined" t
+  _ -> retb t
+                  ---- should really check the absence of arg variables
+ where
+   retb t = return (retc t,True)  -- no further computing needed
+   retf t = return (retc t,False) -- must be computed further
+   retc t = case t of
+     K [] -> t
+     K s  -> foldr1 C (map K (words s))
+     _    -> t
+   norm t = case t of
+     Empty -> K []
+     C u v -> case (norm u,norm v) of
+       (K x,K y) -> K (x +++ y)
+       _ -> t
+     _ -> t
+
+-- read makes variables into constants
+
+predefTrue = QC (cPredef,cPTrue)
+predefFalse = QC (cPredef,cPFalse)
+
+substring :: String -> String -> Bool
+substring s t = case (s,t) of
+  (c:cs, d:ds) -> (c == d && substring cs ds) || substring s ds
+  ([],_) -> True
+  _ -> False
+
+trm2str :: Term -> Err Term
+trm2str t = case t of
+  R ((_,(_,s)):_) -> trm2str s
+  T _ ((_,s):_)   -> trm2str s
+  V _ (s:_)       -> trm2str s
+  C _ _           -> return $ t
+  K _             -> return $ t
+  S c _           -> trm2str c
+  Empty           -> return $ t
+  _               -> Bad (render (text "cannot get Str from term" <+> ppTerm Unqualified 0 t))
+
+-- simultaneous recursion on type and term: type arg is essential!
+-- But simplify the task by assuming records are type-annotated
+-- (this has been done in type checking)
+mapStr :: Type -> Term -> Term -> Term
+mapStr ty f t = case (ty,t) of
+  _ | elem ty [typeStr,typeTok] -> App f t
+  (_,        R ts)    -> R [(l,mapField v)   | (l,v) <- ts]
+  (Table a b,T ti cs) -> T ti [(p,mapStr b f v) | (p,v) <- cs]
+  _    -> t 
+ where
+   mapField (mty,te) = case mty of
+     Just ty -> (mty,mapStr ty f te)
+     _ -> (mty,te)

src/compiler/GF/Compile/Compute/Concrete.hs

@@ -0,0 +1,461 @@
+----------------------------------------------------------------------
+-- |
+-- Module      : GF.Compile.Concrete.Compute
+-- Maintainer  : AR
+-- Stability   : (stable)
+-- Portability : (portable)
+--
+-- > CVS $Date: 2005/11/01 15:39:12 $ 
+-- > CVS $Author: aarne $
+-- > CVS $Revision: 1.19 $
+--
+-- Computation of source terms. Used in compilation and in @cc@ command.
+-----------------------------------------------------------------------------
+
+module GF.Compile.Compute.Concrete (computeConcrete, computeTerm,computeConcreteRec) where
+
+import GF.Data.Operations
+import GF.Grammar.Grammar
+import GF.Infra.Ident
+import GF.Infra.Option
+import GF.Infra.Modules
+import GF.Data.Str
+import GF.Grammar.Printer
+import GF.Grammar.Predef
+import GF.Grammar.Macros
+import GF.Grammar.Lookup
+import GF.Compile.Refresh
+import GF.Grammar.PatternMatch
+import GF.Grammar.Lockfield (isLockLabel,unlockRecord) ----
+
+import GF.Compile.Compute.AppPredefined
+
+import Data.List (nub,intersperse)
+import Control.Monad (liftM2, liftM)
+import Text.PrettyPrint
+
+-- | computation of concrete syntax terms into normal form
+-- used mainly for partial evaluation
+computeConcrete :: SourceGrammar -> Term -> Err Term
+computeConcrete    g t = {- refreshTerm t >>= -} computeTerm g [] t
+computeConcreteRec g t = {- refreshTerm t >>= -} computeTermOpt True g [] t
+
+computeTerm :: SourceGrammar -> Substitution -> Term -> Err Term
+computeTerm = computeTermOpt False
+
+-- rec=True is used if it cannot be assumed that looked-up constants
+-- have already been computed (mainly with -optimize=noexpand in .gfr)
+
+computeTermOpt :: Bool -> SourceGrammar -> Substitution -> Term -> Err Term
+computeTermOpt rec gr = comput True where
+
+   comput full g t = ---- errIn ("subterm" +++ prt t) $ --- for debugging 
+              case t of
+
+     Q (p,c) | p == cPredef -> return t
+             | otherwise    -> look (p,c) 
+
+     Vr x -> do
+       t' <- maybe (Bad (render (text "no value given to variable" <+> ppIdent x))) return $ lookup x g
+       case t' of 
+         _ | t == t' -> return t
+         _ -> comp g t'
+
+     -- Abs x@(IA _) b -> do 
+     Abs _ _ _ | full -> do 
+       let (xs,b1) = termFormCnc t   
+       b' <- comp ([(x,Vr x) | (_,x) <- xs] ++ g) b1
+       return $ mkAbs xs b'
+     --  b' <- comp (ext x (Vr x) g) b
+     --  return $ Abs x b'
+     Abs _ _ _ -> return t -- hnf
+
+     Let (x,(_,a)) b -> do
+       a' <- comp g a
+       comp (ext x a' g) b
+
+     Prod b x a t -> do
+       a' <- comp g a
+       t' <- comp (ext x (Vr x) g) t
+       return $ Prod b x a' t'
+
+     -- beta-convert
+     App f a -> case appForm t of
+      (h,as) | length as > 1 -> do
+        h' <- hnf g h
+        as' <- mapM (comp g) as
+        case h' of
+          _ | not (null [() | FV _ <- as']) -> compApp g (mkApp h' as')
+          c@(QC _) -> do
+            return $ mkApp c as'
+          Q (mod,f) | mod == cPredef -> do     
+            (t',b) <- appPredefined (mkApp h' as')
+            if b then return t' else comp g t'
+
+          Abs _ _ _ -> do
+            let (xs,b) = termFormCnc h'
+            let g' = (zip (map snd xs) as') ++ g
+            let as2 = drop (length xs) as'
+            let xs2 = drop (length as') xs
+            b' <- comp g' (mkAbs xs2 b)
+            if null as2 then return b' else comp g (mkApp b' as2)
+
+          _ -> compApp g (mkApp h' as')
+      _ -> compApp g t
+
+     P t l | isLockLabel l -> return $ R [] 
+     ---- a workaround 18/2/2005: take this away and find the reason
+     ---- why earlier compilation destroys the lock field
+
+
+     P t l  -> do
+       t' <- comp g t
+       case t' of
+         FV rs -> mapM (\c -> comp g (P c l)) rs >>= returnC . variants
+         R r   -> maybe (Bad (render (text "no value for label" <+> ppLabel l))) (comp g . snd) $ 
+                    lookup l $ reverse r 
+
+         ExtR a (R b) ->                 
+           case comp g (P (R b) l) of
+             Ok v -> return v
+             _ -> comp g (P a l)
+
+--- { - --- this is incorrect, since b can contain the proper value
+         ExtR (R a) b ->                 -- NOT POSSIBLE both a and b records!
+           case comp g (P (R a) l) of
+             Ok v -> return v
+             _ -> comp g (P b l)
+--- - } ---
+
+         S (T i cs) e -> prawitz g i (flip P l) cs e
+         S (V i cs) e -> prawitzV g i (flip P l) cs e
+
+         _   -> returnC $ P t' l
+
+     S t v -> do
+       t' <- compTable g t
+       v' <- comp g v
+       t1 <- case t' of
+----           V (RecType fs) _         -> uncurrySelect g fs t' v'
+----           T (TComp (RecType fs)) _ -> uncurrySelect g fs t' v'
+           _ -> return $ S t' v'
+       compSelect g t1
+
+     -- normalize away empty tokens
+     K "" -> return Empty
+
+     -- glue if you can
+     Glue x0 y0 -> do
+       x <- comp g x0
+       y <- comp g y0
+       case (x,y) of
+         (FV ks,_)         -> do
+           kys <- mapM (comp g . flip Glue y) ks
+           return $ variants kys
+         (_,FV ks)         -> do
+           xks <- mapM (comp g . Glue x) ks
+           return $ variants xks
+
+         (S (T i cs) e, s) -> prawitz g i (flip Glue s) cs e
+         (s, S (T i cs) e) -> prawitz g i (Glue s) cs e
+         (S (V i cs) e, s) -> prawitzV g i (flip Glue s) cs e
+         (s, S (V i cs) e) -> prawitzV g i (Glue s) cs e
+         (_,Empty)         -> return x
+         (Empty,_)         -> return y
+         (K a, K b)        -> return $ K (a ++ b)
+         (_, Alts d vs)    -> do
+----         (K a, Alts (d,vs)) -> do
+            let glx = Glue x
+            comp g $ Alts (glx d) [(glx v,c) | (v,c) <- vs]
+         (Alts _ _, ka) -> checks [do
+            y' <- strsFromTerm ka
+----         (Alts _, K a) -> checks [do
+            x' <- strsFromTerm x -- this may fail when compiling opers
+            return $ variants [
+              foldr1 C (map K (str2strings (glueStr v u))) | v <- x', u <- y']
+----              foldr1 C (map K (str2strings (glueStr v (str a)))) | v <- x']
+           ,return $ Glue x y
+           ]
+         (C u v,_) -> comp g $ C u (Glue v y)
+
+         _ -> do
+           mapM_ checkNoArgVars [x,y]
+           r <- composOp (comp g) t
+           returnC r
+
+     Alts d aa -> do
+       d' <- comp g d
+       aa' <- mapM (compInAlts g) aa
+       returnC (Alts d' aa')
+
+     -- remove empty
+     C a b    -> do
+       a' <- comp g a
+       b' <- comp g b
+       case (a',b') of
+         (Alts _ _, K a) -> checks [do
+            as <- strsFromTerm a' -- this may fail when compiling opers
+            return $ variants [
+              foldr1 C (map K (str2strings (plusStr v (str a)))) | v <- as]
+            ,
+            return $ C a' b'
+           ]
+         (Empty,_) -> returnC b'
+         (_,Empty) -> returnC a'
+         _     -> returnC $ C a' b'
+
+     -- reduce free variation as much as you can
+     FV ts -> mapM (comp g) ts >>= returnC . variants
+
+     -- merge record extensions if you can
+     ExtR r s -> do
+       r' <- comp g r
+       s' <- comp g s
+       case (r',s') of
+         (R rs, R ss) -> plusRecord r' s'
+         (RecType rs, RecType ss) -> plusRecType r' s'
+         _ -> return $ ExtR r' s'
+
+     ELin c r -> do
+       r' <- comp g r
+       unlockRecord c r'
+
+     T _ _ -> compTable g t
+     V _ _ -> compTable g t
+
+     -- otherwise go ahead
+     _ -> composOp (comp g) t >>= returnC
+
+    where
+
+     compApp g (App f a) = do
+       f' <- hnf g f
+       a' <- comp g a
+       case (f',a') of
+         (Abs _ x b, FV as) -> 
+           mapM (\c -> comp (ext x c g) b) as >>= return . variants
+         (_, FV as)  -> mapM (\c -> comp g (App f' c)) as >>= return . variants
+         (FV fs, _)  -> mapM (\c -> comp g (App c a')) fs >>= return . variants
+         (Abs _ x b,_) -> comp (ext x a' g) b
+
+         (QC _,_)  -> returnC $ App f' a'
+
+         (S (T i cs) e,_) -> prawitz g i (flip App a') cs e
+         (S (V i cs) e,_) -> prawitzV g i (flip App a') cs e
+
+	 _ -> do
+           (t',b) <- appPredefined (App f' a')
+           if b then return t' else comp g t'
+
+     hnf  = comput False
+     comp = comput True
+
+     look c
+       | rec       = lookupResDef gr c >>= comp []
+       | otherwise = lookupResDef gr 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 c -> case look c of
+         Ok (EPatt p') -> compPatternMacro p'
+         _ -> Bad (render (text "pattern expected as value of" $$ nest 2 (ppPatt Unqualified 0 p)))
+       PAs x p -> do
+         p' <- compPatternMacro p
+         return $ PAs x p'
+       PAlt p q -> do
+         p' <- compPatternMacro p
+         q' <- compPatternMacro q
+         return $ PAlt p' q'
+       PSeq p q -> do
+         p' <- compPatternMacro p
+         q' <- compPatternMacro q
+         return $ PSeq p' q'
+       PRep p -> do
+         p' <- compPatternMacro p
+         return $ PRep p'
+       PNeg p -> do
+         p' <- compPatternMacro p
+         return $ PNeg p'
+       PR rs -> do
+         rs' <- mapPairsM compPatternMacro rs
+         return $ PR rs'
+
+       _ -> return p
+
+     compSelect g (S t' v') = case v' of
+       FV vs -> mapM (\c -> comp g (S t' c)) vs >>= returnC . variants    
+
+----       S (T i cs) e -> prawitz g i (S t') cs e  -- AR 8/7/2010 sometimes better
+----       S (V i cs) e -> prawitzV g i (S t') cs e -- sometimes much worse 
+
+    
+       _ -> case t' of
+         FV ccs -> mapM (\c -> comp g (S c v')) ccs >>= returnC . variants
+
+         T _ [(PW,c)] -> comp g c           --- an optimization
+         T _ [(PT _ PW,c)] -> comp g c
+
+         T _ [(PV z,c)] -> comp (ext z v' g) c --- another optimization
+         T _ [(PT _ (PV z),c)] -> comp (ext z v' g) c
+
+         -- course-of-values table: look up by index, no pattern matching needed
+
+         V ptyp ts -> do
+             vs <- allParamValues gr ptyp
+             case lookupR v' (zip vs [0 .. length vs - 1]) of
+               Just i -> comp g $ ts !! i
+               _ -> return $ S t' v' -- if v' is not canonical
+         T _ cc -> do
+           case matchPattern cc v' of
+             Ok (c,g') -> comp (g' ++ g) c
+             _ | isCan v' -> Bad (render (text "missing case" <+> ppTerm Unqualified 0 v' <+> text "in" <+> ppTerm Unqualified 0 t))
+             _ -> return $ S t' v' -- if v' is not canonical
+
+         S (T i cs) e -> prawitz g i (flip S v') cs e
+         S (V i cs) e -> prawitzV g i (flip S v') cs e
+         _    -> returnC $ S t' v'
+
+     --- needed to match records with and without type information
+     ---- todo: eliminate linear search in a list of records!
+     lookupR v vs = case v of
+       R rs -> lookup ([(x,y) | (x,(_,y)) <- rs]) 
+                                [([(x,y) | (x,(_,y)) <- rs],v) | (R rs,v) <- vs]
+       _ -> lookup v vs
+
+     -- case-expand tables
+     -- if already expanded, don't expand again
+     compTable g t = case t of
+         T i@(TComp ty) cs -> do
+           -- if there are no variables, don't even go inside
+           cs' <- if (null g) then return cs else mapPairsM (comp g) cs
+----           return $ V ty (map snd cs')
+           return $ T i cs'
+         V ty cs -> do
+           ty' <- comp g ty
+           -- if there are no variables, don't even go inside
+           cs' <- if (null g) then return cs else mapM (comp g) cs
+           return $ V ty' cs'
+
+         T i cs -> do
+           pty0 <- getTableType i
+           ptyp <- comp g pty0
+           case allParamValues gr ptyp of
+             Ok vs0 -> do
+               let vs = vs0 ---- [Val v ptyp i | (v,i) <- zip vs0 [0..]]
+               ps0  <- mapM (compPatternMacro . fst) cs
+               cs'  <- mapM (compBranchOpt g) (zip ps0 (map snd cs))
+               sts  <- mapM (matchPattern cs') vs 
+               ts   <- mapM (\ (c,g') -> comp (g' ++ g) c) sts
+               ps   <- mapM term2patt vs
+               let ps' = ps --- PT ptyp (head ps) : tail ps
+----               return $ V ptyp ts -- to save space, just course of values
+               return $ T (TComp ptyp) (zip ps' ts)
+             _ -> do
+               ps0  <- mapM (compPatternMacro . fst) cs
+               cs'  <- mapM (compBranch g) (zip ps0 (map snd cs))
+
+----               cs' <- mapM (compBranch g) cs
+               return $ T i cs'  -- happens with variable types
+         _ -> comp g t
+
+     compBranch g (p,v) = do
+       let g' = contP p ++ g
+       v' <- comp g' v
+       return (p,v')
+
+     compBranchOpt g c@(p,v) = case contP p of
+       [] -> return c
+       _ -> err (const (return c)) return $ compBranch g c
+
+     contP p = case p of
+       PV x -> [(x,Vr x)]
+       PC _ ps -> concatMap contP ps
+       PP _ ps -> concatMap contP ps
+       PT _ p -> contP p
+       PR rs -> concatMap (contP . snd) rs
+
+       PAs x p -> (x,Vr x) : contP p
+
+       PSeq p q -> concatMap contP [p,q]
+       PAlt p q -> concatMap contP [p,q]
+       PRep p   -> contP p
+       PNeg p   -> contP p
+
+       _ -> []
+
+     prawitz g i f cs e = do
+       cs' <- mapM (compBranch g) [(p, f v) | (p,v) <- cs]
+       return $ S (T i cs') e
+     prawitzV g i f cs e = do
+       cs' <- mapM (comp g) [(f v) | v <- cs]
+       return $ S (V i cs') e
+
+     compInAlts g (v,c) = do
+       v' <- comp g v
+       c' <- comp g c
+       c2 <- case c' of
+         EPatt p -> liftM Strs $ getPatts p
+         _ -> return c'
+       return (v',c2)
+      where
+       getPatts p = case p of
+         PAlt a b  -> liftM2 (++) (getPatts a) (getPatts b)
+         PString s -> return [K s]
+         PSeq a b  -> do
+           as <- getPatts a
+           bs <- getPatts b
+           return [K (s ++ t) | K s <- as, K t <- bs]
+         _ -> fail (render (text "not valid pattern in pre expression" <+> ppPatt Unqualified 0 p))
+
+{- ----
+     uncurrySelect g fs t v = do
+       ts <- mapM (allParamValues gr . snd) fs
+       vs <- mapM (comp g) [P v r | r <- map fst fs]
+       return $ reorderSelect t fs ts vs
+
+     reorderSelect t fs pss vs = case (t,fs,pss,vs) of
+       (V _ ts, f:fs1, ps:pss1, v:vs1) -> 
+         S (V (snd f) 
+             [reorderSelect (V (RecType fs1) t) fs1 pss1 vs1 | 
+               t <- segments (length ts `div` length ps) ts]) v 
+       (T (TComp _) cs, f:fs1, ps:pss1, v:vs1) -> 
+         S (T (TComp (snd f)) 
+             [(p,reorderSelect (T (TComp (RecType fs1)) c) fs1 pss1 vs1) | 
+               (ep,c) <- zip ps (segments (length cs `div` length ps) cs),
+               let Ok p = term2patt ep]) v 
+       _ -> t
+
+     segments i xs = 
+       let (x0,xs1) = splitAt i xs in x0 : takeWhile (not . null) (segments i xs1)
+-}
+
+
+-- | argument variables cannot be glued
+checkNoArgVars :: Term -> Err Term
+checkNoArgVars t = case t of
+  Vr (IA _ _)    -> Bad $ glueErrorMsg $ ppTerm Unqualified 0 t 
+  Vr (IAV _ _ _) -> Bad $ glueErrorMsg $ ppTerm Unqualified 0 t 
+  _ -> composOp checkNoArgVars t
+
+glueErrorMsg s = 
+  render (text "Cannot glue (+) term with run-time variable" <+> s <> char '.' $$
+          text "Use Prelude.bind instead.")
+
+getArgType t = case t of
+  V ty _ -> return ty
+  T (TComp ty) _ -> return ty
+  _ -> Bad (render (text "cannot get argument type of table" $$ nest 2 (ppTerm Unqualified 0 t)))