{-# 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
/= :: 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 [(String, [HType])]
_) = Bool
True
isHTUnion HType
_ = Bool
False

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

instance Show HType where
  showsPrec :: Int -> HType -> ShowS
showsPrec Int
_ (HTApp (HTCon String
"[]") HType
t) = String -> ShowS
showString String
"[" 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
. String -> ShowS
showString String
"]"
  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
. String -> ShowS
showString String
" " 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 String
s) = String -> ShowS
showString String
s
  showsPrec Int
_ (HTCon s :: String
s@(Char
c:String
_)) | 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 Int
_ (HTCon String
s) = String -> ShowS
showString String
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 []     = String -> ShowS
forall a. HasCallStack => String -> a
error String
"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
. String -> ShowS
showString String
", " 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
. String -> ShowS
showString String
" -> " 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 [(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 [(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 ((String, t a)
cts : [(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 String
" | " 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 (String
c, t a
ts)   = (ShowS -> a -> ShowS) -> ShowS -> t a -> ShowS
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
. String -> ShowS
showString String
" " 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) (String -> ShowS
showString String
c) t a
ts
  showsPrec Int
_ (HTAbstract String
s HKind
_) = String -> ShowS
showString String
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 (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 (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 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])] -> 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
'('
  Char -> ReadP Char
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 String
"()"

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
'('; Char -> ReadP ()
schar Char
'-'; Char -> ReadP ()
schar Char
'>'; Char -> ReadP ()
schar Char
')'; HType -> ReadP HType
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> HType
HTCon String
"->")

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 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
'.'
  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 Char
','; 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 Char
'['
  HType
t <- ReadP HType
pHType
  Char -> ReadP ()
schar 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
HTApp (String -> HType
HTCon String
"[]") 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 (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 Char
'*'; 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 ReadP a
p = do
  Char -> ReadP ()
schar Char
'('
  a
e <- ReadP a
p
  Char -> ReadP ()
schar Char
')'
  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 (m :: * -> *) a. Monad m => a -> m a
return ()

getHTVars :: HType -> [HSymbol]
getHTVars :: HType -> [String]
getHTVars (HTApp HType
f 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 String
v)     = [String
v]
getHTVars (HTCon String
_)     = []
getHTVars (HTTuple [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 HType
f HType
a) = HType -> [String]
getHTVars HType
f [String] -> [String] -> [String]
forall a. Eq a => [a] -> [a] -> [a]
`union` HType -> [String]
getHTVars HType
a
getHTVars HType
_             = String -> [String]
forall a. HasCallStack => String -> a
error String
"getHTVars"

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

hTypeToFormula :: [(HSymbol, ([HSymbol], HType, a))] -> HType -> Formula
hTypeToFormula :: [(String, ([String], HType, a))] -> HType -> Formula
hTypeToFormula [(String, ([String], HType, a))]
ss (HTTuple [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 [(String, ([String], HType, a))]
ss (HTArrow HType
t1 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 [(String, ([String], HType, a))]
ss (HTUnion [(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)) | (String
c, [HType]
ts) <- [(String, [HType])]
ctss ]
hTypeToFormula [(String, ([String], HType, a))]
ss 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
  Maybe HType
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 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 [(String, ([String], HType, a))]
ss (HTApp HType
f HType
a) [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 [(String, ([String], HType, a))]
ss (HTCon String
c) [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 ([String]
vs, HType
t, a
_) | [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 ([String], HType, a)
_ -> Maybe HType
forall a. Maybe a
Nothing
expandSyn [(String, ([String], HType, a))]
_ HType
_ [HType]
_ = Maybe HType
forall a. Maybe a
Nothing

substHT :: [(HSymbol, HType)] -> HType -> HType
substHT :: [(String, HType)] -> HType -> HType
substHT [(String, HType)]
r (HTApp HType
f 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 [(String, HType)]
r t :: HType
t@(HTVar 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
  Maybe HType
Nothing -> HType
t
  Just HType
t' -> HType
t'
substHT [(String, HType)]
_ t :: HType
t@(HTCon String
_) = HType
t
substHT [(String, HType)]
r (HTTuple [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 [(String, HType)]
r (HTArrow HType
f 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 [(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) | (String
c, [HType]
ts) <- [(String, [HType])]
ctss ]
substHT [(String, HType)]
_ t :: HType
t@(HTAbstract String
_ HKind
_) = HType
t

hTApp :: HType -> HType -> HType
hTApp :: HType -> HType -> HType
hTApp (HTApp (HTCon String
"->") 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 -> 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 HClause
c = Style -> Doc -> String
renderStyle Style
style (Doc -> String) -> Doc -> String
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 String
f [HPat]
ps 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 Int
10) [HPat]
ps) Doc -> Doc -> Doc
<+> String -> Doc
text String
"=",
                                                                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 :: String
s@(Char
c:String
_) | Bool -> Bool
not (Char -> Bool
isAlphaNum Char
c) = String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
prHSymbolOp String
s = String
s

ppPat :: Int -> HPat -> Doc
ppPat :: Int -> HPat -> Doc
ppPat Int
_ (HPVar String
s) = String -> Doc
text String
s
ppPat Int
_ (HPCon String
s) = String -> Doc
text String
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 String
s HPat
p) = String -> Doc
text String
s Doc -> Doc -> Doc
<> String -> Doc
text String
"@" 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 -> String
hPrExpr HExpr
e = Style -> Doc -> String
renderStyle Style
style (Doc -> String) -> Doc -> String
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 [ String -> Doc
text String
"\\" 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
<+> String -> Doc
text String
"->",
                                                Int -> HExpr -> Doc
ppExpr Int
0 HExpr
e]
ppExpr Int
p (HEApply (HEApply (HEVar f :: String
f@(Char
c:String
_)) 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
<+> String -> Doc
text String
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 String
s) = String -> Doc
text String
s
ppExpr Int
_ (HEVar s :: String
s@(Char
c:String
_)) | 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 Int
_ (HEVar String
s) = String -> Doc
text String
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
$ (String -> Doc
text String
"case" Doc -> Doc -> Doc
<+> Int -> HExpr -> Doc
ppExpr Int
0 HExpr
s Doc -> Doc -> Doc
<+> String -> Doc
text String
"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
<+> String -> Doc
text String
"->" 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 -> String
unSymbol (Symbol String
s) = String
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, [(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 [String]
_vs (Var Symbol
s) = (String -> HExpr
HEVar (String -> HExpr) -> String -> HExpr
forall a b. (a -> b) -> a -> b
$ Symbol -> String
unSymbol Symbol
s, [])
        conv [String]
vs (Lam Symbol
s Term
te) =
          let hs :: String
hs = Symbol -> String
unSymbol Symbol
s
              (HExpr
te', [(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 [String]
vs (Apply (Cinj (ConsDesc String
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 (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 (a -> a
f, [HExpr]
as) = Int -> HExpr -> (a -> a, [HExpr])
forall a. Int -> HExpr -> (a -> a, [HExpr])
unTuple Int
n HExpr
ha
                (HExpr
ha, [(String, HPat)]
ss) = [String] -> Term -> (HExpr, [(String, HPat)])
conv [String]
vs Term
a
        conv [String]
vs (Apply Term
te1 Term
te2) = [String] -> Term -> [Term] -> (HExpr, [(String, HPat)])
convAp [String]
vs Term
te1 [Term
te2]
        conv [String]
_vs (Ctuple Int
0) = (String -> HExpr
HECon String
"()", [])
        conv [String]
_vs 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
$ String
"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 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 (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 = 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
$ String
"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 Int
0 HPat
_ = []
--      unTupleP 1 p = [p]
        unTupleP Int
n (HPTuple [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 Int
n HPat
p = String -> [HPat]
forall a. HasCallStack => String -> a
error (String -> [HPat]) -> String -> [HPat]
forall a b. (a -> b) -> a -> b
$ String
"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 [String]
vs (Apply Term
te1 Term
te2) [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 [String]
vs (Ctuple Int
n) [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 ([HExpr]
es, [[(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 [String]
vs (Ccases [ConsDesc]
cds) (Term
se : [Term]
es) =
          let ([(HPat, HExpr)]
alts, [[(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 Symbol
v Term
e) (ConsDesc String
c Int
n) =
                let hv :: String
hv = Symbol -> String
unSymbol Symbol
v
                    (HExpr
he, [(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
                           Maybe HPat
Nothing -> Int -> HPat -> [HPat]
forall a. Int -> a -> [a]
replicate Int
n (String -> HPat
HPVar String
"_")
                           Just 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 Term
e ConsDesc
_ = 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
$ String
"cAlt " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term -> String
forall a. Show a => a -> String
show Term
e
              (HExpr
e', [(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 [String]
vs (Csplit Int
n) (Term
b : Term
a : [Term]
as) =
          let (HExpr
hb, [(String, HPat)]
sb) = [String] -> Term -> (HExpr, [(String, HPat)])
conv [String]
vs Term
b
              (HExpr
a', [(String, HPat)]
sa) = [String] -> Term -> (HExpr, [(String, HPat)])
conv [String]
vs Term
a
              ([HExpr]
as', [[(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
              ([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 (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 = String -> ([HPat], HExpr)
forall a. HasCallStack => String -> a
error (String -> ([HPat], HExpr)) -> String -> ([HPat], HExpr)
forall a b. (a -> b) -> a -> b
$ String
"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 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] -> 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 [String]
vs Term
f [Term]
as =
          let ([HExpr]
es, [[(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 String
hs [(String, HPat)]
ss = case [ HPat
y | (String
x, 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
          [HPat
p] -> String -> HPat -> HPat
HPAt String
hs HPat
p
          [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 HPat
p HPat
p' | HPat
p HPat -> HPat -> Bool
forall a. Eq a => a -> a -> Bool
== HPat
p'             = HPat
p
        combPat (HPVar String
v) HPat
p                = String -> HPat -> HPat
HPAt String
v HPat
p
        combPat HPat
p (HPVar String
v)                = String -> HPat -> HPat
HPAt String
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'                       = String -> HPat
forall a. HasCallStack => String -> a
error (String -> HPat) -> String -> HPat
forall a b. (a -> b) -> a -> b
$ String
"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 [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 = [(String, String)] -> HExpr -> HExpr
fixAt []
  where fixAt :: [(String, String)] -> HExpr -> HExpr
fixAt [(String, String)]
s (HELam [HPat]
ps 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 ([HPat]
ps', [[(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 [(String, String)]
s (HEApply HExpr
f 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 [(String, String)]
_ e :: HExpr
e@(HECon String
_) = HExpr
e
        fixAt [(String, String)]
s e :: HExpr
e@(HEVar 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 [(String, String)]
s (HETuple [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 [(String, String)]
s (HECase HExpr
e [(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 [(String, String)]
s (HPat
p, 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 (HPat
p', [(String, String)]
s') = HPat -> (HPat, [(String, String)])
findSilly HPat
p
        findSilly :: HPat -> (HPat, [(String, String)])
findSilly p :: HPat
p@(HPVar String
_) = (HPat
p, [])
        findSilly p :: HPat
p@(HPCon String
_) = (HPat
p, [])
        findSilly (HPTuple [HPat]
ps) = ([HPat] -> HPat
HPTuple [HPat]
ps', [[(String, String)]] -> [(String, String)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[(String, String)]]
ss) where ([HPat]
ps', [[(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 String
v HPat
p) = case HPat -> (HPat, [(String, String)])
findSilly HPat
p of
                                 (p' :: HPat
p'@(HPVar String
v'), [(String, String)]
s) -> (HPat
p', (String
v, String
v')(String, String) -> [(String, String)] -> [(String, String)]
forall a. a -> [a] -> [a]
:[(String, String)]
s)
                                 (HPat
p', [(String, String)]
s)            -> (String -> HPat -> HPat
HPAt String
v HPat
p', [(String, String)]
s)
        findSilly (HPApply HPat
f 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 (HPat
f', [(String, String)]
sf) = HPat -> (HPat, [(String, String)])
findSilly HPat
f; (HPat
a', [(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 [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 String
_) = HExpr
e
collapeCase e :: HExpr
e@(HEVar String
_) = 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 = (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
"_") ([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 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] -> [String]
forall a b. (a -> b) -> a -> b
$ HExpr -> [String]
getBinderVarsHE HExpr
e
      nvars :: [String]
nvars = [[Char
c] | Char
c <- [Char
'a'..Char
'z']] [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [ String
"x" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
i | Integer
i <- [Integer
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 [] 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 (String -> HExpr
HEVar String
"void") HExpr
e
hECase HExpr
_ [(HPCon String
"()", 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 (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 (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 String
_) = 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
$ [(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 String
v) String
n -> (String
v, String
n)) [HPat]
ps1 [String]
ns) HExpr
e)
                  | (HPat
cps, HELam [HPat]
ps HExpr
e) <- [(HPat, HExpr)]
alts ]
        ns :: [String]
ns = [ String
n | HPVar 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 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 String
s) (HEVar String
s') = String
s String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
s'
eqPatExpr (HPCon String
s) (HECon String
s') = String
s String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
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
      [(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 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 String
s1) (HECon String
s2) = String
s1 String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
s2
alphaEq (HEVar String
s1) (HEVar String
s2) = String
s1 String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
s2
alphaEq (HETuple [HExpr]
es1) (HETuple [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 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 [(String, String)]
matchPat (HPVar String
s1) (HPVar String
s2) = [(String, String)] -> Maybe [(String, String)]
forall (m :: * -> *) a. Monad m => a -> m a
return [(String
s1, String
s2)]
matchPat (HPCon String
s1) (HPCon 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 [HPat]
ps1) (HPTuple [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 String
s1 HPat
p1) (HPAt String
s2 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 HPat
f1 HPat
a1) (HPApply HPat
f2 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 HPat
_ HPat
_ = Maybe [(String, String)]
forall a. Maybe a
Nothing

hESubst :: [(HSymbol, HSymbol)] -> HExpr -> HExpr
hESubst :: [(String, String)] -> HExpr -> HExpr
hESubst [(String, String)]
s (HELam [HPat]
ps 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 [(String, String)]
s (HEApply HExpr
f 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 [(String, String)]
_ e :: HExpr
e@(HECon String
_) = HExpr
e
hESubst [(String, String)]
s (HEVar 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 [(String, String)]
s (HETuple [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 [(String, String)]
s (HECase HExpr
e [(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) | (HPat
p, HExpr
b) <- [(HPat, HExpr)]
alts]

hPSubst :: [(HSymbol, HSymbol)] -> HPat -> HPat
hPSubst :: [(String, String)] -> HPat -> HPat
hPSubst [(String, String)]
s (HPVar 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 [(String, String)]
_ p :: HPat
p@(HPCon String
_) = HPat
p
hPSubst [(String, String)]
s (HPTuple [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 [(String, String)]
s (HPAt String
v 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 [(String, String)]
s (HPApply HPat
f 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 String
i Term
term =
  case Term -> HExpr
termToHExpr Term
term of
  HELam [HPat]
ps HExpr
e -> String -> [HPat] -> HExpr -> HClause
HClause String
i [HPat]
ps HExpr
e
  HExpr
e -> String -> [HPat] -> HExpr -> HClause
HClause String
i [] HExpr
e

remUnusedVars :: HExpr -> HExpr
remUnusedVars :: HExpr -> HExpr
remUnusedVars 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 [HPat]
ps HExpr
e) =
          let (HExpr
e', [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 HExpr
f HExpr
a) =
          let (HExpr
f', [String]
fs) = HExpr -> (HExpr, [String])
remE HExpr
f
              (HExpr
a', [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 [HExpr]
es) =
          let ([HExpr]
es', [[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 HExpr
e [(HPat, HExpr)]
alts) =
          let (HExpr
e', [String]
es) = HExpr -> (HExpr, [String])
remE HExpr
e
              ([(HPat, HExpr)]
alts', [[String]]
sss) = [((HPat, HExpr), [String])] -> ([(HPat, HExpr)], [[String]])
forall a b. [(a, b)] -> ([a], [b])
unzip [ let (HExpr
ee', [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) | (HPat
p, HExpr
ee) <- [(HPat, HExpr)]
alts ]
           in case [(HPat, HExpr)]
alts' of
                [(HPVar String
"_", HExpr
b)] -> (HExpr
b, [[String]] -> [String]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[String]]
sss)
                [(HPat, HExpr)]
_ -> (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 String
_) = (HExpr
e, [])
        remE e :: HExpr
e@(HEVar String
v) = (HExpr
e, [String
v])
        remP :: t String -> HPat -> HPat
remP t String
vs p :: HPat
p@(HPVar 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 String
"_"
        remP t String
_vs p :: HPat
p@(HPCon String
_) = HPat
p
        remP t String
vs (HPTuple [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 t String
vs (HPAt String
v 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 t String
vs (HPApply HPat
f 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 [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 String
"_") [HPat]
ps = String -> HPat
HPVar String
"_"
        hPTuple [HPat]
ps = [HPat] -> HPat
HPTuple [HPat]
ps

getBinderVars :: HClause -> [HSymbol]
getBinderVars :: HClause -> [String]
getBinderVars (HClause String
_ [HPat]
pats 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 HExpr
expr = HExpr -> [String]
gbExp HExpr
expr
  where gbExp :: HExpr -> [String]
gbExp (HELam [HPat]
ps 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 HExpr
f HExpr
a)    = HExpr -> [String]
gbExp HExpr
f [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ HExpr -> [String]
gbExp HExpr
a
        gbExp (HETuple [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 HExpr
se [(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 (\ (HPat
p, HExpr
e) -> HPat -> [String]
getBinderVarsHP HPat
p [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ HExpr -> [String]
gbExp HExpr
e) [(HPat, HExpr)]
alts
        gbExp HExpr
_ = []

getBinderVarsHP :: HPat -> [HSymbol]
getBinderVarsHP :: HPat -> [String]
getBinderVarsHP HPat
pat = HPat -> [String]
gbPat HPat
pat
  where gbPat :: HPat -> [String]
gbPat (HPVar String
s)     = [String
s]
        gbPat (HPCon String
_)     = []
        gbPat (HPTuple [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 String
s HPat
p)    = String
s String -> [String] -> [String]
forall a. a -> [a] -> [a]
: HPat -> [String]
gbPat HPat
p
        gbPat (HPApply HPat
f 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 HExpr
expr = HExpr -> [String]
gaExp HExpr
expr
  where gaExp :: HExpr -> [String]
gaExp (HELam [HPat]
_ps HExpr
e)    = HExpr -> [String]
gaExp HExpr
e
        gaExp (HEApply HExpr
f 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 [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 HExpr
se [(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 (\ (HPat
_p, HExpr
e) -> HExpr -> [String]
gaExp HExpr
e) [(HPat, HExpr)]
alts)
        gaExp (HEVar String
s)        = [String
s]
        gaExp HExpr
_                = []

etaReduce :: HExpr -> HExpr
etaReduce :: HExpr -> HExpr
etaReduce 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 String
v] (HEApply HExpr
f (HEVar 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 (HExpr
f', [String]
vs) = HExpr -> (HExpr, [String])
eta HExpr
f
        eta (HELam [HPat]
ps HExpr
e)    = ([HPat] -> HExpr -> HExpr
HELam [HPat]
ps HExpr
e', [String]
vs) where (HExpr
e', [String]
vs) = HExpr -> (HExpr, [String])
eta HExpr
e
        eta (HEApply HExpr
f HExpr
a)   = (HExpr -> HExpr -> HExpr
HEApply HExpr
f' HExpr
a', [String]
fvs[String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++[String]
avs) where (HExpr
f', [String]
fvs) = HExpr -> (HExpr, [String])
eta HExpr
f; (HExpr
a', [String]
avs) = HExpr -> (HExpr, [String])
eta HExpr
a
        eta e :: HExpr
e@(HECon String
_)     = (HExpr
e, [])
        eta e :: HExpr
e@(HEVar String
s)     = (HExpr
e, [String
s])
        eta (HETuple [HExpr]
es)    = ([HExpr] -> HExpr
HETuple [HExpr]
es', [[String]] -> [String]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[String]]
vss) where ([HExpr]
es', [[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 HExpr
e [(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 (HExpr
e', [String]
vs) = HExpr -> (HExpr, [String])
eta HExpr
e
                ([(HPat, HExpr)]
alts', [[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 (HExpr
a', [String]
ss) = HExpr -> (HExpr, [String])
eta HExpr
a in ((HPat
p, HExpr
a'), [String]
ss) | (HPat
p, HExpr
a) <- [(HPat, HExpr)]
alts ]