Any 1-qubit special gate can be decomposed into a sequence of rotation gates ($R_z$, $R_y$ and $R_z$). This allows us to have the general 1-qubit special gate in matrix form:
$$ U\left(\theta,\phi,\lambda\right)=\left(\begin{array}{cc} e^{-i(\phi+\lambda)}\cos\left(\frac{\theta}{2}\right) & -e^{-i(\phi-\lambda)}\sin\left(\frac{\theta}{2}\right)\\ e^{i(\phi-\lambda)}\sin\left(\frac{\theta}{2}\right) & e^{i(\phi+\lambda)}\cos\left(\frac{\theta}{2}\right) \end{array}\right) $$
If given $U\left(\theta,\phi,\lambda\right)$, how do I decompose it into any arbitrary set of gates such as rotation gates, pauli gates, etc?
To make the question more concrete, here is my current situation: for my project, I am giving users the ability to apply $U\left(\theta,\phi,\lambda\right)$ for specific values of $\theta$, $\phi$ and $\lambda$ to qubits.
But I am targeting real machines that only offer specific gates. For instance, the Rigetti Agave quantum processor only offers $R_z$, $R_x\left(k\pi/2\right)$ and $CZ$ as primitive gates.
One can think of any $U\left(\theta,\phi,\lambda\right)$ as an intermediate form that needs to be transformed into a sequence of whatever is the native gateset of the target quantum processor.
Now, in that spirit, how do I transform any $U\left(\theta,\phi,\lambda\right)$ into say $R_z$ and $R_x\left(k\pi/2\right)$? Let us ignore $CZ$ since it is a 2-qubit gate.
Note: I'm writing a compiler so an algorithm and reference papers or book chapters that solve this exact problems are more than welcome!