[Question]
  [
The [λ-calculus](https://en.wikipedia.org/wiki/Lambda_calculus#Formal_definition), or lambda calculus, is a logical system based on anonymous functions. For example, this a λ-expression:
```
λf.(λx.xx)(λx.f(xx))
```
However, for the purposes of this challenge, we'll simplify the notation:
* Change `λ` to `\` (to make it easier to type): `\f.(\x.xx)(\x.f(xx))`
* The `.` in lambda headers is unnecessary, so we can drop it: `\f(\xxx)(\xf(xx))`
* Use the [Unlambda](https://esolangs.org/wiki/Unlambda)-style prefix notation with ``` for application rather than writing the two functions together (for a full explanation of how to do this, see [Convert between Lambda Calculus Notations](https://codegolf.stackexchange.com/q/110011/61384)): `\f`\x`xx\x`f`xx`
* This is the most complicated substitution. Replace each variable with a number in brackets based on how deeply nested the variable is relative to the lambda header it belongs to (i.e. use 0-based [De Bruijn indexing](https://en.wikipedia.org/wiki/De_Bruijn_index)). For example, in `\xx` (the identity function), the `x` in the body would be replaced with `[0]`, because it belongs to the first (0-based) header encountered when traversing the expression from the variable to the end; `\x\y``\x`xxxy` would be converted into `\x\y``\x`[0][0][1][0]`. We can now drop the variables in the headers, leaving `\\``\`[0][0][1][0]`.
Combinatory logic is basically a [Turing Tarpit](https://esolangs.org/wiki/Turing_tarpit) made out of the λ-calculus (Well, actually, it came first, but that's irrelevant here.)
"Combinatory logic can be viewed as a variant of the lambda calculus, in which lambda expressions (representing functional abstraction) are replaced by a limited set of combinators, primitive functions from which bound variables are absent."1
The most common type of combinatory logic is the [SK combinator calculus](https://en.wikipedia.org/wiki/SKI_combinator_calculus), which uses the following primitives:
```
K = λx.λy.x
S = λx.λy.λz.xz(yz)
```
Sometimes a combinator `I = λx.x` is added, but it is redundant, as `SKK` (or indeed `SKx` for any `x`) is equivalent to `I`.
All you need is K, S, and application to be able to encode any expression in the λ-calculus. As an example, here's a translation from the function `λf.(λx.xx)(λx.f(xx))` to combinatory logic:
```
λf.(λx.xx)(λx.f(xx)) = S(K(λx.xx))(λf.λx.f(xx))
λx.f(xx) = S(Kf)(S(SKK)(SKK))
λf.λx.f(xx) = λf.S(Kf)(S(SKK)(SKK))
λf.S(Sf)(S(SKK)(SKK)) = S(λf.S(Sf))(K(S(SKK)(SKK)))
λf.S(Sf) = S(KS)S
λf.λx.f(xx) = S(S(KS)S)(K(S(SKK)(SKK)))
λx.xx = S(SKK)(SKK)
λf.(λx.xx)(λx.f(xx)) = S(K(S(SKK)(SKK)))(S(S(KS)S)(K(S(SKK)(SKK))))
```
Since we are using the prefix notation, this is ````S`K``S``SKK``SKK``S``S`KSS`K``SKK``.
1 Source: [Wikipedia](https://en.wikipedia.org/wiki/Combinatory_logic#Combinatory_logic_in_computing)
## The Challenge
By now, you've probably guessed what is: Write a program that takes a valid λ-expression (in the notation described above) as input and outputs (or returns) the same function, rewritten in SK-combinator calculus. Note that there are an infinite number of ways to rewrite this; you only need to output one of the infinite ways.
This is [code-golf](/questions/tagged/code-golf "show questions tagged 'code-golf'"), so the shortest valid submission (measured in bytes) wins.
## Test Cases
Each test case shows one possible output. The expression on top is the equivalent λ-calculus expression.
```
λx.x:
\[0]                        -> ``SKK
λx.xx:
\`[0][0]                    -> ```SKK``SKK
λx.λy.y:
\\[0]                       -> `SK
λx.λy.x:
\\[1]                       -> K
λx.λy.λz.xz(yz):
\\\``[2][0]`[1][0]          -> S
λw.w(λx.λy.λz.xz(yz))(λx.λy.x):
\``[0]\\[1]\\\``[2][0]`[1][0] -> ``S``SI`KS`KK
```
  
[Answer]
## Haskell, ~~251 237 222~~ 214 bytes
15 bytes saved thanks to @Ørjan\_Johansen (also see his TIO links in the remarks)!
8 more bytes saved thanks to @nimi!
```
data E=S|K|E:>E|V Int
p(h:s)|h>'_',(u,a)<-p s,(v,b)<-p u=(v,a:>b)|h>'['=a<$>p s|[(n,_:t)]<-reads s=(t,V n)
a(e:>f)=S:>a e:>a f
a(V 0)=S:>K:>K
a(V n)=K:>V(n-1)
a x=K:>x
o(e:>f)='`':o e++o f
o S="S"
o K="K"
f=o.snd.p
```
`p` parses the input, returning the remaining unparsed part in the first component of the resulting pair. The first character of its argument must be a backtick, a backslash or an opening bracket. The pattern guards of `p` check these cases in this order. In the first case, denoting an application, two more expressions are parsed and combined to an element of the `E` data type with the infix constructor `:>`. In the lambda case, the following expression is parsed and immediately given to the `a` function. Otherwise it is a variable, we get its number with the `reads` function (which returns a list) and drop the closing bracket by pattern matching with `(_:t)`. 
The `a` function does the quite well known bracket abstraction. To abstract an application, we abstract the two subexpressions and use the `S` combinator to distribute the argument to both. This is always correct, but with more code we could [do much better](https://codegolf.stackexchange.com/q/105991/56725) by handling special cases in order to get shorter expressions. Abstracting the current variable gives `I` or, when we don't have that, `SKK`. Usually the remaining cases can just add a `K` to the front, but when using this notation we have to renumber the variables as the inner lambda is abstracted.
`o` turns the result to a string for output. `f` is the complete function.
As in many languages, backslash is an escape character, so it has to be given twice in a string literal:
```
*Main> f "\\[0]"
"``SKK"
*Main> f "\\`[0][0]"
"``S``SKK``SKK"
*Main> f "\\\\[0]"
"``S``S`KS`KK`KK"
*Main> f "\\\\[1]"
"``S`KK``SKK"
*Main> f "\\\\\\``[2][0]`[1][0]"
"``S``S`KS``S``S`KS``S`KK`KS``S``S`KS``S``S`KS``S`KK`KS``S``S`KS``S`KK`KK``S`KK``SKK``S``S`KS``S``S`KS``S`KK`KS``S`KK`KK``S`KK`KK``S``S`KS``S``S`KS``S`KK`KS``S``S`KS``S`KK`KK``S``S`KS`KK`KK``S``S`KS``S``S`KS``S`KK`KS``S`KK`KK``S`KK`KK"
```
]