module stlc.examples.coproduct where

open import Data.List

open import config

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

open Utils

--- Example 1 - evaluate case on inr ---

ex1 : ∅ ⊢ nat × nat
ex1 = case (inr (`nat 2)) inl (# 0 , `nat 4) inr (# 0 , `nat 3)

inst1 : List Inst
inst1 = compile ex1

x1 : Result
x1 = run 100 ⟨ inst1 ∣ ⟨⟩ ∣ [] ⟩

--- Example 2 - booleans

Bool : Type
Bool = unit + unit

true : ∀ {Γ} → Γ ⊢ Bool
true = inl ⟨⟩

false : ∀ {Γ} → Γ ⊢ Bool
false = inr ⟨⟩

infix 4 if_then_else_

if_then_else_ : ∀ {Γ A} → Γ ⊢ Bool → Γ ⊢ A → Γ ⊢ A → Γ ⊢ A
if_then_else_ {Γ} e t f = case e inl weaken {Γ} t inr weaken {Γ} f

ex2 : ∅ ⊢ nat
ex2 = if true then `nat 0 else `nat 1

inst2 : List Inst
inst2 = compile ex2

x2 : Result
x2 = run 100 ⟨ inst2 ∣ ⟨⟩ ∣ [] ⟩