{-# LANGUAGE CPP #-}
module Djinn.HTypes(
HKind(..),
HType(..),
HSymbol,
hTypeToFormula,
pHSymbol,
pHType,
pHDataType,
pHTAtom,
pHKind,
prHSymbolOp,
htNot,
isHTUnion,
getHTVars,
substHT,
HClause (..),
HPat (..),
HExpr (..),
hPrClause,
hPrExpr,
termToHExpr,
termToHClause,
getBinderVars
) where
import Control.Monad (zipWithM)
import Data.Char (isAlpha, isAlphaNum, isUpper)
import Data.List (union, (\\))
#if MIN_VERSION_base(4,11,0)
import Prelude hiding ((<>))
#endif
import Text.ParserCombinators.ReadP
import Text.PrettyPrint.HughesPJ (Doc, comma, fsep, nest, parens,
punctuate, renderStyle, sep,
style, text, vcat, ($$), (<+>), (<>))
import Djinn.LJTFormula
type HSymbol = String
data HKind = KStar
| KArrow HKind HKind
| KVar Int
deriving (HKind -> HKind -> Bool
(HKind -> HKind -> Bool) -> (HKind -> HKind -> Bool) -> Eq HKind
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: HKind -> HKind -> Bool
== :: HKind -> HKind -> Bool
$c/= :: HKind -> HKind -> Bool
/= :: HKind -> HKind -> Bool
Eq, Int -> HKind -> ShowS
[HKind] -> ShowS
HKind -> HSymbol
(Int -> HKind -> ShowS)
-> (HKind -> HSymbol) -> ([HKind] -> ShowS) -> Show HKind
forall a.
(Int -> a -> ShowS) -> (a -> HSymbol) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> HKind -> ShowS
showsPrec :: Int -> HKind -> ShowS
$cshow :: HKind -> HSymbol
show :: HKind -> HSymbol
$cshowList :: [HKind] -> ShowS
showList :: [HKind] -> ShowS
Show)
data HType = HTApp HType HType
| HTVar HSymbol
| HTCon HSymbol
| HTTuple [HType]
| HTArrow HType HType
| HTUnion [(HSymbol, [HType])]
| HTAbstract HSymbol HKind
deriving (HType -> HType -> Bool
(HType -> HType -> Bool) -> (HType -> HType -> Bool) -> Eq HType
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: HType -> HType -> Bool
== :: HType -> HType -> Bool
$c/= :: HType -> HType -> Bool
/= :: HType -> HType -> Bool
Eq)
isHTUnion :: HType -> Bool
isHTUnion :: HType -> Bool
isHTUnion (HTUnion [(HSymbol, [HType])]
_) = Bool
True
isHTUnion HType
_ = Bool
False
htNot :: HSymbol -> HType
htNot :: HSymbol -> HType
htNot HSymbol
x = HType -> HType -> HType
HTArrow (HSymbol -> HType
HTVar HSymbol
x) (HSymbol -> HType
HTCon HSymbol
"Void")
instance Show HType where
showsPrec :: Int -> HType -> ShowS
showsPrec Int
_ (HTApp (HTCon HSymbol
"[]") HType
t) = HSymbol -> ShowS
showString HSymbol
"[" ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> HType -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
0 HType
t ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HSymbol -> ShowS
showString HSymbol
"]"
showsPrec Int
p (HTApp HType
f HType
a) = Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
2) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ Int -> HType -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
2 HType
f ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HSymbol -> ShowS
showString HSymbol
" " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> HType -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
3 HType
a
showsPrec Int
_ (HTVar HSymbol
s) = HSymbol -> ShowS
showString HSymbol
s
showsPrec Int
_ (HTCon s :: HSymbol
s@(Char
c:HSymbol
_)) | Bool -> Bool
not (Char -> Bool
isAlpha Char
c) = Bool -> ShowS -> ShowS
showParen Bool
True (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ HSymbol -> ShowS
showString HSymbol
s
showsPrec Int
_ (HTCon HSymbol
s) = HSymbol -> ShowS
showString HSymbol
s
showsPrec Int
_ (HTTuple [HType]
ss) = Bool -> ShowS -> ShowS
showParen Bool
True (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ [HType] -> ShowS
forall {a}. Show a => [a] -> ShowS
f [HType]
ss
where f :: [a] -> ShowS
f [] = HSymbol -> ShowS
forall a. HasCallStack => HSymbol -> a
error HSymbol
"showsPrec HType"
f [a
t] = Int -> a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
0 a
t
f (a
t:[a]
ts) = Int -> a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
0 a
t ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HSymbol -> ShowS
showString HSymbol
", " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [a] -> ShowS
f [a]
ts
showsPrec Int
p (HTArrow HType
s HType
t) = Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ Int -> HType -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
1 HType
s ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HSymbol -> ShowS
showString HSymbol
" -> " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> HType -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
0 HType
t
showsPrec Int
_ (HTUnion [(HSymbol, [HType])]
cs) = [(HSymbol, [HType])] -> ShowS
forall {t :: * -> *} {a}.
(Foldable t, Show a) =>
[(HSymbol, t a)] -> ShowS
f [(HSymbol, [HType])]
cs
where f :: [(HSymbol, t a)] -> ShowS
f [] = ShowS
forall a. a -> a
id
f [(HSymbol, t a)
cts] = (HSymbol, t a) -> ShowS
forall {t :: * -> *} {a}.
(Foldable t, Show a) =>
(HSymbol, t a) -> ShowS
scts (HSymbol, t a)
cts
f ((HSymbol, t a)
cts : [(HSymbol, t a)]
ctss) = (HSymbol, t a) -> ShowS
forall {t :: * -> *} {a}.
(Foldable t, Show a) =>
(HSymbol, t a) -> ShowS
scts (HSymbol, t a)
cts ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HSymbol -> ShowS
showString HSymbol
" | " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(HSymbol, t a)] -> ShowS
f [(HSymbol, t a)]
ctss
scts :: (HSymbol, t a) -> ShowS
scts (HSymbol
c, t a
ts) = (ShowS -> a -> ShowS) -> ShowS -> t a -> ShowS
forall b a. (b -> a -> b) -> b -> t a -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\ ShowS
s a
t -> ShowS
s ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HSymbol -> ShowS
showString HSymbol
" " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
10 a
t) (HSymbol -> ShowS
showString HSymbol
c) t a
ts
showsPrec Int
_ (HTAbstract HSymbol
s HKind
_) = HSymbol -> ShowS
showString HSymbol
s
instance Read HType where
readsPrec :: Int -> ReadS HType
readsPrec Int
_ = ReadP HType -> ReadS HType
forall a. ReadP a -> ReadS a
readP_to_S ReadP HType
pHType'
pHType' :: ReadP HType
pHType' :: ReadP HType
pHType' = do
HType
t <- ReadP HType
pHType
ReadP ()
skipSpaces
HType -> ReadP HType
forall a. a -> ReadP a
forall (m :: * -> *) a. Monad m => a -> m a
return HType
t
pHType :: ReadP HType
pHType :: ReadP HType
pHType = do
[HType]
ts <- ReadP HType -> ReadP Char -> ReadP [HType]
forall a sep. ReadP a -> ReadP sep -> ReadP [a]
sepBy1 ReadP HType
pHTypeApp (do Char -> ReadP ()
schar Char
'-'; Char -> ReadP Char
char Char
'>')
HType -> ReadP HType
forall a. a -> ReadP a
forall (m :: * -> *) a. Monad m => a -> m a
return (HType -> ReadP HType) -> HType -> ReadP HType
forall a b. (a -> b) -> a -> b
$ (HType -> HType -> HType) -> [HType] -> HType
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 HType -> HType -> HType
HTArrow [HType]
ts
pHDataType :: ReadP HType
pHDataType :: ReadP HType
pHDataType = do
let con :: ReadP (HSymbol, [HType])
con = do HSymbol
c <- Bool -> ReadP HSymbol
pHSymbol Bool
True
[HType]
ts <- ReadP HType -> ReadP [HType]
forall a. ReadP a -> ReadP [a]
many ReadP HType
pHTAtom
(HSymbol, [HType]) -> ReadP (HSymbol, [HType])
forall a. a -> ReadP a
forall (m :: * -> *) a. Monad m => a -> m a
return (HSymbol
c, [HType]
ts)
[(HSymbol, [HType])]
cts <- ReadP (HSymbol, [HType]) -> ReadP () -> ReadP [(HSymbol, [HType])]
forall a sep. ReadP a -> ReadP sep -> ReadP [a]
sepBy ReadP (HSymbol, [HType])
con (Char -> ReadP ()
schar Char
'|')
HType -> ReadP HType
forall a. a -> ReadP a
forall (m :: * -> *) a. Monad m => a -> m a
return (HType -> ReadP HType) -> HType -> ReadP HType
forall a b. (a -> b) -> a -> b
$ [(HSymbol, [HType])] -> HType
HTUnion [(HSymbol, [HType])]
cts
pHTAtom :: ReadP HType
pHTAtom :: ReadP HType
pHTAtom = ReadP HType
pHTVar ReadP HType -> ReadP HType -> ReadP HType
forall a. ReadP a -> ReadP a -> ReadP a
+++ ReadP HType
pHTCon ReadP HType -> ReadP HType -> ReadP HType
forall a. ReadP a -> ReadP a -> ReadP a
+++ ReadP HType
pHTList ReadP HType -> ReadP HType -> ReadP HType
forall a. ReadP a -> ReadP a -> ReadP a
+++ ReadP HType -> ReadP HType
forall a. ReadP a -> ReadP a
pParen ReadP HType
pHTTuple ReadP HType -> ReadP HType -> ReadP HType
forall a. ReadP a -> ReadP a -> ReadP a
+++ ReadP HType -> ReadP HType
forall a. ReadP a -> ReadP a
pParen ReadP HType
pHType ReadP HType -> ReadP HType -> ReadP HType
forall a. ReadP a -> ReadP a -> ReadP a
+++ ReadP HType
pUnit
pUnit :: ReadP HType
pUnit :: ReadP HType
pUnit = do
Char -> ReadP ()
schar Char
'('
Char -> ReadP Char
char Char
')'
HType -> ReadP HType
forall a. a -> ReadP a
forall (m :: * -> *) a. Monad m => a -> m a
return (HType -> ReadP HType) -> HType -> ReadP HType
forall a b. (a -> b) -> a -> b
$ HSymbol -> HType
HTCon HSymbol
"()"
pHTCon :: ReadP HType
pHTCon :: ReadP HType
pHTCon = (Bool -> ReadP HSymbol
pHSymbol Bool
True ReadP HSymbol -> (HSymbol -> ReadP HType) -> ReadP HType
forall a b. ReadP a -> (a -> ReadP b) -> ReadP b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= HType -> ReadP HType
forall a. a -> ReadP a
forall (m :: * -> *) a. Monad m => a -> m a
return (HType -> ReadP HType)
-> (HSymbol -> HType) -> HSymbol -> ReadP HType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HSymbol -> HType
HTCon) ReadP HType -> ReadP HType -> ReadP HType
forall a. ReadP a -> ReadP a -> ReadP a
+++
do Char -> ReadP ()
schar Char
'('; Char -> ReadP ()
schar Char
'-'; Char -> ReadP ()
schar Char
'>'; Char -> ReadP ()
schar Char
')'; HType -> ReadP HType
forall a. a -> ReadP a
forall (m :: * -> *) a. Monad m => a -> m a
return (HSymbol -> HType
HTCon HSymbol
"->")
pHTVar :: ReadP HType
pHTVar :: ReadP HType
pHTVar = Bool -> ReadP HSymbol
pHSymbol Bool
False ReadP HSymbol -> (HSymbol -> ReadP HType) -> ReadP HType
forall a b. ReadP a -> (a -> ReadP b) -> ReadP b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= HType -> ReadP HType
forall a. a -> ReadP a
forall (m :: * -> *) a. Monad m => a -> m a
return (HType -> ReadP HType)
-> (HSymbol -> HType) -> HSymbol -> ReadP HType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HSymbol -> HType
HTVar
pHSymbol :: Bool -> ReadP HSymbol
pHSymbol :: Bool -> ReadP HSymbol
pHSymbol Bool
con = do
ReadP ()
skipSpaces
Char
c <- (Char -> Bool) -> ReadP Char
satisfy ((Char -> Bool) -> ReadP Char) -> (Char -> Bool) -> ReadP Char
forall a b. (a -> b) -> a -> b
$ \ Char
c -> Char -> Bool
isAlpha Char
c Bool -> Bool -> Bool
&& Char -> Bool
isUpper Char
c Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool
con
let isSym :: Char -> Bool
isSym Char
d = Char -> Bool
isAlphaNum Char
d Bool -> Bool -> Bool
|| Char
d Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'\'' Bool -> Bool -> Bool
|| Char
d Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'.'
HSymbol
cs <- (Char -> Bool) -> ReadP HSymbol
munch Char -> Bool
isSym
HSymbol -> ReadP HSymbol
forall a. a -> ReadP a
forall (m :: * -> *) a. Monad m => a -> m a
return (HSymbol -> ReadP HSymbol) -> HSymbol -> ReadP HSymbol
forall a b. (a -> b) -> a -> b
$ Char
cChar -> ShowS
forall a. a -> [a] -> [a]
:HSymbol
cs
pHTTuple :: ReadP HType
pHTTuple :: ReadP HType
pHTTuple = do
HType
t <- ReadP HType
pHType
[HType]
ts <- ReadP HType -> ReadP [HType]
forall a. ReadP a -> ReadP [a]
many1 (do Char -> ReadP ()
schar Char
','; ReadP HType
pHType)
HType -> ReadP HType
forall a. a -> ReadP a
forall (m :: * -> *) a. Monad m => a -> m a
return (HType -> ReadP HType) -> HType -> ReadP HType
forall a b. (a -> b) -> a -> b
$ [HType] -> HType
HTTuple ([HType] -> HType) -> [HType] -> HType
forall a b. (a -> b) -> a -> b
$ HType
tHType -> [HType] -> [HType]
forall a. a -> [a] -> [a]
:[HType]
ts
pHTypeApp :: ReadP HType
pHTypeApp :: ReadP HType
pHTypeApp = do
[HType]
ts <- ReadP HType -> ReadP [HType]
forall a. ReadP a -> ReadP [a]
many1 ReadP HType
pHTAtom
HType -> ReadP HType
forall a. a -> ReadP a
forall (m :: * -> *) a. Monad m => a -> m a
return (HType -> ReadP HType) -> HType -> ReadP HType
forall a b. (a -> b) -> a -> b
$ (HType -> HType -> HType) -> [HType] -> HType
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 HType -> HType -> HType
HTApp [HType]
ts
pHTList :: ReadP HType
pHTList :: ReadP HType
pHTList = do
Char -> ReadP ()
schar Char
'['
HType
t <- ReadP HType
pHType
Char -> ReadP ()
schar Char
']'
HType -> ReadP HType
forall a. a -> ReadP a
forall (m :: * -> *) a. Monad m => a -> m a
return (HType -> ReadP HType) -> HType -> ReadP HType
forall a b. (a -> b) -> a -> b
$ HType -> HType -> HType
HTApp (HSymbol -> HType
HTCon HSymbol
"[]") HType
t
pHKind :: ReadP HKind
pHKind :: ReadP HKind
pHKind = do
[HKind]
ts <- ReadP HKind -> ReadP Char -> ReadP [HKind]
forall a sep. ReadP a -> ReadP sep -> ReadP [a]
sepBy1 ReadP HKind
pHKindA (do Char -> ReadP ()
schar Char
'-'; Char -> ReadP Char
char Char
'>')
HKind -> ReadP HKind
forall a. a -> ReadP a
forall (m :: * -> *) a. Monad m => a -> m a
return (HKind -> ReadP HKind) -> HKind -> ReadP HKind
forall a b. (a -> b) -> a -> b
$ (HKind -> HKind -> HKind) -> [HKind] -> HKind
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 HKind -> HKind -> HKind
KArrow [HKind]
ts
pHKindA :: ReadP HKind
pHKindA :: ReadP HKind
pHKindA = (do Char -> ReadP ()
schar Char
'*'; HKind -> ReadP HKind
forall a. a -> ReadP a
forall (m :: * -> *) a. Monad m => a -> m a
return HKind
KStar) ReadP HKind -> ReadP HKind -> ReadP HKind
forall a. ReadP a -> ReadP a -> ReadP a
+++ ReadP HKind -> ReadP HKind
forall a. ReadP a -> ReadP a
pParen ReadP HKind
pHKind
pParen :: ReadP a -> ReadP a
pParen :: forall a. ReadP a -> ReadP a
pParen ReadP a
p = do
Char -> ReadP ()
schar Char
'('
a
e <- ReadP a
p
Char -> ReadP ()
schar Char
')'
a -> ReadP a
forall a. a -> ReadP a
forall (m :: * -> *) a. Monad m => a -> m a
return a
e
schar :: Char -> ReadP ()
schar :: Char -> ReadP ()
schar Char
c = do
ReadP ()
skipSpaces
Char -> ReadP Char
char Char
c
() -> ReadP ()
forall a. a -> ReadP a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
getHTVars :: HType -> [HSymbol]
getHTVars :: HType -> [HSymbol]
getHTVars (HTApp HType
f HType
a) = HType -> [HSymbol]
getHTVars HType
f [HSymbol] -> [HSymbol] -> [HSymbol]
forall a. Eq a => [a] -> [a] -> [a]
`union` HType -> [HSymbol]
getHTVars HType
a
getHTVars (HTVar HSymbol
v) = [HSymbol
v]
getHTVars (HTCon HSymbol
_) = []
getHTVars (HTTuple [HType]
ts) = ([HSymbol] -> [HSymbol] -> [HSymbol])
-> [HSymbol] -> [[HSymbol]] -> [HSymbol]
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr [HSymbol] -> [HSymbol] -> [HSymbol]
forall a. Eq a => [a] -> [a] -> [a]
union [] ((HType -> [HSymbol]) -> [HType] -> [[HSymbol]]
forall a b. (a -> b) -> [a] -> [b]
map HType -> [HSymbol]
getHTVars [HType]
ts)
getHTVars (HTArrow HType
f HType
a) = HType -> [HSymbol]
getHTVars HType
f [HSymbol] -> [HSymbol] -> [HSymbol]
forall a. Eq a => [a] -> [a] -> [a]
`union` HType -> [HSymbol]
getHTVars HType
a
getHTVars HType
_ = HSymbol -> [HSymbol]
forall a. HasCallStack => HSymbol -> a
error HSymbol
"getHTVars"
hTypeToFormula :: [(HSymbol, ([HSymbol], HType, a))] -> HType -> Formula
hTypeToFormula :: forall a. [(HSymbol, ([HSymbol], HType, a))] -> HType -> Formula
hTypeToFormula [(HSymbol, ([HSymbol], HType, a))]
ss (HTTuple [HType]
ts) = [Formula] -> Formula
Conj ((HType -> Formula) -> [HType] -> [Formula]
forall a b. (a -> b) -> [a] -> [b]
map ([(HSymbol, ([HSymbol], HType, a))] -> HType -> Formula
forall a. [(HSymbol, ([HSymbol], HType, a))] -> HType -> Formula
hTypeToFormula [(HSymbol, ([HSymbol], HType, a))]
ss) [HType]
ts)
hTypeToFormula [(HSymbol, ([HSymbol], HType, a))]
ss (HTArrow HType
t1 HType
t2) = [(HSymbol, ([HSymbol], HType, a))] -> HType -> Formula
forall a. [(HSymbol, ([HSymbol], HType, a))] -> HType -> Formula
hTypeToFormula [(HSymbol, ([HSymbol], HType, a))]
ss HType
t1 Formula -> Formula -> Formula
:-> [(HSymbol, ([HSymbol], HType, a))] -> HType -> Formula
forall a. [(HSymbol, ([HSymbol], HType, a))] -> HType -> Formula
hTypeToFormula [(HSymbol, ([HSymbol], HType, a))]
ss HType
t2
hTypeToFormula [(HSymbol, ([HSymbol], HType, a))]
ss (HTUnion [(HSymbol, [HType])]
ctss) = [(ConsDesc, Formula)] -> Formula
Disj [ (HSymbol -> Int -> ConsDesc
ConsDesc HSymbol
c ([HType] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [HType]
ts), [(HSymbol, ([HSymbol], HType, a))] -> HType -> Formula
forall a. [(HSymbol, ([HSymbol], HType, a))] -> HType -> Formula
hTypeToFormula [(HSymbol, ([HSymbol], HType, a))]
ss ([HType] -> HType
HTTuple [HType]
ts)) | (HSymbol
c, [HType]
ts) <- [(HSymbol, [HType])]
ctss ]
hTypeToFormula [(HSymbol, ([HSymbol], HType, a))]
ss HType
t = case [(HSymbol, ([HSymbol], HType, a))]
-> HType -> [HType] -> Maybe HType
forall a.
[(HSymbol, ([HSymbol], HType, a))]
-> HType -> [HType] -> Maybe HType
expandSyn [(HSymbol, ([HSymbol], HType, a))]
ss HType
t [] of
Maybe HType
Nothing -> Symbol -> Formula
PVar (Symbol -> Formula) -> Symbol -> Formula
forall a b. (a -> b) -> a -> b
$ HSymbol -> Symbol
Symbol (HSymbol -> Symbol) -> HSymbol -> Symbol
forall a b. (a -> b) -> a -> b
$ HType -> HSymbol
forall a. Show a => a -> HSymbol
show HType
t
Just HType
t' -> [(HSymbol, ([HSymbol], HType, a))] -> HType -> Formula
forall a. [(HSymbol, ([HSymbol], HType, a))] -> HType -> Formula
hTypeToFormula [(HSymbol, ([HSymbol], HType, a))]
ss HType
t'
expandSyn :: [(HSymbol, ([HSymbol], HType, a))] -> HType -> [HType] -> Maybe HType
expandSyn :: forall a.
[(HSymbol, ([HSymbol], HType, a))]
-> HType -> [HType] -> Maybe HType
expandSyn [(HSymbol, ([HSymbol], HType, a))]
ss (HTApp HType
f HType
a) [HType]
as = [(HSymbol, ([HSymbol], HType, a))]
-> HType -> [HType] -> Maybe HType
forall a.
[(HSymbol, ([HSymbol], HType, a))]
-> HType -> [HType] -> Maybe HType
expandSyn [(HSymbol, ([HSymbol], HType, a))]
ss HType
f (HType
aHType -> [HType] -> [HType]
forall a. a -> [a] -> [a]
:[HType]
as)
expandSyn [(HSymbol, ([HSymbol], HType, a))]
ss (HTCon HSymbol
c) [HType]
as = case HSymbol
-> [(HSymbol, ([HSymbol], HType, a))]
-> Maybe ([HSymbol], HType, a)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup HSymbol
c [(HSymbol, ([HSymbol], HType, a))]
ss of
Just ([HSymbol]
vs, HType
t, a
_) | [HSymbol] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [HSymbol]
vs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [HType] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [HType]
as -> HType -> Maybe HType
forall a. a -> Maybe a
Just (HType -> Maybe HType) -> HType -> Maybe HType
forall a b. (a -> b) -> a -> b
$ [(HSymbol, HType)] -> HType -> HType
substHT ([HSymbol] -> [HType] -> [(HSymbol, HType)]
forall a b. [a] -> [b] -> [(a, b)]
zip [HSymbol]
vs [HType]
as) HType
t
Maybe ([HSymbol], HType, a)
_ -> Maybe HType
forall a. Maybe a
Nothing
expandSyn [(HSymbol, ([HSymbol], HType, a))]
_ HType
_ [HType]
_ = Maybe HType
forall a. Maybe a
Nothing
substHT :: [(HSymbol, HType)] -> HType -> HType
substHT :: [(HSymbol, HType)] -> HType -> HType
substHT [(HSymbol, HType)]
r (HTApp HType
f HType
a) = HType -> HType -> HType
hTApp ([(HSymbol, HType)] -> HType -> HType
substHT [(HSymbol, HType)]
r HType
f) ([(HSymbol, HType)] -> HType -> HType
substHT [(HSymbol, HType)]
r HType
a)
substHT [(HSymbol, HType)]
r t :: HType
t@(HTVar HSymbol
v) = case HSymbol -> [(HSymbol, HType)] -> Maybe HType
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup HSymbol
v [(HSymbol, HType)]
r of
Maybe HType
Nothing -> HType
t
Just HType
t' -> HType
t'
substHT [(HSymbol, HType)]
_ t :: HType
t@(HTCon HSymbol
_) = HType
t
substHT [(HSymbol, HType)]
r (HTTuple [HType]
ts) = [HType] -> HType
HTTuple ((HType -> HType) -> [HType] -> [HType]
forall a b. (a -> b) -> [a] -> [b]
map ([(HSymbol, HType)] -> HType -> HType
substHT [(HSymbol, HType)]
r) [HType]
ts)
substHT [(HSymbol, HType)]
r (HTArrow HType
f HType
a) = HType -> HType -> HType
HTArrow ([(HSymbol, HType)] -> HType -> HType
substHT [(HSymbol, HType)]
r HType
f) ([(HSymbol, HType)] -> HType -> HType
substHT [(HSymbol, HType)]
r HType
a)
substHT [(HSymbol, HType)]
r (HTUnion ([(HSymbol, [HType])]
ctss)) = [(HSymbol, [HType])] -> HType
HTUnion [ (HSymbol
c, (HType -> HType) -> [HType] -> [HType]
forall a b. (a -> b) -> [a] -> [b]
map ([(HSymbol, HType)] -> HType -> HType
substHT [(HSymbol, HType)]
r) [HType]
ts) | (HSymbol
c, [HType]
ts) <- [(HSymbol, [HType])]
ctss ]
substHT [(HSymbol, HType)]
_ t :: HType
t@(HTAbstract HSymbol
_ HKind
_) = HType
t
hTApp :: HType -> HType -> HType
hTApp :: HType -> HType -> HType
hTApp (HTApp (HTCon HSymbol
"->") HType
a) HType
b = HType -> HType -> HType
HTArrow HType
a HType
b
hTApp HType
a HType
b = HType -> HType -> HType
HTApp HType
a HType
b
data HClause = HClause HSymbol [HPat] HExpr
deriving (Int -> HClause -> ShowS
[HClause] -> ShowS
HClause -> HSymbol
(Int -> HClause -> ShowS)
-> (HClause -> HSymbol) -> ([HClause] -> ShowS) -> Show HClause
forall a.
(Int -> a -> ShowS) -> (a -> HSymbol) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> HClause -> ShowS
showsPrec :: Int -> HClause -> ShowS
$cshow :: HClause -> HSymbol
show :: HClause -> HSymbol
$cshowList :: [HClause] -> ShowS
showList :: [HClause] -> ShowS
Show, HClause -> HClause -> Bool
(HClause -> HClause -> Bool)
-> (HClause -> HClause -> Bool) -> Eq HClause
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: HClause -> HClause -> Bool
== :: HClause -> HClause -> Bool
$c/= :: HClause -> HClause -> Bool
/= :: HClause -> HClause -> Bool
Eq)
data HPat = HPVar HSymbol
| HPCon HSymbol
| HPTuple [HPat]
| HPAt HSymbol HPat
| HPApply HPat HPat
deriving (Int -> HPat -> ShowS
[HPat] -> ShowS
HPat -> HSymbol
(Int -> HPat -> ShowS)
-> (HPat -> HSymbol) -> ([HPat] -> ShowS) -> Show HPat
forall a.
(Int -> a -> ShowS) -> (a -> HSymbol) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> HPat -> ShowS
showsPrec :: Int -> HPat -> ShowS
$cshow :: HPat -> HSymbol
show :: HPat -> HSymbol
$cshowList :: [HPat] -> ShowS
showList :: [HPat] -> ShowS
Show, HPat -> HPat -> Bool
(HPat -> HPat -> Bool) -> (HPat -> HPat -> Bool) -> Eq HPat
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: HPat -> HPat -> Bool
== :: HPat -> HPat -> Bool
$c/= :: HPat -> HPat -> Bool
/= :: HPat -> HPat -> Bool
Eq)
data HExpr = HELam [HPat] HExpr
| HEApply HExpr HExpr
| HECon HSymbol
| HEVar HSymbol
| HETuple [HExpr]
| HECase HExpr [(HPat, HExpr)]
deriving (Int -> HExpr -> ShowS
[HExpr] -> ShowS
HExpr -> HSymbol
(Int -> HExpr -> ShowS)
-> (HExpr -> HSymbol) -> ([HExpr] -> ShowS) -> Show HExpr
forall a.
(Int -> a -> ShowS) -> (a -> HSymbol) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> HExpr -> ShowS
showsPrec :: Int -> HExpr -> ShowS
$cshow :: HExpr -> HSymbol
show :: HExpr -> HSymbol
$cshowList :: [HExpr] -> ShowS
showList :: [HExpr] -> ShowS
Show, HExpr -> HExpr -> Bool
(HExpr -> HExpr -> Bool) -> (HExpr -> HExpr -> Bool) -> Eq HExpr
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: HExpr -> HExpr -> Bool
== :: HExpr -> HExpr -> Bool
$c/= :: HExpr -> HExpr -> Bool
/= :: HExpr -> HExpr -> Bool
Eq)
hPrClause :: HClause -> String
hPrClause :: HClause -> HSymbol
hPrClause HClause
c = Style -> Doc -> HSymbol
renderStyle Style
style (Doc -> HSymbol) -> Doc -> HSymbol
forall a b. (a -> b) -> a -> b
$ Int -> HClause -> Doc
ppClause Int
0 HClause
c
ppClause :: Int -> HClause -> Doc
ppClause :: Int -> HClause -> Doc
ppClause Int
_p (HClause HSymbol
f [HPat]
ps HExpr
e) = HSymbol -> Doc
text (ShowS
prHSymbolOp HSymbol
f) Doc -> Doc -> Doc
<+> [Doc] -> Doc
sep [[Doc] -> Doc
sep ((HPat -> Doc) -> [HPat] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> HPat -> Doc
ppPat Int
10) [HPat]
ps) Doc -> Doc -> Doc
<+> HSymbol -> Doc
text HSymbol
"=",
Int -> Doc -> Doc
nest Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Int -> HExpr -> Doc
ppExpr Int
0 HExpr
e]
prHSymbolOp :: HSymbol -> String
prHSymbolOp :: ShowS
prHSymbolOp s :: HSymbol
s@(Char
c:HSymbol
_) | Bool -> Bool
not (Char -> Bool
isAlphaNum Char
c) = HSymbol
"(" HSymbol -> ShowS
forall a. [a] -> [a] -> [a]
++ HSymbol
s HSymbol -> ShowS
forall a. [a] -> [a] -> [a]
++ HSymbol
")"
prHSymbolOp HSymbol
s = HSymbol
s
ppPat :: Int -> HPat -> Doc
ppPat :: Int -> HPat -> Doc
ppPat Int
_ (HPVar HSymbol
s) = HSymbol -> Doc
text HSymbol
s
ppPat Int
_ (HPCon HSymbol
s) = HSymbol -> Doc
text HSymbol
s
ppPat Int
_ (HPTuple [HPat]
ps) = Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
punctuate Doc
comma ((HPat -> Doc) -> [HPat] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> HPat -> Doc
ppPat Int
0) [HPat]
ps)
ppPat Int
_ (HPAt HSymbol
s HPat
p) = HSymbol -> Doc
text HSymbol
s Doc -> Doc -> Doc
<> HSymbol -> Doc
text HSymbol
"@" Doc -> Doc -> Doc
<> Int -> HPat -> Doc
ppPat Int
10 HPat
p
ppPat Int
p (HPApply HPat
a HPat
b) = Bool -> Doc -> Doc
pparens (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
1) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Int -> HPat -> Doc
ppPat Int
1 HPat
a Doc -> Doc -> Doc
<+> Int -> HPat -> Doc
ppPat Int
2 HPat
b
hPrExpr :: HExpr -> String
hPrExpr :: HExpr -> HSymbol
hPrExpr HExpr
e = Style -> Doc -> HSymbol
renderStyle Style
style (Doc -> HSymbol) -> Doc -> HSymbol
forall a b. (a -> b) -> a -> b
$ Int -> HExpr -> Doc
ppExpr Int
0 HExpr
e
ppExpr :: Int -> HExpr -> Doc
ppExpr :: Int -> HExpr -> Doc
ppExpr Int
p (HELam [HPat]
ps HExpr
e) = Bool -> Doc -> Doc
pparens (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
sep [ HSymbol -> Doc
text HSymbol
"\\" Doc -> Doc -> Doc
<+> [Doc] -> Doc
sep ((HPat -> Doc) -> [HPat] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> HPat -> Doc
ppPat Int
10) [HPat]
ps) Doc -> Doc -> Doc
<+> HSymbol -> Doc
text HSymbol
"->",
Int -> HExpr -> Doc
ppExpr Int
0 HExpr
e]
ppExpr Int
p (HEApply (HEApply (HEVar f :: HSymbol
f@(Char
c:HSymbol
_)) HExpr
a1) HExpr
a2) | Bool -> Bool
not (Char -> Bool
isAlphaNum Char
c) =
Bool -> Doc -> Doc
pparens (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
4) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Int -> HExpr -> Doc
ppExpr Int
5 HExpr
a1 Doc -> Doc -> Doc
<+> HSymbol -> Doc
text HSymbol
f Doc -> Doc -> Doc
<+> Int -> HExpr -> Doc
ppExpr Int
5 HExpr
a2
ppExpr Int
p (HEApply HExpr
f HExpr
a) = Bool -> Doc -> Doc
pparens (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
11) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Int -> HExpr -> Doc
ppExpr Int
11 HExpr
f Doc -> Doc -> Doc
<+> Int -> HExpr -> Doc
ppExpr Int
12 HExpr
a
ppExpr Int
_ (HECon HSymbol
s) = HSymbol -> Doc
text HSymbol
s
ppExpr Int
_ (HEVar s :: HSymbol
s@(Char
c:HSymbol
_)) | Bool -> Bool
not (Char -> Bool
isAlphaNum Char
c) = Bool -> Doc -> Doc
pparens Bool
True (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ HSymbol -> Doc
text HSymbol
s
ppExpr Int
_ (HEVar HSymbol
s) = HSymbol -> Doc
text HSymbol
s
ppExpr Int
_ (HETuple [HExpr]
es) = Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
punctuate Doc
comma ((HExpr -> Doc) -> [HExpr] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> HExpr -> Doc
ppExpr Int
0) [HExpr]
es)
ppExpr Int
p (HECase HExpr
s [(HPat, HExpr)]
alts) = Bool -> Doc -> Doc
pparens (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ (HSymbol -> Doc
text HSymbol
"case" Doc -> Doc -> Doc
<+> Int -> HExpr -> Doc
ppExpr Int
0 HExpr
s Doc -> Doc -> Doc
<+> HSymbol -> Doc
text HSymbol
"of") Doc -> Doc -> Doc
$$
Int -> Doc -> Doc
nest Int
2 ([Doc] -> Doc
vcat (((HPat, HExpr) -> Doc) -> [(HPat, HExpr)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (HPat, HExpr) -> Doc
ppAlt [(HPat, HExpr)]
alts))
where ppAlt :: (HPat, HExpr) -> Doc
ppAlt (HPat
pp, HExpr
e) = Int -> HPat -> Doc
ppPat Int
0 HPat
pp Doc -> Doc -> Doc
<+> HSymbol -> Doc
text HSymbol
"->" Doc -> Doc -> Doc
<+> Int -> HExpr -> Doc
ppExpr Int
0 HExpr
e
pparens :: Bool -> Doc -> Doc
pparens :: Bool -> Doc -> Doc
pparens Bool
True Doc
d = Doc -> Doc
parens Doc
d
pparens Bool
False Doc
d = Doc
d
unSymbol :: Symbol -> HSymbol
unSymbol :: Symbol -> HSymbol
unSymbol (Symbol HSymbol
s) = HSymbol
s
termToHExpr :: Term -> HExpr
termToHExpr :: Term -> HExpr
termToHExpr Term
term = HExpr -> HExpr
niceNames (HExpr -> HExpr) -> HExpr -> HExpr
forall a b. (a -> b) -> a -> b
$ HExpr -> HExpr
etaReduce (HExpr -> HExpr) -> HExpr -> HExpr
forall a b. (a -> b) -> a -> b
$ HExpr -> HExpr
remUnusedVars (HExpr -> HExpr) -> HExpr -> HExpr
forall a b. (a -> b) -> a -> b
$ HExpr -> HExpr
collapeCase (HExpr -> HExpr) -> HExpr -> HExpr
forall a b. (a -> b) -> a -> b
$ HExpr -> HExpr
fixSillyAt (HExpr -> HExpr) -> HExpr -> HExpr
forall a b. (a -> b) -> a -> b
$ HExpr -> HExpr
remUnusedVars (HExpr -> HExpr) -> HExpr -> HExpr
forall a b. (a -> b) -> a -> b
$ (HExpr, [(HSymbol, HPat)]) -> HExpr
forall a b. (a, b) -> a
fst ((HExpr, [(HSymbol, HPat)]) -> HExpr)
-> (HExpr, [(HSymbol, HPat)]) -> HExpr
forall a b. (a -> b) -> a -> b
$ [HSymbol] -> Term -> (HExpr, [(HSymbol, HPat)])
conv [] Term
term
where conv :: [HSymbol] -> Term -> (HExpr, [(HSymbol, HPat)])
conv [HSymbol]
_vs (Var Symbol
s) = (HSymbol -> HExpr
HEVar (HSymbol -> HExpr) -> HSymbol -> HExpr
forall a b. (a -> b) -> a -> b
$ Symbol -> HSymbol
unSymbol Symbol
s, [])
conv [HSymbol]
vs (Lam Symbol
s Term
te) =
let hs :: HSymbol
hs = Symbol -> HSymbol
unSymbol Symbol
s
(HExpr
te', [(HSymbol, HPat)]
ss) = [HSymbol] -> Term -> (HExpr, [(HSymbol, HPat)])
conv (HSymbol
hs HSymbol -> [HSymbol] -> [HSymbol]
forall a. a -> [a] -> [a]
: [HSymbol]
vs) Term
te
in ([HPat] -> HExpr -> HExpr
hELam [HSymbol -> [(HSymbol, HPat)] -> HPat
convV HSymbol
hs [(HSymbol, HPat)]
ss] HExpr
te', [(HSymbol, HPat)]
ss)
conv [HSymbol]
vs (Apply (Cinj (ConsDesc HSymbol
s Int
n) Int
_) Term
a) = (HExpr -> HExpr
forall a. a -> a
f (HExpr -> HExpr) -> HExpr -> HExpr
forall a b. (a -> b) -> a -> b
$ (HExpr -> HExpr -> HExpr) -> HExpr -> [HExpr] -> HExpr
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl HExpr -> HExpr -> HExpr
HEApply (HSymbol -> HExpr
HECon HSymbol
s) [HExpr]
as, [(HSymbol, HPat)]
ss)
where (a -> a
f, [HExpr]
as) = Int -> HExpr -> (a -> a, [HExpr])
forall {a}. Int -> HExpr -> (a -> a, [HExpr])
unTuple Int
n HExpr
ha
(HExpr
ha, [(HSymbol, HPat)]
ss) = [HSymbol] -> Term -> (HExpr, [(HSymbol, HPat)])
conv [HSymbol]
vs Term
a
conv [HSymbol]
vs (Apply Term
te1 Term
te2) = [HSymbol] -> Term -> [Term] -> (HExpr, [(HSymbol, HPat)])
convAp [HSymbol]
vs Term
te1 [Term
te2]
conv [HSymbol]
_vs (Ctuple Int
0) = (HSymbol -> HExpr
HECon HSymbol
"()", [])
conv [HSymbol]
_vs Term
e = HSymbol -> (HExpr, [(HSymbol, HPat)])
forall a. HasCallStack => HSymbol -> a
error (HSymbol -> (HExpr, [(HSymbol, HPat)]))
-> HSymbol -> (HExpr, [(HSymbol, HPat)])
forall a b. (a -> b) -> a -> b
$ HSymbol
"termToHExpr " HSymbol -> ShowS
forall a. [a] -> [a] -> [a]
++ Term -> HSymbol
forall a. Show a => a -> HSymbol
show Term
e
unTuple :: Int -> HExpr -> (a -> a, [HExpr])
unTuple Int
0 HExpr
_ = (a -> a
forall a. a -> a
id, [])
unTuple Int
1 HExpr
a = (a -> a
forall a. a -> a
id, [HExpr
a])
unTuple Int
n (HETuple [HExpr]
as) | [HExpr] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [HExpr]
as Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
n = (a -> a
forall a. a -> a
id, [HExpr]
as)
unTuple Int
n HExpr
e = HSymbol -> (a -> a, [HExpr])
forall a. HasCallStack => HSymbol -> a
error (HSymbol -> (a -> a, [HExpr])) -> HSymbol -> (a -> a, [HExpr])
forall a b. (a -> b) -> a -> b
$ HSymbol
"unTuple: unimplemented " HSymbol -> ShowS
forall a. [a] -> [a] -> [a]
++ (Int, HExpr) -> HSymbol
forall a. Show a => a -> HSymbol
show (Int
n, HExpr
e)
unTupleP :: Int -> HPat -> [HPat]
unTupleP Int
0 HPat
_ = []
unTupleP Int
n (HPTuple [HPat]
ps) | [HPat] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [HPat]
ps Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
n = [HPat]
ps
unTupleP Int
n HPat
p = HSymbol -> [HPat]
forall a. HasCallStack => HSymbol -> a
error (HSymbol -> [HPat]) -> HSymbol -> [HPat]
forall a b. (a -> b) -> a -> b
$ HSymbol
"unTupleP: unimplemented " HSymbol -> ShowS
forall a. [a] -> [a] -> [a]
++ (Int, HPat) -> HSymbol
forall a. Show a => a -> HSymbol
show (Int
n, HPat
p)
convAp :: [HSymbol] -> Term -> [Term] -> (HExpr, [(HSymbol, HPat)])
convAp [HSymbol]
vs (Apply Term
te1 Term
te2) [Term]
as = [HSymbol] -> Term -> [Term] -> (HExpr, [(HSymbol, HPat)])
convAp [HSymbol]
vs Term
te1 (Term
te2Term -> [Term] -> [Term]
forall a. a -> [a] -> [a]
:[Term]
as)
convAp [HSymbol]
vs (Ctuple Int
n) [Term]
as | [Term] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term]
as Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
n =
let ([HExpr]
es, [[(HSymbol, HPat)]]
sss) = [(HExpr, [(HSymbol, HPat)])] -> ([HExpr], [[(HSymbol, HPat)]])
forall a b. [(a, b)] -> ([a], [b])
unzip ([(HExpr, [(HSymbol, HPat)])] -> ([HExpr], [[(HSymbol, HPat)]]))
-> [(HExpr, [(HSymbol, HPat)])] -> ([HExpr], [[(HSymbol, HPat)]])
forall a b. (a -> b) -> a -> b
$ (Term -> (HExpr, [(HSymbol, HPat)]))
-> [Term] -> [(HExpr, [(HSymbol, HPat)])]
forall a b. (a -> b) -> [a] -> [b]
map ([HSymbol] -> Term -> (HExpr, [(HSymbol, HPat)])
conv [HSymbol]
vs) [Term]
as
in ([HExpr] -> HExpr
hETuple [HExpr]
es, [[(HSymbol, HPat)]] -> [(HSymbol, HPat)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[(HSymbol, HPat)]]
sss)
convAp [HSymbol]
vs (Ccases [ConsDesc]
cds) (Term
se : [Term]
es) =
let ([(HPat, HExpr)]
alts, [[(HSymbol, HPat)]]
ass) = [((HPat, HExpr), [(HSymbol, HPat)])]
-> ([(HPat, HExpr)], [[(HSymbol, HPat)]])
forall a b. [(a, b)] -> ([a], [b])
unzip ([((HPat, HExpr), [(HSymbol, HPat)])]
-> ([(HPat, HExpr)], [[(HSymbol, HPat)]]))
-> [((HPat, HExpr), [(HSymbol, HPat)])]
-> ([(HPat, HExpr)], [[(HSymbol, HPat)]])
forall a b. (a -> b) -> a -> b
$ (Term -> ConsDesc -> ((HPat, HExpr), [(HSymbol, HPat)]))
-> [Term] -> [ConsDesc] -> [((HPat, HExpr), [(HSymbol, HPat)])]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Term -> ConsDesc -> ((HPat, HExpr), [(HSymbol, HPat)])
cAlt [Term]
es [ConsDesc]
cds
cAlt :: Term -> ConsDesc -> ((HPat, HExpr), [(HSymbol, HPat)])
cAlt (Lam Symbol
v Term
e) (ConsDesc HSymbol
c Int
n) =
let hv :: HSymbol
hv = Symbol -> HSymbol
unSymbol Symbol
v
(HExpr
he, [(HSymbol, HPat)]
ss) = [HSymbol] -> Term -> (HExpr, [(HSymbol, HPat)])
conv (HSymbol
hv HSymbol -> [HSymbol] -> [HSymbol]
forall a. a -> [a] -> [a]
: [HSymbol]
vs) Term
e
ps :: [HPat]
ps = case HSymbol -> [(HSymbol, HPat)] -> Maybe HPat
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup HSymbol
hv [(HSymbol, HPat)]
ss of
Maybe HPat
Nothing -> Int -> HPat -> [HPat]
forall a. Int -> a -> [a]
replicate Int
n (HSymbol -> HPat
HPVar HSymbol
"_")
Just HPat
p -> Int -> HPat -> [HPat]
unTupleP Int
n HPat
p
in (((HPat -> HPat -> HPat) -> HPat -> [HPat] -> HPat
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl HPat -> HPat -> HPat
HPApply (HSymbol -> HPat
HPCon HSymbol
c) [HPat]
ps, HExpr
he), [(HSymbol, HPat)]
ss)
cAlt Term
e ConsDesc
_ = HSymbol -> ((HPat, HExpr), [(HSymbol, HPat)])
forall a. HasCallStack => HSymbol -> a
error (HSymbol -> ((HPat, HExpr), [(HSymbol, HPat)]))
-> HSymbol -> ((HPat, HExpr), [(HSymbol, HPat)])
forall a b. (a -> b) -> a -> b
$ HSymbol
"cAlt " HSymbol -> ShowS
forall a. [a] -> [a] -> [a]
++ Term -> HSymbol
forall a. Show a => a -> HSymbol
show Term
e
(HExpr
e', [(HSymbol, HPat)]
ess) = [HSymbol] -> Term -> (HExpr, [(HSymbol, HPat)])
conv [HSymbol]
vs Term
se
in (HExpr -> [(HPat, HExpr)] -> HExpr
hECase HExpr
e' [(HPat, HExpr)]
alts, [(HSymbol, HPat)]
ess [(HSymbol, HPat)] -> [(HSymbol, HPat)] -> [(HSymbol, HPat)]
forall a. [a] -> [a] -> [a]
++ [[(HSymbol, HPat)]] -> [(HSymbol, HPat)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[(HSymbol, HPat)]]
ass)
convAp [HSymbol]
vs (Csplit Int
n) (Term
b : Term
a : [Term]
as) =
let (HExpr
hb, [(HSymbol, HPat)]
sb) = [HSymbol] -> Term -> (HExpr, [(HSymbol, HPat)])
conv [HSymbol]
vs Term
b
(HExpr
a', [(HSymbol, HPat)]
sa) = [HSymbol] -> Term -> (HExpr, [(HSymbol, HPat)])
conv [HSymbol]
vs Term
a
([HExpr]
as', [[(HSymbol, HPat)]]
sss) = [(HExpr, [(HSymbol, HPat)])] -> ([HExpr], [[(HSymbol, HPat)]])
forall a b. [(a, b)] -> ([a], [b])
unzip ([(HExpr, [(HSymbol, HPat)])] -> ([HExpr], [[(HSymbol, HPat)]]))
-> [(HExpr, [(HSymbol, HPat)])] -> ([HExpr], [[(HSymbol, HPat)]])
forall a b. (a -> b) -> a -> b
$ (Term -> (HExpr, [(HSymbol, HPat)]))
-> [Term] -> [(HExpr, [(HSymbol, HPat)])]
forall a b. (a -> b) -> [a] -> [b]
map ([HSymbol] -> Term -> (HExpr, [(HSymbol, HPat)])
conv [HSymbol]
vs) [Term]
as
([HPat]
ps, HExpr
b') = Int -> HExpr -> ([HPat], HExpr)
unLam Int
n HExpr
hb
unLam :: Int -> HExpr -> ([HPat], HExpr)
unLam Int
0 HExpr
e = ([], HExpr
e)
unLam Int
k (HELam [HPat]
ps0 HExpr
e) | [HPat] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [HPat]
ps0 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
n = let ([HPat]
ps1, [HPat]
ps2) = Int -> [HPat] -> ([HPat], [HPat])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
k [HPat]
ps0 in ([HPat]
ps1, [HPat] -> HExpr -> HExpr
hELam [HPat]
ps2 HExpr
e)
unLam Int
k HExpr
e = HSymbol -> ([HPat], HExpr)
forall a. HasCallStack => HSymbol -> a
error (HSymbol -> ([HPat], HExpr)) -> HSymbol -> ([HPat], HExpr)
forall a b. (a -> b) -> a -> b
$ HSymbol
"unLam: unimplemented" HSymbol -> ShowS
forall a. [a] -> [a] -> [a]
++ (Int, HExpr) -> HSymbol
forall a. Show a => a -> HSymbol
show (Int
k, HExpr
e)
in case HExpr
a' of
HEVar HSymbol
v | HSymbol
v HSymbol -> [HSymbol] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [HSymbol]
vs Bool -> Bool -> Bool
&& [Term] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Term]
as -> (HExpr
b', [(HSymbol
v, [HPat] -> HPat
HPTuple [HPat]
ps)] [(HSymbol, HPat)] -> [(HSymbol, HPat)] -> [(HSymbol, HPat)]
forall a. [a] -> [a] -> [a]
++ [(HSymbol, HPat)]
sb [(HSymbol, HPat)] -> [(HSymbol, HPat)] -> [(HSymbol, HPat)]
forall a. [a] -> [a] -> [a]
++ [(HSymbol, HPat)]
sa)
HExpr
_ -> ((HExpr -> HExpr -> HExpr) -> HExpr -> [HExpr] -> HExpr
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr HExpr -> HExpr -> HExpr
HEApply (HExpr -> [(HPat, HExpr)] -> HExpr
hECase HExpr
a' [([HPat] -> HPat
HPTuple [HPat]
ps, HExpr
b')]) [HExpr]
as', [(HSymbol, HPat)]
sb [(HSymbol, HPat)] -> [(HSymbol, HPat)] -> [(HSymbol, HPat)]
forall a. [a] -> [a] -> [a]
++ [(HSymbol, HPat)]
sa [(HSymbol, HPat)] -> [(HSymbol, HPat)] -> [(HSymbol, HPat)]
forall a. [a] -> [a] -> [a]
++ [[(HSymbol, HPat)]] -> [(HSymbol, HPat)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[(HSymbol, HPat)]]
sss)
convAp [HSymbol]
vs Term
f [Term]
as =
let ([HExpr]
es, [[(HSymbol, HPat)]]
sss) = [(HExpr, [(HSymbol, HPat)])] -> ([HExpr], [[(HSymbol, HPat)]])
forall a b. [(a, b)] -> ([a], [b])
unzip ([(HExpr, [(HSymbol, HPat)])] -> ([HExpr], [[(HSymbol, HPat)]]))
-> [(HExpr, [(HSymbol, HPat)])] -> ([HExpr], [[(HSymbol, HPat)]])
forall a b. (a -> b) -> a -> b
$ (Term -> (HExpr, [(HSymbol, HPat)]))
-> [Term] -> [(HExpr, [(HSymbol, HPat)])]
forall a b. (a -> b) -> [a] -> [b]
map ([HSymbol] -> Term -> (HExpr, [(HSymbol, HPat)])
conv [HSymbol]
vs) (Term
fTerm -> [Term] -> [Term]
forall a. a -> [a] -> [a]
:[Term]
as)
in ((HExpr -> HExpr -> HExpr) -> [HExpr] -> HExpr
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 HExpr -> HExpr -> HExpr
HEApply [HExpr]
es, [[(HSymbol, HPat)]] -> [(HSymbol, HPat)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[(HSymbol, HPat)]]
sss)
convV :: HSymbol -> [(HSymbol, HPat)] -> HPat
convV HSymbol
hs [(HSymbol, HPat)]
ss = case [ HPat
y | (HSymbol
x, HPat
y) <- [(HSymbol, HPat)]
ss, HSymbol
x HSymbol -> HSymbol -> Bool
forall a. Eq a => a -> a -> Bool
== HSymbol
hs ] of
[] -> HSymbol -> HPat
HPVar HSymbol
hs
[HPat
p] -> HSymbol -> HPat -> HPat
HPAt HSymbol
hs HPat
p
[HPat]
ps -> HSymbol -> HPat -> HPat
HPAt HSymbol
hs (HPat -> HPat) -> HPat -> HPat
forall a b. (a -> b) -> a -> b
$ (HPat -> HPat -> HPat) -> [HPat] -> HPat
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 HPat -> HPat -> HPat
combPat [HPat]
ps
combPat :: HPat -> HPat -> HPat
combPat HPat
p HPat
p' | HPat
p HPat -> HPat -> Bool
forall a. Eq a => a -> a -> Bool
== HPat
p' = HPat
p
combPat (HPVar HSymbol
v) HPat
p = HSymbol -> HPat -> HPat
HPAt HSymbol
v HPat
p
combPat HPat
p (HPVar HSymbol
v) = HSymbol -> HPat -> HPat
HPAt HSymbol
v HPat
p
combPat (HPTuple [HPat]
ps) (HPTuple [HPat]
ps') = [HPat] -> HPat
HPTuple ((HPat -> HPat -> HPat) -> [HPat] -> [HPat] -> [HPat]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith HPat -> HPat -> HPat
combPat [HPat]
ps [HPat]
ps')
combPat HPat
p HPat
p' = HSymbol -> HPat
forall a. HasCallStack => HSymbol -> a
error (HSymbol -> HPat) -> HSymbol -> HPat
forall a b. (a -> b) -> a -> b
$ HSymbol
"unimplemented combPat: " HSymbol -> ShowS
forall a. [a] -> [a] -> [a]
++ (HPat, HPat) -> HSymbol
forall a. Show a => a -> HSymbol
show (HPat
p, HPat
p')
hETuple :: [HExpr] -> HExpr
hETuple [HExpr
e] = HExpr
e
hETuple [HExpr]
es = [HExpr] -> HExpr
HETuple [HExpr]
es
fixSillyAt :: HExpr -> HExpr
fixSillyAt :: HExpr -> HExpr
fixSillyAt = [(HSymbol, HSymbol)] -> HExpr -> HExpr
fixAt []
where fixAt :: [(HSymbol, HSymbol)] -> HExpr -> HExpr
fixAt [(HSymbol, HSymbol)]
s (HELam [HPat]
ps HExpr
e) = [HPat] -> HExpr -> HExpr
HELam [HPat]
ps' ([(HSymbol, HSymbol)] -> HExpr -> HExpr
fixAt ([[(HSymbol, HSymbol)]] -> [(HSymbol, HSymbol)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[(HSymbol, HSymbol)]]
ss [(HSymbol, HSymbol)]
-> [(HSymbol, HSymbol)] -> [(HSymbol, HSymbol)]
forall a. [a] -> [a] -> [a]
++ [(HSymbol, HSymbol)]
s) HExpr
e) where ([HPat]
ps', [[(HSymbol, HSymbol)]]
ss) = [(HPat, [(HSymbol, HSymbol)])] -> ([HPat], [[(HSymbol, HSymbol)]])
forall a b. [(a, b)] -> ([a], [b])
unzip ([(HPat, [(HSymbol, HSymbol)])]
-> ([HPat], [[(HSymbol, HSymbol)]]))
-> [(HPat, [(HSymbol, HSymbol)])]
-> ([HPat], [[(HSymbol, HSymbol)]])
forall a b. (a -> b) -> a -> b
$ (HPat -> (HPat, [(HSymbol, HSymbol)]))
-> [HPat] -> [(HPat, [(HSymbol, HSymbol)])]
forall a b. (a -> b) -> [a] -> [b]
map HPat -> (HPat, [(HSymbol, HSymbol)])
findSilly [HPat]
ps
fixAt [(HSymbol, HSymbol)]
s (HEApply HExpr
f HExpr
a) = HExpr -> HExpr -> HExpr
HEApply ([(HSymbol, HSymbol)] -> HExpr -> HExpr
fixAt [(HSymbol, HSymbol)]
s HExpr
f) ([(HSymbol, HSymbol)] -> HExpr -> HExpr
fixAt [(HSymbol, HSymbol)]
s HExpr
a)
fixAt [(HSymbol, HSymbol)]
_ e :: HExpr
e@(HECon HSymbol
_) = HExpr
e
fixAt [(HSymbol, HSymbol)]
s e :: HExpr
e@(HEVar HSymbol
v) = HExpr -> (HSymbol -> HExpr) -> Maybe HSymbol -> HExpr
forall b a. b -> (a -> b) -> Maybe a -> b
maybe HExpr
e HSymbol -> HExpr
HEVar (Maybe HSymbol -> HExpr) -> Maybe HSymbol -> HExpr
forall a b. (a -> b) -> a -> b
$ HSymbol -> [(HSymbol, HSymbol)] -> Maybe HSymbol
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup HSymbol
v [(HSymbol, HSymbol)]
s
fixAt [(HSymbol, HSymbol)]
s (HETuple [HExpr]
es) = [HExpr] -> HExpr
HETuple ((HExpr -> HExpr) -> [HExpr] -> [HExpr]
forall a b. (a -> b) -> [a] -> [b]
map ([(HSymbol, HSymbol)] -> HExpr -> HExpr
fixAt [(HSymbol, HSymbol)]
s) [HExpr]
es)
fixAt [(HSymbol, HSymbol)]
s (HECase HExpr
e [(HPat, HExpr)]
alts) = HExpr -> [(HPat, HExpr)] -> HExpr
HECase ([(HSymbol, HSymbol)] -> HExpr -> HExpr
fixAt [(HSymbol, HSymbol)]
s HExpr
e) (((HPat, HExpr) -> (HPat, HExpr))
-> [(HPat, HExpr)] -> [(HPat, HExpr)]
forall a b. (a -> b) -> [a] -> [b]
map ([(HSymbol, HSymbol)] -> (HPat, HExpr) -> (HPat, HExpr)
fixAtAlt [(HSymbol, HSymbol)]
s) [(HPat, HExpr)]
alts)
fixAtAlt :: [(HSymbol, HSymbol)] -> (HPat, HExpr) -> (HPat, HExpr)
fixAtAlt [(HSymbol, HSymbol)]
s (HPat
p, HExpr
e) = (HPat
p', [(HSymbol, HSymbol)] -> HExpr -> HExpr
fixAt ([(HSymbol, HSymbol)]
s' [(HSymbol, HSymbol)]
-> [(HSymbol, HSymbol)] -> [(HSymbol, HSymbol)]
forall a. [a] -> [a] -> [a]
++ [(HSymbol, HSymbol)]
s) HExpr
e) where (HPat
p', [(HSymbol, HSymbol)]
s') = HPat -> (HPat, [(HSymbol, HSymbol)])
findSilly HPat
p
findSilly :: HPat -> (HPat, [(HSymbol, HSymbol)])
findSilly p :: HPat
p@(HPVar HSymbol
_) = (HPat
p, [])
findSilly p :: HPat
p@(HPCon HSymbol
_) = (HPat
p, [])
findSilly (HPTuple [HPat]
ps) = ([HPat] -> HPat
HPTuple [HPat]
ps', [[(HSymbol, HSymbol)]] -> [(HSymbol, HSymbol)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[(HSymbol, HSymbol)]]
ss) where ([HPat]
ps', [[(HSymbol, HSymbol)]]
ss) = [(HPat, [(HSymbol, HSymbol)])] -> ([HPat], [[(HSymbol, HSymbol)]])
forall a b. [(a, b)] -> ([a], [b])
unzip ([(HPat, [(HSymbol, HSymbol)])]
-> ([HPat], [[(HSymbol, HSymbol)]]))
-> [(HPat, [(HSymbol, HSymbol)])]
-> ([HPat], [[(HSymbol, HSymbol)]])
forall a b. (a -> b) -> a -> b
$ (HPat -> (HPat, [(HSymbol, HSymbol)]))
-> [HPat] -> [(HPat, [(HSymbol, HSymbol)])]
forall a b. (a -> b) -> [a] -> [b]
map HPat -> (HPat, [(HSymbol, HSymbol)])
findSilly [HPat]
ps
findSilly (HPAt HSymbol
v HPat
p) = case HPat -> (HPat, [(HSymbol, HSymbol)])
findSilly HPat
p of
(p' :: HPat
p'@(HPVar HSymbol
v'), [(HSymbol, HSymbol)]
s) -> (HPat
p', (HSymbol
v, HSymbol
v')(HSymbol, HSymbol) -> [(HSymbol, HSymbol)] -> [(HSymbol, HSymbol)]
forall a. a -> [a] -> [a]
:[(HSymbol, HSymbol)]
s)
(HPat
p', [(HSymbol, HSymbol)]
s) -> (HSymbol -> HPat -> HPat
HPAt HSymbol
v HPat
p', [(HSymbol, HSymbol)]
s)
findSilly (HPApply HPat
f HPat
a) = (HPat -> HPat -> HPat
HPApply HPat
f' HPat
a', [(HSymbol, HSymbol)]
sf [(HSymbol, HSymbol)]
-> [(HSymbol, HSymbol)] -> [(HSymbol, HSymbol)]
forall a. [a] -> [a] -> [a]
++ [(HSymbol, HSymbol)]
sa) where (HPat
f', [(HSymbol, HSymbol)]
sf) = HPat -> (HPat, [(HSymbol, HSymbol)])
findSilly HPat
f; (HPat
a', [(HSymbol, HSymbol)]
sa) = HPat -> (HPat, [(HSymbol, HSymbol)])
findSilly HPat
a
collapeCase :: HExpr -> HExpr
collapeCase :: HExpr -> HExpr
collapeCase (HELam [HPat]
ps HExpr
e) = [HPat] -> HExpr -> HExpr
HELam [HPat]
ps (HExpr -> HExpr
collapeCase HExpr
e)
collapeCase (HEApply HExpr
f HExpr
a) = HExpr -> HExpr -> HExpr
HEApply (HExpr -> HExpr
collapeCase HExpr
f) (HExpr -> HExpr
collapeCase HExpr
a)
collapeCase e :: HExpr
e@(HECon HSymbol
_) = HExpr
e
collapeCase e :: HExpr
e@(HEVar HSymbol
_) = HExpr
e
collapeCase (HETuple [HExpr]
es) = [HExpr] -> HExpr
HETuple ((HExpr -> HExpr) -> [HExpr] -> [HExpr]
forall a b. (a -> b) -> [a] -> [b]
map HExpr -> HExpr
collapeCase [HExpr]
es)
collapeCase (HECase HExpr
e [(HPat, HExpr)]
alts) = case [(HPat
p, HExpr -> HExpr
collapeCase HExpr
b) | (HPat
p, HExpr
b) <- [(HPat, HExpr)]
alts ] of
(HPat
p, HExpr
b) : [(HPat, HExpr)]
pes | HPat -> Bool
noBound HPat
p Bool -> Bool -> Bool
&& ((HPat, HExpr) -> Bool) -> [(HPat, HExpr)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\ (HPat
p', HExpr
b') -> HExpr -> HExpr -> Bool
alphaEq HExpr
b HExpr
b' Bool -> Bool -> Bool
&& HPat -> Bool
noBound HPat
p') [(HPat, HExpr)]
pes -> HExpr
b
[(HPat, HExpr)]
pes -> HExpr -> [(HPat, HExpr)] -> HExpr
HECase (HExpr -> HExpr
collapeCase HExpr
e) [(HPat, HExpr)]
pes
where noBound :: HPat -> Bool
noBound = (HSymbol -> Bool) -> [HSymbol] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (HSymbol -> HSymbol -> Bool
forall a. Eq a => a -> a -> Bool
== HSymbol
"_") ([HSymbol] -> Bool) -> (HPat -> [HSymbol]) -> HPat -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HPat -> [HSymbol]
getBinderVarsHP
niceNames :: HExpr -> HExpr
niceNames :: HExpr -> HExpr
niceNames HExpr
e =
let bvars :: [HSymbol]
bvars = (HSymbol -> Bool) -> [HSymbol] -> [HSymbol]
forall a. (a -> Bool) -> [a] -> [a]
filter (HSymbol -> HSymbol -> Bool
forall a. Eq a => a -> a -> Bool
/= HSymbol
"_") ([HSymbol] -> [HSymbol]) -> [HSymbol] -> [HSymbol]
forall a b. (a -> b) -> a -> b
$ HExpr -> [HSymbol]
getBinderVarsHE HExpr
e
nvars :: [HSymbol]
nvars = [[Char
c] | Char
c <- [Char
'a'..Char
'z']] [HSymbol] -> [HSymbol] -> [HSymbol]
forall a. [a] -> [a] -> [a]
++ [ HSymbol
"x" HSymbol -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> HSymbol
forall a. Show a => a -> HSymbol
show Integer
i | Integer
i <- [Integer
1::Integer ..]]
freevars :: [HSymbol]
freevars = HExpr -> [HSymbol]
getAllVars HExpr
e [HSymbol] -> [HSymbol] -> [HSymbol]
forall a. Eq a => [a] -> [a] -> [a]
\\ [HSymbol]
bvars
vars :: [HSymbol]
vars = [HSymbol]
nvars [HSymbol] -> [HSymbol] -> [HSymbol]
forall a. Eq a => [a] -> [a] -> [a]
\\ [HSymbol]
freevars
sub :: [(HSymbol, HSymbol)]
sub = [HSymbol] -> [HSymbol] -> [(HSymbol, HSymbol)]
forall a b. [a] -> [b] -> [(a, b)]
zip [HSymbol]
bvars [HSymbol]
vars
in [(HSymbol, HSymbol)] -> HExpr -> HExpr
hESubst [(HSymbol, HSymbol)]
sub HExpr
e
hELam :: [HPat] -> HExpr -> HExpr
hELam :: [HPat] -> HExpr -> HExpr
hELam [] HExpr
e = HExpr
e
hELam [HPat]
ps (HELam [HPat]
ps' HExpr
e) = [HPat] -> HExpr -> HExpr
HELam ([HPat]
ps [HPat] -> [HPat] -> [HPat]
forall a. [a] -> [a] -> [a]
++ [HPat]
ps') HExpr
e
hELam [HPat]
ps HExpr
e = [HPat] -> HExpr -> HExpr
HELam [HPat]
ps HExpr
e
hECase :: HExpr -> [(HPat, HExpr)] -> HExpr
hECase :: HExpr -> [(HPat, HExpr)] -> HExpr
hECase HExpr
e [] = HExpr -> HExpr -> HExpr
HEApply (HSymbol -> HExpr
HEVar HSymbol
"void") HExpr
e
hECase HExpr
_ [(HPCon HSymbol
"()", HExpr
e)] = HExpr
e
hECase HExpr
e [(HPat, HExpr)]
pes | ((HPat, HExpr) -> Bool) -> [(HPat, HExpr)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ((HPat -> HExpr -> Bool) -> (HPat, HExpr) -> Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry HPat -> HExpr -> Bool
eqPatExpr) [(HPat, HExpr)]
pes = HExpr
e
hECase HExpr
e [(HPat
p, HELam [HPat]
ps HExpr
b)] = [HPat] -> HExpr -> HExpr
HELam [HPat]
ps (HExpr -> HExpr) -> HExpr -> HExpr
forall a b. (a -> b) -> a -> b
$ HExpr -> [(HPat, HExpr)] -> HExpr
hECase HExpr
e [(HPat
p, HExpr
b)]
hECase HExpr
se alts :: [(HPat, HExpr)]
alts@((HPat
_, HELam [HPat]
ops HExpr
_):[(HPat, HExpr)]
_) | Int
m Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0 = [HPat] -> HExpr -> HExpr
HELam (Int -> [HPat] -> [HPat]
forall a. Int -> [a] -> [a]
take Int
m [HPat]
ops) (HExpr -> HExpr) -> HExpr -> HExpr
forall a b. (a -> b) -> a -> b
$ HExpr -> [(HPat, HExpr)] -> HExpr
hECase HExpr
se [(HPat, HExpr)]
alts'
where m :: Int
m = [Int] -> Int
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
minimum (((HPat, HExpr) -> Int) -> [(HPat, HExpr)] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (HExpr -> Int
numBind (HExpr -> Int) -> ((HPat, HExpr) -> HExpr) -> (HPat, HExpr) -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (HPat, HExpr) -> HExpr
forall a b. (a, b) -> b
snd) [(HPat, HExpr)]
alts)
numBind :: HExpr -> Int
numBind (HELam [HPat]
ps HExpr
_) = [HPat] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ((HPat -> Bool) -> [HPat] -> [HPat]
forall a. (a -> Bool) -> [a] -> [a]
takeWhile HPat -> Bool
isPVar [HPat]
ps)
numBind HExpr
_ = Int
0
isPVar :: HPat -> Bool
isPVar (HPVar HSymbol
_) = Bool
True
isPVar HPat
_ = Bool
False
alts' :: [(HPat, HExpr)]
alts' = [ let ([HPat]
ps1, [HPat]
ps2) = Int -> [HPat] -> ([HPat], [HPat])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
m [HPat]
ps in (HPat
cps, [HPat] -> HExpr -> HExpr
hELam [HPat]
ps2 (HExpr -> HExpr) -> HExpr -> HExpr
forall a b. (a -> b) -> a -> b
$ [(HSymbol, HSymbol)] -> HExpr -> HExpr
hESubst ((HPat -> HSymbol -> (HSymbol, HSymbol))
-> [HPat] -> [HSymbol] -> [(HSymbol, HSymbol)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\ (HPVar HSymbol
v) HSymbol
n -> (HSymbol
v, HSymbol
n)) [HPat]
ps1 [HSymbol]
ns) HExpr
e)
| (HPat
cps, HELam [HPat]
ps HExpr
e) <- [(HPat, HExpr)]
alts ]
ns :: [HSymbol]
ns = [ HSymbol
n | HPVar HSymbol
n <- Int -> [HPat] -> [HPat]
forall a. Int -> [a] -> [a]
take Int
m [HPat]
ops ]
hECase HExpr
_ ((HPat
_,HExpr
e):alts :: [(HPat, HExpr)]
alts@((HPat, HExpr)
_:[(HPat, HExpr)]
_)) | ((HPat, HExpr) -> Bool) -> [(HPat, HExpr)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (HExpr -> HExpr -> Bool
alphaEq HExpr
e (HExpr -> Bool)
-> ((HPat, HExpr) -> HExpr) -> (HPat, HExpr) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (HPat, HExpr) -> HExpr
forall a b. (a, b) -> b
snd) [(HPat, HExpr)]
alts = HExpr
e
hECase HExpr
e [(HPat, HExpr)]
alts = HExpr -> [(HPat, HExpr)] -> HExpr
HECase HExpr
e [(HPat, HExpr)]
alts
eqPatExpr :: HPat -> HExpr -> Bool
eqPatExpr :: HPat -> HExpr -> Bool
eqPatExpr (HPVar HSymbol
s) (HEVar HSymbol
s') = HSymbol
s HSymbol -> HSymbol -> Bool
forall a. Eq a => a -> a -> Bool
== HSymbol
s'
eqPatExpr (HPCon HSymbol
s) (HECon HSymbol
s') = HSymbol
s HSymbol -> HSymbol -> Bool
forall a. Eq a => a -> a -> Bool
== HSymbol
s'
eqPatExpr (HPTuple [HPat]
ps) (HETuple [HExpr]
es) = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ((HPat -> HExpr -> Bool) -> [HPat] -> [HExpr] -> [Bool]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith HPat -> HExpr -> Bool
eqPatExpr [HPat]
ps [HExpr]
es)
eqPatExpr (HPApply HPat
pf HPat
pa) (HEApply HExpr
ef HExpr
ea) = HPat -> HExpr -> Bool
eqPatExpr HPat
pf HExpr
ef Bool -> Bool -> Bool
&& HPat -> HExpr -> Bool
eqPatExpr HPat
pa HExpr
ea
eqPatExpr HPat
_ HExpr
_ = Bool
False
alphaEq :: HExpr -> HExpr -> Bool
alphaEq :: HExpr -> HExpr -> Bool
alphaEq HExpr
e1 HExpr
e2 | HExpr
e1 HExpr -> HExpr -> Bool
forall a. Eq a => a -> a -> Bool
== HExpr
e2 = Bool
True
alphaEq (HELam [HPat]
ps1 HExpr
e1) (HELam [HPat]
ps2 HExpr
e2) =
Maybe ()
forall a. Maybe a
Nothing Maybe () -> Maybe () -> Bool
forall a. Eq a => a -> a -> Bool
/= do
[(HSymbol, HSymbol)]
s <- HPat -> HPat -> Maybe [(HSymbol, HSymbol)]
matchPat ([HPat] -> HPat
HPTuple [HPat]
ps1) ([HPat] -> HPat
HPTuple [HPat]
ps2)
if HExpr -> HExpr -> Bool
alphaEq ([(HSymbol, HSymbol)] -> HExpr -> HExpr
hESubst [(HSymbol, HSymbol)]
s HExpr
e1) HExpr
e2
then () -> Maybe ()
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
else Maybe ()
forall a. Maybe a
Nothing
alphaEq (HEApply HExpr
f1 HExpr
a1) (HEApply HExpr
f2 HExpr
a2) = HExpr -> HExpr -> Bool
alphaEq HExpr
f1 HExpr
f2 Bool -> Bool -> Bool
&& HExpr -> HExpr -> Bool
alphaEq HExpr
a1 HExpr
a2
alphaEq (HECon HSymbol
s1) (HECon HSymbol
s2) = HSymbol
s1 HSymbol -> HSymbol -> Bool
forall a. Eq a => a -> a -> Bool
== HSymbol
s2
alphaEq (HEVar HSymbol
s1) (HEVar HSymbol
s2) = HSymbol
s1 HSymbol -> HSymbol -> Bool
forall a. Eq a => a -> a -> Bool
== HSymbol
s2
alphaEq (HETuple [HExpr]
es1) (HETuple [HExpr]
es2) | [HExpr] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [HExpr]
es1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [HExpr] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [HExpr]
es2 = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ((HExpr -> HExpr -> Bool) -> [HExpr] -> [HExpr] -> [Bool]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith HExpr -> HExpr -> Bool
alphaEq [HExpr]
es1 [HExpr]
es2)
alphaEq (HECase HExpr
e1 [(HPat, HExpr)]
alts1) (HECase HExpr
e2 [(HPat, HExpr)]
alts2) =
HExpr -> HExpr -> Bool
alphaEq HExpr
e1 HExpr
e2 Bool -> Bool -> Bool
&& [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ((HExpr -> HExpr -> Bool) -> [HExpr] -> [HExpr] -> [Bool]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith HExpr -> HExpr -> Bool
alphaEq [ [HPat] -> HExpr -> HExpr
HELam [HPat
p] HExpr
e | (HPat
p, HExpr
e) <- [(HPat, HExpr)]
alts1 ] [ [HPat] -> HExpr -> HExpr
HELam [HPat
p] HExpr
e | (HPat
p, HExpr
e) <- [(HPat, HExpr)]
alts2 ])
alphaEq HExpr
_ HExpr
_ = Bool
False
matchPat :: HPat -> HPat -> Maybe [(HSymbol, HSymbol)]
matchPat :: HPat -> HPat -> Maybe [(HSymbol, HSymbol)]
matchPat (HPVar HSymbol
s1) (HPVar HSymbol
s2) = [(HSymbol, HSymbol)] -> Maybe [(HSymbol, HSymbol)]
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return [(HSymbol
s1, HSymbol
s2)]
matchPat (HPCon HSymbol
s1) (HPCon HSymbol
s2) | HSymbol
s1 HSymbol -> HSymbol -> Bool
forall a. Eq a => a -> a -> Bool
== HSymbol
s2 = [(HSymbol, HSymbol)] -> Maybe [(HSymbol, HSymbol)]
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return []
matchPat (HPTuple [HPat]
ps1) (HPTuple [HPat]
ps2) | [HPat] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [HPat]
ps1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [HPat] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [HPat]
ps2 = do
[[(HSymbol, HSymbol)]]
ss <- (HPat -> HPat -> Maybe [(HSymbol, HSymbol)])
-> [HPat] -> [HPat] -> Maybe [[(HSymbol, HSymbol)]]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM HPat -> HPat -> Maybe [(HSymbol, HSymbol)]
matchPat [HPat]
ps1 [HPat]
ps2
[(HSymbol, HSymbol)] -> Maybe [(HSymbol, HSymbol)]
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return ([(HSymbol, HSymbol)] -> Maybe [(HSymbol, HSymbol)])
-> [(HSymbol, HSymbol)] -> Maybe [(HSymbol, HSymbol)]
forall a b. (a -> b) -> a -> b
$ [[(HSymbol, HSymbol)]] -> [(HSymbol, HSymbol)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[(HSymbol, HSymbol)]]
ss
matchPat (HPAt HSymbol
s1 HPat
p1) (HPAt HSymbol
s2 HPat
p2) = do
[(HSymbol, HSymbol)]
s <- HPat -> HPat -> Maybe [(HSymbol, HSymbol)]
matchPat HPat
p1 HPat
p2
[(HSymbol, HSymbol)] -> Maybe [(HSymbol, HSymbol)]
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return ([(HSymbol, HSymbol)] -> Maybe [(HSymbol, HSymbol)])
-> [(HSymbol, HSymbol)] -> Maybe [(HSymbol, HSymbol)]
forall a b. (a -> b) -> a -> b
$ (HSymbol
s1, HSymbol
s2) (HSymbol, HSymbol) -> [(HSymbol, HSymbol)] -> [(HSymbol, HSymbol)]
forall a. a -> [a] -> [a]
: [(HSymbol, HSymbol)]
s
matchPat (HPApply HPat
f1 HPat
a1) (HPApply HPat
f2 HPat
a2) = do
[(HSymbol, HSymbol)]
s1 <- HPat -> HPat -> Maybe [(HSymbol, HSymbol)]
matchPat HPat
f1 HPat
f2
[(HSymbol, HSymbol)]
s2 <- HPat -> HPat -> Maybe [(HSymbol, HSymbol)]
matchPat HPat
a1 HPat
a2
[(HSymbol, HSymbol)] -> Maybe [(HSymbol, HSymbol)]
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return ([(HSymbol, HSymbol)] -> Maybe [(HSymbol, HSymbol)])
-> [(HSymbol, HSymbol)] -> Maybe [(HSymbol, HSymbol)]
forall a b. (a -> b) -> a -> b
$ [(HSymbol, HSymbol)]
s1 [(HSymbol, HSymbol)]
-> [(HSymbol, HSymbol)] -> [(HSymbol, HSymbol)]
forall a. [a] -> [a] -> [a]
++ [(HSymbol, HSymbol)]
s2
matchPat HPat
_ HPat
_ = Maybe [(HSymbol, HSymbol)]
forall a. Maybe a
Nothing
hESubst :: [(HSymbol, HSymbol)] -> HExpr -> HExpr
hESubst :: [(HSymbol, HSymbol)] -> HExpr -> HExpr
hESubst [(HSymbol, HSymbol)]
s (HELam [HPat]
ps HExpr
e) = [HPat] -> HExpr -> HExpr
HELam ((HPat -> HPat) -> [HPat] -> [HPat]
forall a b. (a -> b) -> [a] -> [b]
map ([(HSymbol, HSymbol)] -> HPat -> HPat
hPSubst [(HSymbol, HSymbol)]
s) [HPat]
ps) ([(HSymbol, HSymbol)] -> HExpr -> HExpr
hESubst [(HSymbol, HSymbol)]
s HExpr
e)
hESubst [(HSymbol, HSymbol)]
s (HEApply HExpr
f HExpr
a) = HExpr -> HExpr -> HExpr
HEApply ([(HSymbol, HSymbol)] -> HExpr -> HExpr
hESubst [(HSymbol, HSymbol)]
s HExpr
f) ([(HSymbol, HSymbol)] -> HExpr -> HExpr
hESubst [(HSymbol, HSymbol)]
s HExpr
a)
hESubst [(HSymbol, HSymbol)]
_ e :: HExpr
e@(HECon HSymbol
_) = HExpr
e
hESubst [(HSymbol, HSymbol)]
s (HEVar HSymbol
v) = HSymbol -> HExpr
HEVar (HSymbol -> HExpr) -> HSymbol -> HExpr
forall a b. (a -> b) -> a -> b
$ HSymbol -> ShowS -> Maybe HSymbol -> HSymbol
forall b a. b -> (a -> b) -> Maybe a -> b
maybe HSymbol
v ShowS
forall a. a -> a
id (Maybe HSymbol -> HSymbol) -> Maybe HSymbol -> HSymbol
forall a b. (a -> b) -> a -> b
$ HSymbol -> [(HSymbol, HSymbol)] -> Maybe HSymbol
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup HSymbol
v [(HSymbol, HSymbol)]
s
hESubst [(HSymbol, HSymbol)]
s (HETuple [HExpr]
es) = [HExpr] -> HExpr
HETuple ((HExpr -> HExpr) -> [HExpr] -> [HExpr]
forall a b. (a -> b) -> [a] -> [b]
map ([(HSymbol, HSymbol)] -> HExpr -> HExpr
hESubst [(HSymbol, HSymbol)]
s) [HExpr]
es)
hESubst [(HSymbol, HSymbol)]
s (HECase HExpr
e [(HPat, HExpr)]
alts) = HExpr -> [(HPat, HExpr)] -> HExpr
HECase ([(HSymbol, HSymbol)] -> HExpr -> HExpr
hESubst [(HSymbol, HSymbol)]
s HExpr
e) [([(HSymbol, HSymbol)] -> HPat -> HPat
hPSubst [(HSymbol, HSymbol)]
s HPat
p, [(HSymbol, HSymbol)] -> HExpr -> HExpr
hESubst [(HSymbol, HSymbol)]
s HExpr
b) | (HPat
p, HExpr
b) <- [(HPat, HExpr)]
alts]
hPSubst :: [(HSymbol, HSymbol)] -> HPat -> HPat
hPSubst :: [(HSymbol, HSymbol)] -> HPat -> HPat
hPSubst [(HSymbol, HSymbol)]
s (HPVar HSymbol
v) = HSymbol -> HPat
HPVar (HSymbol -> HPat) -> HSymbol -> HPat
forall a b. (a -> b) -> a -> b
$ HSymbol -> ShowS -> Maybe HSymbol -> HSymbol
forall b a. b -> (a -> b) -> Maybe a -> b
maybe HSymbol
v ShowS
forall a. a -> a
id (Maybe HSymbol -> HSymbol) -> Maybe HSymbol -> HSymbol
forall a b. (a -> b) -> a -> b
$ HSymbol -> [(HSymbol, HSymbol)] -> Maybe HSymbol
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup HSymbol
v [(HSymbol, HSymbol)]
s
hPSubst [(HSymbol, HSymbol)]
_ p :: HPat
p@(HPCon HSymbol
_) = HPat
p
hPSubst [(HSymbol, HSymbol)]
s (HPTuple [HPat]
ps) = [HPat] -> HPat
HPTuple ((HPat -> HPat) -> [HPat] -> [HPat]
forall a b. (a -> b) -> [a] -> [b]
map ([(HSymbol, HSymbol)] -> HPat -> HPat
hPSubst [(HSymbol, HSymbol)]
s) [HPat]
ps)
hPSubst [(HSymbol, HSymbol)]
s (HPAt HSymbol
v HPat
p) = HSymbol -> HPat -> HPat
HPAt (HSymbol -> ShowS -> Maybe HSymbol -> HSymbol
forall b a. b -> (a -> b) -> Maybe a -> b
maybe HSymbol
v ShowS
forall a. a -> a
id (Maybe HSymbol -> HSymbol) -> Maybe HSymbol -> HSymbol
forall a b. (a -> b) -> a -> b
$ HSymbol -> [(HSymbol, HSymbol)] -> Maybe HSymbol
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup HSymbol
v [(HSymbol, HSymbol)]
s) ([(HSymbol, HSymbol)] -> HPat -> HPat
hPSubst [(HSymbol, HSymbol)]
s HPat
p)
hPSubst [(HSymbol, HSymbol)]
s (HPApply HPat
f HPat
a) = HPat -> HPat -> HPat
HPApply ([(HSymbol, HSymbol)] -> HPat -> HPat
hPSubst [(HSymbol, HSymbol)]
s HPat
f) ([(HSymbol, HSymbol)] -> HPat -> HPat
hPSubst [(HSymbol, HSymbol)]
s HPat
a)
termToHClause :: HSymbol -> Term -> HClause
termToHClause :: HSymbol -> Term -> HClause
termToHClause HSymbol
i Term
term =
case Term -> HExpr
termToHExpr Term
term of
HELam [HPat]
ps HExpr
e -> HSymbol -> [HPat] -> HExpr -> HClause
HClause HSymbol
i [HPat]
ps HExpr
e
HExpr
e -> HSymbol -> [HPat] -> HExpr -> HClause
HClause HSymbol
i [] HExpr
e
remUnusedVars :: HExpr -> HExpr
remUnusedVars :: HExpr -> HExpr
remUnusedVars HExpr
expr = (HExpr, [HSymbol]) -> HExpr
forall a b. (a, b) -> a
fst ((HExpr, [HSymbol]) -> HExpr) -> (HExpr, [HSymbol]) -> HExpr
forall a b. (a -> b) -> a -> b
$ HExpr -> (HExpr, [HSymbol])
remE HExpr
expr
where remE :: HExpr -> (HExpr, [HSymbol])
remE (HELam [HPat]
ps HExpr
e) =
let (HExpr
e', [HSymbol]
vs) = HExpr -> (HExpr, [HSymbol])
remE HExpr
e
in ([HPat] -> HExpr -> HExpr
HELam ((HPat -> HPat) -> [HPat] -> [HPat]
forall a b. (a -> b) -> [a] -> [b]
map ([HSymbol] -> HPat -> HPat
forall {t :: * -> *}. Foldable t => t HSymbol -> HPat -> HPat
remP [HSymbol]
vs) [HPat]
ps) HExpr
e', [HSymbol]
vs)
remE (HEApply HExpr
f HExpr
a) =
let (HExpr
f', [HSymbol]
fs) = HExpr -> (HExpr, [HSymbol])
remE HExpr
f
(HExpr
a', [HSymbol]
as) = HExpr -> (HExpr, [HSymbol])
remE HExpr
a
in (HExpr -> HExpr -> HExpr
HEApply HExpr
f' HExpr
a', [HSymbol]
fs [HSymbol] -> [HSymbol] -> [HSymbol]
forall a. [a] -> [a] -> [a]
++ [HSymbol]
as)
remE (HETuple [HExpr]
es) =
let ([HExpr]
es', [[HSymbol]]
sss) = [(HExpr, [HSymbol])] -> ([HExpr], [[HSymbol]])
forall a b. [(a, b)] -> ([a], [b])
unzip ((HExpr -> (HExpr, [HSymbol])) -> [HExpr] -> [(HExpr, [HSymbol])]
forall a b. (a -> b) -> [a] -> [b]
map HExpr -> (HExpr, [HSymbol])
remE [HExpr]
es)
in ([HExpr] -> HExpr
HETuple [HExpr]
es', [[HSymbol]] -> [HSymbol]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[HSymbol]]
sss)
remE (HECase HExpr
e [(HPat, HExpr)]
alts) =
let (HExpr
e', [HSymbol]
es) = HExpr -> (HExpr, [HSymbol])
remE HExpr
e
([(HPat, HExpr)]
alts', [[HSymbol]]
sss) = [((HPat, HExpr), [HSymbol])] -> ([(HPat, HExpr)], [[HSymbol]])
forall a b. [(a, b)] -> ([a], [b])
unzip [ let (HExpr
ee', [HSymbol]
ss) = HExpr -> (HExpr, [HSymbol])
remE HExpr
ee in (([HSymbol] -> HPat -> HPat
forall {t :: * -> *}. Foldable t => t HSymbol -> HPat -> HPat
remP [HSymbol]
ss HPat
p, HExpr
ee'), [HSymbol]
ss) | (HPat
p, HExpr
ee) <- [(HPat, HExpr)]
alts ]
in case [(HPat, HExpr)]
alts' of
[(HPVar HSymbol
"_", HExpr
b)] -> (HExpr
b, [[HSymbol]] -> [HSymbol]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[HSymbol]]
sss)
[(HPat, HExpr)]
_ -> (HExpr -> [(HPat, HExpr)] -> HExpr
hECase HExpr
e' [(HPat, HExpr)]
alts', [HSymbol]
es [HSymbol] -> [HSymbol] -> [HSymbol]
forall a. [a] -> [a] -> [a]
++ [[HSymbol]] -> [HSymbol]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[HSymbol]]
sss)
remE e :: HExpr
e@(HECon HSymbol
_) = (HExpr
e, [])
remE e :: HExpr
e@(HEVar HSymbol
v) = (HExpr
e, [HSymbol
v])
remP :: t HSymbol -> HPat -> HPat
remP t HSymbol
vs p :: HPat
p@(HPVar HSymbol
v) = if HSymbol
v HSymbol -> t HSymbol -> Bool
forall a. Eq a => a -> t a -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t HSymbol
vs then HPat
p else HSymbol -> HPat
HPVar HSymbol
"_"
remP t HSymbol
_vs p :: HPat
p@(HPCon HSymbol
_) = HPat
p
remP t HSymbol
vs (HPTuple [HPat]
ps) = [HPat] -> HPat
hPTuple ((HPat -> HPat) -> [HPat] -> [HPat]
forall a b. (a -> b) -> [a] -> [b]
map (t HSymbol -> HPat -> HPat
remP t HSymbol
vs) [HPat]
ps)
remP t HSymbol
vs (HPAt HSymbol
v HPat
p) = if HSymbol
v HSymbol -> t HSymbol -> Bool
forall a. Eq a => a -> t a -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t HSymbol
vs then HSymbol -> HPat -> HPat
HPAt HSymbol
v (t HSymbol -> HPat -> HPat
remP t HSymbol
vs HPat
p) else t HSymbol -> HPat -> HPat
remP t HSymbol
vs HPat
p
remP t HSymbol
vs (HPApply HPat
f HPat
a) = HPat -> HPat -> HPat
HPApply (t HSymbol -> HPat -> HPat
remP t HSymbol
vs HPat
f) (t HSymbol -> HPat -> HPat
remP t HSymbol
vs HPat
a)
hPTuple :: [HPat] -> HPat
hPTuple [HPat]
ps | (HPat -> Bool) -> [HPat] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (HPat -> HPat -> Bool
forall a. Eq a => a -> a -> Bool
== HSymbol -> HPat
HPVar HSymbol
"_") [HPat]
ps = HSymbol -> HPat
HPVar HSymbol
"_"
hPTuple [HPat]
ps = [HPat] -> HPat
HPTuple [HPat]
ps
getBinderVars :: HClause -> [HSymbol]
getBinderVars :: HClause -> [HSymbol]
getBinderVars (HClause HSymbol
_ [HPat]
pats HExpr
expr) = (HPat -> [HSymbol]) -> [HPat] -> [HSymbol]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap HPat -> [HSymbol]
getBinderVarsHP [HPat]
pats [HSymbol] -> [HSymbol] -> [HSymbol]
forall a. [a] -> [a] -> [a]
++ HExpr -> [HSymbol]
getBinderVarsHE HExpr
expr
getBinderVarsHE :: HExpr -> [HSymbol]
getBinderVarsHE :: HExpr -> [HSymbol]
getBinderVarsHE HExpr
expr = HExpr -> [HSymbol]
gbExp HExpr
expr
where gbExp :: HExpr -> [HSymbol]
gbExp (HELam [HPat]
ps HExpr
e) = (HPat -> [HSymbol]) -> [HPat] -> [HSymbol]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap HPat -> [HSymbol]
getBinderVarsHP [HPat]
ps [HSymbol] -> [HSymbol] -> [HSymbol]
forall a. [a] -> [a] -> [a]
++ HExpr -> [HSymbol]
gbExp HExpr
e
gbExp (HEApply HExpr
f HExpr
a) = HExpr -> [HSymbol]
gbExp HExpr
f [HSymbol] -> [HSymbol] -> [HSymbol]
forall a. [a] -> [a] -> [a]
++ HExpr -> [HSymbol]
gbExp HExpr
a
gbExp (HETuple [HExpr]
es) = (HExpr -> [HSymbol]) -> [HExpr] -> [HSymbol]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap HExpr -> [HSymbol]
gbExp [HExpr]
es
gbExp (HECase HExpr
se [(HPat, HExpr)]
alts) = HExpr -> [HSymbol]
gbExp HExpr
se [HSymbol] -> [HSymbol] -> [HSymbol]
forall a. [a] -> [a] -> [a]
++ ((HPat, HExpr) -> [HSymbol]) -> [(HPat, HExpr)] -> [HSymbol]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\ (HPat
p, HExpr
e) -> HPat -> [HSymbol]
getBinderVarsHP HPat
p [HSymbol] -> [HSymbol] -> [HSymbol]
forall a. [a] -> [a] -> [a]
++ HExpr -> [HSymbol]
gbExp HExpr
e) [(HPat, HExpr)]
alts
gbExp HExpr
_ = []
getBinderVarsHP :: HPat -> [HSymbol]
getBinderVarsHP :: HPat -> [HSymbol]
getBinderVarsHP HPat
pat = HPat -> [HSymbol]
gbPat HPat
pat
where gbPat :: HPat -> [HSymbol]
gbPat (HPVar HSymbol
s) = [HSymbol
s]
gbPat (HPCon HSymbol
_) = []
gbPat (HPTuple [HPat]
ps) = (HPat -> [HSymbol]) -> [HPat] -> [HSymbol]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap HPat -> [HSymbol]
gbPat [HPat]
ps
gbPat (HPAt HSymbol
s HPat
p) = HSymbol
s HSymbol -> [HSymbol] -> [HSymbol]
forall a. a -> [a] -> [a]
: HPat -> [HSymbol]
gbPat HPat
p
gbPat (HPApply HPat
f HPat
a) = HPat -> [HSymbol]
gbPat HPat
f [HSymbol] -> [HSymbol] -> [HSymbol]
forall a. [a] -> [a] -> [a]
++ HPat -> [HSymbol]
gbPat HPat
a
getAllVars :: HExpr -> [HSymbol]
getAllVars :: HExpr -> [HSymbol]
getAllVars HExpr
expr = HExpr -> [HSymbol]
gaExp HExpr
expr
where gaExp :: HExpr -> [HSymbol]
gaExp (HELam [HPat]
_ps HExpr
e) = HExpr -> [HSymbol]
gaExp HExpr
e
gaExp (HEApply HExpr
f HExpr
a) = HExpr -> [HSymbol]
gaExp HExpr
f [HSymbol] -> [HSymbol] -> [HSymbol]
forall a. Eq a => [a] -> [a] -> [a]
`union` HExpr -> [HSymbol]
gaExp HExpr
a
gaExp (HETuple [HExpr]
es) = ([HSymbol] -> [HSymbol] -> [HSymbol])
-> [HSymbol] -> [[HSymbol]] -> [HSymbol]
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr [HSymbol] -> [HSymbol] -> [HSymbol]
forall a. Eq a => [a] -> [a] -> [a]
union [] ((HExpr -> [HSymbol]) -> [HExpr] -> [[HSymbol]]
forall a b. (a -> b) -> [a] -> [b]
map HExpr -> [HSymbol]
gaExp [HExpr]
es)
gaExp (HECase HExpr
se [(HPat, HExpr)]
alts) = ([HSymbol] -> [HSymbol] -> [HSymbol])
-> [HSymbol] -> [[HSymbol]] -> [HSymbol]
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr [HSymbol] -> [HSymbol] -> [HSymbol]
forall a. Eq a => [a] -> [a] -> [a]
union (HExpr -> [HSymbol]
gaExp HExpr
se) (((HPat, HExpr) -> [HSymbol]) -> [(HPat, HExpr)] -> [[HSymbol]]
forall a b. (a -> b) -> [a] -> [b]
map (\ (HPat
_p, HExpr
e) -> HExpr -> [HSymbol]
gaExp HExpr
e) [(HPat, HExpr)]
alts)
gaExp (HEVar HSymbol
s) = [HSymbol
s]
gaExp HExpr
_ = []
etaReduce :: HExpr -> HExpr
etaReduce :: HExpr -> HExpr
etaReduce HExpr
expr = (HExpr, [HSymbol]) -> HExpr
forall a b. (a, b) -> a
fst ((HExpr, [HSymbol]) -> HExpr) -> (HExpr, [HSymbol]) -> HExpr
forall a b. (a -> b) -> a -> b
$ HExpr -> (HExpr, [HSymbol])
eta HExpr
expr
where eta :: HExpr -> (HExpr, [HSymbol])
eta (HELam [HPVar HSymbol
v] (HEApply HExpr
f (HEVar HSymbol
v'))) | HSymbol
v HSymbol -> HSymbol -> Bool
forall a. Eq a => a -> a -> Bool
== HSymbol
v' Bool -> Bool -> Bool
&& HSymbol
v HSymbol -> [HSymbol] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [HSymbol]
vs = (HExpr
f', [HSymbol]
vs)
where (HExpr
f', [HSymbol]
vs) = HExpr -> (HExpr, [HSymbol])
eta HExpr
f
eta (HELam [HPat]
ps HExpr
e) = ([HPat] -> HExpr -> HExpr
HELam [HPat]
ps HExpr
e', [HSymbol]
vs) where (HExpr
e', [HSymbol]
vs) = HExpr -> (HExpr, [HSymbol])
eta HExpr
e
eta (HEApply HExpr
f HExpr
a) = (HExpr -> HExpr -> HExpr
HEApply HExpr
f' HExpr
a', [HSymbol]
fvs[HSymbol] -> [HSymbol] -> [HSymbol]
forall a. [a] -> [a] -> [a]
++[HSymbol]
avs) where (HExpr
f', [HSymbol]
fvs) = HExpr -> (HExpr, [HSymbol])
eta HExpr
f; (HExpr
a', [HSymbol]
avs) = HExpr -> (HExpr, [HSymbol])
eta HExpr
a
eta e :: HExpr
e@(HECon HSymbol
_) = (HExpr
e, [])
eta e :: HExpr
e@(HEVar HSymbol
s) = (HExpr
e, [HSymbol
s])
eta (HETuple [HExpr]
es) = ([HExpr] -> HExpr
HETuple [HExpr]
es', [[HSymbol]] -> [HSymbol]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[HSymbol]]
vss) where ([HExpr]
es', [[HSymbol]]
vss) = [(HExpr, [HSymbol])] -> ([HExpr], [[HSymbol]])
forall a b. [(a, b)] -> ([a], [b])
unzip ([(HExpr, [HSymbol])] -> ([HExpr], [[HSymbol]]))
-> [(HExpr, [HSymbol])] -> ([HExpr], [[HSymbol]])
forall a b. (a -> b) -> a -> b
$ (HExpr -> (HExpr, [HSymbol])) -> [HExpr] -> [(HExpr, [HSymbol])]
forall a b. (a -> b) -> [a] -> [b]
map HExpr -> (HExpr, [HSymbol])
eta [HExpr]
es
eta (HECase HExpr
e [(HPat, HExpr)]
alts) = (HExpr -> [(HPat, HExpr)] -> HExpr
HECase HExpr
e' [(HPat, HExpr)]
alts', [HSymbol]
vs [HSymbol] -> [HSymbol] -> [HSymbol]
forall a. [a] -> [a] -> [a]
++ [[HSymbol]] -> [HSymbol]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[HSymbol]]
vss)
where (HExpr
e', [HSymbol]
vs) = HExpr -> (HExpr, [HSymbol])
eta HExpr
e
([(HPat, HExpr)]
alts', [[HSymbol]]
vss) = [((HPat, HExpr), [HSymbol])] -> ([(HPat, HExpr)], [[HSymbol]])
forall a b. [(a, b)] -> ([a], [b])
unzip ([((HPat, HExpr), [HSymbol])] -> ([(HPat, HExpr)], [[HSymbol]]))
-> [((HPat, HExpr), [HSymbol])] -> ([(HPat, HExpr)], [[HSymbol]])
forall a b. (a -> b) -> a -> b
$ [ let (HExpr
a', [HSymbol]
ss) = HExpr -> (HExpr, [HSymbol])
eta HExpr
a in ((HPat
p, HExpr
a'), [HSymbol]
ss) | (HPat
p, HExpr
a) <- [(HPat, HExpr)]
alts ]