-- | Pattern match coverage checking is implemented following the
-- algorithm described in [Lower Your
-- Guards](https://simon.peytonjones.org/assets/pdfs/lower-your-guards.pdf). The
-- goal of pattern match coverage checking is to identify the
-- following problems that may arise in a pattern match:
--
-- * It is missing clauses (/i.e./ it is non-exhaustive)
-- * It contains redundant patterns (/i.e./ the case can be deleted without altering the program)
-- * It contains inaccessible patterns (/i.e/ the rhs can never be entered)
--
-- Furthermore, in the case of a non-exhaustive match, the goal to
-- present the user with concrete values that do not match any of the
-- existing patterns.
--
-- /N.B./ An inaccessible pattern in unison would be one that performs
-- effects in a guard although the constraints are unsatisfiable. Such
-- a pattern cannot be deleted without altering the program.
--
-- == High-level algorithm overview
--
-- 1. [Desugar]("Unison.PatternMatchCoverage.Desugar") a match expression into a 'Unison.PatternMatchCoverage.GrdTree.GrdTree'.
-- 2. Annotate the @GrdTree@ leaves with [refinement types]("Unison.PatternMatchCoverage.NormalizedConstraints")
-- describing values that match this branch. Redundant and inaccessible patterns are then identified by @GrdTree@ leaves
-- with uninhabited refinement types. Inaccessible patterns are distinguished by an effect being performed between the
-- @GrdTree@ root and the leaf.
-- 3. Traverse the @GrdTree@ building up a refinement type describing uncovered values. If the resulting refinement type
-- is inhabited then the match is missing clauses.
-- 4. Find inhabitants of the uncovered refinement type to present to the user.
--
-- Step (1) is implemented by 'desugarMatch'. Steps (2) and (3) are
-- implemented as a single traversal: 'uncoverAnnotate'/'classify'. Step (4) is
-- implemented by 'expandSolution'/'generateInhabitants'.
module Unison.PatternMatchCoverage
  ( checkMatch,
  )
where

import Data.Set qualified as Set
import Debug.Trace
import Unison.Debug
import Unison.Pattern (Pattern)
import Unison.PatternMatchCoverage.Class (Pmc (..))
import Unison.PatternMatchCoverage.Desugar (desugarMatch)
import Unison.PatternMatchCoverage.GrdTree (prettyGrdTree)
import Unison.PatternMatchCoverage.NormalizedConstraints qualified as NC
import Unison.PatternMatchCoverage.PmGrd (prettyPmGrd)
import Unison.PatternMatchCoverage.Solve (classify, expandSolution, generateInhabitants, uncoverAnnotate)
import Unison.Term qualified as Term
import Unison.Type qualified as Type
import Unison.Util.Pretty qualified as P

-- | Perform pattern match coverage checking on a match expression
checkMatch ::
  forall vt v loc m.
  (Pmc vt v loc m) =>
  -- | scrutinee type
  Type.Type vt loc ->
  -- | match cases
  [Term.MatchCase loc (Term.Term' vt v loc)] ->
  -- | (redundant locations, inaccessible locations, inhabitants of uncovered refinement type)
  m ([loc], [loc], [Pattern ()])
checkMatch :: forall vt v loc (m :: * -> *).
Pmc vt v loc m =>
Type vt loc
-> [MatchCase loc (Term' vt v loc)]
-> m ([loc], [loc], [Pattern ()])
checkMatch Type vt loc
scrutineeType [MatchCase loc (Term' vt v loc)]
cases = do
  PrettyPrintEnv
ppe <- m PrettyPrintEnv
forall vt v loc (m :: * -> *). Pmc vt v loc m => m PrettyPrintEnv
getPrettyPrintEnv
  v
v0 <- m v
forall vt v loc (m :: * -> *). Pmc vt v loc m => m v
fresh
  GrdTree (PmGrd vt v loc) loc
grdtree0 <- Type vt loc
-> v
-> [MatchCase loc (Term' vt v loc)]
-> m (GrdTree (PmGrd vt v loc) loc)
forall loc vt v (m :: * -> *).
Pmc vt v loc m =>
Type vt loc
-> v
-> [MatchCase loc (Term' vt v loc)]
-> m (GrdTree (PmGrd vt v loc) loc)
desugarMatch Type vt loc
scrutineeType v
v0 [MatchCase loc (Term' vt v loc)]
cases
  Pretty ColorText -> m () -> m ()
forall {a}. Pretty ColorText -> a -> a
doDebug (Pretty ColorText -> Pretty ColorText -> Pretty ColorText
forall s.
(ListLike s Char, IsString s) =>
Pretty s -> Pretty s -> Pretty s
P.hang (Pretty ColorText -> Pretty ColorText
title Pretty ColorText
"desugared:") ((PmGrd vt v loc -> Pretty ColorText)
-> (loc -> Pretty ColorText)
-> GrdTree (PmGrd vt v loc) loc
-> Pretty ColorText
forall n l s.
(ListLike s Char, IsString s) =>
(n -> Pretty s) -> (l -> Pretty s) -> GrdTree n l -> Pretty s
prettyGrdTree (PrettyPrintEnv -> PmGrd vt v loc -> Pretty ColorText
forall vt v loc.
(Var vt, Var v) =>
PrettyPrintEnv -> PmGrd vt v loc -> Pretty ColorText
prettyPmGrd PrettyPrintEnv
ppe) (\loc
_ -> Pretty ColorText
"<loc>") GrdTree (PmGrd vt v loc) loc
grdtree0)) (() -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ())
  let initialUncovered :: Set (NormalizedConstraints vt v loc)
initialUncovered = NormalizedConstraints vt v loc
-> Set (NormalizedConstraints vt v loc)
forall a. a -> Set a
Set.singleton (v
-> NormalizedConstraints vt v loc -> NormalizedConstraints vt v loc
forall v vt loc.
Ord v =>
v
-> NormalizedConstraints vt v loc -> NormalizedConstraints vt v loc
NC.markDirty v
v0 (NormalizedConstraints vt v loc -> NormalizedConstraints vt v loc)
-> NormalizedConstraints vt v loc -> NormalizedConstraints vt v loc
forall a b. (a -> b) -> a -> b
$ v
-> Type vt loc
-> (VarInfo vt v loc -> VarInfo vt v loc)
-> NormalizedConstraints vt v loc
-> NormalizedConstraints vt v loc
forall vt v loc.
Var v =>
v
-> Type vt loc
-> (VarInfo vt v loc -> VarInfo vt v loc)
-> NormalizedConstraints vt v loc
-> NormalizedConstraints vt v loc
NC.declVar v
v0 Type vt loc
scrutineeType VarInfo vt v loc -> VarInfo vt v loc
forall a. a -> a
id NormalizedConstraints vt v loc
forall v vt loc. Ord v => NormalizedConstraints vt v loc
NC.emptyNormalizedConstraints)
  (Set (NormalizedConstraints vt v loc)
uncovered, GrdTree
  (Set (NormalizedConstraints vt v loc))
  (Set (NormalizedConstraints vt v loc), loc)
grdtree1) <- Set (NormalizedConstraints vt v loc)
-> GrdTree (PmGrd vt v loc) loc
-> m (Set (NormalizedConstraints vt v loc),
      GrdTree
        (Set (NormalizedConstraints vt v loc))
        (Set (NormalizedConstraints vt v loc), loc))
forall vt v loc (m :: * -> *) l.
Pmc vt v loc m =>
Set (NormalizedConstraints vt v loc)
-> GrdTree (PmGrd vt v loc) l
-> m (Set (NormalizedConstraints vt v loc),
      GrdTree
        (Set (NormalizedConstraints vt v loc))
        (Set (NormalizedConstraints vt v loc), l))
uncoverAnnotate Set (NormalizedConstraints vt v loc)
initialUncovered GrdTree (PmGrd vt v loc) loc
grdtree0
  Pretty ColorText -> m () -> m ()
forall {a}. Pretty ColorText -> a -> a
doDebug
    ( Pretty ColorText -> [Pretty ColorText] -> Pretty ColorText
forall (f :: * -> *) s.
(Foldable f, IsString s) =>
Pretty s -> f (Pretty s) -> Pretty s
P.sep
        Pretty ColorText
"\n"
        [ Pretty ColorText -> Pretty ColorText -> Pretty ColorText
forall s.
(ListLike s Char, IsString s) =>
Pretty s -> Pretty s -> Pretty s
P.hang (Pretty ColorText -> Pretty ColorText
title Pretty ColorText
"annotated:") ((Set (NormalizedConstraints vt v loc) -> Pretty ColorText)
-> ((Set (NormalizedConstraints vt v loc), loc)
    -> Pretty ColorText)
-> GrdTree
     (Set (NormalizedConstraints vt v loc))
     (Set (NormalizedConstraints vt v loc), loc)
-> Pretty ColorText
forall n l s.
(ListLike s Char, IsString s) =>
(n -> Pretty s) -> (l -> Pretty s) -> GrdTree n l -> Pretty s
prettyGrdTree (PrettyPrintEnv
-> Set (NormalizedConstraints vt v loc) -> Pretty ColorText
forall v vt loc.
(Var v, Var vt) =>
PrettyPrintEnv
-> Set (NormalizedConstraints vt v loc) -> Pretty ColorText
NC.prettyDnf PrettyPrintEnv
ppe) (PrettyPrintEnv
-> Set (NormalizedConstraints vt v loc) -> Pretty ColorText
forall v vt loc.
(Var v, Var vt) =>
PrettyPrintEnv
-> Set (NormalizedConstraints vt v loc) -> Pretty ColorText
NC.prettyDnf PrettyPrintEnv
ppe (Set (NormalizedConstraints vt v loc) -> Pretty ColorText)
-> ((Set (NormalizedConstraints vt v loc), loc)
    -> Set (NormalizedConstraints vt v loc))
-> (Set (NormalizedConstraints vt v loc), loc)
-> Pretty ColorText
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Set (NormalizedConstraints vt v loc), loc)
-> Set (NormalizedConstraints vt v loc)
forall a b. (a, b) -> a
fst) GrdTree
  (Set (NormalizedConstraints vt v loc))
  (Set (NormalizedConstraints vt v loc), loc)
grdtree1),
          Pretty ColorText -> Pretty ColorText -> Pretty ColorText
forall s.
(ListLike s Char, IsString s) =>
Pretty s -> Pretty s -> Pretty s
P.hang (Pretty ColorText -> Pretty ColorText
title Pretty ColorText
"uncovered:") (PrettyPrintEnv
-> Set (NormalizedConstraints vt v loc) -> Pretty ColorText
forall v vt loc.
(Var v, Var vt) =>
PrettyPrintEnv
-> Set (NormalizedConstraints vt v loc) -> Pretty ColorText
NC.prettyDnf PrettyPrintEnv
ppe Set (NormalizedConstraints vt v loc)
uncovered)
        ]
    )
    (() -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ())
  [NormalizedConstraints vt v loc]
uncoveredExpanded <- [[NormalizedConstraints vt v loc]]
-> [NormalizedConstraints vt v loc]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[NormalizedConstraints vt v loc]]
 -> [NormalizedConstraints vt v loc])
-> ([Set (NormalizedConstraints vt v loc)]
    -> [[NormalizedConstraints vt v loc]])
-> [Set (NormalizedConstraints vt v loc)]
-> [NormalizedConstraints vt v loc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Set (NormalizedConstraints vt v loc)
 -> [NormalizedConstraints vt v loc])
-> [Set (NormalizedConstraints vt v loc)]
-> [[NormalizedConstraints vt v loc]]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Set (NormalizedConstraints vt v loc)
-> [NormalizedConstraints vt v loc]
forall a. Set a -> [a]
Set.toList ([Set (NormalizedConstraints vt v loc)]
 -> [NormalizedConstraints vt v loc])
-> m [Set (NormalizedConstraints vt v loc)]
-> m [NormalizedConstraints vt v loc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (NormalizedConstraints vt v loc
 -> m (Set (NormalizedConstraints vt v loc)))
-> [NormalizedConstraints vt v loc]
-> m [Set (NormalizedConstraints vt v loc)]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse (v
-> NormalizedConstraints vt v loc
-> m (Set (NormalizedConstraints vt v loc))
forall vt v loc (m :: * -> *).
Pmc vt v loc m =>
v
-> NormalizedConstraints vt v loc
-> m (Set (NormalizedConstraints vt v loc))
expandSolution v
v0) (Set (NormalizedConstraints vt v loc)
-> [NormalizedConstraints vt v loc]
forall a. Set a -> [a]
Set.toList Set (NormalizedConstraints vt v loc)
uncovered)
  Pretty ColorText -> m () -> m ()
forall {a}. Pretty ColorText -> a -> a
doDebug (Pretty ColorText -> Pretty ColorText -> Pretty ColorText
forall s.
(ListLike s Char, IsString s) =>
Pretty s -> Pretty s -> Pretty s
P.hang (Pretty ColorText -> Pretty ColorText
title Pretty ColorText
"uncovered expanded:") (PrettyPrintEnv
-> Set (NormalizedConstraints vt v loc) -> Pretty ColorText
forall v vt loc.
(Var v, Var vt) =>
PrettyPrintEnv
-> Set (NormalizedConstraints vt v loc) -> Pretty ColorText
NC.prettyDnf PrettyPrintEnv
ppe ([NormalizedConstraints vt v loc]
-> Set (NormalizedConstraints vt v loc)
forall a. Ord a => [a] -> Set a
Set.fromList [NormalizedConstraints vt v loc]
uncoveredExpanded))) (() -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ())
  let sols :: [Pattern ()]
sols = (NormalizedConstraints vt v loc -> Pattern ())
-> [NormalizedConstraints vt v loc] -> [Pattern ()]
forall a b. (a -> b) -> [a] -> [b]
map (v -> NormalizedConstraints vt v loc -> Pattern ()
forall vt v loc.
Var v =>
v -> NormalizedConstraints vt v loc -> Pattern ()
generateInhabitants v
v0) [NormalizedConstraints vt v loc]
uncoveredExpanded
  let ([loc]
_accessible, [loc]
inaccessible, [loc]
redundant) = GrdTree
  (Set (NormalizedConstraints vt v loc))
  (Set (NormalizedConstraints vt v loc), loc)
-> ([loc], [loc], [loc])
forall vt v loc l.
GrdTree
  (Set (NormalizedConstraints vt v loc))
  (Set (NormalizedConstraints vt v loc), l)
-> ([l], [l], [l])
classify GrdTree
  (Set (NormalizedConstraints vt v loc))
  (Set (NormalizedConstraints vt v loc), loc)
grdtree1
  pure ([loc]
redundant, [loc]
inaccessible, [Pattern ()]
sols)
  where
    title :: Pretty ColorText -> Pretty ColorText
title = Pretty ColorText -> Pretty ColorText
P.bold
    doDebug :: Pretty ColorText -> a -> a
doDebug Pretty ColorText
out = case DebugFlag -> Bool
shouldDebug DebugFlag
PatternCoverage of
      Bool
True -> String -> a -> a
forall a. String -> a -> a
trace (Pretty ColorText -> String
P.toAnsiUnbroken Pretty ColorText
out)
      Bool
False -> a -> a
forall a. a -> a
id