1 2-- | Code which replaces pattern matching on record constructors with 3-- uses of projection functions. 4 5module Agda.TypeChecking.RecordPatterns 6 ( translateRecordPatterns 7 , translateCompiledClauses 8 , translateSplitTree 9 , recordPatternToProjections 10 ) where 11 12import Control.Arrow (first, second) 13import Control.Monad.Fix 14import Control.Monad.Reader 15import Control.Monad.State 16 17import qualified Data.List as List 18import Data.Maybe 19import qualified Data.Map as Map 20 21import Agda.Syntax.Common 22import Agda.Syntax.Internal as I 23import Agda.Syntax.Internal.Pattern as I 24 25import Agda.TypeChecking.CompiledClause 26import Agda.TypeChecking.Coverage.SplitTree 27import Agda.TypeChecking.Datatypes 28import Agda.TypeChecking.Monad 29import Agda.TypeChecking.Pretty hiding (pretty) 30import Agda.TypeChecking.Records 31import Agda.TypeChecking.Reduce 32import Agda.TypeChecking.Substitute 33import Agda.TypeChecking.Telescope 34 35import Agda.Interaction.Options 36 37import Agda.Utils.Either 38import Agda.Utils.Functor 39import Agda.Utils.Permutation hiding (dropFrom) 40import Agda.Utils.Pretty (Pretty(..)) 41import qualified Agda.Utils.Pretty as P 42import Agda.Utils.Size 43import Agda.Utils.Update (MonadChange, tellDirty) 44 45import Agda.Utils.Impossible 46 47--------------------------------------------------------------------------- 48-- * Record pattern translation for let bindings 49--------------------------------------------------------------------------- 50 51-- | Take a record pattern @p@ and yield a list of projections 52-- corresponding to the pattern variables, from left to right. 53-- 54-- E.g. for @(x , (y , z))@ we return @[ fst, fst . snd, snd . snd ]@. 55-- 56-- If it is not a record pattern, error 'ShouldBeRecordPattern' is raised. 57recordPatternToProjections :: DeBruijnPattern -> TCM [Term -> Term] 58recordPatternToProjections p = 59 case p of 60 VarP{} -> return [ id ] 61 LitP{} -> typeError $ ShouldBeRecordPattern p 62 DotP{} -> typeError $ ShouldBeRecordPattern p 63 ConP c ci ps -> do 64 unless (conPRecord ci) $ 65 typeError $ ShouldBeRecordPattern p 66 let t = unArg $ fromMaybe __IMPOSSIBLE__ $ conPType ci 67 reportSDoc "tc.rec" 45 $ vcat 68 [ "recordPatternToProjections: " 69 , nest 2 $ "constructor pattern " <+> prettyTCM p <+> " has type " <+> prettyTCM t 70 ] 71 reportSLn "tc.rec" 70 $ " type raw: " ++ show t 72 fields <- getRecordTypeFields t 73 concat <$> zipWithM comb (map proj fields) (map namedArg ps) 74 ProjP{} -> __IMPOSSIBLE__ -- copattern cannot appear here 75 IApplyP{} -> typeError $ ShouldBeRecordPattern p 76 DefP{} -> typeError $ ShouldBeRecordPattern p 77 where 78 proj p = (`applyE` [Proj ProjSystem $ unDom p]) 79 comb :: (Term -> Term) -> DeBruijnPattern -> TCM [Term -> Term] 80 comb prj p = map (\ f -> f . prj) <$> recordPatternToProjections p 81 82 83--------------------------------------------------------------------------- 84-- * Record pattern translation for compiled clauses 85--------------------------------------------------------------------------- 86 87-- | Take a matrix of booleans (at least one row!) and summarize the columns 88-- using conjunction. 89conjColumns :: [[Bool]] -> [Bool] 90conjColumns = foldl1 (zipWith (&&)) 91 92-- UNUSED Liang-Ting 2019-07-16 93---- | @insertColumn i a m@ inserts a column before the @i@th column in 94---- matrix @m@ and fills it with value @a@. 95--insertColumn :: Int -> a -> [[a]] -> [[a]] 96--insertColumn i a rows = map ins rows where 97-- ins row = let (init, last) = splitAt i row in init ++ a : last 98 99{- UNUSED 100-- | @cutColumn i m@ removes the @i@th column from matrix @m@. 101cutColumn :: Int -> [[a]] -> [[a]] 102cutColumn i rows = map cut rows where 103 cut row = let (init, _:last) = splitAt i row in init ++ last 104 105-- | @cutColumns i n xss = (yss, xss')@ cuts out a submatrix @yss@ 106-- of width @n@ from @xss@, starting at column @i@. 107cutColumns :: Int -> Int -> [[a]] -> ([[a]], [[a]]) 108cutColumns i n rows = unzip (map (cutSublist i n) rows) 109-} 110 111-- UNUSED Liang-Ting 2019-07-16 112---- | @cutSublist i n xs = (xs', ys, xs'')@ cuts out a sublist @ys@ 113---- of width @n@ from @xs@, starting at column @i@. 114--cutSublist :: Int -> Int -> [a] -> ([a], [a], [a]) 115--cutSublist i n row = 116-- let (init, rest) = splitAt i row 117-- (mid , last) = splitAt n rest 118-- in (init, mid, last) 119 120getEtaAndArity :: SplitTag -> TCM (Bool, Nat) 121getEtaAndArity (SplitCon c) = 122 for (getConstructorInfo c) $ \case 123 DataCon n -> (False, n) 124 RecordCon _ eta fs -> (eta == YesEta, size fs) 125getEtaAndArity (SplitLit l) = return (False, 0) 126getEtaAndArity SplitCatchall = return (False, 1) 127 128translateCompiledClauses 129 :: forall m. (HasConstInfo m, MonadChange m) 130 => CompiledClauses -> m CompiledClauses 131translateCompiledClauses cc = ignoreAbstractMode $ do 132 reportSDoc "tc.cc.record" 20 $ vcat 133 [ "translate record patterns in compiled clauses" 134 , nest 2 $ return $ pretty cc 135 ] 136 cc <- loop cc 137 reportSDoc "tc.cc.record" 20 $ vcat 138 [ "translated compiled clauses (no eta record patterns):" 139 , nest 2 $ return $ pretty cc 140 ] 141 cc <- recordExpressionsToCopatterns cc 142 reportSDoc "tc.cc.record" 20 $ vcat 143 [ "translated compiled clauses (record expressions to copatterns):" 144 , nest 2 $ return $ pretty cc 145 ] 146 return cc 147 where 148 149 loop :: CompiledClauses -> m (CompiledClauses) 150 loop cc = case cc of 151 Fail{} -> return cc 152 Done{} -> return cc 153 Case i cs -> loops i cs 154 155 loops :: Arg Int -- split variable 156 -> Case CompiledClauses -- original split tree 157 -> m CompiledClauses 158 loops i cs@Branches{ projPatterns = comatch 159 , conBranches = conMap 160 , etaBranch = eta 161 , litBranches = litMap 162 , fallThrough = fT 163 , catchAllBranch = catchAll 164 , lazyMatch = lazy } = do 165 166 catchAll <- traverse loop catchAll 167 litMap <- traverse loop litMap 168 (conMap, eta) <- do 169 let noEtaCase = (, Nothing) <$> (traverse . traverse) loop conMap 170 yesEtaCase b ch = (Map.empty,) . Just . (ch,) <$> traverse loop b 171 case Map.toList conMap of 172 -- This is already an eta match. Still need to recurse though. 173 -- This can happen (#2981) when we 174 -- 'revisitRecordPatternTranslation' in Rules.Decl, due to 175 -- inferred eta. 176 _ | Just (ch, b) <- eta -> yesEtaCase b ch 177 [(c, b)] | not comatch -> -- possible eta-match 178 getConstructorInfo c >>= \ case 179 RecordCon pm YesEta fs -> yesEtaCase b $ 180 ConHead c (IsRecord pm) Inductive (map argFromDom fs) 181 _ -> noEtaCase 182 _ -> noEtaCase 183 return $ Case i cs{ conBranches = conMap 184 , etaBranch = eta 185 , litBranches = litMap 186 , fallThrough = fT 187 , catchAllBranch = catchAll 188 } 189 190{- UNUSED 191instance Monoid CompiledClauses where 192 mempty = __IMPOSSIBLE__ 193 mappend (Case n c) (Case n' c') | n == n' = Case n $ mappend c c' 194 mappend _ _ = __IMPOSSIBLE__ 195 196mergeCatchAll :: CompiledClauses -> Maybe CompiledClauses -> CompiledClauses 197mergeCatchAll cc ca = maybe cc (mappend cc) ca 198{- 199 case (cc, ca) of 200 (_ , Nothing) -> cc 201 (Case n c, Just (Case n' c')) | n == n' -> Case n $ mappend c c' 202 _ -> __IMPOSSIBLE__ -- this would mean non-determinism 203-} 204-} 205 206-- | Transform definitions returning record expressions to use copatterns 207-- instead. This prevents terms from blowing up when reduced. 208recordExpressionsToCopatterns 209 :: (HasConstInfo m, MonadChange m) 210 => CompiledClauses 211 -> m CompiledClauses 212recordExpressionsToCopatterns = \case 213 Case i bs -> Case i <$> traverse recordExpressionsToCopatterns bs 214 cc@Fail{} -> return cc 215 cc@(Done xs (Con c ConORec es)) -> do -- don't translate if using the record /constructor/ 216 let vs = map unArg $ fromMaybe __IMPOSSIBLE__ $ allApplyElims es 217 Constructor{ conArity = ar } <- theDef <$> getConstInfo (conName c) 218 irrProj <- optIrrelevantProjections <$> pragmaOptions 219 getConstructorInfo (conName c) >>= \ case 220 RecordCon CopatternMatching YesEta fs 221 | ar <- length fs, ar > 0, -- only for eta-records with at least one field 222 length vs == ar, -- where the constructor application is saturated 223 irrProj || not (any isIrrelevant fs) -> do -- and irrelevant projections (if any) are allowed 224 tellDirty 225 Case (defaultArg $ length xs) <$> do 226 -- translate new cases recursively (there might be nested record expressions) 227 traverse recordExpressionsToCopatterns $ Branches 228 { projPatterns = True 229 , conBranches = Map.fromList $ 230 zipWith (\ f v -> (unDom f, WithArity 0 $ Done xs v)) fs vs 231 , etaBranch = Nothing 232 , litBranches = Map.empty 233 , catchAllBranch = Nothing 234 , fallThrough = Nothing 235 , lazyMatch = False 236 } 237 _ -> return cc 238 cc@Done{} -> return cc 239 240-- UNUSED Liang-Ting Chen 2019-07-16 241---- | @replaceByProjections i projs cc@ replaces variables @i..i+n-1@ 242---- (counted from left) by projections @projs_1 i .. projs_n i@. 243---- 244---- If @n==0@, we matched on a zero-field record, which means that 245---- we are actually introduce a new variable, increasing split 246---- positions greater or equal to @i@ by one. 247---- Otherwise, we have to lower 248---- 249--replaceByProjections :: Arg Int -> [QName] -> CompiledClauses -> CompiledClauses 250--replaceByProjections (Arg ai i) projs cc = 251-- let n = length projs 252-- 253-- loop :: Int -> CompiledClauses -> CompiledClauses 254-- loop i cc = case cc of 255-- Case j cs 256-- 257-- -- if j < i, we leave j untouched, but we increase i by the number 258-- -- of variables replacing j in the branches 259-- | unArg j < i -> Case j $ loops i cs 260-- 261-- -- if j >= i then we shrink j by (n-1) 262-- | otherwise -> Case (j <&> \ k -> k - (n-1)) $ fmap (loop i) cs 263-- 264-- Done xs v -> 265-- -- we have to delete (n-1) variables from xs 266-- -- and instantiate v suitably with the projections 267-- let (xs0,xs1,xs2) = cutSublist i n xs 268-- names | null xs1 = ["r"] 269-- | otherwise = map unArg xs1 270-- x = Arg ai $ foldr1 appendArgNames names 271-- xs' = xs0 ++ x : xs2 272-- us = map (\ p -> Var 0 [Proj ProjSystem p]) (reverse projs) 273-- -- go from level (i + n - 1) to index (subtract from |xs|-1) 274-- index = length xs - (i + n) 275-- in Done xs' $ applySubst (liftS (length xs2) $ us ++# raiseS 1) v 276-- -- The body is NOT guarded by lambdas! 277-- -- WRONG: underLambdas i (flip apply) (map defaultArg us) v 278-- 279-- Fail -> Fail 280-- 281-- loops :: Int -> Case CompiledClauses -> Case CompiledClauses 282-- loops i bs@Branches{ conBranches = conMap 283-- , litBranches = litMap 284-- , catchAllBranch = catchAll } = 285-- bs{ conBranches = fmap (\ (WithArity n c) -> WithArity n $ loop (i + n - 1) c) conMap 286-- , litBranches = fmap (loop (i - 1)) litMap 287-- , catchAllBranch = fmap (loop i) catchAll 288-- } 289-- in loop i cc 290 291-- UNUSED Liang-Ting 2019-07-16 292---- | Check if a split is on a record constructor, and return the projections 293---- if yes. 294--isRecordCase :: Case c -> TCM (Maybe ([QName], c)) 295--isRecordCase (Branches { conBranches = conMap 296-- , litBranches = litMap 297-- , catchAllBranch = Nothing }) 298-- | Map.null litMap 299-- , [(con, WithArity _ br)] <- Map.toList conMap = do 300-- isRC <- isRecordConstructor con 301-- case isRC of 302-- Just (r, Record { recFields = fs }) -> return $ Just (map unArg fs, br) 303-- Just (r, _) -> __IMPOSSIBLE__ 304-- Nothing -> return Nothing 305--isRecordCase _ = return Nothing 306 307--------------------------------------------------------------------------- 308-- * Record pattern translation for split trees 309--------------------------------------------------------------------------- 310--UNUSED Liang-Ting Chen 2019-07-16 311---- | Split tree annotation. 312--data RecordSplitNode = RecordSplitNode 313-- { _splitTag :: SplitTag -- ^ Constructor name/literal for this branch. 314-- , _splitArity :: Int -- ^ Arity of the constructor. 315-- , _splitRecordPattern :: Bool -- ^ Should we translate this split away? 316-- } 317 318-- | Split tree annotated for record pattern translation. 319--type RecordSplitTree = SplitTree' RecordSplitNode 320--type RecordSplitTrees = SplitTrees' RecordSplitNode 321 322--UNUSED Liang-Ting Chen 2019-07-16 323---- | Bottom-up procedure to annotate split tree. 324--recordSplitTree :: SplitTree -> TCM RecordSplitTree 325--recordSplitTree = snd <.> loop 326-- where 327-- 328-- loop :: SplitTree -> TCM ([Bool], RecordSplitTree) 329-- loop = \case 330-- SplittingDone n -> return (replicate n True, SplittingDone n) 331-- SplitAt i ts -> do 332-- (xs, ts) <- loops (unArg i) ts 333-- return (xs, SplitAt i ts) 334-- 335-- loops :: Int -> SplitTrees -> TCM ([Bool], RecordSplitTrees) 336-- loops i ts = do 337-- (xss, ts) <- unzip <$> do 338-- forM ts $ \ (c, t) -> do 339-- (xs, t) <- loop t 340-- (isRC, n) <- getEtaAndArity c 341-- let (xs0, rest) = splitAt i xs 342-- (xs1, xs2) = splitAt n rest 343-- x = isRC && and xs1 344-- xs' = xs0 ++ x : xs2 345-- return (xs, (RecordSplitNode c n x, t)) 346-- return (foldl1 (zipWith (&&)) xss, ts) 347 348-- | Bottom-up procedure to record-pattern-translate split tree. 349translateSplitTree :: SplitTree -> TCM SplitTree 350translateSplitTree = snd <.> loop 351 where 352 353 -- @loop t = return (xs, t')@ returns the translated split tree @t'@ 354 -- plus the status @xs@ of the clause variables 355 -- True = variable will never be split on in @t'@ (virgin variable) 356 -- False = variable will be spilt on in @t'@ 357 loop :: SplitTree -> TCM ([Bool], SplitTree) 358 loop = \case 359 SplittingDone n -> 360 -- start with n virgin variables 361 return (replicate n True, SplittingDone n) 362 SplitAt i lz ts -> do 363 (x, xs, ts) <- loops (unArg i) ts 364 -- if we case on record constructor, drop case 365 let t' = if x then 366 case ts of 367 [(c,t)] -> t 368 _ -> __IMPOSSIBLE__ 369 -- else retain case 370 else SplitAt i lz ts 371 return (xs, t') 372 373 -- @loops i ts = return (x, xs, ts')@ cf. @loop@ 374 -- @x@ says wether at arg @i@ we have a record pattern split 375 -- that can be removed 376 loops :: Int -> SplitTrees -> TCM (Bool, [Bool], SplitTrees) 377 loops i ts = do 378 -- note: ts not empty 379 (rs, xss, ts) <- unzip3 <$> do 380 forM ts $ \ (c, t) -> do 381 (xs, t) <- loop t 382 (isRC, n) <- getEtaAndArity c 383 -- now drop variables from i to i+n-1 384 let (xs0, rest) = splitAt i xs 385 (xs1, xs2) = splitAt n rest 386 -- if all dropped variables are virgins and we are record cons. 387 -- then new variable x is also virgin 388 -- and we can translate away the split 389 x = isRC && and xs1 390 -- xs' = updated variables 391 xs' = xs0 ++ x : xs2 392 -- delete splits from t if record match 393 t' = if x then dropFrom i (n - 1) t else t 394 return (x, xs', (c, t')) 395 -- x = did we split on a record constructor? 396 let x = and rs 397 -- invariant: if record constructor, then exactly one constructor 398 if x then unless (rs == [True]) __IMPOSSIBLE__ 399 -- else no record constructor 400 else when (or rs) __IMPOSSIBLE__ 401 return (x, conjColumns xss, ts) 402 403-- | @dropFrom i n@ drops arguments @j@ with @j < i + n@ and @j >= i@. 404-- NOTE: @n@ can be negative, in which case arguments are inserted. 405class DropFrom a where 406 dropFrom :: Int -> Int -> a -> a 407 408instance DropFrom (SplitTree' c) where 409 dropFrom i n = \case 410 SplittingDone m -> SplittingDone (m - n) 411 SplitAt x@(Arg ai j) lz ts 412 | j >= i + n -> SplitAt (Arg ai $ j - n) lz $ dropFrom i n ts 413 | j < i -> SplitAt x lz $ dropFrom i n ts 414 | otherwise -> __IMPOSSIBLE__ 415 416instance DropFrom (c, SplitTree' c) where 417 dropFrom i n (c, t) = (c, dropFrom i n t) 418 419instance DropFrom a => DropFrom [a] where 420 dropFrom i n ts = map (dropFrom i n) ts 421 422{- 423-- | Check if a split is on a record constructor, and return the projections 424-- if yes. 425isRecordSplit :: SplitTrees -> TCM (Maybe ([QName], c)) 426isRecordSplit (Branches { conBranches = conMap 427 , litBranches = litMap 428 , catchAllBranch = Nothing }) 429 | Map.null litBranches 430 , [(con,br)] <- Map.toList conMap = do 431 isRC <- isRecordConstructor con 432 case isRC of 433 Just (r, Record { recFields = fs }) -> return $ Just (map unArg fs, br) 434 Just (r, _) -> __IMPOSSIBLE__ 435 Nothing -> return Nothing 436isRecordSplit _ = return Nothing 437 438-} 439 440 441--------------------------------------------------------------------------- 442-- * Record pattern translation for function definitions 443--------------------------------------------------------------------------- 444 445-- | Replaces pattern matching on record constructors with uses of 446-- projection functions. Does not remove record constructor patterns 447-- which have sub-patterns containing non-record constructor or 448-- literal patterns. 449 450translateRecordPatterns :: Clause -> TCM Clause 451translateRecordPatterns clause = do 452 -- ps: New patterns, in left-to-right order, in the context of the 453 -- old RHS. 454 455 -- s: Partial substitution taking the old pattern variables 456 -- (including dot patterns; listed from left to right) to terms in 457 -- the context of the new RHS. 458 459 -- cs: List of changes, with types in the context of the old 460 -- telescope. 461 462 (ps, s, cs) <- runRecPatM $ translatePatterns $ unnumberPatVars $ namedClausePats clause 463 464 let -- Number of variables + dot patterns in new clause. 465 noNewPatternVars = size cs 466 467 s' = reverse s 468 mkSub s = s ++# raiseS noNewPatternVars 469 470 -- Substitution used to convert terms in the old RHS's 471 -- context to terms in the new RHS's context. 472 rhsSubst = mkSub s' -- NB:: Defined but not used 473 474 -- Substitution used to convert terms in the old telescope's 475 -- context to terms in the new RHS's context. 476 perm = fromMaybe __IMPOSSIBLE__ $ clausePerm clause 477 rhsSubst' = mkSub $ permute (reverseP perm) s' 478 -- TODO: Is it OK to replace the definition above with the 479 -- following one? 480 -- 481 -- rhsSubst' = mkSub $ permute (clausePerm clause) s 482 483 -- The old telescope, flattened and in textual left-to-right 484 -- order (i.e. the type signature for the variable which occurs 485 -- first in the list of patterns comes first). 486 flattenedOldTel = 487 permute (invertP __IMPOSSIBLE__ $ compactP perm) $ 488 zip (teleNames $ clauseTel clause) $ 489 flattenTel $ 490 clauseTel clause 491 492 -- The new telescope, still flattened, with types in the context 493 -- of the new RHS, in textual left-to-right order, and with 494 -- Nothing in place of dot patterns. 495 substTel = map . fmap . second . applySubst 496 newTel' = 497 substTel rhsSubst' $ 498 translateTel cs $ 499 flattenedOldTel 500 501 -- Permutation taking the new variable and dot patterns to the 502 -- new telescope. 503 newPerm = adjustForDotPatterns $ 504 reorderTel_ $ map (maybe __DUMMY_DOM__ snd) newTel' 505 -- It is important that __DUMMY_DOM__ does not mention any variable 506 -- (see the definition of reorderTel). 507 where 508 isDotP n = case List.genericIndex cs n of 509 Left DotP{} -> True 510 _ -> False 511 512 adjustForDotPatterns (Perm n is) = 513 Perm n (filter (not . isDotP) is) 514 515 -- Substitution used to convert terms in the new RHS's context 516 -- to terms in the new telescope's context. 517 lhsSubst' = renaming impossible (reverseP newPerm) 518 519 -- Substitution used to convert terms in the old telescope's 520 -- context to terms in the new telescope's context. 521 lhsSubst = applySubst lhsSubst' rhsSubst' 522 523 -- The new telescope. 524 newTel = 525 uncurry unflattenTel . unzip $ 526 map (fromMaybe __IMPOSSIBLE__) $ 527 permute newPerm $ 528 substTel lhsSubst' $ 529 newTel' 530 531 -- New clause. 532 c = clause 533 { clauseTel = newTel 534 , namedClausePats = numberPatVars __IMPOSSIBLE__ newPerm $ applySubst lhsSubst ps 535 , clauseBody = applySubst lhsSubst $ clauseBody clause 536 } 537 538 reportSDoc "tc.lhs.recpat" 20 $ vcat 539 [ "Original clause:" 540 , nest 2 $ inTopContext $ vcat 541 [ "delta =" <+> prettyTCM (clauseTel clause) 542 , "pats =" <+> text (show $ clausePats clause) 543 ] 544 , "Intermediate results:" 545 , nest 2 $ vcat 546 [ "ps =" <+> text (show ps) 547 , "s =" <+> prettyTCM s 548 , "cs =" <+> prettyTCM cs 549 , "flattenedOldTel =" <+> (text . show) flattenedOldTel 550 , "newTel' =" <+> (text . show) newTel' 551 , "newPerm =" <+> prettyTCM newPerm 552 ] 553 ] 554 555 reportSDoc "tc.lhs.recpat" 20 $ vcat 556 [ "lhsSubst' =" <+> (text . show) lhsSubst' 557 , "lhsSubst =" <+> (text . show) lhsSubst 558 , "newTel =" <+> prettyTCM newTel 559 ] 560 561 reportSDoc "tc.lhs.recpat" 10 $ 562 escapeContext impossible (size $ clauseTel clause) $ vcat 563 [ "Translated clause:" 564 , nest 2 $ vcat 565 [ "delta =" <+> prettyTCM (clauseTel c) 566 , "ps =" <+> text (show $ clausePats c) 567 , "body =" <+> text (show $ clauseBody c) 568 , "body =" <+> addContext (clauseTel c) (maybe "_|_" prettyTCM (clauseBody c)) 569 ] 570 ] 571 572 return c 573 574------------------------------------------------------------------------ 575-- Record pattern monad 576 577-- | A monad used to translate record patterns. 578-- 579-- The state records the number of variables produced so far, the 580-- reader records the total number of variables produced by the entire 581-- computation. Functions using this monad need to be sufficiently 582-- lazy in the reader component. 583 584newtype RecPatM a = RecPatM (TCMT (ReaderT Nat (StateT Nat IO)) a) 585 deriving (Functor, Applicative, Monad, 586 MonadIO, MonadTCM, HasOptions, 587 MonadTCEnv, MonadTCState) 588 589-- | Runs a computation in the 'RecPatM' monad. 590 591runRecPatM :: RecPatM a -> TCM a 592runRecPatM (RecPatM m) = 593 mapTCMT (\m -> do 594 (x, noVars) <- mfix $ \ ~(_, noVars) -> 595 runStateT (runReaderT m noVars) 0 596 return x) 597 m 598 599-- | Returns the next pattern variable, and the corresponding term. 600 601nextVar :: RecPatM (Pattern, Term) 602nextVar = RecPatM $ do 603 n <- lift get 604 lift $ put $ succ n 605 noVars <- lift ask 606 return (varP "r", var $ noVars - n - 1) 607 608------------------------------------------------------------------------ 609-- Types used to record changes to a clause 610 611-- | @VarPat@ stands for variable patterns, and @DotPat@ for dot 612-- patterns. 613 614data Kind = VarPat | DotPat 615 deriving Eq 616 617-- | @'Left' p@ means that a variable (corresponding to the pattern 618-- @p@, a variable or dot pattern) should be kept unchanged. @'Right' 619-- (n, x, t)@ means that @n 'VarPat'@ variables, and @n 'DotPat'@ dot 620-- patterns, should be removed, and a new variable, with the name @x@, 621-- inserted instead. The type of the new variable is @t@. 622 623type Change = Either Pattern (Kind -> Nat, ArgName, Dom Type) 624type Changes = [Change] 625 626instance Pretty (Kind -> Nat) where 627 pretty f = 628 ("(VarPat:" P.<+> P.text (show $ f VarPat) P.<+> 629 "DotPat:" P.<+> P.text (show $ f DotPat)) <> ")" 630 631instance PrettyTCM (Kind -> Nat) where 632 prettyTCM = return . pretty 633 634instance PrettyTCM Change where 635 prettyTCM (Left p) = prettyTCM p 636 prettyTCM (Right (f, x, t)) = "Change" <+> prettyTCM f <+> text x <+> prettyTCM t 637 638-- | Record pattern trees. 639 640data RecordTree 641 = Leaf Pattern 642 -- ^ Corresponds to variable and dot patterns; contains the 643 -- original pattern. 644 | RecCon (Arg Type) [(Term -> Term, RecordTree)] 645 -- ^ @RecCon t args@ stands for a record constructor application: 646 -- @t@ is the type of the application, and the list contains a 647 -- projection function and a tree for every argument. 648 649------------------------------------------------------------------------ 650-- Record pattern trees 651 652-- | @projections t@ returns a projection for every non-dot leaf 653-- pattern in @t@. The term is the composition of the projection 654-- functions from the leaf to the root. 655-- 656-- Every term is tagged with its origin: a variable pattern or a dot 657-- pattern. 658 659projections :: RecordTree -> [(Term -> Term, Kind)] 660projections (Leaf (DotP{})) = [(id, DotPat)] 661projections (Leaf (VarP{})) = [(id, VarPat)] 662projections (Leaf _) = __IMPOSSIBLE__ 663projections (RecCon _ args) = 664 concatMap (\ (p, t) -> map (first (. p)) $ projections t) 665 args 666 667-- | Converts a record tree to a single pattern along with information 668-- about the deleted pattern variables. 669 670removeTree :: RecordTree -> RecPatM (Pattern, [Term], Changes) 671removeTree tree = do 672 (pat, x) <- nextVar 673 let ps = projections tree 674 s = map (\(p, _) -> p x) ps 675 676 count k = length $ filter ((== k) . snd) ps 677 678 return $ case tree of 679 Leaf p -> (p, s, [Left p]) 680 RecCon t _ -> (pat, s, [Right (count, "r", domFromArg t)]) 681 682------------------------------------------------------------------------ 683-- Translation of patterns 684 685-- | Removes record constructors from patterns. 686-- 687-- Returns the following things: 688-- 689-- * The new pattern. 690-- 691-- * A substitution which maps the /old/ pattern variables (in the 692-- order they occurred in the pattern; not including dot patterns) 693-- to terms (either the new name of the variable, or a projection 694-- applied to a new pattern variable). 695-- 696-- * A list explaining the changes to the variables bound in the 697-- pattern. 698-- 699-- Record patterns containing non-record constructor patterns are not 700-- translated (though their sub-patterns may be). 701-- 702-- Example: The pattern @rec1 (con1 a) (rec2 b c) (rec3 d)@ should 703-- yield the pattern @rec1 (con1 x) y z@, along with a substitution 704-- similar to @[x, proj2-1 y, proj2-2 y, proj3-1 z]@. 705-- 706-- This function assumes that literals are never of record type. 707 708translatePattern :: Pattern -> RecPatM (Pattern, [Term], Changes) 709translatePattern p@(ConP c ci ps) 710 -- Andreas, 2015-05-28 only translate implicit record patterns 711 | conPRecord ci , PatOSystem <- patOrigin (conPInfo ci) = do 712 r <- recordTree p 713 case r of 714 Left r -> r 715 Right t -> removeTree t 716 | otherwise = do 717 (ps, s, cs) <- translatePatterns ps 718 return (ConP c ci ps, s, cs) 719translatePattern p@(DefP o q ps) = do 720 (ps, s, cs) <- translatePatterns ps 721 return (DefP o q ps, s, cs) 722translatePattern p@VarP{} = removeTree (Leaf p) 723translatePattern p@DotP{} = removeTree (Leaf p) 724translatePattern p@LitP{} = return (p, [], []) 725translatePattern p@ProjP{}= return (p, [], []) 726translatePattern p@IApplyP{}= return (p, [], []) 727 728translatePatterns :: [NamedArg Pattern] -> RecPatM ([NamedArg Pattern], [Term], Changes) 729translatePatterns ps = do 730 (ps', ss, cs) <- unzip3 <$> mapM (translatePattern . namedArg) ps 731 return (zipWith (\p -> fmap (p <$)) ps' ps, concat ss, concat cs) 732 733-- | Traverses a pattern and returns one of two things: 734-- 735-- * If there is no non-record constructor in the pattern, then 736-- @'Right' ps@ is returned, where @ps@ contains one projection for 737-- every variable in the input pattern (in the order they are 738-- encountered). 739-- 740-- * Otherwise the output is a computation returning the same kind of 741-- result as that coming from 'translatePattern'. (Computations are 742-- returned rather than values to ensure that variable numbers are 743-- allocated in the right order.) 744-- 745-- Assumes that literals are never of record type. 746 747recordTree :: 748 Pattern -> 749 RecPatM (Either (RecPatM (Pattern, [Term], Changes)) RecordTree) 750-- Andreas, 2015-05-28 only translate implicit record patterns 751recordTree p@(ConP c ci ps) | conPRecord ci , PatOSystem <- patOrigin (conPInfo ci) = do 752 let t = fromMaybe __IMPOSSIBLE__ $ conPType ci 753 rs <- mapM (recordTree . namedArg) ps 754 case allRight rs of 755 Nothing -> 756 return $ Left $ do 757 (ps', ss, cs) <- unzip3 <$> mapM (either id removeTree) rs 758 return (ConP c ci (ps' `withNamedArgsFrom` ps), 759 concat ss, concat cs) 760 Just ts -> liftTCM $ do 761 t <- reduce t 762 reportSDoc "tc.rec" 45 $ vcat 763 [ "recordTree: " 764 , nest 2 $ "constructor pattern " <+> prettyTCM p <+> " has type " <+> prettyTCM t 765 ] 766 -- Andreas, 2018-03-03, see #2989: 767 -- The content of an @Arg@ might not be reduced (if @Arg@ is @Irrelevant@). 768 fields <- getRecordTypeFields =<< reduce (unArg t) 769-- let proj p = \x -> Def (unArg p) [defaultArg x] 770 let proj p = (`applyE` [Proj ProjSystem $ unDom p]) 771 return $ Right $ RecCon t $ zip (map proj fields) ts 772recordTree p@(ConP _ ci _) = return $ Left $ translatePattern p 773recordTree p@DefP{} = return $ Left $ translatePattern p 774recordTree p@VarP{} = return (Right (Leaf p)) 775recordTree p@DotP{} = return (Right (Leaf p)) 776recordTree p@LitP{} = return $ Left $ translatePattern p 777recordTree p@ProjP{}= return $ Left $ translatePattern p 778recordTree p@IApplyP{}= return $ Left $ translatePattern p 779 780------------------------------------------------------------------------ 781-- Translation of the clause telescope and body 782 783-- | Translates the telescope. 784 785translateTel 786 :: Changes 787 -- ^ Explanation of how the telescope should be changed. Types 788 -- should be in the context of the old telescope. 789 -> [(ArgName, Dom Type)] 790 -- ^ Old telescope, flattened, in textual left-to-right 791 -- order. 792 -> [Maybe (ArgName, Dom Type)] 793 -- ^ New telescope, flattened, in textual left-to-right order. 794 -- 'Nothing' is used to indicate the locations of dot patterns. 795translateTel (Left (DotP{}) : rest) tel = Nothing : translateTel rest tel 796translateTel (Right (n, x, t) : rest) tel = Just (x, t) : 797 translateTel rest 798 (drop (n VarPat) tel) 799translateTel (Left _ : rest) (t : tel) = Just t : translateTel rest tel 800translateTel [] [] = [] 801translateTel (Left _ : _) [] = __IMPOSSIBLE__ 802translateTel [] (_ : _) = __IMPOSSIBLE__ 803