-
Notifications
You must be signed in to change notification settings - Fork 0
/
htyp-decidable.agda
84 lines (78 loc) · 3.25 KB
/
htyp-decidable.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
open import Nat
open import Prelude
open import core
open import contexts
module htyp-decidable where
arr-htyp-eq : ∀{τ1 τ2 τ3 τ4} →
τ1 ==> τ2 == τ3 ==> τ4 →
τ1 == τ3 × τ2 == τ4
arr-htyp-eq refl = refl , refl
sum-htyp-eq : ∀{τ1 τ2 τ3 τ4} →
τ1 ⊕ τ2 == τ3 ⊕ τ4 →
τ1 == τ3 × τ2 == τ4
sum-htyp-eq refl = refl , refl
prod-htyp-eq : ∀{τ1 τ2 τ3 τ4} →
τ1 ⊠ τ2 == τ3 ⊠ τ4 →
τ1 == τ3 × τ2 == τ4
prod-htyp-eq refl = refl , refl
htyp-dec : (τ1 τ2 : htyp) →
τ1 == τ2 + (τ1 == τ2 → ⊥)
htyp-dec unit unit = Inl refl
htyp-dec unit num = Inr (λ ())
htyp-dec unit (τ3 ==> τ4) = Inr (λ ())
htyp-dec unit (τ3 ⊕ τ4) = Inr (λ ())
htyp-dec unit (τ3 ⊠ τ4) = Inr (λ ())
htyp-dec num unit = Inr (λ ())
htyp-dec num num = Inl refl
htyp-dec num (τ1 ==> τ2) = Inr (λ ())
htyp-dec num (τ1 ⊕ τ2) = Inr (λ ())
htyp-dec num (τ3 ⊠ τ4) = Inr (λ ())
htyp-dec (τ1 ==> τ2) unit = Inr (λ ())
htyp-dec (τ1 ==> τ2) num = Inr (λ ())
htyp-dec (τ1 ==> τ2) (τ3 ==> τ4)
with htyp-dec τ1 τ3 | htyp-dec τ2 τ4
... | Inl refl | Inl refl = Inl refl
... | Inl refl | Inr τ2≠τ4 =
Inr (λ eq → τ2≠τ4 (π2 (arr-htyp-eq eq)))
... | Inr τ1≠τ3 | Inl refl =
Inr (λ eq → τ1≠τ3 (π1 (arr-htyp-eq eq)))
... | Inr τ1≠τ3 | Inr τ2≠τ4 =
Inr (λ eq → τ1≠τ3 (π1 (arr-htyp-eq eq)))
htyp-dec (τ1 ==> τ2) (τ3 ⊕ τ4) = Inr (λ ())
htyp-dec (τ1 ==> τ2) (τ3 ⊠ τ4) = Inr (λ ())
htyp-dec (τ1 ⊕ τ2) unit = Inr (λ ())
htyp-dec (τ1 ⊕ τ2) num = Inr (λ ())
htyp-dec (τ1 ⊕ τ2) (τ3 ==> τ4) = Inr (λ ())
htyp-dec (τ1 ⊕ τ2) (τ3 ⊕ τ4)
with htyp-dec τ1 τ3 | htyp-dec τ2 τ4
... | Inl refl | Inl refl = Inl refl
... | Inl refl | Inr τ2≠τ4 =
Inr (λ eq → τ2≠τ4 (π2 (sum-htyp-eq eq)))
... | Inr τ1≠τ3 | Inl refl =
Inr (λ eq → τ1≠τ3 (π1 (sum-htyp-eq eq)))
... | Inr τ1≠τ3 | Inr τ2≠τ4 =
Inr (λ eq → τ1≠τ3 (π1 (sum-htyp-eq eq)))
htyp-dec (τ1 ⊕ τ2) (τ3 ⊠ τ4) = Inr (λ ())
htyp-dec (τ1 ⊠ τ2) unit = Inr (λ ())
htyp-dec (τ1 ⊠ τ2) num = Inr (λ ())
htyp-dec (τ1 ⊠ τ2) (τ3 ==> τ4) = Inr (λ ())
htyp-dec (τ1 ⊠ τ2) (τ3 ⊕ τ4) = Inr (λ ())
htyp-dec (τ1 ⊠ τ2) (τ3 ⊠ τ4)
with htyp-dec τ1 τ3 | htyp-dec τ2 τ4
... | Inl refl | Inl refl = Inl refl
... | Inl refl | Inr τ2≠τ4 =
Inr (λ eq → τ2≠τ4 (π2 (prod-htyp-eq eq)))
... | Inr τ1≠τ3 | Inl refl =
Inr (λ eq → τ1≠τ3 (π1 (prod-htyp-eq eq)))
... | Inr τ1≠τ3 | Inr τ2≠τ4 =
Inr (λ eq → τ1≠τ3 (π1 (prod-htyp-eq eq)))
htyp-prod-dec : (τ : htyp) →
(Σ[ τ1 ∈ htyp ] Σ[ τ2 ∈ htyp ]
τ == τ1 ⊠ τ2) +
((Σ[ τ1 ∈ htyp ] Σ[ τ2 ∈ htyp ]
τ == τ1 ⊠ τ2) → ⊥)
htyp-prod-dec unit = Inr (λ{(_ , _ , ())})
htyp-prod-dec num = Inr (λ{(_ , _ , ())})
htyp-prod-dec (τ1 ==> τ2) = Inr (λ{(_ , _ , ())})
htyp-prod-dec (τ1 ⊕ τ2) = Inr (λ{(_ , _ , ())})
htyp-prod-dec (τ1 ⊠ τ2) = Inl (τ1 , τ2 , refl)