-
Notifications
You must be signed in to change notification settings - Fork 26
/
goals.tsx
338 lines (294 loc) · 12.9 KB
/
goals.tsx
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
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
/**
* @fileOverview
*
* Mostly copied from https://github.com/leanprover/vscode-lean4/blob/master/lean4-infoview/src/infoview/goals.tsx
*/
import * as React from 'react'
import { InteractiveHypothesisBundle_nonAnonymousNames, MVarId, TaggedText_stripTags } from '@leanprover/infoview-api'
import { EditorContext } from '../../../../node_modules/lean4-infoview/src/infoview/contexts';
import { Locations, LocationsContext, SelectableLocation } from '../../../../node_modules/lean4-infoview/src/infoview/goalLocation';
import { InteractiveCode } from '../../../../node_modules/lean4-infoview/src/infoview/interactiveCode'
import { WithTooltipOnHover } from '../../../../node_modules/lean4-infoview/src/infoview/tooltips';
import { InputModeContext } from './context';
import { InteractiveGoal, InteractiveGoals, InteractiveHypothesisBundle } from './rpc_api';
/** Returns true if `h` is inaccessible according to Lean's default name rendering. */
function isInaccessibleName(h: string): boolean {
return h.indexOf('✝') >= 0;
}
function goalToString(g: InteractiveGoal): string {
let ret = ''
if (g.userName) {
ret += `case ${g.userName}\n`
}
for (const h of g.hyps) {
const names = InteractiveHypothesisBundle_nonAnonymousNames(h).join(' ')
ret += `${names} : ${TaggedText_stripTags(h.type)}`
if (h.val) {
ret += ` := ${TaggedText_stripTags(h.val)}`
}
ret += '\n'
}
ret += `⊢ ${TaggedText_stripTags(g.type)}`
return ret
}
export function goalsToString(goals: InteractiveGoals): string {
return goals.goals.map(goalToString).join('\n\n')
}
interface GoalFilterState {
/** If true reverse the list of hypotheses, if false present the order received from LSP. */
reverse: boolean,
/** If true show hypotheses that have isType=True, otherwise hide them. */
showType: boolean,
/** If true show hypotheses that have isInstance=True, otherwise hide them. */
showInstance: boolean,
/** If true show hypotheses that contain a dagger in the name, otherwise hide them. */
showHiddenAssumption: boolean
/** If true show the bodies of let-values, otherwise hide them. */
showLetValue: boolean;
}
function getFilteredHypotheses(hyps: InteractiveHypothesisBundle[], filter: GoalFilterState): InteractiveHypothesisBundle[] {
return hyps.reduce((acc: InteractiveHypothesisBundle[], h) => {
if (h.isInstance && !filter.showInstance) return acc
if (h.isType && !filter.showType) return acc
const names = filter.showHiddenAssumption ? h.names : h.names.filter(n => !isInaccessibleName(n))
const hNew: InteractiveHypothesisBundle = filter.showLetValue ? { ...h, names } : { ...h, names, val: undefined }
if (names.length !== 0) acc.push(hNew)
return acc
}, [])
}
interface HypProps {
hyp: InteractiveHypothesisBundle
mvarId?: MVarId
}
function Hyp({ hyp: h, mvarId }: HypProps) {
const locs = React.useContext(LocationsContext)
const namecls: string = 'mr1 ' +
(h.isInserted ? 'inserted-text ' : '') +
(h.isRemoved ? 'removed-text ' : '')
const names = InteractiveHypothesisBundle_nonAnonymousNames(h).map((n, i) =>
<span className={namecls + (isInaccessibleName(n) ? 'goal-inaccessible ' : '')} key={i}>
<SelectableLocation
locs={locs}
loc={mvarId && h.fvarIds && h.fvarIds.length > i ?
{ mvarId, loc: { hyp: h.fvarIds[i] }} :
undefined
}
alwaysHighlight={false}
>{n}</SelectableLocation>
</span>)
const typeLocs: Locations | undefined = React.useMemo(() =>
locs && mvarId && h.fvarIds && h.fvarIds.length > 0 ?
{ ...locs, subexprTemplate: { mvarId, loc: { hypType: [h.fvarIds[0], ''] }}} :
undefined,
[locs, mvarId, h.fvarIds])
const valLocs: Locations | undefined = React.useMemo(() =>
h.val && locs && mvarId && h.fvarIds && h.fvarIds.length > 0 ?
{ ...locs, subexprTemplate: { mvarId, loc: { hypValue: [h.fvarIds[0], ''] }}} :
undefined,
[h.val, locs, mvarId, h.fvarIds])
return <div>
<strong className="goal-hyp">{names}</strong>
:
<LocationsContext.Provider value={typeLocs}>
<InteractiveCode fmt={h.type} />
</LocationsContext.Provider>
{h.val &&
<LocationsContext.Provider value={valLocs}>
:= <InteractiveCode fmt={h.val} />
</LocationsContext.Provider>}
</div>
}
interface GoalProps2 {
goals: InteractiveGoal[]
filter: GoalFilterState
}
interface GoalProps {
goal: InteractiveGoal
filter: GoalFilterState
showHints?: boolean
typewriter: boolean
}
interface ProofDisplayProps {
proof: string
}
/**
* Displays the hypotheses, target type and optional case label of a goal according to the
* provided `filter`. */
export const Goal = React.memo((props: GoalProps) => {
const { goal, filter, showHints, typewriter } = props
// TODO: Apparently `goal` can be `undefined`
if (!goal) {return <></>}
const filteredList = getFilteredHypotheses(goal.hyps, filter);
const hyps = filter.reverse ? filteredList.slice().reverse() : filteredList;
const locs = React.useContext(LocationsContext)
const goalLocs = React.useMemo(() =>
locs && goal.mvarId ?
{ ...locs, subexprTemplate: { mvarId: goal.mvarId, loc: { target: '' }}} :
undefined,
[locs, goal.mvarId])
const goalLi = <div key={'goal'}>
<div className="goal-title">Goal: </div>
<LocationsContext.Provider value={goalLocs}>
<InteractiveCode fmt={goal.type} />
</LocationsContext.Provider>
</div>
// let cn = 'font-code tl pre-wrap bl bw1 pl1 b--transparent '
// if (props.goal.isInserted) cn += 'b--inserted '
// if (props.goal.isRemoved) cn += 'b--removed '
// const hints = <Hints hints={goal.hints} key={goal.mvarId} />
const objectHyps = hyps.filter(hyp => !hyp.isAssumption)
const assumptionHyps = hyps.filter(hyp => hyp.isAssumption)
const {typewriterMode} = React.useContext(InputModeContext)
return <div>
{/* {goal.userName && <div><strong className="goal-case">case </strong>{goal.userName}</div>} */}
{filter.reverse && goalLi}
{! typewriter && objectHyps.length > 0 &&
<div className="hyp-group"><div className="hyp-group-title">Objects:</div>
{objectHyps.map((h, i) => <Hyp hyp={h} mvarId={goal.mvarId} key={i} />)}</div> }
{!typewriter && assumptionHyps.length > 0 &&
<div className="hyp-group"><div className="hyp-group-title">Assumptions:</div>
{assumptionHyps.map((h, i) => <Hyp hyp={h} mvarId={goal.mvarId} key={i} />)}</div> }
{/* {typewriter && typewriterMode && <Typewriter />} */}
{!filter.reverse && goalLi}
{/* {showHints && hints} */}
</div>
})
export const MainAssumptions = React.memo((props: GoalProps2) => {
const { goals, filter } = props
const goal = goals[0]
const filteredList = getFilteredHypotheses(goal.hyps, filter);
const hyps = filter.reverse ? filteredList.slice().reverse() : filteredList;
const locs = React.useContext(LocationsContext)
const goalLocs = React.useMemo(() =>
locs && goal.mvarId ?
{ ...locs, subexprTemplate: { mvarId: goal.mvarId, loc: { target: '' }}} :
undefined,
[locs, goal.mvarId])
const goalLi = <div key={'goal'}>
<div className="goal-title">Goal: </div>
<LocationsContext.Provider value={goalLocs}>
<InteractiveCode fmt={goal.type} />
</LocationsContext.Provider>
</div>
const objectHyps = hyps.filter(hyp => !hyp.isAssumption)
const assumptionHyps = hyps.filter(hyp => hyp.isAssumption)
return <div id="main-assumptions">
<div className="goals-section-title">Current Goal</div>
{filter.reverse && goalLi}
{ objectHyps.length > 0 &&
<div className="hyp-group"><div className="hyp-group-title">Objects:</div>
{objectHyps.map((h, i) => <Hyp hyp={h} mvarId={goal.mvarId} key={i} />)}</div> }
{ assumptionHyps.length > 0 &&
<div className="hyp-group">
<div className="hyp-group-title">Assumptions:</div>
{assumptionHyps.map((h, i) => <Hyp hyp={h} mvarId={goal.mvarId} key={i} />)}
</div> }
</div>
})
export const OtherGoals = React.memo((props: GoalProps2) => {
const { goals, filter } = props
return <>
{goals && goals.length > 1 &&
<div id="other-goals" className="other-goals">
<div className="goals-section-title">Further Goals</div>
{goals.slice(1).map((goal, i) =>
<details key={i}>
<summary>
<InteractiveCode fmt={goal.type} />
</summary>
<Goal typewriter={false} filter={filter} goal={goal} />
</details>)}
</div>}
</>
})
// TODO: deprecated
export const ProofDisplay = React.memo((props : ProofDisplayProps) => {
const { proof } = props
const steps = proof.match(/.+/g)
return <>
{ steps &&
<div id="current-proof">
<div className="goals-section-title">Proof history</div>
<div className="proof-display-wrapper">
<div className="proof-display">
{steps.map((s) =>
<div>{s}</div>
)}
</div>
</div>
</div>}
</>
})
interface GoalsProps {
goals: InteractiveGoals
filter: GoalFilterState
}
export function Goals({ goals, filter }: GoalsProps) {
if (goals.goals.length === 0) {
return <>No goals</>
} else {
return <>
{goals.goals.map((g, i) => <Goal typewriter={false} key={i} goal={g} filter={filter} />)}
</>
}
}
interface FilteredGoalsProps {
/** Components to render in the header. */
headerChildren: React.ReactNode
/**
* When this is `undefined`, the component will not appear at all but will remember its state
* by virtue of still being mounted in the React tree. When it does appear again, the filter
* settings and collapsed state will be as before. */
goals?: InteractiveGoals
}
/**
* Display goals together with a header containing the provided children as well as buttons
* to control how the goals are displayed.
*/
export const FilteredGoals = React.memo(({ headerChildren, goals }: FilteredGoalsProps) => {
const ec = React.useContext(EditorContext)
const copyToCommentButton =
<a className="link pointer mh2 dim codicon codicon-quote"
data-id="copy-goal-to-comment"
onClick={e => {
e.preventDefault();
if (goals) void ec.copyToComment(goalsToString(goals))
}}
title="copy state to comment" />
const [goalFilters, setGoalFilters] = React.useState<GoalFilterState>(
{ reverse: false, showType: true, showInstance: true, showHiddenAssumption: true, showLetValue: true });
const sortClasses = 'link pointer mh2 dim codicon ' + (goalFilters.reverse ? 'codicon-arrow-up ' : 'codicon-arrow-down ');
const sortButton =
<a className={sortClasses} title="reverse list"
onClick={_ => setGoalFilters(s => ({ ...s, reverse: !s.reverse }))} />
const mkFilterButton = (filterFn: React.SetStateAction<GoalFilterState>, filledFn: (_: GoalFilterState) => boolean, name: string) =>
<a className='link pointer tooltip-menu-content' onClick={_ => { setGoalFilters(filterFn) }}>
<span className={'tooltip-menu-icon codicon ' + (filledFn(goalFilters) ? 'codicon-check ' : 'codicon-blank ')}> </span>
<span className='tooltip-menu-text '>{name}</span>
</a>
const filterMenu = <span>
{mkFilterButton(s => ({ ...s, showType: !s.showType }), gf => gf.showType, 'types')}
<br/>
{mkFilterButton(s => ({ ...s, showInstance: !s.showInstance }), gf => gf.showInstance, 'instances')}
<br/>
{mkFilterButton(s => ({ ...s, showHiddenAssumption: !s.showHiddenAssumption }), gf => gf.showHiddenAssumption, 'hidden assumptions')}
<br/>
{mkFilterButton(s => ({ ...s, showLetValue: !s.showLetValue }), gf => gf.showLetValue, 'let-values')}
</span>
const isFiltered = !goalFilters.showInstance || !goalFilters.showType || !goalFilters.showHiddenAssumption || !goalFilters.showLetValue
const filterButton =
<WithTooltipOnHover mkTooltipContent={() => filterMenu}>
<a className={'link pointer mh2 dim codicon ' + (isFiltered ? 'codicon-filter-filled ': 'codicon-filter ')}/>
</WithTooltipOnHover>
return <div style={{display: goals !== undefined ? 'block' : 'none'}}>
<details open>
<summary className='mv2 pointer'>
{headerChildren}
<span className='fr'>{copyToCommentButton}{sortButton}{filterButton}</span>
</summary>
<div className='ml1'>
{goals && <Goals goals={goals} filter={goalFilters}></Goals>}
</div>
</details>
</div>
})