module gy13 where infixr 5 _⇒_ infixl 4 _$_ infixl 3 _▶_ data Ty : Set where BOOL : Ty _⇒_ : Ty → Ty → Ty -- \=> -- variable A B C : Ty -- not function should have type (bool ⇒ bool) -- or function should have type (bool ⇒ (bool ⇒ bool)) data Con : Set where ∙ : Con -- empty, \. _▶_ : Con → Ty → Con -- context extension, \T4 -- variable Γ Δ Θ : Con exΓ exΔ : Con exΓ = ∙ ▶ BOOL ▶ (BOOL ⇒ BOOL) -- length 2 exΔ = ∙ ▶ BOOL ⇒ BOOL ⇒ BOOL ▶ BOOL ▶ BOOL -- length 3 data Var : Con → Ty → Set where zero : {Γ : Con}{A : Ty} → Var (Γ ▶ A) A suc : {Γ : Con}{A B : Ty} → Var Γ B → Var (Γ ▶ A) B -- suc : ℕ → ℕ exv : Var exΓ BOOL exv = suc zero exv' exv'' : Var exΔ BOOL exv' = zero exv'' = suc zero data Tm : Con → Ty → Set where TRUE FALSE : {Γ : Con} → Tm Γ BOOL IF_THEN_ELSE_ : {Γ : Con}{A : Ty} → Tm Γ BOOL → Tm Γ A → Tm Γ A → Tm Γ A _$_ : {Γ : Con}{A B : Ty} → Tm Γ (A ⇒ B) → Tm Γ A → Tm Γ B LAM : {Γ : Con}{A B : Ty} → Tm (Γ ▶ A) B → Tm Γ (A ⇒ B) VAR : {Γ : Con}{A : Ty} → Var Γ A → Tm Γ A -- (λ x → if x then 1 else 2) $ x -- (LAM (IF VAR 0 THEN NUM 1 ELSE NUM 2)) $ ... e1 : Tm ∙ (BOOL ⇒ BOOL) e2 e3 e4 : Tm ∙ (BOOL ⇒ BOOL ⇒ BOOL) -- e1 = λ x → x LAM 0 e1 = LAM (VAR zero) -- e2 = λ x → (λ y → x) LAM (LAM 1) e2 = LAM (LAM (VAR (suc zero))) -- e3 = λ x → (λ y → y) LAM (LAM 0) e3 = LAM (LAM (VAR zero)) -- e4 = λ x → (λ y → if x then y else x) LAM (LAM (IF 1 THEN 0 ELSE 1)) e4 = LAM (LAM (IF VAR (suc zero) THEN VAR zero ELSE VAR (suc zero))) -- De Bruijn indices NOT : {Γ : Con} → Tm Γ (BOOL ⇒ BOOL) NOT = LAM (IF VAR zero THEN FALSE ELSE TRUE) OR : {Γ : Con} → Tm Γ (BOOL ⇒ BOOL ⇒ BOOL) OR = LAM (LAM (IF VAR (suc zero) THEN TRUE ELSE VAR zero)) open import Data.Bool evalTy : Ty → Set evalTy BOOL = Bool evalTy (A ⇒ B) = evalTy A → evalTy B open import Data.Unit open import Data.Product evalCon : Con → Set evalCon ∙ = ⊤ evalCon (Γ ▶ A) = evalCon Γ × evalTy A eval : {Γ : Con}{A : Ty} → Tm Γ A → evalCon Γ → evalTy A eval TRUE ρ = true eval FALSE ρ = false eval (IF t THEN t₁ ELSE t₂) ρ = if eval t ρ then eval t₁ ρ else eval t₂ ρ eval (t $ t₁) ρ = eval t ρ (eval t₁ ρ) eval (LAM t) ρ = λ x → eval t (ρ , x) eval (VAR zero) (ρ , x) = x eval (VAR (suc v)) (ρ , x) = eval (VAR v) ρ ex1 ex2 ex3 : Tm ∙ BOOL ex1 = IF TRUE THEN FALSE ELSE TRUE -- false ex2 = IF TRUE THEN (IF FALSE THEN TRUE ELSE (IF TRUE THEN FALSE ELSE TRUE)) ELSE TRUE -- false ex3 = IF FALSE THEN FALSE ELSE (IF FALSE THEN FALSE ELSE TRUE) -- true eval∙ : {A : Ty} → Tm ∙ A → evalTy A eval∙ t = eval t tt