{-# LANGUAGE OverloadedStrings #-}

module A.Opt ( optA
             ) where

import           A
import           Data.Bits ((.<<.), (.>>.))
import           R
import           R.R

-- TODO zip-of-map->zip

fop :: Builtin -> E (T a) -> E (T a) -> E (T a)
fop Builtin
op E (T a)
e0 = T a -> E (T a) -> E (T a) -> E (T a)
forall a. a -> E a -> E a -> E a
EApp T a
forall a. T a
F (T a -> E (T a) -> E (T a) -> E (T a)
forall a. a -> E a -> E a -> E a
EApp (T a
forall a. T a
F T a -> T a -> T a
forall {a}. T a -> T a -> T a
~> T a
forall a. T a
F) (T a -> Builtin -> E (T a)
forall a. a -> Builtin -> E a
Builtin (T a
forall a. T a
F T a -> T a -> T a
forall {a}. T a -> T a -> T a
~> T a
forall a. T a
F T a -> T a -> T a
forall {a}. T a -> T a -> T a
~> T a
forall a. T a
F) Builtin
op) E (T a)
e0)
eMinus :: E (T a) -> E (T a) -> E (T a)
eMinus = Builtin -> E (T a) -> E (T a) -> E (T a)
forall {a}. Builtin -> E (T a) -> E (T a) -> E (T a)
fop Builtin
Minus; eDiv :: E (T a) -> E (T a) -> E (T a)
eDiv = Builtin -> E (T a) -> E (T a) -> E (T a)
forall {a}. Builtin -> E (T a) -> E (T a) -> E (T a)
fop Builtin
Div

mShLit :: E (T ()) -> Maybe ([Int], [E (T ())])
mShLit (Id T ()
_ (AShLit [Int]
is [E (T ())]
es)) = ([Int], [E (T ())]) -> Maybe ([Int], [E (T ())])
forall a. a -> Maybe a
Just ([Int]
is, [E (T ())]
es)
mShLit (ALit T ()
_ [E (T ())]
es)           = ([Int], [E (T ())]) -> Maybe ([Int], [E (T ())])
forall a. a -> Maybe a
Just ([[E (T ())] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [E (T ())]
es], [E (T ())]
es)
mShLit E (T ())
_                     = Maybe ([Int], [E (T ())])
forall a. Maybe a
Nothing

mSz :: Sh a -> Maybe Int
mSz :: forall a. Sh a -> Maybe Int
mSz (Ix a
_ Int
i `Cons` Sh a
sh) = (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
*)(Int -> Int) -> Maybe Int -> Maybe Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>Sh a -> Maybe Int
forall a. Sh a -> Maybe Int
mSz Sh a
sh
mSz Sh a
Nil                = Int -> Maybe Int
forall a. a -> Maybe a
Just Int
1
mSz Sh a
_                  = Maybe Int
forall a. Maybe a
Nothing

optA :: E (T ()) -> RM (E (T ()))
optA :: E (T ()) -> RM (E (T ()))
optA (ILit T ()
F Integer
x)            = E (T ()) -> RM (E (T ()))
forall a. a -> StateT Rs Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (T () -> Double -> E (T ())
forall a. a -> Double -> E a
FLit T ()
forall a. T a
F (Integer -> Double
forall a b. (Real a, Fractional b) => a -> b
realToFrac Integer
x))
optA e :: E (T ())
e@ILit{}              = E (T ()) -> RM (E (T ()))
forall a. a -> StateT Rs Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure E (T ())
e
optA e :: E (T ())
e@FLit{}              = E (T ()) -> RM (E (T ()))
forall a. a -> StateT Rs Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure E (T ())
e
optA e :: E (T ())
e@BLit{}              = E (T ()) -> RM (E (T ()))
forall a. a -> StateT Rs Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure E (T ())
e
optA e :: E (T ())
e@Var{}               = E (T ()) -> RM (E (T ()))
forall a. a -> StateT Rs Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure E (T ())
e
optA (Builtin T ()
t (Rank [(Int, Maybe [Int])]
rs)) = E (T ()) -> RM (E (T ()))
forall a. a -> StateT Rs Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (T () -> Builtin -> E (T ())
forall a. a -> Builtin -> E a
Builtin T ()
t ([(Int, Maybe [Int])] -> Builtin
Rank ((Int, Maybe [Int]) -> (Int, Maybe [Int])
forall {a}. (Num a, Enum a) => (a, Maybe [a]) -> (a, Maybe [a])
g((Int, Maybe [Int]) -> (Int, Maybe [Int]))
-> [(Int, Maybe [Int])] -> [(Int, Maybe [Int])]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>[(Int, Maybe [Int])]
rs))) where g :: (a, Maybe [a]) -> (a, Maybe [a])
g r :: (a, Maybe [a])
r@(a
_,Just{})=(a, Maybe [a])
r; g (a
cr,Maybe [a]
Nothing)=(a
cr, [a] -> Maybe [a]
forall a. a -> Maybe a
Just [a
1..a
cr])
optA (Builtin T ()
ty Builtin
C)        | Arrow T ()
fTy (Arrow T ()
gTy xTy :: T ()
xTy@(Arrow T ()
tC T ()
tD)) <- T ()
ty = do
    f <- Text -> T () -> RM (Nm (T ()))
forall a. Text -> a -> RM (Nm a)
nextU Text
"f" T ()
fTy; g <- nextU "g" gTy; x <- nextU "x" tC
    pure $ Lam ty f (Lam (gTy ~> xTy) g (Lam (tC ~> tD) x (EApp tD (Var fTy f) (EApp undefined (Var gTy g) (Var tC x)))))
optA e :: E (T ())
e@Builtin{}           = E (T ()) -> RM (E (T ()))
forall a. a -> StateT Rs Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure E (T ())
e
optA (EApp T ()
_ (Builtin T ()
_ Builtin
Size) E (T ())
xs) | Arr Sh ()
sh T ()
_ <- E (T ()) -> T ()
forall a. E a -> a
eAnn E (T ())
xs, Just Int
sz <- Sh () -> Maybe Int
forall a. Sh a -> Maybe Int
mSz Sh ()
sh = E (T ()) -> RM (E (T ()))
forall a. a -> StateT Rs Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (E (T ()) -> RM (E (T ()))) -> E (T ()) -> RM (E (T ()))
forall a b. (a -> b) -> a -> b
$ T () -> Integer -> E (T ())
forall a. a -> Integer -> E a
ILit T ()
forall a. T a
I (Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
sz)
optA (EApp T ()
_ (Builtin T ()
_ Builtin
Dim) E (T ())
xs) | Arr (Ix ()
_ Int
i `Cons` Sh ()
_) T ()
_ <- E (T ()) -> T ()
forall a. E a -> a
eAnn E (T ())
xs = E (T ()) -> RM (E (T ()))
forall a. a -> StateT Rs Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (E (T ()) -> RM (E (T ()))) -> E (T ()) -> RM (E (T ()))
forall a b. (a -> b) -> a -> b
$ T () -> Integer -> E (T ())
forall a. a -> Integer -> E a
ILit T ()
forall a. T a
I (Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
i)
optA (EApp T ()
l0 (EApp T ()
l1 op :: E (T ())
op@(Builtin T ()
_ Builtin
Exp) E (T ())
e0) E (T ())
e1) = do
    e0' <- E (T ()) -> RM (E (T ()))
optA E (T ())
e0
    e1' <- optA e1
    pure $ case (e0', e1') of
        (FLit T ()
_ Double
x, FLit T ()
_ Double
y) -> T () -> Double -> E (T ())
forall a. a -> Double -> E a
FLit T ()
l0 (Double
xDouble -> Double -> Double
forall a. Floating a => a -> a -> a
**Double
y)
        (E (T ()), E (T ()))
_                    -> T () -> E (T ()) -> E (T ()) -> E (T ())
forall a. a -> E a -> E a -> E a
EApp T ()
l0 (T () -> E (T ()) -> E (T ()) -> E (T ())
forall a. a -> E a -> E a -> E a
EApp T ()
l1 E (T ())
op E (T ())
e0') E (T ())
e1'
optA (EApp T ()
l0 (EApp T ()
l1 op :: E (T ())
op@(Builtin T ()
l2 Builtin
Div) E (T ())
e0) E (T ())
e1) = do
    e0' <- E (T ()) -> RM (E (T ()))
optA E (T ())
e0
    e1' <- optA e1
    pure $ case (e0', e1') of
        (FLit T ()
_ Double
x, FLit T ()
_ Double
y) -> T () -> Double -> E (T ())
forall a. a -> Double -> E a
FLit T ()
l0 (Double
xDouble -> Double -> Double
forall a. Fractional a => a -> a -> a
/Double
y)
        (E (T ())
x, FLit T ()
t Double
y)        -> T () -> E (T ()) -> E (T ()) -> E (T ())
forall a. a -> E a -> E a -> E a
EApp T ()
l0 (T () -> E (T ()) -> E (T ()) -> E (T ())
forall a. a -> E a -> E a -> E a
EApp T ()
l1 (T () -> Builtin -> E (T ())
forall a. a -> Builtin -> E a
Builtin T ()
l2 Builtin
Times) E (T ())
x) (T () -> Double -> E (T ())
forall a. a -> Double -> E a
FLit T ()
t (Double
1Double -> Double -> Double
forall a. Fractional a => a -> a -> a
/Double
y))
        (E (T ()), E (T ()))
_                    -> T () -> E (T ()) -> E (T ()) -> E (T ())
forall a. a -> E a -> E a -> E a
EApp T ()
l0 (T () -> E (T ()) -> E (T ()) -> E (T ())
forall a. a -> E a -> E a -> E a
EApp T ()
l1 E (T ())
op E (T ())
e0') E (T ())
e1'
optA (EApp T ()
l0 op :: E (T ())
op@(Builtin T ()
_ Builtin
N) E (T ())
e0) = do
    e0' <- E (T ()) -> RM (E (T ()))
optA E (T ())
e0
    pure $ case e0' of
        (BLit T ()
_ Bool
b) -> T () -> Bool -> E (T ())
forall a. a -> Bool -> E a
BLit T ()
forall a. T a
B (Bool -> Bool
not Bool
b)
        E (T ())
_          -> T () -> E (T ()) -> E (T ()) -> E (T ())
forall a. a -> E a -> E a -> E a
EApp T ()
l0 E (T ())
op E (T ())
e0'
optA (EApp T ()
l0 (EApp T ()
l1 op :: E (T ())
op@(Builtin T ()
_ Builtin
Sr) E (T ())
e0) E (T ())
e1) = do
    e0' <- E (T ()) -> RM (E (T ()))
optA E (T ())
e0
    e1' <- optA e1
    pure $ case (e0', e1') of
        (ILit T ()
_ Integer
m, ILit T ()
_ Integer
n) -> T () -> Integer -> E (T ())
forall a. a -> Integer -> E a
ILit T ()
forall a. T a
I (Integer
m Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
.>>. Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
n)
        (E (T ()), E (T ()))
_                    -> T () -> E (T ()) -> E (T ()) -> E (T ())
forall a. a -> E a -> E a -> E a
EApp T ()
l0 (T () -> E (T ()) -> E (T ()) -> E (T ())
forall a. a -> E a -> E a -> E a
EApp T ()
l1 E (T ())
op E (T ())
e0') E (T ())
e1'
optA (EApp T ()
l0 (EApp T ()
l1 op :: E (T ())
op@(Builtin T ()
_ Builtin
Sl) E (T ())
e0) E (T ())
e1) = do
    e0' <- E (T ()) -> RM (E (T ()))
optA E (T ())
e0
    e1' <- optA e1
    pure $ case (e0', e1') of
        (ILit T ()
_ Integer
m, ILit T ()
_ Integer
n) -> T () -> Integer -> E (T ())
forall a. a -> Integer -> E a
ILit T ()
forall a. T a
I (Integer
m Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
.<<. Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
n)
        (E (T ()), E (T ()))
_                    -> T () -> E (T ()) -> E (T ()) -> E (T ())
forall a. a -> E a -> E a -> E a
EApp T ()
l0 (T () -> E (T ()) -> E (T ()) -> E (T ())
forall a. a -> E a -> E a -> E a
EApp T ()
l1 E (T ())
op E (T ())
e0') E (T ())
e1'
optA (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 ()))
optA E (T ())
e
optA (EApp T ()
l0 (EApp T ()
l1 op :: E (T ())
op@(Builtin T ()
_ Builtin
Times) E (T ())
x) E (T ())
y) = do
    xO <- E (T ()) -> RM (E (T ()))
optA E (T ())
x
    yO <- optA y
    pure $ case (xO, yO) of
        (FLit T ()
_ Double
x', FLit T ()
_ Double
y') -> T () -> Double -> E (T ())
forall a. a -> Double -> E a
FLit T ()
forall a. T a
F (Double
x'Double -> Double -> Double
forall a. Num a => a -> a -> a
*Double
y')
        (FLit T ()
_ Double
x', ILit T ()
_ Integer
y') -> T () -> Double -> E (T ())
forall a. a -> Double -> E a
FLit T ()
forall a. T a
F (Double
x'Double -> Double -> Double
forall a. Num a => a -> a -> a
*Integer -> Double
forall a b. (Real a, Fractional b) => a -> b
realToFrac Integer
y')
        (ILit T ()
_ Integer
x', FLit T ()
_ Double
y') -> T () -> Double -> E (T ())
forall a. a -> Double -> E a
FLit T ()
forall a. T a
F (Integer -> Double
forall a b. (Real a, Fractional b) => a -> b
realToFrac Integer
x'Double -> Double -> Double
forall a. Num a => a -> a -> a
*Double
y')
        (E (T ()), E (T ()))
_                      -> T () -> E (T ()) -> E (T ()) -> E (T ())
forall a. a -> E a -> E a -> E a
EApp T ()
l0 (T () -> E (T ()) -> E (T ()) -> E (T ())
forall a. a -> E a -> E a -> E a
EApp T ()
l1 E (T ())
op E (T ())
xO) E (T ())
yO
optA (EApp T ()
l0 f :: E (T ())
f@(Builtin T ()
_ Builtin
ItoF) E (T ())
x) = do
    x' <- E (T ()) -> RM (E (T ()))
optA E (T ())
x
    pure $ case x' of
        ILit T ()
_ Integer
n -> T () -> Double -> E (T ())
forall a. a -> Double -> E a
FLit T ()
forall a. T a
F (Integer -> Double
forall a b. (Real a, Fractional b) => a -> b
realToFrac Integer
n)
        E (T ())
_        -> T () -> E (T ()) -> E (T ()) -> E (T ())
forall a. a -> E a -> E a -> E a
EApp T ()
l0 E (T ())
f E (T ())
x'
optA (EApp T ()
l0 (EApp T ()
l1 op :: E (T ())
op@(Builtin T ()
_ Builtin
Minus) E (T ())
x) E (T ())
y) = do
    xO <- E (T ()) -> RM (E (T ()))
optA E (T ())
x
    yO <- optA y
    pure $ case (xO, yO) of
        (FLit T ()
_ Double
x', FLit T ()
_ Double
y') -> T () -> Double -> E (T ())
forall a. a -> Double -> E a
FLit T ()
forall a. T a
F (Double
x'Double -> Double -> Double
forall a. Num a => a -> a -> a
-Double
y')
        (FLit T ()
_ Double
x', ILit T ()
_ Integer
y') -> T () -> Double -> E (T ())
forall a. a -> Double -> E a
FLit T ()
forall a. T a
F (Double
x'Double -> Double -> Double
forall a. Num a => a -> a -> a
-Integer -> Double
forall a b. (Real a, Fractional b) => a -> b
realToFrac Integer
y')
        (ILit T ()
_ Integer
x', FLit T ()
_ Double
y') -> T () -> Double -> E (T ())
forall a. a -> Double -> E a
FLit T ()
forall a. T a
F (Integer -> Double
forall a b. (Real a, Fractional b) => a -> b
realToFrac Integer
x'Double -> Double -> Double
forall a. Num a => a -> a -> a
-Double
y')
        (E (T ()), E (T ()))
_                      -> T () -> E (T ()) -> E (T ()) -> E (T ())
forall a. a -> E a -> E a -> E a
EApp T ()
l0 (T () -> E (T ()) -> E (T ()) -> E (T ())
forall a. a -> E a -> E a -> E a
EApp T ()
l1 E (T ())
op E (T ())
xO) E (T ())
yO
optA (EApp T ()
l op :: E (T ())
op@(Builtin T ()
_ Builtin
Sqrt) E (T ())
x) = do
    xO <- E (T ()) -> RM (E (T ()))
optA E (T ())
x
    pure $ case xO of
        FLit T ()
_ Double
z -> T () -> Double -> E (T ())
forall a. a -> Double -> E a
FLit T ()
forall a. T a
F (Double -> Double
forall a. Floating a => a -> a
sqrt Double
z)
        E (T ())
_        -> T () -> E (T ()) -> E (T ()) -> E (T ())
forall a. a -> E a -> E a -> E a
EApp T ()
l E (T ())
op E (T ())
xO
optA (EApp T ()
_ (Builtin T ()
_ Builtin
Floor) (EApp T ()
_ (Builtin T ()
_ Builtin
ItoF) E (T ())
x)) = E (T ()) -> RM (E (T ()))
optA E (T ())
x
optA (EApp T ()
ty (EApp T ()
_ (Builtin T ()
_ Builtin
IntExp) E (T ())
x) (ILit T ()
_ Integer
2)) = E (T ()) -> RM (E (T ()))
forall a. a -> StateT Rs Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (E (T ()) -> RM (E (T ()))) -> E (T ()) -> RM (E (T ()))
forall a b. (a -> b) -> a -> b
$ T () -> E (T ()) -> E (T ()) -> E (T ())
forall a. a -> E a -> E a -> E a
EApp T ()
ty (T () -> E (T ()) -> E (T ()) -> E (T ())
forall a. a -> E a -> E a -> E a
EApp (T ()
ty T () -> T () -> T ()
forall {a}. T a -> T a -> T a
~> T ()
ty) (T () -> Builtin -> E (T ())
forall a. a -> Builtin -> E a
Builtin (T ()
ty T () -> T () -> T ()
forall {a}. T a -> T a -> T a
~> T ()
ty T () -> T () -> T ()
forall {a}. T a -> T a -> T a
~> T ()
ty) Builtin
Times) E (T ())
x) E (T ())
x
optA (EApp T ()
l0 (EApp T ()
_ (Builtin T ()
_ Builtin
Fold) E (T ())
op) (EApp T ()
_ (EApp T ()
_ (EApp T ()
_ (Builtin T ()
_ Builtin
FRange) E (T ())
start) E (T ())
end) E (T ())
nSteps)) = do
    start' <- E (T ()) -> RM (E (T ()))
optA E (T ())
start
    incrN <- optA $ (end `eMinus` start) `eDiv` (EApp F (Builtin (Arrow I F) ItoF) nSteps `eMinus` FLit F 1)
    fF <- optA op
    n <- nextU "n" F
    pure $ Id l0 $ FoldGen start' (Lam (F ~> F) n (EApp F (EApp (F ~> F) (Builtin (F ~> F ~> F) Plus) incrN) (Var F n))) fF nSteps
optA (EApp T ()
l0 (EApp T ()
_ (Builtin T ()
_ Builtin
Fold) E (T ())
op) (EApp T ()
_ (EApp T ()
_ (EApp T ()
_ (Builtin T ()
_ Builtin
Gen) E (T ())
seed) E (T ())
f) E (T ())
n)) =
    T () -> Idiom -> E (T ())
forall a. a -> Idiom -> E a
Id T ()
l0 (Idiom -> E (T ())) -> StateT Rs Identity Idiom -> RM (E (T ()))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (E (T ()) -> E (T ()) -> E (T ()) -> E (T ()) -> Idiom
FoldGen (E (T ()) -> E (T ()) -> E (T ()) -> E (T ()) -> Idiom)
-> RM (E (T ()))
-> StateT Rs 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 ()))
optA E (T ())
seed StateT Rs Identity (E (T ()) -> E (T ()) -> E (T ()) -> Idiom)
-> RM (E (T ()))
-> StateT Rs Identity (E (T ()) -> E (T ()) -> Idiom)
forall a b.
StateT Rs Identity (a -> b)
-> StateT Rs Identity a -> StateT Rs Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> E (T ()) -> RM (E (T ()))
optA E (T ())
f StateT Rs Identity (E (T ()) -> E (T ()) -> Idiom)
-> RM (E (T ())) -> StateT Rs Identity (E (T ()) -> Idiom)
forall a b.
StateT Rs Identity (a -> b)
-> StateT Rs Identity a -> StateT Rs Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> E (T ()) -> RM (E (T ()))
optA E (T ())
op StateT Rs Identity (E (T ()) -> Idiom)
-> RM (E (T ())) -> StateT Rs Identity Idiom
forall a b.
StateT Rs Identity (a -> b)
-> StateT Rs Identity a -> StateT Rs Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> E (T ()) -> RM (E (T ()))
optA E (T ())
n)
optA (EApp T ()
l0 (EApp T ()
_ (EApp T ()
_ (Builtin T ()
_ ho0 :: Builtin
ho0@Builtin
FoldS) E (T ())
op) E (T ())
seed) (EApp T ()
_ (EApp T ()
_ (Builtin T ()
_ Builtin
Map) E (T ())
f) E (T ())
x))
    | Arrow T ()
dom T ()
fCod <- E (T ()) -> T ()
forall a. E a -> a
eAnn E (T ())
f
    , Arrow T ()
_ (Arrow T ()
_ T ()
cod) <- E (T ()) -> T ()
forall a. E a -> a
eAnn E (T ())
op = do
        x' <- E (T ()) -> RM (E (T ()))
optA E (T ())
x
        x0 <- nextU "x" cod; x1 <- nextU "y" dom
        opA <- optA op
        let vx0 = T () -> Nm (T ()) -> E (T ())
forall a. a -> Nm a -> E a
Var T ()
cod Nm (T ())
x0; vx1 = T () -> Nm (T ()) -> E (T ())
forall a. a -> Nm a -> E a
Var T ()
dom Nm (T ())
x1
            opTy = T ()
cod T () -> T () -> T ()
forall {a}. T a -> T a -> T a
~> T ()
dom T () -> T () -> T ()
forall {a}. T a -> T a -> T a
~> T ()
cod
            op' = T () -> Nm (T ()) -> E (T ()) -> E (T ())
forall a. a -> Nm a -> E a -> E a
Lam T ()
opTy Nm (T ())
x0 (T () -> Nm (T ()) -> E (T ()) -> E (T ())
forall a. a -> Nm a -> E a -> E a
Lam (T ()
dom T () -> T () -> T ()
forall {a}. T a -> T a -> T a
~> T ()
cod) Nm (T ())
x1 (T () -> E (T ()) -> E (T ()) -> E (T ())
forall a. a -> E a -> E a -> E a
EApp T ()
cod (T () -> E (T ()) -> E (T ()) -> E (T ())
forall a. a -> E a -> E a -> E a
EApp T ()
forall a. HasCallStack => a
undefined E (T ())
opA E (T ())
vx0) (T () -> E (T ()) -> E (T ()) -> E (T ())
forall a. a -> E a -> E a -> E a
EApp T ()
fCod E (T ())
f E (T ())
vx1)))
            arrTy = E (T ()) -> T ()
forall a. E a -> a
eAnn E (T ())
x'
        optA (EApp l0 (EApp undefined (EApp (arrTy ~> l0) (Builtin (opTy ~> arrTy ~> l0) ho0) op') seed) x')
optA (EApp T ()
l0 (EApp T ()
_ (Builtin T ()
_ Builtin
Succ) E (T ())
f) (EApp T ()
_ (EApp T ()
_ (Builtin T ()
_ Builtin
Map) E (T ())
g) E (T ())
xs))
    | (Arrow T ()
_ (Arrow T ()
_ T ()
fCod)) <- E (T ()) -> T ()
forall a. E a -> a
eAnn E (T ())
f
    , (Arrow T ()
gDom T ()
_) <- E (T ()) -> T ()
forall a. E a -> a
eAnn E (T ())
g = do
        f' <- E (T ()) -> RM (E (T ()))
optA E (T ())
f; g' <- optA g; g'' <- rE g
        xs' <- optA xs
        x <- nextU "w" gDom; y <- nextU "v" gDom
        let vx=T () -> Nm (T ()) -> E (T ())
forall a. a -> Nm a -> E a
Var T ()
gDom Nm (T ())
x; vy=T () -> Nm (T ()) -> E (T ())
forall a. a -> Nm a -> E a
Var T ()
gDom Nm (T ())
y
            f2g=T () -> Nm (T ()) -> E (T ()) -> E (T ())
forall a. a -> Nm a -> E a -> E a
Lam (T ()
gDom T () -> T () -> T ()
forall {a}. T a -> T a -> T a
~> T ()
gDom T () -> T () -> T ()
forall {a}. T a -> T a -> T a
~> T ()
fCod) Nm (T ())
x (T () -> Nm (T ()) -> E (T ()) -> E (T ())
forall a. a -> Nm a -> E a -> E a
Lam (T ()
gDom T () -> T () -> T ()
forall {a}. T a -> T a -> T a
~> T ()
fCod) Nm (T ())
y (T () -> E (T ()) -> E (T ()) -> E (T ())
forall a. a -> E a -> E a -> E a
EApp T ()
forall a. HasCallStack => a
undefined (T () -> E (T ()) -> E (T ()) -> E (T ())
forall a. a -> E a -> E a -> E a
EApp T ()
forall a. HasCallStack => a
undefined E (T ())
f' (T () -> E (T ()) -> E (T ()) -> E (T ())
forall a. a -> E a -> E a -> E a
EApp T ()
forall a. HasCallStack => a
undefined E (T ())
g' E (T ())
vx)) (T () -> E (T ()) -> E (T ()) -> E (T ())
forall a. a -> E a -> E a -> E a
EApp T ()
forall a. HasCallStack => a
undefined E (T ())
g'' E (T ())
vy)))
        pure (EApp l0 (EApp undefined (Builtin undefined Succ) f2g) xs')
optA (EApp T ()
l0 (EApp T ()
_ (Builtin T ()
_ Builtin
Map) E (T ())
f) (EApp T ()
_ (EApp T ()
_ (Builtin T ()
_ Builtin
Map) E (T ())
g) E (T ())
xs))
    | (Arrow T ()
_ T ()
fCod) <- E (T ()) -> T ()
forall a. E a -> a
eAnn E (T ())
f
    , (Arrow T ()
gDom T ()
_) <- E (T ()) -> T ()
forall a. E a -> a
eAnn E (T ())
g = do
        f' <- E (T ()) -> RM (E (T ()))
optA E (T ())
f; g' <- optA g
        xs' <- optA xs
        x <- nextU "x" gDom
        let vx=T () -> Nm (T ()) -> E (T ())
forall a. a -> Nm a -> E a
Var T ()
gDom Nm (T ())
x
            fog=T () -> Nm (T ()) -> E (T ()) -> E (T ())
forall a. a -> Nm a -> E a -> E a
Lam (T ()
gDom T () -> T () -> T ()
forall {a}. T a -> T a -> T a
~> T ()
fCod) Nm (T ())
x (T () -> E (T ()) -> E (T ()) -> E (T ())
forall a. a -> E a -> E a -> E a
EApp T ()
forall a. HasCallStack => a
undefined E (T ())
f' (T () -> E (T ()) -> E (T ()) -> E (T ())
forall a. a -> E a -> E a -> E a
EApp T ()
forall a. HasCallStack => a
undefined E (T ())
g' E (T ())
vx))
        pure (EApp l0 (EApp undefined (Builtin undefined Map) fog) xs')
optA (EApp T ()
l0 (EApp T ()
_ (Builtin T ()
_ Builtin
Fold) E (T ())
op) (EApp T ()
_ (EApp T ()
_ (Builtin T ()
_ Builtin
Map) E (T ())
f) E (T ())
x))
    | fTy :: T ()
fTy@(Arrow T ()
dom T ()
fCod) <- E (T ()) -> T ()
forall a. E a -> a
eAnn E (T ())
f
    , Arrow T ()
_ (Arrow T ()
_ T ()
cod) <- E (T ()) -> T ()
forall a. E a -> a
eAnn E (T ())
op = do
        f' <- E (T ()) -> RM (E (T ()))
optA E (T ())
f; f'' <- rE f'
        x' <- optA x
        x0 <- nextU "x" cod; x1 <- nextU "y" dom
        x0' <- nextU "x" dom
        opA <- optA op
        let vx0 = T () -> Nm (T ()) -> E (T ())
forall a. a -> Nm a -> E a
Var T ()
cod Nm (T ())
x0; vx1 = T () -> Nm (T ()) -> E (T ())
forall a. a -> Nm a -> E a
Var T ()
dom Nm (T ())
x1
            vx0' = T () -> Nm (T ()) -> E (T ())
forall a. a -> Nm a -> E a
Var T ()
dom Nm (T ())
x0'
            opT = T ()
cod T () -> T () -> T ()
forall {a}. T a -> T a -> T a
~> T ()
dom T () -> T () -> T ()
forall {a}. T a -> T a -> T a
~> T ()
cod
            op' = T () -> Nm (T ()) -> E (T ()) -> E (T ())
forall a. a -> Nm a -> E a -> E a
Lam T ()
opT Nm (T ())
x0 (T () -> Nm (T ()) -> E (T ()) -> E (T ())
forall a. a -> Nm a -> E a -> E a
Lam (T ()
dom T () -> T () -> T ()
forall {a}. T a -> T a -> T a
~> T ()
cod) Nm (T ())
x1 (T () -> E (T ()) -> E (T ()) -> E (T ())
forall a. a -> E a -> E a -> E a
EApp T ()
cod (T () -> E (T ()) -> E (T ()) -> E (T ())
forall a. a -> E a -> E a -> E a
EApp T ()
forall a. HasCallStack => a
undefined E (T ())
opA E (T ())
vx0) (T () -> E (T ()) -> E (T ()) -> E (T ())
forall a. a -> E a -> E a -> E a
EApp T ()
fCod E (T ())
f' E (T ())
vx1)))
            f''' = T () -> Nm (T ()) -> E (T ()) -> E (T ())
forall a. a -> Nm a -> E a -> E a
Lam T ()
fTy Nm (T ())
x0' (T () -> E (T ()) -> E (T ()) -> E (T ())
forall a. a -> E a -> E a -> E a
EApp T ()
fCod E (T ())
f'' E (T ())
vx0')
        pure $ Id l0 $ FoldOfZip f''' op' [x']
optA (EApp T ()
l0 (EApp T ()
_ (Builtin T ()
_ (Rank [(Int
0,Maybe [Int]
_)])) E (T ())
f) (EApp T ()
_ (EApp T ()
_ (EApp T ()
_ ho :: E (T ())
ho@(Builtin T ()
_ (Rank [(Int
0,Maybe [Int]
_),(Int
0,Maybe [Int]
_)])) E (T ())
op) E (T ())
xs) E (T ())
ys))
    | Arrow T ()
_ T ()
cod <- E (T ()) -> T ()
forall a. E a -> a
eAnn E (T ())
f
    , Arrow T ()
dom0 (Arrow T ()
dom1 T ()
_) <- E (T ()) -> T ()
forall a. E a -> a
eAnn E (T ())
op = do
        f' <- E (T ()) -> RM (E (T ()))
optA E (T ())
f; opA <- optA op; ho' <- optA ho
        xs' <- optA xs; ys' <- optA ys
        x <- nextU "x" dom0; y <- nextU "y" dom1
        let vx=T () -> Nm (T ()) -> E (T ())
forall a. a -> Nm a -> E a
Var T ()
dom0 Nm (T ())
x; vy=T () -> Nm (T ()) -> E (T ())
forall a. a -> Nm a -> E a
Var T ()
dom1 Nm (T ())
y
            opTy = T ()
dom0 T () -> T () -> T ()
forall {a}. T a -> T a -> T a
~> T ()
dom1 T () -> T () -> T ()
forall {a}. T a -> T a -> T a
~> T ()
cod
            op' = T () -> Nm (T ()) -> E (T ()) -> E (T ())
forall a. a -> Nm a -> E a -> E a
Lam T ()
opTy Nm (T ())
x (T () -> Nm (T ()) -> E (T ()) -> E (T ())
forall a. a -> Nm a -> E a -> E a
Lam T ()
forall a. HasCallStack => a
undefined Nm (T ())
y (T () -> E (T ()) -> E (T ()) -> E (T ())
forall a. a -> E a -> E a -> E a
EApp T ()
forall a. HasCallStack => a
undefined E (T ())
f' (T () -> E (T ()) -> E (T ()) -> E (T ())
forall a. a -> E a -> E a -> E a
EApp T ()
forall a. HasCallStack => a
undefined (T () -> E (T ()) -> E (T ()) -> E (T ())
forall a. a -> E a -> E a -> E a
EApp T ()
forall a. HasCallStack => a
undefined E (T ())
opA E (T ())
vx) E (T ())
vy)))
        pure (EApp l0 (EApp undefined (EApp undefined (ho' { eAnn = undefined }) op') xs') ys')
optA (EApp T ()
l0 (EApp T ()
_ (EApp T ()
_ ho :: E (T ())
ho@(Builtin T ()
_ (Rank [(Int
0,Maybe [Int]
_),(Int
0,Maybe [Int]
_)])) E (T ())
op) (EApp T ()
_ (EApp T ()
_ (Builtin T ()
_ (Rank [(Int
0,Maybe [Int]
_)])) E (T ())
f) E (T ())
xs)) (EApp T ()
_ (EApp T ()
_ (Builtin T ()
_ (Rank [(Int
0,Maybe [Int]
_)])) E (T ())
g) E (T ())
ys))
    | Arrow T ()
dom0 T ()
_ <- E (T ()) -> T ()
forall a. E a -> a
eAnn E (T ())
f
    , Arrow T ()
dom1 T ()
_ <- E (T ()) -> T ()
forall a. E a -> a
eAnn E (T ())
g
    , Arrow T ()
_ (Arrow T ()
_ T ()
cod) <- E (T ()) -> T ()
forall a. E a -> a
eAnn E (T ())
op = do
        f' <- E (T ()) -> RM (E (T ()))
optA E (T ())
f; g' <- optA g
        opA <- optA op; ho' <- optA ho
        xs' <- optA xs; ys' <- optA ys
        x <- nextU "x" dom0; y <- nextU "y" dom1
        let vx = T () -> Nm (T ()) -> E (T ())
forall a. a -> Nm a -> E a
Var T ()
dom0 Nm (T ())
x; vy = T () -> Nm (T ()) -> E (T ())
forall a. a -> Nm a -> E a
Var T ()
dom1 Nm (T ())
y
            opTy = T ()
dom0 T () -> T () -> T ()
forall {a}. T a -> T a -> T a
~> T ()
dom1 T () -> T () -> T ()
forall {a}. T a -> T a -> T a
~> T ()
cod
            op' = T () -> Nm (T ()) -> E (T ()) -> E (T ())
forall a. a -> Nm a -> E a -> E a
Lam T ()
opTy Nm (T ())
x (T () -> Nm (T ()) -> E (T ()) -> E (T ())
forall a. a -> Nm a -> E a -> E a
Lam T ()
forall a. HasCallStack => a
undefined Nm (T ())
y (T () -> E (T ()) -> E (T ()) -> E (T ())
forall a. a -> E a -> E a -> E a
EApp T ()
forall a. HasCallStack => a
undefined (T () -> E (T ()) -> E (T ()) -> E (T ())
forall a. a -> E a -> E a -> E a
EApp T ()
forall a. HasCallStack => a
undefined E (T ())
opA (T () -> E (T ()) -> E (T ()) -> E (T ())
forall a. a -> E a -> E a -> E a
EApp T ()
forall a. HasCallStack => a
undefined E (T ())
f' E (T ())
vx)) (T () -> E (T ()) -> E (T ()) -> E (T ())
forall a. a -> E a -> E a -> E a
EApp T ()
forall a. HasCallStack => a
undefined E (T ())
g' E (T ())
vy)))
        pure (EApp l0 (EApp undefined (EApp undefined (ho' { eAnn = undefined }) op') xs') ys')
optA (EApp T ()
l0 (EApp T ()
_ (EApp T ()
_ ho :: E (T ())
ho@(Builtin T ()
_ (Rank [(Int
0,Maybe [Int]
_),(Int
0,Maybe [Int]
_)])) E (T ())
op) E (T ())
xs) (EApp T ()
_ (EApp T ()
_ (Builtin T ()
_ (Rank [(Int
0,Maybe [Int]
_)])) E (T ())
g) E (T ())
ys))
    | Arrow T ()
dom T ()
_ <- E (T ()) -> T ()
forall a. E a -> a
eAnn E (T ())
g
    , Arrow T ()
xT (Arrow T ()
_ T ()
cod) <- E (T ()) -> T ()
forall a. E a -> a
eAnn E (T ())
op = do
        g' <- E (T ()) -> RM (E (T ()))
optA E (T ())
g
        opA <- optA op; ho' <- optA ho
        xs' <- optA xs; ys' <- optA ys
        x <- nextU "x" xT; y <- nextU "y" dom
        let vx = T () -> Nm (T ()) -> E (T ())
forall a. a -> Nm a -> E a
Var T ()
xT Nm (T ())
x; vy = T () -> Nm (T ()) -> E (T ())
forall a. a -> Nm a -> E a
Var T ()
dom Nm (T ())
y
            opTy = T ()
xT T () -> T () -> T ()
forall {a}. T a -> T a -> T a
~> T ()
dom T () -> T () -> T ()
forall {a}. T a -> T a -> T a
~> T ()
cod
            op' = T () -> Nm (T ()) -> E (T ()) -> E (T ())
forall a. a -> Nm a -> E a -> E a
Lam T ()
opTy Nm (T ())
x (T () -> Nm (T ()) -> E (T ()) -> E (T ())
forall a. a -> Nm a -> E a -> E a
Lam T ()
forall a. HasCallStack => a
undefined Nm (T ())
y (T () -> E (T ()) -> E (T ()) -> E (T ())
forall a. a -> E a -> E a -> E a
EApp T ()
forall a. HasCallStack => a
undefined (T () -> E (T ()) -> E (T ()) -> E (T ())
forall a. a -> E a -> E a -> E a
EApp T ()
forall a. HasCallStack => a
undefined E (T ())
opA E (T ())
vx) (T () -> E (T ()) -> E (T ()) -> E (T ())
forall a. a -> E a -> E a -> E a
EApp T ()
forall a. HasCallStack => a
undefined E (T ())
g' E (T ())
vy)))
        pure (EApp l0 (EApp undefined (EApp undefined (ho' { eAnn = undefined }) op') xs') ys')
optA (EApp T ()
l0 (EApp T ()
_ (EApp T ()
_ ho :: E (T ())
ho@(Builtin T ()
_ (Rank [(Int
0,Maybe [Int]
_),(Int
0,Maybe [Int]
_)])) E (T ())
op) (EApp T ()
_ (EApp T ()
_ (Builtin T ()
_ (Rank [(Int
0,Maybe [Int]
_)])) E (T ())
f) E (T ())
xs)) E (T ())
ys)
    | Arrow T ()
dom T ()
_ <- E (T ()) -> T ()
forall a. E a -> a
eAnn E (T ())
f
    , Arrow T ()
_ (Arrow T ()
yT T ()
cod) <- E (T ()) -> T ()
forall a. E a -> a
eAnn E (T ())
op = do
        f' <- E (T ()) -> RM (E (T ()))
optA E (T ())
f
        opA <- optA op; ho' <- optA ho
        xs' <- optA xs; ys' <- optA ys
        x <- nextU "x" dom; y <- nextU "y" yT
        let vx = T () -> Nm (T ()) -> E (T ())
forall a. a -> Nm a -> E a
Var T ()
dom Nm (T ())
x; vy = T () -> Nm (T ()) -> E (T ())
forall a. a -> Nm a -> E a
Var T ()
yT Nm (T ())
y
            opTy = T ()
dom T () -> T () -> T ()
forall {a}. T a -> T a -> T a
~> T ()
yT T () -> T () -> T ()
forall {a}. T a -> T a -> T a
~> T ()
cod
            op' = T () -> Nm (T ()) -> E (T ()) -> E (T ())
forall a. a -> Nm a -> E a -> E a
Lam T ()
opTy Nm (T ())
x (T () -> Nm (T ()) -> E (T ()) -> E (T ())
forall a. a -> Nm a -> E a -> E a
Lam T ()
forall a. HasCallStack => a
undefined Nm (T ())
y (T () -> E (T ()) -> E (T ()) -> E (T ())
forall a. a -> E a -> E a -> E a
EApp T ()
forall a. HasCallStack => a
undefined (T () -> E (T ()) -> E (T ()) -> E (T ())
forall a. a -> E a -> E a -> E a
EApp T ()
forall a. HasCallStack => a
undefined E (T ())
opA (T () -> E (T ()) -> E (T ()) -> E (T ())
forall a. a -> E a -> E a -> E a
EApp T ()
forall a. HasCallStack => a
undefined E (T ())
f' E (T ())
vx)) E (T ())
vy))
        pure (EApp l0 (EApp undefined (EApp undefined (ho' { eAnn = undefined }) op') xs') ys')
optA (EApp T ()
_ (EApp T ()
_ (EApp T ()
_ (Builtin T ()
_ Builtin
Zip) E (T ())
op) (EApp T ()
_ (EApp T ()
_ (Builtin T ()
_ Builtin
Map) E (T ())
f) E (T ())
xs)) (EApp T ()
_ (EApp T ()
_ (Builtin T ()
_ Builtin
Map) E (T ())
g) E (T ())
ys))
    | Arrow T ()
dom0 T ()
_ <- E (T ()) -> T ()
forall a. E a -> a
eAnn E (T ())
f
    , Arrow T ()
dom1 T ()
_ <- E (T ()) -> T ()
forall a. E a -> a
eAnn E (T ())
g
    , Arrow T ()
_ (Arrow T ()
_ T ()
cod) <- E (T ()) -> T ()
forall a. E a -> a
eAnn E (T ())
op = do
        f' <- E (T ()) -> RM (E (T ()))
optA E (T ())
f; g' <- optA g
        opA <- optA op
        xs' <- optA xs; ys' <- optA ys
        x0 <- nextU "x" dom0; x1 <- nextU "y" dom1
        let vx0 = T () -> Nm (T ()) -> E (T ())
forall a. a -> Nm a -> E a
Var T ()
dom0 Nm (T ())
x0; vx1 = T () -> Nm (T ()) -> E (T ())
forall a. a -> Nm a -> E a
Var T ()
dom1 Nm (T ())
x1
            opTy = T ()
dom0 T () -> T () -> T ()
forall {a}. T a -> T a -> T a
~> T ()
dom1 T () -> T () -> T ()
forall {a}. T a -> T a -> T a
~> T ()
cod
            op' = T () -> Nm (T ()) -> E (T ()) -> E (T ())
forall a. a -> Nm a -> E a -> E a
Lam T ()
opTy Nm (T ())
x0 (T () -> Nm (T ()) -> E (T ()) -> E (T ())
forall a. a -> Nm a -> E a -> E a
Lam T ()
forall a. HasCallStack => a
undefined Nm (T ())
x1 (T () -> E (T ()) -> E (T ()) -> E (T ())
forall a. a -> E a -> E a -> E a
EApp T ()
forall a. HasCallStack => a
undefined (T () -> E (T ()) -> E (T ()) -> E (T ())
forall a. a -> E a -> E a -> E a
EApp T ()
forall a. HasCallStack => a
undefined E (T ())
opA (T () -> E (T ()) -> E (T ()) -> E (T ())
forall a. a -> E a -> E a -> E a
EApp T ()
forall a. HasCallStack => a
undefined E (T ())
f' E (T ())
vx0)) (T () -> E (T ()) -> E (T ()) -> E (T ())
forall a. a -> E a -> E a -> E a
EApp T ()
forall a. HasCallStack => a
undefined E (T ())
g' E (T ())
vx1)))
        pure (EApp undefined (EApp undefined (EApp undefined (Builtin undefined Zip) op') xs') ys')
optA (EApp T ()
l (EApp T ()
_ (EApp T ()
_ (Builtin T ()
_ Builtin
Zip) E (T ())
op) (EApp T ()
_ (EApp T ()
_ (Builtin T ()
_ Builtin
Map) E (T ())
f) E (T ())
xs)) E (T ())
ys)
    | Arrow T ()
dom0 T ()
_ <- E (T ()) -> T ()
forall a. E a -> a
eAnn E (T ())
f
    , Arrow T ()
_ (Arrow T ()
dom1 T ()
cod) <- E (T ()) -> T ()
forall a. E a -> a
eAnn E (T ())
op = do
        f' <- E (T ()) -> RM (E (T ()))
optA E (T ())
f
        opA <- optA op
        xs' <- optA xs; ys' <- optA ys
        x0 <- nextU "x" dom0; x1 <- nextU "y" dom1
        let vx0 = T () -> Nm (T ()) -> E (T ())
forall a. a -> Nm a -> E a
Var T ()
dom0 Nm (T ())
x0; vx1 = T () -> Nm (T ()) -> E (T ())
forall a. a -> Nm a -> E a
Var T ()
dom1 Nm (T ())
x1
            opTy = T ()
dom0 T () -> T () -> T ()
forall {a}. T a -> T a -> T a
~> T ()
dom1 T () -> T () -> T ()
forall {a}. T a -> T a -> T a
~> T ()
cod
            op' = T () -> Nm (T ()) -> E (T ()) -> E (T ())
forall a. a -> Nm a -> E a -> E a
Lam T ()
opTy Nm (T ())
x0 (T () -> Nm (T ()) -> E (T ()) -> E (T ())
forall a. a -> Nm a -> E a -> E a
Lam T ()
forall a. HasCallStack => a
undefined Nm (T ())
x1 (T () -> E (T ()) -> E (T ()) -> E (T ())
forall a. a -> E a -> E a -> E a
EApp T ()
forall a. HasCallStack => a
undefined (T () -> E (T ()) -> E (T ()) -> E (T ())
forall a. a -> E a -> E a -> E a
EApp T ()
forall a. HasCallStack => a
undefined E (T ())
opA (T () -> E (T ()) -> E (T ()) -> E (T ())
forall a. a -> E a -> E a -> E a
EApp T ()
forall a. HasCallStack => a
undefined E (T ())
f' E (T ())
vx0)) E (T ())
vx1))
        pure (EApp l (EApp undefined (EApp undefined (Builtin undefined Zip) op') xs') ys')
optA (EApp T ()
l (EApp T ()
_ (EApp T ()
_ (Builtin T ()
_ Builtin
Zip) E (T ())
op) E (T ())
xs) (EApp T ()
_ (EApp T ()
_ (Builtin T ()
_ Builtin
Map) E (T ())
g) E (T ())
ys))
    | Arrow T ()
dom1 T ()
_ <- E (T ()) -> T ()
forall a. E a -> a
eAnn E (T ())
g
    , Arrow T ()
dom0 (Arrow T ()
_ T ()
cod) <- E (T ()) -> T ()
forall a. E a -> a
eAnn E (T ())
op = do
        g' <- E (T ()) -> RM (E (T ()))
optA E (T ())
g
        opA <- optA op
        xs' <- optA xs; ys' <- optA ys
        x0 <- nextU "x" dom0; x1 <- nextU "y" dom1
        let vx0 = T () -> Nm (T ()) -> E (T ())
forall a. a -> Nm a -> E a
Var T ()
dom0 Nm (T ())
x0; vx1 = T () -> Nm (T ()) -> E (T ())
forall a. a -> Nm a -> E a
Var T ()
dom1 Nm (T ())
x1
            opTy = T ()
dom0 T () -> T () -> T ()
forall {a}. T a -> T a -> T a
~> T ()
dom1 T () -> T () -> T ()
forall {a}. T a -> T a -> T a
~> T ()
cod
            op' = T () -> Nm (T ()) -> E (T ()) -> E (T ())
forall a. a -> Nm a -> E a -> E a
Lam T ()
opTy Nm (T ())
x0 (T () -> Nm (T ()) -> E (T ()) -> E (T ())
forall a. a -> Nm a -> E a -> E a
Lam T ()
forall a. HasCallStack => a
undefined Nm (T ())
x1 (T () -> E (T ()) -> E (T ()) -> E (T ())
forall a. a -> E a -> E a -> E a
EApp T ()
forall a. HasCallStack => a
undefined (T () -> E (T ()) -> E (T ()) -> E (T ())
forall a. a -> E a -> E a -> E a
EApp T ()
forall a. HasCallStack => a
undefined E (T ())
opA E (T ())
vx0) (T () -> E (T ()) -> E (T ()) -> E (T ())
forall a. a -> E a -> E a -> E a
EApp T ()
forall a. HasCallStack => a
undefined E (T ())
g' E (T ())
vx1)))
        pure (EApp l (EApp undefined (EApp undefined (Builtin undefined Zip) op') xs') ys')
optA (EApp T ()
l (EApp T ()
t0 (EApp T ()
t1 (Builtin T ()
bt b :: Builtin
b@Builtin
FoldS) E (T ())
op) E (T ())
seed) E (T ())
arr) = do
    arr' <- E (T ()) -> RM (E (T ()))
optA E (T ())
arr
    seed' <- optA seed
    opA <- optA op
    case arr' of
        (EApp T ()
_ (EApp T ()
_ (EApp T ()
_ (Builtin T ()
_ Builtin
Zip) E (T ())
f) E (T ())
xs) E (T ())
ys)
            | Arrow T ()
dom0 (Arrow T ()
dom1 T ()
dom2) <- E (T ()) -> T ()
forall a. E a -> a
eAnn E (T ())
f
            , Arrow T ()
_ (Arrow T ()
_ T ()
cod) <- E (T ()) -> T ()
forall a. E a -> a
eAnn E (T ())
op -> do
                f' <- E (T ()) -> RM (E (T ()))
optA E (T ())
f
                xs' <- optA xs
                ys' <- optA ys
                x0 <- nextU "x" cod; x1 <- nextU "y" dom0; x2 <- nextU "z" dom1
                let vx0 = T () -> Nm (T ()) -> E (T ())
forall a. a -> Nm a -> E a
Var T ()
cod Nm (T ())
x0; vx1 = T () -> Nm (T ()) -> E (T ())
forall a. a -> Nm a -> E a
Var T ()
dom0 Nm (T ())
x1; vx2 = T () -> Nm (T ()) -> E (T ())
forall a. a -> Nm a -> E a
Var T ()
dom1 Nm (T ())
x2
                    opTy = T ()
cod T () -> T () -> T ()
forall {a}. T a -> T a -> T a
~> T ()
dom0 T () -> T () -> T ()
forall {a}. T a -> T a -> T a
~> T ()
dom1 T () -> T () -> T ()
forall {a}. T a -> T a -> T a
~> T ()
cod
                    op' = T () -> Nm (T ()) -> E (T ()) -> E (T ())
forall a. a -> Nm a -> E a -> E a
Lam T ()
opTy Nm (T ())
x0 (T () -> Nm (T ()) -> E (T ()) -> E (T ())
forall a. a -> Nm a -> E a -> E a
Lam T ()
forall a. HasCallStack => a
undefined Nm (T ())
x1 (T () -> Nm (T ()) -> E (T ()) -> E (T ())
forall a. a -> Nm a -> E a -> E a
Lam (T ()
dom1 T () -> T () -> T ()
forall {a}. T a -> T a -> T a
~> T ()
cod) Nm (T ())
x2 (T () -> E (T ()) -> E (T ()) -> E (T ())
forall a. a -> E a -> E a -> E a
EApp T ()
cod (T () -> E (T ()) -> E (T ()) -> E (T ())
forall a. a -> E a -> E a -> E a
EApp T ()
forall a. HasCallStack => a
undefined E (T ())
opA E (T ())
vx0) (T () -> E (T ()) -> E (T ()) -> E (T ())
forall a. a -> E a -> E a -> E a
EApp T ()
dom2 (T () -> E (T ()) -> E (T ()) -> E (T ())
forall a. a -> E a -> E a -> E a
EApp T ()
forall a. HasCallStack => a
undefined E (T ())
f' E (T ())
vx1) E (T ())
vx2))))
                pure $ Id l $ FoldSOfZip seed' op' [xs',ys']
        E (T ())
_ -> E (T ()) -> RM (E (T ()))
forall a. a -> StateT Rs Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (T () -> E (T ()) -> E (T ()) -> E (T ())
forall a. a -> E a -> E a -> E a
EApp T ()
l (T () -> E (T ()) -> E (T ()) -> E (T ())
forall a. a -> E a -> E a -> E a
EApp T ()
t0 (T () -> E (T ()) -> E (T ()) -> E (T ())
forall a. a -> E a -> E a -> E a
EApp T ()
t1 (T () -> Builtin -> E (T ())
forall a. a -> Builtin -> E a
Builtin T ()
bt Builtin
b) E (T ())
opA) E (T ())
seed') E (T ())
arr')
optA (EApp T ()
t0 (EApp T ()
t1 (Builtin T ()
bt Builtin
Fold) E (T ())
op) E (T ())
arr) = do
    arr' <- E (T ()) -> RM (E (T ()))
optA E (T ())
arr
    opA <- optA op
    case arr' of
        (EApp T ()
_ (EApp T ()
_ (EApp T ()
_ (Builtin T ()
_ Builtin
Zip) E (T ())
f) E (T ())
xs) E (T ())
ys)
            | fTy :: T ()
fTy@(Arrow T ()
dom0 (Arrow T ()
dom1 T ()
dom2)) <- E (T ()) -> T ()
forall a. E a -> a
eAnn E (T ())
f
            , Arrow T ()
_ (Arrow T ()
_ T ()
cod) <- E (T ()) -> T ()
forall a. E a -> a
eAnn E (T ())
op -> do
                f' <- E (T ()) -> RM (E (T ()))
optA E (T ())
f; f'' <- rE f'
                xs' <- optA xs; ys' <- optA ys
                x0 <- nextU "x" cod; x1 <- nextU "y" dom0; x2 <- nextU "z" dom1
                x0' <- nextU "x" dom0; x1' <- nextU "y" dom1
                let vx0 = T () -> Nm (T ()) -> E (T ())
forall a. a -> Nm a -> E a
Var T ()
cod Nm (T ())
x0; vx1 = T () -> Nm (T ()) -> E (T ())
forall a. a -> Nm a -> E a
Var T ()
dom0 Nm (T ())
x1; vx2 = T () -> Nm (T ()) -> E (T ())
forall a. a -> Nm a -> E a
Var T ()
dom1 Nm (T ())
x2
                    vx0' = T () -> Nm (T ()) -> E (T ())
forall a. a -> Nm a -> E a
Var T ()
dom0 Nm (T ())
x0'; vx1' = T () -> Nm (T ()) -> E (T ())
forall a. a -> Nm a -> E a
Var T ()
dom1 Nm (T ())
x1'
                    opT = T ()
cod T () -> T () -> T ()
forall {a}. T a -> T a -> T a
~> T ()
dom0 T () -> T () -> T ()
forall {a}. T a -> T a -> T a
~> T ()
dom1 T () -> T () -> T ()
forall {a}. T a -> T a -> T a
~> T ()
cod
                    op' = T () -> Nm (T ()) -> E (T ()) -> E (T ())
forall a. a -> Nm a -> E a -> E a
Lam T ()
opT Nm (T ())
x0 (T () -> Nm (T ()) -> E (T ()) -> E (T ())
forall a. a -> Nm a -> E a -> E a
Lam T ()
forall a. HasCallStack => a
undefined Nm (T ())
x1 (T () -> Nm (T ()) -> E (T ()) -> E (T ())
forall a. a -> Nm a -> E a -> E a
Lam (T ()
dom1 T () -> T () -> T ()
forall {a}. T a -> T a -> T a
~> T ()
cod) Nm (T ())
x2 (T () -> E (T ()) -> E (T ()) -> E (T ())
forall a. a -> E a -> E a -> E a
EApp T ()
cod (T () -> E (T ()) -> E (T ()) -> E (T ())
forall a. a -> E a -> E a -> E a
EApp T ()
forall a. HasCallStack => a
undefined E (T ())
opA E (T ())
vx0) (T () -> E (T ()) -> E (T ()) -> E (T ())
forall a. a -> E a -> E a -> E a
EApp T ()
dom2 (T () -> E (T ()) -> E (T ()) -> E (T ())
forall a. a -> E a -> E a -> E a
EApp T ()
forall a. HasCallStack => a
undefined E (T ())
f' E (T ())
vx1) E (T ())
vx2))))
                    f''' = T () -> Nm (T ()) -> E (T ()) -> E (T ())
forall a. a -> Nm a -> E a -> E a
Lam T ()
fTy Nm (T ())
x0' (T () -> Nm (T ()) -> E (T ()) -> E (T ())
forall a. a -> Nm a -> E a -> E a
Lam T ()
forall a. HasCallStack => a
undefined Nm (T ())
x1' (T () -> E (T ()) -> E (T ()) -> E (T ())
forall a. a -> E a -> E a -> E a
EApp T ()
dom2 (T () -> E (T ()) -> E (T ()) -> E (T ())
forall a. a -> E a -> E a -> E a
EApp T ()
forall a. HasCallStack => a
undefined E (T ())
f'' E (T ())
vx0') E (T ())
vx1'))
                pure $ Id t0 $ FoldOfZip f''' op' [xs',ys']
        E (T ())
_ -> E (T ()) -> RM (E (T ()))
forall a. a -> StateT Rs Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (T () -> E (T ()) -> E (T ()) -> E (T ())
forall a. a -> E a -> E a -> E a
EApp T ()
t0 (T () -> E (T ()) -> E (T ()) -> E (T ())
forall a. a -> E a -> E a -> E a
EApp T ()
t1 (T () -> Builtin -> E (T ())
forall a. a -> Builtin -> E a
Builtin T ()
bt Builtin
Fold) E (T ())
opA) E (T ())
arr')
optA (EApp T ()
l E (T ())
e0 E (T ())
e1) = T () -> E (T ()) -> E (T ()) -> E (T ())
forall a. a -> E a -> E a -> E a
EApp T ()
l (E (T ()) -> E (T ()) -> E (T ()))
-> RM (E (T ())) -> StateT Rs Identity (E (T ()) -> E (T ()))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E (T ()) -> RM (E (T ()))
optA E (T ())
e0 StateT Rs Identity (E (T ()) -> E (T ()))
-> RM (E (T ())) -> RM (E (T ()))
forall a b.
StateT Rs Identity (a -> b)
-> StateT Rs Identity a -> StateT Rs Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> E (T ()) -> RM (E (T ()))
optA E (T ())
e1
optA (ALit T ()
l [E (T ())]
es) = do
    es' <- (E (T ()) -> RM (E (T ())))
-> [E (T ())] -> StateT Rs 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 ()))
optA [E (T ())]
es
    pure $ case unzip <$> traverse mShLit es' of
        Maybe ([[Int]], [[E (T ())]])
Nothing        -> T () -> Idiom -> E (T ())
forall a. a -> Idiom -> E a
Id T ()
l (Idiom -> E (T ())) -> Idiom -> E (T ())
forall a b. (a -> b) -> a -> b
$ [Int] -> [E (T ())] -> Idiom
AShLit [[E (T ())] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [E (T ())]
es] [E (T ())]
es'
        Just ([[Int]]
ds, [[E (T ())]]
esϵ) -> T () -> Idiom -> E (T ())
forall a. a -> Idiom -> E a
Id T ()
l (Idiom -> E (T ())) -> Idiom -> E (T ())
forall a b. (a -> b) -> a -> b
$ [Int] -> [E (T ())] -> Idiom
AShLit ([[Int]] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [[Int]]
ds Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
: [[Int]] -> [Int]
forall a. HasCallStack => [a] -> a
head [[Int]]
ds) ([[E (T ())]] -> [E (T ())]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[E (T ())]]
esϵ)
optA (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 Rs 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 Rs 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 ()))
optA [E (T ())]
es
optA (Let T ()
l (Nm (T ())
n, E (T ())
e') E (T ())
e) = do
    e'Opt <- E (T ()) -> RM (E (T ()))
optA E (T ())
e'
    eOpt <- optA e
    pure $ Let l (n, e'Opt) eOpt
optA (LLet T ()
l (Nm (T ())
n, E (T ())
e') E (T ())
e) = do
    e'Opt <- E (T ()) -> RM (E (T ()))
optA E (T ())
e'
    eOpt <- optA e
    pure $ LLet l (n, e'Opt) eOpt
optA (Id T ()
l Idiom
idm) = T () -> Idiom -> E (T ())
forall a. a -> Idiom -> E a
Id T ()
l (Idiom -> E (T ())) -> StateT Rs Identity Idiom -> RM (E (T ()))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Idiom -> StateT Rs Identity Idiom
optI Idiom
idm
optA (Cond T ()
l E (T ())
p E (T ())
e0 E (T ())
e1) = 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 Rs Identity (E (T ()) -> E (T ()) -> E (T ()))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E (T ()) -> RM (E (T ()))
optA E (T ())
p StateT Rs Identity (E (T ()) -> E (T ()) -> E (T ()))
-> RM (E (T ())) -> StateT Rs Identity (E (T ()) -> E (T ()))
forall a b.
StateT Rs Identity (a -> b)
-> StateT Rs Identity a -> StateT Rs Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> E (T ()) -> RM (E (T ()))
optA E (T ())
e0 StateT Rs Identity (E (T ()) -> E (T ()))
-> RM (E (T ())) -> RM (E (T ()))
forall a b.
StateT Rs Identity (a -> b)
-> StateT Rs Identity a -> StateT Rs Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> E (T ()) -> RM (E (T ()))
optA E (T ())
e1

optI :: Idiom -> StateT Rs Identity Idiom
optI (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 Rs Identity (E (T ()) -> [E (T ())] -> Idiom)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E (T ()) -> RM (E (T ()))
optA E (T ())
seed StateT Rs Identity (E (T ()) -> [E (T ())] -> Idiom)
-> RM (E (T ())) -> StateT Rs Identity ([E (T ())] -> Idiom)
forall a b.
StateT Rs Identity (a -> b)
-> StateT Rs Identity a -> StateT Rs Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> E (T ()) -> RM (E (T ()))
optA E (T ())
op StateT Rs Identity ([E (T ())] -> Idiom)
-> StateT Rs Identity [E (T ())] -> StateT Rs Identity Idiom
forall a b.
StateT Rs Identity (a -> b)
-> StateT Rs Identity a -> StateT Rs Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (E (T ()) -> RM (E (T ())))
-> [E (T ())] -> StateT Rs 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 ()))
optA [E (T ())]
es
optI (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 Rs Identity (E (T ()) -> [E (T ())] -> Idiom)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E (T ()) -> RM (E (T ()))
optA E (T ())
zop StateT Rs Identity (E (T ()) -> [E (T ())] -> Idiom)
-> RM (E (T ())) -> StateT Rs Identity ([E (T ())] -> Idiom)
forall a b.
StateT Rs Identity (a -> b)
-> StateT Rs Identity a -> StateT Rs Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> E (T ()) -> RM (E (T ()))
optA E (T ())
op StateT Rs Identity ([E (T ())] -> Idiom)
-> StateT Rs Identity [E (T ())] -> StateT Rs Identity Idiom
forall a b.
StateT Rs Identity (a -> b)
-> StateT Rs Identity a -> StateT Rs Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (E (T ()) -> RM (E (T ())))
-> [E (T ())] -> StateT Rs 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 ()))
optA [E (T ())]
es
optI (FoldGen E (T ())
seed E (T ())
f E (T ())
g 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 Rs 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 ()))
optA E (T ())
seed StateT Rs Identity (E (T ()) -> E (T ()) -> E (T ()) -> Idiom)
-> RM (E (T ()))
-> StateT Rs Identity (E (T ()) -> E (T ()) -> Idiom)
forall a b.
StateT Rs Identity (a -> b)
-> StateT Rs Identity a -> StateT Rs Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> E (T ()) -> RM (E (T ()))
optA E (T ())
f StateT Rs Identity (E (T ()) -> E (T ()) -> Idiom)
-> RM (E (T ())) -> StateT Rs Identity (E (T ()) -> Idiom)
forall a b.
StateT Rs Identity (a -> b)
-> StateT Rs Identity a -> StateT Rs Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> E (T ()) -> RM (E (T ()))
optA E (T ())
g StateT Rs Identity (E (T ()) -> Idiom)
-> RM (E (T ())) -> StateT Rs Identity Idiom
forall a b.
StateT Rs Identity (a -> b)
-> StateT Rs Identity a -> StateT Rs Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> E (T ()) -> RM (E (T ()))
optA E (T ())
n
optI (AShLit [Int]
ds [E (T ())]
es)          = [Int] -> [E (T ())] -> Idiom
AShLit [Int]
ds ([E (T ())] -> Idiom)
-> StateT Rs Identity [E (T ())] -> StateT Rs Identity Idiom
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (E (T ()) -> RM (E (T ())))
-> [E (T ())] -> StateT Rs 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 ()))
optA [E (T ())]
es