git.iko.soy/Idris-dev
on dcba960 help sign in
Idris-dev/src/Idris/Coverage.hs
317 lines 13 kB history raw
1{-# LANGUAGE PatternGuards #-}
3module Idris.Coverage where
5import Core.TT
6import Core.Evaluate
7import Core.CaseTree
9import Idris.AbsSyntax
10import Idris.Delaborate
11import Idris.Error
13import Data.List
14import Data.Either
15import Debug.Trace
17-- Given a list of LHSs, generate a extra clauses which cover the remaining
18-- cases. The ones which haven't been provided are marked 'absurd' so that the
19-- checker will make sure they can't happen.
21-- This will only work after the given clauses have been typechecked and the
22-- names are fully explicit!
24genClauses :: FC -> Name -> [Term] -> [PClause] -> Idris [PTerm]
25genClauses fc n xs given
26 = do i <- getIState
27 let lhss = map (getLHS i) xs
28 let argss = transpose lhss
29 let all_args = map (genAll i) argss
30 logLvl 7 $ "COVERAGE of " ++ show n
31 logLvl 10 $ show argss ++ "\n" ++ show all_args
32 logLvl 10 $ "Original: \n" ++
33 showSep "\n" (map (\t -> showImp True (delab' i t True)) xs)
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
38 let new = mnub i $ filter (noMatch i) tryclauses
39 logLvl 7 $ "New clauses: \n" ++ showSep "\n" (map (showImp True) new)
40-- ++ " from:\n" ++ showSep "\n" (map (showImp True) tryclauses)
41 return new
42-- return (map (\t -> PClause n t [] PImpossible []) new)
43 where getLHS i term
44 | (f, args) <- unApply term = map (\t -> delab' i t True) args
45 | otherwise = []
47 lhsApp (PClause _ _ l _ _ _) = l
48 lhsApp (PWith _ _ l _ _ _) = l
50 mnub i [] = []
51 mnub i (x : xs) =
52 if (any (\t -> case matchClause i x t of
53 Right _ -> True
54 Left _ -> False) xs) then mnub i xs
55 else x : mnub i xs
57 noMatch i tm = all (\x -> case matchClause i (delab' i x True) tm of
58 Right _ -> False
59 Left miss -> True) xs
62 mkClauses :: [PArg] -> [[PTerm]] -> [PTerm]
63 mkClauses parg args
64 | all (== [Placeholder]) args = []
65 mkClauses parg args
66 = do args' <- mkArg args
67 let tm = PApp fc (PRef fc n) (zipWith upd args' parg)
68 return tm
69 where
70 mkArg :: [[PTerm]] -> [[PTerm]]
71 mkArg [] = return []
72 mkArg (a : as) = do a' <- a
73 as' <- mkArg as
74 return (a':as')
76-- FIXME: Just look for which one is the deepest, then generate all possibilities
77-- up to that depth.
79genAll :: IState -> [PTerm] -> [PTerm]
80genAll i args = case filter (/=Placeholder) $ concatMap otherPats (nub args) of
81 [] -> [Placeholder]
82 xs -> xs
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
88 otherPats :: PTerm -> [PTerm]
89 otherPats o@(PRef fc n) = ops fc n [] o
90 otherPats o@(PApp _ (PRef fc n) xs) = ops fc n xs o
91 otherPats arg = return Placeholder
93 ops fc n xs o
94 | (TyDecl c@(DCon _ arity) ty : _) <- lookupDef Nothing n (tt_ctxt i)
95 = do xs' <- mapM otherPats (map getTm xs)
96 let p = PApp fc (PRef fc n) (zipWith upd xs' xs)
97 let tyn = getTy n (tt_ctxt i)
98 case lookupCtxt Nothing tyn (idris_datatypes i) of
99 (TI ns : _) -> p : map (mkPat fc) (ns \\ [n])
100 _ -> [p]
101 ops fc n arg o = return Placeholder
103 getTy n ctxt = case lookupTy Nothing n ctxt of
104 (t : _) -> case unApply (getRetTy t) of
105 (P _ tyn _, _) -> tyn
106 x -> error $ "Can't happen getTy 1 " ++ show (n, x)
107 _ -> error "Can't happen getTy 2"
109 mkPat fc x = case lookupCtxt Nothing x (idris_implicits i) of
110 (pargs : _)
111 -> PApp fc (PRef fc x) (map (upd Placeholder) pargs)
112 _ -> error "Can't happen - genAll"
114upd p' p = p { getTm = p' }
116-- recursive calls are well-founded if one of their argument positions is
117-- always decreasing. Return a list of arguments which are either not used
118-- recursively, or always decreasing recursively
120-- If we encounter a non-total name, we'll fail
122wellFounded :: IState -> Name -> SC -> Totality
123wellFounded i n sc = case wff [] sc of
124 RightOK smaller_args ->
125 -- is there a number in every list?
126 -- trace (show (n, smaller_args)) $
127 case smaller_args of
128 [] -> Total []
129 (x : xs) -> let args = foldl intersect x xs in
130 if (null args) then Partial Itself
131 else Total args
132 LeftErr x -> Partial (Other x)
133 where
134 wff :: [Name] -> SC -> EitherErr [Name] [[Int]]
135 wff ns (Case n as) = do is <- mapM (wffC ns) as
136 return $ concat is
137 where wffC ns (ConCase n i ns' sc) = do checkOK n
138 wff (ns ++ ns') sc
139 wffC ns (ConstCase _ sc) = wff ns sc
140 wffC ns (DefaultCase sc) = wff ns sc
141 wff ns (STerm t) = argPos ns t
142 wff ns _ = return []
144 checkOK n' = case lookupTotal n' (tt_ctxt i) of
145 [Partial _] -> LeftErr [n']
146 [Total _] -> RightOK ()
147 x -> RightOK ()
149 argPos ns ap@(App f' a')
150 | (P _ f _, args) <- unApply ap
151 = if f == n then
152 do aa <- argPos ns a'
153 return $ chkArgs 0 ns args : aa
154 else do checkOK f
155 argPos ns a'
156 argPos ns (App f a) = do f' <- argPos ns f
157 a' <- argPos ns a
158 return (f' ++ a')
159 argPos ns (Bind n (Let t v) sc) = do v' <- argPos ns v
160 sc' <- argPos ns sc
161 return (v' ++ sc')
162 argPos ns (Bind n _ sc) = argPos ns sc
163 argPos ns _ = return []
165 chkArgs i ns [] = []
166 chkArgs i ns (P _ n _ : xs) | n `elem` ns = i : chkArgs (i + 1) ns xs
167 chkArgs i ns (_ : xs) = chkArgs (i+1) ns xs
169-- Check if, in a given type n, the constructor cn : ty is strictly positive,
170-- and update the context accordingly
172checkPositive :: Name -> (Name, Type) -> Idris ()
173checkPositive n (cn, ty)
174 = do let p = cp ty
175 i <- getIState
176 let tot = if p then Total (args ty) else Partial NotPositive
177 let ctxt' = setTotal cn tot (tt_ctxt i)
178 putIState (i { tt_ctxt = ctxt' })
179 addIBC (IBCTotal cn tot)
180 where
181 args t = [0..length (getArgTys t)-1]
183 cp (Bind n (Pi aty) sc) = posArg aty && cp sc
184 cp t = True
186 posArg (Bind _ (Pi nty) sc)
187 | (P _ n' _, args) <- unApply nty
188 = n /= n' && posArg sc
189 posArg t = True
191-- Totality checking - check for structural recursion (no mutual definitions yet)
193data LexOrder = LexXX | LexEQ | LexLT
194 deriving (Show, Eq, Ord)
196calcTotality :: [Name] -> FC -> Name -> [(Term, Term)] -> Idris Totality
197calcTotality path fc n pats
198 = do orders <- mapM ctot pats
199 let order = sortBy cmpOrd $ concat orders
200 let (errs, valid) = partitionEithers order
201 let lex = stripNoLT (stripXX valid)
202 case errs of
203 [] -> do logLvl 3 $ show n ++ ":\n" ++ showSep "\n" (map show lex)
204 logLvl 10 $ show pats
205 checkDecreasing lex
206 (e : _) -> return e -- FIXME: should probably combine them
207 where
208 cmpOrd (Left _) (Left _) = EQ
209 cmpOrd (Left _) (Right _) = LT
210 cmpOrd (Right _) (Left _) = GT
211 cmpOrd (Right x) (Right y) = compare x y
213 checkDecreasing [] = return (Total [])
214 checkDecreasing (c : cs) | dec c = checkDecreasing cs
215 | otherwise = return (Partial Itself)
217 dec [] = False
218 dec (LexLT : _) = True
219 dec (LexEQ : xs) = dec xs
220 dec (LexXX : xs) = False
222 stripXX [] = []
223 stripXX v@(c : cs)
224 = case span (==LexXX) c of
225 (ns, rest) -> map (drop (length ns)) v
227 -- argument positions which are never LT are no use to us
228 stripNoLT [] = [] -- no recursive calls
229 stripNoLT xs = case transpose (filter (any (==LexLT)) (transpose xs)) of
230 [] -> [[]] -- recursive calls are all useless...
231 xs -> xs
233 ctot (lhs, rhs)
234 | (_, args) <- unApply lhs
235 = do -- check lhs doesn't use any dodgy names
236 lhsOK <- mapM (chkOrd [] []) args
237 chkOrd (filter isLeft (concat lhsOK)) args rhs
239 isLeft (Left _) = True
240 isLeft _ = False
242 chkOrd ords args (Bind n (Let t v) sc)
243 = do ov <- chkOrd ords args v
244 chkOrd ov args sc
245 chkOrd ords args (Bind n b sc) = chkOrd ords (args ++ [P Ref n Erased]) sc
246 chkOrd ords args ap@(App f a)
247 | (P _ fn _, args') <- unApply ap
248 = if fn == n && length args == length args'
249 then do orf <- chkOrd (Right (zipWith lexOrd args args') : ords) args f
250 chkOrd orf args a
251 else do orf <- chkOrd ords args f
252 chkOrd orf args a
253 | otherwise = do orf <- chkOrd ords args f
254 chkOrd orf args a
255 chkOrd ords args (P _ fn _)
256 | n /= fn
257 = do tf <- checkTotality (n : path) fc fn
258 case tf of
259 Total _ -> return ords
260 p@(Partial (Mutual x)) -> return ((Left p) : ords)
261 _ -> return (Left (Partial (Other [fn])) : ords)
262 | null args = return (Left (Partial Itself) : ords)
263 chkOrd ords args _ = return ords
265 lexOrd x y | x == y = LexEQ
266 lexOrd f@(App _ _) x
267 | (f', args) <- unApply f
268 = let ords = map (\x' -> lexOrd x' x) args in
269 if any (\o -> o == LexEQ || o == LexLT) ords
270 then LexLT
271 else LexXX
272 lexOrd _ _ = LexXX
274checkTotality :: [Name] -> FC -> Name -> Idris Totality
275checkTotality path fc n
276 | n `elem` path = return (Partial (Mutual (n : path)))
277 | otherwise = do
278 t <- getTotality n
279 ctxt <- getContext
280 i <- getIState
281 let opts = case lookupCtxt Nothing n (idris_flags i) of
282 [fs] -> fs
283 [] -> []
284 t' <- case t of
285 Unchecked ->
286 case lookupDef Nothing n ctxt of
287 [CaseOp _ _ pats _ _ _ _] ->
288 do t' <- if AssertTotal `elem` opts
289 then return $ Total []
290 else calcTotality path fc n pats
291 setTotality n t'
292 addIBC (IBCTotal n t')
293 -- if it's not total, it can't reduce, to keep
294 -- typechecking decidable
295 case t' of
296-- FIXME: Put this back when we can handle mutually recursive things
297-- p@(Partial _) ->
298-- do setAccessibility n Frozen
299-- addIBC (IBCAccess n Frozen)
300-- iputStrLn $ "HIDDEN: " ++ show n ++ show p
301 _ -> return ()
302 return t'
303 _ -> return $ Total []
304 x -> return x
305 if TotalFn `elem` opts
306 then case t' of
307 Total _ -> return t'
308 e -> totalityError t'
309 else return t'
310 where
311 totalityError t = tclift $ tfail (At fc (Msg (show n ++ " is " ++ show t)))
313checkDeclTotality :: (FC, Name) -> Idris Totality
314checkDeclTotality (fc, n)
315 = do logLvl 2 $ "Checking " ++ show n ++ " for totality"
316 checkTotality [] fc n