{-# LANGUAGE OverloadedStrings #-}

module R ( rE, rP
         , Renames (..)
         , HasRenames (..)
         ) where

import           A
import           C
import           Control.Monad.State.Strict (MonadState, State, runState)
import           Data.Bifunctor             (second)
import qualified Data.IntMap                as IM
import qualified Data.Text                  as T
import           Lens.Micro                 (Lens', over)
import           Lens.Micro.Mtl             (use, (%=), (.=))
import           Nm
import           U

data Renames = Rs { Renames -> Int
max_ :: Int, Renames -> IntMap Int
bound :: IM.IntMap Int }

class HasRenames a where
    rename :: Lens' a Renames

instance HasRenames Renames where rename :: Lens' Renames Renames
rename=(Renames -> f Renames) -> Renames -> f Renames
forall a. a -> a
id

boundLens :: Lens' Renames (IM.IntMap Int)
boundLens :: Lens' Renames (IntMap Int)
boundLens IntMap Int -> f (IntMap Int)
f Renames
s = (IntMap Int -> Renames) -> f (IntMap Int) -> f Renames
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\IntMap Int
x -> Renames
s { bound = x }) (IntMap Int -> f (IntMap Int)
f (Renames -> IntMap Int
bound Renames
s))

maxLens :: Lens' Renames Int
maxLens :: Lens' Renames Int
maxLens Int -> f Int
f Renames
s = (Int -> Renames) -> f Int -> f Renames
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\Int
x -> Renames
s { max_ = x }) (Int -> f Int
f (Renames -> Int
max_ Renames
s))

type RenameM = State Renames

rP :: Int -> Program a -> (Program a, Int)
rP :: forall a. Int -> Program a -> (Program a, Int)
rP Int
i = Int -> RenameM (Program a) -> (Program a, Int)
forall x. Int -> RenameM x -> (x, Int)
runRM Int
i(RenameM (Program a) -> (Program a, Int))
-> (Program a -> RenameM (Program a))
-> Program a
-> (Program a, Int)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Program a -> RenameM (Program a)
forall a. Program a -> RenameM (Program a)
renameProgram

runRM :: Int -> RenameM x -> (x, Int)
runRM :: forall x. Int -> RenameM x -> (x, Int)
runRM Int
i RenameM x
act = (Renames -> Int) -> (x, Renames) -> (x, Int)
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second Renames -> Int
max_ (RenameM x -> Renames -> (x, Renames)
forall s a. State s a -> s -> (a, s)
runState RenameM x
act (Int -> IntMap Int -> Renames
Rs Int
i IntMap Int
forall a. IntMap a
IM.empty))

replaceUnique :: (MonadState s m, HasRenames s) => U -> m U
replaceUnique :: forall s (m :: * -> *). (MonadState s m, HasRenames s) => U -> m U
replaceUnique u :: U
u@(U Int
i) = do
    rSt <- Getting (IntMap Int) s (IntMap Int) -> m (IntMap Int)
forall s (m :: * -> *) a. MonadState s m => Getting a s a -> m a
use ((Renames -> Const (IntMap Int) Renames)
-> s -> Const (IntMap Int) s
forall a. HasRenames a => Lens' a Renames
Lens' s Renames
rename((Renames -> Const (IntMap Int) Renames)
 -> s -> Const (IntMap Int) s)
-> ((IntMap Int -> Const (IntMap Int) (IntMap Int))
    -> Renames -> Const (IntMap Int) Renames)
-> Getting (IntMap Int) s (IntMap Int)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(IntMap Int -> Const (IntMap Int) (IntMap Int))
-> Renames -> Const (IntMap Int) Renames
Lens' Renames (IntMap Int)
boundLens)
    case IM.lookup i rSt of
        Maybe Int
Nothing -> U -> m U
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure U
u
        Just Int
j  -> (Renames -> Renames) -> m U -> m U
forall s (m :: * -> *) a.
(HasRenames s, MonadState s m) =>
(Renames -> Renames) -> m a -> m a
withRenames (ASetter Renames Renames (IntMap Int) (IntMap Int)
-> (IntMap Int -> IntMap Int) -> Renames -> Renames
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
over ASetter Renames Renames (IntMap Int) (IntMap Int)
Lens' Renames (IntMap Int)
boundLens (Int -> IntMap Int -> IntMap Int
forall a. Int -> IntMap a -> IntMap a
IM.delete Int
i)) (m U -> m U) -> m U -> m U
forall a b. (a -> b) -> a -> b
$ U -> m U
forall s (m :: * -> *). (MonadState s m, HasRenames s) => U -> m U
replaceUnique (Int -> U
U Int
j)

replaceVar :: (MonadState s m, HasRenames s) => Nm a -> m (Nm a)
replaceVar :: forall s (m :: * -> *) a.
(MonadState s m, HasRenames s) =>
Nm a -> m (Nm a)
replaceVar (Nm Text
n U
u a
l) = do
    u' <- U -> m U
forall s (m :: * -> *). (MonadState s m, HasRenames s) => U -> m U
replaceUnique U
u
    pure $ Nm n u' l

dummyName :: (MonadState s m, HasRenames s) => a -> T.Text -> m (Nm a)
dummyName :: forall s (m :: * -> *) a.
(MonadState s m, HasRenames s) =>
a -> Text -> m (Nm a)
dummyName a
l Text
n = do
    (Renames -> Identity Renames) -> s -> Identity s
forall a. HasRenames a => Lens' a Renames
Lens' s Renames
rename((Renames -> Identity Renames) -> s -> Identity s)
-> ((Int -> Identity Int) -> Renames -> Identity Renames)
-> (Int -> Identity Int)
-> s
-> Identity s
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(Int -> Identity Int) -> Renames -> Identity Renames
Lens' Renames Int
maxLens ((Int -> Identity Int) -> s -> Identity s) -> (Int -> Int) -> m ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= (Int -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1)
    st <- Getting Int s Int -> m Int
forall s (m :: * -> *) a. MonadState s m => Getting a s a -> m a
use ((Renames -> Const Int Renames) -> s -> Const Int s
forall a. HasRenames a => Lens' a Renames
Lens' s Renames
rename((Renames -> Const Int Renames) -> s -> Const Int s)
-> ((Int -> Const Int Int) -> Renames -> Const Int Renames)
-> Getting Int s Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(Int -> Const Int Int) -> Renames -> Const Int Renames
Lens' Renames Int
maxLens)
    pure $ Nm n (U st) l

doLocal :: (HasRenames s, MonadState s m) => m a -> m a
doLocal :: forall s (m :: * -> *) a.
(HasRenames s, MonadState s m) =>
m a -> m a
doLocal m a
act = do
    preB <- Getting (IntMap Int) s (IntMap Int) -> m (IntMap Int)
forall s (m :: * -> *) a. MonadState s m => Getting a s a -> m a
use ((Renames -> Const (IntMap Int) Renames)
-> s -> Const (IntMap Int) s
forall a. HasRenames a => Lens' a Renames
Lens' s Renames
rename((Renames -> Const (IntMap Int) Renames)
 -> s -> Const (IntMap Int) s)
-> ((IntMap Int -> Const (IntMap Int) (IntMap Int))
    -> Renames -> Const (IntMap Int) Renames)
-> Getting (IntMap Int) s (IntMap Int)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(IntMap Int -> Const (IntMap Int) (IntMap Int))
-> Renames -> Const (IntMap Int) Renames
Lens' Renames (IntMap Int)
boundLens)
    act <* (rename.boundLens .= preB)

freshen :: (HasRenames s, MonadState s m) => Nm a -> m (Nm a)
freshen :: forall s (m :: * -> *) a.
(HasRenames s, MonadState s m) =>
Nm a -> m (Nm a)
freshen (Nm Text
n (U Int
i) a
l) = do
    (Renames -> Identity Renames) -> s -> Identity s
forall a. HasRenames a => Lens' a Renames
Lens' s Renames
rename((Renames -> Identity Renames) -> s -> Identity s)
-> ((Int -> Identity Int) -> Renames -> Identity Renames)
-> (Int -> Identity Int)
-> s
-> Identity s
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(Int -> Identity Int) -> Renames -> Identity Renames
Lens' Renames Int
maxLens ((Int -> Identity Int) -> s -> Identity s) -> (Int -> Int) -> m ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= (Int -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1)
    nU <- Getting Int s Int -> m Int
forall s (m :: * -> *) a. MonadState s m => Getting a s a -> m a
use ((Renames -> Const Int Renames) -> s -> Const Int s
forall a. HasRenames a => Lens' a Renames
Lens' s Renames
rename((Renames -> Const Int Renames) -> s -> Const Int s)
-> ((Int -> Const Int Int) -> Renames -> Const Int Renames)
-> Getting Int s Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(Int -> Const Int Int) -> Renames -> Const Int Renames
Lens' Renames Int
maxLens)
    rename.boundLens %= IM.insert i nU
    pure (Nm n (U nU) l)

withRenames :: (HasRenames s, MonadState s m) => (Renames -> Renames) -> m a -> m a
withRenames :: forall s (m :: * -> *) a.
(HasRenames s, MonadState s m) =>
(Renames -> Renames) -> m a -> m a
withRenames Renames -> Renames
modSt m a
act = do
    preSt <- Getting Renames s Renames -> m Renames
forall s (m :: * -> *) a. MonadState s m => Getting a s a -> m a
use Getting Renames s Renames
forall a. HasRenames a => Lens' a Renames
Lens' s Renames
rename
    rename %= modSt
    res <- act
    postMax <- use (rename.maxLens)
    rename .= setMax postMax preSt
    pure res

setMax :: Int -> Renames -> Renames
setMax :: Int -> Renames -> Renames
setMax Int
i (Rs Int
_ IntMap Int
b) = Int -> IntMap Int -> Renames
Rs Int
i IntMap Int
b

-- | Desguar top-level functions as lambdas
mkLam :: [Nm a] -> E a -> E a
mkLam :: forall a. [Nm a] -> E a -> E a
mkLam [Nm a]
ns E a
e = (Nm a -> E a -> E a) -> E a -> [Nm a] -> E a
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\Nm a
n -> a -> Nm a -> E a -> E a
forall a. a -> Nm a -> E a -> E a
Lam (Nm a -> a
forall a. Nm a -> a
loc Nm a
n) Nm a
n) E a
e [Nm a]
ns

hasY :: E a -> Bool
hasY :: forall a. E a -> Bool
hasY = E a -> Bool
forall a. E a -> Bool
g where
    g :: E a -> Bool
g (ResVar a
_ DfnVar
Y)           = Bool
True
    g (Tup a
_ [E a]
es)             = (E a -> Bool) -> [E a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any E a -> Bool
g [E a]
es
    g (Rec a
_ [(Nm a, E a)]
es)             = ((Nm a, E a) -> Bool) -> [(Nm a, E a)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (E a -> Bool
g(E a -> Bool) -> ((Nm a, E a) -> E a) -> (Nm a, E a) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(Nm a, E a) -> E a
forall a b. (a, b) -> b
snd) [(Nm a, E a)]
es
    g (OptionVal a
_ (Just E a
e)) = E a -> Bool
g E a
e
    g (EApp a
_ E a
e0 E a
e1)         = E a -> Bool
g E a
e0 Bool -> Bool -> Bool
|| E a -> Bool
g E a
e1
    g Dfn{}                  = [Char] -> Bool
forall a. HasCallStack => [Char] -> a
error [Char]
"nested dfns not yet implemented"
    g (Let a
_ (Nm a
_, E a
be) E a
e)      = E a -> Bool
g E a
e Bool -> Bool -> Bool
|| E a -> Bool
g E a
be
    g (Lam a
_ Nm a
_ E a
e)            = E a -> Bool
g E a
e
    g (Paren a
_ E a
e)            = E a -> Bool
g E a
e
    g (Guarded a
_ E a
p E a
e)        = E a -> Bool
g E a
p Bool -> Bool -> Bool
|| E a -> Bool
g E a
e
    g (Implicit a
_ E a
e)         = E a -> Bool
g E a
e
    g (Arr a
_ Vector (E a)
es)             = (E a -> Bool) -> Vector (E a) -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any E a -> Bool
g Vector (E a)
es
    g (Anchor a
_ [E a]
es)          = (E a -> Bool) -> [E a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any E a -> Bool
g [E a]
es
    g (Cond a
_ E a
p E a
e0 E a
e1)       = E a -> Bool
g E a
e0 Bool -> Bool -> Bool
|| E a -> Bool
g E a
e1 Bool -> Bool -> Bool
|| E a -> Bool
g E a
p
    g E a
_                      = Bool
False

replaceXY :: (a -> Nm a) -- ^ @x@
          -> (a -> Nm a) -- ^ @y@
          -> E a
          -> E a
replaceXY :: forall a. (a -> Nm a) -> (a -> Nm a) -> E a -> E a
replaceXY a -> Nm a
nX a -> Nm a
nY = E a -> E a
r where
    r :: E a -> E a
r (ResVar a
l DfnVar
Y)      = a -> Nm a -> E a
forall a. a -> Nm a -> E a
Var a
l (a -> Nm a
nY a
l)
    r (ResVar a
l DfnVar
X)      = a -> Nm a -> E a
forall a. a -> Nm a -> E a
Var a
l (a -> Nm a
nX a
l)
    r e :: E a
e@Lit{}           = E a
e
    r e :: E a
e@RegexLit{}      = E a
e
    r e :: E a
e@RC{}            = E a
e
    r e :: E a
e@Var{}           = E a
e
    r e :: E a
e@NB{}            = E a
e
    r e :: E a
e@UB{}            = E a
e
    r e :: E a
e@BB{}            = E a
e
    r e :: E a
e@RwB{}           = E a
e
    r e :: E a
e@RwT{}           = E a
e
    r e :: E a
e@TB{}            = E a
e
    r (EApp a
l E a
e0 E a
e1)    = a -> E a -> E a -> E a
forall a. a -> E a -> E a -> E a
EApp a
l (E a -> E a
r E a
e0) (E a -> E a
r E a
e1)
    r (Implicit a
l E a
e)    = a -> E a -> E a
forall a. a -> E a -> E a
Implicit a
l (E a -> E a
r E a
e)
    r (Guarded a
l E a
p E a
e)   = a -> E a -> E a -> E a
forall a. a -> E a -> E a -> E a
Guarded a
l (E a -> E a
r E a
p) (E a -> E a
r E a
e)
    r (Let a
l (Nm a
n, E a
be) E a
e) = a -> (Nm a, E a) -> E a -> E a
forall a. a -> (Nm a, E a) -> E a -> E a
Let a
l (Nm a
n, E a -> E a
r E a
be) (E a -> E a
r E a
e)
    r (Lam a
l Nm a
n E a
e)       = 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
r E a
e)
    r (Cond a
l E a
p E a
e0 E a
e1)  = a -> E a -> E a -> E a -> E a
forall a. a -> E a -> E a -> E a -> E a
Cond a
l (E a -> E a
r E a
p) (E a -> E a
r E a
e0) (E a -> E a
r E a
e1)
    r (OptionVal a
l Maybe (E a)
e)   = a -> Maybe (E a) -> E a
forall a. a -> Maybe (E a) -> E a
OptionVal a
l (E a -> E a
r(E a -> E a) -> Maybe (E a) -> Maybe (E a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>Maybe (E a)
e)
    r (Tup a
l [E a]
es)        = a -> [E a] -> E a
forall a. a -> [E a] -> E a
Tup a
l (E a -> E a
r(E a -> E a) -> [E a] -> [E a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>[E a]
es)
    r (Rec a
l [(Nm a, E a)]
es)        = a -> [(Nm a, E a)] -> E a
forall a. a -> [(Nm a, E a)] -> E a
Rec a
l ((E a -> E a) -> (Nm a, E a) -> (Nm a, E a)
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second E a -> E a
r((Nm a, E a) -> (Nm a, E a)) -> [(Nm a, E a)] -> [(Nm a, E a)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>[(Nm a, E a)]
es)
    r (Arr a
l Vector (E a)
es)        = a -> Vector (E a) -> E a
forall a. a -> Vector (E a) -> E a
Arr a
l (E a -> E a
r(E a -> E a) -> Vector (E a) -> Vector (E a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>Vector (E a)
es)
    r (Anchor a
l [E a]
es)     = a -> [E a] -> E a
forall a. a -> [E a] -> E a
Anchor a
l (E a -> E a
r(E a -> E a) -> [E a] -> [E a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>[E a]
es)
    r e :: E a
e@Column{}        = E a
e
    r e :: E a
e@AllColumn{}     = E a
e
    r e :: E a
e@Field{}         = E a
e
    r e :: E a
e@AllField{}      = E a
e
    r e :: E a
e@LastField{}     = E a
e
    r e :: E a
e@FieldList{}     = E a
e
    r e :: E a
e@FParseAllCol{}  = E a
e
    r e :: E a
e@IParseAllCol{}  = E a
e
    r e :: E a
e@ParseAllCol{}   = E a
e
    r e :: E a
e@FParseCol{}     = E a
e
    r e :: E a
e@IParseCol{}     = E a
e
    r e :: E a
e@ParseCol{}      = E a
e
    r (Paren a
l E a
e)       = a -> E a -> E a
forall a. a -> E a -> E a
Paren a
l (E a -> E a
r E a
e)
    r Dfn{}             = [Char] -> E a
forall a. HasCallStack => [Char] -> a
error [Char]
"nested dfns not yet implemented"
    r F{}               = [Char] -> E a
forall a. HasCallStack => [Char] -> a
error [Char]
"Internal error."

replaceX :: (a -> Nm a) -> E a -> E a
replaceX :: forall a. (a -> Nm a) -> E a -> E a
replaceX a -> Nm a
n = (a -> Nm a) -> (a -> Nm a) -> E a -> E a
forall a. (a -> Nm a) -> (a -> Nm a) -> E a -> E a
replaceXY a -> Nm a
n ([Char] -> a -> Nm a
forall a. HasCallStack => [Char] -> a
error [Char]
"Internal error: 'y' not expected.")

renameD :: D a -> RenameM (D a)
renameD :: forall a. D a -> RenameM (D a)
renameD (FunDecl Nm a
n [Nm a]
ns E a
e) = Nm a -> [Nm a] -> E a -> D a
forall a. Nm a -> [Nm a] -> E a -> D a
FunDecl Nm a
n [] (E a -> D a)
-> StateT Renames Identity (E a) -> StateT Renames Identity (D a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E a -> StateT Renames Identity (E a)
forall s (m :: * -> *) a.
(HasRenames s, MonadState s m) =>
E a -> m (E a)
rE ([Nm a] -> E a -> E a
forall a. [Nm a] -> E a -> E a
mkLam [Nm a]
ns E a
e)
renameD D a
d                = D a -> StateT Renames Identity (D a)
forall a. a -> StateT Renames Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure D a
d

renameProgram :: Program a -> RenameM (Program a)
renameProgram :: forall a. Program a -> RenameM (Program a)
renameProgram (Program [D a]
ds E a
e) = [D a] -> E a -> Program a
forall a. [D a] -> E a -> Program a
Program ([D a] -> E a -> Program a)
-> StateT Renames Identity [D a]
-> StateT Renames Identity (E a -> Program a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (D a -> StateT Renames Identity (D a))
-> [D a] -> StateT Renames Identity [D a]
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 D a -> StateT Renames Identity (D a)
forall a. D a -> RenameM (D a)
renameD [D a]
ds StateT Renames Identity (E a -> Program a)
-> StateT Renames Identity (E a)
-> StateT Renames Identity (Program a)
forall a b.
StateT Renames Identity (a -> b)
-> StateT Renames Identity a -> StateT Renames Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> E a -> StateT Renames Identity (E a)
forall s (m :: * -> *) a.
(HasRenames s, MonadState s m) =>
E a -> m (E a)
rE E a
e

{-# INLINABLE rE #-}
rE :: (HasRenames s, MonadState s m) => E a -> m (E a)
rE :: forall s (m :: * -> *) a.
(HasRenames s, MonadState s m) =>
E a -> m (E a)
rE (EApp a
l E a
e E a
e')   = a -> E a -> E a -> E a
forall a. a -> E a -> E a -> E a
EApp a
l (E a -> E a -> E a) -> m (E a) -> m (E a -> E a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E a -> m (E a)
forall s (m :: * -> *) a.
(HasRenames s, MonadState s m) =>
E a -> m (E a)
rE E a
e m (E a -> E a) -> m (E a) -> m (E a)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> E a -> m (E a)
forall s (m :: * -> *) a.
(HasRenames s, MonadState s m) =>
E a -> m (E a)
rE E a
e'
rE (Tup a
l [E a]
es)      = a -> [E a] -> E a
forall a. a -> [E a] -> E a
Tup a
l ([E a] -> E a) -> m [E a] -> m (E a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (E a -> m (E a)) -> [E a] -> m [E a]
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 a -> m (E a)
forall s (m :: * -> *) a.
(HasRenames s, MonadState s m) =>
E a -> m (E a)
rE [E a]
es
rE (Rec a
l [(Nm a, E a)]
es)      = a -> [(Nm a, E a)] -> E a
forall a. a -> [(Nm a, E a)] -> E a
Rec a
l ([(Nm a, E a)] -> E a) -> m [(Nm a, E a)] -> m (E a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Nm a, E a) -> m (Nm a, E a)) -> [(Nm a, E a)] -> m [(Nm a, E a)]
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 a -> m (E a)) -> (Nm a, E a) -> m (Nm a, E a)
forall (m :: * -> *) b b' a.
Functor m =>
(b -> m b') -> (a, b) -> m (a, b')
secondM E a -> m (E a)
forall s (m :: * -> *) a.
(HasRenames s, MonadState s m) =>
E a -> m (E a)
rE) [(Nm a, E a)]
es
rE (Var a
l Nm a
n)       = a -> Nm a -> E a
forall a. a -> Nm a -> E a
Var a
l (Nm a -> E a) -> m (Nm a) -> m (E a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Nm a -> m (Nm a)
forall s (m :: * -> *) a.
(MonadState s m, HasRenames s) =>
Nm a -> m (Nm a)
replaceVar Nm a
n
rE (Lam a
l Nm a
n E a
e)     = m (E a) -> m (E a)
forall s (m :: * -> *) a.
(HasRenames s, MonadState s m) =>
m a -> m a
doLocal (m (E a) -> m (E a)) -> m (E a) -> m (E a)
forall a b. (a -> b) -> a -> b
$ do
    n' <- Nm a -> m (Nm a)
forall s (m :: * -> *) a.
(HasRenames s, MonadState s m) =>
Nm a -> m (Nm a)
freshen Nm a
n
    Lam l n' <$> rE e
rE (Dfn a
l E a
e) | {-# SCC "hasY" #-} E a -> Bool
forall a. E a -> Bool
hasY E a
e = do
    x@(Nm nX uX _) <- a -> Text -> m (Nm a)
forall s (m :: * -> *) a.
(MonadState s m, HasRenames s) =>
a -> Text -> m (Nm a)
dummyName a
l Text
"x"
    y@(Nm nY uY _) <- dummyName l "y"
    Lam l x . Lam l y <$> rE ({-# SCC "replaceXY" #-} replaceXY (Nm nX uX) (Nm nY uY) e)
                  | Bool
otherwise = do
    x@(Nm n u _) <- a -> Text -> m (Nm a)
forall s (m :: * -> *) a.
(MonadState s m, HasRenames s) =>
a -> Text -> m (Nm a)
dummyName a
l Text
"x"
    Lam l x <$> rE ({-# SCC "replaceX" #-} replaceX (Nm n u) e)
rE (Guarded a
l E a
p E a
e) = a -> E a -> E a -> E a
forall a. a -> E a -> E a -> E a
Guarded a
l (E a -> E a -> E a) -> m (E a) -> m (E a -> E a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E a -> m (E a)
forall s (m :: * -> *) a.
(HasRenames s, MonadState s m) =>
E a -> m (E a)
rE E a
p m (E a -> E a) -> m (E a) -> m (E a)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> E a -> m (E a)
forall s (m :: * -> *) a.
(HasRenames s, MonadState s m) =>
E a -> m (E a)
rE E a
e
rE (Implicit a
l E a
e) = a -> E a -> E a
forall a. a -> E a -> E a
Implicit a
l (E a -> E a) -> m (E a) -> m (E a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E a -> m (E a)
forall s (m :: * -> *) a.
(HasRenames s, MonadState s m) =>
E a -> m (E a)
rE E a
e
rE ResVar{} = [Char] -> m (E a)
forall a. HasCallStack => [Char] -> a
error [Char]
"Bare reserved variable."
rE (Let a
l (Nm a
n, E a
eϵ) E a
e') = m (E a) -> m (E a)
forall s (m :: * -> *) a.
(HasRenames s, MonadState s m) =>
m a -> m a
doLocal (m (E a) -> m (E a)) -> m (E a) -> m (E a)
forall a b. (a -> b) -> a -> b
$ do
    eϵ' <- E a -> m (E a)
forall s (m :: * -> *) a.
(HasRenames s, MonadState s m) =>
E a -> m (E a)
rE E a
eϵ
    n' <- freshen n
    Let l (n', eϵ') <$> rE e'
rE (Paren a
_ E a
e) = E a -> m (E a)
forall s (m :: * -> *) a.
(HasRenames s, MonadState s m) =>
E a -> m (E a)
rE E a
e
rE (Arr a
l Vector (E a)
es) = a -> Vector (E a) -> E a
forall a. a -> Vector (E a) -> E a
Arr a
l (Vector (E a) -> E a) -> m (Vector (E a)) -> m (E a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (E a -> m (E a)) -> Vector (E a) -> m (Vector (E a))
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) -> Vector a -> f (Vector b)
traverse E a -> m (E a)
forall s (m :: * -> *) a.
(HasRenames s, MonadState s m) =>
E a -> m (E a)
rE Vector (E a)
es
rE (Anchor a
l [E a]
es) = a -> [E a] -> E a
forall a. a -> [E a] -> E a
Anchor a
l ([E a] -> E a) -> m [E a] -> m (E a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (E a -> m (E a)) -> [E a] -> m [E a]
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 a -> m (E a)
forall s (m :: * -> *) a.
(HasRenames s, MonadState s m) =>
E a -> m (E a)
rE [E a]
es
rE (OptionVal a
l Maybe (E a)
e) = a -> Maybe (E a) -> E a
forall a. a -> Maybe (E a) -> E a
OptionVal a
l (Maybe (E a) -> E a) -> m (Maybe (E a)) -> m (E a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (E a -> m (E a)) -> Maybe (E a) -> m (Maybe (E a))
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) -> Maybe a -> f (Maybe b)
traverse E a -> m (E a)
forall s (m :: * -> *) a.
(HasRenames s, MonadState s m) =>
E a -> m (E a)
rE Maybe (E a)
e
rE (Cond a
l E a
p E a
e E a
e') = a -> E a -> E a -> E a -> E a
forall a. a -> E a -> E a -> E a -> E a
Cond a
l (E a -> E a -> E a -> E a) -> m (E a) -> m (E a -> E a -> E a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E a -> m (E a)
forall s (m :: * -> *) a.
(HasRenames s, MonadState s m) =>
E a -> m (E a)
rE E a
p m (E a -> E a -> E a) -> m (E a) -> m (E a -> E a)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> E a -> m (E a)
forall s (m :: * -> *) a.
(HasRenames s, MonadState s m) =>
E a -> m (E a)
rE E a
e m (E a -> E a) -> m (E a) -> m (E a)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> E a -> m (E a)
forall s (m :: * -> *) a.
(HasRenames s, MonadState s m) =>
E a -> m (E a)
rE E a
e'
rE E a
e = E a -> m (E a)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure E a
e