-- Agda tutorial at FLOPS 2016
-- Andreas Abel (partially plagiarized from Ulf Norell's ICFP 2013 talk)
-- 2016-03-06

-- Prelude

-- Basic types

data ℕ : Set where
  zero : ℕ
  suc  : (n : ℕ) → ℕ

data List (A : Set) : Set where
  []  : List A
  _∷_ : (x : A) (xs : List A) → List A

-- Basic propositions

-- Truth

record ⊤ : Set where

-- Absurdity

data ⊥ : Set where

⊥-elim : {A : Set} → ⊥ → A
⊥-elim = {!!}

¬ : (A : Set) → Set
¬ A = A → ⊥

-- Decidable propositions

data Dec (P : Set) : Set where

-- Equality

data _≡_ {A : Set} (x : A) : A → Set where
  refl : x ≡ x

_≢_ : {A : Set} (x y : A) → Set
x ≢ y = ¬ (x ≡ y)

-- Simply-typed lambda-calculus

-- Types

data Ty : Set where
  base : Ty
  _⇒_ : (a b : Ty) → Ty

-- Type equality is propositional equality

-- Injectivity properties

⇒≠base : ∀{a b} → (a ⇒ b) ≡ base → ⊥
⇒≠base = {!!}

⇒injl : ∀{a b c d} → (a ⇒ c) ≡ (b ⇒ d) → a ≡ b
⇒injl = {!!}

⇒injr : ∀{a b c d} → (a ⇒ c) ≡ (b ⇒ d) → c ≡ d
⇒injr = {!!}

-- Deciding type equality

eqTy : (a b : Ty) → Dec (a ≡ b)
eqTy = {!!}

-- Raw de Bruijn terms

data Exp : Set where

-- Well typed well-scoped variables

Cxt = List Ty

data Var : ∀(Γ : Cxt) (x : ℕ) (a : Ty) → Set where

-- Bidirectional calculus

mutual
  data Ne (Γ : Cxt) : (e : Exp) (b : Ty) → Set where

  data Nf (Γ : Cxt) : (e : Exp) (a : Ty) → Set where

-- Sound context lookup

data Lookup (Γ : Cxt) (n : ℕ) : Set where

lookupVar : ∀ Γ (x : ℕ) → Lookup Γ x
lookupVar = {!!}

-- Sound type checking

-- Result of type checking

data Infer (Γ : Cxt) (e : Exp) : Set where

data Check (Γ : Cxt) (e : Exp) (a : Ty) : Set where

-- Inference rules

-- Variable

inferVar : {!!}
inferVar = {!!}

-- Application

inferApp : {!!}
inferApp = {!!}

-- nfView

data Inferable : Exp → Set where

data NfView : Exp → Set where

nfView : (e : Exp) → NfView e
nfView e = {!!}

-- Checking rules

-- Neutrals

  checkNe : {!!}
checkNe = {!!}

-- Abstraction

checkAbs : {!!}
checkAbs = {!!}

-- Sound type-checker

mutual
  check : ∀ Γ e a → Check Γ e a
  check Γ e a = {!!}

  infer : ∀ Γ e → Infer Γ e
  infer Γ e = {!!}