------------------------------------------------------------------------ -- Proof of compiler correctness ------------------------------------------------------------------------ module Semantics.BigStep.CompilerCorrectness where open import Syntax open import Semantics.BigStep import CompilerCorrectness as CC; open CC BigStep open import Semantics.BigStep.CompilerCorrectness.Completeness open import Semantics.BigStep.CompilerCorrectness.Soundness open import Data.Product correct : ∀ {t} (e : Expr t) {i} → CompilerCorrect e i correct e = (sound e , (λ {_} → complete₁ e) , complete₂)