Skip to content
Browse files

Unreachable case warning

  • Loading branch information...
1 parent 12c93ed commit 6807cf46411ea8db7d8d3cf14b5084b361e21d44 Edwin Brady committed Jan 21, 2012
Showing with 26 additions and 16 deletions.
  1. +1 −1 Makefile
  2. +16 −12 src/Core/CaseTree.hs
  3. +1 −1 src/Core/Evaluate.hs
  4. +2 −2 src/Idris/AbsSyntax.hs
  5. +6 −0 src/Idris/ElabDecls.hs
View
2 Makefile
@@ -16,7 +16,7 @@ test : .PHONY
relib: .PHONY
make -C lib clean
- make -C lib BINDIR=../dist/build/idris
+ make -C lib IDRIS=../dist/build/idris/idris
linecount : .PHONY
wc -l src/Idris/*.hs src/Core/*.hs
View
28 src/Core/CaseTree.hs
@@ -26,8 +26,8 @@ deriving instance Binary CaseAlt
!-}
type CaseTree = SC
-type Clause = ([Pat], Term)
-type CS = Int
+type Clause = ([Pat], (Term, Term))
+type CS = ([Term], Int)
-- simple terms can be inlined trivially - good for primitives in particular
small :: SC -> Bool
@@ -36,13 +36,13 @@ small _ = False
simpleCase :: Bool -> Bool -> [(Term, Term)] -> CaseDef
simpleCase tc cover []
- = CaseDef [] (UnmatchedCase "No pattern clauses")
+ = CaseDef [] (UnmatchedCase "No pattern clauses") []
simpleCase tc cover cs
- = let pats = map (\ (l, r) -> (toPats tc l, r)) cs
- numargs = length (fst (head pats))
- ns = take numargs args
- tree = evalState (match ns pats (defaultCase cover)) numargs in
- CaseDef ns (prune tree)
+ = let pats = map (\ (l, r) -> (toPats tc l, (l, r))) cs
+ numargs = length (fst (head pats))
+ ns = take numargs args
+ (tree, st) = runState (match ns pats (defaultCase cover)) ([], numargs) in
+ CaseDef ns (prune tree) (fst st)
where args = map (\i -> MN i "e") [0..]
defaultCase True = STerm Erased
defaultCase False = UnmatchedCase "Error"
@@ -109,8 +109,12 @@ partition xs = error $ "Partition " ++ show xs
match :: [Name] -> [Clause] -> SC -- error case
-> State CS SC
-match [] (([], ret) : _) err = return $ STerm ret -- run out of arguments
-match vs cs err = mixture vs (partition cs) err
+match [] (([], ret) : xs) err
+ = do (ts, v) <- get
+ put (ts ++ (map (fst.snd) xs), v)
+ return $ STerm (snd ret) -- run out of arguments
+match vs cs err = do cs <- mixture vs (partition cs) err
+ return cs
mixture :: [Name] -> [Partition] -> SC -> State CS SC
mixture vs [] err = return err
@@ -166,7 +170,7 @@ argsToAlt rs@((r, m) : _)
addRs ((r, (ps, res)) : rs) = ((r++ps, res) : addRs rs)
getVar :: State CS Name
-getVar = do v <- get; put (v+1); return (MN v "e")
+getVar = do (t, v) <- get; put (t, v+1); return (MN v "e")
groupCons :: [Clause] -> State CS [Group]
groupCons cs = gc [] cs
@@ -195,7 +199,7 @@ varRule (v : vs) alts err =
do let alts' = map (repVar v) alts
match vs alts' err
where
- repVar v (PV p : ps , res) = (ps, subst p (P Bound v (V 0)) res)
+ repVar v (PV p : ps , (lhs, res)) = (ps, (lhs, subst p (P Bound v (V 0)) res))
repVar v (PAny : ps , res) = (ps, res)
prune :: SC -> SC
View
2 src/Core/Evaluate.hs
@@ -529,7 +529,7 @@ addCasedef n alwaysInline tcase covering ps psrt ty uctxt
ps' = ps -- simpl ps in
ctxt' = case (simpleCase tcase covering ps',
simpleCase tcase covering psrt) of
- (CaseDef args sc, CaseDef args' sc') ->
+ (CaseDef args sc _, CaseDef args' sc' _) ->
let inl = alwaysInline in
addDef n (CaseOp inl ty ps args sc args' sc',
Public) ctxt in
View
4 src/Idris/AbsSyntax.hs
@@ -1248,11 +1248,11 @@ matchClause' names x y = checkRpts $ match (fullApp x) (fullApp y) where
match (PEq _ l r) (PEq _ l' r') = do ml <- match' l l'
mr <- match' r r'
return (ml ++ mr)
- match (PTyped l r) x = match l x
- match x (PTyped l r) = match x l
match (PTyped l r) (PTyped l' r') = do ml <- match l l'
mr <- match r r'
return (ml ++ mr)
+ match (PTyped l r) x = match l x
+ match x (PTyped l r) = match x l
match (PPair _ l r) (PPair _ l' r') = do ml <- match' l l'
mr <- match' r r'
return (ml ++ mr)
View
6 src/Idris/ElabDecls.hs
@@ -128,6 +128,12 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
else return False
pdef' <- applyOpts pdef
let tree = simpleCase tcase pcover pdef
+ case tree of
+ CaseDef _ _ [] -> return ()
+ CaseDef _ _ xs -> mapM_ (\x ->
+ iputStrLn $ show fc ++
+ ":warning - Unreachable case: " ++
+ show (delab ist x)) xs
let tree' = simpleCase tcase pcover pdef'
tclift $ sameLength pdef
logLvl 3 (show tree)

0 comments on commit 6807cf4

Please sign in to comment.
Something went wrong with that request. Please try again.