Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Multi-expression selection #275

Merged
merged 13 commits into from
Jan 15, 2023
Merged

Multi-expression selection #275

Show file tree
Hide file tree
Changes from 12 commits
Commits
Show all changes
13 commits
Select commit Hold shift + click to select a range
eab4711
doc: update some docs
Vtec234 Dec 13, 2022
d38e48a
refactor: move state down into goal component
Vtec234 Dec 14, 2022
d528800
feat: collapsible `case`s
Vtec234 Dec 14, 2022
f9cef2a
feat: multi-expression contexts
Vtec234 Dec 17, 2022
4fe0946
fix: selection fixes
Vtec234 Dec 18, 2022
35bf7a8
feat: match new goal types
Vtec234 Dec 18, 2022
049843a
feat: make names selectable
Vtec234 Dec 18, 2022
4ca3d7f
chore: lint
Vtec234 Dec 18, 2022
c43cb36
feat: fix many bugs and memoize
Vtec234 Dec 19, 2022
10932c2
fix: React prop
Vtec234 Dec 19, 2022
b501559
feat: export dynamic importer
Vtec234 Jan 10, 2023
3c26b0a
chore: bump package versions
Vtec234 Jan 13, 2023
f63862e
fix: ensure InteractiveCode uses code font
Vtec234 Jan 14, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
16 changes: 8 additions & 8 deletions lean4-infoview-api/package-lock.json
View file
Open in desktop

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

2 changes: 1 addition & 1 deletion lean4-infoview-api/package.json
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
{
"name": "@leanprover/infoview-api",
"version": "0.2.0",
"version": "0.2.1",
"description": "Types and API for @leanprover/infoview.",
"scripts": {
"watch": "tsc --watch",
Expand Down
59 changes: 36 additions & 23 deletions lean4-infoview-api/src/rpcApi.ts
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -22,9 +22,12 @@ export type DiffTag =
| 'wasDeleted' | 'willDelete'
| 'wasInserted' | 'willInsert'

// This is an arbitrary-size `Nat` in Lean which in JS we represent as `string`
export type SubexprPos = string

export interface SubexprInfo {
info: InfoWithCtx
subexprPos?: number
subexprPos?: SubexprPos
diffStatus?: DiffTag
}

Expand All @@ -38,37 +41,47 @@ export interface InfoPopup {
doc?: string
}

export type FVarId = string
export type MVarId = string

export interface InteractiveHypothesisBundle {
isInstance?: boolean,
isType?: boolean,
/** The pretty names of the variables in the bundle.
* If the name is inaccessible this will be `"[anonymous]"`.
* Use `InteractiveHypothesis_accessibleNames` to filter these out.
*/
/** The pretty names of the variables in the bundle. Anonymous names are rendered
* as `"[anonymous]"` whereas inaccessible ones have a `✝` appended at the end.
* Use `InteractiveHypothesisBundle_nonAnonymousNames` to filter anonymouse ones out. */
names: string[]
/** The free variable id associated with each of the vars listed in `names`. */
fvarIds?: string[]
/** Present since server version 1.1.2. */
fvarIds?: FVarId[]
type: CodeWithInfos
val?: CodeWithInfos
/** If true, the hypothesis was not present on the previous tactic state. */
isInserted?: boolean;
/** If true, the hypothesis will be deleted on the next tactic state. */
isRemoved?: boolean;
isInstance?: boolean
isType?: boolean
isInserted?: boolean
isRemoved?: boolean
}

export interface InteractiveGoal {
export type ContextInfo = RpcPtr<'Lean.Elab.ContextInfo'>
export type TermInfo = RpcPtr<'Lean.Elab.TermInfo'>

export interface InteractiveGoalCore {
hyps: InteractiveHypothesisBundle[]
type: CodeWithInfos
/** Present since server version 1.1.2. */
ctx?: ContextInfo
}

export interface InteractiveGoal extends InteractiveGoalCore {
userName?: string
goalPrefix?: string
/** metavariable id associated with the goal.
* This is undefined when the goal is a term goal
* or if we are using an older version of lean. */
mvarId?: string
/** If true, the goal was not present on the previous tactic state. */
isInserted?: boolean;
/** If true, the goal will be deleted on the next tactic state. */
isRemoved?: boolean;
/** Present since server version 1.1.2. */
mvarId?: MVarId
isInserted?: boolean
isRemoved?: boolean
}

export interface InteractiveTermGoal extends InteractiveGoalCore {
range?: Range
/** Present since server version 1.1.2. */
term?: TermInfo
}

export interface InteractiveGoals {
Expand All @@ -79,7 +92,7 @@ export function getInteractiveGoals(rs: RpcSessionAtPos, pos: TextDocumentPositi
return rs.call('Lean.Widget.getInteractiveGoals', pos);
}

export function getInteractiveTermGoal(rs: RpcSessionAtPos, pos: TextDocumentPositionParams): Promise<InteractiveGoal | undefined> {
export function getInteractiveTermGoal(rs: RpcSessionAtPos, pos: TextDocumentPositionParams): Promise<InteractiveTermGoal | undefined> {
return rs.call('Lean.Widget.getInteractiveTermGoal', pos);
}

Expand Down
2 changes: 2 additions & 0 deletions lean4-infoview-api/src/rpcSessions.ts
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -148,6 +148,8 @@ class RpcSessionForFile {
try {
const result = await this.sessions.iface.call({ method, params, sessionId, ... pos });
this.registerRefs(result);
// HACK: most of our types are `T | undefined` so try to return something matching that interface
if (result === null) return undefined;
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is there a reason we can't just use T | null in the interface types instead?

Copy link
Member Author

@Vtec234 Vtec234 Jan 14, 2023 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We could, but this is the least invasive change which doesn't require all downstream code to check for !== null (or use truthish checks). IMO this is justified because null vs undefined is one of the many bizarre parts of JS with unclear semantics and it is easier to stick to always using undefined.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

One concrete case where this pops up is with getInteractiveGoals.

{ goals: await getInteractiveGoals(...) }
-- where { goals?: InteractiveGoals }

If we keep null, then the easy fix would be to add a ?? undefined to the use site. But converting null to undefined seems convenient as well.

Note that we run into exactly the same issue with Option Foo, where the ToJson instance produces null. For consistency it might be better to avoid any special case hacks here (since it gives the incorrect impression that T | undefined is the correct RPC API for Option T).

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ahhh, you correctly point out that our entire RPC API is wrong. We serialize structure fields marked with the magic ? as missing similarly to Serde's skip_serializing_if. In JS accessing those fields gives undefined. But we cannot do this for top-level values as there is only a null but no undefined in JSON. For example

structure Foo where
  a? : Option String
  b  : Option String
  deriving ToJson

/- {"b": null} -/
#eval toJson { a? := none, b := none : Foo }

so all the top-level Option SomeResponse calls really return T | null. In this case I guess we should go through the whole API and adjust it, and make a breaking release. Let's do this in another PR however, and temporarily keep the hack.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Sounds good to me.

return result;
} catch (ex: any) {
if (ex?.code === RpcErrorCode.WorkerCrashed || ex?.code === RpcErrorCode.WorkerExited ||
Expand Down
5 changes: 3 additions & 2 deletions lean4-infoview-api/src/util.ts
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,6 @@
import { InteractiveHypothesisBundle, TaggedText } from './rpcApi'

/** Reduce a `TaggedText` into its text contents without tags. */
export function TaggedText_stripTags<T>(tt: TaggedText<T>): string {
const go = (t: TaggedText<T>): string => {
if ('append' in t)
Expand All @@ -13,7 +14,7 @@ export function TaggedText_stripTags<T>(tt: TaggedText<T>): string {
return go(tt)
}

/** Filter out inaccessible / anonymous pretty names from the names list. */
export function InteractiveHypothesisBundle_accessibleNames(ih : InteractiveHypothesisBundle) : string[] {
/** Filter out anonymous pretty names from the names list. */
export function InteractiveHypothesisBundle_nonAnonymousNames(ih : InteractiveHypothesisBundle) : string[] {
return ih.names.filter(x => !x.includes('[anonymous]'))
}
Loading