Skip to content

Commit

Permalink
Merge pull request #5256 from unisonweb/travis/empty-pattern-match
Browse files Browse the repository at this point in the history
  • Loading branch information
aryairani authored Jul 30, 2024
2 parents f559576 + 72da81f commit 4acebf0
Show file tree
Hide file tree
Showing 3 changed files with 18 additions and 16 deletions.
23 changes: 15 additions & 8 deletions parser-typechecker/src/Unison/PatternMatchCoverage.hs
Original file line number Diff line number Diff line change
Expand Up @@ -35,6 +35,7 @@ module Unison.PatternMatchCoverage
)
where

import Data.List.NonEmpty (nonEmpty)
import Data.Set qualified as Set
import Debug.Trace
import Unison.Debug
Expand All @@ -53,34 +54,40 @@ import Unison.Util.Pretty qualified as P
checkMatch ::
forall vt v loc m.
(Pmc vt v loc m) =>
-- | the match location
loc ->
-- | 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 matchLocation scrutineeType cases = do
checkMatch scrutineeType cases = do
ppe <- getPrettyPrintEnv
v0 <- fresh
grdtree0 <- desugarMatch matchLocation scrutineeType v0 cases
doDebug (P.hang (title "desugared:") (prettyGrdTree (prettyPmGrd ppe) (\_ -> "<loc>") grdtree0)) (pure ())
(uncovered, grdtree1) <- uncoverAnnotate (Set.singleton (NC.markDirty v0 $ NC.declVar v0 scrutineeType id NC.emptyNormalizedConstraints)) grdtree0
mgrdtree0 <- traverse (desugarMatch scrutineeType v0) (nonEmpty cases)
doDebug (P.hang (title "desugared:") (prettyGrdTreeMaybe (prettyPmGrd ppe) (\_ -> "<loc>") mgrdtree0)) (pure ())
let initialUncovered = Set.singleton (NC.markDirty v0 $ NC.declVar v0 scrutineeType id NC.emptyNormalizedConstraints)
(uncovered, grdtree1) <- case mgrdtree0 of
Nothing -> pure (initialUncovered, Nothing)
Just grdtree0 -> fmap Just <$> uncoverAnnotate initialUncovered grdtree0
doDebug
( P.sep
"\n"
[ P.hang (title "annotated:") (prettyGrdTree (NC.prettyDnf ppe) (NC.prettyDnf ppe . fst) grdtree1),
[ P.hang (title "annotated:") (prettyGrdTreeMaybe (NC.prettyDnf ppe) (NC.prettyDnf ppe . fst) grdtree1),
P.hang (title "uncovered:") (NC.prettyDnf ppe uncovered)
]
)
(pure ())
uncoveredExpanded <- concat . fmap Set.toList <$> traverse (expandSolution v0) (Set.toList uncovered)
doDebug (P.hang (title "uncovered expanded:") (NC.prettyDnf ppe (Set.fromList uncoveredExpanded))) (pure ())
let sols = map (generateInhabitants v0) uncoveredExpanded
let (_accessible, inaccessible, redundant) = classify grdtree1
let (_accessible, inaccessible, redundant) = case grdtree1 of
Nothing -> ([], [], [])
Just x -> classify x
pure (redundant, inaccessible, sols)
where
prettyGrdTreeMaybe prettyNode prettyLeaf = \case
Nothing -> "<empty>"
Just x -> prettyGrdTree prettyNode prettyLeaf x
title = P.bold
doDebug out = case shouldDebug PatternCoverage of
True -> trace (P.toAnsiUnbroken out)
Expand Down
9 changes: 2 additions & 7 deletions parser-typechecker/src/Unison/PatternMatchCoverage/Desugar.hs
Original file line number Diff line number Diff line change
Expand Up @@ -20,19 +20,14 @@ import Unison.Type qualified as Type
desugarMatch ::
forall loc vt v m.
(Pmc vt v loc m) =>
-- | loc of match
loc ->
-- | scrutinee type
Type vt loc ->
-- | scrutinee variable
v ->
-- | match cases
[MatchCase loc (Term' vt v loc)] ->
NonEmpty (MatchCase loc (Term' vt v loc)) ->
m (GrdTree (PmGrd vt v loc) loc)
desugarMatch loc0 scrutineeType v0 cs0 =
traverse desugarClause cs0 >>= \case
[] -> pure $ Leaf loc0
x : xs -> pure $ Fork (x :| xs)
desugarMatch scrutineeType v0 cs0 = Fork <$> traverse desugarClause cs0
where
desugarClause :: MatchCase loc (Term' vt v loc) -> m (GrdTree (PmGrd vt v loc) loc)
desugarClause MatchCase {matchPattern, matchGuard} =
Expand Down
2 changes: 1 addition & 1 deletion parser-typechecker/src/Unison/Typechecker/Context.hs
Original file line number Diff line number Diff line change
Expand Up @@ -1525,7 +1525,7 @@ ensurePatternCoverage theMatch _theMatchType _scrutinee scrutineeType cases = do
constructorCache = mempty
}
(redundant, _inaccessible, uncovered) <- flip evalStateT pmcState do
checkMatch matchLoc scrutineeType cases
checkMatch scrutineeType cases
let checkUncovered = case Nel.nonEmpty uncovered of
Nothing -> pure ()
Just xs -> failWith (UncoveredPatterns matchLoc xs)
Expand Down

0 comments on commit 4acebf0

Please sign in to comment.