700759f · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Cache missing cases found by totality checker, for display

700759fEdwin Brady13 years ago

src/Idris/AbsSyntaxTree.hs+2−1

compare with master

unifiedsplit

@@ -62,7 +62,8 @@ data IState = IState {

62 idris_dsls :: Ctxt DSL,

63 idris_optimisation :: Ctxt OptInfo,

64 idris_datatypes :: Ctxt TypeInfo,

65− idris_patdefs :: Ctxt [([Name], Term, Term)], -- not exported

65+ idris_patdefs :: Ctxt ([([Name], Term, Term)], [PTerm]), -- not exported

66+ -- ^ list of lhs/rhs, and a list of missing clauses

66 idris_flags :: Ctxt [FnOpt],

67 idris_flags :: Ctxt [FnOpt],

67 idris_callgraph :: Ctxt CGInfo, -- name, args used in each pos

68 idris_callgraph :: Ctxt CGInfo, -- name, args used in each pos

68 idris_calledgraph :: Ctxt [Name],

69 idris_calledgraph :: Ctxt [Name],

src/Idris/Coverage.hs−110

@@ -17,21 +17,6 @@ import Debug.Trace

18import Control.Monad.State

20−-- Generate the LHSes which are missing from a case tree

21−-- Eliminate the ones which cannot be well typed

22−

23−genMissing :: Name -> [Name] -> SC -> Idris [PTerm]

24−genMissing fn args sc

25− = do sc' <- expandTree sc

26− logLvl 5 $ "Checking missing cases for " ++

27− show fn ++ "\n" ++ (show sc')

28− (got, missing) <- gm fn (map (\x -> P Bound x Erased) args) sc'

29− return $ filter (\x -> not (x `elem` got)) missing

30−

31−-- Make a term to feed to the pattern matcher from a LHS declared impossible

32−-- (we can't type check it, but we need the case analysis to check for

33−-- covering...)

34−

35mkPatTm :: PTerm -> Idris Term

20mkPatTm :: PTerm -> Idris Term

36mkPatTm t = do i <- getIState

21mkPatTm t = do i <- getIState

37 let timp = addImpl' True [] [] i t

22 let timp = addImpl' True [] [] i t

@@ -48,101 +33,6 @@ mkPatTm t = do i <- getIState

48 put (v + 1)

33 put (v + 1)

49 return (P Bound (MN v "imp") Erased)

34 return (P Bound (MN v "imp") Erased)

51−mkPTerm :: Name -> [TT Name] -> Idris PTerm

52−mkPTerm f args = do i <- getIState

53− let fapp = mkApp (P Bound f Erased) (map eraseName args)

54− return $ delab i fapp

55− where eraseName (App f a) = App (eraseName f) (eraseName a)

56− eraseName (P _ (MN _ _) _) = Erased

57− eraseName t = t

58−

59−gm :: Name -> [TT Name] -> SC -> Idris ([PTerm], [PTerm])

60−gm fn args (Case n alts) = do m <- mapM (gmAlt fn args n) alts

61− let (got, missing) = unzip m

62− return (concat got, concat missing)

63−gm fn args (STerm tm) = do logLvl 3 ("Covered: " ++ show args)

64− t <- mkPTerm fn args

65− return ([t], [])

66−gm fn args ImpossibleCase = do logLvl 3 ("Impossible: " ++ show args)

67− t <- mkPTerm fn args

68− return ([], [])

69−gm fn args (UnmatchedCase _) = do logLvl 3 ("Missing: " ++ show args)

70− t <- mkPTerm fn args

71− return ([], [t])

72−

73−gmAlt fn args n (ConCase cn t cargs sc)

74− = do let args' = map (subst n (mkApp (P Bound cn Erased)

75− (map (\x -> P Bound x Erased) cargs)))

76− args

77− gm fn args' sc

78−gmAlt fn args n (ConstCase c sc)

79− = do let args' = map (subst n (Constant c)) args

80− gm fn args' sc

81−gmAlt fn args n (DefaultCase sc)

82− = do gm fn args sc

83−

84−getDefault (DefaultCase sc : _) = sc

85−getDefault (_ : cs) = getDefault cs

86−getDefault [] = UnmatchedCase ""

87−

88−dropDefault (DefaultCase sc : rest) = dropDefault rest

89−dropDefault (c : cs) = c : dropDefault cs

90−dropDefault [] = []

91−

92−expandTree :: SC -> Idris SC

93−expandTree (Case n alts) = do i <- getIState

94− as <- expandAlts i (dropDefault alts)

95− (getDefault alts)

96− alts' <- mapM expandTreeA as

97− return (Case n alts')

98− where expandTreeA (ConCase n i ns sc) = do sc' <- expandTree sc

99− return (ConCase n i ns sc')

100− expandTreeA (ConstCase i sc) = do sc' <- expandTree sc

101− return (ConstCase i sc')

102− expandTreeA (DefaultCase sc) = do sc' <- expandTree sc

103− return (DefaultCase sc')

104−expandTree t = return t

105−

106−expandAlts :: IState -> [CaseAlt] -> SC -> Idris [CaseAlt]

107−expandAlts i all@(ConstCase c _ : alts) def

108− = return $ all ++ [DefaultCase def]

109−expandAlts i all@(ConCase n _ _ _ : alts) def

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

111− = do let tyn = getTy n (tt_ctxt i)

112− case lookupCtxt tyn (idris_datatypes i) of

113− (TI ns _ _: _) -> do let ps = map mkPat ns

114− return $ addAlts ps (altsFor all) all

115− _ -> return all

116− where

117− altsFor [] = []

118− altsFor (ConCase n _ _ _ : alts) = n : altsFor alts

119− altsFor (_ : alts) = altsFor alts

120−

121− addAlts [] got alts = alts

122− addAlts ((n, arity) : ps) got alts

123− | n `elem` got = addAlts ps got alts

124− | otherwise = addAlts ps got (alts ++

125− [ConCase n (-1) (argList arity) def])

126−

127− argList i = take i (map (\x -> (MN x "ign")) [0..])

128−

129− getTy n ctxt

130− = case lookupTy n ctxt of

131− (t : _) -> case unApply (getRetTy t) of

132− (P _ tyn _, _) -> tyn

133− x -> error $ "Can't happen getTy 1 " ++ show (n, x)

134− _ -> error "Can't happen getTy 2"

135−

136− mkPat x = case lookupCtxt x (idris_implicits i) of

137− (pargs : _)

138− -> (x, length pargs)

139− _ -> error "Can't happen - genAll"

140−expandAlts i alts def = return alts

141−

142−

143−

144−-- OLD STUFF: probably broken...

145−

146-- Given a list of LHSs, generate a extra clauses which cover the remaining

36-- Given a list of LHSs, generate a extra clauses which cover the remaining

147-- cases. The ones which haven't been provided are marked 'absurd' so that the

37-- cases. The ones which haven't been provided are marked 'absurd' so that the

148-- checker will make sure they can't happen.

38-- checker will make sure they can't happen.

src/Idris/ElabDecls.hs+13−2

@@ -443,11 +443,17 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

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

444 -- missing <- genMissing n scargs sc

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

446+ let clhs = map getLHS pdef

446 logLvl 2 $ "Must be unreachable:\n" ++

447 logLvl 2 $ "Must be unreachable:\n" ++

447 showSep "\n" (map (showImp True) missing') ++

448 showSep "\n" (map (showImp True) missing') ++

448 "\nAgainst: " ++

449 "\nAgainst: " ++

449 showSep "\n" (map (\t -> showImp True (delab ist t)) (map getLHS pdef))

450 showSep "\n" (map (\t -> showImp True (delab ist t)) (map getLHS pdef))

451+ -- filter out anything in missing' which is

452+ -- matched by any of clhs. This might happen since

453+ -- unification may force a variable to take a

454+ -- particular form, rather than force a case

455+ -- to be impossible.

450− return missing'

456+ return (filter (noMatch ist clhs) missing')

451 else return []

457 else return []

452 let pcover = null pmissing

458 let pcover = null pmissing

453 logLvl 2 $ "Optimising patterns"

459 logLvl 2 $ "Optimising patterns"

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

480 logLvl 3 $ "Optimised: " ++ show tree'

486 logLvl 3 $ "Optimised: " ++ show tree'

481 ctxt <- getContext

487 ctxt <- getContext

482 ist <- getIState

488 ist <- getIState

483− putIState (ist { idris_patdefs = addDef n pdef' (idris_patdefs ist) })

489+ putIState (ist { idris_patdefs = addDef n (pdef', pmissing)

490+ (idris_patdefs ist) })

484 case lookupTy n ctxt of

491 case lookupTy n ctxt of

485 [ty] -> do updateContext (addCasedef n (inlinable opts)

492 [ty] -> do updateContext (addCasedef n (inlinable opts)

486 tcase knowncovering

493 tcase knowncovering

@@ -508,6 +515,10 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

508 [] -> return ()

515 [] -> return ()

509 return ()

516 return ()

510 where

517 where

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

519+ Right _ -> False

520+ Left miss -> True) cs

521+

511 checkUndefined n ctxt = case lookupDef n ctxt of

522 checkUndefined n ctxt = case lookupDef n ctxt of

512 [] -> return ()

523 [] -> return ()

513 [TyDecl _ _] -> return ()

524 [TyDecl _ _] -> return ()

src/Idris/REPL.hs+9−9

@@ -240,8 +240,8 @@ process fn (Defn n) = do i <- getIState

240 liftIO $ print (lookupDef n (tt_ctxt i))

241 case lookupCtxt n (idris_patdefs i) of

242 [] -> return ()

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

243+ [(d, _)] -> do iputStrLn "Original definiton:\n"

244− mapM_ (printCase i) d

244+ mapM_ (printCase i) d

245 case lookupTotal n (tt_ctxt i) of

246 [t] -> iputStrLn (showTotal t i)

247 _ -> return ()

@@ -389,13 +389,13 @@ process fn (Pattelab t)

389 = do (tm, ty) <- elabVal toplevel True t

390 iputStrLn $ show tm ++ "\n\n : " ++ show ty

391

392−process fn (Missing n) = do i <- getIState

392+process fn (Missing n)

393− case lookupDef n (tt_ctxt i) of

393+ = do i <- getIState

394− [CaseOp _ _ _ _ _ args t _ _]

394+ case lookupCtxt n (idris_patdefs i) of

395− -> do tms <- genMissing n args t

395+ [] -> return ()

396+ [(_, tms)] ->

396− iputStrLn (showSep "\n" (map (showImp True) tms))

397+ iputStrLn (showSep "\n" (map (showImp True) tms))

397− [] -> iputStrLn $ show n ++ " undefined"

398− _ -> iputStrLn $ "Ambiguous name"

398+ _ -> iputStrLn $ "Ambiguous name"

399process fn (DynamicLink l) = do i <- getIState

400 let lib = trim l

401 handle <- lift $ tryLoadLib lib