1{-# LANGUAGE NondecreasingIndentation #-} 2 3module Agda.TypeChecking.With where 4 5import Control.Monad 6import Control.Monad.Writer (WriterT, runWriterT, tell) 7 8import Data.Either 9import qualified Data.List as List 10import Data.Maybe 11import Data.Foldable ( foldrM ) 12 13import Agda.Syntax.Common 14import Agda.Syntax.Internal as I 15import Agda.Syntax.Internal.Pattern 16import qualified Agda.Syntax.Abstract as A 17import Agda.Syntax.Abstract.Pattern as A 18import Agda.Syntax.Abstract.Views 19import Agda.Syntax.Info 20import Agda.Syntax.Position 21 22import Agda.TypeChecking.Monad 23import Agda.TypeChecking.Reduce 24import Agda.TypeChecking.Datatypes 25import Agda.TypeChecking.EtaContract 26import Agda.TypeChecking.Free 27import Agda.TypeChecking.Patterns.Abstract 28import Agda.TypeChecking.Pretty 29import Agda.TypeChecking.Primitive ( getRefl ) 30import Agda.TypeChecking.Records 31import Agda.TypeChecking.Substitute 32import Agda.TypeChecking.Telescope 33import Agda.TypeChecking.Telescope.Path 34 35import Agda.TypeChecking.Abstract 36import Agda.TypeChecking.Rules.LHS.Implicit 37import Agda.TypeChecking.Rules.LHS.Problem (ProblemEq(..)) 38 39import Agda.Utils.Functor 40import Agda.Utils.List 41import qualified Agda.Utils.List1 as List1 42import Agda.Utils.Maybe 43import Agda.Utils.Monad 44import Agda.Utils.Null (empty) 45import Agda.Utils.Permutation 46import Agda.Utils.Pretty (prettyShow) 47import qualified Agda.Utils.Pretty as P 48import Agda.Utils.Size 49 50import Agda.Utils.Impossible 51 52-- | Split pattern variables according to with-expressions. 53 54-- Input: 55-- 56-- [@Δ@] context of types and with-arguments. 57-- 58-- [@Δ ⊢ t@] type of rhs. 59-- 60-- [@Δ ⊢ vs : as@] with arguments and their types 61-- 62-- Output: 63-- 64-- [@Δ₁@] part of context needed for with arguments and their types. 65-- 66-- [@Δ₂@] part of context not needed for with arguments and their types. 67-- 68-- [@π@] permutation from Δ to Δ₁Δ₂ as returned by 'splitTelescope'. 69-- 70-- [@Δ₁Δ₂ ⊢ t'@] type of rhs under @π@ 71-- 72-- [@Δ₁ ⊢ vs' : as'@] with-arguments and their types depending only on @Δ₁@. 73 74splitTelForWith 75 -- Input: 76 :: Telescope -- ^ __@Δ@__ context of types and with-arguments. 77 -> Type -- ^ __@Δ ⊢ t@__ type of rhs. 78 -> [Arg (Term, EqualityView)] -- ^ __@Δ ⊢ vs : as@__ with arguments and their types. 79 -- Output: 80 -> ( Telescope -- @Δ₁@ part of context needed for with arguments and their types. 81 , Telescope -- @Δ₂@ part of context not needed for with arguments and their types. 82 , Permutation -- @π@ permutation from Δ to Δ₁Δ₂ as returned by 'splitTelescope'. 83 , Type -- @Δ₁Δ₂ ⊢ t'@ type of rhs under @π@ 84 , [Arg (Term, EqualityView)] -- @Δ₁ ⊢ vs' : as'@ with- and rewrite-arguments and types under @π@. 85 ) -- ^ (__@Δ₁@__,__@Δ₂@__,__@π@__,__@t'@__,__@vtys'@__) where 86-- 87-- [@Δ₁@] part of context needed for with arguments and their types. 88-- 89-- [@Δ₂@] part of context not needed for with arguments and their types. 90-- 91-- [@π@] permutation from Δ to Δ₁Δ₂ as returned by 'splitTelescope'. 92-- 93-- [@Δ₁Δ₂ ⊢ t'@] type of rhs under @π@ 94-- 95-- [@Δ₁ ⊢ vtys'@] with-arguments and their types under @π@. 96 97splitTelForWith delta t vtys = let 98 -- Split the telescope into the part needed to type the with arguments 99 -- and all the other stuff. 100 fv = allFreeVars vtys 101 SplitTel delta1 delta2 perm = splitTelescope fv delta 102 103 -- Δ₁Δ₂ ⊢ π : Δ 104 pi = renaming impossible (reverseP perm) 105 -- Δ₁ ⊢ ρ : Δ₁Δ₂ (We know that as does not depend on Δ₂.) 106 rho = strengthenS impossible $ size delta2 107 -- Δ₁ ⊢ ρ ∘ π : Δ 108 rhopi = composeS rho pi 109 110 -- We need Δ₁Δ₂ ⊢ t' 111 t' = applySubst pi t 112 -- and Δ₁ ⊢ vtys' 113 vtys' = applySubst rhopi vtys 114 115 in (delta1, delta2, perm, t', vtys') 116 117 118-- | Abstract with-expressions @vs@ to generate type for with-helper function. 119-- 120-- Each @EqualityType@, coming from a @rewrite@, will turn into 2 abstractions. 121 122withFunctionType 123 :: Telescope -- ^ @Δ₁@ context for types of with types. 124 -> [Arg (Term, EqualityView)] -- ^ @Δ₁,Δ₂ ⊢ vs : raise Δ₂ as@ with and rewrite-expressions and their type. 125 -> Telescope -- ^ @Δ₁ ⊢ Δ₂@ context extension to type with-expressions. 126 -> Type -- ^ @Δ₁,Δ₂ ⊢ b@ type of rhs. 127 -> [(Int,(Term,Term))] -- ^ @Δ₁,Δ₂ ⊢ [(i,(u0,u1))] : b boundary. 128 -> TCM (Type, Nat) 129 -- ^ @Δ₁ → wtel → Δ₂′ → b′@ such that 130 -- @[vs/wtel]wtel = as@ and 131 -- @[vs/wtel]Δ₂′ = Δ₂@ and 132 -- @[vs/wtel]b′ = b@. 133 -- Plus the final number of with-arguments. 134withFunctionType delta1 vtys delta2 b bndry = addContext delta1 $ do 135 136 reportSLn "tc.with.abstract" 20 $ "preparing for with-abstraction" 137 138 -- Normalize and η-contract the type @b@ of the rhs and the types @delta2@ 139 -- of the pattern variables not mentioned in @vs : as@. 140 let dbg n s x = reportSDoc "tc.with.abstract" n $ nest 2 $ text (s ++ " =") <+> prettyTCM x 141 142 d2b <- telePiPath_ delta2 b bndry 143 dbg 30 "Δ₂ → B" d2b 144 d2b <- normalise d2b 145 dbg 30 "normal Δ₂ → B" d2b 146 d2b <- etaContract d2b 147 dbg 30 "eta-contracted Δ₂ → B" d2b 148 149 vtys <- etaContract =<< normalise vtys 150 151 -- wd2db = wtel → [vs : as] (Δ₂ → B) 152 wd2b <- foldrM piAbstract d2b vtys 153 dbg 30 "wΓ → Δ₂ → B" wd2b 154 155 let nwithargs = countWithArgs (map (snd . unArg) vtys) 156 157 TelV wtel _ <- telViewUpTo nwithargs wd2b 158 159 -- select the boundary for "Δ₁" abstracting over "wΓ.Δ₂" 160 let bndry' = [(i - sd2,(lams u0, lams u1)) | (i,(u0,u1)) <- bndry, i >= sd2] 161 where sd2 = size delta2 162 lams u = teleNoAbs wtel (abstract delta2 u) 163 164 d1wd2b <- telePiPath_ delta1 wd2b bndry' 165 166 dbg 30 "Δ₁ → wΓ → Δ₂ → B" d1wd2b 167 168 return (d1wd2b, nwithargs) 169 170countWithArgs :: [EqualityView] -> Nat 171countWithArgs = sum . map countArgs 172 where 173 countArgs OtherType{} = 1 174 countArgs IdiomType{} = 2 175 countArgs EqualityType{} = 2 176 177-- | From a list of @with@ and @rewrite@ expressions and their types, 178-- compute the list of final @with@ expressions (after expanding the @rewrite@s). 179withArguments :: [Arg (Term, EqualityView)] -> 180 TCM [Arg Term] 181withArguments vtys = do 182 tss <- forM vtys $ \ (Arg info ts) -> fmap (map (Arg info)) $ case ts of 183 (v, OtherType a) -> pure [v] 184 (prf, eqt@(EqualityType s _eq _pars _t v _v')) -> pure [unArg v, prf] 185 (v, IdiomType t) -> do 186 mkRefl <- getRefl 187 pure [v, mkRefl (defaultArg v)] 188 pure (concat tss) 189 190-- | Compute the clauses for the with-function given the original patterns. 191buildWithFunction 192 :: [Name] -- ^ Names of the module parameters of the parent function. 193 -> QName -- ^ Name of the parent function. 194 -> QName -- ^ Name of the with-function. 195 -> Type -- ^ Types of the parent function. 196 -> Telescope -- ^ Context of parent patterns. 197 -> [NamedArg DeBruijnPattern] -- ^ Parent patterns. 198 -> Nat -- ^ Number of module parameters in parent patterns 199 -> Substitution -- ^ Substitution from parent lhs to with function lhs 200 -> Permutation -- ^ Final permutation. 201 -> Nat -- ^ Number of needed vars. 202 -> Nat -- ^ Number of with expressions. 203 -> [A.SpineClause] -- ^ With-clauses. 204 -> TCM [A.SpineClause] -- ^ With-clauses flattened wrt. parent patterns. 205buildWithFunction cxtNames f aux t delta qs npars withSub perm n1 n cs = mapM buildWithClause cs 206 where 207 -- Nested with-functions will iterate this function once for each parent clause. 208 buildWithClause (A.Clause (A.SpineLHS i _ allPs) inheritedPats rhs wh catchall) = do 209 let (ps, wps) = splitOffTrailingWithPatterns allPs 210 (wps0, wps1) = splitAt n wps 211 ps0 = map (updateNamedArg fromWithP) wps0 212 where 213 fromWithP (A.WithP _ p) = p 214 fromWithP _ = __IMPOSSIBLE__ 215 reportSDoc "tc.with" 50 $ "inheritedPats:" <+> vcat 216 [ prettyA p <+> "=" <+> prettyTCM v <+> ":" <+> prettyTCM a 217 | A.ProblemEq p v a <- inheritedPats 218 ] 219 (strippedPats, ps') <- stripWithClausePatterns cxtNames f aux t delta qs npars perm ps 220 reportSDoc "tc.with" 50 $ hang "strippedPats:" 2 $ 221 vcat [ prettyA p <+> "==" <+> prettyTCM v <+> (":" <+> prettyTCM t) 222 | A.ProblemEq p v t <- strippedPats ] 223 rhs <- buildRHS strippedPats rhs 224 let (ps1, ps2) = splitAt n1 ps' 225 let result = A.Clause (A.SpineLHS i aux $ ps1 ++ ps0 ++ ps2 ++ wps1) 226 (inheritedPats ++ strippedPats) 227 rhs wh catchall 228 reportSDoc "tc.with" 20 $ vcat 229 [ "buildWithClause returns" <+> prettyA result 230 ] 231 return result 232 233 buildRHS _ rhs@A.RHS{} = return rhs 234 buildRHS _ rhs@A.AbsurdRHS = return rhs 235 buildRHS _ (A.WithRHS q es cs) = A.WithRHS q es <$> 236 mapM ((A.spineToLhs . permuteNamedDots) <.> buildWithClause . A.lhsToSpine) cs 237 buildRHS strippedPats1 (A.RewriteRHS qes strippedPats2 rhs wh) = 238 flip (A.RewriteRHS qes (applySubst withSub $ strippedPats1 ++ strippedPats2)) wh <$> buildRHS [] rhs 239 240 -- The stripped patterns computed by buildWithClause lives in the context 241 -- of the top with-clause (of the current call to buildWithFunction). When 242 -- we recurse we expect inherited patterns to live in the context 243 -- of the innermost parent clause. Note that this makes them live in the 244 -- context of the with-function arguments before any pattern matching. We 245 -- need to update again once the with-clause patterns have been checked. 246 -- This happens in Rules.Def.checkClause before calling checkRHS. 247 permuteNamedDots :: A.SpineClause -> A.SpineClause 248 permuteNamedDots (A.Clause lhs strippedPats rhs wh catchall) = 249 A.Clause lhs (applySubst withSub strippedPats) rhs wh catchall 250 251 252-- The arguments of @stripWithClausePatterns@ are documented 253-- at its type signature. 254-- The following is duplicate information, but may help reading the examples below. 255-- 256-- [@Δ@] context bound by lhs of original function. 257-- [@f@] name of @with@-function. 258-- [@t@] type of the original function. 259-- [@qs@] internal patterns for original function. 260-- [@np@] number of module parameters in @qs@ 261-- [@π@] permutation taking @vars(qs)@ to @support(Δ)@. 262-- [@ps@] patterns in with clause (eliminating type @t@). 263-- [@ps'@] patterns for with function (presumably of type @Δ@). 264 265{-| @stripWithClausePatterns cxtNames parent f t Δ qs np π ps = ps'@ 266 267Example: 268 269@ 270 record Stream (A : Set) : Set where 271 coinductive 272 constructor delay 273 field force : A × Stream A 274 275 record SEq (s t : Stream A) : Set where 276 coinductive 277 field 278 ~force : let a , as = force s 279 b , bs = force t 280 in a ≡ b × SEq as bs 281 282 test : (s : Nat × Stream Nat) (t : Stream Nat) → SEq (delay s) t → SEq t (delay s) 283 ~force (test (a , as) t p) with force t 284 ~force (test (suc n , as) t p) | b , bs = ? 285@ 286 287With function: 288 289@ 290 f : (t : Stream Nat) (w : Nat × Stream Nat) (a : Nat) (as : Stream Nat) 291 (p : SEq (delay (a , as)) t) → (fst w ≡ a) × SEq (snd w) as 292 293 Δ = t a as p -- reorder to bring with-relevant (= needed) vars first 294 π = a as t p → Δ 295 qs = (a , as) t p ~force 296 ps = (suc n , as) t p ~force 297 ps' = (suc n) as t p 298@ 299 300Resulting with-function clause is: 301 302@ 303 f t (b , bs) (suc n) as t p 304@ 305 306Note: stripWithClausePatterns factors __@ps@__ through __@qs@__, thus 307 308@ 309 ps = qs[ps'] 310@ 311 312where @[..]@ is to be understood as substitution. 313The projection patterns have vanished from __@ps'@__ (as they are already in __@qs@__). 314-} 315 316stripWithClausePatterns 317 :: [Name] -- ^ __@cxtNames@__ names of the module parameters of the parent function 318 -> QName -- ^ __@parent@__ name of the parent function. 319 -> QName -- ^ __@f@__ name of with-function. 320 -> Type -- ^ __@t@__ top-level type of the original function. 321 -> Telescope -- ^ __@Δ@__ context of patterns of parent function. 322 -> [NamedArg DeBruijnPattern] -- ^ __@qs@__ internal patterns for original function. 323 -> Nat -- ^ __@npars@__ number of module parameters in @qs@. 324 -> Permutation -- ^ __@π@__ permutation taking @vars(qs)@ to @support(Δ)@. 325 -> [NamedArg A.Pattern] -- ^ __@ps@__ patterns in with clause (eliminating type @t@). 326 -> TCM ([A.ProblemEq], [NamedArg A.Pattern]) -- ^ __@ps'@__ patterns for with function (presumably of type @Δ@). 327stripWithClausePatterns cxtNames parent f t delta qs npars perm ps = do 328 -- Andreas, 2014-03-05 expand away pattern synoyms (issue 1074) 329 ps <- expandPatternSynonyms ps 330 -- Ulf, 2016-11-16 Issue 2303: We need the module parameter 331 -- instantiations from qs, so we make sure 332 -- that t is the top-level type of the parent function and add patterns for 333 -- the module parameters to ps before stripping. 334 let paramPat i _ = A.VarP $ A.mkBindName $ indexWithDefault __IMPOSSIBLE__ cxtNames i 335 ps' = zipWith (fmap . fmap . paramPat) [0..] (take npars qs) ++ ps 336 psi <- insertImplicitPatternsT ExpandLast ps' t 337 reportSDoc "tc.with.strip" 10 $ vcat 338 [ "stripping patterns" 339 , nest 2 $ "t = " <+> prettyTCM t 340 , nest 2 $ "ps = " <+> fsep (punctuate comma $ map prettyA ps) 341 , nest 2 $ "ps' = " <+> fsep (punctuate comma $ map prettyA ps') 342 , nest 2 $ "psi = " <+> fsep (punctuate comma $ map prettyA psi) 343 , nest 2 $ "qs = " <+> fsep (punctuate comma $ map (prettyTCM . namedArg) qs) 344 , nest 2 $ "perm= " <+> text (show perm) 345 ] 346 347 -- Andreas, 2015-11-09 Issue 1710: self starts with parent-function, not with-function! 348 (ps', strippedPats) <- runWriterT $ strip (Def parent []) t psi qs 349 reportSDoc "tc.with.strip" 50 $ nest 2 $ 350 "strippedPats:" <+> vcat [ prettyA p <+> "=" <+> prettyTCM v <+> ":" <+> prettyTCM a | A.ProblemEq p v a <- strippedPats ] 351 let psp = permute perm ps' 352 reportSDoc "tc.with.strip" 10 $ vcat 353 [ nest 2 $ "ps' = " <+> fsep (punctuate comma $ map prettyA ps') 354 , nest 2 $ "psp = " <+> fsep (punctuate comma $ map prettyA $ psp) 355 ] 356 return (strippedPats, psp) 357 where 358 359 -- We need to get the correct hiding from the lhs context. The unifier may have moved bindings 360 -- sites around so we can't trust the hiding of the parent pattern variables. We should preserve 361 -- the origin though. 362 varArgInfo = \ x -> let n = dbPatVarIndex x in 363 if n < length infos then infos !! n else __IMPOSSIBLE__ 364 where infos = reverse $ map getArgInfo $ telToList delta 365 366 setVarArgInfo x p = setOrigin (getOrigin p) $ setArgInfo (varArgInfo x) p 367 368 strip 369 :: Term -- Self. 370 -> Type -- The type to be eliminated. 371 -> [NamedArg A.Pattern] -- With-clause patterns. 372 -> [NamedArg DeBruijnPattern] -- Parent-clause patterns with de Bruijn indices relative to Δ. 373 -> WriterT [ProblemEq] TCM [NamedArg A.Pattern] 374 -- With-clause patterns decomposed by parent-clause patterns. 375 -- Also outputs named dot patterns from the parent clause that 376 -- we need to add let-bindings for. 377 378 -- Case: out of with-clause patterns. 379 strip self t [] qs@(_ : _) = do 380 reportSDoc "tc.with.strip" 15 $ vcat 381 [ "strip (out of A.Patterns)" 382 , nest 2 $ "qs =" <+> fsep (punctuate comma $ map (prettyTCM . namedArg) qs) 383 , nest 2 $ "self=" <+> prettyTCM self 384 , nest 2 $ "t =" <+> prettyTCM t 385 ] 386 -- Andreas, 2015-06-11, issue 1551: 387 -- As the type t develops, we need to insert more implicit patterns, 388 -- due to copatterns / flexible arity. 389 ps <- liftTCM $ insertImplicitPatternsT ExpandLast [] t 390 if null ps then 391 typeError $ GenericError $ "Too few arguments given in with-clause" 392 else strip self t ps qs 393 394 -- Case: out of parent-clause patterns. 395 -- This is only ok if all remaining with-clause patterns 396 -- are implicit patterns (we inserted too many). 397 strip _ _ ps [] = do 398 let implicit (A.WildP{}) = True 399 implicit (A.ConP ci _ _) = conPatOrigin ci == ConOSystem 400 implicit _ = False 401 unless (all (implicit . namedArg) ps) $ 402 typeError $ GenericError $ "Too many arguments given in with-clause" 403 return [] 404 405 -- Case: both parent-clause pattern and with-clause pattern present. 406 -- Make sure they match, and decompose into subpatterns. 407 strip self t (p0 : ps) qs@(q : _) 408 | A.AsP _ x p <- namedArg p0 = do 409 (a, _) <- mustBePi t 410 let v = patternToTerm (namedArg q) 411 tell [ProblemEq (A.VarP x) v a] 412 strip self t (fmap (p <$) p0 : ps) qs 413 strip self t ps0@(p0 : ps) qs0@(q : qs) = do 414 p <- liftTCM $ (traverse . traverse) expandLitPattern p0 415 reportSDoc "tc.with.strip" 15 $ vcat 416 [ "strip" 417 , nest 2 $ "ps0 =" <+> fsep (punctuate comma $ map prettyA ps0) 418 , nest 2 $ "exp =" <+> prettyA p 419 , nest 2 $ "qs0 =" <+> fsep (punctuate comma $ map (prettyTCM . namedArg) qs0) 420 , nest 2 $ "self=" <+> prettyTCM self 421 , nest 2 $ "t =" <+> prettyTCM t 422 ] 423 case namedArg q of 424 ProjP o d -> case A.isProjP p of 425 Just (o', AmbQ ds) -> do 426 -- We assume here that neither @o@ nor @o'@ can be @ProjSystem@. 427 if o /= o' then liftTCM $ mismatchOrigin o o' else do 428 -- Andreas, 2016-12-28, issue #2360: 429 -- We disambiguate the projection in the with clause 430 -- to the projection in the parent clause. 431 d <- liftTCM $ getOriginalProjection d 432 found <- anyM ds $ \ d' -> liftTCM $ (Just d ==) . fmap projOrig <$> isProjection d' 433 if not found then mismatch else do 434 (self1, t1, ps) <- liftTCM $ do 435 t <- reduce t 436 (_, self1, t1) <- fromMaybe __IMPOSSIBLE__ <$> projectTyped self t o d 437 -- Andreas, 2016-01-21, issue #1791 438 -- The type of a field might start with hidden quantifiers. 439 -- So we may have to insert more implicit patterns here. 440 ps <- insertImplicitPatternsT ExpandLast ps t1 441 return (self1, t1, ps) 442 strip self1 t1 ps qs 443 Nothing -> mismatch 444 445 -- We can safely strip dots from variables. The unifier will put them back when required. 446 VarP _ x | A.DotP _ u <- namedArg p 447 , A.Var y <- unScope u -> do 448 (setVarArgInfo x (setNamedArg p $ A.VarP $ A.mkBindName y) :) <$> 449 recurse (var (dbPatVarIndex x)) 450 451 VarP _ x -> 452 (setVarArgInfo x p :) <$> recurse (var (dbPatVarIndex x)) 453 454 IApplyP _ _ _ x -> 455 (setVarArgInfo x p :) <$> recurse (var (dbPatVarIndex x)) 456 457 DefP{} -> typeError $ GenericError $ "with clauses not supported in the presence of hcomp patterns" -- TODO this should actually be impossible 458 459 DotP i v -> do 460 (a, _) <- mustBePi t 461 tell [ProblemEq (namedArg p) v a] 462 case v of 463 Var x [] | PatOVar{} <- patOrigin i 464 -> (p :) <$> recurse (var x) 465 _ -> (makeWildP p :) <$> recurse v 466 467 q'@(ConP c ci qs') -> do 468 reportSDoc "tc.with.strip" 60 $ 469 "parent pattern is constructor " <+> prettyTCM c 470 (a, b) <- mustBePi t 471 -- The type of the current pattern is a datatype. 472 Def d es <- liftTCM $ reduce (unEl $ unDom a) 473 let us = fromMaybe __IMPOSSIBLE__ $ allApplyElims es 474 -- Get the original constructor and field names. 475 c <- either __IMPOSSIBLE__ (`withRangeOf` c) <$> do liftTCM $ getConForm $ conName c 476 477 case namedArg p of 478 479 -- Andreas, 2015-07-07 Issue 1606. 480 -- Agda sometimes changes a record of dot patterns into a dot pattern, 481 -- so the user should be allowed to do likewise. 482 -- Jesper, 2017-11-16. This is now also allowed for data constructors. 483 A.DotP r e -> do 484 tell [ProblemEq (A.DotP r e) (patternToTerm q') a] 485 ps' <- 486 case appView e of 487 -- If dot-pattern is an application of the constructor, try to preserve the 488 -- arguments. 489 Application (A.Con (A.AmbQ cs')) es -> do 490 cs' <- liftTCM $ List1.rights <$> mapM getConForm cs' 491 unless (c `elem` cs') mismatch 492 return $ (map . fmap . fmap) (A.DotP r) es 493 _ -> return $ map (unnamed (A.WildP empty) <$) qs' 494 stripConP d us b c ConOCon qs' ps' 495 496 -- Andreas, 2016-12-29, issue #2363. 497 -- Allow _ to stand for the corresponding parent pattern. 498 A.WildP{} -> do 499 -- Andreas, 2017-10-13, issue #2803: 500 -- Delete the name, since it can confuse insertImplicitPattern. 501 let ps' = map (unnamed (A.WildP empty) <$) qs' 502 stripConP d us b c ConOCon qs' ps' 503 504 -- Jesper, 2018-05-13, issue #2998. 505 -- We also allow turning a constructor pattern into a variable. 506 -- In general this is not type-safe since the types of some variables 507 -- in the constructor pattern may have changed, so we have to 508 -- re-check these solutions when checking the with clause (see LHS.hs) 509 A.VarP x -> do 510 tell [ProblemEq (A.VarP x) (patternToTerm q') a] 511 let ps' = map (unnamed (A.WildP empty) <$) qs' 512 stripConP d us b c ConOCon qs' ps' 513 514 A.ConP _ (A.AmbQ cs') ps' -> do 515 -- Check whether the with-clause constructor can be (possibly trivially) 516 -- disambiguated to be equal to the parent-clause constructor. 517 -- Andreas, 2017-08-13, herein, ignore abstract constructors. 518 cs' <- liftTCM $ List1.rights <$> mapM getConForm cs' 519 unless (c `elem` cs') mismatch 520 -- Strip the subpatterns ps' and then continue. 521 stripConP d us b c ConOCon qs' ps' 522 523 A.RecP _ fs -> caseMaybeM (liftTCM $ isRecord d) mismatch $ \ def -> do 524 ps' <- liftTCM $ insertMissingFieldsFail d (const $ A.WildP empty) fs 525 (map argFromDom $ recordFieldNames def) 526 stripConP d us b c ConORec qs' ps' 527 528 p@(A.PatternSynP pi' c' ps') -> do 529 reportSDoc "impossible" 10 $ 530 "stripWithClausePatterns: encountered pattern synonym " <+> prettyA p 531 __IMPOSSIBLE__ 532 533 p -> do 534 reportSDoc "tc.with.strip" 60 $ 535 text $ "with clause pattern is " ++ show p 536 mismatch 537 538 LitP _ lit -> case namedArg p of 539 A.LitP _ lit' | lit == lit' -> recurse $ Lit lit 540 A.WildP{} -> recurse $ Lit lit 541 542 p@(A.PatternSynP pi' c' [ps']) -> do 543 reportSDoc "impossible" 10 $ 544 "stripWithClausePatterns: encountered pattern synonym " <+> prettyA p 545 __IMPOSSIBLE__ 546 547 _ -> mismatch 548 where 549 recurse v = do 550 -- caseMaybeM (liftTCM $ isPath t) (return ()) $ \ _ -> 551 -- typeError $ GenericError $ 552 -- "With-clauses currently not supported under Path abstraction." 553 554 let piOrPathApplyM t v = do 555 (TelV tel t', bs) <- telViewUpToPathBoundaryP 1 t 556 unless (size tel == 1) $ __IMPOSSIBLE__ 557 return (teleElims tel bs, subst 0 v t') 558 (e, t') <- piOrPathApplyM t v 559 strip (self `applyE` e) t' ps qs 560 561 mismatch :: forall m a. (MonadAddContext m, MonadTCError m) => m a 562 mismatch = addContext delta $ typeError $ 563 WithClausePatternMismatch (namedArg p0) q 564 mismatchOrigin o o' = addContext delta . typeError . GenericDocError =<< fsep 565 [ "With clause pattern" 566 , prettyA p0 567 , "is not an instance of its parent pattern" 568 , P.fsep <$> prettyTCMPatterns [q] 569 , text $ "since the parent pattern is " ++ prettyProjOrigin o ++ 570 " and the with clause pattern is " ++ prettyProjOrigin o' 571 ] 572 prettyProjOrigin ProjPrefix = "a prefix projection" 573 prettyProjOrigin ProjPostfix = "a postfix projection" 574 prettyProjOrigin ProjSystem = __IMPOSSIBLE__ 575 576 -- Make a WildP, keeping arg. info. 577 makeWildP :: NamedArg A.Pattern -> NamedArg A.Pattern 578 makeWildP = updateNamedArg $ const $ A.WildP patNoRange 579 580 -- case I.ConP / A.ConP 581 stripConP 582 :: QName -- Data type name of this constructor pattern. 583 -> [Arg Term] -- Data type arguments of this constructor pattern. 584 -> Abs Type -- Type the remaining patterns eliminate. 585 -> ConHead -- Constructor of this pattern. 586 -> ConInfo -- Constructor info of this pattern (constructor/record). 587 -> [NamedArg DeBruijnPattern] -- Argument patterns (parent clause). 588 -> [NamedArg A.Pattern] -- Argument patterns (with clause). 589 -> WriterT [ProblemEq] TCM [NamedArg A.Pattern] -- Stripped patterns. 590 stripConP d us b c ci qs' ps' = do 591 592 -- Get the type and number of parameters of the constructor. 593 Defn {defType = ct, theDef = Constructor{conPars = np}} <- getConInfo c 594 -- Compute the argument telescope for the constructor 595 let ct' = ct `piApply` take np us 596 TelV tel' _ <- liftTCM $ telViewPath ct' 597 -- (TelV tel' _, _boundary) <- liftTCM $ telViewPathBoundaryP ct' 598 599 reportSDoc "tc.with.strip" 20 $ 600 vcat [ "ct = " <+> prettyTCM ct 601 , "ct' = " <+> prettyTCM ct' 602 , "np = " <+> text (show np) 603 , "us = " <+> prettyList (map prettyTCM us) 604 , "us' = " <+> prettyList (map prettyTCM $ take np us) 605 ] 606 607 -- TODO Andrea: preserve IApplyP patterns in v, see _boundary? 608 -- Compute the new type 609 let v = Con c ci [ Apply $ Arg info (var i) | (i, Arg info _) <- zip (downFrom $ size qs') qs' ] 610 t' = tel' `abstract` absApp (raise (size tel') b) v 611 self' = tel' `abstract` apply1 (raise (size tel') self) v -- Issue 1546 612 613 reportSDoc "tc.with.strip" 15 $ sep 614 [ "inserting implicit" 615 , nest 2 $ prettyList $ map prettyA (ps' ++ ps) 616 , nest 2 $ ":" <+> prettyTCM t' 617 ] 618 619 -- Insert implicit patterns (just for the constructor arguments) 620 psi' <- liftTCM $ insertImplicitPatterns ExpandLast ps' tel' 621 unless (size psi' == size tel') $ typeError $ 622 WrongNumberOfConstructorArguments (conName c) (size tel') (size psi') 623 624 -- Andreas, Ulf, 2016-06-01, Ulf's variant at issue #679 625 -- Since instantiating the type with a constructor pattern 626 -- can reveal more hidden arguments, we need to insert them here. 627 psi <- liftTCM $ insertImplicitPatternsT ExpandLast (psi' ++ ps) t' 628 629 -- Keep going 630 strip self' t' psi (qs' ++ qs) 631 632-- | Construct the display form for a with function. It will display 633-- applications of the with function as applications to the original function. 634-- For instance, 635-- 636-- @ 637-- aux a b c 638-- @ 639-- 640-- as 641-- 642-- @ 643-- f (suc a) (suc b) | c 644-- @ 645withDisplayForm 646 :: QName 647 -- ^ The name of parent function. 648 -> QName 649 -- ^ The name of the @with@-function. 650 -> Telescope 651 -- ^ __@Δ₁@__ The arguments of the @with@ function before the @with@ expressions. 652 -> Telescope 653 -- ^ __@Δ₂@__ The arguments of the @with@ function after the @with@ expressions. 654 -> Nat 655 -- ^ __@n@__ The number of @with@ expressions. 656 -> [NamedArg DeBruijnPattern] 657 -- ^ __@qs@__ The parent patterns. 658 -> Permutation 659 -- ^ __@perm@__ Permutation to split into needed and unneeded vars. 660 -> Permutation 661 -- ^ __@lhsPerm@__ Permutation reordering the variables in parent patterns. 662 -> TCM DisplayForm 663withDisplayForm f aux delta1 delta2 n qs perm@(Perm m _) lhsPerm = do 664 665 -- Compute the arity of the display form. 666 let arity0 = n + size delta1 + size delta2 667 -- The currently free variables have to be added to the front. 668 topArgs <- raise arity0 <$> getContextArgs 669 let top = length topArgs 670 arity = arity0 + top 671 672 -- Build the rhs of the display form. 673 wild <- freshNoName_ <&> \ x -> Def (qualify_ x) [] 674 let -- Convert the parent patterns to terms. 675 tqs0 = patsToElims qs 676 -- Build a substitution to replace the parent pattern vars 677 -- by the pattern vars of the with-function. 678 (ys0, ys1) = splitAt (size delta1) $ permute perm $ downFrom m 679 ys = reverse (map Just ys0 ++ replicate n Nothing ++ map Just ys1) 680 ++ map (Just . (m +)) [0..top-1] 681 rho = sub top ys wild 682 tqs = applySubst rho tqs0 683 -- Build the arguments to the with function. 684 es = map (Apply . fmap DTerm) topArgs ++ tqs 685 withArgs = map var $ take n $ downFrom $ size delta2 + n 686 dt = DWithApp (DDef f es) (map DTerm withArgs) [] 687 688 -- Build the lhs of the display form and finish. 689 -- @var 0@ is the pattern variable (hole). 690 let display = Display arity [Apply $ defaultArg $ var i | i <- downFrom arity] dt 691 692 -- Debug printing. 693 let addFullCtx = addContext delta1 694 . flip (foldr addContext) (for [1..n] $ \ i -> "w" ++ show i) 695 . addContext delta2 696 reportSDoc "tc.with.display" 20 $ vcat 697 [ "withDisplayForm" 698 , nest 2 $ vcat 699 [ "f =" <+> text (prettyShow f) 700 , "aux =" <+> text (prettyShow aux) 701 , "delta1 =" <+> prettyTCM delta1 702 , "delta2 =" <+> do addContext delta1 $ prettyTCM delta2 703 , "n =" <+> text (show n) 704 , "perm =" <+> text (show perm) 705 , "top =" <+> do addFullCtx $ prettyTCM topArgs 706 , "qs =" <+> prettyList (map pretty qs) 707 , "qsToTm =" <+> prettyTCM tqs0 -- ctx would be permuted form of delta1 ++ delta2 708 , "ys =" <+> text (show ys) 709 , "rho =" <+> text (prettyShow rho) 710 , "qs[rho]=" <+> do addFullCtx $ prettyTCM tqs 711 , "dt =" <+> do addFullCtx $ prettyTCM dt 712 ] 713 ] 714 reportSDoc "tc.with.display" 70 $ nest 2 $ vcat 715 [ "raw =" <+> text (show display) 716 ] 717 718 return display 719 where 720 -- Ulf, 2014-02-19: We need to rename the module parameters as well! (issue1035) 721 -- sub top ys wild = map term [0 .. m - 1] ++# raiseS (length qs) 722 -- Andreas, 2015-10-28: Yes, but properly! (Issue 1407) 723 sub top ys wild = parallelS $ map term [0 .. m + top - 1] 724 where 725 term i = maybe wild var $ List.elemIndex (Just i) ys 726 727-- Andreas, 2014-12-05 refactored using numberPatVars 728-- Andreas, 2013-02-28 modeled after Coverage/Match/buildMPatterns 729patsToElims :: [NamedArg DeBruijnPattern] -> [I.Elim' DisplayTerm] 730patsToElims = map $ toElim . fmap namedThing 731 where 732 toElim :: Arg DeBruijnPattern -> I.Elim' DisplayTerm 733 toElim (Arg ai p) = case p of 734 ProjP o d -> I.Proj o d 735 p -> I.Apply $ Arg ai $ toTerm p 736 737 toTerms :: [NamedArg DeBruijnPattern] -> [Arg DisplayTerm] 738 toTerms = map $ fmap $ toTerm . namedThing 739 740 toTerm :: DeBruijnPattern -> DisplayTerm 741 toTerm p = case patOrigin $ fromMaybe __IMPOSSIBLE__ $ patternInfo p of 742 PatOSystem -> toDisplayPattern p 743 PatOSplit -> toDisplayPattern p 744 PatOVar{} -> toVarOrDot p 745 PatODot -> DDot $ patternToTerm p 746 PatOWild -> toVarOrDot p 747 PatOCon -> toDisplayPattern p 748 PatORec -> toDisplayPattern p 749 PatOLit -> toDisplayPattern p 750 PatOAbsurd -> toDisplayPattern p -- see test/Succeed/Issue2849.agda 751 752 toDisplayPattern :: DeBruijnPattern -> DisplayTerm 753 toDisplayPattern = \case 754 IApplyP _ _ _ x -> DTerm $ var $ dbPatVarIndex x -- TODO, should be an Elim' DisplayTerm ? 755 ProjP _ d -> __IMPOSSIBLE__ 756 VarP i x -> DTerm $ var $ dbPatVarIndex x 757 DotP i t -> DDot $ t 758 p@(ConP c cpi ps) -> DCon c (fromConPatternInfo cpi) $ toTerms ps 759 LitP i l -> DTerm $ Lit l 760 DefP _ q ps -> DDef q $ map Apply $ toTerms ps 761 762 toVarOrDot :: DeBruijnPattern -> DisplayTerm 763 toVarOrDot p = case patternToTerm p of 764 Var i [] -> DTerm $ var i 765 t -> DDot t 766