    {-# 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, (\\))
    #if 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 (HKind -> HKind -> Bool
    (HKind -> HKind -> Bool) -> (HKind -> HKind -> Bool) -> Eq HKind
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: HKind -> HKind -> Bool
    == :: HKind -> HKind -> Bool
    $c/= :: HKind -> HKind -> Bool
    /= :: HKind -> HKind -> Bool
    Eq, Int -> HKind -> ShowS
    [HKind] -> ShowS
    HKind -> HSymbol
    (Int -> HKind -> ShowS)
    -> (HKind -> HSymbol) -> ([HKind] -> ShowS) -> Show HKind
    forall a.
    (Int -> a -> ShowS) -> (a -> HSymbol) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> HKind -> ShowS
    showsPrec :: Int -> HKind -> ShowS
    $cshow :: HKind -> HSymbol
    show :: HKind -> HSymbol
    $cshowList :: [HKind] -> ShowS
    showList :: [HKind] -> ShowS
    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 (HType -> HType -> Bool
    (HType -> HType -> Bool) -> (HType -> HType -> Bool) -> Eq HType
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: HType -> HType -> Bool
    == :: HType -> HType -> Bool
    $c/= :: HType -> HType -> Bool
    /= :: HType -> HType -> Bool
    Eq)

    isHTUnion :: HType -> Bool
    isHTUnion :: HType -> Bool
    isHTUnion (HTUnion [(HSymbol, [HType])]
    _) = Bool
    True
    isHTUnion HType
    _ = Bool
    False

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

    instance Show HType where
      showsPrec :: Int -> HType -> ShowS
    showsPrec Int
    _ (HTApp (HTCon HSymbol
    "[]") HType
    t) = HSymbol -> ShowS
    showString HSymbol
    "[" ShowS -> ShowS -> ShowS
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> HType -> ShowS
    forall a. Show a => Int -> a -> ShowS
    showsPrec Int
    0 HType
    t ShowS -> ShowS -> ShowS
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . HSymbol -> ShowS
    showString HSymbol
    "]"
      showsPrec Int
    p (HTApp HType
    f HType
    a) = Bool -> ShowS -> ShowS
    showParen (Int
    p Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int
    2) (ShowS -> ShowS) -> ShowS -> ShowS
    forall a b. (a -> b) -> a -> b
    $ Int -> HType -> ShowS
    forall a. Show a => Int -> a -> ShowS
    showsPrec Int
    2 HType
    f ShowS -> ShowS -> ShowS
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . HSymbol -> ShowS
    showString HSymbol
    " " ShowS -> ShowS -> ShowS
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> HType -> ShowS
    forall a. Show a => Int -> a -> ShowS
    showsPrec Int
    3 HType
    a
      showsPrec Int
    _ (HTVar HSymbol
    s) = HSymbol -> ShowS
    showString HSymbol
    s
      showsPrec Int
    _ (HTCon s :: HSymbol
    s@(Char
    c:HSymbol
    _)) | Bool -> Bool
    not (Char -> Bool
    isAlpha Char
    c) = Bool -> ShowS -> ShowS
    showParen Bool
    True (ShowS -> ShowS) -> ShowS -> ShowS
    forall a b. (a -> b) -> a -> b
    $ HSymbol -> ShowS
    showString HSymbol
    s
      showsPrec Int
    _ (HTCon HSymbol
    s) = HSymbol -> ShowS
    showString HSymbol
    s
      showsPrec Int
    _ (HTTuple [HType]
    ss) = Bool -> ShowS -> ShowS
    showParen Bool
    True (ShowS -> ShowS) -> ShowS -> ShowS
    forall a b. (a -> b) -> a -> b
    $ [HType] -> ShowS
    forall {a}. Show a => [a] -> ShowS
    f [HType]
    ss
        where f :: [a] -> ShowS
    f []     = HSymbol -> ShowS
    forall a. HasCallStack => HSymbol -> a
    error HSymbol
    "showsPrec HType"
              f [a
    t]    = Int -> a -> ShowS
    forall a. Show a => Int -> a -> ShowS
    showsPrec Int
    0 a
    t
              f (a
    t:[a]
    ts) = Int -> a -> ShowS
    forall a. Show a => Int -> a -> ShowS
    showsPrec Int
    0 a
    t ShowS -> ShowS -> ShowS
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . HSymbol -> ShowS
    showString HSymbol
    ", " ShowS -> ShowS -> ShowS
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [a] -> ShowS
    f [a]
    ts
      showsPrec Int
    p (HTArrow HType
    s HType
    t) = Bool -> ShowS -> ShowS
    showParen (Int
    p Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int
    0) (ShowS -> ShowS) -> ShowS -> ShowS
    forall a b. (a -> b) -> a -> b
    $ Int -> HType -> ShowS
    forall a. Show a => Int -> a -> ShowS
    showsPrec Int
    1 HType
    s ShowS -> ShowS -> ShowS
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . HSymbol -> ShowS
    showString HSymbol
    " -> " ShowS -> ShowS -> ShowS
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> HType -> ShowS
    forall a. Show a => Int -> a -> ShowS
    showsPrec Int
    0 HType
    t
      showsPrec Int
    _ (HTUnion [(HSymbol, [HType])]
    cs) = [(HSymbol, [HType])] -> ShowS
    forall {t :: * -> *} {a}.
    (Foldable t, Show a) =>
    [(HSymbol, t a)] -> ShowS
    f [(HSymbol, [HType])]
    cs
        where f :: [(HSymbol, t a)] -> ShowS
    f []           = ShowS
    forall a. a -> a
    id
              f [(HSymbol, t a)
    cts]        = (HSymbol, t a) -> ShowS
    forall {t :: * -> *} {a}.
    (Foldable t, Show a) =>
    (HSymbol, t a) -> ShowS
    scts (HSymbol, t a)
    cts
              f ((HSymbol, t a)
    cts : [(HSymbol, t a)]
    ctss) = (HSymbol, t a) -> ShowS
    forall {t :: * -> *} {a}.
    (Foldable t, Show a) =>
    (HSymbol, t a) -> ShowS
    scts (HSymbol, t a)
    cts ShowS -> ShowS -> ShowS
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . HSymbol -> ShowS
    showString HSymbol
    " | " ShowS -> ShowS -> ShowS
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [(HSymbol, t a)] -> ShowS
    f [(HSymbol, t a)]
    ctss
              scts :: (HSymbol, t a) -> ShowS
    scts (HSymbol
    c, t a
    ts)   = (ShowS -> a -> ShowS) -> ShowS -> t a -> ShowS
    forall b a. (b -> a -> b) -> b -> t a -> b
    forall (t :: * -> *) b a.
    Foldable t =>
    (b -> a -> b) -> b -> t a -> b
    foldl (\ ShowS
    s a
    t -> ShowS
    s ShowS -> ShowS -> ShowS
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . HSymbol -> ShowS
    showString HSymbol
    " " ShowS -> ShowS -> ShowS
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> a -> ShowS
    forall a. Show a => Int -> a -> ShowS
    showsPrec Int
    10 a
    t) (HSymbol -> ShowS
    showString HSymbol
    c) t a
    ts
      showsPrec Int
    _ (HTAbstract HSymbol
    s HKind
    _) = HSymbol -> ShowS
    showString HSymbol
    s

    instance Read HType where
      readsPrec :: Int -> ReadS HType
    readsPrec Int
    _ = ReadP HType -> ReadS HType
    forall a. ReadP a -> ReadS a
    readP_to_S ReadP HType
    pHType'

    pHType' :: ReadP HType
    pHType' :: ReadP HType
    pHType' = do
      HType
    t <- ReadP HType
    pHType
      ReadP ()
    skipSpaces
      HType -> ReadP HType
    forall a. a -> ReadP a
    forall (m :: * -> *) a. Monad m => a -> m a
    return HType
    t

    pHType :: ReadP HType
    pHType :: ReadP HType
    pHType = do
      [HType]
    ts <- ReadP HType -> ReadP Char -> ReadP [HType]
    forall a sep. ReadP a -> ReadP sep -> ReadP [a]
    sepBy1 ReadP HType
    pHTypeApp (do Char -> ReadP ()
    schar Char
    '-'; Char -> ReadP Char
    char Char
    '>')
      HType -> ReadP HType
    forall a. a -> ReadP a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (HType -> ReadP HType) -> HType -> ReadP HType
    forall a b. (a -> b) -> a -> b
    $ (HType -> HType -> HType) -> [HType] -> HType
    forall a. (a -> a -> a) -> [a] -> a
    forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
    foldr1 HType -> HType -> HType
    HTArrow [HType]
    ts

    pHDataType :: ReadP HType
    pHDataType :: ReadP HType
    pHDataType = do
      let con :: ReadP (HSymbol, [HType])
    con = do HSymbol
    c <- Bool -> ReadP HSymbol
    pHSymbol Bool
    True
                   [HType]
    ts <- ReadP HType -> ReadP [HType]
    forall a. ReadP a -> ReadP [a]
    many ReadP HType
    pHTAtom
                   (HSymbol, [HType]) -> ReadP (HSymbol, [HType])
    forall a. a -> ReadP a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (HSymbol
    c, [HType]
    ts)
      [(HSymbol, [HType])]
    cts <- ReadP (HSymbol, [HType]) -> ReadP () -> ReadP [(HSymbol, [HType])]
    forall a sep. ReadP a -> ReadP sep -> ReadP [a]
    sepBy ReadP (HSymbol, [HType])
    con (Char -> ReadP ()
    schar Char
    '|')
      HType -> ReadP HType
    forall a. a -> ReadP a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (HType -> ReadP HType) -> HType -> ReadP HType
    forall a b. (a -> b) -> a -> b
    $ [(HSymbol, [HType])] -> HType
    HTUnion [(HSymbol, [HType])]
    cts

    pHTAtom :: ReadP HType
    pHTAtom :: ReadP HType
    pHTAtom = ReadP HType
    pHTVar ReadP HType -> ReadP HType -> ReadP HType
    forall a. ReadP a -> ReadP a -> ReadP a
    +++ ReadP HType
    pHTCon ReadP HType -> ReadP HType -> ReadP HType
    forall a. ReadP a -> ReadP a -> ReadP a
    +++ ReadP HType
    pHTList ReadP HType -> ReadP HType -> ReadP HType
    forall a. ReadP a -> ReadP a -> ReadP a
    +++ ReadP HType -> ReadP HType
    forall a. ReadP a -> ReadP a
    pParen ReadP HType
    pHTTuple ReadP HType -> ReadP HType -> ReadP HType
    forall a. ReadP a -> ReadP a -> ReadP a
    +++ ReadP HType -> ReadP HType
    forall a. ReadP a -> ReadP a
    pParen ReadP HType
    pHType ReadP HType -> ReadP HType -> ReadP HType
    forall a. ReadP a -> ReadP a -> ReadP a
    +++ ReadP HType
    pUnit

    pUnit :: ReadP HType
    pUnit :: ReadP HType
    pUnit = do
      Char -> ReadP ()
    schar Char
    '('
      Char -> ReadP Char
    char Char
    ')'
      HType -> ReadP HType
    forall a. a -> ReadP a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (HType -> ReadP HType) -> HType -> ReadP HType
    forall a b. (a -> b) -> a -> b
    $ HSymbol -> HType
    HTCon HSymbol
    "()"

    pHTCon :: ReadP HType
    pHTCon :: ReadP HType
    pHTCon = (Bool -> ReadP HSymbol
    pHSymbol Bool
    True ReadP HSymbol -> (HSymbol -> ReadP HType) -> ReadP HType
    forall a b. ReadP a -> (a -> ReadP b) -> ReadP b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= HType -> ReadP HType
    forall a. a -> ReadP a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (HType -> ReadP HType)
    -> (HSymbol -> HType) -> HSymbol -> ReadP HType
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . HSymbol -> HType
    HTCon) ReadP HType -> ReadP HType -> ReadP HType
    forall a. ReadP a -> ReadP a -> ReadP a
    +++
             do Char -> ReadP ()
    schar Char
    '('; Char -> ReadP ()
    schar Char
    '-'; Char -> ReadP ()
    schar Char
    '>'; Char -> ReadP ()
    schar Char
    ')'; HType -> ReadP HType
    forall a. a -> ReadP a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (HSymbol -> HType
    HTCon HSymbol
    "->")

    pHTVar :: ReadP HType
    pHTVar :: ReadP HType
    pHTVar = Bool -> ReadP HSymbol
    pHSymbol Bool
    False ReadP HSymbol -> (HSymbol -> ReadP HType) -> ReadP HType
    forall a b. ReadP a -> (a -> ReadP b) -> ReadP b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= HType -> ReadP HType
    forall a. a -> ReadP a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (HType -> ReadP HType)
    -> (HSymbol -> HType) -> HSymbol -> ReadP HType
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . HSymbol -> HType
    HTVar

    pHSymbol :: Bool -> ReadP HSymbol
    pHSymbol :: Bool -> ReadP HSymbol
    pHSymbol Bool
    con = do
      ReadP ()
    skipSpaces
      Char
    c <- (Char -> Bool) -> ReadP Char
    satisfy ((Char -> Bool) -> ReadP Char) -> (Char -> Bool) -> ReadP Char
    forall a b. (a -> b) -> a -> b
    $ \ Char
    c -> Char -> Bool
    isAlpha Char
    c Bool -> Bool -> Bool
    && Char -> Bool
    isUpper Char
    c Bool -> Bool -> Bool
    forall a. Eq a => a -> a -> Bool
    == Bool
    con
      let isSym :: Char -> Bool
    isSym Char
    d = Char -> Bool
    isAlphaNum Char
    d Bool -> Bool -> Bool
    || Char
    d Char -> Char -> Bool
    forall a. Eq a => a -> a -> Bool
    == Char
    '\'' Bool -> Bool -> Bool
    || Char
    d Char -> Char -> Bool
    forall a. Eq a => a -> a -> Bool
    == Char
    '.'
      HSymbol
    cs <- (Char -> Bool) -> ReadP HSymbol
    munch Char -> Bool
    isSym
      HSymbol -> ReadP HSymbol
    forall a. a -> ReadP a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (HSymbol -> ReadP HSymbol) -> HSymbol -> ReadP HSymbol
    forall a b. (a -> b) -> a -> b
    $ Char
    cChar -> ShowS
    forall a. a -> [a] -> [a]
    :HSymbol
    cs

    pHTTuple :: ReadP HType
    pHTTuple :: ReadP HType
    pHTTuple = do
      HType
    t <- ReadP HType
    pHType
      [HType]
    ts <- ReadP HType -> ReadP [HType]
    forall a. ReadP a -> ReadP [a]
    many1 (do Char -> ReadP ()
    schar Char
    ','; ReadP HType
    pHType)
      HType -> ReadP HType
    forall a. a -> ReadP a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (HType -> ReadP HType) -> HType -> ReadP HType
    forall a b. (a -> b) -> a -> b
    $ [HType] -> HType
    HTTuple ([HType] -> HType) -> [HType] -> HType
    forall a b. (a -> b) -> a -> b
    $ HType
    tHType -> [HType] -> [HType]
    forall a. a -> [a] -> [a]
    :[HType]
    ts

    pHTypeApp :: ReadP HType
    pHTypeApp :: ReadP HType
    pHTypeApp = do
      [HType]
    ts <- ReadP HType -> ReadP [HType]
    forall a. ReadP a -> ReadP [a]
    many1 ReadP HType
    pHTAtom
      HType -> ReadP HType
    forall a. a -> ReadP a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (HType -> ReadP HType) -> HType -> ReadP HType
    forall a b. (a -> b) -> a -> b
    $ (HType -> HType -> HType) -> [HType] -> HType
    forall a. (a -> a -> a) -> [a] -> a
    forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
    foldl1 HType -> HType -> HType
    HTApp [HType]
    ts

    pHTList :: ReadP HType
    pHTList :: ReadP HType
    pHTList = do
      Char -> ReadP ()
    schar Char
    '['
      HType
    t <- ReadP HType
    pHType
      Char -> ReadP ()
    schar Char
    ']'
      HType -> ReadP HType
    forall a. a -> ReadP a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (HType -> ReadP HType) -> HType -> ReadP HType
    forall a b. (a -> b) -> a -> b
    $ HType -> HType -> HType
    HTApp (HSymbol -> HType
    HTCon HSymbol
    "[]") HType
    t

    pHKind :: ReadP HKind
    pHKind :: ReadP HKind
    pHKind = do
      [HKind]
    ts <- ReadP HKind -> ReadP Char -> ReadP [HKind]
    forall a sep. ReadP a -> ReadP sep -> ReadP [a]
    sepBy1 ReadP HKind
    pHKindA (do Char -> ReadP ()
    schar Char
    '-'; Char -> ReadP Char
    char Char
    '>')
      HKind -> ReadP HKind
    forall a. a -> ReadP a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (HKind -> ReadP HKind) -> HKind -> ReadP HKind
    forall a b. (a -> b) -> a -> b
    $ (HKind -> HKind -> HKind) -> [HKind] -> HKind
    forall a. (a -> a -> a) -> [a] -> a
    forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
    foldr1 HKind -> HKind -> HKind
    KArrow [HKind]
    ts

    pHKindA :: ReadP HKind
    pHKindA :: ReadP HKind
    pHKindA = (do Char -> ReadP ()
    schar Char
    '*'; HKind -> ReadP HKind
    forall a. a -> ReadP a
    forall (m :: * -> *) a. Monad m => a -> m a
    return HKind
    KStar) ReadP HKind -> ReadP HKind -> ReadP HKind
    forall a. ReadP a -> ReadP a -> ReadP a
    +++ ReadP HKind -> ReadP HKind
    forall a. ReadP a -> ReadP a
    pParen ReadP HKind
    pHKind

    pParen :: ReadP a -> ReadP a
    pParen :: forall a. ReadP a -> ReadP a
    pParen ReadP a
    p = do
      Char -> ReadP ()
    schar Char
    '('
      a
    e <- ReadP a
    p
      Char -> ReadP ()
    schar Char
    ')'
      a -> ReadP a
    forall a. a -> ReadP a
    forall (m :: * -> *) a. Monad m => a -> m a
    return a
    e

    schar :: Char -> ReadP ()
    schar :: Char -> ReadP ()
    schar Char
    c = do
      ReadP ()
    skipSpaces
      Char -> ReadP Char
    char Char
    c
      () -> ReadP ()
    forall a. a -> ReadP a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()

    getHTVars :: HType -> [HSymbol]
    getHTVars :: HType -> [HSymbol]
    getHTVars (HTApp HType
    f HType
    a)   = HType -> [HSymbol]
    getHTVars HType
    f [HSymbol] -> [HSymbol] -> [HSymbol]
    forall a. Eq a => [a] -> [a] -> [a]
    `union` HType -> [HSymbol]
    getHTVars HType
    a
    getHTVars (HTVar HSymbol
    v)     = [HSymbol
    v]
    getHTVars (HTCon HSymbol
    _)     = []
    getHTVars (HTTuple [HType]
    ts)  = ([HSymbol] -> [HSymbol] -> [HSymbol])
    -> [HSymbol] -> [[HSymbol]] -> [HSymbol]
    forall a b. (a -> b -> b) -> b -> [a] -> b
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr [HSymbol] -> [HSymbol] -> [HSymbol]
    forall a. Eq a => [a] -> [a] -> [a]
    union [] ((HType -> [HSymbol]) -> [HType] -> [[HSymbol]]
    forall a b. (a -> b) -> [a] -> [b]
    map HType -> [HSymbol]
    getHTVars [HType]
    ts)
    getHTVars (HTArrow HType
    f HType
    a) = HType -> [HSymbol]
    getHTVars HType
    f [HSymbol] -> [HSymbol] -> [HSymbol]
    forall a. Eq a => [a] -> [a] -> [a]
    `union` HType -> [HSymbol]
    getHTVars HType
    a
    getHTVars HType
    _             = HSymbol -> [HSymbol]
    forall a. HasCallStack => HSymbol -> a
    error HSymbol
    "getHTVars"

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

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

    expandSyn :: [(HSymbol, ([HSymbol], HType, a))] -> HType -> [HType] -> Maybe HType
    expandSyn :: forall a.
    [(HSymbol, ([HSymbol], HType, a))]
    -> HType -> [HType] -> Maybe HType
    expandSyn [(HSymbol, ([HSymbol], HType, a))]
    ss (HTApp HType
    f HType
    a) [HType]
    as = [(HSymbol, ([HSymbol], HType, a))]
    -> HType -> [HType] -> Maybe HType
    forall a.
    [(HSymbol, ([HSymbol], HType, a))]
    -> HType -> [HType] -> Maybe HType
    expandSyn [(HSymbol, ([HSymbol], HType, a))]
    ss HType
    f (HType
    aHType -> [HType] -> [HType]
    forall a. a -> [a] -> [a]
    :[HType]
    as)
    expandSyn [(HSymbol, ([HSymbol], HType, a))]
    ss (HTCon HSymbol
    c) [HType]
    as = case HSymbol
    -> [(HSymbol, ([HSymbol], HType, a))]
    -> Maybe ([HSymbol], HType, a)
    forall a b. Eq a => a -> [(a, b)] -> Maybe b
    lookup HSymbol
    c [(HSymbol, ([HSymbol], HType, a))]
    ss of
      Just ([HSymbol]
    vs, HType
    t, a
    _) | [HSymbol] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [HSymbol]
    vs Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == [HType] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [HType]
    as -> HType -> Maybe HType
    forall a. a -> Maybe a
    Just (HType -> Maybe HType) -> HType -> Maybe HType
    forall a b. (a -> b) -> a -> b
    $ [(HSymbol, HType)] -> HType -> HType
    substHT ([HSymbol] -> [HType] -> [(HSymbol, HType)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [HSymbol]
    vs [HType]
    as) HType
    t
      Maybe ([HSymbol], HType, a)
    _ -> Maybe HType
    forall a. Maybe a
    Nothing
    expandSyn [(HSymbol, ([HSymbol], HType, a))]
    _ HType
    _ [HType]
    _ = Maybe HType
    forall a. Maybe a
    Nothing

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

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

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

    data HClause = HClause HSymbol [HPat] HExpr
                 deriving (Int -> HClause -> ShowS
    [HClause] -> ShowS
    HClause -> HSymbol
    (Int -> HClause -> ShowS)
    -> (HClause -> HSymbol) -> ([HClause] -> ShowS) -> Show HClause
    forall a.
    (Int -> a -> ShowS) -> (a -> HSymbol) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> HClause -> ShowS
    showsPrec :: Int -> HClause -> ShowS
    $cshow :: HClause -> HSymbol
    show :: HClause -> HSymbol
    $cshowList :: [HClause] -> ShowS
    showList :: [HClause] -> ShowS
    Show, HClause -> HClause -> Bool
    (HClause -> HClause -> Bool)
    -> (HClause -> HClause -> Bool) -> Eq HClause
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: HClause -> HClause -> Bool
    == :: HClause -> HClause -> Bool
    $c/= :: HClause -> HClause -> Bool
    /= :: HClause -> HClause -> Bool
    Eq)

    data HPat = HPVar HSymbol
              | HPCon HSymbol
              | HPTuple [HPat]
              | HPAt HSymbol HPat
              | HPApply HPat HPat
              deriving (Int -> HPat -> ShowS
    [HPat] -> ShowS
    HPat -> HSymbol
    (Int -> HPat -> ShowS)
    -> (HPat -> HSymbol) -> ([HPat] -> ShowS) -> Show HPat
    forall a.
    (Int -> a -> ShowS) -> (a -> HSymbol) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> HPat -> ShowS
    showsPrec :: Int -> HPat -> ShowS
    $cshow :: HPat -> HSymbol
    show :: HPat -> HSymbol
    $cshowList :: [HPat] -> ShowS
    showList :: [HPat] -> ShowS
    Show, HPat -> HPat -> Bool
    (HPat -> HPat -> Bool) -> (HPat -> HPat -> Bool) -> Eq HPat
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: HPat -> HPat -> Bool
    == :: HPat -> HPat -> Bool
    $c/= :: HPat -> HPat -> Bool
    /= :: HPat -> HPat -> Bool
    Eq)

    data HExpr = HELam [HPat] HExpr
               | HEApply HExpr HExpr
               | HECon HSymbol
               | HEVar HSymbol
               | HETuple [HExpr]
               | HECase HExpr [(HPat, HExpr)]
               deriving (Int -> HExpr -> ShowS
    [HExpr] -> ShowS
    HExpr -> HSymbol
    (Int -> HExpr -> ShowS)
    -> (HExpr -> HSymbol) -> ([HExpr] -> ShowS) -> Show HExpr
    forall a.
    (Int -> a -> ShowS) -> (a -> HSymbol) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> HExpr -> ShowS
    showsPrec :: Int -> HExpr -> ShowS
    $cshow :: HExpr -> HSymbol
    show :: HExpr -> HSymbol
    $cshowList :: [HExpr] -> ShowS
    showList :: [HExpr] -> ShowS
    Show, HExpr -> HExpr -> Bool
    (HExpr -> HExpr -> Bool) -> (HExpr -> HExpr -> Bool) -> Eq HExpr
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: HExpr -> HExpr -> Bool
    == :: HExpr -> HExpr -> Bool
    $c/= :: HExpr -> HExpr -> Bool
    /= :: HExpr -> HExpr -> Bool
    Eq)

    hPrClause :: HClause -> String
    hPrClause :: HClause -> HSymbol
    hPrClause HClause
    c = Style -> Doc -> HSymbol
    renderStyle Style
    style (Doc -> HSymbol) -> Doc -> HSymbol
    forall a b. (a -> b) -> a -> b
    $ Int -> HClause -> Doc
    ppClause Int
    0 HClause
    c

    ppClause :: Int -> HClause -> Doc
    ppClause :: Int -> HClause -> Doc
    ppClause Int
    _p (HClause HSymbol
    f [HPat]
    ps HExpr
    e) = HSymbol -> Doc
    text (ShowS
    prHSymbolOp HSymbol
    f) Doc -> Doc -> Doc
    <+> [Doc] -> Doc
    sep [[Doc] -> Doc
    sep ((HPat -> Doc) -> [HPat] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (Int -> HPat -> Doc
    ppPat Int
    10) [HPat]
    ps) Doc -> Doc -> Doc
    <+> HSymbol -> Doc
    text HSymbol
    "=",
                                                                    Int -> Doc -> Doc
    nest Int
    2 (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ Int -> HExpr -> Doc
    ppExpr Int
    0 HExpr
    e]

    prHSymbolOp :: HSymbol -> String
    prHSymbolOp :: ShowS
    prHSymbolOp s :: HSymbol
    s@(Char
    c:HSymbol
    _) | Bool -> Bool
    not (Char -> Bool
    isAlphaNum Char
    c) = HSymbol
    "(" HSymbol -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ HSymbol
    s HSymbol -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ HSymbol
    ")"
    prHSymbolOp HSymbol
    s = HSymbol
    s

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

    hPrExpr :: HExpr -> String
    hPrExpr :: HExpr -> HSymbol
    hPrExpr HExpr
    e = Style -> Doc -> HSymbol
    renderStyle Style
    style (Doc -> HSymbol) -> Doc -> HSymbol
    forall a b. (a -> b) -> a -> b
    $ Int -> HExpr -> Doc
    ppExpr Int
    0 HExpr
    e

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

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

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

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

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

            unTuple :: Int -> HExpr -> (a -> a, [HExpr])
    unTuple Int
    0 HExpr
    _ = (a -> a
    forall a. a -> a
    id, [])
            unTuple Int
    1 HExpr
    a = (a -> a
    forall a. a -> a
    id, [HExpr
    a])
            unTuple Int
    n (HETuple [HExpr]
    as) | [HExpr] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [HExpr]
    as Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    n = (a -> a
    forall a. a -> a
    id, [HExpr]
    as)
            unTuple Int
    n HExpr
    e = HSymbol -> (a -> a, [HExpr])
    forall a. HasCallStack => HSymbol -> a
    error (HSymbol -> (a -> a, [HExpr])) -> HSymbol -> (a -> a, [HExpr])
    forall a b. (a -> b) -> a -> b
    $ HSymbol
    "unTuple: unimplemented " HSymbol -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ (Int, HExpr) -> HSymbol
    forall a. Show a => a -> HSymbol
    show (Int
    n, HExpr
    e)

            unTupleP :: Int -> HPat -> [HPat]
    unTupleP Int
    0 HPat
    _ = []
    --      unTupleP 1 p = [p]
            unTupleP Int
    n (HPTuple [HPat]
    ps) | [HPat] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [HPat]
    ps Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    n = [HPat]
    ps
            unTupleP Int
    n HPat
    p = HSymbol -> [HPat]
    forall a. HasCallStack => HSymbol -> a
    error (HSymbol -> [HPat]) -> HSymbol -> [HPat]
    forall a b. (a -> b) -> a -> b
    $ HSymbol
    "unTupleP: unimplemented " HSymbol -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ (Int, HPat) -> HSymbol
    forall a. Show a => a -> HSymbol
    show (Int
    n, HPat
    p)

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

            convAp [HSymbol]
    vs Term
    f [Term]
    as =
              let ([HExpr]
    es, [[(HSymbol, HPat)]]
    sss) = [(HExpr, [(HSymbol, HPat)])] -> ([HExpr], [[(HSymbol, HPat)]])
    forall a b. [(a, b)] -> ([a], [b])
    unzip ([(HExpr, [(HSymbol, HPat)])] -> ([HExpr], [[(HSymbol, HPat)]]))
    -> [(HExpr, [(HSymbol, HPat)])] -> ([HExpr], [[(HSymbol, HPat)]])
    forall a b. (a -> b) -> a -> b
    $ (Term -> (HExpr, [(HSymbol, HPat)]))
    -> [Term] -> [(HExpr, [(HSymbol, HPat)])]
    forall a b. (a -> b) -> [a] -> [b]
    map ([HSymbol] -> Term -> (HExpr, [(HSymbol, HPat)])
    conv [HSymbol]
    vs) (Term
    fTerm -> [Term] -> [Term]
    forall a. a -> [a] -> [a]
    :[Term]
    as)
              in ((HExpr -> HExpr -> HExpr) -> [HExpr] -> HExpr
    forall a. (a -> a -> a) -> [a] -> a
    forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
    foldl1 HExpr -> HExpr -> HExpr
    HEApply [HExpr]
    es, [[(HSymbol, HPat)]] -> [(HSymbol, HPat)]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat [[(HSymbol, HPat)]]
    sss)

            convV :: HSymbol -> [(HSymbol, HPat)] -> HPat
    convV HSymbol
    hs [(HSymbol, HPat)]
    ss = case [ HPat
    y | (HSymbol
    x, HPat
    y) <- [(HSymbol, HPat)]
    ss, HSymbol
    x HSymbol -> HSymbol -> Bool
    forall a. Eq a => a -> a -> Bool
    == HSymbol
    hs ] of
              []  -> HSymbol -> HPat
    HPVar HSymbol
    hs
              [HPat
    p] -> HSymbol -> HPat -> HPat
    HPAt HSymbol
    hs HPat
    p
              [HPat]
    ps  -> HSymbol -> HPat -> HPat
    HPAt HSymbol
    hs (HPat -> HPat) -> HPat -> HPat
    forall a b. (a -> b) -> a -> b
    $ (HPat -> HPat -> HPat) -> [HPat] -> HPat
    forall a. (a -> a -> a) -> [a] -> a
    forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
    foldr1 HPat -> HPat -> HPat
    combPat [HPat]
    ps

            combPat :: HPat -> HPat -> HPat
    combPat HPat
    p HPat
    p' | HPat
    p HPat -> HPat -> Bool
    forall a. Eq a => a -> a -> Bool
    == HPat
    p'             = HPat
    p
            combPat (HPVar HSymbol
    v) HPat
    p                = HSymbol -> HPat -> HPat
    HPAt HSymbol
    v HPat
    p
            combPat HPat
    p (HPVar HSymbol
    v)                = HSymbol -> HPat -> HPat
    HPAt HSymbol
    v HPat
    p
            combPat (HPTuple [HPat]
    ps) (HPTuple [HPat]
    ps') = [HPat] -> HPat
    HPTuple ((HPat -> HPat -> HPat) -> [HPat] -> [HPat] -> [HPat]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith HPat -> HPat -> HPat
    combPat [HPat]
    ps [HPat]
    ps')
            combPat HPat
    p HPat
    p'                       = HSymbol -> HPat
    forall a. HasCallStack => HSymbol -> a
    error (HSymbol -> HPat) -> HSymbol -> HPat
    forall a b. (a -> b) -> a -> b
    $ HSymbol
    "unimplemented combPat: " HSymbol -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ (HPat, HPat) -> HSymbol
    forall a. Show a => a -> HSymbol
    show (HPat
    p, HPat
    p')

            hETuple :: [HExpr] -> HExpr
    hETuple [HExpr
    e] = HExpr
    e
            hETuple [HExpr]
    es = [HExpr] -> HExpr
    HETuple [HExpr]
    es

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

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

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

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

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

    eqPatExpr :: HPat -> HExpr -> Bool
    eqPatExpr :: HPat -> HExpr -> Bool
    eqPatExpr (HPVar HSymbol
    s) (HEVar HSymbol
    s') = HSymbol
    s HSymbol -> HSymbol -> Bool
    forall a. Eq a => a -> a -> Bool
    == HSymbol
    s'
    eqPatExpr (HPCon HSymbol
    s) (HECon HSymbol
    s') = HSymbol
    s HSymbol -> HSymbol -> Bool
    forall a. Eq a => a -> a -> Bool
    == HSymbol
    s'
    eqPatExpr (HPTuple [HPat]
    ps) (HETuple [HExpr]
    es) = [Bool] -> Bool
    forall (t :: * -> *). Foldable t => t Bool -> Bool
    and ((HPat -> HExpr -> Bool) -> [HPat] -> [HExpr] -> [Bool]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith HPat -> HExpr -> Bool
    eqPatExpr [HPat]
    ps [HExpr]
    es)
    eqPatExpr (HPApply HPat
    pf HPat
    pa) (HEApply HExpr
    ef HExpr
    ea) = HPat -> HExpr -> Bool
    eqPatExpr HPat
    pf HExpr
    ef Bool -> Bool -> Bool
    && HPat -> HExpr -> Bool
    eqPatExpr HPat
    pa HExpr
    ea
    eqPatExpr HPat
    _ HExpr
    _ = Bool
    False

    alphaEq :: HExpr -> HExpr -> Bool
    alphaEq :: HExpr -> HExpr -> Bool
    alphaEq HExpr
    e1 HExpr
    e2 | HExpr
    e1 HExpr -> HExpr -> Bool
    forall a. Eq a => a -> a -> Bool
    == HExpr
    e2 = Bool
    True
    alphaEq (HELam [HPat]
    ps1 HExpr
    e1) (HELam [HPat]
    ps2 HExpr
    e2) =
      Maybe ()
    forall a. Maybe a
    Nothing Maybe () -> Maybe () -> Bool
    forall a. Eq a => a -> a -> Bool
    /= do
          [(HSymbol, HSymbol)]
    s <- HPat -> HPat -> Maybe [(HSymbol, HSymbol)]
    matchPat ([HPat] -> HPat
    HPTuple [HPat]
    ps1) ([HPat] -> HPat
    HPTuple [HPat]
    ps2)
          if HExpr -> HExpr -> Bool
    alphaEq ([(HSymbol, HSymbol)] -> HExpr -> HExpr
    hESubst [(HSymbol, HSymbol)]
    s HExpr
    e1) HExpr
    e2
             then () -> Maybe ()
    forall a. a -> Maybe a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
             else Maybe ()
    forall a. Maybe a
    Nothing
    alphaEq (HEApply HExpr
    f1 HExpr
    a1) (HEApply HExpr
    f2 HExpr
    a2) = HExpr -> HExpr -> Bool
    alphaEq HExpr
    f1 HExpr
    f2 Bool -> Bool -> Bool
    && HExpr -> HExpr -> Bool
    alphaEq HExpr
    a1 HExpr
    a2
    alphaEq (HECon HSymbol
    s1) (HECon HSymbol
    s2) = HSymbol
    s1 HSymbol -> HSymbol -> Bool
    forall a. Eq a => a -> a -> Bool
    == HSymbol
    s2
    alphaEq (HEVar HSymbol
    s1) (HEVar HSymbol
    s2) = HSymbol
    s1 HSymbol -> HSymbol -> Bool
    forall a. Eq a => a -> a -> Bool
    == HSymbol
    s2
    alphaEq (HETuple [HExpr]
    es1) (HETuple [HExpr]
    es2) | [HExpr] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [HExpr]
    es1 Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == [HExpr] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [HExpr]
    es2 = [Bool] -> Bool
    forall (t :: * -> *). Foldable t => t Bool -> Bool
    and ((HExpr -> HExpr -> Bool) -> [HExpr] -> [HExpr] -> [Bool]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith HExpr -> HExpr -> Bool
    alphaEq [HExpr]
    es1 [HExpr]
    es2)
    alphaEq (HECase HExpr
    e1 [(HPat, HExpr)]
    alts1) (HECase HExpr
    e2 [(HPat, HExpr)]
    alts2) =
        HExpr -> HExpr -> Bool
    alphaEq HExpr
    e1 HExpr
    e2 Bool -> Bool -> Bool
    && [Bool] -> Bool
    forall (t :: * -> *). Foldable t => t Bool -> Bool
    and ((HExpr -> HExpr -> Bool) -> [HExpr] -> [HExpr] -> [Bool]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith HExpr -> HExpr -> Bool
    alphaEq [ [HPat] -> HExpr -> HExpr
    HELam [HPat
    p] HExpr
    e | (HPat
    p, HExpr
    e) <- [(HPat, HExpr)]
    alts1 ] [ [HPat] -> HExpr -> HExpr
    HELam [HPat
    p] HExpr
    e | (HPat
    p, HExpr
    e) <- [(HPat, HExpr)]
    alts2 ])
    alphaEq HExpr
    _ HExpr
    _ = Bool
    False

    matchPat :: HPat -> HPat -> Maybe [(HSymbol, HSymbol)]
    matchPat :: HPat -> HPat -> Maybe [(HSymbol, HSymbol)]
    matchPat (HPVar HSymbol
    s1) (HPVar HSymbol
    s2) = [(HSymbol, HSymbol)] -> Maybe [(HSymbol, HSymbol)]
    forall a. a -> Maybe a
    forall (m :: * -> *) a. Monad m => a -> m a
    return [(HSymbol
    s1, HSymbol
    s2)]
    matchPat (HPCon HSymbol
    s1) (HPCon HSymbol
    s2) | HSymbol
    s1 HSymbol -> HSymbol -> Bool
    forall a. Eq a => a -> a -> Bool
    == HSymbol
    s2 = [(HSymbol, HSymbol)] -> Maybe [(HSymbol, HSymbol)]
    forall a. a -> Maybe a
    forall (m :: * -> *) a. Monad m => a -> m a
    return []
    matchPat (HPTuple [HPat]
    ps1) (HPTuple [HPat]
    ps2) | [HPat] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [HPat]
    ps1 Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == [HPat] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [HPat]
    ps2 = do
      [[(HSymbol, HSymbol)]]
    ss <- (HPat -> HPat -> Maybe [(HSymbol, HSymbol)])
    -> [HPat] -> [HPat] -> Maybe [[(HSymbol, HSymbol)]]
    forall (m :: * -> *) a b c.
    Applicative m =>
    (a -> b -> m c) -> [a] -> [b] -> m [c]
    zipWithM HPat -> HPat -> Maybe [(HSymbol, HSymbol)]
    matchPat [HPat]
    ps1 [HPat]
    ps2
      [(HSymbol, HSymbol)] -> Maybe [(HSymbol, HSymbol)]
    forall a. a -> Maybe a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([(HSymbol, HSymbol)] -> Maybe [(HSymbol, HSymbol)])
    -> [(HSymbol, HSymbol)] -> Maybe [(HSymbol, HSymbol)]
    forall a b. (a -> b) -> a -> b
    $ [[(HSymbol, HSymbol)]] -> [(HSymbol, HSymbol)]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat [[(HSymbol, HSymbol)]]
    ss
    matchPat (HPAt HSymbol
    s1 HPat
    p1) (HPAt HSymbol
    s2 HPat
    p2) = do
      [(HSymbol, HSymbol)]
    s <- HPat -> HPat -> Maybe [(HSymbol, HSymbol)]
    matchPat HPat
    p1 HPat
    p2
      [(HSymbol, HSymbol)] -> Maybe [(HSymbol, HSymbol)]
    forall a. a -> Maybe a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([(HSymbol, HSymbol)] -> Maybe [(HSymbol, HSymbol)])
    -> [(HSymbol, HSymbol)] -> Maybe [(HSymbol, HSymbol)]
    forall a b. (a -> b) -> a -> b
    $ (HSymbol
    s1, HSymbol
    s2) (HSymbol, HSymbol) -> [(HSymbol, HSymbol)] -> [(HSymbol, HSymbol)]
    forall a. a -> [a] -> [a]
    : [(HSymbol, HSymbol)]
    s
    matchPat (HPApply HPat
    f1 HPat
    a1) (HPApply HPat
    f2 HPat
    a2) = do
      [(HSymbol, HSymbol)]
    s1 <- HPat -> HPat -> Maybe [(HSymbol, HSymbol)]
    matchPat HPat
    f1 HPat
    f2
      [(HSymbol, HSymbol)]
    s2 <- HPat -> HPat -> Maybe [(HSymbol, HSymbol)]
    matchPat HPat
    a1 HPat
    a2
      [(HSymbol, HSymbol)] -> Maybe [(HSymbol, HSymbol)]
    forall a. a -> Maybe a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([(HSymbol, HSymbol)] -> Maybe [(HSymbol, HSymbol)])
    -> [(HSymbol, HSymbol)] -> Maybe [(HSymbol, HSymbol)]
    forall a b. (a -> b) -> a -> b
    $ [(HSymbol, HSymbol)]
    s1 [(HSymbol, HSymbol)]
    -> [(HSymbol, HSymbol)] -> [(HSymbol, HSymbol)]
    forall a. [a] -> [a] -> [a]
    ++ [(HSymbol, HSymbol)]
    s2
    matchPat HPat
    _ HPat
    _ = Maybe [(HSymbol, HSymbol)]
    forall a. Maybe a
    Nothing

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

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

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

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

    getBinderVars :: HClause -> [HSymbol]
    getBinderVars :: HClause -> [HSymbol]
    getBinderVars (HClause HSymbol
    _ [HPat]
    pats HExpr
    expr) = (HPat -> [HSymbol]) -> [HPat] -> [HSymbol]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap HPat -> [HSymbol]
    getBinderVarsHP [HPat]
    pats [HSymbol] -> [HSymbol] -> [HSymbol]
    forall a. [a] -> [a] -> [a]
    ++ HExpr -> [HSymbol]
    getBinderVarsHE HExpr
    expr

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

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

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

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