git.iko.soy/Idris-dev
on adbe613 help sign in
Idris-dev/src/Idris/Coverage.hs
386 lines 16 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
17import Control.Monad.State
19-- Generate the LHSes which are missing from a case tree
20-- Eliminate the ones which cannot be well typed
22genMissing :: Name -> [Name] -> SC -> Idris [PTerm]
23genMissing fn args sc
24 = do sc' <- expandTree sc
25 logLvl 5 $ "Checking missing cases for " ++ show fn ++ "\n" ++ (show sc')
26 (got, missing) <- gm fn (map (\x -> P Bound x Erased) args) sc'
27 return $ filter (\x -> not (x `elem` got)) missing
29-- Make a term to feed to the pattern matcher from a LHS declared impossible
30-- (we can't type check it, but we need the case analysis to check for covering...)
32mkPatTm :: PTerm -> Idris Term
33mkPatTm t = do i <- get
34 let timp = addImpl' True [] i t
35 evalStateT (toTT timp) 0
36 where
37 toTT (PRef _ n) = do i <- lift $ get
38 case lookupDef Nothing n (tt_ctxt i) of
39 [TyDecl nt _] -> return $ P nt n Erased
40 _ -> return $ P Ref n Erased
41 toTT (PApp _ t args) = do t' <- toTT t
42 args' <- mapM (toTT . getTm) args
43 return $ mkApp t' args'
44 toTT _ = do v <- get
45 put (v + 1)
46 return (P Bound (MN v "imp") Erased)
48mkPTerm :: Name -> [TT Name] -> Idris PTerm
49mkPTerm f args = do i <- get
50 let fapp = mkApp (P Bound f Erased) (map eraseName args)
51 return $ delab i fapp
52 where eraseName (App f a) = App (eraseName f) (eraseName a)
53 eraseName (P _ (MN _ _) _) = Erased
54 eraseName t = t
56gm :: Name -> [TT Name] -> SC -> Idris ([PTerm], [PTerm])
57gm fn args (Case n alts) = do m <- mapM (gmAlt fn args n) alts
58 let (got, missing) = unzip m
59 return (concat got, concat missing)
60gm fn args (STerm tm) = do logLvl 3 ("Covered: " ++ show args)
61 t <- mkPTerm fn args
62 return ([t], [])
63gm fn args ImpossibleCase = do logLvl 3 ("Impossible: " ++ show args)
64 t <- mkPTerm fn args
65 return ([], [])
66gm fn args (UnmatchedCase _) = do logLvl 3 ("Missing: " ++ show args)
67 t <- mkPTerm fn args
68 return ([], [t])
70gmAlt fn args n (ConCase cn t cargs sc)
71 = do let args' = map (subst n (mkApp (P Bound cn Erased)
72 (map (\x -> P Bound x Erased) cargs))) args
73 gm fn args' sc
74gmAlt fn args n (ConstCase c sc)
75 = do let args' = map (subst n (Constant c)) args
76 gm fn args' sc
77gmAlt fn args n (DefaultCase sc)
78 = do gm fn args sc
80getDefault (DefaultCase sc : _) = sc
81getDefault (_ : cs) = getDefault cs
82getDefault [] = UnmatchedCase ""
84dropDefault (DefaultCase sc : rest) = dropDefault rest
85dropDefault (c : cs) = c : dropDefault cs
86dropDefault [] = []
88expandTree :: SC -> Idris SC
89expandTree (Case n alts) = do i <- get
90 as <- expandAlts i (dropDefault alts) (getDefault alts)
91 alts' <- mapM expandTreeA as
92 return (Case n alts')
93 where expandTreeA (ConCase n i ns sc) = do sc' <- expandTree sc
94 return (ConCase n i ns sc')
95 expandTreeA (ConstCase i sc) = do sc' <- expandTree sc
96 return (ConstCase i sc')
97 expandTreeA (DefaultCase sc) = do sc' <- expandTree sc
98 return (DefaultCase sc')
99expandTree t = return t
101expandAlts :: IState -> [CaseAlt] -> SC -> Idris [CaseAlt]
102expandAlts i all@(ConstCase c _ : alts) def
103 = return $ all ++ [DefaultCase def]
104expandAlts i all@(ConCase n _ _ _ : alts) def
105 | (TyDecl c@(DCon _ arity) ty : _) <- lookupDef Nothing n (tt_ctxt i)
106 = do let tyn = getTy n (tt_ctxt i)
107 case lookupCtxt Nothing tyn (idris_datatypes i) of
108 (TI ns : _) -> do let ps = map mkPat ns
109 return $ addAlts ps (altsFor all) all
110 _ -> return all
111 where
112 altsFor [] = []
113 altsFor (ConCase n _ _ _ : alts) = n : altsFor alts
114 altsFor (_ : alts) = altsFor alts
116 addAlts [] got alts = alts
117 addAlts ((n, arity) : ps) got alts
118 | n `elem` got = addAlts ps got alts
119 | otherwise = addAlts ps got (alts ++ [ConCase n (-1) (argList arity) def])
121 argList i = take i (map (\x -> (MN x "ign")) [0..])
123 getTy n ctxt = case lookupTy Nothing n ctxt of
124 (t : _) -> case unApply (getRetTy t) of
125 (P _ tyn _, _) -> tyn
126 x -> error $ "Can't happen getTy 1 " ++ show (n, x)
127 _ -> error "Can't happen getTy 2"
129 mkPat x = case lookupCtxt Nothing x (idris_implicits i) of
130 (pargs : _)
131 -> (x, length pargs)
132 _ -> error "Can't happen - genAll"
133expandAlts i alts def = return alts
137-- OLD STUFF: probably broken...
139-- Given a list of LHSs, generate a extra clauses which cover the remaining
140-- cases. The ones which haven't been provided are marked 'absurd' so that the
141-- checker will make sure they can't happen.
143-- This will only work after the given clauses have been typechecked and the
144-- names are fully explicit!
146genClauses :: FC -> Name -> [Term] -> [PClause] -> Idris [PTerm]
147genClauses fc n xs given
148 = do i <- getIState
149 let lhss = map (getLHS i) xs
150 let argss = transpose lhss
151 let all_args = map (genAll i) argss
152 logLvl 7 $ "COVERAGE of " ++ show n
153 logLvl 10 $ show argss ++ "\n" ++ show all_args
154 logLvl 10 $ "Original: \n" ++
155 showSep "\n" (map (\t -> showImp True (delab' i t True)) xs)
156 let parg = case lookupCtxt Nothing n (idris_implicits i) of
157 (p : _) -> p
158 _ -> repeat (pexp Placeholder)
159 let tryclauses = mkClauses parg all_args
160 let new = mnub i $ filter (noMatch i) tryclauses
161 logLvl 7 $ "New clauses: \n" ++ showSep "\n" (map (showImp True) new)
162-- ++ " from:\n" ++ showSep "\n" (map (showImp True) tryclauses)
163 return new
164-- return (map (\t -> PClause n t [] PImpossible []) new)
165 where getLHS i term
166 | (f, args) <- unApply term = map (\t -> delab' i t True) args
167 | otherwise = []
169 lhsApp (PClause _ _ l _ _ _) = l
170 lhsApp (PWith _ _ l _ _ _) = l
172 mnub i [] = []
173 mnub i (x : xs) =
174 if (any (\t -> case matchClause i x t of
175 Right _ -> True
176 Left _ -> False) xs) then mnub i xs
177 else x : mnub i xs
179 noMatch i tm = all (\x -> case matchClause i (delab' i x True) tm of
180 Right _ -> False
181 Left miss -> True) xs
184 mkClauses :: [PArg] -> [[PTerm]] -> [PTerm]
185 mkClauses parg args
186 | all (== [Placeholder]) args = []
187 mkClauses parg args
188 = do args' <- mkArg args
189 let tm = PApp fc (PRef fc n) (zipWith upd args' parg)
190 return tm
191 where
192 mkArg :: [[PTerm]] -> [[PTerm]]
193 mkArg [] = return []
194 mkArg (a : as) = do a' <- a
195 as' <- mkArg as
196 return (a':as')
198-- FIXME: Just look for which one is the deepest, then generate all possibilities
199-- up to that depth.
201genAll :: IState -> [PTerm] -> [PTerm]
202genAll i args = case filter (/=Placeholder) $ concatMap otherPats (nub args) of
203 [] -> [Placeholder]
204 xs -> xs
205 where
206 conForm (PApp _ (PRef fc n) _) = isConName Nothing n (tt_ctxt i)
207 conForm (PRef fc n) = isConName Nothing n (tt_ctxt i)
208 conForm _ = False
210 otherPats :: PTerm -> [PTerm]
211 otherPats o@(PRef fc n) = ops fc n [] o
212 otherPats o@(PApp _ (PRef fc n) xs) = ops fc n xs o
213 otherPats arg = return Placeholder
215 ops fc n xs o
216 | (TyDecl c@(DCon _ arity) ty : _) <- lookupDef Nothing n (tt_ctxt i)
217 = do xs' <- mapM otherPats (map getTm xs)
218 let p = PApp fc (PRef fc n) (zipWith upd xs' xs)
219 let tyn = getTy n (tt_ctxt i)
220 case lookupCtxt Nothing tyn (idris_datatypes i) of
221 (TI ns : _) -> p : map (mkPat fc) (ns \\ [n])
222 _ -> [p]
223 ops fc n arg o = return Placeholder
225 getTy n ctxt = case lookupTy Nothing n ctxt of
226 (t : _) -> case unApply (getRetTy t) of
227 (P _ tyn _, _) -> tyn
228 x -> error $ "Can't happen getTy 1 " ++ show (n, x)
229 _ -> error "Can't happen getTy 2"
231 mkPat fc x = case lookupCtxt Nothing x (idris_implicits i) of
232 (pargs : _)
233 -> PApp fc (PRef fc x) (map (upd Placeholder) pargs)
234 _ -> error "Can't happen - genAll"
236upd p' p = p { getTm = p' }
238-- Check if, in a given type n, the constructor cn : ty is strictly positive,
239-- and update the context accordingly
241checkPositive :: Name -> (Name, Type) -> Idris ()
242checkPositive n (cn, ty)
243 = do let p = cp ty
244 i <- getIState
245 let tot = if p then Total (args ty) else Partial NotPositive
246 let ctxt' = setTotal cn tot (tt_ctxt i)
247 putIState (i { tt_ctxt = ctxt' })
248 addIBC (IBCTotal cn tot)
249 where
250 args t = [0..length (getArgTys t)-1]
252 cp (Bind n (Pi aty) sc) = posArg aty && cp sc
253 cp t = True
255 posArg (Bind _ (Pi nty) sc)
256 | (P _ n' _, args) <- unApply nty
257 = n /= n' && posArg sc
258 posArg t = True
260-- Totality checking - check for structural recursion (no mutual definitions yet)
262data LexOrder = LexXX | LexEQ | LexLT
263 deriving (Show, Eq, Ord)
265calcTotality :: [Name] -> FC -> Name -> [([Name], Term, Term)] -> Idris Totality
266calcTotality path fc n pats
267 = do orders <- mapM ctot pats
268 let order = sortBy cmpOrd $ concat orders
269 let (errs, valid) = partitionEithers order
270 let lex = stripNoLT (stripXX valid)
271 case errs of
272 [] -> do logLvl 3 $ show n ++ ":\n" ++ showSep "\n" (map show lex)
273 logLvl 10 $ show pats
274 checkDecreasing lex
275 (e : _) -> return e -- FIXME: should probably combine them
276 where
277 cmpOrd (Left _) (Left _) = EQ
278 cmpOrd (Left _) (Right _) = LT
279 cmpOrd (Right _) (Left _) = GT
280 cmpOrd (Right x) (Right y) = compare x y
282 checkDecreasing [] = return (Total [])
283 checkDecreasing (c : cs) | dec c = checkDecreasing cs
284 | otherwise = return (Partial Itself)
286 dec [] = False
287 dec (LexLT : _) = True
288 dec (LexEQ : xs) = dec xs
289 dec (LexXX : xs) = False
291 stripXX [] = []
292 stripXX v@(c : cs)
293 = case span (==LexXX) c of
294 (ns, rest) -> map (drop (length ns)) v
296 -- argument positions which are never LT are no use to us
297 stripNoLT [] = [] -- no recursive calls
298 stripNoLT xs = case transpose (filter (any (==LexLT)) (transpose xs)) of
299 [] -> [[]] -- recursive calls are all useless...
300 xs -> xs
302 ctot (_, lhs, rhs)
303 | (_, args) <- unApply lhs
304 = do -- check lhs doesn't use any dodgy names
305 lhsOK <- mapM (chkOrd [] []) args
306 chkOrd (filter isLeft (concat lhsOK)) args rhs
308 isLeft (Left _) = True
309 isLeft _ = False
311 chkOrd ords args (Bind n (Let t v) sc)
312 = do ov <- chkOrd ords args v
313 chkOrd ov args sc
314 chkOrd ords args (Bind n b sc) = chkOrd ords (args ++ [P Ref n Erased]) sc
315 chkOrd ords args ap@(App f a)
316 | (P _ fn _, args') <- unApply ap
317 = if fn == n && length args == length args'
318 then do orf <- chkOrd (Right (zipWith lexOrd args args') : ords) args f
319 chkOrd orf args a
320 else do orf <- chkOrd ords args f
321 chkOrd orf args a
322 | otherwise = do orf <- chkOrd ords args f
323 chkOrd orf args a
324 chkOrd ords args (P _ fn _)
325 | n /= fn
326 = do tf <- checkTotality (n : path) fc fn
327 case tf of
328 Total _ -> return ords
329 p@(Partial (Mutual x)) -> return ((Left p) : ords)
330 _ -> return (Left (Partial (Other [fn])) : ords)
331 | null args = return (Left (Partial Itself) : ords)
332 chkOrd ords args _ = return ords
334 lexOrd x y | x == y = LexEQ
335 lexOrd f@(App _ _) x
336 | (f', args) <- unApply f
337 = let ords = map (\x' -> lexOrd x' x) args in
338 if any (\o -> o == LexEQ || o == LexLT) ords
339 then LexLT
340 else LexXX
341 lexOrd _ _ = LexXX
343checkTotality :: [Name] -> FC -> Name -> Idris Totality
344checkTotality path fc n
345 | n `elem` path = return (Partial (Mutual (n : path)))
346 | otherwise = do
347 t <- getTotality n
348 ctxt <- getContext
349 i <- getIState
350 let opts = case lookupCtxt Nothing n (idris_flags i) of
351 [fs] -> fs
352 _ -> []
353 t' <- case t of
354 Unchecked ->
355 case lookupDef Nothing n ctxt of
356 [CaseOp _ _ pats _ _ _ _] ->
357 do t' <- if AssertTotal `elem` opts
358 then return $ Total []
359 else calcTotality path fc n pats
360 setTotality n t'
361 addIBC (IBCTotal n t')
362 -- if it's not total, it can't reduce, to keep
363 -- typechecking decidable
364 case t' of
365-- FIXME: Put this back when we can handle mutually recursive things
366-- p@(Partial _) ->
367-- do setAccessibility n Frozen
368-- addIBC (IBCAccess n Frozen)
369-- iputStrLn $ "HIDDEN: " ++ show n ++ show p
370 _ -> return ()
371 return t'
372 _ -> return $ Total []
373 x -> return x
374 if TotalFn `elem` opts
375 then case t' of
376 Total _ -> return t'
377 e -> totalityError t'
378 else return t'
379 where
380 totalityError t = tclift $ tfail (At fc (Msg (show n ++ " is " ++ show t)))
382checkDeclTotality :: (FC, Name) -> Idris Totality
383checkDeclTotality (fc, n)
384 = do logLvl 2 $ "Checking " ++ show n ++ " for totality"
385 checkTotality [] fc n