use Core values for pattern examples

src/Juvix/Compiler/Core/Pretty/Base.hs

@@ -582,6 +582,15 @@ instance PrettyCode Value where
     ValueWildcard -> return "_"
     ValueFun -> return "<fun>"
 
+ppValueSequence :: Member (Reader Options) r => [Value] -> Sem r (Doc Ann)
+ppValueSequence vs = hsep <$> mapM (ppRightExpression appFixity) vs
+
+docValueSequence :: [Value] -> Doc Ann
+docValueSequence =
+  run
+    . runReader defaultOptions
+    . ppValueSequence
+
 --------------------------------------------------------------------------------
 -- helper functions
 --------------------------------------------------------------------------------

src/Juvix/Compiler/Core/Transformation/MatchToCase.hs

@@ -6,10 +6,10 @@ import Juvix.Compiler.Core.Error
 import Juvix.Compiler.Core.Extra
 import Juvix.Compiler.Core.Info.LocationInfo
 import Juvix.Compiler.Core.Info.NameInfo (setInfoName)
+import Juvix.Compiler.Core.Language.Value
 import Juvix.Compiler.Core.Options
 import Juvix.Compiler.Core.Pretty hiding (Options)
 import Juvix.Compiler.Core.Transformation.Base
-import Juvix.Data.NameKind
 
 data PatternRow = PatternRow
   { _patternRowPatterns :: [Pattern],
@@ -52,7 +52,7 @@ goMatchToCase recur node = case node of
           [] ->
             compile err n [0 .. n - 1] matrix
             where
-              err = hsep . take n
+              err = take n
               matrix = map matchBranchToPatternRow _matchBranches
 
               matchBranchToPatternRow :: MatchBranch -> PatternRow
@@ -77,7 +77,7 @@ goMatchToCase recur node = case node of
     --    first added binder; a value matched on is always a variable referring
     --    to one of the binders added so far
     --  - `matrix` is the pattern matching matrix
-    compile :: ([Doc Ann] -> Doc Ann) -> Level -> [Level] -> PatternMatrix -> Sem r Node
+    compile :: ([Value] -> [Value]) -> Level -> [Level] -> PatternMatrix -> Sem r Node
     compile err bindersNum vs matrix = case matrix of
       [] -> do
         -- The matrix has no rows -- matching fails (Section 4, case 1).
@@ -86,15 +86,23 @@ goMatchToCase recur node = case node of
             | fCoverage ->
                 throw
                   CoreError
-                    { _coreErrorMsg = ppOutput ("Pattern matching not exhaustive. Example pattern sequence not matched: " <> pat),
+                    { _coreErrorMsg =
+                        ppOutput
+                          ( "Pattern matching not exhaustive. Example pattern "
+                              <> seq
+                              <> "not matched: "
+                              <> pat'
+                          ),
                       _coreErrorNode = Nothing,
                       _coreErrorLoc = fromMaybe defaultLoc (getNodeLocation node)
                     }
             | otherwise ->
                 return $
-                  mkBuiltinApp' OpFail [mkConstant' (ConstString ("Pattern sequence not matched: " <> show pat))]
+                  mkBuiltinApp' OpFail [mkConstant' (ConstString ("Pattern sequence not matched: " <> ppTrace pat))]
         where
-          pat = err (replicate (length vs) "_")
+          pat = err (replicate (length vs) ValueWildcard)
+          seq = if length pat == 1 then "" else "sequence "
+          pat' = if length pat == 1 then doc defaultOptions (List.head pat) else docValueSequence pat
           mockFile = $(mkAbsFile "/match-to-case")
           defaultLoc = singletonInterval (mkInitialLoc mockFile)
       r@PatternRow {..} : _
@@ -190,7 +198,7 @@ goMatchToCase recur node = case node of
     -- `compileDefault` computes D(M) where `M = col:matrix`, as described in
     -- Section 2, Figure 1 in the paper. Then it continues compilation with the
     -- new matrix.
-    compileDefault :: Maybe Tag -> ([Doc Ann] -> Doc Ann) -> Level -> [Level] -> [Pattern] -> PatternMatrix -> Sem r Node
+    compileDefault :: Maybe Tag -> ([Value] -> [Value]) -> Level -> [Level] -> [Pattern] -> PatternMatrix -> Sem r Node
     compileDefault mtag err bindersNum vs col matrix = do
       tab <- ask
       compile (err' tab) bindersNum vs matrix'
@@ -199,25 +207,26 @@ goMatchToCase recur node = case node of
         err' tab args =
           case mtag of
             Just tag ->
-              err
-                ( parensIf
-                    (argsNum > 0)
-                    (hsep (ctrName : replicate argsNum "_"))
-                    : args
-                )
+              err (ctr : args)
               where
                 ci = lookupConstructorInfo tab tag
                 ii = lookupInductiveInfo tab (ci ^. constructorInductive)
                 paramsNum = length (ii ^. inductiveParams)
                 argsNum = ci ^. constructorArgsNum - paramsNum
-                ctrName = annotate (AnnKind KNameConstructor) (pretty (ci ^. constructorName))
+                ctr =
+                  ValueConstrApp
+                    ConstrApp
+                      { _constrAppName = ci ^. constructorName,
+                        _constrAppFixity = ci ^. constructorFixity,
+                        _constrAppArgs = replicate argsNum ValueWildcard
+                      }
             Nothing ->
-              err ("_" : args)
+              err (ValueWildcard : args)
 
     -- `compileBranch` computes S(c, M) where `c = Constr tag` and `M =
     -- col:matrix`, as described in Section 2, Figure 1 in the paper. Then it
     -- continues compilation with the new matrix.
-    compileBranch :: ([Doc Ann] -> Doc Ann) -> Level -> [Level] -> [Pattern] -> PatternMatrix -> Tag -> Sem r CaseBranch
+    compileBranch :: ([Value] -> [Value]) -> Level -> [Level] -> [Pattern] -> PatternMatrix -> Tag -> Sem r CaseBranch
     compileBranch err bindersNum vs col matrix tag = do
       tab <- ask
       let ci = lookupConstructorInfo tab tag
@@ -226,14 +235,16 @@ goMatchToCase recur node = case node of
           argsNum = length (typeArgs (ci ^. constructorType))
           bindersNum' = bindersNum + argsNum
           vs' = [bindersNum .. bindersNum + argsNum - 1]
-          ctrName = annotate (AnnKind KNameConstructor) (pretty (ci ^. constructorName))
           err' args =
-            err
-              ( parensIf
-                  (argsNum > paramsNum)
-                  (hsep (ctrName : drop paramsNum (take argsNum args)))
-                  : drop argsNum args
-              )
+            err (ctr : drop argsNum args)
+            where
+              ctr =
+                ValueConstrApp
+                  ConstrApp
+                    { _constrAppName = ci ^. constructorName,
+                      _constrAppFixity = ci ^. constructorFixity,
+                      _constrAppArgs = drop paramsNum (take argsNum args)
+                    }
       binders' <- getBranchBinders col matrix tag
       matrix' <- getBranchMatrix col matrix tag
       body <- compile err' bindersNum' (vs' ++ vs) matrix'

src/Juvix/Compiler/Core/Translation/FromInternal.hs

@@ -418,7 +418,9 @@ goCase c = do
     NTyp {} -> do
       branches <- toList <$> mapM (goCaseBranch ty) (c ^. Internal.caseBranches)
       rty <- goType (fromJust $ c ^. Internal.caseExpressionWholeType)
-      return (mkMatch' (pure ty) rty (pure expr) branches)
+      -- Do not use mkMatch' in this file, or the error messages for pattern
+      -- matching coverage will lack location information
+      return (mkMatch i (pure ty) rty (pure expr) branches)
     _ ->
       case c ^. Internal.caseBranches of
         Internal.CaseBranch {..} :| _ ->