6807cf4 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Unreachable case warning

commit6807cf46411ea8db7d8d3cf14b5084b361e21d44 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateSat 21 Jan 2012, 10:45 (15 years ago) parent12c93ed

5 files changed+26−16

compare with master

unifiedsplit

Makefile+1−1 src/Core/CaseTree.hs+16−12 src/Core/Evaluate.hs+1−1 src/Idris/AbsSyntax.hs+2−2 src/Idris/ElabDecls.hs+6

Makefile+1−1

@@ -16,7 +16,7 @@ test : .PHONY

1616

1717relib: .PHONY

1818 make -C lib clean

19− make -C lib BINDIR=../dist/build/idris

19+ make -C lib IDRIS=../dist/build/idris/idris

2020

2121linecount : .PHONY

2222 wc -l src/Idris/*.hs src/Core/*.hs

src/Core/CaseTree.hs+16−12

@@ -26,8 +26,8 @@ deriving instance Binary CaseAlt

2626!-}

2727

2828type CaseTree = SC

29−type Clause = ([Pat], Term)

30−type CS = Int

29+type Clause = ([Pat], (Term, Term))

30+type CS = ([Term], Int)

3131

3232-- simple terms can be inlined trivially - good for primitives in particular

3333small :: SC -> Bool

@@ -36,13 +36,13 @@ small _ = False

3636

3737simpleCase :: Bool -> Bool -> [(Term, Term)] -> CaseDef

3838simpleCase tc cover []

39− = CaseDef [] (UnmatchedCase "No pattern clauses")

39+ = CaseDef [] (UnmatchedCase "No pattern clauses") []

4040simpleCase tc cover cs

41− = let pats = map (\ (l, r) -> (toPats tc l, r)) cs

42− numargs = length (fst (head pats))

43− ns = take numargs args

44− tree = evalState (match ns pats (defaultCase cover)) numargs in

45− CaseDef ns (prune tree)

41+ = let pats = map (\ (l, r) -> (toPats tc l, (l, r))) cs

42+ numargs = length (fst (head pats))

43+ ns = take numargs args

44+ (tree, st) = runState (match ns pats (defaultCase cover)) ([], numargs) in

45+ CaseDef ns (prune tree) (fst st)

4646 where args = map (\i -> MN i "e") [0..]

4747 defaultCase True = STerm Erased

4848 defaultCase False = UnmatchedCase "Error"

@@ -109,8 +109,12 @@ partition xs = error $ "Partition " ++ show xs

109109

110110match :: [Name] -> [Clause] -> SC -- error case

111111 -> State CS SC

112−match [] (([], ret) : _) err = return $ STerm ret -- run out of arguments

113−match vs cs err = mixture vs (partition cs) err

112+match [] (([], ret) : xs) err

113+ = do (ts, v) <- get

114+ put (ts ++ (map (fst.snd) xs), v)

115+ return $ STerm (snd ret) -- run out of arguments

116+match vs cs err = do cs <- mixture vs (partition cs) err

117+ return cs

114118

115119mixture :: [Name] -> [Partition] -> SC -> State CS SC

116120mixture vs [] err = return err

@@ -166,7 +170,7 @@ argsToAlt rs@((r, m) : _)

166170 addRs ((r, (ps, res)) : rs) = ((r++ps, res) : addRs rs)

167171

168172getVar :: 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")

170174

171175groupCons :: [Clause] -> State CS [Group]

172176groupCons cs = gc [] cs

@@ -195,7 +199,7 @@ varRule (v : vs) alts err =

195199 do let alts' = map (repVar v) alts

196200 match vs alts' err

197201 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))

199203 repVar v (PAny : ps , res) = (ps, res)

200204

201205prune :: SC -> SC

src/Core/Evaluate.hs+1−1

@@ -529,7 +529,7 @@ addCasedef n alwaysInline tcase covering ps psrt ty uctxt

529529 ps' = ps -- simpl ps in

530530 ctxt' = case (simpleCase tcase covering ps',

531531 simpleCase tcase covering psrt) of

532− (CaseDef args sc, CaseDef args' sc') ->

532+ (CaseDef args sc _, CaseDef args' sc' _) ->

533533 let inl = alwaysInline in

534534 addDef n (CaseOp inl ty ps args sc args' sc',

535535 Public) ctxt in

src/Idris/AbsSyntax.hs+2−2

@@ -1248,11 +1248,11 @@ matchClause' names x y = checkRpts $ match (fullApp x) (fullApp y) where

12481248 match (PEq _ l r) (PEq _ l' r') = do ml <- match' l l'

12491249 mr <- match' r r'

12501250 return (ml ++ mr)

1251− match (PTyped l r) x = match l x

1252− match x (PTyped l r) = match x l

12531251 match (PTyped l r) (PTyped l' r') = do ml <- match l l'

12541252 mr <- match r r'

12551253 return (ml ++ mr)

1254+ match (PTyped l r) x = match l x

1255+ match x (PTyped l r) = match x l

12561256 match (PPair _ l r) (PPair _ l' r') = do ml <- match' l l'

12571257 mr <- match' r r'

12581258 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

128128 else return False

129129 pdef' <- applyOpts pdef

130130 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

131137 let tree' = simpleCase tcase pcover pdef'

132138 tclift $ sameLength pdef

133139 logLvl 3 (show tree)