@@ -18,10 +18,14 @@ import Debug.Trace
1818
1919import Control.Monad.State.Strict
2020
21+-- Generate a pattern from an 'impossible' LHS. (Need this to eliminate the
22+-- pattern clauses which have been provided explicitly from new clause
23+-- generation.)
24+
2125mkPatTm :: PTerm -> Idris Term
2226mkPatTm t = do i <- getIState
2327 let timp = addImpl' True [] [] i t
24− evalStateT (toTT timp) 0
28+ evalStateT (toTT (mapPT deNS timp)) 0
2529 where
2630 toTT (PRef _ n) = do i <- lift getIState
2731 case lookupDef n (tt_ctxt i) of
@@ -30,10 +34,16 @@ mkPatTm t = do i <- getIState
3034 toTT (PApp _ t args) = do t' <- toTT t
3135 args' <- mapM (toTT . getTm) args
3236 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
3340 toTT _ = do v <- get
3441 put (v + 1)
3542 return (P Bound (sMN v "imp") Erased)
3643
44+ deNS (PRef f (NS n _)) = PRef f n
45+ deNS t = t
46+
3747-- Given a list of LHSs, generate a extra clauses which cover the remaining
3848-- cases. The ones which haven't been provided are marked 'absurd' so that the
3949-- checker will make sure they can't happen.
@@ -50,10 +60,10 @@ genClauses fc n xs given
5060 logLvl 5 $ "COVERAGE of " ++ show n
5161 logLvl 5 $ show (map length argss) ++ "\n" ++ show (map length all_args)
5262 logLvl 10 $ show argss ++ "\n" ++ show all_args
53− logLvl 10 $ "Original: \n" ++
63+ logLvl 1 $ "Original: \n" ++
5464 showSep "\n" (map (\t -> showTm i (delab' i t True True)) xs)
5565 -- 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
5767 -- there may be more case splitting that the idris_implicits record
5868 -- suggests)
5969 let parg = case lookupCtxt n (idris_implicits i) of
@@ -61,10 +71,10 @@ genClauses fc n xs given
6171 _ -> repeat (pexp Placeholder)
6272 let tryclauses = mkClauses parg all_args
6373 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)
6575 let new = filter (noMatch i) (nub tryclauses)
6676 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)
6878-- ++ " from:\n" ++ showSep "\n" (map (showImp True) tryclauses)
6979 return new
7080-- return (map (\t -> PClause n t [] PImpossible []) new)
@@ -75,9 +85,11 @@ genClauses fc n xs given
7585 lhsApp (PClause _ _ l _ _ _) = l
7686 lhsApp (PWith _ _ l _ _ _) = l
7787
88+ -- Return whether the given clause matches none of the input clauses
89+ -- (xs)
7890 noMatch i tm = all (\x -> case matchClause i (delab' i x True True) tm of
79− Right _ -> False
80− Left miss -> True) xs
91+ Right ms -> False
92+ Left miss -> True) xs
8193
8294
8395 mkClauses :: [PArg] -> [[PTerm]] -> [PTerm]