on 34ba6fe help sign in
elk/src/CheckMatch.hs
158 lines 6.6 kB history raw
1{-# LANGUAGE NamedFieldPuns #-}
2module CheckMatch
3 ( MatchResult (..)
4 , ErrorType (..)
5 , checkModule
6 ) where
8import Control.Applicative ((<$>))
9import qualified AST.Expression.General as General
10import qualified AST.Expression.Canonical as Canonical
11import AST.Module
12import qualified AST.Pattern as Pattern
13import AST.Pattern (CanonicalPattern)
14import qualified AST.Annotation as Annotation
15import qualified Data.Map as Map
16import qualified AST.Variable as Var
17import qualified AST.Literal as Literal
18import Data.Maybe (mapMaybe)
19import Control.Monad (forM)
20import qualified Data.Set as Set
22data MatchResult
23 = Redundant CanonicalPattern
24 | Inexhaustive CanonicalPat
25 | TypeNotFound
26 | Ok
28data 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)
40type CanonicalPat = Pat Var.Canonical
42fromPattern :: CanonicalPattern -> CanonicalPat
43fromPattern 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
51data ErrorType = ConstructorNotFound Var.Canonical
53checkModule :: [CanonicalAdt] -> Module exports CanonicalBody -> [(Either ErrorType MatchResult, Annotation.Region)]
54checkModule (Module {body, datatypes}) = checkBody body where
55 checkBody :: CanonicalBody -> [(Either ErrorType MatchResult, Annotation.Region)]
56 checkBody (CanonicalBody {program}) = checkExpr program
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
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
71 General.Case e branches ->
72 (checkMatch ps, r) : checkExpr e ++ concatMap (checkExpr . snd) branches
73 where ps = map fst branches
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 _ -> []
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 datatypes
91 ctorToAdtExn :: Var.Canonical -> Either ErrorType CanonicalAdt
92 ctorToAdtExn c = case ctorToAdt c of
93 Nothing -> Left (ConstructorNotFound c)
94 Just adt -> Right adt
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
111 argComplement <- fmap concat . forM (zip [0..] ps) $ \(i, argP) ->
112 map (\argP' -> Data ctor (sandwich argP' i)) <$> (complement argP)
114 return (otherCtorPatterns ++ argComplement)
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))
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
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))
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
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