git.iko.soy/Idris-dev
on fb3160e help sign in
Idris-dev/src/Idris/Coverage.hs
97 lines 3.8 kB history raw
1{-# LANGUAGE PatternGuards #-}
3module Idris.Coverage where
5import Core.TT
6import Core.Evaluate
7import Idris.AbsSyntax
8import Idris.Delaborate
10import Data.List
11import Debug.Trace
13-- Given a list of LHSs, generate a extra clauses which cover the remaining
14-- cases. The ones which haven't been provided are marked 'absurd' so that the
15-- checker will make sure they can't happen.
17-- This will only work after the given clauses have been typechecked and the
18-- names are fully explicit!
20genClauses :: FC -> Name -> [Term] -> [PClause] -> Idris [PClause]
21genClauses fc n xs given
22 = do i <- getIState
23 let lhss = map (getLHS i) xs
24 let argss = transpose lhss
25 let all_args = map (genAll i) argss
26 logLvl 7 $ "COVERAGE of " ++ show n
27 logLvl 10 $ show argss ++ "\n" ++ show all_args
28 logLvl 10 $ "Original: \n" ++
29 showSep "\n" (map (\t -> showImp True (delab' i t True)) xs)
30 let parg = case lookupCtxt Nothing n (idris_implicits i) of
31 (p : _) -> p
32 _ -> repeat (pexp Placeholder)
33 let new = mnub i $ filter (noMatch i) $ mkClauses parg all_args
34 logLvl 7 $ "New clauses: \n" ++ showSep "\n" (map (showImp True) new)
35 return (map (\t -> PClause n t [] PImpossible []) new)
36 where getLHS i term
37 | (f, args) <- unApply term = map (\t -> delab' i t True) args
38 | otherwise = []
40 lhsApp (PClause _ l _ _ _) = l
41 lhsApp (PWith _ l _ _ _) = l
43 mnub i [] = []
44 mnub i (x : xs) =
45 if (any (\t -> case matchClause x t of
46 Right _ -> True
47 Left _ -> False) xs) then mnub i xs
48 else x : mnub i xs
50 noMatch i tm = all (\x -> case matchClause (delab' i x True) tm of
51 Right _ -> False
52 Left miss -> True) xs
55 mkClauses :: [PArg] -> [[PTerm]] -> [PTerm]
56 mkClauses parg args
57 = do args' <- mkArg args
58 let tm = PApp fc (PRef fc n) (zipWith upd args' parg)
59 return tm
60 where
61 mkArg :: [[PTerm]] -> [[PTerm]]
62 mkArg [] = return []
63 mkArg (a : as) = do a' <- a
64 as' <- mkArg as
65 return (a':as')
67genAll :: IState -> [PTerm] -> [PTerm]
68genAll i args = concatMap otherPats (nub args)
69 where
70 otherPats :: PTerm -> [PTerm]
71 otherPats o@(PRef fc n) = ops fc n [] o
72 otherPats o@(PApp _ (PRef fc n) xs) = ops fc n xs o
73 otherPats arg = return arg
75 ops fc n xs o
76 | (TyDecl c@(DCon _ arity) ty : _) <- lookupDef Nothing n (tt_ctxt i)
77 = do xs' <- mapM otherPats (map getTm xs)
78 let p = PApp fc (PRef fc n) (zipWith upd xs' xs)
79 let tyn = getTy n (tt_ctxt i)
80 case lookupCtxt Nothing tyn (idris_datatypes i) of
81 (TI ns : _) -> p : map (mkPat fc) (ns \\ [n])
82 _ -> [p]
83 ops fc n arg o = return o
85 getTy n ctxt = case lookupTy Nothing n ctxt of
86 (t : _) -> case unApply (getRetTy t) of
87 (P _ tyn _, _) -> tyn
88 x -> error $ "Can't happen getTy 1 " ++ show (n, x)
89 _ -> error "Can't happen getTy 2"
91 mkPat fc x = case lookupCtxt Nothing x (idris_implicits i) of
92 (pargs : _)
93 -> PApp fc (PRef fc x) (map (upd Placeholder) pargs)
94 _ -> error "Can't happen - genAll"
96upd p' p = p { getTm = p' }