module ICFP where
open import ICFPPrelude
data Type : Set where
nat : Type
_⇒_ : (a b : Type) → Type
infixr 7 _⇒_
data Raw : Set where
var : (n : Nat) → Raw
app : (e₁ e₂ : Raw) → Raw
lam : (a : Type) (e : Raw) → Raw
data Cxt : Set where
[] : Cxt
_,_ : (Γ : Cxt) (a : Type) → Cxt
data Var : Cxt → Type → Set where
zero : ∀ {Γ a} → Var (Γ , a) a
suc : ∀ {Γ a b} → Var Γ a → Var (Γ , b) a
data Term : Cxt → Type → Set where
var : ∀ {Γ a} → Var Γ a → Term Γ a
app : ∀ {Γ a b} (u : Term Γ (a ⇒ b)) (v : Term Γ a) →
Term Γ b
lam : ∀ {Γ} a {b} (u : Term (Γ , a) b) → Term Γ (a ⇒ b)
eraseVar : ∀ {Γ a} → Var Γ a → Nat
eraseVar zero = zero
eraseVar (suc x) = suc (eraseVar x)
erase : ∀ {Γ a} → Term Γ a → Raw
erase (var x) = var (eraseVar x)
erase (app v v₁) = app (erase v) (erase v₁)
erase (lam a v) = lam a (erase v)
data _≠_ : Type → Type → Set where
nat≠fun : ∀ {a b} → nat ≠ a ⇒ b
fun≠nat : ∀ {a b} → a ⇒ b ≠ nat
src≠ : ∀ {a a′ b c} → a ≠ a′ → a ⇒ b ≠ a′ ⇒ c
tgt≠ : ∀ {a b c c′} → c ≠ c′ → a ⇒ c ≠ b ⇒ c′
sound : ∀ a → a ≠ a → ⊥
sound nat ()
sound (a ⇒ b) (src≠ x) = sound a x
sound (a ⇒ b) (tgt≠ x) = sound b x
infix 4 _≠_ _≟_
data _≟_ : Type → Type → Set where
equal : ∀ {a} → a ≟ a
not-equal : ∀ {a b} → a ≠ b → a ≟ b
compareFun : ∀ {a b c d} → a ≟ b → c ≟ d → a ⇒ c ≟ b ⇒ d
compareFun equal equal = equal
compareFun equal (not-equal x) = not-equal (tgt≠ x)
compareFun (not-equal x) q = not-equal (src≠ x)
compare : ∀ a b → a ≟ b
compare nat nat = equal
compare nat (a ⇒ b) = not-equal nat≠fun
compare (a ⇒ b) nat = not-equal fun≠nat
compare (a ⇒ b) (a₁ ⇒ b₁) = compareFun (compare a a₁) (compare b b₁)
data OutOfScope : Cxt → Nat → Set where
oops : ∀ {n} → OutOfScope [] n
suc : ∀ {Γ a n} → OutOfScope Γ n → OutOfScope (Γ , a) (suc n)
data WellScoped? : Cxt → Nat → Set where
yes : ∀ {Γ} a (x : Var Γ a) → WellScoped? Γ (eraseVar x)
no : ∀ {Γ n} → OutOfScope Γ n → WellScoped? Γ n
data TypeError : Cxt → Raw → Set where
arg-mismatch : ∀ {a a′ Γ b} {u : Term Γ (a ⇒ b)} {u₁ : Term Γ a′} →
a ≠ a′ → TypeError Γ (app (erase u) (erase u₁))
not-fun : ∀ {Γ} {u : Term Γ nat} {a₁} {u₁ : Term Γ a₁} →
TypeError Γ (app (erase u) (erase u₁))
bad-arg : ∀ {Γ e₂ e₁} → TypeError Γ e₂ → TypeError Γ (app e₁ e₂)
bad-fun : ∀ {Γ e₁ e₂} → TypeError Γ e₁ → TypeError Γ (app e₁ e₂)
out-of-scope : ∀ {Γ n} → OutOfScope Γ n → TypeError Γ (var n)
lam : ∀ {Γ e} a → TypeError (Γ , a) e → TypeError Γ (lam a e)
data WellTyped? : Cxt → Raw → Set where
yes : ∀ {Γ} a (u : Term Γ a) → WellTyped? Γ (erase u)
no : ∀ {Γ e} (err : TypeError Γ e) → WellTyped? Γ e
checkApp : ∀ {Γ e₁ e₂} → WellTyped? Γ e₁ → WellTyped? Γ e₂ →
WellTyped? Γ (app e₁ e₂)
checkApp (yes nat u) (yes a₁ u₁) = no not-fun
checkApp (yes (a ⇒ b) u) (yes a′ u₁) with compare a a′
checkApp (yes (a ⇒ b) u) (yes .a u₁) | equal = yes b (app u u₁)
checkApp (yes (a ⇒ b) u) (yes a′ u₁) | not-equal err = no (arg-mismatch err)
checkApp (yes a u) (no err) = no (bad-arg err)
checkApp (no err) (yes a u) = no (bad-fun err)
checkApp (no err) (no err₁) = no (bad-arg err₁)
lookupSuc : ∀ {Γ a n} →
WellScoped? Γ n → WellScoped? (Γ , a) (suc n)
lookupSuc (yes a₁ x) = yes a₁ (suc x)
lookupSuc (no x) = no (suc x)
lookupVar : ∀ Γ n → WellScoped? Γ n
lookupVar [] n = no oops
lookupVar (Γ , a) zero = yes a zero
lookupVar (Γ , a) (suc n) = lookupSuc (lookupVar Γ n)
checkVar : ∀ {Γ n} → WellScoped? Γ n → WellTyped? Γ (var n)
checkVar (yes a x) = yes a (var x)
checkVar (no x) = no (out-of-scope x)
checkLam : ∀ {Γ e} a → WellTyped? (Γ , a) e → WellTyped? Γ (lam a e)
checkLam a (yes a₁ u) = yes (a ⇒ a₁) (lam a u)
checkLam a (no err) = no (lam a err)
check : ∀ Γ e → WellTyped? Γ e
check Γ (var n) = checkVar (lookupVar Γ n)
check Γ (app e₁ e₂) = checkApp (check Γ e₁) (check Γ e₂)
check Γ (lam a e) = checkLam a (check (Γ , a) e)