Skip to content

Commit

Permalink
lists & strings work now! Added comments about remaining work
Browse files Browse the repository at this point in the history
LeitMoth committed Jul 20, 2024
1 parent 7c65f3e commit 4bb13fa
Showing 3 changed files with 117 additions and 107 deletions.
2 changes: 1 addition & 1 deletion src/Disco/Eval.hs
Original file line number Diff line number Diff line change
@@ -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
122 changes: 74 additions & 48 deletions src/Disco/Exhaustiveness.hs
Original file line number Diff line number Diff line change
@@ -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?
100 changes: 42 additions & 58 deletions src/Disco/Exhaustiveness/TypeInfo.hs
Original file line number Diff line number Diff line change
@@ -7,29 +7,20 @@ 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
-- 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 -> 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,64 +43,58 @@ 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)

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

0 comments on commit 4bb13fa

Please sign in to comment.