Strong Normalization by Type-Directed Partial Evaluation and Run-Time Code Generation