module Exam where


IMPORTANT For ease of marking, when modifying the given code please write

-- begin
-- end


before and after code you add, to indicate your changes.

## Imports

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; sym; trans; cong; _≢_)
open import Data.Empty using (⊥; ⊥-elim)
open import Data.Nat using (ℕ; zero; suc)
open import Data.List using (List; []; _∷_; _++_)
open import Data.Product using (∃; ∃-syntax) renaming (_,_ to ⟨_,_⟩)
open import Data.String using (String; _≟_)
open import Relation.Nullary using (¬_; Dec; yes; no)
open import Relation.Binary using (Decidable)


## Problem 1

module Problem1 where

open import Function using (_∘_)


Remember to indent all code by two spaces.

## Problem 2

Remember to indent all code by two spaces.

module Problem2 where


### Infix declarations

  infix  4 _⊢_
infix  4 _∋_
infixl 5 _,_

infixr 7 _⇒_

infix  5 ƛ_
infix  5 μ_
infixl 7 _·_
infix  8 suc_
infix  9 _
infix  9 S_
infix  9 #_


### Types and contexts

  data Type : Set where
_⇒_   : Type → Type → Type
ℕ    : Type

data Context : Set where
∅   : Context
_,_ : Context → Type → Context


### Variables and the lookup judgment

  data _∋_ : Context → Type → Set where

Z : ∀ {Γ A}
----------
→ Γ , A ∋ A

S_ : ∀ {Γ A B}
→ Γ ∋ A
---------
→ Γ , B ∋ A


### Terms and the typing judgment

  data _⊢_ : Context → Type → Set where

_ : ∀ {Γ} {A}
→ Γ ∋ A
------
→ Γ ⊢ A

ƛ_  :  ∀ {Γ} {A B}
→ Γ , A ⊢ B
----------
→ Γ ⊢ A ⇒ B

_·_ : ∀ {Γ} {A B}
→ Γ ⊢ A ⇒ B
→ Γ ⊢ A
----------
→ Γ ⊢ B

zero : ∀ {Γ}
----------
→ Γ ⊢ ℕ

suc_ : ∀ {Γ}
→ Γ ⊢ ℕ
-------
→ Γ ⊢ ℕ

case : ∀ {Γ A}
→ Γ ⊢ ℕ
→ Γ ⊢ A
→ Γ , ℕ ⊢ A
-----------
→ Γ ⊢ A

μ_ : ∀ {Γ A}
→ Γ , A ⊢ A
----------
→ Γ ⊢ A


### Abbreviating de Bruijn indices

  lookup : Context → ℕ → Type
lookup (Γ , A) zero     =  A
lookup (Γ , _) (suc n)  =  lookup Γ n
lookup ∅       _        =  ⊥-elim impossible
where postulate impossible : ⊥

count : ∀ {Γ} → (n : ℕ) → Γ ∋ lookup Γ n
count {Γ , _} zero     =  Z
count {Γ , _} (suc n)  =  S (count n)
count {∅}     _        =  ⊥-elim impossible
where postulate impossible : ⊥

#_ : ∀ {Γ} → (n : ℕ) → Γ ⊢ lookup Γ n
# n  =   count n


### Renaming

  ext : ∀ {Γ Δ} → (∀ {A} → Γ ∋ A → Δ ∋ A)
-----------------------------------
→ (∀ {A B} → Γ , B ∋ A → Δ , B ∋ A)
ext ρ Z      =  Z
ext ρ (S x)  =  S (ρ x)

rename : ∀ {Γ Δ}
→ (∀ {A} → Γ ∋ A → Δ ∋ A)
------------------------
→ (∀ {A} → Γ ⊢ A → Δ ⊢ A)
rename ρ ( x)          =   (ρ x)
rename ρ (ƛ N)          =  ƛ (rename (ext ρ) N)
rename ρ (L · M)        =  (rename ρ L) · (rename ρ M)
rename ρ (zero)        =  zero
rename ρ (suc M)       =  suc (rename ρ M)
rename ρ (case L M N)   =  case (rename ρ L) (rename ρ M) (rename (ext ρ) N)
rename ρ (μ N)          =  μ (rename (ext ρ) N)


### Simultaneous Substitution

  exts : ∀ {Γ Δ} → (∀ {A} → Γ ∋ A → Δ ⊢ A)
----------------------------------
→ (∀ {A B} → Γ , B ∋ A → Δ , B ⊢ A)
exts σ Z      =   Z
exts σ (S x)  =  rename S_ (σ x)

subst : ∀ {Γ Δ}
→ (∀ {A} → Γ ∋ A → Δ ⊢ A)
------------------------
→ (∀ {A} → Γ ⊢ A → Δ ⊢ A)
subst σ ( k)          =  σ k
subst σ (ƛ N)          =  ƛ (subst (exts σ) N)
subst σ (L · M)        =  (subst σ L) · (subst σ M)
subst σ (zero)        =  zero
subst σ (suc M)       =  suc (subst σ M)
subst σ (case L M N)   =  case (subst σ L) (subst σ M) (subst (exts σ) N)
subst σ (μ N)          =  μ (subst (exts σ) N)


### Single substitution

  _[_] : ∀ {Γ A B}
→ Γ , B ⊢ A
→ Γ ⊢ B
---------
→ Γ ⊢ A
_[_] {Γ} {A} {B} N M =  subst {Γ , B} {Γ} σ {A} N
where
σ : ∀ {A} → Γ , B ∋ A → Γ ⊢ A
σ Z      =  M
σ (S x)  =   x


### Values

  data Value : ∀ {Γ A} → Γ ⊢ A → Set where

V-ƛ : ∀ {Γ A B} {N : Γ , A ⊢ B}
---------------------------
→ Value (ƛ N)

V-zero : ∀ {Γ}
-----------------
→ Value (zero {Γ})

V-suc : ∀ {Γ} {V : Γ ⊢ ℕ}
→ Value V
--------------
→ Value (suc V)


### Reduction

  infix 2 _—→_

data _—→_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where

ξ-·₁ : ∀ {Γ A B} {L L′ : Γ ⊢ A ⇒ B} {M : Γ ⊢ A}
→ L —→ L′
-----------------
→ L · M —→ L′ · M

ξ-·₂ : ∀ {Γ A B} {V : Γ ⊢ A ⇒ B} {M M′ : Γ ⊢ A}
→ Value V
→ M —→ M′
--------------
→ V · M —→ V · M′

β-ƛ : ∀ {Γ A B} {N : Γ , A ⊢ B} {W : Γ ⊢ A}
→ Value W
-------------------
→ (ƛ N) · W —→ N [ W ]

ξ-suc : ∀ {Γ} {M M′ : Γ ⊢ ℕ}
→ M —→ M′
----------------
→ suc M —→ suc M′

ξ-case : ∀ {Γ A} {L L′ : Γ ⊢ ℕ} {M : Γ ⊢ A} {N : Γ , ℕ ⊢ A}
→ L —→ L′
--------------------------
→ case L M N —→ case L′ M N

β-zero :  ∀ {Γ A} {M : Γ ⊢ A} {N : Γ , ℕ ⊢ A}
-------------------
→ case zero M N —→ M

β-suc : ∀ {Γ A} {V : Γ ⊢ ℕ} {M : Γ ⊢ A} {N : Γ , ℕ ⊢ A}
→ Value V
-----------------------------
→ case (suc V) M N —→ N [ V ]

β-μ : ∀ {Γ A} {N : Γ , A ⊢ A}
---------------
→ μ N —→ N [ μ N ]


### Reflexive and transitive closure

  infix  2 _—↠_
infix  1 begin_
infixr 2 _—→⟨_⟩_
infix  3 _∎

data _—↠_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where

_∎ : ∀ {Γ A} (M : Γ ⊢ A)
--------
→ M —↠ M

_—→⟨_⟩_ : ∀ {Γ A} (L : Γ ⊢ A) {M N : Γ ⊢ A}
→ L —→ M
→ M —↠ N
---------
→ L —↠ N

begin_ : ∀ {Γ} {A} {M N : Γ ⊢ A}
→ M —↠ N
------
→ M —↠ N
begin M—↠N = M—↠N


### Progress

  data Progress {A} (M : ∅ ⊢ A) : Set where

step : ∀ {N : ∅ ⊢ A}
→ M —→ N
-------------
→ Progress M

done :
Value M
----------
→ Progress M

progress : ∀ {A} → (M : ∅ ⊢ A) → Progress M
progress ( ())
progress (ƛ N)                          =  done V-ƛ
progress (L · M) with progress L
...    | step L—→L′                     =  step (ξ-·₁ L—→L′)
...    | done V-ƛ with progress M
...        | step M—→M′                 =  step (ξ-·₂ V-ƛ M—→M′)
...        | done VM                    =  step (β-ƛ VM)
progress (zero)                        =  done V-zero
progress (suc M) with progress M
...    | step M—→M′                     =  step (ξ-suc M—→M′)
...    | done VM                        =  done (V-suc VM)
progress (case L M N) with progress L
...    | step L—→L′                     =  step (ξ-case L—→L′)
...    | done V-zero                    =  step (β-zero)
...    | done (V-suc VL)                =  step (β-suc VL)
progress (μ N)                          =  step (β-μ)


### Evaluation

  data Gas : Set where
gas : ℕ → Gas

data Finished {Γ A} (N : Γ ⊢ A) : Set where

done :
Value N
----------
→ Finished N

out-of-gas :
----------
Finished N

data Steps : ∀ {A} → ∅ ⊢ A → Set where

steps : ∀ {A} {L N : ∅ ⊢ A}
→ L —↠ N
→ Finished N
----------
→ Steps L

eval : ∀ {A}
→ Gas
→ (L : ∅ ⊢ A)
-----------
→ Steps L
eval (gas zero)    L                     =  steps (L ∎) out-of-gas
eval (gas (suc m)) L with progress L
... | done VL                            =  steps (L ∎) (done VL)
... | step {M} L—→M with eval (gas m) M
...    | steps M—↠N fin                  =  steps (L —→⟨ L—→M ⟩ M—↠N) fin


## Problem 3

Remember to indent all code by two spaces.

module Problem3 where


### Imports

  import plfa.part2.DeBruijn as DB


### Syntax

  infix   4  _∋_⦂_
infix   4  _⊢_↑_
infix   4  _⊢_↓_
infixl  5  _,_⦂_

infix   5  ƛ_⇒_
infix   5  μ_⇒_
infix   6  _↑
infix   6  _↓_
infixl  7  _·_
infix   8  suc_
infix   9  _


### Types

  data Type : Set where
_⇒_   : Type → Type → Type
ℕ    : Type


### Identifiers

  Id : Set
Id = String


### Contexts

  data Context : Set where
∅     : Context
_,_⦂_ : Context → Id → Type → Context


### Terms

  data Term⁺ : Set
data Term⁻ : Set

data Term⁺ where
_                        : Id → Term⁺
_·_                       : Term⁺ → Term⁻ → Term⁺
_↓_                       : Term⁻ → Type → Term⁺

data Term⁻ where
ƛ_⇒_                     : Id → Term⁻ → Term⁻
zero                    : Term⁻
suc_                    : Term⁻ → Term⁻
case_[zero⇒_|suc_⇒_]    : Term⁺ → Term⁻ → Id → Term⁻ → Term⁻
μ_⇒_                     : Id → Term⁻ → Term⁻
_↑                       : Term⁺ → Term⁻


### Lookup

  data _∋_⦂_ : Context → Id → Type → Set where

Z : ∀ {Γ x A}
--------------------
→ Γ , x ⦂ A ∋ x ⦂ A

S : ∀ {Γ x y A B}
→ x ≢ y
→ Γ ∋ x ⦂ A
-----------------
→ Γ , y ⦂ B ∋ x ⦂ A


### Bidirectional type checking

  data _⊢_↑_ : Context → Term⁺ → Type → Set
data _⊢_↓_ : Context → Term⁻ → Type → Set

data _⊢_↑_ where

⊢ : ∀ {Γ A x}
→ Γ ∋ x ⦂ A
-----------
→ Γ ⊢  x ↑ A

_·_ : ∀ {Γ L M A B}
→ Γ ⊢ L ↑ A ⇒ B
→ Γ ⊢ M ↓ A
-------------
→ Γ ⊢ L · M ↑ B

⊢↓ : ∀ {Γ M A}
→ Γ ⊢ M ↓ A
---------------
→ Γ ⊢ (M ↓ A) ↑ A

data _⊢_↓_ where

⊢ƛ : ∀ {Γ x N A B}
→ Γ , x ⦂ A ⊢ N ↓ B
-------------------
→ Γ ⊢ ƛ x ⇒ N ↓ A ⇒ B

⊢zero : ∀ {Γ}
--------------
→ Γ ⊢ zero ↓ ℕ

⊢suc : ∀ {Γ M}
→ Γ ⊢ M ↓ ℕ
---------------
→ Γ ⊢ suc M ↓ ℕ

⊢case : ∀ {Γ L M x N A}
→ Γ ⊢ L ↑ ℕ
→ Γ ⊢ M ↓ A
→ Γ , x ⦂ ℕ ⊢ N ↓ A
-------------------------------------
→ Γ ⊢ case L [zero⇒ M |suc x ⇒ N ] ↓ A

⊢μ : ∀ {Γ x N A}
→ Γ , x ⦂ A ⊢ N ↓ A
-----------------
→ Γ ⊢ μ x ⇒ N ↓ A

⊢↑ : ∀ {Γ M A B}
→ Γ ⊢ M ↑ A
→ A ≡ B
-------------
→ Γ ⊢ (M ↑) ↓ B


### Type equality

  _≟Tp_ : (A B : Type) → Dec (A ≡ B)
ℕ      ≟Tp ℕ              =  yes refl
ℕ      ≟Tp (A ⇒ B)         =  no λ()
(A ⇒ B) ≟Tp ℕ              =  no λ()
(A ⇒ B) ≟Tp (A′ ⇒ B′)
with A ≟Tp A′ | B ≟Tp B′
...  | no A≢    | _         =  no λ{refl → A≢ refl}
...  | yes _    | no B≢     =  no λ{refl → B≢ refl}
...  | yes refl | yes refl  =  yes refl


### Prerequisites

  dom≡ : ∀ {A A′ B B′} → A ⇒ B ≡ A′ ⇒ B′ → A ≡ A′
dom≡ refl = refl

rng≡ : ∀ {A A′ B B′} → A ⇒ B ≡ A′ ⇒ B′ → B ≡ B′
rng≡ refl = refl

ℕ≢⇒ : ∀ {A B} → ℕ ≢ A ⇒ B
ℕ≢⇒ ()


### Unique lookup

  uniq-∋ : ∀ {Γ x A B} → Γ ∋ x ⦂ A → Γ ∋ x ⦂ B → A ≡ B
uniq-∋ Z Z                 =  refl
uniq-∋ Z (S x≢y _)         =  ⊥-elim (x≢y refl)
uniq-∋ (S x≢y _) Z         =  ⊥-elim (x≢y refl)
uniq-∋ (S _ ∋x) (S _ ∋x′)  =  uniq-∋ ∋x ∋x′


### Unique synthesis

  uniq-↑ : ∀ {Γ M A B} → Γ ⊢ M ↑ A → Γ ⊢ M ↑ B → A ≡ B
uniq-↑ (⊢ ∋x) (⊢ ∋x′)       =  uniq-∋ ∋x ∋x′
uniq-↑ (⊢L · ⊢M) (⊢L′ · ⊢M′)  =  rng≡ (uniq-↑ ⊢L ⊢L′)
uniq-↑ (⊢↓ ⊢M) (⊢↓ ⊢M′)       =  refl


## Lookup type of a variable in the context

  ext∋ : ∀ {Γ B x y}
→ x ≢ y
→ ¬ ∃[ A ]( Γ ∋ x ⦂ A )
-----------------------------
→ ¬ ∃[ A ]( Γ , y ⦂ B ∋ x ⦂ A )
ext∋ x≢y _  ⟨ A , Z ⟩       =  x≢y refl
ext∋ _   ¬∃ ⟨ A , S _ ⊢x ⟩  =  ¬∃ ⟨ A , ⊢x ⟩

lookup : ∀ (Γ : Context) (x : Id)
-----------------------
→ Dec (∃[ A ](Γ ∋ x ⦂ A))
lookup ∅ x                        =  no  (λ ())
lookup (Γ , y ⦂ B) x with x ≟ y
... | yes refl                    =  yes ⟨ B , Z ⟩
... | no x≢y with lookup Γ x
...             | no  ¬∃          =  no  (ext∋ x≢y ¬∃)
...             | yes ⟨ A , ⊢x ⟩  =  yes ⟨ A , S x≢y ⊢x ⟩


### Promoting negations

  ¬arg : ∀ {Γ A B L M}
→ Γ ⊢ L ↑ A ⇒ B
→ ¬ Γ ⊢ M ↓ A
-------------------------
→ ¬ ∃[ B′ ](Γ ⊢ L · M ↑ B′)
¬arg ⊢L ¬⊢M ⟨ B′ , ⊢L′ · ⊢M′ ⟩ rewrite dom≡ (uniq-↑ ⊢L ⊢L′) = ¬⊢M ⊢M′

¬switch : ∀ {Γ M A B}
→ Γ ⊢ M ↑ A
→ A ≢ B
---------------
→ ¬ Γ ⊢ (M ↑) ↓ B
¬switch ⊢M A≢B (⊢↑ ⊢M′ A′≡B) rewrite uniq-↑ ⊢M ⊢M′ = A≢B A′≡B


## Synthesize and inherit types

  synthesize : ∀ (Γ : Context) (M : Term⁺)
-----------------------
→ Dec (∃[ A ](Γ ⊢ M ↑ A))

inherit : ∀ (Γ : Context) (M : Term⁻) (A : Type)
---------------
→ Dec (Γ ⊢ M ↓ A)

synthesize Γ ( x) with lookup Γ x
... | no  ¬∃              =  no  (λ{ ⟨ A , ⊢ ∋x ⟩ → ¬∃ ⟨ A , ∋x ⟩ })
... | yes ⟨ A , ∋x ⟩      =  yes ⟨ A , ⊢ ∋x ⟩
synthesize Γ (L · M) with synthesize Γ L
... | no  ¬∃              =  no  (λ{ ⟨ _ , ⊢L  · _  ⟩  →  ¬∃ ⟨ _ , ⊢L ⟩ })
... | yes ⟨ ℕ ,    ⊢L ⟩  =  no  (λ{ ⟨ _ , ⊢L′ · _  ⟩  →  ℕ≢⇒ (uniq-↑ ⊢L ⊢L′) })
... | yes ⟨ A ⇒ B , ⊢L ⟩ with inherit Γ M A
...    | no  ¬⊢M          =  no  (¬arg ⊢L ¬⊢M)
...    | yes ⊢M           =  yes ⟨ B , ⊢L · ⊢M ⟩
synthesize Γ (M ↓ A) with inherit Γ M A
... | no  ¬⊢M             =  no  (λ{ ⟨ _ , ⊢↓ ⊢M ⟩  →  ¬⊢M ⊢M })
... | yes ⊢M              =  yes ⟨ A , ⊢↓ ⊢M ⟩

inherit Γ (ƛ x ⇒ N) ℕ      =  no  (λ())
inherit Γ (ƛ x ⇒ N) (A ⇒ B) with inherit (Γ , x ⦂ A) N B
... | no ¬⊢N                =  no  (λ{ (⊢ƛ ⊢N)  →  ¬⊢N ⊢N })
... | yes ⊢N                =  yes (⊢ƛ ⊢N)
inherit Γ zero ℕ          =  yes ⊢zero
inherit Γ zero (A ⇒ B)     =  no  (λ())
inherit Γ (suc M) ℕ with inherit Γ M ℕ
... | no ¬⊢M                =  no  (λ{ (⊢suc ⊢M)  →  ¬⊢M ⊢M })
... | yes ⊢M                =  yes (⊢suc ⊢M)
inherit Γ (suc M) (A ⇒ B)  =  no  (λ())
inherit Γ (case L [zero⇒ M |suc x ⇒ N ]) A with synthesize Γ L
... | no ¬∃                 =  no  (λ{ (⊢case ⊢L  _ _) → ¬∃ ⟨ ℕ , ⊢L ⟩})
... | yes ⟨ _ ⇒ _ , ⊢L ⟩    =  no  (λ{ (⊢case ⊢L′ _ _) → ℕ≢⇒ (uniq-↑ ⊢L′ ⊢L) })
... | yes ⟨ ℕ ,    ⊢L ⟩ with inherit Γ M A
...    | no ¬⊢M             =  no  (λ{ (⊢case _ ⊢M _) → ¬⊢M ⊢M })
...    | yes ⊢M with inherit (Γ , x ⦂ ℕ) N A
...       | no ¬⊢N          =  no  (λ{ (⊢case _ _ ⊢N) → ¬⊢N ⊢N })
...       | yes ⊢N          =  yes (⊢case ⊢L ⊢M ⊢N)
inherit Γ (μ x ⇒ N) A with inherit (Γ , x ⦂ A) N A
... | no ¬⊢N                =  no  (λ{ (⊢μ ⊢N) → ¬⊢N ⊢N })
... | yes ⊢N                =  yes (⊢μ ⊢N)
inherit Γ (M ↑) B with synthesize Γ M
... | no  ¬∃                =  no  (λ{ (⊢↑ ⊢M _) → ¬∃ ⟨ _ , ⊢M ⟩ })
... | yes ⟨ A , ⊢M ⟩ with A ≟Tp B
...   | no  A≢B             =  no  (¬switch ⊢M A≢B)
...   | yes A≡B             =  yes (⊢↑ ⊢M A≡B)
`