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