module A.Eta ( η ) where

import           A
import           Control.Monad ((<=<))
import           R.M

-- domains
doms :: T a -> [T a]
doms :: forall a. T a -> [T a]
doms (Arrow T a
t T a
t') = T a
tT a -> [T a] -> [T a]
forall a. a -> [a] -> [a]
:T a -> [T a]
forall a. T a -> [T a]
doms T a
t'
doms T a
_            = []

-- count lambdas
cLam :: E a -> Int
cLam :: forall a. E a -> Int
cLam (Lam a
_ Nm a
_ E a
e) = Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ E a -> Int
forall a. E a -> Int
cLam E a
e; cLam E a
_ = Int
0

thread :: [b -> b] -> b -> b
thread = ((b -> b) -> (b -> b) -> b -> b) -> (b -> b) -> [b -> b] -> b -> b
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (b -> b) -> (b -> b) -> b -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
(.) b -> b
forall a. a -> a
id

unseam :: [T ()] -> RM (E (T ()) -> E (T ()), E (T ()) -> E (T ()))
unseam :: [T ()] -> RM (E (T ()) -> E (T ()), E (T ()) -> E (T ()))
unseam [T ()]
ts = do
    lApps <- (T () -> RM (E (T ()) -> E (T ()), E (T ()) -> E (T ())))
-> [T ()]
-> StateT
     Int Identity [(E (T ()) -> E (T ()), E (T ()) -> E (T ()))]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse (\T ()
t -> do { n <- T () -> RM (Nm (T ()))
forall a. a -> RM (Nm a)
nextN T ()
t ; pure (\E (T ())
e' -> let t' :: T ()
t' = E (T ()) -> T ()
forall a. E a -> a
eAnn E (T ())
e' in T () -> Nm (T ()) -> E (T ()) -> E (T ())
forall a. a -> Nm a -> E a -> E a
Lam (T ()
t T () -> T () -> T ()
forall {a}. T a -> T a -> T a
~> T ()
t') Nm (T ())
n E (T ())
e', \E (T ())
e' -> let Arrow T ()
_ T ()
cod = E (T ()) -> T ()
forall a. E a -> a
eAnn E (T ())
e' in T () -> E (T ()) -> E (T ()) -> E (T ())
forall a. a -> E a -> E a -> E a
EApp T ()
cod E (T ())
e' (T () -> Nm (T ()) -> E (T ())
forall a. a -> Nm a -> E a
Var T ()
t Nm (T ())
n)) }) [T ()]
ts
    let (ls, eApps) = unzip lApps
    pure (thread ls, thread (reverse eApps))

mkLam :: [T ()] -> E (T ()) -> RM (E (T ()))
mkLam :: [T ()] -> E (T ()) -> RM (E (T ()))
mkLam [T ()]
ts E (T ())
e = do
    (lam, app) <- [T ()] -> RM (E (T ()) -> E (T ()), E (T ()) -> E (T ()))
unseam [T ()]
ts
    pure $ lam (app e)

η :: E (T ()) -> RM (E (T ()))
η :: E (T ()) -> RM (E (T ()))
η = E (T ()) -> RM (E (T ()))
ηM (E (T ()) -> RM (E (T ())))
-> (E (T ()) -> RM (E (T ()))) -> E (T ()) -> RM (E (T ()))
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< E (T ()) -> RM (E (T ()))
ηAt

tuck :: E a -> (E a -> E a, E a)
tuck :: forall a. E a -> (E a -> E a, E a)
tuck (Lam a
l Nm a
n E a
e) = let (E a -> E a
f, E a
e') = E a -> (E a -> E a, E a)
forall a. E a -> (E a -> E a, E a)
tuck E a
e in (a -> Nm a -> E a -> E a
forall a. a -> Nm a -> E a -> E a
Lam a
l Nm a
n(E a -> E a) -> (E a -> E a) -> E a -> E a
forall b c a. (b -> c) -> (a -> b) -> a -> c
.E a -> E a
f, E a
e')
tuck E a
e           = (E a -> E a
forall a. a -> a
id, E a
e)

ηAt :: E (T ()) -> RM (E (T ()))
ηAt :: E (T ()) -> RM (E (T ()))
ηAt (EApp T ()
t0 (EApp T ()
t1 ho :: E (T ())
ho@(Builtin T ()
_ Builtin
Gen) E (T ())
seed) E (T ())
op) = T () -> E (T ()) -> E (T ()) -> E (T ())
forall a. a -> E a -> E a -> E a
EApp T ()
t0 (E (T ()) -> E (T ()) -> E (T ()))
-> (E (T ()) -> E (T ())) -> E (T ()) -> E (T ()) -> E (T ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> T () -> E (T ()) -> E (T ()) -> E (T ())
forall a. a -> E a -> E a -> E a
EApp T ()
t1 E (T ())
ho (E (T ()) -> E (T ()) -> E (T ()))
-> RM (E (T ())) -> StateT Int Identity (E (T ()) -> E (T ()))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E (T ()) -> RM (E (T ()))
ηAt E (T ())
seed StateT Int Identity (E (T ()) -> E (T ()))
-> RM (E (T ())) -> RM (E (T ()))
forall a b.
StateT Int Identity (a -> b)
-> StateT Int Identity a -> StateT Int Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> E (T ()) -> RM (E (T ()))
η E (T ())
op
ηAt (EApp T ()
t ho :: E (T ())
ho@(Builtin T ()
_ Scan{}) E (T ())
op)              = T () -> E (T ()) -> E (T ()) -> E (T ())
forall a. a -> E a -> E a -> E a
EApp T ()
t E (T ())
ho (E (T ()) -> E (T ())) -> RM (E (T ())) -> RM (E (T ()))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E (T ()) -> RM (E (T ()))
η E (T ())
op
ηAt (EApp T ()
t ho :: E (T ())
ho@(Builtin T ()
_ ScanS{}) E (T ())
op)             = T () -> E (T ()) -> E (T ()) -> E (T ())
forall a. a -> E a -> E a -> E a
EApp T ()
t E (T ())
ho (E (T ()) -> E (T ())) -> RM (E (T ())) -> RM (E (T ()))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E (T ()) -> RM (E (T ()))
η E (T ())
op
ηAt (EApp T ()
t ho :: E (T ())
ho@(Builtin T ()
_ Zip{}) E (T ())
op)               = T () -> E (T ()) -> E (T ()) -> E (T ())
forall a. a -> E a -> E a -> E a
EApp T ()
t E (T ())
ho (E (T ()) -> E (T ())) -> RM (E (T ())) -> RM (E (T ()))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E (T ()) -> RM (E (T ()))
η E (T ())
op
ηAt (EApp T ()
t ho :: E (T ())
ho@(Builtin T ()
_ Succ{}) E (T ())
op)              = T () -> E (T ()) -> E (T ()) -> E (T ())
forall a. a -> E a -> E a -> E a
EApp T ()
t E (T ())
ho (E (T ()) -> E (T ())) -> RM (E (T ())) -> RM (E (T ()))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E (T ()) -> RM (E (T ()))
η E (T ())
op
ηAt (EApp T ()
t ho :: E (T ())
ho@(Builtin T ()
_ Builtin
FoldS) E (T ())
op)               = T () -> E (T ()) -> E (T ()) -> E (T ())
forall a. a -> E a -> E a -> E a
EApp T ()
t E (T ())
ho (E (T ()) -> E (T ())) -> RM (E (T ())) -> RM (E (T ()))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E (T ()) -> RM (E (T ()))
η E (T ())
op
ηAt (EApp T ()
t ho :: E (T ())
ho@(Builtin T ()
_ Builtin
Fold) E (T ())
op)                = T () -> E (T ()) -> E (T ()) -> E (T ())
forall a. a -> E a -> E a -> E a
EApp T ()
t E (T ())
ho (E (T ()) -> E (T ())) -> RM (E (T ())) -> RM (E (T ()))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E (T ()) -> RM (E (T ()))
η E (T ())
op
ηAt (EApp T ()
t ho :: E (T ())
ho@(Builtin T ()
_ Builtin
FoldA) E (T ())
op)               = T () -> E (T ()) -> E (T ()) -> E (T ())
forall a. a -> E a -> E a -> E a
EApp T ()
t E (T ())
ho (E (T ()) -> E (T ())) -> RM (E (T ())) -> RM (E (T ()))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E (T ()) -> RM (E (T ()))
η E (T ())
op
ηAt (EApp T ()
t ho :: E (T ())
ho@(Builtin T ()
_ Builtin
Foldl) E (T ())
op)               = T () -> E (T ()) -> E (T ()) -> E (T ())
forall a. a -> E a -> E a -> E a
EApp T ()
t E (T ())
ho (E (T ()) -> E (T ())) -> RM (E (T ())) -> RM (E (T ()))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E (T ()) -> RM (E (T ()))
η E (T ())
op
ηAt (EApp T ()
t ho :: E (T ())
ho@(Builtin T ()
_ Filt{}) E (T ())
f)               = T () -> E (T ()) -> E (T ()) -> E (T ())
forall a. a -> E a -> E a -> E a
EApp T ()
t E (T ())
ho (E (T ()) -> E (T ())) -> RM (E (T ())) -> RM (E (T ()))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E (T ()) -> RM (E (T ()))
η E (T ())
f
ηAt (EApp T ()
t ho :: E (T ())
ho@(Builtin T ()
_ Ices{}) E (T ())
p)               = T () -> E (T ()) -> E (T ()) -> E (T ())
forall a. a -> E a -> E a -> E a
EApp T ()
t E (T ())
ho (E (T ()) -> E (T ())) -> RM (E (T ())) -> RM (E (T ()))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E (T ()) -> RM (E (T ()))
η E (T ())
p
ηAt (EApp T ()
t ho :: E (T ())
ho@(Builtin T ()
_ Map{}) E (T ())
op)               = T () -> E (T ()) -> E (T ()) -> E (T ())
forall a. a -> E a -> E a -> E a
EApp T ()
t E (T ())
ho (E (T ()) -> E (T ())) -> RM (E (T ())) -> RM (E (T ()))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E (T ()) -> RM (E (T ()))
η E (T ())
op
ηAt (EApp T ()
t ho :: E (T ())
ho@(Builtin T ()
_ Rank{}) E (T ())
op)              = T () -> E (T ()) -> E (T ()) -> E (T ())
forall a. a -> E a -> E a -> E a
EApp T ()
t E (T ())
ho (E (T ()) -> E (T ())) -> RM (E (T ())) -> RM (E (T ()))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E (T ()) -> RM (E (T ()))
η E (T ())
op
ηAt (EApp T ()
t ho :: E (T ())
ho@(Builtin T ()
_ DI{}) E (T ())
op)                = T () -> E (T ()) -> E (T ()) -> E (T ())
forall a. a -> E a -> E a -> E a
EApp T ()
t E (T ())
ho (E (T ()) -> E (T ())) -> RM (E (T ())) -> RM (E (T ()))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E (T ()) -> RM (E (T ()))
η E (T ())
op
ηAt (EApp T ()
t ho :: E (T ())
ho@(Builtin T ()
_ Conv{}) E (T ())
op)              = T () -> E (T ()) -> E (T ()) -> E (T ())
forall a. a -> E a -> E a -> E a
EApp T ()
t E (T ())
ho (E (T ()) -> E (T ())) -> RM (E (T ())) -> RM (E (T ()))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E (T ()) -> RM (E (T ()))
η E (T ())
op
ηAt (EApp T ()
t ho :: E (T ())
ho@(Builtin T ()
_ Builtin
Outer) E (T ())
op)               = T () -> E (T ()) -> E (T ()) -> E (T ())
forall a. a -> E a -> E a -> E a
EApp T ()
t E (T ())
ho (E (T ()) -> E (T ())) -> RM (E (T ())) -> RM (E (T ()))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E (T ()) -> RM (E (T ()))
η E (T ())
op
ηAt (EApp T ()
t E (T ())
e0 E (T ())
e1)                                 = T () -> E (T ()) -> E (T ()) -> E (T ())
forall a. a -> E a -> E a -> E a
EApp T ()
t (E (T ()) -> E (T ()) -> E (T ()))
-> RM (E (T ())) -> StateT Int Identity (E (T ()) -> E (T ()))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E (T ()) -> RM (E (T ()))
ηAt E (T ())
e0 StateT Int Identity (E (T ()) -> E (T ()))
-> RM (E (T ())) -> RM (E (T ()))
forall a b.
StateT Int Identity (a -> b)
-> StateT Int Identity a -> StateT Int Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> E (T ()) -> RM (E (T ()))
ηAt E (T ())
e1
ηAt (Lam T ()
l Nm (T ())
n E (T ())
e)                                    = T () -> Nm (T ()) -> E (T ()) -> E (T ())
forall a. a -> Nm a -> E a -> E a
Lam T ()
l Nm (T ())
n (E (T ()) -> E (T ())) -> RM (E (T ())) -> RM (E (T ()))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E (T ()) -> RM (E (T ()))
ηAt E (T ())
e
ηAt (Cond T ()
l E (T ())
p E (T ())
e E (T ())
e')                                = T () -> E (T ()) -> E (T ()) -> E (T ()) -> E (T ())
forall a. a -> E a -> E a -> E a -> E a
Cond T ()
l (E (T ()) -> E (T ()) -> E (T ()) -> E (T ()))
-> RM (E (T ()))
-> StateT Int Identity (E (T ()) -> E (T ()) -> E (T ()))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E (T ()) -> RM (E (T ()))
ηAt E (T ())
p StateT Int Identity (E (T ()) -> E (T ()) -> E (T ()))
-> RM (E (T ())) -> StateT Int Identity (E (T ()) -> E (T ()))
forall a b.
StateT Int Identity (a -> b)
-> StateT Int Identity a -> StateT Int Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> E (T ()) -> RM (E (T ()))
ηAt E (T ())
e StateT Int Identity (E (T ()) -> E (T ()))
-> RM (E (T ())) -> RM (E (T ()))
forall a b.
StateT Int Identity (a -> b)
-> StateT Int Identity a -> StateT Int Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> E (T ()) -> RM (E (T ()))
ηAt E (T ())
e'
ηAt (LLet T ()
l (Nm (T ())
n, E (T ())
e') E (T ())
e)                             = do { e'𝜂 <- E (T ()) -> RM (E (T ()))
ηAt E (T ())
e'; e𝜂 <- ηAt e; pure $ LLet l (n, e'𝜂) e𝜂 }
ηAt (Id T ()
l Idiom
idm)                                     = T () -> Idiom -> E (T ())
forall a. a -> Idiom -> E a
Id T ()
l (Idiom -> E (T ())) -> StateT Int Identity Idiom -> RM (E (T ()))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Idiom -> StateT Int Identity Idiom
ηIdm Idiom
idm
ηAt (ALit T ()
l [E (T ())]
es)                                    = T () -> [E (T ())] -> E (T ())
forall a. a -> [E a] -> E a
ALit T ()
l ([E (T ())] -> E (T ()))
-> StateT Int Identity [E (T ())] -> RM (E (T ()))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (E (T ()) -> RM (E (T ())))
-> [E (T ())] -> StateT Int Identity [E (T ())]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse E (T ()) -> RM (E (T ()))
ηAt [E (T ())]
es
ηAt (Tup T ()
l [E (T ())]
es)                                     = T () -> [E (T ())] -> E (T ())
forall a. a -> [E a] -> E a
Tup T ()
l ([E (T ())] -> E (T ()))
-> StateT Int Identity [E (T ())] -> RM (E (T ()))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (E (T ()) -> RM (E (T ())))
-> [E (T ())] -> StateT Int Identity [E (T ())]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse E (T ()) -> RM (E (T ()))
ηAt [E (T ())]
es
ηAt E (T ())
e                                              = E (T ()) -> RM (E (T ()))
forall a. a -> StateT Int Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure E (T ())
e

ηIdm :: Idiom -> StateT Int Identity Idiom
ηIdm (FoldSOfZip E (T ())
seed E (T ())
op [E (T ())]
es) = E (T ()) -> E (T ()) -> [E (T ())] -> Idiom
FoldSOfZip (E (T ()) -> E (T ()) -> [E (T ())] -> Idiom)
-> RM (E (T ()))
-> StateT Int Identity (E (T ()) -> [E (T ())] -> Idiom)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E (T ()) -> RM (E (T ()))
ηAt E (T ())
seed StateT Int Identity (E (T ()) -> [E (T ())] -> Idiom)
-> RM (E (T ())) -> StateT Int Identity ([E (T ())] -> Idiom)
forall a b.
StateT Int Identity (a -> b)
-> StateT Int Identity a -> StateT Int Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> E (T ()) -> RM (E (T ()))
ηAt E (T ())
op StateT Int Identity ([E (T ())] -> Idiom)
-> StateT Int Identity [E (T ())] -> StateT Int Identity Idiom
forall a b.
StateT Int Identity (a -> b)
-> StateT Int Identity a -> StateT Int Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (E (T ()) -> RM (E (T ())))
-> [E (T ())] -> StateT Int Identity [E (T ())]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse E (T ()) -> RM (E (T ()))
ηAt [E (T ())]
es
ηIdm (FoldOfZip E (T ())
zop E (T ())
op [E (T ())]
es)   = E (T ()) -> E (T ()) -> [E (T ())] -> Idiom
FoldOfZip (E (T ()) -> E (T ()) -> [E (T ())] -> Idiom)
-> RM (E (T ()))
-> StateT Int Identity (E (T ()) -> [E (T ())] -> Idiom)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E (T ()) -> RM (E (T ()))
ηAt E (T ())
zop StateT Int Identity (E (T ()) -> [E (T ())] -> Idiom)
-> RM (E (T ())) -> StateT Int Identity ([E (T ())] -> Idiom)
forall a b.
StateT Int Identity (a -> b)
-> StateT Int Identity a -> StateT Int Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> E (T ()) -> RM (E (T ()))
ηAt E (T ())
op StateT Int Identity ([E (T ())] -> Idiom)
-> StateT Int Identity [E (T ())] -> StateT Int Identity Idiom
forall a b.
StateT Int Identity (a -> b)
-> StateT Int Identity a -> StateT Int Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (E (T ()) -> RM (E (T ())))
-> [E (T ())] -> StateT Int Identity [E (T ())]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse E (T ()) -> RM (E (T ()))
ηAt [E (T ())]
es
ηIdm (FoldGen E (T ())
seed E (T ())
g E (T ())
f E (T ())
n)    = E (T ()) -> E (T ()) -> E (T ()) -> E (T ()) -> Idiom
FoldGen (E (T ()) -> E (T ()) -> E (T ()) -> E (T ()) -> Idiom)
-> RM (E (T ()))
-> StateT Int Identity (E (T ()) -> E (T ()) -> E (T ()) -> Idiom)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E (T ()) -> RM (E (T ()))
ηAt E (T ())
seed StateT Int Identity (E (T ()) -> E (T ()) -> E (T ()) -> Idiom)
-> RM (E (T ()))
-> StateT Int Identity (E (T ()) -> E (T ()) -> Idiom)
forall a b.
StateT Int Identity (a -> b)
-> StateT Int Identity a -> StateT Int Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> E (T ()) -> RM (E (T ()))
ηM E (T ())
g StateT Int Identity (E (T ()) -> E (T ()) -> Idiom)
-> RM (E (T ())) -> StateT Int Identity (E (T ()) -> Idiom)
forall a b.
StateT Int Identity (a -> b)
-> StateT Int Identity a -> StateT Int Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> E (T ()) -> RM (E (T ()))
ηM E (T ())
f StateT Int Identity (E (T ()) -> Idiom)
-> RM (E (T ())) -> StateT Int Identity Idiom
forall a b.
StateT Int Identity (a -> b)
-> StateT Int Identity a -> StateT Int Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> E (T ()) -> RM (E (T ()))
ηAt E (T ())
n
ηIdm (AShLit [Int]
ds [E (T ())]
es)          = [Int] -> [E (T ())] -> Idiom
AShLit [Int]
ds ([E (T ())] -> Idiom)
-> StateT Int Identity [E (T ())] -> StateT Int Identity Idiom
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (E (T ()) -> RM (E (T ())))
-> [E (T ())] -> StateT Int Identity [E (T ())]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse E (T ()) -> RM (E (T ()))
ηAt [E (T ())]
es

-- outermost only
ηM :: E (T ()) -> RM (E (T ()))
ηM :: E (T ()) -> RM (E (T ()))
ηM e :: E (T ())
e@FLit{}                = E (T ()) -> RM (E (T ()))
forall a. a -> StateT Int Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure E (T ())
e
ηM e :: E (T ())
e@ILit{}                = E (T ()) -> RM (E (T ()))
forall a. a -> StateT Int Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure E (T ())
e
ηM e :: E (T ())
e@ALit{}                = E (T ()) -> RM (E (T ()))
forall a. a -> StateT Int Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure E (T ())
e
ηM e :: E (T ())
e@(Id T ()
_ AShLit{})       = E (T ()) -> RM (E (T ()))
forall a. a -> StateT Int Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure E (T ())
e
ηM e :: E (T ())
e@(Id T ()
_ FoldGen{})      = E (T ()) -> RM (E (T ()))
forall a. a -> StateT Int Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure E (T ())
e
ηM e :: E (T ())
e@(Id T ()
_ FoldOfZip{})    = E (T ()) -> RM (E (T ()))
forall a. a -> StateT Int Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure E (T ())
e
ηM e :: E (T ())
e@(Id T ()
_ FoldSOfZip{})   = E (T ()) -> RM (E (T ()))
forall a. a -> StateT Int Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure E (T ())
e
ηM e :: E (T ())
e@Cond{}                = E (T ()) -> RM (E (T ()))
forall a. a -> StateT Int Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure E (T ())
e
ηM e :: E (T ())
e@BLit{}                = E (T ()) -> RM (E (T ()))
forall a. a -> StateT Int Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure E (T ())
e
ηM e :: E (T ())
e@Tup{}                 = E (T ()) -> RM (E (T ()))
forall a. a -> StateT Int Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure E (T ())
e
ηM e :: E (T ())
e@(Var t :: T ()
t@Arrow{} Nm (T ())
_)     = [T ()] -> E (T ()) -> RM (E (T ()))
mkLam (T () -> [T ()]
forall a. T a -> [T a]
doms T ()
t) E (T ())
e
ηM e :: E (T ())
e@Var{}                 = E (T ()) -> RM (E (T ()))
forall a. a -> StateT Int Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure E (T ())
e
ηM e :: E (T ())
e@(Builtin t :: T ()
t@Arrow{} Builtin
_) = [T ()] -> E (T ()) -> RM (E (T ()))
mkLam (T () -> [T ()]
forall a. T a -> [T a]
doms T ()
t) E (T ())
e
ηM e :: E (T ())
e@Builtin{}             = E (T ()) -> RM (E (T ()))
forall a. a -> StateT Int Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure E (T ())
e
ηM e :: E (T ())
e@(EApp t :: T ()
t@Arrow{} E (T ())
_ E (T ())
_)  = [T ()] -> E (T ()) -> RM (E (T ()))
mkLam (T () -> [T ()]
forall a. T a -> [T a]
doms T ()
t) E (T ())
e
ηM e :: E (T ())
e@EApp{}                = E (T ()) -> RM (E (T ()))
forall a. a -> StateT Int Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure E (T ())
e
ηM e :: E (T ())
e@LLet{}                = E (T ()) -> RM (E (T ()))
forall a. a -> StateT Int Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure E (T ())
e
ηM e :: E (T ())
e@(Lam t :: T ()
t@Arrow{} Nm (T ())
_ E (T ())
_)   = do
    let l :: Int
l = [T ()] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (T () -> [T ()]
forall a. T a -> [T a]
doms T ()
t)
        (E (T ()) -> E (T ())
preL, E (T ())
e') = E (T ()) -> (E (T ()) -> E (T ()), E (T ()))
forall a. E a -> (E a -> E a, E a)
tuck E (T ())
e
    (lam, app) <- [T ()] -> RM (E (T ()) -> E (T ()), E (T ()) -> E (T ()))
unseam (Int -> [T ()] -> [T ()]
forall a. Int -> [a] -> [a]
take (Int
lInt -> Int -> Int
forall a. Num a => a -> a -> a
-E (T ()) -> Int
forall a. E a -> Int
cLam E (T ())
e) ([T ()] -> [T ()]) -> [T ()] -> [T ()]
forall a b. (a -> b) -> a -> b
$ T () -> [T ()]
forall a. T a -> [T a]
doms T ()
t)
    pure (lam (preL (app e')))
-- "\\y. (y*)" -> (λx. (λy. (y * x)))