{-# LANGUAGE NondecreasingIndentation   #-}

module Agda.TypeChecking.Rules.Record where

import Prelude hiding (null)

import Control.Monad
import Data.Maybe
import qualified Data.Set as Set

import Agda.Interaction.Options

import qualified Agda.Syntax.Abstract as A
import qualified Agda.Syntax.Abstract.Views as A
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.Syntax.Internal.Pattern
import Agda.Syntax.Position
import qualified Agda.Syntax.Info as Info

import Agda.TypeChecking.Monad
import Agda.TypeChecking.Primitive
import Agda.TypeChecking.Rewriting.Confluence
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Positivity.Occurrence
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Polarity
import Agda.TypeChecking.Warnings
import Agda.TypeChecking.Irrelevance
import Agda.TypeChecking.CompiledClause (hasProjectionPatterns)
import Agda.TypeChecking.CompiledClause.Compile

import Agda.TypeChecking.Rules.Data
  ( getGeneralizedParameters, bindGeneralizedParameters, bindParameters
  , checkDataSort, fitsIn, forceSort
  , defineCompData, defineKanOperationForFields
  )
import Agda.TypeChecking.Rules.Term ( isType_ )
import {-# SOURCE #-} Agda.TypeChecking.Rules.Decl (checkDecl)

import Agda.Utils.List (headWithDefault)
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.Permutation
import Agda.Utils.POMonoid
import Agda.Utils.Pretty (render)
import qualified Agda.Utils.Pretty as P
import Agda.Utils.Size
import Agda.Utils.WithDefault

import Agda.Utils.Impossible

---------------------------------------------------------------------------
-- * Records
---------------------------------------------------------------------------

-- | @checkRecDef i name con ps contel fields@
--
--     [@name@]    Record type identifier.
--
--     [@con@]     Maybe constructor name and info.
--
--     [@ps@]      Record parameters.
--
--     [@contel@]  Approximate type of constructor (@fields@ -> dummy).
--                 Does not include record parameters.
--
--     [@fields@]  List of field signatures.
--
checkRecDef
  :: A.DefInfo                 -- ^ Position and other info.
  -> QName                     -- ^ Record type identifier.
  -> UniverseCheck             -- ^ Check universes?
  -> A.RecordDirectives        -- ^ (Co)Inductive, (No)Eta, (Co)Pattern, Constructor?
  -> A.DataDefParams           -- ^ Record parameters.
  -> A.Expr                    -- ^ Approximate type of constructor (@fields@ -> dummy).
                               --   Does not include record parameters.
  -> [A.Field]                 -- ^ Field signatures.
  -> TCM ()
checkRecDef :: DefInfo
-> QName
-> UniverseCheck
-> RecordDirectives
-> DataDefParams
-> Expr
-> [Field]
-> TCM ()
checkRecDef DefInfo
i QName
name UniverseCheck
uc (RecordDirectives Maybe (Ranged Induction)
ind Maybe HasEta0
eta0 Maybe Range
pat Maybe QName
con) (A.DataDefParams Set Name
gpars [LamBinding]
ps) Expr
contel0 [Field]
fields = do

  -- Andreas, 2022-10-06, issue #6165:
  -- The target type of the constructor is a meaningless dummy expression which does not type-check.
  -- We replace it by Set/Type (builtinSet) which is still incorrect but type-checks.
  -- It will be fixed after type-checking.
  Expr
aType <- QName -> Expr
A.Def forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasBuiltins m => [Char] -> m (Maybe QName)
getBuiltinName' [Char]
builtinSet
  let contel :: Expr
contel = PiView -> Expr
A.unPiView forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\ (A.PiView [(ExprInfo, Telescope1)]
tels Expr
_) -> [(ExprInfo, Telescope1)] -> Expr -> PiView
A.PiView [(ExprInfo, Telescope1)]
tels Expr
aType) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> PiView
A.piView forall a b. (a -> b) -> a -> b
$ Expr
contel0

  forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
traceCall (Range -> QName -> [LamBinding] -> [Field] -> Call
CheckRecDef (forall a. HasRange a => a -> Range
getRange QName
name) QName
name [LamBinding]
ps [Field]
fields) forall a b. (a -> b) -> a -> b
$ do
    forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.rec" Nat
10 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ TCMT IO Doc
"checking record def" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
name
      , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"ps ="     forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList (forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA [LamBinding]
ps)
      , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"contel =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA Expr
contel
      , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"fields =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA (forall a b. (a -> b) -> [a] -> [b]
map forall a. a -> Constr a
Constr [Field]
fields)
      ]
    -- get type of record
    Definition
def <- forall (m :: * -> *).
(Functor m, HasConstInfo m, HasOptions m, ReadTCState m,
 MonadTCEnv m, MonadDebug m) =>
Definition -> m Definition
instantiateDef forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
name
    Type
t   <- forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull forall a b. (a -> b) -> a -> b
$ Definition -> Type
defType Definition
def
    let npars :: Nat
npars =
          case Definition -> Defn
theDef Definition
def of
            DataOrRecSig Nat
n -> Nat
n
            Defn
_              -> forall a. HasCallStack => a
__IMPOSSIBLE__

    [Maybe Name]
parNames <- Set Name -> QName -> TCM [Maybe Name]
getGeneralizedParameters Set Name
gpars QName
name

    forall a.
[Maybe Name] -> Type -> (Telescope -> Type -> TCM a) -> TCM a
bindGeneralizedParameters [Maybe Name]
parNames Type
t forall a b. (a -> b) -> a -> b
$ \ Telescope
gtel Type
t0 ->
     forall a.
Nat
-> [LamBinding] -> Type -> (Telescope -> Type -> TCM a) -> TCM a
bindParameters (Nat
npars forall a. Num a => a -> a -> a
- forall (t :: * -> *) a. Foldable t => t a -> Nat
length [Maybe Name]
parNames) [LamBinding]
ps Type
t0 forall a b. (a -> b) -> a -> b
$ \ Telescope
ptel Type
t0 -> do

      let tel :: Telescope
tel = forall t. Abstract t => Telescope -> t -> t
abstract Telescope
gtel Telescope
ptel

      -- Generate type of constructor from field telescope @contel@,
      -- which is the approximate constructor type (target missing).

      -- Check and evaluate field types.
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.rec" Nat
15 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"checking fields"
      Type
contype <- forall (m :: * -> *) a.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
m a -> m a
workOnTypes forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Expr -> TCMT IO Type
isType_ Expr
contel
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.rec" Nat
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
        [ TCMT IO Doc
"contype = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
contype ]

      -- compute the field telescope (does not include record parameters)
      let TelV Telescope
ftel Type
_ = Type -> TelV Type
telView' Type
contype

      -- Compute correct type of constructor

      -- t = tel -> t0 where t0 must be a sort s
      TelV Telescope
idxTel Type
s <- forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView Type
t0
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a. Null a => a -> Bool
null Telescope
idxTel) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ Type -> TypeError
ShouldBeASort Type
t0
      Sort
s <- Type -> TCM Sort
forceSort Type
s

      -- needed for impredicative Prop (not implemented yet)
      -- ftel <- return $
      --   if s == Prop
      --   then telFromList $ map (setRelevance Irrelevant) $ telToList ftel
      --   else ftel

      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.rec" Nat
20 forall a b. (a -> b) -> a -> b
$ do
        Telescope
gamma <- forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope  -- the record params (incl. module params)
        TCMT IO Doc
"gamma = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
gamma)

      -- record type (name applied to parameters)
      Type
rect <- forall t a. Sort' t -> a -> Type'' t a
El Sort
s forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Elims -> Term
Def QName
name forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall a. Arg a -> Elim' a
Apply forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m [Arg Term]
getContextArgs

      -- Put in @rect@ as correct target of constructor type.
      -- Andreas, 2011-05-10 use telePi_ instead of telePi to preserve
      -- even names of non-dependent fields in constructor type (Issue 322).
      let contype :: Type
contype = Telescope -> Type -> Type
telePi_ Telescope
ftel (forall a. Subst a => Nat -> a -> a
raise (forall a. Sized a => a -> Nat
size Telescope
ftel) Type
rect)
        -- NB: contype does not contain the parameter telescope

      -- Obtain name of constructor (if present).
      (Bool
hasNamedCon, QName
conName) <- case Maybe QName
con of
        Just QName
c  -> forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
True, QName
c)
        Maybe QName
Nothing -> do
          ModuleName
m <- forall a. KillRange a => KillRangeT a
killRange forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). MonadTCEnv m => m ModuleName
currentModule
          -- Andreas, 2020-06-01, AIM XXXII
          -- Using prettyTCM here jinxes the printer, see PR #4699.
          -- r <- prettyTCM name
          let r :: Doc
r = forall a. Pretty a => a -> Doc
P.pretty forall a b. (a -> b) -> a -> b
$ QName -> Name
qnameName QName
name
          QName
c <- ModuleName -> Name -> QName
qualify ModuleName
m forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(FreshName a, MonadFresh NameId m) =>
a -> m Name
freshName_ (Doc -> [Char]
render Doc
r forall a. [a] -> [a] -> [a]
++ [Char]
".constructor")
          forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, QName
c)

      -- Add record type to signature.
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.rec" Nat
15 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"adding record type to signature"

      Bool
etaenabled <- forall (m :: * -> *). HasOptions m => m Bool
etaEnabled

      let getName :: A.Declaration -> [Dom QName]
          getName :: Field -> [Dom' Term QName]
getName (A.Field DefInfo
_ QName
x Arg Expr
arg)    = [QName
x forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall a. Arg a -> Dom a
domFromArg Arg Expr
arg]
          getName (A.ScopedDecl ScopeInfo
_ [Field
f]) = Field -> [Dom' Term QName]
getName Field
f
          getName Field
_                    = []

          setTactic :: Dom' t e -> Dom' t e -> Dom' t e
setTactic Dom' t e
dom Dom' t e
f = Dom' t e
f { domTactic :: Maybe t
domTactic = forall t e. Dom' t e -> Maybe t
domTactic Dom' t e
dom }

          fs :: [Dom' Term QName]
fs = forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith forall {t} {e} {t} {e}. Dom' t e -> Dom' t e -> Dom' t e
setTactic (forall t. Tele (Dom t) -> [Dom ([Char], t)]
telToList Telescope
ftel) forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Field -> [Dom' Term QName]
getName [Field]
fields

          -- indCo is what the user wrote: inductive/coinductive/Nothing.
          -- We drop the Range.
          indCo :: Maybe Induction
indCo = forall a. Ranged a -> a
rangedThing forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (Ranged Induction)
ind
          -- A constructor is inductive unless declared coinductive.
          conInduction :: Induction
conInduction = forall a. a -> Maybe a -> a
fromMaybe Induction
Inductive Maybe Induction
indCo
          -- Andreas, 2016-09-20, issue #2197.
          -- Eta is inferred by the positivity checker.
          -- We should turn it off until it is proven to be safe.
          haveEta :: EtaEquality
haveEta      = forall b a. b -> (a -> b) -> Maybe a -> b
maybe (HasEta -> EtaEquality
Inferred forall a b. (a -> b) -> a -> b
$ forall a. a -> HasEta' a
NoEta PatternOrCopattern
patCopat) HasEta -> EtaEquality
Specified Maybe HasEta
eta
          -- haveEta      = maybe (Inferred $ conInduction == Inductive && etaenabled) Specified eta
          con :: ConHead
con = QName -> DataOrRecord -> Induction -> [Arg QName] -> ConHead
ConHead QName
conName (PatternOrCopattern -> DataOrRecord
IsRecord PatternOrCopattern
patCopat) Induction
conInduction forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall t a. Dom' t a -> Arg a
argFromDom [Dom' Term QName]
fs

          -- A record is irrelevant if all of its fields are.
          -- In this case, the associated module parameter will be irrelevant.
          -- See issue 392.
          -- Unless it's been declared coinductive or no-eta-equality (#2607).
          recordRelevance :: Relevance
recordRelevance
            | Just NoEta{} <- Maybe HasEta
eta         = Relevance
Relevant
            | Induction
CoInductive <- Induction
conInduction = Relevance
Relevant
            | Bool
otherwise                   = forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
minimum forall a b. (a -> b) -> a -> b
$ Relevance
Irrelevant forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map forall a. LensRelevance a => a -> Relevance
getRelevance (forall t. Tele (Dom t) -> [Dom ([Char], t)]
telToList Telescope
ftel)

      -- Andreas, 2017-01-26, issue #2436
      -- Disallow coinductive records with eta-equality
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Induction
conInduction forall a. Eq a => a -> a -> Bool
== Induction
CoInductive Bool -> Bool -> Bool
&& EtaEquality -> HasEta
theEtaEquality EtaEquality
haveEta forall a. Eq a => a -> a -> Bool
== forall a. HasEta' a
YesEta) forall a b. (a -> b) -> a -> b
$ do
        forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
          forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ TCMT IO Doc
"Agda doesn't like coinductive records with eta-equality."
              , TCMT IO Doc
"If you must, use pragma"
              , TCMT IO Doc
"{-# ETA" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
name forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"#-}"
              ]
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.rec" Nat
30 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"record constructor is " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM ConHead
con

      -- Jesper, 2021-05-26: Warn when declaring coinductive record
      -- but neither --guardedness nor --sized-types is enabled.
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Induction
conInduction forall a. Eq a => a -> a -> Bool
== Induction
CoInductive) forall a b. (a -> b) -> a -> b
$ do
        Bool
guardedness <- forall (b :: Bool). KnownBool b => WithDefault b -> Bool
collapseDefault forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> WithDefault 'False
optGuardedness forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
        Bool
sizedTypes  <- forall (b :: Bool). KnownBool b => WithDefault b -> Bool
collapseDefault forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> WithDefault 'False
optSizedTypes  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
        forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Bool
guardedness Bool -> Bool -> Bool
|| Bool
sizedTypes) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(HasCallStack, MonadWarning m) =>
Warning -> m ()
warning forall a b. (a -> b) -> a -> b
$ QName -> Warning
NoGuardednessFlag QName
name

      -- Add the record definition.

      -- Andreas, 2016-06-17, Issue #2018:
      -- Do not rely on @addConstant@ to put in the record parameters,
      -- as they might be renamed in the context.
      -- By putting them ourselves (e.g. by using the original type @t@)
      -- we make sure we get the original names!
      let npars :: Nat
npars = forall a. Sized a => a -> Nat
size Telescope
tel
          telh :: Telescope
telh  = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. (LensHiding a, LensRelevance a) => a -> a
hideAndRelParams Telescope
tel
      forall (m :: * -> *) a.
MonadAddContext m =>
Impossible -> Nat -> m a -> m a
escapeContext HasCallStack => Impossible
impossible Nat
npars forall a b. (a -> b) -> a -> b
$ do
        QName -> ArgInfo -> QName -> Type -> Defn -> TCM ()
addConstant' QName
name ArgInfo
defaultArgInfo QName
name Type
t forall a b. (a -> b) -> a -> b
$
            Record
              { recPars :: Nat
recPars           = Nat
npars
              , recClause :: Maybe Clause
recClause         = forall a. Maybe a
Nothing
              , recConHead :: ConHead
recConHead        = ConHead
con
              , recNamedCon :: Bool
recNamedCon       = Bool
hasNamedCon
              , recFields :: [Dom' Term QName]
recFields         = [Dom' Term QName]
fs
              , recTel :: Telescope
recTel            = Telescope
telh forall t. Abstract t => Telescope -> t -> t
`abstract` Telescope
ftel
              , recAbstr :: IsAbstract
recAbstr          = forall t. DefInfo' t -> IsAbstract
Info.defAbstract DefInfo
i
              , recEtaEquality' :: EtaEquality
recEtaEquality'   = EtaEquality
haveEta
              , recPatternMatching :: PatternOrCopattern
recPatternMatching= PatternOrCopattern
patCopat
              , recInduction :: Maybe Induction
recInduction      = Maybe Induction
indCo
                  -- We retain the original user declaration [(co)inductive]
                  -- in case the record turns out to be recursive.
              -- Determined by positivity checker:
              , recMutual :: Maybe [QName]
recMutual         = forall a. Maybe a
Nothing
              -- Determined by the termination checker:
              , recTerminates :: Maybe Bool
recTerminates     = forall a. Maybe a
Nothing
              , recComp :: CompKit
recComp           = CompKit
emptyCompKit -- filled in later
              }

        -- Add record constructor to signature
        QName -> ArgInfo -> QName -> Type -> Defn -> TCM ()
addConstant' QName
conName ArgInfo
defaultArgInfo QName
conName
             -- The parameters are erased in the constructor's type.
            (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a. LensQuantity a => Quantity -> a -> a
applyQuantity Quantity
zeroQuantity) Telescope
telh
             forall t. Abstract t => Telescope -> t -> t
`abstract` Type
contype) forall a b. (a -> b) -> a -> b
$
            Constructor
              { conPars :: Nat
conPars   = Nat
npars
              , conArity :: Nat
conArity  = forall a. Sized a => a -> Nat
size [Dom' Term QName]
fs
              , conSrcCon :: ConHead
conSrcCon = ConHead
con
              , conData :: QName
conData   = QName
name
              , conAbstr :: IsAbstract
conAbstr  = forall t. DefInfo' t -> IsAbstract
Info.defAbstract DefInfo
i
              , conInd :: Induction
conInd    = Induction
conInduction
              , conComp :: CompKit
conComp   = CompKit
emptyCompKit  -- filled in later
              , conProj :: Maybe [QName]
conProj   = forall a. Maybe a
Nothing       -- filled in later
              , conForced :: [IsForced]
conForced = []
              , conErased :: Maybe [Bool]
conErased = forall a. Maybe a
Nothing
              }

      -- Declare the constructor as eligible for instance search
      case forall t. DefInfo' t -> IsInstance
Info.defInstance DefInfo
i of
        InstanceDef Range
r -> forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange Range
r forall a b. (a -> b) -> a -> b
$ do
          -- Andreas, 2020-01-28, issue #4360:
          -- Use addTypedInstance instead of addNamedInstance
          -- to detect unusable instances.
          QName -> Type -> TCM ()
addTypedInstance QName
conName Type
contype
          -- addNamedInstance conName name
        IsInstance
NotInstanceDef -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

      -- Check that the fields fit inside the sort
      Nat
_ <- UniverseCheck -> [IsForced] -> Type -> Sort -> TCM Nat
fitsIn UniverseCheck
uc [] Type
contype Sort
s

      -- Check that the sort admits record declarations.
      QName -> Sort -> TCM ()
checkDataSort QName
name Sort
s


      {- Andreas, 2011-04-27 WRONG because field types are checked again
         and then non-stricts should not yet be irrelevant

      -- make record parameters hidden and non-stricts irrelevant
      -- ctx <- (reverse . map hideAndRelParams . take (size tel)) <$> getContext
      -}

{- Andreas, 2013-09-13 DEBUGGING the debug printout
      reportSDoc "tc.rec" 80 $ sep
        [ "current module record telescope"
        , nest 2 $ (prettyTCM =<< getContextTelescope)
        ]
      reportSDoc "tc.rec" 80 $ sep
        [ "current module record telescope"
        , nest 2 $ (text . show =<< getContextTelescope)
        ]
      reportSDoc "tc.rec" 80 $ sep
        [ "current module record telescope"
        , nest 2 $ (inTopContext . prettyTCM =<< getContextTelescope)
        ]
      reportSDoc "tc.rec" 80 $ sep
        [ "current module record telescope"
        , nest 2 $ do
           tel <- getContextTelescope
           text (show tel) $+$ do
           inTopContext $ do
             prettyTCM tel $+$ do
               telA <- reify tel
               text (show telA) $+$ do
               ctx <- getContextTelescope
               "should be empty:" <+> prettyTCM ctx
        ]
-}

      let info :: ArgInfo
info = forall a. LensRelevance a => Relevance -> a -> a
setRelevance Relevance
recordRelevance ArgInfo
defaultArgInfo
          addRecordVar :: TCM () -> TCM ()
addRecordVar =
            forall (m :: * -> *) b.
(MonadAddContext m, MonadFresh NameId m) =>
Dom Type -> m b -> m b
addRecordNameContext (forall a. LensArgInfo a => ArgInfo -> a -> a
setArgInfo ArgInfo
info forall a b. (a -> b) -> a -> b
$ forall a. a -> Dom a
defaultDom Type
rect)

      let m :: ModuleName
m = QName -> ModuleName
qnameToMName QName
name  -- Name of record module.

      Bool
eraseRecordParameters <- PragmaOptions -> Bool
optEraseRecordParameters forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
      let maybeErase :: forall a. LensQuantity a => a -> a
          maybeErase :: forall a. LensQuantity a => a -> a
maybeErase | Bool
eraseRecordParameters = forall a. LensQuantity a => Quantity -> a -> a
setQuantity Quantity
zeroQuantity
                     | Bool
otherwise             = forall a. a -> a
id

      -- Andreas, 2016-02-09 setting all parameters hidden in the record
      -- section telescope changes the semantics, see e.g.
      -- test/Succeed/RecordInParModule.
      -- Ulf, 2016-03-02 but it's the right thing to do (#1759)
      forall (tcm :: * -> *) a.
MonadTCEnv tcm =>
(forall e. Dom e -> Dom e) -> tcm a -> tcm a
modifyContextInfo (forall a. LensHiding a => a -> a
hideOrKeepInstance forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. LensQuantity a => a -> a
maybeErase) forall a b. (a -> b) -> a -> b
$ TCM () -> TCM ()
addRecordVar forall a b. (a -> b) -> a -> b
$ do

        -- Add the record section.

        forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.rec.def" Nat
10 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
          [ TCMT IO Doc
"record section:"
          , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
            [ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM ModuleName
m forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope)
            , forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
m Doc -> t (m Doc) -> [m Doc]
punctuate forall (m :: * -> *). Applicative m => m Doc
comma forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Pretty a => a -> Doc
P.pretty forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall t a. Dom' t a -> Arg a
argFromDom forall b c a. (b -> c) -> (a -> b) -> a -> c
. Field -> [Dom' Term QName]
getName) [Field]
fields
            ]
          ]
        forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.rec.def" Nat
15 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
          [ TCMT IO Doc
"field tel =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a.
MonadAddContext m =>
Impossible -> Nat -> m a -> m a
escapeContext HasCallStack => Impossible
impossible Nat
1 (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
ftel)
          ]
        ModuleName -> TCM ()
addSection ModuleName
m

      -- Andreas, 2016-02-09, Issue 1815 (see also issue 1759).
      -- For checking the record declarations, hide the record parameters
      -- and the parameters of the parent modules.
      forall (tcm :: * -> *) a.
MonadTCEnv tcm =>
(forall e. Dom e -> Dom e) -> tcm a -> tcm a
modifyContextInfo (forall a. LensHiding a => a -> a
hideOrKeepInstance forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. LensQuantity a => a -> a
maybeErase) forall a b. (a -> b) -> a -> b
$ do
        -- The parameters are erased in the types of the projections.
        [ContextEntry]
params <- forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a. LensQuantity a => Quantity -> a -> a
applyQuantity Quantity
zeroQuantity) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). MonadTCEnv m => m [ContextEntry]
getContext

        -- Check the types of the fields and the other record declarations.
        TCM () -> TCM ()
addRecordVar forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. MonadTCEnv m => ModuleName -> m a -> m a
withCurrentModule ModuleName
m forall a b. (a -> b) -> a -> b
$ do

          -- Andreas, 2013-09-13, 2016-01-06.
          -- Argument telescope for the projections: all parameters are hidden.
          -- This means parameters of the parent modules and of the current
          -- record type.
          -- See test/Succeed/ProjectionsTakeModuleTelAsParameters.agda.
          Telescope
tel' <- do
            ContextEntry
r <- forall a. a -> [a] -> a
headWithDefault forall a. HasCallStack => a
__IMPOSSIBLE__ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). MonadTCEnv m => m [ContextEntry]
getContext
            forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. (a -> [Char]) -> ListTel' a -> Telescope
telFromList' Name -> [Char]
nameToArgName forall a b. (a -> b) -> a -> b
$ forall a. [a] -> [a]
reverse forall a b. (a -> b) -> a -> b
$ ContextEntry
r forall a. a -> [a] -> [a]
: [ContextEntry]
params
          ModuleName -> TCM ()
setModuleCheckpoint ModuleName
m
          ModuleName
-> QName
-> Bool
-> ConHead
-> Telescope
-> Telescope
-> [Field]
-> TCM ()
checkRecordProjections ModuleName
m QName
name Bool
hasNamedCon ConHead
con Telescope
tel' Telescope
ftel [Field]
fields


      -- we define composition here so that the projections are already in the signature.
      forall (m :: * -> *) a.
MonadAddContext m =>
Impossible -> Nat -> m a -> m a
escapeContext HasCallStack => Impossible
impossible Nat
npars forall a b. (a -> b) -> a -> b
$ do
        QName
-> ConHead
-> Telescope
-> [Arg QName]
-> Telescope
-> Type
-> TCM ()
addCompositionForRecord QName
name ConHead
con Telescope
tel (forall a b. (a -> b) -> [a] -> [b]
map forall t a. Dom' t a -> Arg a
argFromDom [Dom' Term QName]
fs) Telescope
ftel Type
rect

      -- The confluence checker needs to know what symbols match against
      -- the constructor.
      forall (m :: * -> *).
MonadTCState m =>
(Signature -> Signature) -> m ()
modifySignature forall a b. (a -> b) -> a -> b
$ QName -> (Definition -> Definition) -> Signature -> Signature
updateDefinition QName
conName forall a b. (a -> b) -> a -> b
$ \Definition
def ->
        Definition
def { defMatchable :: Set QName
defMatchable = forall a. Ord a => [a] -> Set a
Set.fromList forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall t e. Dom' t e -> e
unDom [Dom' Term QName]
fs }

  where
  -- Andreas, 2020-04-19, issue #4560
  -- If the user declared the record constructor as @pattern@,
  -- then switch on pattern matching for no-eta-equality.
  -- Default is no pattern matching, but definition by copatterns instead.
  patCopat :: PatternOrCopattern
patCopat = forall b a. b -> (a -> b) -> Maybe a -> b
maybe PatternOrCopattern
CopatternMatching (forall a b. a -> b -> a
const PatternOrCopattern
PatternMatching) Maybe Range
pat
  eta :: Maybe HasEta
eta      = (PatternOrCopattern
patCopat forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe HasEta0
eta0


addCompositionForRecord
  :: QName       -- ^ Datatype name.
  -> ConHead
  -> Telescope   -- ^ @Γ@ parameters.
  -> [Arg QName] -- ^ Projection names.
  -> Telescope   -- ^ @Γ ⊢ Φ@ field types.
  -> Type        -- ^ @Γ ⊢ T@ target type.
  -> TCM ()
addCompositionForRecord :: QName
-> ConHead
-> Telescope
-> [Arg QName]
-> Telescope
-> Type
-> TCM ()
addCompositionForRecord QName
name ConHead
con Telescope
tel [Arg QName]
fs Telescope
ftel Type
rect = do
  Telescope
cxt <- forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope
  forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext forall a b. (a -> b) -> a -> b
$ do

    -- Record has no fields: attach composition data to record constructor
    if forall a. Null a => a -> Bool
null [Arg QName]
fs then do
      CompKit
kit <- QName
-> ConHead
-> Telescope
-> [QName]
-> Telescope
-> Type
-> Boundary
-> TCM CompKit
defineCompData QName
name ConHead
con (forall t. Abstract t => Telescope -> t -> t
abstract Telescope
cxt Telescope
tel) [] Telescope
ftel Type
rect []
      forall (m :: * -> *).
MonadTCState m =>
(Signature -> Signature) -> m ()
modifySignature forall a b. (a -> b) -> a -> b
$ QName -> (Definition -> Definition) -> Signature -> Signature
updateDefinition (ConHead -> QName
conName ConHead
con) forall a b. (a -> b) -> a -> b
$ (Defn -> Defn) -> Definition -> Definition
updateTheDef forall a b. (a -> b) -> a -> b
$ \case
        r :: Defn
r@Constructor{} -> Defn
r { conComp :: CompKit
conComp = CompKit
kit, conProj :: Maybe [QName]
conProj = forall a. a -> Maybe a
Just [] }  -- no projections
        Defn
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__

    -- Record has fields: attach composition data to record type
    else do
      -- If record has irrelevant fields but irrelevant projections are disabled,
      -- we cannot generate composition data.
      CompKit
kit <- forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (forall (m :: * -> *) a. Monad m => a -> m a
return (forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any forall a. LensRelevance a => a -> Bool
isIrrelevant [Arg QName]
fs)
                  forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`and2M` do Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> Bool
optIrrelevantProjections forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions)
        {-then-} (forall (m :: * -> *) a. Monad m => a -> m a
return CompKit
emptyCompKit)
        {-else-} (QName
-> Telescope -> Telescope -> [Arg QName] -> Type -> TCM CompKit
defineCompKitR QName
name (forall t. Abstract t => Telescope -> t -> t
abstract Telescope
cxt Telescope
tel) Telescope
ftel [Arg QName]
fs Type
rect)
      forall (m :: * -> *).
MonadTCState m =>
(Signature -> Signature) -> m ()
modifySignature forall a b. (a -> b) -> a -> b
$ QName -> (Definition -> Definition) -> Signature -> Signature
updateDefinition QName
name forall a b. (a -> b) -> a -> b
$ (Defn -> Defn) -> Definition -> Definition
updateTheDef forall a b. (a -> b) -> a -> b
$ \case
        r :: Defn
r@Record{} -> Defn
r { recComp :: CompKit
recComp = CompKit
kit }
        Defn
_          -> forall a. HasCallStack => a
__IMPOSSIBLE__

defineCompKitR ::
    QName          -- ^ some name, e.g. record name
  -> Telescope   -- ^ param types Δ
  -> Telescope   -- ^ fields' types Δ ⊢ Φ
  -> [Arg QName] -- ^ fields' names
  -> Type        -- ^ record type Δ ⊢ T
  -> TCM CompKit
defineCompKitR :: QName
-> Telescope -> Telescope -> [Arg QName] -> Type -> TCM CompKit
defineCompKitR QName
name Telescope
params Telescope
fsT [Arg QName]
fns Type
rect = do
  [Maybe Term]
required <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall (m :: * -> *). HasBuiltins m => [Char] -> m (Maybe Term)
getTerm'
        [ [Char]
builtinInterval
        , [Char]
builtinIZero
        , [Char]
builtinIOne
        , [Char]
builtinIMin
        , [Char]
builtinIMax
        , [Char]
builtinINeg
        , [Char]
builtinPOr
        , [Char]
builtinItIsOne
        ]
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.rec.cxt" Nat
30 forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
params
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.rec.cxt" Nat
30 forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
fsT
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.rec.cxt" Nat
30 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Type
rect
  if Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all forall a. Maybe a -> Bool
isJust [Maybe Term]
required then forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ CompKit
emptyCompKit else do
    Maybe QName
transp <- forall {m :: * -> *} {t :: * -> *} {a}.
(Traversable t, HasBuiltins m) =>
t [Char] -> m (Maybe a) -> m (Maybe a)
whenDefined [[Char]
builtinTrans]              (Command
-> QName
-> Telescope
-> Telescope
-> [Arg QName]
-> Type
-> TCM (Maybe QName)
defineKanOperationR Command
DoTransp QName
name Telescope
params Telescope
fsT [Arg QName]
fns Type
rect)
    Maybe QName
hcomp  <- forall {m :: * -> *} {t :: * -> *} {a}.
(Traversable t, HasBuiltins m) =>
t [Char] -> m (Maybe a) -> m (Maybe a)
whenDefined [[Char]
builtinTrans,[Char]
builtinHComp] (Command
-> QName
-> Telescope
-> Telescope
-> [Arg QName]
-> Type
-> TCM (Maybe QName)
defineKanOperationR Command
DoHComp QName
name Telescope
params Telescope
fsT [Arg QName]
fns Type
rect)
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ CompKit
      { nameOfTransp :: Maybe QName
nameOfTransp = Maybe QName
transp
      , nameOfHComp :: Maybe QName
nameOfHComp  = Maybe QName
hcomp
      }
  where
    whenDefined :: t [Char] -> m (Maybe a) -> m (Maybe a)
whenDefined t [Char]
xs m (Maybe a)
m = do
      t (Maybe Term)
xs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall (m :: * -> *). HasBuiltins m => [Char] -> m (Maybe Term)
getTerm' t [Char]
xs
      if forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all forall a. Maybe a -> Bool
isJust t (Maybe Term)
xs then m (Maybe a)
m else forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing


defineKanOperationR
  :: Command
  -> QName       -- ^ some name, e.g. record name
  -> Telescope   -- ^ param types Δ
  -> Telescope   -- ^ fields' types Δ ⊢ Φ
  -> [Arg QName] -- ^ fields' names
  -> Type        -- ^ record type Δ ⊢ T
  -> TCM (Maybe QName)
defineKanOperationR :: Command
-> QName
-> Telescope
-> Telescope
-> [Arg QName]
-> Type
-> TCM (Maybe QName)
defineKanOperationR Command
cmd QName
name Telescope
params Telescope
fsT [Arg QName]
fns Type
rect = do
  let project :: Term -> QName -> Term
project = (\ Term
t QName
fn -> Term
t forall t. Apply t => t -> Elims -> t
`applyE` [forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
ProjSystem QName
fn])
  Maybe (QName, Telescope, Type, [Dom Type], [Term])
stuff <- forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Command
-> Maybe Term
-> (Term -> QName -> Term)
-> QName
-> Telescope
-> Telescope
-> [Arg QName]
-> Type
-> TCM
     (Maybe
        ((QName, Telescope, Type, [Dom Type], [Term]), Substitution))
defineKanOperationForFields Command
cmd forall a. Maybe a
Nothing Term -> QName -> Term
project QName
name Telescope
params Telescope
fsT [Arg QName]
fns Type
rect

  forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe (QName, Telescope, Type, [Dom Type], [Term])
stuff (forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing) forall a b. (a -> b) -> a -> b
$ \ (QName
theName, Telescope
gamma, Type
rtype, [Dom Type]
clause_types, [Term]
bodies) -> do
  -- phi = 1 clause
  Clause
c' <- do
           Term
io <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIOne
           Just QName
io_name <- forall (m :: * -> *). HasBuiltins m => [Char] -> m (Maybe QName)
getBuiltinName' [Char]
builtinIOne
           Term
one <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primItIsOne
           Type
tInterval <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Type
primIntervalType
           let
              (Nat
ix,Term
rhs) =
                case Command
cmd of
                  -- TranspRArgs = phi : I, a0 : ..
                  -- Γ = Δ^I , CompRArgs
                  -- pats = ... | phi = i1
                  -- body = a0
                  Command
DoTransp -> (Nat
1,Nat -> Elims -> Term
Var Nat
0 [])
                  -- HCompRArgs = phi : I, u : .., a0 : ..
                  -- Γ = Δ, CompRArgs
                  -- pats = ... | phi = i1
                  -- body = u i1 itIsOne
                  Command
DoHComp  -> (Nat
2,Nat -> Elims -> Term
Var Nat
1 [] forall t. Apply t => t -> [Arg Term] -> t
`apply` [forall e. e -> Arg e
argN Term
io, forall a. LensRelevance a => Relevance -> a -> a
setRelevance Relevance
Irrelevant forall a b. (a -> b) -> a -> b
$ forall e. e -> Arg e
argN Term
one])

              p :: Pattern' DBPatVar
p = forall x.
ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
ConP (QName -> DataOrRecord -> Induction -> [Arg QName] -> ConHead
ConHead QName
io_name DataOrRecord
IsData Induction
Inductive [])
                       (ConPatternInfo
noConPatternInfo { conPType :: Maybe (Arg Type)
conPType = forall a. a -> Maybe a
Just (forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
defaultArgInfo Type
tInterval)
                                         , conPFallThrough :: Bool
conPFallThrough = Bool
True })
                         []

              -- gamma, rtype

              s :: Substitution' (Pattern' DBPatVar)
s = forall a. DeBruijn a => Nat -> a -> Substitution' a
singletonS Nat
ix Pattern' DBPatVar
p

              pats :: [NamedArg DeBruijnPattern]
              pats :: [NamedArg (Pattern' DBPatVar)]
pats = Substitution' (Pattern' DBPatVar)
s forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` forall a t. DeBruijn a => Tele (Dom t) -> [NamedArg a]
teleNamedArgs Telescope
gamma

              t :: Type
              t :: Type
t = Substitution' (Pattern' DBPatVar)
s forall a.
TermSubst a =>
Substitution' (Pattern' DBPatVar) -> a -> a
`applyPatSubst` Type
rtype

              gamma' :: Telescope
              gamma' :: Telescope
gamma' = [[Char]] -> [Dom Type] -> Telescope
unflattenTel ([[Char]]
ns0 forall a. [a] -> [a] -> [a]
++ [[Char]]
ns1) forall a b. (a -> b) -> a -> b
$ Substitution' (Pattern' DBPatVar)
s forall a.
TermSubst a =>
Substitution' (Pattern' DBPatVar) -> a -> a
`applyPatSubst` ([Dom Type]
g0 forall a. [a] -> [a] -> [a]
++ [Dom Type]
g1)
               where
                ([Dom Type]
g0,Dom Type
_:[Dom Type]
g1) = forall a. Nat -> [a] -> ([a], [a])
splitAt (forall a. Sized a => a -> Nat
size Telescope
gamma forall a. Num a => a -> a -> a
- Nat
1 forall a. Num a => a -> a -> a
- Nat
ix) forall a b. (a -> b) -> a -> b
$ forall a. TermSubst a => Tele (Dom a) -> [Dom a]
flattenTel Telescope
gamma
                ([[Char]]
ns0,[Char]
_:[[Char]]
ns1) = forall a. Nat -> [a] -> ([a], [a])
splitAt (forall a. Sized a => a -> Nat
size Telescope
gamma forall a. Num a => a -> a -> a
- Nat
1 forall a. Num a => a -> a -> a
- Nat
ix) forall a b. (a -> b) -> a -> b
$ Telescope -> [[Char]]
teleNames Telescope
gamma

              c :: Clause
c = Clause { clauseFullRange :: Range
clauseFullRange = forall a. Range' a
noRange
                         , clauseLHSRange :: Range
clauseLHSRange  = forall a. Range' a
noRange
                         , clauseTel :: Telescope
clauseTel       = Telescope
gamma'
                         , namedClausePats :: [NamedArg (Pattern' DBPatVar)]
namedClausePats = [NamedArg (Pattern' DBPatVar)]
pats
                         , clauseBody :: Maybe Term
clauseBody      = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Term
rhs
                         , clauseType :: Maybe (Arg Type)
clauseType      = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall e. e -> Arg e
argN Type
t
                         , clauseCatchall :: Bool
clauseCatchall    = Bool
False
                         , clauseExact :: Maybe Bool
clauseExact       = forall a. a -> Maybe a
Just Bool
True
                         , clauseRecursive :: Maybe Bool
clauseRecursive   = forall a. a -> Maybe a
Just Bool
False  -- definitely non-recursive!
                         , clauseUnreachable :: Maybe Bool
clauseUnreachable = forall a. a -> Maybe a
Just Bool
False
                         , clauseEllipsis :: ExpandedEllipsis
clauseEllipsis    = ExpandedEllipsis
NoEllipsis
                         , clauseWhereModule :: Maybe ModuleName
clauseWhereModule = forall a. Maybe a
Nothing
                         }
           forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"trans.rec.face" Nat
17 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> [Char]
show Clause
c
           forall (m :: * -> *) a. Monad m => a -> m a
return Clause
c
  [Clause]
cs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (forall a b c. [a] -> [b] -> [c] -> [(a, b, c)]
zip3 [Arg QName]
fns [Dom Type]
clause_types [Term]
bodies) forall a b. (a -> b) -> a -> b
$ \ (Arg QName
fname, Dom Type
clause_ty, Term
body) -> do
          let
              pats :: [NamedArg (Pattern' DBPatVar)]
pats = forall a t. DeBruijn a => Tele (Dom t) -> [NamedArg a]
teleNamedArgs Telescope
gamma forall a. [a] -> [a] -> [a]
++ [forall a. a -> NamedArg a
defaultNamedArg forall a b. (a -> b) -> a -> b
$ forall x. ProjOrigin -> QName -> Pattern' x
ProjP ProjOrigin
ProjSystem forall a b. (a -> b) -> a -> b
$ forall e. Arg e -> e
unArg Arg QName
fname]
              c :: Clause
c = Clause { clauseFullRange :: Range
clauseFullRange = forall a. Range' a
noRange
                         , clauseLHSRange :: Range
clauseLHSRange  = forall a. Range' a
noRange
                         , clauseTel :: Telescope
clauseTel       = Telescope
gamma
                         , namedClausePats :: [NamedArg (Pattern' DBPatVar)]
namedClausePats = [NamedArg (Pattern' DBPatVar)]
pats
                         , clauseBody :: Maybe Term
clauseBody      = forall a. a -> Maybe a
Just Term
body
                         , clauseType :: Maybe (Arg Type)
clauseType      = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall e. e -> Arg e
argN (forall t e. Dom' t e -> e
unDom Dom Type
clause_ty)
                         , clauseCatchall :: Bool
clauseCatchall    = Bool
False
                         , clauseExact :: Maybe Bool
clauseExact       = forall a. a -> Maybe a
Just Bool
True
                         , clauseRecursive :: Maybe Bool
clauseRecursive   = forall a. Maybe a
Nothing
                             -- Andreas 2020-02-06 TODO
                             -- Or: Just False;  is it known to be non-recursive?
                         , clauseUnreachable :: Maybe Bool
clauseUnreachable = forall a. a -> Maybe a
Just Bool
False
                         , clauseEllipsis :: ExpandedEllipsis
clauseEllipsis    = ExpandedEllipsis
NoEllipsis
                         , clauseWhereModule :: Maybe ModuleName
clauseWhereModule = forall a. Maybe a
Nothing
                         }
          forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"trans.rec" Nat
17 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> [Char]
show Clause
c
          forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"trans.rec" Nat
16 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
"type =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => [Char] -> m Doc
text (forall a. Show a => a -> [Char]
show (Clause -> Maybe (Arg Type)
clauseType Clause
c))
          forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"trans.rec" Nat
15 forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM forall a b. (a -> b) -> a -> b
$ forall t. Abstract t => Telescope -> t -> t
abstract Telescope
gamma (forall t e. Dom' t e -> e
unDom Dom Type
clause_ty)
          forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"trans.rec" Nat
10 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
"body =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (forall t. Abstract t => Telescope -> t -> t
abstract Telescope
gamma Term
body)
          forall (m :: * -> *) a. Monad m => a -> m a
return Clause
c
  forall (m :: * -> *).
(MonadConstraint m, MonadTCState m) =>
QName -> [Clause] -> m ()
addClauses QName
theName forall a b. (a -> b) -> a -> b
$ Clause
c' forall a. a -> [a] -> [a]
: [Clause]
cs
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"trans.rec" Nat
15 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall a b. (a -> b) -> a -> b
$ [Char]
"compiling clauses for " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show QName
theName
  (Maybe SplitTree
mst, Bool
_, CompiledClauses
cc) <- forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (Maybe (QName, Type)
-> [Clause] -> TCM (Maybe SplitTree, Bool, CompiledClauses)
compileClauses forall a. Maybe a
Nothing [Clause]
cs)
  forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
whenJust Maybe SplitTree
mst forall a b. (a -> b) -> a -> b
$ QName -> SplitTree -> TCM ()
setSplitTree QName
theName
  QName -> CompiledClauses -> TCM ()
setCompiledClauses QName
theName CompiledClauses
cc
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"trans.rec" Nat
15 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall a b. (a -> b) -> a -> b
$ [Char]
"compiled"
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just QName
theName


{-| @checkRecordProjections m r q tel ftel fs@.

    [@m@    ]  name of the generated module

    [@r@    ]  name of the record type

    [@con@  ]  name of the record constructor

    [@tel@  ]  parameters (erased) and record variable r ("self")

    [@ftel@ ]  telescope of fields

    [@fs@   ]  the fields to be checked
-}
checkRecordProjections ::
  ModuleName -> QName -> Bool -> ConHead -> Telescope -> Telescope ->
  [A.Declaration] -> TCM ()
checkRecordProjections :: ModuleName
-> QName
-> Bool
-> ConHead
-> Telescope
-> Telescope
-> [Field]
-> TCM ()
checkRecordProjections ModuleName
m QName
r Bool
hasNamedCon ConHead
con Telescope
tel Telescope
ftel [Field]
fs = do
    Telescope -> Telescope -> [Term] -> [Field] -> TCM ()
checkProjs forall a. Tele a
EmptyTel Telescope
ftel [] [Field]
fs
  where

    checkProjs :: Telescope -> Telescope -> [Term] -> [A.Declaration] -> TCM ()

    checkProjs :: Telescope -> Telescope -> [Term] -> [Field] -> TCM ()
checkProjs Telescope
_ Telescope
_ [Term]
_ [] = forall (m :: * -> *) a. Monad m => a -> m a
return ()

    checkProjs Telescope
ftel1 Telescope
ftel2 [Term]
vs (A.ScopedDecl ScopeInfo
scope [Field]
fs' : [Field]
fs) =
      ScopeInfo -> TCM ()
setScope ScopeInfo
scope forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Telescope -> Telescope -> [Term] -> [Field] -> TCM ()
checkProjs Telescope
ftel1 Telescope
ftel2 [Term]
vs ([Field]
fs' forall a. [a] -> [a] -> [a]
++ [Field]
fs)

    -- Case: projection.
    checkProjs Telescope
ftel1 (ExtendTel (dom :: Dom Type
dom@Dom{domInfo :: forall t e. Dom' t e -> ArgInfo
domInfo = ArgInfo
ai,unDom :: forall t e. Dom' t e -> e
unDom = Type
t}) Abs Telescope
ftel2) [Term]
vs (A.Field DefInfo
info QName
x Arg Expr
_ : [Field]
fs) =
      forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
traceCall (Range -> QName -> Type -> Call
CheckProjection (forall a. HasRange a => a -> Range
getRange DefInfo
info) QName
x Type
t) forall a b. (a -> b) -> a -> b
$ do
      -- Andreas, 2012-06-07:
      -- Issue 387: It is wrong to just type check field types again
      -- because then meta variables are created again.
      -- Instead, we take the field type t from the field telescope.
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.rec.proj" Nat
5 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
        [ TCMT IO Doc
"checking projection" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
x
        , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
          [ TCMT IO Doc
"top   =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope)
          , TCMT IO Doc
"tel   =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM forall a b. (a -> b) -> a -> b
$ Telescope
tel)
          ]
        ]
      -- Andreas, 2021-05-11, issue #5378
      -- The impossible is sometimes possible, so splitting out this part...
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.rec.proj" Nat
5 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
          [ TCMT IO Doc
"ftel1 =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a.
MonadAddContext m =>
Impossible -> Nat -> m a -> m a
escapeContext HasCallStack => Impossible
impossible Nat
1 (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
ftel1)
          , TCMT IO Doc
"t     =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a.
MonadAddContext m =>
Impossible -> Nat -> m a -> m a
escapeContext HasCallStack => Impossible
impossible Nat
1 (forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
ftel1 forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t)
          , TCMT IO Doc
"ftel2 =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a.
MonadAddContext m =>
Impossible -> Nat -> m a -> m a
escapeContext HasCallStack => Impossible
impossible Nat
1 (forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
ftel1 forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *) b.
(Subst a, MonadAddContext m) =>
Dom Type -> Abs a -> (a -> m b) -> m b
underAbstraction Dom Type
dom Abs Telescope
ftel2 forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM)
          ]
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.rec.proj" Nat
55 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
          [ TCMT IO Doc
"ftel1 (raw) =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Telescope
ftel1
          , TCMT IO Doc
"t     (raw) =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Type
t
          , TCMT IO Doc
"ftel2 (raw) =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Abs Telescope
ftel2
          ]
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.rec.proj" Nat
5 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
          [ TCMT IO Doc
"vs    =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ (forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [Term]
vs)
          , TCMT IO Doc
"abstr =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> [Char]
show) (forall t. DefInfo' t -> IsAbstract
Info.defAbstract DefInfo
info)
          , TCMT IO Doc
"quant =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> [Char]
show) (forall a. LensQuantity a => a -> Quantity
getQuantity ArgInfo
ai)
          , TCMT IO Doc
"coh   =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> [Char]
show) (forall a. LensCohesion a => a -> Cohesion
getCohesion ArgInfo
ai)
          ]

      -- Cohesion check:
      -- For a field `@c π : A` we would create a projection `π : .., (@(c^-1) r : R as) -> A`
      -- So we want to check that `@.., (c^-1 . c) x : A |- x : A` is allowed by the modalities.
      --
      -- Alternatively we could create a projection `.. |- π r :c A`
      -- but that would require support for a `t :c A` judgment.
      if forall a. LeftClosedPOMonoid a => a -> Bool
hasLeftAdjoint (forall t. t -> UnderComposition t
UnderComposition (forall a. LensCohesion a => a -> Cohesion
getCohesion ArgInfo
ai))
        then forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a. LensCohesion a => a -> Cohesion
getCohesion ArgInfo
ai forall a. Eq a => a -> a -> Bool
== Cohesion
Continuous)
                    -- Andrea TODO: properly update the context/type of the projection when we add Sharp
                    forall a. HasCallStack => a
__IMPOSSIBLE__
        else forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
[Char] -> m a
genericError forall a b. (a -> b) -> a -> b
$ [Char]
"Cannot have record fields with modality " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (forall a. LensCohesion a => a -> Cohesion
getCohesion ArgInfo
ai)

      -- The telescope tel includes the variable of record type as last one
      -- e.g. for cartesion product it is
      --
      --   tel = {A' : Set} {B' : Set} (r : Prod A' B')

      -- create the projection functions (instantiate the type with the values
      -- of the previous fields)

      -- The type of the projection function should be
      --  {Δ} -> (r : R Δ) -> t
      -- where Δ are the parameters of R

      {- what are the contexts?

          Δ , ftel₁              ⊢ t
          Δ , (r : R Δ)          ⊢ parallelS vs : ftel₁
          Δ , (r : R Δ) , ftel₁  ⊢ t' = raiseFrom (size ftel₁) 1 t
          Δ , (r : R Δ)          ⊢ t'' = applySubst (parallelS vs) t'
                                 ⊢ finalt = telePi tel t''
      -}
      let t' :: Type
t'       = forall a. Subst a => Nat -> Nat -> a -> a
raiseFrom (forall a. Sized a => a -> Nat
size Telescope
ftel1) Nat
1 Type
t
          t'' :: Type
t''      = forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst (forall a. DeBruijn a => [a] -> Substitution' a
parallelS [Term]
vs) Type
t'
          finalt :: Type
finalt   = Telescope -> Type -> Type
telePi (forall a. [Char] -> Tele a -> Tele a
replaceEmptyName [Char]
"r" Telescope
tel) Type
t''
          projname :: QName
projname = ModuleName -> Name -> QName
qualify ModuleName
m forall a b. (a -> b) -> a -> b
$ QName -> Name
qnameName QName
x
          projcall :: ProjOrigin -> Term
projcall ProjOrigin
o = Nat -> Elims -> Term
Var Nat
0 [forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
o QName
projname]
          rel :: Relevance
rel      = forall a. LensRelevance a => a -> Relevance
getRelevance ArgInfo
ai
          -- the recursive call
          recurse :: TCM ()
recurse  = Telescope -> Telescope -> [Term] -> [Field] -> TCM ()
checkProjs (forall t. Abstract t => Telescope -> t -> t
abstract Telescope
ftel1 forall a b. (a -> b) -> a -> b
$ forall a. a -> Abs (Tele a) -> Tele a
ExtendTel Dom Type
dom
                                 forall a b. (a -> b) -> a -> b
$ forall a. [Char] -> a -> Abs a
Abs (Name -> [Char]
nameToArgName forall a b. (a -> b) -> a -> b
$ QName -> Name
qnameName QName
projname) forall a. Tele a
EmptyTel)
                                (forall a. Subst a => Abs a -> a
absBody Abs Telescope
ftel2) (ProjOrigin -> Term
projcall ProjOrigin
ProjSystem forall a. a -> [a] -> [a]
: [Term]
vs) [Field]
fs

      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.rec.proj" Nat
25 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"finalt=" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do
        forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
finalt

      -- -- Andreas, 2012-02-20 do not add irrelevant projections if
      -- -- disabled by --no-irrelevant-projections
      -- ifM (return (rel == Irrelevant) `and2M` do not . optIrrelevantProjections <$> pragmaOptions) recurse $ do
      -- Andreas, 2018-06-09 issue #2170
      -- Always create irrelevant projections (because the scope checker accepts irrelevant fields).
      -- If --no-irrelevant-projections, then their use should be disallowed by the type checker for expressions.
      do
        forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.rec.proj" Nat
10 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
          [ TCMT IO Doc
"adding projection"
          , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
projname forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
finalt)
          ]

        -- The body should be
        --  P.xi {tel} (r _ .. x .. _) = x
        -- Ulf, 2011-08-22: actually we're dropping the parameters from the
        -- projection functions so the body is now
        --  P.xi (r _ .. x .. _) = x
        -- Andreas, 2012-01-12: irrelevant projections get translated to
        --  P.xi (r _ .. x .. _) = irrAxiom {level of t} {t} x
        -- PROBLEM: because of dropped parameters, cannot refer to t
        -- 2012-04-02: DontCare instead of irrAxiom

        -- compute body modification for irrelevant projections
        let bodyMod :: Term -> Term
bodyMod = case Relevance
rel of
              Relevance
Relevant   -> forall a. a -> a
id
              Relevance
NonStrict  -> forall a. a -> a
id
              Relevance
Irrelevant -> Term -> Term
dontCare

        let -- Andreas, 2010-09-09: comment for existing code
            -- split the telescope into parameters (ptel) and the type or the record
            -- (rt) which should be  R ptel
            telList :: [Dom ([Char], Type)]
telList = forall t. Tele (Dom t) -> [Dom ([Char], t)]
telToList Telescope
tel
            ([Dom ([Char], Type)]
ptelList,[Dom ([Char], Type)
rt]) = forall a. Nat -> [a] -> ([a], [a])
splitAt (forall a. Sized a => a -> Nat
size Telescope
tel forall a. Num a => a -> a -> a
- Nat
1) [Dom ([Char], Type)]
telList
            ptel :: Telescope
ptel   = [Dom ([Char], Type)] -> Telescope
telFromList [Dom ([Char], Type)]
ptelList
            cpo :: PatOrigin
cpo    = if Bool
hasNamedCon then PatOrigin
PatOCon else PatOrigin
PatORec
            cpi :: ConPatternInfo
cpi    = ConPatternInfo { conPInfo :: PatternInfo
conPInfo   = PatOrigin -> [Name] -> PatternInfo
PatternInfo PatOrigin
cpo []
                                    , conPRecord :: Bool
conPRecord = Bool
True
                                    , conPFallThrough :: Bool
conPFallThrough = Bool
False
                                    , conPType :: Maybe (Arg Type)
conPType   = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall t a. Dom' t a -> Arg a
argFromDom forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a, b) -> b
snd Dom ([Char], Type)
rt
                                    , conPLazy :: Bool
conPLazy   = Bool
True }
            conp :: NamedArg (Pattern' DBPatVar)
conp   = forall a. a -> NamedArg a
defaultNamedArg forall a b. (a -> b) -> a -> b
$ forall x.
ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
ConP ConHead
con ConPatternInfo
cpi forall a b. (a -> b) -> a -> b
$ forall a t. DeBruijn a => Tele (Dom t) -> [NamedArg a]
teleNamedArgs Telescope
ftel
            body :: Maybe Term
body   = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Term -> Term
bodyMod forall a b. (a -> b) -> a -> b
$ Nat -> Term
var (forall a. Sized a => a -> Nat
size Abs Telescope
ftel2)
            cltel :: Telescope
cltel  = Telescope
ptel forall t. Abstract t => Telescope -> t -> t
`abstract` Telescope
ftel
            cltype :: Maybe (Arg Type)
cltype = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai forall a b. (a -> b) -> a -> b
$ forall a. Subst a => Nat -> a -> a
raise (Nat
1 forall a. Num a => a -> a -> a
+ forall a. Sized a => a -> Nat
size Abs Telescope
ftel2) Type
t
            clause :: Clause
clause = Clause { clauseLHSRange :: Range
clauseLHSRange  = forall a. HasRange a => a -> Range
getRange DefInfo
info
                            , clauseFullRange :: Range
clauseFullRange = forall a. HasRange a => a -> Range
getRange DefInfo
info
                            , clauseTel :: Telescope
clauseTel       = forall a. KillRange a => KillRangeT a
killRange Telescope
cltel
                            , namedClausePats :: [NamedArg (Pattern' DBPatVar)]
namedClausePats = [NamedArg (Pattern' DBPatVar)
conp]
                            , clauseBody :: Maybe Term
clauseBody      = Maybe Term
body
                            , clauseType :: Maybe (Arg Type)
clauseType      = Maybe (Arg Type)
cltype
                            , clauseCatchall :: Bool
clauseCatchall  = Bool
False
                            , clauseExact :: Maybe Bool
clauseExact       = forall a. a -> Maybe a
Just Bool
True
                            , clauseRecursive :: Maybe Bool
clauseRecursive   = forall a. a -> Maybe a
Just Bool
False
                            , clauseUnreachable :: Maybe Bool
clauseUnreachable = forall a. a -> Maybe a
Just Bool
False
                            , clauseEllipsis :: ExpandedEllipsis
clauseEllipsis    = ExpandedEllipsis
NoEllipsis
                            , clauseWhereModule :: Maybe ModuleName
clauseWhereModule = forall a. Maybe a
Nothing
                            }

        let projection :: Projection
projection = Projection
              { projProper :: Maybe QName
projProper   = forall a. a -> Maybe a
Just QName
r
              , projOrig :: QName
projOrig     = QName
projname
              -- name of the record type:
              , projFromType :: Arg QName
projFromType = forall e. e -> Arg e
defaultArg QName
r
              -- index of the record argument (in the type),
              -- start counting with 1:
              , projIndex :: Nat
projIndex    = forall a. Sized a => a -> Nat
size Telescope
tel -- which is @size ptel + 1@
              , projLams :: ProjLams
projLams     = [Arg [Char]] -> ProjLams
ProjLams forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall t a. Dom' t a -> Arg a
argFromDom forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a, b) -> a
fst) [Dom ([Char], Type)]
telList
              }

        forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.rec.proj" Nat
70 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
          [ TCMT IO Doc
"adding projection"
          , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
projname forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Clause
clause
          ]
        forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.rec.proj" Nat
10 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
          [ TCMT IO Doc
"adding projection"
          , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (forall a. QName -> a -> QNamed a
QNamed QName
projname Clause
clause)
          ]

              -- Record patterns should /not/ be translated when the
              -- projection functions are defined. Record pattern
              -- translation is defined in terms of projection
              -- functions.
        (Maybe SplitTree
mst, Bool
_, CompiledClauses
cc) <- Maybe (QName, Type)
-> [Clause] -> TCM (Maybe SplitTree, Bool, CompiledClauses)
compileClauses forall a. Maybe a
Nothing [Clause
clause]

        forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.cc" Nat
60 forall a b. (a -> b) -> a -> b
$ do
          forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ TCMT IO Doc
"compiled clauses of " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
projname
              , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => [Char] -> m Doc
text (forall a. Show a => a -> [Char]
show CompiledClauses
cc)
              ]

        forall (m :: * -> *) a.
MonadAddContext m =>
Impossible -> Nat -> m a -> m a
escapeContext HasCallStack => Impossible
impossible (forall a. Sized a => a -> Nat
size Telescope
tel) forall a b. (a -> b) -> a -> b
$ do
          Language
lang <- forall (m :: * -> *). HasOptions m => m Language
getLanguage
          QName -> Definition -> TCM ()
addConstant QName
projname forall a b. (a -> b) -> a -> b
$
            (ArgInfo -> QName -> Type -> Language -> Defn -> Definition
defaultDefn ArgInfo
ai QName
projname (forall a. KillRange a => KillRangeT a
killRange Type
finalt) Language
lang forall a b. (a -> b) -> a -> b
$ FunctionData -> Defn
FunctionDefn
              FunctionData
emptyFunctionData
                { _funClauses :: [Clause]
_funClauses        = [Clause
clause]
                , _funCompiled :: Maybe CompiledClauses
_funCompiled       = forall a. a -> Maybe a
Just CompiledClauses
cc
                , _funSplitTree :: Maybe SplitTree
_funSplitTree      = Maybe SplitTree
mst
                , _funProjection :: Either ProjectionLikenessMissing Projection
_funProjection     = forall a b. b -> Either a b
Right Projection
projection
                , _funMutual :: Maybe [QName]
_funMutual         = forall a. a -> Maybe a
Just []  -- Projections are not mutually recursive with anything
                , _funTerminates :: Maybe Bool
_funTerminates     = forall a. a -> Maybe a
Just Bool
True
                })
              { defArgOccurrences :: [Occurrence]
defArgOccurrences = [Occurrence
StrictPos]
              , defCopatternLHS :: Bool
defCopatternLHS   = CompiledClauses -> Bool
hasProjectionPatterns CompiledClauses
cc
              }
          forall (m :: * -> *).
(HasOptions m, HasConstInfo m, HasBuiltins m, MonadTCEnv m,
 MonadTCState m, MonadReduce m, MonadAddContext m, MonadTCError m,
 MonadDebug m, MonadPretty m) =>
[QName] -> m ()
computePolarity [QName
projname]

        case forall t. DefInfo' t -> IsInstance
Info.defInstance DefInfo
info of
          -- fields do not have an @instance@ keyword!?
          InstanceDef Range
_r -> QName -> Type -> TCM ()
addTypedInstance QName
projname Type
t
          IsInstance
NotInstanceDef -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

        TCM ()
recurse

    -- Case: definition.
    checkProjs Telescope
ftel1 Telescope
ftel2 [Term]
vs (Field
d : [Field]
fs) = do
      Field -> TCM ()
checkDecl Field
d
      Telescope -> Telescope -> [Term] -> [Field] -> TCM ()
checkProjs Telescope
ftel1 Telescope
ftel2 [Term]
vs [Field]
fs