module untyped.compile where

open import Data.List hiding (unfold)

open import untyped.term
open import untyped.context
open import untyped.catComb public
open import untyped.inst

⟦_⟧ : ∀ {Γ A} → Γ ⊢ A → CatComb (ctxToType Γ) A
⟦ ` Z ⟧ = p₂
⟦ ` S x ⟧ = ⟦ ` x ⟧ ∘ p₁
⟦ j x x₁ ⟧ = ev ∘ ⟨ unfold ∘ ⟦ x ⟧ , ⟦ x₁ ⟧ ⟩
⟦ i x ⟧ = fold ∘ ⟦ x ⟧
⟦ ƛ x ⟧ = cur ⟦ x ⟧

code : ∀ {A B} → CatComb A B → List Inst
code fold = [ FOLD ]
code unfold = [ UNFOLD ]
code (x₁ ∘ x₂) = code x₂ ++ code x₁
code ⟨ f , g ⟩ =  PUSH ∷ code f ++ [ SWAP ] ++ code g ++ [ PAIR ]
code p₁ = [ FST ]
code p₂ = [ SND ]
code (cur x₁) = [ CUR (code x₁) ]
code ev = [ EV ]