06e2b1d · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Efficiency of coverage check

Instead of checking fully elaborated definitions, make sure we only check cases which the programmer has written explicitly - other cases are ruled out by unification. Fixes #975 I had thought I had done this a while ago, but it turns out I didn't do it properly! This should make many pathological coverage checking examples significantly quicker.

commit06e2b1df5648bf7d01d360823a41a814f9b5196c authorEdwin Brady <ecb10@st-andrews.ac.uk> dateThu 3 Apr 2014, 13:33 (13 years ago) parent4e0bdc8

2 files changed+29−10

compare with master

unifiedsplit

src/Idris/Coverage.hs+18−4 src/Idris/ElabDecls.hs+11−6

src/Idris/Coverage.hs+18−4

@@ -51,13 +51,18 @@ mkPatTm t = do i <- getIState

5151-- This will only work after the given clauses have been typechecked and the

5252-- names are fully explicit!

5353

54−genClauses :: FC -> Name -> [Term] -> [PClause] -> Idris [PTerm]

54+genClauses :: FC -> Name -> [Term] -> [PTerm] -> Idris [PTerm]

5555genClauses fc n xs given

5656 = do i <- getIState

57− let lhss = map (getLHS i) xs

57+ let lhs_tms = map (\x -> delab' i x True True) xs

58+ -- if a placeholder was given, don't bother generating cases for it

59+ let lhs_tms' = zipWith mergePlaceholders lhs_tms given

60+ let lhss = map pUnApply lhs_tms'

61+

5862 let argss = transpose lhss

5963 let all_args = map (genAll i) argss

6064 logLvl 5 $ "COVERAGE of " ++ show n

65+ logLvl 5 $ show lhss

6166 logLvl 5 $ show (map length argss) ++ "\n" ++ show (map length all_args)

6267 logLvl 10 $ show argss ++ "\n" ++ show all_args

6368 logLvl 1 $ "Original: \n" ++

@@ -82,8 +87,8 @@ genClauses fc n xs given

8287 | (f, args) <- unApply term = map (\t -> delab' i t True True) args

8388 | otherwise = []

8489

85− lhsApp (PClause _ _ l _ _ _) = l

86− lhsApp (PWith _ _ l _ _ _) = l

90+ pUnApply (PApp _ _ args) = map getTm args

91+ pUnApply _ = []

8792

8893 -- Return whether the given clause matches none of the input clauses

8994 -- (xs)

@@ -92,6 +97,14 @@ genClauses fc n xs given

9297 Left miss -> True) xs

9398

9499

100+ mergePlaceholders :: PTerm -> PTerm -> PTerm

101+ mergePlaceholders x Placeholder = Placeholder

102+ mergePlaceholders (PApp fc f args) (PApp fc' f' args')

103+ = PApp fc' f' (zipWith mergePArg args args')

104+ where mergePArg x y = let xtm = mergePlaceholders (getTm x) (getTm y) in

105+ x { getTm = xtm}

106+ mergePlaceholders x _ = x

107+

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

96109 mkClauses parg args

97110 | all (== [Placeholder]) args = []

@@ -114,6 +127,7 @@ fnub' acc [] = acc

114127

115128-- quick check for constructor equality

116129quickEq :: PTerm -> PTerm -> Bool

130+quickEq (PConstant n) (PConstant n') = n == n'

117131quickEq (PRef _ n) (PRef _ n') = n == n'

118132quickEq (PApp _ t as) (PApp _ t' as')

119133 | length as == length as'

src/Idris/ElabDecls.hs+11−6

@@ -908,8 +908,10 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

908908 tclift $ tfail $ At fc (NoTypeDecl n)

909909 [ty] -> return ty

910910 let atys = map snd (getArgTys fty)

911− pats_in <- mapM (elabClause info opts)

911+ cs_elab <- mapM (elabClause info opts)

912912 (zip [0..] cs)

913+ let (pats_in, cs_full) = unzip cs_elab

914+

913915 logLvl 3 $ "Elaborated patterns:\n" ++ show pats_in

914916

915917 -- if the return type of 'ty' is collapsible, the optimised version should

@@ -994,7 +996,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

994996 cov <- coverage

995997 pmissing <-

996998 if cov && not (hasDefault cs)

997− then do missing <- genClauses fc n (map getLHS pdef) cs

999+ then do missing <- genClauses fc n (map getLHS pdef) cs_full

9981000 -- missing <- genMissing n scargs sc

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

10001002 let clhs = map getLHS pdef

@@ -1352,16 +1354,19 @@ propagateParams ps t (PRef fc n)

13521354 = PApp fc (PRef fc n) (map (\x -> pimp x (PRef fc x) True) ps)

13531355propagateParams ps t x = x

13541356

1357+-- Return the elaborated LHS/RHS, and the original LHS with implicits added

13551358elabClause :: ElabInfo -> FnOpts -> (Int, PClause) ->

1356− Idris (Either Term (Term, Term))

1359+ Idris (Either Term (Term, Term), PTerm)

13571360elabClause info opts (_, PClause fc fname lhs_in [] PImpossible [])

13581361 = do let tcgen = Dictionary `elem` opts

1362+ i <- get

1363+ let lhs = addImpl i lhs_in

13591364 b <- checkPossible info fc tcgen fname lhs_in

13601365 case b of

13611366 True -> tclift $ tfail (At fc

13621367 (Msg $ show lhs_in ++ " is a valid case"))

13631368 False -> do ptm <- mkPatTm lhs_in

1364− return (Left ptm)

1369+ return (Left ptm, lhs)

13651370elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

13661371 = do let tcgen = Dictionary `elem` opts

13671372 ctxt <- getContext

@@ -1502,7 +1507,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

15021507 when (rev || ErrorReverse `elem` opts) $ do

15031508 addIBC (IBCErrRev (crhs, clhs))

15041509 addErrRev (crhs, clhs)

1505− return $ Right (clhs, crhs)

1510+ return $ (Right (clhs, crhs), lhs)

15061511 where

15071512 mkLHSapp t@(PRef _ _) = trace ("APP " ++ show t) $ PApp fc t []

15081513 mkLHSapp t = t

@@ -1669,7 +1674,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)

16691674 mapM_ (elabCaseBlock info opts) is

16701675 logLvl 5 ("Checked RHS " ++ show rhs')

16711676 (crhs, crhsty) <- recheckC fc [] rhs'

1672− return $ Right (clhs, crhs)

1677+ return $ (Right (clhs, crhs), lhs)

16731678 where

16741679 getImps (Bind n (Pi _) t) = pexp Placeholder : getImps t

16751680 getImps _ = []