mirror of
https://github.com/unisonweb/unison.git
synced 2024-10-04 05:37:14 +03:00
Merge pull request #5298 from sellout/empty-match
Support pattern matching on empty types
This commit is contained in:
commit
7178ec2266
@ -35,7 +35,6 @@ module Unison.PatternMatchCoverage
|
||||
)
|
||||
where
|
||||
|
||||
import Data.List.NonEmpty (nonEmpty)
|
||||
import Data.Set qualified as Set
|
||||
import Debug.Trace
|
||||
import Unison.Debug
|
||||
@ -63,16 +62,14 @@ checkMatch ::
|
||||
checkMatch scrutineeType cases = do
|
||||
ppe <- getPrettyPrintEnv
|
||||
v0 <- fresh
|
||||
mgrdtree0 <- traverse (desugarMatch scrutineeType v0) (nonEmpty cases)
|
||||
doDebug (P.hang (title "desugared:") (prettyGrdTreeMaybe (prettyPmGrd ppe) (\_ -> "<loc>") mgrdtree0)) (pure ())
|
||||
grdtree0 <- desugarMatch scrutineeType v0 cases
|
||||
doDebug (P.hang (title "desugared:") (prettyGrdTree (prettyPmGrd ppe) (\_ -> "<loc>") grdtree0)) (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
|
||||
(uncovered, grdtree1) <- uncoverAnnotate initialUncovered grdtree0
|
||||
doDebug
|
||||
( P.sep
|
||||
"\n"
|
||||
[ P.hang (title "annotated:") (prettyGrdTreeMaybe (NC.prettyDnf ppe) (NC.prettyDnf ppe . fst) grdtree1),
|
||||
[ P.hang (title "annotated:") (prettyGrdTree (NC.prettyDnf ppe) (NC.prettyDnf ppe . fst) grdtree1),
|
||||
P.hang (title "uncovered:") (NC.prettyDnf ppe uncovered)
|
||||
]
|
||||
)
|
||||
@ -80,14 +77,9 @@ checkMatch 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) = case grdtree1 of
|
||||
Nothing -> ([], [], [])
|
||||
Just x -> classify x
|
||||
let (_accessible, inaccessible, redundant) = classify grdtree1
|
||||
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)
|
||||
|
@ -3,7 +3,6 @@ module Unison.PatternMatchCoverage.Desugar
|
||||
)
|
||||
where
|
||||
|
||||
import Data.List.NonEmpty (NonEmpty (..))
|
||||
import U.Core.ABT qualified as ABT
|
||||
import Unison.Pattern
|
||||
import Unison.Pattern qualified as Pattern
|
||||
@ -25,7 +24,7 @@ desugarMatch ::
|
||||
-- | scrutinee variable
|
||||
v ->
|
||||
-- | match cases
|
||||
NonEmpty (MatchCase loc (Term' vt v loc)) ->
|
||||
[MatchCase loc (Term' vt v loc)] ->
|
||||
m (GrdTree (PmGrd vt v loc) loc)
|
||||
desugarMatch scrutineeType v0 cs0 = Fork <$> traverse desugarClause cs0
|
||||
where
|
||||
|
@ -10,8 +10,6 @@ module Unison.PatternMatchCoverage.GrdTree
|
||||
)
|
||||
where
|
||||
|
||||
import Data.List.NonEmpty (NonEmpty (..))
|
||||
import Data.List.NonEmpty qualified as NEL
|
||||
import Data.ListLike (ListLike)
|
||||
import Unison.PatternMatchCoverage.Fix
|
||||
import Unison.Prelude
|
||||
@ -55,7 +53,7 @@ data GrdTreeF n l a
|
||||
| -- | A constraint of some kind (structural pattern match, boolan guard, etc)
|
||||
GrdF n a
|
||||
| -- | A list of alternative matches, tried in order
|
||||
ForkF (NonEmpty a)
|
||||
ForkF [a]
|
||||
deriving stock (Functor, Show)
|
||||
|
||||
prettyGrdTree :: forall n l s. (ListLike s Char, IsString s) => (n -> Pretty s) -> (l -> Pretty s) -> GrdTree n l -> Pretty s
|
||||
@ -64,7 +62,7 @@ prettyGrdTree prettyNode prettyLeaf = cata phi
|
||||
phi = \case
|
||||
LeafF l -> prettyLeaf l
|
||||
GrdF n rest -> sep " " [prettyNode n, "──", rest]
|
||||
ForkF xs -> "──" <> group (sep "\n" (makeTree $ NEL.toList xs))
|
||||
ForkF xs -> "──" <> group (sep "\n" $ makeTree xs)
|
||||
makeTree :: [Pretty s] -> [Pretty s]
|
||||
makeTree = \case
|
||||
[] -> []
|
||||
@ -82,7 +80,7 @@ pattern Leaf x = Fix (LeafF x)
|
||||
pattern Grd :: n -> GrdTree n l -> GrdTree n l
|
||||
pattern Grd x rest = Fix (GrdF x rest)
|
||||
|
||||
pattern Fork :: NonEmpty (GrdTree n l) -> GrdTree n l
|
||||
pattern Fork :: [GrdTree n l] -> GrdTree n l
|
||||
pattern Fork alts = Fix (ForkF alts)
|
||||
|
||||
{-# COMPLETE Leaf, Grd, Fork #-}
|
||||
|
@ -16,7 +16,6 @@ import Data.Foldable
|
||||
import Data.Function
|
||||
import Data.Functor
|
||||
import Data.Functor.Compose
|
||||
import Data.List.NonEmpty (NonEmpty (..))
|
||||
import Data.Map qualified as Map
|
||||
import Data.Sequence qualified as Seq
|
||||
import Data.Set qualified as Set
|
||||
@ -74,12 +73,11 @@ uncoverAnnotate z grdtree0 = cata phi grdtree0 z
|
||||
LeafF l -> \nc -> do
|
||||
nc' <- ensureInhabited' nc
|
||||
pure (Set.empty, Leaf (nc', l))
|
||||
ForkF (kinit :| ks) -> \nc0 -> do
|
||||
ForkF ks -> \nc0 -> do
|
||||
-- depth-first fold in match-case order to acculate the
|
||||
-- constraints for a match failure at every case.
|
||||
(nc1, t1) <- kinit nc0
|
||||
(ncfinal, ts) <- foldlM (\(nc, ts) a -> a nc >>= \(nc', t) -> pure (nc', t : ts)) (nc1, []) ks
|
||||
pure (ncfinal, Fork (t1 :| reverse ts))
|
||||
(ncfinal, ts) <- foldlM (\(nc, ts) a -> a nc >>= \(nc', t) -> pure (nc', t : ts)) (nc0, []) ks
|
||||
pure (ncfinal, Fork $ reverse ts)
|
||||
GrdF grd k -> \nc0 -> case grd of
|
||||
PmEffect var con convars -> handleGrd (PosEffect var (Effect con) convars) (NegEffect var (Effect con)) k nc0
|
||||
PmEffectPure var resume -> handleGrd (PosEffect var NoEffect [resume]) (NegEffect var NoEffect) k nc0
|
||||
|
@ -1774,21 +1774,6 @@ renderParseErrors s = \case
|
||||
tokenAsErrorSite s tok
|
||||
]
|
||||
in (msg, [rangeForToken tok])
|
||||
go (Parser.EmptyMatch tok) =
|
||||
let msg =
|
||||
Pr.indentN 2 . Pr.callout "😶" $
|
||||
Pr.lines
|
||||
[ Pr.wrap
|
||||
( "I expected some patterns after a "
|
||||
<> style ErrorSite "match"
|
||||
<> "/"
|
||||
<> style ErrorSite "with"
|
||||
<> " or cases but I didn't find any."
|
||||
),
|
||||
"",
|
||||
tokenAsErrorSite s tok
|
||||
]
|
||||
in (msg, [rangeForToken tok])
|
||||
go (Parser.EmptyWatch tok) =
|
||||
let msg =
|
||||
Pr.lines
|
||||
|
@ -171,22 +171,13 @@ match = do
|
||||
P.try (openBlockWith "with") <|> do
|
||||
t <- anyToken
|
||||
P.customFailure (ExpectedBlockOpen "with" t)
|
||||
(_arities, cases) <- NonEmpty.unzip <$> matchCases1 start
|
||||
(_arities, cases) <- unzip <$> matchCases
|
||||
_ <- optionalCloseBlock
|
||||
pure $
|
||||
Term.match
|
||||
(ann start <> ann (NonEmpty.last cases))
|
||||
scrutinee
|
||||
(toList cases)
|
||||
let anns = foldr ((<>) . ann) (ann start) $ lastMay cases
|
||||
pure $ Term.match anns scrutinee cases
|
||||
|
||||
matchCases1 :: (Monad m, Var v) => L.Token () -> P v m (NonEmpty (Int, Term.MatchCase Ann (Term v Ann)))
|
||||
matchCases1 start = do
|
||||
cases <-
|
||||
(sepBy semi matchCase)
|
||||
<&> \cases_ -> [(n, c) | (n, cs) <- cases_, c <- cs]
|
||||
case cases of
|
||||
[] -> P.customFailure (EmptyMatch start)
|
||||
(c : cs) -> pure (c NonEmpty.:| cs)
|
||||
matchCases :: (Monad m, Var v) => P v m [(Int, Term.MatchCase Ann (Term v Ann))]
|
||||
matchCases = sepBy semi matchCase <&> \cases_ -> [(n, c) | (n, cs) <- cases_, c <- cs]
|
||||
|
||||
-- Returns the arity of the pattern and the `MatchCase`. Examples:
|
||||
--
|
||||
@ -369,16 +360,17 @@ handle = label "handle" do
|
||||
-- Meaning the newline gets overwritten when pretty-printing and it messes things up.
|
||||
pure $ Term.handle (handleSpan <> ann handler) handler b
|
||||
|
||||
checkCasesArities :: (Ord v, Annotated a) => NonEmpty (Int, a) -> P v m (Int, NonEmpty a)
|
||||
checkCasesArities cases@((i, _) NonEmpty.:| rest) =
|
||||
case List.find (\(j, _) -> j /= i) rest of
|
||||
checkCasesArities :: (Ord v, Annotated a) => [(Int, a)] -> P v m (Int, [a])
|
||||
checkCasesArities = \case
|
||||
[] -> pure (1, [])
|
||||
cases@((i, _) : rest) -> case List.find (\(j, _) -> j /= i) rest of
|
||||
Nothing -> pure (i, snd <$> cases)
|
||||
Just (j, a) -> P.customFailure $ PatternArityMismatch i j (ann a)
|
||||
|
||||
lamCase :: (Monad m, Var v) => TermP v m
|
||||
lamCase = do
|
||||
start <- openBlockWith "cases"
|
||||
cases <- matchCases1 start
|
||||
cases <- matchCases
|
||||
(arity, cases) <- checkCasesArities cases
|
||||
_ <- optionalCloseBlock
|
||||
lamvars <- replicateM arity (Parser.uniqueName 10)
|
||||
@ -390,8 +382,8 @@ lamCase = do
|
||||
lamvarTerm = case lamvarTerms of
|
||||
[e] -> e
|
||||
es -> DD.tupleTerm es
|
||||
anns = ann start <> ann (NonEmpty.last cases)
|
||||
matchTerm = Term.match anns lamvarTerm (toList cases)
|
||||
anns = foldr ((<>) . ann) (ann start) $ lastMay cases
|
||||
matchTerm = Term.match anns lamvarTerm cases
|
||||
let annotatedVars = (Ann.GeneratedFrom $ ann start,) <$> vars
|
||||
pure $ Term.lam' anns annotatedVars matchTerm
|
||||
|
||||
|
@ -1526,10 +1526,8 @@ ensurePatternCoverage theMatch _theMatchType _scrutinee scrutineeType cases = do
|
||||
}
|
||||
(redundant, _inaccessible, uncovered) <- flip evalStateT pmcState do
|
||||
checkMatch scrutineeType cases
|
||||
let checkUncovered = case Nel.nonEmpty uncovered of
|
||||
Nothing -> pure ()
|
||||
Just xs -> failWith (UncoveredPatterns matchLoc xs)
|
||||
checkRedundant = foldr (\a b -> failWith (RedundantPattern a) *> b) (pure ()) redundant
|
||||
let checkUncovered = maybe (pure ()) (failWith . UncoveredPatterns matchLoc) $ Nel.nonEmpty uncovered
|
||||
checkRedundant = foldr ((*>) . failWith . RedundantPattern) (pure ()) redundant
|
||||
checkUncovered *> checkRedundant
|
||||
|
||||
checkCases ::
|
||||
|
@ -191,13 +191,12 @@ foo = match 1 with
|
||||
|
||||
Loading changes detected in scratch.u.
|
||||
|
||||
😶
|
||||
|
||||
I expected some patterns after a match / with or cases but I
|
||||
didn't find any.
|
||||
|
||||
Pattern match doesn't cover all possible cases:
|
||||
2 | foo = match 1 with
|
||||
|
||||
|
||||
Patterns not matched:
|
||||
* _
|
||||
|
||||
```
|
||||
``` unison
|
||||
|
33
unison-src/transcripts/fix4731.md
Normal file
33
unison-src/transcripts/fix4731.md
Normal file
@ -0,0 +1,33 @@
|
||||
```unison
|
||||
structural type Void =
|
||||
```
|
||||
|
||||
```ucm
|
||||
scratch/main> add
|
||||
```
|
||||
|
||||
We should be able to `match` on empty types like `Void`.
|
||||
|
||||
```unison
|
||||
Void.absurdly : '{e} Void ->{e} a
|
||||
Void.absurdly v = match !v with
|
||||
```
|
||||
|
||||
```unison
|
||||
Void.absurdly : Void -> a
|
||||
Void.absurdly v = match v with
|
||||
```
|
||||
|
||||
And empty `cases` should also work.
|
||||
|
||||
```unison
|
||||
Void.absurdly : Void -> a
|
||||
Void.absurdly = cases
|
||||
```
|
||||
|
||||
But empty function bodies are not allowed.
|
||||
|
||||
```unison:error
|
||||
Void.absurd : Void -> a
|
||||
Void.absurd x =
|
||||
```
|
99
unison-src/transcripts/fix4731.output.md
Normal file
99
unison-src/transcripts/fix4731.output.md
Normal file
@ -0,0 +1,99 @@
|
||||
``` unison
|
||||
structural type Void =
|
||||
```
|
||||
|
||||
``` ucm
|
||||
|
||||
Loading changes detected in scratch.u.
|
||||
|
||||
I found and typechecked these definitions in scratch.u. If you
|
||||
do an `add` or `update`, here's how your codebase would
|
||||
change:
|
||||
|
||||
⍟ These new definitions are ok to `add`:
|
||||
|
||||
structural type Void
|
||||
|
||||
```
|
||||
``` ucm
|
||||
scratch/main> add
|
||||
|
||||
⍟ I've added these definitions:
|
||||
|
||||
structural type Void
|
||||
|
||||
```
|
||||
We should be able to `match` on empty types like `Void`.
|
||||
|
||||
``` unison
|
||||
Void.absurdly : '{e} Void ->{e} a
|
||||
Void.absurdly v = match !v with
|
||||
```
|
||||
|
||||
``` ucm
|
||||
|
||||
Loading changes detected in scratch.u.
|
||||
|
||||
I found and typechecked these definitions in scratch.u. If you
|
||||
do an `add` or `update`, here's how your codebase would
|
||||
change:
|
||||
|
||||
⍟ These new definitions are ok to `add`:
|
||||
|
||||
Void.absurdly : '{e} Void ->{e} a
|
||||
|
||||
```
|
||||
``` unison
|
||||
Void.absurdly : Void -> a
|
||||
Void.absurdly v = match v with
|
||||
```
|
||||
|
||||
``` ucm
|
||||
|
||||
Loading changes detected in scratch.u.
|
||||
|
||||
I found and typechecked these definitions in scratch.u. If you
|
||||
do an `add` or `update`, here's how your codebase would
|
||||
change:
|
||||
|
||||
⍟ These new definitions are ok to `add`:
|
||||
|
||||
Void.absurdly : Void -> a
|
||||
|
||||
```
|
||||
And empty `cases` should also work.
|
||||
|
||||
``` unison
|
||||
Void.absurdly : Void -> a
|
||||
Void.absurdly = cases
|
||||
```
|
||||
|
||||
``` ucm
|
||||
|
||||
Loading changes detected in scratch.u.
|
||||
|
||||
I found and typechecked these definitions in scratch.u. If you
|
||||
do an `add` or `update`, here's how your codebase would
|
||||
change:
|
||||
|
||||
⍟ These new definitions are ok to `add`:
|
||||
|
||||
Void.absurdly : Void -> a
|
||||
|
||||
```
|
||||
But empty function bodies are not allowed.
|
||||
|
||||
``` unison
|
||||
Void.absurd : Void -> a
|
||||
Void.absurd x =
|
||||
```
|
||||
|
||||
``` ucm
|
||||
|
||||
Loading changes detected in scratch.u.
|
||||
|
||||
I expected a block after this (in red), but there wasn't one. Maybe check your indentation:
|
||||
2 | Void.absurd x =
|
||||
|
||||
|
||||
```
|
@ -29,6 +29,7 @@ startingLine _ = Nothing
|
||||
instance Monoid Ann where
|
||||
mempty = External
|
||||
|
||||
-- | This instance is commutative.
|
||||
instance Semigroup Ann where
|
||||
Ann s1 e1 <> Ann s2 e2 = Ann (min s1 s2) (max e1 e2)
|
||||
-- If we have a concrete location from a file, use it
|
||||
|
@ -164,8 +164,6 @@ data Error v
|
||||
| UnknownType (L.Token (HQ.HashQualified Name)) (Set Reference)
|
||||
| UnknownId (L.Token (HQ.HashQualified Name)) (Set Referent) (Set Reference)
|
||||
| ExpectedBlockOpen String (L.Token L.Lexeme)
|
||||
| -- | Indicates a cases or match/with which doesn't have any patterns
|
||||
EmptyMatch (L.Token ())
|
||||
| EmptyWatch Ann
|
||||
| UseInvalidPrefixSuffix (Either (L.Token Name) (L.Token Name)) (Maybe [L.Token Name])
|
||||
| UseEmpty (L.Token String) -- an empty `use` statement
|
||||
|
Loading…
Reference in New Issue
Block a user