    {-# LANGUAGE CPP #-}
    --
    -- Copyright (c) 2005 Lennart Augustsson
    -- See LICENSE for licensing details.
    --
    module Djinn.HTypes(
      HKind(..),
      HType(..),
      HSymbol,
      hTypeToFormula,
      pHSymbol,
      pHType,
      pHDataType,
      pHTAtom,
      pHKind,
      prHSymbolOp,
      htNot,
      isHTUnion,
      getHTVars,
      substHT,
      HClause (..),
      HPat (..),
      HExpr (..),
      hPrClause,
      hPrExpr,
      termToHExpr,
      termToHClause,
      getBinderVars
    ) where

    import Control.Monad (zipWithM)
    import Data.Char (isAlpha, isAlphaNum, isUpper)
    import Data.List (union, (\\))
    #ifdef MIN_VERSION_base(4,11,0)
    import Prelude hiding ((<>))
    #endif
    import Text.ParserCombinators.ReadP
    import Text.PrettyPrint.HughesPJ (Doc, comma, fsep, nest, parens,
                                      punctuate, renderStyle, sep,
                                      style, text, vcat, ($$), (<+>), (<>))

    import Djinn.LJTFormula

    type HSymbol = String

    data HKind = KStar
               | KArrow HKind HKind
               | KVar Int
               deriving (Eq, Show)

    data HType = HTApp HType HType
               | HTVar HSymbol
               | HTCon HSymbol
               | HTTuple [HType]
               | HTArrow HType HType
               | HTUnion [(HSymbol, [HType])]  -- Only for data types; only at top level
               | HTAbstract HSymbol HKind      -- XXX Uninterpreted type, like a variable but different kind checking
               deriving (Eq)

    isHTUnion :: HType -> Bool
    isHTUnion (HTUnion _) = True
    isHTUnion _ = False

    htNot :: HSymbol -> HType
    htNot x = HTArrow (HTVar x) (HTCon "Void")

    instance Show HType where
      showsPrec _ (HTApp (HTCon "[]") t) = showString "[" . showsPrec 0 t . showString "]"
      showsPrec p (HTApp f a) = showParen (p > 2) $ showsPrec 2 f . showString " " . showsPrec 3 a
      showsPrec _ (HTVar s) = showString s
      showsPrec _ (HTCon s@(c:_)) | not (isAlpha c) = showParen True $ showString s
      showsPrec _ (HTCon s) = showString s
      showsPrec _ (HTTuple ss) = showParen True $ f ss
        where f []     = error "showsPrec HType"
              f [t]    = showsPrec 0 t
              f (t:ts) = showsPrec 0 t . showString ", " . f ts
      showsPrec p (HTArrow s t) = showParen (p > 0) $ showsPrec 1 s . showString " -> " . showsPrec 0 t
      showsPrec _ (HTUnion cs) = f cs
        where f []           = id
              f [cts]        = scts cts
              f (cts : ctss) = scts cts . showString " | " . f ctss
              scts (c, ts)   = foldl (\ s t -> s . showString " " . showsPrec 10 t) (showString c) ts
      showsPrec _ (HTAbstract s _) = showString s

    instance Read HType where
      readsPrec _ = readP_to_S pHType'

    pHType' :: ReadP HType
    pHType' = do
      t <- pHType
      skipSpaces
      return t

    pHType :: ReadP HType
    pHType = do
      ts <- sepBy1 pHTypeApp (do schar '-'; char '>')
      return $ foldr1 HTArrow ts

    pHDataType :: ReadP HType
    pHDataType = do
      let con = do c <- pHSymbol True
                   ts <- many pHTAtom
                   return (c, ts)
      cts <- sepBy con (schar '|')
      return $ HTUnion cts

    pHTAtom :: ReadP HType
    pHTAtom = pHTVar +++ pHTCon +++ pHTList +++ pParen pHTTuple +++ pParen pHType +++ pUnit

    pUnit :: ReadP HType
    pUnit = do
      schar '('
      char ')'
      return $ HTCon "()"

    pHTCon :: ReadP HType
    pHTCon = (pHSymbol True >>= return . HTCon) +++
             do schar '('; schar '-'; schar '>'; schar ')'; return (HTCon "->")

    pHTVar :: ReadP HType
    pHTVar = pHSymbol False >>= return . HTVar

    pHSymbol :: Bool -> ReadP HSymbol
    pHSymbol con = do
      skipSpaces
      c <- satisfy $ \ c -> isAlpha c && isUpper c == con
      let isSym d = isAlphaNum d || d == '\'' || d == '.'
      cs <- munch isSym
      return $ c:cs

    pHTTuple :: ReadP HType
    pHTTuple = do
      t <- pHType
      ts <- many1 (do schar ','; pHType)
      return $ HTTuple $ t:ts

    pHTypeApp :: ReadP HType
    pHTypeApp = do
      ts <- many1 pHTAtom
      return $ foldl1 HTApp ts

    pHTList :: ReadP HType
    pHTList = do
      schar '['
      t <- pHType
      schar ']'
      return $ HTApp (HTCon "[]") t

    pHKind :: ReadP HKind
    pHKind = do
      ts <- sepBy1 pHKindA (do schar '-'; char '>')
      return $ foldr1 KArrow ts

    pHKindA :: ReadP HKind
    pHKindA = (do schar '*'; return KStar) +++ pParen pHKind

    pParen :: ReadP a -> ReadP a
    pParen p = do
      schar '('
      e <- p
      schar ')'
      return e

    schar :: Char -> ReadP ()
    schar c = do
      skipSpaces
      char c
      return ()

    getHTVars :: HType -> [HSymbol]
    getHTVars (HTApp f a)   = getHTVars f `union` getHTVars a
    getHTVars (HTVar v)     = [v]
    getHTVars (HTCon _)     = []
    getHTVars (HTTuple ts)  = foldr union [] (map getHTVars ts)
    getHTVars (HTArrow f a) = getHTVars f `union` getHTVars a
    getHTVars _             = error "getHTVars"

    -------------------------------

    hTypeToFormula :: [(HSymbol, ([HSymbol], HType, a))] -> HType -> Formula
    hTypeToFormula ss (HTTuple ts) = Conj (map (hTypeToFormula ss) ts)
    hTypeToFormula ss (HTArrow t1 t2) = hTypeToFormula ss t1 :-> hTypeToFormula ss t2
    hTypeToFormula ss (HTUnion ctss) = Disj [ (ConsDesc c (length ts), hTypeToFormula ss (HTTuple ts)) | (c, ts) <- ctss ]
    hTypeToFormula ss t = case expandSyn ss t [] of
      Nothing -> PVar $ Symbol $ show t
      Just t' -> hTypeToFormula ss t'

    expandSyn :: [(HSymbol, ([HSymbol], HType, a))] -> HType -> [HType] -> Maybe HType
    expandSyn ss (HTApp f a) as = expandSyn ss f (a:as)
    expandSyn ss (HTCon c) as = case lookup c ss of
      Just (vs, t, _) | length vs == length as -> Just $ substHT (zip vs as) t
      _ -> Nothing
    expandSyn _ _ _ = Nothing

    substHT :: [(HSymbol, HType)] -> HType -> HType
    substHT r (HTApp f a) = hTApp (substHT r f) (substHT r a)
    substHT r t@(HTVar v) = case lookup v r of
      Nothing -> t
      Just t' -> t'
    substHT _ t@(HTCon _) = t
    substHT r (HTTuple ts) = HTTuple (map (substHT r) ts)
    substHT r (HTArrow f a) = HTArrow (substHT r f) (substHT r a)
    substHT r (HTUnion (ctss)) = HTUnion [ (c, map (substHT r) ts) | (c, ts) <- ctss ]
    substHT _ t@(HTAbstract _ _) = t

    hTApp :: HType -> HType -> HType
    hTApp (HTApp (HTCon "->") a) b = HTArrow a b
    hTApp a b = HTApp a b

    -------------------------------

    data HClause = HClause HSymbol [HPat] HExpr
                 deriving (Show, Eq)

    data HPat = HPVar HSymbol
              | HPCon HSymbol
              | HPTuple [HPat]
              | HPAt HSymbol HPat
              | HPApply HPat HPat
              deriving (Show, Eq)

    data HExpr = HELam [HPat] HExpr
               | HEApply HExpr HExpr
               | HECon HSymbol
               | HEVar HSymbol
               | HETuple [HExpr]
               | HECase HExpr [(HPat, HExpr)]
               deriving (Show, Eq)

    hPrClause :: HClause -> String
    hPrClause c = renderStyle style $ ppClause 0 c

    ppClause :: Int -> HClause -> Doc
    ppClause _p (HClause f ps e) = text (prHSymbolOp f) <+> sep [sep (map (ppPat 10) ps) <+> text "=",
                                                                    nest 2 $ ppExpr 0 e]

    prHSymbolOp :: HSymbol -> String
    prHSymbolOp s@(c:_) | not (isAlphaNum c) = "(" ++ s ++ ")"
    prHSymbolOp s = s

    ppPat :: Int -> HPat -> Doc
    ppPat _ (HPVar s) = text s
    ppPat _ (HPCon s) = text s
    ppPat _ (HPTuple ps) = parens $ fsep $ punctuate comma (map (ppPat 0) ps)
    ppPat _ (HPAt s p) = text s <> text "@" <> ppPat 10 p
    ppPat p (HPApply a b) = pparens (p > 1) $ ppPat 1 a <+> ppPat 2 b

    hPrExpr :: HExpr -> String
    hPrExpr e = renderStyle style $ ppExpr 0 e

    ppExpr :: Int -> HExpr -> Doc
    ppExpr p (HELam ps e) = pparens (p > 0) $ sep [ text "\\" <+> sep (map (ppPat 10) ps) <+> text "->",
                                                    ppExpr 0 e]
    ppExpr p (HEApply (HEApply (HEVar f@(c:_)) a1) a2) | not (isAlphaNum c) =
         pparens (p > 4) $ ppExpr 5 a1 <+> text f <+> ppExpr 5 a2
    ppExpr p (HEApply f a) = pparens (p > 11) $ ppExpr 11 f <+> ppExpr 12 a
    ppExpr _ (HECon s) = text s
    ppExpr _ (HEVar s@(c:_)) | not (isAlphaNum c) = pparens True $ text s
    ppExpr _ (HEVar s) = text s
    ppExpr _ (HETuple es) = parens $ fsep $ punctuate comma (map (ppExpr 0) es)
    ppExpr p (HECase s alts) = pparens (p > 0) $ (text "case" <+> ppExpr 0 s <+> text "of") $$
                                nest 2 (vcat (map ppAlt alts))
      where ppAlt (pp, e) = ppPat 0 pp <+> text "->" <+> ppExpr 0 e

    pparens :: Bool -> Doc -> Doc
    pparens True d = parens d
    pparens False d = d

    -------------------------------

    unSymbol :: Symbol -> HSymbol
    unSymbol (Symbol s) = s

    termToHExpr :: Term -> HExpr
    termToHExpr term = niceNames $ etaReduce $ remUnusedVars $ collapeCase $ fixSillyAt $ remUnusedVars $ fst $ conv [] term
      where conv _vs (Var s) = (HEVar $ unSymbol s, [])
            conv vs (Lam s te) =
              let hs = unSymbol s
                  (te', ss) = conv (hs : vs) te
               in (hELam [convV hs ss] te', ss)
            conv vs (Apply (Cinj (ConsDesc s n) _) a) = (f $ foldl HEApply (HECon s) as, ss)
              where (f, as) = unTuple n ha
                    (ha, ss) = conv vs a
            conv vs (Apply te1 te2) = convAp vs te1 [te2]
            conv _vs (Ctuple 0) = (HECon "()", [])
            conv _vs e = error $ "termToHExpr " ++ show e

            unTuple 0 _ = (id, [])
            unTuple 1 a = (id, [a])
            unTuple n (HETuple as) | length as == n = (id, as)
            unTuple n e = error $ "unTuple: unimplemented " ++ show (n, e)

            unTupleP 0 _ = []
    --      unTupleP 1 p = [p]
            unTupleP n (HPTuple ps) | length ps == n = ps
            unTupleP n p = error $ "unTupleP: unimplemented " ++ show (n, p)

            convAp vs (Apply te1 te2) as = convAp vs te1 (te2:as)
            convAp vs (Ctuple n) as | length as == n =
              let (es, sss) = unzip $ map (conv vs) as
               in (hETuple es, concat sss)
            convAp vs (Ccases cds) (se : es) =
              let (alts, ass) = unzip $ zipWith cAlt es cds
                  cAlt (Lam v e) (ConsDesc c n) =
                    let hv = unSymbol v
                        (he, ss) = conv (hv : vs) e
                        ps = case lookup hv ss of
                               Nothing -> replicate n (HPVar "_")
                               Just p -> unTupleP n p
                     in ((foldl HPApply (HPCon c) ps, he), ss)
                  cAlt e _ = error $ "cAlt " ++ show e
                  (e', ess) = conv vs se
               in (hECase e' alts, ess ++ concat ass)
            convAp vs (Csplit n) (b : a : as) =
              let (hb, sb) = conv vs b
                  (a', sa) = conv vs a
                  (as', sss) = unzip $ map (conv vs) as
                  (ps, b') = unLam n hb
                  unLam 0 e = ([], e)
                  unLam k (HELam ps0 e) | length ps0 >= n = let (ps1, ps2) = splitAt k ps0 in (ps1, hELam ps2 e)
                  unLam k e = error $ "unLam: unimplemented" ++ show (k, e)
               in case a' of
                    HEVar v | v `elem` vs && null as -> (b', [(v, HPTuple ps)] ++ sb ++ sa)
                    _ -> (foldr HEApply (hECase a' [(HPTuple ps, b')]) as', sb ++ sa ++ concat sss)

            convAp vs f as =
              let (es, sss) = unzip $ map (conv vs) (f:as)
              in (foldl1 HEApply es, concat sss)

            convV hs ss = case [ y | (x, y) <- ss, x == hs ] of
              []  -> HPVar hs
              [p] -> HPAt hs p
              ps  -> HPAt hs $ foldr1 combPat ps

            combPat p p' | p == p'             = p
            combPat (HPVar v) p                = HPAt v p
            combPat p (HPVar v)                = HPAt v p
            combPat (HPTuple ps) (HPTuple ps') = HPTuple (zipWith combPat ps ps')
            combPat p p'                       = error $ "unimplemented combPat: " ++ show (p, p')

            hETuple [e] = e
            hETuple es = HETuple es

    -- XXX This should be integrated into some earlier phase, but this is simpler.
    fixSillyAt :: HExpr -> HExpr
    fixSillyAt = fixAt []
      where fixAt s (HELam ps e) = HELam ps' (fixAt (concat ss ++ s) e) where (ps', ss) = unzip $ map findSilly ps
            fixAt s (HEApply f a) = HEApply (fixAt s f) (fixAt s a)
            fixAt _ e@(HECon _) = e
            fixAt s e@(HEVar v) = maybe e HEVar $ lookup v s
            fixAt s (HETuple es) = HETuple (map (fixAt s) es)
            fixAt s (HECase e alts) = HECase (fixAt s e) (map (fixAtAlt s) alts)
            fixAtAlt s (p, e) = (p', fixAt (s' ++ s) e) where (p', s') = findSilly p
            findSilly p@(HPVar _) = (p, [])
            findSilly p@(HPCon _) = (p, [])
            findSilly (HPTuple ps) = (HPTuple ps', concat ss) where (ps', ss) = unzip $ map findSilly ps
            findSilly (HPAt v p) = case findSilly p of
                                     (p'@(HPVar v'), s) -> (p', (v, v'):s)
                                     (p', s)            -> (HPAt v p', s)
            findSilly (HPApply f a) = (HPApply f' a', sf ++ sa) where (f', sf) = findSilly f; (a', sa) = findSilly a

    -- XXX This shouldn't be needed.  There's similar code in hECase,
    -- but the fixSillyAt reveals new opportunities.
    collapeCase :: HExpr -> HExpr
    collapeCase (HELam ps e) = HELam ps (collapeCase e)
    collapeCase (HEApply f a) = HEApply (collapeCase f) (collapeCase a)
    collapeCase e@(HECon _) = e
    collapeCase e@(HEVar _) = e
    collapeCase (HETuple es) = HETuple (map collapeCase es)
    collapeCase (HECase e alts) = case [(p, collapeCase b) | (p, b) <- alts ] of
        (p, b) : pes | noBound p && all (\ (p', b') -> alphaEq b b' && noBound p') pes -> b
        pes -> HECase (collapeCase e) pes
      where noBound = all (== "_") . getBinderVarsHP

    niceNames :: HExpr -> HExpr
    niceNames e =
      let bvars = filter (/= "_") $ getBinderVarsHE e
          nvars = [[c] | c <- ['a'..'z']] ++ [ "x" ++ show i | i <- [1::Integer ..]]
          freevars = getAllVars e \\ bvars
          vars = nvars \\ freevars
          sub = zip bvars vars
       in hESubst sub e

    hELam :: [HPat] -> HExpr -> HExpr
    hELam [] e = e
    hELam ps (HELam ps' e) = HELam (ps ++ ps') e
    hELam ps e = HELam ps e

    hECase :: HExpr -> [(HPat, HExpr)] -> HExpr
    hECase e [] = HEApply (HEVar "void") e
    hECase _ [(HPCon "()", e)] = e
    hECase e pes | all (uncurry eqPatExpr) pes = e
    hECase e [(p, HELam ps b)] = HELam ps $ hECase e [(p, b)]
    hECase se alts@((_, HELam ops _):_) | m > 0 = HELam (take m ops) $ hECase se alts'
      where m = minimum (map (numBind . snd) alts)
            numBind (HELam ps _) = length (takeWhile isPVar ps)
            numBind _ = 0
            isPVar (HPVar _) = True
            isPVar _ = False
            alts' = [ let (ps1, ps2) = splitAt m ps in (cps, hELam ps2 $ hESubst (zipWith (\ (HPVar v) n -> (v, n)) ps1 ns) e)
                      | (cps, HELam ps e) <- alts ]
            ns = [ n | HPVar n <- take m ops ]
    -- if all arms are equal and there are at least two alternatives there can be no bound vars
    -- from the patterns
    hECase _ ((_,e):alts@(_:_)) | all (alphaEq e . snd) alts = e
    hECase e alts = HECase e alts

    eqPatExpr :: HPat -> HExpr -> Bool
    eqPatExpr (HPVar s) (HEVar s') = s == s'
    eqPatExpr (HPCon s) (HECon s') = s == s'
    eqPatExpr (HPTuple ps) (HETuple es) = and (zipWith eqPatExpr ps es)
    eqPatExpr (HPApply pf pa) (HEApply ef ea) = eqPatExpr pf ef && eqPatExpr pa ea
    eqPatExpr _ _ = False

    alphaEq :: HExpr -> HExpr -> Bool
    alphaEq e1 e2 | e1 == e2 = True
    alphaEq (HELam ps1 e1) (HELam ps2 e2) =
      Nothing /= do
          s <- matchPat (HPTuple ps1) (HPTuple ps2)
          if alphaEq (hESubst s e1) e2
             then return ()
             else Nothing
    alphaEq (HEApply f1 a1) (HEApply f2 a2) = alphaEq f1 f2 && alphaEq a1 a2
    alphaEq (HECon s1) (HECon s2) = s1 == s2
    alphaEq (HEVar s1) (HEVar s2) = s1 == s2
    alphaEq (HETuple es1) (HETuple es2) | length es1 == length es2 = and (zipWith alphaEq es1 es2)
    alphaEq (HECase e1 alts1) (HECase e2 alts2) =
        alphaEq e1 e2 && and (zipWith alphaEq [ HELam [p] e | (p, e) <- alts1 ] [ HELam [p] e | (p, e) <- alts2 ])
    alphaEq _ _ = False

    matchPat :: HPat -> HPat -> Maybe [(HSymbol, HSymbol)]
    matchPat (HPVar s1) (HPVar s2) = return [(s1, s2)]
    matchPat (HPCon s1) (HPCon s2) | s1 == s2 = return []
    matchPat (HPTuple ps1) (HPTuple ps2) | length ps1 == length ps2 = do
      ss <- zipWithM matchPat ps1 ps2
      return $ concat ss
    matchPat (HPAt s1 p1) (HPAt s2 p2) = do
      s <- matchPat p1 p2
      return $ (s1, s2) : s
    matchPat (HPApply f1 a1) (HPApply f2 a2) = do
      s1 <- matchPat f1 f2
      s2 <- matchPat a1 a2
      return $ s1 ++ s2
    matchPat _ _ = Nothing

    hESubst :: [(HSymbol, HSymbol)] -> HExpr -> HExpr
    hESubst s (HELam ps e) = HELam (map (hPSubst s) ps) (hESubst s e)
    hESubst s (HEApply f a) = HEApply (hESubst s f) (hESubst s a)
    hESubst _ e@(HECon _) = e
    hESubst s (HEVar v) = HEVar $ maybe v id $ lookup v s
    hESubst s (HETuple es) = HETuple (map (hESubst s) es)
    hESubst s (HECase e alts) = HECase (hESubst s e) [(hPSubst s p, hESubst s b) | (p, b) <- alts]

    hPSubst :: [(HSymbol, HSymbol)] -> HPat -> HPat
    hPSubst s (HPVar v) = HPVar $ maybe v id $ lookup v s
    hPSubst _ p@(HPCon _) = p
    hPSubst s (HPTuple ps) = HPTuple (map (hPSubst s) ps)
    hPSubst s (HPAt v p) = HPAt (maybe v id $ lookup v s) (hPSubst s p)
    hPSubst s (HPApply f a) = HPApply (hPSubst s f) (hPSubst s a)

    termToHClause :: HSymbol -> Term -> HClause
    termToHClause i term =
      case termToHExpr term of
      HELam ps e -> HClause i ps e
      e -> HClause i [] e

    remUnusedVars :: HExpr -> HExpr
    remUnusedVars expr = fst $ remE expr
      where remE (HELam ps e) =
              let (e', vs) = remE e
               in (HELam (map (remP vs) ps) e', vs)
            remE (HEApply f a) =
              let (f', fs) = remE f
                  (a', as) = remE a
               in (HEApply f' a', fs ++ as)
            remE (HETuple es) =
              let (es', sss) = unzip (map remE es)
               in (HETuple es', concat sss)
            remE (HECase e alts) =
              let (e', es) = remE e
                  (alts', sss) = unzip [ let (ee', ss) = remE ee in ((remP ss p, ee'), ss) | (p, ee) <- alts ]
               in case alts' of
                    [(HPVar "_", b)] -> (b, concat sss)
                    _ -> (hECase e' alts', es ++ concat sss)
            remE e@(HECon _) = (e, [])
            remE e@(HEVar v) = (e, [v])
            remP vs p@(HPVar v) = if v `elem` vs then p else HPVar "_"
            remP _vs p@(HPCon _) = p
            remP vs (HPTuple ps) = hPTuple (map (remP vs) ps)
            remP vs (HPAt v p) = if v `elem` vs then HPAt v (remP vs p) else remP vs p
            remP vs (HPApply f a) = HPApply (remP vs f) (remP vs a)
            hPTuple ps | all (== HPVar "_") ps = HPVar "_"
            hPTuple ps = HPTuple ps

    getBinderVars :: HClause -> [HSymbol]
    getBinderVars (HClause _ pats expr) = concatMap getBinderVarsHP pats ++ getBinderVarsHE expr

    getBinderVarsHE :: HExpr -> [HSymbol]
    getBinderVarsHE expr = gbExp expr
      where gbExp (HELam ps e)     = concatMap getBinderVarsHP ps ++ gbExp e
            gbExp (HEApply f a)    = gbExp f ++ gbExp a
            gbExp (HETuple es)     = concatMap gbExp es
            gbExp (HECase se alts) = gbExp se ++ concatMap (\ (p, e) -> getBinderVarsHP p ++ gbExp e) alts
            gbExp _ = []

    getBinderVarsHP :: HPat -> [HSymbol]
    getBinderVarsHP pat = gbPat pat
      where gbPat (HPVar s)     = [s]
            gbPat (HPCon _)     = []
            gbPat (HPTuple ps)  = concatMap gbPat ps
            gbPat (HPAt s p)    = s : gbPat p
            gbPat (HPApply f a) = gbPat f ++ gbPat a

    getAllVars :: HExpr -> [HSymbol]
    getAllVars expr = gaExp expr
      where gaExp (HELam _ps e)    = gaExp e
            gaExp (HEApply f a)    = gaExp f `union` gaExp a
            gaExp (HETuple es)     = foldr union [] (map gaExp es)
            gaExp (HECase se alts) = foldr union (gaExp se) (map (\ (_p, e) -> gaExp e) alts)
            gaExp (HEVar s)        = [s]
            gaExp _                = []

    etaReduce :: HExpr -> HExpr
    etaReduce expr = fst $ eta expr
      where eta (HELam [HPVar v] (HEApply f (HEVar v'))) | v == v' && v `notElem` vs = (f', vs)
                where (f', vs) = eta f
            eta (HELam ps e)    = (HELam ps e', vs) where (e', vs) = eta e
            eta (HEApply f a)   = (HEApply f' a', fvs++avs) where (f', fvs) = eta f; (a', avs) = eta a
            eta e@(HECon _)     = (e, [])
            eta e@(HEVar s)     = (e, [s])
            eta (HETuple es)    = (HETuple es', concat vss) where (es', vss) = unzip $ map eta es
            eta (HECase e alts) = (HECase e' alts', vs ++ concat vss)
              where (e', vs) = eta e
                    (alts', vss) = unzip $ [ let (a', ss) = eta a in ((p, a'), ss) | (p, a) <- alts ]