diff --git a/disco.cabal b/disco.cabal index e1e670fa..f742a162 100644 --- a/disco.cabal +++ b/disco.cabal @@ -445,6 +445,10 @@ library Disco.Value Disco.Error Disco.Eval + Disco.Exhaustiveness + Disco.Exhaustiveness.Constraint + Disco.Exhaustiveness.Possibilities + Disco.Exhaustiveness.TypeInfo Disco.Interpret.CESK Disco.Subst Disco.Typecheck diff --git a/example/lists.disco b/example/lists.disco deleted file mode 100644 index 36a0ee97..00000000 --- a/example/lists.disco +++ /dev/null @@ -1,12 +0,0 @@ -iterateP : (a → a) → a → List(a) -iterateP f p = p :: iterateP f (f p) - -fib2_helper : ℕ×ℕ → ℕ×ℕ -fib2_helper (a,b) = (b,a+b) - -indexP : ℕ -> List(a) -> a -indexP 0 (p::_) = p -indexP (n+1) (_::l') = indexP n l' - -fib2 : ℕ → ℕ -fib2 n = {? x when (indexP n (iterateP fib2_helper (0,1))) is (x,_) ?} diff --git a/src/Disco/AST/Surface.hs b/src/Disco/AST/Surface.hs index 8aab485a..abca2551 100644 --- a/src/Disco/AST/Surface.hs +++ b/src/Disco/AST/Surface.hs @@ -105,6 +105,9 @@ module Disco.AST.Surface ( pattern PFrac, pattern PNonlinear, pattern Binding, + + -- ** Pretty printing + prettyPatternP, ) where diff --git a/src/Disco/Eval.hs b/src/Disco/Eval.hs index 6e2a490e..16600814 100644 --- a/src/Disco/Eval.hs +++ b/src/Disco/Eval.hs @@ -78,11 +78,13 @@ import Polysemy.Output import Polysemy.Random import Polysemy.Reader +import qualified Data.List.NonEmpty as NonEmpty import Disco.AST.Core import Disco.AST.Surface import Disco.Compile (compileDefns) import Disco.Context as Ctx import Disco.Error +import Disco.Exhaustiveness (checkClauses) import Disco.Extensions import Disco.Interpret.CESK import Disco.Messages @@ -384,6 +386,10 @@ loadParsedDiscoModule' quiet mode resolver inProcess name cm@(Module _ mns _ _ _ -- Typecheck (and resolve names in) the module. m <- runTCM tyctx tydefns $ checkModule name importMap cm + -- Check for partial functions + let allTyDefs = M.unionWith const tydefns (m ^. miTydefs) + runFresh $ mapM_ (checkExhaustive allTyDefs) (Ctx.elems $ m ^. miTermdefs) + -- Evaluate all the module definitions and add them to the topEnv. mapError EvalErr $ loadDefsFrom m @@ -443,3 +449,8 @@ loadDef :: loadDef x body = do v <- inputToState @TopInfo . inputTopEnv $ eval body modify @TopInfo $ topEnv %~ Ctx.insert x v + +checkExhaustive :: Members '[Fresh, Output (Message ann), Embed IO] r => TyDefCtx -> Defn -> Sem r () +checkExhaustive tyDefCtx (Defn name argsType _ boundClauses) = do + clauses <- NonEmpty.map fst <$> mapM unbind boundClauses + runReader @TyDefCtx tyDefCtx $ checkClauses name argsType clauses diff --git a/src/Disco/Exhaustiveness.hs b/src/Disco/Exhaustiveness.hs new file mode 100644 index 00000000..41305cd8 --- /dev/null +++ b/src/Disco/Exhaustiveness.hs @@ -0,0 +1,417 @@ +{-# LANGUAGE PatternSynonyms #-} + +-- | +-- Module : Disco.Exhaustiveness +-- Copyright : disco team and contributors +-- Maintainer : byorgey@gmail.com +-- +-- SPDX-License-Identifier: BSD-3-Clause +-- +-- Entry point into the exhaustiveness checker. +-- Converts information into a format the checker understands, +-- then pretty prints the results of running it. +module Disco.Exhaustiveness where + +import Control.Monad (forM, unless, zipWithM) +import Control.Monad.Trans.Maybe (MaybeT, runMaybeT) +import Data.List (nub) +import Data.List.NonEmpty (NonEmpty) +import qualified Data.List.NonEmpty as NonEmpty +import Data.Maybe (catMaybes) +import Disco.AST.Generic (Side (..)) +import Disco.AST.Surface ( + Pattern, + prettyPatternP, + pattern PBool, + pattern PChar, + pattern PInj, + pattern PList, + pattern PNat, + pattern PNeg, + pattern PString, + pattern PTup, + pattern PUnit, + pattern PWild, + ) +import Disco.AST.Typed ( + APattern, + ATerm, + pattern APBool, + pattern APChar, + pattern APCons, + pattern APInj, + pattern APList, + pattern APNat, + pattern APNeg, + pattern APString, + pattern APTup, + pattern APUnit, + pattern APVar, + pattern APWild, + ) +import Disco.Effects.Fresh (Fresh) +import Disco.Effects.LFresh (LFresh, runLFresh) +import qualified Disco.Exhaustiveness.Constraint as C +import qualified Disco.Exhaustiveness.Possibilities as Poss +import qualified Disco.Exhaustiveness.TypeInfo as TI +import Disco.Messages +import Disco.Pretty (Doc, initPA, withPA) +import qualified Disco.Pretty.DSL as DSL +import Disco.Pretty.Prec (PA, funPA) +import qualified Disco.Types as Ty +import Polysemy +import Polysemy.Output +import Polysemy.Reader +import Unbound.Generics.LocallyNameless (Name) + +-- | This exhaustiveness checking algorithm is based on the paper +-- "Lower Your Guards: A Compositional Pattern-Match Coverage Checker": +-- https://www.microsoft.com/en-us/research/uploads/prod/2020/03/lyg.pdf +-- +-- Some simplifications were made to adapt the algorithm to suit Disco. +-- The most notable change is that here we always generate (at most) 3 +-- concrete examples of uncovered patterns, instead of finding the most +-- general complete description of every uncovered input. +checkClauses :: (Members '[Fresh, Reader Ty.TyDefCtx, Output (Message ann), Embed IO] r) => Name ATerm -> [Ty.Type] -> NonEmpty [APattern] -> Sem r () +checkClauses name types pats = do + args <- TI.newVars types + cl <- zipWithM (desugarClause args) [1 ..] (NonEmpty.toList pats) + let gdt = foldr1 Branch cl + + let argsNref = [] + (normalizedNrefs, _) <- ua [argsNref] gdt + + examples <- findPosExamples normalizedNrefs args + + unless (null examples) $ do + let prettyExampleArgs exArgs = + DSL.hcat $ map prettyPrintExample exArgs + + let prettyExampleLine prettyArgs = + DSL.text (show name) DSL.<> prettyArgs DSL.<+> DSL.text "= ..." + + let prettyExamples = + DSL.vcat $ map (prettyExampleLine . prettyExampleArgs) examples + + warn $ + DSL.text "Warning: the function" + DSL.<+> DSL.text (show name) + DSL.<+> DSL.text "is undefined for some inputs. For example:" + DSL.$+$ prettyExamples + +prettyPrintExample :: ExamplePat -> Sem r (Doc ann) +prettyPrintExample = runLFresh . runReader initPA . prettyPrintPattern . exampleToDiscoPattern + +prettyPrintPattern :: (Members '[Reader PA, LFresh] r) => Pattern -> Sem r (Doc ann) +prettyPrintPattern = withPA funPA . prettyPatternP + +exampleToDiscoPattern :: ExamplePat -> Pattern +exampleToDiscoPattern e@(ExamplePat TI.DataCon {TI.dcIdent = ident, TI.dcTypes = types} args) = case (ident, args) of + (TI.KUnknown, _) -> PWild + (TI.KUnit, _) -> PUnit + (TI.KBool b, _) -> PBool b + (TI.KNat n, _) -> PNat n + (TI.KInt z, _) -> + if z >= 0 + then PNat z + else PNeg (PNat (abs z)) + (TI.KPair, _) -> PTup $ map exampleToDiscoPattern $ resugarPair e + (TI.KCons, _) -> + if take 1 types == [Ty.TyC] + then PString $ resugarString e + else PList $ map exampleToDiscoPattern $ resugarList e + (TI.KNil, _) -> PList [] + (TI.KChar c, _) -> PChar c + (TI.KLeft, [l]) -> PInj L $ exampleToDiscoPattern l + (TI.KRight, [r]) -> PInj R $ exampleToDiscoPattern r + (TI.KLeft, _) -> error "Found KLeft data constructor with 0 or multiple arguments" + (TI.KRight, _) -> error "Found KRight data constructor with 0 or multiple arguments" + +resugarPair :: ExamplePat -> [ExamplePat] +resugarPair e@(ExamplePat TI.DataCon {TI.dcIdent = ident} args) = case (ident, args) of + (TI.KPair, [efst, esnd]) -> efst : resugarPair esnd + (_, _) -> [e] + +resugarList :: ExamplePat -> [ExamplePat] +resugarList (ExamplePat TI.DataCon {TI.dcIdent = ident} args) = case (ident, args) of + (TI.KCons, [ehead, etail]) -> ehead : resugarList etail + (_, _) -> [] + +resugarString :: ExamplePat -> String +resugarString (ExamplePat TI.DataCon {TI.dcIdent = ident} args) = case (ident, args) of + (TI.KCons, [ehead, etail]) -> assumeExampleChar ehead : resugarString etail + (_, _) -> [] + +assumeExampleChar :: ExamplePat -> Char +assumeExampleChar (ExamplePat TI.DataCon {TI.dcIdent = TI.KChar c} _) = c +assumeExampleChar _ = error "Wrongly assumed that an ExamplePat was a Char" + +desugarClause :: (Members '[Fresh, Embed IO] r) => [TI.TypedVar] -> Int -> [APattern] -> Sem r Gdt +desugarClause args clauseIdx argsPats = do + guards <- zipWithM desugarMatch args argsPats + return $ foldr Guarded (Grhs clauseIdx) $ concat guards + +-- To work with the LYG algorithm, we need to desugar n-tuples to nested pairs +-- Just having a Tuple type with a variable number of arguments breaks. +-- Imagine we have +-- foo (1,2,3) = ... +-- foo (1,(2,n)) = ... +-- if we keep things in our nice "sugared" form, the solver will get confused, +-- and not realize that the last element of the tuple is fully covered by n, +-- because there will be two notions of last element: the last in the triple and +-- the last in the nested pair +desugarTuplePats :: [APattern] -> APattern +desugarTuplePats [] = error "Found empty tuple, what happened?" +desugarTuplePats [p] = p +desugarTuplePats (pfst : rest) = APTup (Ty.getType pfst Ty.:*: Ty.getType psnd) [pfst, psnd] + where + psnd = desugarTuplePats rest + +-- | Convert a Disco APattern into a list of Guards which cover that pattern +-- +-- These patterns are currently not handled: +-- , APNeg --still need to handle rational case +-- , APFrac --required for rationals? +-- algebraic (probably will be eventually replaced anyway): +-- , APAdd +-- , APMul +-- , APSub +-- These (or some updated version of them) may be handled eventually, +-- once updated arithmetic patterns are merged. +-- +-- We treat unhandled patterns as if they are exhaustively matched against +-- (aka, they are seen as wildcards by the checker). +-- This necessarily results in some false negatives, but no false positives. +desugarMatch :: (Members '[Fresh, Embed IO] r) => TI.TypedVar -> APattern -> Sem r [Guard] +desugarMatch var pat = case pat of + (APTup (ta Ty.:*: tb) [pfst, psnd]) -> do + varFst <- TI.newVar ta + varSnd <- TI.newVar tb + guardsFst <- desugarMatch varFst pfst + guardsSnd <- desugarMatch varSnd psnd + let guardPair = (var, GMatch (TI.pair ta tb) [varFst, varSnd]) + return $ [guardPair] ++ guardsFst ++ guardsSnd + (APTup _ sugary) -> desugarMatch var (desugarTuplePats sugary) + (APCons _ subHead subTail) -> do + let typeHead = Ty.getType subHead + let typeTail = Ty.getType subTail + varHead <- TI.newVar typeHead + varTail <- TI.newVar typeTail + guardsHead <- desugarMatch varHead subHead + guardsTail <- desugarMatch varTail subTail + let guardCons = (var, GMatch (TI.cons typeHead typeTail) [varHead, varTail]) + return $ [guardCons] ++ guardsHead ++ guardsTail + -- We have to desugar Lists into Cons and Nils + (APList _ []) -> return [(var, GMatch TI.nil [])] + (APList ty (phead : ptail)) -> do + -- APCons have the type of the list they are part of + desugarMatch var (APCons ty phead (APList ty ptail)) + -- we have to desugar to a list, becuse we can match strings with cons + (APString str) -> do + let strType = Ty.TyList Ty.TyC + desugarMatch var (APList strType (map APChar str)) + -- A bit of strangeness is required here because of how patterns work + (APNat Ty.TyN nat) -> return [(var, GMatch (TI.natural nat) [])] + (APNat Ty.TyZ z) -> return [(var, GMatch (TI.integer z) [])] + (APNeg Ty.TyZ (APNat Ty.TyN z)) -> return [(var, GMatch (TI.integer (-z)) [])] + -- These are more straightforward: + (APWild _) -> return [] + (APVar ty name) -> do + let newAlias = TI.TypedVar (name, ty) + return [(newAlias, GWasOriginally var)] + APUnit -> return [(var, GMatch TI.unit [])] + (APBool b) -> return [(var, GMatch (TI.bool b) [])] + (APChar c) -> return [(var, GMatch (TI.char c) [])] + (APInj (tl Ty.:+: tr) side subPat) -> do + let dc = case side of + L -> TI.left tl + R -> TI.right tr + newVar <- case side of + L -> TI.newVar tl + R -> TI.newVar tr + guards <- desugarMatch newVar subPat + return $ (var, GMatch dc [newVar]) : guards + _ -> return [] + +data Gdt where + Grhs :: Int -> Gdt + Branch :: Gdt -> Gdt -> Gdt + Guarded :: Guard -> Gdt -> Gdt + deriving (Show, Eq) + +type Guard = (TI.TypedVar, GuardConstraint) + +data GuardConstraint where + GMatch :: TI.DataCon -> [TI.TypedVar] -> GuardConstraint + GWasOriginally :: TI.TypedVar -> GuardConstraint + deriving (Show, Eq) + +newtype Literal = Literal (TI.TypedVar, LitCond) + +data LitCond where + LitMatch :: TI.DataCon -> [TI.TypedVar] -> LitCond + LitNot :: TI.DataCon -> LitCond + LitWasOriginally :: TI.TypedVar -> LitCond + deriving (Show, Eq, Ord) + +data Ant where + AGrhs :: [C.NormRefType] -> Int -> Ant + ABranch :: Ant -> Ant -> Ant + deriving (Show) + +ua :: (Members '[Fresh, Reader Ty.TyDefCtx] r) => [C.NormRefType] -> Gdt -> Sem r ([C.NormRefType], Ant) +ua nrefs gdt = case gdt of + Grhs k -> return ([], AGrhs nrefs k) + Branch t1 t2 -> do + (n1, u1) <- ua nrefs t1 + (n2, u2) <- ua n1 t2 + return (n2, ABranch u1 u2) + Guarded (y, GWasOriginally x) t -> do + n <- addLitMulti nrefs $ Literal (y, LitWasOriginally x) + ua n t + Guarded (x, GMatch dc args) t -> do + n <- addLitMulti nrefs $ Literal (x, LitMatch dc args) + (n', u) <- ua n t + n'' <- addLitMulti nrefs $ Literal (x, LitNot dc) + return (n'' ++ n', u) + +addLitMulti :: (Members '[Fresh, Reader Ty.TyDefCtx] r) => [C.NormRefType] -> Literal -> Sem r [C.NormRefType] +addLitMulti [] _ = return [] +addLitMulti (n : ns) lit = do + r <- runMaybeT $ addLiteral n lit + case r of + Nothing -> addLitMulti ns lit + Just cfs -> do + ns' <- addLitMulti ns lit + return $ cfs : ns' + +addLiteral :: (Members '[Fresh, Reader Ty.TyDefCtx] r) => C.NormRefType -> Literal -> MaybeT (Sem r) C.NormRefType +addLiteral constraints (Literal (x, c)) = case c of + LitWasOriginally z -> + constraints `C.addConstraint` (x, C.CWasOriginally z) + LitMatch dc args -> + constraints `C.addConstraint` (x, C.CMatch dc args) + LitNot dc -> + constraints `C.addConstraint` (x, C.CNot dc) + +data InhabPat where + IPIs :: TI.DataCon -> [InhabPat] -> InhabPat + IPNot :: [TI.DataCon] -> InhabPat + deriving (Show, Eq, Ord) + +-- Sanity check: are we giving the dataconstructor the +-- correct number of arguments? +mkIPMatch :: TI.DataCon -> [InhabPat] -> InhabPat +mkIPMatch k pats = + if length (TI.dcTypes k) /= length pats + then error $ "Wrong number of DataCon args" ++ show (k, pats) + else IPIs k pats + +findInhabitants :: (Members '[Fresh, Reader Ty.TyDefCtx] r) => [C.NormRefType] -> [TI.TypedVar] -> Sem r (Poss.Possibilities [InhabPat]) +findInhabitants nrefs args = do + a <- forM nrefs (`findAllForNref` args) + return $ Poss.anyOf a + +findAllForNref :: (Members '[Fresh, Reader Ty.TyDefCtx] r) => C.NormRefType -> [TI.TypedVar] -> Sem r (Poss.Possibilities [InhabPat]) +findAllForNref nref args = do + argPats <- forM args (`findVarInhabitants` nref) + return $ Poss.allCombinations argPats + +findVarInhabitants :: (Members '[Fresh, Reader Ty.TyDefCtx] r) => TI.TypedVar -> C.NormRefType -> Sem r (Poss.Possibilities InhabPat) +findVarInhabitants var cns = + case posMatch of + Just (k, args) -> do + argPossibilities <- findAllForNref cns args + return (mkIPMatch k <$> argPossibilities) + Nothing -> case nub negMatches of + [] -> Poss.retSingle $ IPNot [] + neg -> do + tyCtx <- ask @Ty.TyDefCtx + case TI.tyDataCons (TI.getType var) tyCtx of + TI.Infinite _ -> Poss.retSingle $ IPNot neg + TI.Finite dcs -> + do + let tryAddDc dc = do + vars <- TI.newVars (TI.dcTypes dc) + runMaybeT (cns `C.addConstraint` (var, C.CMatch dc vars)) + + -- Try to add a positive constraint for each data constructor + -- to the current nref + -- If any of these additions succeed, save that nref, + -- it now has positive information + posNrefs <- catMaybes <$> forM dcs tryAddDc + + if null posNrefs + then Poss.retSingle $ IPNot [] + else Poss.anyOf <$> forM posNrefs (findVarInhabitants var) + where + constraintsOnX = C.onVar var cns + posMatch = C.posMatch constraintsOnX + negMatches = C.negMatches constraintsOnX + +findRedundant :: (Members '[Fresh, Reader Ty.TyDefCtx] r) => Ant -> [TI.TypedVar] -> Sem r [Int] +findRedundant ant args = case ant of + AGrhs ref i -> do + uninhabited <- Poss.none <$> findInhabitants ref args + return [i | uninhabited] + ABranch a1 a2 -> mappend <$> findRedundant a1 args <*> findRedundant a2 args + +data ExamplePat where + ExamplePat :: TI.DataCon -> [ExamplePat] -> ExamplePat + deriving (Show) + +-- | Less general version of the above inhabitant finding function +-- returns a maximum of 3 possible args lists that haven't been matched against, +-- as to not overwhelm new users of the language. +-- This is essentially a DFS, and it has a bad habit of +-- trying to build infinite lists whenever it can, so we give it a max depth of 32 +-- If we reach 32 levels of nested dataconstructors in this language, +-- it is pretty safe to assume we were chasing after an infinite structure +findPosExamples :: (Members '[Fresh, Reader Ty.TyDefCtx] r) => [C.NormRefType] -> [TI.TypedVar] -> Sem r [[ExamplePat]] +findPosExamples nrefs args = do + a <- forM nrefs (\nref -> findAllPosForNref 32 nref args) + return $ take 3 $ Poss.getPossibilities $ Poss.anyOf a + +findAllPosForNref :: (Members '[Fresh, Reader Ty.TyDefCtx] r) => Int -> C.NormRefType -> [TI.TypedVar] -> Sem r (Poss.Possibilities [ExamplePat]) +findAllPosForNref fuel nref args = do + argPats <- forM args (\arg -> findVarPosExamples (fuel - 1) arg nref) + return $ Poss.allCombinations argPats + +findVarPosExamples :: (Members '[Fresh, Reader Ty.TyDefCtx] r) => Int -> TI.TypedVar -> C.NormRefType -> Sem r (Poss.Possibilities ExamplePat) +findVarPosExamples fuel var cns = + if fuel < 0 + then return mempty + else case posMatch of + Just (k, args) -> do + argPossibilities <- findAllPosForNref (fuel - 1) cns args + return (mkExampleMatch k <$> argPossibilities) + Nothing -> do + tyCtx <- ask @Ty.TyDefCtx + let dcs = getPosFrom (TI.getType var) tyCtx negMatches + let tryAddDc dc = do + vars <- TI.newVars (TI.dcTypes dc) + runMaybeT (cns `C.addConstraint` (var, C.CMatch dc vars)) + -- Try to add a positive constraint for each data constructor + -- to the current nref + -- If any of these additions succeed, save that nref, + -- it now has positive information + posNrefs <- catMaybes <$> forM dcs tryAddDc + + Poss.anyOf <$> forM posNrefs (findVarPosExamples (fuel - 1) var) + where + constraintsOnX = C.onVar var cns + posMatch = C.posMatch constraintsOnX + negMatches = C.negMatches constraintsOnX + +getPosFrom :: Ty.Type -> Ty.TyDefCtx -> [TI.DataCon] -> [TI.DataCon] +getPosFrom ty ctx neg = take 3 $ filter (`notElem` neg) dcs + where + dcs = case TI.tyDataCons ty ctx of + TI.Finite dcs' -> dcs' + TI.Infinite dcs' -> dcs' + +mkExampleMatch :: TI.DataCon -> [ExamplePat] -> ExamplePat +mkExampleMatch k pats = + if length (TI.dcTypes k) /= length pats + then error $ "Wrong number of DataCon args" ++ show (k, pats) + else ExamplePat k pats diff --git a/src/Disco/Exhaustiveness/Constraint.hs b/src/Disco/Exhaustiveness/Constraint.hs new file mode 100644 index 00000000..59afb7c6 --- /dev/null +++ b/src/Disco/Exhaustiveness/Constraint.hs @@ -0,0 +1,151 @@ +-- | +-- Module : Disco.Exhaustiveness.Constraint +-- Copyright : disco team and contributors +-- Maintainer : byorgey@gmail.com +-- +-- SPDX-License-Identifier: BSD-3-Clause +-- +-- The heart of the Lower Your Guards algorithm. +-- Functions for converting constraints detailing +-- pattern matches into a normalized description +-- of everything that is left uncovered. +module Disco.Exhaustiveness.Constraint where + +import Control.Applicative (Alternative) +import Control.Monad (foldM, guard) +import Control.Monad.Trans (lift) +import Control.Monad.Trans.Maybe (MaybeT, runMaybeT) +import Data.Bifunctor (first) +import Data.List (partition) +import Data.Maybe (isJust, listToMaybe, mapMaybe) +import Disco.Effects.Fresh (Fresh) +import qualified Disco.Exhaustiveness.TypeInfo as TI +import qualified Disco.Types as Ty +import Polysemy +import Polysemy.Reader + +data Constraint where + CMatch :: TI.DataCon -> [TI.TypedVar] -> Constraint + CNot :: TI.DataCon -> Constraint + CWasOriginally :: TI.TypedVar -> Constraint + deriving (Show, Eq, Ord) + +posMatch :: [Constraint] -> Maybe (TI.DataCon, [TI.TypedVar]) +posMatch constraints = listToMaybe $ mapMaybe (\case (CMatch k ys) -> Just (k, ys); _ -> Nothing) constraints + +negMatches :: [Constraint] -> [TI.DataCon] +negMatches = mapMaybe (\case (CNot k) -> Just k; _ -> Nothing) + +type ConstraintFor = (TI.TypedVar, Constraint) + +-- Resolves term equalities, finding the leftmost id for a variable +-- I believe I3 of section 3.4 allows us to +-- do a linear scan from right to left +lookupVar :: TI.TypedVar -> [ConstraintFor] -> TI.TypedVar +lookupVar x = foldr getNextId x + where + getNextId (x', CWasOriginally y) | x' == x = const y + getNextId _ = id + +alistLookup :: (Eq a) => a -> [(a, b)] -> [b] +alistLookup a = map snd . filter ((== a) . fst) + +onVar :: TI.TypedVar -> [ConstraintFor] -> [Constraint] +onVar x cs = alistLookup (lookupVar x cs) cs + +type NormRefType = [ConstraintFor] + +addConstraints :: Members '[Fresh, Reader Ty.TyDefCtx] r => NormRefType -> [ConstraintFor] -> MaybeT (Sem r) NormRefType +addConstraints = foldM addConstraint + +addConstraint :: Members '[Fresh, Reader Ty.TyDefCtx] r => NormRefType -> ConstraintFor -> MaybeT (Sem r) NormRefType +addConstraint cns (x, c) = do + breakIf $ any (conflictsWith c) (onVar x cns) + addConstraintHelper cns (lookupVar x cns, c) + +addConstraintHelper :: Members '[Fresh, Reader Ty.TyDefCtx] r => NormRefType -> ConstraintFor -> MaybeT (Sem r) NormRefType +addConstraintHelper cns cf@(origX, c) = case c of + --- Equation (10) + CMatch k args -> do + case getConstructorArgs k (onVar origX cns) of + -- 10c + Just args' -> + addConstraints + cns + (zipWith (\a b -> (a, CWasOriginally b)) args args') + Nothing -> return added + --- Equation (11) + CNot _ -> do + inh <- lift (inhabited added origX) + guard inh -- ensure that origX is still inhabited, as per I2 + return added + -- Equation (14) + CWasOriginally y -> do + let origY = lookupVar y cns + if origX == origY + then return cns + else do + let (noX', withX') = partition ((/= origX) . fst) cns + addConstraints (noX' ++ [cf]) (substituteVarIDs origY origX withX') + where + added = cns ++ [cf] + +----- +----- Helper functions for adding constraints: +----- + +breakIf :: (Alternative f) => Bool -> f () +breakIf = guard . not + +-- | Returns a predicate that returns true if another +-- constraint conflicts with the one given. +-- This alone is not sufficient to test +-- if a constraint can be added, but it +-- filters out the easy negatives early on +conflictsWith :: Constraint -> (Constraint -> Bool) +conflictsWith c = case c of + CMatch k _ -> \case + (CMatch k' _) | k /= k' -> True -- 10a + (CNot k') | k == k' -> True -- 10b + _ -> False + CNot k -> \case + (CMatch k' _) | k == k' -> True -- 11a + _ -> False + CWasOriginally _ -> const False + +-- | Search for a MatchDataCon that is matching on k specifically +-- (there should be at most one, see I4 in section 3.4) +-- and if it exists, return the variable ids of its arguments +getConstructorArgs :: TI.DataCon -> [Constraint] -> Maybe [TI.TypedVar] +getConstructorArgs k cfs = + listToMaybe $ + mapMaybe (\case (CMatch k' vs) | k' == k -> Just vs; _ -> Nothing) cfs + +-- | substituting y *for* x +-- ie replace the second with the first, replace x with y +substituteVarIDs :: TI.TypedVar -> TI.TypedVar -> [ConstraintFor] -> [ConstraintFor] +substituteVarIDs y x = map (first subst) + where + subst var = if var == x then y else x + +-- | Deals with I2 from section 3.4 +-- if a variable in the context has a resolvable type, there must be at least one constructor +-- which can be instantiated without contradiction of the refinement type +-- This function tests if this is true +inhabited :: Members '[Fresh, Reader Ty.TyDefCtx] r => NormRefType -> TI.TypedVar -> Sem r Bool +inhabited n var = do + tyCtx <- ask @Ty.TyDefCtx + case TI.tyDataCons (TI.getType var) tyCtx of + TI.Infinite _ -> return True -- assume opaque types are inhabited + TI.Finite constructors -> do + or <$> mapM (instantiate n var) constructors + +-- | Attempts to "instantiate" a match of the dataconstructor k on x +-- If we can add the MatchDataCon constraint to the normalized refinement +-- type without contradiction (a Nothing value), +-- then x is inhabited by k and we return true +instantiate :: Members '[Fresh, Reader Ty.TyDefCtx] r => NormRefType -> TI.TypedVar -> TI.DataCon -> Sem r Bool +instantiate cns var k = do + args <- TI.newVars $ TI.dcTypes k + let attempt = cns `addConstraint` (var, CMatch k args) + isJust <$> runMaybeT attempt diff --git a/src/Disco/Exhaustiveness/Possibilities.hs b/src/Disco/Exhaustiveness/Possibilities.hs new file mode 100644 index 00000000..439174d2 --- /dev/null +++ b/src/Disco/Exhaustiveness/Possibilities.hs @@ -0,0 +1,59 @@ +{-# LANGUAGE GeneralizedNewtypeDeriving #-} + +-- | +-- Module : Disco.Exhaustiveness.Possibilities +-- Copyright : disco team and contributors +-- Maintainer : byorgey@gmail.com +-- +-- SPDX-License-Identifier: BSD-3-Clause +-- +-- Meaningful types and functions for describing +-- combinations of different possible options. +module Disco.Exhaustiveness.Possibilities (Possibilities, retSingle, allCombinations, anyOf, none, getPossibilities) where + +import Data.Foldable (fold) + +newtype Possibilities a = Possibilities {getPossibilities :: [a]} + deriving (Show, Eq, Ord, Functor, Semigroup, Monoid, Applicative) + +anyOf :: [Possibilities a] -> Possibilities a +anyOf = fold + +none :: Possibilities a -> Bool +none = null . getPossibilities + +retSingle :: (Monad m) => a -> m (Possibilities a) +retSingle i = return $ Possibilities [i] + +-- | List all possible paths through the list of Possibilites +-- +-- Ex. +-- > allCombinations +-- [ Possibilities [1] +-- , Possibilities [2,3] +-- , Possibilities [4] +-- , Possibilities [5,6,7] +-- ] +-- === +-- Possibilities {getPossibilities = +-- [[1,2,4,5] +-- ,[1,2,4,6] +-- ,[1,2,4,7] +-- ,[1,3,4,5] +-- ,[1,3,4,6] +-- ,[1,3,4,7] +-- ]} +-- +-- 2 5 +-- / \ / +-- 1 4 --6 +-- \ / \ +-- 3 7 +-- +-- If any any of the Possibilities is empty, +-- an empty Possibility is returned +-- +-- In other words, this lists all elements of the +-- cartesian product of multiple sets +allCombinations :: [Possibilities a] -> Possibilities [a] +allCombinations = sequenceA diff --git a/src/Disco/Exhaustiveness/TypeInfo.hs b/src/Disco/Exhaustiveness/TypeInfo.hs new file mode 100644 index 00000000..14edd7e7 --- /dev/null +++ b/src/Disco/Exhaustiveness/TypeInfo.hs @@ -0,0 +1,183 @@ +-- | +-- Module : Disco.Exhaustiveness.TypeInfo +-- Copyright : disco team and contributors +-- Maintainer : byorgey@gmail.com +-- +-- SPDX-License-Identifier: BSD-3-Clause +-- +-- Utilities for converting Disco types into 'Constructors' +-- that the exhaustiveness checker understands, and utilities +-- for working with 'TypedVar's and their names. +module Disco.Exhaustiveness.TypeInfo where + +import Control.Monad (replicateM) +import Data.Function (on) +import Data.List ((\\)) +import qualified Data.Map as M +import Disco.AST.Typed (ATerm) +import Disco.Effects.Fresh (Fresh, fresh) +import qualified Disco.Types as Ty +import Polysemy +import Unbound.Generics.LocallyNameless (Name, s2n) + +newtype TypedVar = TypedVar (Name ATerm, Ty.Type) + deriving (Show, Ord) + +instance Eq TypedVar where + TypedVar (n1, _) == TypedVar (n2, _) = n1 == n2 + +getType :: TypedVar -> Ty.Type +getType (TypedVar (_, t)) = t + +data DataCon = DataCon + { dcIdent :: Ident + , dcTypes :: [Ty.Type] + } + deriving (Ord, Show) + +-- This is very important, as we have (sometimes recursive) type aliases +-- Equality of dcTypes doesn't measure equality of dataconstructors, +-- because we could have two different aliases for the same type +-- (And we can't just resolve all aliases up front, because they can be recursive) +instance Eq DataCon where + (==) = (==) `on` dcIdent + +-- The Show instance of 'Ident' should never be used +-- for displaying results to the user. +-- Instead, convert to a proper pattern and use the +-- pretty printer, like in Exhaustiveness.hs +data Ident where + KUnit :: Ident + KBool :: Bool -> Ident + KNat :: Integer -> Ident + KInt :: Integer -> Ident + KPair :: Ident + KCons :: Ident + KNil :: Ident + KChar :: Char -> Ident + KLeft :: Ident + KRight :: Ident + KUnknown :: Ident + deriving (Show, Eq, Ord) + +-- | 'Finite' constructors are used in the LYG checker +-- 'Infinite' constructors are used when reporting +-- examples of uncovered patterns, we only pick out a few of them +data Constructors where + Finite :: [DataCon] -> Constructors + Infinite :: [DataCon] -> Constructors + +unknown :: DataCon +unknown = DataCon {dcIdent = KUnknown, dcTypes = []} + +unit :: DataCon +unit = DataCon {dcIdent = KUnit, dcTypes = []} + +bool :: Bool -> DataCon +bool b = DataCon {dcIdent = KBool b, dcTypes = []} + +natural :: Integer -> DataCon +natural n = DataCon {dcIdent = KNat n, dcTypes = []} + +integer :: Integer -> DataCon +integer z = DataCon {dcIdent = KInt z, dcTypes = []} + +char :: Char -> DataCon +char c = DataCon {dcIdent = KChar c, dcTypes = []} + +cons :: Ty.Type -> Ty.Type -> DataCon +cons tHead tTail = DataCon {dcIdent = KCons, dcTypes = [tHead, tTail]} + +nil :: DataCon +nil = DataCon {dcIdent = KNil, dcTypes = []} + +pair :: Ty.Type -> Ty.Type -> DataCon +pair a b = DataCon {dcIdent = KPair, dcTypes = [a, b]} + +left :: Ty.Type -> DataCon +left tl = DataCon {dcIdent = KLeft, dcTypes = [tl]} + +right :: Ty.Type -> DataCon +right tr = DataCon {dcIdent = KRight, dcTypes = [tr]} + +tyDataCons :: Ty.Type -> Ty.TyDefCtx -> Constructors +tyDataCons ty ctx = tyDataConsHelper $ resolveAlias ty ctx + +-- Type aliases that would cause infinite recursion here are +-- not possible to construct, so we don't have to worry about that. +-- (aka cyclic type definitions are not allowed in Disco) +resolveAlias :: Ty.Type -> Ty.TyDefCtx -> Ty.Type +resolveAlias (Ty.TyUser name args) ctx = case M.lookup name ctx of + Nothing -> error $ show ctx ++ "\nType definition not found for: " ++ show name + Just (Ty.TyDefBody _argNames typeCon) -> resolveAlias (typeCon args) ctx +resolveAlias t _ = t + +-- | Assuming type aliases have been resolved, this +-- function converts Disco types into lists of DataCons +-- that are compatible with the LYG checker. +-- +-- A list of constructors is 'Infinite' if the only way to fully +-- match against the type is with a wildcard or variable pattern. +-- Otherwise, it is 'Finite'. +-- +-- The LYG checker only reads the list of constructors if +-- a type is 'Finite'. From the point of view of the checker, +-- 'Infinite' is a synonym for opaque, and the constructors are discarded. +-- The dataconstructors in an `Infinite` list are only +-- used when generating the 3 positive examples of what +-- you haven't matched against. +-- This will probably need to change a bit when bringing +-- exhaustiveness checking to the new arithmetic patterns. +-- +-- Notice the last case of this function, which a wildcard handling the types: +-- (_ Ty.:->: _) (Ty.TySet _) (Ty.TyBag _) (Ty.TyVar _) +-- (Ty.TySkolem _) (Ty.TyProp) (Ty.TyMap _ _) (Ty.TyGraph _) +-- +-- I believe all of these are impossible to pattern match against +-- with anything other than a wildcard (or variable pattern) in Disco, so they should always +-- be fully covered. But if they are in a pair, for example, Set(Int)*Int, +-- we still need to generate 3 examples of the pair if that Int part isn't covered. +-- So how do we fill the concrete part of Set(Int), (or a generic type "a", or a function, etc.)? +-- I'm calling that 'unknown', and printing an underscore. +-- (Also, I'm using 'Infinite' for reasons metioned above). +tyDataConsHelper :: Ty.Type -> Constructors +tyDataConsHelper (a Ty.:*: b) = Finite [pair a b] +tyDataConsHelper (l Ty.:+: r) = Finite [left l, right r] +tyDataConsHelper t@(Ty.TyList a) = Finite [nil, cons a t] +tyDataConsHelper Ty.TyVoid = Finite [] +tyDataConsHelper Ty.TyUnit = Finite [unit] +tyDataConsHelper Ty.TyBool = Finite [bool True, bool False] +tyDataConsHelper Ty.TyN = Infinite $ map natural [0, 1 ..] +-- Many thanks to this answer and its comment for a convenient way to list the integers +-- https://stackoverflow.com/a/9749957 +tyDataConsHelper Ty.TyZ = Infinite $ map integer $ 0 : [y | x <- [1 ..], y <- [x, -x]] +tyDataConsHelper Ty.TyF = Infinite [] +tyDataConsHelper Ty.TyQ = Infinite [] +-- The Char constructors are all unicode characters, but +-- given in a very particular order that I think will +-- make the most sense for students. +-- Many thanks to Dr. Yorgey for mentioning [minBound .. maxBound] and \\ +tyDataConsHelper Ty.TyC = + Infinite $ + map char $ + alphanum ++ (allUnicodeNicelyOrdered \\ alphanum) + where + allUnicodeNicelyOrdered = [(toEnum 32) .. (toEnum 126)] ++ [(toEnum 161) .. maxBound] ++ [minBound .. (toEnum 31)] ++ [(toEnum 127) .. (toEnum 160)] + alphanum = ['a' .. 'z'] ++ ['A' .. 'Z'] ++ ['0' .. '9'] +tyDataConsHelper _ = Infinite [unknown] + +newName :: (Member Fresh r) => Sem r (Name ATerm) +newName = fresh $ s2n "" + +newVar :: (Member Fresh r) => Ty.Type -> Sem r TypedVar +newVar types = do + names <- newName + return $ TypedVar (names, types) + +newNames :: (Member Fresh r) => Int -> Sem r [Name ATerm] +newNames i = replicateM i newName + +newVars :: (Member Fresh r) => [Ty.Type] -> Sem r [TypedVar] +newVars types = do + names <- newNames (length types) + return $ zipWith (curry TypedVar) names types