------------------------------------------------------------------------
-- 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₂)