git.iko.soy/Idris-dev
on master help sign in
Unreachable case warning
6807cf4Edwin Brady
Makefile+1−1
compare with master
unifiedsplit
@@ -16,7 +16,7 @@ test : .PHONY
16
16
17relib: .PHONY
17relib: .PHONY
18 make -C lib clean
18 make -C lib clean
19− make -C lib BINDIR=../dist/build/idris
19+ make -C lib IDRIS=../dist/build/idris/idris
20
20
21linecount : .PHONY
21linecount : .PHONY
22 wc -l src/Idris/*.hs src/Core/*.hs
22 wc -l src/Idris/*.hs src/Core/*.hs
src/Core/CaseTree.hs+16−12
@@ -26,8 +26,8 @@ deriving instance Binary CaseAlt
26!-}
26!-}
27
27
28type CaseTree = SC
28type CaseTree = SC
29−type Clause = ([Pat], Term)
29+type Clause = ([Pat], (Term, Term))
30−type CS = Int
30+type CS = ([Term], Int)
31
31
32-- simple terms can be inlined trivially - good for primitives in particular
32-- simple terms can be inlined trivially - good for primitives in particular
33small :: SC -> Bool
33small :: SC -> Bool
@@ -36,13 +36,13 @@ small _ = False
36
36
37simpleCase :: Bool -> Bool -> [(Term, Term)] -> CaseDef
37simpleCase :: Bool -> Bool -> [(Term, Term)] -> CaseDef
38simpleCase tc cover []
38simpleCase tc cover []
39− = CaseDef [] (UnmatchedCase "No pattern clauses")
39+ = CaseDef [] (UnmatchedCase "No pattern clauses") []
40simpleCase tc cover cs
40simpleCase tc cover cs
41− = let pats = map (\ (l, r) -> (toPats tc l, r)) cs
41+ = let pats = map (\ (l, r) -> (toPats tc l, (l, r))) cs
42− numargs = length (fst (head pats))
42+ numargs = length (fst (head pats))
43− ns = take numargs args
43+ ns = take numargs args
44− tree = evalState (match ns pats (defaultCase cover)) numargs in
44+ (tree, st) = runState (match ns pats (defaultCase cover)) ([], numargs) in
45− CaseDef ns (prune tree)
45+ CaseDef ns (prune tree) (fst st)
46 where args = map (\i -> MN i "e") [0..]
46 where args = map (\i -> MN i "e") [0..]
47 defaultCase True = STerm Erased
47 defaultCase True = STerm Erased
48 defaultCase False = UnmatchedCase "Error"
48 defaultCase False = UnmatchedCase "Error"
@@ -109,8 +109,12 @@ partition xs = error $ "Partition " ++ show xs
109
109
110match :: [Name] -> [Clause] -> SC -- error case
110match :: [Name] -> [Clause] -> SC -- error case
111 -> State CS SC
111 -> State CS SC
112+match [] (([], ret) : xs) err
113+ = do (ts, v) <- get
114+ put (ts ++ (map (fst.snd) xs), v)
112−match [] (([], ret) : _) err = return $ STerm ret -- run out of arguments
115+ return $ STerm (snd ret) -- run out of arguments
113−match vs cs err = mixture vs (partition cs) err
116+match vs cs err = do cs <- mixture vs (partition cs) err
117+ return cs
114
118
115mixture :: [Name] -> [Partition] -> SC -> State CS SC
119mixture :: [Name] -> [Partition] -> SC -> State CS SC
116mixture vs [] err = return err
120mixture vs [] err = return err
@@ -166,7 +170,7 @@ argsToAlt rs@((r, m) : _)
166 addRs ((r, (ps, res)) : rs) = ((r++ps, res) : addRs rs)
170 addRs ((r, (ps, res)) : rs) = ((r++ps, res) : addRs rs)
167
171
168getVar :: State CS Name
172getVar :: State CS Name
169−getVar = do v <- get; put (v+1); return (MN v "e")
173+getVar = do (t, v) <- get; put (t, v+1); return (MN v "e")
170
174
171groupCons :: [Clause] -> State CS [Group]
175groupCons :: [Clause] -> State CS [Group]
172groupCons cs = gc [] cs
176groupCons cs = gc [] cs
@@ -195,7 +199,7 @@ varRule (v : vs) alts err =
195 do let alts' = map (repVar v) alts
199 do let alts' = map (repVar v) alts
196 match vs alts' err
200 match vs alts' err
197 where
201 where
198− repVar v (PV p : ps , res) = (ps, subst p (P Bound v (V 0)) res)
202+ repVar v (PV p : ps , (lhs, res)) = (ps, (lhs, subst p (P Bound v (V 0)) res))
199 repVar v (PAny : ps , res) = (ps, res)
203 repVar v (PAny : ps , res) = (ps, res)
200
204
201prune :: SC -> SC
205prune :: SC -> SC
src/Core/Evaluate.hs+1−1
@@ -529,7 +529,7 @@ addCasedef n alwaysInline tcase covering ps psrt ty uctxt
529 ps' = ps -- simpl ps in
529 ps' = ps -- simpl ps in
530 ctxt' = case (simpleCase tcase covering ps',
530 ctxt' = case (simpleCase tcase covering ps',
531 simpleCase tcase covering psrt) of
531 simpleCase tcase covering psrt) of
532− (CaseDef args sc, CaseDef args' sc') ->
532+ (CaseDef args sc _, CaseDef args' sc' _) ->
533 let inl = alwaysInline in
533 let inl = alwaysInline in
534 addDef n (CaseOp inl ty ps args sc args' sc',
534 addDef n (CaseOp inl ty ps args sc args' sc',
535 Public) ctxt in
535 Public) ctxt in
src/Idris/AbsSyntax.hs+2−2
@@ -1248,11 +1248,11 @@ matchClause' names x y = checkRpts $ match (fullApp x) (fullApp y) where
1248 match (PEq _ l r) (PEq _ l' r') = do ml <- match' l l'
1248 match (PEq _ l r) (PEq _ l' r') = do ml <- match' l l'
1249 mr <- match' r r'
1249 mr <- match' r r'
1250 return (ml ++ mr)
1250 return (ml ++ mr)
1251− match (PTyped l r) x = match l x
1252− match x (PTyped l r) = match x l
1253 match (PTyped l r) (PTyped l' r') = do ml <- match l l'
1251 match (PTyped l r) (PTyped l' r') = do ml <- match l l'
1254 mr <- match r r'
1252 mr <- match r r'
1255 return (ml ++ mr)
1253 return (ml ++ mr)
1254+ match (PTyped l r) x = match l x
1255+ match x (PTyped l r) = match x l
1256 match (PPair _ l r) (PPair _ l' r') = do ml <- match' l l'
1256 match (PPair _ l r) (PPair _ l' r') = do ml <- match' l l'
1257 mr <- match' r r'
1257 mr <- match' r r'
1258 return (ml ++ mr)
1258 return (ml ++ mr)
src/Idris/ElabDecls.hs+6
@@ -128,6 +128,12 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
128 else return False
128 else return False
129 pdef' <- applyOpts pdef
129 pdef' <- applyOpts pdef
130 let tree = simpleCase tcase pcover pdef
130 let tree = simpleCase tcase pcover pdef
131+ case tree of
132+ CaseDef _ _ [] -> return ()
133+ CaseDef _ _ xs -> mapM_ (\x ->
134+ iputStrLn $ show fc ++
135+ ":warning - Unreachable case: " ++
136+ show (delab ist x)) xs
131 let tree' = simpleCase tcase pcover pdef'
137 let tree' = simpleCase tcase pcover pdef'
132 tclift $ sameLength pdef
138 tclift $ sameLength pdef
133 logLvl 3 (show tree)
139 logLvl 3 (show tree)