1{-# LANGUAGE NondecreasingIndentation #-} 2 3-- | Pattern matcher used in the reducer for clauses that 4-- have not been compiled to case trees yet. 5 6module Agda.TypeChecking.Patterns.Match where 7 8import Prelude hiding (null) 9 10import Control.Monad 11import Data.IntMap (IntMap) 12import qualified Data.IntMap as IntMap 13 14import Agda.Syntax.Common 15import Agda.Syntax.Internal 16import Agda.Syntax.Internal.Pattern 17 18import Agda.TypeChecking.Reduce 19import Agda.TypeChecking.Reduce.Monad 20import Agda.TypeChecking.Substitute 21import Agda.TypeChecking.Monad hiding (constructorForm) 22import Agda.TypeChecking.Pretty 23import Agda.TypeChecking.Records 24 25import Agda.Utils.Empty 26import Agda.Utils.Functor (for, ($>), (<&>)) 27import Agda.Utils.Maybe 28import Agda.Utils.Null 29import Agda.Utils.Singleton 30import Agda.Utils.Size 31import Agda.Utils.Tuple 32 33import Agda.Utils.Impossible 34 35-- | If matching is inconclusive (@DontKnow@) we want to know whether 36-- it is due to a particular meta variable. 37data Match a = Yes Simplification (IntMap (Arg a)) 38 | No 39 | DontKnow (Blocked ()) 40 deriving Functor 41 42instance Null (Match a) where 43 empty = Yes empty empty 44 null (Yes simpl as) = null simpl && null as 45 null _ = False 46 47matchedArgs :: Empty -> Int -> IntMap (Arg a) -> [Arg a] 48matchedArgs err n vs = map (fromMaybe (absurd err)) $ matchedArgs' n vs 49 50matchedArgs' :: Int -> IntMap (Arg a) -> [Maybe (Arg a)] 51matchedArgs' n vs = map get [0 .. n - 1] 52 where 53 get k = IntMap.lookup k vs 54 55-- | Builds a proper substitution from an IntMap produced by match(Co)patterns 56buildSubstitution :: (DeBruijn a) 57 => Impossible -> Int -> IntMap (Arg a) -> Substitution' a 58buildSubstitution err n vs = foldr cons idS $ matchedArgs' n vs 59 where cons Nothing = Strengthen err 60 cons (Just v) = consS (unArg v) 61 62 63instance Semigroup (Match a) where 64 -- @NotBlocked (StuckOn e)@ means blocked by a variable. 65 -- In this case, no instantiation of meta-variables will make progress. 66 DontKnow b <> DontKnow b' = DontKnow $ b <> b' 67 DontKnow m <> _ = DontKnow m 68 _ <> DontKnow m = DontKnow m 69 -- One could imagine DontKnow _ <> No = No, but would break the 70 -- equivalence to case-trees (Issue 2964). 71 No <> _ = No 72 _ <> No = No 73 Yes s us <> Yes s' vs = Yes (s <> s') (us <> vs) 74 75instance Monoid (Match a) where 76 mempty = empty 77 mappend = (<>) 78 79-- | Instead of 'zipWithM', we need to use this lazy version 80-- of combining pattern matching computations. 81 82-- Andreas, 2014-05-08, see Issue 1124: 83-- 84-- Due to a bug in TypeChecking.Patterns.Match 85-- a failed match of (C n b) against (C O unit) 86-- turned into (C n unit). 87-- This was because all patterns were matched in 88-- parallel, and evaluations of successfull matches 89-- (and a record constructor like unit can always 90-- be successfully matched) were returned, leading 91-- to a reassembly of (C n b) as (C n unit) which is 92-- illtyped. 93 94-- Now patterns are matched left to right and 95-- upon failure, no further matching is performed. 96 97foldMatch 98 :: forall m p v . (IsProjP p, MonadMatch m) 99 => (p -> v -> m (Match Term, v)) 100 -> [p] -> [v] -> m (Match Term, [v]) 101foldMatch match = loop where 102 loop :: [p] -> [v] -> m (Match Term, [v]) 103 loop ps0 vs0 = do 104 case (ps0, vs0) of 105 ([], []) -> return (empty, []) 106 (p : ps, v : vs) -> do 107 (r, v') <- match p v 108 case r of 109 No | Just{} <- isProjP p -> return (No, v' : vs) 110 No -> do 111 -- Issue 2964: Even when the first pattern doesn't match we should 112 -- continue to the next patterns (and potentially block on them) 113 -- because the splitting order in the case tree may not be 114 -- left-to-right. 115 (r', _vs') <- loop ps vs 116 -- Issue 2968: do not use vs' here, because it might 117 -- contain ill-typed terms due to eta-expansion at wrong 118 -- type. 119 return (r <> r', v' : vs) 120 DontKnow m -> return (DontKnow m, v' : vs) 121 Yes{} -> do 122 (r', vs') <- loop ps vs 123 return (r <> r', v' : vs') 124 _ -> __IMPOSSIBLE__ 125 126 127-- TODO refactor matchPattern* to work with Elim instead. 128mergeElim :: Elim -> Arg Term -> Elim 129mergeElim Apply{} arg = Apply arg 130mergeElim (IApply x y _) arg = IApply x y (unArg arg) 131mergeElim Proj{} _ = __IMPOSSIBLE__ 132 133mergeElims :: [Elim] -> [Arg Term] -> [Elim] 134mergeElims = zipWith mergeElim 135 136type MonadMatch m = PureTCM m 137 138-- | @matchCopatterns ps es@ matches spine @es@ against copattern spine @ps@. 139-- 140-- Returns 'Yes' and a substitution for the pattern variables 141-- (in form of IntMap Term) if matching was successful. 142-- 143-- Returns 'No' if there was a constructor or projection mismatch. 144-- 145-- Returns 'DontKnow' if an argument could not be evaluated to 146-- constructor form because of a blocking meta variable. 147-- 148-- In any case, also returns spine @es@ in reduced form 149-- (with all the weak head reductions performed that were necessary 150-- to come to a decision). 151matchCopatterns :: MonadMatch m 152 => [NamedArg DeBruijnPattern] 153 -> [Elim] 154 -> m (Match Term, [Elim]) 155matchCopatterns ps vs = do 156 traceSDoc "tc.match" 50 157 (vcat [ "matchCopatterns" 158 , nest 2 $ "ps =" <+> fsep (punctuate comma $ map (prettyTCM . namedArg) ps) 159 , nest 2 $ "vs =" <+> fsep (punctuate comma $ map prettyTCM vs) 160 ]) $ do 161 -- Buggy, see issue 1124: 162 -- mapFst mconcat . unzip <$> zipWithM' (matchCopattern . namedArg) ps vs 163 foldMatch (matchCopattern . namedArg) ps vs 164 165-- | Match a single copattern. 166matchCopattern :: MonadMatch m 167 => DeBruijnPattern 168 -> Elim 169 -> m (Match Term, Elim) 170matchCopattern pat@ProjP{} elim@(Proj _ q) = do 171 p <- normaliseProjP pat <&> \case 172 ProjP _ p -> p 173 _ -> __IMPOSSIBLE__ 174 q <- getOriginalProjection q 175 return $ if p == q then (Yes YesSimplification empty, elim) 176 else (No, elim) 177-- The following two cases are not impossible, see #2964 178matchCopattern ProjP{} elim@Apply{} = return (No , elim) 179matchCopattern _ elim@Proj{} = return (No , elim) 180matchCopattern p (Apply v) = mapSnd Apply <$> matchPattern p v 181matchCopattern p e@(IApply x y r) = mapSnd (mergeElim e) <$> matchPattern p (defaultArg r) 182 183matchPatterns :: MonadMatch m 184 => [NamedArg DeBruijnPattern] 185 -> [Arg Term] 186 -> m (Match Term, [Arg Term]) 187matchPatterns ps vs = do 188 reportSDoc "tc.match" 20 $ 189 vcat [ "matchPatterns" 190 , nest 2 $ "ps =" <+> prettyTCMPatternList ps 191 , nest 2 $ "vs =" <+> fsep (punctuate comma $ map prettyTCM vs) 192 ] 193 194 traceSDoc "tc.match" 50 195 (vcat [ "matchPatterns" 196 , nest 2 $ "ps =" <+> fsep (punctuate comma $ map (text . show) ps) 197 , nest 2 $ "vs =" <+> fsep (punctuate comma $ map prettyTCM vs) 198 ]) $ do 199 -- Buggy, see issue 1124: 200 -- (ms,vs) <- unzip <$> zipWithM' (matchPattern . namedArg) ps vs 201 -- return (mconcat ms, vs) 202 foldMatch (matchPattern . namedArg) ps vs 203 204-- | Match a single pattern. 205matchPattern :: MonadMatch m 206 => DeBruijnPattern 207 -> Arg Term 208 -> m (Match Term, Arg Term) 209matchPattern p u = case (p, u) of 210 (ProjP{}, _ ) -> __IMPOSSIBLE__ 211 (IApplyP _ _ _ x , arg ) -> return (Yes NoSimplification entry, arg) 212 where entry = singleton (dbPatVarIndex x, arg) 213 (VarP _ x , arg ) -> return (Yes NoSimplification entry, arg) 214 where entry = singleton (dbPatVarIndex x, arg) 215 (DotP _ _ , arg@(Arg _ v)) -> return (Yes NoSimplification empty, arg) 216 (LitP _ l , arg@(Arg _ v)) -> do 217 w <- reduceB v 218 let arg' = arg $> ignoreBlocking w 219 case w of 220 NotBlocked _ (Lit l') 221 | l == l' -> return (Yes YesSimplification empty , arg') 222 | otherwise -> return (No , arg') 223 Blocked b _ -> return (DontKnow $ Blocked b () , arg') 224 NotBlocked r t -> return (DontKnow $ NotBlocked r' () , arg') 225 where r' = stuckOn (Apply arg') r 226 227 -- Case constructor pattern. 228 (ConP c cpi ps, Arg info v) -> do 229 if not (conPRecord cpi) then fallback c ps (Arg info v) else do 230 isEtaRecordCon (conName c) >>= \case 231 Nothing -> fallback c ps (Arg info v) 232 Just fs -> do 233 -- Case: Eta record constructor. 234 -- This case is necessary if we want to use the clauses before 235 -- record pattern translation (e.g., in type-checking definitions by copatterns). 236 unless (size fs == size ps) __IMPOSSIBLE__ 237 mapSnd (Arg info . Con c (fromConPatternInfo cpi) . map Apply) <$> do 238 matchPatterns ps $ for fs $ \ (Arg ai f) -> Arg ai $ v `applyE` [Proj ProjSystem f] 239 where 240 isEtaRecordCon :: HasConstInfo m => QName -> m (Maybe [Arg QName]) 241 isEtaRecordCon c = do 242 (theDef <$> getConstInfo c) >>= \case 243 Constructor{ conData = d } -> do 244 (theDef <$> getConstInfo d) >>= \case 245 r@Record{ recFields = fs } | YesEta <- recEtaEquality r -> return $ Just $ map argFromDom fs 246 _ -> return Nothing 247 _ -> __IMPOSSIBLE__ 248 (DefP o q ps, v) -> do 249 let f (Def q' vs) | q == q' = Just (Def q, vs) 250 f _ = Nothing 251 fallback' f ps v 252 where 253 -- Default: not an eta record constructor. 254 fallback :: MonadMatch m 255 => ConHead -> [NamedArg DeBruijnPattern] -> Arg Term -> m (Match Term, Arg Term) 256 fallback c ps v = do 257 let f (Con c' ci' vs) | c == c' = Just (Con c' ci',vs) 258 f _ = Nothing 259 fallback' f ps v 260 261 -- Regardless of blocking, constructors and a properly applied @hcomp@ 262 -- can be matched on. 263 isMatchable' :: HasBuiltins m => m (Blocked Term -> Maybe Term) 264 isMatchable' = do 265 mhcomp <- getName' builtinHComp 266 return $ \ r -> 267 case ignoreBlocking r of 268 t@Con{} -> Just t 269 t@(Def q [l,a,phi,u,u0]) | Just q == mhcomp 270 -> Just t 271 _ -> Nothing 272 273 -- DefP hcomp and ConP matching. 274 fallback' :: MonadMatch m 275 => (Term -> Maybe (Elims -> Term , Elims)) 276 -> [NamedArg DeBruijnPattern] 277 -> Arg Term 278 -> m (Match Term, Arg Term) 279 fallback' mtc ps (Arg info v) = do 280 isMatchable <- isMatchable' 281 282 w <- reduceB v 283 -- Unfold delayed (corecursive) definitions one step. This is 284 -- only necessary if c is a coinductive constructor, but 285 -- 1) it does not hurt to do it all the time, and 286 -- 2) whatInduction c sometimes crashes because c may point to 287 -- an axiom at this stage (if we are checking the 288 -- projection functions for a record type). 289{- 290 w <- case w of 291 NotBlocked r (Def f es) -> -- Andreas, 2014-06-12 TODO: r == ReallyNotBlocked sufficient? 292 unfoldDefinitionE True reduceB' (Def f []) f es 293 -- reduceB is used here because some constructors 294 -- are actually definitions which need to be 295 -- unfolded (due to open public). 296 _ -> return w 297-} 298 -- Jesper, 23-06-2016: Note that unfoldCorecursion may destroy 299 -- constructor forms, so we only call constructorForm after. 300 w <- traverse constructorForm =<< case w of 301 NotBlocked r u -> liftReduce $ unfoldCorecursion u -- Andreas, 2014-06-12 TODO: r == ReallyNotBlocked sufficient? 302 _ -> return w 303 let v = ignoreBlocking w 304 arg = Arg info v -- the reduced argument 305 306 case w of 307 b | Just t <- isMatchable b -> 308 case mtc t of 309 Just (bld, vs) -> do 310 (m, vs1) <- yesSimplification <$> matchPatterns ps (fromMaybe __IMPOSSIBLE__ $ allApplyElims vs) 311 return (m, Arg info $ bld (mergeElims vs vs1)) 312 Nothing 313 -> return (No , arg) 314 Blocked b _ -> return (DontKnow $ Blocked b () , arg) 315 NotBlocked r _ -> return (DontKnow $ NotBlocked r' () , arg) 316 where r' = stuckOn (Apply arg) r 317 318-- ASR (08 November 2014). The type of the function could be 319-- 320-- @(Match Term, [Arg Term]) -> (Match Term, [Arg Term])@. 321yesSimplification :: (Match a, b) -> (Match a, b) 322yesSimplification (Yes _ vs, us) = (Yes YesSimplification vs, us) 323yesSimplification r = r 324 325-- Matching patterns against patterns ------------------------------------- 326 327-- | Match a single pattern. 328matchPatternP :: MonadMatch m 329 => DeBruijnPattern 330 -> Arg DeBruijnPattern 331 -> m (Match DeBruijnPattern) 332matchPatternP p (Arg info (DotP _ v)) = do 333 (m, arg) <- matchPattern p (Arg info v) 334 return $ fmap (DotP defaultPatternInfo) m 335matchPatternP p arg@(Arg info q) = do 336 let varMatch x = return $ Yes NoSimplification $ singleton (dbPatVarIndex x, arg) 337 termMatch = do 338 (m, arg) <- matchPattern p (fmap patternToTerm arg) 339 return $ fmap (DotP defaultPatternInfo) m 340 case p of 341 ProjP{} -> __IMPOSSIBLE__ 342 IApplyP _ _ _ x -> varMatch x 343 VarP _ x -> varMatch x 344 DotP _ _ -> return $ Yes NoSimplification empty 345 LitP{} -> termMatch -- Literal patterns bind no variables so we can fall back to the Term version. 346 DefP{} -> termMatch 347 348 ConP c cpi ps -> 349 case q of 350 ConP c' _ qs | c == c' -> matchPatternsP ps ((map . fmap) namedThing qs) 351 | otherwise -> return No 352 LitP{} -> fmap toLitP <$> termMatch 353 where toLitP (DotP _ (Lit l)) = litP l -- All bindings should be to literals 354 toLitP _ = __IMPOSSIBLE__ 355 _ -> termMatch 356 357matchPatternsP :: MonadMatch m 358 => [NamedArg DeBruijnPattern] 359 -> [Arg DeBruijnPattern] 360 -> m (Match DeBruijnPattern) 361matchPatternsP ps qs = do 362 mconcat <$> zipWithM matchPatternP (map namedArg ps) qs 363