From 53d303cd2596a87f2e1ee1ea95cb84d4d2e0c5ff Mon Sep 17 00:00:00 2001
From: Philipp Joram <mail@phijor.me>
Date: Sat, 22 Mar 2025 15:36:19 +0200
Subject: [PATCH] Display list of possible constructors to introduce

When refining a goal whose type is a `data` type, and if there is more
than one matching constructor, Agda replies with a list of possible
constructors to introduce.  We parse this reply and display the list of
constructors in the info view.  This fixes #141.
---
 src/Cornelis/Pretty.hs | 5 +++++
 src/Cornelis/Types.hs  | 2 ++
 2 files changed, 7 insertions(+)

diff --git a/src/Cornelis/Pretty.hs b/src/Cornelis/Pretty.hs
index 0600e3c..9130ceb 100644
--- a/src/Cornelis/Pretty.hs
+++ b/src/Cornelis/Pretty.hs
@@ -176,6 +176,11 @@ prettyGoals (InferredType ty) =
 prettyGoals (WhyInScope msg) = pretty msg
 prettyGoals (NormalForm expr) = pretty expr
 prettyGoals (DisplayError err) = annotate CornelisError $ pretty err
+prettyGoals (IntroConstructorUnknown constructors) = vsep
+  [ annotate CornelisErrorWarning "Don't know which constructor to introduce."
+  , mempty
+  , section "Constructors available" constructors prettyName
+  ]
 prettyGoals (UnknownDisplayInfo v) = annotate CornelisError $ pretty $ show v
 
 prettyInterval :: AgdaInterval -> Doc HighlightGroup
diff --git a/src/Cornelis/Types.hs b/src/Cornelis/Types.hs
index bfea1dc..59e356b 100644
--- a/src/Cornelis/Types.hs
+++ b/src/Cornelis/Types.hs
@@ -314,6 +314,7 @@ data DisplayInfo
   | HelperFunction Text
   | InferredType Type
   | DisplayError Text
+  | IntroConstructorUnknown [Text]
   | WhyInScope Text
   | NormalForm Text
   | UnknownDisplayInfo Value
@@ -339,6 +340,7 @@ instance FromJSON DisplayInfo where
       "Error" ->
         obj .: "error" >>= \err ->
           DisplayError <$> err .: "message"
+      "IntroConstructorUnknown" -> IntroConstructorUnknown <$> obj .: "constructors"
       "InferredType" ->
         InferredType <$> obj .: "expr"
       "WhyInScope" ->