1{-# LANGUAGE NondecreasingIndentation #-} 2 3module Agda.TypeChecking.Rules.Record where 4 5import Prelude hiding (null) 6 7import Control.Monad 8import Data.Maybe 9import qualified Data.Set as Set 10 11import Agda.Interaction.Options 12 13import qualified Agda.Syntax.Abstract as A 14import Agda.Syntax.Common 15import Agda.Syntax.Internal 16import Agda.Syntax.Internal.Pattern 17import Agda.Syntax.Position 18import qualified Agda.Syntax.Info as Info 19 20import Agda.TypeChecking.Monad 21import Agda.TypeChecking.Primitive 22import Agda.TypeChecking.Rewriting.Confluence 23import Agda.TypeChecking.Substitute 24import Agda.TypeChecking.Telescope 25import Agda.TypeChecking.Reduce 26import Agda.TypeChecking.Positivity.Occurrence 27import Agda.TypeChecking.Pretty 28import Agda.TypeChecking.Polarity 29import Agda.TypeChecking.Warnings 30import Agda.TypeChecking.Irrelevance 31import Agda.TypeChecking.CompiledClause (hasProjectionPatterns) 32import Agda.TypeChecking.CompiledClause.Compile 33 34import Agda.TypeChecking.Rules.Data ( getGeneralizedParameters, bindGeneralizedParameters, bindParameters, fitsIn, forceSort, 35 defineCompData, defineTranspOrHCompForFields ) 36import Agda.TypeChecking.Rules.Term ( isType_ ) 37import {-# SOURCE #-} Agda.TypeChecking.Rules.Decl (checkDecl) 38 39import Agda.Utils.Maybe 40import Agda.Utils.Monad 41import Agda.Utils.Null 42import Agda.Utils.Permutation 43import Agda.Utils.POMonoid 44import Agda.Utils.Pretty (render) 45import qualified Agda.Utils.Pretty as P 46import Agda.Utils.Size 47import Agda.Utils.WithDefault 48 49import Agda.Utils.Impossible 50 51--------------------------------------------------------------------------- 52-- * Records 53--------------------------------------------------------------------------- 54 55-- | @checkRecDef i name con ps contel fields@ 56-- 57-- [@name@] Record type identifier. 58-- 59-- [@con@] Maybe constructor name and info. 60-- 61-- [@ps@] Record parameters. 62-- 63-- [@contel@] Approximate type of constructor (@fields@ -> Set). 64-- Does not include record parameters. 65-- 66-- [@fields@] List of field signatures. 67-- 68checkRecDef 69 :: A.DefInfo -- ^ Position and other info. 70 -> QName -- ^ Record type identifier. 71 -> UniverseCheck -- ^ Check universes? 72 -> A.RecordDirectives -- ^ (Co)Inductive, (No)Eta, (Co)Pattern, Constructor? 73 -> A.DataDefParams -- ^ Record parameters. 74 -> A.Expr -- ^ Approximate type of constructor (@fields@ -> Set). 75 -- Does not include record parameters. 76 -> [A.Field] -- ^ Field signatures. 77 -> TCM () 78checkRecDef i name uc (RecordDirectives ind eta0 pat con) (A.DataDefParams gpars ps) contel fields = 79 traceCall (CheckRecDef (getRange name) name ps fields) $ do 80 reportSDoc "tc.rec" 10 $ vcat 81 [ "checking record def" <+> prettyTCM name 82 , nest 2 $ "ps =" <+> prettyList (map prettyA ps) 83 , nest 2 $ "contel =" <+> prettyA contel 84 , nest 2 $ "fields =" <+> prettyA (map Constr fields) 85 ] 86 -- get type of record 87 def <- instantiateDef =<< getConstInfo name 88 t <- instantiateFull $ defType def 89 let npars = 90 case theDef def of 91 DataOrRecSig n -> n 92 _ -> __IMPOSSIBLE__ 93 94 parNames <- getGeneralizedParameters gpars name 95 96 bindGeneralizedParameters parNames t $ \ gtel t0 -> 97 bindParameters (npars - length parNames) ps t0 $ \ ptel t0 -> do 98 99 let tel = abstract gtel ptel 100 101 -- Generate type of constructor from field telescope @contel@, 102 -- which is the approximate constructor type (target missing). 103 104 -- Check and evaluate field types. 105 reportSDoc "tc.rec" 15 $ "checking fields" 106 contype <- workOnTypes $ instantiateFull =<< isType_ contel 107 reportSDoc "tc.rec" 20 $ vcat 108 [ "contype = " <+> prettyTCM contype ] 109 110 -- compute the field telescope (does not include record parameters) 111 let TelV ftel _ = telView' contype 112 113 -- Compute correct type of constructor 114 115 -- t = tel -> t0 where t0 must be a sort s 116 TelV idxTel s <- telView t0 117 unless (null idxTel) $ typeError $ ShouldBeASort t0 118 s <- forceSort s 119 120 -- needed for impredicative Prop (not implemented yet) 121 -- ftel <- return $ 122 -- if s == Prop 123 -- then telFromList $ map (setRelevance Irrelevant) $ telToList ftel 124 -- else ftel 125 126 reportSDoc "tc.rec" 20 $ do 127 gamma <- getContextTelescope -- the record params (incl. module params) 128 "gamma = " <+> inTopContext (prettyTCM gamma) 129 130 -- record type (name applied to parameters) 131 rect <- El s . Def name . map Apply <$> getContextArgs 132 133 -- Put in @rect@ as correct target of constructor type. 134 -- Andreas, 2011-05-10 use telePi_ instead of telePi to preserve 135 -- even names of non-dependent fields in constructor type (Issue 322). 136 let contype = telePi_ ftel (raise (size ftel) rect) 137 -- NB: contype does not contain the parameter telescope 138 139 -- Obtain name of constructor (if present). 140 (hasNamedCon, conName) <- case con of 141 Just c -> return (True, c) 142 Nothing -> do 143 m <- killRange <$> currentModule 144 -- Andreas, 2020-06-01, AIM XXXII 145 -- Using prettyTCM here jinxes the printer, see PR #4699. 146 -- r <- prettyTCM name 147 let r = P.pretty $ qnameName name 148 c <- qualify m <$> freshName_ (render r ++ ".constructor") 149 return (False, c) 150 151 -- Add record type to signature. 152 reportSDoc "tc.rec" 15 $ "adding record type to signature" 153 154 etaenabled <- etaEnabled 155 156 let getName :: A.Declaration -> [Dom QName] 157 getName (A.Field _ x arg) = [x <$ domFromArg arg] 158 getName (A.ScopedDecl _ [f]) = getName f 159 getName _ = [] 160 161 setTactic dom f = f { domTactic = domTactic dom } 162 163 fs = zipWith setTactic (telToList ftel) $ concatMap getName fields 164 165 -- indCo is what the user wrote: inductive/coinductive/Nothing. 166 -- We drop the Range. 167 indCo = rangedThing <$> ind 168 -- A constructor is inductive unless declared coinductive. 169 conInduction = fromMaybe Inductive indCo 170 -- Andreas, 2016-09-20, issue #2197. 171 -- Eta is inferred by the positivity checker. 172 -- We should turn it off until it is proven to be safe. 173 haveEta = maybe (Inferred $ NoEta patCopat) Specified eta 174 -- haveEta = maybe (Inferred $ conInduction == Inductive && etaenabled) Specified eta 175 con = ConHead conName (IsRecord patCopat) conInduction $ map argFromDom fs 176 177 -- A record is irrelevant if all of its fields are. 178 -- In this case, the associated module parameter will be irrelevant. 179 -- See issue 392. 180 -- Unless it's been declared coinductive or no-eta-equality (#2607). 181 recordRelevance 182 | Just NoEta{} <- eta = Relevant 183 | CoInductive <- conInduction = Relevant 184 | otherwise = minimum $ Irrelevant : map getRelevance (telToList ftel) 185 186 -- Andreas, 2017-01-26, issue #2436 187 -- Disallow coinductive records with eta-equality 188 when (conInduction == CoInductive && theEtaEquality haveEta == YesEta) $ do 189 typeError . GenericDocError =<< do 190 sep [ "Agda doesn't like coinductive records with eta-equality." 191 , "If you must, use pragma" 192 , "{-# ETA" <+> prettyTCM name <+> "#-}" 193 ] 194 reportSDoc "tc.rec" 30 $ "record constructor is " <+> prettyTCM con 195 196 -- Jesper, 2021-05-26: Warn when declaring coinductive record 197 -- but neither --guardedness nor --sized-types is enabled. 198 when (conInduction == CoInductive) $ do 199 guardedness <- collapseDefault . optGuardedness <$> pragmaOptions 200 sizedTypes <- collapseDefault . optSizedTypes <$> pragmaOptions 201 unless (guardedness || sizedTypes) $ warning $ NoGuardednessFlag name 202 203 -- Add the record definition. 204 205 -- Andreas, 2016-06-17, Issue #2018: 206 -- Do not rely on @addConstant@ to put in the record parameters, 207 -- as they might be renamed in the context. 208 -- By putting them ourselves (e.g. by using the original type @t@) 209 -- we make sure we get the original names! 210 let npars = size tel 211 telh = fmap hideAndRelParams tel 212 escapeContext impossible npars $ do 213 addConstant name $ 214 defaultDefn defaultArgInfo name t $ 215 Record 216 { recPars = npars 217 , recClause = Nothing 218 , recConHead = con 219 , recNamedCon = hasNamedCon 220 , recFields = fs 221 , recTel = telh `abstract` ftel 222 , recAbstr = Info.defAbstract i 223 , recEtaEquality' = haveEta 224 , recPatternMatching= patCopat 225 , recInduction = indCo 226 -- We retain the original user declaration [(co)inductive] 227 -- in case the record turns out to be recursive. 228 -- Determined by positivity checker: 229 , recMutual = Nothing 230 , recComp = emptyCompKit -- filled in later 231 } 232 233 -- Add record constructor to signature 234 addConstant conName $ 235 defaultDefn defaultArgInfo conName (telh `abstract` contype) $ 236 Constructor 237 { conPars = npars 238 , conArity = size fs 239 , conSrcCon = con 240 , conData = name 241 , conAbstr = Info.defAbstract i 242 , conInd = conInduction 243 , conComp = emptyCompKit -- filled in later 244 , conProj = Nothing -- filled in later 245 , conForced = [] 246 , conErased = Nothing 247 } 248 249 -- Declare the constructor as eligible for instance search 250 case Info.defInstance i of 251 InstanceDef r -> setCurrentRange r $ do 252 -- Andreas, 2020-01-28, issue #4360: 253 -- Use addTypedInstance instead of addNamedInstance 254 -- to detect unusable instances. 255 addTypedInstance conName contype 256 -- addNamedInstance conName name 257 NotInstanceDef -> pure () 258 259 -- Check that the fields fit inside the sort 260 _ <- fitsIn uc [] contype s 261 262 {- Andreas, 2011-04-27 WRONG because field types are checked again 263 and then non-stricts should not yet be irrelevant 264 265 -- make record parameters hidden and non-stricts irrelevant 266 -- ctx <- (reverse . map hideAndRelParams . take (size tel)) <$> getContext 267 -} 268 269{- Andreas, 2013-09-13 DEBUGGING the debug printout 270 reportSDoc "tc.rec" 80 $ sep 271 [ "current module record telescope" 272 , nest 2 $ (prettyTCM =<< getContextTelescope) 273 ] 274 reportSDoc "tc.rec" 80 $ sep 275 [ "current module record telescope" 276 , nest 2 $ (text . show =<< getContextTelescope) 277 ] 278 reportSDoc "tc.rec" 80 $ sep 279 [ "current module record telescope" 280 , nest 2 $ (inTopContext . prettyTCM =<< getContextTelescope) 281 ] 282 reportSDoc "tc.rec" 80 $ sep 283 [ "current module record telescope" 284 , nest 2 $ do 285 tel <- getContextTelescope 286 text (show tel) $+$ do 287 inTopContext $ do 288 prettyTCM tel $+$ do 289 telA <- reify tel 290 text (show telA) $+$ do 291 ctx <- getContextTelescope 292 "should be empty:" <+> prettyTCM ctx 293 ] 294-} 295 296 let info = setRelevance recordRelevance defaultArgInfo 297 addRecordVar = 298 addRecordNameContext (setArgInfo info $ defaultDom rect) 299 300 let m = qnameToMName name -- Name of record module. 301 302 -- Andreas, 2016-02-09 setting all parameters hidden in the record 303 -- section telescope changes the semantics, see e.g. 304 -- test/Succeed/RecordInParModule. 305 -- Ulf, 2016-03-02 but it's the right thing to do (#1759) 306 modifyContextInfo hideOrKeepInstance $ addRecordVar $ do 307 308 -- Add the record section. 309 310 reportSDoc "tc.rec.def" 10 $ sep 311 [ "record section:" 312 , nest 2 $ sep 313 [ prettyTCM m <+> (inTopContext . prettyTCM =<< getContextTelescope) 314 , fsep $ punctuate comma $ map (return . P.pretty . map argFromDom . getName) fields 315 ] 316 ] 317 reportSDoc "tc.rec.def" 15 $ nest 2 $ vcat 318 [ "field tel =" <+> escapeContext impossible 1 (prettyTCM ftel) 319 ] 320 addSection m 321 322 -- Andreas, 2016-02-09, Issue 1815 (see also issue 1759). 323 -- For checking the record declarations, hide the record parameters 324 -- and the parameters of the parent modules. 325 modifyContextInfo hideOrKeepInstance $ addRecordVar $ do 326 327 -- Check the types of the fields and the other record declarations. 328 withCurrentModule m $ do 329 330 -- Andreas, 2013-09-13, 2016-01-06. 331 -- Argument telescope for the projections: all parameters are hidden. 332 -- This means parameters of the parent modules and of the current 333 -- record type. 334 -- See test/Succeed/ProjectionsTakeModuleTelAsParameters.agda. 335 tel' <- getContextTelescope 336 setModuleCheckpoint m 337 checkRecordProjections m name hasNamedCon con tel' ftel fields 338 339 340 -- we define composition here so that the projections are already in the signature. 341 escapeContext impossible npars $ do 342 addCompositionForRecord name con tel (map argFromDom fs) ftel rect 343 344 -- The confluence checker needs to know what symbols match against 345 -- the constructor. 346 modifySignature $ updateDefinition conName $ \def -> 347 def { defMatchable = Set.fromList $ map unDom fs } 348 349 return () 350 where 351 -- Andreas, 2020-04-19, issue #4560 352 -- If the user declared the record constructor as @pattern@, 353 -- then switch on pattern matching for no-eta-equality. 354 -- Default is no pattern matching, but definition by copatterns instead. 355 patCopat = maybe CopatternMatching (const PatternMatching) pat 356 eta = (patCopat <$) <$> eta0 357 358 359addCompositionForRecord 360 :: QName -- ^ Datatype name. 361 -> ConHead 362 -> Telescope -- ^ @Γ@ parameters. 363 -> [Arg QName] -- ^ Projection names. 364 -> Telescope -- ^ @Γ ⊢ Φ@ field types. 365 -> Type -- ^ @Γ ⊢ T@ target type. 366 -> TCM () 367addCompositionForRecord name con tel fs ftel rect = do 368 cxt <- getContextTelescope 369 inTopContext $ do 370 371 -- Record has no fields: attach composition data to record constructor 372 if null fs then do 373 kit <- defineCompData name con (abstract cxt tel) [] ftel rect [] 374 modifySignature $ updateDefinition (conName con) $ updateTheDef $ \case 375 r@Constructor{} -> r { conComp = kit, conProj = Just [] } -- no projections 376 _ -> __IMPOSSIBLE__ 377 378 -- Record has fields: attach composition data to record type 379 else do 380 -- If record has irrelevant fields but irrelevant projections are disabled, 381 -- we cannot generate composition data. 382 kit <- ifM (return (any isIrrelevant fs) 383 `and2M` do not . optIrrelevantProjections <$> pragmaOptions) 384 {-then-} (return emptyCompKit) 385 {-else-} (defineCompKitR name (abstract cxt tel) ftel fs rect) 386 modifySignature $ updateDefinition name $ updateTheDef $ \case 387 r@Record{} -> r { recComp = kit } 388 _ -> __IMPOSSIBLE__ 389 390defineCompKitR :: 391 QName -- ^ some name, e.g. record name 392 -> Telescope -- ^ param types Δ 393 -> Telescope -- ^ fields' types Δ ⊢ Φ 394 -> [Arg QName] -- ^ fields' names 395 -> Type -- ^ record type Δ ⊢ T 396 -> TCM CompKit 397defineCompKitR name params fsT fns rect = do 398 required <- mapM getTerm' 399 [ builtinInterval 400 , builtinIZero 401 , builtinIOne 402 , builtinIMin 403 , builtinIMax 404 , builtinINeg 405 , builtinPOr 406 , builtinItIsOne 407 ] 408 reportSDoc "tc.rec.cxt" 30 $ prettyTCM params 409 reportSDoc "tc.rec.cxt" 30 $ prettyTCM fsT 410 reportSDoc "tc.rec.cxt" 30 $ pretty rect 411 if not $ all isJust required then return $ emptyCompKit else do 412 transp <- whenDefined [builtinTrans] (defineTranspOrHCompR DoTransp name params fsT fns rect) 413 hcomp <- whenDefined [builtinTrans,builtinHComp] (defineTranspOrHCompR DoHComp name params fsT fns rect) 414 return $ CompKit 415 { nameOfTransp = transp 416 , nameOfHComp = hcomp 417 } 418 where 419 whenDefined xs m = do 420 xs <- mapM getTerm' xs 421 if all isJust xs then m else return Nothing 422 423 424defineTranspOrHCompR :: 425 TranspOrHComp 426 -> QName -- ^ some name, e.g. record name 427 -> Telescope -- ^ param types Δ 428 -> Telescope -- ^ fields' types Δ ⊢ Φ 429 -> [Arg QName] -- ^ fields' names 430 -> Type -- ^ record type Δ ⊢ T 431 -> TCM (Maybe QName) 432defineTranspOrHCompR cmd name params fsT fns rect = do 433 let project = (\ t fn -> t `applyE` [Proj ProjSystem fn]) 434 stuff <- fmap fst <$> defineTranspOrHCompForFields cmd Nothing project name params fsT fns rect 435 436 caseMaybe stuff (return Nothing) $ \ (theName, gamma, rtype, clause_types, bodies) -> do 437 -- phi = 1 clause 438 c' <- do 439 io <- primIOne 440 Just io_name <- getBuiltinName' builtinIOne 441 one <- primItIsOne 442 tInterval <- primIntervalType 443 let 444 (ix,rhs) = 445 case cmd of 446 -- TranspRArgs = phi : I, a0 : .. 447 -- Γ = Δ^I , CompRArgs 448 -- pats = ... | phi = i1 449 -- body = a0 450 DoTransp -> (1,Var 0 []) 451 -- HCompRArgs = phi : I, u : .., a0 : .. 452 -- Γ = Δ, CompRArgs 453 -- pats = ... | phi = i1 454 -- body = u i1 itIsOne 455 DoHComp -> (2,Var 1 [] `apply` [argN io, setRelevance Irrelevant $ argN one]) 456 457 p = ConP (ConHead io_name IsData Inductive []) 458 (noConPatternInfo { conPType = Just (Arg defaultArgInfo tInterval) 459 , conPFallThrough = True }) 460 [] 461 462 -- gamma, rtype 463 464 s = singletonS ix p 465 466 pats :: [NamedArg DeBruijnPattern] 467 pats = s `applySubst` teleNamedArgs gamma 468 469 t :: Type 470 t = s `applyPatSubst` rtype 471 472 gamma' :: Telescope 473 gamma' = unflattenTel (ns0 ++ ns1) $ s `applyPatSubst` (g0 ++ g1) 474 where 475 (g0,_:g1) = splitAt (size gamma - 1 - ix) $ flattenTel gamma 476 (ns0,_:ns1) = splitAt (size gamma - 1 - ix) $ teleNames gamma 477 478 c = Clause { clauseTel = gamma' 479 , clauseType = Just $ argN t 480 , namedClausePats = pats 481 , clauseFullRange = noRange 482 , clauseLHSRange = noRange 483 , clauseCatchall = False 484 , clauseBody = Just $ rhs 485 , clauseExact = Just True 486 , clauseRecursive = Just False -- definitely non-recursive! 487 , clauseUnreachable = Just False 488 , clauseEllipsis = NoEllipsis 489 } 490 reportSDoc "trans.rec.face" 17 $ text $ show c 491 return c 492 cs <- forM (zip3 fns clause_types bodies) $ \ (fname, clause_ty, body) -> do 493 let 494 pats = teleNamedArgs gamma ++ [defaultNamedArg $ ProjP ProjSystem $ unArg fname] 495 c = Clause { clauseTel = gamma 496 , clauseType = Just $ argN (unDom clause_ty) 497 , namedClausePats = pats 498 , clauseFullRange = noRange 499 , clauseLHSRange = noRange 500 , clauseCatchall = False 501 , clauseBody = Just body 502 , clauseExact = Just True 503 , clauseRecursive = Nothing 504 -- Andreas 2020-02-06 TODO 505 -- Or: Just False; is it known to be non-recursive? 506 , clauseUnreachable = Just False 507 , clauseEllipsis = NoEllipsis 508 } 509 reportSDoc "trans.rec" 17 $ text $ show c 510 reportSDoc "trans.rec" 16 $ text "type =" <+> text (show (clauseType c)) 511 reportSDoc "trans.rec" 15 $ prettyTCM $ abstract gamma (unDom clause_ty) 512 reportSDoc "trans.rec" 10 $ text "body =" <+> prettyTCM (abstract gamma body) 513 return c 514 addClauses theName $ c' : cs 515 reportSDoc "trans.rec" 15 $ text $ "compiling clauses for " ++ show theName 516 (mst, _, cc) <- inTopContext (compileClauses Nothing cs) 517 whenJust mst $ setSplitTree theName 518 setCompiledClauses theName cc 519 reportSDoc "trans.rec" 15 $ text $ "compiled" 520 return $ Just theName 521 522 523{-| @checkRecordProjections m r q tel ftel fs@. 524 525 [@m@ ] name of the generated module 526 527 [@r@ ] name of the record type 528 529 [@con@ ] name of the record constructor 530 531 [@tel@ ] parameters and record variable r ("self") 532 533 [@ftel@ ] telescope of fields 534 535 [@fs@ ] the fields to be checked 536-} 537checkRecordProjections :: 538 ModuleName -> QName -> Bool -> ConHead -> Telescope -> Telescope -> 539 [A.Declaration] -> TCM () 540checkRecordProjections m r hasNamedCon con tel ftel fs = do 541 checkProjs EmptyTel ftel [] fs 542 where 543 544 checkProjs :: Telescope -> Telescope -> [Term] -> [A.Declaration] -> TCM () 545 546 checkProjs _ _ _ [] = return () 547 548 checkProjs ftel1 ftel2 vs (A.ScopedDecl scope fs' : fs) = 549 setScope scope >> checkProjs ftel1 ftel2 vs (fs' ++ fs) 550 551 -- Case: projection. 552 checkProjs ftel1 (ExtendTel (dom@Dom{domInfo = ai,unDom = t}) ftel2) vs (A.Field info x _ : fs) = 553 traceCall (CheckProjection (getRange info) x t) $ do 554 -- Andreas, 2012-06-07: 555 -- Issue 387: It is wrong to just type check field types again 556 -- because then meta variables are created again. 557 -- Instead, we take the field type t from the field telescope. 558 reportSDoc "tc.rec.proj" 5 $ sep 559 [ "checking projection" <+> prettyTCM x 560 , nest 2 $ vcat 561 [ "top =" <+> (inTopContext . prettyTCM =<< getContextTelescope) 562 , "tel =" <+> (inTopContext . prettyTCM $ tel) 563 ] 564 ] 565 -- Andreas, 2021-05-11, issue #5378 566 -- The impossible is sometimes possible, so splitting out this part... 567 reportSDoc "tc.rec.proj" 5 $ nest 2 $ vcat 568 [ "ftel1 =" <+> escapeContext impossible 1 (prettyTCM ftel1) 569 , "t =" <+> escapeContext impossible 1 (addContext ftel1 $ prettyTCM t) 570 , "ftel2 =" <+> escapeContext impossible 1 (addContext ftel1 $ underAbstraction dom ftel2 prettyTCM) 571 ] 572 reportSDoc "tc.rec.proj" 55 $ nest 2 $ vcat 573 [ "ftel1 (raw) =" <+> pretty ftel1 574 , "t (raw) =" <+> pretty t 575 , "ftel2 (raw) =" <+> pretty ftel2 576 ] 577 reportSDoc "tc.rec.proj" 5 $ nest 2 $ vcat 578 [ "vs =" <+> prettyList_ (map prettyTCM vs) 579 , "abstr =" <+> (text . show) (Info.defAbstract info) 580 , "quant =" <+> (text . show) (getQuantity ai) 581 , "coh =" <+> (text . show) (getCohesion ai) 582 ] 583 584 -- Cohesion check: 585 -- For a field `@c π : A` we would create a projection `π : .., (@(c^-1) r : R as) -> A` 586 -- So we want to check that `@.., (c^-1 . c) x : A |- x : A` is allowed by the modalities. 587 -- 588 -- Alternatively we could create a projection `.. |- π r :c A` 589 -- but that would require support for a `t :c A` judgment. 590 if hasLeftAdjoint (UnderComposition (getCohesion ai)) 591 then unless (getCohesion ai == Continuous) 592 -- Andrea TODO: properly update the context/type of the projection when we add Sharp 593 __IMPOSSIBLE__ 594 else genericError $ "Cannot have record fields with modality " ++ show (getCohesion ai) 595 596 -- The telescope tel includes the variable of record type as last one 597 -- e.g. for cartesion product it is 598 -- 599 -- tel = {A' : Set} {B' : Set} (r : Prod A' B') 600 601 -- create the projection functions (instantiate the type with the values 602 -- of the previous fields) 603 604 -- The type of the projection function should be 605 -- {Δ} -> (r : R Δ) -> t 606 -- where Δ are the parameters of R 607 608 {- what are the contexts? 609 610 Δ , ftel₁ ⊢ t 611 Δ , (r : R Δ) ⊢ parallelS vs : ftel₁ 612 Δ , (r : R Δ) , ftel₁ ⊢ t' = raiseFrom (size ftel₁) 1 t 613 Δ , (r : R Δ) ⊢ t'' = applySubst (parallelS vs) t' 614 ⊢ finalt = telePi tel t'' 615 -} 616 let t' = raiseFrom (size ftel1) 1 t 617 t'' = applySubst (parallelS vs) t' 618 finalt = telePi (replaceEmptyName "r" tel) t'' 619 projname = qualify m $ qnameName x 620 projcall o = Var 0 [Proj o projname] 621 rel = getRelevance ai 622 -- the recursive call 623 recurse = checkProjs (abstract ftel1 $ ExtendTel dom 624 $ Abs (nameToArgName $ qnameName projname) EmptyTel) 625 (absBody ftel2) (projcall ProjSystem : vs) fs 626 627 reportSDoc "tc.rec.proj" 25 $ nest 2 $ "finalt=" <+> do 628 inTopContext $ prettyTCM finalt 629 630 -- -- Andreas, 2012-02-20 do not add irrelevant projections if 631 -- -- disabled by --no-irrelevant-projections 632 -- ifM (return (rel == Irrelevant) `and2M` do not . optIrrelevantProjections <$> pragmaOptions) recurse $ do 633 -- Andreas, 2018-06-09 issue #2170 634 -- Always create irrelevant projections (because the scope checker accepts irrelevant fields). 635 -- If --no-irrelevant-projections, then their use should be disallowed by the type checker for expressions. 636 do 637 reportSDoc "tc.rec.proj" 10 $ sep 638 [ "adding projection" 639 , nest 2 $ prettyTCM projname <+> ":" <+> inTopContext (prettyTCM finalt) 640 ] 641 642 -- The body should be 643 -- P.xi {tel} (r _ .. x .. _) = x 644 -- Ulf, 2011-08-22: actually we're dropping the parameters from the 645 -- projection functions so the body is now 646 -- P.xi (r _ .. x .. _) = x 647 -- Andreas, 2012-01-12: irrelevant projections get translated to 648 -- P.xi (r _ .. x .. _) = irrAxiom {level of t} {t} x 649 -- PROBLEM: because of dropped parameters, cannot refer to t 650 -- 2012-04-02: DontCare instead of irrAxiom 651 652 -- compute body modification for irrelevant projections 653 let bodyMod = case rel of 654 Relevant -> id 655 NonStrict -> id 656 Irrelevant -> dontCare 657 658 let -- Andreas, 2010-09-09: comment for existing code 659 -- split the telescope into parameters (ptel) and the type or the record 660 -- (rt) which should be R ptel 661 telList = telToList tel 662 (ptelList,[rt]) = splitAt (size tel - 1) telList 663 ptel = telFromList ptelList 664 cpo = if hasNamedCon then PatOCon else PatORec 665 cpi = ConPatternInfo { conPInfo = PatternInfo cpo [] 666 , conPRecord = True 667 , conPFallThrough = False 668 , conPType = Just $ argFromDom $ fmap snd rt 669 , conPLazy = True } 670 conp = defaultNamedArg $ ConP con cpi $ teleNamedArgs ftel 671 body = Just $ bodyMod $ var (size ftel2) 672 cltel = ptel `abstract` ftel 673 cltype = Just $ Arg ai $ raise (1 + size ftel2) t 674 clause = Clause { clauseLHSRange = getRange info 675 , clauseFullRange = getRange info 676 , clauseTel = killRange cltel 677 , namedClausePats = [conp] 678 , clauseBody = body 679 , clauseType = cltype 680 , clauseCatchall = False 681 , clauseExact = Just True 682 , clauseRecursive = Just False 683 , clauseUnreachable = Just False 684 , clauseEllipsis = NoEllipsis 685 } 686 687 let projection = Projection 688 { projProper = Just r 689 , projOrig = projname 690 -- name of the record type: 691 , projFromType = defaultArg r 692 -- index of the record argument (in the type), 693 -- start counting with 1: 694 , projIndex = size tel -- which is @size ptel + 1@ 695 , projLams = ProjLams $ map (argFromDom . fmap fst) telList 696 } 697 698 reportSDoc "tc.rec.proj" 70 $ sep 699 [ "adding projection" 700 , nest 2 $ prettyTCM projname <+> pretty clause 701 ] 702 reportSDoc "tc.rec.proj" 10 $ sep 703 [ "adding projection" 704 , nest 2 $ prettyTCM (QNamed projname clause) 705 ] 706 707 -- Record patterns should /not/ be translated when the 708 -- projection functions are defined. Record pattern 709 -- translation is defined in terms of projection 710 -- functions. 711 (mst, _, cc) <- compileClauses Nothing [clause] 712 713 reportSDoc "tc.cc" 60 $ do 714 sep [ "compiled clauses of " <+> prettyTCM projname 715 , nest 2 $ text (show cc) 716 ] 717 718 escapeContext impossible (size tel) $ do 719 addConstant projname $ 720 (defaultDefn ai projname (killRange finalt) 721 emptyFunction 722 { funClauses = [clause] 723 , funCompiled = Just cc 724 , funSplitTree = mst 725 , funProjection = Just projection 726 , funMutual = Just [] -- Projections are not mutually recursive with anything 727 , funTerminates = Just True 728 }) 729 { defArgOccurrences = [StrictPos] 730 , defCopatternLHS = hasProjectionPatterns cc 731 } 732 computePolarity [projname] 733 734 case Info.defInstance info of 735 -- fields do not have an @instance@ keyword!? 736 InstanceDef _r -> addTypedInstance projname t 737 NotInstanceDef -> pure () 738 739 recurse 740 741 -- Case: definition. 742 checkProjs ftel1 ftel2 vs (d : fs) = do 743 checkDecl d 744 checkProjs ftel1 ftel2 vs fs 745