From 9e3dbb62b80df53a1ad5c019987d2c5a56f87674 Mon Sep 17 00:00:00 2001 From: Travis Staton Date: Thu, 29 Sep 2022 16:33:23 -0400 Subject: [PATCH 01/54] Add pattern match coverage checking --- .../src/Unison/PatternMatchCoverage.hs | 45 + .../src/Unison/PatternMatchCoverage/Class.hs | 32 + .../Unison/PatternMatchCoverage/Constraint.hs | 52 + .../Unison/PatternMatchCoverage/Desugar.hs | 204 ++++ .../src/Unison/PatternMatchCoverage/Fix.hs | 20 + .../Unison/PatternMatchCoverage/GrdTree.hs | 45 + .../PatternMatchCoverage/IntervalSet.hs | 203 ++++ .../Unison/PatternMatchCoverage/ListPat.hs | 15 + .../Unison/PatternMatchCoverage/Literal.hs | 61 ++ .../NormalizedConstraints.hs | 248 +++++ .../src/Unison/PatternMatchCoverage/PmGrd.hs | 64 ++ .../src/Unison/PatternMatchCoverage/PmLit.hs | 23 + .../src/Unison/PatternMatchCoverage/Solve.hs | 930 ++++++++++++++++++ .../src/Unison/PatternMatchCoverage/UFMap.hs | 227 +++++ parser-typechecker/src/Unison/PrintError.hs | 47 +- .../src/Unison/Syntax/TermPrinter.hs | 1 + .../src/Unison/Typechecker/Context.hs | 96 ++ .../src/Unison/Typechecker/Extractor.hs | 13 + .../src/Unison/Typechecker/TypeError.hs | 17 +- .../unison-parser-typechecker.cabal | 14 + unison-cli/src/Unison/LSP/FileAnalysis.hs | 28 +- .../transcripts/pattern-match-coverage.md | 190 ++++ .../pattern-match-coverage.output.md | 436 ++++++++ 23 files changed, 2997 insertions(+), 14 deletions(-) create mode 100644 parser-typechecker/src/Unison/PatternMatchCoverage.hs create mode 100644 parser-typechecker/src/Unison/PatternMatchCoverage/Class.hs create mode 100644 parser-typechecker/src/Unison/PatternMatchCoverage/Constraint.hs create mode 100644 parser-typechecker/src/Unison/PatternMatchCoverage/Desugar.hs create mode 100644 parser-typechecker/src/Unison/PatternMatchCoverage/Fix.hs create mode 100644 parser-typechecker/src/Unison/PatternMatchCoverage/GrdTree.hs create mode 100644 parser-typechecker/src/Unison/PatternMatchCoverage/IntervalSet.hs create mode 100644 parser-typechecker/src/Unison/PatternMatchCoverage/ListPat.hs create mode 100644 parser-typechecker/src/Unison/PatternMatchCoverage/Literal.hs create mode 100644 parser-typechecker/src/Unison/PatternMatchCoverage/NormalizedConstraints.hs create mode 100644 parser-typechecker/src/Unison/PatternMatchCoverage/PmGrd.hs create mode 100644 parser-typechecker/src/Unison/PatternMatchCoverage/PmLit.hs create mode 100644 parser-typechecker/src/Unison/PatternMatchCoverage/Solve.hs create mode 100644 parser-typechecker/src/Unison/PatternMatchCoverage/UFMap.hs create mode 100644 unison-src/transcripts/pattern-match-coverage.md create mode 100644 unison-src/transcripts/pattern-match-coverage.output.md diff --git a/parser-typechecker/src/Unison/PatternMatchCoverage.hs b/parser-typechecker/src/Unison/PatternMatchCoverage.hs new file mode 100644 index 000000000..3ef3c8a94 --- /dev/null +++ b/parser-typechecker/src/Unison/PatternMatchCoverage.hs @@ -0,0 +1,45 @@ +-- Pattern match coverage checking following the algorithm described +-- in "Lower Your Guards". +-- https://simon.peytonjones.org/assets/pdfs/lower-your-guards.pdf +module Unison.PatternMatchCoverage where + +import qualified Data.Set as Set +import Debug.Trace +import Unison.Pattern (Pattern) +import Unison.PatternMatchCoverage.Class (Pmc (..)) +import Unison.PatternMatchCoverage.Desugar (desugarMatch) +import Unison.PatternMatchCoverage.GrdTree (prettyGrdTree) +import qualified Unison.PatternMatchCoverage.NormalizedConstraints as NC +import Unison.PatternMatchCoverage.PmGrd (prettyPmGrd) +import Unison.PatternMatchCoverage.Solve (classify, expand, expandSolution, uncoverAnnotate) +import qualified Unison.Term as Term +import qualified Unison.Type as Type +import qualified Unison.Util.Pretty as P + +checkMatch :: + forall vt v loc m. + (Pmc vt v loc m) => + loc -> + Type.Type vt loc -> + [Term.MatchCase loc (Term.Term' vt v loc)] -> + m ([loc], [loc], [Pattern ()]) +checkMatch matchLocation scrutineeType cases = do + v0 <- fresh + grdtree0 <- desugarMatch matchLocation scrutineeType v0 cases + (uncovered, grdtree1) <- uncoverAnnotate (Set.singleton (NC.declVar v0 scrutineeType id NC.emptyNormalizedConstraints)) grdtree0 + uncoveredExpanded <- concat . fmap Set.toList <$> traverse (expandSolution v0) (Set.toList uncovered) + let sols = map (expand v0) uncoveredExpanded + let (_accessible, inaccessible, redundant) = classify grdtree1 + let debugOutput = + P.sep + "\n" + [ P.hang "desugared:" (prettyGrdTree prettyPmGrd (\_ -> "") grdtree0), + P.hang "annotated:" (prettyGrdTree NC.prettyDnf (NC.prettyDnf . fst) grdtree1), + P.hang "uncovered:" (NC.prettyDnf uncovered), + P.hang "uncovered expanded:" (NC.prettyDnf (Set.fromList uncoveredExpanded)) + ] + shouldDebug = False + doDebug = case shouldDebug of + True -> trace (P.toPlainUnbroken debugOutput) + False -> id + doDebug (pure (redundant, inaccessible, sols)) diff --git a/parser-typechecker/src/Unison/PatternMatchCoverage/Class.hs b/parser-typechecker/src/Unison/PatternMatchCoverage/Class.hs new file mode 100644 index 000000000..f908a2072 --- /dev/null +++ b/parser-typechecker/src/Unison/PatternMatchCoverage/Class.hs @@ -0,0 +1,32 @@ +{-# LANGUAGE FunctionalDependencies #-} + +module Unison.PatternMatchCoverage.Class where + +import Control.Monad.Fix (MonadFix) +import Unison.ConstructorReference (ConstructorReference) +import Unison.PatternMatchCoverage.ListPat (ListPat) +import Unison.Type (Type) +import Unison.Var (Var) + +class (Ord loc, Var vt, Var v, MonadFix m) => Pmc vt v loc m | m -> vt v loc where + getConstructors :: Type vt loc -> m (EnumeratedConstructors vt v loc) + getConstructorVarTypes :: Type vt loc -> ConstructorReference -> m [Type vt loc] + fresh :: m v + +data EnumeratedConstructors vt v loc + = ConstructorType [(v, ConstructorReference, Type vt loc)] + | SequenceType [(ListPat, [Type vt loc])] + | BooleanType + | OtherType + deriving stock (Show) + +traverseConstructors :: + Applicative f => + (v -> ConstructorReference -> Type vt loc -> f (v, ConstructorReference, Type vt loc)) -> + EnumeratedConstructors vt v loc -> + f (EnumeratedConstructors vt v loc) +traverseConstructors f = \case + ConstructorType xs -> ConstructorType <$> traverse (\(a, b, c) -> f a b c) xs + SequenceType x -> pure (SequenceType x) + BooleanType -> pure BooleanType + OtherType -> pure OtherType diff --git a/parser-typechecker/src/Unison/PatternMatchCoverage/Constraint.hs b/parser-typechecker/src/Unison/PatternMatchCoverage/Constraint.hs new file mode 100644 index 000000000..c465e023d --- /dev/null +++ b/parser-typechecker/src/Unison/PatternMatchCoverage/Constraint.hs @@ -0,0 +1,52 @@ +module Unison.PatternMatchCoverage.Constraint where + +import Unison.ConstructorReference (ConstructorReference) +import Unison.PatternMatchCoverage.IntervalSet (IntervalSet) +import Unison.PatternMatchCoverage.PmLit +import qualified Unison.PrettyPrintEnv as PPE +import qualified Unison.Syntax.TypePrinter as TypePrinter +import Unison.Type (Type) +import Unison.Util.Pretty +import Unison.Var (Var) + +data Constraint vt v loc + = PosCon v ConstructorReference [(v, Type vt loc)] + | NegCon v ConstructorReference + | PosLit v PmLit + | NegLit v PmLit + | PosListHead + v + -- ^ list root + Int + -- ^ cons position (0 is head) + v + -- ^ element variable + | PosListTail + v + -- ^ list root + Int + -- ^ snoc position (0 is last) + v + -- ^ element variable + | NegListInterval v IntervalSet + | Effectful v + | Eq v v + deriving stock (Eq, Ord) + +prettyConstraint :: (Var vt, Var v) => Constraint vt v loc -> Pretty ColorText +prettyConstraint = \case + PosCon var con convars -> + let xs = pc con : fmap (\(trm, typ) -> sep " " [pv trm, ":", TypePrinter.pretty PPE.empty typ]) convars ++ ["<-", pv var] + in sep " " xs + NegCon var con -> sep " " [pv var, "≠", pc con] + PosLit var lit -> sep " " [prettyPmLit lit, "<-", pv var] + NegLit var lit -> sep " " [pv var, "≠", prettyPmLit lit] + PosListHead root n el -> sep " " [pv el, "<-", "head", pc n, pv root] + PosListTail root n el -> sep " " [pv el, "<-", "tail", pc n, pv root] + NegListInterval var x -> sep " " [pv var, "≠", string (show x)] + Effectful var -> "!" <> pv var + Eq v0 v1 -> sep " " [pv v0, "=", pv v1] + where + pv = string . show + pc :: forall a. Show a => a -> Pretty ColorText + pc = string . show diff --git a/parser-typechecker/src/Unison/PatternMatchCoverage/Desugar.hs b/parser-typechecker/src/Unison/PatternMatchCoverage/Desugar.hs new file mode 100644 index 000000000..af81e3368 --- /dev/null +++ b/parser-typechecker/src/Unison/PatternMatchCoverage/Desugar.hs @@ -0,0 +1,204 @@ +module Unison.PatternMatchCoverage.Desugar where + +import Data.Functor.Compose +import Data.List.NonEmpty (NonEmpty (..)) +import qualified U.Core.ABT as ABT +import Unison.Pattern +import qualified Unison.Pattern as Pattern +import Unison.PatternMatchCoverage.Class +import Unison.PatternMatchCoverage.Fix +import Unison.PatternMatchCoverage.GrdTree +import Unison.PatternMatchCoverage.PmGrd +import qualified Unison.PatternMatchCoverage.PmLit as PmLit +import Unison.Term (MatchCase (..), Term', app, var) +import Unison.Type (Type) +import qualified Unison.Type as Type + +desugarMatch :: + forall loc vt v m. + Pmc vt v loc m => + -- | loc of match + loc -> + Type vt loc -> + v -> + [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) + where + desugarClause :: MatchCase loc (Term' vt v loc) -> m (GrdTree (PmGrd vt v loc) loc) + desugarClause MatchCase {matchPattern, matchGuard} = + desugarPattern scrutineeType v0 matchPattern (finalK (Pattern.loc matchPattern) matchGuard) [] + + finalK :: loc -> Maybe (Term' vt v loc) -> [v] -> m (GrdTree (PmGrd vt v loc) loc) + finalK loc mterm vs = case mterm of + Nothing -> pure (Leaf loc) + Just grdExpr -> do + let ann = ABT.annotation grdExpr + expr = foldr (\a b -> app ann (var ann a) b) grdExpr vs + typ = Type.boolean ann + v <- fresh + pure (Grd (PmLet v expr typ) (Grd (PmLit v (PmLit.Boolean True)) (Leaf loc))) + +desugarPattern :: + forall v vt loc m. + Pmc vt v loc m => + Type vt loc -> + v -> + Pattern loc -> + ([v] -> m (GrdTree (PmGrd vt v loc) loc)) -> + [v] -> + m (GrdTree (PmGrd vt v loc) loc) +desugarPattern typ v0 pat k vs = case pat of + Unbound _ -> k vs + Var _ -> k (v0 : vs) + Boolean _ x -> Grd (PmLit v0 $ PmLit.Boolean x) <$> k vs + Int _ x -> Grd (PmLit v0 $ PmLit.Int x) <$> k vs + Nat _ x -> Grd (PmLit v0 $ PmLit.Nat x) <$> k vs + Float _ x -> Grd (PmLit v0 $ PmLit.Float x) <$> k vs + Text _ x -> Grd (PmLit v0 $ PmLit.Text x) <$> k vs + Char _ x -> Grd (PmLit v0 $ PmLit.Char x) <$> k vs + Constructor _loc consRef pats -> do + contyps <- getConstructorVarTypes typ consRef + patvars <- assignFreshPatternVars pats + let c = PmCon v0 consRef convars + convars :: [(v, Type vt loc)] + convars = map (\(v, _, t) -> (v, t)) tpatvars + tpatvars = zipWith (\(v, p) t -> (v, p, t)) patvars contyps + rest <- foldr (\(v, pat, t) b -> desugarPattern t v pat b) k tpatvars vs + pure (Grd c rest) + As _ _ -> k (v0 : vs) + EffectPure {} -> k vs + EffectBind {} -> k vs + SequenceLiteral {} -> handleSequence typ v0 pat k vs + SequenceOp {} -> handleSequence typ v0 pat k vs + +handleSequence :: + forall v vt loc m. + Pmc vt v loc m => + Type vt loc -> + v -> + Pattern loc -> + ([v] -> m (GrdTree (PmGrd vt v loc) loc)) -> + [v] -> + m (GrdTree (PmGrd vt v loc) loc) +handleSequence typ v pat k vs = do + let listArg = case typ of + Type.App' _list arg -> arg + _ -> error "list type is not an application?" + listToGrdTree typ listArg v (normalizeList pat) k vs + +listToGrdTree :: + forall v vt loc m. + Pmc vt v loc m => + Type vt loc -> + Type vt loc -> + v -> + NormalizedList loc -> + ([v] -> m (GrdTree (PmGrd vt v loc) loc)) -> + [v] -> + m (GrdTree (PmGrd vt v loc) loc) +listToGrdTree _listTyp elemTyp listVar nl0 k0 vs0 = + let (minLen, maxLen) = countMinListLen nl0 + in Grd (PmListInterval listVar minLen maxLen) <$> go 0 0 nl0 k0 vs0 + where + go consCount snocCount (Fix pat) k vs = case pat of + N'ConsF x xs -> do + element <- fresh + let grd = PmListHead listVar consCount element elemTyp + let !consCount' = consCount + 1 + Grd grd <$> desugarPattern elemTyp element x (go consCount' snocCount xs k) vs + N'SnocF xs x -> do + element <- fresh + let grd = PmListTail listVar snocCount element elemTyp + let !snocCount' = snocCount + 1 + Grd grd <$> go consCount snocCount' xs (desugarPattern elemTyp element x k) vs + N'NilF -> k vs + N'VarF _ -> k (listVar : vs) + N'UnboundF _ -> k vs + + countMinListLen :: NormalizedList loc -> (Int, Int) + countMinListLen = + ($ 0) . cata \case + N'ConsF _ b -> \acc -> b $! acc + 1 + N'SnocF b _ -> \acc -> b $! acc + 1 + N'NilF -> \n -> (n, n) + N'VarF _ -> \n -> (n, maxBound) + N'UnboundF _ -> \n -> (n, maxBound) + +data NormalizedListF loc a + = N'ConsF (Pattern loc) a + | N'SnocF a (Pattern loc) + | N'NilF + | N'VarF loc + | N'UnboundF loc + deriving stock (Functor) + +type NormalizedList loc = Fix (NormalizedListF loc) + +type AnnotatedList loc = Fix (Compose ((,) (Int, Int)) (NormalizedListF loc)) + +pattern Ann :: Int -> Int -> NormalizedListF loc (AnnotatedList loc) -> AnnotatedList loc +pattern Ann lb ub rest = Fix (Compose ((lb, ub), rest)) + +pattern N'Cons x xs = Fix (N'ConsF x xs) + +pattern N'Snoc xs x = Fix (N'SnocF xs x) + +pattern N'Nil = Fix N'NilF + +pattern N'Var x = Fix (N'VarF x) + +pattern N'Unbound x = Fix (N'UnboundF x) + +-- | strip out sequence literals and concats +normalizeList :: Pattern loc -> NormalizedList loc +normalizeList pat0 = case goCons pat0 of + Left f -> f N'Nil + Right x -> x + where + goCons :: Pattern loc -> Either (NormalizedList loc -> NormalizedList loc) (NormalizedList loc) + goCons = \case + SequenceLiteral _loc xs -> + Left \nil -> foldr N'Cons nil xs + SequenceOp _loc lhs op rhs -> case op of + Cons -> + case goCons rhs of + Left f -> Left (N'Cons lhs . f) + Right x -> Right (N'Cons lhs x) + Snoc -> + case goCons lhs of + Left f -> Left (f . N'Cons rhs) + Right x -> Right (N'Snoc x rhs) + Concat -> + case goCons lhs of + Left f -> case goCons rhs of + Left g -> Left (f . g) + Right x -> Right (f x) + Right x -> Right (goSnoc rhs x) + Var loc -> Right (N'Var loc) + Unbound loc -> Right (N'Unbound loc) + -- as-patterns are not handled properly here, which is fine while we + -- only have boolean guards, but this needs to be fixed if we + -- introduce pattern guards + As _loc pat -> goCons pat + _ -> error "goCons: unexpected pattern" + + goSnoc :: Pattern loc -> NormalizedList loc -> NormalizedList loc + goSnoc pat nlp = case pat of + SequenceLiteral _loc xs -> + foldl N'Snoc nlp xs + SequenceOp _loc lhs op rhs -> case op of + Cons -> + goSnoc rhs (N'Snoc nlp lhs) + Snoc -> + N'Snoc (goSnoc rhs nlp) lhs + Concat -> + goSnoc rhs (goSnoc lhs nlp) + As _loc pat -> goSnoc pat nlp + _ -> error "goSnoc: unexpected pattern" + +assignFreshPatternVars :: Pmc vt v loc m => [Pattern loc] -> m [(v, Pattern loc)] +assignFreshPatternVars pats = traverse (\p -> (,p) <$> fresh) pats diff --git a/parser-typechecker/src/Unison/PatternMatchCoverage/Fix.hs b/parser-typechecker/src/Unison/PatternMatchCoverage/Fix.hs new file mode 100644 index 000000000..99974ba72 --- /dev/null +++ b/parser-typechecker/src/Unison/PatternMatchCoverage/Fix.hs @@ -0,0 +1,20 @@ +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE QuantifiedConstraints #-} +{-# LANGUAGE TypeSynonymInstances #-} +{-# LANGUAGE UndecidableInstances #-} + +module Unison.PatternMatchCoverage.Fix where + +newtype Fix f = Fix {unFix :: f (Fix f)} + +deriving instance (forall a. Show a => Show (f a)) => Show (Fix f) + +deriving instance (forall a. Eq a => Eq (f a)) => Eq (Fix f) + +deriving instance (Eq (Fix f), forall a. Ord a => Ord (f a)) => Ord (Fix f) + +cata :: Functor f => (f a -> a) -> Fix f -> a +cata alg = let c = alg . fmap c . unFix in c + +para :: Functor f => (f (Fix f, a) -> a) -> Fix f -> a +para alg = let c = alg . fmap (\x -> (x, c x)) . unFix in c diff --git a/parser-typechecker/src/Unison/PatternMatchCoverage/GrdTree.hs b/parser-typechecker/src/Unison/PatternMatchCoverage/GrdTree.hs new file mode 100644 index 000000000..c84e2daa7 --- /dev/null +++ b/parser-typechecker/src/Unison/PatternMatchCoverage/GrdTree.hs @@ -0,0 +1,45 @@ +{-# LANGUAGE OverloadedStrings #-} + +module Unison.PatternMatchCoverage.GrdTree where + +import Data.List.NonEmpty (NonEmpty (..)) +import qualified Data.List.NonEmpty as NEL +import Data.ListLike (ListLike) +import Unison.PatternMatchCoverage.Fix +import Unison.Prelude +import Unison.Util.Pretty + +type GrdTree n l = Fix (GrdTreeF n l) + +data GrdTreeF n l a + = LeafF l + | GrdF n a + | ForkF (NonEmpty 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 +prettyGrdTree prettyNode prettyLeaf = cata phi + where + phi = \case + LeafF l -> prettyLeaf l + GrdF n rest -> sep " " [prettyNode n, "──", rest] + ForkF xs -> "──" <> group (sep "\n" (makeTree $ NEL.toList xs)) + makeTree :: [Pretty s] -> [Pretty s] + makeTree = \case + [] -> [] + x : [] -> [sep " " ["──", x]] + x0 : x1 : xs -> + sep " " ["┬─", x0] : + let go y0 = \case + [] -> [sep " " ["└─", y0]] + y1 : ys -> "├─ " <> y0 : go y1 ys + in [indent " " (sep "\n" (go x1 xs))] + +pattern Leaf :: l -> GrdTree n l +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 alts = Fix (ForkF alts) diff --git a/parser-typechecker/src/Unison/PatternMatchCoverage/IntervalSet.hs b/parser-typechecker/src/Unison/PatternMatchCoverage/IntervalSet.hs new file mode 100644 index 000000000..ab1d2d4b3 --- /dev/null +++ b/parser-typechecker/src/Unison/PatternMatchCoverage/IntervalSet.hs @@ -0,0 +1,203 @@ +module Unison.PatternMatchCoverage.IntervalSet + ( IntervalSet, + empty, + singleton, + fromList, + insert, + delete, + difference, + intersection, + complement, + null, + member, + extractSingleton, + intersectIntervals, + map, + foldr, + lookupMin, + lookupMax, + ) +where + +import Data.Coerce (coerce) +import Data.Function (on) +import Data.IntMap (IntMap) +import qualified Data.IntMap.Strict as IntMap +import Data.List (sortOn) +import Data.Maybe (catMaybes, fromMaybe, maybeToList) +import Prelude hiding (foldr, map, null) +import qualified Prelude + +newtype IntervalSet = IntervalSet {unIntervalSet :: IntMap Int} + deriving stock (Show, Eq, Ord) + +empty :: IntervalSet +empty = IntervalSet IntMap.empty + +singleton :: (Int, Int) -> IntervalSet +singleton x = insert x empty + +lookupMin :: IntervalSet -> Maybe Int +lookupMin = fmap fst . IntMap.lookupMin . unIntervalSet + +lookupMax :: IntervalSet -> Maybe Int +lookupMax = fmap snd . IntMap.lookupMax . unIntervalSet + +member :: Int -> IntervalSet -> Bool +member i is = + case splitLookupLE i is of + (_, m, _) -> case m of + Nothing -> False + Just (_, ub) -> i <= ub + +foldr :: (Int -> Int -> b -> b) -> b -> IntervalSet -> b +foldr f z = IntMap.foldrWithKey f z . unIntervalSet + +map :: ((Int, Int) -> (Int, Int)) -> IntervalSet -> IntervalSet +map f = IntervalSet . foldr phi IntMap.empty + where + phi k v b = let (k', v') = f (k, v) in IntMap.insert k' v' b + +-- | insert inclusive bounds interval into set +insert :: (Int, Int) -> IntervalSet -> IntervalSet +insert i@(lb, ub) is + | nullInterval i = is + | otherwise = + case splitLookupLE lb is of + (smaller, m1, xs) -> + case splitLookupLE ub xs of + (_, m2, larger) -> + IntervalSet $ + IntMap.unions + [ unIntervalSet smaller, + unIntervalSet $ fromList (maybeToList m1 ++ [i] ++ maybeToList m2), + unIntervalSet larger + ] + +delete :: (Int, Int) -> IntervalSet -> IntervalSet +delete i@(lb, ub) is + | nullInterval i = is + | otherwise = + case splitLookupLE lb is of + (smaller, m1, xs) -> + case splitLookupLE ub xs of + (_, m2, larger) -> + IntervalSet $ + IntMap.unions + [ unIntervalSet smaller, + case m1 of + Nothing -> IntMap.empty + Just j -> IntMap.fromList (catMaybes (Prelude.map (intersectIntervals j =<<) [upTo lb, downTo ub])), + fromMaybe IntMap.empty do + j <- m2 + aboveDelete <- downTo ub + uncurry IntMap.singleton <$> intersectIntervals aboveDelete j, + unIntervalSet larger + ] + +complement :: IntervalSet -> IntervalSet +complement (IntervalSet m) = fromAscList . (\xs -> Prelude.foldr phi z xs Nothing) . IntMap.toAscList $ m + where + phi (lb, ub) b mprevUb = + case mprevUb of + Nothing -> case upTo lb of + Nothing -> b (Just ub) + Just x -> x : b (Just ub) + Just lastUb -> + let !lbPred = safeAdd lb (-1) + !lastUbSucc = safeAdd lastUb 1 + proposedInterval = (lastUbSucc, lbPred) + in case nullInterval proposedInterval of + True -> b (Just ub) + False -> proposedInterval : b (Just ub) + z = \case + Nothing -> [(0, maxBound)] + Just prev -> case downTo prev of + Nothing -> [] + Just x -> [x] + +intersection :: IntervalSet -> IntervalSet -> IntervalSet +intersection a b = difference a (complement b) + +null :: IntervalSet -> Bool +null = IntMap.null . unIntervalSet + +extractSingleton :: IntervalSet -> Maybe Int +extractSingleton (IntervalSet m) = case IntMap.toList m of + [(lb, ub)] + | lb == ub -> Just lb + _ -> Nothing + +-- | add two integers, sticking to a bound if it would overflow +safeAdd :: Int -> Int -> Int +safeAdd a b = + let c = a + b + in case a > 0 && b > 0 of + True -> case c < 0 of + True -> maxBound + False -> c + False -> case a < 0 && b < 0 of + True -> case c >= 0 of + True -> minBound + False -> c + False -> c + +difference :: IntervalSet -> IntervalSet -> IntervalSet +difference x (IntervalSet y) = IntMap.foldlWithKey' (\b k v -> delete (k, v) b) x y + +-- | the interval [0, lb) +upTo :: Int -> Maybe (Int, Int) +upTo lb = case lb <= 0 of + True -> Nothing + False -> Just (0, safeAdd lb (-1)) + +-- | the interval (ub, maxBound] +downTo :: Int -> Maybe (Int, Int) +downTo ub = case ub == maxBound of + True -> Nothing + False -> Just (safeAdd ub 1, maxBound) + +nullInterval :: (Int, Int) -> Bool +nullInterval (lb, ub) = ub < lb + +-- | merge a list sorted on the lower bound ascending +fromAscList :: [(Int, Int)] -> IntervalSet +fromAscList = IntervalSet . IntMap.fromAscList . mergeOverlappingAscList + +fromList :: [(Int, Int)] -> IntervalSet +fromList = fromAscList . sortOn fst . filter (not . nullInterval) + +intersectIntervals :: (Int, Int) -> (Int, Int) -> Maybe (Int, Int) +intersectIntervals a b + | doOverlap a b = + let !lb = on max fst a b + !ub = on min snd a b + in Just (lb, ub) + | otherwise = Nothing + +mergeOverlappingAscList :: [(Int, Int)] -> [(Int, Int)] +mergeOverlappingAscList = \case + x0 : x1 : xs -> case doOverlap x0 x1 of + True -> spanIntervals x0 x1 : mergeOverlappingAscList xs + False -> x0 : x1 : mergeOverlappingAscList xs + [x] -> [x] + [] -> [] + +doOverlap :: (Int, Int) -> (Int, Int) -> Bool +doOverlap (lb0, ub0) (lb1, ub1) + | ub0 >= lb1 && lb0 <= ub1 = True + | otherwise = False + +spanIntervals :: (Int, Int) -> (Int, Int) -> (Int, Int) +spanIntervals (lb0, ub0) (lb1, ub1) = + let !lb = min lb0 lb1 + !ub = max ub0 ub1 + in (lb, ub) + +splitLookupLE :: Int -> IntervalSet -> (IntervalSet, Maybe (Int, Int), IntervalSet) +splitLookupLE k (IntervalSet m) = + coerce case IntMap.splitLookup k m of + (smaller, Just v, larger) -> (smaller, Just (k, v), larger) + (smaller, Nothing, larger) -> case IntMap.maxViewWithKey smaller of + Just ((k, v), smaller) -> (smaller, Just (k, v), larger) + Nothing -> (smaller, Nothing, larger) diff --git a/parser-typechecker/src/Unison/PatternMatchCoverage/ListPat.hs b/parser-typechecker/src/Unison/PatternMatchCoverage/ListPat.hs new file mode 100644 index 000000000..60178fb11 --- /dev/null +++ b/parser-typechecker/src/Unison/PatternMatchCoverage/ListPat.hs @@ -0,0 +1,15 @@ +module Unison.PatternMatchCoverage.ListPat where + +import Unison.Util.Pretty + +data ListPat + = Cons + | Snoc + | Nil + deriving stock (Show, Eq, Ord) + +prettyListPat :: ListPat -> Pretty ColorText +prettyListPat = \case + Cons -> "Cons" + Snoc -> "Snoc" + Nil -> "Nil" diff --git a/parser-typechecker/src/Unison/PatternMatchCoverage/Literal.hs b/parser-typechecker/src/Unison/PatternMatchCoverage/Literal.hs new file mode 100644 index 000000000..dd38f85b3 --- /dev/null +++ b/parser-typechecker/src/Unison/PatternMatchCoverage/Literal.hs @@ -0,0 +1,61 @@ +module Unison.PatternMatchCoverage.Literal where + +import Unison.ConstructorReference (ConstructorReference) +import Unison.PatternMatchCoverage.IntervalSet (IntervalSet) +import Unison.PatternMatchCoverage.PmLit (PmLit, prettyPmLit) +import qualified Unison.PrettyPrintEnv as PPE +import qualified Unison.Syntax.TermPrinter as TermPrinter +import qualified Unison.Syntax.TypePrinter as TypePrinter +import Unison.Term (Term') +import Unison.Type (Type) +import Unison.Typechecker.TypeVar (TypeVar, lowerTerm) +import Unison.Util.Pretty +import Unison.Var (Var) + +data Literal vt v loc + = T + | F + | PosCon v ConstructorReference [(v, Type vt loc)] + | NegCon v ConstructorReference + | PosLit v PmLit + | NegLit v PmLit + | PosListHead + v + -- ^ list root + Int + -- ^ cons position (0 is head) + v + -- ^ element variable + (Type vt loc) + | PosListTail + v + -- ^ list root + Int + -- ^ snoc position (0 is last) + v + -- ^ element variable + (Type vt loc) + | NegListInterval v IntervalSet + | Effectful v + | Let v (Term' vt v loc) (Type vt loc) + deriving stock (Show) + +prettyLiteral :: Var v => Literal (TypeVar b v) v loc -> Pretty ColorText +prettyLiteral = \case + T -> "✓" + F -> "⨉" + PosCon var con convars -> + let xs = pc con : fmap (\(trm, typ) -> sep " " [pv trm, ":", TypePrinter.pretty PPE.empty typ]) convars ++ ["<-", pv var] + in sep " " xs + NegCon var con -> sep " " [pv var, "≠", pc con] + PosLit var lit -> sep " " [prettyPmLit lit, "<-", pv var] + NegLit var lit -> sep " " [pv var, "≠", prettyPmLit lit] + PosListHead root n el _ -> sep " " [pv el, "<-", "head", pc n, pv root] + PosListTail root n el _ -> sep " " [pv el, "<-", "tail", pc n, pv root] + NegListInterval var x -> sep " " [pv var, "≠", string (show x)] + Effectful var -> "!" <> pv var + Let var expr typ -> sep " " ["let", pv var, "=", TermPrinter.pretty PPE.empty (lowerTerm expr), ":", TypePrinter.pretty PPE.empty typ] + where + pv = string . show + pc :: forall a. Show a => a -> Pretty ColorText + pc = string . show diff --git a/parser-typechecker/src/Unison/PatternMatchCoverage/NormalizedConstraints.hs b/parser-typechecker/src/Unison/PatternMatchCoverage/NormalizedConstraints.hs new file mode 100644 index 000000000..da0af8dfd --- /dev/null +++ b/parser-typechecker/src/Unison/PatternMatchCoverage/NormalizedConstraints.hs @@ -0,0 +1,248 @@ +module Unison.PatternMatchCoverage.NormalizedConstraints where + +import Data.Functor.Compose +import Data.List (intersperse) +import Data.Sequence (pattern Empty) +import qualified Data.Set as Set +import Unison.ConstructorReference (ConstructorReference) +import Unison.PatternMatchCoverage.Constraint +import Unison.PatternMatchCoverage.IntervalSet (IntervalSet) +import qualified Unison.PatternMatchCoverage.IntervalSet as IntervalSet +import qualified Unison.PatternMatchCoverage.PmLit as PmLit +import Unison.PatternMatchCoverage.UFMap (UFMap) +import qualified Unison.PatternMatchCoverage.UFMap as UFMap +import Unison.Prelude +import qualified Unison.PrettyPrintEnv as PPE +import qualified Unison.Syntax.TypePrinter as TypePrinter +import Unison.Type (Type, booleanRef, charRef, floatRef, intRef, listRef, natRef, textRef, pattern App', pattern Ref') +import Unison.Util.Pretty +import Unison.Var (Var) + +-- | Normalized refinement types (fig 6) +-- +-- Each variable may be associated with a number of constraints +-- represented by 'VarInfo'. A 'NormalizedConstraints' is conceptually +-- the conjunction of all constraints in the map. Disjunction is +-- represented by passing a Set of NormalizedConstraints. So, the +-- constraints are normalized into disjunctive normal form and each +-- @NormalizedConstraints@ is a DNF term. +-- +-- Additionally, the following invariants are enforced (Section 3.4) +-- +-- * Mutual compatibility: No two constraints should conflict with +-- each other. +-- +-- * Inhabitation: There must be at least one value that inhabits +-- each refinement type. (N.B. We only do a best effort enforcement of +-- this invariant, see 'inhabited' in +-- Unison.PatternMatchCoverage.NormalizedConstraints.Solve for +-- additional info) +-- +-- These invariants ensure that each term in our DNF has at least one +-- solution, and it is easy to expand and print these solutions. +data NormalizedConstraints vt v loc = NormalizedConstraints + { -- | Constraints keyed by the variable they constrain. Equality + -- constraints are handled by 'UFMap'. + constraintMap :: UFMap v (VarInfo vt v loc), + -- | dirty variables are ones that must be checked for inhabitance + dirtySet :: Set v + } + deriving stock (Eq, Ord, Show) + +-- | Mark a variable as requiring a new test for inhabitation. +markDirty :: + Ord v => + v -> + NormalizedConstraints vt v loc -> + NormalizedConstraints vt v loc +markDirty k nc@NormalizedConstraints {dirtySet} = + nc {dirtySet = Set.insert k dirtySet} + +dom :: NormalizedConstraints vt v loc -> [v] +dom NormalizedConstraints {constraintMap} = UFMap.keys constraintMap + +emptyNormalizedConstraints :: Ord v => NormalizedConstraints vt v loc +emptyNormalizedConstraints = + NormalizedConstraints + { constraintMap = UFMap.empty, + dirtySet = mempty + } + +expectCanon :: + forall vt v loc. + (Var v) => + v -> + NormalizedConstraints vt v loc -> + (v, VarInfo vt v loc, NormalizedConstraints vt v loc) +expectCanon k nc = + let ((v, vi), nc') = updateF k (\v vi -> ((v, vi), Ignore)) nc + in (v, vi, nc') + +-- | Alter a constraint, marks var as dirty if updated +alterF :: + forall vt v loc f. + (Var v, Functor f) => + v -> + f (ConstraintUpdate (VarInfo vt v loc)) -> + (v -> VarInfo vt v loc -> f (ConstraintUpdate (VarInfo vt v loc))) -> + NormalizedConstraints vt v loc -> + f (NormalizedConstraints vt v loc) +alterF v nothing just nc = + (\(f, x) -> f nc {constraintMap = x}) + <$> getCompose + ( UFMap.alterF + v + nothing' + just' + (constraintMap nc) + ) + where + just' canonK eqClassSize vi = + fmap (UFMap.Canonical eqClassSize) $ + Compose $ + just canonK vi <&> \case + Ignore -> (id, vi) + Update vi -> (markDirty canonK, vi) + nothing' = + Compose $ + nothing <&> \case + Ignore -> (id, Nothing) + Update x -> (markDirty v, Just x) +{-# INLINE alterF #-} + +updateF :: + forall vt v loc f. + (Var v, Functor f) => + v -> + (v -> VarInfo vt v loc -> f (ConstraintUpdate (VarInfo vt v loc))) -> + NormalizedConstraints vt v loc -> + f (NormalizedConstraints vt v loc) +updateF v just nc = + alterF v nothing just nc + where + nothing = error ("expected " <> show v <> " to be in UFMap") + +data ConstraintUpdate a + = Update a + | Ignore + deriving stock (Functor) + +declVar :: + 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 +declVar v t f nc@NormalizedConstraints {constraintMap} = + nc {constraintMap = UFMap.alter v nothing just constraintMap} + where + nothing = + let !vi = f (mkVarInfo v t) + in Just vi + just _ _ _ = error ("attempted to declare: " <> show v <> " but it already exists") + +mkVarInfo :: forall vt v loc. v -> Type vt loc -> VarInfo vt v loc +mkVarInfo v t = + VarInfo + { vi_id = v, + vi_typ = t, + vi_con = case t of + App' (Ref' r) t + | r == listRef -> Vc'ListRoot t Empty Empty (IntervalSet.singleton (0, maxBound)) + Ref' r + | r == booleanRef -> Vc'Boolean Nothing mempty + | r == intRef -> Vc'Int Nothing mempty + | r == natRef -> Vc'Nat Nothing mempty + | r == floatRef -> Vc'Float Nothing mempty + | r == textRef -> Vc'Text Nothing mempty + | r == charRef -> Vc'Char Nothing mempty + -- this may not be a constructor, but we won't be producing + -- any constraints for it in that case anyway + _ -> Vc'Constructor Nothing mempty, + vi_eff = IsNotEffectful + } + +data VarInfo vt v loc = VarInfo + { vi_id :: v, + vi_typ :: Type vt loc, + vi_con :: VarConstraints vt v loc, + vi_eff :: EffectInfo + } + deriving stock (Show, Eq, Ord, Generic) + +data VarConstraints vt v loc + = Vc'Constructor + (Maybe (ConstructorReference, [(v, Type vt loc)])) + (Set ConstructorReference) + | Vc'Boolean (Maybe Bool) (Set Bool) + | Vc'Int (Maybe Int64) (Set Int64) + | Vc'Nat (Maybe Word64) (Set Word64) + | Vc'Float (Maybe Double) (Set Double) + | Vc'Text (Maybe Text) (Set Text) + | Vc'Char (Maybe Char) (Set Char) + | -- | Vc'ListElem v (Either Int Int) + Vc'ListRoot + (Type vt loc) + -- ^ type of list elems + (Seq v) + -- ^ Positive constraint on cons elements + (Seq v) + -- ^ Positive constraint on snoc elements + IntervalSet + -- ^ positive constraint on input list size + deriving stock (Show, Eq, Ord, Generic) + +data EffectInfo + = IsEffectful + | IsNotEffectful + deriving stock (Show, Eq, Ord) + +prettyNormalizedConstraints :: forall vt v loc. (Var v, Var vt) => NormalizedConstraints vt v loc -> Pretty ColorText +prettyNormalizedConstraints (NormalizedConstraints {constraintMap}) = sep " " ["⟨", pconstraints, "⟩"] + where + cls = UFMap.toClasses constraintMap + + pconstraints = sep " " (intersperse "," $ prettyCon <$> cls) + prettyCon (kcanon, ks, vi) = + let posCon = fromMaybe [] $ case vi_con vi of + Vc'Constructor pos _neg -> + (\(datacon, convars) -> [PosCon kcanon datacon convars]) <$> pos + Vc'Boolean pos _neg -> + (\x -> [PosLit kcanon (PmLit.Boolean x)]) <$> pos + Vc'Int pos _neg -> + (\x -> [PosLit kcanon (PmLit.Int x)]) <$> pos + Vc'Nat pos _neg -> + (\x -> [PosLit kcanon (PmLit.Nat x)]) <$> pos + Vc'Float pos _neg -> + (\x -> [PosLit kcanon (PmLit.Float x)]) <$> pos + Vc'Text pos _neg -> + (\x -> [PosLit kcanon (PmLit.Text x)]) <$> pos + Vc'Char pos _neg -> + (\x -> [PosLit kcanon (PmLit.Char x)]) <$> pos + Vc'ListRoot _typ posCons posSnoc _iset -> + let consConstraints = fmap (\(i, x) -> PosListHead kcanon i x) (zip [0 ..] (toList posCons)) + snocConstraints = fmap (\(i, x) -> PosListTail kcanon i x) (zip [0 ..] (toList posSnoc)) + in Just (consConstraints ++ snocConstraints) + negConK :: forall x. Set x -> (v -> x -> Constraint vt v loc) -> [Constraint vt v loc] + negConK s f = foldr (\a b -> f kcanon a : b) [] s + negCon = case vi_con vi of + Vc'Constructor _pos neg -> negConK neg NegCon + Vc'Boolean _pos neg -> negConK neg (\v a -> NegLit v (PmLit.Boolean a)) + Vc'Int _pos neg -> negConK neg (\v a -> NegLit v (PmLit.Int a)) + Vc'Nat _pos neg -> negConK neg (\v a -> NegLit v (PmLit.Nat a)) + Vc'Float _pos neg -> negConK neg (\v a -> NegLit v (PmLit.Float a)) + Vc'Text _pos neg -> negConK neg (\v a -> NegLit v (PmLit.Text a)) + Vc'Char _pos neg -> negConK neg (\v a -> NegLit v (PmLit.Char a)) + Vc'ListRoot _typ _posCons _posSnoc iset -> [NegListInterval kcanon (IntervalSet.complement iset)] + botCon = case vi_eff vi of + IsNotEffectful -> [] + IsEffectful -> [Effectful kcanon] + in sep " " $ + pv kcanon : + fmap pv (Set.toList $ Set.delete kcanon ks) ++ [":", TypePrinter.pretty PPE.empty (vi_typ vi)] ++ ["|"] ++ [sep ", " $ fmap prettyConstraint (posCon ++ negCon ++ botCon)] + pv = string . show + +prettyDnf :: (Var v, Var vt) => Set (NormalizedConstraints vt v loc) -> Pretty ColorText +prettyDnf xs = sep " " ("{" : intersperse "," (prettyNormalizedConstraints <$> Set.toList xs) ++ ["}"]) diff --git a/parser-typechecker/src/Unison/PatternMatchCoverage/PmGrd.hs b/parser-typechecker/src/Unison/PatternMatchCoverage/PmGrd.hs new file mode 100644 index 000000000..8638c0c38 --- /dev/null +++ b/parser-typechecker/src/Unison/PatternMatchCoverage/PmGrd.hs @@ -0,0 +1,64 @@ +module Unison.PatternMatchCoverage.PmGrd where + +import Unison.ConstructorReference (ConstructorReference) +import Unison.PatternMatchCoverage.PmLit (PmLit, prettyPmLit) +import qualified Unison.PrettyPrintEnv as PPE +import qualified Unison.Syntax.TypePrinter as TypePrinter +import Unison.Term (Term') +import Unison.Type (Type) +import Unison.Util.Pretty +import Unison.Var (Var) + +data + PmGrd + vt -- Type variable + v -- Term variable + loc -- annotation + = -- | @PmCon x Con xs ys@ corresponds to the constraint @Con ys <- x@ + PmCon + v + -- ^ Variable + ConstructorReference + -- ^ Constructor + [(v, Type vt loc)] + -- ^ Constructor argument values and types + | PmLit v PmLit + | PmListHead + v + -- ^ list root + Int + -- ^ cons position (0 is head) + v + -- ^ element variable + (Type vt loc) + -- ^ element type + | PmListTail + v + -- ^ list root + Int + -- ^ snoc position (0 is last) + v + -- ^ element variable + (Type vt loc) + -- ^ element type + | -- | The size of the list must fall within this inclusive range + PmListInterval v Int Int + | -- | If a guard performs an effect + PmBang v + | -- | @PmLet x expr@ corresponds to a @let x = expr@ guard. This actually + -- /binds/ @x@. + PmLet v (Term' vt v loc) (Type vt loc) + deriving stock (Show) + +prettyPmGrd :: (Var vt, Var v) => PmGrd vt v loc -> Pretty ColorText +prettyPmGrd = \case + PmCon var con convars -> + let xs = string (show con) : (formatConVar <$> convars) ++ ["<-", string (show var)] + formatConVar (v, t) = sep " " ["(", string (show v), "::", TypePrinter.pretty PPE.empty t, ")"] + in sep " " xs + PmListHead var n el _ -> sep " " ["Cons", string (show n), string (show el), "<-", string (show var)] + PmListTail var n el _ -> sep " " ["Snoc", string (show n), string (show el), "<-", string (show var)] + PmListInterval var minLen maxLen -> sep " " ["Interval", string (show (minLen, maxLen)), "<-", string (show var)] + PmLit var lit -> sep " " [prettyPmLit lit, "<-", string (show var)] + PmBang v -> "!" <> string (show v) + PmLet v _expr _ -> sep " " ["let", string (show v), "=", ""] diff --git a/parser-typechecker/src/Unison/PatternMatchCoverage/PmLit.hs b/parser-typechecker/src/Unison/PatternMatchCoverage/PmLit.hs new file mode 100644 index 000000000..42ec9389f --- /dev/null +++ b/parser-typechecker/src/Unison/PatternMatchCoverage/PmLit.hs @@ -0,0 +1,23 @@ +module Unison.PatternMatchCoverage.PmLit where + +import Unison.Prelude +import Unison.Util.Pretty (Pretty, string) + +data PmLit + = Int Int64 + | Nat Word64 + | Boolean Bool + | Float Double + | Text Text + | Char Char + deriving stock (Show, Eq, Ord) + +prettyPmLit :: IsString s => PmLit -> Pretty s +prettyPmLit = + string . \case + Int x -> show x + Nat x -> show x + Boolean x -> show x + Float x -> show x + Text x -> show x + Char x -> show x diff --git a/parser-typechecker/src/Unison/PatternMatchCoverage/Solve.hs b/parser-typechecker/src/Unison/PatternMatchCoverage/Solve.hs new file mode 100644 index 000000000..8134aa5b7 --- /dev/null +++ b/parser-typechecker/src/Unison/PatternMatchCoverage/Solve.hs @@ -0,0 +1,930 @@ +{-# LANGUAGE DataKinds #-} + +module Unison.PatternMatchCoverage.Solve where + +import Control.Monad.State +import Control.Monad.Trans.Compose +import Control.Monad.Trans.Maybe +import Data.Foldable +import Data.Function +import Data.Functor +import Data.Functor.Compose +import Data.List.NonEmpty (NonEmpty (..)) +import qualified Data.Sequence as Seq +import qualified Data.Set as Set +import Unison.ConstructorReference (ConstructorReference) +import Unison.Pattern (Pattern) +import qualified Unison.Pattern as Pattern +import Unison.PatternMatchCoverage.Class +import Unison.PatternMatchCoverage.Constraint (Constraint) +import qualified Unison.PatternMatchCoverage.Constraint as C +import Unison.PatternMatchCoverage.Fix +import Unison.PatternMatchCoverage.GrdTree +import Unison.PatternMatchCoverage.IntervalSet (IntervalSet) +import qualified Unison.PatternMatchCoverage.IntervalSet as IntervalSet +import Unison.PatternMatchCoverage.ListPat +import Unison.PatternMatchCoverage.Literal +import Unison.PatternMatchCoverage.NormalizedConstraints +import Unison.PatternMatchCoverage.PmGrd +import Unison.PatternMatchCoverage.PmLit (PmLit) +import qualified Unison.PatternMatchCoverage.PmLit as PmLit +import qualified Unison.PatternMatchCoverage.UFMap as UFMap +import Unison.Prelude +import Unison.Type (Type) +import qualified Unison.Util.Pretty as P +import Unison.Var (Var) + +-- | top-down traversal of the 'GrdTree' that produces: +-- +-- * a refinement type for values that do not match the 'GrdTree' +-- * a new 'GrdTree' annotated with refinement types at the nodes for +-- values that cause an effect to be performed and values that match +-- the case at the leaves. +-- +-- If the former is inhabited then its inhabitants are unmatched +-- values. If the leaves of the latter are inhabited then the case is +-- redundant. +uncoverAnnotate :: + 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 z grdtree0 = cata phi grdtree0 z + where + phi = \case + -- There is no way to fail matching a leaf, return the empty set + -- to represent false. + LeafF l -> \nc -> pure (Set.empty, Leaf (nc, l)) + ForkF (kinit :| 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)) + GrdF grd k -> \nc0 -> case grd of + PmCon var con convars -> do + handleGrd (PosCon var con convars) (NegCon var con) k nc0 + PmLit var lit -> do + handleGrd (PosLit var lit) (NegLit var lit) k nc0 + PmListHead listVar n el elt -> do + nc <- addLiteral' nc0 (PosListHead listVar n el elt) + k nc + PmListTail listVar n el elt -> do + nc <- addLiteral' nc0 (PosListTail listVar n el elt) + k nc + PmListInterval listVar lb ub -> do + let iset = IntervalSet.singleton (lb, ub) + handleGrd (NegListInterval listVar (IntervalSet.complement iset)) (NegListInterval listVar iset) k nc0 + -- (ncmatch, t) <- k nc0 + -- ncNoMatch <- addLiteral' nc0 (NegListInterval listVar miset) + -- -- todo: limit size + -- pure (Set.union ncMatch ncNoMatch, t) + -- PmList var listPat mi convars -> + -- let miset = IntervalSet.singleton mi + -- in handleGrd (PosList var listPat miset convars) (NegList var miset) k nc0 + PmBang var -> do + (ncCont, t) <- k nc0 + ncEff <- addLiteral' nc0 (Effectful var) + let t' = Grd ncEff t + pure (ncCont, t') + PmLet var expr typ -> do + nc <- addLiteral' nc0 (Let var expr typ) + k nc + + -- Constructors and literals are handled uniformly except that + -- they pass different positive and negative literals. + handleGrd pos neg k nc0 = do + ncNoMatch <- addLiteral' nc0 neg + ncMatch <- addLiteral' nc0 pos + (ncMatch, t) <- k ncMatch + -- A match can fail bacause it fails to match the immediate + -- pattern or it can match the immediate pattern but fail to + -- match some pattern or guard defined later in this same case. + -- + -- This split can lead to an exponential number of terms, so we + -- limit this growth to a constant, conservatively + -- approximating. This is known as "throttling" in the paper and + -- described in section 5.2. + let ncFinalCandidate = Set.union ncMatch ncNoMatch + ncFinal = case Set.size ncFinalCandidate >= 30 of + True -> nc0 + False -> ncFinalCandidate + pure (ncFinal, t) + + -- Add a literal to each term in our DNF, dropping terms that + -- become contradictory + addLiteral' :: + Set (NormalizedConstraints vt v loc) -> + Literal vt v loc -> + m (Set (NormalizedConstraints vt v loc)) + addLiteral' ncs0 lit = foldlM phi Set.empty ncs0 + where + phi ncs nc = + addLiteral lit nc <&> \case + Nothing -> ncs + Just nc -> Set.insert nc ncs + +-- | Collect accessible, inaccessible, and redundant GRHSs +classify :: + forall vt v loc l. + GrdTree (Set (NormalizedConstraints vt v loc)) (Set (NormalizedConstraints vt v loc), l) -> + ([l], [l], [l]) +classify = cata classifyAlg + +classifyAlg :: + forall vt v loc l. + GrdTreeF (Set (NormalizedConstraints vt v loc)) (Set (NormalizedConstraints vt v loc), l) ([l], [l], [l]) -> + ([l], [l], [l]) +classifyAlg = \case + LeafF (rt, l) -> + case inh rt of + True -> ([l], [], []) + False -> ([], [], [l]) + GrdF rt rest -> + case inh rt of + True -> + -- The rest of the subtree is redundant, but an effect is + -- performed. Classify this as "Inaccessible". + case rest of + ([], [], x : xs) -> ([], [x], xs) + _ -> rest + False -> rest + ForkF xs -> foldr (\(a, b, c) ~(acc, inacc, redun) -> (a ++ acc, b ++ inacc, c ++ redun)) ([], [], []) xs + where + -- inhabitation check + inh = not . Set.null + +-- | Expand a full DNF term (i.e. each term identifies one and only +-- one solution) into a pattern. +expand :: + forall vt v loc. + Var v => + v -> + NormalizedConstraints vt v loc -> + Pattern () +expand x nc = + let (_xcanon, xvi, nc') = expectCanon x nc + in case vi_con xvi of + Vc'Constructor pos _neg -> case pos of + Nothing -> Pattern.Unbound () + Just (dc, convars) -> + Pattern.Constructor () dc (map (\(v, _) -> expand v nc') convars) + Vc'Boolean pos _neg -> case pos of + Nothing -> Pattern.Unbound () + Just b -> Pattern.Boolean () b + Vc'ListRoot _typ consPos snocPos intset -> + let matchedLength = on (+) length consPos snocPos + mmaxLength = IntervalSet.lookupMax intset + matchIsIncomplete = case mmaxLength of + Nothing -> True + Just maxLength -> matchedLength < maxLength + rootPat = case matchIsIncomplete of + True -> Pattern.Unbound () + False -> Pattern.SequenceLiteral () [] + snoced = foldr (\a b -> Pattern.SequenceOp () b Pattern.Snoc (expand a nc')) rootPat snocPos + consed = foldr (\a b -> Pattern.SequenceOp () (expand a nc') Pattern.Cons b) snoced consPos + in consed + _ -> Pattern.Unbound () + +-- | Expand the given variable into inhabited patterns. This is done +-- as a final step on the refinement type unmatched terms (see +-- 'uncoverAnnotate'). +generateInhabitants :: (Pmc vt v loc m) => v -> Set (NormalizedConstraints vt v loc) -> m [Pattern ()] +generateInhabitants v ncs = do + sols <- concat . fmap toList <$> traverse (expandSolution v) (toList ncs) + pure $ map (expand v) sols + +-- | Instantiate a variable to a given constructor. +instantiate :: + forall vt v loc x m. + (Pmc vt v loc m) => + Fuel -> + NormalizedConstraints vt v loc -> + v -> + -- | constructor + x -> + -- | type of datacon's args + [Type vt loc] -> + -- | produce positive constraint + (v -> x -> [(v, Type vt loc)] -> [Constraint vt v loc]) -> + m (Maybe (NormalizedConstraints vt v loc, [(v, Type vt loc)])) +instantiate fuel nc x c argTyps posConstraint = do + -- todo: centralize this declVar logic. Currently in 'addLiteral' and here. + newVars :: [(var, typ)] <- traverse (\t -> (,t) <$> fresh) argTyps + let nc' = foldr (\(v, t) b -> declVar v t id b) nc newVars + cons = posConstraint x c newVars + mnc <- runMaybeT do + nc <- MaybeT (addConstraints cons nc') + -- mark all new fields as dirty as we need to ensure they are + -- inhabited + let nc' = foldr (\(v, _) b -> markDirty v b) nc newVars + -- branching factor + let newFuel = case length newVars > 1 of + True -> min fuel 3 + False -> fuel + -- we must ensure that all strict fields are inhabited + MaybeT (ensureInhabited newFuel nc') + pure ((\x -> (x, newVars)) <$> mnc) + +-- | Given a variable and a term in DNF, expand it to an identical DNF +-- expression with enough positive info to print pattern suggestions. +expandSolution :: + forall vt v loc m. + Pmc vt v loc m => + v -> + NormalizedConstraints vt v loc -> + m (Set (NormalizedConstraints vt v loc)) +expandSolution x nc = + let go fuel x nc + -- If we run out of fuel conservatively assume the term is + -- inhabited. + | fuel == 0 = pure (Set.singleton nc) + | otherwise = + let (_xcanon, xvi, nc') = expectCanon x nc + in withConstructors (pure (Set.singleton nc')) xvi \cs posConstraint _negConstraint -> + -- We have some constructors to attempt + -- instantiation with. Instantiate each one, if + -- doesn't lead to a contradiction then add it to + -- the set of valid solutions. + let phi (cref, cvt) = do + instantiate initFuel nc' x cref cvt posConstraint >>= \case + Nothing -> pure Set.empty -- contradiction + Just (nc'', newVars) -> case newVars of + [] -> pure (Set.singleton nc'') + _ -> + -- If we have the match expression: + -- @ + -- match blerg : Maybe (Maybe ()) with + -- Nothing -> () + -- Just Nothing -> () + -- @ + -- + -- Then we would like to suggest @Just (Just _)@ rather than @Just _@. + -- To accomplish this, we recurse and expand variables for which we have + -- negative information. + + -- branching factor + let newFuel = case length newVars > 1 of + True -> min fuel 3 + False -> fuel + in Set.fromList + <$> foldlM + ( \b (v, _t) -> + Set.toList . Set.unions + <$> traverse + ( \nc -> + case expectCanon v nc of + (_vc, vi, nc') -> case vi_con vi of + Vc'Constructor _pos neg + | not (Set.null neg) -> go (newFuel - 1) v nc' + Vc'Boolean _pos neg + | not (Set.null neg) -> go (newFuel - 1) v nc' + Vc'ListRoot _typ _posCons _posSnoc neg + | not (IntervalSet.singleton (0, maxBound) == neg) -> go (newFuel - 1) v nc' + _ -> pure (Set.singleton nc') + ) + b + ) + [nc''] + newVars + in foldr (\a b s -> phi a >>= \a' -> b (Set.union a' s)) pure cs Set.empty + in go initFuel x nc + +withConstructors :: + forall vt v loc r m. + Pmc vt v loc m => + m r -> + VarInfo vt v loc -> + ( forall x. + [(x, [Type vt loc])] -> + (v -> x -> [(v, Type vt loc)] -> [Constraint vt v loc]) -> + (v -> x -> Constraint vt v loc) -> + m r + ) -> + m r +withConstructors nil vinfo k = do + getConstructors typ >>= \case + ConstructorType cs -> do + arg <- for cs \(v, cref, _) -> do + cvts <- getConstructorVarTypes typ cref + pure ((v, cref), cvts) + k arg (\v (_, cref) args -> [C.PosCon v cref args]) (\v (_, cref) -> C.NegCon v cref) + SequenceType _cs -> + let Vc'ListRoot elemType consPos snocPos iset = case vi_con vinfo of + Vc'ListRoot {} -> vi_con vinfo + _ -> error "impossible: constraint for sequence type not a list root" + varCount = length consPos + length snocPos + minLen = fromMaybe 0 $ IntervalSet.lookupMin iset + + mkPosCons :: (Int -> [v] -> [Constraint vt v loc]) -> Int -> [v] -> [Constraint vt v loc] + mkPosCons z elvs0 = foldr (\_ b n (elv : elvs) -> C.PosListHead v n elv : b (n + 1) elvs) z consPos elvs0 + + mkPosSnoc :: (Int -> [v] -> [Constraint vt v loc]) -> Int -> [v] -> [Constraint vt v loc] + mkPosSnoc z elvs0 = foldr (\_ b n (elv : elvs) -> C.PosListTail v n elv : b (n + 1) elvs) z snocPos elvs0 + + constraints :: [(([(v, Type vt loc)] -> [Constraint vt v loc], Constraint vt v loc), [Type vt loc])] + constraints = + let mk f elvs = mkPosCons (\_ elvs -> mkPosSnoc (\_ elvs -> f elvs) 0 elvs) 0 (map fst elvs) + in [ ((mk \[] -> [], C.NegListInterval v (IntervalSet.singleton (minLen, maxBound))), replicate varCount elemType) + ] + + mkPos _v (pos, _neg) args = + pos args + mkNeg _v (_pos, neg) = + neg + in k constraints mkPos mkNeg + BooleanType -> do + k [(True, []), (False, [])] (\v b _ -> [C.PosLit v (PmLit.Boolean b)]) (\v b -> C.NegLit v (PmLit.Boolean b)) + OtherType -> nil + where + typ = vi_typ vinfo + v = vi_id vinfo + +mkMatchingInterval :: ListPat -> IntervalSet +mkMatchingInterval = \case + Cons -> IntervalSet.singleton (1, maxBound) + Snoc -> IntervalSet.singleton (1, maxBound) + Nil -> IntervalSet.singleton (0, 0) + +-- | Test that the given variable is inhabited. This test is +-- undecidable in general so we adopt a fuel based approach as +-- described in section 3.7. +inhabited :: + forall vt v loc m. + Pmc vt v loc m => + Fuel -> + v -> + NormalizedConstraints vt v loc -> + m (Maybe (NormalizedConstraints vt v loc)) +inhabited fuel x nc0 = + let (_xcanon, xvi, nc') = expectCanon x nc0 + in withConstructors (pure (Just nc')) xvi \cs posConstraint negConstraint -> + -- one of the constructors must be inhabited, Return the + -- first non-contradictory instantiation. + let phi (cref, cvt) b nc = do + instantiate fuel nc x cref cvt posConstraint >>= \case + Nothing -> do + -- record failed instantiation attempt so we don't + -- attempt to instantiate this constructor again + addConstraint (negConstraint x cref) nc >>= \case + Nothing -> b nc + Just nc -> b nc + Just _ -> pure (Just nc) + in foldr phi (\_ -> pure Nothing) cs nc' + +newtype Fuel = Fuel Int + deriving newtype (Show, Eq, Ord, Enum, Bounded, Num) + +initFuel :: Fuel +initFuel = 8 + +-- | Check that all variables marked dirty are inhabited. +ensureInhabited :: + forall vt v loc m. + Pmc vt v loc m => + Fuel -> + NormalizedConstraints vt v loc -> + m (Maybe (NormalizedConstraints vt v loc)) +ensureInhabited fuel nc0@NormalizedConstraints {dirtySet} + | fuel == 0 = pure (Just clean) -- out of fuel, assume inhabited + | otherwise = do + -- all dirty vars must be inhabited or this NormalizedConstraints + -- is dropped + let phi dirtyVar b nc = do + nc <- MaybeT (inhabited (fuel - 1) dirtyVar nc) + b nc + in runMaybeT (foldr phi pure dirtySet clean) + where + clean = nc0 {dirtySet = mempty} + +-- | Add a formula literal to our normalized constraint set. This +-- corresponds to fig 7. +addLiteral :: + forall vt v loc m. + (Pmc vt v loc m) => + Literal vt v loc -> + NormalizedConstraints vt v loc -> + m (Maybe (NormalizedConstraints vt v loc)) +addLiteral lit0 nabla0 = runMaybeT do + nc <- MaybeT $ case lit0 of + F -> pure Nothing + T -> pure (Just nabla0) + PosCon var datacon convars -> + let ctx = foldr (\(trm, typ) b -> declVar trm typ id b) nabla0 convars + c = C.PosCon var datacon convars + in addConstraint c ctx + NegCon var datacon -> addConstraint (C.NegCon var datacon) nabla0 + PosLit var lit -> addConstraint (C.PosLit var lit) nabla0 + NegLit var lit -> addConstraint (C.NegLit var lit) nabla0 + PosListHead listRoot n listElem listElemType -> do + let nabla1 = declVar listElem listElemType id nabla0 + c = C.PosListHead listRoot n listElem + addConstraint c nabla1 + PosListTail listRoot n listElem listElemType -> do + let nabla1 = declVar listElem listElemType id nabla0 + c = C.PosListTail listRoot n listElem + addConstraint c nabla1 + NegListInterval listVar iset -> addConstraint (C.NegListInterval listVar iset) nabla0 + Effectful var -> addConstraint (C.Effectful var) nabla0 + Let var _expr typ -> pure (Just (declVar var typ id nabla0)) + MaybeT (ensureInhabited initFuel nc) + +insertVarInfo :: + forall vt v loc. + Ord v => + v -> + VarInfo vt v loc -> + NormalizedConstraints vt v loc -> + NormalizedConstraints vt v loc +insertVarInfo k v nc@NormalizedConstraints {constraintMap} = + nc {constraintMap = UFMap.insert k v constraintMap} + +-- | Add a constraint to our normalized constraint set. This +-- corresponds to fig 7. +addConstraint :: + forall vt v loc m. + (Pmc vt v loc m) => + Constraint vt v loc -> + NormalizedConstraints vt v loc -> + m (Maybe (NormalizedConstraints vt v loc)) +addConstraint con0 nc = + debugConstraint <$> case con0 of + C.PosLit var pmlit -> + let updateLiteral pos neg lit + | Just lit1 <- pos, + lit1 == lit = case lit1 == lit of + -- we already have this positive constraint + True -> (pure (), Ignore) + -- contradicts positive info + False -> (contradiction, Ignore) + -- the constraint contradicts negative info + | Set.member lit neg = (contradiction, Ignore) + | otherwise = (pure (), Update (Just lit, neg)) + in modifyLiteralC var pmlit updateLiteral nc + C.NegLit var pmlit -> + let updateLiteral pos neg lit + -- the constraint contradicts positive info + | Just lit1 <- pos, lit1 == lit = (contradiction, Ignore) + -- we already have this negative constraint + | Set.member lit neg = (pure (), Ignore) + | otherwise = (pure (), Update (pos, Set.insert lit neg)) + in modifyLiteralC var pmlit updateLiteral nc + C.NegListInterval var negMatchInterval -> + let updateList _typ pCons pSnoc posMatchInterval + -- No lengths are accepted + | IntervalSet.null newMatchInterval = (contradiction, Ignore) + -- This length constraint forces equating some cons and snoc matches + | let unconflictedLen = length pCons + length pSnoc, + Just maxLen <- IntervalSet.lookupMax newMatchInterval, + maxLen < unconflictedLen = + let varsToEquate = unconflictedLen - maxLen + (newPSnoc, vars) = + let (_as, bs) = Seq.splitAt (length pCons - varsToEquate) pCons + (cs, ds) = Seq.splitAt (length pSnoc - varsToEquate) pSnoc + in (cs, zip (toList bs) (toList ds)) + in (equate vars, Update (pCons, newPSnoc, newMatchInterval)) + | otherwise = + (populateCons var pCons newMatchInterval, Update (pCons, pSnoc, newMatchInterval)) + where + newMatchInterval = IntervalSet.difference posMatchInterval negMatchInterval + in modifyListC var updateList nc + C.PosListHead r n e -> + let updateList _elmType posCons posSnocs iset + -- there is an existing positive constraint on this element + | Just existingElemVar <- Seq.lookup n posCons = (equate [(e, existingElemVar)], Ignore) + -- a list of this length is proscribed + | let minPatLen = length posCons + 1, + Just maxLen <- IntervalSet.lookupMax iset, + maxLen < minPatLen = + (contradiction, Ignore) + -- the length constraint forces us to equate some cons and snoc patterns + | let unconflictedLen = length posCons + length posSnocs + 1, + Just maxLen <- IntervalSet.lookupMax iset, + maxLen < unconflictedLen = + let posCons' = posCons Seq.|> e + e' = Seq.index posSnocs (maxLen - length posCons') + in (equate [(e, e')], Update (posCons', posSnocs, iset)) + | otherwise = + let posCons' = posCons Seq.|> e + iset' = IntervalSet.delete (0, length posCons' - 1) iset + in (pure (), Update (posCons', posSnocs, iset')) + in modifyListC r updateList nc + C.PosListTail r n e -> + let updateList _elmType posCons posSnoc iset + -- there is an existing positive constraint on this element + | Just existingElemVar <- Seq.lookup n posSnoc = (equate [(e, existingElemVar)], Ignore) + -- a list of this length is proscribed + | let minPatLen = length posSnoc + 1, + Just maxLen <- IntervalSet.lookupMax iset, + maxLen < minPatLen = + (contradiction, Ignore) + -- the length constraint forces us to equate some cons and snoc patterns + | let unconflictedLen = length posCons + length posSnoc + 1, + Just maxLen <- IntervalSet.lookupMax iset, + maxLen < unconflictedLen = + let posSnoc' = posSnoc Seq.|> e + e' = Seq.index posCons (maxLen - length posSnoc') + in (equate [(e, e')], Update (posCons, posSnoc', iset)) + | otherwise = + let posSnoc' = posSnoc Seq.|> e + iset' = IntervalSet.delete (0, length posSnoc' - 1) iset + in (populateCons r posCons iset', Update (posCons, posSnoc', iset')) + in modifyListC r updateList nc + C.PosCon var datacon convars -> + let updateConstructor pos neg + | Just (datacon1, convars1) <- pos = case datacon == datacon1 of + True -> do + -- we already have an assertion, so equate convars + let varsToEquate = zipWith (\(y, _) (z, _) -> (y, z)) convars convars1 + (equate varsToEquate, Ignore) + False -> (contradiction, Ignore) + -- contradicts negative info + | True <- Set.member datacon neg = (contradiction, Ignore) + | otherwise = + -- no conflicting info, add constraint + (pure (), Update (Just (datacon, convars), neg)) + in modifyConstructorC var updateConstructor nc -- runC nc (put =<< modifyConstructor var updateConstructor =<< get) + C.NegCon var datacon -> + let updateConstructor pos neg + -- contradicts positive info + | Just (datacon1, _) <- pos, datacon1 == datacon = (contradiction, Ignore) + -- we already have this negative constraint + | Set.member datacon neg = (pure (), Ignore) + | otherwise = (pure (), Update (pos, Set.insert datacon neg)) + in modifyConstructorC var updateConstructor nc + C.Effectful var -> + case expectCanon var nc of + (var, vi, nc) + | otherwise -> pure $ Just $ insertVarInfo var vi {vi_eff = IsEffectful} nc + C.Eq x y -> union x y nc + where + debugConstraint x = + let debugOutput = + P.sep + "\n" + [ P.hang (P.red "input constraints: ") (prettyNormalizedConstraints nc), + P.hang (P.yellow "additional constraint: ") (C.prettyConstraint con0), + P.hang (P.green "resulting constraint: ") (maybe "contradiction" prettyNormalizedConstraints x), + "" + ] + in if False then trace (P.toAnsiUnbroken debugOutput) x else x + +-- | Like 'addConstraint', but for a list of constraints +addConstraints :: + forall vt v loc m. + (Pmc vt v loc m) => + [Constraint vt v loc] -> + NormalizedConstraints vt v loc -> + m (Maybe (NormalizedConstraints vt v loc)) +addConstraints cs nc0 = runMaybeT $ foldlM (\b a -> MaybeT (addConstraint a b)) nc0 cs + +-- | Equate two variables +union :: + forall vt v loc m. + (Pmc vt v loc m) => + v -> + v -> + NormalizedConstraints vt v loc -> + m (Maybe (NormalizedConstraints vt v loc)) +union v0 v1 nc@NormalizedConstraints {constraintMap} = + UFMap.union v0 v1 constraintMap \chosenCanon nonCanonValue m -> + -- In this block we want to collect the constraints from the + -- non-canonical value and add them to the canonical value. + + -- literals are handled uniformly + let handleLit :: forall x. (x -> PmLit) -> Maybe x -> Set x -> ([Constraint vt v loc], [Constraint vt v loc]) + handleLit toPmLit pos neg = + let posC = case pos of + Nothing -> [] + Just lit -> [C.PosLit chosenCanon (toPmLit lit)] + negC = foldr (\a b -> C.NegLit chosenCanon (toPmLit a) : b) [] neg + in (posC, negC) + constraints = posCon ++ negCon ++ effCon + (posCon, negCon) = case vi_con nonCanonValue of + Vc'Constructor pos neg -> + let posC = case pos of + Nothing -> [] + Just (datacon, convars) -> [C.PosCon chosenCanon datacon convars] + negC = foldr (\a b -> C.NegCon chosenCanon a : b) [] neg + in (posC, negC) + Vc'ListRoot _typ posCons posSnoc iset -> + let consConstraints = map (\(i, x) -> C.PosListHead chosenCanon i x) (zip [0 ..] (toList posCons)) + snocConstraints = map (\(i, x) -> C.PosListTail chosenCanon i x) (zip [0 ..] (toList posSnoc)) + neg = [C.NegListInterval chosenCanon (IntervalSet.complement iset)] + in (consConstraints ++ snocConstraints, neg) + Vc'Boolean pos neg -> handleLit PmLit.Boolean pos neg + Vc'Int pos neg -> handleLit PmLit.Int pos neg + Vc'Nat pos neg -> handleLit PmLit.Nat pos neg + Vc'Float pos neg -> handleLit PmLit.Float pos neg + Vc'Text pos neg -> handleLit PmLit.Text pos neg + Vc'Char pos neg -> handleLit PmLit.Char pos neg + effCon = case vi_eff nonCanonValue of + IsNotEffectful -> [] + IsEffectful -> [C.Effectful chosenCanon] + in addConstraints constraints nc {constraintMap = m} + +modifyList :: + forall vt v loc. + (Var v) => + v -> + ( Type vt loc -> + Seq v -> + Seq v -> + IntervalSet -> + ConstraintUpdate (Seq v, Seq v, IntervalSet) + ) -> + NormalizedConstraints vt v loc -> + NormalizedConstraints vt v loc +modifyList v f nc = runIdentity $ modifyListF v (\a b c d -> Identity (f a b c d)) nc + +modifyListC :: + forall vt v loc m. + (Pmc vt v loc m) => + v -> + ( Type vt loc -> + Seq v -> + Seq v -> + IntervalSet -> + (C vt v loc m (), ConstraintUpdate (Seq v, Seq v, IntervalSet)) + ) -> + NormalizedConstraints vt v loc -> + m (Maybe (NormalizedConstraints vt v loc)) +modifyListC v f nc0 = + let (ccomp, nc1) = modifyListF v f nc0 + in fmap snd <$> runC nc1 ccomp + +modifyListF :: + forall vt v loc f. + (Var v, Functor f) => + v -> + ( Type vt loc -> + Seq v -> + Seq v -> + IntervalSet -> + f (ConstraintUpdate (Seq v, Seq v, IntervalSet)) + ) -> + NormalizedConstraints vt v loc -> + f (NormalizedConstraints vt v loc) +modifyListF v f nc = + let g vc = getCompose (posAndNegList (\typ pcons psnoc iset -> Compose (f typ pcons psnoc iset)) vc) + in modifyVarConstraints v g nc + +modifyConstructor :: + forall vt v loc. + (Var v) => + v -> + ( (Maybe (ConstructorReference, [(v, Type vt loc)])) -> + Set ConstructorReference -> + (ConstraintUpdate (Maybe (ConstructorReference, [(v, Type vt loc)]), Set ConstructorReference)) + ) -> + NormalizedConstraints vt v loc -> + NormalizedConstraints vt v loc +modifyConstructor v f nc = runIdentity $ modifyConstructorF v (\a b -> Identity (f a b)) nc + +modifyConstructorC :: + forall vt v loc m. + Pmc vt v loc m => + v -> + ( (Maybe (ConstructorReference, [(v, Type vt loc)])) -> + Set ConstructorReference -> + (C vt v loc m (), ConstraintUpdate (Maybe (ConstructorReference, [(v, Type vt loc)]), Set ConstructorReference)) + ) -> + NormalizedConstraints vt v loc -> + m (Maybe (NormalizedConstraints vt v loc)) +modifyConstructorC v f nc0 = + let (ccomp, nc1) = modifyConstructorF v f nc0 + in fmap snd <$> runC nc1 ccomp + +modifyConstructorF :: + forall vt v loc f. + (Var v, Functor f) => + v -> + ( (Maybe (ConstructorReference, [(v, Type vt loc)])) -> + Set ConstructorReference -> + f (ConstraintUpdate (Maybe (ConstructorReference, [(v, Type vt loc)]), Set ConstructorReference)) + ) -> + NormalizedConstraints vt v loc -> + f (NormalizedConstraints vt v loc) +modifyConstructorF v f nc = + let g vc = getCompose (posAndNegConstructor (\pos neg -> Compose (f pos neg)) vc) + in modifyVarConstraints v g nc + +modifyLiteral :: + forall vt v loc. + (Var v) => + v -> + PmLit -> + ( forall a. + (Ord a) => + -- positive info + Maybe a -> + -- negative info + Set a -> + -- the passed in PmLit, unpacked + a -> + ConstraintUpdate (Maybe a, Set a) + ) -> + NormalizedConstraints vt v loc -> + NormalizedConstraints vt v loc +modifyLiteral v lit f nc = runIdentity $ modifyLiteralF v lit (\a b c -> Identity (f a b c)) nc + +modifyLiteralC :: + forall vt v loc m. + (Pmc vt v loc m) => + v -> + PmLit -> + ( forall a. + (Ord a) => + -- positive info + Maybe a -> + -- negative info + Set a -> + -- the passed in PmLit, unpacked + a -> + (C vt v loc m (), ConstraintUpdate (Maybe a, Set a)) + ) -> + NormalizedConstraints vt v loc -> + m (Maybe (NormalizedConstraints vt v loc)) +modifyLiteralC v lit f nc0 = + let (ccomp, nc1) = modifyLiteralF v lit f nc0 + in fmap snd <$> runC nc1 ccomp + +-- | Update constraints on some literal by only depending on their Ord +-- instance. +modifyLiteralF :: + forall vt v loc f. + (Var v, Functor f) => + v -> + PmLit -> + ( forall a. + (Ord a) => + -- positive info + Maybe a -> + -- negative info + Set a -> + -- the passed in PmLit, unpacked + a -> + f (ConstraintUpdate (Maybe a, Set a)) + ) -> + NormalizedConstraints vt v loc -> + f (NormalizedConstraints vt v loc) +modifyLiteralF v lit f nc = + let g vc = getCompose (posAndNegLiteral (\pos neg candidate -> Compose (f pos neg candidate)) lit vc) + in modifyVarConstraints v g nc + +modifyVarConstraints :: + forall vt v loc f. + (Var v, Functor f) => + v -> + ( VarConstraints vt v loc -> + f (ConstraintUpdate (VarConstraints vt v loc)) + ) -> + NormalizedConstraints vt v loc -> + -- | applied to 'Vc'Constructor' + f (NormalizedConstraints vt v loc) +modifyVarConstraints v updateVarConstraint nc0 = do + updateF v (\_v vi -> fmap (\vc -> vi {vi_con = vc}) <$> updateVarConstraint (vi_con vi)) nc0 +{-# INLINE modifyVarConstraints #-} + +-- | Modify the positive and negative constraints of a constructor. +posAndNegConstructor :: + forall f vt v loc. + Functor f => + ( (Maybe (ConstructorReference, [(v, Type vt loc)])) -> + Set ConstructorReference -> + f (Maybe (ConstructorReference, [(v, Type vt loc)]), Set ConstructorReference) + ) -> + VarConstraints vt v loc -> + f (VarConstraints vt v loc) +posAndNegConstructor f = \case + Vc'Constructor pos neg -> uncurry Vc'Constructor <$> f pos neg + _ -> error "impossible: posAndNegConstructor called on a literal" +{-# INLINE posAndNegConstructor #-} + +-- | Modify the positive and negative constraints in a way that +-- doesn't rely upon the particular literal type, but only on it being +-- an instance of Ord. +posAndNegLiteral :: + forall f vt v loc. + Functor f => + ( forall a. + (Ord a) => + Maybe a -> + Set a -> + a -> + f (Maybe a, Set a) + ) -> + PmLit -> + VarConstraints vt v loc -> + f (VarConstraints vt v loc) +posAndNegLiteral f lit = \case + Vc'Boolean pos neg + | PmLit.Boolean b <- lit -> uncurry Vc'Boolean <$> f pos neg b + Vc'Int pos neg + | PmLit.Int b <- lit -> uncurry Vc'Int <$> f pos neg b + Vc'Nat pos neg + | PmLit.Nat b <- lit -> uncurry Vc'Nat <$> f pos neg b + Vc'Float pos neg + | PmLit.Float b <- lit -> uncurry Vc'Float <$> f pos neg b + Vc'Text pos neg + | PmLit.Text b <- lit -> uncurry Vc'Text <$> f pos neg b + Vc'Char pos neg + | PmLit.Char b <- lit -> uncurry Vc'Char <$> f pos neg b + Vc'Constructor _ _ -> error "impossible: posAndNegLiteral called on constructor" + _ -> error "impossible: incompatible PmLit and VarConstraints types" +{-# INLINE posAndNegLiteral #-} + +posAndNegList :: + forall f vt v loc. + Functor f => + ( Type vt loc -> + Seq v -> + Seq v -> + IntervalSet -> + f (Seq v, Seq v, IntervalSet) + ) -> + VarConstraints vt v loc -> + f (VarConstraints vt v loc) +posAndNegList f = \case + Vc'ListRoot typ posCons posSnocs iset -> (\(posCons, posSnocs, iset) -> Vc'ListRoot typ posCons posSnocs iset) <$> f typ posCons posSnocs iset + _ -> error "impossible: posAndNegList called on a something that isn't a list" +{-# INLINE posAndNegList #-} + +newtype C vt v loc m a = C + { unC :: + NormalizedConstraints vt v loc -> + m (Maybe (a, NormalizedConstraints vt v loc)) + } + deriving + (Functor, Applicative, Monad, MonadState (NormalizedConstraints vt v loc)) + via StateT (NormalizedConstraints vt v loc) (MaybeT m) + deriving (MonadTrans) via ComposeT (StateT (NormalizedConstraints vt v loc)) MaybeT + +contradiction :: Applicative m => C vt v loc m a +contradiction = C \_ -> pure Nothing + +update :: Pmc vt v loc m => v -> VarConstraints vt v loc -> C vt v loc m () +update v vc = do + nc0 <- get + let (var, vi, nc1) = expectCanon v nc0 + nc2 = markDirty var ((insertVarInfo var vi {vi_con = vc}) nc1) + put nc2 + +equate :: Pmc vt v loc m => [(v, v)] -> C vt v loc m () +equate vs = addConstraintsC (map (uncurry C.Eq) vs) + +lookupListElemTypeC :: Pmc vt v loc m => v -> C vt v loc m (Type vt loc) +lookupListElemTypeC listVar = do + nc0 <- get + let (_var, vi, nc1) = expectCanon listVar nc0 + put nc1 + pure $ getConst (posAndNegList (\elemTyp _ _ _ -> Const elemTyp) (vi_con vi)) + +addConstraintsC :: Pmc vt v loc m => [Constraint vt v loc] -> C vt v loc m () +addConstraintsC cs = do + nc <- get + lift (addConstraints cs nc) >>= \case + Nothing -> contradiction + Just nc -> put nc + +declVarC :: + Pmc vt v loc m => + v -> + Type vt loc -> + (VarInfo vt v loc -> VarInfo vt v loc) -> + C vt v loc m () +declVarC v vt vimod = do + nc0 <- get + let nc1 = declVar v vt vimod nc0 + put nc1 + +freshC :: + Pmc vt v loc m => + C vt v loc m v +freshC = lift fresh + +populateCons :: Pmc vt v loc m => v -> Seq v -> IntervalSet -> C vt v loc m () +populateCons listVar pCons iset = do + case IntervalSet.lookupMin iset of + Just minLen + | minLen > 0, + let targets = [length pCons .. minLen - 1], + not (null targets) -> do + elemTyp <- lookupListElemTypeC listVar + for_ targets \idx -> do + elv <- freshC + declVarC elv elemTyp id + addConstraintsC [C.PosListHead listVar idx elv] + _ -> pure () + +runC :: + Applicative m => + NormalizedConstraints vt v loc -> + C vt v loc m a -> + m (Maybe (a, NormalizedConstraints vt v loc)) +runC nc0 ca = unC ca nc0 diff --git a/parser-typechecker/src/Unison/PatternMatchCoverage/UFMap.hs b/parser-typechecker/src/Unison/PatternMatchCoverage/UFMap.hs new file mode 100644 index 000000000..1b95f1c19 --- /dev/null +++ b/parser-typechecker/src/Unison/PatternMatchCoverage/UFMap.hs @@ -0,0 +1,227 @@ +{-# LANGUAGE RecursiveDo #-} + +module Unison.PatternMatchCoverage.UFMap + ( UFMap, + UFValue (..), + empty, + lookupCanon, + insert, + union, + alterF, + alter, + keys, + toClasses, + ) +where + +import Control.Monad.Fix (MonadFix) +import Control.Monad.Trans.Except (ExceptT (..)) +import Data.Foldable (foldl') +import Data.Functor ((<&>)) +import Data.Functor.Compose (Compose (..)) +import Data.Functor.Identity (Identity (Identity, runIdentity)) +import Data.Functor.Sum (Sum (..)) +import Data.Map (Map) +import qualified Data.Map.Lazy as LazyMap +import qualified Data.Map.Strict as Map +import Data.Maybe (fromJust) +import Data.Set (Set) +import qualified Data.Set as Set + +-- import Lyg.Pretty + +newtype UFMap k v = UFMap (Map k (UFValue k v)) + deriving stock (Eq, Ord, Show) + +data UFValue k v + = -- | This is not the canonical value, lookup k in the map to try again + Indirection !k + | -- | The number of elements in the equivalence class + Canonical !Int !v + deriving stock (Eq, Ord, Show) + +empty :: UFMap k v +empty = UFMap Map.empty + +insert :: Ord k => k -> v -> UFMap k v -> UFMap k v +insert k !v m = + alter k (Just v) (\_ s _ -> Canonical s v) m + +alterF' :: + forall f k v. + (Functor f, Ord k) => + -- | The key to lookup + k -> + -- | The canonical key (use laziness to supply if unknown) + k -> + (k -> UFMap k v -> Maybe (f (UFMap k v))) -> + -- How to alter the canonical value + -- + -- N.B. deleting keys from a UFMap is not supported + -- + + -- | Nothing case + f (Maybe v) -> + -- | Just case + -- canonicalKey -> size -> value + (k -> Int -> v -> f (UFValue k v)) -> + UFMap k v -> + -- | Returns the canonical k, the size, the value, and the path + -- compressed UFMap + f (UFMap k v) +alterF' k0 kcanon loopGuard handleNothing handleJust map0 = + let phi :: k -> Maybe (UFValue k v) -> Sum ((,) k) f (Maybe (UFValue k v)) + phi k = + \case + Nothing -> InR (fmap (Canonical 1) <$> handleNothing) + Just alpha -> case alpha of + Indirection k -> InL (k, Just (Indirection kcanon)) + Canonical sizeOrig v -> InR (Just <$> handleJust k sizeOrig v) + go :: k -> UFMap k v -> f (UFMap k v) + go k ufm@(UFMap m) = case loopGuard k ufm of + Just short -> short + Nothing -> case LazyMap.alterF (phi k) k m of + InL (k, m') -> go k (UFMap m') + InR res -> UFMap <$> res + in go k0 map0 +{-# INLINE alterF' #-} + +alterFWithHalt :: + forall f k v. + (Functor f, Ord k) => + k -> + (k -> UFMap k v -> Maybe (f (UFMap k v))) -> + f (Maybe v) -> + (k -> Int -> v -> f (UFValue k v)) -> + UFMap k v -> + f (UFMap k v) +alterFWithHalt k0 isCanonical handleNothing handleJust map0 = + -- tie the canonicalK knot + let (canonicalK, res) = getCompose (alterF' k0 canonicalK loopGuard handleNothing' handleJust' map0) + handleNothing' = Compose (k0, handleNothing) + handleJust' k s v = Compose (k, handleJust k s v) + -- if the key is canonical then we halt and return it as the + -- left element of the tuple + loopGuard k m = Compose . (k,) <$> isCanonical k m + in res +{-# INLINE alterFWithHalt #-} + +alterF :: + forall f k v. + (Functor f, Ord k) => + k -> + f (Maybe v) -> + (k -> Int -> v -> f (UFValue k v)) -> + UFMap k v -> + f (UFMap k v) +alterF k = alterFWithHalt k (\_ _ -> Nothing) +{-# INLINE alterF #-} + +alter :: + forall k v. + (Ord k) => + k -> + Maybe v -> + (k -> Int -> v -> UFValue k v) -> + UFMap k v -> + UFMap k v +alter k handleNothing handleJust map0 = + runIdentity (alterF k (Identity handleNothing) (\k s v -> Identity (handleJust k s v)) map0) + +lookupCanon :: + Ord k => + k -> + UFMap k v -> + Maybe (k, Int, v, UFMap k v) +lookupCanon k m = + getCompose (alterF k nothing just m) + where + nothing = Compose Nothing + just k s v = Compose (Just (k, s, v, Canonical s v)) + +data UnionHaltReason k v + = KeyNotFound k + | MergeFailed v v + +data UnionValue k v a + = UnionValue k Int v (UFValue k v) a + deriving stock (Functor) + +union :: + forall m k v r. + (MonadFix m, Ord k) => + k -> + k -> + UFMap k v -> + (k -> v -> UFMap k v -> m (Maybe r)) -> + m (Maybe r) +union k0 k1 mapinit mergeValues = toMaybe do + rec let lu :: + k -> + UFMap k v -> + (k -> UFMap k v -> Maybe (Compose (Either (UnionHaltReason k v)) (UnionValue k v) (UFMap k v))) -> + Either (UnionHaltReason k v) (UnionValue k v (UFMap k v)) + lu k m loopGuard = getCompose (alterFWithHalt k loopGuard luNothing luJust m) + where + luNothing = Compose (Left (KeyNotFound k)) + luJust k s v = + -- a final value thunk is inserted before it is resolved, + -- as the final result cannot be known before we have + -- looked up both values and merged them + let newValue = + let newSize = case kcanon0 == kcanon1 of + True -> size0 + False -> size0 + size1 + in case chosenCanon == k of + True -> Canonical newSize canonValue + False -> Indirection chosenCanon + in Compose (Right (UnionValue k s v newValue newValue)) + UnionValue kcanon0 size0 v0 vfinal0 map0 <- ExceptT $ pure $ lu k0 mapinit \_ _ -> Nothing + UnionValue kcanon1 size1 v1 vfinal1 map1 <- ExceptT $ + pure $ lu k1 map0 \k m -> case k == kcanon0 of + False -> Nothing + True -> Just (Compose (Right (UnionValue k size0 v0 vfinal0 m))) + -- Join the smaller equivalence class to the larger to bound + -- worst case number of lookups to log(n). This is the same + -- strategy as the weighted fast-union algorithm. + let (chosenCanon, canonValue, nonCanonValue) = case size0 > size1 of + True -> (kcanon0, v0, v1) + False -> (kcanon1, v1, v0) + map2 <- + let res = + ExceptT $ + mergeValues chosenCanon nonCanonValue map1 <&> \case + Nothing -> Left (MergeFailed v0 v1) + Just x -> Right x + in -- Now that both lookups have completed we can safely force the + -- final values + vfinal0 `seq` vfinal1 `seq` res + pure map2 + where + toMaybe :: ExceptT (UnionHaltReason k v) m r -> m (Maybe r) + toMaybe (ExceptT action) = + action <&> \case + Right m -> Just m + Left r -> case r of + KeyNotFound _k -> Nothing + MergeFailed _v0 _v1 -> Nothing + +toClasses :: forall k v. Ord k => UFMap k v -> [(k, Set k, v)] +toClasses m0 = + let cmFinal :: Map k (k, Set k, v) + (_mfinal, cmFinal) = foldl' phi (m0, Map.empty) keys + keys = case m0 of + UFMap m -> Map.keys m + phi (m, cm) k = + let (kcanon, _, v, m') = fromJust (lookupCanon k m) + cm' = + Map.insertWith + (\(k0, s0, v0) (_k1, s1, _v1) -> (k0, s0 <> s1, v0)) + kcanon + (k, Set.singleton k, v) + cm + in (m', cm') + in Map.elems cmFinal + +keys :: UFMap k v -> [k] +keys (UFMap m) = Map.keys m diff --git a/parser-typechecker/src/Unison/PrintError.hs b/parser-typechecker/src/Unison/PrintError.hs index d785307b2..b4022f891 100644 --- a/parser-typechecker/src/Unison/PrintError.hs +++ b/parser-typechecker/src/Unison/PrintError.hs @@ -29,6 +29,7 @@ import qualified Unison.Names as Names import qualified Unison.Names.ResolutionResult as Names import qualified Unison.NamesWithHistory as NamesWithHistory import Unison.Parser.Ann (Ann (..)) +import Unison.Pattern (Pattern) import Unison.Prelude import qualified Unison.PrettyPrintEnv as PPE import qualified Unison.PrettyPrintEnv.Names as PPE @@ -37,6 +38,7 @@ import Unison.Referent (Referent, pattern Ref) import Unison.Result (Note (..)) import qualified Unison.Result as Result import qualified Unison.Settings as Settings +import Unison.Symbol (Symbol) import qualified Unison.Syntax.HashQualified as HQ (toString) import qualified Unison.Syntax.Lexer as L import qualified Unison.Syntax.Name as Name (toText) @@ -592,6 +594,24 @@ renderTypeError e env src curPath = case e of <> annotatedAsErrorSite src typeSite, "Make sure it's imported and spelled correctly." ] + UncoveredPatterns loc tms -> + mconcat + [ "Pattern match is non-exhaustive\n", + Pr.hang + "In the match:" + (annotatedAsErrorSite src loc), + "\n\n" + ] + <> Pr.hang + "Patterns not matched:\n" + ( Pr.bulleted + (map (\x -> Pr.lit (renderPattern env x)) (Nel.toList tms)) + ) + RedundantPattern loc -> + mconcat + [ "Pattern match is redundant\n", + Pr.hang "In the match case:" (annotatedAsErrorSite src loc) + ] UnknownTerm {..} -> let (correct, wrongTypes, wrongNames) = foldr sep id suggestions ([], [], []) @@ -810,6 +830,26 @@ renderTypeError e env src curPath = case e of -- C.InMatchBody -> "InMatchBody" simpleCause :: C.Cause v loc -> Pretty ColorText simpleCause = \case + C.UncoveredPatterns loc tms -> + mconcat + [ "Incomplete pattern matches:\n", + annotatedAsErrorSite src loc, + "\n\n", + "Uncovered cases:\n" + ] + <> Pr.sep "\n" (map (\x -> Pr.lit (renderPattern env x)) (Nel.toList tms)) + C.RedundantPattern loc -> + mconcat + [ "Redundant pattern match: ", + "\n", + annotatedAsErrorSite src loc + ] + C.InaccessiblePattern loc -> + mconcat + [ "Inaccessible pattern match: ", + "\n", + annotatedAsErrorSite src loc + ] C.TypeMismatch c -> mconcat ["TypeMismatch\n", " context:\n", renderContext env c] C.HandlerOfUnexpectedType loc typ -> @@ -1020,13 +1060,18 @@ renderContext env ctx@(C.Context es) = shortName v <> " : " <> renderType' env (C.apply ctx t) showElem _ (C.Marker v) = "|" <> shortName v <> "|" -renderTerm :: (IsString s, Var v) => Env -> C.Term v loc -> s +-- Term.Term' (TypeVar v loc) v loc + +renderTerm :: (IsString s, Var v) => Env -> Term.Term' (TypeVar.TypeVar loc0 v) v loc1 -> s renderTerm env e = let s = Color.toPlain $ TermPrinter.pretty' (Just 80) env (TypeVar.lowerTerm e) in if length s > Settings.renderTermMaxLength then fromString (take Settings.renderTermMaxLength s <> "...") else fromString s +renderPattern :: Env -> Pattern ann -> ColorText +renderPattern env e = Pr.renderUnbroken . Pr.syntaxToColor . fst $ TermPrinter.prettyPattern env TermPrinter.emptyAc 0 ([] :: [Symbol]) e + -- | renders a type with no special styling renderType' :: (IsString s, Var v) => Env -> Type v loc -> s renderType' env typ = diff --git a/parser-typechecker/src/Unison/Syntax/TermPrinter.hs b/parser-typechecker/src/Unison/Syntax/TermPrinter.hs index 9ed7c6d06..f2be2c7e3 100644 --- a/parser-typechecker/src/Unison/Syntax/TermPrinter.hs +++ b/parser-typechecker/src/Unison/Syntax/TermPrinter.hs @@ -9,6 +9,7 @@ module Unison.Syntax.TermPrinter prettyBindingWithoutTypeSignature, pretty0, runPretty, + prettyPattern, ) where diff --git a/parser-typechecker/src/Unison/Typechecker/Context.hs b/parser-typechecker/src/Unison/Typechecker/Context.hs index 161b07c28..0230fca92 100644 --- a/parser-typechecker/src/Unison/Typechecker/Context.hs +++ b/parser-typechecker/src/Unison/Typechecker/Context.hs @@ -42,10 +42,12 @@ where import Control.Lens (over, view, _2) import qualified Control.Monad.Fail as MonadFail +import Control.Monad.Fix (MonadFix (..)) import Control.Monad.State ( MonadState, StateT, evalState, + evalStateT, get, gets, put, @@ -59,6 +61,7 @@ import qualified Data.Foldable as Foldable import Data.Function (on) import Data.List import Data.List.NonEmpty (NonEmpty) +import qualified Data.List.NonEmpty as Nel import qualified Data.Map as Map import qualified Data.Sequence as Seq import Data.Sequence.NonEmpty (NESeq) @@ -81,9 +84,13 @@ import qualified Unison.DataDeclaration as DD import Unison.DataDeclaration.ConstructorId (ConstructorId) import Unison.Pattern (Pattern) import qualified Unison.Pattern as Pattern +import Unison.PatternMatchCoverage (checkMatch) +import Unison.PatternMatchCoverage.Class (EnumeratedConstructors (..), Pmc (..), traverseConstructors) +import qualified Unison.PatternMatchCoverage.ListPat as ListPat import Unison.Prelude import qualified Unison.PrettyPrintEnv as PPE import Unison.Reference (Reference) +import qualified Unison.Reference as Reference import Unison.Referent (Referent) import qualified Unison.Syntax.TypePrinter as TP import qualified Unison.Term as Term @@ -173,6 +180,14 @@ instance Monad (Result v loc) where CompilerBug bug es is >>= _ = CompilerBug bug es is {-# INLINE (>>=) #-} +instance MonadFix (Result v loc) where + mfix f = + let res = f theA + theA = case res of + Success _ a -> a + _ -> error "mfix Result: forced an unsuccessful value" + in res + btw' :: InfoNote v loc -> Result v loc () btw' note = Success (Seq.singleton note) () @@ -374,6 +389,9 @@ data Cause v loc | ConcatPatternWithoutConstantLength loc (Type v loc) | HandlerOfUnexpectedType loc (Type v loc) | DataEffectMismatch Unknown Reference (DataDeclaration v loc) + | UncoveredPatterns loc (NonEmpty (Pattern ())) + | RedundantPattern loc + | InaccessiblePattern loc deriving (Show) errorTerms :: ErrorNote v loc -> [Term v loc] @@ -765,6 +783,27 @@ getEffectDeclaration r = do getDataConstructorType :: (Var v, Ord loc) => ConstructorReference -> M v loc (Type v loc) getDataConstructorType = getConstructorType' Data getDataDeclaration +getDataConstructors :: (Var v) => Type v loc -> M v loc (EnumeratedConstructors (TypeVar v loc) v loc) +getDataConstructors typ + | Type.Ref' r <- typ, r == Type.booleanRef = pure BooleanType + | Type.App' (Type.Ref' r) arg <- typ, + r == Type.listRef = + let xs = + [ (ListPat.Cons, [arg]), + -- (ListPat.Snoc, [typ, arg]), + (ListPat.Nil, []) + ] + in pure (SequenceType xs) + | Just r <- theRef = do + decl <- getDataDeclaration r + pure $ ConstructorType [(v, ConstructorReference r i, ABT.vmap TypeVar.Universal t) | (i, (v, t)) <- zip [0 ..] (DD.constructors decl)] + | otherwise = pure OtherType + where + theRef = case typ of + Type.Apps' (Type.Ref' r@Reference.DerivedId {}) _targs -> Just r + Type.Ref' r@Reference.DerivedId {} -> Just r + _ -> Nothing + getEffectConstructorType :: (Var v, Ord loc) => ConstructorReference -> M v loc (Type v loc) getEffectConstructorType = getConstructorType' Effect go where @@ -1212,6 +1251,7 @@ synthesizeWanted e let outputType = existential' l B.Blank outputTypev appendContext [existential outputTypev] cwant <- checkCases scrutineeType outputType cases + pmcStuff e scrutinee scrutineeType cases want <- coalesceWanted cwant swant ctx <- getContext pure $ (apply ctx outputType, want) @@ -1219,6 +1259,57 @@ synthesizeWanted e l = loc e synthesizeWanted _e = compilerCrash PatternMatchFailure +getDataConstructorsAtType :: (Ord loc, Var v) => Type v loc -> M v loc (EnumeratedConstructors (TypeVar v loc) v loc) +getDataConstructorsAtType t0 = do + dataConstructors <- getDataConstructors t0 + res <- traverseConstructors (\v cr t -> (v,cr,) <$> fixType t) dataConstructors + pure res + where + fixType t = do + t <- ungeneralize t + let lastT = case t of + Type.Arrows' xs -> last xs + _ -> t + equate t0 lastT + applyM t + +instance (Ord loc, Var v) => Pmc (TypeVar v loc) v loc (StateT (Set v) (M v loc)) where + getConstructors = lift . getDataConstructorsAtType + getConstructorVarTypes t cref@(ConstructorReference _r cid) = do + getConstructors t >>= \case + ConstructorType cs -> case drop (fromIntegral cid) cs of + [] -> error $ show cref <> " not found in constructor list: " <> show cs + (_, _, consArgs) : _ -> case consArgs of + Type.Arrows' xs -> pure (init xs) + _ -> pure [] + BooleanType -> pure [] + OtherType -> pure [] + SequenceType {} -> pure [] + fresh = do + vs <- get + let v = Var.freshIn vs (Var.typed Var.Pattern) + put (Set.insert v vs) + pure v + +pmcStuff :: + forall v loc. + (Ord loc, Var v) => + Term v loc -> + Term v loc -> + Type v loc -> + [Term.MatchCase loc (Term v loc)] -> + MT v loc (Result v loc) () +pmcStuff wholeMatch _scrutinee scrutineeType cases = do + let matchLoc = ABT.annotation wholeMatch + scrutineeType <- applyM scrutineeType + (redundant, _inaccessible, uncovered) <- flip evalStateT (ABT.freeVars wholeMatch) do + checkMatch matchLoc 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 + checkUncovered *> checkRedundant + checkCases :: (Var v) => (Ord loc) => @@ -3051,3 +3142,8 @@ instance (Monad f) => Applicative (MT v loc f) where instance (Monad f) => MonadState (Env v loc) (MT v loc f) where get = MT \_ _ env -> pure (env, env) put env = MT \_ _ _ -> pure ((), env) + +instance MonadFix f => MonadFix (MT v loc f) where + mfix f = MT \a b c -> + let res = mfix (\ ~(wubble, _finalenv) -> runM (f wubble) a b c) + in res diff --git a/parser-typechecker/src/Unison/Typechecker/Extractor.hs b/parser-typechecker/src/Unison/Typechecker/Extractor.hs index 8d1952b1d..8f98e16aa 100644 --- a/parser-typechecker/src/Unison/Typechecker/Extractor.hs +++ b/parser-typechecker/src/Unison/Typechecker/Extractor.hs @@ -6,6 +6,7 @@ import Data.List.NonEmpty (NonEmpty) import qualified Data.Set as Set import qualified Unison.Blank as B import Unison.ConstructorReference (ConstructorReference) +import Unison.Pattern (Pattern) import Unison.Prelude hiding (whenM) import qualified Unison.Term as Term import Unison.Type (Type) @@ -242,6 +243,18 @@ duplicateDefinitions = C.DuplicateDefinitions vs -> pure vs _ -> mzero +uncoveredPatterns :: ErrorExtractor v loc (loc, NonEmpty (Pattern ())) +uncoveredPatterns = + cause >>= \case + C.UncoveredPatterns matchLoc xs -> pure (matchLoc, xs) + _ -> empty + +redundantPattern :: ErrorExtractor v loc loc +redundantPattern = + cause >>= \case + C.RedundantPattern patternLoc -> pure patternLoc + _ -> empty + typeMismatch :: ErrorExtractor v loc (C.Context v loc) typeMismatch = cause >>= \case diff --git a/parser-typechecker/src/Unison/Typechecker/TypeError.hs b/parser-typechecker/src/Unison/Typechecker/TypeError.hs index f09d1ffe4..4670ead83 100644 --- a/parser-typechecker/src/Unison/Typechecker/TypeError.hs +++ b/parser-typechecker/src/Unison/Typechecker/TypeError.hs @@ -5,6 +5,7 @@ module Unison.Typechecker.TypeError where import Data.Bifunctor (second) import Data.List.NonEmpty (NonEmpty) import qualified Unison.ABT as ABT +import Unison.Pattern (Pattern) import Unison.Prelude hiding (whenM) import Unison.Type (Type) import qualified Unison.Type as Type @@ -103,6 +104,8 @@ data TypeError v loc { defns :: NonEmpty (v, [loc]), note :: C.ErrorNote v loc } + | UncoveredPatterns loc (NonEmpty (Pattern ())) + | RedundantPattern loc | Other (C.ErrorNote v loc) deriving (Show) @@ -145,7 +148,9 @@ allErrors = unguardedCycle, unknownType, unknownTerm, - duplicateDefinitions + duplicateDefinitions, + redundantPattern, + uncoveredPatterns ] topLevelComponent :: Ex.InfoExtractor v a (TypeInfo v a) @@ -153,6 +158,16 @@ topLevelComponent = do defs <- Ex.topLevelComponent pure $ TopLevelComponent defs +redundantPattern :: Ex.ErrorExtractor v a (TypeError v a) +redundantPattern = do + ploc <- Ex.redundantPattern + pure (RedundantPattern ploc) + +uncoveredPatterns :: Ex.ErrorExtractor v a (TypeError v a) +uncoveredPatterns = do + (mloc, uncoveredCases) <- Ex.uncoveredPatterns + pure (UncoveredPatterns mloc uncoveredCases) + abilityCheckFailure :: Ex.ErrorExtractor v a (TypeError v a) abilityCheckFailure = do (ambient, requested, _ctx) <- Ex.abilityCheckFailure diff --git a/parser-typechecker/unison-parser-typechecker.cabal b/parser-typechecker/unison-parser-typechecker.cabal index 45a5ae71c..5e6b8305b 100644 --- a/parser-typechecker/unison-parser-typechecker.cabal +++ b/parser-typechecker/unison-parser-typechecker.cabal @@ -97,6 +97,20 @@ library Unison.FileParsers Unison.Hashing.V2.Convert Unison.Parsers + Unison.PatternMatchCoverage + Unison.PatternMatchCoverage.Class + Unison.PatternMatchCoverage.Constraint + Unison.PatternMatchCoverage.Desugar + Unison.PatternMatchCoverage.Fix + Unison.PatternMatchCoverage.GrdTree + Unison.PatternMatchCoverage.IntervalSet + Unison.PatternMatchCoverage.ListPat + Unison.PatternMatchCoverage.Literal + Unison.PatternMatchCoverage.NormalizedConstraints + Unison.PatternMatchCoverage.PmGrd + Unison.PatternMatchCoverage.PmLit + Unison.PatternMatchCoverage.Solve + Unison.PatternMatchCoverage.UFMap Unison.PrettyPrintEnv Unison.PrettyPrintEnv.FQN Unison.PrettyPrintEnv.MonadPretty diff --git a/unison-cli/src/Unison/LSP/FileAnalysis.hs b/unison-cli/src/Unison/LSP/FileAnalysis.hs index 74cf42685..ae4bcf753 100644 --- a/unison-cli/src/Unison/LSP/FileAnalysis.hs +++ b/unison-cli/src/Unison/LSP/FileAnalysis.hs @@ -234,6 +234,10 @@ analyseNotes fileUri ppe src notes = do (_v, locs) <- toList defns (r, rs) <- withNeighbours (locs >>= aToR) pure (r, ("duplicate definition",) <$> rs) + TypeError.RedundantPattern _ploc -> do + empty + TypeError.UncoveredPatterns _mloc _pats -> do + empty -- These type errors don't have custom type error conversions, but some -- still have valid diagnostics. TypeError.Other e@(Context.ErrorNote {cause}) -> case cause of @@ -338,18 +342,18 @@ analyseNotes fileUri ppe src notes = do typeHoleReplacementCodeActions diags v typ | not (isUserBlank v) = pure [] | otherwise = do - Env {codebase} <- ask - ppe <- PPED.suffixifiedPPE <$> globalPPED - let cleanedTyp = Context.generalizeAndUnTypeVar typ -- TODO: is this right? - refs <- liftIO . Codebase.runTransaction codebase $ Codebase.termsOfType codebase cleanedTyp - forMaybe (toList refs) $ \ref -> runMaybeT $ do - hqNameSuggestion <- MaybeT . pure $ PPE.terms ppe ref - typ <- MaybeT . liftIO . Codebase.runTransaction codebase $ Codebase.getTypeOfReferent codebase ref - let prettyType = TypePrinter.prettyStr Nothing ppe typ - let txtName = HQ'.toText hqNameSuggestion - let ranges = (diags ^.. folded . range) - let rca = rangedCodeAction ("Use " <> txtName <> " : " <> Text.pack prettyType) diags ranges - pure $ includeEdits fileUri txtName ranges rca + Env {codebase} <- ask + ppe <- PPED.suffixifiedPPE <$> globalPPED + let cleanedTyp = Context.generalizeAndUnTypeVar typ -- TODO: is this right? + refs <- liftIO . Codebase.runTransaction codebase $ Codebase.termsOfType codebase cleanedTyp + forMaybe (toList refs) $ \ref -> runMaybeT $ do + hqNameSuggestion <- MaybeT . pure $ PPE.terms ppe ref + typ <- MaybeT . liftIO . Codebase.runTransaction codebase $ Codebase.getTypeOfReferent codebase ref + let prettyType = TypePrinter.prettyStr Nothing ppe typ + let txtName = HQ'.toText hqNameSuggestion + let ranges = (diags ^.. folded . range) + let rca = rangedCodeAction ("Use " <> txtName <> " : " <> Text.pack prettyType) diags ranges + pure $ includeEdits fileUri txtName ranges rca isUserBlank :: Symbol -> Bool isUserBlank v = case Var.typeOf v of Var.User name -> Text.isPrefixOf "_" name diff --git a/unison-src/transcripts/pattern-match-coverage.md b/unison-src/transcripts/pattern-match-coverage.md new file mode 100644 index 000000000..1affffa78 --- /dev/null +++ b/unison-src/transcripts/pattern-match-coverage.md @@ -0,0 +1,190 @@ +```ucm:hide +.> builtins.merge +``` + +# Basics +non-exhaustive patterns are reported +```unison:error +unique type T = A | B | C + +test : T -> () +test = cases + A -> 0 +``` + +redundant matches are reported +```unison:error +unique type T = A | B | C + +test : T -> () +test = cases + A -> 0 + B -> 0 + C -> 0 + _ -> 0 +``` + +patterns that would imply supplying an uninhabited type are not expected +```unison +unique type V = + +test : Optional (Optional V) -> () +test = cases + None -> () + Some None -> () +``` + +they are reported as redundant +```unison:error +unique type V = + +test : Optional (Optional V) -> () +test = cases + None -> () + Some None -> () + Some _ -> () +``` + +boolean guards are considered +```unison:error +test : () -> () +test = cases + () | false -> () +``` + +uncovered patterns are only instantiated as deeply as necessary to +distinguish them from existing patterns +```unison:error +unique type T = A | B | C + +test : Optional (Optional T) -> () +test = cases + None -> () + Some None -> () +``` + +```unison:error +unique type T = A | B | C + +test : Optional (Optional T) -> () +test = cases + None -> () + Some None -> () + Some (Some A) -> () +``` + +# Literals +non-exhaustive nat +```unison:error +test : Nat -> () +test = cases + 0 -> () +``` + +```unison +test : Nat -> () +test = cases + 0 -> () + _ -> () +``` + +non-exhaustive boolean +```unison:error +test : Boolean -> () +test = cases + true -> () +``` + +```unison +test : Boolean -> () +test = cases + true -> () + false -> () +``` + +redundant boolean +```unison:error +test : Boolean -> () +test = cases + true -> () + false -> () + _ -> () +``` + +# Sequences +```unison +test : [()] -> () +test = cases + [] -> () + x +: xs -> () +``` + +```unison:error +test : [()] -> () +test = cases + [] -> () +``` + +```unison:error +test : [()] -> () +test = cases + x +: xs -> () +``` + +```unison:error +test : [()] -> () +test = cases + xs :+ x -> () +``` + +```unison +unique type V = + +test : [V] -> () +test = cases + [] -> () +``` + +```unison:error +test : [()] -> () +test = cases + x0 +: (x1 +: xs) -> () + [] -> () +``` + +```unison:error +test : [()] -> () +test = cases + [] -> () + x0 +: [] -> () +``` + +cons and snoc patterns are equated when a length restriction implies +that they refer to the same element +```unison +test : [Boolean] -> () +test = cases + [a, b] ++ xs -> () + [] -> () + xs :+ false -> () + true +: xs -> () +``` + +```unison:error +test : [Boolean] -> () +test = cases + [a, b] ++ xs -> () + [] -> () + xs :+ true -> () + true +: xs -> () + _ -> () +``` + +```unison:error +test : [Boolean] -> () +test = cases + [a, b, c, d, f] ++ xs -> () + [true, _, true, _] ++ _ -> () + _ ++ [true, false, true, false] -> () + _ -> () +``` diff --git a/unison-src/transcripts/pattern-match-coverage.output.md b/unison-src/transcripts/pattern-match-coverage.output.md new file mode 100644 index 000000000..0103006da --- /dev/null +++ b/unison-src/transcripts/pattern-match-coverage.output.md @@ -0,0 +1,436 @@ +# Basics +non-exhaustive patterns are reported +```unison +unique type T = A | B | C + +test : T -> () +test = cases + A -> 0 +``` + +```ucm + + Pattern match is non-exhaustive + In the match: + 4 | test = cases + 5 | A -> 0 + + + Patterns not matched: + + * B + * C + +``` +redundant matches are reported +```unison +unique type T = A | B | C + +test : T -> () +test = cases + A -> 0 + B -> 0 + C -> 0 + _ -> 0 +``` + +```ucm + + Pattern match is redundant + In the match case: + 8 | _ -> 0 + + +``` +patterns that would imply supplying an uninhabited type are not expected +```unison +unique type V = + +test : Optional (Optional V) -> () +test = cases + None -> () + Some None -> () +``` + +```ucm + + 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`: + + unique type V + test : Optional (Optional V) -> () + +``` +they are reported as redundant +```unison +unique type V = + +test : Optional (Optional V) -> () +test = cases + None -> () + Some None -> () + Some _ -> () +``` + +```ucm + + Pattern match is redundant + In the match case: + 7 | Some _ -> () + + +``` +boolean guards are considered +```unison +test : () -> () +test = cases + () | false -> () +``` + +```ucm + + Pattern match is non-exhaustive + In the match: + 2 | test = cases + 3 | () | false -> () + + + Patterns not matched: + * () + +``` +uncovered patterns are only instantiated as deeply as necessary to +distinguish them from existing patterns +```unison +unique type T = A | B | C + +test : Optional (Optional T) -> () +test = cases + None -> () + Some None -> () +``` + +```ucm + + Pattern match is non-exhaustive + In the match: + 4 | test = cases + 5 | None -> () + 6 | Some None -> () + + + Patterns not matched: + * Some (Some _) + +``` +```unison +unique type T = A | B | C + +test : Optional (Optional T) -> () +test = cases + None -> () + Some None -> () + Some (Some A) -> () +``` + +```ucm + + Pattern match is non-exhaustive + In the match: + 4 | test = cases + 5 | None -> () + 6 | Some None -> () + 7 | Some (Some A) -> () + + + Patterns not matched: + + * Some (Some B) + * Some (Some C) + +``` +# Literals +non-exhaustive nat +```unison +test : Nat -> () +test = cases + 0 -> () +``` + +```ucm + + Pattern match is non-exhaustive + In the match: + 2 | test = cases + 3 | 0 -> () + + + Patterns not matched: + * _ + +``` +```unison +test : Nat -> () +test = cases + 0 -> () + _ -> () +``` + +```ucm + + 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`: + + test : Nat -> () + +``` +non-exhaustive boolean +```unison +test : Boolean -> () +test = cases + true -> () +``` + +```ucm + + Pattern match is non-exhaustive + In the match: + 2 | test = cases + 3 | true -> () + + + Patterns not matched: + * false + +``` +```unison +test : Boolean -> () +test = cases + true -> () + false -> () +``` + +```ucm + + 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`: + + test : Boolean -> () + +``` +redundant boolean +```unison +test : Boolean -> () +test = cases + true -> () + false -> () + _ -> () +``` + +```ucm + + Pattern match is redundant + In the match case: + 5 | _ -> () + + +``` +# Sequences +```unison +test : [()] -> () +test = cases + [] -> () + x +: xs -> () +``` + +```ucm + + 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`: + + test : [()] -> () + +``` +```unison +test : [()] -> () +test = cases + [] -> () +``` + +```ucm + + Pattern match is non-exhaustive + In the match: + 2 | test = cases + 3 | [] -> () + + + Patterns not matched: + * (_ +: _) + +``` +```unison +test : [()] -> () +test = cases + x +: xs -> () +``` + +```ucm + + Pattern match is non-exhaustive + In the match: + 2 | test = cases + 3 | x +: xs -> () + + + Patterns not matched: + * [] + +``` +```unison +test : [()] -> () +test = cases + xs :+ x -> () +``` + +```ucm + + Pattern match is non-exhaustive + In the match: + 2 | test = cases + 3 | xs :+ x -> () + + + Patterns not matched: + * [] + +``` +```unison +unique type V = + +test : [V] -> () +test = cases + [] -> () +``` + +```ucm + + 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`: + + unique type V + test : [V] -> () + +``` +```unison +test : [()] -> () +test = cases + x0 +: (x1 +: xs) -> () + [] -> () +``` + +```ucm + + Pattern match is non-exhaustive + In the match: + 2 | test = cases + 3 | x0 +: (x1 +: xs) -> () + 4 | [] -> () + + + Patterns not matched: + * (_ +: []) + +``` +```unison +test : [()] -> () +test = cases + [] -> () + x0 +: [] -> () +``` + +```ucm + + Pattern match is non-exhaustive + In the match: + 2 | test = cases + 3 | [] -> () + 4 | x0 +: [] -> () + + + Patterns not matched: + * (_ +: (_ +: _)) + +``` +cons and snoc patterns are equated when a length restriction implies +that they refer to the same element +```unison +test : [Boolean] -> () +test = cases + [a, b] ++ xs -> () + [] -> () + xs :+ false -> () + true +: xs -> () +``` + +```ucm + + 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`: + + test : [Boolean] -> () + +``` +```unison +test : [Boolean] -> () +test = cases + [a, b] ++ xs -> () + [] -> () + xs :+ true -> () + true +: xs -> () + _ -> () +``` + +```ucm + + Pattern match is redundant + In the match case: + 6 | true +: xs -> () + + +``` +```unison +test : [Boolean] -> () +test = cases + [a, b, c, d, f] ++ xs -> () + [true, _, true, _] ++ _ -> () + _ ++ [true, false, true, false] -> () + _ -> () +``` + +```ucm + + Pattern match is redundant + In the match case: + 5 | _ ++ [true, false, true, false] -> () + + +``` From 768270a664e4f1d19765f97615e9737f7d75b404 Mon Sep 17 00:00:00 2001 From: Travis Staton Date: Thu, 12 Jan 2023 16:42:59 -0500 Subject: [PATCH 02/54] don't check coverage for ability handlers (yet) --- .../src/Unison/Typechecker/Context.hs | 24 +++++++++++-------- 1 file changed, 14 insertions(+), 10 deletions(-) diff --git a/parser-typechecker/src/Unison/Typechecker/Context.hs b/parser-typechecker/src/Unison/Typechecker/Context.hs index 0230fca92..e6b826c17 100644 --- a/parser-typechecker/src/Unison/Typechecker/Context.hs +++ b/parser-typechecker/src/Unison/Typechecker/Context.hs @@ -1251,7 +1251,7 @@ synthesizeWanted e let outputType = existential' l B.Blank outputTypev appendContext [existential outputTypev] cwant <- checkCases scrutineeType outputType cases - pmcStuff e scrutinee scrutineeType cases + ensurePatternCoverage e scrutinee scrutineeType cases want <- coalesceWanted cwant swant ctx <- getContext pure $ (apply ctx outputType, want) @@ -1291,7 +1291,7 @@ instance (Ord loc, Var v) => Pmc (TypeVar v loc) v loc (StateT (Set v) (M v loc) put (Set.insert v vs) pure v -pmcStuff :: +ensurePatternCoverage :: forall v loc. (Ord loc, Var v) => Term v loc -> @@ -1299,16 +1299,20 @@ pmcStuff :: Type v loc -> [Term.MatchCase loc (Term v loc)] -> MT v loc (Result v loc) () -pmcStuff wholeMatch _scrutinee scrutineeType cases = do +ensurePatternCoverage wholeMatch _scrutinee scrutineeType cases = do let matchLoc = ABT.annotation wholeMatch scrutineeType <- applyM scrutineeType - (redundant, _inaccessible, uncovered) <- flip evalStateT (ABT.freeVars wholeMatch) do - checkMatch matchLoc 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 - checkUncovered *> checkRedundant + case scrutineeType of + -- Don't check coverage on ability handlers yet + Type.Apps' (Type.Ref' r) _args | r == Type.effectRef -> pure () + _ -> do + (redundant, _inaccessible, uncovered) <- flip evalStateT (ABT.freeVars wholeMatch) do + checkMatch matchLoc 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 + checkUncovered *> checkRedundant checkCases :: (Var v) => From e2c0cb376e87510075f25164844211ecd0b26667 Mon Sep 17 00:00:00 2001 From: Travis Staton Date: Thu, 12 Jan 2023 16:43:38 -0500 Subject: [PATCH 03/54] print type failures in IOSource --- .../src/Unison/Runtime/IOSource.hs | 50 +++++++++++++++++-- 1 file changed, 46 insertions(+), 4 deletions(-) diff --git a/parser-typechecker/src/Unison/Runtime/IOSource.hs b/parser-typechecker/src/Unison/Runtime/IOSource.hs index f784e9576..0c437c2ef 100644 --- a/parser-typechecker/src/Unison/Runtime/IOSource.hs +++ b/parser-typechecker/src/Unison/Runtime/IOSource.hs @@ -7,18 +7,24 @@ import Control.Lens (view, _1) import Control.Monad.Morph (hoist) import Data.List (elemIndex, genericIndex) import qualified Data.Map as Map +import qualified Data.Text as Text import Debug.RecoverRTTI (anythingToString) import Text.RawString.QQ (r) import qualified Unison.Builtin as Builtin import Unison.Codebase.CodeLookup (CodeLookup (..)) import qualified Unison.Codebase.CodeLookup.Util as CL +import qualified Unison.Codebase.Path as Path import Unison.ConstructorReference (GConstructorReference (..)) import qualified Unison.DataDeclaration as DD import qualified Unison.DataDeclaration.ConstructorId as DD import Unison.FileParsers (parseAndSynthesizeFile) import qualified Unison.NamesWithHistory as Names +import qualified Unison.NamesWithHistory as NamesWithHistory import Unison.Parser.Ann (Ann (..)) import Unison.Prelude +import qualified Unison.PrettyPrintEnv as PPE +import qualified Unison.PrettyPrintEnv.Names as PPE +import qualified Unison.PrintError as PrintError import qualified Unison.Reference as R import qualified Unison.Result as Result import Unison.Symbol (Symbol) @@ -26,6 +32,8 @@ import qualified Unison.Syntax.Parser as Parser import qualified Unison.Term as Term import qualified Unison.Typechecker.TypeLookup as TL import qualified Unison.UnisonFile as UF +import qualified Unison.UnisonFile.Names as UF +import Unison.Util.Monoid (intercalateMap) import qualified Unison.Var as Var debug :: Bool @@ -42,10 +50,9 @@ typecheckedFile' = tl = const $ pure (External <$ Builtin.typeLookup) env = Parser.ParsingEnv mempty (Names.NamesWithHistory Builtin.names0 mempty) r = parseAndSynthesizeFile [] tl env "" source - in case runIdentity $ Result.runResultT r of - (Nothing, notes) -> error $ "parsing failed: " <> anythingToString (toList notes) - (Just Left {}, notes) -> error $ "typechecking failed" <> anythingToString (toList notes) - (Just (Right file), _) -> file + in case decodeResult (Text.unpack source) r of + Left str -> error str + Right file -> file typecheckedFileTerms :: Map.Map Symbol R.Reference typecheckedFileTerms = view _1 <$> UF.hashTerms typecheckedFile @@ -959,3 +966,38 @@ syntax.docFormatConsole d = Special sf -> Pretty.lit (Left sf) go d |] + +type Note = Result.Note Symbol Ann + +type TFile = UF.TypecheckedUnisonFile Symbol Ann + +type SynthResult = + Result.Result + (Seq Note) + (Either (UF.UnisonFile Symbol Ann) TFile) + +type EitherResult = Either String TFile + +showNotes :: Foldable f => String -> PrintError.Env -> f Note -> String +showNotes source env = + intercalateMap "\n\n" $ PrintError.renderNoteAsANSI 60 env source Path.absoluteEmpty + +decodeResult :: + String -> SynthResult -> EitherResult -- String (UF.TypecheckedUnisonFile Symbol Ann) +decodeResult source (Result.Result notes Nothing) = + Left $ showNotes source ppEnv notes +decodeResult source (Result.Result notes (Just (Left uf))) = + let errNames = UF.toNames uf + in Left $ + showNotes + source + ( PPE.fromNames + 10 + (NamesWithHistory.shadowing errNames Builtin.names) + ) + notes +decodeResult _source (Result.Result _notes (Just (Right uf))) = + Right uf + +ppEnv :: PPE.PrettyPrintEnv +ppEnv = PPE.fromNames 10 Builtin.names From c69dc75fd19c33a6536d8fd1ba235d6bb81e6b2a Mon Sep 17 00:00:00 2001 From: Travis Staton Date: Thu, 12 Jan 2023 16:44:11 -0500 Subject: [PATCH 04/54] fix builtins.mergeio bug --- parser-typechecker/src/Unison/Runtime/IOSource.hs | 1 + 1 file changed, 1 insertion(+) diff --git a/parser-typechecker/src/Unison/Runtime/IOSource.hs b/parser-typechecker/src/Unison/Runtime/IOSource.hs index 0c437c2ef..33b1392c7 100644 --- a/parser-typechecker/src/Unison/Runtime/IOSource.hs +++ b/parser-typechecker/src/Unison/Runtime/IOSource.hs @@ -715,6 +715,7 @@ Pretty.map f p = Lit _ t -> Lit () (f t) Wrap _ p -> Wrap () (go p) OrElse _ p1 p2 -> OrElse () (go p1) (go p2) + Table _ xs -> Table () (List.map (List.map go) xs) Indent _ i0 iN p -> Indent () (go i0) (go iN) (go p) Annotated.Append _ ps -> Annotated.Append () (List.map go ps) Pretty (go (Pretty.get p)) From 1cf470a7074623bf6355b7f62ca6ddf232323c27 Mon Sep 17 00:00:00 2001 From: Travis Staton Date: Fri, 13 Jan 2023 10:01:25 -0500 Subject: [PATCH 05/54] Fix bug in desugarPattern --- parser-typechecker/src/Unison/PatternMatchCoverage/Desugar.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/parser-typechecker/src/Unison/PatternMatchCoverage/Desugar.hs b/parser-typechecker/src/Unison/PatternMatchCoverage/Desugar.hs index af81e3368..3551d863b 100644 --- a/parser-typechecker/src/Unison/PatternMatchCoverage/Desugar.hs +++ b/parser-typechecker/src/Unison/PatternMatchCoverage/Desugar.hs @@ -69,7 +69,7 @@ desugarPattern typ v0 pat k vs = case pat of tpatvars = zipWith (\(v, p) t -> (v, p, t)) patvars contyps rest <- foldr (\(v, pat, t) b -> desugarPattern t v pat b) k tpatvars vs pure (Grd c rest) - As _ _ -> k (v0 : vs) + As _ rest -> desugarPattern typ v0 rest k (v0 : vs) EffectPure {} -> k vs EffectBind {} -> k vs SequenceLiteral {} -> handleSequence typ v0 pat k vs From bfe8364bb0f4b125e86f62993e1d12d8da3040a1 Mon Sep 17 00:00:00 2001 From: Travis Staton Date: Fri, 13 Jan 2023 10:07:03 -0500 Subject: [PATCH 06/54] make patterns complete in base.u --- .../src/Unison/Runtime/IOSource.hs | 1 - .../all-base-hashes.output.md | 24 +++++++++---------- unison-src/transcripts-using-base/base.u | 4 ++-- .../transcripts/move-namespace.output.md | 24 +++++++++---------- 4 files changed, 26 insertions(+), 27 deletions(-) diff --git a/parser-typechecker/src/Unison/Runtime/IOSource.hs b/parser-typechecker/src/Unison/Runtime/IOSource.hs index 33b1392c7..c7c589389 100644 --- a/parser-typechecker/src/Unison/Runtime/IOSource.hs +++ b/parser-typechecker/src/Unison/Runtime/IOSource.hs @@ -8,7 +8,6 @@ import Control.Monad.Morph (hoist) import Data.List (elemIndex, genericIndex) import qualified Data.Map as Map import qualified Data.Text as Text -import Debug.RecoverRTTI (anythingToString) import Text.RawString.QQ (r) import qualified Unison.Builtin as Builtin import Unison.Codebase.CodeLookup (CodeLookup (..)) diff --git a/unison-src/transcripts-using-base/all-base-hashes.output.md b/unison-src/transcripts-using-base/all-base-hashes.output.md index 61393a036..1af0e709f 100644 --- a/unison-src/transcripts-using-base/all-base-hashes.output.md +++ b/unison-src/transcripts-using-base/all-base-hashes.output.md @@ -13,19 +13,19 @@ This transcript is intended to make visible accidental changes to the hashing al autoCleaned.handler : '{IO} (Request {TempDirs} r ->{IO, Exception} r) - 4. -- #fajcv3ki8h80htov5pu2beu6f9d5dqsr0he47jssjvivgcpo2n1mqmbh7e0plv5cuqte3kjg18ken8gv1kmtpppkjjein4rr7a50ep8 + 4. -- #p1lh7ba73bdka6e18v9hmkrj811f2qsrogjumssr36drdjfgrfd6e6qotaqksb3o4lk44274fbcaqnj8e41rh0pjn56cbvsb3gv0880 bContains : [(a, b)] -> a -> Boolean - 5. -- #js3u40odrqs74lpcqjoemr1b08cbu7co41sf0ubp7gq3eaohl72db3khi0p1neqtmk2ede9f00n07no0kju13i7tliopsgsm69nh38o + 5. -- #ck9knej1qu6jt87i9qun1btc67kvthamubpl658se75po13oe2vto97jck965ibs6uspmopt3097lqd1pmqnegmba8e2bbfgtre9ovo bInsert : [(a, b)] -> a -> b -> [(a, b)] - 6. -- #avou19csadtmkejvdovufstrhtsbvnauqan05o9na0kqo7jon7ql05f7ooccbv777k68jj56ufufthp1cjd0jvium7j2ghrlpghnh58 + 6. -- #k1ge36n1ouvbaqjamm69pu7uuul0qc842tgqufm0ncaeb5h7im3r3vh9b7vikdu896p3f9ep2tf0dec3ifnrbr197k9lucl733rjpc0 bSearch : [(a, b)] -> a -> Optional b - 7. -- #ps5jpme6lr6fgv1a3cjmd4tpqr62pg3flmunkhcu9creojv2hsmei86nb6nndiam5p4q79nlerddrgto5um4ugm0p9evb8isoqu9ur0 + 7. -- #0nmd69uoat0mr9tl1917mdb16cpvd2q8oev5uj9s5d6virfcolc4t7js3l9do0c6c26tj7mvd82fpcumjr513bfudelnunvbok317fo bSort : [(a, b)] -> [(a, b)] - 8. -- #vb7eo70iavak378net6hohjkosud6ooabo1j0dev8l7254ls2j48f4e8gmk46d4016l41tpe7k8gqjqtb84g0gdc93vrh8bh4d62nf8 + 8. -- #re1saul4fhhdmg0b91ssrp3ok604nitpsler5dijra4eutcugsinmqvh9om3ah7qmcj1da57h3git1fn032lj8qs9kpqj3ujfs2ueig bSplit : [(a, b)] -> a -> ([(a, b)], [(a, b)]) 9. -- #1j3e8vsn97qrprjr69ls6llab601sdh577uuvtu8pafmngf59suakbjr7asheadidcj3red140fnmdagsv9ihhdar1mc05ig28jtfr0 @@ -2069,7 +2069,7 @@ This transcript is intended to make visible accidental changes to the hashing al 584. -- #jtn2i6bg3gargdp2rbk08jfd327htap62brih8phdfm2m4d6ib9cu0o2k5vrh7f4jik99eufu4hi0114akgd1oiivi8p1pa9m2fvjv0 builtin.Pretty.lit : txt -> Pretty txt - 585. -- #pn811nf59d63s8711bpktjqub65sb748pmajg7r8n7h7cnap5ecb4n1072ccult24q6gcfac66scrm77cjsa779mcckqrs8si4716sg + 585. -- #kfgfekabh7tiprb6ljjkf4qa5puqp6bbpe1oiqv9r39taljs8ahtb518mpcmec3plesvpssn3bpgvq3e7d71giot6lb2j7mbk23dtqo builtin.Pretty.map : (txt ->{g} txt2) -> Pretty txt ->{g} Pretty txt2 @@ -2202,7 +2202,7 @@ This transcript is intended to make visible accidental changes to the hashing al [Doc2.Term])] -> Doc2 - 624. -- #4rv8dvuvf5br3vhhuturaejt1l2u8j5eidjid01f5mo7o0fgjatttmph34ma0b9s1i2badcqj3ale005jb1hnisabnh93i4is1d8kng + 624. -- #inrar1e9lnt58n0ru88v05a9d9d0la94m7ok5l6i7pr3pg4lapc9vegr542ffog1kl7pfqhmltr53of3qkci8nnrt8gig93qsnggisg builtin.syntax.docFormatConsole : Doc2 -> Pretty (Either SpecialForm ConsoleText) @@ -2474,7 +2474,7 @@ This transcript is intended to make visible accidental changes to the hashing al 710. -- #4e6qn65v05l32n380lpf536u4llnp6f6tvvt13hvo0bhqeh3f3i8bquekc120c8h59gld1mf02ok0sje7037ipg1fsu97fqrm01oi00 closeSocket : Socket ->{IO, Exception} () - 711. -- #7o1e77u808vpg8i6k1mvutg8h6tdr14hegfad23e9sjou1ft10kvfr95goo0kv2ldqlsaa4pmvdl8d7jd6h252i3jija05b4vpqbg5g + 711. -- #2cl9ivrimnadurkum2blduls21kcihu89oasj2efmi03s1vfm433pi6c4k1d2a3obpmf2orm3c9lfgffnlhuc6ktaa98a1ccdhfueqo Code.transitiveDeps : Link.Term ->{IO} [(Link.Term, Code)] @@ -2502,7 +2502,7 @@ This transcript is intended to make visible accidental changes to the hashing al 715. -- #ilkeid6l866bmq90d2v1ilqp9dsjo6ucmf8udgrokq3nr3mo9skl2vao2mo7ish136as52rsf19u9v3jkmd85bl08gnmamo4e5v2fqo contains : Text -> Text -> Boolean - 716. -- #tgvna0i8ea98jvnd2oka85cdtas1prcbq3snvc4qfns6082mlckps2cspk8jln11mklg19bna025tog5m9sb671o27ujsa90lfrbnkg + 716. -- #pen6v1vcqdsg5ar8ajio0baiujthquamelbqd00p66amfjftk2o3stod4n81snc3hb9sc4fmnitf6ada0n5sfqfroi8sv1nbn7rnq48 crawl : [(Link.Term, Code)] -> [Link.Term] ->{IO} [(Link.Term, Code)] @@ -2708,10 +2708,10 @@ This transcript is intended to make visible accidental changes to the hashing al runTest : '{IO, TempDirs, Exception, Stream Result} a ->{IO} [Result] - 779. -- #va4fcp72qog4dvo8dn4gipr2i1big1lqgpcqfuv9kc98ut8le1bj23s68df7svam7b5sg01s4uf95o458f4rs90mtp71nj84t90ra1o + 779. -- #b59q94bf9mrvv4gl8gqjd04dc3ahq373ka5esh4grtjupkm8ov7o7h0n56q2dg3ocdsreqvm973rlhs4etua1tbrsuabc398e5pvs0o saveSelfContained : a -> Text ->{IO, Exception} () - 780. -- #5hbn4gflbo8l4jq0s9l1r0fpee6ie44fbbl6j6km67l25inaaq5avg18g7j6mig2m6eaod04smif7el34tcclvvf8oll39rfonupt2o + 780. -- #f55p4o2hlhka9olk8a9dnan57o51605g4q26jtpsbkt0g652s322779sej71182ntb6lkh01gom3g26cmngqq7vtl7m7oovdi0koc70 saveTestCase : Text -> (a -> Text) -> a @@ -2801,7 +2801,7 @@ This transcript is intended to make visible accidental changes to the hashing al uncurry : ∀ o g1 i g i1. (i1 ->{g} i ->{g1} o) -> (i1, i) ->{g1, g} o - 807. -- #u2j1bektndcqdo1m13fvu6apt9td96s4tqonelg23tauklak2pqnbisf41v632fmlrcc6f9orqo3iu9757q36ue5ol1khe0hh8pktro + 807. -- #rhak55ntto40n4utgv5o93jvlmv82lceb625slrt8tsmg74vin5bclf10vkl1sgpau3thqsa6guiihog74qoknlsqbuce5th60bu2eg Value.transitiveDeps : Value ->{IO} [(Link.Term, Code)] 808. -- #o5bg5el7ckak28ib98j5b6rt26bqbprpddd1brrg3s18qahhbbe3uohufjjnt5eenvtjg0hrvnvpra95jmdppqrovvmcfm1ih2k7guo diff --git a/unison-src/transcripts-using-base/base.u b/unison-src/transcripts-using-base/base.u index daaa0e5aa..84afda95c 100644 --- a/unison-src/transcripts-using-base/base.u +++ b/unison-src/transcripts-using-base/base.u @@ -274,7 +274,7 @@ bSearch m k = Some (k', v) | k == k' -> Some v | k > k' -> find (i+1) u - | k < k' -> find l i + | otherwise -> find l i None -> None find 0 (size m) @@ -299,7 +299,7 @@ bSplit m k = Some (k', _) | k == k' -> (List.take i m, List.drop (i+1) m) | k > k' -> find (i+1) u - | k < k' -> find l i + | otherwise -> find l i None -> (m, []) find 0 (size m) diff --git a/unison-src/transcripts/move-namespace.output.md b/unison-src/transcripts/move-namespace.output.md index 030e44616..9689c3d79 100644 --- a/unison-src/transcripts/move-namespace.output.md +++ b/unison-src/transcripts/move-namespace.output.md @@ -278,7 +278,7 @@ I should be able to move the root into a sub-namespace - □ 1. #hu6p22qbe4 (start of history) + □ 1. #j17hvtt1rm (start of history) ``` ```ucm @@ -294,7 +294,7 @@ I should be able to move the root into a sub-namespace Note: The most recent namespace hash is immediately below this message. - ⊙ 1. #8rae339vn9 + ⊙ 1. #epknijg4pk - Deletes: @@ -305,7 +305,7 @@ I should be able to move the root into a sub-namespace Original name New name existing.a.termInA existing.b.termInA - ⊙ 2. #r697qei02b + ⊙ 2. #pmecta5so9 + Adds / updates: @@ -317,26 +317,26 @@ I should be able to move the root into a sub-namespace happy.b.termInA existing.a.termInA history.b.termInA existing.a.termInA - ⊙ 3. #ca0k6ug92t + ⊙ 3. #lc7lsqgcmo + Adds / updates: existing.a.termInA existing.b.termInB - ⊙ 4. #7nnrjj85km + ⊙ 4. #j36gjaovv9 > Moves: Original name New name history.a.termInA history.b.termInA - ⊙ 5. #01cflse46b + ⊙ 5. #domisg9f2n - Deletes: history.b.termInB - ⊙ 6. #cna2qqmgcq + ⊙ 6. #69vk74hidq + Adds / updates: @@ -347,13 +347,13 @@ I should be able to move the root into a sub-namespace Original name New name(s) happy.b.termInA history.a.termInA - ⊙ 7. #qoce7dt2h1 + ⊙ 7. #hslilthrkd + Adds / updates: history.a.termInA history.b.termInB - ⊙ 8. #g8m2g6bd1g + ⊙ 8. #ap9o8u4m1a > Moves: @@ -363,7 +363,7 @@ I should be able to move the root into a sub-namespace happy.a.T.T2 happy.b.T.T2 happy.a.termInA happy.b.termInA - ⊙ 9. #ngl33npfah + ⊙ 9. #tpka2u10nq + Adds / updates: @@ -373,7 +373,7 @@ I should be able to move the root into a sub-namespace happy.a.T.T - ⊙ 10. #1rnd8dpisq + ⊙ 10. #ebk6c1po2f + Adds / updates: @@ -385,7 +385,7 @@ I should be able to move the root into a sub-namespace ⠇ - ⊙ 11. #7s9j9tscke + ⊙ 11. #c5i2vql0hi ``` From 4482098370e728fa60d6126f5386f113b702243d Mon Sep 17 00:00:00 2001 From: Travis Staton Date: Fri, 13 Jan 2023 10:15:24 -0500 Subject: [PATCH 07/54] Remove test catching missing case in match this is handled at compile time now --- unison-src/transcripts-using-base/fix2049.md | 2 -- unison-src/transcripts-using-base/fix2049.output.md | 5 +---- 2 files changed, 1 insertion(+), 6 deletions(-) diff --git a/unison-src/transcripts-using-base/fix2049.md b/unison-src/transcripts-using-base/fix2049.md index 4fa2edf70..5ccb89a46 100644 --- a/unison-src/transcripts-using-base/fix2049.md +++ b/unison-src/transcripts-using-base/fix2049.md @@ -13,8 +13,6 @@ catcher act = tests _ = [ catcher do - match None with Some x -> x - , catcher do _ = 1/0 () , catcher '(bug "testing") diff --git a/unison-src/transcripts-using-base/fix2049.output.md b/unison-src/transcripts-using-base/fix2049.output.md index bbc29e767..9ed56a65d 100644 --- a/unison-src/transcripts-using-base/fix2049.output.md +++ b/unison-src/transcripts-using-base/fix2049.output.md @@ -9,8 +9,6 @@ catcher act = tests _ = [ catcher do - match None with Some x -> x - , catcher do _ = 1/0 () , catcher '(bug "testing") @@ -45,12 +43,11 @@ tests _ = New test results: - ◉ tests caught ◉ tests caught ◉ tests caught ◉ tests got the right answer - ✅ 4 test(s) passing + ✅ 3 test(s) passing Tip: Use view tests to view the source of a test. From aab7d46677d3e0e95cea57c3f99cb8a4d6c893f5 Mon Sep 17 00:00:00 2001 From: Travis Staton Date: Fri, 13 Jan 2023 10:16:07 -0500 Subject: [PATCH 08/54] complete patterns in random-deserial --- unison-src/transcripts-using-base/random-deserial.md | 1 + unison-src/transcripts-using-base/random-deserial.output.md | 1 + 2 files changed, 2 insertions(+) diff --git a/unison-src/transcripts-using-base/random-deserial.md b/unison-src/transcripts-using-base/random-deserial.md index 526705b3b..9b0672764 100644 --- a/unison-src/transcripts-using-base/random-deserial.md +++ b/unison-src/transcripts-using-base/random-deserial.md @@ -23,6 +23,7 @@ shuffle = | otherwise -> match gen seed (size l) with (k, seed) -> match (take k l, drop k l) with (pre, x +: post) -> pick (acc :+ x) seed (pre ++ post) + (pre, []) -> pick acc seed pre pick [] diff --git a/unison-src/transcripts-using-base/random-deserial.output.md b/unison-src/transcripts-using-base/random-deserial.output.md index d7f278426..24f21d771 100644 --- a/unison-src/transcripts-using-base/random-deserial.output.md +++ b/unison-src/transcripts-using-base/random-deserial.output.md @@ -19,6 +19,7 @@ shuffle = | otherwise -> match gen seed (size l) with (k, seed) -> match (take k l, drop k l) with (pre, x +: post) -> pick (acc :+ x) seed (pre ++ post) + (pre, []) -> pick acc seed pre pick [] From c2a896eeac1c4898d9626be5ec9a390c197b49c9 Mon Sep 17 00:00:00 2001 From: Travis Staton Date: Fri, 13 Jan 2023 10:16:36 -0500 Subject: [PATCH 09/54] complete patterns in tls --- unison-src/transcripts-using-base/tls.md | 4 +++- unison-src/transcripts-using-base/tls.output.md | 4 +++- 2 files changed, 6 insertions(+), 2 deletions(-) diff --git a/unison-src/transcripts-using-base/tls.md b/unison-src/transcripts-using-base/tls.md index fff979ede..7da872603 100644 --- a/unison-src/transcripts-using-base/tls.md +++ b/unison-src/transcripts-using-base/tls.md @@ -61,7 +61,9 @@ serverThread portVar toSend = 'let cert = decodeCert (toUtf8 self_signed_cert_pem2) -- assume there is exactly one key decoded from our Bytes - key = match (decodePrivateKey (toUtf8 self_signed_key_pem)) with k +: _ -> k + key = match (decodePrivateKey (toUtf8 self_signed_key_pem)) with + k +: _ -> k + [] -> bug "oh no" -- create a default configuration using our credentials (certificate chain and key) tlsconfig = Tls.ServerConfig.default [cert] key diff --git a/unison-src/transcripts-using-base/tls.output.md b/unison-src/transcripts-using-base/tls.output.md index 1e4cb5120..52dae392d 100644 --- a/unison-src/transcripts-using-base/tls.output.md +++ b/unison-src/transcripts-using-base/tls.output.md @@ -78,7 +78,9 @@ serverThread portVar toSend = 'let cert = decodeCert (toUtf8 self_signed_cert_pem2) -- assume there is exactly one key decoded from our Bytes - key = match (decodePrivateKey (toUtf8 self_signed_key_pem)) with k +: _ -> k + key = match (decodePrivateKey (toUtf8 self_signed_key_pem)) with + k +: _ -> k + [] -> bug "oh no" -- create a default configuration using our credentials (certificate chain and key) tlsconfig = Tls.ServerConfig.default [cert] key From fb039aaa53f277a92336eddb683f4f63b49cafba Mon Sep 17 00:00:00 2001 From: Travis Staton Date: Fri, 13 Jan 2023 10:16:55 -0500 Subject: [PATCH 10/54] complete patterns in utf8 --- unison-src/transcripts-using-base/utf8.md | 1 + unison-src/transcripts-using-base/utf8.output.md | 1 + 2 files changed, 2 insertions(+) diff --git a/unison-src/transcripts-using-base/utf8.md b/unison-src/transcripts-using-base/utf8.md index 127f46660..07cd53a4b 100644 --- a/unison-src/transcripts-using-base/utf8.md +++ b/unison-src/transcripts-using-base/utf8.md @@ -55,5 +55,6 @@ greek_bytes = Bytes.fromList [206, 145, 206, 146, 206, 147, 206, 148, 206] -- Its an error if we drop the first byte > match fromUtf8.impl (drop 1 greek_bytes) with Left (Failure _ t _) -> t + _ -> bug "expected a left" ``` diff --git a/unison-src/transcripts-using-base/utf8.output.md b/unison-src/transcripts-using-base/utf8.output.md index 372185222..ab99fd866 100644 --- a/unison-src/transcripts-using-base/utf8.output.md +++ b/unison-src/transcripts-using-base/utf8.output.md @@ -111,6 +111,7 @@ greek_bytes = Bytes.fromList [206, 145, 206, 146, 206, 147, 206, 148, 206] -- Its an error if we drop the first byte > match fromUtf8.impl (drop 1 greek_bytes) with Left (Failure _ t _) -> t + _ -> bug "expected a left" ``` From 96197d9d188f15521f238f5380836ed84c9bc390 Mon Sep 17 00:00:00 2001 From: Travis Staton Date: Fri, 13 Jan 2023 10:18:20 -0500 Subject: [PATCH 11/54] complete patterns in destructuring-binds --- unison-src/transcripts/destructuring-binds.md | 2 ++ unison-src/transcripts/destructuring-binds.output.md | 7 ++++++- 2 files changed, 8 insertions(+), 1 deletion(-) diff --git a/unison-src/transcripts/destructuring-binds.md b/unison-src/transcripts/destructuring-binds.md index 953cf6349..f9a1eef97 100644 --- a/unison-src/transcripts/destructuring-binds.md +++ b/unison-src/transcripts/destructuring-binds.md @@ -49,10 +49,12 @@ Even though the parser accepts any pattern on the LHS of a bind, it looks pretty ex5 : 'Text ex5 _ = match 99 + 1 with 12 -> "Hi" + _ -> "Bye" ex5a : 'Text ex5a _ = match (99 + 1, "hi") with (x, "hi") -> "Not printed as a destructuring bind." + _ -> "impossible" ``` ```ucm diff --git a/unison-src/transcripts/destructuring-binds.output.md b/unison-src/transcripts/destructuring-binds.output.md index f4c759964..1ca633ea7 100644 --- a/unison-src/transcripts/destructuring-binds.output.md +++ b/unison-src/transcripts/destructuring-binds.output.md @@ -106,10 +106,12 @@ Even though the parser accepts any pattern on the LHS of a bind, it looks pretty ex5 : 'Text ex5 _ = match 99 + 1 with 12 -> "Hi" + _ -> "Bye" ex5a : 'Text ex5a _ = match (99 + 1, "hi") with (x, "hi") -> "Not printed as a destructuring bind." + _ -> "impossible" ``` ```ucm @@ -137,13 +139,16 @@ ex5a _ = match (99 + 1, "hi") with ex5 : 'Text ex5 _ = use Nat + - match 99 + 1 with 12 -> "Hi" + match 99 + 1 with + 12 -> "Hi" + _ -> "Bye" ex5a : 'Text ex5a _ = use Nat + match (99 + 1, "hi") with (x, "hi") -> "Not printed as a destructuring bind." + _ -> "impossible" ``` Notice how it prints both an ordinary match. From 05edb55049924e69a2f5b4300953aee2b7235578 Mon Sep 17 00:00:00 2001 From: Travis Staton Date: Tue, 17 Jan 2023 09:55:24 -0500 Subject: [PATCH 12/54] complete patterns in lambdacase --- unison-src/transcripts/lambdacase.md | 4 ++-- unison-src/transcripts/lambdacase.output.md | 6 +++--- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/unison-src/transcripts/lambdacase.md b/unison-src/transcripts/lambdacase.md index dcbc2559d..1b794b5ba 100644 --- a/unison-src/transcripts/lambdacase.md +++ b/unison-src/transcripts/lambdacase.md @@ -77,11 +77,11 @@ structural type B = T | F blah = cases T, x -> "hi" - x, F -> "bye" + x, y -> "bye" blorf = cases x, T -> x - T, x -> x + x, y -> y > blah T F > blah F F diff --git a/unison-src/transcripts/lambdacase.output.md b/unison-src/transcripts/lambdacase.output.md index 573138be6..31cd7b599 100644 --- a/unison-src/transcripts/lambdacase.output.md +++ b/unison-src/transcripts/lambdacase.output.md @@ -121,11 +121,11 @@ structural type B = T | F blah = cases T, x -> "hi" - x, F -> "bye" + x, y -> "bye" blorf = cases x, T -> x - T, x -> x + x, y -> y > blah T F > blah F F @@ -141,7 +141,7 @@ blorf = cases ⍟ These new definitions are ok to `add`: structural type B - blah : B -> B -> Text + blah : B -> hod1jusqau2 -> Text blorf : B -> B -> B Now evaluating any watch expressions (lines starting with From b7da02658d15eb375a9203bcd6da598155623379 Mon Sep 17 00:00:00 2001 From: Travis Staton Date: Tue, 17 Jan 2023 09:55:38 -0500 Subject: [PATCH 13/54] complete patterns in pattern-pretty-print-2345 --- .../transcripts/pattern-pretty-print-2345.md | 11 ++++ .../pattern-pretty-print-2345.output.md | 61 ++++++++++++++----- 2 files changed, 58 insertions(+), 14 deletions(-) diff --git a/unison-src/transcripts/pattern-pretty-print-2345.md b/unison-src/transcripts/pattern-pretty-print-2345.md index 83cb13d7a..8f77046d3 100644 --- a/unison-src/transcripts/pattern-pretty-print-2345.md +++ b/unison-src/transcripts/pattern-pretty-print-2345.md @@ -11,45 +11,56 @@ structural ability Ab where dopey = cases ?0 -> () + _ -> () grumpy = cases d -> () happy = cases true -> () + false -> () sneezy = cases +1 -> () + _ -> () bashful = cases Some a -> () + _ -> () mouthy = cases [] -> () + _ -> () pokey = cases h +: t -> () + _ -> () sleepy = cases i :+ l -> () + _ -> () demure = cases [0] -> () + _ -> () angry = cases a ++ [] -> () tremulous = cases (0,1) -> () + _ -> () throaty = cases { Ab.a a -> k } -> () agitated = cases a | a == 2 -> () + _ -> () doc = cases y@4 -> () + _ -> () ``` ```ucm diff --git a/unison-src/transcripts/pattern-pretty-print-2345.output.md b/unison-src/transcripts/pattern-pretty-print-2345.output.md index a764580fa..610c75699 100644 --- a/unison-src/transcripts/pattern-pretty-print-2345.output.md +++ b/unison-src/transcripts/pattern-pretty-print-2345.output.md @@ -7,45 +7,56 @@ structural ability Ab where dopey = cases ?0 -> () + _ -> () grumpy = cases d -> () happy = cases true -> () + false -> () sneezy = cases +1 -> () + _ -> () bashful = cases Some a -> () + _ -> () mouthy = cases [] -> () + _ -> () pokey = cases h +: t -> () + _ -> () sleepy = cases i :+ l -> () + _ -> () demure = cases [0] -> () + _ -> () angry = cases a ++ [] -> () tremulous = cases (0,1) -> () + _ -> () throaty = cases { Ab.a a -> k } -> () agitated = cases a | a == 2 -> () + _ -> () doc = cases y@4 -> () + _ -> () ``` ```ucm @@ -63,7 +74,7 @@ doc = cases demure : [Nat] -> () doc : Nat -> () dopey : Char -> () - grumpy : p4kl4dn7b41 -> () + grumpy : ff284oqf651 -> () happy : Boolean -> () mouthy : [t] -> () pokey : [t] -> () @@ -85,7 +96,7 @@ doc = cases demure : [Nat] -> () doc : Nat -> () dopey : Char -> () - grumpy : p4kl4dn7b41 -> () + grumpy : ff284oqf651 -> () happy : Boolean -> () mouthy : [t] -> () pokey : [t] -> () @@ -97,47 +108,63 @@ doc = cases .> view dopey dopey : Char -> () - dopey = cases ?0 -> () + dopey = cases + ?0 -> () + _ -> () .> view grumpy - grumpy : p4kl4dn7b41 -> () + grumpy : ff284oqf651 -> () grumpy = cases d -> () .> view happy happy : Boolean -> () - happy = cases true -> () + happy = cases + true -> () + false -> () .> view sneezy sneezy : Int -> () - sneezy = cases +1 -> () + sneezy = cases + +1 -> () + _ -> () .> view bashful bashful : Optional a -> () - bashful = cases Some a -> () + bashful = cases + Some a -> () + _ -> () .> view mouthy mouthy : [t] -> () - mouthy = cases [] -> () + mouthy = cases + [] -> () + _ -> () .> view pokey pokey : [t] -> () - pokey = cases h +: t -> () + pokey = cases + h +: t -> () + _ -> () .> view sleepy sleepy : [t] -> () - sleepy = cases i :+ l -> () + sleepy = cases + i :+ l -> () + _ -> () .> view demure demure : [Nat] -> () - demure = cases [0] -> () + demure = cases + [0] -> () + _ -> () .> view angry @@ -147,7 +174,9 @@ doc = cases .> view tremulous tremulous : (Nat, Nat) -> () - tremulous = cases (0, 1) -> () + tremulous = cases + (0, 1) -> () + _ -> () .> view throaty @@ -157,11 +186,15 @@ doc = cases .> view agitated agitated : Nat -> () - agitated = cases a | a == 2 -> () + agitated = cases + a | a == 2 -> () + _ -> () .> view doc doc : Nat -> () - doc = cases y@4 -> () + doc = cases + y@4 -> () + _ -> () ``` From e63e37c2723b48a80a01736472dc95667d19509e Mon Sep 17 00:00:00 2001 From: Travis Staton Date: Tue, 17 Jan 2023 10:26:38 -0500 Subject: [PATCH 14/54] complete patterns in caseguard.u --- unison-src/tests/caseguard.u | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/unison-src/tests/caseguard.u b/unison-src/tests/caseguard.u index 16e949af5..94eb6ce1a 100644 --- a/unison-src/tests/caseguard.u +++ b/unison-src/tests/caseguard.u @@ -10,6 +10,6 @@ use Universal == f = cases x | x == "woot" -> false - y | y == "foo" -> true + y | otherwise -> true -- > f "woot" From 21a2fdff08a0e2b5fbd1a64165559d9c1d900843 Mon Sep 17 00:00:00 2001 From: Travis Staton Date: Tue, 17 Jan 2023 10:26:47 -0500 Subject: [PATCH 15/54] complete patterns in imports.u --- unison-src/tests/imports.u | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/unison-src/tests/imports.u b/unison-src/tests/imports.u index 0748ae284..2647c9f57 100644 --- a/unison-src/tests/imports.u +++ b/unison-src/tests/imports.u @@ -19,4 +19,4 @@ use Nat drop > match Some (100 + 200 / 3 * 2) with Optional.None -> 19 - Some 200 -> 20 + Some _ -> 20 From 8d2e57f29a718e03e00034cd364d14f4b75c8e2f Mon Sep 17 00:00:00 2001 From: Travis Staton Date: Tue, 17 Jan 2023 10:26:59 -0500 Subject: [PATCH 16/54] complete patterns in inner-lambda.u --- unison-src/tests/inner-lambda1.u | 1 + 1 file changed, 1 insertion(+) diff --git a/unison-src/tests/inner-lambda1.u b/unison-src/tests/inner-lambda1.u index 708a59e78..43c196c8d 100644 --- a/unison-src/tests/inner-lambda1.u +++ b/unison-src/tests/inner-lambda1.u @@ -12,4 +12,5 @@ search hit bot top = +0 -> Some mid -1 -> go bot (drop mid 1) +1 -> go (mid + 1) top + _ -> bug "unexpected" go bot top From 271a7211aff2dff11864bdc6984ce564938e59dd Mon Sep 17 00:00:00 2001 From: Travis Staton Date: Tue, 17 Jan 2023 10:27:42 -0500 Subject: [PATCH 17/54] complete patterns in inner-lambda2 --- unison-src/tests/inner-lambda2.u | 1 + 1 file changed, 1 insertion(+) diff --git a/unison-src/tests/inner-lambda2.u b/unison-src/tests/inner-lambda2.u index 6900e8fd3..f356cbcfe 100644 --- a/unison-src/tests/inner-lambda2.u +++ b/unison-src/tests/inner-lambda2.u @@ -13,4 +13,5 @@ search hit bot top = +0 -> Some mid -1 -> go bot (drop mid 1) +1 -> go (mid + 1) top + _ -> bug "unexpected" go bot top From c0da1727c03ce65d82953efebfb6eed459a3de2b Mon Sep 17 00:00:00 2001 From: Travis Staton Date: Tue, 17 Jan 2023 11:05:53 -0500 Subject: [PATCH 18/54] complete patterns in pattern-matching.u --- unison-src/tests/methodical/pattern-matching.u | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/unison-src/tests/methodical/pattern-matching.u b/unison-src/tests/methodical/pattern-matching.u index e1883d120..9740b29b2 100644 --- a/unison-src/tests/methodical/pattern-matching.u +++ b/unison-src/tests/methodical/pattern-matching.u @@ -17,7 +17,7 @@ pat6 x y = cases (p1, _) -> (x + y : Nat, p1) pat7 x y = cases (p1, _) | p1 == 9 -> (x + y : Nat, p1) - (p1, _) | true -> (0, p1) + (p1, _) | otherwise -> (0, p1) bpat = cases false -> 0 From 6b0021f1cd130e25f3400dbc248b333ed01bce1e Mon Sep 17 00:00:00 2001 From: Travis Staton Date: Tue, 17 Jan 2023 11:06:14 -0500 Subject: [PATCH 19/54] complete patterns in parenthesized-blocks --- unison-src/tests/parenthesized-blocks.u | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/unison-src/tests/parenthesized-blocks.u b/unison-src/tests/parenthesized-blocks.u index 5824dbbec..db7bff5db 100644 --- a/unison-src/tests/parenthesized-blocks.u +++ b/unison-src/tests/parenthesized-blocks.u @@ -1,5 +1,5 @@ x = (if true then 1 else 0) + 1 -y = (match 1 with 1 -> 1) + 1 +y = (match 1 with _ -> 1) + 1 > (x, y) From 344949c03658e6f5310afc74d6cf64c6b44e2a61 Mon Sep 17 00:00:00 2001 From: Travis Staton Date: Tue, 17 Jan 2023 11:08:52 -0500 Subject: [PATCH 20/54] fix pattern coverage in pattern-match-seq --- unison-src/tests/pattern-match-seq.u | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/unison-src/tests/pattern-match-seq.u b/unison-src/tests/pattern-match-seq.u index 58c0a0484..c1485544a 100644 --- a/unison-src/tests/pattern-match-seq.u +++ b/unison-src/tests/pattern-match-seq.u @@ -11,12 +11,12 @@ lenLit = cases [_] -> 1 [_, _] -> 2 [_, _, _] -> 3 + _ -> bug "unexpected" lenCons : [a] -> Nat lenCons = cases [] -> 0 _ +: t -> 1 + lenCons t - _ +: (_ +: t) -> 2 + lenCons t lenSnoc : [a] -> Nat lenSnoc = cases From e8c6ad06113f5f65444ab55477b8b466b0ce5efa Mon Sep 17 00:00:00 2001 From: Travis Staton Date: Wed, 18 Jan 2023 09:49:25 -0500 Subject: [PATCH 21/54] fix pattern coverage in pattern-matching.u --- unison-src/tests/pattern-matching.u | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/unison-src/tests/pattern-matching.u b/unison-src/tests/pattern-matching.u index b1e2b3c7e..8be597d2f 100644 --- a/unison-src/tests/pattern-matching.u +++ b/unison-src/tests/pattern-matching.u @@ -16,8 +16,8 @@ y = match Foo1 1 with Foo1 _ -> 10 z = match Foo2 1 "hi" with - Foo2 x _ -> x Foo2 1 _ -> 1 + Foo2 x _ -> x w = match Foo3.Foo3 1 2 "bye" with Foo3.Foo3 1 2 x -> x Text.++ "bye" @@ -26,7 +26,6 @@ w = match Foo3.Foo3 1 2 "bye" with w2 = cases Foo3.Foo3 1 4 x -> x Text.++ "bye" Foo3.Foo3 x y z -> z Text.++ z - _ -> "hi" len : List a -> Nat len = cases From 9724f26c211cab915b3f9fdade823059093c4c95 Mon Sep 17 00:00:00 2001 From: Travis Staton Date: Wed, 18 Jan 2023 09:50:15 -0500 Subject: [PATCH 22/54] fix pattern coverage in pattern-matching2.u --- unison-src/tests/pattern-matching2.u | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/unison-src/tests/pattern-matching2.u b/unison-src/tests/pattern-matching2.u index 4f6dd8c40..e17364946 100644 --- a/unison-src/tests/pattern-matching2.u +++ b/unison-src/tests/pattern-matching2.u @@ -15,7 +15,8 @@ y = match Foo1 1 with Foo1 _ -> 10 z = match Foo2 1 "hi" with - Foo2 x "bye" -> x Foo2 1 "hi" -> 1 + Foo2 x "bye" -> x + _ -> bug "unexpected" > z From f1c74c22f3a94b9abd1114a3e52e2ac9c8bbd991 Mon Sep 17 00:00:00 2001 From: Travis Staton Date: Wed, 18 Jan 2023 09:51:25 -0500 Subject: [PATCH 23/54] fix pattern coverage in r2 --- unison-src/tests/r2.u | 1 + 1 file changed, 1 insertion(+) diff --git a/unison-src/tests/r2.u b/unison-src/tests/r2.u index 8218decb7..b7eaf7d71 100644 --- a/unison-src/tests/r2.u +++ b/unison-src/tests/r2.u @@ -3,4 +3,5 @@ r2 : Nat r2 = match Optional.Some true with Optional.Some true -> 1 Optional.Some false -> 0 + Optional.None -> bug "unexpected" From f38e5d3a1c5c1ae6e5d172b6b6ed2bcca2b34760 Mon Sep 17 00:00:00 2001 From: Travis Staton Date: Wed, 18 Jan 2023 09:51:36 -0500 Subject: [PATCH 24/54] fix pattern coverage in r3 --- unison-src/tests/r3.u | 1 + 1 file changed, 1 insertion(+) diff --git a/unison-src/tests/r3.u b/unison-src/tests/r3.u index 74b76105f..93e13894c 100644 --- a/unison-src/tests/r3.u +++ b/unison-src/tests/r3.u @@ -2,5 +2,6 @@ r3 : Nat r3 = match Optional.Some true with Optional.Some true -> 1 Optional.Some false -> 0 + Optional.None -> bug "unexpected" From 45238c72e8de5a782fb2219d936c37efc8784ff6 Mon Sep 17 00:00:00 2001 From: Travis Staton Date: Wed, 18 Jan 2023 09:52:22 -0500 Subject: [PATCH 25/54] fix pattern coverage in r4x --- unison-src/tests/r4x.u | 1 + 1 file changed, 1 insertion(+) diff --git a/unison-src/tests/r4x.u b/unison-src/tests/r4x.u index 1e7123f6e..dda1d0227 100644 --- a/unison-src/tests/r4x.u +++ b/unison-src/tests/r4x.u @@ -1,3 +1,4 @@ r4 : Int -> Int r4 = cases +1 -> +1 + x -> x From 1488d7fc0d04347d586d58ea219d77c194fd4f83 Mon Sep 17 00:00:00 2001 From: Travis Staton Date: Wed, 18 Jan 2023 09:53:13 -0500 Subject: [PATCH 26/54] fix pattern coverage in sequence-at-0 --- unison-src/tests/sequence-at-0.u | 1 + 1 file changed, 1 insertion(+) diff --git a/unison-src/tests/sequence-at-0.u b/unison-src/tests/sequence-at-0.u index 37f642935..ea80e80d0 100644 --- a/unison-src/tests/sequence-at-0.u +++ b/unison-src/tests/sequence-at-0.u @@ -1,2 +1,3 @@ > match at 0 [100] with Optional.Some _ -> "Hooray!" + Optional.None -> bug "unexpected" From 60482576b647846c48e44be2925341c4b230464a Mon Sep 17 00:00:00 2001 From: Travis Staton Date: Wed, 18 Jan 2023 09:53:53 -0500 Subject: [PATCH 27/54] fix pattern coverage in sequence-literal-argument-parsing.u --- unison-src/tests/sequence-literal-argument-parsing.u | 1 + 1 file changed, 1 insertion(+) diff --git a/unison-src/tests/sequence-literal-argument-parsing.u b/unison-src/tests/sequence-literal-argument-parsing.u index d6d495bca..f5901bb1e 100644 --- a/unison-src/tests/sequence-literal-argument-parsing.u +++ b/unison-src/tests/sequence-literal-argument-parsing.u @@ -3,3 +3,4 @@ structural type X a = X [a] f : X a -> a f = cases X.X [b] -> b + X.X _ -> bug "unexpected" From 1739cafc8338ad7fd67a51932351a668b74730e2 Mon Sep 17 00:00:00 2001 From: Travis Staton Date: Wed, 18 Jan 2023 10:28:20 -0500 Subject: [PATCH 28/54] fix pattern coverage in tictactoe2 --- unison-src/tests/tictactoe2.u | 55 ++++++++++++++++------------------- 1 file changed, 25 insertions(+), 30 deletions(-) diff --git a/unison-src/tests/tictactoe2.u b/unison-src/tests/tictactoe2.u index 9ebaf3b30..d5965c244 100644 --- a/unison-src/tests/tictactoe2.u +++ b/unison-src/tests/tictactoe2.u @@ -7,6 +7,18 @@ use Board Board use P O X E use Optional Some None +foldLeft : (b -> a -> b) -> b -> [a] -> b +foldLeft f = + go z xs = match xs with + [] -> z + a +: as -> go (f z a) as + go + +orElse a b = + match a with + None -> b + a -> a + isWin : Board -> Optional P isWin board = same : P -> P -> P -> Optional P @@ -18,36 +30,19 @@ isWin board = -- horizontal left/center/right -- diagonal rising/falling Board a b c - _ _ _ - _ _ _ -> same a b c - - Board _ _ _ - a b c - _ _ _ -> same a b c - - Board _ _ _ - _ _ _ - a b c -> same a b c - - Board a _ _ - b _ _ - c _ _ -> same a b c - - Board _ a _ - _ b _ - _ c _ -> same a b c - - Board _ _ a - _ _ b - _ _ c -> same a b c - - Board a _ _ - _ b _ - _ _ c -> same a b c - - Board _ _ a - _ b _ - c _ _ -> same a b c + d e f + g h i + -> + foldLeft orElse None + [ same a b c + , same d e f + , same g h i + , same a d g + , same b e h + , same c f i + , same a e i + , same g e c + ] x = isWin (Board X O X O X X From 281e8f1ddfbb1b3b93aaced365973bb5cbdf0fe7 Mon Sep 17 00:00:00 2001 From: Travis Staton Date: Mon, 27 Feb 2023 11:30:44 -0500 Subject: [PATCH 29/54] complete patterns in patternMatchTls --- unison-src/transcripts/patternMatchTls.md | 15 ++++++++----- .../transcripts/patternMatchTls.output.md | 21 ++++++++++++------- 2 files changed, 24 insertions(+), 12 deletions(-) diff --git a/unison-src/transcripts/patternMatchTls.md b/unison-src/transcripts/patternMatchTls.md index 6d600f535..1fe2c295b 100644 --- a/unison-src/transcripts/patternMatchTls.md +++ b/unison-src/transcripts/patternMatchTls.md @@ -13,13 +13,18 @@ use builtin.io2.Tls newClient send handshake terminate frank: '{IO} () frank = do - (Right socket) = clientSocket.impl "example.com" "443" + socket = assertRight (clientSocket.impl "example.com" "443") config = ClientConfig.default "example.com" 0xs - (Right tls) = newClient.impl config socket - (Right ()) = handshake.impl tls - (Right ()) = send.impl tls 0xs - (Right ()) = terminate.impl tls + tls = assertRight (newClient.impl config socket) + () = assertRight (handshake.impl tls) + () = assertRight (send.impl tls 0xs) + () = assertRight (terminate.impl tls) () + +assertRight : Either a b -> b +assertRight = cases + Right x -> x + Left _ -> bug "expected a right but got a left" ``` diff --git a/unison-src/transcripts/patternMatchTls.output.md b/unison-src/transcripts/patternMatchTls.output.md index b1dd77c96..726af9f86 100644 --- a/unison-src/transcripts/patternMatchTls.output.md +++ b/unison-src/transcripts/patternMatchTls.output.md @@ -8,13 +8,18 @@ use builtin.io2.Tls newClient send handshake terminate frank: '{IO} () frank = do - (Right socket) = clientSocket.impl "example.com" "443" + socket = assertRight (clientSocket.impl "example.com" "443") config = ClientConfig.default "example.com" 0xs - (Right tls) = newClient.impl config socket - (Right ()) = handshake.impl tls - (Right ()) = send.impl tls 0xs - (Right ()) = terminate.impl tls + tls = assertRight (newClient.impl config socket) + () = assertRight (handshake.impl tls) + () = assertRight (send.impl tls 0xs) + () = assertRight (terminate.impl tls) () + +assertRight : Either a b -> b +assertRight = cases + Right x -> x + Left _ -> bug "expected a right but got a left" ``` ```ucm @@ -25,7 +30,8 @@ frank = do ⍟ These new definitions are ok to `add`: - frank : '{IO} () + assertRight : Either a b -> b + frank : '{IO} () ``` ```ucm @@ -33,7 +39,8 @@ frank = do ⍟ I've added these definitions: - frank : '{IO} () + assertRight : Either a b -> b + frank : '{IO} () .> run frank From 2833779f58929c77f79fe62414f6805e083d29b9 Mon Sep 17 00:00:00 2001 From: Travis Staton Date: Mon, 27 Feb 2023 11:31:41 -0500 Subject: [PATCH 30/54] update pattern-match-coverage transcript --- .../transcripts/pattern-match-coverage.output.md | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/unison-src/transcripts/pattern-match-coverage.output.md b/unison-src/transcripts/pattern-match-coverage.output.md index 0103006da..c9c5cf96c 100644 --- a/unison-src/transcripts/pattern-match-coverage.output.md +++ b/unison-src/transcripts/pattern-match-coverage.output.md @@ -5,7 +5,7 @@ unique type T = A | B | C test : T -> () test = cases - A -> 0 + A -> () ``` ```ucm @@ -13,7 +13,7 @@ test = cases Pattern match is non-exhaustive In the match: 4 | test = cases - 5 | A -> 0 + 5 | A -> () Patterns not matched: @@ -28,17 +28,17 @@ unique type T = A | B | C test : T -> () test = cases - A -> 0 - B -> 0 - C -> 0 - _ -> 0 + A -> () + B -> () + C -> () + _ -> () ``` ```ucm Pattern match is redundant In the match case: - 8 | _ -> 0 + 8 | _ -> () ``` From ecae9aa967b9739d689a3b7d1f8ac8abd960f158 Mon Sep 17 00:00:00 2001 From: Travis Staton Date: Mon, 27 Feb 2023 11:32:23 -0500 Subject: [PATCH 31/54] ormolu --- unison-core/src/Unison/Term.hs | 22 +++++++++++----------- 1 file changed, 11 insertions(+), 11 deletions(-) diff --git a/unison-core/src/Unison/Term.hs b/unison-core/src/Unison/Term.hs index 1656d3380..7a84998e9 100644 --- a/unison-core/src/Unison/Term.hs +++ b/unison-core/src/Unison/Term.hs @@ -164,16 +164,16 @@ bindNames unsafeVarToName keepFreeTerms ns0 e = do okTm (v, a) = case Names.lookupHQTerm (Name.convert $ unsafeVarToName v) ns of rs | Set.size rs == 1 -> - pure (v, fromReferent a $ Set.findMin rs) + pure (v, fromReferent a $ Set.findMin rs) | otherwise -> case NES.nonEmptySet rs of - Nothing -> Left (pure (Names.TermResolutionFailure v a Names.NotFound)) - Just refs -> Left (pure (Names.TermResolutionFailure v a (Names.Ambiguous ns0 refs))) + Nothing -> Left (pure (Names.TermResolutionFailure v a Names.NotFound)) + Just refs -> Left (pure (Names.TermResolutionFailure v a (Names.Ambiguous ns0 refs))) okTy (v, a) = case Names.lookupHQType (Name.convert $ unsafeVarToName v) ns of rs | Set.size rs == 1 -> pure (v, Type.ref a $ Set.findMin rs) | otherwise -> case NES.nonEmptySet rs of - Nothing -> Left (pure (Names.TypeResolutionFailure v a Names.NotFound)) - Just refs -> Left (pure (Names.TypeResolutionFailure v a (Names.Ambiguous ns0 refs))) + Nothing -> Left (pure (Names.TypeResolutionFailure v a Names.NotFound)) + Just refs -> Left (pure (Names.TypeResolutionFailure v a (Names.Ambiguous ns0 refs))) termSubsts <- validate okTm freeTmVars typeSubsts <- validate okTy freeTyVars pure . substTypeVars typeSubsts . ABT.substsInheritAnnotation termSubsts $ e @@ -218,7 +218,7 @@ prepareTDNR t = fmap fst . ABT.visitPure f $ ABT.annotateBound t where f (ABT.Term _ (a, bound) (ABT.Var v)) | Set.notMember v bound = - Just $ resolve (a, bound) a (Text.unpack $ Var.name v) + Just $ resolve (a, bound) a (Text.unpack $ Var.name v) f _ = Nothing amap :: (Ord v) => (a -> a2) -> Term v a -> Term v a2 @@ -390,10 +390,10 @@ substTypeVar vt ty = go Set.empty -- variable name for v which is unique, v', and rename v to v' in e. uncapture vs e t@(Type.Forall' body) | Set.member (ABT.variable body) fvs = - let v = ABT.variable body - v2 = Var.freshIn (ABT.freeVars t) . Var.freshIn (Set.insert vt fvs) $ v - t2 = ABT.bindInheritAnnotation body (Type.var () v2) - in uncapture ((ABT.annotation t, v2) : vs) (renameTypeVar v v2 e) t2 + let v = ABT.variable body + v2 = Var.freshIn (ABT.freeVars t) . Var.freshIn (Set.insert vt fvs) $ v + t2 = ABT.bindInheritAnnotation body (Type.var () v2) + in uncapture ((ABT.annotation t, v2) : vs) (renameTypeVar v v2 e) t2 uncapture vs e t0 = let t = foldl (\body (loc, v) -> Type.forall loc v body) t0 vs bound' = case Type.unForalls (Type.stripIntroOuters t) of @@ -631,7 +631,7 @@ unDelay :: (Ord v) => Term2 vt at ap v a -> Maybe (Term2 vt at ap v a) unDelay tm = case ABT.out tm of ABT.Tm (Lam (ABT.Term _ _ (ABT.Abs v body))) | Set.notMember v (ABT.freeVars body) -> - Just body + Just body _ -> Nothing pattern LamNamed' :: From 16585a41509c1be120618868f63e63e64900afab Mon Sep 17 00:00:00 2001 From: Travis Staton Date: Mon, 27 Feb 2023 16:02:22 -0500 Subject: [PATCH 32/54] Ensure data declaration map is populated as expected by pattern match coverage checker --- parser-typechecker/src/Unison/Codebase.hs | 39 +++++++++++++++++------ 1 file changed, 29 insertions(+), 10 deletions(-) diff --git a/parser-typechecker/src/Unison/Codebase.hs b/parser-typechecker/src/Unison/Codebase.hs index b38a404c6..757f87ea5 100644 --- a/parser-typechecker/src/Unison/Codebase.hs +++ b/parser-typechecker/src/Unison/Codebase.hs @@ -161,6 +161,7 @@ import Unison.Symbol (Symbol) import Unison.Term (Term) import qualified Unison.Term as Term import Unison.Type (Type) +import qualified Unison.Type as Type import Unison.Typechecker.TypeLookup (TypeLookup (TypeLookup)) import qualified Unison.Typechecker.TypeLookup as TL import qualified Unison.UnisonFile as UF @@ -338,6 +339,7 @@ lookupWatchCache codebase h = do maybe (getWatch codebase WK.TestWatch h) (pure . Just) m1 typeLookupForDependencies :: + forall m a. (BuiltinAnnotation a) => Codebase m Symbol a -> Set Reference -> @@ -347,17 +349,34 @@ typeLookupForDependencies codebase s = do foldM go mempty s where go tl ref@(Reference.DerivedId id) = - fmap (tl <>) $ - getTypeOfTerm codebase ref >>= \case - Just typ -> pure $ TypeLookup (Map.singleton ref typ) mempty mempty - Nothing -> - getTypeDeclaration codebase id >>= \case - Just (Left ed) -> - pure $ TypeLookup mempty mempty (Map.singleton ref ed) - Just (Right dd) -> - pure $ TypeLookup mempty (Map.singleton ref dd) mempty - Nothing -> pure mempty + getTypeOfTerm codebase ref >>= \case + Just typ -> pure $ tl <> TypeLookup (Map.singleton ref typ) mempty mempty + Nothing -> + getTypeDeclaration codebase id >>= \case + Just (Left ed) -> + pure $ tl <> TypeLookup mempty mempty (Map.singleton ref ed) + Just (Right dd) -> do + -- We need the transitive dependencies of data decls + -- that are scrutinized in a match expression for + -- pattern match coverage checking (specifically for + -- the inhabitation check). We ensure these are found + -- by collecting all type dependencies for all data + -- decls. + let constructorTypes :: [Type Symbol a] + constructorTypes = snd <$> DD.constructors dd + + -- All references from constructorTypes that we + -- have not already gathered. + constructorRefs :: Set Reference + constructorRefs = foldl' (\b a -> Set.filter (unseen tl) (Type.dependencies a) <> b) mempty constructorTypes + + -- recursively call go for each constructor ref + let z = tl <> TypeLookup mempty (Map.singleton ref dd) mempty + foldM go z constructorRefs + Nothing -> pure tl go tl Reference.Builtin {} = pure tl -- codebase isn't consulted for builtins + unseen :: TL.TypeLookup Symbol a -> Reference -> Bool + unseen tl r = isNothing (Map.lookup r (TL.dataDecls tl)) toCodeLookup :: (MonadIO m) => Codebase m Symbol Parser.Ann -> CL.CodeLookup Symbol m Parser.Ann toCodeLookup c = From 74cd76b49f586cd8e883cbec824e8044f74827e6 Mon Sep 17 00:00:00 2001 From: Travis Staton Date: Mon, 27 Feb 2023 16:12:10 -0500 Subject: [PATCH 33/54] typos and transcript edit --- parser-typechecker/src/Unison/PrintError.hs | 2 +- parser-typechecker/src/Unison/Runtime/Interface.hs | 2 ++ unison-cli/src/Unison/Codebase/Editor/Propagate.hs | 2 +- unison-src/transcripts/pattern-match-coverage.md | 10 +++++----- 4 files changed, 9 insertions(+), 7 deletions(-) diff --git a/parser-typechecker/src/Unison/PrintError.hs b/parser-typechecker/src/Unison/PrintError.hs index b4022f891..cc352f778 100644 --- a/parser-typechecker/src/Unison/PrintError.hs +++ b/parser-typechecker/src/Unison/PrintError.hs @@ -976,7 +976,7 @@ renderCompilerBug env _src bug = mconcat $ case bug of C.Data -> " data type" C.Effect -> " ability", "\n", - " reerence = ", + " reference = ", showTypeRef env rf ] C.UnknownConstructor sort (ConstructorReference rf i) _decl -> diff --git a/parser-typechecker/src/Unison/Runtime/Interface.hs b/parser-typechecker/src/Unison/Runtime/Interface.hs index 22ca1cfe4..c1374f169 100644 --- a/parser-typechecker/src/Unison/Runtime/Interface.hs +++ b/parser-typechecker/src/Unison/Runtime/Interface.hs @@ -151,6 +151,7 @@ recursiveDeclDeps :: Set RF.LabeledDependency -> CodeLookup Symbol IO () -> Decl Symbol () -> + -- (type deps, term deps) IO (Set Reference, Set Reference) recursiveDeclDeps seen0 cl d = do rec <- for (toList newDeps) $ \case @@ -176,6 +177,7 @@ recursiveTermDeps :: Set RF.LabeledDependency -> CodeLookup Symbol IO () -> Term Symbol -> + -- (type deps, term deps) IO (Set Reference, Set Reference) recursiveTermDeps seen0 cl tm = do rec <- for (toList (deps \\ seen0)) $ \case diff --git a/unison-cli/src/Unison/Codebase/Editor/Propagate.hs b/unison-cli/src/Unison/Codebase/Editor/Propagate.hs index af90bd55f..61a56d03e 100644 --- a/unison-cli/src/Unison/Codebase/Editor/Propagate.hs +++ b/unison-cli/src/Unison/Codebase/Editor/Propagate.hs @@ -559,7 +559,7 @@ typecheckFile :: Codebase m Symbol Ann -> [Type Symbol Ann] -> UF.UnisonFile Symbol Ann -> - Sqlite.Transaction (Result.Result (Seq (Result.Note Symbol Ann)) (Either Names (UF.TypecheckedUnisonFile Symbol Ann))) + Sqlite.Transaction (Result.Result (Seq (Result.Note Symbol Ann)) (Either x (UF.TypecheckedUnisonFile Symbol Ann))) typecheckFile codebase ambient file = do typeLookup <- Codebase.typeLookupForDependencies codebase (UF.dependencies file) pure . fmap Right $ synthesizeFile' ambient (typeLookup <> Builtin.typeLookup) file diff --git a/unison-src/transcripts/pattern-match-coverage.md b/unison-src/transcripts/pattern-match-coverage.md index 1affffa78..6034984b8 100644 --- a/unison-src/transcripts/pattern-match-coverage.md +++ b/unison-src/transcripts/pattern-match-coverage.md @@ -9,7 +9,7 @@ unique type T = A | B | C test : T -> () test = cases - A -> 0 + A -> () ``` redundant matches are reported @@ -18,10 +18,10 @@ unique type T = A | B | C test : T -> () test = cases - A -> 0 - B -> 0 - C -> 0 - _ -> 0 + A -> () + B -> () + C -> () + _ -> () ``` patterns that would imply supplying an uninhabited type are not expected From e11574e4723c28a19fc5bcf978dd4ee9feb76259 Mon Sep 17 00:00:00 2001 From: Travis Staton Date: Mon, 27 Feb 2023 16:14:19 -0500 Subject: [PATCH 34/54] ormolu --- unison-core/src/Unison/Term.hs | 22 +++++++++++----------- 1 file changed, 11 insertions(+), 11 deletions(-) diff --git a/unison-core/src/Unison/Term.hs b/unison-core/src/Unison/Term.hs index 7a84998e9..1656d3380 100644 --- a/unison-core/src/Unison/Term.hs +++ b/unison-core/src/Unison/Term.hs @@ -164,16 +164,16 @@ bindNames unsafeVarToName keepFreeTerms ns0 e = do okTm (v, a) = case Names.lookupHQTerm (Name.convert $ unsafeVarToName v) ns of rs | Set.size rs == 1 -> - pure (v, fromReferent a $ Set.findMin rs) + pure (v, fromReferent a $ Set.findMin rs) | otherwise -> case NES.nonEmptySet rs of - Nothing -> Left (pure (Names.TermResolutionFailure v a Names.NotFound)) - Just refs -> Left (pure (Names.TermResolutionFailure v a (Names.Ambiguous ns0 refs))) + Nothing -> Left (pure (Names.TermResolutionFailure v a Names.NotFound)) + Just refs -> Left (pure (Names.TermResolutionFailure v a (Names.Ambiguous ns0 refs))) okTy (v, a) = case Names.lookupHQType (Name.convert $ unsafeVarToName v) ns of rs | Set.size rs == 1 -> pure (v, Type.ref a $ Set.findMin rs) | otherwise -> case NES.nonEmptySet rs of - Nothing -> Left (pure (Names.TypeResolutionFailure v a Names.NotFound)) - Just refs -> Left (pure (Names.TypeResolutionFailure v a (Names.Ambiguous ns0 refs))) + Nothing -> Left (pure (Names.TypeResolutionFailure v a Names.NotFound)) + Just refs -> Left (pure (Names.TypeResolutionFailure v a (Names.Ambiguous ns0 refs))) termSubsts <- validate okTm freeTmVars typeSubsts <- validate okTy freeTyVars pure . substTypeVars typeSubsts . ABT.substsInheritAnnotation termSubsts $ e @@ -218,7 +218,7 @@ prepareTDNR t = fmap fst . ABT.visitPure f $ ABT.annotateBound t where f (ABT.Term _ (a, bound) (ABT.Var v)) | Set.notMember v bound = - Just $ resolve (a, bound) a (Text.unpack $ Var.name v) + Just $ resolve (a, bound) a (Text.unpack $ Var.name v) f _ = Nothing amap :: (Ord v) => (a -> a2) -> Term v a -> Term v a2 @@ -390,10 +390,10 @@ substTypeVar vt ty = go Set.empty -- variable name for v which is unique, v', and rename v to v' in e. uncapture vs e t@(Type.Forall' body) | Set.member (ABT.variable body) fvs = - let v = ABT.variable body - v2 = Var.freshIn (ABT.freeVars t) . Var.freshIn (Set.insert vt fvs) $ v - t2 = ABT.bindInheritAnnotation body (Type.var () v2) - in uncapture ((ABT.annotation t, v2) : vs) (renameTypeVar v v2 e) t2 + let v = ABT.variable body + v2 = Var.freshIn (ABT.freeVars t) . Var.freshIn (Set.insert vt fvs) $ v + t2 = ABT.bindInheritAnnotation body (Type.var () v2) + in uncapture ((ABT.annotation t, v2) : vs) (renameTypeVar v v2 e) t2 uncapture vs e t0 = let t = foldl (\body (loc, v) -> Type.forall loc v body) t0 vs bound' = case Type.unForalls (Type.stripIntroOuters t) of @@ -631,7 +631,7 @@ unDelay :: (Ord v) => Term2 vt at ap v a -> Maybe (Term2 vt at ap v a) unDelay tm = case ABT.out tm of ABT.Tm (Lam (ABT.Term _ _ (ABT.Abs v body))) | Set.notMember v (ABT.freeVars body) -> - Just body + Just body _ -> Nothing pattern LamNamed' :: From 41d05fc145943b383895d7d30273cb64a0c0cf5c Mon Sep 17 00:00:00 2001 From: Travis Staton Date: Mon, 27 Feb 2023 17:48:25 -0500 Subject: [PATCH 35/54] ormolu --- .../src/Unison/PatternMatchCoverage/Class.hs | 2 +- .../Unison/PatternMatchCoverage/Constraint.hs | 2 +- .../Unison/PatternMatchCoverage/Desugar.hs | 10 ++--- .../src/Unison/PatternMatchCoverage/Fix.hs | 10 ++--- .../Unison/PatternMatchCoverage/GrdTree.hs | 10 ++--- .../Unison/PatternMatchCoverage/Literal.hs | 4 +- .../NormalizedConstraints.hs | 11 +++-- .../src/Unison/PatternMatchCoverage/PmLit.hs | 2 +- .../src/Unison/PatternMatchCoverage/Solve.hs | 40 +++++++++---------- .../src/Unison/PatternMatchCoverage/UFMap.hs | 6 +-- 10 files changed, 50 insertions(+), 47 deletions(-) diff --git a/parser-typechecker/src/Unison/PatternMatchCoverage/Class.hs b/parser-typechecker/src/Unison/PatternMatchCoverage/Class.hs index f908a2072..30f5407f4 100644 --- a/parser-typechecker/src/Unison/PatternMatchCoverage/Class.hs +++ b/parser-typechecker/src/Unison/PatternMatchCoverage/Class.hs @@ -21,7 +21,7 @@ data EnumeratedConstructors vt v loc deriving stock (Show) traverseConstructors :: - Applicative f => + (Applicative f) => (v -> ConstructorReference -> Type vt loc -> f (v, ConstructorReference, Type vt loc)) -> EnumeratedConstructors vt v loc -> f (EnumeratedConstructors vt v loc) diff --git a/parser-typechecker/src/Unison/PatternMatchCoverage/Constraint.hs b/parser-typechecker/src/Unison/PatternMatchCoverage/Constraint.hs index c465e023d..034d5cf75 100644 --- a/parser-typechecker/src/Unison/PatternMatchCoverage/Constraint.hs +++ b/parser-typechecker/src/Unison/PatternMatchCoverage/Constraint.hs @@ -48,5 +48,5 @@ prettyConstraint = \case Eq v0 v1 -> sep " " [pv v0, "=", pv v1] where pv = string . show - pc :: forall a. Show a => a -> Pretty ColorText + pc :: forall a. (Show a) => a -> Pretty ColorText pc = string . show diff --git a/parser-typechecker/src/Unison/PatternMatchCoverage/Desugar.hs b/parser-typechecker/src/Unison/PatternMatchCoverage/Desugar.hs index 3551d863b..d60ef92c8 100644 --- a/parser-typechecker/src/Unison/PatternMatchCoverage/Desugar.hs +++ b/parser-typechecker/src/Unison/PatternMatchCoverage/Desugar.hs @@ -16,7 +16,7 @@ import qualified Unison.Type as Type desugarMatch :: forall loc vt v m. - Pmc vt v loc m => + (Pmc vt v loc m) => -- | loc of match loc -> Type vt loc -> @@ -44,7 +44,7 @@ desugarMatch loc0 scrutineeType v0 cs0 = desugarPattern :: forall v vt loc m. - Pmc vt v loc m => + (Pmc vt v loc m) => Type vt loc -> v -> Pattern loc -> @@ -77,7 +77,7 @@ desugarPattern typ v0 pat k vs = case pat of handleSequence :: forall v vt loc m. - Pmc vt v loc m => + (Pmc vt v loc m) => Type vt loc -> v -> Pattern loc -> @@ -92,7 +92,7 @@ handleSequence typ v pat k vs = do listToGrdTree :: forall v vt loc m. - Pmc vt v loc m => + (Pmc vt v loc m) => Type vt loc -> Type vt loc -> v -> @@ -200,5 +200,5 @@ normalizeList pat0 = case goCons pat0 of As _loc pat -> goSnoc pat nlp _ -> error "goSnoc: unexpected pattern" -assignFreshPatternVars :: Pmc vt v loc m => [Pattern loc] -> m [(v, Pattern loc)] +assignFreshPatternVars :: (Pmc vt v loc m) => [Pattern loc] -> m [(v, Pattern loc)] assignFreshPatternVars pats = traverse (\p -> (,p) <$> fresh) pats diff --git a/parser-typechecker/src/Unison/PatternMatchCoverage/Fix.hs b/parser-typechecker/src/Unison/PatternMatchCoverage/Fix.hs index 99974ba72..9accc06fb 100644 --- a/parser-typechecker/src/Unison/PatternMatchCoverage/Fix.hs +++ b/parser-typechecker/src/Unison/PatternMatchCoverage/Fix.hs @@ -7,14 +7,14 @@ module Unison.PatternMatchCoverage.Fix where newtype Fix f = Fix {unFix :: f (Fix f)} -deriving instance (forall a. Show a => Show (f a)) => Show (Fix f) +deriving instance (forall a. (Show a) => Show (f a)) => Show (Fix f) -deriving instance (forall a. Eq a => Eq (f a)) => Eq (Fix f) +deriving instance (forall a. (Eq a) => Eq (f a)) => Eq (Fix f) -deriving instance (Eq (Fix f), forall a. Ord a => Ord (f a)) => Ord (Fix f) +deriving instance (Eq (Fix f), forall a. (Ord a) => Ord (f a)) => Ord (Fix f) -cata :: Functor f => (f a -> a) -> Fix f -> a +cata :: (Functor f) => (f a -> a) -> Fix f -> a cata alg = let c = alg . fmap c . unFix in c -para :: Functor f => (f (Fix f, a) -> a) -> Fix f -> a +para :: (Functor f) => (f (Fix f, a) -> a) -> Fix f -> a para alg = let c = alg . fmap (\x -> (x, c x)) . unFix in c diff --git a/parser-typechecker/src/Unison/PatternMatchCoverage/GrdTree.hs b/parser-typechecker/src/Unison/PatternMatchCoverage/GrdTree.hs index c84e2daa7..e11a5b842 100644 --- a/parser-typechecker/src/Unison/PatternMatchCoverage/GrdTree.hs +++ b/parser-typechecker/src/Unison/PatternMatchCoverage/GrdTree.hs @@ -29,11 +29,11 @@ prettyGrdTree prettyNode prettyLeaf = cata phi [] -> [] x : [] -> [sep " " ["──", x]] x0 : x1 : xs -> - sep " " ["┬─", x0] : - let go y0 = \case - [] -> [sep " " ["└─", y0]] - y1 : ys -> "├─ " <> y0 : go y1 ys - in [indent " " (sep "\n" (go x1 xs))] + sep " " ["┬─", x0] + : let go y0 = \case + [] -> [sep " " ["└─", y0]] + y1 : ys -> "├─ " <> y0 : go y1 ys + in [indent " " (sep "\n" (go x1 xs))] pattern Leaf :: l -> GrdTree n l pattern Leaf x = Fix (LeafF x) diff --git a/parser-typechecker/src/Unison/PatternMatchCoverage/Literal.hs b/parser-typechecker/src/Unison/PatternMatchCoverage/Literal.hs index dd38f85b3..7d0f52c54 100644 --- a/parser-typechecker/src/Unison/PatternMatchCoverage/Literal.hs +++ b/parser-typechecker/src/Unison/PatternMatchCoverage/Literal.hs @@ -40,7 +40,7 @@ data Literal vt v loc | Let v (Term' vt v loc) (Type vt loc) deriving stock (Show) -prettyLiteral :: Var v => Literal (TypeVar b v) v loc -> Pretty ColorText +prettyLiteral :: (Var v) => Literal (TypeVar b v) v loc -> Pretty ColorText prettyLiteral = \case T -> "✓" F -> "⨉" @@ -57,5 +57,5 @@ prettyLiteral = \case Let var expr typ -> sep " " ["let", pv var, "=", TermPrinter.pretty PPE.empty (lowerTerm expr), ":", TypePrinter.pretty PPE.empty typ] where pv = string . show - pc :: forall a. Show a => a -> Pretty ColorText + pc :: forall a. (Show a) => a -> Pretty ColorText pc = string . show diff --git a/parser-typechecker/src/Unison/PatternMatchCoverage/NormalizedConstraints.hs b/parser-typechecker/src/Unison/PatternMatchCoverage/NormalizedConstraints.hs index da0af8dfd..44a6fabaa 100644 --- a/parser-typechecker/src/Unison/PatternMatchCoverage/NormalizedConstraints.hs +++ b/parser-typechecker/src/Unison/PatternMatchCoverage/NormalizedConstraints.hs @@ -51,7 +51,7 @@ data NormalizedConstraints vt v loc = NormalizedConstraints -- | Mark a variable as requiring a new test for inhabitation. markDirty :: - Ord v => + (Ord v) => v -> NormalizedConstraints vt v loc -> NormalizedConstraints vt v loc @@ -61,7 +61,7 @@ markDirty k nc@NormalizedConstraints {dirtySet} = dom :: NormalizedConstraints vt v loc -> [v] dom NormalizedConstraints {constraintMap} = UFMap.keys constraintMap -emptyNormalizedConstraints :: Ord v => NormalizedConstraints vt v loc +emptyNormalizedConstraints :: (Ord v) => NormalizedConstraints vt v loc emptyNormalizedConstraints = NormalizedConstraints { constraintMap = UFMap.empty, @@ -240,8 +240,11 @@ prettyNormalizedConstraints (NormalizedConstraints {constraintMap}) = sep " " [" IsNotEffectful -> [] IsEffectful -> [Effectful kcanon] in sep " " $ - pv kcanon : - fmap pv (Set.toList $ Set.delete kcanon ks) ++ [":", TypePrinter.pretty PPE.empty (vi_typ vi)] ++ ["|"] ++ [sep ", " $ fmap prettyConstraint (posCon ++ negCon ++ botCon)] + pv kcanon + : fmap pv (Set.toList $ Set.delete kcanon ks) + ++ [":", TypePrinter.pretty PPE.empty (vi_typ vi)] + ++ ["|"] + ++ [sep ", " $ fmap prettyConstraint (posCon ++ negCon ++ botCon)] pv = string . show prettyDnf :: (Var v, Var vt) => Set (NormalizedConstraints vt v loc) -> Pretty ColorText diff --git a/parser-typechecker/src/Unison/PatternMatchCoverage/PmLit.hs b/parser-typechecker/src/Unison/PatternMatchCoverage/PmLit.hs index 42ec9389f..1a2f5e2a2 100644 --- a/parser-typechecker/src/Unison/PatternMatchCoverage/PmLit.hs +++ b/parser-typechecker/src/Unison/PatternMatchCoverage/PmLit.hs @@ -12,7 +12,7 @@ data PmLit | Char Char deriving stock (Show, Eq, Ord) -prettyPmLit :: IsString s => PmLit -> Pretty s +prettyPmLit :: (IsString s) => PmLit -> Pretty s prettyPmLit = string . \case Int x -> show x diff --git a/parser-typechecker/src/Unison/PatternMatchCoverage/Solve.hs b/parser-typechecker/src/Unison/PatternMatchCoverage/Solve.hs index 8134aa5b7..742d78656 100644 --- a/parser-typechecker/src/Unison/PatternMatchCoverage/Solve.hs +++ b/parser-typechecker/src/Unison/PatternMatchCoverage/Solve.hs @@ -46,7 +46,7 @@ import Unison.Var (Var) -- redundant. uncoverAnnotate :: forall vt v loc m l. - Pmc vt v loc m => + (Pmc vt v loc m) => Set (NormalizedConstraints vt v loc) -> GrdTree (PmGrd vt v loc) l -> ( m @@ -163,7 +163,7 @@ classifyAlg = \case -- one solution) into a pattern. expand :: forall vt v loc. - Var v => + (Var v) => v -> NormalizedConstraints vt v loc -> Pattern () @@ -235,7 +235,7 @@ instantiate fuel nc x c argTyps posConstraint = do -- expression with enough positive info to print pattern suggestions. expandSolution :: forall vt v loc m. - Pmc vt v loc m => + (Pmc vt v loc m) => v -> NormalizedConstraints vt v loc -> m (Set (NormalizedConstraints vt v loc)) @@ -297,7 +297,7 @@ expandSolution x nc = withConstructors :: forall vt v loc r m. - Pmc vt v loc m => + (Pmc vt v loc m) => m r -> VarInfo vt v loc -> ( forall x. @@ -356,7 +356,7 @@ mkMatchingInterval = \case -- described in section 3.7. inhabited :: forall vt v loc m. - Pmc vt v loc m => + (Pmc vt v loc m) => Fuel -> v -> NormalizedConstraints vt v loc -> @@ -386,7 +386,7 @@ initFuel = 8 -- | Check that all variables marked dirty are inhabited. ensureInhabited :: forall vt v loc m. - Pmc vt v loc m => + (Pmc vt v loc m) => Fuel -> NormalizedConstraints vt v loc -> m (Maybe (NormalizedConstraints vt v loc)) @@ -436,7 +436,7 @@ addLiteral lit0 nabla0 = runMaybeT do insertVarInfo :: forall vt v loc. - Ord v => + (Ord v) => v -> VarInfo vt v loc -> NormalizedConstraints vt v loc -> @@ -688,7 +688,7 @@ modifyConstructor v f nc = runIdentity $ modifyConstructorF v (\a b -> Identity modifyConstructorC :: forall vt v loc m. - Pmc vt v loc m => + (Pmc vt v loc m) => v -> ( (Maybe (ConstructorReference, [(v, Type vt loc)])) -> Set ConstructorReference -> @@ -794,7 +794,7 @@ modifyVarConstraints v updateVarConstraint nc0 = do -- | Modify the positive and negative constraints of a constructor. posAndNegConstructor :: forall f vt v loc. - Functor f => + (Functor f) => ( (Maybe (ConstructorReference, [(v, Type vt loc)])) -> Set ConstructorReference -> f (Maybe (ConstructorReference, [(v, Type vt loc)]), Set ConstructorReference) @@ -811,7 +811,7 @@ posAndNegConstructor f = \case -- an instance of Ord. posAndNegLiteral :: forall f vt v loc. - Functor f => + (Functor f) => ( forall a. (Ord a) => Maybe a -> @@ -841,7 +841,7 @@ posAndNegLiteral f lit = \case posAndNegList :: forall f vt v loc. - Functor f => + (Functor f) => ( Type vt loc -> Seq v -> Seq v -> @@ -865,27 +865,27 @@ newtype C vt v loc m a = C via StateT (NormalizedConstraints vt v loc) (MaybeT m) deriving (MonadTrans) via ComposeT (StateT (NormalizedConstraints vt v loc)) MaybeT -contradiction :: Applicative m => C vt v loc m a +contradiction :: (Applicative m) => C vt v loc m a contradiction = C \_ -> pure Nothing -update :: Pmc vt v loc m => v -> VarConstraints vt v loc -> C vt v loc m () +update :: (Pmc vt v loc m) => v -> VarConstraints vt v loc -> C vt v loc m () update v vc = do nc0 <- get let (var, vi, nc1) = expectCanon v nc0 nc2 = markDirty var ((insertVarInfo var vi {vi_con = vc}) nc1) put nc2 -equate :: Pmc vt v loc m => [(v, v)] -> C vt v loc m () +equate :: (Pmc vt v loc m) => [(v, v)] -> C vt v loc m () equate vs = addConstraintsC (map (uncurry C.Eq) vs) -lookupListElemTypeC :: Pmc vt v loc m => v -> C vt v loc m (Type vt loc) +lookupListElemTypeC :: (Pmc vt v loc m) => v -> C vt v loc m (Type vt loc) lookupListElemTypeC listVar = do nc0 <- get let (_var, vi, nc1) = expectCanon listVar nc0 put nc1 pure $ getConst (posAndNegList (\elemTyp _ _ _ -> Const elemTyp) (vi_con vi)) -addConstraintsC :: Pmc vt v loc m => [Constraint vt v loc] -> C vt v loc m () +addConstraintsC :: (Pmc vt v loc m) => [Constraint vt v loc] -> C vt v loc m () addConstraintsC cs = do nc <- get lift (addConstraints cs nc) >>= \case @@ -893,7 +893,7 @@ addConstraintsC cs = do Just nc -> put nc declVarC :: - Pmc vt v loc m => + (Pmc vt v loc m) => v -> Type vt loc -> (VarInfo vt v loc -> VarInfo vt v loc) -> @@ -904,11 +904,11 @@ declVarC v vt vimod = do put nc1 freshC :: - Pmc vt v loc m => + (Pmc vt v loc m) => C vt v loc m v freshC = lift fresh -populateCons :: Pmc vt v loc m => v -> Seq v -> IntervalSet -> C vt v loc m () +populateCons :: (Pmc vt v loc m) => v -> Seq v -> IntervalSet -> C vt v loc m () populateCons listVar pCons iset = do case IntervalSet.lookupMin iset of Just minLen @@ -923,7 +923,7 @@ populateCons listVar pCons iset = do _ -> pure () runC :: - Applicative m => + (Applicative m) => NormalizedConstraints vt v loc -> C vt v loc m a -> m (Maybe (a, NormalizedConstraints vt v loc)) diff --git a/parser-typechecker/src/Unison/PatternMatchCoverage/UFMap.hs b/parser-typechecker/src/Unison/PatternMatchCoverage/UFMap.hs index 1b95f1c19..d5d2ca9e4 100644 --- a/parser-typechecker/src/Unison/PatternMatchCoverage/UFMap.hs +++ b/parser-typechecker/src/Unison/PatternMatchCoverage/UFMap.hs @@ -43,7 +43,7 @@ data UFValue k v empty :: UFMap k v empty = UFMap Map.empty -insert :: Ord k => k -> v -> UFMap k v -> UFMap k v +insert :: (Ord k) => k -> v -> UFMap k v -> UFMap k v insert k !v m = alter k (Just v) (\_ s _ -> Canonical s v) m @@ -129,7 +129,7 @@ alter k handleNothing handleJust map0 = runIdentity (alterF k (Identity handleNothing) (\k s v -> Identity (handleJust k s v)) map0) lookupCanon :: - Ord k => + (Ord k) => k -> UFMap k v -> Maybe (k, Int, v, UFMap k v) @@ -206,7 +206,7 @@ union k0 k1 mapinit mergeValues = toMaybe do KeyNotFound _k -> Nothing MergeFailed _v0 _v1 -> Nothing -toClasses :: forall k v. Ord k => UFMap k v -> [(k, Set k, v)] +toClasses :: forall k v. (Ord k) => UFMap k v -> [(k, Set k, v)] toClasses m0 = let cmFinal :: Map k (k, Set k, v) (_mfinal, cmFinal) = foldl' phi (m0, Map.empty) keys From d69071fb2ca90e8836375e292f17aee9cbeb98ef Mon Sep 17 00:00:00 2001 From: Travis Staton Date: Mon, 27 Feb 2023 17:51:17 -0500 Subject: [PATCH 36/54] ormolu --- .../src/Unison/Runtime/IOSource.hs | 2 +- .../src/Unison/Typechecker/Context.hs | 2 +- unison-cli/src/Unison/LSP/FileAnalysis.hs | 24 +++++++++---------- 3 files changed, 14 insertions(+), 14 deletions(-) diff --git a/parser-typechecker/src/Unison/Runtime/IOSource.hs b/parser-typechecker/src/Unison/Runtime/IOSource.hs index c7c589389..11bec2fa3 100644 --- a/parser-typechecker/src/Unison/Runtime/IOSource.hs +++ b/parser-typechecker/src/Unison/Runtime/IOSource.hs @@ -978,7 +978,7 @@ type SynthResult = type EitherResult = Either String TFile -showNotes :: Foldable f => String -> PrintError.Env -> f Note -> String +showNotes :: (Foldable f) => String -> PrintError.Env -> f Note -> String showNotes source env = intercalateMap "\n\n" $ PrintError.renderNoteAsANSI 60 env source Path.absoluteEmpty diff --git a/parser-typechecker/src/Unison/Typechecker/Context.hs b/parser-typechecker/src/Unison/Typechecker/Context.hs index e6b826c17..54b4a578c 100644 --- a/parser-typechecker/src/Unison/Typechecker/Context.hs +++ b/parser-typechecker/src/Unison/Typechecker/Context.hs @@ -3147,7 +3147,7 @@ instance (Monad f) => MonadState (Env v loc) (MT v loc f) where get = MT \_ _ env -> pure (env, env) put env = MT \_ _ _ -> pure ((), env) -instance MonadFix f => MonadFix (MT v loc f) where +instance (MonadFix f) => MonadFix (MT v loc f) where mfix f = MT \a b c -> let res = mfix (\ ~(wubble, _finalenv) -> runM (f wubble) a b c) in res diff --git a/unison-cli/src/Unison/LSP/FileAnalysis.hs b/unison-cli/src/Unison/LSP/FileAnalysis.hs index ae4bcf753..7b264d3c1 100644 --- a/unison-cli/src/Unison/LSP/FileAnalysis.hs +++ b/unison-cli/src/Unison/LSP/FileAnalysis.hs @@ -342,18 +342,18 @@ analyseNotes fileUri ppe src notes = do typeHoleReplacementCodeActions diags v typ | not (isUserBlank v) = pure [] | otherwise = do - Env {codebase} <- ask - ppe <- PPED.suffixifiedPPE <$> globalPPED - let cleanedTyp = Context.generalizeAndUnTypeVar typ -- TODO: is this right? - refs <- liftIO . Codebase.runTransaction codebase $ Codebase.termsOfType codebase cleanedTyp - forMaybe (toList refs) $ \ref -> runMaybeT $ do - hqNameSuggestion <- MaybeT . pure $ PPE.terms ppe ref - typ <- MaybeT . liftIO . Codebase.runTransaction codebase $ Codebase.getTypeOfReferent codebase ref - let prettyType = TypePrinter.prettyStr Nothing ppe typ - let txtName = HQ'.toText hqNameSuggestion - let ranges = (diags ^.. folded . range) - let rca = rangedCodeAction ("Use " <> txtName <> " : " <> Text.pack prettyType) diags ranges - pure $ includeEdits fileUri txtName ranges rca + Env {codebase} <- ask + ppe <- PPED.suffixifiedPPE <$> globalPPED + let cleanedTyp = Context.generalizeAndUnTypeVar typ -- TODO: is this right? + refs <- liftIO . Codebase.runTransaction codebase $ Codebase.termsOfType codebase cleanedTyp + forMaybe (toList refs) $ \ref -> runMaybeT $ do + hqNameSuggestion <- MaybeT . pure $ PPE.terms ppe ref + typ <- MaybeT . liftIO . Codebase.runTransaction codebase $ Codebase.getTypeOfReferent codebase ref + let prettyType = TypePrinter.prettyStr Nothing ppe typ + let txtName = HQ'.toText hqNameSuggestion + let ranges = (diags ^.. folded . range) + let rca = rangedCodeAction ("Use " <> txtName <> " : " <> Text.pack prettyType) diags ranges + pure $ includeEdits fileUri txtName ranges rca isUserBlank :: Symbol -> Bool isUserBlank v = case Var.typeOf v of Var.User name -> Text.isPrefixOf "_" name From 184e47f44732779d1feadc608cd63118d667d816 Mon Sep 17 00:00:00 2001 From: Travis Staton Date: Tue, 28 Feb 2023 09:56:53 -0500 Subject: [PATCH 37/54] make pattern match complete in LSP test --- unison-cli/tests/Unison/Test/LSP.hs | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/unison-cli/tests/Unison/Test/LSP.hs b/unison-cli/tests/Unison/Test/LSP.hs index 0db0a3c44..95b7aaeda 100644 --- a/unison-cli/tests/Unison/Test/LSP.hs +++ b/unison-cli/tests/Unison/Test/LSP.hs @@ -11,10 +11,12 @@ import qualified Data.Text as Text import EasyTest import qualified System.IO.Temp as Temp import qualified Unison.ABT as ABT +import Unison.Builtin.Decls (unitRef) import qualified Unison.Cli.TypeCheck as Typecheck import Unison.Codebase (Codebase) import qualified Unison.Codebase.Init as Codebase.Init import qualified Unison.Codebase.SqliteCodebase as SC +import Unison.ConstructorReference (GConstructorReference (..)) import qualified Unison.LSP.Queries as LSPQ import qualified Unison.Lexer.Pos as Lexer import Unison.Parser.Ann (Ann (..)) @@ -138,11 +140,11 @@ term = let ( "Test annotations within pattern binds", [here| term = let - (third, tr^ue) = (false, true) + (third, (^)) = (false, ()) true |], True, - pat (Pattern.Boolean () True) + pat (Pattern.Constructor () (ConstructorReference unitRef 0) []) ), ( "Test annotations for types with arrows", [here| From ecfc8b84527fa875a851d914efaf8291a3e2be98 Mon Sep 17 00:00:00 2001 From: Travis Staton Date: Tue, 28 Feb 2023 10:23:29 -0500 Subject: [PATCH 38/54] complete patterns in prettyprint round trip tests --- unison-src/transcripts-round-trip/main.md | 13 +- .../transcripts-round-trip/main.output.md | 189 +++++++++--------- 2 files changed, 109 insertions(+), 93 deletions(-) diff --git a/unison-src/transcripts-round-trip/main.md b/unison-src/transcripts-round-trip/main.md index 26f5ab918..17ec97087 100644 --- a/unison-src/transcripts-round-trip/main.md +++ b/unison-src/transcripts-round-trip/main.md @@ -84,17 +84,20 @@ f x = let Regression test for https://github.com/unisonweb/unison/issues/2224 ```unison:hide -f : [a] -> a +f : [()] -> () f xs = match xs with x +: (x' +: rest) -> x + _ -> () -g : [a] -> a +g : [()] -> () g xs = match xs with - (rest :+ x') :+ x -> x + (rest :+ x') :+ x -> () + _ -> () -h : [[a]] -> a +h : [[()]] -> () h xs = match xs with (rest :+ (rest' :+ x)) -> x + _ -> () ``` ```ucm @@ -301,6 +304,7 @@ broken tvar = ```unison:hide broken = cases Some loooooooooooooooooooooooooooooooooooooooooooooooooooooooong | loooooooooooooooooooooooooooooooooooooooooooooooooooooooong == 1 -> () + _ -> () ``` ``` ucm @@ -325,6 +329,7 @@ foo = let lijaefliejalfijelfj == aefilaeifhlei -> 0 SomethingUnusuallyLong lijaefliejalfijelfj aefilaeifhlei liaehjffeafijij | lijaefliejalfijelfj == liaehjffeafijij -> 1 + _ -> 2 go (SomethingUnusuallyLong "one" "two" "three") ``` diff --git a/unison-src/transcripts-round-trip/main.output.md b/unison-src/transcripts-round-trip/main.output.md index 9f8099478..51fa395e3 100644 --- a/unison-src/transcripts-round-trip/main.output.md +++ b/unison-src/transcripts-round-trip/main.output.md @@ -34,17 +34,17 @@ x = 1 + 1 most recent, along with the command that got us there. Try: `fork 2 .old` - `fork #l7cnk7raag .old` to make an old namespace + `fork #c5i2vql0hi .old` to make an old namespace accessible again, - `reset-root #l7cnk7raag` to reset the root namespace and + `reset-root #c5i2vql0hi` to reset the root namespace and its history to that of the specified namespace. - When Root Hash Action - 1. now #pdrl1ktsa0 add - 2. 1 secs ago #l7cnk7raag builtins.mergeio - 3. #sg60bvjo91 history starts here + When Root Hash Action + 1. now #88srvru2o0 add + 2. now #c5i2vql0hi builtins.mergeio + 3. #sg60bvjo91 history starts here Tip: Use `diff.namespace 1 7` to compare namespaces between two points in history. @@ -120,19 +120,19 @@ Without the above stanza, the `edit` will send the definition to the most recent most recent, along with the command that got us there. Try: `fork 2 .old` - `fork #l7cnk7raag .old` to make an old namespace + `fork #c5i2vql0hi .old` to make an old namespace accessible again, - `reset-root #l7cnk7raag` to reset the root namespace and + `reset-root #c5i2vql0hi` to reset the root namespace and its history to that of the specified namespace. - When Root Hash Action - 1. now #7a6vnmv5c9 add - 2. now #l7cnk7raag reset-root #l7cnk7raag - 3. now #pdrl1ktsa0 add - 4. 1 secs ago #l7cnk7raag builtins.mergeio - 5. #sg60bvjo91 history starts here + When Root Hash Action + 1. now #a16i2glj04 add + 2. now #c5i2vql0hi reset-root #c5i2vql0hi + 3. now #88srvru2o0 add + 4. now #c5i2vql0hi builtins.mergeio + 5. #sg60bvjo91 history starts here Tip: Use `diff.namespace 1 7` to compare namespaces between two points in history. @@ -199,21 +199,21 @@ f x = let most recent, along with the command that got us there. Try: `fork 2 .old` - `fork #l7cnk7raag .old` to make an old namespace + `fork #c5i2vql0hi .old` to make an old namespace accessible again, - `reset-root #l7cnk7raag` to reset the root namespace and + `reset-root #c5i2vql0hi` to reset the root namespace and its history to that of the specified namespace. - When Root Hash Action - 1. now #obak7jnhcv add - 2. now #l7cnk7raag reset-root #l7cnk7raag - 3. now #7a6vnmv5c9 add - 4. now #l7cnk7raag reset-root #l7cnk7raag - 5. now #pdrl1ktsa0 add - 6. 1 secs ago #l7cnk7raag builtins.mergeio - 7. #sg60bvjo91 history starts here + When Root Hash Action + 1. now #8pc9a0uci4 add + 2. now #c5i2vql0hi reset-root #c5i2vql0hi + 3. now #a16i2glj04 add + 4. now #c5i2vql0hi reset-root #c5i2vql0hi + 5. now #88srvru2o0 add + 6. now #c5i2vql0hi builtins.mergeio + 7. #sg60bvjo91 history starts here Tip: Use `diff.namespace 1 7` to compare namespaces between two points in history. @@ -241,17 +241,20 @@ f x = let Regression test for https://github.com/unisonweb/unison/issues/2224 ```unison -f : [a] -> a +f : [()] -> () f xs = match xs with x +: (x' +: rest) -> x + _ -> () -g : [a] -> a +g : [()] -> () g xs = match xs with - (rest :+ x') :+ x -> x + (rest :+ x') :+ x -> () + _ -> () -h : [[a]] -> a +h : [[()]] -> () h xs = match xs with (rest :+ (rest' :+ x)) -> x + _ -> () ``` ```ucm @@ -259,22 +262,26 @@ h xs = match xs with ⍟ I've added these definitions: - f : [a] -> a - g : [a] -> a - h : [[a]] -> a + f : [()] -> () + g : [()] -> () + h : [[()]] -> () .> edit f g ☝️ I added these definitions to the top of - /Users/runar/work/unison/scratch.u + /home/traveler/code/haskell/unison/pattern-match-coverage/scratch.u - f : [a] -> a - f = cases x +: (x' +: rest) -> x + f : [()] -> () + f = cases + x +: (x' +: rest) -> x + _ -> () - g : [a] -> a - g = cases rest :+ x' :+ x -> x + g : [()] -> () + g = cases + rest :+ x' :+ x -> () + _ -> () You can edit them there, then do `update` to replace the definitions currently in this namespace. @@ -285,23 +292,23 @@ h xs = match xs with most recent, along with the command that got us there. Try: `fork 2 .old` - `fork #l7cnk7raag .old` to make an old namespace + `fork #c5i2vql0hi .old` to make an old namespace accessible again, - `reset-root #l7cnk7raag` to reset the root namespace and + `reset-root #c5i2vql0hi` to reset the root namespace and its history to that of the specified namespace. - When Root Hash Action - 1. now #4skv4f38cf add - 2. now #l7cnk7raag reset-root #l7cnk7raag - 3. now #obak7jnhcv add - 4. now #l7cnk7raag reset-root #l7cnk7raag - 5. now #7a6vnmv5c9 add - 6. now #l7cnk7raag reset-root #l7cnk7raag - 7. now #pdrl1ktsa0 add - 8. 1 secs ago #l7cnk7raag builtins.mergeio - 9. #sg60bvjo91 history starts here + When Root Hash Action + 1. now #psi40d6du2 add + 2. now #c5i2vql0hi reset-root #c5i2vql0hi + 3. now #8pc9a0uci4 add + 4. now #c5i2vql0hi reset-root #c5i2vql0hi + 5. now #a16i2glj04 add + 6. now #c5i2vql0hi reset-root #c5i2vql0hi + 7. now #88srvru2o0 add + 8. now #c5i2vql0hi builtins.mergeio + 9. #sg60bvjo91 history starts here Tip: Use `diff.namespace 1 7` to compare namespaces between two points in history. @@ -320,8 +327,8 @@ h xs = match xs with ⍟ These new definitions are ok to `add`: - f : [a] -> a - g : [a] -> a + f : [()] -> () + g : [()] -> () ``` ## Type application inserts necessary parens @@ -350,7 +357,7 @@ foo n _ = n ☝️ I added these definitions to the top of - /Users/runar/work/unison/scratch.u + /home/traveler/code/haskell/unison/pattern-match-coverage/scratch.u unique type Foo x y = @@ -369,25 +376,25 @@ foo n _ = n most recent, along with the command that got us there. Try: `fork 2 .old` - `fork #l7cnk7raag .old` to make an old namespace + `fork #c5i2vql0hi .old` to make an old namespace accessible again, - `reset-root #l7cnk7raag` to reset the root namespace and + `reset-root #c5i2vql0hi` to reset the root namespace and its history to that of the specified namespace. - When Root Hash Action - 1. now #fdnrhfkoot add - 2. now #l7cnk7raag reset-root #l7cnk7raag - 3. now #4skv4f38cf add - 4. now #l7cnk7raag reset-root #l7cnk7raag - 5. now #obak7jnhcv add - 6. now #l7cnk7raag reset-root #l7cnk7raag - 7. now #7a6vnmv5c9 add - 8. now #l7cnk7raag reset-root #l7cnk7raag - 9. now #pdrl1ktsa0 add - 10. 1 secs ago #l7cnk7raag builtins.mergeio - 11. #sg60bvjo91 history starts here + When Root Hash Action + 1. now #9i8g6b1m8k add + 2. now #c5i2vql0hi reset-root #c5i2vql0hi + 3. now #psi40d6du2 add + 4. now #c5i2vql0hi reset-root #c5i2vql0hi + 5. now #8pc9a0uci4 add + 6. now #c5i2vql0hi reset-root #c5i2vql0hi + 7. now #a16i2glj04 add + 8. now #c5i2vql0hi reset-root #c5i2vql0hi + 9. now #88srvru2o0 add + 10. now #c5i2vql0hi builtins.mergeio + 11. #sg60bvjo91 history starts here Tip: Use `diff.namespace 1 7` to compare namespaces between two points in history. @@ -452,27 +459,27 @@ foo = most recent, along with the command that got us there. Try: `fork 2 .old` - `fork #l7cnk7raag .old` to make an old namespace + `fork #c5i2vql0hi .old` to make an old namespace accessible again, - `reset-root #l7cnk7raag` to reset the root namespace and + `reset-root #c5i2vql0hi` to reset the root namespace and its history to that of the specified namespace. - When Root Hash Action - 1. now #dblf9f7ggq add - 2. now #l7cnk7raag reset-root #l7cnk7raag - 3. now #fdnrhfkoot add - 4. now #l7cnk7raag reset-root #l7cnk7raag - 5. now #4skv4f38cf add - 6. now #l7cnk7raag reset-root #l7cnk7raag - 7. now #obak7jnhcv add - 8. now #l7cnk7raag reset-root #l7cnk7raag - 9. now #7a6vnmv5c9 add - 10. now #l7cnk7raag reset-root #l7cnk7raag - 11. now #pdrl1ktsa0 add - 12. 1 secs ago #l7cnk7raag builtins.mergeio - 13. #sg60bvjo91 history starts here + When Root Hash Action + 1. now #mqg8tqk7i6 add + 2. now #c5i2vql0hi reset-root #c5i2vql0hi + 3. now #9i8g6b1m8k add + 4. now #c5i2vql0hi reset-root #c5i2vql0hi + 5. now #psi40d6du2 add + 6. now #c5i2vql0hi reset-root #c5i2vql0hi + 7. now #8pc9a0uci4 add + 8. now #c5i2vql0hi reset-root #c5i2vql0hi + 9. now #a16i2glj04 add + 10. now #c5i2vql0hi reset-root #c5i2vql0hi + 11. now #88srvru2o0 add + 12. now #c5i2vql0hi builtins.mergeio + 13. #sg60bvjo91 history starts here Tip: Use `diff.namespace 1 7` to compare namespaces between two points in history. @@ -875,7 +882,7 @@ broken tvar = (cases Some _ -> "oh boy isn't this a very very very very very very very long string?" - None -> "")) + None -> "")) tvarmodify : tvar -> fun -> () tvarmodify tvar fun = () @@ -909,6 +916,7 @@ broken tvar = ```unison broken = cases Some loooooooooooooooooooooooooooooooooooooooooooooooooooooooong | loooooooooooooooooooooooooooooooooooooooooooooooooooooooong == 1 -> () + _ -> () ``` ```ucm @@ -928,9 +936,10 @@ broken = cases broken : Optional Nat -> () broken = cases Some - loooooooooooooooooooooooooooooooooooooooooooooooooooooooong | loooooooooooooooooooooooooooooooooooooooooooooooooooooooong - == 1 -> + loooooooooooooooooooooooooooooooooooooooooooooooooooooooong| loooooooooooooooooooooooooooooooooooooooooooooooooooooooong + == 1 -> () + _ -> () You can edit them there, then do `update` to replace the definitions currently in this namespace. @@ -968,6 +977,7 @@ foo = let lijaefliejalfijelfj == aefilaeifhlei -> 0 SomethingUnusuallyLong lijaefliejalfijelfj aefilaeifhlei liaehjffeafijij | lijaefliejalfijelfj == liaehjffeafijij -> 1 + _ -> 2 go (SomethingUnusuallyLong "one" "two" "three") ``` @@ -994,9 +1004,10 @@ foo = let go x = '(match (a -> a) x with SomethingUnusuallyLong - lijaefliejalfijelfj aefilaeifhlei liaehjffeafijij - | lijaefliejalfijelfj == aefilaeifhlei -> 0 - | lijaefliejalfijelfj == liaehjffeafijij -> 1) + lijaefliejalfijelfj aefilaeifhlei liaehjffeafijij + | lijaefliejalfijelfj == aefilaeifhlei -> 0 + | lijaefliejalfijelfj == liaehjffeafijij -> 1 + _ -> 2) go (SomethingUnusuallyLong "one" "two" "three") You can edit them there, then do `update` to replace the @@ -1375,7 +1386,7 @@ afun x f = f x roundtripLastLam = afun "foo" (n -> let - 1 + 1 + _ = 1 + 1 3 ) ``` @@ -1402,7 +1413,7 @@ roundtripLastLam = roundtripLastLam : Nat roundtripLastLam = afun "foo" do - 1 + 1 + _ = 1 + 1 3 You can edit them there, then do `update` to replace the From e80e87f755ab895985e348c9ac2c185324d67317 Mon Sep 17 00:00:00 2001 From: Travis Staton Date: Tue, 28 Feb 2023 16:15:52 -0500 Subject: [PATCH 39/54] documentation --- .../src/Unison/PatternMatchCoverage.hs | 45 +++++++++++++++++-- .../NormalizedConstraints.hs | 10 ++--- 2 files changed, 46 insertions(+), 9 deletions(-) diff --git a/parser-typechecker/src/Unison/PatternMatchCoverage.hs b/parser-typechecker/src/Unison/PatternMatchCoverage.hs index 3ef3c8a94..d3fc4a530 100644 --- a/parser-typechecker/src/Unison/PatternMatchCoverage.hs +++ b/parser-typechecker/src/Unison/PatternMatchCoverage.hs @@ -1,7 +1,39 @@ --- Pattern match coverage checking following the algorithm described --- in "Lower Your Guards". --- https://simon.peytonjones.org/assets/pdfs/lower-your-guards.pdf -module Unison.PatternMatchCoverage where +-- | 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@ nodes with [refinement types]("Unison.PatternMatchCoverage.NormalizedConstraints") +-- representing values that match this node. 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 representing 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'. Step (4) is +-- implemented by 'expandSolution'. +module Unison.PatternMatchCoverage + ( checkMatch, + ) +where import qualified Data.Set as Set import Debug.Trace @@ -16,12 +48,17 @@ import qualified Unison.Term as Term import qualified Unison.Type as Type import qualified Unison.Util.Pretty as P +-- | Perform pattern match coverage checking on a match expression 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 v0 <- fresh diff --git a/parser-typechecker/src/Unison/PatternMatchCoverage/NormalizedConstraints.hs b/parser-typechecker/src/Unison/PatternMatchCoverage/NormalizedConstraints.hs index 44a6fabaa..50ef55483 100644 --- a/parser-typechecker/src/Unison/PatternMatchCoverage/NormalizedConstraints.hs +++ b/parser-typechecker/src/Unison/PatternMatchCoverage/NormalizedConstraints.hs @@ -32,11 +32,11 @@ import Unison.Var (Var) -- * Mutual compatibility: No two constraints should conflict with -- each other. -- --- * Inhabitation: There must be at least one value that inhabits --- each refinement type. (N.B. We only do a best effort enforcement of --- this invariant, see 'inhabited' in --- Unison.PatternMatchCoverage.NormalizedConstraints.Solve for --- additional info) +-- * Inhabitation: There must be at least one value that inhabits each +-- refinement type. (N.B. We don't truly know if a type is inhabited, +-- see 'inhabited' in "Unison.PatternMatchCoverage.Solve" for +-- details. However, the refinement type is inhabited as far as our +-- inhabitation checker is concerned.) -- -- These invariants ensure that each term in our DNF has at least one -- solution, and it is easy to expand and print these solutions. From 1ab327e01bae6adb403f0e588b418a78a83e5177 Mon Sep 17 00:00:00 2001 From: Travis Staton Date: Wed, 1 Mar 2023 10:28:44 -0500 Subject: [PATCH 40/54] document GrdTree --- .../Unison/PatternMatchCoverage/GrdTree.hs | 49 +++++++++++++++++-- 1 file changed, 45 insertions(+), 4 deletions(-) diff --git a/parser-typechecker/src/Unison/PatternMatchCoverage/GrdTree.hs b/parser-typechecker/src/Unison/PatternMatchCoverage/GrdTree.hs index e11a5b842..681382f5d 100644 --- a/parser-typechecker/src/Unison/PatternMatchCoverage/GrdTree.hs +++ b/parser-typechecker/src/Unison/PatternMatchCoverage/GrdTree.hs @@ -1,6 +1,14 @@ {-# LANGUAGE OverloadedStrings #-} -module Unison.PatternMatchCoverage.GrdTree where +module Unison.PatternMatchCoverage.GrdTree + ( GrdTree, + GrdTreeF (..), + pattern Leaf, + pattern Grd, + pattern Fork, + prettyGrdTree, + ) +where import Data.List.NonEmpty (NonEmpty (..)) import qualified Data.List.NonEmpty as NEL @@ -9,12 +17,45 @@ import Unison.PatternMatchCoverage.Fix import Unison.Prelude import Unison.Util.Pretty +-- | A @GrdTree@ is the simple language to desugar matches into. All +-- pattern matching constructs (/e.g./ structural pattern matching, +-- boolean guards, pattern guards, view patterns, etc) are desugared +-- into this simpler structure. +-- +-- It is parameterized by the values at guard nodes, @n@, and the +-- values at the leaves, @l@. When desugaring, @n@ is +-- 'Unison.PatternMatchCoverage.PmGrd.PmGrd' and @l@ is the source +-- location. After annotating the @GrdTree@, @n@ is a refinement type +-- representing matching values and the @l@ is pairs of the +-- aforementioned refinement type and source location. +-- +-- For example: +-- +-- @ +-- example : Optional Nat -> Nat +-- example = cases +-- None -> 0 +-- Some x +-- | isEven x -> 0 +-- | otherwise -> 1 +-- @ +-- +-- is desugared into +-- +-- @ +-- ──┬─ None <- v0 ── srcloc +-- ├─ Some ( v1 :: ##Nat ) <- v0 ── let v2 = isEven v1 ── True <- v2 ── srcloc +-- └─ Some ( v3 :: ##Nat ) <- v0 ── srcloc +-- @ type GrdTree n l = Fix (GrdTreeF n l) data GrdTreeF n l a - = LeafF l - | GrdF n a - | ForkF (NonEmpty a) + = -- | A successful match + LeafF l + | -- | 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) 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 From d9eeea9012afd85b9b9e8e2207dd198ca3a0d4d5 Mon Sep 17 00:00:00 2001 From: Travis Staton Date: Wed, 1 Mar 2023 14:53:57 -0500 Subject: [PATCH 41/54] documentation and cleanup --- .../src/Unison/PatternMatchCoverage.hs | 14 +-- .../src/Unison/PatternMatchCoverage/Class.hs | 14 ++- .../Unison/PatternMatchCoverage/Constraint.hs | 40 +++++-- .../Unison/PatternMatchCoverage/Desugar.hs | 26 +++-- .../Unison/PatternMatchCoverage/Literal.hs | 44 ++++++-- .../NormalizedConstraints.hs | 39 ++++++- .../src/Unison/PatternMatchCoverage/Solve.hs | 103 ++++-------------- .../src/Unison/PatternMatchCoverage/UFMap.hs | 23 ++-- 8 files changed, 165 insertions(+), 138 deletions(-) diff --git a/parser-typechecker/src/Unison/PatternMatchCoverage.hs b/parser-typechecker/src/Unison/PatternMatchCoverage.hs index d3fc4a530..a43bc0e38 100644 --- a/parser-typechecker/src/Unison/PatternMatchCoverage.hs +++ b/parser-typechecker/src/Unison/PatternMatchCoverage.hs @@ -19,17 +19,17 @@ -- == High-level algorithm overview -- -- 1. [Desugar]("Unison.PatternMatchCoverage.Desugar") a match expression into a 'Unison.PatternMatchCoverage.GrdTree.GrdTree'. --- 2. Annotate the @GrdTree@ nodes with [refinement types]("Unison.PatternMatchCoverage.NormalizedConstraints") --- representing values that match this node. Redundant and inaccessible patterns are then identified by @GrdTree@ leaves +-- 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 representing uncovered values. If the resulting refinement type +-- 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'. Step (4) is --- implemented by 'expandSolution'. +-- implemented as a single traversal: 'uncoverAnnotate'/'classify'. Step (4) is +-- implemented by 'expandSolution'/'generateInhabitants'. module Unison.PatternMatchCoverage ( checkMatch, ) @@ -43,7 +43,7 @@ import Unison.PatternMatchCoverage.Desugar (desugarMatch) import Unison.PatternMatchCoverage.GrdTree (prettyGrdTree) import qualified Unison.PatternMatchCoverage.NormalizedConstraints as NC import Unison.PatternMatchCoverage.PmGrd (prettyPmGrd) -import Unison.PatternMatchCoverage.Solve (classify, expand, expandSolution, uncoverAnnotate) +import Unison.PatternMatchCoverage.Solve (classify, expandSolution, generateInhabitants, uncoverAnnotate) import qualified Unison.Term as Term import qualified Unison.Type as Type import qualified Unison.Util.Pretty as P @@ -65,7 +65,7 @@ checkMatch matchLocation scrutineeType cases = do grdtree0 <- desugarMatch matchLocation scrutineeType v0 cases (uncovered, grdtree1) <- uncoverAnnotate (Set.singleton (NC.declVar v0 scrutineeType id NC.emptyNormalizedConstraints)) grdtree0 uncoveredExpanded <- concat . fmap Set.toList <$> traverse (expandSolution v0) (Set.toList uncovered) - let sols = map (expand v0) uncoveredExpanded + let sols = map (generateInhabitants v0) uncoveredExpanded let (_accessible, inaccessible, redundant) = classify grdtree1 let debugOutput = P.sep diff --git a/parser-typechecker/src/Unison/PatternMatchCoverage/Class.hs b/parser-typechecker/src/Unison/PatternMatchCoverage/Class.hs index 30f5407f4..55647a570 100644 --- a/parser-typechecker/src/Unison/PatternMatchCoverage/Class.hs +++ b/parser-typechecker/src/Unison/PatternMatchCoverage/Class.hs @@ -1,6 +1,11 @@ {-# LANGUAGE FunctionalDependencies #-} -module Unison.PatternMatchCoverage.Class where +module Unison.PatternMatchCoverage.Class + ( Pmc (..), + EnumeratedConstructors (..), + traverseConstructors, + ) +where import Control.Monad.Fix (MonadFix) import Unison.ConstructorReference (ConstructorReference) @@ -8,9 +13,16 @@ import Unison.PatternMatchCoverage.ListPat (ListPat) import Unison.Type (Type) import Unison.Var (Var) +-- | A typeclass for the queries required to perform pattern match +-- coverage checking. class (Ord loc, Var vt, Var v, MonadFix m) => Pmc vt v loc m | m -> vt v loc where + -- | Get the constructors of a type getConstructors :: Type vt loc -> m (EnumeratedConstructors vt v loc) + + -- | Get the types of the arguments of a specific constructor getConstructorVarTypes :: Type vt loc -> ConstructorReference -> m [Type vt loc] + + -- | Get a fresh variable fresh :: m v data EnumeratedConstructors vt v loc diff --git a/parser-typechecker/src/Unison/PatternMatchCoverage/Constraint.hs b/parser-typechecker/src/Unison/PatternMatchCoverage/Constraint.hs index 034d5cf75..70bc4613d 100644 --- a/parser-typechecker/src/Unison/PatternMatchCoverage/Constraint.hs +++ b/parser-typechecker/src/Unison/PatternMatchCoverage/Constraint.hs @@ -1,4 +1,8 @@ -module Unison.PatternMatchCoverage.Constraint where +module Unison.PatternMatchCoverage.Constraint + ( Constraint (..), + prettyConstraint, + ) +where import Unison.ConstructorReference (ConstructorReference) import Unison.PatternMatchCoverage.IntervalSet (IntervalSet) @@ -9,28 +13,44 @@ import Unison.Type (Type) import Unison.Util.Pretty import Unison.Var (Var) +-- | A constraint to add to a [normalized constraint +-- set]("Unison.PatternMatchCoverage.NormalizedConstraints") (fig 6) +-- See 'Unison.PatternMatchCoverage.Solve.addConstraint' data Constraint vt v loc - = PosCon v ConstructorReference [(v, Type vt loc)] - | NegCon v ConstructorReference - | PosLit v PmLit - | NegLit v PmLit - | PosListHead + = -- | Positive constraint regarding data type. States that the + -- given variable must be the given constructor, and it also binds + -- variables corresponding to constructor arguments. + PosCon v ConstructorReference [(v, Type vt loc)] + | -- | Negative constraint concerning data type. States that the + -- given variable must not be the given constructor. + NegCon v ConstructorReference + | -- | Positive constraint regarding literal + PosLit v PmLit + | -- | Negative constraint regarding literal + NegLit v PmLit + | -- | Positive constraint on list element with position relative to head of list + PosListHead v -- ^ list root Int -- ^ cons position (0 is head) v -- ^ element variable - | PosListTail + | -- | Positive constraint on list element with position relative to end of list + PosListTail v -- ^ list root Int -- ^ snoc position (0 is last) v -- ^ element variable - | NegListInterval v IntervalSet - | Effectful v - | Eq v v + | -- | Negative constraint on length of the list (/i.e./ the list + -- may not be an element of the interval set) + NegListInterval v IntervalSet + | -- | An effect is performed + Effectful v + | -- | Equality constraint + Eq v v deriving stock (Eq, Ord) prettyConstraint :: (Var vt, Var v) => Constraint vt v loc -> Pretty ColorText diff --git a/parser-typechecker/src/Unison/PatternMatchCoverage/Desugar.hs b/parser-typechecker/src/Unison/PatternMatchCoverage/Desugar.hs index d60ef92c8..5a3741f14 100644 --- a/parser-typechecker/src/Unison/PatternMatchCoverage/Desugar.hs +++ b/parser-typechecker/src/Unison/PatternMatchCoverage/Desugar.hs @@ -1,6 +1,8 @@ -module Unison.PatternMatchCoverage.Desugar where +module Unison.PatternMatchCoverage.Desugar + ( desugarMatch, + ) +where -import Data.Functor.Compose import Data.List.NonEmpty (NonEmpty (..)) import qualified U.Core.ABT as ABT import Unison.Pattern @@ -14,13 +16,17 @@ import Unison.Term (MatchCase (..), Term', app, var) import Unison.Type (Type) import qualified Unison.Type as Type +-- | Desugar a match into a 'GrdTree' 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)] -> m (GrdTree (PmGrd vt v loc) loc) desugarMatch loc0 scrutineeType v0 cs0 = @@ -124,9 +130,9 @@ listToGrdTree _listTyp elemTyp listVar nl0 k0 vs0 = ($ 0) . cata \case N'ConsF _ b -> \acc -> b $! acc + 1 N'SnocF b _ -> \acc -> b $! acc + 1 - N'NilF -> \n -> (n, n) - N'VarF _ -> \n -> (n, maxBound) - N'UnboundF _ -> \n -> (n, maxBound) + N'NilF -> \ !n -> (n, n) + N'VarF _ -> \ !n -> (n, maxBound) + N'UnboundF _ -> \ !n -> (n, maxBound) data NormalizedListF loc a = N'ConsF (Pattern loc) a @@ -138,19 +144,19 @@ data NormalizedListF loc a type NormalizedList loc = Fix (NormalizedListF loc) -type AnnotatedList loc = Fix (Compose ((,) (Int, Int)) (NormalizedListF loc)) - -pattern Ann :: Int -> Int -> NormalizedListF loc (AnnotatedList loc) -> AnnotatedList loc -pattern Ann lb ub rest = Fix (Compose ((lb, ub), rest)) - +pattern N'Cons :: Pattern loc -> Fix (NormalizedListF loc) -> Fix (NormalizedListF loc) pattern N'Cons x xs = Fix (N'ConsF x xs) +pattern N'Snoc :: Fix (NormalizedListF loc) -> Pattern loc -> Fix (NormalizedListF loc) pattern N'Snoc xs x = Fix (N'SnocF xs x) +pattern N'Nil :: Fix (NormalizedListF loc) pattern N'Nil = Fix N'NilF +pattern N'Var :: loc -> Fix (NormalizedListF loc) pattern N'Var x = Fix (N'VarF x) +pattern N'Unbound :: loc -> Fix (NormalizedListF loc) pattern N'Unbound x = Fix (N'UnboundF x) -- | strip out sequence literals and concats diff --git a/parser-typechecker/src/Unison/PatternMatchCoverage/Literal.hs b/parser-typechecker/src/Unison/PatternMatchCoverage/Literal.hs index 7d0f52c54..312ba394b 100644 --- a/parser-typechecker/src/Unison/PatternMatchCoverage/Literal.hs +++ b/parser-typechecker/src/Unison/PatternMatchCoverage/Literal.hs @@ -1,4 +1,8 @@ -module Unison.PatternMatchCoverage.Literal where +module Unison.PatternMatchCoverage.Literal + ( Literal (..), + prettyLiteral, + ) +where import Unison.ConstructorReference (ConstructorReference) import Unison.PatternMatchCoverage.IntervalSet (IntervalSet) @@ -12,14 +16,25 @@ import Unison.Typechecker.TypeVar (TypeVar, lowerTerm) import Unison.Util.Pretty import Unison.Var (Var) +-- | Refinement type literals (fig 3) data Literal vt v loc - = T - | F - | PosCon v ConstructorReference [(v, Type vt loc)] - | NegCon v ConstructorReference - | PosLit v PmLit - | NegLit v PmLit - | PosListHead + = -- | True + T + | -- | False + F + | -- | Positive constraint regarding data type. States that the + -- given variable must be the given constructor, and it also binds + -- variables corresponding to constructor arguments. + PosCon v ConstructorReference [(v, Type vt loc)] + | -- | Negative constraint concerning data type. States that the + -- given variable must not be the given constructor. + NegCon v ConstructorReference + | -- | Positive constraint regarding literal + PosLit v PmLit + | -- | Negative constraint regarding literal + NegLit v PmLit + | -- | Positive constraint on list element with position relative to head of list + PosListHead v -- ^ list root Int @@ -27,7 +42,8 @@ data Literal vt v loc v -- ^ element variable (Type vt loc) - | PosListTail + | -- | Positive constraint on list element with position relative to end of list + PosListTail v -- ^ list root Int @@ -35,9 +51,13 @@ data Literal vt v loc v -- ^ element variable (Type vt loc) - | NegListInterval v IntervalSet - | Effectful v - | Let v (Term' vt v loc) (Type vt loc) + | -- | Negative constraint on length of the list (/i.e./ the list + -- may not be an element of the interval set) + NegListInterval v IntervalSet + | -- | An effect is performed + Effectful v + | -- | Introduce a binding for a term + Let v (Term' vt v loc) (Type vt loc) deriving stock (Show) prettyLiteral :: (Var v) => Literal (TypeVar b v) v loc -> Pretty ColorText diff --git a/parser-typechecker/src/Unison/PatternMatchCoverage/NormalizedConstraints.hs b/parser-typechecker/src/Unison/PatternMatchCoverage/NormalizedConstraints.hs index 50ef55483..97740b417 100644 --- a/parser-typechecker/src/Unison/PatternMatchCoverage/NormalizedConstraints.hs +++ b/parser-typechecker/src/Unison/PatternMatchCoverage/NormalizedConstraints.hs @@ -1,4 +1,18 @@ -module Unison.PatternMatchCoverage.NormalizedConstraints where +module Unison.PatternMatchCoverage.NormalizedConstraints + ( NormalizedConstraints (..), + VarInfo (..), + VarConstraints (..), + EffectInfo (..), + markDirty, + emptyNormalizedConstraints, + updateF, + ConstraintUpdate (..), + expectCanon, + declVar, + prettyNormalizedConstraints, + prettyDnf, + ) +where import Data.Functor.Compose import Data.List (intersperse) @@ -58,9 +72,6 @@ markDirty :: markDirty k nc@NormalizedConstraints {dirtySet} = nc {dirtySet = Set.insert k dirtySet} -dom :: NormalizedConstraints vt v loc -> [v] -dom NormalizedConstraints {constraintMap} = UFMap.keys constraintMap - emptyNormalizedConstraints :: (Ord v) => NormalizedConstraints vt v loc emptyNormalizedConstraints = NormalizedConstraints @@ -68,6 +79,8 @@ emptyNormalizedConstraints = dirtySet = mempty } +-- | Lookup the canonical value of @v@ from the constraint map. Throws +-- an error if the variable is not in the map. expectCanon :: forall vt v loc. (Var v) => @@ -110,11 +123,16 @@ alterF v nothing just nc = Update x -> (markDirty v, Just x) {-# INLINE alterF #-} +-- | Generic function to lookup or alter constraints in the constraint +-- map. Throws an error if the variable is not in the map. updateF :: forall vt v loc f. (Var v, Functor f) => + -- | variable to lookup v -> + -- | update function (v -> VarInfo vt v loc -> f (ConstraintUpdate (VarInfo vt v loc))) -> + -- | constraint map NormalizedConstraints vt v loc -> f (NormalizedConstraints vt v loc) updateF v just nc = @@ -127,12 +145,18 @@ data ConstraintUpdate a | Ignore deriving stock (Functor) +-- | Install a new variable into the constraint map. Throws an error +-- if the variable already exists in the map. declVar :: forall vt v loc. (Var v) => + -- | new variable to install v -> + -- | type of variable Type vt loc -> + -- | modifier for the default var info of the given type (VarInfo vt v loc -> VarInfo vt v loc) -> + -- | Normalized constraints to install the variable into NormalizedConstraints vt v loc -> NormalizedConstraints vt v loc declVar v t f nc@NormalizedConstraints {constraintMap} = @@ -164,6 +188,7 @@ mkVarInfo v t = vi_eff = IsNotEffectful } +-- | Normalized constraints on a specific variable data VarInfo vt v loc = VarInfo { vi_id :: v, vi_typ :: Type vt loc, @@ -172,6 +197,9 @@ data VarInfo vt v loc = VarInfo } deriving stock (Show, Eq, Ord, Generic) +-- | The constraints are different for different types, although most +-- of them take the form of an optional positive constraint and a set +-- of negative constraints. data VarConstraints vt v loc = Vc'Constructor (Maybe (ConstructorReference, [(v, Type vt loc)])) @@ -182,8 +210,7 @@ data VarConstraints vt v loc | Vc'Float (Maybe Double) (Set Double) | Vc'Text (Maybe Text) (Set Text) | Vc'Char (Maybe Char) (Set Char) - | -- | Vc'ListElem v (Either Int Int) - Vc'ListRoot + | Vc'ListRoot (Type vt loc) -- ^ type of list elems (Seq v) diff --git a/parser-typechecker/src/Unison/PatternMatchCoverage/Solve.hs b/parser-typechecker/src/Unison/PatternMatchCoverage/Solve.hs index 742d78656..ae6d75853 100644 --- a/parser-typechecker/src/Unison/PatternMatchCoverage/Solve.hs +++ b/parser-typechecker/src/Unison/PatternMatchCoverage/Solve.hs @@ -1,6 +1,12 @@ {-# LANGUAGE DataKinds #-} -module Unison.PatternMatchCoverage.Solve where +module Unison.PatternMatchCoverage.Solve + ( uncoverAnnotate, + classify, + expandSolution, + generateInhabitants, + ) +where import Control.Monad.State import Control.Monad.Trans.Compose @@ -22,7 +28,6 @@ import Unison.PatternMatchCoverage.Fix import Unison.PatternMatchCoverage.GrdTree import Unison.PatternMatchCoverage.IntervalSet (IntervalSet) import qualified Unison.PatternMatchCoverage.IntervalSet as IntervalSet -import Unison.PatternMatchCoverage.ListPat import Unison.PatternMatchCoverage.Literal import Unison.PatternMatchCoverage.NormalizedConstraints import Unison.PatternMatchCoverage.PmGrd @@ -36,8 +41,9 @@ import Unison.Var (Var) -- | top-down traversal of the 'GrdTree' that produces: -- --- * a refinement type for values that do not match the 'GrdTree' --- * a new 'GrdTree' annotated with refinement types at the nodes for +-- * a refinement type describing values that do not match the 'GrdTree' +-- (the "uncovered" set) +-- * a new 'GrdTree' annotated with refinement types at the nodes describing -- values that cause an effect to be performed and values that match -- the case at the leaves. -- @@ -80,13 +86,6 @@ uncoverAnnotate z grdtree0 = cata phi grdtree0 z PmListInterval listVar lb ub -> do let iset = IntervalSet.singleton (lb, ub) handleGrd (NegListInterval listVar (IntervalSet.complement iset)) (NegListInterval listVar iset) k nc0 - -- (ncmatch, t) <- k nc0 - -- ncNoMatch <- addLiteral' nc0 (NegListInterval listVar miset) - -- -- todo: limit size - -- pure (Set.union ncMatch ncNoMatch, t) - -- PmList var listPat mi convars -> - -- let miset = IntervalSet.singleton mi - -- in handleGrd (PosList var listPat miset convars) (NegList var miset) k nc0 PmBang var -> do (ncCont, t) <- k nc0 ncEff <- addLiteral' nc0 (Effectful var) @@ -146,6 +145,8 @@ classifyAlg = \case True -> ([l], [], []) False -> ([], [], [l]) GrdF rt rest -> + -- The presence of a 'GrdF' node indicates that an effect was + -- performed (see 'uncoverAnnotate'). case inh rt of True -> -- The rest of the subtree is redundant, but an effect is @@ -159,21 +160,21 @@ classifyAlg = \case -- inhabitation check inh = not . Set.null --- | Expand a full DNF term (i.e. each term identifies one and only --- one solution) into a pattern. -expand :: +-- | Expand a full DNF term (i.e. each term identifies exactly one +-- solution) into an inhabiting pattern. +generateInhabitants :: forall vt v loc. (Var v) => v -> NormalizedConstraints vt v loc -> Pattern () -expand x nc = +generateInhabitants x nc = let (_xcanon, xvi, nc') = expectCanon x nc in case vi_con xvi of Vc'Constructor pos _neg -> case pos of Nothing -> Pattern.Unbound () Just (dc, convars) -> - Pattern.Constructor () dc (map (\(v, _) -> expand v nc') convars) + Pattern.Constructor () dc (map (\(v, _) -> generateInhabitants v nc') convars) Vc'Boolean pos _neg -> case pos of Nothing -> Pattern.Unbound () Just b -> Pattern.Boolean () b @@ -186,19 +187,11 @@ expand x nc = rootPat = case matchIsIncomplete of True -> Pattern.Unbound () False -> Pattern.SequenceLiteral () [] - snoced = foldr (\a b -> Pattern.SequenceOp () b Pattern.Snoc (expand a nc')) rootPat snocPos - consed = foldr (\a b -> Pattern.SequenceOp () (expand a nc') Pattern.Cons b) snoced consPos + snoced = foldr (\a b -> Pattern.SequenceOp () b Pattern.Snoc (generateInhabitants a nc')) rootPat snocPos + consed = foldr (\a b -> Pattern.SequenceOp () (generateInhabitants a nc') Pattern.Cons b) snoced consPos in consed _ -> Pattern.Unbound () --- | Expand the given variable into inhabited patterns. This is done --- as a final step on the refinement type unmatched terms (see --- 'uncoverAnnotate'). -generateInhabitants :: (Pmc vt v loc m) => v -> Set (NormalizedConstraints vt v loc) -> m [Pattern ()] -generateInhabitants v ncs = do - sols <- concat . fmap toList <$> traverse (expandSolution v) (toList ncs) - pure $ map (expand v) sols - -- | Instantiate a variable to a given constructor. instantiate :: forall vt v loc x m. @@ -345,12 +338,6 @@ withConstructors nil vinfo k = do typ = vi_typ vinfo v = vi_id vinfo -mkMatchingInterval :: ListPat -> IntervalSet -mkMatchingInterval = \case - Cons -> IntervalSet.singleton (1, maxBound) - Snoc -> IntervalSet.singleton (1, maxBound) - Nil -> IntervalSet.singleton (0, 0) - -- | Test that the given variable is inhabited. This test is -- undecidable in general so we adopt a fuel based approach as -- described in section 3.7. @@ -628,20 +615,6 @@ union v0 v1 nc@NormalizedConstraints {constraintMap} = IsEffectful -> [C.Effectful chosenCanon] in addConstraints constraints nc {constraintMap = m} -modifyList :: - forall vt v loc. - (Var v) => - v -> - ( Type vt loc -> - Seq v -> - Seq v -> - IntervalSet -> - ConstraintUpdate (Seq v, Seq v, IntervalSet) - ) -> - NormalizedConstraints vt v loc -> - NormalizedConstraints vt v loc -modifyList v f nc = runIdentity $ modifyListF v (\a b c d -> Identity (f a b c d)) nc - modifyListC :: forall vt v loc m. (Pmc vt v loc m) => @@ -674,18 +647,6 @@ modifyListF v f nc = let g vc = getCompose (posAndNegList (\typ pcons psnoc iset -> Compose (f typ pcons psnoc iset)) vc) in modifyVarConstraints v g nc -modifyConstructor :: - forall vt v loc. - (Var v) => - v -> - ( (Maybe (ConstructorReference, [(v, Type vt loc)])) -> - Set ConstructorReference -> - (ConstraintUpdate (Maybe (ConstructorReference, [(v, Type vt loc)]), Set ConstructorReference)) - ) -> - NormalizedConstraints vt v loc -> - NormalizedConstraints vt v loc -modifyConstructor v f nc = runIdentity $ modifyConstructorF v (\a b -> Identity (f a b)) nc - modifyConstructorC :: forall vt v loc m. (Pmc vt v loc m) => @@ -714,25 +675,6 @@ modifyConstructorF v f nc = let g vc = getCompose (posAndNegConstructor (\pos neg -> Compose (f pos neg)) vc) in modifyVarConstraints v g nc -modifyLiteral :: - forall vt v loc. - (Var v) => - v -> - PmLit -> - ( forall a. - (Ord a) => - -- positive info - Maybe a -> - -- negative info - Set a -> - -- the passed in PmLit, unpacked - a -> - ConstraintUpdate (Maybe a, Set a) - ) -> - NormalizedConstraints vt v loc -> - NormalizedConstraints vt v loc -modifyLiteral v lit f nc = runIdentity $ modifyLiteralF v lit (\a b c -> Identity (f a b c)) nc - modifyLiteralC :: forall vt v loc m. (Pmc vt v loc m) => @@ -868,13 +810,6 @@ newtype C vt v loc m a = C contradiction :: (Applicative m) => C vt v loc m a contradiction = C \_ -> pure Nothing -update :: (Pmc vt v loc m) => v -> VarConstraints vt v loc -> C vt v loc m () -update v vc = do - nc0 <- get - let (var, vi, nc1) = expectCanon v nc0 - nc2 = markDirty var ((insertVarInfo var vi {vi_con = vc}) nc1) - put nc2 - equate :: (Pmc vt v loc m) => [(v, v)] -> C vt v loc m () equate vs = addConstraintsC (map (uncurry C.Eq) vs) diff --git a/parser-typechecker/src/Unison/PatternMatchCoverage/UFMap.hs b/parser-typechecker/src/Unison/PatternMatchCoverage/UFMap.hs index d5d2ca9e4..0fdab0e59 100644 --- a/parser-typechecker/src/Unison/PatternMatchCoverage/UFMap.hs +++ b/parser-typechecker/src/Unison/PatternMatchCoverage/UFMap.hs @@ -28,8 +28,9 @@ import Data.Maybe (fromJust) import Data.Set (Set) import qualified Data.Set as Set --- import Lyg.Pretty - +-- | A union-find structure. Used by +-- 'Unison.PatternMatchCoverage.NormalizedConstraints.NormalizedConstraints' +-- to provide efficient unification. newtype UFMap k v = UFMap (Map k (UFValue k v)) deriving stock (Eq, Ord, Show) @@ -54,16 +55,15 @@ alterF' :: k -> -- | The canonical key (use laziness to supply if unknown) k -> + -- | Return Just to short-circuit the indirection lookup loop (k -> UFMap k v -> Maybe (f (UFMap k v))) -> - -- How to alter the canonical value - -- - -- N.B. deleting keys from a UFMap is not supported - -- - -- | Nothing case f (Maybe v) -> -- | Just case - -- canonicalKey -> size -> value + -- + -- @canonicalKey -> size -> value -> new value@ + -- + -- /N.B./ deleting a value is not supported (k -> Int -> v -> f (UFValue k v)) -> UFMap k v -> -- | Returns the canonical k, the size, the value, and the path @@ -128,10 +128,17 @@ alter :: alter k handleNothing handleJust map0 = runIdentity (alterF k (Identity handleNothing) (\k s v -> Identity (handleJust k s v)) map0) +-- | Lookup the canonical value lookupCanon :: (Ord k) => k -> UFMap k v -> + -- | returns: + -- + -- * the canonical member of the equivalence set + -- * the size of the equivalence set + -- * the associated value + -- * the @UFMap@ after path compression Maybe (k, Int, v, UFMap k v) lookupCanon k m = getCompose (alterF k nothing just m) From 7314d09623835160243811827e0dcd9d9c86a93b Mon Sep 17 00:00:00 2001 From: Travis Staton Date: Wed, 1 Mar 2023 15:28:16 -0500 Subject: [PATCH 42/54] error message tweaks --- parser-typechecker/src/Unison/PrintError.hs | 12 ++--- .../transcripts/pattern-match-coverage.md | 2 +- .../pattern-match-coverage.output.md | 50 +++++++------------ 3 files changed, 23 insertions(+), 41 deletions(-) diff --git a/parser-typechecker/src/Unison/PrintError.hs b/parser-typechecker/src/Unison/PrintError.hs index cc352f778..3e54f177e 100644 --- a/parser-typechecker/src/Unison/PrintError.hs +++ b/parser-typechecker/src/Unison/PrintError.hs @@ -596,9 +596,8 @@ renderTypeError e env src curPath = case e of ] UncoveredPatterns loc tms -> mconcat - [ "Pattern match is non-exhaustive\n", - Pr.hang - "In the match:" + [ Pr.hang + "Pattern match doesn't cover all possible cases:" (annotatedAsErrorSite src loc), "\n\n" ] @@ -608,10 +607,9 @@ renderTypeError e env src curPath = case e of (map (\x -> Pr.lit (renderPattern env x)) (Nel.toList tms)) ) RedundantPattern loc -> - mconcat - [ "Pattern match is redundant\n", - Pr.hang "In the match case:" (annotatedAsErrorSite src loc) - ] + Pr.hang + "This case would be ignored because it's already covered by the preceding case(s):" + (annotatedAsErrorSite src loc) UnknownTerm {..} -> let (correct, wrongTypes, wrongNames) = foldr sep id suggestions ([], [], []) diff --git a/unison-src/transcripts/pattern-match-coverage.md b/unison-src/transcripts/pattern-match-coverage.md index 6034984b8..b6e478256 100644 --- a/unison-src/transcripts/pattern-match-coverage.md +++ b/unison-src/transcripts/pattern-match-coverage.md @@ -24,7 +24,7 @@ test = cases _ -> () ``` -patterns that would imply supplying an uninhabited type are not expected +uninhabited patterns are not expected ```unison unique type V = diff --git a/unison-src/transcripts/pattern-match-coverage.output.md b/unison-src/transcripts/pattern-match-coverage.output.md index c9c5cf96c..34d874134 100644 --- a/unison-src/transcripts/pattern-match-coverage.output.md +++ b/unison-src/transcripts/pattern-match-coverage.output.md @@ -10,8 +10,7 @@ test = cases ```ucm - Pattern match is non-exhaustive - In the match: + Pattern match doesn't cover all possible cases: 4 | test = cases 5 | A -> () @@ -36,13 +35,12 @@ test = cases ```ucm - Pattern match is redundant - In the match case: + This case would be ignored because it's already covered by the preceding case(s): 8 | _ -> () ``` -patterns that would imply supplying an uninhabited type are not expected +uninhabited patterns are not expected ```unison unique type V = @@ -77,8 +75,7 @@ test = cases ```ucm - Pattern match is redundant - In the match case: + This case would be ignored because it's already covered by the preceding case(s): 7 | Some _ -> () @@ -92,8 +89,7 @@ test = cases ```ucm - Pattern match is non-exhaustive - In the match: + Pattern match doesn't cover all possible cases: 2 | test = cases 3 | () | false -> () @@ -115,8 +111,7 @@ test = cases ```ucm - Pattern match is non-exhaustive - In the match: + Pattern match doesn't cover all possible cases: 4 | test = cases 5 | None -> () 6 | Some None -> () @@ -138,8 +133,7 @@ test = cases ```ucm - Pattern match is non-exhaustive - In the match: + Pattern match doesn't cover all possible cases: 4 | test = cases 5 | None -> () 6 | Some None -> () @@ -162,8 +156,7 @@ test = cases ```ucm - Pattern match is non-exhaustive - In the match: + Pattern match doesn't cover all possible cases: 2 | test = cases 3 | 0 -> () @@ -199,8 +192,7 @@ test = cases ```ucm - Pattern match is non-exhaustive - In the match: + Pattern match doesn't cover all possible cases: 2 | test = cases 3 | true -> () @@ -238,8 +230,7 @@ test = cases ```ucm - Pattern match is redundant - In the match case: + This case would be ignored because it's already covered by the preceding case(s): 5 | _ -> () @@ -271,8 +262,7 @@ test = cases ```ucm - Pattern match is non-exhaustive - In the match: + Pattern match doesn't cover all possible cases: 2 | test = cases 3 | [] -> () @@ -289,8 +279,7 @@ test = cases ```ucm - Pattern match is non-exhaustive - In the match: + Pattern match doesn't cover all possible cases: 2 | test = cases 3 | x +: xs -> () @@ -307,8 +296,7 @@ test = cases ```ucm - Pattern match is non-exhaustive - In the match: + Pattern match doesn't cover all possible cases: 2 | test = cases 3 | xs :+ x -> () @@ -346,8 +334,7 @@ test = cases ```ucm - Pattern match is non-exhaustive - In the match: + Pattern match doesn't cover all possible cases: 2 | test = cases 3 | x0 +: (x1 +: xs) -> () 4 | [] -> () @@ -366,8 +353,7 @@ test = cases ```ucm - Pattern match is non-exhaustive - In the match: + Pattern match doesn't cover all possible cases: 2 | test = cases 3 | [] -> () 4 | x0 +: [] -> () @@ -411,8 +397,7 @@ test = cases ```ucm - Pattern match is redundant - In the match case: + This case would be ignored because it's already covered by the preceding case(s): 6 | true +: xs -> () @@ -428,8 +413,7 @@ test = cases ```ucm - Pattern match is redundant - In the match case: + This case would be ignored because it's already covered by the preceding case(s): 5 | _ ++ [true, false, true, false] -> () From a3e760f6674176da88963330218d5e9e790ad735 Mon Sep 17 00:00:00 2001 From: Chris Penner Date: Wed, 1 Mar 2023 16:46:06 -0600 Subject: [PATCH 43/54] Add diagnostic ranges for pattern match errors in LSP --- unison-cli/src/Unison/LSP/FileAnalysis.hs | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/unison-cli/src/Unison/LSP/FileAnalysis.hs b/unison-cli/src/Unison/LSP/FileAnalysis.hs index 7b264d3c1..18b58bfc7 100644 --- a/unison-cli/src/Unison/LSP/FileAnalysis.hs +++ b/unison-cli/src/Unison/LSP/FileAnalysis.hs @@ -234,10 +234,8 @@ analyseNotes fileUri ppe src notes = do (_v, locs) <- toList defns (r, rs) <- withNeighbours (locs >>= aToR) pure (r, ("duplicate definition",) <$> rs) - TypeError.RedundantPattern _ploc -> do - empty - TypeError.UncoveredPatterns _mloc _pats -> do - empty + TypeError.RedundantPattern loc -> singleRange loc + TypeError.UncoveredPatterns loc _pats -> singleRange loc -- These type errors don't have custom type error conversions, but some -- still have valid diagnostics. TypeError.Other e@(Context.ErrorNote {cause}) -> case cause of From 1e66edcdf2996f1c6c7dfa99de7dc1c7e94825af Mon Sep 17 00:00:00 2001 From: Travis Staton Date: Thu, 2 Mar 2023 09:11:13 -0500 Subject: [PATCH 44/54] add type sig to lambdacase transcript --- unison-src/transcripts/lambdacase.md | 1 + unison-src/transcripts/lambdacase.output.md | 9 +++++---- 2 files changed, 6 insertions(+), 4 deletions(-) diff --git a/unison-src/transcripts/lambdacase.md b/unison-src/transcripts/lambdacase.md index 1b794b5ba..e2e3a557e 100644 --- a/unison-src/transcripts/lambdacase.md +++ b/unison-src/transcripts/lambdacase.md @@ -75,6 +75,7 @@ Here's another example: ```unison structural type B = T | F +blah : B -> B -> Text blah = cases T, x -> "hi" x, y -> "bye" diff --git a/unison-src/transcripts/lambdacase.output.md b/unison-src/transcripts/lambdacase.output.md index 31cd7b599..6fc1d5387 100644 --- a/unison-src/transcripts/lambdacase.output.md +++ b/unison-src/transcripts/lambdacase.output.md @@ -119,6 +119,7 @@ Here's another example: ```unison structural type B = T | F +blah : B -> B -> Text blah = cases T, x -> "hi" x, y -> "bye" @@ -141,21 +142,21 @@ blorf = cases ⍟ These new definitions are ok to `add`: structural type B - blah : B -> hod1jusqau2 -> Text + blah : B -> B -> Text blorf : B -> B -> B Now evaluating any watch expressions (lines starting with `>`)... Ctrl+C cancels. - 11 | > blah T F + 12 | > blah T F ⧩ "hi" - 12 | > blah F F + 13 | > blah F F ⧩ "bye" - 13 | > blorf T F + 14 | > blorf T F ⧩ F From 7d1a03b38536e95985fe67070b5e6a1b66ef541d Mon Sep 17 00:00:00 2001 From: Travis Staton Date: Thu, 2 Mar 2023 11:21:41 -0500 Subject: [PATCH 45/54] instantiate when we have positive information as well --- parser-typechecker/src/Unison/PatternMatchCoverage/Solve.hs | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/parser-typechecker/src/Unison/PatternMatchCoverage/Solve.hs b/parser-typechecker/src/Unison/PatternMatchCoverage/Solve.hs index ae6d75853..6a6ef469c 100644 --- a/parser-typechecker/src/Unison/PatternMatchCoverage/Solve.hs +++ b/parser-typechecker/src/Unison/PatternMatchCoverage/Solve.hs @@ -259,7 +259,7 @@ expandSolution x nc = -- -- Then we would like to suggest @Just (Just _)@ rather than @Just _@. -- To accomplish this, we recurse and expand variables for which we have - -- negative information. + -- positive or negative information. -- branching factor let newFuel = case length newVars > 1 of @@ -273,7 +273,8 @@ expandSolution x nc = ( \nc -> case expectCanon v nc of (_vc, vi, nc') -> case vi_con vi of - Vc'Constructor _pos neg + Vc'Constructor pos neg + | Just _ <- pos -> go newFuel v nc' | not (Set.null neg) -> go (newFuel - 1) v nc' Vc'Boolean _pos neg | not (Set.null neg) -> go (newFuel - 1) v nc' From de90ae783b842e542b0384d4f296b64fb1d77da5 Mon Sep 17 00:00:00 2001 From: Travis Staton Date: Thu, 2 Mar 2023 11:22:52 -0500 Subject: [PATCH 46/54] always instantiate Unit --- parser-typechecker/src/Unison/PatternMatchCoverage/Solve.hs | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/parser-typechecker/src/Unison/PatternMatchCoverage/Solve.hs b/parser-typechecker/src/Unison/PatternMatchCoverage/Solve.hs index 6a6ef469c..9b2c067b2 100644 --- a/parser-typechecker/src/Unison/PatternMatchCoverage/Solve.hs +++ b/parser-typechecker/src/Unison/PatternMatchCoverage/Solve.hs @@ -18,6 +18,7 @@ import Data.Functor.Compose import Data.List.NonEmpty (NonEmpty (..)) import qualified Data.Sequence as Seq import qualified Data.Set as Set +import Unison.Builtin.Decls (unitRef) import Unison.ConstructorReference (ConstructorReference) import Unison.Pattern (Pattern) import qualified Unison.Pattern as Pattern @@ -36,6 +37,7 @@ import qualified Unison.PatternMatchCoverage.PmLit as PmLit import qualified Unison.PatternMatchCoverage.UFMap as UFMap import Unison.Prelude import Unison.Type (Type) +import qualified Unison.Type as Type import qualified Unison.Util.Pretty as P import Unison.Var (Var) @@ -274,6 +276,8 @@ expandSolution x nc = case expectCanon v nc of (_vc, vi, nc') -> case vi_con vi of Vc'Constructor pos neg + -- always instantiate unit, this ensures we print tuple patterns correctly + | Type.Ref' x <- vi_typ vi, x == unitRef -> go newFuel v nc' | Just _ <- pos -> go newFuel v nc' | not (Set.null neg) -> go (newFuel - 1) v nc' Vc'Boolean _pos neg From bda4ea5382ff3e153959c2e016325c6d30659d66 Mon Sep 17 00:00:00 2001 From: Travis Staton Date: Thu, 2 Mar 2023 10:04:36 -0500 Subject: [PATCH 47/54] expand pattern match coverage transcript --- .../transcripts/pattern-match-coverage.md | 136 +++++++-- .../pattern-match-coverage.output.md | 270 +++++++++++++----- 2 files changed, 313 insertions(+), 93 deletions(-) diff --git a/unison-src/transcripts/pattern-match-coverage.md b/unison-src/transcripts/pattern-match-coverage.md index b6e478256..85eab251c 100644 --- a/unison-src/transcripts/pattern-match-coverage.md +++ b/unison-src/transcripts/pattern-match-coverage.md @@ -3,7 +3,7 @@ ``` # Basics -non-exhaustive patterns are reported +## non-exhaustive patterns ```unison:error unique type T = A | B | C @@ -12,7 +12,18 @@ test = cases A -> () ``` -redundant matches are reported +```unison:error +unique type T = A | B + +test : (T, Optional T) -> () +test = cases + (A, Some _) -> () + (A, None) -> () + (B, Some A) -> () + (B, None) -> () +``` + +## redundant patterns ```unison:error unique type T = A | B | C @@ -24,7 +35,21 @@ test = cases _ -> () ``` -uninhabited patterns are not expected +```unison:error +unique type T = A | B + +test : (T, Optional T) -> () +test = cases + (A, Some _) -> () + (A, None) -> () + (B, Some _) -> () + (B, None) -> () + (A, Some A) -> () +``` + +# Uninhabited patterns + +match is complete without covering uninhabited patterns ```unison unique type V = @@ -34,7 +59,7 @@ test = cases Some None -> () ``` -they are reported as redundant +uninhabited patterns are reported as redundant ```unison:error unique type V = @@ -45,15 +70,37 @@ test = cases Some _ -> () ``` -boolean guards are considered +# Guards + +## Incomplete patterns due to guards should be reported ```unison:error test : () -> () test = cases () | false -> () ``` -uncovered patterns are only instantiated as deeply as necessary to -distinguish them from existing patterns +```unison:error +test : Optional Nat -> Nat +test = cases + None -> 0 + Some x + | isEven x -> x +``` + +## Complete patterns with guards should be accepted +```unison:error +test : Optional Nat -> Nat +test = cases + None -> 0 + Some x + | isEven x -> x + | otherwise -> 0 +``` + +# Pattern instantiation depth + +Uncovered patterns are only instantiated as deeply as necessary to +distinguish them from existing patterns. ```unison:error unique type T = A | B | C @@ -74,13 +121,26 @@ test = cases ``` # Literals -non-exhaustive nat + +## Non-exhaustive + +Nat ```unison:error test : Nat -> () test = cases 0 -> () ``` +Boolean +```unison:error +test : Boolean -> () +test = cases + true -> () +``` + +## Exhaustive + +Nat ```unison test : Nat -> () test = cases @@ -88,13 +148,7 @@ test = cases _ -> () ``` -non-exhaustive boolean -```unison:error -test : Boolean -> () -test = cases - true -> () -``` - +Boolean ```unison test : Boolean -> () test = cases @@ -102,7 +156,18 @@ test = cases false -> () ``` -redundant boolean +# Redundant + +Nat +```unison:error +test : Nat -> () +test = cases + 0 -> () + 0 -> () + _ -> () +``` + +Boolean ```unison:error test : Boolean -> () test = cases @@ -112,6 +177,8 @@ test = cases ``` # Sequences + +## Exhaustive ```unison test : [()] -> () test = cases @@ -119,6 +186,7 @@ test = cases x +: xs -> () ``` +## Non-exhaustive ```unison:error test : [()] -> () test = cases @@ -137,14 +205,6 @@ test = cases xs :+ x -> () ``` -```unison -unique type V = - -test : [V] -> () -test = cases - [] -> () -``` - ```unison:error test : [()] -> () test = cases @@ -159,8 +219,25 @@ test = cases x0 +: [] -> () ``` -cons and snoc patterns are equated when a length restriction implies -that they refer to the same element +## Uninhabited + +`Cons` is not expected since `V` is uninhabited +```unison +unique type V = + +test : [V] -> () +test = cases + [] -> () +``` + +## Length restrictions can equate cons and nil patterns + +Here the first pattern matches lists of length two or greater, the +second pattern matches lists of length 0. The third case matches when the +final element is `false`, while the fourth pattern matches when the +first element is `true`. However, the only possible list length at +the third or fourth clause is 1, so the first and final element must +be equal. Thus, the pattern match is exhaustive. ```unison test : [Boolean] -> () test = cases @@ -170,6 +247,7 @@ test = cases true +: xs -> () ``` +This is the same idea as above but shows that fourth match is redundant. ```unison:error test : [Boolean] -> () test = cases @@ -180,6 +258,12 @@ test = cases _ -> () ``` +This is another similar example. The first pattern matches lists of +length 5 or greater. The second matches lists of length 4 or greater where the +first and third element are true. The third matches lists of length 4 +or greater where the final 4 elements are `true, false, true, false`. +The list must be exactly of length 4 to arrive at the second or third +clause, so the third pattern is redundant. ```unison:error test : [Boolean] -> () test = cases diff --git a/unison-src/transcripts/pattern-match-coverage.output.md b/unison-src/transcripts/pattern-match-coverage.output.md index 34d874134..400a4382d 100644 --- a/unison-src/transcripts/pattern-match-coverage.output.md +++ b/unison-src/transcripts/pattern-match-coverage.output.md @@ -1,5 +1,5 @@ # Basics -non-exhaustive patterns are reported +## non-exhaustive patterns ```unison unique type T = A | B | C @@ -21,7 +21,32 @@ test = cases * C ``` -redundant matches are reported +```unison +unique type T = A | B + +test : (T, Optional T) -> () +test = cases + (A, Some _) -> () + (A, None) -> () + (B, Some A) -> () + (B, None) -> () +``` + +```ucm + + Pattern match doesn't cover all possible cases: + 4 | test = cases + 5 | (A, Some _) -> () + 6 | (A, None) -> () + 7 | (B, Some A) -> () + 8 | (B, None) -> () + + + Patterns not matched: + * (B, Some B) + +``` +## redundant patterns ```unison unique type T = A | B | C @@ -40,7 +65,28 @@ test = cases ``` -uninhabited patterns are not expected +```unison +unique type T = A | B + +test : (T, Optional T) -> () +test = cases + (A, Some _) -> () + (A, None) -> () + (B, Some _) -> () + (B, None) -> () + (A, Some A) -> () +``` + +```ucm + + This case would be ignored because it's already covered by the preceding case(s): + 9 | (A, Some A) -> () + + +``` +# Uninhabited patterns + +match is complete without covering uninhabited patterns ```unison unique type V = @@ -62,7 +108,7 @@ test = cases test : Optional (Optional V) -> () ``` -they are reported as redundant +uninhabited patterns are reported as redundant ```unison unique type V = @@ -80,7 +126,9 @@ test = cases ``` -boolean guards are considered +# Guards + +## Incomplete patterns due to guards should be reported ```unison test : () -> () test = cases @@ -98,8 +146,52 @@ test = cases * () ``` -uncovered patterns are only instantiated as deeply as necessary to -distinguish them from existing patterns +```unison +test : Optional Nat -> Nat +test = cases + None -> 0 + Some x + | isEven x -> x +``` + +```ucm + + Pattern match doesn't cover all possible cases: + 2 | test = cases + 3 | None -> 0 + 4 | Some x + 5 | | isEven x -> x + + + Patterns not matched: + * Some _ + +``` +## Complete patterns with guards should be accepted +```unison +test : Optional Nat -> Nat +test = cases + None -> 0 + Some x + | isEven x -> x + | otherwise -> 0 +``` + +```ucm + + 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`: + + test : Optional Nat -> Nat + +``` +# Pattern instantiation depth + +Uncovered patterns are only instantiated as deeply as necessary to +distinguish them from existing patterns. ```unison unique type T = A | B | C @@ -147,7 +239,10 @@ test = cases ``` # Literals -non-exhaustive nat + +## Non-exhaustive + +Nat ```unison test : Nat -> () test = cases @@ -165,6 +260,27 @@ test = cases * _ ``` +Boolean +```unison +test : Boolean -> () +test = cases + true -> () +``` + +```ucm + + Pattern match doesn't cover all possible cases: + 2 | test = cases + 3 | true -> () + + + Patterns not matched: + * false + +``` +## Exhaustive + +Nat ```unison test : Nat -> () test = cases @@ -183,24 +299,7 @@ test = cases test : Nat -> () ``` -non-exhaustive boolean -```unison -test : Boolean -> () -test = cases - true -> () -``` - -```ucm - - Pattern match doesn't cover all possible cases: - 2 | test = cases - 3 | true -> () - - - Patterns not matched: - * false - -``` +Boolean ```unison test : Boolean -> () test = cases @@ -219,7 +318,25 @@ test = cases test : Boolean -> () ``` -redundant boolean +# Redundant + +Nat +```unison +test : Nat -> () +test = cases + 0 -> () + 0 -> () + _ -> () +``` + +```ucm + + This case would be ignored because it's already covered by the preceding case(s): + 4 | 0 -> () + + +``` +Boolean ```unison test : Boolean -> () test = cases @@ -236,6 +353,8 @@ test = cases ``` # Sequences + +## Exhaustive ```unison test : [()] -> () test = cases @@ -254,6 +373,7 @@ test = cases test : [()] -> () ``` +## Non-exhaustive ```unison test : [()] -> () test = cases @@ -268,7 +388,7 @@ test = cases Patterns not matched: - * (_ +: _) + * (() +: _) ``` ```unison @@ -306,6 +426,47 @@ test = cases ``` ```unison +test : [()] -> () +test = cases + x0 +: (x1 +: xs) -> () + [] -> () +``` + +```ucm + + Pattern match doesn't cover all possible cases: + 2 | test = cases + 3 | x0 +: (x1 +: xs) -> () + 4 | [] -> () + + + Patterns not matched: + * (() +: []) + +``` +```unison +test : [()] -> () +test = cases + [] -> () + x0 +: [] -> () +``` + +```ucm + + Pattern match doesn't cover all possible cases: + 2 | test = cases + 3 | [] -> () + 4 | x0 +: [] -> () + + + Patterns not matched: + * (() +: (() +: _)) + +``` +## Uninhabited + +`Cons` is not expected since `V` is uninhabited +```unison unique type V = test : [V] -> () @@ -325,46 +486,14 @@ test = cases test : [V] -> () ``` -```unison -test : [()] -> () -test = cases - x0 +: (x1 +: xs) -> () - [] -> () -``` +## Length restrictions can equate cons and nil patterns -```ucm - - Pattern match doesn't cover all possible cases: - 2 | test = cases - 3 | x0 +: (x1 +: xs) -> () - 4 | [] -> () - - - Patterns not matched: - * (_ +: []) - -``` -```unison -test : [()] -> () -test = cases - [] -> () - x0 +: [] -> () -``` - -```ucm - - Pattern match doesn't cover all possible cases: - 2 | test = cases - 3 | [] -> () - 4 | x0 +: [] -> () - - - Patterns not matched: - * (_ +: (_ +: _)) - -``` -cons and snoc patterns are equated when a length restriction implies -that they refer to the same element +Here the first pattern matches lists of length two or greater, the +second pattern matches lists of length 0. The third case matches when the +final element is `false`, while the fourth pattern matches when the +first element is `true`. However, the only possible list length at +the third or fourth clause is 1, so the first and final element must +be equal. Thus, the pattern match is exhaustive. ```unison test : [Boolean] -> () test = cases @@ -385,6 +514,7 @@ test = cases test : [Boolean] -> () ``` +This is the same idea as above but shows that fourth match is redundant. ```unison test : [Boolean] -> () test = cases @@ -402,6 +532,12 @@ test = cases ``` +This is another similar example. The first pattern matches lists of +length 5 or greater. The second matches lists of length 4 or greater where the +first and third element are true. The third matches lists of length 4 +or greater where the final 4 elements are `true, false, true, false`. +The list must be exactly of length 4 to arrive at the second or third +clause, so the third pattern is redundant. ```unison test : [Boolean] -> () test = cases From fe619f612fd3955e055cba1587299f1788b18dea Mon Sep 17 00:00:00 2001 From: Travis Staton Date: Thu, 2 Mar 2023 17:08:04 -0500 Subject: [PATCH 48/54] Update parser-typechecker/src/Unison/PatternMatchCoverage/PmGrd.hs Co-authored-by: Chris Penner --- parser-typechecker/src/Unison/PatternMatchCoverage/PmGrd.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/parser-typechecker/src/Unison/PatternMatchCoverage/PmGrd.hs b/parser-typechecker/src/Unison/PatternMatchCoverage/PmGrd.hs index 8638c0c38..64d86b5a5 100644 --- a/parser-typechecker/src/Unison/PatternMatchCoverage/PmGrd.hs +++ b/parser-typechecker/src/Unison/PatternMatchCoverage/PmGrd.hs @@ -54,7 +54,7 @@ prettyPmGrd :: (Var vt, Var v) => PmGrd vt v loc -> Pretty ColorText prettyPmGrd = \case PmCon var con convars -> let xs = string (show con) : (formatConVar <$> convars) ++ ["<-", string (show var)] - formatConVar (v, t) = sep " " ["(", string (show v), "::", TypePrinter.pretty PPE.empty t, ")"] + formatConVar (v, t) = sep " " ["(", string (show v), ":", TypePrinter.pretty PPE.empty t, ")"] in sep " " xs PmListHead var n el _ -> sep " " ["Cons", string (show n), string (show el), "<-", string (show var)] PmListTail var n el _ -> sep " " ["Snoc", string (show n), string (show el), "<-", string (show var)] From 465737054bd5d461554d3884f7d1be986de13284 Mon Sep 17 00:00:00 2001 From: Travis Staton Date: Thu, 2 Mar 2023 11:57:00 -0500 Subject: [PATCH 49/54] Use Unison.DataDeclaration.dependencies --- parser-typechecker/src/Unison/Codebase.hs | 11 ++++------- 1 file changed, 4 insertions(+), 7 deletions(-) diff --git a/parser-typechecker/src/Unison/Codebase.hs b/parser-typechecker/src/Unison/Codebase.hs index 757f87ea5..f93099367 100644 --- a/parser-typechecker/src/Unison/Codebase.hs +++ b/parser-typechecker/src/Unison/Codebase.hs @@ -161,7 +161,6 @@ import Unison.Symbol (Symbol) import Unison.Term (Term) import qualified Unison.Term as Term import Unison.Type (Type) -import qualified Unison.Type as Type import Unison.Typechecker.TypeLookup (TypeLookup (TypeLookup)) import qualified Unison.Typechecker.TypeLookup as TL import qualified Unison.UnisonFile as UF @@ -362,13 +361,11 @@ typeLookupForDependencies codebase s = do -- the inhabitation check). We ensure these are found -- by collecting all type dependencies for all data -- decls. - let constructorTypes :: [Type Symbol a] - constructorTypes = snd <$> DD.constructors dd - -- All references from constructorTypes that we - -- have not already gathered. - constructorRefs :: Set Reference - constructorRefs = foldl' (\b a -> Set.filter (unseen tl) (Type.dependencies a) <> b) mempty constructorTypes + -- All references from constructorTypes that we + -- have not already gathered. + let constructorRefs :: Set Reference + constructorRefs = Set.filter (unseen tl) (DD.dependencies dd) -- recursively call go for each constructor ref let z = tl <> TypeLookup mempty (Map.singleton ref dd) mempty From a7f201ef6e4b67a87b59a08e6cbcc99448643693 Mon Sep 17 00:00:00 2001 From: Travis Staton Date: Thu, 2 Mar 2023 17:04:43 -0500 Subject: [PATCH 50/54] stray trash comments --- parser-typechecker/src/Unison/PrintError.hs | 2 -- parser-typechecker/src/Unison/Typechecker/Context.hs | 1 - 2 files changed, 3 deletions(-) diff --git a/parser-typechecker/src/Unison/PrintError.hs b/parser-typechecker/src/Unison/PrintError.hs index 3e54f177e..4c52a7ccf 100644 --- a/parser-typechecker/src/Unison/PrintError.hs +++ b/parser-typechecker/src/Unison/PrintError.hs @@ -1058,8 +1058,6 @@ renderContext env ctx@(C.Context es) = shortName v <> " : " <> renderType' env (C.apply ctx t) showElem _ (C.Marker v) = "|" <> shortName v <> "|" --- Term.Term' (TypeVar v loc) v loc - renderTerm :: (IsString s, Var v) => Env -> Term.Term' (TypeVar.TypeVar loc0 v) v loc1 -> s renderTerm env e = let s = Color.toPlain $ TermPrinter.pretty' (Just 80) env (TypeVar.lowerTerm e) diff --git a/parser-typechecker/src/Unison/Typechecker/Context.hs b/parser-typechecker/src/Unison/Typechecker/Context.hs index 54b4a578c..15d2e1529 100644 --- a/parser-typechecker/src/Unison/Typechecker/Context.hs +++ b/parser-typechecker/src/Unison/Typechecker/Context.hs @@ -790,7 +790,6 @@ getDataConstructors typ r == Type.listRef = let xs = [ (ListPat.Cons, [arg]), - -- (ListPat.Snoc, [typ, arg]), (ListPat.Nil, []) ] in pure (SequenceType xs) From 2cadd28947ff28bf4af36be7c81e46476064b911 Mon Sep 17 00:00:00 2001 From: Travis Staton Date: Thu, 2 Mar 2023 17:05:49 -0500 Subject: [PATCH 51/54] document toClasses --- .../src/Unison/PatternMatchCoverage/UFMap.hs | 15 ++++++++++++--- 1 file changed, 12 insertions(+), 3 deletions(-) diff --git a/parser-typechecker/src/Unison/PatternMatchCoverage/UFMap.hs b/parser-typechecker/src/Unison/PatternMatchCoverage/UFMap.hs index 0fdab0e59..f33e1a5bd 100644 --- a/parser-typechecker/src/Unison/PatternMatchCoverage/UFMap.hs +++ b/parser-typechecker/src/Unison/PatternMatchCoverage/UFMap.hs @@ -213,13 +213,22 @@ union k0 k1 mapinit mergeValues = toMaybe do KeyNotFound _k -> Nothing MergeFailed _v0 _v1 -> Nothing -toClasses :: forall k v. (Ord k) => UFMap k v -> [(k, Set k, v)] +-- | Dump the @UFmap@ to a list grouped by equivalence class +toClasses :: + forall k v. + (Ord k) => + UFMap k v -> + -- | [(canonical key, equivalence class, value)] + [(k, Set k, v)] toClasses m0 = let cmFinal :: Map k (k, Set k, v) - (_mfinal, cmFinal) = foldl' phi (m0, Map.empty) keys + (_mfinal, cmFinal) = + -- we fold over the UFMap's keys and build up a Map that + -- groups the keys by equivalence class. + foldl' buildCmFinal (m0, Map.empty) keys keys = case m0 of UFMap m -> Map.keys m - phi (m, cm) k = + buildCmFinal (m, cm) k = let (kcanon, _, v, m') = fromJust (lookupCanon k m) cm' = Map.insertWith From 8faa72a349822e037f3a1c900cf879bed19c6193 Mon Sep 17 00:00:00 2001 From: Travis Staton Date: Fri, 3 Mar 2023 10:25:41 -0500 Subject: [PATCH 52/54] Use Unison.Debug flags --- lib/unison-prelude/src/Unison/Debug.hs | 14 ++++++++++++++ .../src/Unison/PatternMatchCoverage.hs | 4 ++-- .../src/Unison/PatternMatchCoverage/Solve.hs | 3 ++- 3 files changed, 18 insertions(+), 3 deletions(-) diff --git a/lib/unison-prelude/src/Unison/Debug.hs b/lib/unison-prelude/src/Unison/Debug.hs index defaff3b0..f646b48d7 100644 --- a/lib/unison-prelude/src/Unison/Debug.hs +++ b/lib/unison-prelude/src/Unison/Debug.hs @@ -39,6 +39,8 @@ data DebugFlag Temp | -- | Shows Annotations when printing terms Annotations + | PatternCoverage + | PatternCoverageConstraintSolver deriving (Eq, Ord, Show, Bounded, Enum) debugFlags :: Set DebugFlag @@ -61,6 +63,8 @@ debugFlags = case (unsafePerformIO (lookupEnv "UNISON_DEBUG")) of "TIMING" -> pure Timing "TEMP" -> pure Temp "ANNOTATIONS" -> pure Annotations + "PATTERN_COVERAGE" -> pure PatternCoverage + "PATTERN_COVERAGE_CONSTRAINT_SOLVER" -> pure PatternCoverageConstraintSolver _ -> empty {-# NOINLINE debugFlags #-} @@ -108,6 +112,14 @@ debugAnnotations :: Bool debugAnnotations = Annotations `Set.member` debugFlags {-# NOINLINE debugAnnotations #-} +debugPatternCoverage :: Bool +debugPatternCoverage = PatternCoverage `Set.member` debugFlags +{-# NOINLINE debugPatternCoverage #-} + +debugPatternCoverageConstraintSolver :: Bool +debugPatternCoverageConstraintSolver = PatternCoverageConstraintSolver `Set.member` debugFlags +{-# NOINLINE debugPatternCoverageConstraintSolver #-} + -- | Use for trace-style selective debugging. -- E.g. 1 + (debug Git "The second number" 2) -- @@ -159,3 +171,5 @@ shouldDebug = \case Timing -> debugTiming Temp -> debugTemp Annotations -> debugAnnotations + PatternCoverage -> debugPatternCoverage + PatternCoverageConstraintSolver -> debugPatternCoverageConstraintSolver diff --git a/parser-typechecker/src/Unison/PatternMatchCoverage.hs b/parser-typechecker/src/Unison/PatternMatchCoverage.hs index a43bc0e38..05a1531fe 100644 --- a/parser-typechecker/src/Unison/PatternMatchCoverage.hs +++ b/parser-typechecker/src/Unison/PatternMatchCoverage.hs @@ -37,6 +37,7 @@ where import qualified Data.Set as Set import Debug.Trace +import Unison.Debug import Unison.Pattern (Pattern) import Unison.PatternMatchCoverage.Class (Pmc (..)) import Unison.PatternMatchCoverage.Desugar (desugarMatch) @@ -75,8 +76,7 @@ checkMatch matchLocation scrutineeType cases = do P.hang "uncovered:" (NC.prettyDnf uncovered), P.hang "uncovered expanded:" (NC.prettyDnf (Set.fromList uncoveredExpanded)) ] - shouldDebug = False - doDebug = case shouldDebug of + doDebug = case shouldDebug PatternCoverage of True -> trace (P.toPlainUnbroken debugOutput) False -> id doDebug (pure (redundant, inaccessible, sols)) diff --git a/parser-typechecker/src/Unison/PatternMatchCoverage/Solve.hs b/parser-typechecker/src/Unison/PatternMatchCoverage/Solve.hs index 9b2c067b2..72146fed0 100644 --- a/parser-typechecker/src/Unison/PatternMatchCoverage/Solve.hs +++ b/parser-typechecker/src/Unison/PatternMatchCoverage/Solve.hs @@ -20,6 +20,7 @@ import qualified Data.Sequence as Seq import qualified Data.Set as Set import Unison.Builtin.Decls (unitRef) import Unison.ConstructorReference (ConstructorReference) +import Unison.Debug (DebugFlag (PatternCoverageConstraintSolver), shouldDebug) import Unison.Pattern (Pattern) import qualified Unison.Pattern as Pattern import Unison.PatternMatchCoverage.Class @@ -564,7 +565,7 @@ addConstraint con0 nc = P.hang (P.green "resulting constraint: ") (maybe "contradiction" prettyNormalizedConstraints x), "" ] - in if False then trace (P.toAnsiUnbroken debugOutput) x else x + in if shouldDebug PatternCoverageConstraintSolver then trace (P.toAnsiUnbroken debugOutput) x else x -- | Like 'addConstraint', but for a list of constraints addConstraints :: From 1eefcdc5d3ed6d0d2281b24908d323efe24baa02 Mon Sep 17 00:00:00 2001 From: Travis Staton Date: Fri, 3 Mar 2023 10:42:07 -0500 Subject: [PATCH 53/54] stray comment --- parser-typechecker/src/Unison/Runtime/IOSource.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/parser-typechecker/src/Unison/Runtime/IOSource.hs b/parser-typechecker/src/Unison/Runtime/IOSource.hs index 11bec2fa3..458398f8e 100644 --- a/parser-typechecker/src/Unison/Runtime/IOSource.hs +++ b/parser-typechecker/src/Unison/Runtime/IOSource.hs @@ -983,7 +983,7 @@ showNotes source env = intercalateMap "\n\n" $ PrintError.renderNoteAsANSI 60 env source Path.absoluteEmpty decodeResult :: - String -> SynthResult -> EitherResult -- String (UF.TypecheckedUnisonFile Symbol Ann) + String -> SynthResult -> EitherResult decodeResult source (Result.Result notes Nothing) = Left $ showNotes source ppEnv notes decodeResult source (Result.Result notes (Just (Left uf))) = From 96bcbcf2b7edf139cab152d286150b03c13fc5c9 Mon Sep 17 00:00:00 2001 From: Travis Staton Date: Fri, 3 Mar 2023 10:50:35 -0500 Subject: [PATCH 54/54] add complete pragma --- parser-typechecker/src/Unison/PatternMatchCoverage/GrdTree.hs | 2 ++ 1 file changed, 2 insertions(+) diff --git a/parser-typechecker/src/Unison/PatternMatchCoverage/GrdTree.hs b/parser-typechecker/src/Unison/PatternMatchCoverage/GrdTree.hs index 681382f5d..7644cacf3 100644 --- a/parser-typechecker/src/Unison/PatternMatchCoverage/GrdTree.hs +++ b/parser-typechecker/src/Unison/PatternMatchCoverage/GrdTree.hs @@ -84,3 +84,5 @@ pattern Grd x rest = Fix (GrdF x rest) pattern Fork :: NonEmpty (GrdTree n l) -> GrdTree n l pattern Fork alts = Fix (ForkF alts) + +{-# COMPLETE Leaf, Grd, Fork #-}