@@ -40,6 +40,12 @@ mkPatTm t = do i <- getIState
40 toTT (PApp _ t args) = do t' <- toTT t
40 toTT (PApp _ t args) = do t' <- toTT t
41 args' <- mapM (toTT . getTm) args
41 args' <- mapM (toTT . getTm) args
42 return $ mkApp t' args'
42 return $ mkApp t' args'
43+ toTT (PDPair _ _ _ l _ r) = do l' <- toTT l
45+ return $ mkApp (P Ref sigmaCon Erased) [Erased, Erased, l', r']
46+ toTT (PPair _ _ _ l r) = do l' <- toTT l
48+ return $ mkApp (P Ref pairCon Erased) [Erased, Erased, l', r']
43 -- For alternatives, pick the first and drop the namespaces. It doesn't
49 -- For alternatives, pick the first and drop the namespaces. It doesn't
44 -- really matter which is taken since matching will ignore the namespace.
50 -- really matter which is taken since matching will ignore the namespace.
45 toTT (PAlternative _ _ (a : as)) = toTT a
51 toTT (PAlternative _ _ (a : as)) = toTT a
@@ -78,7 +84,7 @@ genClauses fc n xs given
78 logCoverage 5 $ show (map length argss) ++ "\n" ++ show (map length all_args)
84 logCoverage 5 $ show (map length argss) ++ "\n" ++ show (map length all_args)
79 logCoverage 10 $ show argss ++ "\n" ++ show all_args
85 logCoverage 10 $ show argss ++ "\n" ++ show all_args
80 logCoverage 3 $ "Original: \n" ++
86 logCoverage 3 $ "Original: \n" ++
81− showSep "\n" (map (\t -> showTm i (delab' i t True True)) xs)
87+ showSep "\n" (map (\t -> showTmImpls (delab' i t True True)) xs)
82 -- add an infinite supply of explicit arguments to update the possible
88 -- add an infinite supply of explicit arguments to update the possible
83 -- cases for (the return type may be variadic, or function type, so
89 -- cases for (the return type may be variadic, or function type, so
84 -- there may be more case splitting that the idris_implicits record
90 -- there may be more case splitting that the idris_implicits record