{-# LANGUAGE OverloadedStrings #-}

module R.Dfn ( dedfn ) where

import           A
import           Control.Monad.State.Strict (get, modify)
import qualified Data.Text                  as T
import           Nm
import           R.M
import           U

dummyName :: T.Text -> RM (a -> Nm a)
dummyName :: forall a. Text -> RM (a -> Nm a)
dummyName Text
n = do
    st <- StateT Int Identity Int
forall s (m :: * -> *). MonadState s m => m s
get
    Nm n (U$st+1) <$ modify (+1)

dedfn :: Int -> E a -> (E a, Int)
dedfn :: forall a. Int -> E a -> (E a, Int)
dedfn Int
i = Int -> RM (E a) -> (E a, Int)
forall x. Int -> RM x -> (x, Int)
runR Int
i (RM (E a) -> (E a, Int)) -> (E a -> RM (E a)) -> E a -> (E a, Int)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. E a -> RM (E a)
forall a. E a -> RM (E a)
dedfnM

-- bottom-up
dedfnM :: E a -> RM (E a)
dedfnM :: forall a. E a -> RM (E a)
dedfnM e :: E a
e@ILit{} = E a -> StateT Int Identity (E a)
forall a. a -> StateT Int Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure E a
e
dedfnM e :: E a
e@FLit{} = E a -> StateT Int Identity (E a)
forall a. a -> StateT Int Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure E a
e
dedfnM e :: E a
e@BLit{} = E a -> StateT Int Identity (E a)
forall a. a -> StateT Int Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure E a
e
dedfnM e :: E a
e@Var{} = E a -> StateT Int Identity (E a)
forall a. a -> StateT Int Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure E a
e
dedfnM e :: E a
e@Builtin{} = E a -> StateT Int Identity (E a)
forall a. a -> StateT Int Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure E a
e
dedfnM e :: E a
e@ResVar{} = E a -> StateT Int Identity (E a)
forall a. a -> StateT Int Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure E a
e
dedfnM (Ann a
l E a
e T a
t) = a -> E a -> T a -> E a
forall a. a -> E a -> T a -> E a
Ann a
l (E a -> T a -> E a)
-> StateT Int Identity (E a) -> StateT Int Identity (T a -> E a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E a -> StateT Int Identity (E a)
forall a. E a -> RM (E a)
dedfnM E a
e StateT Int Identity (T a -> E a)
-> StateT Int Identity (T a) -> StateT Int Identity (E a)
forall a b.
StateT Int Identity (a -> b)
-> StateT Int Identity a -> StateT Int Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> T a -> StateT Int Identity (T a)
forall a. a -> StateT Int Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure T a
t
dedfnM (ALit a
l [E a]
es) = a -> [E a] -> E a
forall a. a -> [E a] -> E a
ALit a
l ([E a] -> E a)
-> StateT Int Identity [E a] -> StateT Int Identity (E a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (E a -> StateT Int Identity (E a))
-> [E a] -> StateT Int Identity [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 -> StateT Int Identity (E a)
forall a. E a -> RM (E a)
dedfnM [E a]
es
dedfnM (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)
-> StateT Int Identity [E a] -> StateT Int Identity (E a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (E a -> StateT Int Identity (E a))
-> [E a] -> StateT Int Identity [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 -> StateT Int Identity (E a)
forall a. E a -> RM (E a)
dedfnM [E a]
es
dedfnM (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)
-> StateT Int Identity (E a) -> StateT Int Identity (E a -> E a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E a -> StateT Int Identity (E a)
forall a. E a -> RM (E a)
dedfnM E a
e StateT Int Identity (E a -> E a)
-> StateT Int Identity (E a) -> StateT Int Identity (E a)
forall a b.
StateT Int Identity (a -> b)
-> StateT Int Identity a -> StateT Int Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> E a -> StateT Int Identity (E a)
forall a. E a -> RM (E a)
dedfnM E a
e'
dedfnM (Cond a
l E a
e 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)
-> StateT Int Identity (E a)
-> StateT Int Identity (E a -> E a -> E a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E a -> StateT Int Identity (E a)
forall a. E a -> RM (E a)
dedfnM E a
e StateT Int Identity (E a -> E a -> E a)
-> StateT Int Identity (E a) -> StateT Int Identity (E a -> E a)
forall a b.
StateT Int Identity (a -> b)
-> StateT Int Identity a -> StateT Int Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> E a -> StateT Int Identity (E a)
forall a. E a -> RM (E a)
dedfnM E a
e' StateT Int Identity (E a -> E a)
-> StateT Int Identity (E a) -> StateT Int Identity (E a)
forall a b.
StateT Int Identity (a -> b)
-> StateT Int Identity a -> StateT Int Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> E a -> StateT Int Identity (E a)
forall a. E a -> RM (E a)
dedfnM E a
e''
dedfnM (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)
-> StateT Int Identity (E a) -> StateT Int Identity (E a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E a -> StateT Int Identity (E a)
forall a. E a -> RM (E a)
dedfnM E a
e
dedfnM (Let a
l (Nm a
n, E a
e) E a
eBody) = do
    e' <- E a -> StateT Int Identity (E a)
forall a. E a -> RM (E a)
dedfnM E a
e
    Let l (n, e') <$> dedfnM eBody
dedfnM (Def a
l (Nm a
n, E a
e) E a
eBody) = do
    e' <- E a -> StateT Int Identity (E a)
forall a. E a -> RM (E a)
dedfnM E a
e
    Def l (n, e') <$> dedfnM eBody
dedfnM (LLet a
l (Nm a
n, E a
e) E a
eBody) = do
    e' <- E a -> StateT Int Identity (E a)
forall a. E a -> RM (E a)
dedfnM E a
e
    LLet l (n, e') <$> dedfnM eBody
dedfnM (Dfn a
l E a
e) = do
    e' <- E a -> StateT Int Identity (E a)
forall a. E a -> RM (E a)
dedfnM E a
e
    x <- dummyName "x" -- TODO: do we need uniques? could rename it later
    y <- dummyName "y"
    let (eDone, hasY) = replaceXY x y e'
    pure $ if hasY
        then Lam l (x l) (Lam l (y l) eDone)
        else Lam l (x l) eDone
dedfnM (Parens a
_ E a
e) = E a -> StateT Int Identity (E a)
forall a. E a -> RM (E a)
dedfnM E a
e

-- this approach is criminally inefficient
replaceXY :: (a -> Nm a) -- ^ x
          -> (a -> Nm a) -- ^ y
          -> E a -> (E a, Bool) -- True if it has 'y'
replaceXY :: forall a. (a -> Nm a) -> (a -> Nm a) -> E a -> (E a, Bool)
replaceXY a -> Nm a
_ a -> Nm a
y (ResVar a
l ResVar
Y) = (a -> Nm a -> E a
forall a. a -> Nm a -> E a
Var a
l (a -> Nm a
y a
l), Bool
True)
replaceXY a -> Nm a
x a -> Nm a
_ (ResVar a
l ResVar
X) = (a -> Nm a -> E a
forall a. a -> Nm a -> E a
Var a
l (a -> Nm a
x a
l), Bool
False)
replaceXY a -> Nm a
_ a -> Nm a
_ e :: E a
e@FLit{} = (E a
e, Bool
False)
replaceXY a -> Nm a
_ a -> Nm a
_ e :: E a
e@ILit{} = (E a
e, Bool
False)
replaceXY a -> Nm a
_ a -> Nm a
_ e :: E a
e@BLit{} = (E a
e, Bool
False)
replaceXY a -> Nm a
_ a -> Nm a
_ e :: E a
e@Var{} = (E a
e, Bool
False)
replaceXY a -> Nm a
_ a -> Nm a
_ e :: E a
e@Builtin{} = (E a
e, Bool
False)
replaceXY a -> Nm a
x a -> Nm a
y (Ann a
l E a
e T a
t) =
    let (E a
e', Bool
b) = (a -> Nm a) -> (a -> Nm a) -> E a -> (E a, Bool)
forall a. (a -> Nm a) -> (a -> Nm a) -> E a -> (E a, Bool)
replaceXY a -> Nm a
x a -> Nm a
y E a
e
        in (a -> E a -> T a -> E a
forall a. a -> E a -> T a -> E a
Ann a
l E a
e' T a
t, Bool
b)
replaceXY a -> Nm a
x a -> Nm a
y (Lam a
l Nm a
n E a
e) =
    let (E a
e', Bool
b) = (a -> Nm a) -> (a -> Nm a) -> E a -> (E a, Bool)
forall a. (a -> Nm a) -> (a -> Nm a) -> E a -> (E a, Bool)
replaceXY a -> Nm a
x a -> Nm a
y E a
e
        in (a -> Nm a -> E a -> E a
forall a. a -> Nm a -> E a -> E a
Lam a
l Nm a
n E a
e', Bool
b)
replaceXY a -> Nm a
x a -> Nm a
y (EApp a
l E a
e E a
e') =
    let (E a
eR, Bool
b) = (a -> Nm a) -> (a -> Nm a) -> E a -> (E a, Bool)
forall a. (a -> Nm a) -> (a -> Nm a) -> E a -> (E a, Bool)
replaceXY a -> Nm a
x a -> Nm a
y E a
e
        (E a
eR', Bool
b') = (a -> Nm a) -> (a -> Nm a) -> E a -> (E a, Bool)
forall a. (a -> Nm a) -> (a -> Nm a) -> E a -> (E a, Bool)
replaceXY a -> Nm a
x a -> Nm a
y E a
e'
        in (a -> E a -> E a -> E a
forall a. a -> E a -> E a -> E a
EApp a
l E a
eR E a
eR', Bool
b Bool -> Bool -> Bool
|| Bool
b')
replaceXY a -> Nm a
x a -> Nm a
y (Cond a
l E a
p E a
e E a
e') =
    let (E a
pR, Bool
b0) = (a -> Nm a) -> (a -> Nm a) -> E a -> (E a, Bool)
forall a. (a -> Nm a) -> (a -> Nm a) -> E a -> (E a, Bool)
replaceXY a -> Nm a
x a -> Nm a
y E a
p
        (E a
eR, Bool
b1) = (a -> Nm a) -> (a -> Nm a) -> E a -> (E a, Bool)
forall a. (a -> Nm a) -> (a -> Nm a) -> E a -> (E a, Bool)
replaceXY a -> Nm a
x a -> Nm a
y E a
e
        (E a
eR', Bool
b2) = (a -> Nm a) -> (a -> Nm a) -> E a -> (E a, Bool)
forall a. (a -> Nm a) -> (a -> Nm a) -> E a -> (E a, Bool)
replaceXY a -> Nm a
x a -> Nm a
y E a
e'
    in (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
pR E a
eR E a
eR', Bool
b0 Bool -> Bool -> Bool
|| Bool
b1 Bool -> Bool -> Bool
|| Bool
b2)
replaceXY a -> Nm a
x a -> Nm a
y (Let a
l (Nm a
n, E a
e) E a
e') =
    let (E a
eR, Bool
b) = (a -> Nm a) -> (a -> Nm a) -> E a -> (E a, Bool)
forall a. (a -> Nm a) -> (a -> Nm a) -> E a -> (E a, Bool)
replaceXY a -> Nm a
x a -> Nm a
y E a
e
        (E a
eR', Bool
b') = (a -> Nm a) -> (a -> Nm a) -> E a -> (E a, Bool)
forall a. (a -> Nm a) -> (a -> Nm a) -> E a -> (E a, Bool)
replaceXY a -> Nm a
x a -> Nm a
y E a
e'
        in (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
eR) E a
eR', Bool
b Bool -> Bool -> Bool
|| Bool
b')
replaceXY a -> Nm a
x a -> Nm a
y (LLet a
l (Nm a
n, E a
e) E a
e') =
    let (E a
eR, Bool
b) = (a -> Nm a) -> (a -> Nm a) -> E a -> (E a, Bool)
forall a. (a -> Nm a) -> (a -> Nm a) -> E a -> (E a, Bool)
replaceXY a -> Nm a
x a -> Nm a
y E a
e
        (E a
eR', Bool
b') = (a -> Nm a) -> (a -> Nm a) -> E a -> (E a, Bool)
forall a. (a -> Nm a) -> (a -> Nm a) -> E a -> (E a, Bool)
replaceXY a -> Nm a
x a -> Nm a
y E a
e'
        in (a -> (Nm a, E a) -> E a -> E a
forall a. a -> (Nm a, E a) -> E a -> E a
LLet a
l (Nm a
n, E a
eR) E a
eR', Bool
b Bool -> Bool -> Bool
|| Bool
b')
replaceXY a -> Nm a
x a -> Nm a
y (Def a
l (Nm a
n, E a
e) E a
e') =
    let (E a
eR, Bool
b) = (a -> Nm a) -> (a -> Nm a) -> E a -> (E a, Bool)
forall a. (a -> Nm a) -> (a -> Nm a) -> E a -> (E a, Bool)
replaceXY a -> Nm a
x a -> Nm a
y E a
e
        (E a
eR', Bool
b') = (a -> Nm a) -> (a -> Nm a) -> E a -> (E a, Bool)
forall a. (a -> Nm a) -> (a -> Nm a) -> E a -> (E a, Bool)
replaceXY a -> Nm a
x a -> Nm a
y E a
e'
        in (a -> (Nm a, E a) -> E a -> E a
forall a. a -> (Nm a, E a) -> E a -> E a
Def a
l (Nm a
n, E a
eR) E a
eR', Bool
b Bool -> Bool -> Bool
|| Bool
b')
replaceXY a -> Nm a
x a -> Nm a
y (ALit a
l [E a]
es) =
    let ([E a]
esR, [Bool]
bs) = [(E a, Bool)] -> ([E a], [Bool])
forall a b. [(a, b)] -> ([a], [b])
unzip ((E a -> (E a, Bool)) -> [E a] -> [(E a, Bool)]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((a -> Nm a) -> (a -> Nm a) -> E a -> (E a, Bool)
forall a. (a -> Nm a) -> (a -> Nm a) -> E a -> (E a, Bool)
replaceXY a -> Nm a
x a -> Nm a
y) [E a]
es)
    in (a -> [E a] -> E a
forall a. a -> [E a] -> E a
ALit a
l [E a]
esR, [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or [Bool]
bs)
replaceXY a -> Nm a
x a -> Nm a
y (Tup a
l [E a]
es) =
    let ([E a]
esR, [Bool]
bs) = [(E a, Bool)] -> ([E a], [Bool])
forall a b. [(a, b)] -> ([a], [b])
unzip ((E a -> (E a, Bool)) -> [E a] -> [(E a, Bool)]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((a -> Nm a) -> (a -> Nm a) -> E a -> (E a, Bool)
forall a. (a -> Nm a) -> (a -> Nm a) -> E a -> (E a, Bool)
replaceXY a -> Nm a
x a -> Nm a
y) [E a]
es)
    in (a -> [E a] -> E a
forall a. a -> [E a] -> E a
Tup a
l [E a]
esR, [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or [Bool]
bs)