git.iko.soy/Idris-dev
on fa0ecde help sign in
Idris-dev/src/Idris/Coverage.hs
264 lines 10 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-- Check if, in a given type n, the constructor cn : ty is strictly positive,
117-- and update the context accordingly
119checkPositive :: Name -> (Name, Type) -> Idris ()
120checkPositive n (cn, ty)
121 = do let p = cp ty
122 i <- getIState
123 let tot = if p then Total (args ty) else Partial NotPositive
124 let ctxt' = setTotal cn tot (tt_ctxt i)
125 putIState (i { tt_ctxt = ctxt' })
126 addIBC (IBCTotal cn tot)
127 where
128 args t = [0..length (getArgTys t)-1]
130 cp (Bind n (Pi aty) sc) = posArg aty && cp sc
131 cp t = True
133 posArg (Bind _ (Pi nty) sc)
134 | (P _ n' _, args) <- unApply nty
135 = n /= n' && posArg sc
136 posArg t = True
138-- Totality checking - check for structural recursion (no mutual definitions yet)
140data LexOrder = LexXX | LexEQ | LexLT
141 deriving (Show, Eq, Ord)
143calcTotality :: [Name] -> FC -> Name -> [([Name], Term, Term)] -> Idris Totality
144calcTotality path fc n pats
145 = do orders <- mapM ctot pats
146 let order = sortBy cmpOrd $ concat orders
147 let (errs, valid) = partitionEithers order
148 let lex = stripNoLT (stripXX valid)
149 case errs of
150 [] -> do logLvl 3 $ show n ++ ":\n" ++ showSep "\n" (map show lex)
151 logLvl 10 $ show pats
152 checkDecreasing lex
153 (e : _) -> return e -- FIXME: should probably combine them
154 where
155 cmpOrd (Left _) (Left _) = EQ
156 cmpOrd (Left _) (Right _) = LT
157 cmpOrd (Right _) (Left _) = GT
158 cmpOrd (Right x) (Right y) = compare x y
160 checkDecreasing [] = return (Total [])
161 checkDecreasing (c : cs) | dec c = checkDecreasing cs
162 | otherwise = return (Partial Itself)
164 dec [] = False
165 dec (LexLT : _) = True
166 dec (LexEQ : xs) = dec xs
167 dec (LexXX : xs) = False
169 stripXX [] = []
170 stripXX v@(c : cs)
171 = case span (==LexXX) c of
172 (ns, rest) -> map (drop (length ns)) v
174 -- argument positions which are never LT are no use to us
175 stripNoLT [] = [] -- no recursive calls
176 stripNoLT xs = case transpose (filter (any (==LexLT)) (transpose xs)) of
177 [] -> [[]] -- recursive calls are all useless...
178 xs -> xs
180 ctot (_, lhs, rhs)
181 | (_, args) <- unApply lhs
182 = do -- check lhs doesn't use any dodgy names
183 lhsOK <- mapM (chkOrd [] []) args
184 chkOrd (filter isLeft (concat lhsOK)) args rhs
186 isLeft (Left _) = True
187 isLeft _ = False
189 chkOrd ords args (Bind n (Let t v) sc)
190 = do ov <- chkOrd ords args v
191 chkOrd ov args sc
192 chkOrd ords args (Bind n b sc) = chkOrd ords (args ++ [P Ref n Erased]) sc
193 chkOrd ords args ap@(App f a)
194 | (P _ fn _, args') <- unApply ap
195 = if fn == n && length args == length args'
196 then do orf <- chkOrd (Right (zipWith lexOrd args args') : ords) args f
197 chkOrd orf args a
198 else do orf <- chkOrd ords args f
199 chkOrd orf args a
200 | otherwise = do orf <- chkOrd ords args f
201 chkOrd orf args a
202 chkOrd ords args (P _ fn _)
203 | n /= fn
204 = do tf <- checkTotality (n : path) fc fn
205 case tf of
206 Total _ -> return ords
207 p@(Partial (Mutual x)) -> return ((Left p) : ords)
208 _ -> return (Left (Partial (Other [fn])) : ords)
209 | null args = return (Left (Partial Itself) : ords)
210 chkOrd ords args _ = return ords
212 lexOrd x y | x == y = LexEQ
213 lexOrd f@(App _ _) x
214 | (f', args) <- unApply f
215 = let ords = map (\x' -> lexOrd x' x) args in
216 if any (\o -> o == LexEQ || o == LexLT) ords
217 then LexLT
218 else LexXX
219 lexOrd _ _ = LexXX
221checkTotality :: [Name] -> FC -> Name -> Idris Totality
222checkTotality path fc n
223 | n `elem` path = return (Partial (Mutual (n : path)))
224 | otherwise = do
225 t <- getTotality n
226 ctxt <- getContext
227 i <- getIState
228 let opts = case lookupCtxt Nothing n (idris_flags i) of
229 [fs] -> fs
230 _ -> []
231 t' <- case t of
232 Unchecked ->
233 case lookupDef Nothing n ctxt of
234 [CaseOp _ _ pats _ _ _ _] ->
235 do t' <- if AssertTotal `elem` opts
236 then return $ Total []
237 else calcTotality path fc n pats
238 setTotality n t'
239 addIBC (IBCTotal n t')
240 -- if it's not total, it can't reduce, to keep
241 -- typechecking decidable
242 case t' of
243-- FIXME: Put this back when we can handle mutually recursive things
244-- p@(Partial _) ->
245-- do setAccessibility n Frozen
246-- addIBC (IBCAccess n Frozen)
247-- iputStrLn $ "HIDDEN: " ++ show n ++ show p
248 _ -> return ()
249 return t'
250 _ -> return $ Total []
251 x -> return x
252 if TotalFn `elem` opts
253 then case t' of
254 Total _ -> return t'
255 e -> totalityError t'
256 else return t'
257 where
258 totalityError t = tclift $ tfail (At fc (Msg (show n ++ " is " ++ show t)))
260checkDeclTotality :: (FC, Name) -> Idris Totality
261checkDeclTotality (fc, n)
262 = do logLvl 2 $ "Checking " ++ show n ++ " for totality"
263 checkTotality [] fc n