summaryrefslogtreecommitdiff
path: root/src/full/Agda/TypeChecking/CompiledClause/Compile.hs
diff options
context:
space:
mode:
Diffstat (limited to 'src/full/Agda/TypeChecking/CompiledClause/Compile.hs')
-rw-r--r--src/full/Agda/TypeChecking/CompiledClause/Compile.hs127
1 files changed, 85 insertions, 42 deletions
diff --git a/src/full/Agda/TypeChecking/CompiledClause/Compile.hs b/src/full/Agda/TypeChecking/CompiledClause/Compile.hs
index 19adc97..1a57b0d 100644
--- a/src/full/Agda/TypeChecking/CompiledClause/Compile.hs
+++ b/src/full/Agda/TypeChecking/CompiledClause/Compile.hs
@@ -1,5 +1,4 @@
{-# LANGUAGE CPP #-}
-{-# LANGUAGE TupleSections #-}
module Agda.TypeChecking.CompiledClause.Compile where
@@ -8,7 +7,7 @@ import Prelude hiding (null)
import Data.Maybe
import Data.Monoid
import qualified Data.Map as Map
-import Data.List (genericReplicate, nubBy, findIndex)
+import Data.List (nubBy)
import Data.Function
import Debug.Trace
@@ -45,13 +44,21 @@ compileClauses ::
Maybe (QName, Type) -- ^ Translate record patterns and coverage check with given type?
-> [Clause] -> TCM CompiledClauses
compileClauses mt cs = do
- let cls = [ Cl (unnumberPatVars $ clausePats c) (clauseBody c) | c <- cs ]
+ -- Construct clauses with pattern variables bound in left-to-right order.
+ -- Discard de Bruijn indices in patterns.
+ cs <- normaliseProjP cs
+ let unBruijn cs = [ Cl (map (fmap (fmap dbPatVarName . namedThing)) $ namedClausePats c)
+ (compiledClauseBody c) | c <- cs ]
shared <- sharedFun
case mt of
- Nothing -> return $ compile shared cls
+ Nothing -> return $ compile shared $ unBruijn cs
Just (q, t) -> do
splitTree <- coverageCheck q t cs
+ -- The coverage checker might have added some clauses (#2288)!
+ cs <- normaliseProjP =<< defClauses <$> getConstInfo q
+ let cls = unBruijn cs
+
reportSDoc "tc.cc" 30 $ sep $ do
(text "clauses patterns before compilation") : do
map (prettyTCM . map unArg . clPats) cls
@@ -71,11 +78,12 @@ compileClauses mt cs = do
-- used in clause compiler.
data Cl = Cl
{ clPats :: [Arg Pattern]
- , clBody :: ClauseBody
+ -- ^ Pattern variables are considered in left-to-right order.
+ , clBody :: Maybe Term
} deriving (Show)
instance Pretty Cl where
- pretty (Cl ps b) = P.prettyList ps P.<+> P.text "->" P.<+> pretty b
+ pretty (Cl ps b) = P.prettyList ps P.<+> P.text "->" P.<+> maybe (P.text "_|_") pretty b
type Cls = [Cl]
@@ -108,13 +116,14 @@ compileWithSplitTree shared t cs = case t of
compile :: (Term -> Term) -> Cls -> CompiledClauses
compile shared cs = case nextSplit cs of
Just (isRecP, n)-> Case n $ fmap (compile shared) $ splitOn isRecP (unArg n) cs
- Nothing -> case map (getBody . clBody) cs of
+ Nothing -> case clBody c of
-- It's possible to get more than one clause here due to
-- catch-all expansion.
- Just t : _ -> Done (map (fmap name) $ clPats $ head cs) (shared t)
- Nothing : _ -> Fail
- [] -> __IMPOSSIBLE__
+ Just t -> Done (map (fmap name) $ clPats c) (shared t)
+ Nothing -> Fail
where
+ -- If there are more than one clauses, take the first one.
+ c = headWithDefault __IMPOSSIBLE__ cs
name (VarP x) = x
name (DotP _) = underscore
name ConP{} = __IMPOSSIBLE__
@@ -130,7 +139,7 @@ nextSplit (Cl ps _ : _) = headMaybe $ catMaybes $
-- | Is is not a variable pattern?
-- And if yes, is it a record pattern?
-properSplit :: Pattern -> Maybe Bool
+properSplit :: Pattern' a -> Maybe Bool
properSplit (ConP _ cpi _) = Just $ isJust $ conPRecord cpi
properSplit LitP{} = Just False
properSplit ProjP{} = Just False
@@ -140,7 +149,7 @@ properSplit DotP{} = Nothing
-- | Is this a variable pattern?
--
-- Maintain invariant: @isVar = isNothing . properSplit@!
-isVar :: Pattern -> Bool
+isVar :: Pattern' a -> Bool
isVar VarP{} = True
isVar DotP{} = True
isVar ConP{} = False
@@ -155,15 +164,18 @@ splitOn single n cs = mconcat $ map (fmap (:[]) . splitC n) $
expandCatchAlls single n cs
splitC :: Int -> Cl -> Case Cl
-splitC n (Cl ps b) = case unArg p of
- ProjP d -> projCase d $ Cl (ps0 ++ ps1) b
+splitC n (Cl ps b) = caseMaybe mp fallback $ \case
+ ProjP _ d -> projCase d $ Cl (ps0 ++ ps1) b
ConP c _ qs -> conCase (conName c) $ WithArity (length qs) $
Cl (ps0 ++ map (fmap namedThing) qs ++ ps1) b
LitP l -> litCase l $ Cl (ps0 ++ ps1) b
- VarP{} -> catchAll $ Cl ps b
- DotP{} -> catchAll $ Cl ps b
+ VarP{} -> fallback
+ DotP{} -> fallback
where
- (ps0, p, ps1) = extractNthElement' n ps
+ (ps0, rest) = splitAt n ps
+ mp = unArg <$> headMaybe rest
+ ps1 = drop 1 rest
+ fallback = catchAll $ Cl ps b
-- | Expand catch-alls that appear before actual matches.
--
@@ -202,6 +214,21 @@ splitC n (Cl ps b) = case unArg p of
-- _ -> case 3 of true -> a; false -> b
-- _ -> case 3 of true -> a; false -> b
-- @
+--
+-- Example from issue #2168:
+-- @
+-- f x false = a
+-- f false = \ _ -> b
+-- f x true = c
+-- @
+-- case tree:
+-- @
+-- f x y = case y of
+-- true -> case x of
+-- true -> c
+-- false -> b
+-- false -> a
+-- @
expandCatchAlls :: Bool -> Int -> Cls -> Cls
expandCatchAlls single n cs =
-- Andreas, 2013-03-22
@@ -209,23 +236,24 @@ expandCatchAlls single n cs =
-- we force expansion
if single then doExpand =<< cs else
case cs of
- _ | all (isCatchAllNth . clPats) cs -> cs
- Cl ps b : cs | not (isCatchAllNth ps) -> Cl ps b : expandCatchAlls False n cs
- | otherwise -> map (expand ps b) expansions ++ Cl ps b : expandCatchAlls False n cs
+ _ | all (isCatchAllNth . clPats) cs -> cs
+ c@(Cl ps b) : cs | not (isCatchAllNth ps) -> c : expandCatchAlls False n cs
+ | otherwise -> map (expand c) expansions ++ c : expandCatchAlls False n cs
_ -> __IMPOSSIBLE__
where
-- In case there is only one branch in the split tree, we expand all
-- catch-alls for this position
-- The @expansions@ are collected from all the clauses @cs@ then.
-- Note: @expansions@ could be empty, so we keep the orignal clause.
- doExpand c@(Cl ps b)
- | isVar $ unArg $ nth ps = map (expand ps b) expansions ++ [c]
- | otherwise = [c]
+ doExpand c@(Cl ps _)
+ | exCatchAllNth ps = map (expand c) expansions ++ [c]
+ | otherwise = [c]
-- True if nth pattern is variable or there are less than n patterns.
isCatchAllNth ps = all (isVar . unArg) $ take 1 $ drop n ps
- nth qs = headWithDefault __IMPOSSIBLE__ $ drop n qs
+ -- True if nth pattern exists and is variable.
+ exCatchAllNth ps = any (isVar . unArg) $ take 1 $ drop n ps
classify (LitP l) = Left l
classify (ConP c _ _) = Right c
@@ -233,38 +261,53 @@ expandCatchAlls single n cs =
-- All non-catch-all patterns following this one (at position n).
-- These are the cases the wildcard needs to be expanded into.
- expansions = nubBy ((==) `on` (classify . unArg))
- . filter (not . isVar . unArg)
- . map (nth . clPats)
+ expansions = nubBy ((==) `on` (classify . unArg . snd))
+ . mapMaybe (notVarNth . clPats)
$ cs
+ notVarNth ps = caseMaybe (headMaybe ps2) Nothing $ \ p ->
+ if isVar (unArg p) then Nothing else Just (ps1, p)
+ where (ps1, ps2) = splitAt n ps
- expand ps b q =
+ expand cl (qs, q) =
case unArg q of
ConP c mt qs' -> Cl (ps0 ++ [q $> ConP c mt conPArgs] ++ ps1)
- (substBody n' m (Con c conArgs) b)
+ (substBody n' m (Con c ci conArgs) b)
where
+ ci = fromConPatternInfo mt
m = length qs'
-- replace all direct subpatterns of q by _
- conPArgs = map (fmap ($> VarP underscore)) qs'
- conArgs = zipWith (\ q n -> q $> var n) qs' $ downFrom m
+ conPArgs = map (fmap ($> VarP "_")) qs'
+ conArgs = zipWith (\ q' i -> q' $> var i) qs' $ downFrom m
LitP l -> Cl (ps0 ++ [q $> LitP l] ++ ps1) (substBody n' 0 (Lit l) b)
_ -> __IMPOSSIBLE__
where
- (ps0, rest) = splitAt n ps
- ps1 = maybe __IMPOSSIBLE__ snd $ uncons rest
+ -- Andreas, 2016-09-19 issue #2168
+ -- Due to varying function arity, some clauses might be eta-contracted.
+ -- Thus, we eta-expand them.
+ Cl ps b = ensureNPatterns (n + 1) (map getArgInfo $ qs ++ [q]) cl
+ -- The following pattern match cannot fail (by construction of @ps@).
+ (ps0, _:ps1) = splitAt n ps
- n' = countVars ps0
+ n' = countVars ps1
countVars = sum . map (count . unArg)
count VarP{} = 1
count (ConP _ _ ps) = countVars $ map (fmap namedThing) ps
count DotP{} = 1 -- dot patterns are treated as variables in the clauses
count _ = 0
-substBody :: Int -> Int -> Term -> ClauseBody -> ClauseBody
-substBody _ _ _ NoBody = NoBody
-substBody 0 m v b = case b of
- Bind b -> foldr (.) id (replicate m (Bind . Abs underscore)) $ subst 0 v (absBody $ raise m b)
- _ -> __IMPOSSIBLE__
-substBody n m v b = case b of
- Bind b -> Bind $ fmap (substBody (n - 1) m v) b
- _ -> __IMPOSSIBLE__
+-- | Make sure (by eta-expansion) that clause has arity at least @n@
+-- where @n@ is also the length of the provided list.
+ensureNPatterns :: Int -> [ArgInfo] -> Cl -> Cl
+ensureNPatterns n ais0 cl@(Cl ps b)
+ | m <= 0 = cl
+ | otherwise = Cl (ps ++ ps') (raise m b `apply` args)
+ where
+ k = length ps
+ ais = drop k ais0
+ -- m = Number of arguments to add
+ m = n - k
+ ps' = for ais $ \ ai -> Arg ai $ VarP "_"
+ args = zipWith (\ i ai -> Arg ai $ var i) (downFrom m) ais
+
+substBody :: (Subst t a) => Int -> Int -> t -> a -> a
+substBody n m v = applySubst $ liftS n $ v :# raiseS m