{-# 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 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, fitsIn, forceSort,
                                      defineCompData, defineTranspOrHCompForFields )
import Agda.TypeChecking.Rules.Term ( isType_ )
import {-# SOURCE #-} Agda.TypeChecking.Rules.Decl (checkDecl)

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

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

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

      let tel :: Telescope
tel = Telescope -> Telescope -> Telescope
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.
      VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.rec" VerboseLevel
15 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"checking fields"
      Type
contype <- TCMT IO Type -> TCMT IO Type
forall (m :: * -> *) a.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
m a -> m a
workOnTypes (TCMT IO Type -> TCMT IO Type) -> TCMT IO Type -> TCMT IO Type
forall a b. (a -> b) -> a -> b
$ Type -> TCMT IO Type
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull (Type -> TCMT IO Type) -> TCMT IO Type -> TCMT IO Type
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Expr -> TCMT IO Type
isType_ Expr
contel
      VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.rec" VerboseLevel
20 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
        [ TCM Doc
"contype = " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCM 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 <- Type -> TCMT IO (TelV Type)
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView Type
t0
      Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Telescope -> Bool
forall a. Null a => a -> Bool
null Telescope
idxTel) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ TypeError -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
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

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

      -- record type (name applied to parameters)
      Type
rect <- Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El Sort
s (Term -> Type) -> ([Arg Term] -> Term) -> [Arg Term] -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Elims -> Term
Def QName
name (Elims -> Term) -> ([Arg Term] -> Elims) -> [Arg Term] -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Arg Term -> Elim' Term) -> [Arg Term] -> Elims
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply ([Arg Term] -> Type) -> TCMT IO [Arg Term] -> TCMT IO Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO [Arg Term]
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 (VerboseLevel -> Type -> Type
forall a. Subst a => VerboseLevel -> a -> a
raise (Telescope -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
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  -> (Bool, QName) -> TCMT IO (Bool, QName)
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
True, QName
c)
        Maybe QName
Nothing -> do
          ModuleName
m <- KillRangeT ModuleName
forall a. KillRange a => KillRangeT a
killRange KillRangeT ModuleName -> TCMT IO ModuleName -> TCMT IO ModuleName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO ModuleName
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 = Name -> Doc
forall a. Pretty a => a -> Doc
P.pretty (Name -> Doc) -> Name -> Doc
forall a b. (a -> b) -> a -> b
$ QName -> Name
qnameName QName
name
          QName
c <- ModuleName -> Name -> QName
qualify ModuleName
m (Name -> QName) -> TCMT IO Name -> TCMT IO QName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> VerboseKey -> TCMT IO Name
forall a (m :: * -> *).
(FreshName a, MonadFresh NameId m) =>
a -> m Name
freshName_ (Doc -> VerboseKey
render Doc
r VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseKey
".constructor")
          (Bool, QName) -> TCMT IO (Bool, QName)
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, QName
c)

      -- Add record type to signature.
      VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.rec" VerboseLevel
15 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"adding record type to signature"

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

      let getName :: A.Declaration -> [Dom QName]
          getName :: Field -> [Dom QName]
getName (A.Field DefInfo
_ QName
x Arg Expr
arg)    = [QName
x QName -> Dom' Term Expr -> Dom QName
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Arg Expr -> Dom' Term Expr
forall a. Arg a -> Dom a
domFromArg Arg Expr
arg]
          getName (A.ScopedDecl ScopeInfo
_ [Field
f]) = Field -> [Dom 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 = Dom' t e -> Maybe t
forall t e. Dom' t e -> Maybe t
domTactic Dom' t e
dom }

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

          -- indCo is what the user wrote: inductive/coinductive/Nothing.
          -- We drop the Range.
          indCo :: Maybe Induction
indCo = Ranged Induction -> Induction
forall a. Ranged a -> a
rangedThing (Ranged Induction -> Induction)
-> Maybe (Ranged Induction) -> Maybe Induction
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 = Induction -> Maybe Induction -> Induction
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      = EtaEquality
-> (HasEta -> EtaEquality) -> Maybe HasEta -> EtaEquality
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (HasEta -> EtaEquality
Inferred (HasEta -> EtaEquality) -> HasEta -> EtaEquality
forall a b. (a -> b) -> a -> b
$ PatternOrCopattern -> HasEta
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 ([Arg QName] -> ConHead) -> [Arg QName] -> ConHead
forall a b. (a -> b) -> a -> b
$ (Dom QName -> Arg QName) -> [Dom QName] -> [Arg QName]
forall a b. (a -> b) -> [a] -> [b]
map Dom QName -> Arg QName
forall t a. Dom' t a -> Arg a
argFromDom [Dom 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                   = [Relevance] -> Relevance
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
minimum ([Relevance] -> Relevance) -> [Relevance] -> Relevance
forall a b. (a -> b) -> a -> b
$ Relevance
Irrelevant Relevance -> [Relevance] -> [Relevance]
forall a. a -> [a] -> [a]
: (Dom' Term (VerboseKey, Type) -> Relevance)
-> [Dom' Term (VerboseKey, Type)] -> [Relevance]
forall a b. (a -> b) -> [a] -> [b]
map Dom' Term (VerboseKey, Type) -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance (Telescope -> [Dom' Term (VerboseKey, Type)]
forall t. Tele (Dom t) -> [Dom (VerboseKey, t)]
telToList Telescope
ftel)

      -- Andreas, 2017-01-26, issue #2436
      -- Disallow coinductive records with eta-equality
      Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Induction
conInduction Induction -> Induction -> Bool
forall a. Eq a => a -> a -> Bool
== Induction
CoInductive Bool -> Bool -> Bool
&& EtaEquality -> HasEta
theEtaEquality EtaEquality
haveEta HasEta -> HasEta -> Bool
forall a. Eq a => a -> a -> Bool
== HasEta
forall a. HasEta' a
YesEta) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
        TypeError -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM ()) -> (Doc -> TypeError) -> Doc -> TCM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError (Doc -> TCM ()) -> TCM Doc -> TCM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
          [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ TCM Doc
"Agda doesn't like coinductive records with eta-equality."
              , TCM Doc
"If you must, use pragma"
              , TCM Doc
"{-# ETA" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
name TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
"#-}"
              ]
      VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.rec" VerboseLevel
30 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"record constructor is " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ConHead -> TCM 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.
      Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Induction
conInduction Induction -> Induction -> Bool
forall a. Eq a => a -> a -> Bool
== Induction
CoInductive) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
        Bool
guardedness <- WithDefault 'False -> Bool
forall (b :: Bool). KnownBool b => WithDefault b -> Bool
collapseDefault (WithDefault 'False -> Bool)
-> (PragmaOptions -> WithDefault 'False) -> PragmaOptions -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> WithDefault 'False
optGuardedness (PragmaOptions -> Bool) -> TCMT IO PragmaOptions -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
        Bool
sizedTypes  <- WithDefault 'False -> Bool
forall (b :: Bool). KnownBool b => WithDefault b -> Bool
collapseDefault (WithDefault 'False -> Bool)
-> (PragmaOptions -> WithDefault 'False) -> PragmaOptions -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> WithDefault 'False
optSizedTypes  (PragmaOptions -> Bool) -> TCMT IO PragmaOptions -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
        Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Bool
guardedness Bool -> Bool -> Bool
|| Bool
sizedTypes) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ Warning -> TCM ()
forall (m :: * -> *).
(HasCallStack, MonadWarning m) =>
Warning -> m ()
warning (Warning -> TCM ()) -> Warning -> TCM ()
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 :: VerboseLevel
npars = Telescope -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size Telescope
tel
          telh :: Telescope
telh  = (Dom Type -> Dom Type) -> Telescope -> Telescope
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Dom Type -> Dom Type
forall a. (LensHiding a, LensRelevance a) => a -> a
hideAndRelParams Telescope
tel
      Impossible -> VerboseLevel -> TCM () -> TCM ()
forall (m :: * -> *) a.
MonadAddContext m =>
Impossible -> VerboseLevel -> m a -> m a
escapeContext Impossible
HasCallStack => Impossible
impossible VerboseLevel
npars (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
        QName -> ArgInfo -> QName -> Type -> Defn -> TCM ()
addConstant' QName
name ArgInfo
defaultArgInfo QName
name Type
t (Defn -> TCM ()) -> Defn -> TCM ()
forall a b. (a -> b) -> a -> b
$
            Record :: VerboseLevel
-> Maybe Clause
-> ConHead
-> Bool
-> [Dom QName]
-> Telescope
-> Maybe [QName]
-> EtaEquality
-> PatternOrCopattern
-> Maybe Induction
-> IsAbstract
-> CompKit
-> Defn
Record
              { recPars :: VerboseLevel
recPars           = VerboseLevel
npars
              , recClause :: Maybe Clause
recClause         = Maybe Clause
forall a. Maybe a
Nothing
              , recConHead :: ConHead
recConHead        = ConHead
con
              , recNamedCon :: Bool
recNamedCon       = Bool
hasNamedCon
              , recFields :: [Dom QName]
recFields         = [Dom QName]
fs
              , recTel :: Telescope
recTel            = Telescope
telh Telescope -> Telescope -> Telescope
forall t. Abstract t => Telescope -> t -> t
`abstract` Telescope
ftel
              , recAbstr :: IsAbstract
recAbstr          = DefInfo -> IsAbstract
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         = Maybe [QName]
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
            (Telescope
telh Telescope -> Type -> Type
forall t. Abstract t => Telescope -> t -> t
`abstract` Type
contype) (Defn -> TCM ()) -> Defn -> TCM ()
forall a b. (a -> b) -> a -> b
$
            Constructor :: VerboseLevel
-> VerboseLevel
-> ConHead
-> QName
-> IsAbstract
-> Induction
-> CompKit
-> Maybe [QName]
-> [IsForced]
-> Maybe [Bool]
-> Defn
Constructor
              { conPars :: VerboseLevel
conPars   = VerboseLevel
npars
              , conArity :: VerboseLevel
conArity  = [Dom QName] -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size [Dom QName]
fs
              , conSrcCon :: ConHead
conSrcCon = ConHead
con
              , conData :: QName
conData   = QName
name
              , conAbstr :: IsAbstract
conAbstr  = DefInfo -> IsAbstract
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   = Maybe [QName]
forall a. Maybe a
Nothing       -- filled in later
              , conForced :: [IsForced]
conForced = []
              , conErased :: Maybe [Bool]
conErased = Maybe [Bool]
forall a. Maybe a
Nothing
              }

      -- Declare the constructor as eligible for instance search
      case DefInfo -> IsInstance
forall t. DefInfo' t -> IsInstance
Info.defInstance DefInfo
i of
        InstanceDef Range
r -> Range -> TCM () -> TCM ()
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange Range
r (TCM () -> TCM ()) -> TCM () -> TCM ()
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 -> () -> TCM ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

      -- Check that the fields fit inside the sort
      VerboseLevel
_ <- UniverseCheck -> [IsForced] -> Type -> Sort -> TCM VerboseLevel
fitsIn UniverseCheck
uc [] Type
contype 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 = Relevance -> ArgInfo -> ArgInfo
forall a. LensRelevance a => Relevance -> a -> a
setRelevance Relevance
recordRelevance ArgInfo
defaultArgInfo
          addRecordVar :: TCM () -> TCM ()
addRecordVar =
            Dom Type -> TCM () -> TCM ()
forall (m :: * -> *) b.
(MonadAddContext m, MonadFresh NameId m) =>
Dom Type -> m b -> m b
addRecordNameContext (ArgInfo -> Dom Type -> Dom Type
forall a. LensArgInfo a => ArgInfo -> a -> a
setArgInfo ArgInfo
info (Dom Type -> Dom Type) -> Dom Type -> Dom Type
forall a b. (a -> b) -> a -> b
$ Type -> Dom Type
forall a. a -> Dom a
defaultDom Type
rect)

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

      -- 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 e. Dom e -> Dom e) -> TCM () -> TCM ()
forall (tcm :: * -> *) a.
MonadTCEnv tcm =>
(forall e. Dom e -> Dom e) -> tcm a -> tcm a
modifyContextInfo forall a. LensHiding a => a -> a
forall e. Dom e -> Dom e
hideOrKeepInstance (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM () -> TCM ()
addRecordVar (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do

        -- Add the record section.

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

        -- Check the types of the fields and the other record declarations.
        ModuleName -> TCM () -> TCM ()
forall (m :: * -> *) a. MonadTCEnv m => ModuleName -> m a -> m a
withCurrentModule ModuleName
m (TCM () -> TCM ()) -> TCM () -> TCM ()
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' <- TCMT IO Telescope
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope
          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.
      Impossible -> VerboseLevel -> TCM () -> TCM ()
forall (m :: * -> *) a.
MonadAddContext m =>
Impossible -> VerboseLevel -> m a -> m a
escapeContext Impossible
HasCallStack => Impossible
impossible VerboseLevel
npars (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
        QName
-> ConHead
-> Telescope
-> [Arg QName]
-> Telescope
-> Type
-> TCM ()
addCompositionForRecord QName
name ConHead
con Telescope
tel ((Dom QName -> Arg QName) -> [Dom QName] -> [Arg QName]
forall a b. (a -> b) -> [a] -> [b]
map Dom QName -> Arg QName
forall t a. Dom' t a -> Arg a
argFromDom [Dom QName]
fs) Telescope
ftel Type
rect

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

      () -> TCM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  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 = PatternOrCopattern
-> (Range -> PatternOrCopattern)
-> Maybe Range
-> PatternOrCopattern
forall b a. b -> (a -> b) -> Maybe a -> b
maybe PatternOrCopattern
CopatternMatching (PatternOrCopattern -> Range -> PatternOrCopattern
forall a b. a -> b -> a
const PatternOrCopattern
PatternMatching) Maybe Range
pat
  eta :: Maybe HasEta
eta      = (PatternOrCopattern
patCopat PatternOrCopattern -> HasEta0 -> HasEta
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$) (HasEta0 -> HasEta) -> Maybe HasEta0 -> Maybe HasEta
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 <- TCMT IO Telescope
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope
  TCM () -> TCM ()
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do

    -- Record has no fields: attach composition data to record constructor
    if [Arg QName] -> Bool
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 (Telescope -> Telescope -> Telescope
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
cxt Telescope
tel) [] Telescope
ftel Type
rect []
      (Signature -> Signature) -> TCM ()
forall (m :: * -> *).
MonadTCState m =>
(Signature -> Signature) -> m ()
modifySignature ((Signature -> Signature) -> TCM ())
-> (Signature -> Signature) -> TCM ()
forall a b. (a -> b) -> a -> b
$ QName -> (Definition -> Definition) -> Signature -> Signature
updateDefinition (ConHead -> QName
conName ConHead
con) ((Definition -> Definition) -> Signature -> Signature)
-> (Definition -> Definition) -> Signature -> Signature
forall a b. (a -> b) -> a -> b
$ (Defn -> Defn) -> Definition -> Definition
updateTheDef ((Defn -> Defn) -> Definition -> Definition)
-> (Defn -> Defn) -> Definition -> Definition
forall a b. (a -> b) -> a -> b
$ \case
        r :: Defn
r@Constructor{} -> Defn
r { conComp :: CompKit
conComp = CompKit
kit, conProj :: Maybe [QName]
conProj = [QName] -> Maybe [QName]
forall a. a -> Maybe a
Just [] }  -- no projections
        Defn
_ -> 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 <- TCMT IO Bool -> TCM CompKit -> TCM CompKit -> TCM CompKit
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (Bool -> TCMT IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return ((Arg QName -> Bool) -> [Arg QName] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Arg QName -> Bool
forall a. LensRelevance a => a -> Bool
isIrrelevant [Arg QName]
fs)
                  TCMT IO Bool -> TCMT IO Bool -> TCMT IO Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`and2M` do Bool -> Bool
not (Bool -> Bool) -> (PragmaOptions -> Bool) -> PragmaOptions -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> Bool
optIrrelevantProjections (PragmaOptions -> Bool) -> TCMT IO PragmaOptions -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions)
        {-then-} (CompKit -> TCM CompKit
forall (m :: * -> *) a. Monad m => a -> m a
return CompKit
emptyCompKit)
        {-else-} (QName
-> Telescope -> Telescope -> [Arg QName] -> Type -> TCM CompKit
defineCompKitR QName
name (Telescope -> Telescope -> Telescope
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
cxt Telescope
tel) Telescope
ftel [Arg QName]
fs Type
rect)
      (Signature -> Signature) -> TCM ()
forall (m :: * -> *).
MonadTCState m =>
(Signature -> Signature) -> m ()
modifySignature ((Signature -> Signature) -> TCM ())
-> (Signature -> Signature) -> TCM ()
forall a b. (a -> b) -> a -> b
$ QName -> (Definition -> Definition) -> Signature -> Signature
updateDefinition QName
name ((Definition -> Definition) -> Signature -> Signature)
-> (Definition -> Definition) -> Signature -> Signature
forall a b. (a -> b) -> a -> b
$ (Defn -> Defn) -> Definition -> Definition
updateTheDef ((Defn -> Defn) -> Definition -> Definition)
-> (Defn -> Defn) -> Definition -> Definition
forall a b. (a -> b) -> a -> b
$ \case
        r :: Defn
r@Record{} -> Defn
r { recComp :: CompKit
recComp = CompKit
kit }
        Defn
_          -> 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 <- (VerboseKey -> TCMT IO (Maybe Term))
-> [VerboseKey] -> TCMT IO [Maybe Term]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM VerboseKey -> TCMT IO (Maybe Term)
forall (m :: * -> *). HasBuiltins m => VerboseKey -> m (Maybe Term)
getTerm'
        [ VerboseKey
builtinInterval
        , VerboseKey
builtinIZero
        , VerboseKey
builtinIOne
        , VerboseKey
builtinIMin
        , VerboseKey
builtinIMax
        , VerboseKey
builtinINeg
        , VerboseKey
builtinPOr
        , VerboseKey
builtinItIsOne
        ]
  VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.rec.cxt" VerboseLevel
30 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ Telescope -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
params
  VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.rec.cxt" VerboseLevel
30 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ Telescope -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
fsT
  VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.rec.cxt" VerboseLevel
30 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ Type -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Type
rect
  if Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ (Maybe Term -> Bool) -> [Maybe Term] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Maybe Term -> Bool
forall a. Maybe a -> Bool
isJust [Maybe Term]
required then CompKit -> TCM CompKit
forall (m :: * -> *) a. Monad m => a -> m a
return (CompKit -> TCM CompKit) -> CompKit -> TCM CompKit
forall a b. (a -> b) -> a -> b
$ CompKit
emptyCompKit else do
    Maybe QName
transp <- [VerboseKey] -> TCMT IO (Maybe QName) -> TCMT IO (Maybe QName)
forall (m :: * -> *) (t :: * -> *) a.
(Traversable t, HasBuiltins m) =>
t VerboseKey -> m (Maybe a) -> m (Maybe a)
whenDefined [VerboseKey
builtinTrans]              (TranspOrHComp
-> QName
-> Telescope
-> Telescope
-> [Arg QName]
-> Type
-> TCMT IO (Maybe QName)
defineTranspOrHCompR TranspOrHComp
DoTransp QName
name Telescope
params Telescope
fsT [Arg QName]
fns Type
rect)
    Maybe QName
hcomp  <- [VerboseKey] -> TCMT IO (Maybe QName) -> TCMT IO (Maybe QName)
forall (m :: * -> *) (t :: * -> *) a.
(Traversable t, HasBuiltins m) =>
t VerboseKey -> m (Maybe a) -> m (Maybe a)
whenDefined [VerboseKey
builtinTrans,VerboseKey
builtinHComp] (TranspOrHComp
-> QName
-> Telescope
-> Telescope
-> [Arg QName]
-> Type
-> TCMT IO (Maybe QName)
defineTranspOrHCompR TranspOrHComp
DoHComp QName
name Telescope
params Telescope
fsT [Arg QName]
fns Type
rect)
    CompKit -> TCM CompKit
forall (m :: * -> *) a. Monad m => a -> m a
return (CompKit -> TCM CompKit) -> CompKit -> TCM CompKit
forall a b. (a -> b) -> a -> b
$ CompKit :: Maybe QName -> Maybe QName -> CompKit
CompKit
      { nameOfTransp :: Maybe QName
nameOfTransp = Maybe QName
transp
      , nameOfHComp :: Maybe QName
nameOfHComp  = Maybe QName
hcomp
      }
  where
    whenDefined :: t VerboseKey -> m (Maybe a) -> m (Maybe a)
whenDefined t VerboseKey
xs m (Maybe a)
m = do
      t (Maybe Term)
xs <- (VerboseKey -> m (Maybe Term))
-> t VerboseKey -> m (t (Maybe Term))
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM VerboseKey -> m (Maybe Term)
forall (m :: * -> *). HasBuiltins m => VerboseKey -> m (Maybe Term)
getTerm' t VerboseKey
xs
      if (Maybe Term -> Bool) -> t (Maybe Term) -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Maybe Term -> Bool
forall a. Maybe a -> Bool
isJust t (Maybe Term)
xs then m (Maybe a)
m else Maybe a -> m (Maybe a)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe a
forall a. Maybe a
Nothing


defineTranspOrHCompR ::
  TranspOrHComp
  -> QName       -- ^ some name, e.g. record name
  -> Telescope   -- ^ param types Δ
  -> Telescope   -- ^ fields' types Δ ⊢ Φ
  -> [Arg QName] -- ^ fields' names
  -> Type        -- ^ record type Δ ⊢ T
  -> TCM (Maybe QName)
defineTranspOrHCompR :: TranspOrHComp
-> QName
-> Telescope
-> Telescope
-> [Arg QName]
-> Type
-> TCMT IO (Maybe QName)
defineTranspOrHCompR TranspOrHComp
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 Term -> Elims -> Term
forall t. Apply t => t -> Elims -> t
`applyE` [ProjOrigin -> QName -> Elim' Term
forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
ProjSystem QName
fn])
  Maybe (QName, Telescope, Type, [Dom Type], [Term])
stuff <- (((QName, Telescope, Type, [Dom Type], [Term]), Substitution)
 -> (QName, Telescope, Type, [Dom Type], [Term]))
-> Maybe
     ((QName, Telescope, Type, [Dom Type], [Term]), Substitution)
-> Maybe (QName, Telescope, Type, [Dom Type], [Term])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((QName, Telescope, Type, [Dom Type], [Term]), Substitution)
-> (QName, Telescope, Type, [Dom Type], [Term])
forall a b. (a, b) -> a
fst (Maybe ((QName, Telescope, Type, [Dom Type], [Term]), Substitution)
 -> Maybe (QName, Telescope, Type, [Dom Type], [Term]))
-> TCMT
     IO
     (Maybe
        ((QName, Telescope, Type, [Dom Type], [Term]), Substitution))
-> TCMT IO (Maybe (QName, Telescope, Type, [Dom Type], [Term]))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TranspOrHComp
-> Maybe Term
-> (Term -> QName -> Term)
-> QName
-> Telescope
-> Telescope
-> [Arg QName]
-> Type
-> TCMT
     IO
     (Maybe
        ((QName, Telescope, Type, [Dom Type], [Term]), Substitution))
defineTranspOrHCompForFields TranspOrHComp
cmd Maybe Term
forall a. Maybe a
Nothing Term -> QName -> Term
project QName
name Telescope
params Telescope
fsT [Arg QName]
fns Type
rect

  Maybe (QName, Telescope, Type, [Dom Type], [Term])
-> TCMT IO (Maybe QName)
-> ((QName, Telescope, Type, [Dom Type], [Term])
    -> TCMT IO (Maybe QName))
-> TCMT IO (Maybe QName)
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe (QName, Telescope, Type, [Dom Type], [Term])
stuff (Maybe QName -> TCMT IO (Maybe QName)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe QName
forall a. Maybe a
Nothing) (((QName, Telescope, Type, [Dom Type], [Term])
  -> TCMT IO (Maybe QName))
 -> TCMT IO (Maybe QName))
-> ((QName, Telescope, Type, [Dom Type], [Term])
    -> TCMT IO (Maybe QName))
-> TCMT IO (Maybe QName)
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 <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIOne
           Just QName
io_name <- VerboseKey -> TCMT IO (Maybe QName)
forall (m :: * -> *).
HasBuiltins m =>
VerboseKey -> m (Maybe QName)
getBuiltinName' VerboseKey
builtinIOne
           Term
one <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primItIsOne
           Type
tInterval <- TCMT IO Type
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Type
primIntervalType
           let
              (VerboseLevel
ix,Term
rhs) =
                case TranspOrHComp
cmd of
                  -- TranspRArgs = phi : I, a0 : ..
                  -- Γ = Δ^I , CompRArgs
                  -- pats = ... | phi = i1
                  -- body = a0
                  TranspOrHComp
DoTransp -> (VerboseLevel
1,VerboseLevel -> Elims -> Term
Var VerboseLevel
0 [])
                  -- HCompRArgs = phi : I, u : .., a0 : ..
                  -- Γ = Δ, CompRArgs
                  -- pats = ... | phi = i1
                  -- body = u i1 itIsOne
                  TranspOrHComp
DoHComp  -> (VerboseLevel
2,VerboseLevel -> Elims -> Term
Var VerboseLevel
1 [] Term -> [Arg Term] -> Term
forall t. Apply t => t -> [Arg Term] -> t
`apply` [Term -> Arg Term
forall e. e -> Arg e
argN Term
io, Relevance -> Arg Term -> Arg Term
forall a. LensRelevance a => Relevance -> a -> a
setRelevance Relevance
Irrelevant (Arg Term -> Arg Term) -> Arg Term -> Arg Term
forall a b. (a -> b) -> a -> b
$ Term -> Arg Term
forall e. e -> Arg e
argN Term
one])

              p :: Pattern' DBPatVar
p = ConHead
-> ConPatternInfo
-> [NamedArg (Pattern' DBPatVar)]
-> Pattern' DBPatVar
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 = Arg Type -> Maybe (Arg Type)
forall a. a -> Maybe a
Just (ArgInfo -> Type -> Arg Type
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
defaultArgInfo Type
tInterval)
                                         , conPFallThrough :: Bool
conPFallThrough = Bool
True })
                         []

              -- gamma, rtype

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

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

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

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

              c :: Clause
c = Clause :: Range
-> Range
-> Telescope
-> [NamedArg (Pattern' DBPatVar)]
-> Maybe Term
-> Maybe (Arg Type)
-> Bool
-> Maybe Bool
-> Maybe Bool
-> Maybe Bool
-> ExpandedEllipsis
-> Clause
Clause { clauseTel :: Telescope
clauseTel       = Telescope
gamma'
                         , clauseType :: Maybe (Arg Type)
clauseType      = Arg Type -> Maybe (Arg Type)
forall a. a -> Maybe a
Just (Arg Type -> Maybe (Arg Type)) -> Arg Type -> Maybe (Arg Type)
forall a b. (a -> b) -> a -> b
$ Type -> Arg Type
forall e. e -> Arg e
argN Type
t
                         , namedClausePats :: [NamedArg (Pattern' DBPatVar)]
namedClausePats = [NamedArg (Pattern' DBPatVar)]
pats
                         , clauseFullRange :: Range
clauseFullRange = Range
forall a. Range' a
noRange
                         , clauseLHSRange :: Range
clauseLHSRange  = Range
forall a. Range' a
noRange
                         , clauseCatchall :: Bool
clauseCatchall  = Bool
False
                         , clauseBody :: Maybe Term
clauseBody      = Term -> Maybe Term
forall a. a -> Maybe a
Just (Term -> Maybe Term) -> Term -> Maybe Term
forall a b. (a -> b) -> a -> b
$ Term
rhs
                         , clauseExact :: Maybe Bool
clauseExact       = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True
                         , clauseRecursive :: Maybe Bool
clauseRecursive   = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False  -- definitely non-recursive!
                         , clauseUnreachable :: Maybe Bool
clauseUnreachable = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False
                         , clauseEllipsis :: ExpandedEllipsis
clauseEllipsis  = ExpandedEllipsis
NoEllipsis
                         }
           VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"trans.rec.face" VerboseLevel
17 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey -> TCM Doc
forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
text (VerboseKey -> TCM Doc) -> VerboseKey -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Clause -> VerboseKey
forall a. Show a => a -> VerboseKey
show Clause
c
           Clause -> TCMT IO Clause
forall (m :: * -> *) a. Monad m => a -> m a
return Clause
c
  [Clause]
cs <- [(Arg QName, Dom Type, Term)]
-> ((Arg QName, Dom Type, Term) -> TCMT IO Clause)
-> TCMT IO [Clause]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM ([Arg QName]
-> [Dom Type] -> [Term] -> [(Arg QName, Dom Type, Term)]
forall a b c. [a] -> [b] -> [c] -> [(a, b, c)]
zip3 [Arg QName]
fns [Dom Type]
clause_types [Term]
bodies) (((Arg QName, Dom Type, Term) -> TCMT IO Clause)
 -> TCMT IO [Clause])
-> ((Arg QName, Dom Type, Term) -> TCMT IO Clause)
-> TCMT IO [Clause]
forall a b. (a -> b) -> a -> b
$ \ (Arg QName
fname, Dom Type
clause_ty, Term
body) -> do
          let
              pats :: [NamedArg (Pattern' DBPatVar)]
pats = Telescope -> [NamedArg (Pattern' DBPatVar)]
forall a. DeBruijn a => Telescope -> [NamedArg a]
teleNamedArgs Telescope
gamma [NamedArg (Pattern' DBPatVar)]
-> [NamedArg (Pattern' DBPatVar)] -> [NamedArg (Pattern' DBPatVar)]
forall a. [a] -> [a] -> [a]
++ [Pattern' DBPatVar -> NamedArg (Pattern' DBPatVar)
forall a. a -> NamedArg a
defaultNamedArg (Pattern' DBPatVar -> NamedArg (Pattern' DBPatVar))
-> Pattern' DBPatVar -> NamedArg (Pattern' DBPatVar)
forall a b. (a -> b) -> a -> b
$ ProjOrigin -> QName -> Pattern' DBPatVar
forall x. ProjOrigin -> QName -> Pattern' x
ProjP ProjOrigin
ProjSystem (QName -> Pattern' DBPatVar) -> QName -> Pattern' DBPatVar
forall a b. (a -> b) -> a -> b
$ Arg QName -> QName
forall e. Arg e -> e
unArg Arg QName
fname]
              c :: Clause
c = Clause :: Range
-> Range
-> Telescope
-> [NamedArg (Pattern' DBPatVar)]
-> Maybe Term
-> Maybe (Arg Type)
-> Bool
-> Maybe Bool
-> Maybe Bool
-> Maybe Bool
-> ExpandedEllipsis
-> Clause
Clause { clauseTel :: Telescope
clauseTel       = Telescope
gamma
                         , clauseType :: Maybe (Arg Type)
clauseType      = Arg Type -> Maybe (Arg Type)
forall a. a -> Maybe a
Just (Arg Type -> Maybe (Arg Type)) -> Arg Type -> Maybe (Arg Type)
forall a b. (a -> b) -> a -> b
$ Type -> Arg Type
forall e. e -> Arg e
argN (Dom Type -> Type
forall t e. Dom' t e -> e
unDom Dom Type
clause_ty)
                         , namedClausePats :: [NamedArg (Pattern' DBPatVar)]
namedClausePats = [NamedArg (Pattern' DBPatVar)]
pats
                         , clauseFullRange :: Range
clauseFullRange = Range
forall a. Range' a
noRange
                         , clauseLHSRange :: Range
clauseLHSRange  = Range
forall a. Range' a
noRange
                         , clauseCatchall :: Bool
clauseCatchall  = Bool
False
                         , clauseBody :: Maybe Term
clauseBody      = Term -> Maybe Term
forall a. a -> Maybe a
Just Term
body
                         , clauseExact :: Maybe Bool
clauseExact       = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True
                         , clauseRecursive :: Maybe Bool
clauseRecursive   = Maybe Bool
forall a. Maybe a
Nothing
                             -- Andreas 2020-02-06 TODO
                             -- Or: Just False;  is it known to be non-recursive?
                         , clauseUnreachable :: Maybe Bool
clauseUnreachable = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False
                         , clauseEllipsis :: ExpandedEllipsis
clauseEllipsis  = ExpandedEllipsis
NoEllipsis
                         }
          VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"trans.rec" VerboseLevel
17 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey -> TCM Doc
forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
text (VerboseKey -> TCM Doc) -> VerboseKey -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Clause -> VerboseKey
forall a. Show a => a -> VerboseKey
show Clause
c
          VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"trans.rec" VerboseLevel
16 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey -> TCM Doc
forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
text VerboseKey
"type =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> VerboseKey -> TCM Doc
forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
text (Maybe (Arg Type) -> VerboseKey
forall a. Show a => a -> VerboseKey
show (Clause -> Maybe (Arg Type)
clauseType Clause
c))
          VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"trans.rec" VerboseLevel
15 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Type -> TCM Doc) -> Type -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Telescope -> Type -> Type
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
gamma (Dom Type -> Type
forall t e. Dom' t e -> e
unDom Dom Type
clause_ty)
          VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"trans.rec" VerboseLevel
10 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey -> TCM Doc
forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
text VerboseKey
"body =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Telescope -> Term -> Term
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
gamma Term
body)
          Clause -> TCMT IO Clause
forall (m :: * -> *) a. Monad m => a -> m a
return Clause
c
  QName -> [Clause] -> TCM ()
addClauses QName
theName ([Clause] -> TCM ()) -> [Clause] -> TCM ()
forall a b. (a -> b) -> a -> b
$ Clause
c' Clause -> [Clause] -> [Clause]
forall a. a -> [a] -> [a]
: [Clause]
cs
  VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"trans.rec" VerboseLevel
15 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey -> TCM Doc
forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
text (VerboseKey -> TCM Doc) -> VerboseKey -> TCM Doc
forall a b. (a -> b) -> a -> b
$ VerboseKey
"compiling clauses for " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ QName -> VerboseKey
forall a. Show a => a -> VerboseKey
show QName
theName
  (Maybe SplitTree
mst, Bool
_, CompiledClauses
cc) <- TCMT IO (Maybe SplitTree, Bool, CompiledClauses)
-> TCMT IO (Maybe SplitTree, Bool, CompiledClauses)
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (Maybe (QName, Type)
-> [Clause] -> TCMT IO (Maybe SplitTree, Bool, CompiledClauses)
compileClauses Maybe (QName, Type)
forall a. Maybe a
Nothing [Clause]
cs)
  Maybe SplitTree -> (SplitTree -> TCM ()) -> TCM ()
forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
whenJust Maybe SplitTree
mst ((SplitTree -> TCM ()) -> TCM ())
-> (SplitTree -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ QName -> SplitTree -> TCM ()
setSplitTree QName
theName
  QName -> CompiledClauses -> TCM ()
setCompiledClauses QName
theName CompiledClauses
cc
  VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"trans.rec" VerboseLevel
15 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey -> TCM Doc
forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
text (VerboseKey -> TCM Doc) -> VerboseKey -> TCM Doc
forall a b. (a -> b) -> a -> b
$ VerboseKey
"compiled"
  Maybe QName -> TCMT IO (Maybe QName)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe QName -> TCMT IO (Maybe QName))
-> Maybe QName -> TCMT IO (Maybe QName)
forall a b. (a -> b) -> a -> b
$ QName -> Maybe QName
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 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 Telescope
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]
_ [] = () -> TCM ()
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 TCM () -> TCM () -> TCM ()
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' [Field] -> [Field] -> [Field]
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) =
      Call -> TCM () -> TCM ()
forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
traceCall (Range -> QName -> Type -> Call
CheckProjection (DefInfo -> Range
forall a. HasRange a => a -> Range
getRange DefInfo
info) QName
x Type
t) (TCM () -> TCM ()) -> TCM () -> TCM ()
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.
      VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.rec.proj" VerboseLevel
5 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
        [ TCM Doc
"checking projection" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
x
        , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
          [ TCM Doc
"top   =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (TCM Doc -> TCM Doc
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (TCM Doc -> TCM Doc)
-> (Telescope -> TCM Doc) -> Telescope -> TCM Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Telescope -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Telescope -> TCM Doc) -> TCMT IO Telescope -> TCM Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO Telescope
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope)
          , TCM Doc
"tel   =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (TCM Doc -> TCM Doc
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (TCM Doc -> TCM Doc)
-> (Telescope -> TCM Doc) -> Telescope -> TCM Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Telescope -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Telescope -> TCM Doc) -> Telescope -> TCM Doc
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...
      VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.rec.proj" VerboseLevel
5 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
          [ TCM Doc
"ftel1 =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Impossible -> VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *) a.
MonadAddContext m =>
Impossible -> VerboseLevel -> m a -> m a
escapeContext Impossible
HasCallStack => Impossible
impossible VerboseLevel
1 (Telescope -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
ftel1)
          , TCM Doc
"t     =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Impossible -> VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *) a.
MonadAddContext m =>
Impossible -> VerboseLevel -> m a -> m a
escapeContext Impossible
HasCallStack => Impossible
impossible VerboseLevel
1 (Telescope -> TCM Doc -> TCM Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
ftel1 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t)
          , TCM Doc
"ftel2 =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Impossible -> VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *) a.
MonadAddContext m =>
Impossible -> VerboseLevel -> m a -> m a
escapeContext Impossible
HasCallStack => Impossible
impossible VerboseLevel
1 (Telescope -> TCM Doc -> TCM Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
ftel1 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Dom Type -> Abs Telescope -> (Telescope -> TCM Doc) -> TCM Doc
forall a (m :: * -> *) b.
(Subst a, MonadAddContext m) =>
Dom Type -> Abs a -> (a -> m b) -> m b
underAbstraction Dom Type
dom Abs Telescope
ftel2 Telescope -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM)
          ]
      VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.rec.proj" VerboseLevel
55 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
          [ TCM Doc
"ftel1 (raw) =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Telescope -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Telescope
ftel1
          , TCM Doc
"t     (raw) =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Type
t
          , TCM Doc
"ftel2 (raw) =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Abs Telescope -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Abs Telescope
ftel2
          ]
      VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.rec.proj" VerboseLevel
5 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
          [ TCM Doc
"vs    =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ ((Term -> TCM Doc) -> [Term] -> [TCM Doc]
forall a b. (a -> b) -> [a] -> [b]
map Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [Term]
vs)
          , TCM Doc
"abstr =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (VerboseKey -> TCM Doc
forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
text (VerboseKey -> TCM Doc)
-> (IsAbstract -> VerboseKey) -> IsAbstract -> TCM Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IsAbstract -> VerboseKey
forall a. Show a => a -> VerboseKey
show) (DefInfo -> IsAbstract
forall t. DefInfo' t -> IsAbstract
Info.defAbstract DefInfo
info)
          , TCM Doc
"quant =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (VerboseKey -> TCM Doc
forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
text (VerboseKey -> TCM Doc)
-> (Quantity -> VerboseKey) -> Quantity -> TCM Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Quantity -> VerboseKey
forall a. Show a => a -> VerboseKey
show) (ArgInfo -> Quantity
forall a. LensQuantity a => a -> Quantity
getQuantity ArgInfo
ai)
          , TCM Doc
"coh   =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (VerboseKey -> TCM Doc
forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
text (VerboseKey -> TCM Doc)
-> (Cohesion -> VerboseKey) -> Cohesion -> TCM Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Cohesion -> VerboseKey
forall a. Show a => a -> VerboseKey
show) (ArgInfo -> Cohesion
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 UnderComposition Cohesion -> Bool
forall a. LeftClosedPOMonoid a => a -> Bool
hasLeftAdjoint (Cohesion -> UnderComposition Cohesion
forall t. t -> UnderComposition t
UnderComposition (ArgInfo -> Cohesion
forall a. LensCohesion a => a -> Cohesion
getCohesion ArgInfo
ai))
        then Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (ArgInfo -> Cohesion
forall a. LensCohesion a => a -> Cohesion
getCohesion ArgInfo
ai Cohesion -> Cohesion -> Bool
forall a. Eq a => a -> a -> Bool
== Cohesion
Continuous)
                    -- Andrea TODO: properly update the context/type of the projection when we add Sharp
                    TCM ()
forall a. HasCallStack => a
__IMPOSSIBLE__
        else VerboseKey -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
VerboseKey -> m a
genericError (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey
"Cannot have record fields with modality " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ Cohesion -> VerboseKey
forall a. Show a => a -> VerboseKey
show (ArgInfo -> Cohesion
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'       = VerboseLevel -> VerboseLevel -> Type -> Type
forall a. Subst a => VerboseLevel -> VerboseLevel -> a -> a
raiseFrom (Telescope -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size Telescope
ftel1) VerboseLevel
1 Type
t
          t'' :: Type
t''      = Substitution' (SubstArg Type) -> Type -> Type
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst ([Term] -> Substitution
forall a. DeBruijn a => [a] -> Substitution' a
parallelS [Term]
vs) Type
t'
          finalt :: Type
finalt   = Telescope -> Type -> Type
telePi (VerboseKey -> Telescope -> Telescope
forall a. VerboseKey -> Tele a -> Tele a
replaceEmptyName VerboseKey
"r" Telescope
tel) Type
t''
          projname :: QName
projname = ModuleName -> Name -> QName
qualify ModuleName
m (Name -> QName) -> Name -> QName
forall a b. (a -> b) -> a -> b
$ QName -> Name
qnameName QName
x
          projcall :: ProjOrigin -> Term
projcall ProjOrigin
o = VerboseLevel -> Elims -> Term
Var VerboseLevel
0 [ProjOrigin -> QName -> Elim' Term
forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
o QName
projname]
          rel :: Relevance
rel      = ArgInfo -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance ArgInfo
ai
          -- the recursive call
          recurse :: TCM ()
recurse  = Telescope -> Telescope -> [Term] -> [Field] -> TCM ()
checkProjs (Telescope -> Telescope -> Telescope
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
ftel1 (Telescope -> Telescope) -> Telescope -> Telescope
forall a b. (a -> b) -> a -> b
$ Dom Type -> Abs Telescope -> Telescope
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel Dom Type
dom
                                 (Abs Telescope -> Telescope) -> Abs Telescope -> Telescope
forall a b. (a -> b) -> a -> b
$ VerboseKey -> Telescope -> Abs Telescope
forall a. VerboseKey -> a -> Abs a
Abs (Name -> VerboseKey
nameToArgName (Name -> VerboseKey) -> Name -> VerboseKey
forall a b. (a -> b) -> a -> b
$ QName -> Name
qnameName QName
projname) Telescope
forall a. Tele a
EmptyTel)
                                (Abs Telescope -> Telescope
forall a. Subst a => Abs a -> a
absBody Abs Telescope
ftel2) (ProjOrigin -> Term
projcall ProjOrigin
ProjSystem Term -> [Term] -> [Term]
forall a. a -> [a] -> [a]
: [Term]
vs) [Field]
fs

      VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.rec.proj" VerboseLevel
25 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"finalt=" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do
        TCM Doc -> TCM Doc
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Type -> TCM Doc
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
        VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.rec.proj" VerboseLevel
10 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
          [ TCM Doc
"adding projection"
          , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ QName -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
projname TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
":" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc -> TCM Doc
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (Type -> TCM Doc
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   -> Term -> Term
forall a. a -> a
id
              Relevance
NonStrict  -> Term -> Term
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' Term (VerboseKey, Type)]
telList = Telescope -> [Dom' Term (VerboseKey, Type)]
forall t. Tele (Dom t) -> [Dom (VerboseKey, t)]
telToList Telescope
tel
            ([Dom' Term (VerboseKey, Type)]
ptelList,[Dom' Term (VerboseKey, Type)
rt]) = VerboseLevel
-> [Dom' Term (VerboseKey, Type)]
-> ([Dom' Term (VerboseKey, Type)], [Dom' Term (VerboseKey, Type)])
forall a. VerboseLevel -> [a] -> ([a], [a])
splitAt (Telescope -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size Telescope
tel VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
- VerboseLevel
1) [Dom' Term (VerboseKey, Type)]
telList
            ptel :: Telescope
ptel   = [Dom' Term (VerboseKey, Type)] -> Telescope
telFromList [Dom' Term (VerboseKey, Type)]
ptelList
            cpo :: PatOrigin
cpo    = if Bool
hasNamedCon then PatOrigin
PatOCon else PatOrigin
PatORec
            cpi :: ConPatternInfo
cpi    = ConPatternInfo :: PatternInfo
-> Bool -> Bool -> Maybe (Arg Type) -> Bool -> ConPatternInfo
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   = Arg Type -> Maybe (Arg Type)
forall a. a -> Maybe a
Just (Arg Type -> Maybe (Arg Type)) -> Arg Type -> Maybe (Arg Type)
forall a b. (a -> b) -> a -> b
$ Dom Type -> Arg Type
forall t a. Dom' t a -> Arg a
argFromDom (Dom Type -> Arg Type) -> Dom Type -> Arg Type
forall a b. (a -> b) -> a -> b
$ ((VerboseKey, Type) -> Type)
-> Dom' Term (VerboseKey, Type) -> Dom Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (VerboseKey, Type) -> Type
forall a b. (a, b) -> b
snd Dom' Term (VerboseKey, Type)
rt
                                    , conPLazy :: Bool
conPLazy   = Bool
True }
            conp :: NamedArg (Pattern' DBPatVar)
conp   = Pattern' DBPatVar -> NamedArg (Pattern' DBPatVar)
forall a. a -> NamedArg a
defaultNamedArg (Pattern' DBPatVar -> NamedArg (Pattern' DBPatVar))
-> Pattern' DBPatVar -> NamedArg (Pattern' DBPatVar)
forall a b. (a -> b) -> a -> b
$ ConHead
-> ConPatternInfo
-> [NamedArg (Pattern' DBPatVar)]
-> Pattern' DBPatVar
forall x.
ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
ConP ConHead
con ConPatternInfo
cpi ([NamedArg (Pattern' DBPatVar)] -> Pattern' DBPatVar)
-> [NamedArg (Pattern' DBPatVar)] -> Pattern' DBPatVar
forall a b. (a -> b) -> a -> b
$ Telescope -> [NamedArg (Pattern' DBPatVar)]
forall a. DeBruijn a => Telescope -> [NamedArg a]
teleNamedArgs Telescope
ftel
            body :: Maybe Term
body   = Term -> Maybe Term
forall a. a -> Maybe a
Just (Term -> Maybe Term) -> Term -> Maybe Term
forall a b. (a -> b) -> a -> b
$ Term -> Term
bodyMod (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ VerboseLevel -> Term
var (Abs Telescope -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size Abs Telescope
ftel2)
            cltel :: Telescope
cltel  = Telescope
ptel Telescope -> Telescope -> Telescope
forall t. Abstract t => Telescope -> t -> t
`abstract` Telescope
ftel
            cltype :: Maybe (Arg Type)
cltype = Arg Type -> Maybe (Arg Type)
forall a. a -> Maybe a
Just (Arg Type -> Maybe (Arg Type)) -> Arg Type -> Maybe (Arg Type)
forall a b. (a -> b) -> a -> b
$ ArgInfo -> Type -> Arg Type
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai (Type -> Arg Type) -> Type -> Arg Type
forall a b. (a -> b) -> a -> b
$ VerboseLevel -> Type -> Type
forall a. Subst a => VerboseLevel -> a -> a
raise (VerboseLevel
1 VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
+ Abs Telescope -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size Abs Telescope
ftel2) Type
t
            clause :: Clause
clause = Clause :: Range
-> Range
-> Telescope
-> [NamedArg (Pattern' DBPatVar)]
-> Maybe Term
-> Maybe (Arg Type)
-> Bool
-> Maybe Bool
-> Maybe Bool
-> Maybe Bool
-> ExpandedEllipsis
-> Clause
Clause { clauseLHSRange :: Range
clauseLHSRange  = DefInfo -> Range
forall a. HasRange a => a -> Range
getRange DefInfo
info
                            , clauseFullRange :: Range
clauseFullRange = DefInfo -> Range
forall a. HasRange a => a -> Range
getRange DefInfo
info
                            , clauseTel :: Telescope
clauseTel       = Telescope -> Telescope
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       = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True
                            , clauseRecursive :: Maybe Bool
clauseRecursive   = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False
                            , clauseUnreachable :: Maybe Bool
clauseUnreachable = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False
                            , clauseEllipsis :: ExpandedEllipsis
clauseEllipsis  = ExpandedEllipsis
NoEllipsis
                            }

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

        VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.rec.proj" VerboseLevel
70 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
          [ TCM Doc
"adding projection"
          , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ QName -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
projname TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Clause -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Clause
clause
          ]
        VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.rec.proj" VerboseLevel
10 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
          [ TCM Doc
"adding projection"
          , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ QNamed Clause -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (QName -> Clause -> QNamed Clause
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] -> TCMT IO (Maybe SplitTree, Bool, CompiledClauses)
compileClauses Maybe (QName, Type)
forall a. Maybe a
Nothing [Clause
clause]

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

        Impossible -> VerboseLevel -> TCM () -> TCM ()
forall (m :: * -> *) a.
MonadAddContext m =>
Impossible -> VerboseLevel -> m a -> m a
escapeContext Impossible
HasCallStack => Impossible
impossible (Telescope -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size Telescope
tel) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
          Language
lang <- TCMT IO Language
forall (m :: * -> *). HasOptions m => m Language
getLanguage
          QName -> Definition -> TCM ()
addConstant QName
projname (Definition -> TCM ()) -> Definition -> TCM ()
forall a b. (a -> b) -> a -> b
$
            (ArgInfo -> QName -> Type -> Language -> Defn -> Definition
defaultDefn ArgInfo
ai QName
projname (Type -> Type
forall a. KillRange a => KillRangeT a
killRange Type
finalt) Language
lang
              Defn
emptyFunction
                { funClauses :: [Clause]
funClauses        = [Clause
clause]
                , funCompiled :: Maybe CompiledClauses
funCompiled       = CompiledClauses -> Maybe CompiledClauses
forall a. a -> Maybe a
Just CompiledClauses
cc
                , funSplitTree :: Maybe SplitTree
funSplitTree      = Maybe SplitTree
mst
                , funProjection :: Maybe Projection
funProjection     = Projection -> Maybe Projection
forall a. a -> Maybe a
Just Projection
projection
                , funMutual :: Maybe [QName]
funMutual         = [QName] -> Maybe [QName]
forall a. a -> Maybe a
Just []  -- Projections are not mutually recursive with anything
                , funTerminates :: Maybe Bool
funTerminates     = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True
                })
              { defArgOccurrences :: [Occurrence]
defArgOccurrences = [Occurrence
StrictPos]
              , defCopatternLHS :: Bool
defCopatternLHS   = CompiledClauses -> Bool
hasProjectionPatterns CompiledClauses
cc
              }
          [QName] -> TCM ()
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 DefInfo -> IsInstance
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 -> () -> TCM ()
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