module stlc.catComb.compile where

open import Data.List

open import stlc.term
open import stlc.value
open import stlc.catComb public
open import stlc.inst
open import context
open import stlc.monad
open import stlc.monad.impl

⟦_⟧ : ∀ {Γ A} → Γ ⊢ A → CatComb (ctxToType Γ) A
⟦ ⟨⟩ ⟧ = !
⟦ `nat n ⟧ = nat n
⟦ ` Z ⟧ = p₂
⟦ ` (S x) ⟧ = ⟦ ` x ⟧ ∘ p₁
⟦ ƛ M ⟧ = cur ⟦ M ⟧
⟦ M · N ⟧ = app ∘ ⟨ ⟦ M ⟧ , ⟦ N ⟧ ⟩
⟦ fst M ⟧ = p₁ ∘ ⟦ M ⟧
⟦ snd M ⟧ = p₂ ∘ ⟦ M ⟧
⟦ M , N ⟧ = ⟨ ⟦ M ⟧ , ⟦ N ⟧ ⟩
--- COPRODUCT ---
⟦ inl M ⟧ = i1 ∘ ⟦ M ⟧
⟦ inr M ⟧ = i2 ∘ ⟦ M ⟧
⟦ case M inl M₁ inr M₂ ⟧ = [_,_] ⟦ M₁ ⟧ ⟦ M₂ ⟧ ∘ ⟨ id , ⟦ M ⟧ ⟩
--- LIST OBJECT ---
⟦ [] ⟧ = nil ∘ !
⟦ h ⦂ t ⟧ = cons ∘ ⟨ ⟦ h ⟧ , ⟦ t ⟧ ⟩
⟦ it x r l ⟧  = it ⟦ x ⟧ ⟦ r ⟧ ∘ ⟨ id , ⟦ l ⟧ ⟩
--- MONAD ---
⟦ `let_`in_ {s = s} x x₁ ⟧ = bind {s = s} ∘ ⟨ ⟦ x ⟧ , cur ⟦ x₁ ⟧ ⟩
⟦ return {m = m} x ⟧ = ret {m = m} ∘ ⟦ x ⟧

useMonadImpl : ∀ {A B} → CatComb A B → CatComb A B
useMonadImpl ! = !
useMonadImpl (nat x) = nat x
useMonadImpl id = id
useMonadImpl (x ∘ x₁) = useMonadImpl x ∘ useMonadImpl x₁
useMonadImpl ⟨ x , x₁ ⟩ = ⟨ useMonadImpl x , useMonadImpl x₁ ⟩
useMonadImpl p₁ = p₁
useMonadImpl p₂ = p₂
useMonadImpl (cur x) = cur (useMonadImpl x)
useMonadImpl app = app
useMonadImpl [ x , x₁ ] = [_,_] (useMonadImpl x) (useMonadImpl x₁)
useMonadImpl i1 = i1
useMonadImpl i2 = i2
useMonadImpl nil = nil
useMonadImpl cons = cons
useMonadImpl (it x x₁) = it (useMonadImpl x) (useMonadImpl x₁)
--- MONAD ---
useMonadImpl (ret {m = m}) = getReturnImpl m
useMonadImpl (bind {s = s}) = getBindImpl s

code : ∀ {A B} → CatComb A B → List Inst
code ! = [ UNIT ]
code (nat n) = [ NAT n ]
code id = [ SKIP ]
code (g ∘ f) = code f ++ code g
code ⟨ f , g ⟩ = PUSH ∷ code f ++ [ SWAP ] ++ code g ++ [ PAIR ]
code p₁ = [ FST ]
code p₂ = [ SND ]
code (cur f) = [ CUR (code f) ]
code app = [ APP ]
--- COPRODUCT ---
code [ f , g ] = [ CASE (code f) (code g) ]
code i1 = [ INL ]
code i2 = [ INR ]
--- LIST OBJECT ---
code nil = [ NIL ]
code cons = [ C ]
code (it x r) = [ IT (code x) (code r) ]
--- MONAD ---
code (ret {m = m}) = getReturnInst m
code (bind {s = s}) = getBindInst s

compile : ∀ {Γ A} → Γ ⊢ A → List Inst
compile M = code (useMonadImpl ⟦ M ⟧)

catCombValueToMachineValue : ∀ {A} → CatCombValue A → MachineValue
catCombValueToMachineValue (`nat n) = `nat n
catCombValueToMachineValue ⟨⟩ = ⟨⟩
catCombValueToMachineValue (s₁ , s₂) = catCombValueToMachineValue s₁ , catCombValueToMachineValue s₂
catCombValueToMachineValue (cur f s) = cur (code f) (catCombValueToMachineValue s)
catCombValueToMachineValue (L x) = L catCombValueToMachineValue x
catCombValueToMachineValue (R x) = R catCombValueToMachineValue x
catCombValueToMachineValue [] = []
catCombValueToMachineValue (h ⦂ t) = catCombValueToMachineValue h ⦂ catCombValueToMachineValue t

ctxToMachineValue : ∀ {Γ} → ValueOfContext Γ → MachineValue
ctxToMachineValue empty = ⟨⟩
ctxToMachineValue (cons x x₁) with ctxToMachineValue x | catCombValueToMachineValue x₁
... | z | w = z , w