open import Prelude
import Lambda.Syntax
module Lambda.Compiler
{Name : Type}
(open Lambda.Syntax Name)
(def : Name → Tm 1)
where
open import Equality.Propositional
open import Tactic.By.Propositional
open import List equality-with-J using (_++_)
open import Vec.Data equality-with-J
open import Lambda.Virtual-machine.Instructions Name
private
module C = Closure Code
module T = Closure Tm
In-tail-context : Type
In-tail-context = Bool
mutual
comp : ∀ {n} → In-tail-context → Tm n → Code n → Code n
comp _ (var x) c = var x ∷ c
comp _ (lam t) c = clo (comp-body t) ∷ c
comp _ (t₁ · t₂) c = comp false t₁ (comp false t₂ (app ∷ c))
comp true (call f t) c = comp false t (tcl f ∷ c)
comp false (call f t) c = comp false t (cal f ∷ c)
comp _ (con b) c = con b ∷ c
comp tc (if t₁ t₂ t₃) c =
comp false t₁ (bra (comp tc t₂ []) (comp tc t₃ []) ∷ c)
comp-body : ∀ {n} → Tm (suc n) → Code (suc n)
comp-body t = comp true t (ret ∷ [])
comp-name : Name → Code 1
comp-name f = comp-body (def f)
comp₀ : Tm 0 → Code 0
comp₀ t = comp false t []
mutual
comp-env : ∀ {n} → T.Env n → C.Env n
comp-env [] = []
comp-env (v ∷ ρ) = comp-val v ∷ comp-env ρ
comp-val : T.Value → C.Value
comp-val (T.lam t ρ) = C.lam (comp-body t) (comp-env ρ)
comp-val (T.con b) = C.con b
comp-index : ∀ {n} (ρ : T.Env n) (x : Fin n) →
index (comp-env ρ) x ≡ comp-val (index ρ x)
comp-index (v ∷ ρ) fzero = refl
comp-index (v ∷ ρ) (fsuc i) = comp-index ρ i
comp-++ :
∀ {n} tc (t : Tm n) {c₁ c₂ : Code n} →
comp tc t c₁ ++ c₂ ≡ comp tc t (c₁ ++ c₂)
comp-++ _ (var x) = refl
comp-++ _ (lam t) = refl
comp-++ true (call f t) = comp-++ _ t
comp-++ false (call f t) = comp-++ _ t
comp-++ _ (con b) = refl
comp-++ _ (if t₁ t₂ t₃) = comp-++ _ t₁
comp-++ _ (t₁ · t₂) {c₁} {c₂} =
comp false t₁ (comp false t₂ (app ∷ c₁)) ++ c₂ ≡⟨ comp-++ _ t₁ ⟩
comp false t₁ (comp false t₂ (app ∷ c₁) ++ c₂) ≡⟨ by (comp-++ _ t₂) ⟩∎
comp false t₁ (comp false t₂ (app ∷ c₁ ++ c₂)) ∎