{-# OPTIONS --cubical --safe #-}
module Lambda.Simplified.Partiality-monad.Inductive.Compiler-correctness
where
open import Equality.Propositional.Cubical
open import Prelude hiding (⊥)
open import Monad equality-with-J
open import Vec.Function equality-with-J
open import Partiality-monad.Inductive
open import Partiality-monad.Inductive.Fixpoints hiding (comp; app)
open import Partiality-monad.Inductive.Monad
open import Lambda.Simplified.Compiler
open import Lambda.Simplified.Partiality-monad.Inductive.Interpreter
open import Lambda.Simplified.Partiality-monad.Inductive.Virtual-machine
open import Lambda.Simplified.Syntax
open import Lambda.Simplified.Virtual-machine
private
module C = Closure Code
module T = Closure Tm
open Partial
open Trans-⊑
evalⁿ : ∀ {n} → Tm n → T.Env n → ℕ → T.Value ⊥
evalⁿ t ρ n = app→ eval n (_ , t , ρ)
_∙ⁿ_ : T.Value → T.Value → ℕ → T.Value ⊥
(v₁ ∙ⁿ v₂) n = function (v₁ ∙ v₂) (app→ eval n)
execⁿ : State → ℕ → Maybe C.Value ⊥
execⁿ s n = app→ (transformer execP) n s
mutual
⟦⟧-correct :
∀ {n} t {ρ : T.Env n} {c s}
{k : ℕ → T.Value → Maybe C.Value ⊥} {n} →
(∀ v → execⁿ ⟨ c , val (comp-val v) ∷ s , comp-env ρ ⟩ ≳[ n ]
λ n → k n v) →
execⁿ ⟨ comp t c , s , comp-env ρ ⟩ ≳[ n ]
λ n → evalⁿ t ρ (suc n) >>= k n
⟦⟧-correct (var x) {ρ} {c} {s} {k} hyp =
execⁿ ⟨ var x ∷ c , s , comp-env ρ ⟩ ≳⟨ step⇓ ⟩
execⁿ ⟨ c , val (comp-val (ρ x)) ∷ s , comp-env ρ ⟩ ≳⟨ hyp (ρ x) ⟩
(λ n → k n (ρ x)) ≡⟨ sym now->>= ⟩≳
(λ n → evalⁿ (var x) ρ (suc n) >>= k n) ∎≳
⟦⟧-correct (ƛ t) {ρ} {c} {s} {k} hyp =
execⁿ ⟨ clo (comp t (ret ∷ [])) ∷ c , s , comp-env ρ ⟩ ≳⟨ step⇓ ⟩
execⁿ ⟨ c , val (comp-val (T.ƛ t ρ)) ∷ s , comp-env ρ ⟩ ≳⟨ hyp (T.ƛ t ρ) ⟩
(λ n → k n (T.ƛ t ρ)) ≡⟨ sym now->>= ⟩≳
(λ n → evalⁿ (ƛ t) ρ (suc n) >>= k n) ∎≳
⟦⟧-correct (t₁ · t₂) {ρ} {c} {s} {k} {n} hyp =
execⁿ ⟨ comp t₁ (comp t₂ (app ∷ c)) , s , comp-env ρ ⟩ ≳⟨ (⟦⟧-correct t₁ {n = n} λ v₁ → ⟦⟧-correct t₂ λ v₂ → ∙-correct v₁ v₂ hyp) ⟩
(λ n → evalⁿ t₁ ρ (suc n) >>=′ λ v₁ →
evalⁿ t₂ ρ (suc n) >>=′ λ v₂ →
(v₁ ∙ⁿ v₂) n >>=
k n) ≡⟨ cong (evalⁿ t₁ ρ (suc n) >>=′_)
(⟨ext⟩ λ _ → associativity (evalⁿ t₂ ρ (suc n)) _ _) ⟩≳
(λ n → evalⁿ t₁ ρ (suc n) >>=′ λ v₁ →
(evalⁿ t₂ ρ (suc n) >>=′ λ v₂ → (v₁ ∙ⁿ v₂) n) >>=
k n) ≡⟨ associativity (evalⁿ t₁ ρ (suc n)) _ _ ⟩≳
(λ n → evalⁿ (t₁ · t₂) ρ (suc n) >>= k n) ∎≳
∙-correct :
∀ {n} v₁ v₂ {ρ : T.Env n} {c s}
{k : ℕ → T.Value → Maybe C.Value ⊥} {n} →
(∀ v → execⁿ ⟨ c , val (comp-val v) ∷ s , comp-env ρ ⟩ ≳[ n ]
λ n → k n v) →
execⁿ ⟨ app ∷ c
, val (comp-val v₂) ∷ val (comp-val v₁) ∷ s
, comp-env ρ
⟩ ≳[ n ]
λ n → (v₁ ∙ⁿ v₂) n >>= k n
∙-correct (T.ƛ t₁ ρ₁) v₂ {ρ} {c} {s} {k} {zero} hyp =
execⁿ ⟨ app ∷ c
, val (comp-val v₂) ∷ val (comp-val (T.ƛ t₁ ρ₁)) ∷ s
, comp-env ρ
⟩ ≡⟨ refl ⟩≳
const never ≡⟨ sym never->>= ⟩≳
(λ n → (T.ƛ t₁ ρ₁ ∙ⁿ v₂) n >>= k n) ∎≳
∙-correct (T.ƛ t₁ ρ₁) v₂ {ρ} {c} {s} {k} {suc n} hyp = later (
execⁿ ⟨ app ∷ c
, val (comp-val v₂) ∷ val (comp-val (T.ƛ t₁ ρ₁)) ∷ s
, comp-env ρ
⟩ ∘ suc ≳⟨⟩
execⁿ ⟨ comp t₁ (ret ∷ [])
, ret c (comp-env ρ) ∷ s
, cons (comp-val v₂) (comp-env ρ₁)
⟩ ∀≡⟨ (λ n → cong (λ ρ′ → execⁿ ⟨ comp t₁ (ret ∷ []) , ret c (comp-env ρ) ∷ s , ρ′ ⟩ n)
(sym comp-cons)) ⟩≳
execⁿ ⟨ comp t₁ (ret ∷ [])
, ret c (comp-env ρ) ∷ s
, comp-env (cons v₂ ρ₁)
⟩ ≳⟨ (⟦⟧-correct t₁ {n = n} λ v →
execⁿ ⟨ ret ∷ []
, val (comp-val v) ∷ ret c (comp-env ρ) ∷ s
, comp-env (cons v₂ ρ₁)
⟩ ≳⟨ step⇓ ⟩
execⁿ ⟨ c , val (comp-val v) ∷ s , comp-env ρ ⟩ ≳⟨ hyp v ⟩
(λ n → k n v) ≳⟨ step⇓ ⟩
(λ n → k (suc n) v) ∎≳) ⟩
(λ n → evalⁿ t₁ (cons v₂ ρ₁) (suc n) >>= k (suc n)) ≳⟨⟩
(λ n → (T.ƛ t₁ ρ₁ ∙ⁿ v₂) (suc n) >>= k (suc n)) ∎≳)
correct :
∀ t →
exec ⟨ comp t [] , [] , nil ⟩ ≡
(⟦ t ⟧ nil >>= λ v → return (just (comp-val v)))
correct t =
exec ⟨ comp t [] , [] , nil ⟩ ≡⟨ cong (λ ρ → exec ⟨ comp t [] , [] , ρ ⟩) $ sym comp-nil ⟩
exec ⟨ comp t [] , [] , comp-env nil ⟩ ≡⟨⟩
⨆ ( execⁿ ⟨ comp t [] , [] , comp-env nil ⟩
, _
) ≡⟨ ≳→⨆≡⨆ 1 (⟦⟧-correct t $ λ v →
execⁿ ⟨ [] , val (comp-val v) ∷ [] , comp-env nil ⟩ ≳⟨ step⇓ ⟩
const (return (just (comp-val v))) ∎≳) ⟩
⨆ ( (λ n → evalⁿ t nil n >>= λ v →
return (just (comp-val v)))
, _
) ≡⟨ sym ⨆->>= ⟩
(⟦ t ⟧ nil >>= λ v → return (just (comp-val v))) ∎