-
Notifications
You must be signed in to change notification settings - Fork 0
/
ccg.agda
78 lines (59 loc) · 2.14 KB
/
ccg.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
module ccg where
record ⊤ : Set where constructor tt
data ⊥ : Set where
data mod : Set where
∙ ◆ × ★ : mod
data Dec (P : Set) : Set where
yes : P → Dec P
no : (P → ⊥) → Dec P
_≤_ : mod → mod → Set
∙ ≤ n = ⊤
◆ ≤ ◆ = ⊤
◆ ≤ ★ = ⊤
× ≤ × = ⊤
× ≤ ★ = ⊤
★ ≤ ★ = ⊤
_ ≤ _ = ⊥
_≤?_ : (m n : mod) → Dec (m ≤ n)
∙ ≤? n = yes tt
◆ ≤? ∙ = no (λ z → z)
◆ ≤? ◆ = yes tt
◆ ≤? × = no (λ z → z)
◆ ≤? ★ = yes tt
× ≤? ∙ = no (λ z → z)
× ≤? ◆ = no (λ z → z)
× ≤? × = yes tt
× ≤? ★ = yes tt
★ ≤? ∙ = no (λ z → z)
★ ≤? ◆ = no (λ z → z)
★ ≤? × = no (λ z → z)
★ ≤? ★ = yes tt
_∨_ : (m n : mod) → mod
m ∨ n with m ≤? n
... | yes p = m
... | no np = n
data syn (b : Set) : Set where
⟨_⟩ : b → syn _
_/[_]_ : (t : syn b) (m : mod) (s : syn b) → syn _
_\[_]_ : (t : syn b) (m : mod) (s : syn b) → syn _
module Terms {b : Set} (lex : syn b → Set) where
data trm_ : syn b → Set where
-- embedding of lexical items
[_] : ∀ {s} → lex s → trm s
-- forward application
_>_ : ∀ {s t m} → trm t /[ m ] s → trm s → trm t
-- backward application
_<_ : ∀ {s t m} → trm s → trm t \[ m ] s → trm t
-- forward harmonic composition
_>B_ : ∀ {x y z m n} {_ : ◆ ≤ m} {_ : ◆ ≤ n} → trm x /[ m ] y → trm y /[ n ] z → trm x /[ m ∨ n ] z
-- backward harmonic composition
_<B_ : ∀ {x y z m n} {_ : ◆ ≤ m} {_ : ◆ ≤ n} → trm y \[ m ] z → trm x \[ n ] y → trm x \[ n ∨ m ] z
-- forward crossed composition
_>B×_ : ∀ {x y z m n} {_ : × ≤ m} {_ : × ≤ n} → trm x /[ m ] y → trm y \[ n ] z → trm x \[ m ∨ n ] z
-- backward crossed composition
_<B×_ : ∀ {x y z m n} {_ : × ≤ m} {_ : × ≤ n} → trm y /[ m ] z → trm x \[ n ] y → trm x /[ n ∨ m ] z
-- forward type raising
_>T_ : ∀ {x} → trm x → ∀ {y} → trm y /[ ★ ] (y \[ ★ ] x)
-- backward type raising
_<T_ : ∀ {x} → trm x → ∀ {y} → trm y \[ ★ ] (y /[ ★ ] x)
infixl 9 trm_