/
Typecheck.agda
105 lines (93 loc) · 4.41 KB
/
Typecheck.agda
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
open import Relation.Binary
open import Relation.Binary.PropositionalEquality
module STLC.Typecheck {U : Set} (UEq : IsDecEquivalence {A = U} _≡_) where
open import STLC.Typing U
open import STLC.Bound Type
open import STLC.Embedded as E hiding (Expr; Ctxt)
open IsDecEquivalence UEq using (_≟_)
open import Data.Nat hiding (_≟_)
open import Data.Fin
open import Data.Vec
open import Function using (_∘_; _$_)
open import Data.Product
open import STLC.Utils
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality
el-inj : ∀ {A B} → el A ≡ el B → A ≡ B
el-inj refl = refl
arr-injˡ : ∀ {τ τ′ τ₂ τ₂′} → τ ↣ τ₂ ≡ τ′ ↣ τ₂′ → τ ≡ τ′
arr-injˡ refl = refl
arr-injʳ : ∀ {τ τ′ τ″} → τ ↣ τ′ ≡ τ ↣ τ″ → τ′ ≡ τ″
arr-injʳ refl = refl
_T≟_ : (τ τ′ : Type) → Dec (τ ≡ τ′)
el A T≟ el B with A ≟ B
el A T≟ el .A | yes refl = yes refl
el A T≟ el B | no A≢B = no (A≢B ∘ el-inj)
el A T≟ (_ ↣ _) = no (λ ())
(τ₁ ↣ τ₂) T≟ el B = no (λ ())
(τ₁ ↣ τ₂) T≟ (τ₁′ ↣ τ₂′) with τ₁ T≟ τ₁′
(τ₁ ↣ τ₂) T≟ (τ₁′ ↣ τ₂′) | no ¬p = no (¬p ∘ arr-injˡ)
(τ₁ ↣ τ₂) T≟ (.τ₁ ↣ τ₂′) | yes refl with τ₂ T≟ τ₂′
(τ₁ ↣ τ₂) T≟ (.τ₁ ↣ .τ₂) | yes refl | yes refl = yes refl
(τ₁ ↣ τ₂) T≟ (.τ₁ ↣ τ₂′) | yes refl | no ¬p = no (¬p ∘ arr-injʳ)
⊢-inj : ∀ {n Γ} {E : Expr n} → ∀ {τ τ′} → Γ ⊢ E ∶ τ → Γ ⊢ E ∶ τ′ → τ ≡ τ′
⊢-inj tVar tVar = refl
⊢-inj {E = lam τ E} (tLam t) (tLam t′) = cong (_↣_ τ) (⊢-inj t t′)
⊢-inj (t₁ · t₂) (t₁′ · t₂′) with ⊢-inj t₁ t₁′
⊢-inj (t₁ · t₂) (t₁′ · t₂′) | refl with ⊢-inj t₂ t₂′
⊢-inj (t₁ · t₂) (t₁′ · t₂′) | refl | refl = refl
lam-injˡ : ∀ {n τ₁ τ₂ τ} {Γ : Ctxt n} {E : Expr (suc n)} →
Γ ⊢ lam τ E ∶ (τ₁ ↣ τ₂) → τ₁ ≡ τ
lam-injˡ (tLam t) = refl
mutual
infer : ∀ {n} Γ (E : Expr n) → Dec (∃[ τ ] Γ ⊢ E ∶ τ)
infer Γ (var x) = yes (lookup x Γ , tVar)
infer Γ (lam τ E) with infer (τ ∷ Γ) E
infer Γ (lam τ E) | yes (τ′ , E∷τ′) = yes (τ ↣ τ′ , tLam E∷τ′)
infer Γ (lam τ E) | no ¬p = no lem
where
lem : ∄[ τ′ ] Γ ⊢ lam τ E ∶ τ′
lem (el A , ())
lem (.τ ↣ _ , tLam t) = ¬p (_ , t)
infer Γ (E · F) with infer Γ E
infer Γ (E · F) | yes (el A , t) = no lem
where
lem : ∄[ τ ] Γ ⊢ E · F ∶ τ
lem (_ , t₁ · _) with ⊢-inj t t₁
lem (_ , t₁ · _) | ()
infer Γ (E · F) | yes (τ₁ ↣ τ₂ , tE) with check Γ F τ₁
infer Γ (E · F) | yes (τ₁ ↣ τ₂ , tE) | yes tF = yes (τ₂ , tE · tF)
infer Γ (E · F) | yes (τ₁ ↣ τ₂ , tE) | no ¬p = no lem
where
lem : ∄[ τ ] Γ ⊢ E · F ∶ τ
lem (_ , t₁ · _) with ⊢-inj t₁ tE
lem (.τ₂ , _ · t₂) | refl = ¬p t₂
infer Γ (E · F) | no ¬p = no lem
where
lem : ∄[ τ ] Γ ⊢ E · F ∶ τ
lem (_ , t · _) = ¬p (_ , t)
check : ∀ {n} Γ (E : Expr n) → ∀ τ → Dec (Γ ⊢ E ∶ τ)
check Γ (var x) τ with lookup x Γ T≟ τ
check Γ (var x) .(lookup x Γ) | yes refl = yes tVar
check Γ (var x) τ | no ¬p = no (¬p ∘ ⊢-inj tVar)
check Γ (lam τ′ E) (el A) = no (λ ())
check Γ (lam τ′ E) (τ₁ ↣ τ₂) with τ₁ T≟ τ′
check Γ (lam τ′ E) (.τ′ ↣ τ₂) | yes refl with check (τ′ ∷ Γ) E τ₂
check Γ (lam τ′ E) (.τ′ ↣ τ₂) | yes refl | yes t = yes (tLam t)
check Γ (lam τ′ E) (.τ′ ↣ τ₂) | yes refl | no ¬p = no lem
where
lem : ¬ Γ ⊢ lam τ′ E ∶ τ′ ↣ τ₂
lem (tLam t) = ¬p t
check Γ (lam τ′ E) (τ₁ ↣ τ₂) | no ¬p = no (¬p ∘ lam-injˡ)
check Γ (E · F) τ with infer Γ F
check Γ (E · F) τ | yes (τ′ , F∷τ′) with check Γ E (τ′ ↣ τ)
check Γ (E · F) τ | yes (τ′ , F∷τ′) | yes E∷τ′↣τ = yes (E∷τ′↣τ · F∷τ′)
check Γ (E · F) τ | yes (τ′ , F∷τ′) | no ¬p = no lem
where
lem : ¬ Γ ⊢ E · F ∶ τ
lem (_·_ {τ = τ₀} t t′) with ⊢-inj F∷τ′ t′
lem (t · t′) | refl = ¬p t
check Γ (E · F) τ | no ¬tF = no lem
where
lem : ¬ Γ ⊢ E · F ∶ τ
lem (_·_ {τ = τ} t t′) = ¬tF (τ , t′)