@@ -1,9 +1,9 @@
11{-# LANGUAGE NamedFieldPuns #-}
22module CheckMatch
3− ( MatchResult (..)
4− , ErrorType (..)
5− , checkModule
6− ) where
3+ ( MatchResult (..)
4+ , ErrorType (..)
5+ , checkModule
6+ ) where
77
88import Control.Applicative ((<$>))
99import qualified AST.Expression.General as General
@@ -20,139 +20,139 @@ import Control.Monad (forM)
2020import qualified Data.Set as Set
2121
2222data MatchResult
23− = Redundant CanonicalPattern
24− | Inexhaustive CanonicalPat
25− | TypeNotFound
26− | Ok
23+ = Redundant CanonicalPattern
24+ | Inexhaustive CanonicalPat
25+ | TypeNotFound
26+ | Ok
2727
2828data Pat var
29− = Data var [Pat var]
30− | Record [String]
31− | Alias String (Pat var)
32− | Var String
33− | Anything
34− | Literal Literal.Literal
35− -- It's a shame that I had to replicate the entire pattern type, but it's
36− -- essential to have this constructor.
37− | AnythingBut (Set.Set Literal.Literal)
38− deriving (Show, Eq, Ord)
29+ = Data var [Pat var]
30+ | Record [String]
31+ | Alias String (Pat var)
32+ | Var String
33+ | Anything
34+ | Literal Literal.Literal
35+ -- It's a shame that I had to replicate the entire pattern type, but it's
36+ -- essential to have this constructor.
37+ | AnythingBut (Set.Set Literal.Literal)
38+ deriving (Show, Eq, Ord)
3939
4040type CanonicalPat = Pat Var.Canonical
4141
4242fromPattern :: CanonicalPattern -> CanonicalPat
4343fromPattern p = case p of
44− Pattern.Data ctor ps -> Data ctor (map fromPattern ps)
45− Pattern.Record fs -> Record fs
46− Pattern.Alias s p -> Alias s (fromPattern p)
47− Pattern.Var s -> Var s
48− Pattern.Anything -> Anything
49− Pattern.Literal l -> Literal l
44+ Pattern.Data ctor ps -> Data ctor (map fromPattern ps)
45+ Pattern.Record fs -> Record fs
46+ Pattern.Alias s p -> Alias s (fromPattern p)
47+ Pattern.Var s -> Var s
48+ Pattern.Anything -> Anything
49+ Pattern.Literal l -> Literal l
5050
5151data ErrorType = ConstructorNotFound Var.Canonical
5252
5353checkModule :: [CanonicalAdt] -> Module exports CanonicalBody -> [(Either ErrorType MatchResult, Annotation.Region)]
5454checkModule adts (Module {body}) = checkBody body where
55− checkBody :: CanonicalBody -> [(Either ErrorType MatchResult, Annotation.Region)]
56− checkBody (CanonicalBody {program}) = checkExpr program
57−
58− checkExpr :: Canonical.Expr -> [(Either ErrorType MatchResult, Annotation.Region)]
59− checkExpr (Annotation.A r e) = case e of
60− General.ExplicitList es -> concatMap checkExpr es
61− General.Binop _ e e' -> checkExpr e ++ checkExpr e'
62− General.Lambda p e -> (checkMatch [p], r) : checkExpr e
63− General.App e e' -> checkExpr e ++ checkExpr e'
64− General.MultiIf branches -> concatMap (\(b,e) -> checkExpr b ++ checkExpr e) branches
65−
66− General.Let defs e -> ps ++ rhssResults ++ checkExpr e
67− where
68− ps = map (\(Canonical.Definition p _ _) -> (checkMatch [p], r)) defs
69− rhssResults = concatMap (\(Canonical.Definition _ e _) -> checkExpr e) defs
70−
71− General.Case e branches ->
72− (checkMatch ps, r) : checkExpr e ++ concatMap (checkExpr . snd) branches
73− where ps = map fst branches
74−
75− General.Data _ctor es -> concatMap checkExpr es
76− General.Access e _f -> checkExpr e
77− General.Remove e _f -> checkExpr e
78− General.Insert e _f e' -> checkExpr e ++ checkExpr e'
79− General.Modify e _ -> checkExpr e
80− General.Record fields -> concatMap (checkExpr . snd) fields
81− General.Port _pi -> []
82− _ -> []
83−
84− ctorToAdt :: Var.Canonical -> Maybe CanonicalAdt
85− ctorToAdt = \k -> Map.lookup k m where
86− m =
87− Map.fromList $ concatMap (\adt@(_adtName, (_tyVars, ctors)) ->
88− map (\(ctor,_args) -> (ctor, adt)) ctors)
89− adts
90−
91− ctorToAdtExn :: Var.Canonical -> Either ErrorType CanonicalAdt
92− ctorToAdtExn c = case ctorToAdt c of
93− Nothing -> Left (ConstructorNotFound c)
94− Just adt -> Right adt
95−
96− complement :: CanonicalPat -> Either ErrorType [CanonicalPat]
97− complement p = case p of
98− Data ctor ps -> do
99− (_adtName, (_tyVars, ctors)) <- ctorToAdtExn ctor
100− -- A pattern is in the complement of this one if it uses one of the
101− -- other constructors of this type...
102− let otherCtorPatterns =
103− map (\(ctor',args) ->
104− Data ctor' (replicate (length args) Anything))
105− (filter (\(ctor', _) -> ctor' /= ctor) ctors)
106− -- or if it uses this constructor and one of its argument patterns is
107− -- in the complement of an argument pattern here.
108− numArgs = length ps
109− sandwich pat i = replicate i Anything ++ pat : replicate (numArgs - i - 1) Anything
110−
111− argComplement <- fmap concat . forM (zip [0..] ps) $ \(i, argP) ->
112− map (\argP' -> Data ctor (sandwich argP' i)) <$> (complement argP)
113−
114− return (otherCtorPatterns ++ argComplement)
115−
116− Record _fs -> return []
117− Alias _s p -> complement p
118− Var _s -> return []
119− Anything -> return []
120− Literal l -> return [AnythingBut (Set.singleton l)]
121− AnythingBut ls -> return (map Literal (Set.toList ls))
122−
123− intersection :: CanonicalPat -> CanonicalPat -> Maybe CanonicalPat
124− intersection p1 p2 = case (p1, p2) of
125− (Alias _ p1', _) -> intersection p1' p2
126− (_, Alias _ p2') -> intersection p1 p2'
127− (Anything, _) -> Just p2
128− (Var _, _) -> Just p2
129− (_, Anything) -> Just p1
130− (_, Var _) -> Just p1
131−
132− (Data ctor1 args1, Data ctor2 args2) ->
133− if ctor1 /= ctor2
134− then Nothing
135− -- TODO: Assumes that args must be the same length. I think that's ok.
136− else fmap (Data ctor1) (sequence (zipWith intersection args1 args2))
137−
138− -- TODO Assuming the fields are identical.
139− (Record _fs, Record _) -> Just p1
140− (Literal l1, Literal l2) -> if l1 == l2 then Just p1 else Nothing
141− (AnythingBut ls, Literal l) -> if l `Set.member` ls then Nothing else Just p2
142− (Literal l, AnythingBut ls) -> if l `Set.member` ls then Nothing else Just p1
143− (AnythingBut ls1, AnythingBut ls2) -> Just (AnythingBut (Set.union ls1 ls2))
144− _ -> Nothing
145−
146− checkMatch :: [CanonicalPattern] -> Either ErrorType MatchResult
147− checkMatch = go [Anything] where
148− go :: [CanonicalPat] -> [CanonicalPattern] -> Either ErrorType MatchResult
149− go [] [] = return Ok
150− go (q:_) [] = return (Inexhaustive q)
151− go unhandled (p:ps) =
152− let pp = fromPattern p in
153− if all (\q -> intersection q pp == Nothing) unhandled
154− then return (Redundant p)
155− else do
156− pComp <- complement pp
157− go (concatMap (\q -> mapMaybe (intersection q) pComp) unhandled) ps
55+ checkBody :: CanonicalBody -> [(Either ErrorType MatchResult, Annotation.Region)]
56+ checkBody (CanonicalBody {program}) = checkExpr program
57+
58+ checkExpr :: Canonical.Expr -> [(Either ErrorType MatchResult, Annotation.Region)]
59+ checkExpr (Annotation.A r e) = case e of
60+ General.ExplicitList es -> concatMap checkExpr es
61+ General.Binop _ e e' -> checkExpr e ++ checkExpr e'
62+ General.Lambda p e -> (checkMatch [p], r) : checkExpr e
63+ General.App e e' -> checkExpr e ++ checkExpr e'
64+ General.MultiIf branches -> concatMap (\(b,e) -> checkExpr b ++ checkExpr e) branches
65+
66+ General.Let defs e -> ps ++ rhssResults ++ checkExpr e
67+ where
68+ ps = map (\(Canonical.Definition p _ _) -> (checkMatch [p], r)) defs
69+ rhssResults = concatMap (\(Canonical.Definition _ e _) -> checkExpr e) defs
70+
71+ General.Case e branches ->
72+ (checkMatch ps, r) : checkExpr e ++ concatMap (checkExpr . snd) branches
73+ where ps = map fst branches
74+
75+ General.Data _ctor es -> concatMap checkExpr es
76+ General.Access e _f -> checkExpr e
77+ General.Remove e _f -> checkExpr e
78+ General.Insert e _f e' -> checkExpr e ++ checkExpr e'
79+ General.Modify e _ -> checkExpr e
80+ General.Record fields -> concatMap (checkExpr . snd) fields
81+ General.Port _pi -> []
82+ _ -> []
83+
84+ ctorToAdt :: Var.Canonical -> Maybe CanonicalAdt
85+ ctorToAdt = \k -> Map.lookup k m where
86+ m =
87+ Map.fromList $ concatMap (\adt@(_adtName, (_tyVars, ctors)) ->
88+ map (\(ctor,_args) -> (ctor, adt)) ctors)
89+ adts
90+
91+ ctorToAdtExn :: Var.Canonical -> Either ErrorType CanonicalAdt
92+ ctorToAdtExn c = case ctorToAdt c of
93+ Nothing -> Left (ConstructorNotFound c)
94+ Just adt -> Right adt
95+
96+ complement :: CanonicalPat -> Either ErrorType [CanonicalPat]
97+ complement p = case p of
98+ Data ctor ps -> do
99+ (_adtName, (_tyVars, ctors)) <- ctorToAdtExn ctor
100+ -- A pattern is in the complement of this one if it uses one of the
101+ -- other constructors of this type...
102+ let otherCtorPatterns =
103+ map (\(ctor',args) ->
104+ Data ctor' (replicate (length args) Anything))
105+ (filter (\(ctor', _) -> ctor' /= ctor) ctors)
106+ -- or if it uses this constructor and one of its argument patterns is
107+ -- in the complement of an argument pattern here.
108+ numArgs = length ps
109+ sandwich pat i = replicate i Anything ++ pat : replicate (numArgs - i - 1) Anything
110+
111+ argComplement <- fmap concat . forM (zip [0..] ps) $ \(i, argP) ->
112+ map (\argP' -> Data ctor (sandwich argP' i)) <$> (complement argP)
113+
114+ return (otherCtorPatterns ++ argComplement)
115+
116+ Record _fs -> return []
117+ Alias _s p -> complement p
118+ Var _s -> return []
119+ Anything -> return []
120+ Literal l -> return [AnythingBut (Set.singleton l)]
121+ AnythingBut ls -> return (map Literal (Set.toList ls))
122+
123+ intersection :: CanonicalPat -> CanonicalPat -> Maybe CanonicalPat
124+ intersection p1 p2 = case (p1, p2) of
125+ (Alias _ p1', _) -> intersection p1' p2
126+ (_, Alias _ p2') -> intersection p1 p2'
127+ (Anything, _) -> Just p2
128+ (Var _, _) -> Just p2
129+ (_, Anything) -> Just p1
130+ (_, Var _) -> Just p1
131+
132+ (Data ctor1 args1, Data ctor2 args2) ->
133+ if ctor1 /= ctor2
134+ then Nothing
135+ -- TODO: Assumes that args must be the same length. I think that's ok.
136+ else fmap (Data ctor1) (sequence (zipWith intersection args1 args2))
137+
138+ -- TODO Assuming the fields are identical.
139+ (Record _fs, Record _) -> Just p1
140+ (Literal l1, Literal l2) -> if l1 == l2 then Just p1 else Nothing
141+ (AnythingBut ls, Literal l) -> if l `Set.member` ls then Nothing else Just p2
142+ (Literal l, AnythingBut ls) -> if l `Set.member` ls then Nothing else Just p1
143+ (AnythingBut ls1, AnythingBut ls2) -> Just (AnythingBut (Set.union ls1 ls2))
144+ _ -> Nothing
145+
146+ checkMatch :: [CanonicalPattern] -> Either ErrorType MatchResult
147+ checkMatch = go [Anything] where
148+ go :: [CanonicalPat] -> [CanonicalPattern] -> Either ErrorType MatchResult
149+ go [] [] = return Ok
150+ go (q:_) [] = return (Inexhaustive q)
151+ go unhandled (p:ps) =
152+ let pp = fromPattern p in
153+ if all (\q -> intersection q pp == Nothing) unhandled
154+ then return (Redundant p)
155+ else do
156+ pComp <- complement pp
157+ go (concatMap (\q -> mapMaybe (intersection q) pComp) unhandled) ps
158158