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.

Author: phijor

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

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" ->