-
Notifications
You must be signed in to change notification settings - Fork 1
/
reachability.agda
198 lines (184 loc) · 9.97 KB
/
reachability.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
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
open import Nat
open import Prelude
open import List
open import core
open import judgemental-erase
open import checks
open import moveerase
open import sensibility
module reachability where
-- algorithmically, we break reachability into two halves: first you
-- produce a list of actions that are all "move parent" to pull the cursor
-- to the very top of the expression in question. then, you go back down
-- into the expression with a sequence of move firstChild and move
-- nextSibs as appropriate. the append of these two lists will reach from
-- one expression to the other.
--
-- there may well be a shorter list of actions that does the same thing;
-- the expression with top-level cursor may not be the Least Common
-- Ancestor in the expression tree of the given pair. however, the work
-- of this less minimal thing and corresponding size of the proof term is
-- still bounded linearly by the size of the expression, and is far
-- easier to maniupulate judgementally.
reachup-type : {t : τ̂} {t' : τ̇} →
erase-t t t' →
Σ[ L ∈ List action ] (runtype t L (▹ t' ◃) × movements L)
reachup-type ETTop = [] , DoRefl , AM[]
reachup-type (ETArrL er) with reachup-type er
... | (l , ih , m ) = l ++ [ move parent ] ,
runtype++ (ziplem-tmarr1 ih) (DoType TMArrParent1 DoRefl) ,
movements++ m (AM:: AM[])
reachup-type (ETArrR er) with reachup-type er
... | (l , ih , m ) = l ++ [ move parent ] ,
runtype++ (ziplem-tmarr2 ih) (DoType TMArrParent2 DoRefl) ,
movements++ m (AM:: AM[])
mutual
reachup-synth : {Γ : ·ctx} {e : ê} {t : τ̇} {e' : ė} →
erase-e e e' →
Γ ⊢ e' => t →
Σ[ L ∈ List action ] (runsynth Γ e t L ▹ e' ◃ t × movements L)
reachup-synth (EELam _) ()
reachup-synth EETop _ = [] , DoRefl , AM[]
reachup-synth (EEAscL er) (SAsc x) with reachup-ana er x
... | l , ih , m = l ++ [ move parent ] ,
runsynth++ (ziplem-asc1 ih) (DoSynth (SAMove EMAscParent1) DoRefl) ,
movements++ m (AM:: AM[])
reachup-synth (EEAscR er) (SAsc x₁) with reachup-type er
... | l , ih , m = l ++ [ move parent ] ,
runsynth++ {L1 = l} (ziplem-moves-asc2 m er x₁ ih) (DoSynth (SAMove EMAscParent2) DoRefl) ,
movements++ m (AM:: AM[])
reachup-synth (EEApL er) (SAp wt x x₁) with reachup-synth er wt
... | l , ih , m = l ++ [ move parent ] ,
runsynth++ {L1 = l} (ziplem-moves-ap1 (lem-erase-synth er wt) x x₁ m ih) (DoSynth (SAMove EMApParent1) DoRefl) ,
movements++ m (AM:: AM[])
reachup-synth (EEApR er) (SAp wt x x₁) with reachup-ana er x₁
... | l , ih , m = l ++ [ move parent ] ,
runsynth++ (ziplem-ap2 wt x ih) (DoSynth (SAMove EMApParent2) DoRefl) ,
movements++ m (AM:: AM[])
reachup-synth (EEPlusL er) (SPlus x x₁) with reachup-ana er x
... | l , ih , m = l ++ [ move parent ] ,
runsynth++ (ziplem-plus1 ih) (DoSynth (SAMove EMPlusParent1) DoRefl) ,
movements++ m (AM:: AM[])
reachup-synth (EEPlusR er) (SPlus x x₁) with reachup-ana er x₁
... | l , ih , m = l ++ [ move parent ] ,
runsynth++ (ziplem-plus2 ih) (DoSynth (SAMove EMPlusParent2) DoRefl) ,
movements++ m (AM:: AM[])
reachup-synth (EENEHole er) (SNEHole wt) with reachup-synth er wt
... | l , ih , m = l ++ [ move parent ] ,
runsynth++ (ziplem-nehole-a (lem-erase-synth er wt) ih) (DoSynth (SAMove EMNEHoleParent) DoRefl) ,
movements++ m (AM:: AM[])
reachup-ana : {Γ : ·ctx} {e : ê} {t : τ̇} {e' : ė} →
erase-e e e' →
Γ ⊢ e' <= t →
Σ[ L ∈ List action ] (runana Γ e L ▹ e' ◃ t × movements L)
reachup-ana EETop _ = [] , DoRefl , AM[]
reachup-ana er (ASubsume x x₁) with reachup-synth er x
... | l , ih , m = l ,
synthana-moves (lem-erase-synth er x) m x₁ ih ,
m
reachup-ana (EELam er) (ALam x₁ x₂ wt) with reachup-ana er wt
... | l , ih , m = l ++ [ move parent ] ,
runana++ (ziplem-lam x₁ x₂ ih) (DoAna (AAMove EMLamParent) DoRefl) ,
movements++ m (AM:: AM[])
--------------------------
reachdown-type : {t : τ̇} {t' : τ̂} → (p : erase-t t' t) →
Σ[ L ∈ List action ] (runtype (▹ t ◃) L t' × movements L)
reachdown-type ETTop = [] , DoRefl , AM[]
reachdown-type (ETArrL er) with reachdown-type er
... | (l , ih , m ) = move (child 1) :: l ,
DoType TMArrChild1 (ziplem-tmarr1 ih) ,
AM:: m
reachdown-type (ETArrR er) with reachdown-type er
... | (l , ih , m ) = move (child 2) :: l ,
DoType TMArrChild2 (ziplem-tmarr2 ih) ,
AM:: m
mutual
reachdown-synth : {Γ : ·ctx} {e : ê} {t : τ̇} {e' : ė} →
(p : erase-e e e') →
(wt : Γ ⊢ e' => t) →
Σ[ L ∈ List action ] (runsynth Γ ▹ e' ◃ t L e t × movements L)
reachdown-synth (EELam _) ()
reachdown-synth EETop _ = [] , DoRefl , AM[]
reachdown-synth (EEAscL er) (SAsc x) with reachdown-ana er x
... | l , ih , m = move (child 1) :: l ,
DoSynth (SAMove EMAscChild1) (ziplem-asc1 ih) ,
AM:: m
reachdown-synth (EEAscR er) (SAsc x₁) with reachdown-type er
... | l , ih , m = move (child 2) :: l ,
DoSynth (SAMove EMAscChild2) (ziplem-moves-asc2 m ETTop x₁ ih) ,
AM:: m
reachdown-synth (EEApL er) (SAp wt x x₁) with reachdown-synth er wt
... | l , ih , m = move (child 1) :: l ,
DoSynth (SAMove EMApChild1) (ziplem-moves-ap1 wt x x₁ m ih) ,
AM:: m
reachdown-synth (EEApR er) (SAp wt x x₁) with reachdown-ana er x₁
... | l , ih , m = move (child 2) :: l ,
DoSynth (SAMove EMApChild2) (ziplem-ap2 wt x ih) ,
AM:: m
reachdown-synth (EEPlusL er) (SPlus x x₁) with reachdown-ana er x
... | l , ih , m = move (child 1) :: l ,
DoSynth (SAMove EMPlusChild1) (ziplem-plus1 ih) ,
AM:: m
reachdown-synth (EEPlusR er) (SPlus x x₁) with reachdown-ana er x₁
... | l , ih , m = move (child 2) :: l ,
DoSynth (SAMove EMPlusChild2) (ziplem-plus2 ih) ,
AM:: m
reachdown-synth (EENEHole er) (SNEHole wt) with reachdown-synth er wt
... | l , ih , m = move (child 1) :: l ,
DoSynth (SAMove EMNEHoleChild1) (ziplem-nehole-a wt ih) ,
AM:: m
reachdown-ana : {Γ : ·ctx} {e : ê} {t : τ̇} {e' : ė} →
(p : erase-e e e') →
(wt : Γ ⊢ e' <= t) →
Σ[ L ∈ List action ] (runana Γ ▹ e' ◃ L e t × movements L)
reachdown-ana EETop _ = [] , DoRefl , AM[]
reachdown-ana er (ASubsume x x₁) with reachdown-synth er x
... | l , ih , m = l ,
synthana-moves x m x₁ ih ,
m
reachdown-ana (EELam er) (ALam x₁ x₂ wt) with reachdown-ana er wt
... | l , ih , m = move (child 1) :: l ,
DoAna (AAMove EMLamChild1) (ziplem-lam x₁ x₂ ih) ,
AM:: m
--------------------------
-- this is the final statement of the reachability triplet. the movement
-- between judgemental and metafunctional erasure happens internally to
-- theses statements to present a consistent interface with the text of
-- the paper, while also allowing easy pattern matching in the proofs.
--
-- the intuition for these statements is that the cursor cannot change
-- the type of things because the typing judgement is defined on the
-- cursor-erased terms and types.
reachability-types : (t1 t2 : τ̂) → (t1 ◆t) == (t2 ◆t) →
Σ[ L ∈ List action ] (runtype t1 L t2 × movements L)
reachability-types t1 t2 eq
with ◆erase-t t1 (t2 ◆t) eq | ◆erase-t t2 (t1 ◆t) (! eq)
... | er1 | er2 with reachup-type er1 | reachdown-type er2
... | (lup , rup , mvup) | (ldwn , rdwn , mvdwn) =
lup ++ ldwn ,
runtype++ rup (tr (λ x → runtype ▹ x ◃ ldwn t2) eq rdwn) ,
movements++ mvup mvdwn
reachability-synth : (Γ : ·ctx) (t : τ̇) (e1 e2 : ê) →
Γ ⊢ e1 ◆e => t →
e1 ◆e == e2 ◆e →
Σ[ L ∈ List action ] (runsynth Γ e1 t L e2 t × movements L)
reachability-synth Γ t e1 e2 wt1 eq
with ◆erase-e e1 (e2 ◆e) eq | ◆erase-e e2 (e1 ◆e) (! eq)
... | er1 | er2 with reachup-synth er1 (tr (λ x → Γ ⊢ x => t) eq wt1)
| reachdown-synth er2 wt1
... | (lup , rup , mvup) | (ldwn , rdwn , mvdwn) =
(lup ++ ldwn) ,
runsynth++ rup (tr (λ x → runsynth Γ ▹ x ◃ t ldwn e2 t) eq rdwn) ,
movements++ mvup mvdwn
reachability-ana : (Γ : ·ctx) (t : τ̇) (e1 e2 : ê) →
Γ ⊢ e1 ◆e <= t →
e1 ◆e == e2 ◆e →
Σ[ L ∈ List action ] (runana Γ e1 L e2 t × movements L)
reachability-ana Γ t e1 e2 wt1 eq
with ◆erase-e e1 (e2 ◆e) eq | ◆erase-e e2 (e1 ◆e) (! eq)
... | er1 | er2 with reachup-ana er1 (tr (λ x → Γ ⊢ x <= t) eq wt1)
| reachdown-ana er2 wt1
... | (lup , rup , mvup) | (ldwn , rdwn , mvdwn) =
lup ++ ldwn ,
(runana++ rup (tr (λ x → runana Γ ▹ x ◃ ldwn e2 t) eq rdwn)) ,
(movements++ mvup mvdwn)