{-# LANGUAGE CPP
           , DataKinds
           , EmptyCase
           , ExistentialQuantification
           , FlexibleContexts
           , GADTs
           , GeneralizedNewtypeDeriving
           , KindSignatures
           , MultiParamTypeClasses
           , OverloadedStrings
           , PolyKinds
           , ScopedTypeVariables
           , TypeFamilies
           , TypeOperators
           #-}


{-# OPTIONS_GHC -Wall -fwarn-tabs #-}
----------------------------------------------------------------
--                                                    2017.02.01
-- |
-- Module      :  Language.Hakaru.Syntax.CSE
-- Copyright   :  Copyright (c) 2016 the Hakaru team
-- License     :  BSD3
-- Maintainer  :
-- Stability   :  experimental
-- Portability :  GHC-only
--
--
----------------------------------------------------------------
module Language.Hakaru.Syntax.CSE (cse) where

import           Control.Monad.Reader

import           Language.Hakaru.Syntax.ABT
import           Language.Hakaru.Syntax.AST
import           Language.Hakaru.Syntax.AST.Eq
import           Language.Hakaru.Syntax.IClasses
import           Language.Hakaru.Syntax.TypeOf
import           Language.Hakaru.Types.DataKind

#if __GLASGOW_HASKELL__ < 710
import           Control.Applicative
#endif

-- What we need is an environment like data structure which maps Terms (or
-- general abts?) to other abts. Can such a mapping be implemented efficiently?
-- This would seem to require a hash operation to make efficient.

data EAssoc (abt :: [Hakaru] -> Hakaru -> *)
  = forall a . EAssoc !(abt '[] a) !(abt '[] a)

-- An association list for now
newtype Env (abt :: [Hakaru] -> Hakaru -> *) = Env [EAssoc abt]

emptyEnv :: Env a
emptyEnv :: Env a
emptyEnv = [EAssoc a] -> Env a
forall (abt :: [Hakaru] -> Hakaru -> *). [EAssoc abt] -> Env abt
Env []

trivial :: (ABT Term abt) => abt '[] a -> Bool
trivial :: abt '[] a -> Bool
trivial abt '[] a
abt = case abt '[] a -> View (Term abt) '[] a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> View (syn abt) xs a
viewABT abt '[] a
abt of
                Var Variable a
_            -> Bool
True
                Syn (Literal_ _) -> Bool
True
                View (Term abt) '[] a
_                -> Bool
False

-- Attempt to find a new expression in the environment. The lookup is chained
-- to iteratively perform lookup until no match is found, resulting in an
-- equivalence-relation in the environment. This could be made faster with path
-- compression and a more efficient lookup structure.
-- NB: This code could potentially produce an infinite loop depending on how
-- terms are added to the environment. How do we want to prevent this?
lookupEnv
  :: forall abt a . (ABT Term abt)
  => abt '[] a
  -> Env abt
  -> abt '[] a
lookupEnv :: abt '[] a -> Env abt -> abt '[] a
lookupEnv abt '[] a
start (Env [EAssoc abt]
env) = abt '[] a -> [EAssoc abt] -> abt '[] a
go abt '[] a
start [EAssoc abt]
env
  where
    go :: abt '[] a -> [EAssoc abt] -> abt '[] a
    go :: abt '[] a -> [EAssoc abt] -> abt '[] a
go abt '[] a
ast []                = abt '[] a
ast
    go abt '[] a
ast (EAssoc abt '[] a
a abt '[] a
b : [EAssoc abt]
xs) =
      case Sing a -> Sing a -> Maybe (TypeEq a a)
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 (abt '[] a -> Sing a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> Sing a
typeOf abt '[] a
ast) (abt '[] a -> Sing a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> Sing a
typeOf abt '[] a
a) of
        Just TypeEq a a
Refl | abt '[] a -> abt '[] a -> Bool
forall (abt :: [Hakaru] -> Hakaru -> *) (d :: Hakaru).
ABT Term abt =>
abt '[] d -> abt '[] d -> Bool
alphaEq abt '[] a
ast abt '[] a
abt '[] a
a -> abt '[] a -> [EAssoc abt] -> abt '[] a
go abt '[] a
abt '[] a
b [EAssoc abt]
env
        Maybe (TypeEq a a)
_         -> abt '[] a -> [EAssoc abt] -> abt '[] a
go abt '[] a
ast [EAssoc abt]
xs

insertEnv
  :: forall abt a . (ABT Term abt)
  => abt '[] a
  -> abt '[] a
  -> Env abt
  -> Env abt
insertEnv :: abt '[] a -> abt '[] a -> Env abt -> Env abt
insertEnv abt '[] a
ast1 abt '[] a
ast2 (Env [EAssoc abt]
env)
  -- Point new variables to the older ones, this does not affect the amount of
  -- work done, since ast2 is always a variable. This allows the pass to
  -- eliminate redundant variables, as we only eliminate binders during CSE.
  | abt '[] a -> Bool
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> Bool
trivial abt '[] a
ast1 = [EAssoc abt] -> Env abt
forall (abt :: [Hakaru] -> Hakaru -> *). [EAssoc abt] -> Env abt
Env (abt '[] a -> abt '[] a -> EAssoc abt
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
abt '[] a -> abt '[] a -> EAssoc abt
EAssoc abt '[] a
ast2 abt '[] a
ast1 EAssoc abt -> [EAssoc abt] -> [EAssoc abt]
forall a. a -> [a] -> [a]
: [EAssoc abt]
env)
  -- Otherwise map expressions to their binding variables
  | Bool
otherwise    = [EAssoc abt] -> Env abt
forall (abt :: [Hakaru] -> Hakaru -> *). [EAssoc abt] -> Env abt
Env (abt '[] a -> abt '[] a -> EAssoc abt
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
abt '[] a -> abt '[] a -> EAssoc abt
EAssoc abt '[] a
ast1 abt '[] a
ast2 EAssoc abt -> [EAssoc abt] -> [EAssoc abt]
forall a. a -> [a] -> [a]
: [EAssoc abt]
env)

newtype CSE (abt :: [Hakaru] -> Hakaru -> *) a = CSE { CSE abt a -> Reader (Env abt) a
runCSE :: Reader (Env abt) a }
  deriving (a -> CSE abt b -> CSE abt a
(a -> b) -> CSE abt a -> CSE abt b
(forall a b. (a -> b) -> CSE abt a -> CSE abt b)
-> (forall a b. a -> CSE abt b -> CSE abt a) -> Functor (CSE abt)
forall a b. a -> CSE abt b -> CSE abt a
forall a b. (a -> b) -> CSE abt a -> CSE abt b
forall (abt :: [Hakaru] -> Hakaru -> *) a b.
a -> CSE abt b -> CSE abt a
forall (abt :: [Hakaru] -> Hakaru -> *) a b.
(a -> b) -> CSE abt a -> CSE abt b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> CSE abt b -> CSE abt a
$c<$ :: forall (abt :: [Hakaru] -> Hakaru -> *) a b.
a -> CSE abt b -> CSE abt a
fmap :: (a -> b) -> CSE abt a -> CSE abt b
$cfmap :: forall (abt :: [Hakaru] -> Hakaru -> *) a b.
(a -> b) -> CSE abt a -> CSE abt b
Functor, Functor (CSE abt)
a -> CSE abt a
Functor (CSE abt)
-> (forall a. a -> CSE abt a)
-> (forall a b. CSE abt (a -> b) -> CSE abt a -> CSE abt b)
-> (forall a b c.
    (a -> b -> c) -> CSE abt a -> CSE abt b -> CSE abt c)
-> (forall a b. CSE abt a -> CSE abt b -> CSE abt b)
-> (forall a b. CSE abt a -> CSE abt b -> CSE abt a)
-> Applicative (CSE abt)
CSE abt a -> CSE abt b -> CSE abt b
CSE abt a -> CSE abt b -> CSE abt a
CSE abt (a -> b) -> CSE abt a -> CSE abt b
(a -> b -> c) -> CSE abt a -> CSE abt b -> CSE abt c
forall a. a -> CSE abt a
forall a b. CSE abt a -> CSE abt b -> CSE abt a
forall a b. CSE abt a -> CSE abt b -> CSE abt b
forall a b. CSE abt (a -> b) -> CSE abt a -> CSE abt b
forall a b c. (a -> b -> c) -> CSE abt a -> CSE abt b -> CSE abt c
forall (abt :: [Hakaru] -> Hakaru -> *). Functor (CSE abt)
forall (abt :: [Hakaru] -> Hakaru -> *) a. a -> CSE abt a
forall (abt :: [Hakaru] -> Hakaru -> *) a b.
CSE abt a -> CSE abt b -> CSE abt a
forall (abt :: [Hakaru] -> Hakaru -> *) a b.
CSE abt a -> CSE abt b -> CSE abt b
forall (abt :: [Hakaru] -> Hakaru -> *) a b.
CSE abt (a -> b) -> CSE abt a -> CSE abt b
forall (abt :: [Hakaru] -> Hakaru -> *) a b c.
(a -> b -> c) -> CSE abt a -> CSE abt b -> CSE abt c
forall (f :: * -> *).
Functor f
-> (forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
<* :: CSE abt a -> CSE abt b -> CSE abt a
$c<* :: forall (abt :: [Hakaru] -> Hakaru -> *) a b.
CSE abt a -> CSE abt b -> CSE abt a
*> :: CSE abt a -> CSE abt b -> CSE abt b
$c*> :: forall (abt :: [Hakaru] -> Hakaru -> *) a b.
CSE abt a -> CSE abt b -> CSE abt b
liftA2 :: (a -> b -> c) -> CSE abt a -> CSE abt b -> CSE abt c
$cliftA2 :: forall (abt :: [Hakaru] -> Hakaru -> *) a b c.
(a -> b -> c) -> CSE abt a -> CSE abt b -> CSE abt c
<*> :: CSE abt (a -> b) -> CSE abt a -> CSE abt b
$c<*> :: forall (abt :: [Hakaru] -> Hakaru -> *) a b.
CSE abt (a -> b) -> CSE abt a -> CSE abt b
pure :: a -> CSE abt a
$cpure :: forall (abt :: [Hakaru] -> Hakaru -> *) a. a -> CSE abt a
$cp1Applicative :: forall (abt :: [Hakaru] -> Hakaru -> *). Functor (CSE abt)
Applicative, Applicative (CSE abt)
a -> CSE abt a
Applicative (CSE abt)
-> (forall a b. CSE abt a -> (a -> CSE abt b) -> CSE abt b)
-> (forall a b. CSE abt a -> CSE abt b -> CSE abt b)
-> (forall a. a -> CSE abt a)
-> Monad (CSE abt)
CSE abt a -> (a -> CSE abt b) -> CSE abt b
CSE abt a -> CSE abt b -> CSE abt b
forall a. a -> CSE abt a
forall a b. CSE abt a -> CSE abt b -> CSE abt b
forall a b. CSE abt a -> (a -> CSE abt b) -> CSE abt b
forall (abt :: [Hakaru] -> Hakaru -> *). Applicative (CSE abt)
forall (abt :: [Hakaru] -> Hakaru -> *) a. a -> CSE abt a
forall (abt :: [Hakaru] -> Hakaru -> *) a b.
CSE abt a -> CSE abt b -> CSE abt b
forall (abt :: [Hakaru] -> Hakaru -> *) a b.
CSE abt a -> (a -> CSE abt b) -> CSE abt b
forall (m :: * -> *).
Applicative m
-> (forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
return :: a -> CSE abt a
$creturn :: forall (abt :: [Hakaru] -> Hakaru -> *) a. a -> CSE abt a
>> :: CSE abt a -> CSE abt b -> CSE abt b
$c>> :: forall (abt :: [Hakaru] -> Hakaru -> *) a b.
CSE abt a -> CSE abt b -> CSE abt b
>>= :: CSE abt a -> (a -> CSE abt b) -> CSE abt b
$c>>= :: forall (abt :: [Hakaru] -> Hakaru -> *) a b.
CSE abt a -> (a -> CSE abt b) -> CSE abt b
$cp1Monad :: forall (abt :: [Hakaru] -> Hakaru -> *). Applicative (CSE abt)
Monad, MonadReader (Env abt))

replaceCSE
  :: (ABT Term abt)
  => abt '[] a
  -> CSE abt (abt '[] a)
replaceCSE :: abt '[] a -> CSE abt (abt '[] a)
replaceCSE abt '[] a
abt = abt '[] a -> Env abt -> abt '[] a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> Env abt -> abt '[] a
lookupEnv abt '[] a
abt (Env abt -> abt '[] a) -> CSE abt (Env abt) -> CSE abt (abt '[] a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` CSE abt (Env abt)
forall r (m :: * -> *). MonadReader r m => m r
ask

cse :: forall abt a . (ABT Term abt) => abt '[] a -> abt '[] a
cse :: abt '[] a -> abt '[] a
cse abt '[] a
abt = Reader (Env abt) (abt '[] a) -> Env abt -> abt '[] a
forall r a. Reader r a -> r -> a
runReader (CSE abt (abt '[] a) -> Reader (Env abt) (abt '[] a)
forall (abt :: [Hakaru] -> Hakaru -> *) a.
CSE abt a -> Reader (Env abt) a
runCSE (abt '[] a -> CSE abt (abt '[] a)
forall (abt :: [Hakaru] -> Hakaru -> *) (xs :: [Hakaru])
       (a :: Hakaru).
ABT Term abt =>
abt xs a -> CSE abt (abt xs a)
cse' abt '[] a
abt)) Env abt
forall (a :: [Hakaru] -> Hakaru -> *). Env a
emptyEnv

cse' :: forall abt xs a . (ABT Term abt) => abt xs a -> CSE abt (abt xs a)
cse' :: abt xs a -> CSE abt (abt xs a)
cse' = View (Term abt) xs a -> CSE abt (abt xs a)
forall (ys :: [Hakaru]). View (Term abt) ys a -> CSE abt (abt ys a)
loop (View (Term abt) xs a -> CSE abt (abt xs a))
-> (abt xs a -> View (Term abt) xs a)
-> abt xs a
-> CSE abt (abt xs a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. abt xs a -> View (Term abt) xs a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> View (syn abt) xs a
viewABT
  where
    loop :: View (Term abt) ys a ->  CSE abt (abt ys a)
    loop :: View (Term abt) ys a -> CSE abt (abt ys a)
loop (Var Variable a
v)    = Variable a -> CSE abt (abt '[] a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Variable a -> CSE abt (abt '[] a)
cseVar Variable a
v
    loop (Syn Term abt a
s)    = Term abt a -> CSE abt (abt '[] a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Term abt a -> CSE abt (abt '[] a)
cseTerm Term abt a
s
    loop (Bind Variable a
v View (Term abt) xs a
b) = (abt xs a -> abt (a : xs) a)
-> CSE abt (abt xs a) -> CSE abt (abt (a : xs) a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Variable a -> abt xs a -> abt (a : xs) a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k) (xs :: [k]) (b :: k).
ABT syn abt =>
Variable a -> abt xs b -> abt (a : xs) b
bind Variable a
v) (View (Term abt) xs a -> CSE abt (abt xs a)
forall (ys :: [Hakaru]). View (Term abt) ys a -> CSE abt (abt ys a)
loop View (Term abt) xs a
b)

-- Variables can be equivalent to other variables
-- TODO: A good sanity check would be to ensure the result in this case is
-- always a variable or constant. A variable should never be substituted for
-- a more complex expression.
cseVar
  :: (ABT Term abt)
  => Variable a
  -> CSE abt (abt '[] a)
cseVar :: Variable a -> CSE abt (abt '[] a)
cseVar = abt '[] a -> CSE abt (abt '[] a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> CSE abt (abt '[] a)
replaceCSE  (abt '[] a -> CSE abt (abt '[] a))
-> (Variable a -> abt '[] a) -> Variable a -> CSE abt (abt '[] a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Variable a -> abt '[] a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k).
ABT syn abt =>
Variable a -> abt '[] a
var

mklet :: ABT Term abt => Variable b -> abt '[] b -> abt '[] a -> abt '[] a
mklet :: Variable b -> abt '[] b -> abt '[] a -> abt '[] a
mklet Variable b
v abt '[] b
rhs abt '[] a
body = Term abt a -> abt '[] a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn (SCon '[LC b, '( '[b], a)] a
forall (a :: Hakaru) (b :: Hakaru). SCon '[LC a, '( '[a], b)] b
Let_ SCon '[LC b, '( '[b], a)] a
-> SArgs abt '[LC b, '( '[b], a)] -> Term abt a
forall (args :: [([Hakaru], Hakaru)]) (a :: Hakaru)
       (abt :: [Hakaru] -> Hakaru -> *).
SCon args a -> SArgs abt args -> Term abt a
:$ abt '[] b
rhs abt '[] b
-> SArgs abt '[ '( '[b], a)] -> SArgs abt '[LC b, '( '[b], a)]
forall (abt :: [Hakaru] -> Hakaru -> *) (vars :: [Hakaru])
       (a :: Hakaru) (args :: [([Hakaru], Hakaru)]).
abt vars a -> SArgs abt args -> SArgs abt ('(vars, a) : args)
:* Variable b -> abt '[] a -> abt '[b] a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k) (xs :: [k]) (b :: k).
ABT syn abt =>
Variable a -> abt xs b -> abt (a : xs) b
bind Variable b
v abt '[] a
body abt '[b] a -> SArgs abt '[] -> SArgs abt '[ '( '[b], a)]
forall (abt :: [Hakaru] -> Hakaru -> *) (vars :: [Hakaru])
       (a :: Hakaru) (args :: [([Hakaru], Hakaru)]).
abt vars a -> SArgs abt args -> SArgs abt ('(vars, a) : args)
:* SArgs abt '[]
forall (abt :: [Hakaru] -> Hakaru -> *). SArgs abt '[]
End)

-- Thanks to A-normalization, the only case we need to care about is let bindings.
-- Everything else is just structural recursion.
cseTerm
  :: (ABT Term abt)
  => Term abt a
  -> CSE abt (abt '[] a)

cseTerm :: Term abt a -> CSE abt (abt '[] a)
cseTerm (SCon args a
Let_ :$ abt vars a
rhs :* abt vars a
body :* SArgs abt args
End) = do
  abt vars a
rhs' <- abt vars a -> CSE abt (abt vars a)
forall (abt :: [Hakaru] -> Hakaru -> *) (xs :: [Hakaru])
       (a :: Hakaru).
ABT Term abt =>
abt xs a -> CSE abt (abt xs a)
cse' abt vars a
rhs
  abt '[a] a
-> (Variable a -> abt '[] a -> CSE abt (abt '[] a))
-> CSE abt (abt '[] a)
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (x :: k) (xs :: [k]) (a :: k) r.
ABT syn abt =>
abt (x : xs) a -> (Variable x -> abt xs a -> r) -> r
caseBind abt vars a
abt '[a] a
body ((Variable a -> abt '[] a -> CSE abt (abt '[] a))
 -> CSE abt (abt '[] a))
-> (Variable a -> abt '[] a -> CSE abt (abt '[] a))
-> CSE abt (abt '[] a)
forall a b. (a -> b) -> a -> b
$ \Variable a
v abt '[] a
body' ->
    (Env abt -> Env abt) -> CSE abt (abt '[] a) -> CSE abt (abt '[] a)
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (abt '[] a -> abt '[] a -> Env abt -> Env abt
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> abt '[] a -> Env abt -> Env abt
insertEnv abt vars a
abt '[] a
rhs' (Variable a -> abt '[] a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k).
ABT syn abt =>
Variable a -> abt '[] a
var Variable a
v)) (CSE abt (abt '[] a) -> CSE abt (abt '[] a))
-> CSE abt (abt '[] a) -> CSE abt (abt '[] a)
forall a b. (a -> b) -> a -> b
$
      if abt '[] a -> Bool
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> Bool
trivial abt vars a
abt '[] a
rhs'
      then abt '[] a -> CSE abt (abt '[] a)
forall (abt :: [Hakaru] -> Hakaru -> *) (xs :: [Hakaru])
       (a :: Hakaru).
ABT Term abt =>
abt xs a -> CSE abt (abt xs a)
cse' abt '[] a
body'
      else (abt '[] a -> abt '[] a)
-> CSE abt (abt '[] a) -> CSE abt (abt '[] a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Variable a -> abt '[] a -> abt '[] a -> abt '[] a
forall (abt :: [Hakaru] -> Hakaru -> *) (b :: Hakaru)
       (a :: Hakaru).
ABT Term abt =>
Variable b -> abt '[] b -> abt '[] a -> abt '[] a
mklet Variable a
v abt vars a
abt '[] a
rhs') (abt '[] a -> CSE abt (abt '[] a)
forall (abt :: [Hakaru] -> Hakaru -> *) (xs :: [Hakaru])
       (a :: Hakaru).
ABT Term abt =>
abt xs a -> CSE abt (abt xs a)
cse' abt '[] a
body')

cseTerm Term abt a
term = (forall (h :: [Hakaru]) (i :: Hakaru).
 abt h i -> CSE abt (abt h i))
-> Term abt a -> CSE abt (Term abt a)
forall k1 k2 k3 (t :: (k1 -> k2 -> *) -> k3 -> *) (f :: * -> *)
       (a :: k1 -> k2 -> *) (b :: k1 -> k2 -> *) (j :: k3).
(Traversable21 t, Applicative f) =>
(forall (h :: k1) (i :: k2). a h i -> f (b h i))
-> t a j -> f (t b j)
traverse21 forall (h :: [Hakaru]) (i :: Hakaru). abt h i -> CSE abt (abt h i)
forall (abt :: [Hakaru] -> Hakaru -> *) (xs :: [Hakaru])
       (a :: Hakaru).
ABT Term abt =>
abt xs a -> CSE abt (abt xs a)
cse' Term abt a
term CSE abt (Term abt a)
-> (Term abt a -> CSE abt (abt '[] a)) -> CSE abt (abt '[] a)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= abt '[] a -> CSE abt (abt '[] a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> CSE abt (abt '[] a)
replaceCSE (abt '[] a -> CSE abt (abt '[] a))
-> (Term abt a -> abt '[] a) -> Term abt a -> CSE abt (abt '[] a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term abt a -> abt '[] a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn