From 94209eae14bc9600d3fcdc382263f1768230d408 Mon Sep 17 00:00:00 2001 From: Travis Staton Date: Mon, 29 Jul 2024 19:45:48 -0400 Subject: [PATCH 1/2] permit empty matches --- .../src/Unison/PatternMatchCoverage.hs | 19 ++++++++++++++----- .../Unison/PatternMatchCoverage/Desugar.hs | 7 ++----- 2 files changed, 16 insertions(+), 10 deletions(-) diff --git a/parser-typechecker/src/Unison/PatternMatchCoverage.hs b/parser-typechecker/src/Unison/PatternMatchCoverage.hs index 7a431a486a..62d04167ff 100644 --- a/parser-typechecker/src/Unison/PatternMatchCoverage.hs +++ b/parser-typechecker/src/Unison/PatternMatchCoverage.hs @@ -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 @@ -64,13 +65,16 @@ checkMatch :: checkMatch matchLocation scrutineeType cases = do ppe <- getPrettyPrintEnv v0 <- fresh - grdtree0 <- desugarMatch matchLocation scrutineeType v0 cases - doDebug (P.hang (title "desugared:") (prettyGrdTree (prettyPmGrd ppe) (\_ -> "") grdtree0)) (pure ()) - (uncovered, grdtree1) <- uncoverAnnotate (Set.singleton (NC.markDirty v0 $ NC.declVar v0 scrutineeType id NC.emptyNormalizedConstraints)) grdtree0 + mgrdtree0 <- traverse (desugarMatch matchLocation scrutineeType v0) (nonEmpty cases) + doDebug (P.hang (title "desugared:") (prettyGrdTreeMaybe (prettyPmGrd ppe) (\_ -> "") 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) ] ) @@ -78,9 +82,14 @@ checkMatch matchLocation scrutineeType cases = do 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 -> "" + Just x -> prettyGrdTree prettyNode prettyLeaf x title = P.bold doDebug out = case shouldDebug PatternCoverage of True -> trace (P.toAnsiUnbroken out) diff --git a/parser-typechecker/src/Unison/PatternMatchCoverage/Desugar.hs b/parser-typechecker/src/Unison/PatternMatchCoverage/Desugar.hs index ce015cc51b..28bf29b754 100644 --- a/parser-typechecker/src/Unison/PatternMatchCoverage/Desugar.hs +++ b/parser-typechecker/src/Unison/PatternMatchCoverage/Desugar.hs @@ -27,12 +27,9 @@ desugarMatch :: -- | 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 loc0 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} = From 72da81f18ba7204f4a3d8a2eaad83f218f65d7b6 Mon Sep 17 00:00:00 2001 From: Travis Staton Date: Mon, 29 Jul 2024 21:21:09 -0400 Subject: [PATCH 2/2] remove unused arg --- parser-typechecker/src/Unison/PatternMatchCoverage.hs | 6 ++---- .../src/Unison/PatternMatchCoverage/Desugar.hs | 4 +--- parser-typechecker/src/Unison/Typechecker/Context.hs | 2 +- 3 files changed, 4 insertions(+), 8 deletions(-) diff --git a/parser-typechecker/src/Unison/PatternMatchCoverage.hs b/parser-typechecker/src/Unison/PatternMatchCoverage.hs index 62d04167ff..30973b8256 100644 --- a/parser-typechecker/src/Unison/PatternMatchCoverage.hs +++ b/parser-typechecker/src/Unison/PatternMatchCoverage.hs @@ -54,18 +54,16 @@ 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 - mgrdtree0 <- traverse (desugarMatch matchLocation scrutineeType v0) (nonEmpty cases) + mgrdtree0 <- traverse (desugarMatch scrutineeType v0) (nonEmpty cases) doDebug (P.hang (title "desugared:") (prettyGrdTreeMaybe (prettyPmGrd ppe) (\_ -> "") mgrdtree0)) (pure ()) let initialUncovered = Set.singleton (NC.markDirty v0 $ NC.declVar v0 scrutineeType id NC.emptyNormalizedConstraints) (uncovered, grdtree1) <- case mgrdtree0 of diff --git a/parser-typechecker/src/Unison/PatternMatchCoverage/Desugar.hs b/parser-typechecker/src/Unison/PatternMatchCoverage/Desugar.hs index 28bf29b754..8587d44d6c 100644 --- a/parser-typechecker/src/Unison/PatternMatchCoverage/Desugar.hs +++ b/parser-typechecker/src/Unison/PatternMatchCoverage/Desugar.hs @@ -20,8 +20,6 @@ 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 @@ -29,7 +27,7 @@ desugarMatch :: -- | match cases NonEmpty (MatchCase loc (Term' vt v loc)) -> m (GrdTree (PmGrd vt v loc) loc) -desugarMatch loc0 scrutineeType v0 cs0 = Fork <$> traverse desugarClause cs0 +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} = diff --git a/parser-typechecker/src/Unison/Typechecker/Context.hs b/parser-typechecker/src/Unison/Typechecker/Context.hs index 89eb193212..214fe95a0c 100644 --- a/parser-typechecker/src/Unison/Typechecker/Context.hs +++ b/parser-typechecker/src/Unison/Typechecker/Context.hs @@ -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)