From 503ea51f956c36d9064aa9355c4a141b5995b1ae Mon Sep 17 00:00:00 2001
From: Jon Eugster <eugster.jon@gmail.com>
Date: Tue, 11 Jun 2024 23:42:58 +0200
Subject: [PATCH] add framework to allow unbundle hypotheses #105

---
 client/src/components/infoview/goals.tsx | 13 ++++++++++---
 client/src/components/infoview/main.tsx  |  2 +-
 2 files changed, 11 insertions(+), 4 deletions(-)

diff --git a/client/src/components/infoview/goals.tsx b/client/src/components/infoview/goals.tsx
index 1325bf4..14ea2ae 100644
--- a/client/src/components/infoview/goals.tsx
+++ b/client/src/components/infoview/goals.tsx
@@ -133,13 +133,14 @@ interface GoalProps {
     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 } = props
+    const { goal, filter, showHints, typewriter, unbundle } = props
     let { t } = useTranslation()
 
     // TODO: Apparently `goal` can be `undefined`
@@ -164,9 +165,15 @@ export const Goal = React.memo((props: GoalProps) => {
     // 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 = hyps.filter(hyp => !hyp.isAssumption)
-    const assumptionHyps = hyps.filter(hyp => hyp.isAssumption)
+    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>} */}
diff --git a/client/src/components/infoview/main.tsx b/client/src/components/infoview/main.tsx
index f9d4c62..c8a9363 100644
--- a/client/src/components/infoview/main.tsx
+++ b/client/src/components/infoview/main.tsx
@@ -358,7 +358,7 @@ function GoalsTabs({ proofStep, last, onClick, onGoalChange=(n)=>{}}: { proofSte
       ))}
     </div>
     <div className="goal-tab vscode-light">
-      <Goal typewriter={false} filter={goalFilter} goal={proofStep.goals[selectedGoal]?.goal} />
+      <Goal typewriter={false} filter={goalFilter} goal={proofStep.goals[selectedGoal]?.goal} unbundle={false} />
     </div>
   </div>
 }