Split assumptions and objects

Fixes #9
Fixes #24

client/src/components/infoview/goals.tsx

@@ -2,11 +2,11 @@
 
 import * as React from 'react'
 import { InteractiveCode } from '../../../../node_modules/lean4-infoview/src/infoview/interactiveCode'
-import { InteractiveHypothesisBundle, InteractiveHypothesisBundle_nonAnonymousNames, MVarId, TaggedText_stripTags } from '@leanprover/infoview-api'
+import { InteractiveHypothesisBundle_nonAnonymousNames, MVarId, TaggedText_stripTags } from '@leanprover/infoview-api'
 import { WithTooltipOnHover } from '../../../../node_modules/lean4-infoview/src/infoview/tooltips';
 import { EditorContext } from '../../../../node_modules/lean4-infoview/src/infoview/contexts';
 import { Locations, LocationsContext, SelectableLocation } from '../../../../node_modules/lean4-infoview/src/infoview/goalLocation';
-import { InteractiveGoal, InteractiveGoals } from './rpcApi';
+import { InteractiveGoal, InteractiveGoals, InteractiveHypothesisBundle } from './rpcApi';
 import { Hints } from './hints';
 
 /** Returns true if `h` is inaccessible according to Lean's default name rendering. */
@@ -144,20 +144,16 @@ export const Goal = React.memo((props: GoalProps) => {
     if (props.goal.isRemoved) cn += 'b--removed '
 
     const hints = <Hints hints={goal.hints} />
+    const objectHyps = hyps.filter(hyp => !hyp.isAssumption)
+    const assumptionHyps = hyps.filter(hyp => hyp.isAssumption)
 
-    if (goal.userName) {
-        return <details open className={cn}>
-            <summary className='mv1 pointer'>
-                <strong className="goal-case">case </strong>{goal.userName}
-            </summary>
-            {filter.reverse && goalLi}
-            {hyps.map((h, i) => <Hyp hyp={h} mvarId={goal.mvarId} key={i} />)}
-            {!filter.reverse && goalLi}
-            {hints}
-        </details>
-    } else return <div className={cn}>
+    return <div className={cn}>
+        {goal.userName && <div><strong className="goal-case">case </strong>{goal.userName}</div>}
         {filter.reverse && goalLi}
-        {hyps.map((h, i) => <Hyp hyp={h} mvarId={goal.mvarId} key={i} />)}
+        <div>Objects:</div>
+        {objectHyps.map((h, i) => <Hyp hyp={h} mvarId={goal.mvarId} key={i} />)}
+        <div>Assumptions:</div>
+        {assumptionHyps.map((h, i) => <Hyp hyp={h} mvarId={goal.mvarId} key={i} />)}
         {!filter.reverse && goalLi}
         {hints}
     </div>

client/src/components/infoview/rpcApi.ts

@@ -1,10 +1,28 @@
-import { ContextInfo, InteractiveHypothesisBundle, CodeWithInfos, MVarId } from '@leanprover/infoview-api';
+/* This file is based on `vscode-lean4/vscode-lean4/src/rpcApi.ts ` */
+
+import { ContextInfo, FVarId, CodeWithInfos, MVarId } from '@leanprover/infoview-api';
 
 export interface GameHint {
   text: string;
   hidden: boolean;
 }
 
+export interface InteractiveHypothesisBundle {
+  /** 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[];
+  /** Present since server version 1.1.2. */
+  fvarIds?: FVarId[];
+  type: CodeWithInfos;
+  val?: CodeWithInfos;
+  isInstance?: boolean;
+  isType?: boolean;
+  isAssumption?: boolean;
+  isInserted?: boolean;
+  isRemoved?: boolean;
+}
+
 export interface InteractiveGoalCore {
   hyps: InteractiveHypothesisBundle[];
   type: CodeWithInfos;

server/leanserver/GameServer/InteractiveGoal.lean

@@ -27,6 +27,8 @@ structure InteractiveHypothesisBundle where
   isInstance? : Option Bool := none
   /-- The hypothesis is a type. -/
   isType? : Option Bool := none
+  /-- The hypothesis's type is of type `Prop` -/
+  isAssumption? : Option Bool := none
   /-- If true, the hypothesis was not present on the previous tactic state.
   Only present in tactic-mode goals. -/
   isInserted? : Option Bool := none
@@ -123,10 +125,11 @@ def addInteractiveHypothesisBundle (hyps : Array InteractiveHypothesisBundle)
   return hyps.push {
     names
     fvarIds
-    type        := (← ppExprTagged type)
-    val?        := (← value?.mapM ppExprTagged)
-    isInstance? := if (← isClass? type).isSome then true else none
-    isType?     := if (← instantiateMVars type).isSort then true else none
+    type           := (← ppExprTagged type)
+    val?           := (← value?.mapM ppExprTagged)
+    isInstance?    := if (← isClass? type).isSome then true else none
+    isType?        := if (← instantiateMVars type).isSort then true else none
+    isAssumption?  := if (← inferType type).isProp then true else none
   }
 
 open Meta in