@@ -451,29 +451,28 @@ isEtaRecord r = do
451 451
isRec <- isRecord r
452 452
case isRec of
453 453
Nothing -> return False
454 -
Just r
455 -
| recEtaEquality r /= YesEta -> return False
456 -
| otherwise -> do
457 -
constructorQ <- getQuantity <$>
458 -
getConstInfo (conName (recConHead r))
459 -
currentQ <- viewTC eQuantity
460 -
return $ constructorQ `moreQuantity` currentQ
454 +
Just r -> isEtaRecordDef r
455 + 456 +
isEtaRecordDef :: HasConstInfo m => Defn -> m Bool
457 +
isEtaRecordDef r
458 +
| recEtaEquality r /= YesEta = return False
459 +
| otherwise = do
460 +
constructorQ <- getQuantity <$>
461 +
getConstInfo (conName (recConHead r))
462 +
currentQ <- viewTC eQuantity
463 +
return $ constructorQ `moreQuantity` currentQ
464 + 461 465 462 466
{-# SPECIALIZE isEtaCon :: QName -> TCM Bool #-}
463 467
isEtaCon :: HasConstInfo m => QName -> m Bool
464 -
isEtaCon c = getConstInfo' c >>= \case
465 -
Left (SigUnknown err) -> __IMPOSSIBLE__
466 -
Left SigCubicalNotErasure -> __IMPOSSIBLE__
467 -
Left SigAbstract -> return False
468 -
Right def -> case theDef def of
469 -
Constructor {conData = r} -> isEtaRecord r
470 -
_ -> return False
468 +
isEtaCon c = isJust <$> isEtaRecordConstructor c
471 469 472 470
-- | Going under one of these does not count as a decrease in size for the termination checker.
473 471
isEtaOrCoinductiveRecordConstructor :: HasConstInfo m => QName -> m Bool
474 472
isEtaOrCoinductiveRecordConstructor c =
475 -
caseMaybeM (isRecordConstructor c) (return False) $ \ (_, def) -> return $
476 -
recEtaEquality def == YesEta || recInduction def /= Just Inductive
473 +
caseMaybeM (isRecordConstructor c) (return False) $ \ (_, def) ->
474 +
isEtaRecordDef def `or2M`
475 +
return (recInduction def /= Just Inductive)
477 476
-- If in doubt about coinductivity, then yes.
478 477 479 478
-- | Check if a name refers to a record which is not coinductive. (Projections are then size-preserving)
@@ -500,6 +499,11 @@ isRecordConstructor c = getConstInfo' c >>= \case
500 499
Constructor{ conData = r } -> fmap (r,) <$> isRecord r
501 500
_ -> return Nothing
502 501 502 +
isEtaRecordConstructor :: HasConstInfo m => QName -> m (Maybe (QName, Defn))
503 +
isEtaRecordConstructor c = isRecordConstructor c >>= \case
504 +
Nothing -> return Nothing
505 +
Just (d, def) -> ifM (isEtaRecordDef def) (return $ Just (d, def)) (return Nothing)
506 + 503 507
-- | Check if a constructor name is the internally generated record constructor.
504 508
--
505 509
-- Works also for abstract constructors.
@@ -583,9 +587,9 @@ expandRecordVar i gamma0 = do
583 587
" since its type " <+> prettyTCM a <+>
584 588
" is not a record type"
585 589
return Nothing
586 -
caseMaybeM (isRecordType a) failure $ \ (r, pars, def) -> case recEtaEquality def of
587 -
NoEta{} -> return Nothing
588 -
YesEta -> Just <$> do
590 +
caseMaybeM (isRecordType a) failure $ \ (r, pars, def) -> isEtaRecordDef def >>= \case
591 +
False -> return Nothing
592 +
True -> Just <$> do
589 593
-- Get the record fields @Γ₁ ⊢ tel@ (@tel = Γ'@).
590 594
-- TODO: compose argInfo ai with tel.
591 595
let tel = recTel def `apply` pars
@@ -905,7 +909,7 @@ isSingletonType' regardIrrelevance t rs = do
905 909
record :: m (Maybe Term)
906 910
record = runMaybeT $ do
907 911
(r, ps, def) <- MaybeT $ isRecordType t
908 -
guard (YesEta == recEtaEquality def)
912 +
guardM $ isEtaRecordDef def
909 913
abstract tel <$> MaybeT (isSingletonRecord' regardIrrelevance r ps rs)
910 914 911 915
-- Slightly harder case: η for Sub {level} tA phi elt.
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4