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

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

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

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

    instance Read HType where
      readsPrec :: Int -> ReadS HType
    readsPrec _ = 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 (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 -> ReadP Char
    char '>')
      HType -> ReadP HType
    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 (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 (String, [HType])
    con = do String
    c <- Bool -> ReadP String
    pHSymbol Bool
    True
                   [HType]
    ts <- ReadP HType -> ReadP [HType]
    forall a. ReadP a -> ReadP [a]
    many ReadP HType
    pHTAtom
                   (String, [HType]) -> ReadP (String, [HType])
    forall (m :: * -> *) a. Monad m => a -> m a
    return (String
    c, [HType]
    ts)
      [(String, [HType])]
    cts <- ReadP (String, [HType]) -> ReadP () -> ReadP [(String, [HType])]
    forall a sep. ReadP a -> ReadP sep -> ReadP [a]
    sepBy ReadP (String, [HType])
    con (Char -> ReadP ()
    schar '|')
      HType -> ReadP HType
    forall (m :: * -> *) a. Monad m => a -> m a
    return (HType -> ReadP HType) -> HType -> ReadP HType
    forall a b. (a -> b) -> a -> b
    $ [(String, [HType])] -> HType
    HTUnion [(String, [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 -> ReadP Char
    char ')'
      HType -> ReadP HType
    forall (m :: * -> *) a. Monad m => a -> m a
    return (HType -> ReadP HType) -> HType -> ReadP HType
    forall a b. (a -> b) -> a -> b
    $ String -> HType
    HTCon "()"

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

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

    pHSymbol :: Bool -> ReadP HSymbol
    pHSymbol :: Bool -> ReadP String
    pHSymbol con :: 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
    $ \ c :: 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 d :: Char
    d = Char -> Bool
    isAlphaNum Char
    d Bool -> Bool -> Bool
    || Char
    d Char -> Char -> Bool
    forall a. Eq a => a -> a -> Bool
    == '\'' Bool -> Bool -> Bool
    || Char
    d Char -> Char -> Bool
    forall a. Eq a => a -> a -> Bool
    == '.'
      String
    cs <- (Char -> Bool) -> ReadP String
    munch Char -> Bool
    isSym
      String -> ReadP String
    forall (m :: * -> *) a. Monad m => a -> m a
    return (String -> ReadP String) -> String -> ReadP String
    forall a b. (a -> b) -> a -> b
    $ Char
    cChar -> ShowS
    forall a. a -> [a] -> [a]
    :String
    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 ','; ReadP HType
    pHType)
      HType -> ReadP HType
    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 (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 (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 '['
      HType
    t <- ReadP HType
    pHType
      Char -> ReadP ()
    schar ']'
      HType -> ReadP HType
    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 (String -> HType
    HTCon "[]") 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 -> ReadP Char
    char '>')
      HKind -> ReadP HKind
    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 (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 '*'; HKind -> ReadP HKind
    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 :: ReadP a -> ReadP a
    pParen p :: ReadP a
    p = do
      Char -> ReadP ()
    schar '('
      a
    e <- ReadP a
    p
      Char -> ReadP ()
    schar ')'
      a -> ReadP a
    forall (m :: * -> *) a. Monad m => a -> m a
    return a
    e

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

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

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

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

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

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

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

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

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

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

    ppClause :: Int -> HClause -> Doc
    ppClause :: Int -> HClause -> Doc
    ppClause _p :: Int
    _p (HClause f :: String
    f ps :: [HPat]
    ps e :: HExpr
    e) = String -> Doc
    text (ShowS
    prHSymbolOp String
    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 10) [HPat]
    ps) Doc -> Doc -> Doc
    <+> String -> Doc
    text "=",
                                                                    Int -> Doc -> Doc
    nest 2 (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ Int -> HExpr -> Doc
    ppExpr 0 HExpr
    e]

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

    ppPat :: Int -> HPat -> Doc
    ppPat :: Int -> HPat -> Doc
    ppPat _ (HPVar s :: String
    s) = String -> Doc
    text String
    s
    ppPat _ (HPCon s :: String
    s) = String -> Doc
    text String
    s
    ppPat _ (HPTuple ps :: [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 0) [HPat]
    ps)
    ppPat _ (HPAt s :: String
    s p :: HPat
    p) = String -> Doc
    text String
    s Doc -> Doc -> Doc
    <> String -> Doc
    text "@" Doc -> Doc -> Doc
    <> Int -> HPat -> Doc
    ppPat 10 HPat
    p
    ppPat p :: Int
    p (HPApply a :: HPat
    a b :: HPat
    b) = Bool -> Doc -> Doc
    pparens (Int
    p Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > 1) (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ Int -> HPat -> Doc
    ppPat 1 HPat
    a Doc -> Doc -> Doc
    <+> Int -> HPat -> Doc
    ppPat 2 HPat
    b

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

    ppExpr :: Int -> HExpr -> Doc
    ppExpr :: Int -> HExpr -> Doc
    ppExpr p :: Int
    p (HELam ps :: [HPat]
    ps e :: HExpr
    e) = Bool -> Doc -> Doc
    pparens (Int
    p Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > 0) (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ [Doc] -> Doc
    sep [ String -> Doc
    text "\\" Doc -> Doc -> Doc
    <+> [Doc] -> Doc
    sep ((HPat -> Doc) -> [HPat] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (Int -> HPat -> Doc
    ppPat 10) [HPat]
    ps) Doc -> Doc -> Doc
    <+> String -> Doc
    text "->",
                                                    Int -> HExpr -> Doc
    ppExpr 0 HExpr
    e]
    ppExpr p :: Int
    p (HEApply (HEApply (HEVar f :: String
    f@(c :: Char
    c:_)) a1 :: HExpr
    a1) a2 :: 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
    > 4) (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ Int -> HExpr -> Doc
    ppExpr 5 HExpr
    a1 Doc -> Doc -> Doc
    <+> String -> Doc
    text String
    f Doc -> Doc -> Doc
    <+> Int -> HExpr -> Doc
    ppExpr 5 HExpr
    a2
    ppExpr p :: Int
    p (HEApply f :: HExpr
    f a :: HExpr
    a) = Bool -> Doc -> Doc
    pparens (Int
    p Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > 11) (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ Int -> HExpr -> Doc
    ppExpr 11 HExpr
    f Doc -> Doc -> Doc
    <+> Int -> HExpr -> Doc
    ppExpr 12 HExpr
    a
    ppExpr _ (HECon s :: String
    s) = String -> Doc
    text String
    s
    ppExpr _ (HEVar s :: String
    s@(c :: Char
    c:_)) | 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
    $ String -> Doc
    text String
    s
    ppExpr _ (HEVar s :: String
    s) = String -> Doc
    text String
    s
    ppExpr _ (HETuple es :: [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 0) [HExpr]
    es)
    ppExpr p :: Int
    p (HECase s :: HExpr
    s alts :: [(HPat, HExpr)]
    alts) = Bool -> Doc -> Doc
    pparens (Int
    p Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > 0) (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ (String -> Doc
    text "case" Doc -> Doc -> Doc
    <+> Int -> HExpr -> Doc
    ppExpr 0 HExpr
    s Doc -> Doc -> Doc
    <+> String -> Doc
    text "of") Doc -> Doc -> Doc
    $$
                                Int -> Doc -> Doc
    nest 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 (pp :: HPat
    pp, e :: HExpr
    e) = Int -> HPat -> Doc
    ppPat 0 HPat
    pp Doc -> Doc -> Doc
    <+> String -> Doc
    text "->" Doc -> Doc -> Doc
    <+> Int -> HExpr -> Doc
    ppExpr 0 HExpr
    e

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

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

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

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

            unTuple :: Int -> HExpr -> (a -> a, [HExpr])
    unTuple 0 _ = (a -> a
    forall a. a -> a
    id, [])
            unTuple 1 a :: HExpr
    a = (a -> a
    forall a. a -> a
    id, [HExpr
    a])
            unTuple n :: Int
    n (HETuple as :: [HExpr]
    as) | [HExpr] -> 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 n :: Int
    n e :: HExpr
    e = String -> (a -> a, [HExpr])
    forall a. HasCallStack => String -> a
    error (String -> (a -> a, [HExpr])) -> String -> (a -> a, [HExpr])
    forall a b. (a -> b) -> a -> b
    $ "unTuple: unimplemented " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ (Int, HExpr) -> String
    forall a. Show a => a -> String
    show (Int
    n, HExpr
    e)

            unTupleP :: Int -> HPat -> [HPat]
    unTupleP 0 _ = []
    --      unTupleP 1 p = [p]
            unTupleP n :: Int
    n (HPTuple ps :: [HPat]
    ps) | [HPat] -> 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 n :: Int
    n p :: HPat
    p = String -> [HPat]
    forall a. HasCallStack => String -> a
    error (String -> [HPat]) -> String -> [HPat]
    forall a b. (a -> b) -> a -> b
    $ "unTupleP: unimplemented " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ (Int, HPat) -> String
    forall a. Show a => a -> String
    show (Int
    n, HPat
    p)

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

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

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

            combPat :: HPat -> HPat -> HPat
    combPat p :: HPat
    p p' :: HPat
    p' | HPat
    p HPat -> HPat -> Bool
    forall a. Eq a => a -> a -> Bool
    == HPat
    p'             = HPat
    p
            combPat (HPVar v :: String
    v) p :: HPat
    p                = String -> HPat -> HPat
    HPAt String
    v HPat
    p
            combPat p :: HPat
    p (HPVar v :: String
    v)                = String -> HPat -> HPat
    HPAt String
    v HPat
    p
            combPat (HPTuple ps :: [HPat]
    ps) (HPTuple ps' :: [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 p :: HPat
    p p' :: HPat
    p'                       = String -> HPat
    forall a. HasCallStack => String -> a
    error (String -> HPat) -> String -> HPat
    forall a b. (a -> b) -> a -> b
    $ "unimplemented combPat: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ (HPat, HPat) -> String
    forall a. Show a => a -> String
    show (HPat
    p, HPat
    p')

            hETuple :: [HExpr] -> HExpr
    hETuple [e :: HExpr
    e] = HExpr
    e
            hETuple es :: [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 = [(String, String)] -> HExpr -> HExpr
    fixAt []
      where fixAt :: [(String, String)] -> HExpr -> HExpr
    fixAt s :: [(String, String)]
    s (HELam ps :: [HPat]
    ps e :: HExpr
    e) = [HPat] -> HExpr -> HExpr
    HELam [HPat]
    ps' ([(String, String)] -> HExpr -> HExpr
    fixAt ([[(String, String)]] -> [(String, String)]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat [[(String, String)]]
    ss [(String, String)] -> [(String, String)] -> [(String, String)]
    forall a. [a] -> [a] -> [a]
    ++ [(String, String)]
    s) HExpr
    e) where (ps' :: [HPat]
    ps', ss :: [[(String, String)]]
    ss) = [(HPat, [(String, String)])] -> ([HPat], [[(String, String)]])
    forall a b. [(a, b)] -> ([a], [b])
    unzip ([(HPat, [(String, String)])] -> ([HPat], [[(String, String)]]))
    -> [(HPat, [(String, String)])] -> ([HPat], [[(String, String)]])
    forall a b. (a -> b) -> a -> b
    $ (HPat -> (HPat, [(String, String)]))
    -> [HPat] -> [(HPat, [(String, String)])]
    forall a b. (a -> b) -> [a] -> [b]
    map HPat -> (HPat, [(String, String)])
    findSilly [HPat]
    ps
            fixAt s :: [(String, String)]
    s (HEApply f :: HExpr
    f a :: HExpr
    a) = HExpr -> HExpr -> HExpr
    HEApply ([(String, String)] -> HExpr -> HExpr
    fixAt [(String, String)]
    s HExpr
    f) ([(String, String)] -> HExpr -> HExpr
    fixAt [(String, String)]
    s HExpr
    a)
            fixAt _ e :: HExpr
    e@(HECon _) = HExpr
    e
            fixAt s :: [(String, String)]
    s e :: HExpr
    e@(HEVar v :: String
    v) = HExpr -> (String -> HExpr) -> Maybe String -> HExpr
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe HExpr
    e String -> HExpr
    HEVar (Maybe String -> HExpr) -> Maybe String -> HExpr
    forall a b. (a -> b) -> a -> b
    $ String -> [(String, String)] -> Maybe String
    forall a b. Eq a => a -> [(a, b)] -> Maybe b
    lookup String
    v [(String, String)]
    s
            fixAt s :: [(String, String)]
    s (HETuple es :: [HExpr]
    es) = [HExpr] -> HExpr
    HETuple ((HExpr -> HExpr) -> [HExpr] -> [HExpr]
    forall a b. (a -> b) -> [a] -> [b]
    map ([(String, String)] -> HExpr -> HExpr
    fixAt [(String, String)]
    s) [HExpr]
    es)
            fixAt s :: [(String, String)]
    s (HECase e :: HExpr
    e alts :: [(HPat, HExpr)]
    alts) = HExpr -> [(HPat, HExpr)] -> HExpr
    HECase ([(String, String)] -> HExpr -> HExpr
    fixAt [(String, String)]
    s HExpr
    e) (((HPat, HExpr) -> (HPat, HExpr))
    -> [(HPat, HExpr)] -> [(HPat, HExpr)]
    forall a b. (a -> b) -> [a] -> [b]
    map ([(String, String)] -> (HPat, HExpr) -> (HPat, HExpr)
    fixAtAlt [(String, String)]
    s) [(HPat, HExpr)]
    alts)
            fixAtAlt :: [(String, String)] -> (HPat, HExpr) -> (HPat, HExpr)
    fixAtAlt s :: [(String, String)]
    s (p :: HPat
    p, e :: HExpr
    e) = (HPat
    p', [(String, String)] -> HExpr -> HExpr
    fixAt ([(String, String)]
    s' [(String, String)] -> [(String, String)] -> [(String, String)]
    forall a. [a] -> [a] -> [a]
    ++ [(String, String)]
    s) HExpr
    e) where (p' :: HPat
    p', s' :: [(String, String)]
    s') = HPat -> (HPat, [(String, String)])
    findSilly HPat
    p
            findSilly :: HPat -> (HPat, [(String, String)])
    findSilly p :: HPat
    p@(HPVar _) = (HPat
    p, [])
            findSilly p :: HPat
    p@(HPCon _) = (HPat
    p, [])
            findSilly (HPTuple ps :: [HPat]
    ps) = ([HPat] -> HPat
    HPTuple [HPat]
    ps', [[(String, String)]] -> [(String, String)]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat [[(String, String)]]
    ss) where (ps' :: [HPat]
    ps', ss :: [[(String, String)]]
    ss) = [(HPat, [(String, String)])] -> ([HPat], [[(String, String)]])
    forall a b. [(a, b)] -> ([a], [b])
    unzip ([(HPat, [(String, String)])] -> ([HPat], [[(String, String)]]))
    -> [(HPat, [(String, String)])] -> ([HPat], [[(String, String)]])
    forall a b. (a -> b) -> a -> b
    $ (HPat -> (HPat, [(String, String)]))
    -> [HPat] -> [(HPat, [(String, String)])]
    forall a b. (a -> b) -> [a] -> [b]
    map HPat -> (HPat, [(String, String)])
    findSilly [HPat]
    ps
            findSilly (HPAt v :: String
    v p :: HPat
    p) = case HPat -> (HPat, [(String, String)])
    findSilly HPat
    p of
                                     (p' :: HPat
    p'@(HPVar v' :: String
    v'), s :: [(String, String)]
    s) -> (HPat
    p', (String
    v, String
    v')(String, String) -> [(String, String)] -> [(String, String)]
    forall a. a -> [a] -> [a]
    :[(String, String)]
    s)
                                     (p' :: HPat
    p', s :: [(String, String)]
    s)            -> (String -> HPat -> HPat
    HPAt String
    v HPat
    p', [(String, String)]
    s)
            findSilly (HPApply f :: HPat
    f a :: HPat
    a) = (HPat -> HPat -> HPat
    HPApply HPat
    f' HPat
    a', [(String, String)]
    sf [(String, String)] -> [(String, String)] -> [(String, String)]
    forall a. [a] -> [a] -> [a]
    ++ [(String, String)]
    sa) where (f' :: HPat
    f', sf :: [(String, String)]
    sf) = HPat -> (HPat, [(String, String)])
    findSilly HPat
    f; (a' :: HPat
    a', sa :: [(String, String)]
    sa) = HPat -> (HPat, [(String, String)])
    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 ps :: [HPat]
    ps e :: HExpr
    e) = [HPat] -> HExpr -> HExpr
    HELam [HPat]
    ps (HExpr -> HExpr
    collapeCase HExpr
    e)
    collapeCase (HEApply f :: HExpr
    f a :: HExpr
    a) = HExpr -> HExpr -> HExpr
    HEApply (HExpr -> HExpr
    collapeCase HExpr
    f) (HExpr -> HExpr
    collapeCase HExpr
    a)
    collapeCase e :: HExpr
    e@(HECon _) = HExpr
    e
    collapeCase e :: HExpr
    e@(HEVar _) = HExpr
    e
    collapeCase (HETuple es :: [HExpr]
    es) = [HExpr] -> HExpr
    HETuple ((HExpr -> HExpr) -> [HExpr] -> [HExpr]
    forall a b. (a -> b) -> [a] -> [b]
    map HExpr -> HExpr
    collapeCase [HExpr]
    es)
    collapeCase (HECase e :: HExpr
    e alts :: [(HPat, HExpr)]
    alts) = case [(HPat
    p, HExpr -> HExpr
    collapeCase HExpr
    b) | (p :: HPat
    p, b :: HExpr
    b) <- [(HPat, HExpr)]
    alts ] of
        (p :: HPat
    p, b :: HExpr
    b) : pes :: [(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 (\ (p' :: HPat
    p', b' :: HExpr
    b') -> HExpr -> HExpr -> Bool
    alphaEq HExpr
    b HExpr
    b' Bool -> Bool -> Bool
    && HPat -> Bool
    noBound HPat
    p') [(HPat, HExpr)]
    pes -> HExpr
    b
        pes :: [(HPat, HExpr)]
    pes -> HExpr -> [(HPat, HExpr)] -> HExpr
    HECase (HExpr -> HExpr
    collapeCase HExpr
    e) [(HPat, HExpr)]
    pes
      where noBound :: HPat -> Bool
    noBound = (String -> Bool) -> [String] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all (String -> String -> Bool
    forall a. Eq a => a -> a -> Bool
    == "_") ([String] -> Bool) -> (HPat -> [String]) -> HPat -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . HPat -> [String]
    getBinderVarsHP

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

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

    hECase :: HExpr -> [(HPat, HExpr)] -> HExpr
    hECase :: HExpr -> [(HPat, HExpr)] -> HExpr
    hECase e :: HExpr
    e [] = HExpr -> HExpr -> HExpr
    HEApply (String -> HExpr
    HEVar "void") HExpr
    e
    hECase _ [(HPCon "()", e :: HExpr
    e)] = HExpr
    e
    hECase e :: HExpr
    e pes :: [(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 e :: HExpr
    e [(p :: HPat
    p, HELam ps :: [HPat]
    ps b :: 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 se :: HExpr
    se alts :: [(HPat, HExpr)]
    alts@((_, HELam ops :: [HPat]
    ops _):_) | Int
    m Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > 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 (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 ps :: [HPat]
    ps _) = [HPat] -> 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 _ = 0
            isPVar :: HPat -> Bool
    isPVar (HPVar _) = Bool
    True
            isPVar _ = Bool
    False
            alts' :: [(HPat, HExpr)]
    alts' = [ let (ps1 :: [HPat]
    ps1, ps2 :: [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
    $ [(String, String)] -> HExpr -> HExpr
    hESubst ((HPat -> String -> (String, String))
    -> [HPat] -> [String] -> [(String, String)]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith (\ (HPVar v :: String
    v) n :: String
    n -> (String
    v, String
    n)) [HPat]
    ps1 [String]
    ns) HExpr
    e)
                      | (cps :: HPat
    cps, HELam ps :: [HPat]
    ps e :: HExpr
    e) <- [(HPat, HExpr)]
    alts ]
            ns :: [String]
    ns = [ String
    n | HPVar n :: String
    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 _ ((_,e :: HExpr
    e):alts :: [(HPat, HExpr)]
    alts@(_:_)) | ((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 e :: HExpr
    e alts :: [(HPat, HExpr)]
    alts = HExpr -> [(HPat, HExpr)] -> HExpr
    HECase HExpr
    e [(HPat, HExpr)]
    alts

    eqPatExpr :: HPat -> HExpr -> Bool
    eqPatExpr :: HPat -> HExpr -> Bool
    eqPatExpr (HPVar s :: String
    s) (HEVar s' :: String
    s') = String
    s String -> String -> Bool
    forall a. Eq a => a -> a -> Bool
    == String
    s'
    eqPatExpr (HPCon s :: String
    s) (HECon s' :: String
    s') = String
    s String -> String -> Bool
    forall a. Eq a => a -> a -> Bool
    == String
    s'
    eqPatExpr (HPTuple ps :: [HPat]
    ps) (HETuple es :: [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 pf :: HPat
    pf pa :: HPat
    pa) (HEApply ef :: HExpr
    ef ea :: HExpr
    ea) = HPat -> HExpr -> Bool
    eqPatExpr HPat
    pf HExpr
    ef Bool -> Bool -> Bool
    && HPat -> HExpr -> Bool
    eqPatExpr HPat
    pa HExpr
    ea
    eqPatExpr _ _ = Bool
    False

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

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

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

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

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

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

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

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

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

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

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