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
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
|
local M = {}
local domain = require("clever_f.domain")
local text_topology = require("clever_f.text_topology")
local function same(expected, actual, message)
if expected ~= actual then
error((message or "invariant failed")
.. ": expected " .. tostring(expected)
.. ", got " .. tostring(actual), 3)
end
end
local function same_map_values(expected, actual, excluded, message)
for key, value in pairs(expected) do
if key ~= excluded then
same(value, actual[key], message .. " for " .. key.key)
end
end
for key, value in pairs(actual) do
if key ~= excluded then
same(expected[key], value, message .. " for " .. key.key)
end
end
end
local function resolved_action(options)
if options.action == "RepeatSameDirection"
or options.action == "RepeatOppositeDirection"
then
return options.coordinator:last_explicit_resolution()
end
if options.action == "DotRepeat" then
return nil
end
return options.coordinator:last_primary_resolution()
end
local function assert_valid_endpoint(options)
local outcome = options.outcome
if outcome.search_outcome == nil or outcome.successful_steps == 0 then
return
end
local view = options.before_view
if not text_topology.TextView.is(view) then
error("landing invariant requires the pre-action TextView", 3)
end
if not view:is_valid_cursor_position(outcome.search_outcome.endpoint) then
error("a reached landing must be a valid byte-start position", 3)
end
end
local function assert_success_history(options, before, after, context)
local outcome = options.outcome
if outcome.search_outcome == nil then
return
end
local before_landing = before.previous_landing[context]
local after_landing = after.previous_landing[context]
if outcome.complete then
same(
outcome.search_outcome.endpoint,
after_landing,
"a complete move must commit its reached landing"
)
same(false, after.first_move[context], "a complete move must finish first_move")
if context.visual then
same(
before.moved_forward,
after.moved_forward,
"a Visual move must preserve command direction"
)
same(
before.moved_forward_initialized,
after.moved_forward_initialized,
"a Visual move must preserve direction initialization"
)
else
local moved_forward = domain.Position.compare(
outcome.search_outcome.endpoint,
options.origin
) > 0
same(
moved_forward,
after.moved_forward,
"a complete command move must commit its direction"
)
same(true, after.moved_forward_initialized, "command direction must be initialized")
end
else
same(
before_landing,
after_landing,
"an incomplete move must preserve its successful landing"
)
same(
before.moved_forward,
after.moved_forward,
"an incomplete move must preserve command direction"
)
same(
before.moved_forward_initialized,
after.moved_forward_initialized,
"an incomplete move must preserve direction initialization"
)
end
end
local function assert_context_partition(options, before, after, context)
if options.action == "Reset" or options.action == "DiagnosticFullReset" then
return
end
same_map_values(
before.previous_descriptor,
after.previous_descriptor,
context,
"an action must preserve peer descriptors"
)
same_map_values(
before.previous_landing,
after.previous_landing,
context,
"an action must preserve peer landings"
)
same_map_values(
before.first_move,
after.first_move,
context,
"an action must preserve peer first-move values"
)
same_map_values(
before.previous_target,
after.previous_target,
context,
"an action must preserve peer targets"
)
end
local function assert_family(options, after, context, resolution)
if options.outcome.effective_descriptor == nil then
return
end
local initiating = after.previous_descriptor[context]
if initiating == nil then
return
end
same(
initiating.family,
options.outcome.effective_descriptor.family,
"effective motion family must come from the initiating descriptor"
)
if resolution ~= nil and resolution.motion_plan ~= nil then
same(
initiating.family,
resolution.motion_plan.descriptor.family,
"resolved motion family must come from the initiating descriptor"
)
end
end
local function assert_overlay_plans(options, resolution)
if resolution == nil or resolution.target_plan == nil then
return
end
local requests = options.feedback:persistent_requests()
for index = options.persistent_request_count + 1, #requests do
same(
resolution.target_plan,
requests[index].target_plan,
"a new persistent overlay must use the action TargetPlan"
)
end
end
local function assert_timer_owner(options, after)
local identity = after.highlight_timer
if identity == nil then
return
end
local timers = options.host:timers()
local timer = timers[identity]
if timer == nil or not timer.active then
error("the current timer identity must name the sole active cleanup timer", 3)
end
local active = 0
for _, candidate in pairs(timers) do
if candidate.active then
active = active + 1
end
end
same(1, active, "only the current cleanup timer can remain active")
end
local function assert_temporary_ownership(options, after)
same(0, #after.temporary_overlays, "an action must release temporary overlay ownership")
for _, highlight in pairs(options.host:highlights()) do
if highlight.group == "CleverFCursor" or highlight.group == "CleverFDirect" then
error("an action must release each temporary presentation resource", 3)
end
end
end
function M.after_action(options)
if type(options) ~= "table"
or not domain.ActionOutcome.is(options.outcome)
or type(options.host) ~= "table"
or type(options.coordinator) ~= "table"
or type(options.feedback) ~= "table"
or type(options.before_state) ~= "table"
then
error("action invariants require a complete observation", 2)
end
local context = domain.ModeContext.from_full_mode(options.mode)
local after = options.state:snapshot()
assert_valid_endpoint(options)
assert_success_history(options, options.before_state, after, context)
assert_context_partition(options, options.before_state, after, context)
local resolution = resolved_action(options)
assert_family(options, after, context, resolution)
assert_overlay_plans(options, resolution)
assert_timer_owner(options, after)
assert_temporary_ownership(options, after)
return true
end
return M
|
