-
Notifications
You must be signed in to change notification settings - Fork 42
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
1 parent
c199947
commit a0edece
Showing
33 changed files
with
5,688 additions
and
740 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,154 @@ | ||
| import * as React from 'react'; | ||
| import { InteractiveGoal, InteractiveHypothesisBundle } from '../Defs'; | ||
| import { useTranslation } from 'react-i18next'; | ||
| import { InteractiveCode, InteractiveHypothesisBundle_nonAnonymousNames, LocationsContext, SubexprInfo, TaggedText } from '@leanprover/infoview'; | ||
| import { SelectableLocation } from '../../../../../node_modules/lean4-infoview/src/infoview/goalLocation'; | ||
|
|
||
| /** Returns true if `h` is inaccessible according to Lean's default name rendering. */ | ||
| function isInaccessibleName(h: string): boolean { | ||
| return h.indexOf('✝') >= 0; | ||
| } | ||
|
|
||
| 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; | ||
| } | ||
|
|
||
| interface HypProps { | ||
| hyp: InteractiveHypothesisBundle | ||
| mvarId?: any // 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 as InteractiveHypothesisBundle).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> | ||
| // } | ||
|
|
||
| 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 GoalProps { | ||
| goal: InteractiveGoal | ||
| filter: GoalFilterState | ||
| showHints?: boolean | ||
| typewriter: boolean | ||
| unbundle?: boolean /** unbundle `x y : Nat` into `x : Nat` and `y : Nat` */ | ||
| } | ||
|
|
||
| /** | ||
| * 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, unbundle } = props | ||
| let { t } = useTranslation() | ||
|
|
||
| // 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'} className="goal"> | ||
| {/* <div className="goal-title">{t("Goal")}:</div> */} | ||
| <LocationsContext.Provider value={goalLocs}> | ||
| <InteractiveCode fmt={goal.type as TaggedText<SubexprInfo>} /> | ||
| </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 ' | ||
|
|
||
| function unbundleHyps (hyps: InteractiveHypothesisBundle[]) : InteractiveHypothesisBundle[] { | ||
| return hyps.flatMap(hyp => ( | ||
| unbundle ? hyp.names.map(name => {return {...hyp, names: [name]}}) : [hyp] | ||
| )) | ||
| } | ||
|
|
||
| // const hints = <Hints hints={goal.hints} key={goal.mvarId} /> | ||
| const objectHyps = unbundleHyps(hyps.filter(hyp => !hyp.isAssumption)) | ||
| const assumptionHyps = unbundleHyps(hyps.filter(hyp => hyp.isAssumption)) | ||
|
|
||
| return <> | ||
| {/* {goal.userName && <div><strong className="goal-case">case </strong>{goal.userName}</div>} */} | ||
| {filter.reverse && goalLi} | ||
| <div className="hypotheses"> | ||
| {! typewriter && objectHyps.length > 0 && | ||
| <div className="hyp-group"><div className="hyp-group-title">{t("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">{t("Assumptions")}:</div> | ||
| {assumptionHyps.map((h, i) => <Hyp hyp={h} mvarId={goal.mvarId} key={i} />)}</div> } | ||
| </div> | ||
| {!filter.reverse && <> | ||
| <div className='goal-sign'> | ||
| <svg width="100%" height="100%"> | ||
| <line x1="0%" y1="0%" x2="0%" y2="100%" /> | ||
| <line x1="0%" y1="50%" x2="100%" y2="50%" /> | ||
| </svg> | ||
| </div> | ||
| {goalLi} | ||
| </>} | ||
| {/* {showHints && hints} */} | ||
| </> | ||
| }) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,36 @@ | ||
| import * as React from 'react'; | ||
| import { useTranslation } from "react-i18next"; | ||
| import { InteractiveGoalWithHints } from "../Defs"; | ||
| import { Goal } from './goal'; | ||
|
|
||
| const goalFilter = { | ||
| reverse: false, | ||
| showType: true, | ||
| showInstance: true, | ||
| showHiddenAssumption: true, | ||
| showLetValue: true | ||
| } | ||
|
|
||
| /** The tabs of goals that lean has after the command of this step has been processed */ | ||
| export function GoalTabs({ goals, last, onClick, onGoalChange=(n)=>{}}: { goals: InteractiveGoalWithHints[], last : boolean, onClick? : any, onGoalChange?: (n?: number) => void }) { | ||
| let { t } = useTranslation() | ||
| const [selectedGoal, setSelectedGoal] = React.useState<number>(0) | ||
|
|
||
| if (goals.length == 0) { | ||
| return <></> | ||
| } | ||
|
|
||
| return <div className="goal-tabs" onClick={onClick}> | ||
| <div className={`tab-bar ${last ? 'current' : ''}`}> | ||
| {goals.map((goal, i) => ( | ||
| // TODO: Should not use index as key. | ||
| <div key={`proof-goal-${i}`} className={`tab ${i == (selectedGoal) ? "active" : ""}`} onClick={(ev) => { onGoalChange(i); setSelectedGoal(i); ev.stopPropagation() }}> | ||
| {i ? t("Goal") + ` ${i + 1}` : t("Active Goal")} | ||
| </div> | ||
| ))} | ||
| </div> | ||
| <div className="goal-tab vscode-light"> | ||
| <Goal typewriter={false} filter={goalFilter} goal={goals[selectedGoal]?.goal} unbundle={false} /> | ||
| </div> | ||
| </div> | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,47 @@ | ||
| import { InteractiveDiagnostics_msgToInteractive, MessageData } from '@leanprover/infoview-api' | ||
| import { useRpcSession } from './infoview/rpcSessions' | ||
| import { InteractiveMessage } from './infoview/traceExplorer' | ||
| import { mapRpcError, useAsync } from './infoview/util' | ||
|
|
||
| export * from '@leanprover/infoview-api' | ||
| export { EditorContext, EnvPosContext, VersionContext } from './infoview/contexts' | ||
| export { EditorConnection } from './infoview/editorConnection' | ||
| export { GoalLocation, GoalsLocation, LocationsContext } from './infoview/goalLocation' | ||
| export { InteractiveCode, /*InteractiveCodeProps*/ } from './infoview/interactiveCode' | ||
| export { renderInfoview } from './infoview/main' | ||
| export { RpcContext, useRpcSession } from './infoview/rpcSessions' | ||
| export { ServerVersion } from './infoview/serverVersion' | ||
| export { DynamicComponent, /*DynamicComponentProps, PanelWidgetProps,*/ importWidgetModule } from './infoview/userWidget' | ||
| export { | ||
| DocumentPosition, | ||
| mapRpcError, | ||
| useAsync, | ||
| useAsyncPersistent, | ||
| useAsyncWithTrigger, | ||
| useClientNotificationEffect, | ||
| useClientNotificationState, | ||
| useEvent, | ||
| useEventResult, | ||
| useServerNotificationEffect, | ||
| useServerNotificationState, | ||
| } from './infoview/util' | ||
| // export { MessageData } | ||
|
|
||
| /** Display the given message data as interactive, pretty-printed text. */ | ||
| export function InteractiveMessageData({ msg }: { msg: MessageData }) { | ||
| const rs = useRpcSession() | ||
| const interactive = useAsync(() => InteractiveDiagnostics_msgToInteractive(rs, msg, 0), [rs, msg]) | ||
|
|
||
| if (interactive.state === 'resolved') { | ||
| return <InteractiveMessage fmt={interactive.value} /> | ||
| } else if (interactive.state === 'loading') { | ||
| return <>...</> | ||
| } else { | ||
| return ( | ||
| <div> | ||
| Failed to display message: | ||
| {<span>{mapRpcError(interactive.error).message}</span>} | ||
| </div> | ||
| ) | ||
| } | ||
| } |
Oops, something went wrong.