From 1a91697f46b7e3aee3fe20cce72efb497a202f94 Mon Sep 17 00:00:00 2001 From: LeitMoth Date: Wed, 10 Jul 2024 20:48:14 -0500 Subject: [PATCH 01/44] hook into eval and build guard tree --- disco.cabal | 1 + src/Disco/Eval.hs | 10 +++++ src/Disco/Exhaustiveness.hs | 79 +++++++++++++++++++++++++++++++++++++ 3 files changed, 90 insertions(+) create mode 100644 src/Disco/Exhaustiveness.hs diff --git a/disco.cabal b/disco.cabal index 96787632..283dba29 100644 --- a/disco.cabal +++ b/disco.cabal @@ -445,6 +445,7 @@ library Disco.Value Disco.Error Disco.Eval + Disco.Exhaustiveness Disco.Interpret.CESK Disco.Subst Disco.Typecheck diff --git a/src/Disco/Eval.hs b/src/Disco/Eval.hs index 6e2a490e..4301c0f9 100644 --- a/src/Disco/Eval.hs +++ b/src/Disco/Eval.hs @@ -95,6 +95,8 @@ import Disco.Typecheck (checkModule) import Disco.Typecheck.Util import Disco.Types import Disco.Value +import qualified Data.List.NonEmpty as NonEmpty +import Disco.Exhaustiveness (checkClauses) ------------------------------------------------------------ -- Configuation options @@ -384,6 +386,9 @@ 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 + runFresh $ mapM_ checkExhaustive $ (Ctx.elems $ m^.miTermdefs) + -- Evaluate all the module definitions and add them to the topEnv. mapError EvalErr $ loadDefsFrom m @@ -443,3 +448,8 @@ loadDef :: loadDef x body = do v <- inputToState @TopInfo . inputTopEnv $ eval body modify @TopInfo $ topEnv %~ Ctx.insert x v + +checkExhaustive :: Members '[Fresh, Embed IO] r => Defn -> Sem r () +checkExhaustive (Defn name argsType _ boundClauses) = do + clauses <- NonEmpty.map fst <$> mapM unbind boundClauses + checkClauses clauses diff --git a/src/Disco/Exhaustiveness.hs b/src/Disco/Exhaustiveness.hs new file mode 100644 index 00000000..b14707fb --- /dev/null +++ b/src/Disco/Exhaustiveness.hs @@ -0,0 +1,79 @@ +module Disco.Exhaustiveness where + +import Control.Monad (replicateM, zipWithM) +import Data.List.NonEmpty (NonEmpty) +import qualified Data.List.NonEmpty as NonEmpty +import Disco.AST.Generic (Pattern_ (..), X_PVar) +import Disco.AST.Typed (APattern, ATerm) +import Disco.Effects.Fresh (Fresh, fresh) +import Disco.Types (Type) +import Polysemy +import Text.Show.Pretty (pPrint) +import Unbound.Generics.LocallyNameless (Name, s2n, unembed) + +checkClauses :: (Members '[Fresh, Embed IO] r) => NonEmpty [APattern] -> Sem r () +checkClauses pats = do + cl <- zipWithM desugarClause [1 ..] (NonEmpty.toList pats) + let gdt = foldr1 Branch cl + + embed $ pPrint gdt + +-- TODO: should these really just be blank names? +newName :: (Member Fresh r) => Sem r (Name ATerm) +newName = fresh $ s2n "" + +newNames :: (Member Fresh r) => Int -> Sem r [Name ATerm] +newNames i = replicateM i newName + +desugarClause :: (Member Fresh r) => Int -> [APattern] -> Sem r Gdt +desugarClause clauseIdx args = do + names <- newNames (length args) + guards <- zipWithM desugarMatch names args + return $ foldr Guarded (Grhs clauseIdx) $ concat guards + +desugarMatch :: (Member Fresh r) => Name ATerm -> APattern -> Sem r [Guard] +desugarMatch var pat = do + case pat of + (PWild_ _) -> return [] + (PVar_ ty name) -> do + return $ [(var, Let name (unembed ty))] + (PNat_ _ nat) -> return [(var, Nat nat)] + (PUnit_ _) -> return [(var, DataCon Unit)] + (PBool_ _ b) -> return [(var, DataCon $ Bool b)] + (PTup_ _ subs) -> do + names <- newNames (length subs) + guards <- sequence $ zipWith desugarMatch names subs + return $ (var, (DataCon (Tuple names))) : concat guards + (PList_ _ subs) -> do + names <- newNames (length subs) + guards <- sequence $ zipWith desugarMatch names subs + return $ (var, (DataCon (List names))) : concat guards + (PCons_ _ subHead subTail) -> do + nameHead <- newName + nameTail <- newName + guardsHead <- desugarMatch nameHead subHead + guardsTail <- desugarMatch nameTail subTail + return $ (var, (DataCon (Cons nameHead nameTail))) : guardsHead ++ guardsTail + e -> return [] + +data Gdt where + Grhs :: Int -> Gdt + Branch :: Gdt -> Gdt -> Gdt + Guarded :: Guard -> Gdt -> Gdt + deriving (Show, Eq) + +type Guard = (Name ATerm, GuardConstraint) + +data GuardConstraint where + DataCon :: DataCon -> GuardConstraint + Nat :: Integer -> GuardConstraint + Let :: Name ATerm -> Type -> GuardConstraint + deriving (Show, Eq) + +data DataCon where + Unit :: DataCon + Bool :: Bool -> DataCon + Tuple :: [Name ATerm] -> DataCon + List :: [Name ATerm] -> DataCon + Cons :: Name ATerm -> Name ATerm -> DataCon + deriving (Show, Eq) From d1a0c3460a6008bbe8ca952bc98f565184f6f53f Mon Sep 17 00:00:00 2001 From: LeitMoth Date: Mon, 15 Jul 2024 18:06:22 -0500 Subject: [PATCH 02/44] massive mess, decided to keep around my own TypeInfo --- disco.cabal | 1 + src/Disco/Eval.hs | 2 +- src/Disco/Exhaustiveness.hs | 263 +++++++++++++++++++++++---- src/Disco/Exhaustiveness/TypeInfo.hs | 55 ++++++ 4 files changed, 288 insertions(+), 33 deletions(-) create mode 100644 src/Disco/Exhaustiveness/TypeInfo.hs diff --git a/disco.cabal b/disco.cabal index 283dba29..238e3451 100644 --- a/disco.cabal +++ b/disco.cabal @@ -446,6 +446,7 @@ library Disco.Error Disco.Eval Disco.Exhaustiveness + Disco.Exhaustiveness.TypeInfo Disco.Interpret.CESK Disco.Subst Disco.Typecheck diff --git a/src/Disco/Eval.hs b/src/Disco/Eval.hs index 4301c0f9..945c492a 100644 --- a/src/Disco/Eval.hs +++ b/src/Disco/Eval.hs @@ -452,4 +452,4 @@ loadDef x body = do checkExhaustive :: Members '[Fresh, Embed IO] r => Defn -> Sem r () checkExhaustive (Defn name argsType _ boundClauses) = do clauses <- NonEmpty.map fst <$> mapM unbind boundClauses - checkClauses clauses + checkClauses argsType clauses diff --git a/src/Disco/Exhaustiveness.hs b/src/Disco/Exhaustiveness.hs index b14707fb..338cf17a 100644 --- a/src/Disco/Exhaustiveness.hs +++ b/src/Disco/Exhaustiveness.hs @@ -1,22 +1,39 @@ +{-# LANGUAGE PatternSynonyms #-} + module Disco.Exhaustiveness where import Control.Monad (replicateM, zipWithM) +import Control.Monad.Trans.Maybe (MaybeT (MaybeT), runMaybeT) import Data.List.NonEmpty (NonEmpty) import qualified Data.List.NonEmpty as NonEmpty import Disco.AST.Generic (Pattern_ (..), X_PVar) -import Disco.AST.Typed (APattern, ATerm) +import Disco.AST.Typed + ( APattern, + ATerm, + pattern APBool, + pattern APCons, + pattern APList, + pattern APNat, + pattern APTup, + pattern APUnit, + pattern APVar, + pattern APWild, + ) import Disco.Effects.Fresh (Fresh, fresh) -import Disco.Types (Type) +import qualified Disco.Exhaustiveness.TypeInfo as TI +import qualified Disco.Types as Ty import Polysemy import Text.Show.Pretty (pPrint) import Unbound.Generics.LocallyNameless (Name, s2n, unembed) -checkClauses :: (Members '[Fresh, Embed IO] r) => NonEmpty [APattern] -> Sem r () -checkClauses pats = do - cl <- zipWithM desugarClause [1 ..] (NonEmpty.toList pats) +checkClauses :: (Members '[Fresh, Embed IO] r) => [Ty.Type] -> NonEmpty [APattern] -> Sem r () +checkClauses types pats = do + let relTypes = map TI.extractRelevant types + cl <- zipWithM (desugarClause relTypes) [1 ..] (NonEmpty.toList pats) let gdt = foldr1 Branch cl embed $ pPrint gdt + return () -- TODO: should these really just be blank names? newName :: (Member Fresh r) => Sem r (Name ATerm) @@ -25,35 +42,54 @@ newName = fresh $ s2n "" newNames :: (Member Fresh r) => Int -> Sem r [Name ATerm] newNames i = replicateM i newName -desugarClause :: (Member Fresh r) => Int -> [APattern] -> Sem r Gdt -desugarClause clauseIdx args = do +desugarClause :: (Members '[Fresh, Embed IO] r) => [TI.Type] -> Int -> [APattern] -> Sem r Gdt +desugarClause types clauseIdx args = do names <- newNames (length args) - guards <- zipWithM desugarMatch names args + -- embed $ putStr "YO: " + -- embed $ pPrint names + guards <- zipWithM desugarMatch (zip names types) args return $ foldr Guarded (Grhs clauseIdx) $ concat guards -desugarMatch :: (Member Fresh r) => Name ATerm -> APattern -> Sem r [Guard] +type TypedVar = (Name ATerm, TI.Type) + +-- maybe `varsBound` will be useful later? + +desugarMatch :: (Members '[Fresh, Embed IO] r) => TypedVar -> APattern -> Sem r [Guard] desugarMatch var pat = do case pat of - (PWild_ _) -> return [] - (PVar_ ty name) -> do - return $ [(var, Let name (unembed ty))] - (PNat_ _ nat) -> return [(var, Nat nat)] - (PUnit_ _) -> return [(var, DataCon Unit)] - (PBool_ _ b) -> return [(var, DataCon $ Bool b)] - (PTup_ _ subs) -> do + (APWild _) -> return [] + (APVar ty name) -> do + return $ [(var, MakeAlias (name, TI.extractRelevant ty))] + (APNat _ nat) -> return [(var, Nat nat)] + (APUnit) -> return [(var, DataCon KUnit)] + (APBool b) -> return [(var, DataCon $ Bool b)] + (APTup _ subs) -> do + embed $ putStr "TUP: " + embed $ pPrint subs + let types = map (TI.extractRelevant . Ty.getType) subs names <- newNames (length subs) - guards <- sequence $ zipWith desugarMatch names subs - return $ (var, (DataCon (Tuple names))) : concat guards - (PList_ _ subs) -> do + let vars = zip names types + guards <- sequence $ zipWith desugarMatch vars subs + return $ (var, (DataCon (Tuple vars))) : concat guards + (APList _ subs) -> do + embed $ putStr "List: " + embed $ pPrint subs + let types = map (TI.extractRelevant . Ty.getType) subs names <- newNames (length subs) - guards <- sequence $ zipWith desugarMatch names subs - return $ (var, (DataCon (List names))) : concat guards - (PCons_ _ subHead subTail) -> do + let vars = zip names types + guards <- sequence $ zipWith desugarMatch vars subs + return $ (var, (DataCon (List vars))) : concat guards + (APCons _ subHead subTail) -> do + embed $ putStr "Cons: " + embed $ pPrint (subHead, subTail) nameHead <- newName + let varHead = (nameHead, (TI.extractRelevant . Ty.getType) subHead) nameTail <- newName - guardsHead <- desugarMatch nameHead subHead - guardsTail <- desugarMatch nameTail subTail - return $ (var, (DataCon (Cons nameHead nameTail))) : guardsHead ++ guardsTail + let varTail = (nameTail, (TI.extractRelevant . Ty.getType) subTail) + guardsHead <- desugarMatch varHead subHead + guardsTail <- desugarMatch varTail subTail + return $ (var, (DataCon (Cons varHead varTail))) : guardsHead ++ guardsTail + -- (APAdd) e -> return [] data Gdt where @@ -62,18 +98,181 @@ data Gdt where Guarded :: Guard -> Gdt -> Gdt deriving (Show, Eq) -type Guard = (Name ATerm, GuardConstraint) +type Guard = (TypedVar, GuardConstraint) data GuardConstraint where DataCon :: DataCon -> GuardConstraint Nat :: Integer -> GuardConstraint - Let :: Name ATerm -> Type -> GuardConstraint + MakeAlias :: TypedVar -> GuardConstraint deriving (Show, Eq) data DataCon where - Unit :: DataCon + KUnit :: DataCon Bool :: Bool -> DataCon - Tuple :: [Name ATerm] -> DataCon - List :: [Name ATerm] -> DataCon - Cons :: Name ATerm -> Name ATerm -> DataCon - deriving (Show, Eq) + Tuple :: [TypedVar] -> DataCon + List :: [TypedVar] -> DataCon + Cons :: TypedVar -> TypedVar -> DataCon + deriving (Show, Eq, Ord) + +data DataConName = NUnit | NBool Bool | NTuple | NList | NCons + deriving (Show, Eq, Ord) + +getName :: DataCon -> DataConName +getName KUnit = NUnit +getName (Bool b) = NBool b +getName (Tuple _) = NTuple +getName (List _) = NList +getName (Cons _ _) = NCons + +data Literal where + T :: Literal + F :: Literal + LitCond :: (TypedVar, LitCond) -> Literal + deriving (Show, Eq, Ord) + +data LitCond where + Is :: DataCon -> LitCond + Not :: DataConName -> LitCond + IsInt :: Integer -> LitCond + NotInt :: Integer -> LitCond + LitMakeAlias :: TypedVar -> LitCond + deriving (Show, Eq, Ord) + +type NormRefType = (Context, [ConstraintFor]) + +type ConstraintFor = (Name ATerm, Constraint) + +type Context = [TypedVar] + +data Constraint where + CIs :: DataCon -> Constraint + CNot :: DataConName -> Constraint + CIsInt :: Integer -> Constraint + CNotInt :: Integer -> Constraint + CMakeAlias :: TypedVar -> Constraint + deriving (Show, Eq, Ord) + +data Ant where + AGrhs :: [NormRefType] -> Int -> Ant + ABranch :: Ant -> Ant -> Ant + deriving (Show) + +ua :: (Member Fresh r) => [NormRefType] -> Gdt -> Sem r ([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 (x, MakeAlias z) t -> do + n <- addLitMulti nrefs $ LitCond (x, LitMakeAlias z) + ua n t + Guarded (x, (DataCon dc)) t -> do + n <- addLitMulti nrefs $ LitCond (x, Is dc) + (n', u) <- ua n t + n'' <- addLitMulti nrefs $ LitCond (x, Not $ getName dc) + return (n'' ++ n', u) + Guarded (x, (Nat i)) t -> do + n <- addLitMulti nrefs $ LitCond (x, IsInt i) + (n', u) <- ua n t + n'' <- addLitMulti nrefs $ LitCond (x, NotInt i) + return (n'' ++ n', u) + +addLitMulti :: (Members '[Fresh] r) => [NormRefType] -> Literal -> Sem r [NormRefType] +addLitMulti [] _ = return [] +addLitMulti (n : ns) lit = do + r <- runMaybeT $ addLiteral n lit + case r of + Nothing -> addLitMulti ns lit + Just (ctx, cfs) -> do + ns' <- addLitMulti ns lit + return $ (ctx, cfs) : ns' + +redundantNorm :: (Member Fresh r) => Ant -> Context -> Sem r [Int] +redundantNorm ant args = case ant of + AGrhs ref i -> do + inhabited <- null <$> genInhabNorm ref args + return [i | inhabited] + ABranch a1 a2 -> mappend <$> redundantNorm a1 args <*> redundantNorm a2 args + +addLiteral :: (Members '[Fresh] r) => NormRefType -> Literal -> MaybeT (Sem r) NormRefType +addLiteral n@(context, constraints) flit = case flit of + F -> MaybeT $ pure Nothing + T -> return n + LitCond (x, c) -> case c of + LitMakeAlias z -> (n <> ([z], [])) `addConstraint` (x, CMakeAlias z) + NotInt i -> n `addConstraint` (x, CNotInt i) + IsInt i -> n `addConstraint` (x, CIsInt i) + Not dc -> n `addConstraint` (x, CNot dc) + Is dc -> case dc of + KUnit -> n `addConstraint` (x, CIs dc) + Bool b -> n `addConstraint` (x, CIs $ Bool b) + +-- Tuple types names -> (context ++ zip names types, constraints) `addConstraint` (x, CIs $ Tuple names) +-- List :: [Name ATerm] -> DataCon +-- Cons :: Name ATerm -> Name ATerm -> DataCon + +-- MatchDataCon k ys x -> (context ++ zip ys (Ty.dcTypes k), constraints) `addConstraint` (x, MatchDataCon k ys) +-- NotDataCon k x -> n `addConstraint` (x, NotDataCon k) + +{- +genInhabNorm :: Members '[Fresh] r => [NormRefType] -> Context -> Sem r (Poss.Possibilities InhabPat) +genInhabNorm nrefs args = do + n <- sequence [findVarInhabitants arg nref | nref <- nrefs, arg <- args] + return $ Poss.anyOf n + +-- Sanity check: are we giving the dataconstructor the +-- correct number of arguments? +mkIPMatch :: Ty.DataConstructor -> [InhabPat] -> InhabPat +mkIPMatch k pats = + if length (Ty.dcTypes k) /= length pats + then error $ "Wrong number of DataCon args" ++ show (k, pats) + else IPIs k pats + +findVarInhabitants :: TypedVar -> NormRefType -> F.Fresh (Poss.Possibilities InhabPat) +findVarInhabitants var nref@(_, cns) = + case posMatch of + Just (k, args) -> do + argPats <- forM args (`findVarInhabitants` nref) + let argPossibilities = Poss.allCombinations argPats + + return (mkIPMatch k <$> argPossibilities) + Nothing -> case nub negMatch of + [] -> Poss.retSingle $ IPNot [] + neg -> + case getDataCons var of + Nothing -> Poss.retSingle $ IPNot neg + Just dcs -> + do + let tryAddDc dc = do + newVars <- mkNewVars (Ty.dcTypes dc) + runMaybeT (nref `addConstraint` (var, MatchInfo $ Match dc newVars)) + + -- 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 = onVar var cns + posMatch = listToMaybe $ mapMaybe (\case MatchInfo (Match k ys) -> Just (k, ys); _ -> Nothing) constraintsOnX + negMatch = mapMaybe (\case MatchInfo (Not k) -> Just k; _ -> Nothing) constraintsOnX + +normalize :: NormRefType -> U.Formula -> F.Fresh (S.Set NormRefType) +normalize nref (f1 `U.And` f2) = do + n1 <- S.toList <$> normalize nref f1 + rest <- traverse (`normalize` f2) n1 + return $ S.unions rest +normalize nref (f1 `U.Or` f2) = S.union <$> normalize nref f1 <*> normalize nref f2 +normalize nref (U.Literal fl) = maybe S.empty S.singleton <$> runMaybeT (nref `addLiteral` fl) +-} + +addConstraint a b = undefined + +genInhabNorm a b = undefined + +genInhabNorm :: p1 -> p2 -> Sem r [Int] diff --git a/src/Disco/Exhaustiveness/TypeInfo.hs b/src/Disco/Exhaustiveness/TypeInfo.hs new file mode 100644 index 00000000..ccbe3dcb --- /dev/null +++ b/src/Disco/Exhaustiveness/TypeInfo.hs @@ -0,0 +1,55 @@ +module Disco.Exhaustiveness.TypeInfo where + +import qualified Disco.Types as Ty + +data Type = Type + { tyIdent :: Ty.Type, + tyDataCons :: Maybe [DataCon] -- Set to Nothing for opaque types + } + deriving (Eq, Ord, Show) + +data DataCon = DataCon + { dcIdent :: Ident, + dcTypes :: [Type] + } + deriving (Eq, Ord, Show) + +data Ident where + KBool :: Bool -> Ident + KUnit :: Ident + KDummy :: Ident + deriving (Eq, Ord, Show) + +data TypeName = TBool | TUnit | TPair | TEither | TInt | TThrool + deriving (Eq, Ord, Show) + +extractRelevant :: Ty.Type -> Type +-- extractRelevant Ty.TyVoid = Just [] +-- extractRelevant (a Ty.:*: b) = enumProd (enumType a) (enumType b) +-- extractRelevant (a Ty.:+: b) = enumSum (enumType a) (enumType b) +-- extractRelevant (a Ty.:->: b) = enumFunction (enumType a) (enumType b) +-- extractRelevant (Ty.TySet t) = ? +-- extractRelevant (Ty.TyList t) = ? +extractRelevant Ty.TyBool = + Type + { tyIdent = Ty.TyBool, + tyDataCons = + Just + [ DataCon {dcIdent = KBool True, dcTypes = []}, + DataCon {dcIdent = KBool False, dcTypes = []} + ] + } +extractRelevant Ty.TyUnit = + Type + { tyIdent = Ty.TyUnit, + tyDataCons = + Just + [DataCon {dcIdent = KUnit, dcTypes = []}] + } +extractRelevant t@Ty.TyN = Type {tyIdent = t, tyDataCons = Nothing} +extractRelevant t@Ty.TyZ = Type {tyIdent = t, tyDataCons = Nothing} +extractRelevant t@Ty.TyF = Type {tyIdent = t, tyDataCons = Nothing} +extractRelevant t@Ty.TyQ = Type {tyIdent = t, tyDataCons = Nothing} +extractRelevant t@Ty.TyC = Type {tyIdent = t, tyDataCons = Nothing} +extractRelevant t = Type {tyIdent = t, tyDataCons = Nothing} +-- extractRelevant ty = error $ "Bad type in exhaust" ++ show ty From c6ab2011cb52e3bb493ca0cf693d446eedd9dcc8 Mon Sep 17 00:00:00 2001 From: LeitMoth Date: Mon, 15 Jul 2024 20:28:14 -0500 Subject: [PATCH 03/44] port over inhabpat generation + mostly finish up TypeInfo. constraints next --- disco.cabal | 1 + src/Disco/Exhaustiveness.hs | 149 ++++++++++------------ src/Disco/Exhaustiveness/Possibilities.hs | 64 ++++++++++ src/Disco/Exhaustiveness/TypeInfo.hs | 61 +++++++-- 4 files changed, 186 insertions(+), 89 deletions(-) create mode 100644 src/Disco/Exhaustiveness/Possibilities.hs diff --git a/disco.cabal b/disco.cabal index 238e3451..b03efc5e 100644 --- a/disco.cabal +++ b/disco.cabal @@ -447,6 +447,7 @@ library Disco.Eval Disco.Exhaustiveness Disco.Exhaustiveness.TypeInfo + Disco.Exhaustiveness.Possibilities Disco.Interpret.CESK Disco.Subst Disco.Typecheck diff --git a/src/Disco/Exhaustiveness.hs b/src/Disco/Exhaustiveness.hs index 338cf17a..7ac39dfb 100644 --- a/src/Disco/Exhaustiveness.hs +++ b/src/Disco/Exhaustiveness.hs @@ -2,11 +2,10 @@ module Disco.Exhaustiveness where -import Control.Monad (replicateM, zipWithM) +import Control.Monad (replicateM, when, zipWithM, forM) import Control.Monad.Trans.Maybe (MaybeT (MaybeT), runMaybeT) import Data.List.NonEmpty (NonEmpty) import qualified Data.List.NonEmpty as NonEmpty -import Disco.AST.Generic (Pattern_ (..), X_PVar) import Disco.AST.Typed ( APattern, ATerm, @@ -20,11 +19,14 @@ import Disco.AST.Typed pattern APWild, ) import Disco.Effects.Fresh (Fresh, fresh) +import qualified Disco.Exhaustiveness.Possibilities as Poss import qualified Disco.Exhaustiveness.TypeInfo as TI import qualified Disco.Types as Ty import Polysemy import Text.Show.Pretty (pPrint) -import Unbound.Generics.LocallyNameless (Name, s2n, unembed) +import Unbound.Generics.LocallyNameless (Name, s2n) +import Data.List (nub) +import Data.Maybe (catMaybes, mapMaybe, listToMaybe) checkClauses :: (Members '[Fresh, Embed IO] r) => [Ty.Type] -> NonEmpty [APattern] -> Sem r () checkClauses types pats = do @@ -42,53 +44,62 @@ newName = fresh $ s2n "" newNames :: (Member Fresh r) => Int -> Sem r [Name ATerm] newNames i = replicateM i newName +newVars :: Member Fresh r => [b] -> Sem r [(Name ATerm, b)] +newVars types = do + names <- newNames (length types) + return $ zip names types + desugarClause :: (Members '[Fresh, Embed IO] r) => [TI.Type] -> Int -> [APattern] -> Sem r Gdt desugarClause types clauseIdx args = do - names <- newNames (length args) + vars <- newVars types -- embed $ putStr "YO: " -- embed $ pPrint names - guards <- zipWithM desugarMatch (zip names types) args + guards <- zipWithM desugarMatch vars args return $ foldr Guarded (Grhs clauseIdx) $ concat guards type TypedVar = (Name ATerm, TI.Type) -- maybe `varsBound` will be useful later? +-- borrowed from `extra` +allSame :: (Eq a) => [a] -> Bool +allSame [] = True +allSame (x : xs) = all (x ==) xs + desugarMatch :: (Members '[Fresh, Embed IO] r) => TypedVar -> APattern -> Sem r [Guard] desugarMatch var pat = do case pat of (APWild _) -> return [] (APVar ty name) -> do - return $ [(var, MakeAlias (name, TI.extractRelevant ty))] - (APNat _ nat) -> return [(var, Nat nat)] - (APUnit) -> return [(var, DataCon KUnit)] - (APBool b) -> return [(var, DataCon $ Bool b)] + return $ [(var, GHerebyBe (name, TI.extractRelevant ty))] + (APNat _ nat) -> return [(var, GMatch (TI.natural nat) [])] + (APUnit) -> return [(var, GMatch TI.unit [])] + (APBool b) -> return [(var, GMatch (TI.bool b) [])] (APTup _ subs) -> do - embed $ putStr "TUP: " - embed $ pPrint subs let types = map (TI.extractRelevant . Ty.getType) subs - names <- newNames (length subs) - let vars = zip names types + vars <- newVars types guards <- sequence $ zipWith desugarMatch vars subs - return $ (var, (DataCon (Tuple vars))) : concat guards + return $ (var, (GMatch (TI.tuple types) vars)) : concat guards (APList _ subs) -> do - embed $ putStr "List: " - embed $ pPrint subs let types = map (TI.extractRelevant . Ty.getType) subs - names <- newNames (length subs) - let vars = zip names types + when + (not . allSame $ types) + (embed . putStrLn $ "WARNING, mismatched types in list!: " ++ show types) + vars <- newVars types guards <- sequence $ zipWith desugarMatch vars subs - return $ (var, (DataCon (List vars))) : concat guards + return $ (var, (GMatch (TI.list types) vars)) : concat guards (APCons _ subHead subTail) -> do embed $ putStr "Cons: " embed $ pPrint (subHead, subTail) nameHead <- newName - let varHead = (nameHead, (TI.extractRelevant . Ty.getType) subHead) nameTail <- newName - let varTail = (nameTail, (TI.extractRelevant . Ty.getType) subTail) + let typeHead = (TI.extractRelevant . Ty.getType) subHead + let typeTail = (TI.extractRelevant . Ty.getType) subTail + let varHead = (nameHead, typeHead) + let varTail = (nameTail, typeTail) guardsHead <- desugarMatch varHead subHead guardsTail <- desugarMatch varTail subTail - return $ (var, (DataCon (Cons varHead varTail))) : guardsHead ++ guardsTail + return $ (var, (GMatch (TI.cons typeHead typeTail) [varHead, varTail])) : guardsHead ++ guardsTail -- (APAdd) e -> return [] @@ -101,9 +112,8 @@ data Gdt where type Guard = (TypedVar, GuardConstraint) data GuardConstraint where - DataCon :: DataCon -> GuardConstraint - Nat :: Integer -> GuardConstraint - MakeAlias :: TypedVar -> GuardConstraint + GMatch :: TI.DataCon -> [TypedVar] -> GuardConstraint + GHerebyBe :: TypedVar -> GuardConstraint deriving (Show, Eq) data DataCon where @@ -131,25 +141,21 @@ data Literal where deriving (Show, Eq, Ord) data LitCond where - Is :: DataCon -> LitCond - Not :: DataConName -> LitCond - IsInt :: Integer -> LitCond - NotInt :: Integer -> LitCond - LitMakeAlias :: TypedVar -> LitCond + LitMatch :: TI.DataCon -> [TypedVar] -> LitCond + LitNot :: TI.DataCon -> LitCond + LitHerebyBe :: TypedVar -> LitCond deriving (Show, Eq, Ord) type NormRefType = (Context, [ConstraintFor]) -type ConstraintFor = (Name ATerm, Constraint) +type ConstraintFor = (TypedVar, Constraint) type Context = [TypedVar] data Constraint where - CIs :: DataCon -> Constraint - CNot :: DataConName -> Constraint - CIsInt :: Integer -> Constraint - CNotInt :: Integer -> Constraint - CMakeAlias :: TypedVar -> Constraint + CMatch :: TI.DataCon -> [TypedVar] -> Constraint + CNot :: TI.DataCon -> Constraint + CHerebyBe :: TypedVar -> Constraint deriving (Show, Eq, Ord) data Ant where @@ -164,18 +170,13 @@ ua nrefs gdt = case gdt of (n1, u1) <- ua nrefs t1 (n2, u2) <- ua n1 t2 return (n2, ABranch u1 u2) - Guarded (x, MakeAlias z) t -> do - n <- addLitMulti nrefs $ LitCond (x, LitMakeAlias z) + Guarded (x, GHerebyBe z) t -> do + n <- addLitMulti nrefs $ LitCond (x, LitHerebyBe z) ua n t - Guarded (x, (DataCon dc)) t -> do - n <- addLitMulti nrefs $ LitCond (x, Is dc) + Guarded (x, (GMatch dc args)) t -> do + n <- addLitMulti nrefs $ LitCond (x, LitMatch dc args) (n', u) <- ua n t - n'' <- addLitMulti nrefs $ LitCond (x, Not $ getName dc) - return (n'' ++ n', u) - Guarded (x, (Nat i)) t -> do - n <- addLitMulti nrefs $ LitCond (x, IsInt i) - (n', u) <- ua n t - n'' <- addLitMulti nrefs $ LitCond (x, NotInt i) + n'' <- addLitMulti nrefs $ LitCond (x, LitNot dc) return (n'' ++ n', u) addLitMulti :: (Members '[Fresh] r) => [NormRefType] -> Literal -> Sem r [NormRefType] @@ -191,7 +192,7 @@ addLitMulti (n : ns) lit = do redundantNorm :: (Member Fresh r) => Ant -> Context -> Sem r [Int] redundantNorm ant args = case ant of AGrhs ref i -> do - inhabited <- null <$> genInhabNorm ref args + inhabited <- null <$> genInhab ref args return [i | inhabited] ABranch a1 a2 -> mappend <$> redundantNorm a1 args <*> redundantNorm a2 args @@ -200,13 +201,9 @@ addLiteral n@(context, constraints) flit = case flit of F -> MaybeT $ pure Nothing T -> return n LitCond (x, c) -> case c of - LitMakeAlias z -> (n <> ([z], [])) `addConstraint` (x, CMakeAlias z) - NotInt i -> n `addConstraint` (x, CNotInt i) - IsInt i -> n `addConstraint` (x, CIsInt i) - Not dc -> n `addConstraint` (x, CNot dc) - Is dc -> case dc of - KUnit -> n `addConstraint` (x, CIs dc) - Bool b -> n `addConstraint` (x, CIs $ Bool b) + LitHerebyBe z -> (n <> ([z], [])) `addConstraint` (x, CHerebyBe z) + LitMatch dc args -> (n <> (args, [])) `addConstraint` (x, CMatch dc args) + LitNot dc -> n `addConstraint` (x, CNot dc) -- Tuple types names -> (context ++ zip names types, constraints) `addConstraint` (x, CIs $ Tuple names) -- List :: [Name ATerm] -> DataCon @@ -215,21 +212,25 @@ addLiteral n@(context, constraints) flit = case flit of -- MatchDataCon k ys x -> (context ++ zip ys (Ty.dcTypes k), constraints) `addConstraint` (x, MatchDataCon k ys) -- NotDataCon k x -> n `addConstraint` (x, NotDataCon k) -{- -genInhabNorm :: Members '[Fresh] r => [NormRefType] -> Context -> Sem r (Poss.Possibilities InhabPat) -genInhabNorm nrefs args = do +data InhabPat where + IPIs :: TI.DataCon -> [InhabPat] -> InhabPat + IPNot :: [TI.DataCon] -> InhabPat + deriving (Show, Eq, Ord) + +genInhab :: (Members '[Fresh] r) => [NormRefType] -> Context -> Sem r (Poss.Possibilities InhabPat) +genInhab nrefs args = do n <- sequence [findVarInhabitants arg nref | nref <- nrefs, arg <- args] return $ Poss.anyOf n -- Sanity check: are we giving the dataconstructor the -- correct number of arguments? -mkIPMatch :: Ty.DataConstructor -> [InhabPat] -> InhabPat +mkIPMatch :: TI.DataCon -> [InhabPat] -> InhabPat mkIPMatch k pats = - if length (Ty.dcTypes k) /= length pats + if length (TI.dcTypes k) /= length pats then error $ "Wrong number of DataCon args" ++ show (k, pats) else IPIs k pats -findVarInhabitants :: TypedVar -> NormRefType -> F.Fresh (Poss.Possibilities InhabPat) +findVarInhabitants :: (Members '[Fresh] r) => TypedVar -> NormRefType -> Sem r (Poss.Possibilities InhabPat) findVarInhabitants var nref@(_, cns) = case posMatch of Just (k, args) -> do @@ -240,13 +241,13 @@ findVarInhabitants var nref@(_, cns) = Nothing -> case nub negMatch of [] -> Poss.retSingle $ IPNot [] neg -> - case getDataCons var of + case TI.tyDataCons (snd var) of Nothing -> Poss.retSingle $ IPNot neg Just dcs -> do let tryAddDc dc = do - newVars <- mkNewVars (Ty.dcTypes dc) - runMaybeT (nref `addConstraint` (var, MatchInfo $ Match dc newVars)) + vars <- newVars (TI.dcTypes dc) + runMaybeT (nref `addConstraint` (var, CMatch dc vars)) -- Try to add a positive constraint for each data constructor -- to the current nref @@ -259,20 +260,10 @@ findVarInhabitants var nref@(_, cns) = else Poss.anyOf <$> forM posNrefs (findVarInhabitants var) where constraintsOnX = onVar var cns - posMatch = listToMaybe $ mapMaybe (\case MatchInfo (Match k ys) -> Just (k, ys); _ -> Nothing) constraintsOnX - negMatch = mapMaybe (\case MatchInfo (Not k) -> Just k; _ -> Nothing) constraintsOnX - -normalize :: NormRefType -> U.Formula -> F.Fresh (S.Set NormRefType) -normalize nref (f1 `U.And` f2) = do - n1 <- S.toList <$> normalize nref f1 - rest <- traverse (`normalize` f2) n1 - return $ S.unions rest -normalize nref (f1 `U.Or` f2) = S.union <$> normalize nref f1 <*> normalize nref f2 -normalize nref (U.Literal fl) = maybe S.empty S.singleton <$> runMaybeT (nref `addLiteral` fl) --} - -addConstraint a b = undefined - -genInhabNorm a b = undefined + posMatch = listToMaybe $ mapMaybe (\case (CMatch k ys) -> Just (k, ys); _ -> Nothing) constraintsOnX + negMatch = mapMaybe (\case (CNot k) -> Just k; _ -> Nothing) constraintsOnX -genInhabNorm :: p1 -> p2 -> Sem r [Int] +,,,TODO I recommend breaking things up into a "Constraint.hs" file, which imports a "Context.hs" file, in + which we make Context a newtype instead of a alias for a pair, and expose the correct functions + adding constraints shouldn't depend on how the context is implemented + the only weird thing is going to be the substituting all the variables for the herebys diff --git a/src/Disco/Exhaustiveness/Possibilities.hs b/src/Disco/Exhaustiveness/Possibilities.hs new file mode 100644 index 00000000..1e300dee --- /dev/null +++ b/src/Disco/Exhaustiveness/Possibilities.hs @@ -0,0 +1,64 @@ +module Disco.Exhaustiveness.Possibilities (Possibilities, retSingle, allCombinations, anyOf, none, getPossibilities) where + +import Data.Foldable (Foldable (fold)) + +newtype Possibilities a = Possibilities {getPossibilities :: [a]} + deriving (Show, Eq, Ord) + +instance Functor Possibilities where + fmap f (Possibilities a) = Possibilities (f <$> a) + +instance Semigroup (Possibilities a) where + (Possibilities p1) <> (Possibilities p2) = Possibilities $ p1 <> p2 + +instance Monoid (Possibilities a) where + mempty = Possibilities [] + +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 = foldr prod nil + where + -- note, nil /= mempty + -- VERY important + nil = Possibilities [[]] + +prod :: Possibilities a -> Possibilities [a] -> Possibilities [a] +prod (Possibilities xs) (Possibilities yss) = Possibilities [x : ys | x <- xs, ys <- yss] diff --git a/src/Disco/Exhaustiveness/TypeInfo.hs b/src/Disco/Exhaustiveness/TypeInfo.hs index ccbe3dcb..deee774e 100644 --- a/src/Disco/Exhaustiveness/TypeInfo.hs +++ b/src/Disco/Exhaustiveness/TypeInfo.hs @@ -2,6 +2,32 @@ module Disco.Exhaustiveness.TypeInfo where import qualified Disco.Types as Ty +{- + +Motivation: + +Imagine the function + +foo : N * N * N -> Unit +foo (x,y,z) -> unit +foo (x,(y,z)) -> unit + +So, we must make the decision on how we want to report back +the uncovered patterns +I am choosing to preserve the visual structure of what the user put in, +So I must turn these product types into tuples, in order to get +back out a similar pattern. + +I cannot look to Haskell for guidance, as +(Int,Int,Int) /= (Int,(Int,Int)) in Haskell + +Also having convient lists of types and constructors +Makes the algorithm easier to implement +-} + +data TypeName = TBool | TUnit | TPair | TEither | TInt | TThrool + deriving (Eq, Ord, Show) + data Type = Type { tyIdent :: Ty.Type, tyDataCons :: Maybe [DataCon] -- Set to Nothing for opaque types @@ -18,10 +44,30 @@ data Ident where KBool :: Bool -> Ident KUnit :: Ident KDummy :: Ident + KTuple :: Ident + KNat :: Integer -> Ident + KList :: Ident + KCons :: Ident deriving (Eq, Ord, Show) -data TypeName = TBool | TUnit | TPair | TEither | TInt | TThrool - deriving (Eq, Ord, Show) +unit :: DataCon +unit = DataCon {dcIdent = KUnit, dcTypes = []} + +bool :: Bool -> DataCon +bool b = DataCon {dcIdent = KBool b, dcTypes = []} + +tuple :: [Type] -> DataCon +tuple types = DataCon {dcIdent = KTuple, dcTypes = types} + +natural :: Integer -> DataCon +natural n = DataCon {dcIdent = KNat n, dcTypes = []} + +-- Don't mix and match types here, +-- we are going on the honor system +list :: [Type] -> DataCon +list types = DataCon {dcIdent = KList, dcTypes = types } + +cons tHead tTail = DataCon {dcIdent = KCons, dcTypes = [tHead, tTail]} extractRelevant :: Ty.Type -> Type -- extractRelevant Ty.TyVoid = Just [] @@ -33,18 +79,12 @@ extractRelevant :: Ty.Type -> Type extractRelevant Ty.TyBool = Type { tyIdent = Ty.TyBool, - tyDataCons = - Just - [ DataCon {dcIdent = KBool True, dcTypes = []}, - DataCon {dcIdent = KBool False, dcTypes = []} - ] + tyDataCons = Just [bool True, bool False] } extractRelevant Ty.TyUnit = Type { tyIdent = Ty.TyUnit, - tyDataCons = - Just - [DataCon {dcIdent = KUnit, dcTypes = []}] + tyDataCons = Just [unit] } extractRelevant t@Ty.TyN = Type {tyIdent = t, tyDataCons = Nothing} extractRelevant t@Ty.TyZ = Type {tyIdent = t, tyDataCons = Nothing} @@ -52,4 +92,5 @@ extractRelevant t@Ty.TyF = Type {tyIdent = t, tyDataCons = Nothing} extractRelevant t@Ty.TyQ = Type {tyIdent = t, tyDataCons = Nothing} extractRelevant t@Ty.TyC = Type {tyIdent = t, tyDataCons = Nothing} extractRelevant t = Type {tyIdent = t, tyDataCons = Nothing} + -- extractRelevant ty = error $ "Bad type in exhaust" ++ show ty From 86190d33c4ca089b3936c0099d7101c20812ef2c Mon Sep 17 00:00:00 2001 From: LeitMoth Date: Wed, 17 Jul 2024 19:47:51 -0500 Subject: [PATCH 04/44] kind of works, pairs super broken --- disco.cabal | 3 +- src/Disco/Exhaustiveness.hs | 217 ++++++++++++------------- src/Disco/Exhaustiveness/Constraint.hs | 143 ++++++++++++++++ src/Disco/Exhaustiveness/TypeInfo.hs | 52 +++++- 4 files changed, 295 insertions(+), 120 deletions(-) create mode 100644 src/Disco/Exhaustiveness/Constraint.hs diff --git a/disco.cabal b/disco.cabal index b03efc5e..ab9295bb 100644 --- a/disco.cabal +++ b/disco.cabal @@ -446,8 +446,9 @@ library Disco.Error Disco.Eval Disco.Exhaustiveness - Disco.Exhaustiveness.TypeInfo + Disco.Exhaustiveness.Constraint Disco.Exhaustiveness.Possibilities + Disco.Exhaustiveness.TypeInfo Disco.Interpret.CESK Disco.Subst Disco.Typecheck diff --git a/src/Disco/Exhaustiveness.hs b/src/Disco/Exhaustiveness.hs index 7ac39dfb..2e41e068 100644 --- a/src/Disco/Exhaustiveness.hs +++ b/src/Disco/Exhaustiveness.hs @@ -2,10 +2,12 @@ module Disco.Exhaustiveness where -import Control.Monad (replicateM, when, zipWithM, forM) +import Control.Monad (forM, replicateM, when, zipWithM) import Control.Monad.Trans.Maybe (MaybeT (MaybeT), runMaybeT) +import Data.List (nub) import Data.List.NonEmpty (NonEmpty) import qualified Data.List.NonEmpty as NonEmpty +import Data.Maybe (catMaybes, listToMaybe, mapMaybe) import Disco.AST.Typed ( APattern, ATerm, @@ -19,65 +21,72 @@ import Disco.AST.Typed pattern APWild, ) import Disco.Effects.Fresh (Fresh, fresh) +import qualified Disco.Exhaustiveness.Constraint as C import qualified Disco.Exhaustiveness.Possibilities as Poss import qualified Disco.Exhaustiveness.TypeInfo as TI import qualified Disco.Types as Ty import Polysemy import Text.Show.Pretty (pPrint) import Unbound.Generics.LocallyNameless (Name, s2n) -import Data.List (nub) -import Data.Maybe (catMaybes, mapMaybe, listToMaybe) checkClauses :: (Members '[Fresh, Embed IO] r) => [Ty.Type] -> NonEmpty [APattern] -> Sem r () checkClauses types pats = do - let relTypes = map TI.extractRelevant types - cl <- zipWithM (desugarClause relTypes) [1 ..] (NonEmpty.toList pats) + args <- TI.newVars (map TI.extractRelevant types) + cl <- zipWithM (desugarClause args) [1 ..] (NonEmpty.toList pats) let gdt = foldr1 Branch cl - embed $ pPrint gdt - return () + let argsNref = (C.Context args, []) + (normalizedNrefs, annotated) <- ua [argsNref] gdt --- TODO: should these really just be blank names? -newName :: (Member Fresh r) => Sem r (Name ATerm) -newName = fresh $ s2n "" + inhab <- Poss.getPossibilities <$> findInhabitants normalizedNrefs args -newNames :: (Member Fresh r) => Int -> Sem r [Name ATerm] -newNames i = replicateM i newName + redundant <- findRedundant annotated args -newVars :: Member Fresh r => [b] -> Sem r [(Name ATerm, b)] -newVars types = do - names <- newNames (length types) - return $ zip names types + when False $ do + embed $ putStrLn "=====DEBUG==============================" + embed $ putStrLn "GDT:" + embed $ pPrint gdt + embed $ putStrLn "UNCOVERED:" + embed $ pPrint inhab + embed $ putStrLn "REDUNDANT:" + embed $ pPrint redundant + embed $ putStrLn "=====GUBED==============================" -desugarClause :: (Members '[Fresh, Embed IO] r) => [TI.Type] -> Int -> [APattern] -> Sem r Gdt -desugarClause types clauseIdx args = do - vars <- newVars types - -- embed $ putStr "YO: " - -- embed $ pPrint names - guards <- zipWithM desugarMatch vars args - return $ foldr Guarded (Grhs clauseIdx) $ concat guards + let jspace = foldr (\a b -> a ++ " " ++ b) "" -type TypedVar = (Name ATerm, TI.Type) + when (not . null $ inhab) $ do + embed $ putStrLn "Warning: You haven't matched against:" + embed $ mapM_ (putStrLn . jspace . map prettyInhab) inhab + -- embed $ mapM_ (putStrLn . show) inhab --- maybe `varsBound` will be useful later? + when (not . null $ redundant) $ do + embed $ putStrLn "Warning: These clause numbers (1-indexed) are redundant" + embed $ putStrLn $ show redundant + + return () + +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 -- borrowed from `extra` allSame :: (Eq a) => [a] -> Bool allSame [] = True allSame (x : xs) = all (x ==) xs -desugarMatch :: (Members '[Fresh, Embed IO] r) => TypedVar -> APattern -> Sem r [Guard] +desugarMatch :: (Members '[Fresh, Embed IO] r) => TI.TypedVar -> APattern -> Sem r [Guard] desugarMatch var pat = do case pat of (APWild _) -> return [] (APVar ty name) -> do - return $ [(var, GHerebyBe (name, TI.extractRelevant ty))] + return $ [(var, GHerebyBe $ TI.TypedVar (name, TI.extractRelevant ty))] (APNat _ nat) -> return [(var, GMatch (TI.natural nat) [])] (APUnit) -> return [(var, GMatch TI.unit [])] (APBool b) -> return [(var, GMatch (TI.bool b) [])] (APTup _ subs) -> do let types = map (TI.extractRelevant . Ty.getType) subs - vars <- newVars types + vars <- TI.newVars types guards <- sequence $ zipWith desugarMatch vars subs return $ (var, (GMatch (TI.tuple types) vars)) : concat guards (APList _ subs) -> do @@ -85,18 +94,18 @@ desugarMatch var pat = do when (not . allSame $ types) (embed . putStrLn $ "WARNING, mismatched types in list!: " ++ show types) - vars <- newVars types + vars <- TI.newVars types guards <- sequence $ zipWith desugarMatch vars subs return $ (var, (GMatch (TI.list types) vars)) : concat guards (APCons _ subHead subTail) -> do embed $ putStr "Cons: " embed $ pPrint (subHead, subTail) - nameHead <- newName - nameTail <- newName + nameHead <- TI.newName + nameTail <- TI.newName let typeHead = (TI.extractRelevant . Ty.getType) subHead let typeTail = (TI.extractRelevant . Ty.getType) subTail - let varHead = (nameHead, typeHead) - let varTail = (nameTail, typeTail) + let varHead = TI.TypedVar (nameHead, typeHead) + let varTail = TI.TypedVar (nameTail, typeTail) guardsHead <- desugarMatch varHead subHead guardsTail <- desugarMatch varTail subTail return $ (var, (GMatch (TI.cons typeHead typeTail) [varHead, varTail])) : guardsHead ++ guardsTail @@ -109,61 +118,31 @@ data Gdt where Guarded :: Guard -> Gdt -> Gdt deriving (Show, Eq) -type Guard = (TypedVar, GuardConstraint) +type Guard = (TI.TypedVar, GuardConstraint) data GuardConstraint where - GMatch :: TI.DataCon -> [TypedVar] -> GuardConstraint - GHerebyBe :: TypedVar -> GuardConstraint + GMatch :: TI.DataCon -> [TI.TypedVar] -> GuardConstraint + GHerebyBe :: TI.TypedVar -> GuardConstraint deriving (Show, Eq) -data DataCon where - KUnit :: DataCon - Bool :: Bool -> DataCon - Tuple :: [TypedVar] -> DataCon - List :: [TypedVar] -> DataCon - Cons :: TypedVar -> TypedVar -> DataCon - deriving (Show, Eq, Ord) - -data DataConName = NUnit | NBool Bool | NTuple | NList | NCons - deriving (Show, Eq, Ord) - -getName :: DataCon -> DataConName -getName KUnit = NUnit -getName (Bool b) = NBool b -getName (Tuple _) = NTuple -getName (List _) = NList -getName (Cons _ _) = NCons - data Literal where T :: Literal F :: Literal - LitCond :: (TypedVar, LitCond) -> Literal + LitCond :: (TI.TypedVar, LitCond) -> Literal deriving (Show, Eq, Ord) data LitCond where - LitMatch :: TI.DataCon -> [TypedVar] -> LitCond + LitMatch :: TI.DataCon -> [TI.TypedVar] -> LitCond LitNot :: TI.DataCon -> LitCond - LitHerebyBe :: TypedVar -> LitCond - deriving (Show, Eq, Ord) - -type NormRefType = (Context, [ConstraintFor]) - -type ConstraintFor = (TypedVar, Constraint) - -type Context = [TypedVar] - -data Constraint where - CMatch :: TI.DataCon -> [TypedVar] -> Constraint - CNot :: TI.DataCon -> Constraint - CHerebyBe :: TypedVar -> Constraint + LitHerebyBe :: TI.TypedVar -> LitCond deriving (Show, Eq, Ord) data Ant where - AGrhs :: [NormRefType] -> Int -> Ant + AGrhs :: [C.NormRefType] -> Int -> Ant ABranch :: Ant -> Ant -> Ant deriving (Show) -ua :: (Member Fresh r) => [NormRefType] -> Gdt -> Sem r ([NormRefType], Ant) +ua :: (Member Fresh 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 @@ -179,7 +158,7 @@ ua nrefs gdt = case gdt of n'' <- addLitMulti nrefs $ LitCond (x, LitNot dc) return (n'' ++ n', u) -addLitMulti :: (Members '[Fresh] r) => [NormRefType] -> Literal -> Sem r [NormRefType] +addLitMulti :: (Members '[Fresh] r) => [C.NormRefType] -> Literal -> Sem r [C.NormRefType] addLitMulti [] _ = return [] addLitMulti (n : ns) lit = do r <- runMaybeT $ addLiteral n lit @@ -189,38 +168,42 @@ addLitMulti (n : ns) lit = do ns' <- addLitMulti ns lit return $ (ctx, cfs) : ns' -redundantNorm :: (Member Fresh r) => Ant -> Context -> Sem r [Int] -redundantNorm ant args = case ant of - AGrhs ref i -> do - inhabited <- null <$> genInhab ref args - return [i | inhabited] - ABranch a1 a2 -> mappend <$> redundantNorm a1 args <*> redundantNorm a2 args - -addLiteral :: (Members '[Fresh] r) => NormRefType -> Literal -> MaybeT (Sem r) NormRefType -addLiteral n@(context, constraints) flit = case flit of +addLiteral :: (Members '[Fresh] r) => C.NormRefType -> Literal -> MaybeT (Sem r) C.NormRefType +addLiteral (context, constraints) flit = case flit of F -> MaybeT $ pure Nothing - T -> return n + T -> return (context, constraints) LitCond (x, c) -> case c of - LitHerebyBe z -> (n <> ([z], [])) `addConstraint` (x, CHerebyBe z) - LitMatch dc args -> (n <> (args, [])) `addConstraint` (x, CMatch dc args) - LitNot dc -> n `addConstraint` (x, CNot dc) - --- Tuple types names -> (context ++ zip names types, constraints) `addConstraint` (x, CIs $ Tuple names) --- List :: [Name ATerm] -> DataCon --- Cons :: Name ATerm -> Name ATerm -> DataCon - --- MatchDataCon k ys x -> (context ++ zip ys (Ty.dcTypes k), constraints) `addConstraint` (x, MatchDataCon k ys) --- NotDataCon k x -> n `addConstraint` (x, NotDataCon k) + LitHerebyBe z -> + (context `C.addVars` [z], constraints) `C.addConstraint` (x, C.CHerebyBe z) + LitMatch dc args -> + (context `C.addVars` args, constraints) `C.addConstraint` (x, C.CMatch dc args) + LitNot dc -> + (context, constraints) `C.addConstraint` (x, C.CNot dc) data InhabPat where IPIs :: TI.DataCon -> [InhabPat] -> InhabPat IPNot :: [TI.DataCon] -> InhabPat deriving (Show, Eq, Ord) -genInhab :: (Members '[Fresh] r) => [NormRefType] -> Context -> Sem r (Poss.Possibilities InhabPat) -genInhab nrefs args = do - n <- sequence [findVarInhabitants arg nref | nref <- nrefs, arg <- args] - return $ Poss.anyOf n +join j a b = a ++ j ++ b + +joinComma = foldl (join ", ") "" + +joinSpace = foldl (join " ") "" + +prettyInhab :: InhabPat -> String +prettyInhab (IPNot []) = "_" +prettyInhab (IPNot nots) = "Not{" ++ joinComma (map dcToString nots) ++ "}" +prettyInhab (IPIs TI.DataCon {TI.dcIdent = TI.KTuple, TI.dcTypes = _} args) = + "(" ++ joinComma (map prettyInhab args) ++ ")" +prettyInhab (IPIs dc []) = dcToString dc +prettyInhab (IPIs dc args) = dcToString dc ++ " " ++ joinSpace (map prettyInhab args) + +dcToString TI.DataCon {TI.dcIdent = TI.KNat n} = show n +dcToString TI.DataCon {TI.dcIdent = TI.KBool b} = show b +dcToString TI.DataCon {TI.dcIdent = TI.KUnit} = "Unit" +dcToString TI.DataCon {TI.dcIdent = TI.KTuple} = "Tuple?" +dcToString TI.DataCon {TI.dcIdent = _} = "AAAAA" -- Sanity check: are we giving the dataconstructor the -- correct number of arguments? @@ -230,24 +213,32 @@ mkIPMatch k pats = then error $ "Wrong number of DataCon args" ++ show (k, pats) else IPIs k pats -findVarInhabitants :: (Members '[Fresh] r) => TypedVar -> NormRefType -> Sem r (Poss.Possibilities InhabPat) +findInhabitants :: (Members '[Fresh] r) => [C.NormRefType] -> [TI.TypedVar] -> Sem r (Poss.Possibilities [InhabPat]) +findInhabitants nrefs args = do + a <- forM nrefs (`findAllForNref` args) + return $ Poss.anyOf a + +findAllForNref :: (Member Fresh 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] r) => TI.TypedVar -> C.NormRefType -> Sem r (Poss.Possibilities InhabPat) findVarInhabitants var nref@(_, cns) = case posMatch of Just (k, args) -> do - argPats <- forM args (`findVarInhabitants` nref) - let argPossibilities = Poss.allCombinations argPats - + argPossibilities <- findAllForNref nref args return (mkIPMatch k <$> argPossibilities) - Nothing -> case nub negMatch of + Nothing -> case nub negMatches of [] -> Poss.retSingle $ IPNot [] neg -> - case TI.tyDataCons (snd var) of + case TI.tyDataCons . TI.getType $ var of Nothing -> Poss.retSingle $ IPNot neg Just dcs -> do let tryAddDc dc = do - vars <- newVars (TI.dcTypes dc) - runMaybeT (nref `addConstraint` (var, CMatch dc vars)) + vars <- TI.newVars (TI.dcTypes dc) + runMaybeT (nref `C.addConstraint` (var, C.CMatch dc vars)) -- Try to add a positive constraint for each data constructor -- to the current nref @@ -259,11 +250,13 @@ findVarInhabitants var nref@(_, cns) = then Poss.retSingle $ IPNot [] else Poss.anyOf <$> forM posNrefs (findVarInhabitants var) where - constraintsOnX = onVar var cns - posMatch = listToMaybe $ mapMaybe (\case (CMatch k ys) -> Just (k, ys); _ -> Nothing) constraintsOnX - negMatch = mapMaybe (\case (CNot k) -> Just k; _ -> Nothing) constraintsOnX - -,,,TODO I recommend breaking things up into a "Constraint.hs" file, which imports a "Context.hs" file, in - which we make Context a newtype instead of a alias for a pair, and expose the correct functions - adding constraints shouldn't depend on how the context is implemented - the only weird thing is going to be the substituting all the variables for the herebys + constraintsOnX = C.onVar var cns + posMatch = C.posMatch constraintsOnX + negMatches = C.negMatches constraintsOnX + +findRedundant :: (Member Fresh 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 diff --git a/src/Disco/Exhaustiveness/Constraint.hs b/src/Disco/Exhaustiveness/Constraint.hs new file mode 100644 index 00000000..ee46bb9b --- /dev/null +++ b/src/Disco/Exhaustiveness/Constraint.hs @@ -0,0 +1,143 @@ +module Disco.Exhaustiveness.Constraint where + +import Control.Applicative (Alternative) +import Control.Monad (foldM, guard, replicateM) +import Control.Monad.Trans (lift) +import Control.Monad.Trans.Maybe (MaybeT, runMaybeT) +import Data.List (partition) +import Data.Maybe (isJust, listToMaybe, mapMaybe) +import Disco.Effects.Fresh (Fresh) +import qualified Disco.Exhaustiveness.TypeInfo as TI +import Polysemy + +newtype Context = Context {getCtxVars :: [TI.TypedVar]} + deriving (Show, Eq) + +addVars :: Context -> [TI.TypedVar] -> Context +addVars (Context ctx) vars = Context (ctx ++ vars) + +data Constraint where + CMatch :: TI.DataCon -> [TI.TypedVar] -> Constraint + CNot :: TI.DataCon -> Constraint + CHerebyBe :: 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 constraints = mapMaybe (\case (CNot k) -> Just k; _ -> Nothing) constraints + +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', CHerebyBe 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 = (Context, [ConstraintFor]) + +addConstraints :: (Members '[Fresh] r) => NormRefType -> [ConstraintFor] -> MaybeT (Sem r) NormRefType +addConstraints = foldM addConstraint + +addConstraint :: (Members '[Fresh] r) => NormRefType -> ConstraintFor -> MaybeT (Sem r) NormRefType +addConstraint nref@(_, cns) (x, c) = do + breakIf $ any (conflictsWith c) (onVar x cns) + addConstraintHelper nref (lookupVar x cns, c) + +addConstraintHelper :: (Members '[Fresh] r) => NormRefType -> ConstraintFor -> MaybeT (Sem r) NormRefType +addConstraintHelper nref@(ctx, cns) cf@(origX, c) = case c of + --- Equation (10) + CMatch k args -> do + case getConstructorArgs k (onVar origX cns) of + -- 10c -- TODO(colin): Still need to add type constraints! + Just args' -> + addConstraints + nref + (zipWith (\a b -> (a, CHerebyBe 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) + CHerebyBe y -> do + let origY = lookupVar y cns + if origX == origY + then return nref + else do + let (noX', withX') = partition ((/= origX) . fst) cns + addConstraints (ctx, noX' ++ [cf]) (substituteVarIDs origY origX withX') + where + added = (ctx, 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 + CHerebyBe _ -> 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 (\(var, c) -> (subst var, c)) + where + subst var = if var == x then y else x + +-- Deals with I2 form 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 +-- NOTE: we may eventually have type constraints +-- and we would need to worry pulling them from nref here +inhabited :: (Members '[Fresh] r) => NormRefType -> TI.TypedVar -> Sem r Bool +inhabited n var = case TI.tyDataCons . TI.getType $ var of + Nothing -> return True -- assume opaque types are inhabited + Just 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] r) => NormRefType -> TI.TypedVar -> TI.DataCon -> Sem r Bool +instantiate (ctx, cns) var k = do + args <- TI.newVars $ TI.dcTypes k + let attempt = (ctx `addVars` args, cns) `addConstraint` (var, CMatch k args) + isJust <$> runMaybeT attempt diff --git a/src/Disco/Exhaustiveness/TypeInfo.hs b/src/Disco/Exhaustiveness/TypeInfo.hs index deee774e..831cf618 100644 --- a/src/Disco/Exhaustiveness/TypeInfo.hs +++ b/src/Disco/Exhaustiveness/TypeInfo.hs @@ -1,6 +1,11 @@ module Disco.Exhaustiveness.TypeInfo where +import Control.Monad (replicateM) +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) {- @@ -25,8 +30,19 @@ Also having convient lists of types and constructors Makes the algorithm easier to implement -} -data TypeName = TBool | TUnit | TPair | TEither | TInt | TThrool - deriving (Eq, Ord, Show) +newtype TypedVar = TypedVar (Name ATerm, Type) + deriving (Show, Ord) + +-- For now, equality is always in terms of the name +-- We will see if the causes problems later +instance Eq TypedVar where + TypedVar (n1, _t1) == TypedVar (n2, _t2) = n1 == n2 + +getType :: TypedVar -> Type +getType (TypedVar (_, t)) = t + +-- data TypeName = TBool | TUnit | TPair | TEither | TInt | TThrool +-- deriving (Eq, Ord, Show) data Type = Type { tyIdent :: Ty.Type, @@ -41,13 +57,14 @@ data DataCon = DataCon deriving (Eq, Ord, Show) data Ident where - KBool :: Bool -> Ident KUnit :: Ident - KDummy :: Ident - KTuple :: Ident + KBool :: Bool -> Ident KNat :: Integer -> Ident + KPair :: Ident + KTuple :: Ident KList :: Ident KCons :: Ident + KDummy :: Ident deriving (Eq, Ord, Show) unit :: DataCon @@ -65,13 +82,22 @@ natural n = DataCon {dcIdent = KNat n, dcTypes = []} -- Don't mix and match types here, -- we are going on the honor system list :: [Type] -> DataCon -list types = DataCon {dcIdent = KList, dcTypes = types } +list types = DataCon {dcIdent = KList, dcTypes = types} +cons :: Type -> Type -> DataCon cons tHead tTail = DataCon {dcIdent = KCons, dcTypes = [tHead, tTail]} extractRelevant :: Ty.Type -> Type -- extractRelevant Ty.TyVoid = Just [] --- extractRelevant (a Ty.:*: b) = enumProd (enumType a) (enumType b) +-- extractRelevant t@(a Ty.:*: b) = Type {tyIdent = t, tyDataCons = Just [tuple [natT, natT, natT]]} +extractRelevant t@(a Ty.:*: b) = + Type + { tyIdent = t, + tyDataCons = + Just + [ DataCon {dcIdent = KPair, dcTypes = [extractRelevant a, extractRelevant b]} + ] + } -- extractRelevant (a Ty.:+: b) = enumSum (enumType a) (enumType b) -- extractRelevant (a Ty.:->: b) = enumFunction (enumType a) (enumType b) -- extractRelevant (Ty.TySet t) = ? @@ -94,3 +120,15 @@ extractRelevant t@Ty.TyC = Type {tyIdent = t, tyDataCons = Nothing} extractRelevant t = Type {tyIdent = t, tyDataCons = Nothing} -- extractRelevant ty = error $ "Bad type in exhaust" ++ show ty + +-- TODO: should these really just be blank names? +newName :: (Member Fresh r) => Sem r (Name ATerm) +newName = fresh $ s2n "" + +newNames :: (Member Fresh r) => Int -> Sem r [Name ATerm] +newNames i = replicateM i newName + +newVars :: (Member Fresh r) => [Type] -> Sem r [TypedVar] +newVars types = do + names <- newNames (length types) + return $ map TypedVar $ zip names types From fe5da6760ab4eed8b8213a81d5871800094a2323 Mon Sep 17 00:00:00 2001 From: LeitMoth Date: Wed, 17 Jul 2024 21:57:45 -0500 Subject: [PATCH 05/44] tuples now turn into pairs and work! (mostly. Found weeks old bug in code I thought was good!) --- src/Disco/Exhaustiveness.hs | 64 ++++++++++++++++++---------- src/Disco/Exhaustiveness/TypeInfo.hs | 21 +++++---- 2 files changed, 55 insertions(+), 30 deletions(-) diff --git a/src/Disco/Exhaustiveness.hs b/src/Disco/Exhaustiveness.hs index 2e41e068..51217784 100644 --- a/src/Disco/Exhaustiveness.hs +++ b/src/Disco/Exhaustiveness.hs @@ -2,15 +2,14 @@ module Disco.Exhaustiveness where -import Control.Monad (forM, replicateM, when, zipWithM) +import Control.Monad (forM, when, zipWithM) import Control.Monad.Trans.Maybe (MaybeT (MaybeT), runMaybeT) import Data.List (nub) import Data.List.NonEmpty (NonEmpty) import qualified Data.List.NonEmpty as NonEmpty -import Data.Maybe (catMaybes, listToMaybe, mapMaybe) +import Data.Maybe (catMaybes) import Disco.AST.Typed ( APattern, - ATerm, pattern APBool, pattern APCons, pattern APList, @@ -20,14 +19,13 @@ import Disco.AST.Typed pattern APVar, pattern APWild, ) -import Disco.Effects.Fresh (Fresh, fresh) +import Disco.Effects.Fresh (Fresh) import qualified Disco.Exhaustiveness.Constraint as C import qualified Disco.Exhaustiveness.Possibilities as Poss import qualified Disco.Exhaustiveness.TypeInfo as TI import qualified Disco.Types as Ty import Polysemy import Text.Show.Pretty (pPrint) -import Unbound.Generics.LocallyNameless (Name, s2n) checkClauses :: (Members '[Fresh, Embed IO] r) => [Ty.Type] -> NonEmpty [APattern] -> Sem r () checkClauses types pats = do @@ -75,6 +73,13 @@ allSame :: (Eq a) => [a] -> Bool allSame [] = True allSame (x : xs) = all (x ==) xs +-- TODO: explain. this was a pain +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 + desugarMatch :: (Members '[Fresh, Embed IO] r) => TI.TypedVar -> APattern -> Sem r [Guard] desugarMatch var pat = do case pat of @@ -84,12 +89,22 @@ desugarMatch var pat = do (APNat _ nat) -> return [(var, GMatch (TI.natural nat) [])] (APUnit) -> return [(var, GMatch TI.unit [])] (APBool b) -> return [(var, GMatch (TI.bool b) [])] - (APTup _ subs) -> do - let types = map (TI.extractRelevant . Ty.getType) subs - vars <- TI.newVars types - guards <- sequence $ zipWith desugarMatch vars subs - return $ (var, (GMatch (TI.tuple types) vars)) : concat guards + (APTup (ta Ty.:*: tb) [pfst, psnd]) -> do + let tia = TI.extractRelevant ta + let tib = TI.extractRelevant tb + + varFst <- TI.newVar tia + varSnd <- TI.newVar tib + + guardsFst <- desugarMatch varFst pfst + guardsSnd <- desugarMatch varSnd psnd + + let guardPair = (var, GMatch (TI.pair tia tib) [varFst, varSnd]) + return $ [guardPair] ++ guardsFst ++ guardsSnd + (APTup ty [_, _]) -> error $ "Tuple type that wasn't a pair???: " ++ show ty + (APTup _ sugary) -> desugarMatch var (desugarTuplePats sugary) (APList _ subs) -> do + -- TODO: review, will this be a problem like tuples? let types = map (TI.extractRelevant . Ty.getType) subs when (not . allSame $ types) @@ -98,17 +113,16 @@ desugarMatch var pat = do guards <- sequence $ zipWith desugarMatch vars subs return $ (var, (GMatch (TI.list types) vars)) : concat guards (APCons _ subHead subTail) -> do - embed $ putStr "Cons: " - embed $ pPrint (subHead, subTail) - nameHead <- TI.newName - nameTail <- TI.newName + -- TODO: review, will this be a problem like tuples? let typeHead = (TI.extractRelevant . Ty.getType) subHead let typeTail = (TI.extractRelevant . Ty.getType) subTail - let varHead = TI.TypedVar (nameHead, typeHead) - let varTail = TI.TypedVar (nameTail, typeTail) + varHead <- TI.newVar typeHead + varTail <- TI.newVar typeTail guardsHead <- desugarMatch varHead subHead guardsTail <- desugarMatch varTail subTail - return $ (var, (GMatch (TI.cons typeHead typeTail) [varHead, varTail])) : guardsHead ++ guardsTail + let guardCons = (var, (GMatch (TI.cons typeHead typeTail) [varHead, varTail])) + return $ [guardCons] ++ guardsHead ++ guardsTail + -- TODO: consider the rest of the patterns -- (APAdd) e -> return [] @@ -185,24 +199,30 @@ data InhabPat where IPNot :: [TI.DataCon] -> InhabPat deriving (Show, Eq, Ord) +join :: [a] -> [a] -> [a] -> [a] join j a b = a ++ j ++ b -joinComma = foldl (join ", ") "" +joinComma :: [String] -> String +joinComma = foldr1 (join ", ") -joinSpace = foldl (join " ") "" +joinSpace :: [String] -> String +joinSpace = foldr1 (join " ") +-- TODO: maybe fully print out tuples even if they have wildcars in the middle? +-- e.g. (1,_,_) instead of just (1,_) prettyInhab :: InhabPat -> String prettyInhab (IPNot []) = "_" prettyInhab (IPNot nots) = "Not{" ++ joinComma (map dcToString nots) ++ "}" -prettyInhab (IPIs TI.DataCon {TI.dcIdent = TI.KTuple, TI.dcTypes = _} args) = - "(" ++ joinComma (map prettyInhab args) ++ ")" +prettyInhab (IPIs TI.DataCon {TI.dcIdent = TI.KPair, TI.dcTypes = _} [ifst, isnd]) = + "(" ++ prettyInhab ifst ++ ", " ++ prettyInhab isnd ++ ")" prettyInhab (IPIs dc []) = dcToString dc prettyInhab (IPIs dc args) = dcToString dc ++ " " ++ joinSpace (map prettyInhab args) +dcToString :: TI.DataCon -> String dcToString TI.DataCon {TI.dcIdent = TI.KNat n} = show n dcToString TI.DataCon {TI.dcIdent = TI.KBool b} = show b dcToString TI.DataCon {TI.dcIdent = TI.KUnit} = "Unit" -dcToString TI.DataCon {TI.dcIdent = TI.KTuple} = "Tuple?" +dcToString TI.DataCon {TI.dcIdent = TI.KPair} = "Pair?" dcToString TI.DataCon {TI.dcIdent = _} = "AAAAA" -- Sanity check: are we giving the dataconstructor the diff --git a/src/Disco/Exhaustiveness/TypeInfo.hs b/src/Disco/Exhaustiveness/TypeInfo.hs index 831cf618..39e3120c 100644 --- a/src/Disco/Exhaustiveness/TypeInfo.hs +++ b/src/Disco/Exhaustiveness/TypeInfo.hs @@ -61,7 +61,7 @@ data Ident where KBool :: Bool -> Ident KNat :: Integer -> Ident KPair :: Ident - KTuple :: Ident + -- KTuple :: Ident KList :: Ident KCons :: Ident KDummy :: Ident @@ -73,9 +73,6 @@ unit = DataCon {dcIdent = KUnit, dcTypes = []} bool :: Bool -> DataCon bool b = DataCon {dcIdent = KBool b, dcTypes = []} -tuple :: [Type] -> DataCon -tuple types = DataCon {dcIdent = KTuple, dcTypes = types} - natural :: Integer -> DataCon natural n = DataCon {dcIdent = KNat n, dcTypes = []} @@ -87,6 +84,9 @@ list types = DataCon {dcIdent = KList, dcTypes = types} cons :: Type -> Type -> DataCon cons tHead tTail = DataCon {dcIdent = KCons, dcTypes = [tHead, tTail]} +pair :: Type -> Type -> DataCon +pair a b = DataCon {dcIdent = KPair, dcTypes = [a, b]} + extractRelevant :: Ty.Type -> Type -- extractRelevant Ty.TyVoid = Just [] -- extractRelevant t@(a Ty.:*: b) = Type {tyIdent = t, tyDataCons = Just [tuple [natT, natT, natT]]} @@ -102,14 +102,14 @@ extractRelevant t@(a Ty.:*: b) = -- extractRelevant (a Ty.:->: b) = enumFunction (enumType a) (enumType b) -- extractRelevant (Ty.TySet t) = ? -- extractRelevant (Ty.TyList t) = ? -extractRelevant Ty.TyBool = +extractRelevant t@Ty.TyBool = Type - { tyIdent = Ty.TyBool, + { tyIdent = t, tyDataCons = Just [bool True, bool False] } -extractRelevant Ty.TyUnit = +extractRelevant t@Ty.TyUnit = Type - { tyIdent = Ty.TyUnit, + { tyIdent = t, tyDataCons = Just [unit] } extractRelevant t@Ty.TyN = Type {tyIdent = t, tyDataCons = Nothing} @@ -125,6 +125,11 @@ extractRelevant t = Type {tyIdent = t, tyDataCons = Nothing} newName :: (Member Fresh r) => Sem r (Name ATerm) newName = fresh $ s2n "" +newVar :: (Member Fresh r) => 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 From c7ba83e0f362526f00c43add6ab70b36cacdb189 Mon Sep 17 00:00:00 2001 From: LeitMoth Date: Wed, 17 Jul 2024 22:04:31 -0500 Subject: [PATCH 06/44] remove old typeinfo doc, add fixme note about pair / order based bug --- src/Disco/Exhaustiveness/Constraint.hs | 27 ++++++++++++++++++++++++++ src/Disco/Exhaustiveness/TypeInfo.hs | 23 ---------------------- 2 files changed, 27 insertions(+), 23 deletions(-) diff --git a/src/Disco/Exhaustiveness/Constraint.hs b/src/Disco/Exhaustiveness/Constraint.hs index ee46bb9b..34d97bd9 100644 --- a/src/Disco/Exhaustiveness/Constraint.hs +++ b/src/Disco/Exhaustiveness/Constraint.hs @@ -47,6 +47,33 @@ onVar x cs = alistLookup (lookupVar x cs) cs type NormRefType = (Context, [ConstraintFor]) +{- + TODO: fix this! +FIXME: big bug! + +in haskell, look at this: + +thing :: (Int, Bool) -> () +thing (n,True) = () +thing (0,n) = () + +haskell reports (p, False) uncovered where p is one of {0} + +but our solver just responds with (_, False) uncovered. +Its dropping the info about the 0!!! + +This is present in my test implementation, +I just didn't discover it until now :[ + +Clue discovered! +If we swap these like this: +thing (0,n) = unit +thing (n,True) = unit +Our solver actually gets this right! + +This is a good clue to start with +-} + addConstraints :: (Members '[Fresh] r) => NormRefType -> [ConstraintFor] -> MaybeT (Sem r) NormRefType addConstraints = foldM addConstraint diff --git a/src/Disco/Exhaustiveness/TypeInfo.hs b/src/Disco/Exhaustiveness/TypeInfo.hs index 39e3120c..42f4a016 100644 --- a/src/Disco/Exhaustiveness/TypeInfo.hs +++ b/src/Disco/Exhaustiveness/TypeInfo.hs @@ -7,29 +7,6 @@ import qualified Disco.Types as Ty import Polysemy import Unbound.Generics.LocallyNameless (Name, s2n) -{- - -Motivation: - -Imagine the function - -foo : N * N * N -> Unit -foo (x,y,z) -> unit -foo (x,(y,z)) -> unit - -So, we must make the decision on how we want to report back -the uncovered patterns -I am choosing to preserve the visual structure of what the user put in, -So I must turn these product types into tuples, in order to get -back out a similar pattern. - -I cannot look to Haskell for guidance, as -(Int,Int,Int) /= (Int,(Int,Int)) in Haskell - -Also having convient lists of types and constructors -Makes the algorithm easier to implement --} - newtype TypedVar = TypedVar (Name ATerm, Type) deriving (Show, Ord) From 7c65f3efaa960ef86595d63af54d7002ea908932 Mon Sep 17 00:00:00 2001 From: LeitMoth Date: Fri, 19 Jul 2024 17:39:55 -0500 Subject: [PATCH 07/44] fix term equality bug, I just had things backwards --- src/Disco/Exhaustiveness.hs | 25 +++++++++-------- src/Disco/Exhaustiveness/Constraint.hs | 39 ++++---------------------- src/Disco/Exhaustiveness/TypeInfo.hs | 2 +- 3 files changed, 20 insertions(+), 46 deletions(-) diff --git a/src/Disco/Exhaustiveness.hs b/src/Disco/Exhaustiveness.hs index 51217784..fa225d12 100644 --- a/src/Disco/Exhaustiveness.hs +++ b/src/Disco/Exhaustiveness.hs @@ -73,7 +73,7 @@ allSame :: (Eq a) => [a] -> Bool allSame [] = True allSame (x : xs) = all (x ==) xs --- TODO: explain. this was a pain +-- TODO(colin): explain. this was a pain desugarTuplePats :: [APattern] -> APattern desugarTuplePats [] = error "Found empty tuple, what happened?" desugarTuplePats [p] = p @@ -85,7 +85,8 @@ desugarMatch var pat = do case pat of (APWild _) -> return [] (APVar ty name) -> do - return $ [(var, GHerebyBe $ TI.TypedVar (name, TI.extractRelevant ty))] + let newAlias = TI.TypedVar (name, TI.extractRelevant ty) + return $ [(newAlias, GWasOriginally var)] (APNat _ nat) -> return [(var, GMatch (TI.natural nat) [])] (APUnit) -> return [(var, GMatch TI.unit [])] (APBool b) -> return [(var, GMatch (TI.bool b) [])] @@ -104,7 +105,7 @@ desugarMatch var pat = do (APTup ty [_, _]) -> error $ "Tuple type that wasn't a pair???: " ++ show ty (APTup _ sugary) -> desugarMatch var (desugarTuplePats sugary) (APList _ subs) -> do - -- TODO: review, will this be a problem like tuples? + -- TODO(colin): review, will this be a problem like tuples? let types = map (TI.extractRelevant . Ty.getType) subs when (not . allSame $ types) @@ -113,7 +114,7 @@ desugarMatch var pat = do guards <- sequence $ zipWith desugarMatch vars subs return $ (var, (GMatch (TI.list types) vars)) : concat guards (APCons _ subHead subTail) -> do - -- TODO: review, will this be a problem like tuples? + -- TODO(colin): review, will this be a problem like tuples? let typeHead = (TI.extractRelevant . Ty.getType) subHead let typeTail = (TI.extractRelevant . Ty.getType) subTail varHead <- TI.newVar typeHead @@ -122,7 +123,7 @@ desugarMatch var pat = do guardsTail <- desugarMatch varTail subTail let guardCons = (var, (GMatch (TI.cons typeHead typeTail) [varHead, varTail])) return $ [guardCons] ++ guardsHead ++ guardsTail - -- TODO: consider the rest of the patterns + -- TODO(colin): consider the rest of the patterns -- (APAdd) e -> return [] @@ -136,7 +137,7 @@ type Guard = (TI.TypedVar, GuardConstraint) data GuardConstraint where GMatch :: TI.DataCon -> [TI.TypedVar] -> GuardConstraint - GHerebyBe :: TI.TypedVar -> GuardConstraint + GWasOriginally :: TI.TypedVar -> GuardConstraint deriving (Show, Eq) data Literal where @@ -148,7 +149,7 @@ data Literal where data LitCond where LitMatch :: TI.DataCon -> [TI.TypedVar] -> LitCond LitNot :: TI.DataCon -> LitCond - LitHerebyBe :: TI.TypedVar -> LitCond + LitWasOriginally :: TI.TypedVar -> LitCond deriving (Show, Eq, Ord) data Ant where @@ -163,8 +164,8 @@ ua nrefs gdt = case gdt of (n1, u1) <- ua nrefs t1 (n2, u2) <- ua n1 t2 return (n2, ABranch u1 u2) - Guarded (x, GHerebyBe z) t -> do - n <- addLitMulti nrefs $ LitCond (x, LitHerebyBe z) + Guarded (y, GWasOriginally x) t -> do + n <- addLitMulti nrefs $ LitCond (y, LitWasOriginally x) ua n t Guarded (x, (GMatch dc args)) t -> do n <- addLitMulti nrefs $ LitCond (x, LitMatch dc args) @@ -187,8 +188,8 @@ addLiteral (context, constraints) flit = case flit of F -> MaybeT $ pure Nothing T -> return (context, constraints) LitCond (x, c) -> case c of - LitHerebyBe z -> - (context `C.addVars` [z], constraints) `C.addConstraint` (x, C.CHerebyBe z) + LitWasOriginally z -> + (context `C.addVars` [x], constraints) `C.addConstraint` (x, C.CWasOriginally z) LitMatch dc args -> (context `C.addVars` args, constraints) `C.addConstraint` (x, C.CMatch dc args) LitNot dc -> @@ -208,7 +209,7 @@ joinComma = foldr1 (join ", ") joinSpace :: [String] -> String joinSpace = foldr1 (join " ") --- TODO: maybe fully print out tuples even if they have wildcars in the middle? +-- TODO(colin): maybe fully print out tuples even if they have wildcars in the middle? -- e.g. (1,_,_) instead of just (1,_) prettyInhab :: InhabPat -> String prettyInhab (IPNot []) = "_" diff --git a/src/Disco/Exhaustiveness/Constraint.hs b/src/Disco/Exhaustiveness/Constraint.hs index 34d97bd9..646c97d6 100644 --- a/src/Disco/Exhaustiveness/Constraint.hs +++ b/src/Disco/Exhaustiveness/Constraint.hs @@ -19,7 +19,7 @@ addVars (Context ctx) vars = Context (ctx ++ vars) data Constraint where CMatch :: TI.DataCon -> [TI.TypedVar] -> Constraint CNot :: TI.DataCon -> Constraint - CHerebyBe :: TI.TypedVar -> Constraint + CWasOriginally :: TI.TypedVar -> Constraint deriving (Show, Eq, Ord) posMatch :: [Constraint] -> Maybe (TI.DataCon, [TI.TypedVar]) @@ -36,7 +36,7 @@ type ConstraintFor = (TI.TypedVar, Constraint) lookupVar :: TI.TypedVar -> [ConstraintFor] -> TI.TypedVar lookupVar x = foldr getNextId x where - getNextId (x', CHerebyBe y) | x' == x = const y + getNextId (x', CWasOriginally y) | x' == x = const y getNextId _ = id alistLookup :: (Eq a) => a -> [(a, b)] -> [b] @@ -47,33 +47,6 @@ onVar x cs = alistLookup (lookupVar x cs) cs type NormRefType = (Context, [ConstraintFor]) -{- - TODO: fix this! -FIXME: big bug! - -in haskell, look at this: - -thing :: (Int, Bool) -> () -thing (n,True) = () -thing (0,n) = () - -haskell reports (p, False) uncovered where p is one of {0} - -but our solver just responds with (_, False) uncovered. -Its dropping the info about the 0!!! - -This is present in my test implementation, -I just didn't discover it until now :[ - -Clue discovered! -If we swap these like this: -thing (0,n) = unit -thing (n,True) = unit -Our solver actually gets this right! - -This is a good clue to start with --} - addConstraints :: (Members '[Fresh] r) => NormRefType -> [ConstraintFor] -> MaybeT (Sem r) NormRefType addConstraints = foldM addConstraint @@ -91,7 +64,7 @@ addConstraintHelper nref@(ctx, cns) cf@(origX, c) = case c of Just args' -> addConstraints nref - (zipWith (\a b -> (a, CHerebyBe b)) args args') + (zipWith (\a b -> (a, CWasOriginally b)) args args') Nothing -> return added --- Equation (11) CNot _ -> do @@ -99,7 +72,7 @@ addConstraintHelper nref@(ctx, cns) cf@(origX, c) = case c of guard inh -- ensure that origX is still inhabited, as per I2 return added -- Equation (14) - CHerebyBe y -> do + CWasOriginally y -> do let origY = lookupVar y cns if origX == origY then return nref @@ -130,7 +103,7 @@ conflictsWith c = case c of CNot k -> \case (CMatch k' _) | k == k' -> True -- 11a _ -> False - CHerebyBe _ -> const 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) @@ -151,7 +124,7 @@ substituteVarIDs y x = map (\(var, c) -> (subst var, c)) -- 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 --- NOTE: we may eventually have type constraints +-- NOTE(colin): we may eventually have type constraints -- and we would need to worry pulling them from nref here inhabited :: (Members '[Fresh] r) => NormRefType -> TI.TypedVar -> Sem r Bool inhabited n var = case TI.tyDataCons . TI.getType $ var of diff --git a/src/Disco/Exhaustiveness/TypeInfo.hs b/src/Disco/Exhaustiveness/TypeInfo.hs index 42f4a016..e4804b85 100644 --- a/src/Disco/Exhaustiveness/TypeInfo.hs +++ b/src/Disco/Exhaustiveness/TypeInfo.hs @@ -98,7 +98,7 @@ extractRelevant t = Type {tyIdent = t, tyDataCons = Nothing} -- extractRelevant ty = error $ "Bad type in exhaust" ++ show ty --- TODO: should these really just be blank names? +-- TODO(colin): should these really just be blank names? newName :: (Member Fresh r) => Sem r (Name ATerm) newName = fresh $ s2n "" From 4bb13fa4ef1ead825f26cbedfb872dfd4487c085 Mon Sep 17 00:00:00 2001 From: LeitMoth Date: Sat, 20 Jul 2024 02:59:01 -0500 Subject: [PATCH 08/44] lists & strings work now! Added comments about remaining work --- src/Disco/Eval.hs | 2 +- src/Disco/Exhaustiveness.hs | 122 ++++++++++++++++----------- src/Disco/Exhaustiveness/TypeInfo.hs | 100 +++++++++------------- 3 files changed, 117 insertions(+), 107 deletions(-) diff --git a/src/Disco/Eval.hs b/src/Disco/Eval.hs index 945c492a..a40bd5f4 100644 --- a/src/Disco/Eval.hs +++ b/src/Disco/Eval.hs @@ -452,4 +452,4 @@ loadDef x body = do checkExhaustive :: Members '[Fresh, Embed IO] r => Defn -> Sem r () checkExhaustive (Defn name argsType _ boundClauses) = do clauses <- NonEmpty.map fst <$> mapM unbind boundClauses - checkClauses argsType clauses + checkClauses name argsType clauses diff --git a/src/Disco/Exhaustiveness.hs b/src/Disco/Exhaustiveness.hs index fa225d12..f691c1f6 100644 --- a/src/Disco/Exhaustiveness.hs +++ b/src/Disco/Exhaustiveness.hs @@ -10,14 +10,17 @@ import qualified Data.List.NonEmpty as NonEmpty import Data.Maybe (catMaybes) import Disco.AST.Typed ( APattern, + ATerm, pattern APBool, + pattern APChar, pattern APCons, pattern APList, pattern APNat, pattern APTup, pattern APUnit, pattern APVar, - pattern APWild, + pattern APWild, + pattern APString, ) import Disco.Effects.Fresh (Fresh) import qualified Disco.Exhaustiveness.Constraint as C @@ -26,10 +29,11 @@ import qualified Disco.Exhaustiveness.TypeInfo as TI import qualified Disco.Types as Ty import Polysemy import Text.Show.Pretty (pPrint) +import Unbound.Generics.LocallyNameless (Name) -checkClauses :: (Members '[Fresh, Embed IO] r) => [Ty.Type] -> NonEmpty [APattern] -> Sem r () -checkClauses types pats = do - args <- TI.newVars (map TI.extractRelevant types) +checkClauses :: (Members '[Fresh, 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 @@ -53,12 +57,11 @@ checkClauses types pats = do let jspace = foldr (\a b -> a ++ " " ++ b) "" when (not . null $ inhab) $ do - embed $ putStrLn "Warning: You haven't matched against:" + embed $ putStrLn $ "Warning: In function \"" ++ show name ++ "\", you haven't matched against:" embed $ mapM_ (putStrLn . jspace . map prettyInhab) inhab - -- embed $ mapM_ (putStrLn . show) inhab when (not . null $ redundant) $ do - embed $ putStrLn "Warning: These clause numbers (1-indexed) are redundant" + embed $ putStrLn $ "Warning: In function \"" ++ show name ++ "\", these clause numbers (1-indexed) are redundant:" embed $ putStrLn $ show redundant return () @@ -68,63 +71,73 @@ desugarClause args clauseIdx argsPats = do guards <- zipWithM desugarMatch args argsPats return $ foldr Guarded (Grhs clauseIdx) $ concat guards --- borrowed from `extra` -allSame :: (Eq a) => [a] -> Bool -allSame [] = True -allSame (x : xs) = all (x ==) xs - --- TODO(colin): explain. this was a pain +-- 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 - + where + psnd = desugarTuplePats rest + +{- +TODO(colin): handle remaining patterns + , APInj --what is this? + , APNeg --required for integers / rationals? + , APFrac --required for rationals? + algebraic (probably will be replaced anyway): + , APAdd + , APMul + , APSub +-} desugarMatch :: (Members '[Fresh, Embed IO] r) => TI.TypedVar -> APattern -> Sem r [Guard] desugarMatch var pat = do case pat of - (APWild _) -> return [] - (APVar ty name) -> do - let newAlias = TI.TypedVar (name, TI.extractRelevant ty) - return $ [(newAlias, GWasOriginally var)] - (APNat _ nat) -> return [(var, GMatch (TI.natural nat) [])] - (APUnit) -> return [(var, GMatch TI.unit [])] - (APBool b) -> return [(var, GMatch (TI.bool b) [])] (APTup (ta Ty.:*: tb) [pfst, psnd]) -> do - let tia = TI.extractRelevant ta - let tib = TI.extractRelevant tb - - varFst <- TI.newVar tia - varSnd <- TI.newVar tib - + varFst <- TI.newVar ta + varSnd <- TI.newVar tb guardsFst <- desugarMatch varFst pfst guardsSnd <- desugarMatch varSnd psnd - - let guardPair = (var, GMatch (TI.pair tia tib) [varFst, varSnd]) + let guardPair = (var, GMatch (TI.pair ta tb) [varFst, varSnd]) return $ [guardPair] ++ guardsFst ++ guardsSnd (APTup ty [_, _]) -> error $ "Tuple type that wasn't a pair???: " ++ show ty (APTup _ sugary) -> desugarMatch var (desugarTuplePats sugary) - (APList _ subs) -> do - -- TODO(colin): review, will this be a problem like tuples? - let types = map (TI.extractRelevant . Ty.getType) subs - when - (not . allSame $ types) - (embed . putStrLn $ "WARNING, mismatched types in list!: " ++ show types) - vars <- TI.newVars types - guards <- sequence $ zipWith desugarMatch vars subs - return $ (var, (GMatch (TI.list types) vars)) : concat guards (APCons _ subHead subTail) -> do - -- TODO(colin): review, will this be a problem like tuples? - let typeHead = (TI.extractRelevant . Ty.getType) subHead - let typeTail = (TI.extractRelevant . Ty.getType) subTail + 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 _ []) -> do + 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)) + -- These are more straightforward: + (APWild _) -> return [] + (APVar ty name) -> do + let newAlias = TI.TypedVar (name, ty) + return [(newAlias, GWasOriginally var)] + (APNat _ nat) -> return [(var, GMatch (TI.natural nat) [])] + (APUnit) -> return [(var, GMatch TI.unit [])] + (APBool b) -> return [(var, GMatch (TI.bool b) [])] + (APChar c) -> return [(var, GMatch (TI.char c) [])] -- TODO(colin): consider the rest of the patterns - -- (APAdd) e -> return [] data Gdt where @@ -211,20 +224,33 @@ joinSpace = foldr1 (join " ") -- TODO(colin): maybe fully print out tuples even if they have wildcars in the middle? -- e.g. (1,_,_) instead of just (1,_) +-- Also, the display for matches against strings is really weird, +-- as strings are lists of chars. +-- Maybe for strings, we just list the top 3 uncovered patterns +-- consiting of only postive information, sorted by length? prettyInhab :: InhabPat -> String prettyInhab (IPNot []) = "_" prettyInhab (IPNot nots) = "Not{" ++ joinComma (map dcToString nots) ++ "}" prettyInhab (IPIs TI.DataCon {TI.dcIdent = TI.KPair, TI.dcTypes = _} [ifst, isnd]) = "(" ++ prettyInhab ifst ++ ", " ++ prettyInhab isnd ++ ")" +prettyInhab (IPIs TI.DataCon {TI.dcIdent = TI.KCons, TI.dcTypes = _} [ihead, itail]) = + "(" ++ prettyInhab ihead ++ " :: " ++ prettyInhab itail ++ ")" prettyInhab (IPIs dc []) = dcToString dc prettyInhab (IPIs dc args) = dcToString dc ++ " " ++ joinSpace (map prettyInhab args) dcToString :: TI.DataCon -> String -dcToString TI.DataCon {TI.dcIdent = TI.KNat n} = show n -dcToString TI.DataCon {TI.dcIdent = TI.KBool b} = show b -dcToString TI.DataCon {TI.dcIdent = TI.KUnit} = "Unit" -dcToString TI.DataCon {TI.dcIdent = TI.KPair} = "Pair?" -dcToString TI.DataCon {TI.dcIdent = _} = "AAAAA" +dcToString TI.DataCon {TI.dcIdent = ident} = case ident of + TI.KBool b -> show b + TI.KChar c -> show c + TI.KNat n -> show n + TI.KNil -> "[]" + TI.KUnit -> "unit" + -- TODO(colin): find a way to remove these? These two shouldn't be reachable + -- If we were in an IPIs, we already handled these above + -- If we were in an IPNot, these aren't fromo opaque types, + -- so they shouldn't appear in a Not{} + TI.KPair -> "," + TI.KCons -> "::" -- Sanity check: are we giving the dataconstructor the -- correct number of arguments? diff --git a/src/Disco/Exhaustiveness/TypeInfo.hs b/src/Disco/Exhaustiveness/TypeInfo.hs index e4804b85..a2b7b3f8 100644 --- a/src/Disco/Exhaustiveness/TypeInfo.hs +++ b/src/Disco/Exhaustiveness/TypeInfo.hs @@ -7,7 +7,7 @@ import qualified Disco.Types as Ty import Polysemy import Unbound.Generics.LocallyNameless (Name, s2n) -newtype TypedVar = TypedVar (Name ATerm, Type) +newtype TypedVar = TypedVar (Name ATerm, Ty.Type) deriving (Show, Ord) -- For now, equality is always in terms of the name @@ -15,21 +15,12 @@ newtype TypedVar = TypedVar (Name ATerm, Type) instance Eq TypedVar where TypedVar (n1, _t1) == TypedVar (n2, _t2) = n1 == n2 -getType :: TypedVar -> Type +getType :: TypedVar -> Ty.Type getType (TypedVar (_, t)) = t --- data TypeName = TBool | TUnit | TPair | TEither | TInt | TThrool --- deriving (Eq, Ord, Show) - -data Type = Type - { tyIdent :: Ty.Type, - tyDataCons :: Maybe [DataCon] -- Set to Nothing for opaque types - } - deriving (Eq, Ord, Show) - data DataCon = DataCon { dcIdent :: Ident, - dcTypes :: [Type] + dcTypes :: [Ty.Type] } deriving (Eq, Ord, Show) @@ -38,10 +29,9 @@ data Ident where KBool :: Bool -> Ident KNat :: Integer -> Ident KPair :: Ident - -- KTuple :: Ident - KList :: Ident KCons :: Ident - KDummy :: Ident + KNil :: Ident + KChar :: Char -> Ident deriving (Eq, Ord, Show) unit :: DataCon @@ -53,56 +43,50 @@ bool b = DataCon {dcIdent = KBool b, dcTypes = []} natural :: Integer -> DataCon natural n = DataCon {dcIdent = KNat n, dcTypes = []} --- Don't mix and match types here, --- we are going on the honor system -list :: [Type] -> DataCon -list types = DataCon {dcIdent = KList, dcTypes = types} +char :: Char -> DataCon +char c = DataCon {dcIdent = KChar c, dcTypes = []} -cons :: Type -> Type -> DataCon +cons :: Ty.Type -> Ty.Type -> DataCon cons tHead tTail = DataCon {dcIdent = KCons, dcTypes = [tHead, tTail]} -pair :: Type -> Type -> DataCon +nil :: DataCon +nil = DataCon {dcIdent = KNil, dcTypes = []} + +pair :: Ty.Type -> Ty.Type -> DataCon pair a b = DataCon {dcIdent = KPair, dcTypes = [a, b]} -extractRelevant :: Ty.Type -> Type --- extractRelevant Ty.TyVoid = Just [] --- extractRelevant t@(a Ty.:*: b) = Type {tyIdent = t, tyDataCons = Just [tuple [natT, natT, natT]]} -extractRelevant t@(a Ty.:*: b) = - Type - { tyIdent = t, - tyDataCons = - Just - [ DataCon {dcIdent = KPair, dcTypes = [extractRelevant a, extractRelevant b]} - ] - } --- extractRelevant (a Ty.:+: b) = enumSum (enumType a) (enumType b) --- extractRelevant (a Ty.:->: b) = enumFunction (enumType a) (enumType b) --- extractRelevant (Ty.TySet t) = ? --- extractRelevant (Ty.TyList t) = ? -extractRelevant t@Ty.TyBool = - Type - { tyIdent = t, - tyDataCons = Just [bool True, bool False] - } -extractRelevant t@Ty.TyUnit = - Type - { tyIdent = t, - tyDataCons = Just [unit] - } -extractRelevant t@Ty.TyN = Type {tyIdent = t, tyDataCons = Nothing} -extractRelevant t@Ty.TyZ = Type {tyIdent = t, tyDataCons = Nothing} -extractRelevant t@Ty.TyF = Type {tyIdent = t, tyDataCons = Nothing} -extractRelevant t@Ty.TyQ = Type {tyIdent = t, tyDataCons = Nothing} -extractRelevant t@Ty.TyC = Type {tyIdent = t, tyDataCons = Nothing} -extractRelevant t = Type {tyIdent = t, tyDataCons = Nothing} - --- extractRelevant ty = error $ "Bad type in exhaust" ++ show ty - --- TODO(colin): should these really just be blank names? +{- +TODO(colin): Fill out the remaining types here +Remaining: + TyVar + , TySkolem + , TyProp + , TyBag + , TySet + , TyGraph + , TyMap + , TyUser +Needed: + , (:+:) +Impossible: + , (:->:) +-} +tyDataCons :: Ty.Type -> Maybe [DataCon] +tyDataCons (a Ty.:*: b) = Just [pair a b] +tyDataCons t@(Ty.TyList a) = Just [cons a t, nil] +tyDataCons Ty.TyVoid = Just [] +tyDataCons Ty.TyUnit = Just [unit] +tyDataCons Ty.TyBool = Just [bool True, bool False] +tyDataCons Ty.TyN = Nothing +tyDataCons Ty.TyZ = Nothing +tyDataCons Ty.TyF = Nothing +tyDataCons Ty.TyQ = Nothing +tyDataCons Ty.TyC = Nothing + newName :: (Member Fresh r) => Sem r (Name ATerm) newName = fresh $ s2n "" -newVar :: (Member Fresh r) => Type -> Sem r TypedVar +newVar :: (Member Fresh r) => Ty.Type -> Sem r TypedVar newVar types = do names <- newName return $ TypedVar $ (names, types) @@ -110,7 +94,7 @@ newVar types = do newNames :: (Member Fresh r) => Int -> Sem r [Name ATerm] newNames i = replicateM i newName -newVars :: (Member Fresh r) => [Type] -> Sem r [TypedVar] +newVars :: (Member Fresh r) => [Ty.Type] -> Sem r [TypedVar] newVars types = do names <- newNames (length types) return $ map TypedVar $ zip names types From 965cc73226a18cad2944e84a376948569b803939 Mon Sep 17 00:00:00 2001 From: LeitMoth Date: Sat, 20 Jul 2024 03:19:33 -0500 Subject: [PATCH 09/44] remove unused lit variants T/F, improve warning message --- src/Disco/Exhaustiveness.hs | 45 +++++++++++++++++-------------------- 1 file changed, 21 insertions(+), 24 deletions(-) diff --git a/src/Disco/Exhaustiveness.hs b/src/Disco/Exhaustiveness.hs index f691c1f6..1de955ed 100644 --- a/src/Disco/Exhaustiveness.hs +++ b/src/Disco/Exhaustiveness.hs @@ -2,7 +2,7 @@ module Disco.Exhaustiveness where -import Control.Monad (forM, when, zipWithM) +import Control.Monad (forM, forM_, when, zipWithM) import Control.Monad.Trans.Maybe (MaybeT (MaybeT), runMaybeT) import Data.List (nub) import Data.List.NonEmpty (NonEmpty) @@ -16,11 +16,11 @@ import Disco.AST.Typed pattern APCons, pattern APList, pattern APNat, + pattern APString, pattern APTup, pattern APUnit, pattern APVar, - pattern APWild, - pattern APString, + pattern APWild, ) import Disco.Effects.Fresh (Fresh) import qualified Disco.Exhaustiveness.Constraint as C @@ -57,8 +57,12 @@ checkClauses name types pats = do let jspace = foldr (\a b -> a ++ " " ++ b) "" when (not . null $ inhab) $ do - embed $ putStrLn $ "Warning: In function \"" ++ show name ++ "\", you haven't matched against:" - embed $ mapM_ (putStrLn . jspace . map prettyInhab) inhab + let patLine ipats = do + let ipatArgs = jspace (map prettyInhab ipats) + putStrLn $ show name ++ " " ++ ipatArgs ++ "= ..." + + embed $ putStrLn $ "Warning: You haven't matched against:" + embed $ forM_ inhab patLine when (not . null $ redundant) $ do embed $ putStrLn $ "Warning: In function \"" ++ show name ++ "\", these clause numbers (1-indexed) are redundant:" @@ -153,11 +157,7 @@ data GuardConstraint where GWasOriginally :: TI.TypedVar -> GuardConstraint deriving (Show, Eq) -data Literal where - T :: Literal - F :: Literal - LitCond :: (TI.TypedVar, LitCond) -> Literal - deriving (Show, Eq, Ord) +newtype Literal = Literal (TI.TypedVar, LitCond) data LitCond where LitMatch :: TI.DataCon -> [TI.TypedVar] -> LitCond @@ -178,12 +178,12 @@ ua nrefs gdt = case gdt of (n2, u2) <- ua n1 t2 return (n2, ABranch u1 u2) Guarded (y, GWasOriginally x) t -> do - n <- addLitMulti nrefs $ LitCond (y, LitWasOriginally x) + n <- addLitMulti nrefs $ Literal (y, LitWasOriginally x) ua n t Guarded (x, (GMatch dc args)) t -> do - n <- addLitMulti nrefs $ LitCond (x, LitMatch dc args) + n <- addLitMulti nrefs $ Literal (x, LitMatch dc args) (n', u) <- ua n t - n'' <- addLitMulti nrefs $ LitCond (x, LitNot dc) + n'' <- addLitMulti nrefs $ Literal (x, LitNot dc) return (n'' ++ n', u) addLitMulti :: (Members '[Fresh] r) => [C.NormRefType] -> Literal -> Sem r [C.NormRefType] @@ -197,16 +197,13 @@ addLitMulti (n : ns) lit = do return $ (ctx, cfs) : ns' addLiteral :: (Members '[Fresh] r) => C.NormRefType -> Literal -> MaybeT (Sem r) C.NormRefType -addLiteral (context, constraints) flit = case flit of - F -> MaybeT $ pure Nothing - T -> return (context, constraints) - LitCond (x, c) -> case c of - LitWasOriginally z -> - (context `C.addVars` [x], constraints) `C.addConstraint` (x, C.CWasOriginally z) - LitMatch dc args -> - (context `C.addVars` args, constraints) `C.addConstraint` (x, C.CMatch dc args) - LitNot dc -> - (context, constraints) `C.addConstraint` (x, C.CNot dc) +addLiteral (context, constraints) (Literal (x, c)) = case c of + LitWasOriginally z -> + (context `C.addVars` [x], constraints) `C.addConstraint` (x, C.CWasOriginally z) + LitMatch dc args -> + (context `C.addVars` args, constraints) `C.addConstraint` (x, C.CMatch dc args) + LitNot dc -> + (context, constraints) `C.addConstraint` (x, C.CNot dc) data InhabPat where IPIs :: TI.DataCon -> [InhabPat] -> InhabPat @@ -224,7 +221,7 @@ joinSpace = foldr1 (join " ") -- TODO(colin): maybe fully print out tuples even if they have wildcars in the middle? -- e.g. (1,_,_) instead of just (1,_) --- Also, the display for matches against strings is really weird, +-- Also, the display for matches against strings is really weird, -- as strings are lists of chars. -- Maybe for strings, we just list the top 3 uncovered patterns -- consiting of only postive information, sorted by length? From f2dd4791a69bb4f0a52dfeb88cbda7caf79ac3ba Mon Sep 17 00:00:00 2001 From: LeitMoth Date: Sat, 20 Jul 2024 12:36:44 -0500 Subject: [PATCH 10/44] sum types now work! --- src/Disco/Exhaustiveness.hs | 23 +++++++++++++++++++---- src/Disco/Exhaustiveness/TypeInfo.hs | 11 +++++++++-- 2 files changed, 28 insertions(+), 6 deletions(-) diff --git a/src/Disco/Exhaustiveness.hs b/src/Disco/Exhaustiveness.hs index 1de955ed..0a7ff5f9 100644 --- a/src/Disco/Exhaustiveness.hs +++ b/src/Disco/Exhaustiveness.hs @@ -3,17 +3,19 @@ module Disco.Exhaustiveness where import Control.Monad (forM, forM_, when, zipWithM) -import Control.Monad.Trans.Maybe (MaybeT (MaybeT), runMaybeT) +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.Typed ( APattern, ATerm, pattern APBool, pattern APChar, pattern APCons, + pattern APInj, pattern APList, pattern APNat, pattern APString, @@ -93,7 +95,6 @@ desugarTuplePats (pfst : rest) = APTup (Ty.getType pfst Ty.:*: Ty.getType psnd) {- TODO(colin): handle remaining patterns - , APInj --what is this? , APNeg --required for integers / rationals? , APFrac --required for rationals? algebraic (probably will be replaced anyway): @@ -141,7 +142,15 @@ desugarMatch var pat = do (APUnit) -> return [(var, GMatch TI.unit [])] (APBool b) -> return [(var, GMatch (TI.bool b) [])] (APChar c) -> return [(var, GMatch (TI.char c) [])] - -- TODO(colin): consider the rest of the patterns + (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 e -> return [] data Gdt where @@ -232,6 +241,10 @@ prettyInhab (IPIs TI.DataCon {TI.dcIdent = TI.KPair, TI.dcTypes = _} [ifst, isnd "(" ++ prettyInhab ifst ++ ", " ++ prettyInhab isnd ++ ")" prettyInhab (IPIs TI.DataCon {TI.dcIdent = TI.KCons, TI.dcTypes = _} [ihead, itail]) = "(" ++ prettyInhab ihead ++ " :: " ++ prettyInhab itail ++ ")" +prettyInhab (IPIs TI.DataCon {TI.dcIdent = TI.KLeft, TI.dcTypes = _} [l]) = + "left(" ++ prettyInhab l ++ ")" +prettyInhab (IPIs TI.DataCon {TI.dcIdent = TI.KRight, TI.dcTypes = _} [r]) = + "right(" ++ prettyInhab r ++ ")" prettyInhab (IPIs dc []) = dcToString dc prettyInhab (IPIs dc args) = dcToString dc ++ " " ++ joinSpace (map prettyInhab args) @@ -244,10 +257,12 @@ dcToString TI.DataCon {TI.dcIdent = ident} = case ident of TI.KUnit -> "unit" -- TODO(colin): find a way to remove these? These two shouldn't be reachable -- If we were in an IPIs, we already handled these above - -- If we were in an IPNot, these aren't fromo opaque types, + -- If we were in an IPNot, these aren't from opaque types, -- so they shouldn't appear in a Not{} TI.KPair -> "," TI.KCons -> "::" + TI.KLeft -> "left()" + TI.KRight -> "right()" -- Sanity check: are we giving the dataconstructor the -- correct number of arguments? diff --git a/src/Disco/Exhaustiveness/TypeInfo.hs b/src/Disco/Exhaustiveness/TypeInfo.hs index a2b7b3f8..462158a2 100644 --- a/src/Disco/Exhaustiveness/TypeInfo.hs +++ b/src/Disco/Exhaustiveness/TypeInfo.hs @@ -32,6 +32,8 @@ data Ident where KCons :: Ident KNil :: Ident KChar :: Char -> Ident + KLeft :: Ident + KRight :: Ident deriving (Eq, Ord, Show) unit :: DataCon @@ -55,6 +57,12 @@ 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]} + {- TODO(colin): Fill out the remaining types here Remaining: @@ -66,13 +74,12 @@ Remaining: , TyGraph , TyMap , TyUser -Needed: - , (:+:) Impossible: , (:->:) -} tyDataCons :: Ty.Type -> Maybe [DataCon] tyDataCons (a Ty.:*: b) = Just [pair a b] +tyDataCons (l Ty.:+: r) = Just [left l, right r] tyDataCons t@(Ty.TyList a) = Just [cons a t, nil] tyDataCons Ty.TyVoid = Just [] tyDataCons Ty.TyUnit = Just [unit] From 03e051abb08e30dfb96b0857d6715917200acf5d Mon Sep 17 00:00:00 2001 From: LeitMoth Date: Sat, 20 Jul 2024 13:52:56 -0500 Subject: [PATCH 11/44] User defined types now work! --- src/Disco/Eval.hs | 8 ++-- src/Disco/Exhaustiveness.hs | 25 ++++++----- src/Disco/Exhaustiveness/Constraint.hs | 24 ++++++----- src/Disco/Exhaustiveness/TypeInfo.hs | 59 ++++++++++++++------------ 4 files changed, 66 insertions(+), 50 deletions(-) diff --git a/src/Disco/Eval.hs b/src/Disco/Eval.hs index a40bd5f4..a66aee96 100644 --- a/src/Disco/Eval.hs +++ b/src/Disco/Eval.hs @@ -387,7 +387,7 @@ loadParsedDiscoModule' quiet mode resolver inProcess name cm@(Module _ mns _ _ _ m <- runTCM tyctx tydefns $ checkModule name importMap cm -- Check for partial functions - runFresh $ mapM_ checkExhaustive $ (Ctx.elems $ m^.miTermdefs) + runFresh $ mapM_ (checkExhaustive tydefns) (Ctx.elems $ m^.miTermdefs) -- Evaluate all the module definitions and add them to the topEnv. mapError EvalErr $ loadDefsFrom m @@ -449,7 +449,7 @@ loadDef x body = do v <- inputToState @TopInfo . inputTopEnv $ eval body modify @TopInfo $ topEnv %~ Ctx.insert x v -checkExhaustive :: Members '[Fresh, Embed IO] r => Defn -> Sem r () -checkExhaustive (Defn name argsType _ boundClauses) = do +checkExhaustive :: Members '[Fresh, Embed IO] r => TyDefCtx -> Defn -> Sem r () +checkExhaustive tyDefCtx (Defn name argsType _ boundClauses) = do clauses <- NonEmpty.map fst <$> mapM unbind boundClauses - checkClauses name argsType clauses + runReader @TyDefCtx tyDefCtx $ checkClauses name argsType clauses diff --git a/src/Disco/Exhaustiveness.hs b/src/Disco/Exhaustiveness.hs index 0a7ff5f9..f07ee642 100644 --- a/src/Disco/Exhaustiveness.hs +++ b/src/Disco/Exhaustiveness.hs @@ -32,8 +32,9 @@ import qualified Disco.Types as Ty import Polysemy import Text.Show.Pretty (pPrint) import Unbound.Generics.LocallyNameless (Name) +import Polysemy.Reader -checkClauses :: (Members '[Fresh, Embed IO] r) => Name ATerm -> [Ty.Type] -> NonEmpty [APattern] -> Sem r () +checkClauses :: Members '[Fresh, Reader Ty.TyDefCtx, 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) @@ -179,7 +180,7 @@ data Ant where ABranch :: Ant -> Ant -> Ant deriving (Show) -ua :: (Member Fresh r) => [C.NormRefType] -> Gdt -> Sem r ([C.NormRefType], Ant) +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 @@ -195,7 +196,7 @@ ua nrefs gdt = case gdt of n'' <- addLitMulti nrefs $ Literal (x, LitNot dc) return (n'' ++ n', u) -addLitMulti :: (Members '[Fresh] r) => [C.NormRefType] -> Literal -> Sem r [C.NormRefType] +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 @@ -205,7 +206,7 @@ addLitMulti (n : ns) lit = do ns' <- addLitMulti ns lit return $ (ctx, cfs) : ns' -addLiteral :: (Members '[Fresh] r) => C.NormRefType -> Literal -> MaybeT (Sem r) C.NormRefType +addLiteral :: Members '[Fresh, Reader Ty.TyDefCtx] r => C.NormRefType -> Literal -> MaybeT (Sem r) C.NormRefType addLiteral (context, constraints) (Literal (x, c)) = case c of LitWasOriginally z -> (context `C.addVars` [x], constraints) `C.addConstraint` (x, C.CWasOriginally z) @@ -234,6 +235,9 @@ joinSpace = foldr1 (join " ") -- as strings are lists of chars. -- Maybe for strings, we just list the top 3 uncovered patterns -- consiting of only postive information, sorted by length? +-- Also, how should we print out sum types? +-- We can do right(thing) or (right thing), or (right(thing)) +-- Which should we chose? prettyInhab :: InhabPat -> String prettyInhab (IPNot []) = "_" prettyInhab (IPNot nots) = "Not{" ++ joinComma (map dcToString nots) ++ "}" @@ -272,17 +276,17 @@ mkIPMatch k pats = then error $ "Wrong number of DataCon args" ++ show (k, pats) else IPIs k pats -findInhabitants :: (Members '[Fresh] r) => [C.NormRefType] -> [TI.TypedVar] -> Sem r (Poss.Possibilities [InhabPat]) +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 :: (Member Fresh r) => C.NormRefType -> [TI.TypedVar] -> Sem r (Poss.Possibilities [InhabPat]) +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] r) => TI.TypedVar -> C.NormRefType -> Sem r (Poss.Possibilities InhabPat) +findVarInhabitants :: Members '[Fresh, Reader Ty.TyDefCtx] r => TI.TypedVar -> C.NormRefType -> Sem r (Poss.Possibilities InhabPat) findVarInhabitants var nref@(_, cns) = case posMatch of Just (k, args) -> do @@ -290,8 +294,9 @@ findVarInhabitants var nref@(_, cns) = return (mkIPMatch k <$> argPossibilities) Nothing -> case nub negMatches of [] -> Poss.retSingle $ IPNot [] - neg -> - case TI.tyDataCons . TI.getType $ var of + neg -> do + tyCtx <- ask @Ty.TyDefCtx + case TI.tyDataCons (TI.getType var) tyCtx of Nothing -> Poss.retSingle $ IPNot neg Just dcs -> do @@ -313,7 +318,7 @@ findVarInhabitants var nref@(_, cns) = posMatch = C.posMatch constraintsOnX negMatches = C.negMatches constraintsOnX -findRedundant :: (Member Fresh r) => Ant -> [TI.TypedVar] -> Sem r [Int] +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 diff --git a/src/Disco/Exhaustiveness/Constraint.hs b/src/Disco/Exhaustiveness/Constraint.hs index 646c97d6..a1ced538 100644 --- a/src/Disco/Exhaustiveness/Constraint.hs +++ b/src/Disco/Exhaustiveness/Constraint.hs @@ -1,7 +1,7 @@ module Disco.Exhaustiveness.Constraint where import Control.Applicative (Alternative) -import Control.Monad (foldM, guard, replicateM) +import Control.Monad (foldM, guard) import Control.Monad.Trans (lift) import Control.Monad.Trans.Maybe (MaybeT, runMaybeT) import Data.List (partition) @@ -9,6 +9,8 @@ import Data.Maybe (isJust, listToMaybe, mapMaybe) import Disco.Effects.Fresh (Fresh) import qualified Disco.Exhaustiveness.TypeInfo as TI import Polysemy +import qualified Disco.Types as Ty +import Polysemy.Reader newtype Context = Context {getCtxVars :: [TI.TypedVar]} deriving (Show, Eq) @@ -47,15 +49,15 @@ onVar x cs = alistLookup (lookupVar x cs) cs type NormRefType = (Context, [ConstraintFor]) -addConstraints :: (Members '[Fresh] r) => NormRefType -> [ConstraintFor] -> MaybeT (Sem r) NormRefType +addConstraints :: Members '[Fresh, Reader Ty.TyDefCtx] r => NormRefType -> [ConstraintFor] -> MaybeT (Sem r) NormRefType addConstraints = foldM addConstraint -addConstraint :: (Members '[Fresh] r) => NormRefType -> ConstraintFor -> MaybeT (Sem r) NormRefType +addConstraint :: Members '[Fresh, Reader Ty.TyDefCtx] r => NormRefType -> ConstraintFor -> MaybeT (Sem r) NormRefType addConstraint nref@(_, cns) (x, c) = do breakIf $ any (conflictsWith c) (onVar x cns) addConstraintHelper nref (lookupVar x cns, c) -addConstraintHelper :: (Members '[Fresh] r) => NormRefType -> ConstraintFor -> MaybeT (Sem r) NormRefType +addConstraintHelper :: Members '[Fresh, Reader Ty.TyDefCtx] r => NormRefType -> ConstraintFor -> MaybeT (Sem r) NormRefType addConstraintHelper nref@(ctx, cns) cf@(origX, c) = case c of --- Equation (10) CMatch k args -> do @@ -126,17 +128,19 @@ substituteVarIDs y x = map (\(var, c) -> (subst var, c)) -- This function tests if this is true -- NOTE(colin): we may eventually have type constraints -- and we would need to worry pulling them from nref here -inhabited :: (Members '[Fresh] r) => NormRefType -> TI.TypedVar -> Sem r Bool -inhabited n var = case TI.tyDataCons . TI.getType $ var of - Nothing -> return True -- assume opaque types are inhabited - Just constructors -> do - or <$> mapM (instantiate n var) constructors +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 + Nothing -> return True -- assume opaque types are inhabited + Just 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] r) => NormRefType -> TI.TypedVar -> TI.DataCon -> Sem r Bool +instantiate :: Members '[Fresh, Reader Ty.TyDefCtx] r => NormRefType -> TI.TypedVar -> TI.DataCon -> Sem r Bool instantiate (ctx, cns) var k = do args <- TI.newVars $ TI.dcTypes k let attempt = (ctx `addVars` args, cns) `addConstraint` (var, CMatch k args) diff --git a/src/Disco/Exhaustiveness/TypeInfo.hs b/src/Disco/Exhaustiveness/TypeInfo.hs index 462158a2..1fd098dc 100644 --- a/src/Disco/Exhaustiveness/TypeInfo.hs +++ b/src/Disco/Exhaustiveness/TypeInfo.hs @@ -1,6 +1,7 @@ module Disco.Exhaustiveness.TypeInfo where import Control.Monad (replicateM) +import qualified Data.Map as M import Disco.AST.Typed (ATerm) import Disco.Effects.Fresh (Fresh, fresh) import qualified Disco.Types as Ty @@ -63,32 +64,38 @@ left tl = DataCon {dcIdent = KLeft, dcTypes = [tl]} right :: Ty.Type -> DataCon right tr = DataCon {dcIdent = KRight, dcTypes = [tr]} -{- -TODO(colin): Fill out the remaining types here -Remaining: - TyVar - , TySkolem - , TyProp - , TyBag - , TySet - , TyGraph - , TyMap - , TyUser -Impossible: - , (:->:) --} -tyDataCons :: Ty.Type -> Maybe [DataCon] -tyDataCons (a Ty.:*: b) = Just [pair a b] -tyDataCons (l Ty.:+: r) = Just [left l, right r] -tyDataCons t@(Ty.TyList a) = Just [cons a t, nil] -tyDataCons Ty.TyVoid = Just [] -tyDataCons Ty.TyUnit = Just [unit] -tyDataCons Ty.TyBool = Just [bool True, bool False] -tyDataCons Ty.TyN = Nothing -tyDataCons Ty.TyZ = Nothing -tyDataCons Ty.TyF = Nothing -tyDataCons Ty.TyQ = Nothing -tyDataCons Ty.TyC = Nothing +-- TODO(colin): ask yorgey, make sure I've done this correctly +-- If I have, and this is enough, I can remove all mentions +-- of type equality constraints in Constraint.hs, +-- the lookup here will have handled that behavoir already +tyDataCons :: Ty.Type -> Ty.TyDefCtx -> Maybe [DataCon] +tyDataCons (Ty.TyUser name args) ctx = case M.lookup name ctx of + Nothing -> error $ "Type definition not found for: " ++ show name + Just (Ty.TyDefBody _argNames typeCon) -> tyDataCons (typeCon args) ctx +tyDataCons (a Ty.:*: b) _ = Just [pair a b] +tyDataCons (l Ty.:+: r) _ = Just [left l, right r] +tyDataCons t@(Ty.TyList a) _ = Just [cons a t, nil] +tyDataCons Ty.TyVoid _ = Just [] +tyDataCons Ty.TyUnit _ = Just [unit] +tyDataCons Ty.TyBool _ = Just [bool True, bool False] +tyDataCons Ty.TyN _ = Nothing +tyDataCons Ty.TyZ _ = Nothing +tyDataCons Ty.TyF _ = Nothing +tyDataCons Ty.TyQ _ = Nothing +tyDataCons Ty.TyC _ = Nothing +tyDataCons (_ Ty.:->: _) _ = error "Functions not allowed in patterns." +tyDataCons (Ty.TySet _) _ = error "Sets not allowed in patterns." +tyDataCons (Ty.TyBag _) _ = error "Bags not allowed in patterns." +-- I'm unsure about these two. +-- They may come up when doing generic stuff, +-- I haven't ecnountered them so far +-- TODO(colin): ask Yorgey about this +tyDataCons (Ty.TyVar _) _ = error "Encountered type var in pattern" +tyDataCons (Ty.TySkolem _) _ = error "Encountered skolem in pattern" +-- Unsure about these as well +tyDataCons (Ty.TyProp) _ = error "Propositions not allowed in patterns." +tyDataCons (Ty.TyMap _ _) _ = error "Maps not allowed in patterns." +tyDataCons (Ty.TyGraph _) _ = error "Graph not allowed in patterns." newName :: (Member Fresh r) => Sem r (Name ATerm) newName = fresh $ s2n "" From cbde20ef59d07950a0aa9bf56c28da9c24a7cda6 Mon Sep 17 00:00:00 2001 From: LeitMoth Date: Thu, 25 Jul 2024 22:02:59 -0500 Subject: [PATCH 12/44] Create differen inhab fn to find 3 positive examples only, more nuance in tyDataCons --- src/Disco/Exhaustiveness.hs | 141 +++++++++++++++++++------ src/Disco/Exhaustiveness/Constraint.hs | 4 +- src/Disco/Exhaustiveness/TypeInfo.hs | 45 ++++---- 3 files changed, 139 insertions(+), 51 deletions(-) diff --git a/src/Disco/Exhaustiveness.hs b/src/Disco/Exhaustiveness.hs index f07ee642..4d262fac 100644 --- a/src/Disco/Exhaustiveness.hs +++ b/src/Disco/Exhaustiveness.hs @@ -30,11 +30,11 @@ import qualified Disco.Exhaustiveness.Possibilities as Poss import qualified Disco.Exhaustiveness.TypeInfo as TI import qualified Disco.Types as Ty import Polysemy +import Polysemy.Reader import Text.Show.Pretty (pPrint) import Unbound.Generics.LocallyNameless (Name) -import Polysemy.Reader -checkClauses :: Members '[Fresh, Reader Ty.TyDefCtx, Embed IO] r => Name ATerm -> [Ty.Type] -> NonEmpty [APattern] -> Sem r () +checkClauses :: (Members '[Fresh, Reader Ty.TyDefCtx, 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) @@ -43,29 +43,37 @@ checkClauses name types pats = do let argsNref = (C.Context args, []) (normalizedNrefs, annotated) <- ua [argsNref] gdt - inhab <- Poss.getPossibilities <$> findInhabitants normalizedNrefs args - + -- inhab <- Poss.getPossibilities <$> findInhabitants normalizedNrefs args redundant <- findRedundant annotated args - when False $ do - embed $ putStrLn "=====DEBUG==============================" - embed $ putStrLn "GDT:" - embed $ pPrint gdt - embed $ putStrLn "UNCOVERED:" - embed $ pPrint inhab - embed $ putStrLn "REDUNDANT:" - embed $ pPrint redundant - embed $ putStrLn "=====GUBED==============================" + examples <- findPosExamples normalizedNrefs args - let jspace = foldr (\a b -> a ++ " " ++ b) "" + -- when False $ do + -- embed $ putStrLn "=====DEBUG==============================" + -- embed $ putStrLn "GDT:" + -- embed $ pPrint gdt + -- embed $ putStrLn "UNCOVERED:" + -- embed $ pPrint inhab + -- embed $ putStrLn "REDUNDANT:" + -- embed $ pPrint redundant + -- embed $ putStrLn "=====GUBED==============================" - when (not . null $ inhab) $ do - let patLine ipats = do - let ipatArgs = jspace (map prettyInhab ipats) - putStrLn $ show name ++ " " ++ ipatArgs ++ "= ..." + let jspace = foldr (\a b -> a ++ " " ++ b) "" - embed $ putStrLn $ "Warning: You haven't matched against:" - embed $ forM_ inhab patLine + -- when (not . null $ inhab) $ do + -- let patLine ipats = do + -- let ipatArgs = jspace (map prettyInhab ipats) + -- putStrLn $ show name ++ " " ++ ipatArgs ++ "= ..." + -- + -- embed $ putStrLn $ "Warning: You haven't matched against:" + -- embed $ forM_ inhab patLine + + when (not . null $ examples) $ do + embed $ putStrLn $ "Warning: You haven't covered these cases:" + let exampleLine exArgs = do + let line = jspace (map prettyExample exArgs) + putStrLn $ show name ++ " " ++ line ++ "= ..." + embed $ forM_ examples exampleLine when (not . null $ redundant) $ do embed $ putStrLn $ "Warning: In function \"" ++ show name ++ "\", these clause numbers (1-indexed) are redundant:" @@ -180,7 +188,7 @@ data Ant where ABranch :: Ant -> Ant -> Ant deriving (Show) -ua :: Members '[Fresh, Reader Ty.TyDefCtx] r => [C.NormRefType] -> Gdt -> Sem r ([C.NormRefType], Ant) +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 @@ -196,7 +204,7 @@ ua nrefs gdt = case gdt of 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 :: (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 @@ -206,7 +214,7 @@ addLitMulti (n : ns) lit = do ns' <- addLitMulti ns lit return $ (ctx, cfs) : ns' -addLiteral :: Members '[Fresh, Reader Ty.TyDefCtx] r => C.NormRefType -> Literal -> MaybeT (Sem r) C.NormRefType +addLiteral :: (Members '[Fresh, Reader Ty.TyDefCtx] r) => C.NormRefType -> Literal -> MaybeT (Sem r) C.NormRefType addLiteral (context, constraints) (Literal (x, c)) = case c of LitWasOriginally z -> (context `C.addVars` [x], constraints) `C.addConstraint` (x, C.CWasOriginally z) @@ -246,12 +254,28 @@ prettyInhab (IPIs TI.DataCon {TI.dcIdent = TI.KPair, TI.dcTypes = _} [ifst, isnd prettyInhab (IPIs TI.DataCon {TI.dcIdent = TI.KCons, TI.dcTypes = _} [ihead, itail]) = "(" ++ prettyInhab ihead ++ " :: " ++ prettyInhab itail ++ ")" prettyInhab (IPIs TI.DataCon {TI.dcIdent = TI.KLeft, TI.dcTypes = _} [l]) = - "left(" ++ prettyInhab l ++ ")" + "(left " ++ prettyInhab l ++ ")" prettyInhab (IPIs TI.DataCon {TI.dcIdent = TI.KRight, TI.dcTypes = _} [r]) = - "right(" ++ prettyInhab r ++ ")" + "(right " ++ prettyInhab r ++ ")" prettyInhab (IPIs dc []) = dcToString dc prettyInhab (IPIs dc args) = dcToString dc ++ " " ++ joinSpace (map prettyInhab args) +data ExamplePat where + ExamplePat :: TI.DataCon -> [ExamplePat] -> ExamplePat + deriving (Show) + +prettyExample :: ExamplePat -> String +prettyExample (ExamplePat TI.DataCon {TI.dcIdent = TI.KPair, TI.dcTypes = _} [ifst, isnd]) = + "(" ++ prettyExample ifst ++ ", " ++ prettyExample isnd ++ ")" +prettyExample (ExamplePat TI.DataCon {TI.dcIdent = TI.KCons, TI.dcTypes = _} [ihead, itail]) = + "(" ++ prettyExample ihead ++ " :: " ++ prettyExample itail ++ ")" +prettyExample (ExamplePat TI.DataCon {TI.dcIdent = TI.KLeft, TI.dcTypes = _} [l]) = + "(left " ++ prettyExample l ++ ")" +prettyExample (ExamplePat TI.DataCon {TI.dcIdent = TI.KRight, TI.dcTypes = _} [r]) = + "(right " ++ prettyExample r ++ ")" +prettyExample (ExamplePat dc []) = dcToString dc +prettyExample (ExamplePat dc args) = dcToString dc ++ " " ++ joinSpace (map prettyExample args) + dcToString :: TI.DataCon -> String dcToString TI.DataCon {TI.dcIdent = ident} = case ident of TI.KBool b -> show b @@ -259,6 +283,7 @@ dcToString TI.DataCon {TI.dcIdent = ident} = case ident of TI.KNat n -> show n TI.KNil -> "[]" TI.KUnit -> "unit" + TI.KUnkown -> "_" -- TODO(colin): find a way to remove these? These two shouldn't be reachable -- If we were in an IPIs, we already handled these above -- If we were in an IPNot, these aren't from opaque types, @@ -276,17 +301,21 @@ mkIPMatch k 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]) +-- No longer used to report to the user like in Haskell +-- we use findPosExamples instead because we think that will be easier +-- on a student using disco for the first time +-- However, this function is still used in redundancy checking +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 :: (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 :: (Members '[Fresh, Reader Ty.TyDefCtx] r) => TI.TypedVar -> C.NormRefType -> Sem r (Poss.Possibilities InhabPat) findVarInhabitants var nref@(_, cns) = case posMatch of Just (k, args) -> do @@ -297,8 +326,8 @@ findVarInhabitants var nref@(_, cns) = neg -> do tyCtx <- ask @Ty.TyDefCtx case TI.tyDataCons (TI.getType var) tyCtx of - Nothing -> Poss.retSingle $ IPNot neg - Just dcs -> + TI.Infinite _ -> Poss.retSingle $ IPNot neg + TI.Finite dcs -> do let tryAddDc dc = do vars <- TI.newVars (TI.dcTypes dc) @@ -318,9 +347,59 @@ findVarInhabitants var nref@(_, cns) = posMatch = C.posMatch constraintsOnX negMatches = C.negMatches constraintsOnX -findRedundant :: Members '[Fresh, Reader Ty.TyDefCtx] r => Ant -> [TI.TypedVar] -> Sem r [Int] +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 + +-- 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. +findPosExamples :: (Members '[Fresh, Reader Ty.TyDefCtx] r) => [C.NormRefType] -> [TI.TypedVar] -> Sem r [[ExamplePat]] +findPosExamples nrefs args = do + a <- forM nrefs (`findAllPosForNref` args) + return $ take 3 $ Poss.getPossibilities $ Poss.anyOf a + +findAllPosForNref :: (Members '[Fresh, Reader Ty.TyDefCtx] r) => C.NormRefType -> [TI.TypedVar] -> Sem r (Poss.Possibilities [ExamplePat]) +findAllPosForNref nref args = do + argPats <- forM args (`findVarPosExamples` nref) + return $ Poss.allCombinations argPats + +findVarPosExamples :: (Members '[Fresh, Reader Ty.TyDefCtx] r) => TI.TypedVar -> C.NormRefType -> Sem r (Poss.Possibilities ExamplePat) +findVarPosExamples var nref@(_, cns) = + case posMatch of + Just (k, args) -> do + argPossibilities <- findAllPosForNref nref 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 (nref `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 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 (\x -> not (x `elem` 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 index a1ced538..95187964 100644 --- a/src/Disco/Exhaustiveness/Constraint.hs +++ b/src/Disco/Exhaustiveness/Constraint.hs @@ -132,8 +132,8 @@ inhabited :: Members '[Fresh, Reader Ty.TyDefCtx] r => NormRefType -> TI.TypedVa inhabited n var = do tyCtx <- ask @Ty.TyDefCtx case TI.tyDataCons (TI.getType var) tyCtx of - Nothing -> return True -- assume opaque types are inhabited - Just constructors -> do + 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 diff --git a/src/Disco/Exhaustiveness/TypeInfo.hs b/src/Disco/Exhaustiveness/TypeInfo.hs index 1fd098dc..c7693944 100644 --- a/src/Disco/Exhaustiveness/TypeInfo.hs +++ b/src/Disco/Exhaustiveness/TypeInfo.hs @@ -35,8 +35,16 @@ data Ident where KChar :: Char -> Ident KLeft :: Ident KRight :: Ident + KUnkown :: Ident deriving (Eq, Ord, Show) +data Constructors where + Finite :: [DataCon] -> Constructors + Infinite :: [DataCon] -> Constructors + +unknown :: DataCon +unknown = DataCon {dcIdent = KUnkown, dcTypes = []} + unit :: DataCon unit = DataCon {dcIdent = KUnit, dcTypes = []} @@ -68,31 +76,32 @@ right tr = DataCon {dcIdent = KRight, dcTypes = [tr]} -- If I have, and this is enough, I can remove all mentions -- of type equality constraints in Constraint.hs, -- the lookup here will have handled that behavoir already -tyDataCons :: Ty.Type -> Ty.TyDefCtx -> Maybe [DataCon] +tyDataCons :: Ty.Type -> Ty.TyDefCtx -> Constructors tyDataCons (Ty.TyUser name args) ctx = case M.lookup name ctx of Nothing -> error $ "Type definition not found for: " ++ show name Just (Ty.TyDefBody _argNames typeCon) -> tyDataCons (typeCon args) ctx -tyDataCons (a Ty.:*: b) _ = Just [pair a b] -tyDataCons (l Ty.:+: r) _ = Just [left l, right r] -tyDataCons t@(Ty.TyList a) _ = Just [cons a t, nil] -tyDataCons Ty.TyVoid _ = Just [] -tyDataCons Ty.TyUnit _ = Just [unit] -tyDataCons Ty.TyBool _ = Just [bool True, bool False] -tyDataCons Ty.TyN _ = Nothing -tyDataCons Ty.TyZ _ = Nothing -tyDataCons Ty.TyF _ = Nothing -tyDataCons Ty.TyQ _ = Nothing -tyDataCons Ty.TyC _ = Nothing +tyDataCons (a Ty.:*: b) _ = Finite [pair a b] +tyDataCons (l Ty.:+: r) _ = Finite [left l, right r] +tyDataCons t@(Ty.TyList a) _ = Finite [cons a t, nil] +tyDataCons Ty.TyVoid _ = Finite [] +tyDataCons Ty.TyUnit _ = Finite [unit] +tyDataCons Ty.TyBool _ = Finite [bool True, bool False] +tyDataCons Ty.TyN _ = Infinite $ map natural [0,1..] +tyDataCons Ty.TyZ _ = Infinite [] -- TODO(colin): IMPORTANT! fill these in! +tyDataCons Ty.TyF _ = Infinite [] +tyDataCons Ty.TyQ _ = Infinite [] +tyDataCons Ty.TyC _ = Infinite [] tyDataCons (_ Ty.:->: _) _ = error "Functions not allowed in patterns." tyDataCons (Ty.TySet _) _ = error "Sets not allowed in patterns." tyDataCons (Ty.TyBag _) _ = error "Bags not allowed in patterns." --- I'm unsure about these two. --- They may come up when doing generic stuff, --- I haven't ecnountered them so far --- TODO(colin): ask Yorgey about this -tyDataCons (Ty.TyVar _) _ = error "Encountered type var in pattern" +-- This caused a problem in findPosExamples, +-- we were trying to list of the constructors of an unknown type +-- Here we return an Infinite to prevent the lyg algorithm +-- from thinking a complete list of constructors exists, +-- and pretty print this as "_" when displaying the result of findPosExamples +tyDataCons (Ty.TyVar _) _ = Infinite [unknown] +-- Unsure about these... tyDataCons (Ty.TySkolem _) _ = error "Encountered skolem in pattern" --- Unsure about these as well tyDataCons (Ty.TyProp) _ = error "Propositions not allowed in patterns." tyDataCons (Ty.TyMap _ _) _ = error "Maps not allowed in patterns." tyDataCons (Ty.TyGraph _) _ = error "Graph not allowed in patterns." From d7bc449d16a684dc3e0a59ec33f725ffc5e54260 Mon Sep 17 00:00:00 2001 From: LeitMoth Date: Wed, 31 Jul 2024 18:43:10 -0500 Subject: [PATCH 13/44] use Output Messages / limit depth of example-finding to stop infinite loops in list examples --- src/Disco/Eval.hs | 2 +- src/Disco/Exhaustiveness.hs | 83 +++++++++++++++++----------- src/Disco/Exhaustiveness/TypeInfo.hs | 11 +++- 3 files changed, 61 insertions(+), 35 deletions(-) diff --git a/src/Disco/Eval.hs b/src/Disco/Eval.hs index a66aee96..834679e0 100644 --- a/src/Disco/Eval.hs +++ b/src/Disco/Eval.hs @@ -449,7 +449,7 @@ loadDef x body = do v <- inputToState @TopInfo . inputTopEnv $ eval body modify @TopInfo $ topEnv %~ Ctx.insert x v -checkExhaustive :: Members '[Fresh, Embed IO] r => TyDefCtx -> Defn -> Sem r () +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 index 4d262fac..fd5cae6b 100644 --- a/src/Disco/Exhaustiveness.hs +++ b/src/Disco/Exhaustiveness.hs @@ -28,13 +28,16 @@ import Disco.Effects.Fresh (Fresh) 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 qualified Disco.Pretty.DSL as DSL import qualified Disco.Types as Ty import Polysemy +import Polysemy.Output import Polysemy.Reader import Text.Show.Pretty (pPrint) import Unbound.Generics.LocallyNameless (Name) -checkClauses :: (Members '[Fresh, Reader Ty.TyDefCtx, Embed IO] r) => Name ATerm -> [Ty.Type] -> NonEmpty [APattern] -> Sem r () +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) @@ -58,8 +61,6 @@ checkClauses name types pats = do -- embed $ pPrint redundant -- embed $ putStrLn "=====GUBED==============================" - let jspace = foldr (\a b -> a ++ " " ++ b) "" - -- when (not . null $ inhab) $ do -- let patLine ipats = do -- let ipatArgs = jspace (map prettyInhab ipats) @@ -69,11 +70,25 @@ checkClauses name types pats = do -- embed $ forM_ inhab patLine when (not . null $ examples) $ do - embed $ putStrLn $ "Warning: You haven't covered these cases:" - let exampleLine exArgs = do - let line = jspace (map prettyExample exArgs) - putStrLn $ show name ++ " " ++ line ++ "= ..." - embed $ forM_ examples exampleLine + -- let jspace = foldr (\a b -> a ++ " " ++ b) "" + -- embed $ putStrLn $ "Warning: You haven't covered these cases:" + -- let exampleLine exArgs = do + -- let line = jspace (map prettyExample exArgs) + -- putStrLn $ show name ++ " " ++ line ++ "= ..." + -- embed $ forM_ examples exampleLine + + let prettyExampleArgs exArgs = + DSL.hsep $ map (DSL.text . prettyExample) 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: You haven't covered these cases:" + DSL.$+$ prettyExamples when (not . null $ redundant) $ do embed $ putStrLn $ "Warning: In function \"" ++ show name ++ "\", these clause numbers (1-indexed) are redundant:" @@ -357,35 +372,41 @@ findRedundant ant args = case ant of -- 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 habbit 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 (`findAllPosForNref` args) + a <- forM nrefs (\nref -> findAllPosForNref 32 nref args) return $ take 3 $ Poss.getPossibilities $ Poss.anyOf a -findAllPosForNref :: (Members '[Fresh, Reader Ty.TyDefCtx] r) => C.NormRefType -> [TI.TypedVar] -> Sem r (Poss.Possibilities [ExamplePat]) -findAllPosForNref nref args = do - argPats <- forM args (`findVarPosExamples` nref) +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) => TI.TypedVar -> C.NormRefType -> Sem r (Poss.Possibilities ExamplePat) -findVarPosExamples var nref@(_, cns) = - case posMatch of - Just (k, args) -> do - argPossibilities <- findAllPosForNref nref 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 (nref `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 var) +findVarPosExamples :: (Members '[Fresh, Reader Ty.TyDefCtx] r) => Int -> TI.TypedVar -> C.NormRefType -> Sem r (Poss.Possibilities ExamplePat) +findVarPosExamples fuel var nref@(_, cns) = + if fuel < 0 + then return mempty + else case posMatch of + Just (k, args) -> do + argPossibilities <- findAllPosForNref (fuel - 1) nref 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 (nref `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 diff --git a/src/Disco/Exhaustiveness/TypeInfo.hs b/src/Disco/Exhaustiveness/TypeInfo.hs index c7693944..78749dc0 100644 --- a/src/Disco/Exhaustiveness/TypeInfo.hs +++ b/src/Disco/Exhaustiveness/TypeInfo.hs @@ -82,15 +82,20 @@ tyDataCons (Ty.TyUser name args) ctx = case M.lookup name ctx of Just (Ty.TyDefBody _argNames typeCon) -> tyDataCons (typeCon args) ctx tyDataCons (a Ty.:*: b) _ = Finite [pair a b] tyDataCons (l Ty.:+: r) _ = Finite [left l, right r] -tyDataCons t@(Ty.TyList a) _ = Finite [cons a t, nil] +tyDataCons t@(Ty.TyList a) _ = Finite [nil, cons a t] tyDataCons Ty.TyVoid _ = Finite [] tyDataCons Ty.TyUnit _ = Finite [unit] tyDataCons Ty.TyBool _ = Finite [bool True, bool False] -tyDataCons Ty.TyN _ = Infinite $ map natural [0,1..] +tyDataCons Ty.TyN _ = Infinite $ map natural [0, 1 ..] tyDataCons Ty.TyZ _ = Infinite [] -- TODO(colin): IMPORTANT! fill these in! tyDataCons Ty.TyF _ = Infinite [] tyDataCons Ty.TyQ _ = Infinite [] -tyDataCons Ty.TyC _ = Infinite [] +-- We could do all valid ASCII, but this is most likely good enough +-- I think these starting from 'a' is good for students learning the language +tyDataCons Ty.TyC _ = + Infinite $ + map char $ + ['a' .. 'z'] ++ ['A' .. 'Z'] ++ ['0' .. '9'] tyDataCons (_ Ty.:->: _) _ = error "Functions not allowed in patterns." tyDataCons (Ty.TySet _) _ = error "Sets not allowed in patterns." tyDataCons (Ty.TyBag _) _ = error "Bags not allowed in patterns." From 4e6c24da347315e2d39978c00346f691d30df63f Mon Sep 17 00:00:00 2001 From: LeitMoth Date: Wed, 14 Aug 2024 22:02:01 -0500 Subject: [PATCH 14/44] Fix bug, now we get the Tydefs from the correct location --- src/Disco/Eval.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Disco/Eval.hs b/src/Disco/Eval.hs index 834679e0..a0c8c654 100644 --- a/src/Disco/Eval.hs +++ b/src/Disco/Eval.hs @@ -387,7 +387,7 @@ loadParsedDiscoModule' quiet mode resolver inProcess name cm@(Module _ mns _ _ _ m <- runTCM tyctx tydefns $ checkModule name importMap cm -- Check for partial functions - runFresh $ mapM_ (checkExhaustive tydefns) (Ctx.elems $ m^.miTermdefs) + runFresh $ mapM_ (checkExhaustive $ m^.miTydefs) (Ctx.elems $ m^.miTermdefs) -- Evaluate all the module definitions and add them to the topEnv. mapError EvalErr $ loadDefsFrom m From d2915633ca35239011985f9cfbaaec8bacf0a8ec Mon Sep 17 00:00:00 2001 From: LeitMoth Date: Wed, 14 Aug 2024 22:16:22 -0500 Subject: [PATCH 15/44] Fix bug cause by previous fix, now we merge both repl and module tydefs --- src/Disco/Eval.hs | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/Disco/Eval.hs b/src/Disco/Eval.hs index a0c8c654..758041be 100644 --- a/src/Disco/Eval.hs +++ b/src/Disco/Eval.hs @@ -387,7 +387,8 @@ loadParsedDiscoModule' quiet mode resolver inProcess name cm@(Module _ mns _ _ _ m <- runTCM tyctx tydefns $ checkModule name importMap cm -- Check for partial functions - runFresh $ mapM_ (checkExhaustive $ m^.miTydefs) (Ctx.elems $ m^.miTermdefs) + 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 From 6ac776cd49423443176aa2708a6bec313bce8f9b Mon Sep 17 00:00:00 2001 From: LeitMoth Date: Wed, 14 Aug 2024 23:53:02 -0500 Subject: [PATCH 16/44] mid refactor - all tests pass! --- src/Disco/Exhaustiveness.hs | 14 +++---- src/Disco/Exhaustiveness/TypeInfo.hs | 61 ++++++++++++++++------------ 2 files changed, 43 insertions(+), 32 deletions(-) diff --git a/src/Disco/Exhaustiveness.hs b/src/Disco/Exhaustiveness.hs index fd5cae6b..4516c361 100644 --- a/src/Disco/Exhaustiveness.hs +++ b/src/Disco/Exhaustiveness.hs @@ -50,17 +50,17 @@ checkClauses name types pats = do redundant <- findRedundant annotated args examples <- findPosExamples normalizedNrefs args - - -- when False $ do + -- + -- when True $ do -- embed $ putStrLn "=====DEBUG==============================" -- embed $ putStrLn "GDT:" -- embed $ pPrint gdt -- embed $ putStrLn "UNCOVERED:" - -- embed $ pPrint inhab + -- embed $ pPrint normalizedNrefs -- embed $ putStrLn "REDUNDANT:" -- embed $ pPrint redundant -- embed $ putStrLn "=====GUBED==============================" - + -- -- when (not . null $ inhab) $ do -- let patLine ipats = do -- let ipatArgs = jspace (map prettyInhab ipats) @@ -90,9 +90,9 @@ checkClauses name types pats = do DSL.text "Warning: You haven't covered these cases:" DSL.$+$ prettyExamples - when (not . null $ redundant) $ do - embed $ putStrLn $ "Warning: In function \"" ++ show name ++ "\", these clause numbers (1-indexed) are redundant:" - embed $ putStrLn $ show redundant + -- when (not . null $ redundant) $ do + -- embed $ putStrLn $ "Warning: In function \"" ++ show name ++ "\", these clause numbers (1-indexed) are redundant:" + -- embed $ putStrLn $ show redundant return () diff --git a/src/Disco/Exhaustiveness/TypeInfo.hs b/src/Disco/Exhaustiveness/TypeInfo.hs index 78749dc0..b161e0de 100644 --- a/src/Disco/Exhaustiveness/TypeInfo.hs +++ b/src/Disco/Exhaustiveness/TypeInfo.hs @@ -1,6 +1,7 @@ module Disco.Exhaustiveness.TypeInfo where import Control.Monad (replicateM) +import Data.Function (on) import qualified Data.Map as M import Disco.AST.Typed (ATerm) import Disco.Effects.Fresh (Fresh, fresh) @@ -23,7 +24,10 @@ data DataCon = DataCon { dcIdent :: Ident, dcTypes :: [Ty.Type] } - deriving (Eq, Ord, Show) + deriving (Ord, Show) + +instance Eq DataCon where + (==) = (==) `on` dcIdent data Ident where KUnit :: Ident @@ -72,44 +76,51 @@ 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 + +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 + -- TODO(colin): ask yorgey, make sure I've done this correctly -- If I have, and this is enough, I can remove all mentions -- of type equality constraints in Constraint.hs, -- the lookup here will have handled that behavoir already -tyDataCons :: Ty.Type -> Ty.TyDefCtx -> Constructors -tyDataCons (Ty.TyUser name args) ctx = case M.lookup name ctx of - Nothing -> error $ "Type definition not found for: " ++ show name - Just (Ty.TyDefBody _argNames typeCon) -> tyDataCons (typeCon args) ctx -tyDataCons (a Ty.:*: b) _ = Finite [pair a b] -tyDataCons (l Ty.:+: r) _ = Finite [left l, right r] -tyDataCons t@(Ty.TyList a) _ = Finite [nil, cons a t] -tyDataCons Ty.TyVoid _ = Finite [] -tyDataCons Ty.TyUnit _ = Finite [unit] -tyDataCons Ty.TyBool _ = Finite [bool True, bool False] -tyDataCons Ty.TyN _ = Infinite $ map natural [0, 1 ..] -tyDataCons Ty.TyZ _ = Infinite [] -- TODO(colin): IMPORTANT! fill these in! -tyDataCons Ty.TyF _ = Infinite [] -tyDataCons Ty.TyQ _ = Infinite [] +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 ..] +tyDataConsHelper Ty.TyZ = Infinite [] -- TODO(colin): IMPORTANT! fill these in! +tyDataConsHelper Ty.TyF = Infinite [] +tyDataConsHelper Ty.TyQ = Infinite [] -- We could do all valid ASCII, but this is most likely good enough -- I think these starting from 'a' is good for students learning the language -tyDataCons Ty.TyC _ = +tyDataConsHelper Ty.TyC = Infinite $ map char $ ['a' .. 'z'] ++ ['A' .. 'Z'] ++ ['0' .. '9'] -tyDataCons (_ Ty.:->: _) _ = error "Functions not allowed in patterns." -tyDataCons (Ty.TySet _) _ = error "Sets not allowed in patterns." -tyDataCons (Ty.TyBag _) _ = error "Bags not allowed in patterns." -- This caused a problem in findPosExamples, -- we were trying to list of the constructors of an unknown type -- Here we return an Infinite to prevent the lyg algorithm -- from thinking a complete list of constructors exists, -- and pretty print this as "_" when displaying the result of findPosExamples -tyDataCons (Ty.TyVar _) _ = Infinite [unknown] --- Unsure about these... -tyDataCons (Ty.TySkolem _) _ = error "Encountered skolem in pattern" -tyDataCons (Ty.TyProp) _ = error "Propositions not allowed in patterns." -tyDataCons (Ty.TyMap _ _) _ = error "Maps not allowed in patterns." -tyDataCons (Ty.TyGraph _) _ = error "Graph not allowed in patterns." +tyDataConsHelper _ = Infinite [unknown] +-- ^ This includes: +-- tyDataCons (_ Ty.:->: _) +-- tyDataCons (Ty.TySet _) +-- tyDataCons (Ty.TyBag _) +-- tyDataCons (Ty.TyVar _) +-- tyDataCons (Ty.TySkolem _) +-- tyDataCons (Ty.TyProp) +-- tyDataCons (Ty.TyMap _ _) +-- tyDataCons (Ty.TyGraph _) newName :: (Member Fresh r) => Sem r (Name ATerm) newName = fresh $ s2n "" From 5bd7d59fb3cf6f36d943b096655e620ac2db446a Mon Sep 17 00:00:00 2001 From: LeitMoth Date: Thu, 15 Aug 2024 00:25:28 -0500 Subject: [PATCH 17/44] add integers + small cleanup --- src/Disco/Exhaustiveness.hs | 66 ++++++----------------- src/Disco/Exhaustiveness/Constraint.hs | 40 +++++++------- src/Disco/Exhaustiveness/Possibilities.hs | 50 ++++++++--------- src/Disco/Exhaustiveness/TypeInfo.hs | 29 +++++----- 4 files changed, 74 insertions(+), 111 deletions(-) diff --git a/src/Disco/Exhaustiveness.hs b/src/Disco/Exhaustiveness.hs index 4516c361..20dd4822 100644 --- a/src/Disco/Exhaustiveness.hs +++ b/src/Disco/Exhaustiveness.hs @@ -2,7 +2,7 @@ module Disco.Exhaustiveness where -import Control.Monad (forM, forM_, when, zipWithM) +import Control.Monad (forM, when, zipWithM) import Control.Monad.Trans.Maybe (MaybeT, runMaybeT) import Data.List (nub) import Data.List.NonEmpty (NonEmpty) @@ -23,6 +23,7 @@ import Disco.AST.Typed pattern APUnit, pattern APVar, pattern APWild, + pattern APNeg, ) import Disco.Effects.Fresh (Fresh) import qualified Disco.Exhaustiveness.Constraint as C @@ -34,7 +35,6 @@ import qualified Disco.Types as Ty import Polysemy import Polysemy.Output import Polysemy.Reader -import Text.Show.Pretty (pPrint) import Unbound.Generics.LocallyNameless (Name) checkClauses :: (Members '[Fresh, Reader Ty.TyDefCtx, Output (Message ann), Embed IO] r) => Name ATerm -> [Ty.Type] -> NonEmpty [APattern] -> Sem r () @@ -44,39 +44,11 @@ checkClauses name types pats = do let gdt = foldr1 Branch cl let argsNref = (C.Context args, []) - (normalizedNrefs, annotated) <- ua [argsNref] gdt - - -- inhab <- Poss.getPossibilities <$> findInhabitants normalizedNrefs args - redundant <- findRedundant annotated args + (normalizedNrefs, _) <- ua [argsNref] gdt examples <- findPosExamples normalizedNrefs args - -- - -- when True $ do - -- embed $ putStrLn "=====DEBUG==============================" - -- embed $ putStrLn "GDT:" - -- embed $ pPrint gdt - -- embed $ putStrLn "UNCOVERED:" - -- embed $ pPrint normalizedNrefs - -- embed $ putStrLn "REDUNDANT:" - -- embed $ pPrint redundant - -- embed $ putStrLn "=====GUBED==============================" - -- - -- when (not . null $ inhab) $ do - -- let patLine ipats = do - -- let ipatArgs = jspace (map prettyInhab ipats) - -- putStrLn $ show name ++ " " ++ ipatArgs ++ "= ..." - -- - -- embed $ putStrLn $ "Warning: You haven't matched against:" - -- embed $ forM_ inhab patLine when (not . null $ examples) $ do - -- let jspace = foldr (\a b -> a ++ " " ++ b) "" - -- embed $ putStrLn $ "Warning: You haven't covered these cases:" - -- let exampleLine exArgs = do - -- let line = jspace (map prettyExample exArgs) - -- putStrLn $ show name ++ " " ++ line ++ "= ..." - -- embed $ forM_ examples exampleLine - let prettyExampleArgs exArgs = DSL.hsep $ map (DSL.text . prettyExample) exArgs @@ -90,10 +62,6 @@ checkClauses name types pats = do DSL.text "Warning: You haven't covered these cases:" DSL.$+$ prettyExamples - -- when (not . null $ redundant) $ do - -- embed $ putStrLn $ "Warning: In function \"" ++ show name ++ "\", these clause numbers (1-indexed) are redundant:" - -- embed $ putStrLn $ show redundant - return () desugarClause :: (Members '[Fresh, Embed IO] r) => [TI.TypedVar] -> Int -> [APattern] -> Sem r Gdt @@ -119,7 +87,7 @@ desugarTuplePats (pfst : rest) = APTup (Ty.getType pfst Ty.:*: Ty.getType psnd) {- TODO(colin): handle remaining patterns - , APNeg --required for integers / rationals? + , APNeg --still need to handle rational case , APFrac --required for rationals? algebraic (probably will be replaced anyway): , APAdd @@ -157,12 +125,15 @@ desugarMatch var pat = do (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)] - (APNat _ nat) -> return [(var, GMatch (TI.natural nat) [])] (APUnit) -> return [(var, GMatch TI.unit [])] (APBool b) -> return [(var, GMatch (TI.bool b) [])] (APChar c) -> return [(var, GMatch (TI.char c) [])] @@ -175,7 +146,7 @@ desugarMatch var pat = do R -> TI.newVar tr guards <- desugarMatch newVar subPat return $ [(var, GMatch dc [newVar])] ++ guards - e -> return [] + _ -> return [] data Gdt where Grhs :: Int -> Gdt @@ -296,6 +267,7 @@ dcToString TI.DataCon {TI.dcIdent = ident} = case ident of TI.KBool b -> show b TI.KChar c -> show c TI.KNat n -> show n + TI.KInt z -> show z TI.KNil -> "[]" TI.KUnit -> "unit" TI.KUnkown -> "_" @@ -316,10 +288,6 @@ mkIPMatch k pats = then error $ "Wrong number of DataCon args" ++ show (k, pats) else IPIs k pats --- No longer used to report to the user like in Haskell --- we use findPosExamples instead because we think that will be easier --- on a student using disco for the first time --- However, this function is still used in redundancy checking 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) @@ -369,13 +337,13 @@ findRedundant ant args = case ant of return [i | uninhabited] ABranch a1 a2 -> mappend <$> findRedundant a1 args <*> findRedundant a2 args --- 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 habbit 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 +-- | 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) diff --git a/src/Disco/Exhaustiveness/Constraint.hs b/src/Disco/Exhaustiveness/Constraint.hs index 95187964..99fb12e3 100644 --- a/src/Disco/Exhaustiveness/Constraint.hs +++ b/src/Disco/Exhaustiveness/Constraint.hs @@ -91,11 +91,11 @@ addConstraintHelper nref@(ctx, cns) cf@(origX, c) = case c of 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 +-- | 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 @@ -107,27 +107,27 @@ conflictsWith c = case c of _ -> 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 +-- | 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 +-- | 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 (\(var, c) -> (subst var, c)) where subst var = if var == x then y else x --- Deals with I2 form 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 --- NOTE(colin): we may eventually have type constraints --- and we would need to worry pulling them from nref here +-- | Deals with I2 form 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 +-- NOTE(colin): we may eventually have type constraints +-- and we would need to worry pulling them from nref here inhabited :: Members '[Fresh, Reader Ty.TyDefCtx] r => NormRefType -> TI.TypedVar -> Sem r Bool inhabited n var = do tyCtx <- ask @Ty.TyDefCtx @@ -136,10 +136,10 @@ inhabited n var = do 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 +-- | 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 (ctx, cns) var k = do args <- TI.newVars $ TI.dcTypes k diff --git a/src/Disco/Exhaustiveness/Possibilities.hs b/src/Disco/Exhaustiveness/Possibilities.hs index 1e300dee..f0352da0 100644 --- a/src/Disco/Exhaustiveness/Possibilities.hs +++ b/src/Disco/Exhaustiveness/Possibilities.hs @@ -25,34 +25,34 @@ 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] --- ]} +-- 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 +-- 2 5 +-- / \ / +-- 1 4 --6 +-- \ / \ +-- 3 7 -- --- If any any of the Possibilities is empty, --- an empty Possibility is returned +-- 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 +-- In other words, this lists all elements of the +-- cartesian product of multiple sets allCombinations :: [Possibilities a] -> Possibilities [a] allCombinations = foldr prod nil where diff --git a/src/Disco/Exhaustiveness/TypeInfo.hs b/src/Disco/Exhaustiveness/TypeInfo.hs index b161e0de..08c94e07 100644 --- a/src/Disco/Exhaustiveness/TypeInfo.hs +++ b/src/Disco/Exhaustiveness/TypeInfo.hs @@ -12,10 +12,8 @@ import Unbound.Generics.LocallyNameless (Name, s2n) newtype TypedVar = TypedVar (Name ATerm, Ty.Type) deriving (Show, Ord) --- For now, equality is always in terms of the name --- We will see if the causes problems later instance Eq TypedVar where - TypedVar (n1, _t1) == TypedVar (n2, _t2) = n1 == n2 + TypedVar (n1, _) == TypedVar (n2, _) = n1 == n2 getType :: TypedVar -> Ty.Type getType (TypedVar (_, t)) = t @@ -33,6 +31,7 @@ data Ident where KUnit :: Ident KBool :: Bool -> Ident KNat :: Integer -> Ident + KInt :: Integer -> Ident KPair :: Ident KCons :: Ident KNil :: Ident @@ -42,6 +41,9 @@ data Ident where KUnkown :: Ident deriving (Eq, Ord, Show) +-- | 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 @@ -58,6 +60,9 @@ 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 = []} @@ -97,7 +102,8 @@ 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 ..] -tyDataConsHelper Ty.TyZ = Infinite [] -- TODO(colin): IMPORTANT! fill these in! +-- TODO(colin): this integer generation was taken from stackoverflow. Is that okay? +tyDataConsHelper Ty.TyZ = Infinite $ map integer $ 0 : [y | x <- [1 ..], y <- [x, -x]] tyDataConsHelper Ty.TyF = Infinite [] tyDataConsHelper Ty.TyQ = Infinite [] -- We could do all valid ASCII, but this is most likely good enough @@ -106,21 +112,10 @@ tyDataConsHelper Ty.TyC = Infinite $ map char $ ['a' .. 'z'] ++ ['A' .. 'Z'] ++ ['0' .. '9'] --- This caused a problem in findPosExamples, --- we were trying to list of the constructors of an unknown type --- Here we return an Infinite to prevent the lyg algorithm --- from thinking a complete list of constructors exists, --- and pretty print this as "_" when displaying the result of findPosExamples tyDataConsHelper _ = Infinite [unknown] -- ^ This includes: --- tyDataCons (_ Ty.:->: _) --- tyDataCons (Ty.TySet _) --- tyDataCons (Ty.TyBag _) --- tyDataCons (Ty.TyVar _) --- tyDataCons (Ty.TySkolem _) --- tyDataCons (Ty.TyProp) --- tyDataCons (Ty.TyMap _ _) --- tyDataCons (Ty.TyGraph _) +-- (_ Ty.:->: _) (Ty.TySet _) (Ty.TyBag _) (Ty.TyVar _) +-- (Ty.TySkolem _) (Ty.TyProp) (Ty.TyMap _ _) (Ty.TyGraph _) newName :: (Member Fresh r) => Sem r (Name ATerm) newName = fresh $ s2n "" From ee39666a65c6ff99ba63227e78ecaa79fb81ad3f Mon Sep 17 00:00:00 2001 From: LeitMoth Date: Sat, 21 Sep 2024 15:53:47 -0500 Subject: [PATCH 18/44] resugar truples and lists + use prettyprinter to better display output --- src/Disco/Exhaustiveness.hs | 32 ++++++++++++++++++++++++++-- src/Disco/Exhaustiveness/TypeInfo.hs | 24 ++++++++++++++++++++- 2 files changed, 53 insertions(+), 3 deletions(-) diff --git a/src/Disco/Exhaustiveness.hs b/src/Disco/Exhaustiveness.hs index 20dd4822..c59c305a 100644 --- a/src/Disco/Exhaustiveness.hs +++ b/src/Disco/Exhaustiveness.hs @@ -18,23 +18,25 @@ import Disco.AST.Typed pattern APInj, pattern APList, pattern APNat, + pattern APNeg, pattern APString, pattern APTup, pattern APUnit, pattern APVar, pattern APWild, - pattern APNeg, ) import Disco.Effects.Fresh (Fresh) 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) import qualified Disco.Pretty.DSL as DSL import qualified Disco.Types as Ty import Polysemy import Polysemy.Output import Polysemy.Reader +import qualified Prettyprinter as PP import Unbound.Generics.LocallyNameless (Name) checkClauses :: (Members '[Fresh, Reader Ty.TyDefCtx, Output (Message ann), Embed IO] r) => Name ATerm -> [Ty.Type] -> NonEmpty [APattern] -> Sem r () @@ -50,7 +52,7 @@ checkClauses name types pats = do when (not . null $ examples) $ do let prettyExampleArgs exArgs = - DSL.hsep $ map (DSL.text . prettyExample) exArgs + DSL.hsep $ map pe exArgs let prettyExampleLine prettyArgs = DSL.text (show name) DSL.<+> prettyArgs DSL.<+> DSL.text "= ..." @@ -64,6 +66,30 @@ checkClauses name types pats = do return () +pe :: (Applicative f) => ExamplePat -> f (Doc ann) +pe e@(ExamplePat TI.DataCon {TI.dcIdent = ident} args) = case (ident, args) of + (TI.KPair, _) -> tupled (traverse pe (resugarPair e)) + (TI.KCons, _) -> list (traverse pe (resugarList e)) + (TI.KLeft, [l]) -> DSL.parens $ DSL.text "left" DSL.<+> pe l + (TI.KRight, [r]) -> DSL.parens $ DSL.text "right" DSL.<+> pe r + (_, _) -> DSL.hsep $ DSL.text (show ident) : map pe args + +tupled :: (Applicative f) => f [Doc ann] -> f (Doc ann) +tupled = fmap (PP.tupled) + +list :: (Applicative f) => f [Doc ann] -> f (Doc ann) +list = fmap (PP.list) + +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 + (_, _) -> [] + desugarClause :: (Members '[Fresh, Embed IO] r) => [TI.TypedVar] -> Int -> [APattern] -> Sem r Gdt desugarClause args clauseIdx argsPats = do guards <- zipWithM desugarMatch args argsPats @@ -93,6 +119,8 @@ TODO(colin): handle remaining patterns , APAdd , APMul , APSub +We treat unhandled patterns as if they are exhaustively matched against +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 = do diff --git a/src/Disco/Exhaustiveness/TypeInfo.hs b/src/Disco/Exhaustiveness/TypeInfo.hs index 08c94e07..71461f59 100644 --- a/src/Disco/Exhaustiveness/TypeInfo.hs +++ b/src/Disco/Exhaustiveness/TypeInfo.hs @@ -24,6 +24,10 @@ data DataCon = DataCon } 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 @@ -39,7 +43,25 @@ data Ident where KLeft :: Ident KRight :: Ident KUnkown :: Ident - deriving (Eq, Ord, Show) + deriving (Eq, Ord) + +instance Show Ident where + show i = case i of + KBool b -> show b + KChar c -> show c + KNat n -> show n + KInt z -> + if z < 0 + then "(" ++ show z ++ ")" + else show z + KNil -> "[]" + KUnit -> "unit" + KUnkown -> "_" + -- These should never actually be printed in warnings + KPair -> "," + KCons -> "::" + KLeft -> "left()" + KRight -> "right()" -- | Finite constructors are used in the LYG checker -- 'Infinite' constructors are used when reporting From 66be01311b228fd36e085a3abd9b1cdd18d85c18 Mon Sep 17 00:00:00 2001 From: LeitMoth Date: Wed, 1 Jan 2025 23:38:18 -0600 Subject: [PATCH 19/44] add credit for infinite list of integers --- src/Disco/Exhaustiveness/TypeInfo.hs | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/Disco/Exhaustiveness/TypeInfo.hs b/src/Disco/Exhaustiveness/TypeInfo.hs index 71461f59..43ef67be 100644 --- a/src/Disco/Exhaustiveness/TypeInfo.hs +++ b/src/Disco/Exhaustiveness/TypeInfo.hs @@ -124,7 +124,8 @@ 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 ..] --- TODO(colin): this integer generation was taken from stackoverflow. Is that okay? +-- 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 [] From 8683dd8ed8147cc61ecb0571bf023a1a82322610 Mon Sep 17 00:00:00 2001 From: LeitMoth Date: Thu, 2 Jan 2025 00:29:58 -0600 Subject: [PATCH 20/44] add more TODOs --- src/Disco/Exhaustiveness/TypeInfo.hs | 26 +++++++++++++++++++++----- 1 file changed, 21 insertions(+), 5 deletions(-) diff --git a/src/Disco/Exhaustiveness/TypeInfo.hs b/src/Disco/Exhaustiveness/TypeInfo.hs index 43ef67be..06e906c0 100644 --- a/src/Disco/Exhaustiveness/TypeInfo.hs +++ b/src/Disco/Exhaustiveness/TypeInfo.hs @@ -106,16 +106,18 @@ right tr = DataCon {dcIdent = KRight, dcTypes = [tr]} tyDataCons :: Ty.Type -> Ty.TyDefCtx -> Constructors tyDataCons ty ctx = tyDataConsHelper $ resolveAlias ty ctx +-- TODO(colin): ask yorgey, make sure I've done this correctly +-- If I have, and this is enough, I can remove all mentions +-- of type equality constraints in Constraint.hs, +-- the lookup here will have handled that behavoir already 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 --- TODO(colin): ask yorgey, make sure I've done this correctly --- If I have, and this is enough, I can remove all mentions --- of type equality constraints in Constraint.hs, --- the lookup here will have handled that behavoir already +-- TODO(colin): ask yorgey to see if I've handled all the thing +-- I need to here. The list of things caught by the wildcard is below tyDataConsHelper :: Ty.Type -> Constructors tyDataConsHelper (a Ty.:*: b) = Finite [pair a b] tyDataConsHelper (l Ty.:+: r) = Finite [left l, right r] @@ -129,7 +131,7 @@ tyDataConsHelper Ty.TyN = Infinite $ map natural [0, 1 ..] tyDataConsHelper Ty.TyZ = Infinite $ map integer $ 0 : [y | x <- [1 ..], y <- [x, -x]] tyDataConsHelper Ty.TyF = Infinite [] tyDataConsHelper Ty.TyQ = Infinite [] --- We could do all valid ASCII, but this is most likely good enough +-- TODO(colin): We could do all valid ASCII, but this is most likely good enough -- I think these starting from 'a' is good for students learning the language tyDataConsHelper Ty.TyC = Infinite $ @@ -139,6 +141,20 @@ tyDataConsHelper _ = Infinite [unknown] -- ^ This includes: -- (_ Ty.:->: _) (Ty.TySet _) (Ty.TyBag _) (Ty.TyVar _) -- (Ty.TySkolem _) (Ty.TyProp) (Ty.TyMap _ _) (Ty.TyGraph _) +-- TODO(colin): confim below: +-- I think all of these are impossible to pattern match against +-- with anything other than a wildcard. +-- So they should be always fully covered. +-- But if they are in a pair, like a 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)? +-- For now I'm calling that unknown, and printing an underscore +-- I believe this also applies when pattern matching 'Maybe a' types +-- We need stand in for an example of a concrete 'a' +-- +-- I remember the Infinite part making sense at the time +-- but I should probably double check that newName :: (Member Fresh r) => Sem r (Name ATerm) newName = fresh $ s2n "" From e64c82917281b8881b509c794365b88ac899fbba Mon Sep 17 00:00:00 2001 From: LeitMoth Date: Thu, 9 Jan 2025 05:35:35 +0000 Subject: [PATCH 21/44] apply all lsp hints on my files --- src/Disco/Exhaustiveness.hs | 118 ++++++++++++------------- src/Disco/Exhaustiveness/Constraint.hs | 5 +- src/Disco/Exhaustiveness/TypeInfo.hs | 4 +- 3 files changed, 62 insertions(+), 65 deletions(-) diff --git a/src/Disco/Exhaustiveness.hs b/src/Disco/Exhaustiveness.hs index c59c305a..3c05a7de 100644 --- a/src/Disco/Exhaustiveness.hs +++ b/src/Disco/Exhaustiveness.hs @@ -2,7 +2,7 @@ module Disco.Exhaustiveness where -import Control.Monad (forM, when, zipWithM) +import Control.Monad (forM, zipWithM, unless) import Control.Monad.Trans.Maybe (MaybeT, runMaybeT) import Data.List (nub) import Data.List.NonEmpty (NonEmpty) @@ -50,7 +50,7 @@ checkClauses name types pats = do examples <- findPosExamples normalizedNrefs args - when (not . null $ examples) $ do + unless (null examples) $ do let prettyExampleArgs exArgs = DSL.hsep $ map pe exArgs @@ -64,8 +64,6 @@ checkClauses name types pats = do DSL.text "Warning: You haven't covered these cases:" DSL.$+$ prettyExamples - return () - pe :: (Applicative f) => ExamplePat -> f (Doc ann) pe e@(ExamplePat TI.DataCon {TI.dcIdent = ident} args) = case (ident, args) of (TI.KPair, _) -> tupled (traverse pe (resugarPair e)) @@ -75,15 +73,15 @@ pe e@(ExamplePat TI.DataCon {TI.dcIdent = ident} args) = case (ident, args) of (_, _) -> DSL.hsep $ DSL.text (show ident) : map pe args tupled :: (Applicative f) => f [Doc ann] -> f (Doc ann) -tupled = fmap (PP.tupled) +tupled = fmap PP.tupled list :: (Applicative f) => f [Doc ann] -> f (Doc ann) -list = fmap (PP.list) +list = fmap PP.list resugarPair :: ExamplePat -> [ExamplePat] resugarPair e@(ExamplePat TI.DataCon {TI.dcIdent = ident} args) = case (ident, args) of (TI.KPair, [efst, esnd]) -> efst : resugarPair esnd - (_, _) -> e : [] + (_, _) -> [e] resugarList :: ExamplePat -> [ExamplePat] resugarList (ExamplePat TI.DataCon {TI.dcIdent = ident} args) = case (ident, args) of @@ -123,58 +121,56 @@ We treat unhandled patterns as if they are exhaustively matched against 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 = do - 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 ty [_, _]) -> error $ "Tuple type that wasn't a pair???: " ++ show ty - (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 _ []) -> do - 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 [] +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 ty [_, _]) -> error $ "Tuple type that wasn't a pair???: " ++ show ty + (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 @@ -212,7 +208,7 @@ ua nrefs gdt = case gdt of Guarded (y, GWasOriginally x) t -> do n <- addLitMulti nrefs $ Literal (y, LitWasOriginally x) ua n t - Guarded (x, (GMatch dc args)) t -> do + 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) @@ -409,7 +405,7 @@ findVarPosExamples fuel var nref@(_, cns) = negMatches = C.negMatches constraintsOnX getPosFrom :: Ty.Type -> Ty.TyDefCtx -> [TI.DataCon] -> [TI.DataCon] -getPosFrom ty ctx neg = take 3 $ filter (\x -> not (x `elem` neg)) dcs +getPosFrom ty ctx neg = take 3 $ filter (`notElem` neg) dcs where dcs = case TI.tyDataCons ty ctx of TI.Finite dcs' -> dcs' diff --git a/src/Disco/Exhaustiveness/Constraint.hs b/src/Disco/Exhaustiveness/Constraint.hs index 99fb12e3..37d23c81 100644 --- a/src/Disco/Exhaustiveness/Constraint.hs +++ b/src/Disco/Exhaustiveness/Constraint.hs @@ -11,6 +11,7 @@ import qualified Disco.Exhaustiveness.TypeInfo as TI import Polysemy import qualified Disco.Types as Ty import Polysemy.Reader +import Data.Bifunctor (first) newtype Context = Context {getCtxVars :: [TI.TypedVar]} deriving (Show, Eq) @@ -28,7 +29,7 @@ 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 constraints = mapMaybe (\case (CNot k) -> Just k; _ -> Nothing) constraints +negMatches = mapMaybe (\case (CNot k) -> Just k; _ -> Nothing) type ConstraintFor = (TI.TypedVar, Constraint) @@ -118,7 +119,7 @@ getConstructorArgs k 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 (\(var, c) -> (subst var, c)) +substituteVarIDs y x = map (first subst) where subst var = if var == x then y else x diff --git a/src/Disco/Exhaustiveness/TypeInfo.hs b/src/Disco/Exhaustiveness/TypeInfo.hs index 06e906c0..67fb30cf 100644 --- a/src/Disco/Exhaustiveness/TypeInfo.hs +++ b/src/Disco/Exhaustiveness/TypeInfo.hs @@ -162,7 +162,7 @@ newName = fresh $ s2n "" newVar :: (Member Fresh r) => Ty.Type -> Sem r TypedVar newVar types = do names <- newName - return $ TypedVar $ (names, types) + return $ TypedVar (names, types) newNames :: (Member Fresh r) => Int -> Sem r [Name ATerm] newNames i = replicateM i newName @@ -170,4 +170,4 @@ newNames i = replicateM i newName newVars :: (Member Fresh r) => [Ty.Type] -> Sem r [TypedVar] newVars types = do names <- newNames (length types) - return $ map TypedVar $ zip names types + return $ zipWith (curry TypedVar) names types From 23e1775741e2f10b62a025619510abf5dc96ad3d Mon Sep 17 00:00:00 2001 From: LeitMoth Date: Thu, 9 Jan 2025 06:15:00 +0000 Subject: [PATCH 22/44] remove old prettyrprint and rename new prettyprint --- src/Disco/Exhaustiveness.hs | 86 ++++++------------------------------- 1 file changed, 12 insertions(+), 74 deletions(-) diff --git a/src/Disco/Exhaustiveness.hs b/src/Disco/Exhaustiveness.hs index 3c05a7de..93cba434 100644 --- a/src/Disco/Exhaustiveness.hs +++ b/src/Disco/Exhaustiveness.hs @@ -52,7 +52,7 @@ checkClauses name types pats = do unless (null examples) $ do let prettyExampleArgs exArgs = - DSL.hsep $ map pe exArgs + DSL.hsep $ map prettyPrintExample exArgs let prettyExampleLine prettyArgs = DSL.text (show name) DSL.<+> prettyArgs DSL.<+> DSL.text "= ..." @@ -64,13 +64,13 @@ checkClauses name types pats = do DSL.text "Warning: You haven't covered these cases:" DSL.$+$ prettyExamples -pe :: (Applicative f) => ExamplePat -> f (Doc ann) -pe e@(ExamplePat TI.DataCon {TI.dcIdent = ident} args) = case (ident, args) of - (TI.KPair, _) -> tupled (traverse pe (resugarPair e)) - (TI.KCons, _) -> list (traverse pe (resugarList e)) - (TI.KLeft, [l]) -> DSL.parens $ DSL.text "left" DSL.<+> pe l - (TI.KRight, [r]) -> DSL.parens $ DSL.text "right" DSL.<+> pe r - (_, _) -> DSL.hsep $ DSL.text (show ident) : map pe args +prettyPrintExample :: (Applicative f) => ExamplePat -> f (Doc ann) +prettyPrintExample e@(ExamplePat TI.DataCon {TI.dcIdent = ident} args) = case (ident, args) of + (TI.KPair, _) -> tupled (traverse prettyPrintExample (resugarPair e)) + (TI.KCons, _) -> list (traverse prettyPrintExample (resugarList e)) + (TI.KLeft, [l]) -> DSL.parens $ DSL.text "left" DSL.<+> prettyPrintExample l + (TI.KRight, [r]) -> DSL.parens $ DSL.text "right" DSL.<+> prettyPrintExample r + (_, _) -> DSL.hsep $ DSL.text (show ident) : map prettyPrintExample args tupled :: (Applicative f) => f [Doc ann] -> f (Doc ann) tupled = fmap PP.tupled @@ -238,72 +238,6 @@ data InhabPat where IPNot :: [TI.DataCon] -> InhabPat deriving (Show, Eq, Ord) -join :: [a] -> [a] -> [a] -> [a] -join j a b = a ++ j ++ b - -joinComma :: [String] -> String -joinComma = foldr1 (join ", ") - -joinSpace :: [String] -> String -joinSpace = foldr1 (join " ") - --- TODO(colin): maybe fully print out tuples even if they have wildcars in the middle? --- e.g. (1,_,_) instead of just (1,_) --- Also, the display for matches against strings is really weird, --- as strings are lists of chars. --- Maybe for strings, we just list the top 3 uncovered patterns --- consiting of only postive information, sorted by length? --- Also, how should we print out sum types? --- We can do right(thing) or (right thing), or (right(thing)) --- Which should we chose? -prettyInhab :: InhabPat -> String -prettyInhab (IPNot []) = "_" -prettyInhab (IPNot nots) = "Not{" ++ joinComma (map dcToString nots) ++ "}" -prettyInhab (IPIs TI.DataCon {TI.dcIdent = TI.KPair, TI.dcTypes = _} [ifst, isnd]) = - "(" ++ prettyInhab ifst ++ ", " ++ prettyInhab isnd ++ ")" -prettyInhab (IPIs TI.DataCon {TI.dcIdent = TI.KCons, TI.dcTypes = _} [ihead, itail]) = - "(" ++ prettyInhab ihead ++ " :: " ++ prettyInhab itail ++ ")" -prettyInhab (IPIs TI.DataCon {TI.dcIdent = TI.KLeft, TI.dcTypes = _} [l]) = - "(left " ++ prettyInhab l ++ ")" -prettyInhab (IPIs TI.DataCon {TI.dcIdent = TI.KRight, TI.dcTypes = _} [r]) = - "(right " ++ prettyInhab r ++ ")" -prettyInhab (IPIs dc []) = dcToString dc -prettyInhab (IPIs dc args) = dcToString dc ++ " " ++ joinSpace (map prettyInhab args) - -data ExamplePat where - ExamplePat :: TI.DataCon -> [ExamplePat] -> ExamplePat - deriving (Show) - -prettyExample :: ExamplePat -> String -prettyExample (ExamplePat TI.DataCon {TI.dcIdent = TI.KPair, TI.dcTypes = _} [ifst, isnd]) = - "(" ++ prettyExample ifst ++ ", " ++ prettyExample isnd ++ ")" -prettyExample (ExamplePat TI.DataCon {TI.dcIdent = TI.KCons, TI.dcTypes = _} [ihead, itail]) = - "(" ++ prettyExample ihead ++ " :: " ++ prettyExample itail ++ ")" -prettyExample (ExamplePat TI.DataCon {TI.dcIdent = TI.KLeft, TI.dcTypes = _} [l]) = - "(left " ++ prettyExample l ++ ")" -prettyExample (ExamplePat TI.DataCon {TI.dcIdent = TI.KRight, TI.dcTypes = _} [r]) = - "(right " ++ prettyExample r ++ ")" -prettyExample (ExamplePat dc []) = dcToString dc -prettyExample (ExamplePat dc args) = dcToString dc ++ " " ++ joinSpace (map prettyExample args) - -dcToString :: TI.DataCon -> String -dcToString TI.DataCon {TI.dcIdent = ident} = case ident of - TI.KBool b -> show b - TI.KChar c -> show c - TI.KNat n -> show n - TI.KInt z -> show z - TI.KNil -> "[]" - TI.KUnit -> "unit" - TI.KUnkown -> "_" - -- TODO(colin): find a way to remove these? These two shouldn't be reachable - -- If we were in an IPIs, we already handled these above - -- If we were in an IPNot, these aren't from opaque types, - -- so they shouldn't appear in a Not{} - TI.KPair -> "," - TI.KCons -> "::" - TI.KLeft -> "left()" - TI.KRight -> "right()" - -- Sanity check: are we giving the dataconstructor the -- correct number of arguments? mkIPMatch :: TI.DataCon -> [InhabPat] -> InhabPat @@ -361,6 +295,10 @@ findRedundant ant args = case ant of 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. From 5d6ffad703cec62ed3f287e34209e99a7eb1d431 Mon Sep 17 00:00:00 2001 From: LeitMoth Date: Thu, 9 Jan 2025 06:34:22 +0000 Subject: [PATCH 23/44] tweak desugarMatch and update comment --- src/Disco/Exhaustiveness.hs | 27 +++++++++++++++------------ 1 file changed, 15 insertions(+), 12 deletions(-) diff --git a/src/Disco/Exhaustiveness.hs b/src/Disco/Exhaustiveness.hs index 93cba434..22945f76 100644 --- a/src/Disco/Exhaustiveness.hs +++ b/src/Disco/Exhaustiveness.hs @@ -109,17 +109,21 @@ desugarTuplePats (pfst : rest) = APTup (Ty.getType pfst Ty.:*: Ty.getType psnd) where psnd = desugarTuplePats rest -{- -TODO(colin): handle remaining patterns - , APNeg --still need to handle rational case - , APFrac --required for rationals? - algebraic (probably will be replaced anyway): - , APAdd - , APMul - , APSub -We treat unhandled patterns as if they are exhaustively matched against -This necessarily results in some false negatives, but no false positives. --} +-- | 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 +-- We treat unhandled patterns as if they are exhaustively matched against +-- This necessarily results in some false negatives, but no false positives. +-- +-- TODO(colin): +-- Without general arithmetic patterns, maybe we should just leave these unhandled? +-- not much else we can do 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 @@ -129,7 +133,6 @@ desugarMatch var pat = case pat of guardsSnd <- desugarMatch varSnd psnd let guardPair = (var, GMatch (TI.pair ta tb) [varFst, varSnd]) return $ [guardPair] ++ guardsFst ++ guardsSnd - (APTup ty [_, _]) -> error $ "Tuple type that wasn't a pair???: " ++ show ty (APTup _ sugary) -> desugarMatch var (desugarTuplePats sugary) (APCons _ subHead subTail) -> do let typeHead = Ty.getType subHead From 89f098789024cc54ffb4130a7022c133a76b8b77 Mon Sep 17 00:00:00 2001 From: LeitMoth Date: Thu, 9 Jan 2025 06:40:46 +0000 Subject: [PATCH 24/44] update comments in typeinfo --- src/Disco/Exhaustiveness/TypeInfo.hs | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/src/Disco/Exhaustiveness/TypeInfo.hs b/src/Disco/Exhaustiveness/TypeInfo.hs index 67fb30cf..e2d34025 100644 --- a/src/Disco/Exhaustiveness/TypeInfo.hs +++ b/src/Disco/Exhaustiveness/TypeInfo.hs @@ -64,8 +64,8 @@ instance Show Ident where KRight -> "right()" -- | 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 +-- '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 @@ -153,8 +153,11 @@ tyDataConsHelper _ = Infinite [unknown] -- I believe this also applies when pattern matching 'Maybe a' types -- We need stand in for an example of a concrete 'a' -- --- I remember the Infinite part making sense at the time --- but I should probably double check that +-- iirc, these are 'Infinite' because the only way to match against +-- them is with a wildcard or variable pattern, and marking them 'Infinite' +-- conveys essentially just that to the LYG checker +-- +-- Maybe this should be in a big doc comment above? newName :: (Member Fresh r) => Sem r (Name ATerm) newName = fresh $ s2n "" From ad5d6a9376cdfaa690aa8695997b07d128dc210a Mon Sep 17 00:00:00 2001 From: LeitMoth Date: Thu, 9 Jan 2025 07:08:03 +0000 Subject: [PATCH 25/44] add more todo comments --- src/Disco/Exhaustiveness.hs | 2 ++ src/Disco/Exhaustiveness/Constraint.hs | 5 ++++- src/Disco/Exhaustiveness/TypeInfo.hs | 13 +++++++++++-- 3 files changed, 17 insertions(+), 3 deletions(-) diff --git a/src/Disco/Exhaustiveness.hs b/src/Disco/Exhaustiveness.hs index 22945f76..e58808d9 100644 --- a/src/Disco/Exhaustiveness.hs +++ b/src/Disco/Exhaustiveness.hs @@ -39,6 +39,8 @@ import Polysemy.Reader import qualified Prettyprinter as PP import Unbound.Generics.LocallyNameless (Name) +-- TODO(colin): should I explain that this comes from the LYG paper +-- in some sort of comment, of leave some sort of link to the publication, etc? 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 diff --git a/src/Disco/Exhaustiveness/Constraint.hs b/src/Disco/Exhaustiveness/Constraint.hs index 37d23c81..4ebc70f5 100644 --- a/src/Disco/Exhaustiveness/Constraint.hs +++ b/src/Disco/Exhaustiveness/Constraint.hs @@ -64,6 +64,8 @@ addConstraintHelper nref@(ctx, cns) cf@(origX, c) = case c of CMatch k args -> do case getConstructorArgs k (onVar origX cns) of -- 10c -- TODO(colin): Still need to add type constraints! + -- ...unless resolveAlias in TypeInfo works all of the time. + -- then we are actually done Just args' -> addConstraints nref @@ -127,8 +129,9 @@ substituteVarIDs y x = map (first subst) -- 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 --- NOTE(colin): we may eventually have type constraints +-- TODO(colin): we may eventually have type constraints -- and we would need to worry pulling them from nref here +-- ...unless resolveAlias works. see above note inhabited :: Members '[Fresh, Reader Ty.TyDefCtx] r => NormRefType -> TI.TypedVar -> Sem r Bool inhabited n var = do tyCtx <- ask @Ty.TyDefCtx diff --git a/src/Disco/Exhaustiveness/TypeInfo.hs b/src/Disco/Exhaustiveness/TypeInfo.hs index e2d34025..7516f770 100644 --- a/src/Disco/Exhaustiveness/TypeInfo.hs +++ b/src/Disco/Exhaustiveness/TypeInfo.hs @@ -69,6 +69,9 @@ instance Show Ident where data Constructors where Finite :: [DataCon] -> Constructors Infinite :: [DataCon] -> Constructors +-- TODO(colin): should I quote 'Infinite' with single quotes in the above doc comment? +-- is there a proper way to reference that that will get +-- picked up and put in the docs in a nice way? unknown :: DataCon unknown = DataCon {dcIdent = KUnkown, dcTypes = []} @@ -110,6 +113,12 @@ tyDataCons ty ctx = tyDataConsHelper $ resolveAlias ty ctx -- If I have, and this is enough, I can remove all mentions -- of type equality constraints in Constraint.hs, -- the lookup here will have handled that behavoir already +-- +-- I was worried about infinite recursion at first, +-- but I think the types that that would happen for +-- are rejected with an error: +-- Error: cyclic type definition for A. +-- So I don't think that is an issue, but I would like confirmation 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 @@ -117,7 +126,7 @@ resolveAlias (Ty.TyUser name args) ctx = case M.lookup name ctx of resolveAlias t _ = t -- TODO(colin): ask yorgey to see if I've handled all the thing --- I need to here. The list of things caught by the wildcard is below +-- I need to here. The list of things caught by the wildcard is in the comment below the function tyDataConsHelper :: Ty.Type -> Constructors tyDataConsHelper (a Ty.:*: b) = Finite [pair a b] tyDataConsHelper (l Ty.:+: r) = Finite [left l, right r] @@ -157,7 +166,7 @@ tyDataConsHelper _ = Infinite [unknown] -- them is with a wildcard or variable pattern, and marking them 'Infinite' -- conveys essentially just that to the LYG checker -- --- Maybe this should be in a big doc comment above? +-- Maybe this should be rewritten in a big doc comment above? newName :: (Member Fresh r) => Sem r (Name ATerm) newName = fresh $ s2n "" From 8737963b834309e2635d78839b5fc38b38664183 Mon Sep 17 00:00:00 2001 From: LeitMoth Date: Thu, 9 Jan 2025 22:30:28 +0000 Subject: [PATCH 26/44] refactor context to set --- src/Disco/Exhaustiveness.hs | 3 ++- src/Disco/Exhaustiveness/Constraint.hs | 5 +++-- 2 files changed, 5 insertions(+), 3 deletions(-) diff --git a/src/Disco/Exhaustiveness.hs b/src/Disco/Exhaustiveness.hs index e58808d9..e8a5b34a 100644 --- a/src/Disco/Exhaustiveness.hs +++ b/src/Disco/Exhaustiveness.hs @@ -38,6 +38,7 @@ import Polysemy.Output import Polysemy.Reader import qualified Prettyprinter as PP import Unbound.Generics.LocallyNameless (Name) +import qualified Data.Set as S -- TODO(colin): should I explain that this comes from the LYG paper -- in some sort of comment, of leave some sort of link to the publication, etc? @@ -47,7 +48,7 @@ checkClauses name types pats = do cl <- zipWithM (desugarClause args) [1 ..] (NonEmpty.toList pats) let gdt = foldr1 Branch cl - let argsNref = (C.Context args, []) + let argsNref = (C.Context (S.fromList args), []) (normalizedNrefs, _) <- ua [argsNref] gdt examples <- findPosExamples normalizedNrefs args diff --git a/src/Disco/Exhaustiveness/Constraint.hs b/src/Disco/Exhaustiveness/Constraint.hs index 4ebc70f5..5687ecf6 100644 --- a/src/Disco/Exhaustiveness/Constraint.hs +++ b/src/Disco/Exhaustiveness/Constraint.hs @@ -12,12 +12,13 @@ import Polysemy import qualified Disco.Types as Ty import Polysemy.Reader import Data.Bifunctor (first) +import qualified Data.Set as S -newtype Context = Context {getCtxVars :: [TI.TypedVar]} +newtype Context = Context {getCtxVars :: S.Set TI.TypedVar} deriving (Show, Eq) addVars :: Context -> [TI.TypedVar] -> Context -addVars (Context ctx) vars = Context (ctx ++ vars) +addVars (Context ctx) vars = Context (foldr S.insert ctx vars) data Constraint where CMatch :: TI.DataCon -> [TI.TypedVar] -> Constraint From 4cc31dee9e400032ec9b097a1166fd08137f2420 Mon Sep 17 00:00:00 2001 From: LeitMoth Date: Thu, 9 Jan 2025 23:14:28 +0000 Subject: [PATCH 27/44] remove redundant Context from Nref --- src/Disco/Exhaustiveness.hs | 27 +++++++++++++------------- src/Disco/Exhaustiveness/Constraint.hs | 27 ++++++++++---------------- 2 files changed, 23 insertions(+), 31 deletions(-) diff --git a/src/Disco/Exhaustiveness.hs b/src/Disco/Exhaustiveness.hs index e8a5b34a..c609f0d7 100644 --- a/src/Disco/Exhaustiveness.hs +++ b/src/Disco/Exhaustiveness.hs @@ -38,7 +38,6 @@ import Polysemy.Output import Polysemy.Reader import qualified Prettyprinter as PP import Unbound.Generics.LocallyNameless (Name) -import qualified Data.Set as S -- TODO(colin): should I explain that this comes from the LYG paper -- in some sort of comment, of leave some sort of link to the publication, etc? @@ -48,7 +47,7 @@ checkClauses name types pats = do cl <- zipWithM (desugarClause args) [1 ..] (NonEmpty.toList pats) let gdt = foldr1 Branch cl - let argsNref = (C.Context (S.fromList args), []) + let argsNref = [] (normalizedNrefs, _) <- ua [argsNref] gdt examples <- findPosExamples normalizedNrefs args @@ -226,18 +225,18 @@ addLitMulti (n : ns) lit = do r <- runMaybeT $ addLiteral n lit case r of Nothing -> addLitMulti ns lit - Just (ctx, cfs) -> do + Just cfs -> do ns' <- addLitMulti ns lit - return $ (ctx, cfs) : ns' + return $ cfs : ns' addLiteral :: (Members '[Fresh, Reader Ty.TyDefCtx] r) => C.NormRefType -> Literal -> MaybeT (Sem r) C.NormRefType -addLiteral (context, constraints) (Literal (x, c)) = case c of +addLiteral constraints (Literal (x, c)) = case c of LitWasOriginally z -> - (context `C.addVars` [x], constraints) `C.addConstraint` (x, C.CWasOriginally z) + constraints `C.addConstraint` (x, C.CWasOriginally z) LitMatch dc args -> - (context `C.addVars` args, constraints) `C.addConstraint` (x, C.CMatch dc args) + constraints `C.addConstraint` (x, C.CMatch dc args) LitNot dc -> - (context, constraints) `C.addConstraint` (x, C.CNot dc) + constraints `C.addConstraint` (x, C.CNot dc) data InhabPat where IPIs :: TI.DataCon -> [InhabPat] -> InhabPat @@ -263,10 +262,10 @@ findAllForNref nref args = do return $ Poss.allCombinations argPats findVarInhabitants :: (Members '[Fresh, Reader Ty.TyDefCtx] r) => TI.TypedVar -> C.NormRefType -> Sem r (Poss.Possibilities InhabPat) -findVarInhabitants var nref@(_, cns) = +findVarInhabitants var cns = case posMatch of Just (k, args) -> do - argPossibilities <- findAllForNref nref args + argPossibilities <- findAllForNref cns args return (mkIPMatch k <$> argPossibilities) Nothing -> case nub negMatches of [] -> Poss.retSingle $ IPNot [] @@ -278,7 +277,7 @@ findVarInhabitants var nref@(_, cns) = do let tryAddDc dc = do vars <- TI.newVars (TI.dcTypes dc) - runMaybeT (nref `C.addConstraint` (var, C.CMatch dc vars)) + runMaybeT (cns `C.addConstraint` (var, C.CMatch dc vars)) -- Try to add a positive constraint for each data constructor -- to the current nref @@ -323,19 +322,19 @@ findAllPosForNref fuel nref args = do return $ Poss.allCombinations argPats findVarPosExamples :: (Members '[Fresh, Reader Ty.TyDefCtx] r) => Int -> TI.TypedVar -> C.NormRefType -> Sem r (Poss.Possibilities ExamplePat) -findVarPosExamples fuel var nref@(_, cns) = +findVarPosExamples fuel var cns = if fuel < 0 then return mempty else case posMatch of Just (k, args) -> do - argPossibilities <- findAllPosForNref (fuel - 1) nref args + 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 (nref `C.addConstraint` (var, C.CMatch dc vars)) + 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, diff --git a/src/Disco/Exhaustiveness/Constraint.hs b/src/Disco/Exhaustiveness/Constraint.hs index 5687ecf6..f99703b5 100644 --- a/src/Disco/Exhaustiveness/Constraint.hs +++ b/src/Disco/Exhaustiveness/Constraint.hs @@ -12,13 +12,6 @@ import Polysemy import qualified Disco.Types as Ty import Polysemy.Reader import Data.Bifunctor (first) -import qualified Data.Set as S - -newtype Context = Context {getCtxVars :: S.Set TI.TypedVar} - deriving (Show, Eq) - -addVars :: Context -> [TI.TypedVar] -> Context -addVars (Context ctx) vars = Context (foldr S.insert ctx vars) data Constraint where CMatch :: TI.DataCon -> [TI.TypedVar] -> Constraint @@ -49,18 +42,18 @@ alistLookup a = map snd . filter ((== a) . fst) onVar :: TI.TypedVar -> [ConstraintFor] -> [Constraint] onVar x cs = alistLookup (lookupVar x cs) cs -type NormRefType = (Context, [ConstraintFor]) +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 nref@(_, cns) (x, c) = do +addConstraint cns (x, c) = do breakIf $ any (conflictsWith c) (onVar x cns) - addConstraintHelper nref (lookupVar x cns, c) + addConstraintHelper cns (lookupVar x cns, c) addConstraintHelper :: Members '[Fresh, Reader Ty.TyDefCtx] r => NormRefType -> ConstraintFor -> MaybeT (Sem r) NormRefType -addConstraintHelper nref@(ctx, cns) cf@(origX, c) = case c of +addConstraintHelper cns cf@(origX, c) = case c of --- Equation (10) CMatch k args -> do case getConstructorArgs k (onVar origX cns) of @@ -69,7 +62,7 @@ addConstraintHelper nref@(ctx, cns) cf@(origX, c) = case c of -- then we are actually done Just args' -> addConstraints - nref + cns (zipWith (\a b -> (a, CWasOriginally b)) args args') Nothing -> return added --- Equation (11) @@ -81,12 +74,12 @@ addConstraintHelper nref@(ctx, cns) cf@(origX, c) = case c of CWasOriginally y -> do let origY = lookupVar y cns if origX == origY - then return nref + then return cns else do let (noX', withX') = partition ((/= origX) . fst) cns - addConstraints (ctx, noX' ++ [cf]) (substituteVarIDs origY origX withX') + addConstraints (noX' ++ [cf]) (substituteVarIDs origY origX withX') where - added = (ctx, cns ++ [cf]) + added = cns ++ [cf] ----- ----- Helper functions for adding constraints: @@ -146,7 +139,7 @@ inhabited n var = do -- 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 (ctx, cns) var k = do +instantiate cns var k = do args <- TI.newVars $ TI.dcTypes k - let attempt = (ctx `addVars` args, cns) `addConstraint` (var, CMatch k args) + let attempt = cns `addConstraint` (var, CMatch k args) isJust <$> runMaybeT attempt From 16f4e33d986d5bc3399b66d07d6fa6244f385b22 Mon Sep 17 00:00:00 2001 From: LeitMoth Date: Thu, 9 Jan 2025 17:16:05 -0600 Subject: [PATCH 28/44] Fix typo in Constraint.hs Co-authored-by: Brent Yorgey --- src/Disco/Exhaustiveness/Constraint.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Disco/Exhaustiveness/Constraint.hs b/src/Disco/Exhaustiveness/Constraint.hs index f99703b5..7019cbdb 100644 --- a/src/Disco/Exhaustiveness/Constraint.hs +++ b/src/Disco/Exhaustiveness/Constraint.hs @@ -119,7 +119,7 @@ substituteVarIDs y x = map (first subst) where subst var = if var == x then y else x --- | Deals with I2 form section 3.4 +-- | 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 From c4c88bcf6994c5c4ca34dc79e7a2c8d4319f5624 Mon Sep 17 00:00:00 2001 From: LeitMoth Date: Thu, 9 Jan 2025 23:42:51 +0000 Subject: [PATCH 29/44] small doc cleanup --- src/Disco/Exhaustiveness/TypeInfo.hs | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/src/Disco/Exhaustiveness/TypeInfo.hs b/src/Disco/Exhaustiveness/TypeInfo.hs index 7516f770..de681b3d 100644 --- a/src/Disco/Exhaustiveness/TypeInfo.hs +++ b/src/Disco/Exhaustiveness/TypeInfo.hs @@ -63,15 +63,12 @@ instance Show Ident where KLeft -> "left()" KRight -> "right()" --- | Finite constructors are used in the LYG checker +-- | '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 --- TODO(colin): should I quote 'Infinite' with single quotes in the above doc comment? --- is there a proper way to reference that that will get --- picked up and put in the docs in a nice way? unknown :: DataCon unknown = DataCon {dcIdent = KUnkown, dcTypes = []} From 7d0716ffd020bac0f46570683e7c9dbe17a0152f Mon Sep 17 00:00:00 2001 From: LeitMoth Date: Thu, 9 Jan 2025 23:50:11 +0000 Subject: [PATCH 30/44] update desugarMatch documentation --- src/Disco/Exhaustiveness.hs | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/Disco/Exhaustiveness.hs b/src/Disco/Exhaustiveness.hs index c609f0d7..259955aa 100644 --- a/src/Disco/Exhaustiveness.hs +++ b/src/Disco/Exhaustiveness.hs @@ -120,12 +120,12 @@ desugarTuplePats (pfst : rest) = APTup (Ty.getType pfst Ty.:*: Ty.getType psnd) -- , 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. --- --- TODO(colin): --- Without general arithmetic patterns, maybe we should just leave these unhandled? --- not much else we can do 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 From ed831fe0cbaba68a8073b28d9f106bb1d0f7450b Mon Sep 17 00:00:00 2001 From: LeitMoth Date: Fri, 10 Jan 2025 01:02:42 +0000 Subject: [PATCH 31/44] simplify possibilities by deriving everything --- src/Disco/Exhaustiveness/Possibilities.hs | 24 +++++------------------ 1 file changed, 5 insertions(+), 19 deletions(-) diff --git a/src/Disco/Exhaustiveness/Possibilities.hs b/src/Disco/Exhaustiveness/Possibilities.hs index f0352da0..4c969137 100644 --- a/src/Disco/Exhaustiveness/Possibilities.hs +++ b/src/Disco/Exhaustiveness/Possibilities.hs @@ -1,18 +1,11 @@ +{-# LANGUAGE GeneralizedNewtypeDeriving #-} + module Disco.Exhaustiveness.Possibilities (Possibilities, retSingle, allCombinations, anyOf, none, getPossibilities) where -import Data.Foldable (Foldable (fold)) +import Data.Foldable (fold) newtype Possibilities a = Possibilities {getPossibilities :: [a]} - deriving (Show, Eq, Ord) - -instance Functor Possibilities where - fmap f (Possibilities a) = Possibilities (f <$> a) - -instance Semigroup (Possibilities a) where - (Possibilities p1) <> (Possibilities p2) = Possibilities $ p1 <> p2 - -instance Monoid (Possibilities a) where - mempty = Possibilities [] + deriving (Show, Eq, Ord, Functor, Semigroup, Monoid, Applicative) anyOf :: [Possibilities a] -> Possibilities a anyOf = fold @@ -54,11 +47,4 @@ retSingle i = return $ Possibilities [i] -- In other words, this lists all elements of the -- cartesian product of multiple sets allCombinations :: [Possibilities a] -> Possibilities [a] -allCombinations = foldr prod nil - where - -- note, nil /= mempty - -- VERY important - nil = Possibilities [[]] - -prod :: Possibilities a -> Possibilities [a] -> Possibilities [a] -prod (Possibilities xs) (Possibilities yss) = Possibilities [x : ys | x <- xs, ys <- yss] +allCombinations = sequenceA From 516cb467faf5f934fdb30f899bd312b78e2cd8dc Mon Sep 17 00:00:00 2001 From: LeitMoth Date: Thu, 16 Jan 2025 07:08:15 +0000 Subject: [PATCH 32/44] add comment and link to LYG paper on checkClauses function --- src/Disco/Exhaustiveness.hs | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/src/Disco/Exhaustiveness.hs b/src/Disco/Exhaustiveness.hs index 259955aa..d0b26eb3 100644 --- a/src/Disco/Exhaustiveness.hs +++ b/src/Disco/Exhaustiveness.hs @@ -39,8 +39,14 @@ import Polysemy.Reader import qualified Prettyprinter as PP import Unbound.Generics.LocallyNameless (Name) --- TODO(colin): should I explain that this comes from the LYG paper --- in some sort of comment, of leave some sort of link to the publication, etc? +-- | 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 From 6d49bbcc2773ed5b87108b25fcf8c070641189e2 Mon Sep 17 00:00:00 2001 From: LeitMoth Date: Thu, 16 Jan 2025 07:12:18 +0000 Subject: [PATCH 33/44] rephrase warning message --- src/Disco/Exhaustiveness.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Disco/Exhaustiveness.hs b/src/Disco/Exhaustiveness.hs index d0b26eb3..2658e7b7 100644 --- a/src/Disco/Exhaustiveness.hs +++ b/src/Disco/Exhaustiveness.hs @@ -69,7 +69,7 @@ checkClauses name types pats = do DSL.vcat $ map (prettyExampleLine . prettyExampleArgs) examples warn $ - DSL.text "Warning: You haven't covered these cases:" + DSL.text "Warning: the function" DSL.<+> DSL.text (show name) DSL.<+> DSL.text "is undefined for some inputs. For example:" DSL.$+$ prettyExamples prettyPrintExample :: (Applicative f) => ExamplePat -> f (Doc ann) From 7a036e61f9dd4326c6101ce2c8847886ffbbb05a Mon Sep 17 00:00:00 2001 From: LeitMoth Date: Thu, 16 Jan 2025 07:19:03 +0000 Subject: [PATCH 34/44] comment on resolveAlias why infinite recursion is impossible --- src/Disco/Exhaustiveness/TypeInfo.hs | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) diff --git a/src/Disco/Exhaustiveness/TypeInfo.hs b/src/Disco/Exhaustiveness/TypeInfo.hs index de681b3d..ed126b17 100644 --- a/src/Disco/Exhaustiveness/TypeInfo.hs +++ b/src/Disco/Exhaustiveness/TypeInfo.hs @@ -111,11 +111,9 @@ tyDataCons ty ctx = tyDataConsHelper $ resolveAlias ty ctx -- of type equality constraints in Constraint.hs, -- the lookup here will have handled that behavoir already -- --- I was worried about infinite recursion at first, --- but I think the types that that would happen for --- are rejected with an error: --- Error: cyclic type definition for A. --- So I don't think that is an issue, but I would like confirmation +-- 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 From d9d316960a308031a2b4854a22ab46728a303b59 Mon Sep 17 00:00:00 2001 From: LeitMoth Date: Thu, 16 Jan 2025 07:23:30 +0000 Subject: [PATCH 35/44] remove unneeded comments about type constraints; I got confirmation resolveAlias is good --- src/Disco/Exhaustiveness/Constraint.hs | 7 +------ 1 file changed, 1 insertion(+), 6 deletions(-) diff --git a/src/Disco/Exhaustiveness/Constraint.hs b/src/Disco/Exhaustiveness/Constraint.hs index 7019cbdb..6ae3be0e 100644 --- a/src/Disco/Exhaustiveness/Constraint.hs +++ b/src/Disco/Exhaustiveness/Constraint.hs @@ -57,9 +57,7 @@ addConstraintHelper cns cf@(origX, c) = case c of --- Equation (10) CMatch k args -> do case getConstructorArgs k (onVar origX cns) of - -- 10c -- TODO(colin): Still need to add type constraints! - -- ...unless resolveAlias in TypeInfo works all of the time. - -- then we are actually done + -- 10c Just args' -> addConstraints cns @@ -123,9 +121,6 @@ substituteVarIDs y x = map (first subst) -- 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 --- TODO(colin): we may eventually have type constraints --- and we would need to worry pulling them from nref here --- ...unless resolveAlias works. see above note inhabited :: Members '[Fresh, Reader Ty.TyDefCtx] r => NormRefType -> TI.TypedVar -> Sem r Bool inhabited n var = do tyCtx <- ask @Ty.TyDefCtx From c22b1d37ca6de90d5038b5886daaef654996e5ec Mon Sep 17 00:00:00 2001 From: LeitMoth Date: Thu, 16 Jan 2025 07:49:52 +0000 Subject: [PATCH 36/44] list all unicode characters as constructors for Char (alphanumeric then noncontrol ascii then rest) --- src/Disco/Exhaustiveness/TypeInfo.hs | 14 +++++++++++--- 1 file changed, 11 insertions(+), 3 deletions(-) diff --git a/src/Disco/Exhaustiveness/TypeInfo.hs b/src/Disco/Exhaustiveness/TypeInfo.hs index ed126b17..66e12df1 100644 --- a/src/Disco/Exhaustiveness/TypeInfo.hs +++ b/src/Disco/Exhaustiveness/TypeInfo.hs @@ -2,6 +2,7 @@ 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) @@ -135,12 +136,19 @@ tyDataConsHelper Ty.TyN = Infinite $ map natural [0, 1 ..] tyDataConsHelper Ty.TyZ = Infinite $ map integer $ 0 : [y | x <- [1 ..], y <- [x, -x]] tyDataConsHelper Ty.TyF = Infinite [] tyDataConsHelper Ty.TyQ = Infinite [] --- TODO(colin): We could do all valid ASCII, but this is most likely good enough --- I think these starting from 'a' is good for students learning the language +-- The Char constructors are all unicode characters, but +-- starting with the alphanumerics and ending with the +-- ascii control characters to give nice warnings. +-- Many thanks to Dr. Yorgey for mentioning [minBound .. maxBound] and \\ tyDataConsHelper Ty.TyC = Infinite $ map char $ - ['a' .. 'z'] ++ ['A' .. 'Z'] ++ ['0' .. '9'] + alphanum ++ rest ++ controlChars + where + allChars = [minBound .. maxBound] + alphanum = ['a' .. 'z'] ++ ['A' .. 'Z'] ++ ['0' .. '9'] + noAlphanum = allChars \\ alphanum + (controlChars, rest) = splitAt 32 noAlphanum tyDataConsHelper _ = Infinite [unknown] -- ^ This includes: -- (_ Ty.:->: _) (Ty.TySet _) (Ty.TyBag _) (Ty.TyVar _) From 02611f66193f1eb4bbe051e490d16d9512901332 Mon Sep 17 00:00:00 2001 From: LeitMoth Date: Sat, 18 Jan 2025 17:37:20 -0600 Subject: [PATCH 37/44] remove outdated example/lists.disco --- example/lists.disco | 12 ------------ 1 file changed, 12 deletions(-) delete mode 100644 example/lists.disco 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,_) ?} From f03bce7ee83f8d2ac248621ea88baecf462fd17b Mon Sep 17 00:00:00 2001 From: LeitMoth Date: Sat, 18 Jan 2025 18:02:18 -0600 Subject: [PATCH 38/44] make chars all unicode but ordered nicely --- src/Disco/Exhaustiveness/TypeInfo.hs | 12 +++++------- 1 file changed, 5 insertions(+), 7 deletions(-) diff --git a/src/Disco/Exhaustiveness/TypeInfo.hs b/src/Disco/Exhaustiveness/TypeInfo.hs index 66e12df1..b7341c46 100644 --- a/src/Disco/Exhaustiveness/TypeInfo.hs +++ b/src/Disco/Exhaustiveness/TypeInfo.hs @@ -137,18 +137,16 @@ tyDataConsHelper Ty.TyZ = Infinite $ map integer $ 0 : [y | x <- [1 ..], y <- [x tyDataConsHelper Ty.TyF = Infinite [] tyDataConsHelper Ty.TyQ = Infinite [] -- The Char constructors are all unicode characters, but --- starting with the alphanumerics and ending with the --- ascii control characters to give nice warnings. +-- 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 ++ rest ++ controlChars + alphanum ++ (allUnicodeNicelyOrdered \\ alphanum) where - allChars = [minBound .. maxBound] + allUnicodeNicelyOrdered = [(toEnum 32) .. (toEnum 126)] ++ [(toEnum 161) .. maxBound] ++ [minBound .. (toEnum 31)] ++ [(toEnum 127) .. (toEnum 160)] alphanum = ['a' .. 'z'] ++ ['A' .. 'Z'] ++ ['0' .. '9'] - noAlphanum = allChars \\ alphanum - (controlChars, rest) = splitAt 32 noAlphanum tyDataConsHelper _ = Infinite [unknown] -- ^ This includes: -- (_ Ty.:->: _) (Ty.TySet _) (Ty.TyBag _) (Ty.TyVar _) @@ -156,7 +154,7 @@ tyDataConsHelper _ = Infinite [unknown] -- TODO(colin): confim below: -- I think all of these are impossible to pattern match against -- with anything other than a wildcard. --- So they should be always fully covered. +-- So they should be always fully covered. -- But if they are in a pair, like a Set(Int)*Int, -- We still need to generate 3 examples of the pair if that Int -- part isn't covered. From b65c89f53524719ad97a46cf70b00d578b2c60e2 Mon Sep 17 00:00:00 2001 From: LeitMoth Date: Sat, 18 Jan 2025 18:21:12 -0600 Subject: [PATCH 39/44] consolidate doc comment for tyDataConsHelper --- src/Disco/Exhaustiveness/TypeInfo.hs | 50 ++++++++++++++++------------ 1 file changed, 28 insertions(+), 22 deletions(-) diff --git a/src/Disco/Exhaustiveness/TypeInfo.hs b/src/Disco/Exhaustiveness/TypeInfo.hs index b7341c46..701d716d 100644 --- a/src/Disco/Exhaustiveness/TypeInfo.hs +++ b/src/Disco/Exhaustiveness/TypeInfo.hs @@ -121,8 +121,34 @@ resolveAlias (Ty.TyUser name args) ctx = case M.lookup name ctx of Just (Ty.TyDefBody _argNames typeCon) -> resolveAlias (typeCon args) ctx resolveAlias t _ = t --- TODO(colin): ask yorgey to see if I've handled all the thing --- I need to here. The list of things caught by the wildcard is in the comment below the function +-- | 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] @@ -148,26 +174,6 @@ tyDataConsHelper Ty.TyC = 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] --- ^ This includes: --- (_ Ty.:->: _) (Ty.TySet _) (Ty.TyBag _) (Ty.TyVar _) --- (Ty.TySkolem _) (Ty.TyProp) (Ty.TyMap _ _) (Ty.TyGraph _) --- TODO(colin): confim below: --- I think all of these are impossible to pattern match against --- with anything other than a wildcard. --- So they should be always fully covered. --- But if they are in a pair, like a 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)? --- For now I'm calling that unknown, and printing an underscore --- I believe this also applies when pattern matching 'Maybe a' types --- We need stand in for an example of a concrete 'a' --- --- iirc, these are 'Infinite' because the only way to match against --- them is with a wildcard or variable pattern, and marking them 'Infinite' --- conveys essentially just that to the LYG checker --- --- Maybe this should be rewritten in a big doc comment above? newName :: (Member Fresh r) => Sem r (Name ATerm) newName = fresh $ s2n "" From c6e2d65849ae50ebdc15b5f3301114109c3ff5b8 Mon Sep 17 00:00:00 2001 From: LeitMoth Date: Sat, 18 Jan 2025 18:22:45 -0600 Subject: [PATCH 40/44] fix typo in KUnknown --- src/Disco/Exhaustiveness/TypeInfo.hs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Disco/Exhaustiveness/TypeInfo.hs b/src/Disco/Exhaustiveness/TypeInfo.hs index 701d716d..59704199 100644 --- a/src/Disco/Exhaustiveness/TypeInfo.hs +++ b/src/Disco/Exhaustiveness/TypeInfo.hs @@ -43,7 +43,7 @@ data Ident where KChar :: Char -> Ident KLeft :: Ident KRight :: Ident - KUnkown :: Ident + KUnknown :: Ident deriving (Eq, Ord) instance Show Ident where @@ -57,7 +57,7 @@ instance Show Ident where else show z KNil -> "[]" KUnit -> "unit" - KUnkown -> "_" + KUnknown -> "_" -- These should never actually be printed in warnings KPair -> "," KCons -> "::" @@ -72,7 +72,7 @@ data Constructors where Infinite :: [DataCon] -> Constructors unknown :: DataCon -unknown = DataCon {dcIdent = KUnkown, dcTypes = []} +unknown = DataCon {dcIdent = KUnknown, dcTypes = []} unit :: DataCon unit = DataCon {dcIdent = KUnit, dcTypes = []} From d1fb240ea50df2b90c0e159b8e7256f0479c6eb8 Mon Sep 17 00:00:00 2001 From: LeitMoth Date: Sat, 18 Jan 2025 18:42:34 -0600 Subject: [PATCH 41/44] add Haddock module comments --- src/Disco/Exhaustiveness.hs | 10 ++++++++++ src/Disco/Exhaustiveness/Constraint.hs | 11 +++++++++++ src/Disco/Exhaustiveness/Possibilities.hs | 9 +++++++++ src/Disco/Exhaustiveness/TypeInfo.hs | 10 ++++++++++ 4 files changed, 40 insertions(+) diff --git a/src/Disco/Exhaustiveness.hs b/src/Disco/Exhaustiveness.hs index 2658e7b7..ad8d01a4 100644 --- a/src/Disco/Exhaustiveness.hs +++ b/src/Disco/Exhaustiveness.hs @@ -1,5 +1,15 @@ {-# 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, zipWithM, unless) diff --git a/src/Disco/Exhaustiveness/Constraint.hs b/src/Disco/Exhaustiveness/Constraint.hs index 6ae3be0e..9c4ccab4 100644 --- a/src/Disco/Exhaustiveness/Constraint.hs +++ b/src/Disco/Exhaustiveness/Constraint.hs @@ -1,3 +1,14 @@ +-- | +-- 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) diff --git a/src/Disco/Exhaustiveness/Possibilities.hs b/src/Disco/Exhaustiveness/Possibilities.hs index 4c969137..439174d2 100644 --- a/src/Disco/Exhaustiveness/Possibilities.hs +++ b/src/Disco/Exhaustiveness/Possibilities.hs @@ -1,5 +1,14 @@ {-# 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) diff --git a/src/Disco/Exhaustiveness/TypeInfo.hs b/src/Disco/Exhaustiveness/TypeInfo.hs index 59704199..2e449cf1 100644 --- a/src/Disco/Exhaustiveness/TypeInfo.hs +++ b/src/Disco/Exhaustiveness/TypeInfo.hs @@ -1,3 +1,13 @@ +-- | +-- 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) From 653737e53bf5fc835f872d77e3768b7435a522e7 Mon Sep 17 00:00:00 2001 From: LeitMoth Date: Sat, 18 Jan 2025 18:43:57 -0600 Subject: [PATCH 42/44] remove old typeinfo comment --- src/Disco/Exhaustiveness/TypeInfo.hs | 5 ----- 1 file changed, 5 deletions(-) diff --git a/src/Disco/Exhaustiveness/TypeInfo.hs b/src/Disco/Exhaustiveness/TypeInfo.hs index 2e449cf1..65dcaf68 100644 --- a/src/Disco/Exhaustiveness/TypeInfo.hs +++ b/src/Disco/Exhaustiveness/TypeInfo.hs @@ -117,11 +117,6 @@ right tr = DataCon {dcIdent = KRight, dcTypes = [tr]} tyDataCons :: Ty.Type -> Ty.TyDefCtx -> Constructors tyDataCons ty ctx = tyDataConsHelper $ resolveAlias ty ctx --- TODO(colin): ask yorgey, make sure I've done this correctly --- If I have, and this is enough, I can remove all mentions --- of type equality constraints in Constraint.hs, --- the lookup here will have handled that behavoir already --- -- 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) From 565da272fb11914094230fc0058bca6358f603bd Mon Sep 17 00:00:00 2001 From: LeitMoth Date: Mon, 20 Jan 2025 17:12:16 -0600 Subject: [PATCH 43/44] convert back to patterns and use disco pretty printing --- src/Disco/AST/Surface.hs | 3 ++ src/Disco/Exhaustiveness.hs | 80 +++++++++++++++++++++------- src/Disco/Exhaustiveness/TypeInfo.hs | 24 ++------- 3 files changed, 68 insertions(+), 39 deletions(-) diff --git a/src/Disco/AST/Surface.hs b/src/Disco/AST/Surface.hs index 3ea57456..3ac0b09a 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/Exhaustiveness.hs b/src/Disco/Exhaustiveness.hs index ad8d01a4..b83a361c 100644 --- a/src/Disco/Exhaustiveness.hs +++ b/src/Disco/Exhaustiveness.hs @@ -12,13 +12,27 @@ -- then pretty prints the results of running it. module Disco.Exhaustiveness where -import Control.Monad (forM, zipWithM, unless) +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, @@ -36,17 +50,18 @@ import Disco.AST.Typed 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) +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 qualified Prettyprinter as PP import Unbound.Generics.LocallyNameless (Name) -- | This exhaustiveness checking algorithm is based on the paper @@ -70,31 +85,47 @@ checkClauses name types pats = do unless (null examples) $ do let prettyExampleArgs exArgs = - DSL.hsep $ map prettyPrintExample exArgs + DSL.hcat $ map prettyPrintExample exArgs let prettyExampleLine prettyArgs = - DSL.text (show name) DSL.<+> prettyArgs DSL.<+> DSL.text "= ..." + 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.text "Warning: the function" + DSL.<+> DSL.text (show name) + DSL.<+> DSL.text "is undefined for some inputs. For example:" DSL.$+$ prettyExamples -prettyPrintExample :: (Applicative f) => ExamplePat -> f (Doc ann) -prettyPrintExample e@(ExamplePat TI.DataCon {TI.dcIdent = ident} args) = case (ident, args) of - (TI.KPair, _) -> tupled (traverse prettyPrintExample (resugarPair e)) - (TI.KCons, _) -> list (traverse prettyPrintExample (resugarList e)) - (TI.KLeft, [l]) -> DSL.parens $ DSL.text "left" DSL.<+> prettyPrintExample l - (TI.KRight, [r]) -> DSL.parens $ DSL.text "right" DSL.<+> prettyPrintExample r - (_, _) -> DSL.hsep $ DSL.text (show ident) : map prettyPrintExample args - -tupled :: (Applicative f) => f [Doc ann] -> f (Doc ann) -tupled = fmap PP.tupled - -list :: (Applicative f) => f [Doc ann] -> f (Doc ann) -list = fmap PP.list +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 @@ -106,6 +137,15 @@ resugarList (ExamplePat TI.DataCon {TI.dcIdent = ident} args) = case (ident, arg (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 @@ -136,7 +176,7 @@ desugarTuplePats (pfst : rest) = APTup (Ty.getType pfst Ty.:*: Ty.getType psnd) -- , APAdd -- , APMul -- , APSub --- These (or some updated version of them) may be handled eventually, +-- 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 diff --git a/src/Disco/Exhaustiveness/TypeInfo.hs b/src/Disco/Exhaustiveness/TypeInfo.hs index 65dcaf68..b4f30a19 100644 --- a/src/Disco/Exhaustiveness/TypeInfo.hs +++ b/src/Disco/Exhaustiveness/TypeInfo.hs @@ -42,6 +42,10 @@ data DataCon = DataCon 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 @@ -54,25 +58,7 @@ data Ident where KLeft :: Ident KRight :: Ident KUnknown :: Ident - deriving (Eq, Ord) - -instance Show Ident where - show i = case i of - KBool b -> show b - KChar c -> show c - KNat n -> show n - KInt z -> - if z < 0 - then "(" ++ show z ++ ")" - else show z - KNil -> "[]" - KUnit -> "unit" - KUnknown -> "_" - -- These should never actually be printed in warnings - KPair -> "," - KCons -> "::" - KLeft -> "left()" - KRight -> "right()" + deriving (Show, Eq, Ord) -- | 'Finite' constructors are used in the LYG checker -- 'Infinite' constructors are used when reporting From 996d74bb9c7c2352757f55cf3f2c0f0b472ec4e0 Mon Sep 17 00:00:00 2001 From: "github-actions[bot]" <41898282+github-actions[bot]@users.noreply.github.com> Date: Tue, 21 Jan 2025 06:42:03 -0600 Subject: [PATCH 44/44] Restyled by fourmolu (#435) Co-authored-by: Restyled.io --- src/Disco/Eval.hs | 8 +-- src/Disco/Exhaustiveness.hs | 88 +++++++++++++------------- src/Disco/Exhaustiveness/Constraint.hs | 18 +++--- src/Disco/Exhaustiveness/TypeInfo.hs | 10 +-- 4 files changed, 62 insertions(+), 62 deletions(-) diff --git a/src/Disco/Eval.hs b/src/Disco/Eval.hs index 758041be..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 @@ -95,8 +97,6 @@ import Disco.Typecheck (checkModule) import Disco.Typecheck.Util import Disco.Types import Disco.Value -import qualified Data.List.NonEmpty as NonEmpty -import Disco.Exhaustiveness (checkClauses) ------------------------------------------------------------ -- Configuation options @@ -387,8 +387,8 @@ loadParsedDiscoModule' quiet mode resolver inProcess name cm@(Module _ mns _ _ _ 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) + 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 diff --git a/src/Disco/Exhaustiveness.hs b/src/Disco/Exhaustiveness.hs index b83a361c..41305cd8 100644 --- a/src/Disco/Exhaustiveness.hs +++ b/src/Disco/Exhaustiveness.hs @@ -19,36 +19,36 @@ 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.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 @@ -164,8 +164,8 @@ 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 + where + psnd = desugarTuplePats rest -- | Convert a Disco APattern into a list of Guards which cover that pattern -- @@ -344,10 +344,10 @@ findVarInhabitants var cns = 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 + 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 @@ -398,17 +398,17 @@ findVarPosExamples fuel var cns = 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 + 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' + where + dcs = case TI.tyDataCons ty ctx of + TI.Finite dcs' -> dcs' + TI.Infinite dcs' -> dcs' mkExampleMatch :: TI.DataCon -> [ExamplePat] -> ExamplePat mkExampleMatch k pats = diff --git a/src/Disco/Exhaustiveness/Constraint.hs b/src/Disco/Exhaustiveness/Constraint.hs index 9c4ccab4..59afb7c6 100644 --- a/src/Disco/Exhaustiveness/Constraint.hs +++ b/src/Disco/Exhaustiveness/Constraint.hs @@ -15,14 +15,14 @@ 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 Polysemy import qualified Disco.Types as Ty +import Polysemy import Polysemy.Reader -import Data.Bifunctor (first) data Constraint where CMatch :: TI.DataCon -> [TI.TypedVar] -> Constraint @@ -43,9 +43,9 @@ type ConstraintFor = (TI.TypedVar, Constraint) -- 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 + 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) @@ -87,8 +87,8 @@ addConstraintHelper cns cf@(origX, c) = case c of else do let (noX', withX') = partition ((/= origX) . fst) cns addConstraints (noX' ++ [cf]) (substituteVarIDs origY origX withX') - where - added = cns ++ [cf] + where + added = cns ++ [cf] ----- ----- Helper functions for adding constraints: @@ -125,8 +125,8 @@ getConstructorArgs k cfs = -- 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 + 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 diff --git a/src/Disco/Exhaustiveness/TypeInfo.hs b/src/Disco/Exhaustiveness/TypeInfo.hs index b4f30a19..14edd7e7 100644 --- a/src/Disco/Exhaustiveness/TypeInfo.hs +++ b/src/Disco/Exhaustiveness/TypeInfo.hs @@ -30,8 +30,8 @@ getType :: TypedVar -> Ty.Type getType (TypedVar (_, t)) = t data DataCon = DataCon - { dcIdent :: Ident, - dcTypes :: [Ty.Type] + { dcIdent :: Ident + , dcTypes :: [Ty.Type] } deriving (Ord, Show) @@ -161,9 +161,9 @@ 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'] + 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)