679 lines
17 KiB
Markdown
679 lines
17 KiB
Markdown
---
|
||
title : "Exam: TSPL Exam file"
|
||
layout : page
|
||
permalink : /TSPL/2019/Exam/
|
||
---
|
||
|
||
|
||
```
|
||
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.
|
||
|
||
### (a)
|
||
|
||
### (b)
|
||
|
||
|
||
## 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
|
||
|
||
```
|
||
record Gas : Set where
|
||
constructor gas
|
||
field
|
||
amount : ℕ
|
||
|
||
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)
|
||
```
|