{-# 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 ]