module stlc.examples.list where

open import Data.Nat hiding (_≤_; _+_)
open import Data.List

open import config
open import stlc.term
open import stlc.catComb.compile
open import stlc.run

open Utils

Nat : Type
Nat = list unit

z : ∀ {Γ} → Γ ⊢ Nat
z = []

infixr 7 s_

s_ : ∀ {Γ} → Γ ⊢ Nat → Γ ⊢ Nat
s x = ⟨⟩ ⦂ x

module NatUtils where
  len : MachineValue → ℕ
  len [] = zero
  len (⟨⟩ ⦂ t) = suc (len t)
  len _ = zero

  toNat : ∀ {Γ} → ℕ → Γ ⊢ Nat
  toNat zero = z
  toNat (suc x) = s (toNat x)

  decodeNat : Result → ℕ
  decodeNat (done x) = len x
  decodeNat _ = 0

  decodeListNat : Result → List ℕ
  decodeListNat (done []) = []
  decodeListNat (done (x₁ ⦂ x₂)) = len x₁ ∷ decodeListNat (done x₂)
  decodeListNat _ = []

  encode : List ℕ → ∅ ⊢ list Nat
  encode l = foldr _⦂_ [] (map toNat l)

--- Example 1 - increment numbers in list ---
x : ∅ ⊢ list Nat
x = []

r : ∅ , (Nat × list Nat) ⊢ list Nat
r = s fst (` Z) ⦂ snd (` Z)

list012 : ∅ ⊢ list Nat
list012 = NatUtils.encode (0 ∷ 1 ∷ 2 ∷ [])

map+1 : ∅ ⊢ list Nat
map+1 = it x r list012

inst1 : List Inst
inst1 = compile map+1

result1 : Result
result1 = run 1000 ⟨ inst1 ∣ ⟨⟩ ∣ [] ⟩

res1 : List ℕ
res1 = NatUtils.decodeListNat result1

--- Example 2 - reverse list ---
xₐ : ∀ {Γ A} → Γ , (A × list A) ⊢ list A
xₐ = fst (` Z) ⦂ []

rₐ : ∀ {Γ A} → Γ , (A × list A) , (A × list A) ⊢ list A
rₐ = fst (` Z) ⦂ snd (` Z)

append : ∀ {Γ A} → Γ , (A × list A) ⊢ list A
append = it xₐ rₐ (snd (` Z))

x₁ : ∅ , list Nat ⊢ list Nat
x₁ = []

r₁ : ∅ , list Nat , (Nat × list Nat) ⊢ list Nat
r₁ = (ƛ append) · (` Z)

rev : ∅ , list Nat ⊢ list Nat
rev = it x₁ r₁ (` Z)

rev012 : ∅ ⊢ list Nat
rev012 = (ƛ rev)  · list012

inst2 : List Inst
inst2 = compile rev012

result2 : Result
result2 = run 1000 ⟨ inst2 ∣ ⟨⟩ ∣ [] ⟩

res2 : List ℕ
res2 = NatUtils.decodeListNat result2

--- Example 3 - compare numbers ---

open import stlc.examples.coproduct
open import stlc.proof.wellTyped

comp : ∀ {Γ} → CatCombValue Nat → CatCombValue Nat → Γ ⊢ Bool
comp [] y = true
comp (⟨⟩ ⦂ _) [] = false
comp (⟨⟩ ⦂ x) (⟨⟩ ⦂ y) = comp x y

infix 5 _≤_

_≤_ : ∀ {Γ} → ∅ ⊢ Nat → ∅ ⊢ Nat → Γ ⊢ Bool
x ≤ y = comp (eval x) (eval y)

ex3 : ∅ ⊢ Nat
ex3 = if (s s z) ≤ (s s s s z) then (s s z) else (s s s z)

inst3 : List Inst
inst3 = compile ex3

result3 : Result
result3 = run 100 ⟨ inst3 ∣ ⟨⟩ ∣ [] ⟩

res3 : ℕ
res3 = NatUtils.decodeNat result3

--- Example 4 - concat two lists ---
concatList : ∀ {Γ A} → Γ , (list A × list A) ⊢ list A
concatList = it (snd (# 0)) ((fst (# 0)) ⦂ (snd (# 0))) (fst # 0)

add : ∀ {Γ} → Γ , (Nat × Nat) ⊢ Nat
add = concatList

_+Nat_ : ∀ {Γ} → Γ ⊢ Nat → Γ ⊢ Nat → Γ ⊢ Nat
a +Nat b = (ƛ add) · (a , b)

ex4 : ∅ ⊢ Nat
ex4 = (NatUtils.toNat 2) +Nat (NatUtils.toNat 3)

inst4 : List Inst
inst4 = compile ex4

result4 : Result
result4 = run 100 ⟨ inst4 ∣ ⟨⟩ ∣ [] ⟩

res4 : ℕ
res4 = NatUtils.decodeNat result4