b1e95cb · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Fix coverage checker

b1e95cbEdwin Brady15 years ago

src/Core/CaseTree.hs+2−1

compare with master

unifiedsplit

@@ -4,6 +4,7 @@ module Core.CaseTree(CaseDef(..), SC(..), CaseAlt(..), CaseTree,

4import Core.TT

6import Control.Monad.State

7+import Data.Maybe

7import Data.List hiding (partition)

8import Data.List hiding (partition)

8import Debug.Trace

9import Debug.Trace

@@ -227,7 +228,7 @@ prune (Case n alts)

227 case alts' of

228 case alts' of

228 [] -> STerm Erased

229 [] -> STerm Erased

229 as -> Case n as

230 as -> Case n as

230− where pruneAlt (ConCase n i ns sc) = ConCase n i ns (prune sc)

231+ where pruneAlt (ConCase cn i ns sc) = ConCase cn i ns (prune sc)

231 pruneAlt (ConstCase c sc) = ConstCase c (prune sc)

232 pruneAlt (ConstCase c sc) = ConstCase c (prune sc)

232 pruneAlt (DefaultCase sc) = DefaultCase (prune sc)

233 pruneAlt (DefaultCase sc) = DefaultCase (prune sc)

233

234

src/Idris/AbsSyntax.hs+7−5

@@ -1324,11 +1324,11 @@ toEither (RightOK ho) = Right ho

1324-- syntactic match of a against b, returning pair of variables in a

1325-- and what they match. Returns the pair that failed if not a match.

1326

1327−matchClause :: PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]

1327+matchClause :: IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]

1328matchClause = matchClause' False

1329

1330−matchClause' :: Bool -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]

1330+matchClause' :: Bool -> IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]

1331−matchClause' names x y = checkRpts $ match (fullApp x) (fullApp y) where

1331+matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where

1332 matchArg x y = match (fullApp (getTm x)) (fullApp (getTm y))

1333

1334 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))

@@ -1349,7 +1349,9 @@ matchClause' names x y = checkRpts $ match (fullApp x) (fullApp y) where

1349 match (PRef f n) (PApp _ x []) = match (PRef f n) x

1350 match (PApp _ x []) (PRef f n) = match x (PRef f n)

1351 match (PRef _ n) (PRef _ n') | n == n' = return []

1352− match (PRef _ n) tm | not names = return [(n, tm)]

1352+ match (PRef _ n) tm

1353+ | not names && not (isConName Nothing n (tt_ctxt i))

1354+ = return [(n, tm)]

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

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

1354 mr <- match' r r'

1356 mr <- match' r r'

1355 return (ml ++ mr)

1357 return (ml ++ mr)

@@ -1395,7 +1397,7 @@ matchClause' names x y = checkRpts $ match (fullApp x) (fullApp y) where

1395 return (mt ++ mty ++ ms)

1397 return (mt ++ mty ++ ms)

1396 match (PHidden x) (PHidden y) = match' x y

1398 match (PHidden x) (PHidden y) = match' x y

1397 match Placeholder _ = return []

1399 match Placeholder _ = return []

1398− match _ Placeholder = return []

1400+-- match _ Placeholder = return []

1399 match (PResolveTC _) _ = return []

1401 match (PResolveTC _) _ = return []

1400 match a b | a == b = return []

1402 match a b | a == b = return []

1401 | otherwise = LeftErr (a, b)

1403 | otherwise = LeftErr (a, b)

src/Idris/Coverage.hs+19−6

@@ -34,8 +34,10 @@ genClauses fc n xs given

34 let parg = case lookupCtxt Nothing n (idris_implicits i) of

35 (p : _) -> p

36 _ -> repeat (pexp Placeholder)

37+ let tryclauses = mkClauses parg all_args

37− let new = mnub i $ filter (noMatch i) $ mkClauses parg all_args

38+ let new = mnub i $ filter (noMatch i) tryclauses

38 logLvl 7 $ "New clauses: \n" ++ showSep "\n" (map (showImp True) new)

39 logLvl 7 $ "New clauses: \n" ++ showSep "\n" (map (showImp True) new)

40+ ++ " from:\n" ++ showSep "\n" (map (showImp True) tryclauses)

39 return new

41 return new

40-- return (map (\t -> PClause n t [] PImpossible []) new)

42-- return (map (\t -> PClause n t [] PImpossible []) new)

41 where getLHS i term

43 where getLHS i term

@@ -47,17 +49,19 @@ genClauses fc n xs given

48 mnub i [] = []

50 mnub i [] = []

49 mnub i (x : xs) =

51 mnub i (x : xs) =

50− if (any (\t -> case matchClause x t of

52+ if (any (\t -> case matchClause i x t of

51 Right _ -> True

53 Right _ -> True

52 Left _ -> False) xs) then mnub i xs

54 Left _ -> False) xs) then mnub i xs

53 else x : mnub i xs

55 else x : mnub i xs

55− noMatch i tm = all (\x -> case matchClause (delab' i x True) tm of

57+ noMatch i tm = all (\x -> case matchClause i (delab' i x True) tm of

56 Right _ -> False

58 Right _ -> False

57 Left miss -> True) xs

59 Left miss -> True) xs

60 mkClauses :: [PArg] -> [[PTerm]] -> [PTerm]

62 mkClauses :: [PArg] -> [[PTerm]] -> [PTerm]

63+ mkClauses parg args

64+ | all (== [Placeholder]) args = []

61 mkClauses parg args

65 mkClauses parg args

62 = do args' <- mkArg args

66 = do args' <- mkArg args

63 let tm = PApp fc (PRef fc n) (zipWith upd args' parg)

67 let tm = PApp fc (PRef fc n) (zipWith upd args' parg)

@@ -69,13 +73,22 @@ genClauses fc n xs given

69 as' <- mkArg as

73 as' <- mkArg as

70 return (a':as')

74 return (a':as')

76+-- FIXME: Just look for which one is the deepest, then generate all possibilities

77+-- up to that depth.

78+

72genAll :: IState -> [PTerm] -> [PTerm]

79genAll :: IState -> [PTerm] -> [PTerm]

73−genAll i args = concatMap otherPats (nub args)

80+genAll i args = case filter (/=Placeholder) $ concatMap otherPats (nub args) of

81+ [] -> [Placeholder]

82+ xs -> xs

74 where

83 where

84+ conForm (PApp _ (PRef fc n) _) = isConName Nothing n (tt_ctxt i)

85+ conForm (PRef fc n) = isConName Nothing n (tt_ctxt i)

86+ conForm _ = False

87+

75 otherPats :: PTerm -> [PTerm]

88 otherPats :: PTerm -> [PTerm]

76 otherPats o@(PRef fc n) = ops fc n [] o

89 otherPats o@(PRef fc n) = ops fc n [] o

77 otherPats o@(PApp _ (PRef fc n) xs) = ops fc n xs o

90 otherPats o@(PApp _ (PRef fc n) xs) = ops fc n xs o

78− otherPats arg = return arg

91+ otherPats arg = return Placeholder

80 ops fc n xs o

93 ops fc n xs o

81 | (TyDecl c@(DCon _ arity) ty : _) <- lookupDef Nothing n (tt_ctxt i)

94 | (TyDecl c@(DCon _ arity) ty : _) <- lookupDef Nothing n (tt_ctxt i)

@@ -85,7 +98,7 @@ genAll i args = concatMap otherPats (nub args)

85 case lookupCtxt Nothing tyn (idris_datatypes i) of

98 case lookupCtxt Nothing tyn (idris_datatypes i) of

86 (TI ns : _) -> p : map (mkPat fc) (ns \\ [n])

99 (TI ns : _) -> p : map (mkPat fc) (ns \\ [n])

87 _ -> [p]

100 _ -> [p]

88− ops fc n arg o = return o

101+ ops fc n arg o = return Placeholder

102

90 getTy n ctxt = case lookupTy Nothing n ctxt of

103 getTy n ctxt = case lookupTy Nothing n ctxt of

91 (t : _) -> case unApply (getRetTy t) of

104 (t : _) -> case unApply (getRetTy t) of

src/Idris/ElabDecls.hs+35−14

@@ -227,9 +227,23 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

227 pcover <-

228 if cov

229 then do missing <- genClauses fc n (map fst pdef) cs

230− missing' <- filterM (checkPossible info fc True n) missing

230+ poss <- mapM (checkPossible info fc True n) missing

231+ let missing' = mapMaybe id poss

231− logLvl 5 $ "Must be unreachable: " ++ show missing' ++ " from " ++ show missing

232+ logLvl 3 $ "Must be unreachable: " ++ show missing' ++ " from " ++ show missing

232− return (null missing')

233+ if null missing'

234+ then return True

235+ else return False

236+-- -- if there's missing cases, add a catch all case. If it's

237+-- -- unreachable, we're still covering

238+-- do let mrhs = P Ref (MN 0 "reach?") undefined

239+-- let (f,as) = unApply $ depat (head missing')

240+-- let arity = length as

241+-- let mlhs = mkApp f (map (\a -> P Bound (MN a "v") undefined)

242+-- [0..arity-1])

243+-- let untree@(CaseDef _ sc _) = simpleCase tcase True

244+-- (pdef ++ [(mlhs, mrhs)])

245+-- logLvl 5 $ "Tree is " ++ show sc

246+-- return False

233 else return False

247 else return False

234 pdef' <- applyOpts pdef

248 pdef' <- applyOpts pdef

235 let tree@(CaseDef _ sc _) = simpleCase tcase pcover pdef

249 let tree@(CaseDef _ sc _) = simpleCase tcase pcover pdef

@@ -263,7 +277,8 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

263 tcase pcover pdef pdef' ty)

277 tcase pcover pdef pdef' ty)

264 addIBC (IBCDef n)

278 addIBC (IBCDef n)

265 setTotality n tot

279 setTotality n tot

266− when (tot == Unchecked) $ totcheck (fc, n)

280+ if (tot == Unchecked) then totcheck (fc, n)

281+ else addIBC (IBCTotal n tot)

267 i <- get

282 i <- get

268 case lookupDef Nothing n (tt_ctxt i) of

283 case lookupDef Nothing n (tt_ctxt i) of

269 (CaseOp _ _ _ _ sc _ _ : _) ->

284 (CaseOp _ _ _ _ sc _ _ : _) ->

@@ -301,7 +316,10 @@ elabVal info aspat tm_in

301 logLvl 2 (show vtm)

316 logLvl 2 (show vtm)

302 recheckC ctxt (FC "prompt" 0) [] vtm

317 recheckC ctxt (FC "prompt" 0) [] vtm

303

318

319+-- checks if the clause is a possible left hand side. Returns the term if

320+-- possible, otherwise Nothing.

321+

304−checkPossible :: ElabInfo -> FC -> Bool -> Name -> PTerm -> Idris Bool

322+checkPossible :: ElabInfo -> FC -> Bool -> Name -> PTerm -> Idris (Maybe Term)

305checkPossible info fc tcgen fname lhs_in

323checkPossible info fc tcgen fname lhs_in

306 = do ctxt <- getContext

324 = do ctxt <- getContext

307 i <- get

325 i <- get

@@ -312,15 +330,16 @@ checkPossible info fc tcgen fname lhs_in

312 OK ((lhs', _, _), _) ->

330 OK ((lhs', _, _), _) ->

313 do let lhs_tm = orderPats (getInferTerm lhs')

331 do let lhs_tm = orderPats (getInferTerm lhs')

314 b <- inferredDiff fc (delab' i lhs_tm True) lhs

332 b <- inferredDiff fc (delab' i lhs_tm True) lhs

315− return (not b)

333+ if not b then return (Just lhs_tm) else return Nothing

316-- trace (show (delab' i lhs_tm True) ++ "\n" ++ show lhs) $ return (not b)

334-- trace (show (delab' i lhs_tm True) ++ "\n" ++ show lhs) $ return (not b)

317− Error _ -> return False

335+ Error _ -> return Nothing

318

336

319elabClause :: ElabInfo -> FC -> Bool -> PClause -> Idris (Maybe (Term, Term))

337elabClause :: ElabInfo -> FC -> Bool -> PClause -> Idris (Maybe (Term, Term))

320elabClause info fc tcgen (PClause fname lhs_in [] PImpossible [])

338elabClause info fc tcgen (PClause fname lhs_in [] PImpossible [])

321 = do b <- checkPossible info fc tcgen fname lhs_in

339 = do b <- checkPossible info fc tcgen fname lhs_in

340+ case b of

322− if b then fail $ show fc ++ ":" ++ show lhs_in ++ " is a possible case"

341+ Just _ -> fail $ show fc ++ ":" ++ show lhs_in ++ " is a possible case"

323− else return Nothing

342+ Nothing -> return Nothing

324elabClause info fc tcgen (PClause fname lhs_in withs rhs_in whereblock)

343elabClause info fc tcgen (PClause fname lhs_in withs rhs_in whereblock)

325 = do ctxt <- getContext

344 = do ctxt <- getContext

326 -- Build the LHS as an "Infer", and pull out its type and

345 -- Build the LHS as an "Infer", and pull out its type and

@@ -471,7 +490,7 @@ elabClause info fc tcgen (PWith fname lhs_in withs wval_in withblock)

471 let tm = addImpl i tm_in

490 let tm = addImpl i tm_in

472 logLvl 2 ("Matching " ++ showImp True tm ++ " against " ++

491 logLvl 2 ("Matching " ++ showImp True tm ++ " against " ++

473 showImp True toplhs)

492 showImp True toplhs)

474− case matchClause toplhs tm of

493+ case matchClause i toplhs tm of

475 Left _ -> fail $ show fc ++ "with clause does not match top level"

494 Left _ -> fail $ show fc ++ "with clause does not match top level"

476 Right mvars -> do logLvl 3 ("Match vars : " ++ show mvars)

495 Right mvars -> do logLvl 3 ("Match vars : " ++ show mvars)

477 lhs <- updateLHS n wname mvars ns (fullApp tm) w

496 lhs <- updateLHS n wname mvars ns (fullApp tm) w

@@ -482,7 +501,7 @@ elabClause info fc tcgen (PWith fname lhs_in withs wval_in withblock)

482 logLvl 2 ("Matching " ++ showImp True tm ++ " against " ++

501 logLvl 2 ("Matching " ++ showImp True tm ++ " against " ++

483 showImp True toplhs)

502 showImp True toplhs)

484 withs' <- mapM (mkAuxC wname toplhs ns) withs

503 withs' <- mapM (mkAuxC wname toplhs ns) withs

485− case matchClause toplhs tm of

504+ case matchClause i toplhs tm of

486 Left _ -> fail $ show fc ++ "with clause does not match top level"

505 Left _ -> fail $ show fc ++ "with clause does not match top level"

487 Right mvars -> do lhs <- updateLHS n wname mvars ns (fullApp tm) w

506 Right mvars -> do lhs <- updateLHS n wname mvars ns (fullApp tm) w

488 return $ PWith wname lhs ws wval withs'

507 return $ PWith wname lhs ws wval withs'

@@ -797,7 +816,8 @@ checkInferred :: FC -> PTerm -> PTerm -> Idris ()

797checkInferred fc inf user =

816checkInferred fc inf user =

798 do logLvl 6 $ "Checked to\n" ++ showImp True inf ++ "\n" ++

817 do logLvl 6 $ "Checked to\n" ++ showImp True inf ++ "\n" ++

799 showImp True user

818 showImp True user

819+ i <- get

800− tclift $ case matchClause' True user inf of

820+ tclift $ case matchClause' True i user inf of

801 Right vs -> return ()

821 Right vs -> return ()

802 Left (x, y) -> tfail $ At fc

822 Left (x, y) -> tfail $ At fc

803 (Msg $ "The type-checked term and given term do not match: "

823 (Msg $ "The type-checked term and given term do not match: "

@@ -809,9 +829,10 @@ checkInferred fc inf user =

809

829

810inferredDiff :: FC -> PTerm -> PTerm -> Idris Bool

830inferredDiff :: FC -> PTerm -> PTerm -> Idris Bool

811inferredDiff fc inf user =

831inferredDiff fc inf user =

832+ do i <- get

812− do logLvl 6 $ "Checked to\n" ++ showImp True inf ++ "\n" ++

833+ logLvl 6 $ "Checked to\n" ++ showImp True inf ++ "\n" ++

813 showImp True user

834 showImp True user

814− tclift $ case matchClause' True user inf of

835+ tclift $ case matchClause' True i user inf of

815 Right vs -> return False

836 Right vs -> return False

816 Left (x, y) -> return True

837 Left (x, y) -> return True

817

838

src/Idris/REPL.hs+7−1

@@ -177,11 +177,17 @@ process fn (Defn n) = do i <- get

177 [d] -> do iputStrLn "Original definiton:\n"

178 mapM_ (printCase i) d

179 case lookupTotal n (tt_ctxt i) of

180− [t] -> iputStrLn (show t)

180+ [t] -> iputStrLn (showTotal t i)

181 _ -> return ()

182 where printCase i (lhs, rhs) = do liftIO $ putStr $ showImp True (delab i lhs)

183 liftIO $ putStr " = "

184 liftIO $ putStrLn $ showImp True (delab i rhs)

185+ showTotal t@(Partial (Other ns)) i

186+ = show t ++ "\n\t" ++ showSep "\n\t" (map (showTotalN i) ns)

187+ showTotal t i = show t

188+ showTotalN i n = case lookupTotal n (tt_ctxt i) of

189+ [t] -> showTotal t i

190+ _ -> ""

185process fn (Info n) = do i <- get

191process fn (Info n) = do i <- get

186 let oi = lookupCtxt Nothing n (idris_optimisation i)

192 let oi = lookupCtxt Nothing n (idris_optimisation i)

187 liftIO $ print oi

193 liftIO $ print oi