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

git.iko.soy/Idris-dev

on master help sign in

Efficiency of coverage check

06e2b1dEdwin Brady13 years ago

src/Idris/Coverage.hs+18−4

compare with master

unifiedsplit

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

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

52-- names are fully explicit!

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

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

55genClauses fc n xs given

56 = 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+

58 let argss = transpose lhss

62 let argss = transpose lhss

59 let all_args = map (genAll i) argss

63 let all_args = map (genAll i) argss

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

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

65+ logLvl 5 $ show lhss

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

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

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

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

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

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

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

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

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

83 | otherwise = []

88 | otherwise = []

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

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

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

91+ pUnApply _ = []

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

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

89 -- (xs)

94 -- (xs)

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

92 Left miss -> True) xs

97 Left miss -> True) xs

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+

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

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

96 mkClauses parg args

109 mkClauses parg args

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

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

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

114

127

115-- quick check for constructor equality

128-- quick check for constructor equality

116quickEq :: PTerm -> PTerm -> Bool

129quickEq :: PTerm -> PTerm -> Bool

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

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

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

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

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

119 | length as == length as'

133 | 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

908 tclift $ tfail $ At fc (NoTypeDecl n)

909 [ty] -> return ty

910 let atys = map snd (getArgTys fty)

911− pats_in <- mapM (elabClause info opts)

911+ cs_elab <- mapM (elabClause info opts)

912 (zip [0..] cs)

913+ let (pats_in, cs_full) = unzip cs_elab

914+

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

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

914

916

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

917 -- 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

994 cov <- coverage

996 cov <- coverage

995 pmissing <-

997 pmissing <-

996 if cov && not (hasDefault cs)

998 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

998 -- missing <- genMissing n scargs sc

1000 -- missing <- genMissing n scargs sc

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

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

1000 let clhs = map getLHS pdef

1002 let clhs = map getLHS pdef

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

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

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

1353propagateParams ps t x = x

1355propagateParams ps t x = x

1354

1356

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

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

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

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

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

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

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

1358 = do let tcgen = Dictionary `elem` opts

1361 = do let tcgen = Dictionary `elem` opts

1362+ i <- get

1363+ let lhs = addImpl i lhs_in

1359 b <- checkPossible info fc tcgen fname lhs_in

1364 b <- checkPossible info fc tcgen fname lhs_in

1360 case b of

1365 case b of

1361 True -> tclift $ tfail (At fc

1366 True -> tclift $ tfail (At fc

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

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

1363 False -> do ptm <- mkPatTm lhs_in

1368 False -> do ptm <- mkPatTm lhs_in

1364− return (Left ptm)

1369+ return (Left ptm, lhs)

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

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

1366 = do let tcgen = Dictionary `elem` opts

1371 = do let tcgen = Dictionary `elem` opts

1367 ctxt <- getContext

1372 ctxt <- getContext

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

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

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

1503 addIBC (IBCErrRev (crhs, clhs))

1508 addIBC (IBCErrRev (crhs, clhs))

1504 addErrRev (crhs, clhs)

1509 addErrRev (crhs, clhs)

1505− return $ Right (clhs, crhs)

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

1506 where

1511 where

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

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

1508 mkLHSapp t = t

1513 mkLHSapp t = t

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

1669 mapM_ (elabCaseBlock info opts) is

1674 mapM_ (elabCaseBlock info opts) is

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

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

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

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

1672− return $ Right (clhs, crhs)

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

1673 where

1678 where

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

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

1675 getImps _ = []

1680 getImps _ = []