b1e95cb · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Fix coverage checker

commitb1e95cb87eabed5408783781821163ae4cbcbb0a authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateWed 1 Feb 2012, 14:41 (15 years ago) parent7fb7dec

5 files changed+70−27

compare with master

unifiedsplit

src/Core/CaseTree.hs+2−1 src/Idris/AbsSyntax.hs+7−5 src/Idris/Coverage.hs+19−6 src/Idris/ElabDecls.hs+35−14 src/Idris/REPL.hs+7−1

src/Core/CaseTree.hs+2−1

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

44import Core.TT

66import Control.Monad.State

7+import Data.Maybe

78import Data.List hiding (partition)

89import Debug.Trace

910

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

227228 case alts' of

228229 [] -> STerm Erased

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

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

232233 pruneAlt (DefaultCase sc) = DefaultCase (prune sc)

233234

src/Idris/AbsSyntax.hs+7−5

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

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

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

13261326

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

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

13281328matchClause = matchClause' False

13291329

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

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

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

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

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

13331333

13341334 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

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

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

13511351 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)]

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

13541356 mr <- match' r r'

13551357 return (ml ++ mr)

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

13951397 return (mt ++ mty ++ ms)

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

13971399 match Placeholder _ = return []

1398− match _ Placeholder = return []

1400+-- match _ Placeholder = return []

13991401 match (PResolveTC _) _ = return []

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

14011403 | otherwise = LeftErr (a, b)

src/Idris/Coverage.hs+19−6

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

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

3535 (p : _) -> p

3636 _ -> repeat (pexp Placeholder)

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

37+ let tryclauses = mkClauses parg all_args

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

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

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

3941 return new

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

4143 where getLHS i term

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

4749

4850 mnub i [] = []

4951 mnub i (x : xs) =

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

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

5153 Right _ -> True

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

5355 else x : mnub i xs

5456

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

5658 Right _ -> False

5759 Left miss -> True) xs

5860

5961

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

63+ mkClauses parg args

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

6165 mkClauses parg args

6266 = do args' <- mkArg args

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

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

6973 as' <- mkArg as

7074 return (a':as')

7175

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

77+-- up to that depth.

78+

7279genAll :: 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

7483 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+

7588 otherPats :: PTerm -> [PTerm]

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

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

78− otherPats arg = return arg

91+ otherPats arg = return Placeholder

7992

8093 ops fc n xs o

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

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

8598 case lookupCtxt Nothing tyn (idris_datatypes i) of

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

87100 _ -> [p]

88− ops fc n arg o = return o

101+ ops fc n arg o = return Placeholder

89102

90103 getTy n ctxt = case lookupTy Nothing n ctxt of

91104 (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

227227 pcover <-

228228 if cov

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

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

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

232− return (null missing')

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

231+ let missing' = mapMaybe id poss

232+ logLvl 3 $ "Must be unreachable: " ++ show missing' ++ " from " ++ show 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

233247 else return False

234248 pdef' <- applyOpts pdef

235249 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

263277 tcase pcover pdef pdef' ty)

264278 addIBC (IBCDef n)

265279 setTotality n tot

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

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

281+ else addIBC (IBCTotal n tot)

267282 i <- get

268283 case lookupDef Nothing n (tt_ctxt i) of

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

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

301316 logLvl 2 (show vtm)

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

303318

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

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

320+-- possible, otherwise Nothing.

321+

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

305323checkPossible info fc tcgen fname lhs_in

306324 = do ctxt <- getContext

307325 i <- get

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

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

313331 do let lhs_tm = orderPats (getInferTerm lhs')

314332 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

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

317− Error _ -> return False

335+ Error _ -> return Nothing

318336

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

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

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

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

323− else return Nothing

340+ case b of

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

342+ Nothing -> return Nothing

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

325344 = do ctxt <- getContext

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

471490 let tm = addImpl i tm_in

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

473492 showImp True toplhs)

474− case matchClause toplhs tm of

493+ case matchClause i toplhs tm of

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

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

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

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

483502 showImp True toplhs)

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

485− case matchClause toplhs tm of

504+ case matchClause i toplhs tm of

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

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

488507 return $ PWith wname lhs ws wval withs'

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

797816checkInferred fc inf user =

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

799818 showImp True user

800− tclift $ case matchClause' True user inf of

819+ i <- get

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

801821 Right vs -> return ()

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

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

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

809829

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

811831inferredDiff fc inf user =

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

832+ do i <- get

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

813834 showImp True user

814− tclift $ case matchClause' True user inf of

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

815836 Right vs -> return False

816837 Left (x, y) -> return True

817838

src/Idris/REPL.hs+7−1

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

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

178178 mapM_ (printCase i) d

179179 case lookupTotal n (tt_ctxt i) of

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

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

181181 _ -> return ()

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

183183 liftIO $ putStr " = "

184184 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+ _ -> ""

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

186192 let oi = lookupCtxt Nothing n (idris_optimisation i)

187193 liftIO $ print oi