@@ -18,10 +18,14 @@ import Debug.Trace
19import Control.Monad.State.Strict
19import Control.Monad.State.Strict
21+-- Generate a pattern from an 'impossible' LHS. (Need this to eliminate the
22+-- pattern clauses which have been provided explicitly from new clause
21mkPatTm :: PTerm -> Idris Term
25mkPatTm :: PTerm -> Idris Term
22mkPatTm t = do i <- getIState
26mkPatTm t = do i <- getIState
23 let timp = addImpl' True [] [] i t
27 let timp = addImpl' True [] [] i t
24− evalStateT (toTT timp) 0
28+ evalStateT (toTT (mapPT deNS timp)) 0
26 toTT (PRef _ n) = do i <- lift getIState
30 toTT (PRef _ n) = do i <- lift getIState
27 case lookupDef n (tt_ctxt i) of
31 case lookupDef n (tt_ctxt i) of
@@ -30,10 +34,16 @@ mkPatTm t = do i <- getIState
30 toTT (PApp _ t args) = do t' <- toTT t
34 toTT (PApp _ t args) = do t' <- toTT t
31 args' <- mapM (toTT . getTm) args
35 args' <- mapM (toTT . getTm) args
32 return $ mkApp t' args'
36 return $ mkApp t' args'
37+ -- For alternatives, pick the first and drop the namespaces. It doesn't
38+ -- really matter which is taken since matching will ignore the namespace.
39+ toTT (PAlternative _ (a : as)) = toTT a
33 toTT _ = do v <- get
40 toTT _ = do v <- get
34 put (v + 1)
41 put (v + 1)
35 return (P Bound (sMN v "imp") Erased)
42 return (P Bound (sMN v "imp") Erased)
44+ deNS (PRef f (NS n _)) = PRef f n
37-- Given a list of LHSs, generate a extra clauses which cover the remaining
47-- Given a list of LHSs, generate a extra clauses which cover the remaining
38-- cases. The ones which haven't been provided are marked 'absurd' so that the
48-- cases. The ones which haven't been provided are marked 'absurd' so that the
39-- checker will make sure they can't happen.
49-- checker will make sure they can't happen.
@@ -50,10 +60,10 @@ genClauses fc n xs given
50 logLvl 5 $ "COVERAGE of " ++ show n
60 logLvl 5 $ "COVERAGE of " ++ show n
51 logLvl 5 $ show (map length argss) ++ "\n" ++ show (map length all_args)
61 logLvl 5 $ show (map length argss) ++ "\n" ++ show (map length all_args)
52 logLvl 10 $ show argss ++ "\n" ++ show all_args
62 logLvl 10 $ show argss ++ "\n" ++ show all_args
53− logLvl 10 $ "Original: \n" ++
63+ logLvl 1 $ "Original: \n" ++
54 showSep "\n" (map (\t -> showTm i (delab' i t True True)) xs)
64 showSep "\n" (map (\t -> showTm i (delab' i t True True)) xs)
55 -- add an infinite supply of explicit arguments to update the possible
65 -- add an infinite supply of explicit arguments to update the possible
56− -- cases for (the return type may be variadic, or function type, sp
66+ -- cases for (the return type may be variadic, or function type, so
57 -- there may be more case splitting that the idris_implicits record
67 -- there may be more case splitting that the idris_implicits record
58 -- suggests)
68 -- suggests)
59 let parg = case lookupCtxt n (idris_implicits i) of
69 let parg = case lookupCtxt n (idris_implicits i) of
@@ -61,10 +71,10 @@ genClauses fc n xs given
61 _ -> repeat (pexp Placeholder)
71 _ -> repeat (pexp Placeholder)
62 let tryclauses = mkClauses parg all_args
72 let tryclauses = mkClauses parg all_args
63 logLvl 2 $ show (length tryclauses) ++ " initially to check"
73 logLvl 2 $ show (length tryclauses) ++ " initially to check"
64− logLvl 5 $ showSep "\n" (map (showTm i) tryclauses)
74+ logLvl 1 $ showSep "\n" (map (showTm i) tryclauses)
65 let new = filter (noMatch i) (nub tryclauses)
75 let new = filter (noMatch i) (nub tryclauses)
66 logLvl 1 $ show (length new) ++ " clauses to check for impossibility"
76 logLvl 1 $ show (length new) ++ " clauses to check for impossibility"
67− logLvl 5 $ "New clauses: \n" ++ showSep "\n" (map (showTm i) new)
77+ logLvl 3 $ "New clauses: \n" ++ showSep "\n" (map (showTm i) new)
68-- ++ " from:\n" ++ showSep "\n" (map (showImp True) tryclauses)
78-- ++ " from:\n" ++ showSep "\n" (map (showImp True) tryclauses)
69 return new
79 return new
70-- return (map (\t -> PClause n t [] PImpossible []) new)
80-- return (map (\t -> PClause n t [] PImpossible []) new)
@@ -75,9 +85,11 @@ genClauses fc n xs given
75 lhsApp (PClause _ _ l _ _ _) = l
85 lhsApp (PClause _ _ l _ _ _) = l
76 lhsApp (PWith _ _ l _ _ _) = l
86 lhsApp (PWith _ _ l _ _ _) = l
88+ -- Return whether the given clause matches none of the input clauses
78 noMatch i tm = all (\x -> case matchClause i (delab' i x True True) tm of
90 noMatch i tm = all (\x -> case matchClause i (delab' i x True True) tm of
79− Right _ -> False
91+ Right ms -> False
80− Left miss -> True) xs
92+ Left miss -> True) xs
83 mkClauses :: [PArg] -> [[PTerm]] -> [PTerm]
95 mkClauses :: [PArg] -> [[PTerm]] -> [PTerm]